============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3929 was started by mccune on cleo.thornwood, Wed Nov 22 11:25:20 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). formulas(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. formulas(goals). c(c(x)) = x # answer(CC). x v c(x) = y v c(y) # answer(ONE). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 c(c(x)) = x # answer(CC) # label(goal). [goal]. 2 x v c(x) = y v c(y) # answer(ONE) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v (y v z) = y v (x v z) # label(AJ). [assumption]. x v (x ^ y) = x # label(B1). [assumption]. x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. x v (c(x) ^ (x v y)) = x v y # label(OM). [assumption]. c(c(c1)) != c1 # answer(CC). [deny(1)]. c3 v c(c3) != c2 v c(c2) # answer(ONE). [deny(2)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 2). % (Horn set with more than one neg. clause) Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, v, ^, c ]). After inverse_order: (no changes). 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: formulas(usable). end_of_list. formulas(sos). 3 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 5 x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. 7 x v c(c(c(x)) v c(x v y)) = x v y. [copy(6),rewrite(5(3))]. 8 c(c(c1)) != c1 # answer(CC). [deny(1)]. 9 c3 v c(c3) != c2 v c(c2) # answer(ONE). [deny(2)]. 10 x v c(c(x) v c(y)) = x. [back_rewrite(4),rewrite(5(1))]. end_of_list. formulas(demodulators). 3 x v (y v z) = y v (x v z) # label(AJ). [assumption]. % (lex-dep) 5 x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. 7 x v c(c(c(x)) v c(x v y)) = x v y. [copy(6),rewrite(5(3))]. 10 x v c(c(x) v c(y)) = x. [back_rewrite(4),rewrite(5(1))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=11): 3 x v (y v z) = y v (x v z) # label(AJ). [assumption]. given #2 (I,wt=10): 5 x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. given #3 (I,wt=15): 7 x v c(c(c(x)) v c(x v y)) = x v y. [copy(6),rewrite(5(3))]. given #4 (I,wt=5): 8 c(c(c1)) != c1 # answer(CC). [deny(1)]. given #5 (I,wt=9): 9 c3 v c(c3) != c2 v c(c2) # answer(ONE). [deny(2)]. given #6 (I,wt=10): 10 x v c(c(x) v c(y)) = x. [back_rewrite(4),rewrite(5(1))]. given #7 (F,wt=7): 17 x v c(c(x)) = x. [para(10(a,1),10(a,1,2,1))]. given #8 (F,wt=9): 16 x v c(c(x) v y) = x. [para(7(a,1),10(a,1,2,1))]. given #9 (T,wt=11): 15 x v c(c(c(x)) v c(x)) = x. [para(10(a,1),7(a,1,2,1,2,1)),rewrite(10(11))]. given #10 (T,wt=11): 18 x v (y v c(c(x))) = y v x. [para(17(a,1),3(a,1,2)),flip(a)]. given #11 (A,wt=15): 11 x v (y v (z v u)) = z v (x v (y v u)). [para(3(a,1),3(a,1,2))]. given #12 (F,wt=9): 24 x v c(y v c(x)) = x. [para(18(a,1),16(a,1,2,1))]. given #13 (F,wt=8): 44 c(x) v c(x) = c(x). [para(17(a,1),24(a,1,2,1))]. given #14 (T,wt=7): 49 c(c(x)) v x = x. [para(44(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. given #15 (T,wt=9): 54 c(c(c(c(x)))) v x = x. [para(49(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. given #16 (A,wt=19): 12 x v (y v c(c(c(x)) v c(x v z))) = y v (x v z). [para(7(a,1),3(a,1,2)),flip(a)]. given #17 (F,wt=7): 63 c(c(c(x))) = c(x). [para(54(a,1),16(a,1,2,1)),rewrite(49(5)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: CC. % Length of proof is 21. % Level of proof is 11. % Maximum clause weight is 19. % Given clauses 17. 1 c(c(x)) = x # answer(CC) # label(goal). [goal]. 3 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 4 x v (x ^ y) = x # label(B1). [assumption]. 5 x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. 6 x v (c(x) ^ (x v y)) = x v y # label(OM). [assumption]. 7 x v c(c(c(x)) v c(x v y)) = x v y. [copy(6),rewrite(5(3))]. 8 c(c(c1)) != c1 # answer(CC). [deny(1)]. 10 x v c(c(x) v c(y)) = x. [back_rewrite(4),rewrite(5(1))]. 16 x v c(c(x) v y) = x. [para(7(a,1),10(a,1,2,1))]. 17 x v c(c(x)) = x. [para(10(a,1),10(a,1,2,1))]. 18 x v (y v c(c(x))) = y v x. [para(17(a,1),3(a,1,2)),flip(a)]. 24 x v c(y v c(x)) = x. [para(18(a,1),16(a,1,2,1))]. 44 c(x) v c(x) = c(x). [para(17(a,1),24(a,1,2,1))]. 49 c(c(x)) v x = x. [para(44(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. 54 c(c(c(c(x)))) v x = x. [para(49(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. 62 c(c(c(c(x)))) v c(c(c(c(c(c(c(x)))))) v c(x)) = x. [para(54(a,1),7(a,1,2,1,2,1)),rewrite(54(19))]. 63 c(c(c(x))) = c(x). [para(54(a,1),16(a,1,2,1)),rewrite(49(5)),flip(a)]. 64 c(c(x)) v c(c(c(x)) v c(x)) = x. [back_rewrite(62),rewrite(63(3),63(5),63(5))]. 78 c(c(x)) v c(y v c(x)) = c(c(x)). [para(63(a,1),24(a,1,2,1,2))]. 81 c(c(x)) = x. [back_rewrite(64),rewrite(78(8))]. 82 $F # answer(CC). [resolve(81,a,8,a)]. ============================== end of proof ========================== % Redundant proof: 102 $F # answer(CC). [back_rewrite(8),rewrite(81(3)),xx(a)]. % Disable descendants (x means already disabled): 8x given #18 (F,wt=5): 81 c(c(x)) = x. [back_rewrite(64),rewrite(78(8))]. given #19 (T,wt=5): 95 x v x = x. [back_rewrite(49),rewrite(81(2))]. given #20 (T,wt=9): 93 x v (x v y) = x v y. [back_rewrite(52),rewrite(81(3),72(3))]. given #21 (A,wt=13): 19 x v (y v c(c(x) v z)) = y v x. [para(16(a,1),3(a,1,2)),flip(a)]. % Operation v is commutative; C redundancy checks enabled. given #22 (F,wt=7): 112 x v y = y v x. [para(24(a,1),19(a,1,2))]. given #23 (F,wt=9): 94 x v (y v x) = y v x. [back_rewrite(51),rewrite(81(2))]. given #24 (T,wt=10): 105 c(x) v c(x v y) = c(x). [para(81(a,1),16(a,1,2,1,1))]. given #25 (T,wt=10): 106 c(x) v c(y v x) = c(x). [para(81(a,1),24(a,1,2,1,2))]. given #26 (A,wt=11): 20 x v c(y v (c(x) v z)) = x. [para(3(a,1),16(a,1,2,1))]. given #27 (F,wt=11): 66 x v (c(x) v y) = x v c(x). [para(16(a,1),12(a,1,2)),rewrite(3(5)),flip(a)]. given #28 (F,wt=11): 114 x v (y v z) = z v (x v y). [para(112(a,1),3(a,1,2))]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 114 x v (y v z) = z v (x v y). [para(112(a,1),3(a,1,2))]. % back CAC tautology: 11 x v (y v (z v u)) = z v (x v (y v u)). [para(3(a,1),3(a,1,2))]. % back CAC tautology: 160 x v (y v (z v u)) = u v (y v (x v z)). [para(114(a,2),11(a,2,2)),flip(a)]. % back CAC tautology: 159 x v (y v (z v (u v v))) = z v (x v (u v (v v y))). [para(114(a,2),11(a,2,2,2))]. % back CAC tautology: 157 x v (y v (z v u)) = z v (u v (x v y)). [para(114(a,1),11(a,2,2))]. % back CAC tautology: 156 x v (y v (z v (u v v))) = z v (x v (v v (y v u))). [para(114(a,1),11(a,2,2,2))]. % back CAC tautology: 154 x v (y v (z v u)) = y v (x v (u v z)). [para(114(a,2),11(a,1,2))]. % back CAC tautology: 153 x v (y v (z v (u v v))) = v v (x v (y v (z v u))). [para(114(a,2),11(a,1,2,2))]. % back CAC tautology: 151 x v (y v (z v u)) = u v (x v (z v y)). [para(114(a,1),11(a,1,2))]. % back CAC tautology: 150 x v (y v (z v (u v v))) = u v (x v (y v (v v z))). [para(114(a,1),11(a,1,2,2))]. % back CAC tautology: 148 x v (y v z) = z v (y v x). [para(114(a,1),3(a,1))]. % back CAC tautology: 119 x v (y v (z v u)) = z v (x v (u v y)). [para(112(a,1),11(a,2,2,2))]. % back CAC tautology: 116 x v (y v (z v u)) = u v (x v (y v z)). [para(112(a,1),11(a,1,2,2))]. % back CAC tautology: 71 x v (y v (z v (u v v))) = x v (u v (y v (z v v))). [para(11(a,1),12(a,2,2)),rewrite(12(10))]. % back CAC tautology: 69 x v (y v (z v (u v v))) = x v (y v (u v (z v v))). [para(11(a,1),12(a,1,2,2,1,2,1)),rewrite(65(10))]. % back CAC tautology: 41 x v (y v (z v (u v v))) = u v (y v (x v (z v v))). [para(11(a,2),11(a,2,2)),flip(a)]. % back CAC tautology: 40 x v (y v (z v (u v (v v w)))) = z v (x v (u v (v v (y v w)))). [para(11(a,2),11(a,2,2,2))]. % back CAC tautology: 39 x v (y v (z v (u v v))) = z v (u v (x v (y v v))). [para(11(a,1),11(a,2,2))]. % back CAC tautology: 38 x v (y v (z v (u v (v v w)))) = z v (x v (v v (y v (u v w)))). [para(11(a,1),11(a,2,2,2))]. % back CAC tautology: 37 x v (y v (z v (u v v))) = y v (x v (u v (z v v))). [para(11(a,2),11(a,1,2))]. % back CAC tautology: 36 x v (y v (z v (u v (v v w)))) = v v (x v (y v (z v (u v w)))). [para(11(a,2),11(a,1,2,2))]. % back CAC tautology: 35 x v (y v (z v (u v v))) = u v (x v (z v (y v v))). [para(11(a,1),11(a,1,2))]. % back CAC tautology: 34 x v (y v (z v (u v (v v w)))) = u v (x v (y v (v v (z v w)))). [para(11(a,1),11(a,1,2,2))]. % back CAC tautology: 28 x v (y v (z v u)) = x v (z v (y v u)). [para(11(a,2),3(a,1))]. % back CAC tautology: 27 x v (y v (z v (u v v))) = u v (x v (y v (z v v))). [para(11(a,2),3(a,1,2))]. % back CAC tautology: 26 x v (y v (z v u)) = z v (y v (x v u)). [para(11(a,1),3(a,1))]. % back CAC tautology: 25 x v (y v (z v (u v v))) = z v (x v (u v (y v v))). [para(11(a,1),3(a,1,2))]. given #29 (T,wt=11): 138 x v c(y v (z v c(x))) = x. [para(19(a,1),20(a,1,2,1,2))]. given #30 (T,wt=9): 181 x v c(y v c(y)) = x. [para(66(a,1),138(a,1,2,1))]. given #31 (A,wt=13): 31 x v c(y v (z v (c(x) v u))) = x. [para(11(a,2),16(a,1,2,1))]. given #32 (F,wt=9): 182 c(x v c(x)) v y = y. [para(181(a,1),19(a,2)),rewrite(81(7),171(6),66(6),181(7))]. NOTE: New constant: c(x v c(x)) = c_0. [new_symbol(183)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c_0, v, ^, c ]). given #33 (F,wt=5): 185 c_0 v x = x. [back_rewrite(182),rewrite(184(3))]. given #34 (T,wt=5): 186 x v c_0 = x. [back_rewrite(181),rewrite(184(3))]. given #35 (T,wt=7): 184 c(x v c(x)) = c_0. [new_symbol(183)]. given #36 (A,wt=17): 32 x v (y v (z v c(c(x) v u))) = y v (z v x). [para(16(a,1),11(a,1,2,2)),flip(a)]. given #37 (F,wt=7): 188 c(x v c(c_0)) = c_0. [para(185(a,1),24(a,1))]. given #38 (F,wt=7): 191 c(c_0) v x = c(c_0). [para(185(a,1),66(a,1)),rewrite(185(7))]. given #39 (T,wt=7): 193 c(c_0) = x v c(x). [para(184(a,1),81(a,1,1))]. ============================== PROOF ================================= % Proof 2 at 0.02 (+ 0.00) seconds: ONE. % Length of proof is 35. % Level of proof is 16. % Maximum clause weight is 19. % Given clauses 39. 2 x v c(x) = y v c(y) # answer(ONE) # label(goal). [goal]. 3 x v (y v z) = y v (x v z) # label(AJ). [assumption]. 4 x v (x ^ y) = x # label(B1). [assumption]. 5 x ^ y = c(c(x) v c(y)) # label(DM). [assumption]. 6 x v (c(x) ^ (x v y)) = x v y # label(OM). [assumption]. 7 x v c(c(c(x)) v c(x v y)) = x v y. [copy(6),rewrite(5(3))]. 9 c3 v c(c3) != c2 v c(c2) # answer(ONE). [deny(2)]. 10 x v c(c(x) v c(y)) = x. [back_rewrite(4),rewrite(5(1))]. 12 x v (y v c(c(c(x)) v c(x v z))) = y v (x v z). [para(7(a,1),3(a,1,2)),flip(a)]. 16 x v c(c(x) v y) = x. [para(7(a,1),10(a,1,2,1))]. 17 x v c(c(x)) = x. [para(10(a,1),10(a,1,2,1))]. 18 x v (y v c(c(x))) = y v x. [para(17(a,1),3(a,1,2)),flip(a)]. 19 x v (y v c(c(x) v z)) = y v x. [para(16(a,1),3(a,1,2)),flip(a)]. 20 x v c(y v (c(x) v z)) = x. [para(3(a,1),16(a,1,2,1))]. 24 x v c(y v c(x)) = x. [para(18(a,1),16(a,1,2,1))]. 44 c(x) v c(x) = c(x). [para(17(a,1),24(a,1,2,1))]. 49 c(c(x)) v x = x. [para(44(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. 54 c(c(c(c(x)))) v x = x. [para(49(a,1),18(a,1,2)),rewrite(17(3)),flip(a)]. 62 c(c(c(c(x)))) v c(c(c(c(c(c(c(x)))))) v c(x)) = x. [para(54(a,1),7(a,1,2,1,2,1)),rewrite(54(19))]. 63 c(c(c(x))) = c(x). [para(54(a,1),16(a,1,2,1)),rewrite(49(5)),flip(a)]. 64 c(c(x)) v c(c(c(x)) v c(x)) = x. [back_rewrite(62),rewrite(63(3),63(5),63(5))]. 66 x v (c(x) v y) = x v c(x). [para(16(a,1),12(a,1,2)),rewrite(3(5)),flip(a)]. 78 c(c(x)) v c(y v c(x)) = c(c(x)). [para(63(a,1),24(a,1,2,1,2))]. 81 c(c(x)) = x. [back_rewrite(64),rewrite(78(8))]. 112 x v y = y v x. [para(24(a,1),19(a,1,2))]. 114 x v (y v z) = z v (x v y). [para(112(a,1),3(a,1,2))]. 138 x v c(y v (z v c(x))) = x. [para(19(a,1),20(a,1,2,1,2))]. 171 (x v y) v z = x v (y v z). [para(114(a,2),112(a,1)),flip(a)]. 181 x v c(y v c(y)) = x. [para(66(a,1),138(a,1,2,1))]. 182 c(x v c(x)) v y = y. [para(181(a,1),19(a,2)),rewrite(81(7),171(6),66(6),181(7))]. 183 c(x v c(x)) = c(y v c(y)). [para(182(a,1),181(a,1))]. 184 c(x v c(x)) = c_0. [new_symbol(183)]. 193 c(c_0) = x v c(x). [para(184(a,1),81(a,1,1))]. 207 c(c_0) != c2 v c(c2) # answer(ONE). [para(193(a,2),9(a,1))]. 208 $F # answer(ONE). [resolve(207,a,193,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=39. Generated=1248. Kept=202. proofs=2. Usable=23. Sos=62. Demods=76. Limbo=0, Disabled=122. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=1045. Back_subsumed=15. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=145 (6 lex), Back_demodulated=74. Back_unit_deleted=0. Demod_attempts=11371. Demod_rewrites=1851. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.17. User_CPU=0.02, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 2 proofs. Process 3929 exit (max_proofs) Wed Nov 22 11:25:20 2006