============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13585 was started by mccune on cleo.thornwood, Mon Jun 19 16:43:06 2006 The command was "/home/mccune/bin/prover9 -f oml-4basis.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file oml-4basis.in assign(new_constants,1). clauses(sos). x v (y v z) = y v (x v z) # label(AJ). x v (x ^ y) = x # label(B1). x ^ y = c(c(x) v c(y)) # label(DM). x v (c(x) ^ (x v y)) = x v y # label(OM). end_of_list. clauses(goals). c(c(x)) = x # answer(CC). x v c(x) = y v c(y) # answer(ONE). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c(c(c1)) != c1 # answer(CC). c3 v c(c3) != c2 v c(c2) # answer(ONE). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v (y v z) = y v (x v z) # label(AJ). [input]. 2 x v (x ^ y) = x # label(B1). [input]. 3 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 4 x v (c(x) ^ (x v y)) = x v y # label(OM). [input]. 5 c(c(c1)) != c1 # answer(CC). [clausify]. 6 c3 v c(c3) != c2 v c(c2) # answer(ONE). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 2). % (Horn set with more than one neg. clause) % assign(max_proofs, 2) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 5 c(c(c1)) != c1 # answer(CC). [clausify]. 6 c3 v c(c3) != c2 v c(c2) # answer(ONE). [clausify]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, v, ^, c ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, v, ^, c ]). Unfolding symbols: ^/2. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: no changes. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 7 x v (y v z) = y v (x v z) # label(AJ). [input]. 9 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 10 x v c(c(c(x)) v c(x v y)) = x v y # label(OM). [copy(4),demod(9(3))]. 11 x v c(c(x) v c(y)) = x. [back_demod(8),demod(9(1))]. end_of_list. clauses(demodulators). 7 x v (y v z) = y v (x v z) # label(AJ). [input]. % (lex-dep) 9 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 10 x v c(c(c(x)) v c(x v y)) = x v y # label(OM). [copy(4),demod(9(3))]. 11 x v c(c(x) v c(y)) = x. [back_demod(8),demod(9(1))]. end_of_list. clauses(denials). 12 c(c(c1)) != c1 # answer(CC). [clausify]. 13 c3 v c(c3) != c2 v c(c2) # answer(ONE). [clausify]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 7 x v (y v z) = y v (x v z) # label(AJ). [input]. given #2 (I,wt=10): 9 x ^ y = c(c(x) v c(y)) # label(DM). [input]. given #3 (I,wt=15): 10 x v c(c(c(x)) v c(x v y)) = x v y # label(OM). [copy(4),demod(9(3))]. given #4 (I,wt=10): 11 x v c(c(x) v c(y)) = x. [back_demod(8),demod(9(1))]. given #5 (T,wt=7): 20 x v c(c(x)) = x. [para(11(a,1),11(a,1,2,1))]. given #6 (A,wt=15): 14 x v (y v (z v u)) = z v (x v (y v u)). [para(7(a,1),7(a,1,2))]. given #7 (F,wt=9): 19 x v c(c(x) v y) = x. [para(10(a,1),11(a,1,2,1))]. given #8 (F,wt=11): 18 x v c(c(c(x)) v c(x)) = x. [para(11(a,1),10(a,1,2,1,2,1)),demod(11(11))]. given #9 (T,wt=11): 21 x v (y v c(c(x))) = y v x. [para(20(a,1),7(a,1,2)),flip(a)]. given #10 (T,wt=9): 45 x v c(y v c(x)) = x. [para(21(a,1),19(a,1,2,1))]. given #11 (A,wt=19): 15 x v (y v c(c(c(x)) v c(x v z))) = y v (x v z). [para(10(a,1),7(a,1,2)),flip(a)]. given #12 (F,wt=8): 48 c(x) v c(x) = c(x). [para(20(a,1),45(a,1,2,1))]. given #13 (F,wt=7): 62 c(c(x)) v x = x. [para(48(a,1),21(a,1,2)),demod(20(3)),flip(a)]. given #14 (T,wt=9): 72 c(c(c(c(x)))) v x = x. [para(62(a,1),21(a,1,2)),demod(20(3)),flip(a)]. given #15 (T,wt=7): 83 c(c(c(x))) = c(x). [para(72(a,1),19(a,1,2,1)),demod(62(5)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: CC. % Length of proof is 21. % Level of proof is 12. % Maximum clause weight is 19. % Given clauses 15. 2 x v (x ^ y) = x # label(B1). [input]. 4 x v (c(x) ^ (x v y)) = x v y # label(OM). [input]. 7 x v (y v z) = y v (x v z) # label(AJ). [input]. 8 x v (x ^ y) = x # label(B1). [copy(2)]. 9 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 10 x v c(c(c(x)) v c(x v y)) = x v y # label(OM). [copy(4),demod(9(3))]. 11 x v c(c(x) v c(y)) = x. [back_demod(8),demod(9(1))]. 12 c(c(c1)) != c1 # answer(CC). [clausify]. 19 x v c(c(x) v y) = x. [para(10(a,1),11(a,1,2,1))]. 20 x v c(c(x)) = x. [para(11(a,1),11(a,1,2,1))]. 21 x v (y v c(c(x))) = y v x. [para(20(a,1),7(a,1,2)),flip(a)]. 45 x v c(y v c(x)) = x. [para(21(a,1),19(a,1,2,1))]. 48 c(x) v c(x) = c(x). [para(20(a,1),45(a,1,2,1))]. 62 c(c(x)) v x = x. [para(48(a,1),21(a,1,2)),demod(20(3)),flip(a)]. 72 c(c(c(c(x)))) v x = x. [para(62(a,1),21(a,1,2)),demod(20(3)),flip(a)]. 77 c(c(c(c(x)))) v c(c(c(c(c(c(c(x)))))) v c(x)) = x. [para(72(a,1),10(a,1,2,1,2,1)),demod(72(19))]. 83 c(c(c(x))) = c(x). [para(72(a,1),19(a,1,2,1)),demod(62(5)),flip(a)]. 85 c(c(x)) v c(c(c(x)) v c(x)) = x. [back_demod(77),demod(83(3),83(5),83(5))]. 89 c(c(x)) v c(y v c(x)) = c(c(x)). [para(83(a,1),45(a,1,2,1,2))]. 92 c(c(x)) = x. [back_demod(85),demod(89(8))]. 93 $F # answer(CC). [resolve(92,a,12,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 12. given #16 (A,wt=19): 22 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(14(a,1),7(a,1,2))]. given #17 (F,wt=5): 92 c(c(x)) = x. [back_demod(85),demod(89(8))]. given #18 (F,wt=5): 102 x v x = x. [back_demod(62),demod(92(2))]. given #19 (T,wt=9): 99 x v (x v y) = x v y. [back_demod(65),demod(92(3),59(3))]. given #20 (T,wt=9): 100 x v (y v x) = y v x. [back_demod(64),demod(92(2))]. given #21 (A,wt=15): 23 x v (y v (z v u)) = z v (y v (x v u)). [para(14(a,1),7(a,1))]. given #22 (F,wt=9): 152 c(c(x) v y) v x = x. [para(19(a,1),100(a,1,2)),demod(19(8))]. given #23 (F,wt=9): 153 c(x v c(y)) v y = y. [para(45(a,1),100(a,1,2)),demod(45(8))]. given #24 (T,wt=10): 142 c(x) v c(x v y) = c(x). [para(92(a,1),19(a,1,2,1,1))]. given #25 (T,wt=9): 201 (x v y) v x = x v y. [para(142(a,1),45(a,1,2,1)),demod(92(3))]. given #26 (A,wt=19): 24 x v (y v (z v (u v v))) = u v (x v (y v (z v v))). [para(14(a,2),7(a,1,2))]. given #27 (F,wt=9): 219 (x v y) v y = x v y. [para(100(a,1),201(a,1,1)),demod(100(4))]. given #28 (F,wt=10): 143 c(x) v c(y v x) = c(x). [para(92(a,1),45(a,1,2,1,2))]. given #29 (T,wt=10): 182 c(x v y) v c(x) = c(x). [para(92(a,1),152(a,1,1,1,1))]. given #30 (T,wt=10): 196 c(x v y) v c(y) = c(y). [para(92(a,1),153(a,1,1,1,2))]. given #31 (A,wt=15): 25 x v (y v (z v u)) = x v (z v (y v u)). [para(14(a,2),7(a,1))]. given #32 (F,wt=11): 38 x v c(y v (c(x) v z)) = x. [para(7(a,1),19(a,1,2,1))]. given #33 (F,wt=11): 57 x v (c(x) v y) = x v c(x). [para(19(a,1),15(a,1,2)),demod(7(5)),flip(a)]. given #34 (T,wt=9): 387 c(x) v x = x v c(x). [para(92(a,1),57(a,1,2,1)),demod(7(3),57(3),92(5)),flip(a)]. given #35 (T,wt=11): 169 c(x v (c(y) v z)) v y = y. [para(7(a,1),152(a,1,1,1))]. given #36 (A,wt=23): 29 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))). [para(14(a,1),14(a,1,2,2))]. given #37 (F,wt=11): 374 x v c(y v (z v c(x))) = x. [para(100(a,1),38(a,1,2,1,2))]. given #38 (F,wt=9): 596 x v c(y v c(y)) = x. [para(57(a,1),374(a,1,2,1))]. % Operation v is associative-commutative; redundancy checks enabled. given #39 (T,wt=7): 598 x v y = y v x. [para(596(a,1),7(a,1,2)),demod(596(5))]. given #40 (T,wt=9): 600 c(x v c(x)) v y = y. [para(596(a,1),100(a,1,2)),demod(596(8))]. NOTE: New constant: 0 c(x v c(x)) = c_0. [new_symbol(685)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, v, ^, c ]). given #41 (A,wt=19): 30 x v (y v (z v (u v v))) = u v (x v (z v (y v v))). [para(14(a,1),14(a,1,2))]. given #42 (F,wt=5): 687 c_0 v x = x. [back_demod(600),demod(686(3))]. given #43 (F,wt=5): 688 x v c_0 = x. [back_demod(596),demod(686(3))]. given #44 (T,wt=7): 686 c(x v c(x)) = c_0. [new_symbol(685)]. given #45 (T,wt=7): 696 c(x v c(c_0)) = c_0. [para(687(a,1),45(a,1))]. given #46 (A,wt=23): 31 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))). [para(14(a,2),14(a,1,2,2))]. given #47 (F,wt=7): 699 c(c_0) v x = c(c_0). [para(687(a,1),57(a,1)),demod(687(7))]. given #48 (F,wt=7): 701 c(c_0) = x v c(x). [para(686(a,1),92(a,1,1))]. ============================== PROOF ================================= % Proof 2 at 0.11 (+ 0.01) seconds: ONE. % Length of proof is 33. % Level of proof is 20. % Maximum clause weight is 19. % Given clauses 48. 2 x v (x ^ y) = x # label(B1). [input]. 4 x v (c(x) ^ (x v y)) = x v y # label(OM). [input]. 7 x v (y v z) = y v (x v z) # label(AJ). [input]. 8 x v (x ^ y) = x # label(B1). [copy(2)]. 9 x ^ y = c(c(x) v c(y)) # label(DM). [input]. 10 x v c(c(c(x)) v c(x v y)) = x v y # label(OM). [copy(4),demod(9(3))]. 11 x v c(c(x) v c(y)) = x. [back_demod(8),demod(9(1))]. 13 c3 v c(c3) != c2 v c(c2) # answer(ONE). [clausify]. 15 x v (y v c(c(c(x)) v c(x v z))) = y v (x v z). [para(10(a,1),7(a,1,2)),flip(a)]. 19 x v c(c(x) v y) = x. [para(10(a,1),11(a,1,2,1))]. 20 x v c(c(x)) = x. [para(11(a,1),11(a,1,2,1))]. 21 x v (y v c(c(x))) = y v x. [para(20(a,1),7(a,1,2)),flip(a)]. 38 x v c(y v (c(x) v z)) = x. [para(7(a,1),19(a,1,2,1))]. 45 x v c(y v c(x)) = x. [para(21(a,1),19(a,1,2,1))]. 48 c(x) v c(x) = c(x). [para(20(a,1),45(a,1,2,1))]. 57 x v (c(x) v y) = x v c(x). [para(19(a,1),15(a,1,2)),demod(7(5)),flip(a)]. 62 c(c(x)) v x = x. [para(48(a,1),21(a,1,2)),demod(20(3)),flip(a)]. 64 c(c(x)) v (y v x) = y v x. [para(62(a,1),7(a,1,2)),flip(a)]. 72 c(c(c(c(x)))) v x = x. [para(62(a,1),21(a,1,2)),demod(20(3)),flip(a)]. 77 c(c(c(c(x)))) v c(c(c(c(c(c(c(x)))))) v c(x)) = x. [para(72(a,1),10(a,1,2,1,2,1)),demod(72(19))]. 83 c(c(c(x))) = c(x). [para(72(a,1),19(a,1,2,1)),demod(62(5)),flip(a)]. 85 c(c(x)) v c(c(c(x)) v c(x)) = x. [back_demod(77),demod(83(3),83(5),83(5))]. 89 c(c(x)) v c(y v c(x)) = c(c(x)). [para(83(a,1),45(a,1,2,1,2))]. 92 c(c(x)) = x. [back_demod(85),demod(89(8))]. 100 x v (y v x) = y v x. [back_demod(64),demod(92(2))]. 374 x v c(y v (z v c(x))) = x. [para(100(a,1),38(a,1,2,1,2))]. 596 x v c(y v c(y)) = x. [para(57(a,1),374(a,1,2,1))]. 600 c(x v c(x)) v y = y. [para(596(a,1),100(a,1,2)),demod(596(8))]. 685 c(x v c(x)) = c(y v c(y)). [para(600(a,1),596(a,1))]. 686 c(x v c(x)) = c_0. [new_symbol(685)]. 701 c(c_0) = x v c(x). [para(686(a,1),92(a,1,1))]. 733 x v c(x) = y v c(y). [para(701(a,1),701(a,1))]. 734 $F # answer(ONE). [resolve(733,a,13,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=48. Generated=3704. Kept=726. proofs=2. Usable=27. Sos=469. Demods=210. Denials=1. Limbo=5, Disabled=229. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=2978. Back_subsumed=22. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=423 (2 lex), Back_demodulated=200. Back_unit_deleted=0. Demod_attempts=42348. Demod_rewrites=3861. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.73. User_CPU=0.11, System_CPU=0.01, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 2 proofs. Process 13585 exit (max_proofs) Mon Jun 19 16:43:06 2006