============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 6676 was started by mccune on cleo, Tue Nov 3 10:20:08 2009 The command was "/home/mccune/LADR/bin/prover9 -f LT.in LT-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file LT.in assign(max_seconds,30). set(lex_order_vars). assign(max_weight,30). 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])]). 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(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v y = 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]. c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, ^, v ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) Auto_process settings: (no changes). % Operation v is commutative; C redundancy checks enabled. kept: 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. kept: 4 x v (y v z) = z v (x v y). [copy(3),rewrite([2(2)]),flip(a)]. % Operation ^ is commutative; C redundancy checks enabled. kept: 5 x ^ y = y ^ x. [assumption]. 6 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. kept: 7 x ^ (y ^ z) = z ^ (x ^ y). [copy(6),rewrite([5(2)]),flip(a)]. kept: 8 x ^ (x v y) = x. [assumption]. kept: 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]. kept: 11 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [copy(10),rewrite([2(8)]),flip(a),rewrite([2(5),2(9)])]. 12 c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2) # answer(H2). [deny(1)]. kept: 13 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # 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 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # 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.01 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 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(12),rewrite([2(12)])]. 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 w)))) = 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 ^ w)))) = 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 ^ w)))) = x. [para(244(a,1),224(a,1,2))]. given #73 (A,wt=19): 60 x ^ (y ^ (z ^ (u ^ (x v w)))) = 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.58 (+ 0.00) seconds: H2. % Length of proof is 63. % Level of proof is 21. % Maximum clause weight is 29.000. % Given clauses 85. 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2) # label(non_clause) # 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 c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2) # answer(H2). [deny(1)]. 13 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # 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 ^ w) 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 ^ w) v (x ^ v5))) = (z v u) ^ ((x ^ w) v (x ^ v5)). [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=12601. Kept=756. proofs=1. Usable=61. Sos=425. Demods=446. Limbo=1, Disabled=277. Hints=0. Kept_by_rule=0, Deleted_by_rule=3300. Forward_subsumed=8544. 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=299458. Demod_rewrites=71778. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.90. User_CPU=0.58, System_CPU=0.00, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 6676 exit (max_proofs) Tue Nov 3 10:20:09 2009