============================== Prover9 =============================== Prover9 (32) version 2009-02A, February 2009. Process 11588 was started by mccune on cleo, Wed Feb 25 09:32:45 2009 The command was "/home/mccune/bin/prover9 -f mckenzie.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mckenzie.in assign(max_seconds,30). formulas(sos). x v (y ^ (x ^ z)) = x # label(McKenzie_1). x ^ (y v (x v z)) = x # label(McKenzie_2). ((y ^ x) v (x ^ z)) v x = x # label(McKenzie_3). ((y v x) ^ (x v z)) ^ x = x # label(McKenzie_4). end_of_list. set(restrict_denials). formulas(goals). x v y = y v x # answer(commute_join). (x v y) v z = x v (y v z) # answer(assoc_join). x ^ y = y ^ x # answer(commute_meet). (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet). x ^ (x v y) = x # answer(absorb_1). x v (x ^ y) = x # answer(absorb_2). x v y = y v x & (x v y) v z = x v (y v z) & x ^ y = y ^ x & (x ^ y) ^ z = x ^ (y ^ z) & x ^ (x v y) = x & x v (x ^ y) = x # label(all_six). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x v y = y v x # answer(commute_join) # label(non_clause) # label(goal). [goal]. 2 (x v y) v z = x v (y v z) # answer(assoc_join) # label(non_clause) # label(goal). [goal]. 3 x ^ y = y ^ x # answer(commute_meet) # label(non_clause) # label(goal). [goal]. 4 (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet) # label(non_clause) # label(goal). [goal]. 5 x ^ (x v y) = x # answer(absorb_1) # label(non_clause) # label(goal). [goal]. 6 x v (x ^ y) = x # answer(absorb_2) # label(non_clause) # label(goal). [goal]. 7 x v y = y v x & (x v y) v z = x v (y v z) & x ^ y = y ^ x & (x ^ y) ^ z = x ^ (y ^ z) & x ^ (x v y) = x & x v (x ^ y) = x # label(all_six) # label(non_clause) # 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 ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. c2 v c1 != c1 v c2 # answer(commute_join). [deny(1)]. (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [deny(2)]. c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [deny(3)]. (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [deny(4)]. c11 ^ (c11 v c12) != c11 # answer(absorb_1). [deny(5)]. c13 v (c13 ^ c14) != c13 # answer(absorb_2). [deny(6)]. c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) | c15 ^ (c15 v c16) != c15 | c15 v (c15 ^ c16) != c15 # label(all_six). [deny(7)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label all_six to answer in negative clause % assign(max_proofs, 7). % (Horn set with more than one neg. clause) Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 6). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. kept: 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. kept: 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. kept: 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. kept: 12 c2 v c1 != c1 v c2 # answer(commute_join). [deny(1)]. kept: 13 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [deny(2)]. kept: 14 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [deny(3)]. kept: 15 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [deny(4)]. kept: 16 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [deny(5)]. kept: 17 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [deny(6)]. kept: 18 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) | c15 ^ (c15 v c16) != c15 | c15 v (c15 ^ c16) != c15 # label(all_six) # answer(all_six). [deny(7)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). 12 c2 v c1 != c1 v c2 # answer(commute_join). [deny(1)]. 13 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [deny(2)]. 14 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [deny(3)]. 15 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [deny(4)]. 16 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [deny(5)]. 17 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [deny(6)]. 18 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) | c15 ^ (c15 v c16) != c15 | c15 v (c15 ^ c16) != c15 # label(all_six) # answer(all_six). [deny(7)]. end_of_list. formulas(sos). 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. end_of_list. formulas(demodulators). 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.01 seconds. given #1 (I,wt=9): 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. given #2 (I,wt=9): 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. given #3 (I,wt=11): 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. ============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds: absorb_1. % Length of proof is 6. % Level of proof is 2. % Maximum clause weight is 11. % Given clauses 3. 5 x ^ (x v y) = x # answer(absorb_1) # label(non_clause) # label(goal). [goal]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 16 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [deny(5)]. 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. 24 $F # answer(absorb_1). [resolve(23,a,16,a)]. ============================== end of proof ========================== % Redundant proof: 28 $F # answer(absorb_1). [back_rewrite(16),rewrite([23(5)]),xx(a)]. % Disable descendants (x means already disabled): 16x given #4 (I,wt=11): 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. ============================== PROOF ================================= % Proof 2 at 0.01 (+ 0.00) seconds: absorb_2. % Length of proof is 6. % Level of proof is 2. % Maximum clause weight is 11. % Given clauses 4. 6 x v (x ^ y) = x # answer(absorb_2) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 17 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [deny(6)]. 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. 31 $F # answer(absorb_2). [resolve(30,a,17,a)]. ============================== end of proof ========================== % Redundant proof: 39 $F # answer(absorb_2). [back_rewrite(17),rewrite([30(5)]),xx(a)]. % Disable descendants (x means already disabled): 17x given #5 (A,wt=7): 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. given #6 (T,wt=5): 26 x v x = x. [para(9(a,1),10(a,1,1,2)),rewrite([21(2)])]. given #7 (T,wt=5): 36 x ^ x = x. [para(10(a,1),11(a,1,1,1)),rewrite([23(2)])]. given #8 (T,wt=7): 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. given #9 (T,wt=7): 21 (x ^ y) v y = y. [para(8(a,1),10(a,1,1))]. given #10 (A,wt=19): 22 ((x ^ y) v (y ^ z)) ^ (u v y) = (x ^ y) v (y ^ z). [para(10(a,1),9(a,1,2,2))]. given #11 (T,wt=7): 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. given #12 (T,wt=7): 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. given #13 (T,wt=7): 34 (x v y) ^ y = y. [para(9(a,1),11(a,1,1))]. given #14 (T,wt=9): 44 (x v y) v y = x v y. [para(20(a,1),19(a,1,2))]. given #15 (A,wt=21): 25 (x v ((y v (x v z)) ^ u)) v (y v (x v z)) = y v (x v z). [para(9(a,1),10(a,1,1,1))]. given #16 (T,wt=9): 45 (x ^ y) ^ y = x ^ y. [para(19(a,1),20(a,1,2))]. given #17 (T,wt=9): 49 x v (y v x) = y v x. [para(20(a,1),21(a,1,1))]. given #18 (T,wt=7): 81 (x ^ y) v x = x. [para(30(a,1),49(a,1,2)),rewrite([30(4)])]. given #19 (T,wt=9): 61 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. given #20 (A,wt=19): 29 ((x v y) ^ (y v z)) v (u ^ y) = (x v y) ^ (y v z). [para(11(a,1),8(a,1,2,2))]. given #21 (T,wt=7): 91 (x v y) ^ x = x. [para(61(a,1),34(a,1,1))]. given #22 (T,wt=9): 62 x v (x v y) = x v y. [para(23(a,1),21(a,1,1))]. given #23 (T,wt=9): 66 (x ^ y) ^ x = x ^ y. [para(30(a,1),20(a,1,2))]. given #24 (T,wt=9): 71 x ^ (y ^ x) = y ^ x. [para(19(a,1),34(a,1,1))]. given #25 (A,wt=21): 32 (x ^ ((y ^ (x ^ z)) v u)) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),11(a,1,1,1))]. given #26 (T,wt=9): 73 x ^ (x ^ y) = x ^ y. [para(30(a,1),34(a,1,1))]. given #27 (T,wt=9): 78 (x ^ (y ^ z)) v y = y. [para(8(a,1),49(a,1,2)),rewrite([8(6)])]. given #28 (T,wt=9): 79 x ^ (y v (z v x)) = x. [para(49(a,1),9(a,1,2,2))]. given #29 (T,wt=9): 87 x ^ ((x v y) v z) = x. [para(61(a,1),9(a,1,2))]. given #30 (A,wt=27): 35 ((x ^ ((y v z) ^ (z v u))) v z) v ((y v z) ^ (z v u)) = (y v z) ^ (z v u). [para(11(a,1),10(a,1,1,2))]. given #31 (T,wt=9): 119 x v ((x ^ y) ^ z) = x. [para(66(a,1),8(a,1,2))]. given #32 (T,wt=9): 124 x v (y ^ (z ^ x)) = x. [para(71(a,1),8(a,1,2,2))]. given #33 (T,wt=9): 125 (x v (y v z)) ^ y = y. [para(9(a,1),71(a,1,2)),rewrite([9(6)])]. given #34 (T,wt=9): 148 ((x ^ y) ^ z) v x = x. [para(66(a,1),78(a,1,1))]. given #35 (A,wt=27): 37 ((x v ((y ^ z) v (z ^ u))) ^ z) ^ ((y ^ z) v (z ^ u)) = (y ^ z) v (z ^ u). [para(10(a,1),11(a,1,1,2))]. given #36 (T,wt=9): 149 (x ^ (y ^ z)) v z = z. [para(71(a,1),78(a,1,1,2))]. given #37 (T,wt=9): 154 x ^ ((y v x) v z) = x. [para(61(a,1),79(a,1,2))]. given #38 (T,wt=9): 157 (x v (y v z)) ^ z = z. [para(79(a,1),71(a,1,2)),rewrite([79(6)])]. given #39 (T,wt=9): 165 ((x v y) v z) ^ x = x. [para(87(a,1),71(a,1,2)),rewrite([87(6)])]. given #40 (A,wt=13): 40 (x v (y v z)) v y = x v (y v z). [para(9(a,1),19(a,1,2))]. given #41 (T,wt=9): 192 x v ((y ^ x) ^ z) = x. [para(71(a,1),119(a,1,2,1))]. given #42 (T,wt=9): 222 ((x ^ y) ^ z) v y = y. [para(71(a,1),148(a,1,1,1))]. given #43 (T,wt=9): 265 ((x v y) v z) ^ y = y. [para(154(a,1),71(a,1,2)),rewrite([154(6)])]. given #44 (T,wt=11): 46 (x ^ y) ^ (z v y) = x ^ y. [para(21(a,1),9(a,1,2,2))]. given #45 (A,wt=15): 41 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(19(a,1),11(a,1,1,1))]. given #46 (T,wt=11): 68 (x v y) v (z ^ y) = x v y. [para(34(a,1),8(a,1,2,2))]. given #47 (T,wt=11): 80 ((x v y) ^ (z v y)) ^ y = y. [para(49(a,1),11(a,1,1,2))]. given #48 (T,wt=11): 83 (x ^ y) ^ (z v x) = x ^ y. [para(81(a,1),9(a,1,2,2))]. given #49 (T,wt=11): 88 x v ((y ^ x) v (x ^ z)) = x. [para(10(a,1),61(a,1,1)),rewrite([10(8)])]. given #50 (A,wt=13): 42 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(8(a,1),20(a,1,2))]. given #51 (T,wt=11): 89 ((x v y) ^ (x v z)) ^ x = x. [para(61(a,1),11(a,1,1,1))]. given #52 (T,wt=11): 113 (x v y) v (z ^ x) = x v y. [para(91(a,1),8(a,1,2,2))]. given #53 (T,wt=11): 120 ((x ^ y) v (x ^ z)) v x = x. [para(66(a,1),10(a,1,1,1))]. given #54 (T,wt=11): 121 x ^ ((y v x) ^ (x v z)) = x. [para(11(a,1),66(a,1,1)),rewrite([11(8)])]. given #55 (A,wt=15): 43 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(20(a,1),10(a,1,1,1))]. given #56 (T,wt=11): 126 ((x ^ y) v (z ^ y)) v y = y. [para(71(a,1),10(a,1,1,2))]. given #57 (T,wt=11): 144 (x ^ y) v (z v y) = z v y. [para(34(a,1),78(a,1,1,2))]. given #58 (T,wt=11): 147 (x ^ y) v (y v z) = y v z. [para(91(a,1),78(a,1,1,2))]. given #59 (T,wt=11): 160 (x ^ y) ^ (y v z) = x ^ y. [para(21(a,1),87(a,1,2,1))]. given #60 (A,wt=13): 47 x v (y v (x v z)) = y v (x v z). [para(9(a,1),21(a,1,1))]. given #61 (T,wt=11): 163 (x ^ y) ^ (x v z) = x ^ y. [para(81(a,1),87(a,1,2,1))]. given #62 (T,wt=11): 189 (x v y) v (y ^ z) = x v y. [para(34(a,1),119(a,1,2,1))]. given #63 (T,wt=11): 191 (x v y) v (x ^ z) = x v y. [para(91(a,1),119(a,1,2,1))]. given #64 (T,wt=11): 207 (x v y) ^ (z ^ y) = z ^ y. [para(21(a,1),125(a,1,1,2))]. given #65 (A,wt=15): 48 ((x v (y ^ z)) ^ z) ^ (y ^ z) = y ^ z. [para(21(a,1),11(a,1,1,2))]. given #66 (T,wt=11): 210 (x v y) ^ (y ^ z) = y ^ z. [para(81(a,1),125(a,1,1,2))]. given #67 (T,wt=11): 218 (x ^ y) v (z v x) = z v x. [para(34(a,1),148(a,1,1,1))]. given #68 (T,wt=11): 221 (x ^ y) v (x v z) = x v z. [para(91(a,1),148(a,1,1,1))]. given #69 (T,wt=11): 278 (x v y) ^ (z ^ x) = z ^ x. [para(21(a,1),165(a,1,1,1))]. given #70 (A,wt=33): 50 ((x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ w)) ^ z = (x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ w). [para(8(a,1),22(a,1,2))]. given #71 (T,wt=11): 282 (x v y) ^ (x ^ z) = x ^ z. [para(81(a,1),165(a,1,1,1))]. given #72 (T,wt=11): 291 x ^ (y v ((x v z) v u)) = x. [para(40(a,1),9(a,1,2))]. given #73 (T,wt=11): 298 x ^ (y v (z v (x v u))) = x. [para(40(a,1),79(a,1,2,2))]. given #74 (T,wt=11): 299 x ^ (y v ((z v x) v u)) = x. [para(40(a,1),79(a,1,2))]. given #75 (A,wt=27): 51 (x v ((y v (x v z)) ^ u)) ^ (w v (y v (x v z))) = x v ((y v (x v z)) ^ u). [para(9(a,1),22(a,1,1,1)),rewrite([9(11)])]. given #76 (T,wt=11): 302 (x v ((y v z) v u)) ^ y = y. [para(40(a,1),125(a,1,1))]. given #77 (T,wt=11): 306 x ^ ((y v (x v z)) v u) = x. [para(40(a,1),154(a,1,2,1))]. given #78 (T,wt=11): 307 (x v (y v (z v u))) ^ z = z. [para(40(a,1),157(a,1,1,2))]. given #79 (T,wt=11): 308 (x v ((y v z) v u)) ^ z = z. [para(40(a,1),157(a,1,1))]. given #80 (A,wt=21): 52 (((x ^ y) v (y ^ z)) v ((u v y) ^ w)) v (u v y) = u v y. [para(22(a,1),10(a,1,1,1))]. given #81 (T,wt=11): 336 ((x v (y v z)) v u) ^ y = y. [para(40(a,1),265(a,1,1,1))]. given #82 (T,wt=11): 342 x ^ (y v (z v (u v x))) = x. [para(79(a,1),46(a,1,1)),rewrite([79(7)])]. given #83 (T,wt=11): 356 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. % Operation ^ is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 3 at 0.18 (+ 0.01) seconds: commute_meet. % Length of proof is 17. % Level of proof is 7. % Maximum clause weight is 15. % Given clauses 83. 3 x ^ y = y ^ x # answer(commute_meet) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 14 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [deny(3)]. 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. 21 (x ^ y) v y = y. [para(8(a,1),10(a,1,1))]. 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. 41 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(19(a,1),11(a,1,1,1))]. 49 x v (y v x) = y v x. [para(20(a,1),21(a,1,1))]. 81 (x ^ y) v x = x. [para(30(a,1),49(a,1,2)),rewrite([30(4)])]. 356 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 1261 (x ^ y) v (y ^ x) = x ^ y. [para(356(a,1),30(a,1,2))]. 1262 x ^ y = y ^ x. [para(356(a,1),81(a,1,1)),rewrite([1261(3)])]. 1263 $F # answer(commute_meet). [resolve(1262,a,14,a)]. ============================== end of proof ========================== % Redundant proof: 1474 $F # answer(commute_meet). [back_rewrite(14),rewrite([1262(3)]),xx(a)]. % Disable descendants (x means already disabled): 14x given #84 (T,wt=7): 1262 x ^ y = y ^ x. [para(356(a,1),81(a,1,1)),rewrite([1261(3)])]. given #85 (A,wt=33): 54 ((x ^ ((y v z) ^ (z v u))) v z) ^ (w v ((y v z) ^ (z v u))) = (x ^ ((y v z) ^ (z v u))) v z. [para(11(a,1),22(a,1,1,2)),rewrite([11(18)])]. given #86 (T,wt=11): 368 x v (y ^ (z ^ (x ^ u))) = x. [para(8(a,1),68(a,1,1)),rewrite([8(7)])]. given #87 (T,wt=11): 376 x v (y ^ ((x ^ z) ^ u)) = x. [para(119(a,1),68(a,1,1)),rewrite([119(7)])]. given #88 (T,wt=11): 377 x v (y ^ (z ^ (u ^ x))) = x. [para(124(a,1),68(a,1,1)),rewrite([124(7)])]. given #89 (T,wt=11): 381 x v (y ^ ((z ^ x) ^ u)) = x. [para(192(a,1),68(a,1,1)),rewrite([192(7)])]. given #90 (A,wt=15): 55 (x v y) v ((z ^ y) v (y ^ u)) = x v y. [para(22(a,1),19(a,1,2))]. given #91 (T,wt=11): 390 x ^ ((y v x) ^ (z v x)) = x. [para(80(a,1),66(a,1,1)),rewrite([80(8)])]. given #92 (T,wt=11): 429 x v ((x ^ y) v (x ^ z)) = x. [para(66(a,1),88(a,1,2,1))]. given #93 (T,wt=11): 430 x v ((y ^ x) v (z ^ x)) = x. [para(71(a,1),88(a,1,2,2))]. given #94 (T,wt=11): 454 (x ^ ((y ^ z) ^ u)) v y = y. [para(42(a,1),78(a,1,1))]. given #95 (A,wt=21): 57 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(20(a,1),22(a,1,1,1)),rewrite([20(8)])]. given #96 (T,wt=11): 458 (x ^ (y ^ (z ^ u))) v z = z. [para(42(a,1),149(a,1,1,2))]. given #97 (T,wt=11): 459 (x ^ ((y ^ z) ^ u)) v z = z. [para(42(a,1),149(a,1,1))]. given #98 (T,wt=11): 461 x v ((y ^ (x ^ z)) ^ u) = x. [para(42(a,1),192(a,1,2,1))]. given #99 (T,wt=11): 462 ((x ^ (y ^ z)) ^ u) v y = y. [para(42(a,1),222(a,1,1,1))]. given #100 (A,wt=15): 58 ((x ^ y) v (y ^ z)) v (u v y) = u v y. [para(22(a,1),21(a,1,1))]. given #101 (T,wt=11): 473 x ^ ((x v y) ^ (x v z)) = x. [para(89(a,1),66(a,1,1)),rewrite([89(8)])]. given #102 (T,wt=11): 511 ((x ^ y) v (z ^ x)) v x = x. [para(71(a,1),120(a,1,1,2))]. given #103 (T,wt=11): 564 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. % Operation v is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 4 at 0.32 (+ 0.01) seconds: commute_join. % Length of proof is 16. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 103. 1 x v y = y v x # answer(commute_join) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 12 c2 v c1 != c1 v c2 # answer(commute_join). [deny(1)]. 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. 34 (x v y) ^ y = y. [para(9(a,1),11(a,1,1))]. 43 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(20(a,1),10(a,1,1,1))]. 61 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 91 (x v y) ^ x = x. [para(61(a,1),34(a,1,1))]. 564 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. 1933 x v y = y v x. [para(564(a,1),61(a,1,1)),rewrite([564(3),564(4)])]. 1934 $F # answer(commute_join). [resolve(1933,a,12,a)]. ============================== end of proof ========================== % Redundant proof: 2250 $F # answer(commute_join). [back_rewrite(12),rewrite([1933(3)]),xx(a)]. % Disable descendants (x means already disabled): 12x given #104 (T,wt=7): 1933 x v y = y v x. [para(564(a,1),61(a,1,1)),rewrite([564(3),564(4)])]. given #105 (A,wt=33): 59 (((x ^ y) v (y ^ z)) v ((u v y) ^ w)) ^ (v5 v (u v y)) = ((x ^ y) v (y ^ z)) v ((u v y) ^ w). [para(22(a,1),22(a,1,1,1)),rewrite([22(14)])]. given #106 (T,wt=11): 646 x ^ ((y v (z v x)) v u) = x. [para(79(a,1),160(a,1,1)),rewrite([79(7)])]. given #107 (T,wt=11): 647 x ^ (((x v y) v z) v u) = x. [para(87(a,1),160(a,1,1)),rewrite([87(7)])]. given #108 (T,wt=11): 650 x ^ (((y v x) v z) v u) = x. [para(154(a,1),160(a,1,1)),rewrite([154(7)])]. given #109 (T,wt=11): 699 x v (((x ^ y) ^ z) ^ u) = x. [para(119(a,1),189(a,1,1)),rewrite([119(7)])]. given #110 (A,wt=21): 63 (x v ((x v y) ^ z)) ^ (u v (x v y)) = x v ((x v y) ^ z). [para(23(a,1),22(a,1,1,1)),rewrite([23(8)])]. given #111 (T,wt=11): 700 x v ((y ^ (z ^ x)) ^ u) = x. [para(124(a,1),189(a,1,1)),rewrite([124(7)])]. given #112 (T,wt=11): 703 x v (((y ^ x) ^ z) ^ u) = x. [para(192(a,1),189(a,1,1)),rewrite([192(7)])]. given #113 (T,wt=11): 1261 (x ^ y) v (y ^ x) = x ^ y. [para(356(a,1),30(a,1,2))]. given #114 (T,wt=11): 1417 x ^ ((x v y) ^ (z v x)) = x. [back_rewrite(387),rewrite([1262(4)])]. given #115 (A,wt=13): 69 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),34(a,1,1))]. given #116 (T,wt=11): 1690 x v ((x ^ y) v (z ^ x)) = x. [para(71(a,1),429(a,1,2,2))]. given #117 (T,wt=11): 1931 (x v y) ^ (y v x) = x v y. [para(564(a,1),23(a,1,2))]. given #118 (T,wt=13): 152 x v (y v (z v x)) = y v (z v x). [para(79(a,1),21(a,1,1))]. given #119 (T,wt=13): 159 x v ((x v y) v z) = (x v y) v z. [para(87(a,1),21(a,1,1))]. given #120 (A,wt=17): 85 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(11(a,1),81(a,1,1))]. given #121 (T,wt=13): 188 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(119(a,1),34(a,1,1))]. given #122 (T,wt=13): 200 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(124(a,1),34(a,1,1))]. given #123 (T,wt=13): 261 x v ((y v x) v z) = (y v x) v z. [para(154(a,1),21(a,1,1))]. given #124 (T,wt=13): 297 (x v y) v (z ^ (y ^ u)) = x v y. [para(78(a,1),40(a,1,1,2)),rewrite([78(7)])]. given #125 (A,wt=19): 90 ((x ^ y) v (y ^ z)) ^ (y v u) = (x ^ y) v (y ^ z). [para(61(a,1),22(a,1,2))]. given #126 (T,wt=13): 303 (x v y) v ((y ^ z) ^ u) = x v y. [para(148(a,1),40(a,1,1,2)),rewrite([148(7)])]. given #127 (T,wt=13): 305 (x v y) v (z ^ (u ^ y)) = x v y. [para(149(a,1),40(a,1,1,2)),rewrite([149(7)])]. given #128 (T,wt=13): 314 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(192(a,1),34(a,1,1))]. given #129 (T,wt=13): 329 (x v y) v ((z ^ y) ^ u) = x v y. [para(222(a,1),40(a,1,1,2)),rewrite([222(7)])]. given #130 (A,wt=21): 93 (x v (y v z)) v (y v ((x v (y v z)) ^ u)) = x v (y v z). [para(25(a,1),61(a,1,1)),rewrite([25(14)])]. given #131 (T,wt=13): 346 (x ^ (y ^ z)) v (u v z) = u v z. [para(46(a,1),149(a,1,1,2))]. given #132 (T,wt=13): 347 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(40(a,1),46(a,1,2))]. given #133 (T,wt=13): 349 ((x ^ y) ^ z) v (u v y) = u v y. [para(46(a,1),222(a,1,1,1))]. given #134 (T,wt=13): 350 (x ^ y) ^ (z v (u v y)) = x ^ y. [para(46(a,1),46(a,1,1)),rewrite([46(7)])]. given #135 (A,wt=27): 94 (x ^ ((y ^ (x ^ z)) v u)) v (w ^ (y ^ (x ^ z))) = x ^ ((y ^ (x ^ z)) v u). [para(8(a,1),29(a,1,1,1)),rewrite([8(11)])]. given #136 (T,wt=13): 378 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(68(a,1),154(a,1,2,1))]. given #137 (T,wt=13): 380 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(68(a,1),157(a,1,1,2))]. given #138 (T,wt=13): 382 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(68(a,1),265(a,1,1,1))]. given #139 (T,wt=13): 404 x ^ (y v ((z v x) ^ (x v u))) = x. [para(11(a,1),83(a,1,1)),rewrite([11(9)])]. given #140 (A,wt=21): 98 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(19(a,1),29(a,1,1,1)),rewrite([19(8)])]. given #141 (T,wt=13): 413 (x ^ (y ^ z)) v (u v y) = u v y. [para(83(a,1),149(a,1,1,2))]. given #142 (T,wt=13): 414 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(40(a,1),83(a,1,2))]. given #143 (T,wt=13): 416 ((x ^ y) ^ z) v (u v x) = u v x. [para(83(a,1),222(a,1,1,1))]. given #144 (T,wt=13): 417 (x ^ y) ^ (z v (u v x)) = x ^ y. [para(83(a,1),46(a,1,1)),rewrite([83(7)])]. given #145 (A,wt=15): 99 (x ^ y) ^ ((z v y) ^ (y v u)) = x ^ y. [para(29(a,1),20(a,1,2))]. given #146 (T,wt=13): 420 x ^ (y v ((z v x) ^ (u v x))) = x. [para(80(a,1),83(a,1,1)),rewrite([80(9)])]. given #147 (T,wt=13): 444 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(88(a,1),68(a,1,1)),rewrite([88(9)])]. given #148 (T,wt=13): 460 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(165(a,1),42(a,1,1,2)),rewrite([165(7)])]. given #149 (T,wt=13): 465 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [para(42(a,1),88(a,1,2,1))]. given #150 (A,wt=31): 102 ((x ^ (y ^ z)) v ((y ^ z) ^ u)) ^ ((w v z) ^ (z v v5)) = (x ^ (y ^ z)) v ((y ^ z) ^ u). [para(29(a,1),22(a,1,2))]. given #151 (T,wt=13): 485 x ^ (y v ((x v z) ^ (x v u))) = x. [para(89(a,1),83(a,1,1)),rewrite([89(9)])]. given #152 (T,wt=13): 498 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(113(a,1),157(a,1,1,2))]. given #153 (T,wt=13): 499 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(113(a,1),265(a,1,1,1))]. given #154 (T,wt=13): 500 (x v y) v (z ^ (u ^ x)) = x v y. [para(113(a,1),68(a,1,1)),rewrite([113(7)])]. given #155 (A,wt=31): 103 ((x v (y v z)) ^ ((y v z) v u)) v ((w ^ z) v (z ^ v5)) = (x v (y v z)) ^ ((y v z) v u). [para(22(a,1),29(a,1,2))]. given #156 (T,wt=13): 503 (x v y) v (z ^ (x ^ u)) = x v y. [para(42(a,1),113(a,1,2))]. given #157 (T,wt=13): 533 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(120(a,1),113(a,1,1)),rewrite([120(9)])]. given #158 (T,wt=13): 548 x ^ ((y v (x v z)) ^ (x v u)) = x. [para(40(a,1),121(a,1,2,1))]. given #159 (T,wt=13): 605 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(126(a,1),113(a,1,1)),rewrite([126(9)])]. given #160 (A,wt=21): 105 (x ^ ((x ^ y) v z)) v (u ^ (x ^ y)) = x ^ ((x ^ y) v z). [para(30(a,1),29(a,1,1,1)),rewrite([30(8)])]. given #161 (T,wt=13): 621 (x ^ (y ^ z)) v (z v u) = z v u. [para(113(a,1),144(a,1,2)),rewrite([113(7)])]. given #162 (T,wt=13): 635 (x ^ (y ^ z)) v (y v u) = y v u. [para(42(a,1),147(a,1,1))]. given #163 (T,wt=13): 651 (x v y) v ((z ^ x) ^ u) = x v y. [para(160(a,1),192(a,1,2,1))]. given #164 (T,wt=13): 652 ((x ^ y) ^ z) v (y v u) = y v u. [para(160(a,1),222(a,1,1,1))]. given #165 (A,wt=15): 106 ((x v y) ^ (y v z)) ^ (u ^ y) = u ^ y. [para(29(a,1),34(a,1,1))]. given #166 (T,wt=13): 653 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(83(a,1),160(a,1,1)),rewrite([83(7)])]. given #167 (T,wt=13): 656 x ^ (((y v x) ^ (x v z)) v u) = x. [para(121(a,1),160(a,1,1)),rewrite([121(9)])]. given #168 (T,wt=13): 670 x ^ ((y v x) ^ (z v (x v u))) = x. [para(47(a,1),121(a,1,2,2))]. given #169 (T,wt=13): 681 (x v y) v ((x ^ z) ^ u) = x v y. [para(163(a,1),192(a,1,2,1))]. given #170 (A,wt=19): 108 (x ^ y) v ((z v y) ^ (y v u)) = (z v y) ^ (y v u). [para(29(a,1),49(a,1,2)),rewrite([29(10)])]. given #171 (T,wt=13): 682 ((x ^ y) ^ z) v (x v u) = x v u. [para(163(a,1),222(a,1,1,1))]. given #172 (T,wt=13): 685 x ^ (((y v x) ^ (z v x)) v u) = x. [para(80(a,1),163(a,1,1)),rewrite([80(9)])]. given #173 (T,wt=13): 687 x ^ (((x v y) ^ (x v z)) v u) = x. [para(89(a,1),163(a,1,1)),rewrite([89(9)])]. given #174 (T,wt=13): 693 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(163(a,1),160(a,1,1)),rewrite([163(7)])]. given #175 (A,wt=19): 109 ((x v y) ^ (z v y)) v (u ^ y) = (x v y) ^ (z v y). [para(49(a,1),29(a,1,1,2)),rewrite([49(8)])]. given #176 (T,wt=13): 702 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(189(a,1),157(a,1,1,2))]. given #177 (T,wt=13): 704 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(189(a,1),265(a,1,1,1))]. given #178 (T,wt=13): 709 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(88(a,1),189(a,1,1)),rewrite([88(9)])]. given #179 (T,wt=13): 719 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(191(a,1),157(a,1,1,2))]. given #180 (A,wt=19): 111 ((x v y) ^ (x v z)) v (u ^ x) = (x v y) ^ (x v z). [para(61(a,1),29(a,1,1,1)),rewrite([61(7)])]. given #181 (T,wt=13): 720 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(191(a,1),265(a,1,1,1))]. given #182 (T,wt=13): 726 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(120(a,1),191(a,1,1)),rewrite([120(9)])]. given #183 (T,wt=13): 729 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(126(a,1),191(a,1,1)),rewrite([126(9)])]. given #184 (T,wt=13): 799 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(218(a,1),41(a,1,1,2))]. given #185 (A,wt=33): 112 (((x v y) ^ (y v z)) ^ ((u ^ y) v w)) v (v5 ^ (u ^ y)) = ((x v y) ^ (y v z)) ^ ((u ^ y) v w). [para(29(a,1),29(a,1,1,1)),rewrite([29(14)])]. given #186 (T,wt=13): 815 (x ^ (y v z)) ^ (y ^ x) = y ^ x. [para(221(a,1),41(a,1,1,2))]. given #187 (T,wt=13): 839 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. given #188 (T,wt=13): 906 (x v (y ^ z)) v (y v x) = y v x. [para(282(a,1),43(a,1,1,2))]. given #189 (T,wt=13): 920 x ^ (y v (((x v z) v u) v w)) = x. [para(40(a,1),291(a,1,2))]. given #190 (A,wt=17): 115 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(10(a,1),91(a,1,1))]. given #191 (T,wt=13): 924 x ^ (y v (z v ((x v u) v w))) = x. [para(291(a,1),46(a,1,1)),rewrite([291(9)])]. given #192 (T,wt=13): 938 x ^ ((y v ((x v z) v u)) v w) = x. [para(291(a,1),160(a,1,1)),rewrite([291(9)])]. given #193 (T,wt=13): 939 x ^ (y v ((z v (x v u)) v w)) = x. [para(47(a,1),291(a,1,2,2,1))]. given #194 (T,wt=13): 958 x ^ (y v (z v (u v (x v w)))) = x. [para(298(a,1),46(a,1,1)),rewrite([298(9)])]. given #195 (A,wt=15): 117 (x v y) v (y v (x v z)) = y v (x v z). [para(91(a,1),25(a,1,1,2))]. given #196 (T,wt=11): 7006 x v (y v (z ^ x)) = x v y. [para(839(a,1),117(a,1,2)),rewrite([1933(5),6927(5),839(7)])]. given #197 (T,wt=11): 7008 x v (y v (x ^ z)) = x v y. [para(906(a,1),117(a,1,2)),rewrite([1933(5),6927(5),906(7)])]. given #198 (T,wt=11): 7074 x v ((y ^ x) v z) = x v z. [para(1933(a,1),7006(a,1,2))]. ============================== PROOF ================================= % Proof 5 at 1.94 (+ 0.04) seconds: assoc_join. % Length of proof is 40. % Level of proof is 13. % Maximum clause weight is 21. % Given clauses 198. 2 (x v y) v z = x v (y v z) # answer(assoc_join) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 13 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [deny(2)]. 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. 21 (x ^ y) v y = y. [para(8(a,1),10(a,1,1))]. 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. 25 (x v ((y v (x v z)) ^ u)) v (y v (x v z)) = y v (x v z). [para(9(a,1),10(a,1,1,1))]. 34 (x v y) ^ y = y. [para(9(a,1),11(a,1,1))]. 43 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(20(a,1),10(a,1,1,1))]. 47 x v (y v (x v z)) = y v (x v z). [para(9(a,1),21(a,1,1))]. 61 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 62 x v (x v y) = x v y. [para(23(a,1),21(a,1,1))]. 71 x ^ (y ^ x) = y ^ x. [para(19(a,1),34(a,1,1))]. 87 x ^ ((x v y) v z) = x. [para(61(a,1),9(a,1,2))]. 91 (x v y) ^ x = x. [para(61(a,1),34(a,1,1))]. 117 (x v y) v (y v (x v z)) = y v (x v z). [para(91(a,1),25(a,1,1,2))]. 165 ((x v y) v z) ^ x = x. [para(87(a,1),71(a,1,2)),rewrite([87(6)])]. 278 (x v y) ^ (z ^ x) = z ^ x. [para(21(a,1),165(a,1,1,1))]. 564 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. 572 (x v y) v ((y v z) v x) = (y v z) v x. [para(165(a,1),43(a,1,1,2))]. 839 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. 1931 (x v y) ^ (y v x) = x v y. [para(564(a,1),23(a,1,2))]. 1933 x v y = y v x. [para(564(a,1),61(a,1,1)),rewrite([564(3),564(4)])]. 2249 c5 v (c3 v c4) != c3 v (c4 v c5) # answer(assoc_join). [back_rewrite(13),rewrite([1933(5)])]. 6927 (x v y) v (x v (y v z)) = x v (y v z). [para(47(a,1),117(a,1,2)),rewrite([47(7)])]. 6945 (x v y) v ((x v z) v y) = y v (x v z). [para(1933(a,1),117(a,1,2))]. 7006 x v (y v (z ^ x)) = x v y. [para(839(a,1),117(a,1,2)),rewrite([1933(5),6927(5),839(7)])]. 7052 (x v y) v (z v y) = (x v y) v z. [para(20(a,1),7006(a,1,2,2))]. 7054 (x v y) v (z v x) = (x v y) v z. [para(23(a,1),7006(a,1,2,2))]. 7074 x v ((y ^ x) v z) = x v z. [para(1933(a,1),7006(a,1,2))]. 7119 (x v y) v (x v z) = y v (x v z). [back_rewrite(6945),rewrite([7052(4)])]. 7177 (x v y) v (y v z) = (y v z) v x. [back_rewrite(572),rewrite([7054(4)])]. 7204 (x v y) v z = y v (x v z). [para(23(a,1),7074(a,1,2,1)),rewrite([7119(3)]),flip(a)]. 7237 x v (y v z) = y v (x v z). [para(1931(a,1),7074(a,1,2,1)),rewrite([7204(3),7204(4),62(3),47(3),7204(4)])]. 7279 x v (y v z) = z v (x v y). [back_rewrite(7177),rewrite([7237(3),7204(2),62(3),7204(4)])]. 7280 $F # answer(assoc_join). [resolve(7279,a,2249,a(flip))]. ============================== end of proof ========================== % Redundant proof: 8617 $F # answer(assoc_join). [back_rewrite(2249),rewrite([7237(5),1933(4)]),xx(a)]. % Disable descendants (x means already disabled): 13x 2249x given #199 (T,wt=11): 7182 x v ((x ^ y) v z) = x v z. [para(1933(a,1),7008(a,1,2))]. given #200 (A,wt=25): 118 (x v (y v z)) ^ (y v ((x v (y v z)) ^ u)) = y v ((x v (y v z)) ^ u). [para(25(a,1),91(a,1,1))]. given #201 (T,wt=11): 7204 (x v y) v z = y v (x v z). [para(23(a,1),7074(a,1,2,1)),rewrite([7119(3)]),flip(a)]. given #202 (T,wt=11): 7237 x v (y v z) = y v (x v z). [para(1931(a,1),7074(a,1,2,1)),rewrite([7204(3),7204(4),62(3),47(3),7204(4)])]. given #203 (T,wt=11): 7257 x v (y v z) = z v (y v x). [para(103(a,1),7074(a,1,2)),rewrite([7204(2),7204(6),19(8),7204(4),7204(8),7008(7),19(5),7204(4)])]. given #204 (T,wt=11): 7279 x v (y v z) = z v (x v y). [back_rewrite(7177),rewrite([7237(3),7204(2),62(3),7204(4)])]. given #205 (A,wt=19): 122 ((x ^ y) v (x ^ z)) ^ (u v x) = (x ^ y) v (x ^ z). [para(66(a,1),22(a,1,1,1)),rewrite([66(7)])]. given #206 (T,wt=13): 1244 x ^ (y v (z v (u v (w v x)))) = x. [para(342(a,1),46(a,1,1)),rewrite([342(9)])]. given #207 (T,wt=13): 1258 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(356(a,1),8(a,1,2,2))]. given #208 (T,wt=13): 1265 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(356(a,1),78(a,1,1,2))]. given #209 (T,wt=13): 1266 (x ^ y) v ((y ^ x) ^ z) = x ^ y. [para(356(a,1),119(a,1,2,1))]. given #210 (A,wt=19): 123 ((x v y) ^ (y v z)) v (y ^ u) = (x v y) ^ (y v z). [para(66(a,1),29(a,1,2))]. given #211 (T,wt=13): 1270 (x ^ y) ^ (z v (y ^ x)) = x ^ y. [para(356(a,1),83(a,1,1)),rewrite([356(7)])]. given #212 (T,wt=13): 1272 (x ^ y) ^ ((y ^ x) v z) = x ^ y. [para(356(a,1),163(a,1,1)),rewrite([356(7)])]. given #213 (T,wt=13): 1343 (x ^ y) ^ ((x v z) ^ y) = x ^ y. [back_rewrite(770),rewrite([1262(4)])]. given #214 (T,wt=13): 1345 (x ^ y) ^ ((z v x) ^ y) = x ^ y. [back_rewrite(768),rewrite([1262(4)])]. given #215 (A,wt=19): 127 ((x ^ y) v (z ^ y)) ^ (u v y) = (x ^ y) v (z ^ y). [para(71(a,1),22(a,1,1,2)),rewrite([71(8)])]. given #216 (T,wt=13): 1358 x ^ ((y v x) ^ (z v (u v x))) = x. [back_rewrite(751),rewrite([1262(5)])]. given #217 (T,wt=13): 1372 x ^ ((x v y) ^ (z v (x v u))) = x. [back_rewrite(668),rewrite([1262(5)])]. given #218 (T,wt=13): 1412 x ^ ((y v (x v z)) ^ (u v x)) = x. [back_rewrite(398),rewrite([1262(5)])]. given #219 (T,wt=13): 1421 x ^ ((y v (z v x)) ^ (x v u)) = x. [back_rewrite(360),rewrite([1262(5)])]. given #220 (A,wt=19): 128 (x v y) ^ ((z ^ y) v (y ^ u)) = (z ^ y) v (y ^ u). [para(22(a,1),71(a,1,2)),rewrite([22(10)])]. given #221 (T,wt=13): 1534 x v (y ^ (z ^ (u ^ (x ^ w)))) = x. [para(368(a,1),68(a,1,1)),rewrite([368(9)])]. given #222 (T,wt=13): 1539 x v ((y ^ (z ^ (x ^ u))) ^ w) = x. [para(368(a,1),189(a,1,1)),rewrite([368(9)])]. given #223 (T,wt=13): 1555 x v (y ^ (z ^ ((x ^ u) ^ w))) = x. [para(376(a,1),68(a,1,1)),rewrite([376(9)])]. given #224 (T,wt=13): 1559 x v ((y ^ ((x ^ z) ^ u)) ^ w) = x. [para(376(a,1),189(a,1,1)),rewrite([376(9)])]. given #225 (A,wt=25): 135 (x ^ (y ^ z)) v (y ^ ((x ^ (y ^ z)) v u)) = y ^ ((x ^ (y ^ z)) v u). [para(32(a,1),81(a,1,1))]. given #226 (T,wt=13): 1581 x v (y ^ (z ^ (u ^ (w ^ x)))) = x. [para(377(a,1),68(a,1,1)),rewrite([377(9)])]. given #227 (T,wt=13): 1586 x v ((y ^ (z ^ (u ^ x))) ^ w) = x. [para(377(a,1),189(a,1,1)),rewrite([377(9)])]. given #228 (T,wt=13): 1610 x v (y ^ (z ^ ((u ^ x) ^ w))) = x. [para(381(a,1),68(a,1,1)),rewrite([381(9)])]. given #229 (T,wt=13): 1615 x v ((y ^ ((z ^ x) ^ u)) ^ w) = x. [para(381(a,1),189(a,1,1)),rewrite([381(9)])]. given #230 (A,wt=15): 136 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(81(a,1),32(a,1,1,2))]. given #231 (T,wt=11): 10430 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite([1262(5),10395(5),799(7)])]. given #232 (T,wt=11): 10432 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite([1262(5),10395(5),815(7)])]. given #233 (T,wt=11): 10468 x ^ ((y v x) ^ z) = x ^ z. [para(1262(a,1),10430(a,1,2))]. ============================== PROOF ================================= % Proof 6 at 3.54 (+ 0.04) seconds: all_six. % Length of proof is 73. % Level of proof is 14. % Maximum clause weight is 50. % Given clauses 233. 7 x v y = y v x & (x v y) v z = x v (y v z) & x ^ y = y ^ x & (x ^ y) ^ z = x ^ (y ^ z) & x ^ (x v y) = x & x v (x ^ y) = x # label(all_six) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 18 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) | c15 ^ (c15 v c16) != c15 | c15 v (c15 ^ c16) != c15 # label(all_six) # answer(all_six). [deny(7)]. 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. 21 (x ^ y) v y = y. [para(8(a,1),10(a,1,1))]. 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. 25 (x v ((y v (x v z)) ^ u)) v (y v (x v z)) = y v (x v z). [para(9(a,1),10(a,1,1,1))]. 27 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) | c15 v (c15 ^ c16) != c15 # answer(all_six). [back_rewrite(18),rewrite([23(41)]),xx(e)]. 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. 32 (x ^ ((y ^ (x ^ z)) v u)) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),11(a,1,1,1))]. 34 (x v y) ^ y = y. [para(9(a,1),11(a,1,1))]. 38 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c16 ^ c15 != c15 ^ c16 | (c15 ^ c16) ^ c17 != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(27),rewrite([30(41)]),xx(e)]. 41 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(19(a,1),11(a,1,1,1))]. 43 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(20(a,1),10(a,1,1,1))]. 47 x v (y v (x v z)) = y v (x v z). [para(9(a,1),21(a,1,1))]. 49 x v (y v x) = y v x. [para(20(a,1),21(a,1,1))]. 61 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 62 x v (x v y) = x v y. [para(23(a,1),21(a,1,1))]. 66 (x ^ y) ^ x = x ^ y. [para(30(a,1),20(a,1,2))]. 69 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),34(a,1,1))]. 71 x ^ (y ^ x) = y ^ x. [para(19(a,1),34(a,1,1))]. 78 (x ^ (y ^ z)) v y = y. [para(8(a,1),49(a,1,2)),rewrite([8(6)])]. 81 (x ^ y) v x = x. [para(30(a,1),49(a,1,2)),rewrite([30(4)])]. 87 x ^ ((x v y) v z) = x. [para(61(a,1),9(a,1,2))]. 91 (x v y) ^ x = x. [para(61(a,1),34(a,1,1))]. 117 (x v y) v (y v (x v z)) = y v (x v z). [para(91(a,1),25(a,1,1,2))]. 124 x v (y ^ (z ^ x)) = x. [para(71(a,1),8(a,1,2,2))]. 136 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(81(a,1),32(a,1,1,2))]. 148 ((x ^ y) ^ z) v x = x. [para(66(a,1),78(a,1,1))]. 165 ((x v y) v z) ^ x = x. [para(87(a,1),71(a,1,2)),rewrite([87(6)])]. 200 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(124(a,1),34(a,1,1))]. 218 (x ^ y) v (z v x) = z v x. [para(34(a,1),148(a,1,1,1))]. 221 (x ^ y) v (x v z) = x v z. [para(91(a,1),148(a,1,1,1))]. 278 (x v y) ^ (z ^ x) = z ^ x. [para(21(a,1),165(a,1,1,1))]. 356 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 364 (x ^ y) ^ ((y ^ z) ^ x) = (y ^ z) ^ x. [para(148(a,1),41(a,1,1,2))]. 564 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. 799 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(218(a,1),41(a,1,1,2))]. 815 (x ^ (y v z)) ^ (y ^ x) = y ^ x. [para(221(a,1),41(a,1,1,2))]. 839 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. 1261 (x ^ y) v (y ^ x) = x ^ y. [para(356(a,1),30(a,1,2))]. 1262 x ^ y = y ^ x. [para(356(a,1),81(a,1,1)),rewrite([1261(3)])]. 1472 c16 v c15 != c15 v c16 | (c15 v c16) v c17 != c15 v (c16 v c17) | c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(38),rewrite([1262(21),1262(30)]),xx(c)]. 1931 (x v y) ^ (y v x) = x v y. [para(564(a,1),23(a,1,2))]. 1933 x v y = y v x. [para(564(a,1),61(a,1,1)),rewrite([564(3),564(4)])]. 2070 c17 v (c15 v c16) != c15 v (c16 v c17) | c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(1472),rewrite([1933(3),1933(12)]),xx(a)]. 6927 (x v y) v (x v (y v z)) = x v (y v z). [para(47(a,1),117(a,1,2)),rewrite([47(7)])]. 6945 (x v y) v ((x v z) v y) = y v (x v z). [para(1933(a,1),117(a,1,2))]. 7006 x v (y v (z ^ x)) = x v y. [para(839(a,1),117(a,1,2)),rewrite([1933(5),6927(5),839(7)])]. 7052 (x v y) v (z v y) = (x v y) v z. [para(20(a,1),7006(a,1,2,2))]. 7074 x v ((y ^ x) v z) = x v z. [para(1933(a,1),7006(a,1,2))]. 7119 (x v y) v (x v z) = y v (x v z). [back_rewrite(6945),rewrite([7052(4)])]. 7204 (x v y) v z = y v (x v z). [para(23(a,1),7074(a,1,2,1)),rewrite([7119(3)]),flip(a)]. 7237 x v (y v z) = y v (x v z). [para(1931(a,1),7074(a,1,2,1)),rewrite([7204(3),7204(4),62(3),47(3),7204(4)])]. 8618 c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(2070),rewrite([7237(5),1933(4)]),xx(a)]. 10395 (x ^ y) ^ (x ^ (y ^ z)) = x ^ (y ^ z). [para(1262(a,1),136(a,1,1))]. 10430 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite([1262(5),10395(5),799(7)])]. 10431 ((x ^ (y v z)) ^ u) ^ (u ^ (y ^ x)) = u ^ (y ^ x). [para(815(a,1),136(a,1,2,2)),rewrite([815(10)])]. 10432 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite([1262(5),10395(5),815(7)])]. 10463 (x ^ y) ^ (z ^ x) = (x ^ y) ^ z. [para(30(a,1),10430(a,1,2,2))]. 10468 x ^ ((y v x) ^ z) = x ^ z. [para(1262(a,1),10430(a,1,2))]. 10625 (x ^ y) ^ (y ^ z) = (y ^ z) ^ x. [back_rewrite(364),rewrite([10463(4)])]. 10627 x ^ ((x v y) ^ z) = x ^ z. [para(1262(a,1),10432(a,1,2))]. 10644 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(19(a,1),10468(a,1,2,1))]. 10645 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(30(a,1),10468(a,1,2,1))]. 10692 (x ^ y) ^ z = y ^ (x ^ z). [para(10468(a,1),136(a,1,2,2)),rewrite([10644(4),10645(3),10468(5)])]. 10695 x ^ (y ^ z) = z ^ (y ^ x). [back_rewrite(10625),rewrite([10692(3),69(3),10692(4)])]. 10696 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(10431),rewrite([10692(3),10695(6),200(5),10692(5),10627(4),69(3)])]. 10697 $F # answer(all_six). [resolve(10696,a,8618,a(flip))]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 7 at 3.54 (+ 0.04) seconds: assoc_meet. % Length of proof is 49. % Level of proof is 14. % Maximum clause weight is 21. % Given clauses 233. 4 (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet) # label(non_clause) # label(goal). [goal]. 8 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [assumption]. 9 x ^ (y v (x v z)) = x # label(McKenzie_2). [assumption]. 10 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [assumption]. 11 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [assumption]. 15 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [deny(4)]. 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. 20 x ^ (y v x) = x. [para(8(a,1),9(a,1,2,2))]. 21 (x ^ y) v y = y. [para(8(a,1),10(a,1,1))]. 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. 32 (x ^ ((y ^ (x ^ z)) v u)) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),11(a,1,1,1))]. 34 (x v y) ^ y = y. [para(9(a,1),11(a,1,1))]. 41 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(19(a,1),11(a,1,1,1))]. 49 x v (y v x) = y v x. [para(20(a,1),21(a,1,1))]. 61 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 66 (x ^ y) ^ x = x ^ y. [para(30(a,1),20(a,1,2))]. 69 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),34(a,1,1))]. 71 x ^ (y ^ x) = y ^ x. [para(19(a,1),34(a,1,1))]. 78 (x ^ (y ^ z)) v y = y. [para(8(a,1),49(a,1,2)),rewrite([8(6)])]. 81 (x ^ y) v x = x. [para(30(a,1),49(a,1,2)),rewrite([30(4)])]. 91 (x v y) ^ x = x. [para(61(a,1),34(a,1,1))]. 124 x v (y ^ (z ^ x)) = x. [para(71(a,1),8(a,1,2,2))]. 136 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(81(a,1),32(a,1,1,2))]. 148 ((x ^ y) ^ z) v x = x. [para(66(a,1),78(a,1,1))]. 200 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(124(a,1),34(a,1,1))]. 218 (x ^ y) v (z v x) = z v x. [para(34(a,1),148(a,1,1,1))]. 221 (x ^ y) v (x v z) = x v z. [para(91(a,1),148(a,1,1,1))]. 356 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 364 (x ^ y) ^ ((y ^ z) ^ x) = (y ^ z) ^ x. [para(148(a,1),41(a,1,1,2))]. 799 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(218(a,1),41(a,1,1,2))]. 815 (x ^ (y v z)) ^ (y ^ x) = y ^ x. [para(221(a,1),41(a,1,1,2))]. 1261 (x ^ y) v (y ^ x) = x ^ y. [para(356(a,1),30(a,1,2))]. 1262 x ^ y = y ^ x. [para(356(a,1),81(a,1,1)),rewrite([1261(3)])]. 1473 c10 ^ (c8 ^ c9) != c8 ^ (c9 ^ c10) # answer(assoc_meet). [back_rewrite(15),rewrite([1262(5)])]. 10395 (x ^ y) ^ (x ^ (y ^ z)) = x ^ (y ^ z). [para(1262(a,1),136(a,1,1))]. 10430 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite([1262(5),10395(5),799(7)])]. 10431 ((x ^ (y v z)) ^ u) ^ (u ^ (y ^ x)) = u ^ (y ^ x). [para(815(a,1),136(a,1,2,2)),rewrite([815(10)])]. 10432 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite([1262(5),10395(5),815(7)])]. 10463 (x ^ y) ^ (z ^ x) = (x ^ y) ^ z. [para(30(a,1),10430(a,1,2,2))]. 10468 x ^ ((y v x) ^ z) = x ^ z. [para(1262(a,1),10430(a,1,2))]. 10625 (x ^ y) ^ (y ^ z) = (y ^ z) ^ x. [back_rewrite(364),rewrite([10463(4)])]. 10627 x ^ ((x v y) ^ z) = x ^ z. [para(1262(a,1),10432(a,1,2))]. 10644 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(19(a,1),10468(a,1,2,1))]. 10645 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(30(a,1),10468(a,1,2,1))]. 10692 (x ^ y) ^ z = y ^ (x ^ z). [para(10468(a,1),136(a,1,2,2)),rewrite([10644(4),10645(3),10468(5)])]. 10695 x ^ (y ^ z) = z ^ (y ^ x). [back_rewrite(10625),rewrite([10692(3),69(3),10692(4)])]. 10696 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(10431),rewrite([10692(3),10695(6),200(5),10692(5),10627(4),69(3)])]. 10698 $F # answer(assoc_meet). [resolve(10696,a,1473,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=233. Generated=67541. Kept=10679. proofs=7. Usable=117. Sos=5331. Demods=5131. Limbo=52, Disabled=5189. Hints=0. Kept_by_rule=0, Deleted_by_rule=0. Forward_subsumed=56857. Back_subsumed=69. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10202 (9 lex), Back_demodulated=5109. Back_unit_deleted=0. Demod_attempts=935188. Demod_rewrites=145937. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=5. Megabytes=11.64. User_CPU=3.54, System_CPU=0.04, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 11588 exit (max_proofs) Wed Feb 25 09:32:48 2009