============================== Prover9 =============================== Prover9 (32) version March-2007, March 2007. Process 22065 was started by mccune on cleo, Mon Mar 19 17:41:42 2007 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(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 (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 #10 (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 #11 (F,wt=21): 24 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 #12 (T,wt=5): 16 x ^ x = x. [para(9(a,1),8(a,1,2))]. given #13 (T,wt=5): 17 x v x = x. [para(8(a,1),9(a,1,2))]. given #14 (T,wt=9): 27 x ^ (x ^ y) = x ^ y. [para(9(a,1),24(a,2)),rewrite(5(1),2(2),5(4),2(5),9(5),5(4),2(5),9(5),5(3))]. given #15 (T,wt=9): 32 x v (x v y) = x v y. [para(17(a,1),14(a,1)),rewrite(2(3),14(3),17(2)),flip(a)]. given #16 (A,wt=11): 15 x ^ (y ^ z) = y ^ (x ^ z). [para(7(a,1),5(a,1)),rewrite(5(3),5(4))]. given #17 (T,wt=11): 22 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 (T,wt=13): 33 x ^ ((x v y) v (y ^ (x v y))) = x. [back_rewrite(30),rewrite(32(3))]. given #20 (T,wt=15): 42 x v (y v (z v (x ^ u))) = x v (y v z). [para(22(a,1),14(a,2,2)),rewrite(14(6))]. given #21 (A,wt=27): 23 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 #22 (T,wt=15): 47 x ^ (y ^ (z ^ (x v u))) = x ^ (y ^ z). [para(38(a,1),15(a,2,2)),rewrite(15(6))]. given #23 (T,wt=15): 52 x ^ ((x v y) v (y ^ (x v (y v z)))) = x. [para(8(a,1),23(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 #24 (T,wt=15): 56 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 #25 (T,wt=11): 68 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),56(a,2)),rewrite(27(5))]. given #26 (A,wt=25): 28 (x ^ y) v (x ^ (y ^ z)) = (x ^ y) ^ ((x ^ z) v (x ^ (z v (x ^ y)))). [back_rewrite(26),rewrite(27(2))]. given #27 (T,wt=11): 72 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),68(a,1,1)),rewrite(5(4))]. given #28 (T,wt=13): 80 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(68(a,1),68(a,1,1)),rewrite(2(3),68(7))]. given #29 (T,wt=13): 85 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(28(a,2),9(a,1,2)),rewrite(32(6))]. given #30 (T,wt=15): 77 (x ^ (y ^ z)) ^ (y v u) = x ^ (y ^ z). [para(15(a,1),68(a,1,1)),rewrite(15(6))]. given #31 (A,wt=19): 34 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [back_rewrite(25),rewrite(32(3))]. given #32 (T,wt=15): 93 x v ((x ^ y) v (z ^ u)) = x v (z ^ u). [para(28(a,1),42(a,2,2)),rewrite(2(5),14(6),85(5),83(11))]. given #33 (T,wt=15): 108 (x ^ y) ^ (z v (y ^ (x v u))) = x ^ y. [para(38(a,1),72(a,1,1)),rewrite(2(4),38(8))]. given #34 (T,wt=13): 147 x ^ (y v ((x v z) ^ (x v u))) = x. [para(8(a,1),108(a,1,1)),rewrite(8(7))]. given #35 (T,wt=15): 109 x ^ (y v ((x v z) v (z ^ (x v z)))) = x. [para(33(a,1),72(a,1,1)),rewrite(2(5),33(11))]. given #36 (A,wt=17): 35 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(11(a,1),27(a,1,2)),rewrite(11(10))]. given #37 (T,wt=15): 119 (x ^ y) ^ (z v (u v (x ^ y))) = x ^ y. [para(80(a,1),72(a,1,1)),rewrite(2(4),14(4),80(9))]. given #38 (T,wt=15): 123 (x ^ (y ^ z)) ^ (z v u) = x ^ (y ^ z). [para(5(a,1),77(a,1,1,2)),rewrite(5(5))]. given #39 (T,wt=15): 129 x v ((x v y) v (z ^ (x v y))) = x v y. [para(34(a,1),9(a,1,2)),rewrite(14(5))]. given #40 (T,wt=13): 211 (x v y) ^ (x v (y v z)) = x v y. [back_rewrite(172),rewrite(206(5))]. given #41 (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 #42 (T,wt=13): 212 (x v y) v (z ^ (x v y)) = x v y. [back_rewrite(54),rewrite(211(7),2(5),8(6)),flip(a)]. given #43 (T,wt=13): 224 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(39(a,1),9(a,1,2))]. given #44 (T,wt=13): 254 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [back_rewrite(223),rewrite(5(3),244(6),76(5),5(5))]. given #45 (T,wt=11): 299 x ^ (y v (x ^ y)) = x ^ y. [para(8(a,1),254(a,1,2,2)),rewrite(2(2))]. given #46 (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(22(a,1),11(a,1,2,1,2)),rewrite(5(6),2(13)),flip(a)]. given #47 (F,wt=25): 308 x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(299(a,1),11(a,2,2)),rewrite(5(4),22(7),2(7),2(11))]. given #48 (F,wt=29): 309 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),299(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 #49 (F,wt=29): 321 x ^ (((x v y) ^ (z v (x ^ z))) v ((x v z) ^ (y v (x ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(299(a,1),308(a,2,2)),rewrite(5(4),22(7),2(13))]. given #50 (T,wt=13): 293 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(80),rewrite(244(4))]. given #51 (T,wt=13): 322 x ^ ((x v y) v (x ^ (y v z))) = x. [para(211(a,1),309(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 #52 (T,wt=13): 335 (x v y) v (x ^ (y v z)) = x v y. [para(322(a,1),212(a,1,2)),rewrite(2(5),22(5),32(2)),flip(a)]. given #53 (T,wt=13): 338 (x v y) v (y ^ (x v z)) = x v y. [para(2(a,1),335(a,1,1)),rewrite(2(5))]. given #54 (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 #55 (F,wt=25): 356 (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 #56 (F,wt=25): 364 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (x ^ z) v (x ^ y) # label(false). [para(356(a,1),2(a,2)),flip(a)]. given #57 (F,wt=29): 370 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v ((x v (y ^ (x v z))) ^ (z v (x ^ z)))) # label(false). [para(299(a,1),356(a,1,2)),rewrite(22(6),22(10),5(11))]. given #58 (F,wt=29): 372 x ^ ((y ^ (x v z)) v ((x v (y ^ (x v z))) ^ (z v (x ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(370(a,1),2(a,2)),flip(a)]. given #59 (T,wt=13): 371 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(356(a,1),293(a,1,2,2)),rewrite(364(8),175(5))]. given #60 (T,wt=15): 167 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(147(a,1),72(a,1,1)),rewrite(2(5),14(5),147(11))]. given #61 (T,wt=15): 219 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(211(a,1),47(a,2,2)),rewrite(5(5),15(6),211(5))]. given #62 (T,wt=15): 244 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [para(212(a,1),47(a,1,2,2,2)),rewrite(15(5),15(4),16(3),5(6)),flip(a)]. given #63 (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 #64 (T,wt=15): 279 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [back_rewrite(146),rewrite(244(5))]. given #65 (T,wt=15): 281 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [back_rewrite(119),rewrite(244(5))]. given #66 (T,wt=15): 283 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [back_rewrite(108),rewrite(244(5))]. given #67 (T,wt=15): 310 x ^ (y ^ (z v (x ^ z))) = x ^ (y ^ z). [para(299(a,1),15(a,2,2)),rewrite(15(6))]. given #68 (A,wt=19): 50 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 #69 (T,wt=15): 327 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(34(a,1),293(a,1,2))]. given #70 (T,wt=15): 384 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(254(a,1),219(a,1,2)),rewrite(5(2),38(3),5(3),2(5)),flip(a)]. given #71 (T,wt=15): 397 (x v y) v (z ^ (u ^ (x v y))) = x v y. [para(244(a,1),212(a,1,2))]. given #72 (T,wt=15): 399 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(244(a,1),224(a,1,2))]. given #73 (A,wt=19): 60 x ^ (y ^ (z ^ (u ^ (x v v)))) = x ^ (y ^ (z ^ u)). [para(47(a,1),15(a,2,2)),rewrite(15(8))]. given #74 (F,wt=23): 459 x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(false). [para(11(a,1),327(a,1,2,2)),rewrite(2(5),14(6),2(5),2(12),11(13))]. given #75 (F,wt=23): 534 x ^ ((x ^ y) v ((x ^ z) v (z ^ (x v y)))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),459(a,1,2)),rewrite(2(6),14(6),2(10))]. given #76 (F,wt=25): 464 x ^ ((y ^ (x v z)) v ((x v y) ^ (z v (x ^ y)))) = x ^ (z v (x ^ y)) # label(false). [para(327(a,1),39(a,2)),rewrite(2(2),5(4),2(6),22(7),2(7),27(9),2(10))]. given #77 (F,wt=23): 563 x ^ ((y ^ (x v z)) v (x ^ (z v (x ^ y)))) = x ^ (z v (x ^ y)) # label(false). [para(464(a,1),327(a,1,2,2)),rewrite(464(15))]. given #78 (T,wt=15): 460 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(327(a,1),18(a,1,2,1)),rewrite(2(7),9(7),5(5),2(6),244(7),419(6),27(3),15(5),8(4),5(6),27(6)),flip(a)]. given #79 (T,wt=15): 476 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(5(a,1),384(a,1,2,1))]. given #80 (T,wt=11): 621 x ^ (y v (z ^ y)) = x ^ y. [para(147(a,1),476(a,1,2,2)),rewrite(2(2))]. given #81 (T,wt=13): 610 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(9(a,1),476(a,1,2,2,2)),rewrite(5(2),2(3))]. given #82 (A,wt=23): 75 (x v y) ^ ((x ^ z) v (u ^ (x v y))) = (x ^ z) v (u ^ (x v y)). [para(68(a,1),18(a,2,1)),rewrite(14(4),2(3),22(4),2(6),14(6),2(5),68(7),2(5),5(9))]. given #83 (F,wt=19): 604 (x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(534(a,1),460(a,1,2)),rewrite(27(2),32(5),577(8))]. given #84 (F,wt=19): 679 (x ^ y) v (x ^ z) = x ^ ((x ^ z) v (y ^ (x v z))) # label(false). [para(604(a,1),2(a,2))]. given #85 (F,wt=19): 680 (x ^ y) v (y ^ z) = y ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(5(a,1),604(a,1,1)),rewrite(5(4),2(5))]. ============================== PROOF ================================= % Proof 1 at 0.52 (+ 0.00) seconds: H2. % Length of proof is 63. % Level of proof is 21. % Maximum clause weight is 29. % Given clauses 85. 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 v (y v (x ^ z)) = x v y. [para(9(a,1),14(a,2,2)),rewrite(2(4))]. 23 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))]. 24 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))]. 25 (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))]. 27 x ^ (x ^ y) = x ^ y. [para(9(a,1),24(a,2)),rewrite(5(1),2(2),5(4),2(5),9(5),5(4),2(5),9(5),5(3))]. 30 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))]. 32 x v (x v y) = x v y. [para(17(a,1),14(a,1)),rewrite(2(3),14(3),17(2)),flip(a)]. 33 x ^ ((x v y) v (y ^ (x v y))) = x. [back_rewrite(30),rewrite(32(3))]. 34 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [back_rewrite(25),rewrite(32(3))]. 35 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(11(a,1),27(a,1,2)),rewrite(11(10))]. 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))]. 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))]. 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))]. 54 (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),23(a,2,2)),rewrite(2(3),14(3),2(2),5(5),17(8),2(8),5(11),2(13))]. 56 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)]. 68 (x ^ y) ^ (x v z) = x ^ y. [para(16(a,1),56(a,2)),rewrite(27(5))]. 72 (x ^ y) ^ (y v z) = x ^ y. [para(5(a,1),68(a,1,1)),rewrite(5(4))]. 80 (x ^ y) ^ (z v (x ^ y)) = x ^ y. [para(68(a,1),68(a,1,1)),rewrite(2(3),68(7))]. 109 x ^ (y v ((x v z) v (z ^ (x v z)))) = x. [para(33(a,1),72(a,1,1)),rewrite(2(5),33(11))]. 129 x v ((x v y) v (z ^ (x v y))) = x v y. [para(34(a,1),9(a,1,2)),rewrite(14(5))]. 172 (x v y) ^ (x v ((y v z) v (z ^ (y v z)))) = x v y. [para(109(a,1),34(a,1,2,2)),rewrite(5(7),109(13))]. 175 x ^ (y ^ ((x ^ z) v (x ^ u))) = y ^ ((x ^ z) v (x ^ u)). [para(35(a,1),15(a,2,2))]. 206 (x v y) v (y ^ (x v y)) = x v y. [para(33(a,1),129(a,1,2,2)),rewrite(2(6),129(6),17(3)),flip(a)]. 211 (x v y) ^ (x v (y v z)) = x v y. [back_rewrite(172),rewrite(206(5))]. 212 (x v y) v (z ^ (x v y)) = x v y. [back_rewrite(54),rewrite(211(7),2(5),8(6)),flip(a)]. 219 x ^ ((x v y) ^ (z v u)) = x ^ (z v u). [para(211(a,1),47(a,2,2)),rewrite(5(5),15(6),211(5))]. 244 (x ^ y) ^ (z v u) = x ^ (y ^ (z v u)). [para(212(a,1),47(a,1,2,2,2)),rewrite(15(5),15(4),16(3),5(6)),flip(a)]. 293 x ^ (y ^ (z v (x ^ y))) = x ^ y. [back_rewrite(80),rewrite(244(4))]. 327 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(34(a,1),293(a,1,2))]. 356 (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)]. 364 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (x ^ z) v (x ^ y) # label(false). [para(356(a,1),2(a,2)),flip(a)]. 371 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(356(a,1),293(a,1,2,2)),rewrite(364(8),175(5))]. 386 (x v y) ^ ((z v u) ^ ((x ^ v) v (x ^ (z v u)))) = x ^ (z v u). [para(219(a,1),371(a,1,2,1)),rewrite(2(7),244(8),219(12))]. 418 (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)]. 419 (x v y) ^ ((z ^ u) v (z ^ (x v y))) = z ^ (x v y). [back_rewrite(386),rewrite(418(8))]. 459 x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) = (x ^ y) v (x ^ z) # label(false). [para(11(a,1),327(a,1,2,2)),rewrite(2(5),14(6),2(5),2(12),11(13))]. 460 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(327(a,1),18(a,1,2,1)),rewrite(2(7),9(7),5(5),2(6),244(7),419(6),27(3),15(5),8(4),5(6),27(6)),flip(a)]. 534 x ^ ((x ^ y) v ((x ^ z) v (z ^ (x v y)))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),459(a,1,2)),rewrite(2(6),14(6),2(10))]. 577 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(5(a,1),460(a,1,1))]. 604 (x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(534(a,1),460(a,1,2)),rewrite(27(2),32(5),577(8))]. 680 (x ^ y) v (y ^ z) = y ^ ((x ^ y) v (z ^ (x v y))) # label(false). [para(5(a,1),604(a,1,1)),rewrite(5(4),2(5))]. 762 $F # answer(H2). [para(680(a,2),13(a,1,2,2)),rewrite(5(8),2(9),22(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=85. Generated=12784. Kept=756. proofs=1. Usable=61. Sos=425. Demods=446. Limbo=1, Disabled=277. Hints=0. Weight_deleted=3304. Literals_deleted=0. Forward_subsumed=8723. Back_subsumed=39. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=695 (6 lex), Back_demodulated=230. Back_unit_deleted=0. Demod_attempts=301779. Demod_rewrites=72401. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.89. User_CPU=0.52, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 22065 exit (max_proofs) Mon Mar 19 17:41:42 2007