proposition: Theorem F3 : Tautology (normalize.N (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 2))) (V (P_of_succ_nat 1))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 9))) (V (P_of_succ_nat 3))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 7))) (V (P_of_succ_nat 10))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 5))) (V (P_of_succ_nat 8))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 1))) (V (P_of_succ_nat 4))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 6))) (V (P_of_succ_nat 2))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 11))) (normalize.N (V (P_of_succ_nat 3)))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 4))) (V (P_of_succ_nat 5))) (Node ANd (Node Or (V (P_of_succ_nat 6)) (V (P_of_succ_nat 7))) (Node ANd (Node Or (normalize.N (V (P_of_succ_nat 8))) (V (P_of_succ_nat 9))) (Node ANd (normalize.N (V (P_of_succ_nat 10))) (V (P_of_succ_nat 11)))))))))))))).
proof: Proof. apply (runC 0); exact (refl_equal true). Qed.
imports: Coq(ZArith)