============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4385 was started by mccune on cleo.thornwood, Wed Nov 22 12:03:35 2006 The command was "/home/mccune/bin/prover9 -f LT.in LT-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file LT.in set(lex_order_vars). assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_weight,30). assign(max_minutes,10). % assign(max_minutes, 10) -> assign(max_seconds, 600). formulas(sos). 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. end_of_list. formulas(sos). (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). end_of_list. formulas(goals). x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2). end_of_list. % Reading from file LT-interp.outx list(interpretations). interpretation(6,[number = 1,seconds = 0],[function(_ ^ _,[0,0,0,0,0,0,0,1,2,3,4,5,0,2,2,0,0,0,0,3,0,3,5,5,0,4,0,5,4,5,0,5,0,5,5,5]),function(_ v _,[0,1,2,3,4,5,1,1,1,1,1,1,2,1,2,1,1,1,3,1,1,3,1,3,4,1,1,1,4,4,5,1,1,3,4,5]),function(c1,[2]),function(c2,[3]),function(c3,[4]),function(c4,[2]),function(c5,[3]),function(c6,[4])]). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2) # 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 = y v x. [assumption]. (x v y) v z = x v (y v z). [assumption]. x ^ y = y ^ x. [assumption]. (x ^ y) ^ z = x ^ (y ^ z). [assumption]. x ^ (x v y) = x. [assumption]. x v (x ^ y) = x. [assumption]. (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [assumption]. c7 ^ (c8 v (c9 ^ ((c7 ^ (c8 v c9)) v (c8 ^ c9)))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label H2 to answer in negative clause Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c7, c8, c9, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [copy(12),rewrite(2(12))]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 x v y = y v x. [assumption]. 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. 5 x ^ y = y ^ x. [assumption]. 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. 13 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [copy(12),rewrite(2(12))]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. % (lex-dep) 5 x ^ y = y ^ x. [assumption]. % (lex-dep) 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. % (lex-dep) 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 x v y = y v x. [assumption]. given #2 (I,wt=11): 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. given #3 (I,wt=7): 5 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. given #5 (I,wt=7): 8 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 9 x v (x ^ y) = x. [assumption]. given #7 (I,wt=21): 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. given #8 (I,wt=23): 13 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [copy(12),rewrite(2(12))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(2(a,1),13(a,1,2,2,2,2,2)),rewrite(2(10))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(2(a,1),13(a,1,2,2,2)),rewrite(2(12))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(2(a,1),13(a,1,2)),rewrite(2(14))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(2(a,1),13(a,2,2)),rewrite(2(21))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,1,2,2,2,1)),rewrite(5(6))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,1,2,2,2,2)),rewrite(5(11))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,1,2,2)),rewrite(5(13))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,1)),rewrite(5(15))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,2,2,2)),rewrite(5(20))]. not interpretable: c7 % Clause contains symbol not in interpretation: % c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [para(5(a,1),13(a,2)),rewrite(5(22))]. given #9 (F,wt=21): 18 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (z ^ x) v (x ^ y) # label(false). [para(11(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. given #10 (F,wt=21): 22 x ^ ((y ^ (z v x)) v (z ^ (y v x))) = (z ^ x) v (y ^ x) # label(false). [para(18(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. given #11 (F,wt=5): 16 x ^ x = x. [para(9(a,1),8(a,1,2))]. given #12 (T,wt=5): 17 x v x = x. [para(8(a,1),9(a,1,2))]. given #13 (A,wt=11): 14 x v (y v z) = y v (x v z). [para(4(a,1),2(a,1)),rewrite(2(3),2(4))]. given #14 (F,wt=9): 25 x ^ (x ^ y) = x ^ y. [para(9(a,1),22(a,2)),rewrite(5(1),2(2),5(4),2(5),9(5),5(4),2(5),9(5),5(3))]. given #15 (F,wt=9): 32 x v (x v y) = x v y. [para(14(a,1),17(a,1)),rewrite(2(2),14(2),17(1))]. given #16 (F,wt=11): 15 x ^ (y ^ z) = y ^ (x ^ z). [para(7(a,1),5(a,1)),rewrite(5(3),5(4))]. given #17 (F,wt=11): 30 x v (y v (x ^ z)) = x v y. [para(9(a,1),14(a,2,2)),rewrite(2(4))]. given #18 (T,wt=11): 38 x ^ (y ^ (x v z)) = x ^ y. [para(8(a,1),15(a,2,2)),rewrite(5(4))]. given #19 (A,wt=25): 26 (x ^ y) v (x ^ (y ^ z)) = (x ^ y) ^ ((x ^ z) v (x ^ (z v (x ^ y)))). [back_rewrite(24),rewrite(25(2))]. given #20 (F,wt=13): 34 x ^ ((x v y) v (y ^ (x v y))) = x. [back_rewrite(28),rewrite(32(3))]. given #21 (F,wt=13): 52 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(26(a,2),9(a,1,2)),rewrite(32(6))]. given #22 (F,wt=15): 42 x v (y v (z v (x ^ u))) = x v (y v z). [para(30(a,1),14(a,2,2)),rewrite(14(6))]. given #23 (F,wt=15): 47 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(38(a,1),15(a,2,2)),rewrite(15(6))]. given #24 (T,wt=15): 69 x v ((x ^ y) v (z ^ u)) = x v (z ^ u). [para(52(a,1),42(a,2,2)),rewrite(2(5),14(6),52(5))]. given #25 (A,wt=21): 27 x ^ ((x ^ y) v ((x ^ z) ^ (x v y))) = (x ^ y) v (x ^ z). [back_rewrite(21),rewrite(25(9))]. given #26 (F,wt=15): 70 x ^ ((y ^ z) ^ (y v u)) = x ^ (y ^ z). [para(11(a,1),47(a,1,2,2)),rewrite(5(4),2(5),15(7),44(6),15(2),5(1),5(5),5(6),15(6)),flip(a)]. given #27 (F,wt=11): 87 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),70(a,2)),rewrite(25(5))]. given #28 (F,wt=11): 92 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),87(a,1,1)),rewrite(5(4))]. given #29 (F,wt=13): 99 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(87(a,1),87(a,1,1)),rewrite(2(3),87(7))]. given #30 (T,wt=15): 97 (x ^ (y ^ z)) ^ (y v u) = x ^ (y ^ z). [para(15(a,1),87(a,1,1)),rewrite(15(6))]. given #31 (A,wt=27): 31 x ^ (((x v y) ^ (z v u)) v (y ^ (x v (z v u)))) = (x ^ y) v (x ^ (z v u)). [para(14(a,1),11(a,1,2,1,2)),rewrite(14(2),5(6),2(7),2(12))]. given #32 (F,wt=15): 108 (x ^ y) ^ (z v (y ^ (x v u))) = x ^ y. [para(38(a,1),92(a,1,1)),rewrite(2(4),38(8))]. given #33 (F,wt=13): 132 x ^ (y v ((x v z) ^ (x v u))) = x. [para(8(a,1),108(a,1,1)),rewrite(8(7))]. given #34 (F,wt=15): 109 x ^ (y v ((x v z) v (z ^ (x v z)))) = x. [para(34(a,1),92(a,1,1)),rewrite(2(5),34(11))]. given #35 (F,wt=15): 118 (x ^ y) ^ (z v (u v (x ^ y))) = x ^ y. [para(99(a,1),92(a,1,1)),rewrite(2(4),14(4),99(9))]. given #36 (T,wt=15): 119 (x ^ (y ^ z)) ^ (z v u) = x ^ (y ^ z). [para(5(a,1),97(a,1,1,2)),rewrite(5(5))]. given #37 (A,wt=19): 35 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [back_rewrite(23),rewrite(32(3))]. given #38 (F,wt=15): 124 x ^ ((x v y) v (y ^ (x v (y v z)))) = x. [para(8(a,1),31(a,1,2,1)),rewrite(2(3),14(3),2(2),32(4),2(9),14(9),2(8),8(10),2(8),9(8))]. given #39 (F,wt=15): 131 (x ^ y) ^ (z v (x ^ (y v u))) = x ^ y. [para(108(a,1),5(a,2)),rewrite(5(4),5(5),5(6))]. given #40 (F,wt=15): 149 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(132(a,1),92(a,1,1)),rewrite(2(5),14(5),132(11))]. given #41 (F,wt=15): 180 x v ((x v y) v (z ^ (x v y))) = x v y. [para(35(a,1),9(a,1,2)),rewrite(14(5))]. given #42 (T,wt=13): 228 (x v y) ^ (x v (y v z)) = x v y. [back_rewrite(193),rewrite(223(5))]. given #43 (A,wt=17): 36 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(11(a,1),25(a,1,2)),rewrite(11(10))]. given #44 (F,wt=13): 229 (x v y) v (z ^ (x v y)) = x v y. [back_rewrite(126),rewrite(228(7),2(5),8(6)),flip(a)]. given #45 (F,wt=13): 285 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(99),rewrite(244(4))]. given #46 (F,wt=13): 293 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [back_rewrite(44),rewrite(244(6),96(5))]. given #47 (F,wt=11): 297 x ^ (y v (x ^ y)) = x ^ y. [para(8(a,1),293(a,1,2,2)),rewrite(2(2))]. given #48 (T,wt=15): 236 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(228(a,1),47(a,2,2)),rewrite(5(5),15(6),228(5))]. given #49 (A,wt=25): 39 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(11(a,1),15(a,2,2)),rewrite(2(5),2(10))]. given #50 (F,wt=25): 306 x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(297(a,1),11(a,2,2)),rewrite(5(4),30(7),2(7),2(11))]. given #51 (F,wt=25): 332 x ^ ((y ^ (x v z)) v ((y v x) ^ (z v (x ^ z)))) = (y ^ x) v (x ^ z) # label(false). [para(306(a,1),5(a,2)),rewrite(2(3),5(8),5(10),2(11))]. given #52 (F,wt=29): 307 x ^ ((x ^ y) v ((x ^ z) v ((z ^ (x v y)) v (y ^ (x v z))))) = (x ^ y) v (x ^ z) # label(false). [para(11(a,1),297(a,1,2,2)),rewrite(2(5),2(8),2(9),14(9),2(8),14(8),2(7),14(9),14(8),2(15),11(16))]. given #53 (F,wt=25): 338 x ^ ((x ^ y) v ((z ^ (x v y)) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(false). [para(307(a,1),18(a,1,2,1)),rewrite(2(6),2(10),2(17),2(19),244(20),38(20),2(12),14(12),17(11),5(11),102(11),2(10),244(12),2(18),5(20),2(21),312(21)),flip(a)]. given #54 (T,wt=13): 318 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(8(a,1),39(a,1,2)),rewrite(38(3),2(6),244(7),45(6)),flip(a)]. given #55 (A,wt=29): 40 (x ^ y) v (x ^ (z v (x ^ u))) = x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ u)))). [para(30(a,1),11(a,1,2,1,2)),rewrite(5(6),2(13)),flip(a)]. given #56 (F,wt=25): 340 x ^ ((x ^ y) v ((y ^ (x v z)) v (z ^ (x v y)))) = (x ^ z) v (x ^ y) # label(false). [para(2(a,1),338(a,1,2)),rewrite(2(5),2(7),2(11))]. given #57 (F,wt=29): 336 x ^ (((x v y) ^ (z v (x ^ z))) v ((x v z) ^ (y v (x ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(297(a,1),306(a,2,2)),rewrite(5(4),30(7),2(13))]. given #58 (F,wt=29): 342 x ^ ((x ^ y) v ((z ^ (x v y)) v ((x v z) ^ (y v (x ^ y))))) = (x ^ y) v (x ^ z) # label(false). [para(297(a,1),338(a,1,2,1)),rewrite(30(4),5(7),297(13))]. given #59 (F,wt=29): 343 x ^ ((x ^ y) v ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ z))))) = (x ^ y) v (x ^ z) # label(false). [para(297(a,1),338(a,2,2)),rewrite(5(5),30(8),2(8))]. given #60 (T,wt=13): 319 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(39(a,1),9(a,1,2))]. given #61 (A,wt=29): 43 x ^ ((y ^ ((x v z) ^ (x v u))) v (z ^ (x v (y ^ (x v u))))) = (x ^ z) v (x ^ y). [para(38(a,1),11(a,2,1)),rewrite(5(8),15(8),2(9),2(13))]. given #62 (F,wt=25): 363 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) # label(false). [para(16(a,1),43(a,1,2,1,2)),rewrite(2(11)),flip(a)]. given #63 (F,wt=25): 371 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (x ^ z) v (x ^ y) # label(false). [para(363(a,1),2(a,2)),flip(a)]. given #64 (F,wt=29): 377 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v ((x v (y ^ (x v z))) ^ (z v (x ^ z)))) # label(false). [para(297(a,1),363(a,1,2)),rewrite(30(6),30(10),5(11))]. given #65 (F,wt=29): 378 x ^ ((y ^ (x v z)) v ((x v (y ^ (x v z))) ^ (z v (x ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(377(a,1),2(a,2)),flip(a)]. given #66 (T,wt=13): 339 x ^ ((x v y) v (x ^ (y v z))) = x. [para(228(a,1),307(a,1,2,2,2,1)),rewrite(8(4),32(6),5(6),9(7),32(4),2(4),8(9),2(8),9(8))]. given #67 (A,wt=19): 45 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(11(a,1),38(a,2)),rewrite(2(5),5(7),39(8),2(8))]. given #68 (F,wt=13): 386 (x v y) v (x ^ (y v z)) = x v y. [para(339(a,1),229(a,1,2)),rewrite(2(5),30(5),32(2)),flip(a)]. given #69 (F,wt=13): 396 (x v y) v (y ^ (x v z)) = x v y. [para(2(a,1),386(a,1,1)),rewrite(2(5))]. given #70 (F,wt=15): 244 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [para(229(a,1),47(a,1,2,2,2)),rewrite(15(5),15(4),16(3),5(6)),flip(a)]. given #71 (F,wt=15): 278 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [back_rewrite(131),rewrite(244(5))]. given #72 (T,wt=15): 280 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [back_rewrite(118),rewrite(244(5))]. given #73 (A,wt=19): 55 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(15(a,1),26(a,2,1)),rewrite(5(4),15(4),5(3),15(8),50(15))]. given #74 (F,wt=15): 282 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [back_rewrite(108),rewrite(244(5))]. given #75 (F,wt=15): 296 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(35(a,1),285(a,1,2))]. given #76 (F,wt=23): 470 x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(false). [para(11(a,1),296(a,1,2,2)),rewrite(2(5),14(6),2(5),2(12),11(13))]. given #77 (F,wt=23): 488 x ^ ((x ^ y) v ((x ^ z) v (z ^ (x v y)))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),470(a,1,2)),rewrite(2(6),14(6),2(10))]. given #78 (T,wt=15): 308 x ^ (y ^ (z v (x ^ z))) = x ^ (y ^ z). [para(297(a,1),15(a,2,2)),rewrite(15(6))]. given #79 (A,wt=17): 64 (x ^ y) v (x ^ ((y ^ z) v (y ^ u))) = x ^ y. [para(11(a,1),52(a,1,2,2))]. given #80 (F,wt=25): 478 x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ y)))) = x ^ (z v (x ^ y)) # label(false). [para(296(a,1),39(a,2)),rewrite(2(2),5(4),2(6),30(7),2(7),25(9),2(10))]. given #81 (F,wt=23): 542 x ^ ((y ^ (x v z)) v (x ^ (z v (x ^ y)))) = x ^ (z v (x ^ y)) # label(false). [para(478(a,1),296(a,1,2,2)),rewrite(478(15))]. given #82 (F,wt=23): 544 x ^ ((y ^ (x v z)) v (x ^ (z v (y ^ x)))) = x ^ (z v (y ^ x)) # label(false). [para(542(a,1),5(a,2)),rewrite(5(3),5(7),5(8))]. given #83 (F,wt=25): 535 x ^ ((y ^ (x v z)) v ((y v x) ^ (z v (y ^ x)))) = x ^ (z v (y ^ x)) # label(false). [para(478(a,1),5(a,2)),rewrite(2(3),5(4),5(8),5(9))]. given #84 (T,wt=15): 315 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(293(a,1),236(a,1,2)),rewrite(5(2),38(3),5(3),2(5)),flip(a)]. given #85 (A,wt=19): 68 x v (y v (z v (u v (x ^ v)))) = x v (y v (z v u)). [para(42(a,1),14(a,2,2)),rewrite(14(8))]. given #86 (F,wt=27): 481 x ^ ((x ^ y) v ((x ^ z) v ((x v y) ^ (z v (x ^ z))))) = (x ^ y) v (x ^ z) # label(false). [para(336(a,1),296(a,1,2,2)),rewrite(2(7),14(8),2(7),2(18),336(19))]. given #87 (F,wt=27): 499 x ^ ((x ^ y) v ((x ^ z) v ((x v z) ^ (y v (x ^ y))))) = (x ^ y) v (x ^ z) # label(false). [para(297(a,1),470(a,1,2,1)),rewrite(5(6),297(12))]. given #88 (F,wt=27): 551 x ^ (((x v y) ^ (z v (x ^ z))) v (x ^ (y v (x ^ z)))) = x ^ (y v (x ^ z)) # label(false). [para(297(a,1),542(a,1,2,2,2,2)),rewrite(5(4),297(12))]. given #89 (F,wt=27): 600 x ^ ((x ^ (y v (x ^ z))) v ((x v y) ^ (z v (x ^ z)))) = x ^ (y v (x ^ z)) # label(false). [para(2(a,1),551(a,1,2,1,1)),rewrite(2(1),2(8))]. given #90 (T,wt=15): 423 (x v y) v (z ^ (u ^ (x v y))) = x v y. [para(244(a,1),229(a,1,2))]. given #91 (A,wt=19): 74 x ^ (y ^ (z ^ (u ^ (x v v)))) = x ^ (y ^ (z ^ u)). [para(47(a,1),15(a,2,2)),rewrite(15(8))]. given #92 (F,wt=29): 538 x ^ (((x v y) ^ (z v (x ^ z))) v ((x v z) ^ (y v (x ^ z)))) = x ^ (y v (x ^ z)) # label(false). [para(297(a,1),478(a,1,2,2,2,2)),rewrite(5(4),30(7),297(13))]. given #93 (F,wt=29): 621 x ^ (((x v y) ^ (z v (x ^ y))) v ((x v z) ^ (y v (x ^ y)))) = x ^ (z v (x ^ y)) # label(false). [para(2(a,1),538(a,1,2,1,1)),rewrite(2(1),2(9))]. given #94 (F,wt=15): 433 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(244(a,1),319(a,1,2))]. given #95 (F,wt=15): 471 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(296(a,1),18(a,1,2,1)),rewrite(2(7),9(7),5(5),2(6),244(7),438(6),25(3),15(5),8(4),5(6),25(6)),flip(a)]. given #96 (T,wt=15): 554 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(5(a,1),315(a,1,2,1))]. given #97 (A,wt=23): 76 x v ((x ^ y) v ((z ^ u) v (z ^ v))) = x v ((z ^ u) v (z ^ v)). [para(11(a,1),69(a,1,2,2)),rewrite(11(12))]. given #98 (F,wt=19): 656 (x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(488(a,1),471(a,1,2)),rewrite(25(2),32(5),631(8))]. given #99 (F,wt=19): 704 (x ^ y) v (x ^ z) = x ^ ((x ^ z) v (y ^ (x v z))) # label(false). [para(656(a,1),2(a,2))]. given #100 (F,wt=19): 705 (x ^ y) v (y ^ z) = y ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(5(a,1),656(a,1,1)),rewrite(5(4),2(5))]. ============================== PROOF ================================= % Proof 1 at 0.92 (+ 0.00) seconds: H2. % Length of proof is 58. % Level of proof is 20. % Maximum clause weight is 29. % Given clauses 100. 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2) # label(goal). [goal]. 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x v (y v z) = z v (x v y). [copy(3),rewrite(2(2)),flip(a)]. 5 x ^ y = y ^ x. [assumption]. 6 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite(5(2)),flip(a)]. 8 x ^ (x v y) = x. [assumption]. 9 x v (x ^ y) = x. [assumption]. 10 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [assumption]. 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [copy(10),rewrite(2(8)),flip(a),rewrite(2(5),2(9))]. 12 c7 ^ (c8 v (c9 ^ ((c7 ^ (c8 v c9)) v (c8 ^ c9)))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2) # answer(H2). [deny(1)]. 13 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # answer(H2). [copy(12),rewrite(2(12))]. 14 x v (y v z) = y v (x v z). [para(4(a,1),2(a,1)),rewrite(2(3),2(4))]. 15 x ^ (y ^ z) = y ^ (x ^ z). [para(7(a,1),5(a,1)),rewrite(5(3),5(4))]. 16 x ^ x = x. [para(9(a,1),8(a,1,2))]. 17 x v x = x. [para(8(a,1),9(a,1,2))]. 18 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (z ^ x) v (x ^ y) # label(false). [para(11(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. 22 x ^ ((y ^ (z v x)) v (z ^ (y v x))) = (z ^ x) v (y ^ x) # label(false). [para(18(a,1),5(a,2)),rewrite(2(3),2(5),5(6),5(8),2(9))]. 23 (x v y) ^ (x v (z ^ (x v (x v y)))) = x v (z ^ (x v y)). [para(8(a,1),18(a,2,1)),rewrite(2(6),14(6),2(5),8(7),2(5),5(8))]. 25 x ^ (x ^ y) = x ^ y. [para(9(a,1),22(a,2)),rewrite(5(1),2(2),5(4),2(5),9(5),5(4),2(5),9(5),5(3))]. 28 x ^ ((x v y) v (y ^ (x v (x v y)))) = x. [para(16(a,1),11(a,1,2,1)),rewrite(8(9),2(8),9(8))]. 30 x v (y v (x ^ z)) = x v y. [para(9(a,1),14(a,2,2)),rewrite(2(4))]. 31 x ^ (((x v y) ^ (z v u)) v (y ^ (x v (z v u)))) = (x ^ y) v (x ^ (z v u)). [para(14(a,1),11(a,1,2,1,2)),rewrite(14(2),5(6),2(7),2(12))]. 32 x v (x v y) = x v y. [para(14(a,1),17(a,1)),rewrite(2(2),14(2),17(1))]. 34 x ^ ((x v y) v (y ^ (x v y))) = x. [back_rewrite(28),rewrite(32(3))]. 35 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [back_rewrite(23),rewrite(32(3))]. 38 x ^ (y ^ (x v z)) = x ^ y. [para(8(a,1),15(a,2,2)),rewrite(5(4))]. 39 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(11(a,1),15(a,2,2)),rewrite(2(5),2(10))]. 44 (x ^ (y v z)) ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(11(a,1),38(a,1,2)),rewrite(5(4),2(5),5(9),15(9),8(8))]. 45 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(11(a,1),38(a,2)),rewrite(2(5),5(7),39(8),2(8))]. 47 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(38(a,1),15(a,2,2)),rewrite(15(6))]. 70 x ^ ((y ^ z) ^ (y v u)) = x ^ (y ^ z). [para(11(a,1),47(a,1,2,2)),rewrite(5(4),2(5),15(7),44(6),15(2),5(1),5(5),5(6),15(6)),flip(a)]. 87 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),70(a,2)),rewrite(25(5))]. 92 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),87(a,1,1)),rewrite(5(4))]. 99 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(87(a,1),87(a,1,1)),rewrite(2(3),87(7))]. 109 x ^ (y v ((x v z) v (z ^ (x v z)))) = x. [para(34(a,1),92(a,1,1)),rewrite(2(5),34(11))]. 126 (x v y) ^ ((z ^ (x v y)) v ((x v y) ^ (x v (y v z)))) = (x v y) v (z ^ (x v y)). [para(16(a,1),31(a,2,2)),rewrite(2(3),14(3),2(2),5(5),17(8),2(8),5(11),2(13))]. 180 x v ((x v y) v (z ^ (x v y))) = x v y. [para(35(a,1),9(a,1,2)),rewrite(14(5))]. 193 (x v y) ^ (x v ((y v z) v (z ^ (y v z)))) = x v y. [para(109(a,1),35(a,1,2,2)),rewrite(5(7),109(13))]. 223 (x v y) v (y ^ (x v y)) = x v y. [para(34(a,1),180(a,1,2,2)),rewrite(2(6),180(6),17(3)),flip(a)]. 228 (x v y) ^ (x v (y v z)) = x v y. [back_rewrite(193),rewrite(223(5))]. 229 (x v y) v (z ^ (x v y)) = x v y. [back_rewrite(126),rewrite(228(7),2(5),8(6)),flip(a)]. 236 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(228(a,1),47(a,2,2)),rewrite(5(5),15(6),228(5))]. 244 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [para(229(a,1),47(a,1,2,2,2)),rewrite(15(5),15(4),16(3),5(6)),flip(a)]. 285 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(99),rewrite(244(4))]. 296 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(35(a,1),285(a,1,2))]. 318 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(8(a,1),39(a,1,2)),rewrite(38(3),2(6),244(7),45(6)),flip(a)]. 349 (x v y) ^ ((z v u) ^ ((x ^ v) v (x ^ (z v u)))) = x ^ (z v u). [para(236(a,1),318(a,1,2,1)),rewrite(2(7),244(8),236(12))]. 434 (x v y) ^ ((z v u) ^ ((x ^ v) v (x ^ w))) = (z v u) ^ ((x ^ v) v (x ^ w)). [para(45(a,1),244(a,1,1)),rewrite(5(5),5(11)),flip(a)]. 438 (x v y) ^ ((z ^ u) v (z ^ (x v y))) = z ^ (x v y). [back_rewrite(349),rewrite(434(8))]. 470 x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(false). [para(11(a,1),296(a,1,2,2)),rewrite(2(5),14(6),2(5),2(12),11(13))]. 471 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(296(a,1),18(a,1,2,1)),rewrite(2(7),9(7),5(5),2(6),244(7),438(6),25(3),15(5),8(4),5(6),25(6)),flip(a)]. 488 x ^ ((x ^ y) v ((x ^ z) v (z ^ (x v y)))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),470(a,1,2)),rewrite(2(6),14(6),2(10))]. 631 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(5(a,1),471(a,1,1))]. 656 (x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(488(a,1),471(a,1,2)),rewrite(25(2),32(5),631(8))]. 705 (x ^ y) v (y ^ z) = y ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(5(a,1),656(a,1,1)),rewrite(5(4),2(5))]. 792 $F # answer(H2). [para(705(a,2),13(a,1,2,2)),rewrite(5(8),2(9),30(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=100. Generated=18975. Kept=786. proofs=1. Usable=65. Sos=444. Demods=465. Limbo=1, Disabled=284. Hints=0. Weight_deleted=6697. Literals_deleted=0. Forward_subsumed=11491. Back_subsumed=40. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=722 (6 lex), Back_demodulated=236. Back_unit_deleted=0. Demod_attempts=536279. Demod_rewrites=123446. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.93. User_CPU=0.92, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4385 exit (max_proofs) Wed Nov 22 12:03:36 2006