============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3831 was started by mccune on cleo.thornwood, Wed Nov 22 11:24:02 2006 The command was "/home/mccune/bin/prover9 -f mckenzie.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file mckenzie.in 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(goal). [goal]. 2 (x v y) v z = x v (y v z) # answer(assoc_join) # label(goal). [goal]. 3 x ^ y = y ^ x # answer(commute_meet) # label(goal). [goal]. 4 (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet) # label(goal). [goal]. 5 x ^ (x v y) = x # answer(absorb_1) # label(goal). [goal]. 6 x v (x ^ y) = x # answer(absorb_2) # 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(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: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 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(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 6). % (nonunit Horn with equality) Auto_process settings: % set(back_unit_deletion). % (Horn set with negative nonunits) % set(back_unit_deletion) -> set(unit_deletion). restricted denial: (wt=7): 12 c2 v c1 != c1 v c2 # answer(commute_join). [deny(1)]. restricted denial: (wt=11): 13 (c3 v c4) v c5 != c3 v (c4 v c5) # answer(assoc_join). [deny(2)]. restricted denial: (wt=7): 14 c7 ^ c6 != c6 ^ c7 # answer(commute_meet). [deny(3)]. restricted denial: (wt=11): 15 (c8 ^ c9) ^ c10 != c8 ^ (c9 ^ c10) # answer(assoc_meet). [deny(4)]. restricted denial: (wt=7): 16 c11 ^ (c11 v c12) != c11 # answer(absorb_1). [deny(5)]. restricted denial: (wt=7): 17 c13 v (c13 ^ c14) != c13 # answer(absorb_2). [deny(6)]. restricted denial: (wt=50): 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.00 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.00 (+ 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(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)]. restricted denial: (wt=43): 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)]. % 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.00 (+ 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(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)]. restricted denial: (wt=36): 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)]. % Disable descendants (x means already disabled): 17x given #5 (T,wt=5): 26 x v x = x. [para(9(a,1),10(a,1,1,2)),rewrite(21(2))]. given #6 (A,wt=7): 19 x v (y ^ x) = x. [para(9(a,1),8(a,1,2,2))]. given #7 (F,wt=5): 36 x ^ x = x. [para(10(a,1),11(a,1,1,1)),rewrite(23(2))]. given #8 (F,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 (T,wt=7): 23 x ^ (x v y) = x. [para(10(a,1),9(a,1,2))]. given #11 (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 #12 (F,wt=7): 30 x v (x ^ y) = x. [para(11(a,1),8(a,1,2))]. given #13 (F,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 (T,wt=9): 45 (x ^ y) ^ y = x ^ y. [para(19(a,1),20(a,1,2))]. given #16 (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 #17 (F,wt=9): 49 x v (y v x) = y v x. [para(20(a,1),21(a,1,1))]. given #18 (F,wt=7): 81 (x ^ y) v x = x. [para(30(a,1),49(a,1,2)),rewrite(30(4))]. given #19 (T,wt=9): 52 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. given #20 (T,wt=7): 91 (x v y) ^ x = x. [para(52(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(11(a,1),8(a,1,2,2))]. given #22 (F,wt=9): 53 x v (x v y) = x v y. [para(23(a,1),21(a,1,1))]. given #23 (F,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 (T,wt=9): 73 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(8(a,1),11(a,1,1,1))]. given #27 (F,wt=9): 78 (x ^ (y ^ z)) v y = y. [para(8(a,1),49(a,1,2)),rewrite(8(6))]. given #28 (F,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(52(a,1),9(a,1,2))]. given #30 (T,wt=9): 119 x v ((x ^ y) ^ z) = x. [para(66(a,1),8(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(11(a,1),10(a,1,1,2))]. given #32 (F,wt=9): 124 x v (y ^ (z ^ x)) = x. [para(71(a,1),8(a,1,2,2))]. given #33 (F,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 (T,wt=9): 149 (x ^ (y ^ z)) v z = z. [para(71(a,1),78(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(10(a,1),11(a,1,1,2))]. given #37 (F,wt=9): 154 x ^ ((y v x) v z) = x. [para(52(a,1),79(a,1,2))]. given #38 (F,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 (T,wt=9): 173 x v ((y ^ x) ^ z) = x. [para(71(a,1),119(a,1,2,1))]. given #41 (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 #42 (F,wt=9): 222 ((x ^ y) ^ z) v y = y. [para(71(a,1),148(a,1,1,1))]. given #43 (F,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 (T,wt=11): 68 (x v y) v (z ^ y) = x v y. [para(34(a,1),8(a,1,2,2))]. given #46 (A,wt=15): 41 (x ^ ((y ^ x) v z)) ^ (y ^ x) = y ^ x. [para(19(a,1),11(a,1,1,1))]. given #47 (F,wt=11): 80 ((x v y) ^ (z v y)) ^ y = y. [para(49(a,1),11(a,1,1,2))]. given #48 (F,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),52(a,1,1)),rewrite(10(8))]. given #50 (T,wt=11): 89 ((x v y) ^ (x v z)) ^ x = x. [para(52(a,1),11(a,1,1,1))]. given #51 (A,wt=13): 42 (x ^ (y ^ z)) ^ y = x ^ (y ^ z). [para(8(a,1),20(a,1,2))]. given #52 (F,wt=11): 94 (x v y) v (z ^ x) = x v y. [para(91(a,1),8(a,1,2,2))]. given #53 (F,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 (T,wt=11): 126 ((x ^ y) v (z ^ y)) v y = y. [para(71(a,1),10(a,1,1,2))]. given #56 (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 #57 (F,wt=11): 144 (x ^ y) v (z v y) = z v y. [para(34(a,1),78(a,1,1,2))]. given #58 (F,wt=11): 146 (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 (T,wt=11): 163 (x ^ y) ^ (x v z) = x ^ y. [para(81(a,1),87(a,1,2,1))]. given #61 (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 #62 (F,wt=11): 170 (x v y) v (y ^ z) = x v y. [para(34(a,1),119(a,1,2,1))]. given #63 (F,wt=11): 171 (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 (T,wt=11): 210 (x v y) ^ (y ^ z) = y ^ z. [para(81(a,1),125(a,1,1,2))]. given #66 (A,wt=15): 48 ((x v (y ^ z)) ^ z) ^ (y ^ z) = y ^ z. [para(21(a,1),11(a,1,1,2))]. given #67 (F,wt=11): 218 (x ^ y) v (z v x) = z v x. [para(34(a,1),148(a,1,1,1))]. given #68 (F,wt=11): 220 (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 (T,wt=11): 282 (x v y) ^ (x ^ z) = x ^ z. [para(81(a,1),165(a,1,1,1))]. given #71 (A,wt=15): 50 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(23(a,1),10(a,1,1,1))]. given #72 (F,wt=11): 302 x ^ (y v ((x v z) v u)) = x. [para(40(a,1),9(a,1,2))]. given #73 (F,wt=11): 309 x ^ (y v (z v (x v u))) = x. [para(40(a,1),79(a,1,2,2))]. given #74 (T,wt=11): 310 x ^ (y v ((z v x) v u)) = x. [para(40(a,1),79(a,1,2))]. given #75 (T,wt=11): 313 (x v ((y v z) v u)) ^ y = y. [para(40(a,1),125(a,1,1))]. given #76 (A,wt=17): 51 ((x ^ y) v (y ^ z)) ^ y = (x ^ y) v (y ^ z). [para(10(a,1),23(a,1,2))]. given #77 (F,wt=11): 317 x ^ ((y v (x v z)) v u) = x. [para(40(a,1),154(a,1,2,1))]. given #78 (F,wt=11): 318 (x v (y v (z v u))) ^ z = z. [para(40(a,1),157(a,1,1,2))]. given #79 (T,wt=11): 319 (x v ((y v z) v u)) ^ z = z. [para(40(a,1),157(a,1,1))]. given #80 (T,wt=11): 336 ((x v (y v z)) v u) ^ y = y. [para(40(a,1),265(a,1,1,1))]. given #81 (A,wt=33): 54 ((x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ v)) ^ z = (x ^ (y ^ (z ^ u))) v ((y ^ (z ^ u)) ^ v). [para(8(a,1),22(a,1,2))]. given #82 (F,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 (F,wt=11): 351 x v (y ^ (z ^ (x ^ u))) = x. [para(8(a,1),68(a,1,1)),rewrite(8(7))]. given #84 (T,wt=11): 358 x v (y ^ ((x ^ z) ^ u)) = x. [para(119(a,1),68(a,1,1)),rewrite(119(7))]. given #85 (T,wt=11): 360 x v (y ^ (z ^ (u ^ x))) = x. [para(124(a,1),68(a,1,1)),rewrite(124(7))]. given #86 (A,wt=27): 55 (x v ((y v (x v z)) ^ u)) ^ (v 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 #87 (F,wt=11): 364 x v (y ^ ((z ^ x) ^ u)) = x. [para(173(a,1),68(a,1,1)),rewrite(173(7))]. given #88 (F,wt=11): 371 (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 88. 3 x ^ y = y ^ x # answer(commute_meet) # 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))]. 371 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 1414 (x ^ y) v (y ^ x) = x ^ y. [para(371(a,1),30(a,1,2))]. 1415 x ^ y = y ^ x. [para(371(a,1),81(a,1,1)),rewrite(1414(3))]. 1416 $F # answer(commute_meet). [resolve(1415,a,14,a)]. ============================== end of proof ========================== % Redundant proof: 1678 $F # answer(commute_meet). [back_rewrite(14),rewrite(1415(3)),xx(a)]. restricted denial: (wt=29): 1676 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(1415(21),1415(30)),xx(c)]. restricted denial: (wt=11): 1677 c10 ^ (c8 ^ c9) != c8 ^ (c9 ^ c10) # answer(assoc_meet). [back_rewrite(15),rewrite(1415(5))]. % Disable descendants (x means already disabled): 14x given #89 (T,wt=7): 1415 x ^ y = y ^ x. [para(371(a,1),81(a,1,1)),rewrite(1414(3))]. given #90 (T,wt=11): 390 x ^ ((y v x) ^ (z v x)) = x. [para(80(a,1),66(a,1,1)),rewrite(80(8))]. given #91 (A,wt=21): 56 (((x ^ y) v (y ^ z)) v ((u v y) ^ v)) v (u v y) = u v y. [para(22(a,1),10(a,1,1,1))]. given #92 (F,wt=11): 429 x v ((x ^ y) v (x ^ z)) = x. [para(66(a,1),88(a,1,2,1))]. given #93 (F,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): 456 x ^ ((x v y) ^ (x v z)) = x. [para(89(a,1),66(a,1,1)),rewrite(89(8))]. given #95 (T,wt=11): 475 (x ^ ((y ^ z) ^ u)) v y = y. [para(42(a,1),78(a,1,1))]. given #96 (A,wt=33): 57 ((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(11(a,1),22(a,1,1,2)),rewrite(11(18))]. given #97 (F,wt=11): 477 (x ^ (y ^ (z ^ u))) v z = z. [para(42(a,1),149(a,1,1,2))]. given #98 (F,wt=11): 478 (x ^ ((y ^ z) ^ u)) v z = z. [para(42(a,1),149(a,1,1))]. given #99 (T,wt=11): 482 x v ((y ^ (x ^ z)) ^ u) = x. [para(42(a,1),173(a,1,2,1))]. given #100 (T,wt=11): 483 ((x ^ (y ^ z)) ^ u) v y = y. [para(42(a,1),222(a,1,1,1))]. given #101 (A,wt=15): 58 (x v y) v ((z ^ y) v (y ^ u)) = x v y. [para(22(a,1),19(a,1,2))]. given #102 (F,wt=11): 511 ((x ^ y) v (z ^ x)) v x = x. [para(71(a,1),120(a,1,1,2))]. given #103 (F,wt=11): 589 (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.30 (+ 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(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))]. 52 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 91 (x v y) ^ x = x. [para(52(a,1),34(a,1,1))]. 589 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. 1998 x v y = y v x. [para(589(a,1),52(a,1,1)),rewrite(589(3),589(4))]. 1999 $F # answer(commute_join). [resolve(1998,a,12,a)]. ============================== end of proof ========================== % Redundant proof: 2315 $F # answer(commute_join). [back_rewrite(12),rewrite(1998(3)),xx(a)]. restricted denial: (wt=22): 2155 c17 v (c15 v c16) != c15 v (c16 v c17) | c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(1676),rewrite(1998(3),1998(12)),xx(a)]. restricted denial: (wt=11): 2314 c5 v (c3 v c4) != c3 v (c4 v c5) # answer(assoc_join). [back_rewrite(13),rewrite(1998(5))]. % Disable descendants (x means already disabled): 12x given #104 (T,wt=7): 1998 x v y = y v x. [para(589(a,1),52(a,1,1)),rewrite(589(3),589(4))]. given #105 (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 #106 (A,wt=21): 60 (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 #107 (F,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 (F,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): 698 x v (((x ^ y) ^ z) ^ u) = x. [para(119(a,1),170(a,1,1)),rewrite(119(7))]. given #110 (T,wt=11): 700 x v ((y ^ (z ^ x)) ^ u) = x. [para(124(a,1),170(a,1,1)),rewrite(124(7))]. given #111 (A,wt=15): 61 ((x ^ y) v (y ^ z)) v (u v y) = u v y. [para(22(a,1),21(a,1,1))]. given #112 (F,wt=11): 703 x v (((y ^ x) ^ z) ^ u) = x. [para(173(a,1),170(a,1,1)),rewrite(173(7))]. given #113 (F,wt=11): 1414 (x ^ y) v (y ^ x) = x ^ y. [para(371(a,1),30(a,1,2))]. given #114 (T,wt=11): 1621 x ^ ((x v y) ^ (z v x)) = x. [back_rewrite(387),rewrite(1415(4))]. given #115 (T,wt=11): 1746 x v ((x ^ y) v (z ^ x)) = x. [para(71(a,1),429(a,1,2,2))]. given #116 (A,wt=21): 62 (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 #117 (F,wt=11): 1996 (x v y) ^ (y v x) = x v y. [para(589(a,1),23(a,1,2))]. given #118 (F,wt=13): 69 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(8(a,1),34(a,1,1))]. given #119 (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 #120 (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 #121 (A,wt=33): 63 (((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(22(a,1),22(a,1,1,1)),rewrite(22(14))]. given #122 (F,wt=13): 169 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(119(a,1),34(a,1,1))]. given #123 (F,wt=13): 200 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(124(a,1),34(a,1,1))]. given #124 (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 #125 (T,wt=13): 295 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(173(a,1),34(a,1,1))]. given #126 (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 #127 (F,wt=13): 308 (x v y) v (z ^ (y ^ u)) = x v y. [para(78(a,1),40(a,1,1,2)),rewrite(78(7))]. given #128 (F,wt=13): 314 (x v y) v ((y ^ z) ^ u) = x v y. [para(148(a,1),40(a,1,1,2)),rewrite(148(7))]. given #129 (T,wt=13): 315 (x v y) v (z ^ (u ^ y)) = x v y. [para(149(a,1),40(a,1,1,2)),rewrite(149(7))]. given #130 (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 #131 (A,wt=19): 90 ((x ^ y) v (y ^ z)) ^ (y v u) = (x ^ y) v (y ^ z). [para(52(a,1),22(a,1,2))]. given #132 (F,wt=13): 345 (x ^ (y ^ z)) v (u v z) = u v z. [para(46(a,1),149(a,1,1,2))]. given #133 (F,wt=13): 348 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(40(a,1),46(a,1,2))]. given #134 (T,wt=13): 349 ((x ^ y) ^ z) v (u v y) = u v y. [para(46(a,1),222(a,1,1,1))]. given #135 (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 #136 (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),52(a,1,1)),rewrite(25(14))]. given #137 (F,wt=13): 361 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(68(a,1),154(a,1,2,1))]. given #138 (F,wt=13): 363 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(68(a,1),157(a,1,1,2))]. given #139 (T,wt=13): 365 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(68(a,1),265(a,1,1,1))]. given #140 (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 #141 (A,wt=17): 96 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(10(a,1),91(a,1,1))]. given #142 (F,wt=13): 411 (x ^ (y ^ z)) v (u v y) = u v y. [para(83(a,1),149(a,1,1,2))]. given #143 (F,wt=13): 415 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(40(a,1),83(a,1,2))]. given #144 (T,wt=13): 416 ((x ^ y) ^ z) v (u v x) = u v x. [para(83(a,1),222(a,1,1,1))]. given #145 (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 #146 (A,wt=15): 98 (x v y) v (y v (x v z)) = y v (x v z). [para(91(a,1),25(a,1,1,2))]. given #147 (F,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 #148 (F,wt=13): 443 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(88(a,1),68(a,1,1)),rewrite(88(9))]. given #149 (T,wt=13): 468 x ^ (y v ((x v z) ^ (x v u))) = x. [para(89(a,1),83(a,1,1)),rewrite(89(9))]. given #150 (T,wt=13): 481 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(165(a,1),42(a,1,1,2)),rewrite(165(7))]. given #151 (A,wt=25): 99 (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 #152 (F,wt=13): 486 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [para(42(a,1),88(a,1,2,1))]. given #153 (F,wt=13): 498 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(94(a,1),157(a,1,1,2))]. given #154 (T,wt=13): 499 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(94(a,1),265(a,1,1,1))]. given #155 (T,wt=13): 500 (x v y) v (z ^ (u ^ x)) = x v y. [para(94(a,1),68(a,1,1)),rewrite(94(7))]. given #156 (A,wt=27): 100 (x ^ ((y ^ (x ^ z)) v u)) v (v ^ (y ^ (x ^ z))) = x ^ ((y ^ (x ^ z)) v u). [para(8(a,1),29(a,1,1,1)),rewrite(8(11))]. given #157 (F,wt=13): 503 (x v y) v (z ^ (x ^ u)) = x v y. [para(42(a,1),94(a,1,2))]. given #158 (F,wt=13): 533 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(120(a,1),94(a,1,1)),rewrite(120(9))]. given #159 (T,wt=13): 549 x ^ ((y v (x v z)) ^ (x v u)) = x. [para(40(a,1),121(a,1,2,1))]. given #160 (T,wt=13): 583 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(126(a,1),94(a,1,1)),rewrite(126(9))]. given #161 (A,wt=21): 104 (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 #162 (F,wt=13): 621 (x ^ (y ^ z)) v (z v u) = z v u. [para(94(a,1),144(a,1,2)),rewrite(94(7))]. given #163 (F,wt=13): 636 (x ^ (y ^ z)) v (y v u) = y v u. [para(42(a,1),146(a,1,1))]. given #164 (T,wt=13): 651 (x v y) v ((z ^ x) ^ u) = x v y. [para(160(a,1),173(a,1,2,1))]. given #165 (T,wt=13): 652 ((x ^ y) ^ z) v (y v u) = y v u. [para(160(a,1),222(a,1,1,1))]. given #166 (A,wt=15): 105 (x ^ y) ^ ((z v y) ^ (y v u)) = x ^ y. [para(29(a,1),20(a,1,2))]. given #167 (F,wt=13): 653 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(83(a,1),160(a,1,1)),rewrite(83(7))]. given #168 (F,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 #169 (T,wt=13): 669 (x v y) v ((x ^ z) ^ u) = x v y. [para(163(a,1),173(a,1,2,1))]. given #170 (T,wt=13): 670 ((x ^ y) ^ z) v (x v u) = x v u. [para(163(a,1),222(a,1,1,1))]. given #171 (A,wt=31): 109 ((x ^ (y ^ z)) v ((y ^ z) ^ u)) ^ ((v v z) ^ (z v w)) = (x ^ (y ^ z)) v ((y ^ z) ^ u). [para(29(a,1),22(a,1,2))]. given #172 (F,wt=13): 673 x ^ (((y v x) ^ (z v x)) v u) = x. [para(80(a,1),163(a,1,1)),rewrite(80(9))]. given #173 (F,wt=13): 675 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): 681 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(163(a,1),160(a,1,1)),rewrite(163(7))]. given #175 (T,wt=13): 691 x ^ ((y v x) ^ (z v (x v u))) = x. [para(47(a,1),121(a,1,2,2))]. given #176 (A,wt=31): 110 ((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(22(a,1),29(a,1,2))]. given #177 (F,wt=13): 702 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(170(a,1),157(a,1,1,2))]. given #178 (F,wt=13): 704 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(170(a,1),265(a,1,1,1))]. given #179 (T,wt=13): 709 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(88(a,1),170(a,1,1)),rewrite(88(9))]. given #180 (T,wt=13): 719 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(171(a,1),157(a,1,1,2))]. given #181 (A,wt=21): 111 (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 #182 (F,wt=13): 720 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(171(a,1),265(a,1,1,1))]. given #183 (F,wt=13): 726 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(120(a,1),171(a,1,1)),rewrite(120(9))]. given #184 (T,wt=13): 728 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(126(a,1),171(a,1,1)),rewrite(126(9))]. given #185 (T,wt=13): 799 (x ^ (y v z)) ^ (z ^ x) = z ^ x. [para(218(a,1),41(a,1,1,2))]. given #186 (A,wt=15): 112 ((x v y) ^ (y v z)) ^ (u ^ y) = u ^ y. [para(29(a,1),34(a,1,1))]. given #187 (F,wt=13): 815 (x ^ (y v z)) ^ (y ^ x) = y ^ x. [para(220(a,1),41(a,1,1,2))]. given #188 (F,wt=13): 840 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. given #189 (T,wt=11): 6174 x v (y v (z ^ x)) = x v y. [para(840(a,1),98(a,1,2)),rewrite(1998(5),869(5),840(7))]. given #190 (T,wt=11): 6249 x v (y v (x ^ z)) = x v y. [para(1415(a,1),6174(a,1,2,2))]. given #191 (A,wt=19): 114 (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 #192 (F,wt=11): 6253 x v ((y ^ x) v z) = x v z. [para(1998(a,1),6174(a,1,2))]. ============================== PROOF ================================= % Proof 5 at 1.53 (+ 0.03) seconds: assoc_join. % Length of proof is 42. % Level of proof is 13. % Maximum clause weight is 21. % Given clauses 192. 2 (x v y) v z = x v (y v z) # answer(assoc_join) # 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))]. 50 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(23(a,1),10(a,1,1,1))]. 52 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 53 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(52(a,1),9(a,1,2))]. 91 (x v y) ^ x = x. [para(52(a,1),34(a,1,1))]. 98 (x v y) v (y v (x v z)) = y v (x v z). [para(91(a,1),25(a,1,1,2))]. 125 (x v (y v z)) ^ y = y. [para(9(a,1),71(a,1,2)),rewrite(9(6))]. 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))]. 589 (x v y) v (y v x) = y v x. [para(91(a,1),43(a,1,1,2))]. 598 (x v y) v ((y v z) v x) = (y v z) v x. [para(165(a,1),43(a,1,1,2))]. 840 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. 869 (x v y) v (x v (y v z)) = x v (y v z). [para(125(a,1),50(a,1,1,2))]. 1996 (x v y) ^ (y v x) = x v y. [para(589(a,1),23(a,1,2))]. 1998 x v y = y v x. [para(589(a,1),52(a,1,1)),rewrite(589(3),589(4))]. 2314 c5 v (c3 v c4) != c3 v (c4 v c5) # answer(assoc_join). [back_rewrite(13),rewrite(1998(5))]. 3523 (x v y) v ((x v z) v y) = y v (x v z). [para(1998(a,1),98(a,1,2))]. 6174 x v (y v (z ^ x)) = x v y. [para(840(a,1),98(a,1,2)),rewrite(1998(5),869(5),840(7))]. 6231 (x v y) v (z v y) = (x v y) v z. [para(20(a,1),6174(a,1,2,2))]. 6232 (x v y) v (z v x) = (x v y) v z. [para(23(a,1),6174(a,1,2,2))]. 6253 x v ((y ^ x) v z) = x v z. [para(1998(a,1),6174(a,1,2))]. 6292 (x v y) v (x v z) = y v (x v z). [back_rewrite(3523),rewrite(6231(4))]. 6338 (x v y) v (y v z) = (y v z) v x. [back_rewrite(598),rewrite(6232(4))]. 6502 (x v y) v z = y v (x v z). [para(23(a,1),6253(a,1,2,1)),rewrite(6292(3)),flip(a)]. 6534 x v (y v z) = y v (x v z). [para(1996(a,1),6253(a,1,2,1)),rewrite(6502(3),6502(4),53(3),47(3),6502(4))]. 6577 x v (y v z) = z v (x v y). [back_rewrite(6338),rewrite(6534(3),6502(2),53(3),6502(4))]. 6578 $F # answer(assoc_join). [resolve(6577,a,2314,a(flip))]. ============================== end of proof ========================== % Redundant proof: 7802 $F # answer(assoc_join). [back_rewrite(2314),rewrite(6534(5),1998(4)),xx(a)]. restricted denial: (wt=11): 7803 c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(2155),rewrite(6534(5),1998(4)),xx(a)]. % Disable descendants (x means already disabled): 13x 2314x given #193 (F,wt=11): 6366 x v ((x ^ y) v z) = x v z. [para(1998(a,1),6249(a,1,2))]. given #194 (T,wt=11): 6502 (x v y) v z = y v (x v z). [para(23(a,1),6253(a,1,2,1)),rewrite(6292(3)),flip(a)]. given #195 (T,wt=11): 6534 x v (y v z) = y v (x v z). [para(1996(a,1),6253(a,1,2,1)),rewrite(6502(3),6502(4),53(3),47(3),6502(4))]. given #196 (A,wt=19): 115 ((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 #197 (F,wt=11): 6567 x v (y v z) = z v (y v x). [para(110(a,1),6253(a,1,2)),rewrite(6502(2),6502(6),19(8),6502(4),6502(8),6249(7),19(5),6502(4))]. given #198 (F,wt=11): 6577 x v (y v z) = z v (x v y). [back_rewrite(6338),rewrite(6534(3),6502(2),53(3),6502(4))]. given #199 (T,wt=13): 939 x ^ (y v (z v (u v (x v v)))) = x. [para(309(a,1),46(a,1,1)),rewrite(309(9))]. given #200 (T,wt=13): 1207 x ^ (y v (z v (u v (v v x)))) = x. [para(342(a,1),46(a,1,1)),rewrite(342(9))]. given #201 (A,wt=19): 117 ((x v y) ^ (x v z)) v (u ^ x) = (x v y) ^ (x v z). [para(52(a,1),29(a,1,1,1)),rewrite(52(7))]. given #202 (F,wt=13): 1236 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(351(a,1),68(a,1,1)),rewrite(351(9))]. given #203 (F,wt=13): 1243 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(42(a,1),351(a,1,2,2))]. given #204 (T,wt=13): 1244 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(42(a,1),351(a,1,2))]. given #205 (T,wt=13): 1248 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(351(a,1),170(a,1,1)),rewrite(351(9))]. given #206 (A,wt=33): 118 (((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)),rewrite(29(14))]. given #207 (F,wt=13): 1286 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(42(a,1),358(a,1,2))]. given #208 (F,wt=13): 1290 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(358(a,1),170(a,1,1)),rewrite(358(9))]. given #209 (T,wt=13): 1318 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(360(a,1),68(a,1,1)),rewrite(360(9))]. given #210 (T,wt=13): 1322 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(42(a,1),360(a,1,2,2))]. given #211 (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 #212 (F,wt=13): 1323 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(42(a,1),360(a,1,2))]. given #213 (F,wt=13): 1327 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(360(a,1),170(a,1,1)),rewrite(360(9))]. given #214 (T,wt=13): 1394 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(42(a,1),364(a,1,2))]. given #215 (T,wt=13): 1398 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(364(a,1),170(a,1,1)),rewrite(364(9))]. given #216 (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 #217 (F,wt=13): 1411 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(371(a,1),8(a,1,2,2))]. given #218 (F,wt=13): 1418 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(371(a,1),78(a,1,1,2))]. given #219 (T,wt=13): 1419 (x ^ y) v ((y ^ x) ^ z) = x ^ y. [para(371(a,1),119(a,1,2,1))]. given #220 (T,wt=13): 1423 (x ^ y) ^ (z v (y ^ x)) = x ^ y. [para(371(a,1),83(a,1,1)),rewrite(371(7))]. given #221 (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 #222 (F,wt=13): 1425 (x ^ y) ^ ((y ^ x) v z) = x ^ y. [para(371(a,1),163(a,1,1)),rewrite(371(7))]. given #223 (F,wt=13): 1545 (x ^ y) ^ ((x v z) ^ y) = x ^ y. [back_rewrite(787),rewrite(1415(4))]. given #224 (T,wt=13): 1547 (x ^ y) ^ ((z v x) ^ y) = x ^ y. [back_rewrite(785),rewrite(1415(4))]. given #225 (T,wt=13): 1560 x ^ ((y v x) ^ (z v (u v x))) = x. [back_rewrite(768),rewrite(1415(5))]. given #226 (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 #227 (F,wt=13): 1576 x ^ ((x v y) ^ (z v (x v u))) = x. [back_rewrite(689),rewrite(1415(5))]. given #228 (F,wt=13): 1616 x ^ ((y v (x v z)) ^ (u v x)) = x. [back_rewrite(399),rewrite(1415(5))]. given #229 (T,wt=13): 1625 x ^ ((y v (z v x)) ^ (x v u)) = x. [back_rewrite(375),rewrite(1415(5))]. given #230 (T,wt=13): 1900 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(482(a,1),170(a,1,1)),rewrite(482(9))]. given #231 (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 #232 (F,wt=13): 1977 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(511(a,1),94(a,1,1)),rewrite(511(9))]. given #233 (F,wt=13): 1983 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(511(a,1),171(a,1,1)),rewrite(511(9))]. given #234 (T,wt=13): 1995 (x v y) ^ (z v (y v x)) = x v y. [para(589(a,1),9(a,1,2,2))]. given #235 (T,wt=13): 2316 (x v (y v z)) ^ (z v y) = y v z. [back_rewrite(2005),rewrite(2012(6))]. given #236 (A,wt=15): 136 (x ^ y) ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(81(a,1),32(a,1,1,2))]. given #237 (F,wt=11): 10273 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite(1415(5),10239(5),799(7))]. given #238 (F,wt=11): 10277 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite(1415(5),10239(5),815(7))]. given #239 (T,wt=11): 10310 x ^ ((y v x) ^ z) = x ^ z. [para(1415(a,1),10273(a,1,2))]. ============================== PROOF ================================= % Proof 6 at 3.16 (+ 0.04) seconds: all_six. % Length of proof is 75. % Level of proof is 14. % Maximum clause weight is 50. % Given clauses 239. 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(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))]. 50 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(23(a,1),10(a,1,1,1))]. 52 (x v y) v x = x v y. [para(23(a,1),19(a,1,2))]. 53 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(52(a,1),9(a,1,2))]. 91 (x v y) ^ x = x. [para(52(a,1),34(a,1,1))]. 98 (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))]. 125 (x v (y v z)) ^ y = y. [para(9(a,1),71(a,1,2)),rewrite(9(6))]. 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))]. 220 (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))]. 371 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 379 (x ^ y) ^ ((y ^ z) ^ x) = (y ^ z) ^ x. [para(148(a,1),41(a,1,1,2))]. 589 (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(220(a,1),41(a,1,1,2))]. 840 (x v (y ^ z)) v (z v x) = z v x. [para(278(a,1),43(a,1,1,2))]. 869 (x v y) v (x v (y v z)) = x v (y v z). [para(125(a,1),50(a,1,1,2))]. 1414 (x ^ y) v (y ^ x) = x ^ y. [para(371(a,1),30(a,1,2))]. 1415 x ^ y = y ^ x. [para(371(a,1),81(a,1,1)),rewrite(1414(3))]. 1676 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(1415(21),1415(30)),xx(c)]. 1996 (x v y) ^ (y v x) = x v y. [para(589(a,1),23(a,1,2))]. 1998 x v y = y v x. [para(589(a,1),52(a,1,1)),rewrite(589(3),589(4))]. 2155 c17 v (c15 v c16) != c15 v (c16 v c17) | c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(1676),rewrite(1998(3),1998(12)),xx(a)]. 3523 (x v y) v ((x v z) v y) = y v (x v z). [para(1998(a,1),98(a,1,2))]. 6174 x v (y v (z ^ x)) = x v y. [para(840(a,1),98(a,1,2)),rewrite(1998(5),869(5),840(7))]. 6231 (x v y) v (z v y) = (x v y) v z. [para(20(a,1),6174(a,1,2,2))]. 6253 x v ((y ^ x) v z) = x v z. [para(1998(a,1),6174(a,1,2))]. 6292 (x v y) v (x v z) = y v (x v z). [back_rewrite(3523),rewrite(6231(4))]. 6502 (x v y) v z = y v (x v z). [para(23(a,1),6253(a,1,2,1)),rewrite(6292(3)),flip(a)]. 6534 x v (y v z) = y v (x v z). [para(1996(a,1),6253(a,1,2,1)),rewrite(6502(3),6502(4),53(3),47(3),6502(4))]. 7803 c17 ^ (c15 ^ c16) != c15 ^ (c16 ^ c17) # answer(all_six). [back_rewrite(2155),rewrite(6534(5),1998(4)),xx(a)]. 10239 (x ^ y) ^ (x ^ (y ^ z)) = x ^ (y ^ z). [para(1415(a,1),136(a,1,1))]. 10273 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite(1415(5),10239(5),799(7))]. 10276 ((x ^ (y v z)) ^ u) ^ (u ^ (y ^ x)) = u ^ (y ^ x). [para(815(a,1),136(a,1,2,2)),rewrite(815(10))]. 10277 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite(1415(5),10239(5),815(7))]. 10301 (x ^ y) ^ (z ^ x) = (x ^ y) ^ z. [para(30(a,1),10273(a,1,2,2))]. 10310 x ^ ((y v x) ^ z) = x ^ z. [para(1415(a,1),10273(a,1,2))]. 10482 (x ^ y) ^ (y ^ z) = (y ^ z) ^ x. [back_rewrite(379),rewrite(10301(4))]. 10485 x ^ ((x v y) ^ z) = x ^ z. [para(1415(a,1),10277(a,1,2))]. 10500 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(19(a,1),10310(a,1,2,1))]. 10501 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(30(a,1),10310(a,1,2,1))]. 10555 (x ^ y) ^ z = y ^ (x ^ z). [para(10310(a,1),136(a,1,2,2)),rewrite(10500(4),10501(3),10310(5))]. 10558 x ^ (y ^ z) = z ^ (y ^ x). [back_rewrite(10482),rewrite(10555(3),69(3),10555(4))]. 10559 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(10276),rewrite(10555(3),10558(6),200(5),10555(5),10485(4),69(3))]. 10560 $F # answer(all_six). [resolve(10559,a,7803,a(flip))]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 7 at 3.16 (+ 0.04) seconds: assoc_meet. % Length of proof is 49. % Level of proof is 14. % Maximum clause weight is 21. % Given clauses 239. 4 (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet) # 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))]. 52 (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(52(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))]. 220 (x ^ y) v (x v z) = x v z. [para(91(a,1),148(a,1,1,1))]. 371 (x ^ y) ^ (y ^ x) = y ^ x. [para(81(a,1),41(a,1,1,2))]. 379 (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(220(a,1),41(a,1,1,2))]. 1414 (x ^ y) v (y ^ x) = x ^ y. [para(371(a,1),30(a,1,2))]. 1415 x ^ y = y ^ x. [para(371(a,1),81(a,1,1)),rewrite(1414(3))]. 1677 c10 ^ (c8 ^ c9) != c8 ^ (c9 ^ c10) # answer(assoc_meet). [back_rewrite(15),rewrite(1415(5))]. 10239 (x ^ y) ^ (x ^ (y ^ z)) = x ^ (y ^ z). [para(1415(a,1),136(a,1,1))]. 10273 x ^ (y ^ (z v x)) = x ^ y. [para(799(a,1),136(a,1,2)),rewrite(1415(5),10239(5),799(7))]. 10276 ((x ^ (y v z)) ^ u) ^ (u ^ (y ^ x)) = u ^ (y ^ x). [para(815(a,1),136(a,1,2,2)),rewrite(815(10))]. 10277 x ^ (y ^ (x v z)) = x ^ y. [para(815(a,1),136(a,1,2)),rewrite(1415(5),10239(5),815(7))]. 10301 (x ^ y) ^ (z ^ x) = (x ^ y) ^ z. [para(30(a,1),10273(a,1,2,2))]. 10310 x ^ ((y v x) ^ z) = x ^ z. [para(1415(a,1),10273(a,1,2))]. 10482 (x ^ y) ^ (y ^ z) = (y ^ z) ^ x. [back_rewrite(379),rewrite(10301(4))]. 10485 x ^ ((x v y) ^ z) = x ^ z. [para(1415(a,1),10277(a,1,2))]. 10500 (x ^ y) ^ (y ^ z) = (x ^ y) ^ z. [para(19(a,1),10310(a,1,2,1))]. 10501 (x ^ y) ^ (x ^ z) = (x ^ y) ^ z. [para(30(a,1),10310(a,1,2,1))]. 10555 (x ^ y) ^ z = y ^ (x ^ z). [para(10310(a,1),136(a,1,2,2)),rewrite(10500(4),10501(3),10310(5))]. 10558 x ^ (y ^ z) = z ^ (y ^ x). [back_rewrite(10482),rewrite(10555(3),69(3),10555(4))]. 10559 x ^ (y ^ z) = z ^ (x ^ y). [back_rewrite(10276),rewrite(10555(3),10558(6),200(5),10555(5),10485(4),69(3))]. 10561 $F # answer(assoc_meet). [resolve(10559,a,1677,a(flip))]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=239. Generated=68632. Kept=10542. proofs=7. Usable=126. Sos=5517. Demods=5293. Limbo=59, Disabled=4850. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=58085. Back_subsumed=65. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10022 (9 lex), Back_demodulated=4774. Back_unit_deleted=0. Demod_attempts=934915. Demod_rewrites=147518. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=5. Megabytes=11.35. User_CPU=3.16, System_CPU=0.04, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 7 proofs. Process 3831 exit (max_proofs) Wed Nov 22 11:24:06 2006