============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13095 was started by mccune on cleo.thornwood, Mon Jun 19 16:41:20 2006 The command was "/home/mccune/bin/prover9 -f mckenzie.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mckenzie.in clauses(sos). x v (y ^ (x ^ z)) = x # label(McKenzie_1). x ^ (y v (x v z)) = x # label(McKenzie_2). ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). end_of_list. set(restrict_denials). assign(max_proofs,6). % assign(max_proofs, 6) -> set(restrict_denials). clauses(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). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c2 v c1 != c1 v c2 # answer(commute_join). (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). c7 ^ c6 != c6 ^ c7 # answer(commute_meet). (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). c11 ^ (c11 v c12) != c11 # answer(absorb_1). c13 v (c13 ^ c14) != c13 # answer(absorb_2). 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 ^ (x ^ z)) = x # label(McKenzie_1). [input]. 2 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 3 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 4 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 5 c2 v c1 != c1 v c2 # answer(commute_join). [clausify]. 6 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [clausify]. 7 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [clausify]. 8 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [clausify]. 9 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [clausify]. 10 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: % assign(max_proofs, 6). % (Horn set with more than one neg. clause) % assign(max_proofs, 6) -> set(restrict_denials). % Restrict denials; moving clauses to denials list: clauses(denials). 5 c2 v c1 != c1 v c2 # answer(commute_join). [clausify]. 6 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [clausify]. 7 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [clausify]. 8 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [clausify]. 9 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [clausify]. 10 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [clausify]. end_of_list. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, ^, v ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, ^, v ]). Unfolding symbols: (none). 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). 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. end_of_list. clauses(demodulators). 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. end_of_list. clauses(denials). 15 c2 v c1 != c1 v c2 # answer(commute_join). [clausify]. 16 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [clausify]. 17 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [clausify]. 18 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [clausify]. 19 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [clausify]. 20 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [clausify]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=9): 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. given #2 (I,wt=9): 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. given #3 (I,wt=11): 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. ============================== PROOF ================================= % Proof 1 at 0.00 (+ 0.00) seconds: absorb_1. % Length of proof is 5. % Level of proof is 2. % Maximum clause weight is 11. % Given clauses 3. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 19 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [clausify]. 25 x ^ (x v y) = x. [para(13(a,1),12(a,1,2))]. 26 $F # answer(absorb_1). [resolve(25,a,19,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 19. given #4 (I,wt=11): 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. ============================== PROOF ================================= % Proof 2 at 0.00 (+ 0.00) seconds: absorb_2. % Length of proof is 5. % Level of proof is 2. % Maximum clause weight is 11. % Given clauses 4. 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 20 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [clausify]. 30 x v (x ^ y) = x. [para(14(a,1),11(a,1,2))]. 31 $F # answer(absorb_2). [resolve(30,a,20,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 20. given #5 (T,wt=5): 28 x v x = x. [para(12(a,1),13(a,1,1,2)),demod(23(2))]. given #6 (A,wt=7): 21 x v (y ^ x) = x. [para(12(a,1),11(a,1,2,2))]. given #7 (F,wt=5): 36 x ^ x = x. [para(13(a,1),14(a,1,1,1)),demod(25(2))]. given #8 (F,wt=7): 22 x ^ (y v x) = x. [para(11(a,1),12(a,1,2,2))]. given #9 (T,wt=7): 23 (x ^ y) v y = y. [para(11(a,1),13(a,1,1))]. given #10 (T,wt=7): 25 x ^ (x v y) = x. [para(13(a,1),12(a,1,2))]. given #11 (A,wt=19): 24 ((x ^ y) v (y ^ z)) ^ (u v y) = (x ^ y) v (y ^ z). [para(13(a,1),12(a,1,2,2))]. given #12 (F,wt=7): 30 x v (x ^ y) = x. [para(14(a,1),11(a,1,2))]. given #13 (F,wt=7): 34 (x v y) ^ y = y. [para(12(a,1),14(a,1,1))]. given #14 (T,wt=9): 42 (x v y) v y = x v y. [para(22(a,1),21(a,1,2))]. given #15 (T,wt=9): 43 (x ^ y) ^ y = x ^ y. [para(21(a,1),22(a,1,2))]. given #16 (A,wt=21): 27 (x v ((y v (x v z)) ^ u)) v (y v (x v z)) = y v (x v z). [para(12(a,1),13(a,1,1,1))]. given #17 (F,wt=9): 47 x v (y v x) = y v x. [para(22(a,1),23(a,1,1))]. given #18 (F,wt=7): 79 (x ^ y) v x = x. [para(30(a,1),47(a,1,2)),demod(30(4))]. given #19 (T,wt=9): 50 (x v y) v x = x v y. [para(25(a,1),21(a,1,2))]. given #20 (T,wt=7): 89 (x v y) ^ x = x. [para(50(a,1),34(a,1,1))]. given #21 (A,wt=19): 29 ((x v y) ^ (y v z)) v (u ^ y) = (x v y) ^ (y v z). [para(14(a,1),11(a,1,2,2))]. given #22 (F,wt=9): 51 x v (x v y) = x v y. [para(25(a,1),23(a,1,1))]. given #23 (F,wt=9): 64 (x ^ y) ^ x = x ^ y. [para(30(a,1),22(a,1,2))]. given #24 (T,wt=9): 69 x ^ (y ^ x) = y ^ x. [para(21(a,1),34(a,1,1))]. given #25 (T,wt=9): 71 x ^ (x ^ y) = x ^ y. [para(30(a,1),34(a,1,1))]. given #26 (A,wt=21): 32 (x ^ ((y ^ (x ^ z)) v u)) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(11(a,1),14(a,1,1,1))]. given #27 (F,wt=9): 76 (x ^ (y ^ z)) v y = y. [para(11(a,1),47(a,1,2)),demod(11(6))]. given #28 (F,wt=9): 77 x ^ (y v (z v x)) = x. [para(47(a,1),12(a,1,2,2))]. given #29 (T,wt=9): 85 x ^ ((x v y) v z) = x. [para(50(a,1),12(a,1,2))]. given #30 (T,wt=9): 117 x v ((x ^ y) ^ z) = x. [para(64(a,1),11(a,1,2))]. given #31 (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(14(a,1),13(a,1,1,2))]. given #32 (F,wt=9): 122 x v (y ^ (z ^ x)) = x. [para(69(a,1),11(a,1,2,2))]. given #33 (F,wt=9): 123 (x v (y v z)) ^ y = y. [para(12(a,1),69(a,1,2)),demod(12(6))]. given #34 (T,wt=9): 146 ((x ^ y) ^ z) v x = x. [para(64(a,1),76(a,1,1))]. given #35 (T,wt=9): 147 (x ^ (y ^ z)) v z = z. [para(69(a,1),76(a,1,1,2))]. given #36 (A,wt=27): 37 ((x v ((y ^ z) v (z ^ u))) ^ z) ^ ((y ^ z) v (z ^ u)) = (y ^ z) v (z ^ u). [para(13(a,1),14(a,1,1,2))]. given #37 (F,wt=9): 152 x ^ ((y v x) v z) = x. [para(50(a,1),77(a,1,2))]. given #38 (F,wt=9): 155 (x v (y v z)) ^ z = z. [para(77(a,1),69(a,1,2)),demod(77(6))]. given #39 (T,wt=9): 163 ((x v y) v z) ^ x = x. [para(85(a,1),69(a,1,2)),demod(85(6))]. given #40 (T,wt=9): 171 x v ((y ^ x) ^ z) = x. [para(69(a,1),117(a,1,2,1))]. given #41 (A,wt=13): 38 (x v (y v z)) v y = x v (y v z). [para(12(a,1),21(a,1,2))]. given #42 (F,wt=9): 220 ((x ^ y) ^ z) v y = y. [para(69(a,1),146(a,1,1,1))]. given #43 (F,wt=9): 263 ((x v y) v z) ^ y = y. [para(152(a,1),69(a,1,2)),demod(152(6))]. given #44 (T,wt=11): 44 (x ^ y) ^ (z v y) = x ^ y. [para(23(a,1),12(a,1,2,2))]. given #45 (T,wt=11): 66 (x v y) v (z ^ y) = x v y. [para(34(a,1),11(a,1,2,2))]. given #46 (A,wt=15): 39 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(21(a,1),14(a,1,1,1))]. given #47 (F,wt=11): 78 ((x v y) ^ (z v y)) ^ y = y. [para(47(a,1),14(a,1,1,2))]. given #48 (F,wt=11): 81 (x ^ y) ^ (z v x) = x ^ y. [para(79(a,1),12(a,1,2,2))]. given #49 (T,wt=11): 86 x v ((y ^ x) v (x ^ z)) = x. [para(13(a,1),50(a,1,1)),demod(13(8))]. given #50 (T,wt=11): 87 ((x v y) ^ (x v z)) ^ x = x. [para(50(a,1),14(a,1,1,1))]. given #51 (A,wt=13): 40 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(11(a,1),22(a,1,2))]. given #52 (F,wt=11): 92 (x v y) v (z ^ x) = x v y. [para(89(a,1),11(a,1,2,2))]. given #53 (F,wt=11): 118 ((x ^ y) v (x ^ z)) v x = x. [para(64(a,1),13(a,1,1,1))]. given #54 (T,wt=11): 119 x ^ ((y v x) ^ (x v z)) = x. [para(14(a,1),64(a,1,1)),demod(14(8))]. given #55 (T,wt=11): 124 ((x ^ y) v (z ^ y)) v y = y. [para(69(a,1),13(a,1,1,2))]. given #56 (A,wt=15): 41 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(22(a,1),13(a,1,1,1))]. given #57 (F,wt=11): 142 (x ^ y) v (z v y) = z v y. [para(34(a,1),76(a,1,1,2))]. given #58 (F,wt=11): 144 (x ^ y) v (y v z) = y v z. [para(89(a,1),76(a,1,1,2))]. given #59 (T,wt=11): 158 (x ^ y) ^ (y v z) = x ^ y. [para(23(a,1),85(a,1,2,1))]. given #60 (T,wt=11): 161 (x ^ y) ^ (x v z) = x ^ y. [para(79(a,1),85(a,1,2,1))]. given #61 (A,wt=13): 45 x v (y v (x v z)) = y v (x v z). [para(12(a,1),23(a,1,1))]. given #62 (F,wt=11): 168 (x v y) v (y ^ z) = x v y. [para(34(a,1),117(a,1,2,1))]. given #63 (F,wt=11): 169 (x v y) v (x ^ z) = x v y. [para(89(a,1),117(a,1,2,1))]. given #64 (T,wt=11): 205 (x v y) ^ (z ^ y) = z ^ y. [para(23(a,1),123(a,1,1,2))]. given #65 (T,wt=11): 208 (x v y) ^ (y ^ z) = y ^ z. [para(79(a,1),123(a,1,1,2))]. given #66 (A,wt=15): 46 ((x v (y ^ z)) ^ z) ^ (y ^ z) = y ^ z. [para(23(a,1),14(a,1,1,2))]. given #67 (F,wt=11): 216 (x ^ y) v (z v x) = z v x. [para(34(a,1),146(a,1,1,1))]. given #68 (F,wt=11): 218 (x ^ y) v (x v z) = x v z. [para(89(a,1),146(a,1,1,1))]. given #69 (T,wt=11): 276 (x v y) ^ (z ^ x) = z ^ x. [para(23(a,1),163(a,1,1,1))]. given #70 (T,wt=11): 280 (x v y) ^ (x ^ z) = x ^ z. [para(79(a,1),163(a,1,1,1))]. given #71 (A,wt=15): 48 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(25(a,1),13(a,1,1,1))]. given #72 (F,wt=11): 300 x ^ (y v ((x v z) v u)) = x. [para(38(a,1),12(a,1,2))]. given #73 (F,wt=11): 307 x ^ (y v (z v (x v u))) = x. [para(38(a,1),77(a,1,2,2))]. given #74 (T,wt=11): 308 x ^ (y v ((z v x) v u)) = x. [para(38(a,1),77(a,1,2))]. given #75 (T,wt=11): 311 (x v ((y v z) v u)) ^ y = y. [para(38(a,1),123(a,1,1))]. given #76 (A,wt=17): 49 ((x ^ y) v (y ^ z)) ^ y = (x ^ y) v (y ^ z). [para(13(a,1),25(a,1,2))]. given #77 (F,wt=11): 315 x ^ ((y v (x v z)) v u) = x. [para(38(a,1),152(a,1,2,1))]. given #78 (F,wt=11): 316 (x v (y v (z v u))) ^ z = z. [para(38(a,1),155(a,1,1,2))]. given #79 (T,wt=11): 317 (x v ((y v z) v u)) ^ z = z. [para(38(a,1),155(a,1,1))]. given #80 (T,wt=11): 334 ((x v (y v z)) v u) ^ y = y. [para(38(a,1),263(a,1,1,1))]. given #81 (A,wt=33): 52 ((x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ v)) ^ z = (x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ v). [para(11(a,1),24(a,1,2))]. given #82 (F,wt=11): 340 x ^ (y v (z v (u v x))) = x. [para(77(a,1),44(a,1,1)),demod(77(7))]. given #83 (F,wt=11): 349 x v (y ^ (z ^ (x ^ u))) = x. [para(11(a,1),66(a,1,1)),demod(11(7))]. given #84 (T,wt=11): 356 x v (y ^ ((x ^ z) ^ u)) = x. [para(117(a,1),66(a,1,1)),demod(117(7))]. given #85 (T,wt=11): 358 x v (y ^ (z ^ (u ^ x))) = x. [para(122(a,1),66(a,1,1)),demod(122(7))]. given #86 (A,wt=27): 53 (x v ((y v (x v z)) ^ u)) ^ (v v (y v (x v z))) = x v ((y v (x v z)) ^ u). [para(12(a,1),24(a,1,1,1)),demod(12(11))]. given #87 (F,wt=11): 362 x v (y ^ ((z ^ x) ^ u)) = x. [para(171(a,1),66(a,1,1)),demod(171(7))]. given #88 (F,wt=11): 369 (x ^ y) ^ (y ^ x) = y ^ x. [para(79(a,1),39(a,1,1,2))]. % Operation ^ is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 3 at 0.17 (+ 0.01) seconds: commute_meet. % Length of proof is 16. % Level of proof is 7. % Maximum clause weight is 15. % Given clauses 88. 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 17 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [clausify]. 21 x v (y ^ x) = x. [para(12(a,1),11(a,1,2,2))]. 22 x ^ (y v x) = x. [para(11(a,1),12(a,1,2,2))]. 23 (x ^ y) v y = y. [para(11(a,1),13(a,1,1))]. 30 x v (x ^ y) = x. [para(14(a,1),11(a,1,2))]. 39 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(21(a,1),14(a,1,1,1))]. 47 x v (y v x) = y v x. [para(22(a,1),23(a,1,1))]. 79 (x ^ y) v x = x. [para(30(a,1),47(a,1,2)),demod(30(4))]. 369 (x ^ y) ^ (y ^ x) = y ^ x. [para(79(a,1),39(a,1,1,2))]. 1412 (x ^ y) v (y ^ x) = x ^ y. [para(369(a,1),30(a,1,2))]. 1413 x ^ y = y ^ x. [para(369(a,1),79(a,1,1)),demod(1412(3))]. 1414 $F # answer(commute_meet). [resolve(1413,a,17,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 17. given #89 (T,wt=7): 1413 x ^ y = y ^ x. [para(369(a,1),79(a,1,1)),demod(1412(3))]. given #90 (T,wt=11): 388 x ^ ((y v x) ^ (z v x)) = x. [para(78(a,1),64(a,1,1)),demod(78(8))]. given #91 (A,wt=21): 54 (((x ^ y) v (y ^ z)) v ((u v y) ^ v)) v (u v y) = u v y. [para(24(a,1),13(a,1,1,1))]. given #92 (F,wt=11): 427 x v ((x ^ y) v (x ^ z)) = x. [para(64(a,1),86(a,1,2,1))]. given #93 (F,wt=11): 428 x v ((y ^ x) v (z ^ x)) = x. [para(69(a,1),86(a,1,2,2))]. given #94 (T,wt=11): 454 x ^ ((x v y) ^ (x v z)) = x. [para(87(a,1),64(a,1,1)),demod(87(8))]. given #95 (T,wt=11): 473 (x ^ ((y ^ z) ^ u)) v y = y. [para(40(a,1),76(a,1,1))]. given #96 (A,wt=33): 55 ((x ^ ((y v z) ^ (z v u))) v z) ^ (v v ((y v z) ^ (z v u))) = (x ^ ((y v z) ^ (z v u))) v z. [para(14(a,1),24(a,1,1,2)),demod(14(18))]. given #97 (F,wt=11): 475 (x ^ (y ^ (z ^ u))) v z = z. [para(40(a,1),147(a,1,1,2))]. given #98 (F,wt=11): 476 (x ^ ((y ^ z) ^ u)) v z = z. [para(40(a,1),147(a,1,1))]. given #99 (T,wt=11): 480 x v ((y ^ (x ^ z)) ^ u) = x. [para(40(a,1),171(a,1,2,1))]. given #100 (T,wt=11): 481 ((x ^ (y ^ z)) ^ u) v y = y. [para(40(a,1),220(a,1,1,1))]. given #101 (A,wt=15): 56 (x v y) v ((z ^ y) v (y ^ u)) = x v y. [para(24(a,1),21(a,1,2))]. given #102 (F,wt=11): 509 ((x ^ y) v (z ^ x)) v x = x. [para(69(a,1),118(a,1,1,2))]. given #103 (F,wt=11): 587 (x v y) v (y v x) = y v x. [para(89(a,1),41(a,1,1,2))]. % Operation v is commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 4 at 0.29 (+ 0.01) seconds: commute_join. % Length of proof is 15. % Level of proof is 6. % Maximum clause weight is 15. % Given clauses 103. 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 15 c2 v c1 != c1 v c2 # answer(commute_join). [clausify]. 21 x v (y ^ x) = x. [para(12(a,1),11(a,1,2,2))]. 22 x ^ (y v x) = x. [para(11(a,1),12(a,1,2,2))]. 25 x ^ (x v y) = x. [para(13(a,1),12(a,1,2))]. 34 (x v y) ^ y = y. [para(12(a,1),14(a,1,1))]. 41 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(22(a,1),13(a,1,1,1))]. 50 (x v y) v x = x v y. [para(25(a,1),21(a,1,2))]. 89 (x v y) ^ x = x. [para(50(a,1),34(a,1,1))]. 587 (x v y) v (y v x) = y v x. [para(89(a,1),41(a,1,1,2))]. 1994 x v y = y v x. [para(587(a,1),50(a,1,1)),demod(587(3),587(4))]. 1995 $F # answer(commute_join). [resolve(1994,a,15,a)]. ============================== end of proof ========================== NOTE: Disabling denial clause 15. given #104 (T,wt=7): 1994 x v y = y v x. [para(587(a,1),50(a,1,1)),demod(587(3),587(4))]. given #105 (T,wt=11): 644 x ^ ((y v (z v x)) v u) = x. [para(77(a,1),158(a,1,1)),demod(77(7))]. given #106 (A,wt=21): 58 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(22(a,1),24(a,1,1,1)),demod(22(8))]. given #107 (F,wt=11): 645 x ^ (((x v y) v z) v u) = x. [para(85(a,1),158(a,1,1)),demod(85(7))]. given #108 (F,wt=11): 648 x ^ (((y v x) v z) v u) = x. [para(152(a,1),158(a,1,1)),demod(152(7))]. given #109 (T,wt=11): 696 x v (((x ^ y) ^ z) ^ u) = x. [para(117(a,1),168(a,1,1)),demod(117(7))]. given #110 (T,wt=11): 698 x v ((y ^ (z ^ x)) ^ u) = x. [para(122(a,1),168(a,1,1)),demod(122(7))]. given #111 (A,wt=15): 59 ((x ^ y) v (y ^ z)) v (u v y) = u v y. [para(24(a,1),23(a,1,1))]. given #112 (F,wt=11): 701 x v (((y ^ x) ^ z) ^ u) = x. [para(171(a,1),168(a,1,1)),demod(171(7))]. given #113 (F,wt=11): 1412 (x ^ y) v (y ^ x) = x ^ y. [para(369(a,1),30(a,1,2))]. given #114 (T,wt=11): 1619 x ^ ((x v y) ^ (z v x)) = x. [back_demod(385),demod(1413(4))]. given #115 (T,wt=11): 1742 x v ((x ^ y) v (z ^ x)) = x. [para(69(a,1),427(a,1,2,2))]. given #116 (A,wt=21): 60 (x v ((x v y) ^ z)) ^ (u v (x v y)) = x v ((x v y) ^ z). [para(25(a,1),24(a,1,1,1)),demod(25(8))]. given #117 (F,wt=11): 1992 (x v y) ^ (y v x) = x v y. [para(587(a,1),25(a,1,2))]. given #118 (F,wt=13): 67 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(11(a,1),34(a,1,1))]. given #119 (T,wt=13): 150 x v (y v (z v x)) = y v (z v x). [para(77(a,1),23(a,1,1))]. given #120 (T,wt=13): 157 x v ((x v y) v z) = (x v y) v z. [para(85(a,1),23(a,1,1))]. given #121 (A,wt=33): 61 (((x ^ y) v (y ^ z)) v ((u v y) ^ v)) ^ (w v (u v y)) = ((x ^ y) v (y ^ z)) v ((u v y) ^ v). [para(24(a,1),24(a,1,1,1)),demod(24(14))]. given #122 (F,wt=13): 167 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(117(a,1),34(a,1,1))]. given #123 (F,wt=13): 198 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(122(a,1),34(a,1,1))]. given #124 (T,wt=13): 259 x v ((y v x) v z) = (y v x) v z. [para(152(a,1),23(a,1,1))]. given #125 (T,wt=13): 293 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(171(a,1),34(a,1,1))]. given #126 (A,wt=17): 83 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(14(a,1),79(a,1,1))]. given #127 (F,wt=13): 306 (x v y) v (z ^ (y ^ u)) = x v y. [para(76(a,1),38(a,1,1,2)),demod(76(7))]. given #128 (F,wt=13): 312 (x v y) v ((y ^ z) ^ u) = x v y. [para(146(a,1),38(a,1,1,2)),demod(146(7))]. given #129 (T,wt=13): 313 (x v y) v (z ^ (u ^ y)) = x v y. [para(147(a,1),38(a,1,1,2)),demod(147(7))]. given #130 (T,wt=13): 327 (x v y) v ((z ^ y) ^ u) = x v y. [para(220(a,1),38(a,1,1,2)),demod(220(7))]. given #131 (A,wt=19): 88 ((x ^ y) v (y ^ z)) ^ (y v u) = (x ^ y) v (y ^ z). [para(50(a,1),24(a,1,2))]. given #132 (F,wt=13): 343 (x ^ (y ^ z)) v (u v z) = u v z. [para(44(a,1),147(a,1,1,2))]. given #133 (F,wt=13): 346 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(38(a,1),44(a,1,2))]. given #134 (T,wt=13): 347 ((x ^ y) ^ z) v (u v y) = u v y. [para(44(a,1),220(a,1,1,1))]. given #135 (T,wt=13): 348 (x ^ y) ^ (z v (u v y)) = x ^ y. [para(44(a,1),44(a,1,1)),demod(44(7))]. given #136 (A,wt=21): 91 (x v (y v z)) v (y v ((x v (y v z)) ^ u)) = x v (y v z). [para(27(a,1),50(a,1,1)),demod(27(14))]. given #137 (F,wt=13): 359 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(66(a,1),152(a,1,2,1))]. given #138 (F,wt=13): 361 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(66(a,1),155(a,1,1,2))]. given #139 (T,wt=13): 363 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(66(a,1),263(a,1,1,1))]. given #140 (T,wt=13): 402 x ^ (y v ((z v x) ^ (x v u))) = x. [para(14(a,1),81(a,1,1)),demod(14(9))]. given #141 (A,wt=17): 94 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(13(a,1),89(a,1,1))]. given #142 (F,wt=13): 409 (x ^ (y ^ z)) v (u v y) = u v y. [para(81(a,1),147(a,1,1,2))]. given #143 (F,wt=13): 413 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(38(a,1),81(a,1,2))]. given #144 (T,wt=13): 414 ((x ^ y) ^ z) v (u v x) = u v x. [para(81(a,1),220(a,1,1,1))]. given #145 (T,wt=13): 415 (x ^ y) ^ (z v (u v x)) = x ^ y. [para(81(a,1),44(a,1,1)),demod(81(7))]. given #146 (A,wt=15): 96 (x v y) v (y v (x v z)) = y v (x v z). [para(89(a,1),27(a,1,1,2))]. given #147 (F,wt=13): 418 x ^ (y v ((z v x) ^ (u v x))) = x. [para(78(a,1),81(a,1,1)),demod(78(9))]. given #148 (F,wt=13): 441 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(86(a,1),66(a,1,1)),demod(86(9))]. given #149 (T,wt=13): 466 x ^ (y v ((x v z) ^ (x v u))) = x. [para(87(a,1),81(a,1,1)),demod(87(9))]. given #150 (T,wt=13): 479 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(163(a,1),40(a,1,1,2)),demod(163(7))]. given #151 (A,wt=25): 97 (x v (y v z)) ^ (y v ((x v (y v z)) ^ u)) = y v ((x v (y v z)) ^ u). [para(27(a,1),89(a,1,1))]. given #152 (F,wt=13): 484 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [para(40(a,1),86(a,1,2,1))]. given #153 (F,wt=13): 496 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(92(a,1),155(a,1,1,2))]. given #154 (T,wt=13): 497 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(92(a,1),263(a,1,1,1))]. given #155 (T,wt=13): 498 (x v y) v (z ^ (u ^ x)) = x v y. [para(92(a,1),66(a,1,1)),demod(92(7))]. given #156 (A,wt=27): 98 (x ^ ((y ^ (x ^ z)) v u)) v (v ^ (y ^ (x ^ z))) = x ^ ((y ^ (x ^ z)) v u). [para(11(a,1),29(a,1,1,1)),demod(11(11))]. given #157 (F,wt=13): 501 (x v y) v (z ^ (x ^ u)) = x v y. [para(40(a,1),92(a,1,2))]. given #158 (F,wt=13): 531 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(118(a,1),92(a,1,1)),demod(118(9))]. given #159 (T,wt=13): 547 x ^ ((y v (x v z)) ^ (x v u)) = x. [para(38(a,1),119(a,1,2,1))]. given #160 (T,wt=13): 581 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(124(a,1),92(a,1,1)),demod(124(9))]. given #161 (A,wt=21): 102 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(21(a,1),29(a,1,1,1)),demod(21(8))]. given #162 (F,wt=13): 619 (x ^ (y ^ z)) v (z v u) = z v u. [para(92(a,1),142(a,1,2)),demod(92(7))]. given #163 (F,wt=13): 634 (x ^ (y ^ z)) v (y v u) = y v u. [para(40(a,1),144(a,1,1))]. given #164 (T,wt=13): 649 (x v y) v ((z ^ x) ^ u) = x v y. [para(158(a,1),171(a,1,2,1))]. given #165 (T,wt=13): 650 ((x ^ y) ^ z) v (y v u) = y v u. [para(158(a,1),220(a,1,1,1))]. given #166 (A,wt=15): 103 (x ^ y) ^ ((z v y) ^ (y v u)) = x ^ y. [para(29(a,1),22(a,1,2))]. given #167 (F,wt=13): 651 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(81(a,1),158(a,1,1)),demod(81(7))]. given #168 (F,wt=13): 654 x ^ (((y v x) ^ (x v z)) v u) = x. [para(119(a,1),158(a,1,1)),demod(119(9))]. given #169 (T,wt=13): 667 (x v y) v ((x ^ z) ^ u) = x v y. [para(161(a,1),171(a,1,2,1))]. given #170 (T,wt=13): 668 ((x ^ y) ^ z) v (x v u) = x v u. [para(161(a,1),220(a,1,1,1))]. given #171 (A,wt=31): 107 ((x ^ (y ^ z)) v ((y ^ z) ^ u)) ^ ((v v z) ^ (z v w)) = (x ^ (y ^ z)) v ((y ^ z) ^ u). [para(29(a,1),24(a,1,2))]. given #172 (F,wt=13): 671 x ^ (((y v x) ^ (z v x)) v u) = x. [para(78(a,1),161(a,1,1)),demod(78(9))]. given #173 (F,wt=13): 673 x ^ (((x v y) ^ (x v z)) v u) = x. [para(87(a,1),161(a,1,1)),demod(87(9))]. given #174 (T,wt=13): 679 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(161(a,1),158(a,1,1)),demod(161(7))]. given #175 (T,wt=13): 689 x ^ ((y v x) ^ (z v (x v u))) = x. [para(45(a,1),119(a,1,2,2))]. given #176 (A,wt=31): 108 ((x v (y v z)) ^ ((y v z) v u)) v ((v ^ z) v (z ^ w)) = (x v (y v z)) ^ ((y v z) v u). [para(24(a,1),29(a,1,2))]. given #177 (F,wt=13): 700 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(168(a,1),155(a,1,1,2))]. given #178 (F,wt=13): 702 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(168(a,1),263(a,1,1,1))]. given #179 (T,wt=13): 707 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(86(a,1),168(a,1,1)),demod(86(9))]. given #180 (T,wt=13): 717 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(169(a,1),155(a,1,1,2))]. given #181 (A,wt=21): 109 (x ^ ((x ^ y) v z)) v (u ^ (x ^ y)) = x ^ ((x ^ y) v z). [para(30(a,1),29(a,1,1,1)),demod(30(8))]. given #182 (F,wt=13): 718 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(169(a,1),263(a,1,1,1))]. given #183 (F,wt=13): 724 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(118(a,1),169(a,1,1)),demod(118(9))]. given #184 (T,wt=13): 726 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(124(a,1),169(a,1,1)),demod(124(9))]. given #185 (T,wt=13): 797 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(216(a,1),39(a,1,1,2))]. given #186 (A,wt=15): 110 ((x v y) ^ (y v z)) ^ (u ^ y) = u ^ y. [para(29(a,1),34(a,1,1))]. given #187 (F,wt=13): 813 (x ^ (y v z)) ^ (y ^ x) = y ^ x. [para(218(a,1),39(a,1,1,2))]. given #188 (F,wt=13): 838 (x v (y ^ z)) v (z v x) = z v x. [para(276(a,1),41(a,1,1,2))]. given #189 (T,wt=11): 6168 x v (y v (z ^ x)) = x v y. [para(838(a,1),96(a,1,2)),demod(1994(5),867(5),838(7))]. given #190 (T,wt=11): 6243 x v (y v (x ^ z)) = x v y. [para(1413(a,1),6168(a,1,2,2))]. given #191 (A,wt=19): 112 (x ^ y) v ((z v y) ^ (y v u)) = (z v y) ^ (y v u). [para(29(a,1),47(a,1,2)),demod(29(10))]. given #192 (F,wt=11): 6247 x v ((y ^ x) v z) = x v z. [para(1994(a,1),6168(a,1,2))]. % Operation v is associative-commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 5 at 1.87 (+ 0.01) seconds: assoc_join. % Length of proof is 37. % Level of proof is 12. % Maximum clause weight is 21. % Given clauses 192. 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 16 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [clausify]. 21 x v (y ^ x) = x. [para(12(a,1),11(a,1,2,2))]. 22 x ^ (y v x) = x. [para(11(a,1),12(a,1,2,2))]. 23 (x ^ y) v y = y. [para(11(a,1),13(a,1,1))]. 25 x ^ (x v y) = x. [para(13(a,1),12(a,1,2))]. 27 (x v ((y v (x v z)) ^ u)) v (y v (x v z)) = y v (x v z). [para(12(a,1),13(a,1,1,1))]. 34 (x v y) ^ y = y. [para(12(a,1),14(a,1,1))]. 41 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(22(a,1),13(a,1,1,1))]. 45 x v (y v (x v z)) = y v (x v z). [para(12(a,1),23(a,1,1))]. 48 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(25(a,1),13(a,1,1,1))]. 50 (x v y) v x = x v y. [para(25(a,1),21(a,1,2))]. 51 x v (x v y) = x v y. [para(25(a,1),23(a,1,1))]. 69 x ^ (y ^ x) = y ^ x. [para(21(a,1),34(a,1,1))]. 85 x ^ ((x v y) v z) = x. [para(50(a,1),12(a,1,2))]. 89 (x v y) ^ x = x. [para(50(a,1),34(a,1,1))]. 96 (x v y) v (y v (x v z)) = y v (x v z). [para(89(a,1),27(a,1,1,2))]. 123 (x v (y v z)) ^ y = y. [para(12(a,1),69(a,1,2)),demod(12(6))]. 163 ((x v y) v z) ^ x = x. [para(85(a,1),69(a,1,2)),demod(85(6))]. 276 (x v y) ^ (z ^ x) = z ^ x. [para(23(a,1),163(a,1,1,1))]. 587 (x v y) v (y v x) = y v x. [para(89(a,1),41(a,1,1,2))]. 838 (x v (y ^ z)) v (z v x) = z v x. [para(276(a,1),41(a,1,1,2))]. 867 (x v y) v (x v (y v z)) = x v (y v z). [para(123(a,1),48(a,1,1,2))]. 1992 (x v y) ^ (y v x) = x v y. [para(587(a,1),25(a,1,2))]. 1994 x v y = y v x. [para(587(a,1),50(a,1,1)),demod(587(3),587(4))]. 2309 c5 v (c3 v c4) != c3 v (c4 v c5) # answer(assoc_join). [back_demod(16),demod(1994(5))]. 3517 (x v y) v ((x v z) v y) = y v (x v z). [para(1994(a,1),96(a,1,2))]. 6168 x v (y v (z ^ x)) = x v y. [para(838(a,1),96(a,1,2)),demod(1994(5),867(5),838(7))]. 6225 (x v y) v (z v y) = (x v y) v z. [para(22(a,1),6168(a,1,2,2))]. 6247 x v ((y ^ x) v z) = x v z. [para(1994(a,1),6168(a,1,2))]. 6286 (x v y) v (x v z) = y v (x v z). [back_demod(3517),demod(6225(4))]. 6496 (x v y) v z = y v (x v z). [para(25(a,1),6247(a,1,2,1)),demod(6286(3)),flip(a)]. 6523 x v (y v z) = y v (x v z). [para(1992(a,1),6247(a,1,2,1)),demod(6496(3),6496(4),51(3),45(3),6496(4))]. 7778 $F # answer(assoc_join). [back_demod(2309),demod(6523(5),1994(4)),xx(a)]. ============================== end of proof ========================== given #193 (F,wt=11): 6360 x v ((x ^ y) v z) = x v z. [para(1994(a,1),6243(a,1,2))]. given #194 (T,wt=11): 6496 (x v y) v z = y v (x v z). [para(25(a,1),6247(a,1,2,1)),demod(6286(3)),flip(a)]. given #195 (T,wt=11): 6523 x v (y v z) = y v (x v z). [para(1992(a,1),6247(a,1,2,1)),demod(6496(3),6496(4),51(3),45(3),6496(4))]. given #196 (A,wt=19): 113 ((x v y) ^ (z v y)) v (u ^ y) = (x v y) ^ (z v y). [para(47(a,1),29(a,1,1,2)),demod(47(8))]. given #197 (F,wt=13): 937 x ^ (y v (z v (u v (x v v)))) = x. [para(307(a,1),44(a,1,1)),demod(307(9))]. given #198 (F,wt=13): 1205 x ^ (y v (z v (u v (v v x)))) = x. [para(340(a,1),44(a,1,1)),demod(340(9))]. given #199 (T,wt=13): 1234 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(349(a,1),66(a,1,1)),demod(349(9))]. given #200 (T,wt=13): 1241 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(40(a,1),349(a,1,2,2))]. given #201 (A,wt=19): 115 ((x v y) ^ (x v z)) v (u ^ x) = (x v y) ^ (x v z). [para(50(a,1),29(a,1,1,1)),demod(50(7))]. given #202 (F,wt=13): 1242 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(40(a,1),349(a,1,2))]. given #203 (F,wt=13): 1246 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(349(a,1),168(a,1,1)),demod(349(9))]. given #204 (T,wt=13): 1284 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(40(a,1),356(a,1,2))]. given #205 (T,wt=13): 1288 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(356(a,1),168(a,1,1)),demod(356(9))]. given #206 (A,wt=33): 116 (((x v y) ^ (y v z)) ^ ((u ^ y) v v)) v (w ^ (u ^ y)) = ((x v y) ^ (y v z)) ^ ((u ^ y) v v). [para(29(a,1),29(a,1,1,1)),demod(29(14))]. given #207 (F,wt=13): 1316 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(358(a,1),66(a,1,1)),demod(358(9))]. given #208 (F,wt=13): 1320 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(40(a,1),358(a,1,2,2))]. given #209 (T,wt=13): 1321 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(40(a,1),358(a,1,2))]. given #210 (T,wt=13): 1325 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(358(a,1),168(a,1,1)),demod(358(9))]. given #211 (A,wt=19): 120 ((x ^ y) v (x ^ z)) ^ (u v x) = (x ^ y) v (x ^ z). [para(64(a,1),24(a,1,1,1)),demod(64(7))]. given #212 (F,wt=13): 1392 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(40(a,1),362(a,1,2))]. given #213 (F,wt=13): 1396 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(362(a,1),168(a,1,1)),demod(362(9))]. given #214 (T,wt=13): 1409 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(369(a,1),11(a,1,2,2))]. given #215 (T,wt=13): 1416 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(369(a,1),76(a,1,1,2))]. given #216 (A,wt=19): 121 ((x v y) ^ (y v z)) v (y ^ u) = (x v y) ^ (y v z). [para(64(a,1),29(a,1,2))]. given #217 (F,wt=13): 1417 (x ^ y) v ((y ^ x) ^ z) = x ^ y. [para(369(a,1),117(a,1,2,1))]. given #218 (F,wt=13): 1421 (x ^ y) ^ (z v (y ^ x)) = x ^ y. [para(369(a,1),81(a,1,1)),demod(369(7))]. given #219 (T,wt=13): 1423 (x ^ y) ^ ((y ^ x) v z) = x ^ y. [para(369(a,1),161(a,1,1)),demod(369(7))]. given #220 (T,wt=13): 1543 (x ^ y) ^ ((x v z) ^ y) = x ^ y. [back_demod(785),demod(1413(4))]. given #221 (A,wt=19): 125 ((x ^ y) v (z ^ y)) ^ (u v y) = (x ^ y) v (z ^ y). [para(69(a,1),24(a,1,1,2)),demod(69(8))]. given #222 (F,wt=13): 1545 (x ^ y) ^ ((z v x) ^ y) = x ^ y. [back_demod(783),demod(1413(4))]. given #223 (F,wt=13): 1558 x ^ ((y v x) ^ (z v (u v x))) = x. [back_demod(766),demod(1413(5))]. given #224 (T,wt=13): 1574 x ^ ((x v y) ^ (z v (x v u))) = x. [back_demod(687),demod(1413(5))]. given #225 (T,wt=13): 1614 x ^ ((y v (x v z)) ^ (u v x)) = x. [back_demod(397),demod(1413(5))]. given #226 (A,wt=19): 126 (x v y) ^ ((z ^ y) v (y ^ u)) = (z ^ y) v (y ^ u). [para(24(a,1),69(a,1,2)),demod(24(10))]. given #227 (F,wt=13): 1623 x ^ ((y v (z v x)) ^ (x v u)) = x. [back_demod(373),demod(1413(5))]. given #228 (F,wt=13): 1896 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(480(a,1),168(a,1,1)),demod(480(9))]. given #229 (T,wt=13): 1973 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(509(a,1),92(a,1,1)),demod(509(9))]. given #230 (T,wt=13): 1979 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(509(a,1),169(a,1,1)),demod(509(9))]. given #231 (A,wt=25): 133 (x ^ (y ^ z)) v (y ^ ((x ^ (y ^ z)) v u)) = y ^ ((x ^ (y ^ z)) v u). [para(32(a,1),79(a,1,1))]. given #232 (F,wt=13): 1991 (x v y) ^ (z v (y v x)) = x v y. [para(587(a,1),12(a,1,2,2))]. given #233 (F,wt=13): 2310 (x v (y v z)) ^ (z v y) = y v z. [back_demod(2001),demod(2008(6))]. given #234 (T,wt=13): 2411 x v ((((x ^ y) ^ z) ^ u) ^ v) = x. [para(696(a,1),168(a,1,1)),demod(696(9))]. given #235 (T,wt=13): 2436 x v (((y ^ (z ^ x)) ^ u) ^ v) = x. [para(698(a,1),168(a,1,1)),demod(698(9))]. given #236 (A,wt=15): 134 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(79(a,1),32(a,1,1,2))]. given #237 (F,wt=11): 10282 x ^ (y ^ (z v x)) = x ^ y. [para(797(a,1),134(a,1,2)),demod(1413(5),10246(5),797(7))]. given #238 (F,wt=11): 10286 x ^ (y ^ (x v z)) = x ^ y. [para(813(a,1),134(a,1,2)),demod(1413(5),10246(5),813(7))]. given #239 (T,wt=11): 10320 x ^ ((y v x) ^ z) = x ^ z. [para(1413(a,1),10282(a,1,2))]. % Operation ^ is associative-commutative; redundancy checks enabled. ============================== PROOF ================================= % Proof 6 at 3.70 (+ 0.01) seconds: assoc_meet. % Length of proof is 33. % Level of proof is 13. % Maximum clause weight is 21. % Given clauses 239. 11 x v (y ^ (x ^ z)) = x # label(McKenzie_1). [input]. 12 x ^ (y v (x v z)) = x # label(McKenzie_2). [input]. 13 ((x ^ y) v (y ^ z)) v y = y # label(McKenzie_3). [input]. 14 ((x v y) ^ (y v z)) ^ y = y # label(McKenzie_4). [input]. 18 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [clausify]. 21 x v (y ^ x) = x. [para(12(a,1),11(a,1,2,2))]. 22 x ^ (y v x) = x. [para(11(a,1),12(a,1,2,2))]. 23 (x ^ y) v y = y. [para(11(a,1),13(a,1,1))]. 30 x v (x ^ y) = x. [para(14(a,1),11(a,1,2))]. 32 (x ^ ((y ^ (x ^ z)) v u)) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(11(a,1),14(a,1,1,1))]. 34 (x v y) ^ y = y. [para(12(a,1),14(a,1,1))]. 39 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(21(a,1),14(a,1,1,1))]. 47 x v (y v x) = y v x. [para(22(a,1),23(a,1,1))]. 64 (x ^ y) ^ x = x ^ y. [para(30(a,1),22(a,1,2))]. 67 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(11(a,1),34(a,1,1))]. 76 (x ^ (y ^ z)) v y = y. [para(11(a,1),47(a,1,2)),demod(11(6))]. 79 (x ^ y) v x = x. [para(30(a,1),47(a,1,2)),demod(30(4))]. 134 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(79(a,1),32(a,1,1,2))]. 146 ((x ^ y) ^ z) v x = x. [para(64(a,1),76(a,1,1))]. 216 (x ^ y) v (z v x) = z v x. [para(34(a,1),146(a,1,1,1))]. 369 (x ^ y) ^ (y ^ x) = y ^ x. [para(79(a,1),39(a,1,1,2))]. 797 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(216(a,1),39(a,1,1,2))]. 1412 (x ^ y) v (y ^ x) = x ^ y. [para(369(a,1),30(a,1,2))]. 1413 x ^ y = y ^ x. [para(369(a,1),79(a,1,1)),demod(1412(3))]. 1674 c10 ^ (c8 ^ c9) != c8 ^ (c9 ^ c10) # answer(assoc_meet). [back_demod(18),demod(1413(5))]. 10246 (x ^ y) ^ (x ^ (y ^ z)) = x ^ (y ^ z). [para(1413(a,1),134(a,1,1))]. 10282 x ^ (y ^ (z v x)) = x ^ y. [para(797(a,1),134(a,1,2)),demod(1413(5),10246(5),797(7))]. 10320 x ^ ((y v x) ^ z) = x ^ z. [para(1413(a,1),10282(a,1,2))]. 10518 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(21(a,1),10320(a,1,2,1))]. 10519 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(30(a,1),10320(a,1,2,1))]. 10572 (x ^ y) ^ z = y ^ (x ^ z). [para(10320(a,1),134(a,1,2,2)),demod(10518(4),10519(3),10320(5))]. 10608 x ^ (y ^ z) = y ^ (x ^ z). [back_demod(10518),demod(10572(3),67(3),10572(4))]. 11921 $F # answer(assoc_meet). [back_demod(1674),demod(10608(5),1413(4)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=239. Generated=72572. Kept=11905. proofs=6. Usable=89. Sos=2526. Demods=3672. Denials=0. Limbo=1313, Disabled=7987. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=60562. Back_subsumed=62. Sos_limit_deleted=103. Sos_displaced=0. Sos_removed=0. New_demodulators=11354 (7 lex), Back_demodulated=7911. Back_unit_deleted=0. Demod_attempts=1020641. Demod_rewrites=165129. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=10.01. User_CPU=3.70, System_CPU=0.01, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 6 proofs. Process 13095 exit (max_proofs) Mon Jun 19 16:41:24 2006