============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 9935 was started by mccune on cleo.thornwood, Sat Aug 12 20:54:00 2006 The command was "/home/mccune/bin/prover9 -f LT-82-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file LT-82-2.in assign(order,kbo). assign(max_weight,25). assign(max_seconds,3600). 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. list(interpretations). interpretation(6,[],[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). [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: Function symbol KB weights: c1=1. c2=1. c3=1. ^=1. v=1. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, ^, v ]). Skipping inverse_order, because term ordering is KBO. 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: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(10),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]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 9 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [copy(8),flip(a)]. 11 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(10),rewrite(2(12))]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. % (lex-dep) 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 9 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [copy(8),flip(a)]. 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): 3 (x v y) v z = x v (y v z). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 12 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 14 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=21): 9 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [copy(8),flip(a)]. given #8 (I,wt=23): 11 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(10),rewrite(2(12))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(2(a,1),11(a,1,2,2,2,2,2)),rewrite(2(10))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(2(a,1),11(a,1,2,2,2)),rewrite(2(12))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(2(a,1),11(a,1,2)),rewrite(2(14))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(2(a,1),11(a,2,2)),rewrite(2(21))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,1,2,2,2,1)),rewrite(4(6))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,1,2,2,2,2)),rewrite(4(11))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,1,2,2)),rewrite(4(13))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,1)),rewrite(4(15))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,2,2,2)),rewrite(4(20))]. not interpretable: c1 % Clause contains symbol not in interpretation: % c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [para(4(a,1),11(a,2)),rewrite(4(22))]. given #9 (T,wt=5): 24 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #10 (T,wt=5): 25 x v x = x. [para(6(a,1),7(a,1,2))]. given #11 (A,wt=11): 13 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #12 (F,wt=21): 26 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),9(a,1,2,1,2))]. given #13 (F,wt=21): 27 x ^ ((y ^ (x v z)) v (z ^ (y v x))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),9(a,1,2,2,2))]. given #14 (T,wt=7): 16 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #15 (T,wt=7): 22 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #16 (A,wt=11): 15 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #17 (F,wt=21): 28 x ^ ((y ^ (x v z)) v ((x v y) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),9(a,1,2,1)),rewrite(2(5))]. given #18 (F,wt=21): 40 x ^ ((y ^ (z v x)) v (z ^ (y v x))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),26(a,1,2,2,2))]. given #19 (T,wt=9): 31 x ^ (x ^ y) = x ^ y. [para(24(a,1),5(a,1,1)),flip(a)]. given #20 (T,wt=9): 33 x ^ (y ^ x) = y ^ x. [para(24(a,1),5(a,2,2)),rewrite(4(2))]. given #21 (A,wt=13): 17 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #22 (F,wt=21): 41 x ^ ((y ^ (x v z)) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),26(a,1,2,1)),rewrite(2(5))]. given #23 (F,wt=21): 42 x ^ ((y ^ (z v x)) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),26(a,1,2,2))]. given #24 (T,wt=9): 35 x v (x v y) = x v y. [para(25(a,1),3(a,1,1)),flip(a)]. given #25 (T,wt=9): 37 x v (y v x) = y v x. [para(25(a,1),3(a,2,2)),rewrite(2(2))]. given #26 (A,wt=11): 18 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #27 (F,wt=21): 69 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),28(a,1,2,1))]. given #28 (F,wt=21): 79 x ^ ((y ^ (z v x)) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),40(a,1,2,1)),rewrite(2(5))]. given #29 (T,wt=9): 38 x ^ (y v (x v z)) = x. [para(13(a,1),6(a,1,2))]. given #30 (T,wt=9): 49 x ^ (y v (z v x)) = x. [para(3(a,1),16(a,1,2))]. given #31 (A,wt=13): 19 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #32 (F,wt=21): 100 x ^ (((x v y) ^ z) v ((z v x) ^ y)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),41(a,1,2,1))]. given #33 (F,wt=21): 109 x ^ (((y v x) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),42(a,1,2,1))]. given #34 (T,wt=9): 57 x v (y ^ (z ^ x)) = x. [para(5(a,1),22(a,1,2))]. given #35 (T,wt=9): 63 x v (y ^ (x ^ z)) = x. [para(15(a,1),7(a,1,2))]. given #36 (A,wt=11): 20 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #37 (F,wt=21): 132 x ^ (((y v x) ^ z) v ((z v x) ^ y)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),79(a,1,2,1))]. given #38 (F,wt=25): 87 x ^ (((x v y) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(31(a,1),28(a,1,2,2)),rewrite(2(7),18(11))]. given #39 (T,wt=11): 39 x v (y v (x ^ z)) = y v x. [para(7(a,1),13(a,1,2)),flip(a)]. given #40 (T,wt=11): 50 x ^ ((y v x) ^ z) = x ^ z. [para(16(a,1),5(a,1,1)),flip(a)]. given #41 (A,wt=13): 21 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #42 (F,wt=25): 90 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z) # label(false). [para(33(a,1),28(a,1,2,2)),rewrite(2(7),62(11))]. given #43 (F,wt=25): 107 x ^ (((y v x) ^ z) v (y ^ (x v ((y v x) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(31(a,1),41(a,1,2,2)),rewrite(2(7),50(11))]. given #44 (T,wt=11): 55 x v ((y ^ x) v z) = x v z. [para(22(a,1),3(a,1,1)),flip(a)]. given #45 (T,wt=11): 60 x v (y v (z ^ x)) = y v x. [para(22(a,1),13(a,1,2)),flip(a)]. given #46 (A,wt=13): 23 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #47 (F,wt=25): 108 x ^ ((y ^ (z v x)) v (z ^ (x v (y ^ (z v x))))) = (y ^ x) v (x ^ z) # label(false). [para(33(a,1),41(a,1,2,2)),rewrite(2(7),67(11))]. given #48 (F,wt=25): 216 x ^ (((y v x) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(2(a,1),87(a,1,2,1,1))]. given #49 (T,wt=11): 62 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),15(a,1,2)),flip(a)]. given #50 (T,wt=11): 67 x ^ (y ^ (z v x)) = y ^ x. [para(16(a,1),15(a,1,2)),flip(a)]. given #51 (A,wt=25): 29 x ^ (((y ^ (x v z)) v (z ^ (x v y))) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(9(a,1),5(a,1,1)),flip(a)]. given #52 (F,wt=25): 217 x ^ (((x v y) ^ z) v (y ^ (x v ((y v x) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(2(a,1),87(a,1,2,2,2,2,1))]. given #53 (F,wt=25): 218 x ^ ((y ^ (x v z)) v (z ^ (x v ((x v z) ^ y)))) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),87(a,1,2,1))]. given #54 (T,wt=11): 119 (x v y) ^ (y v x) = x v y. [para(37(a,1),17(a,1,2))]. given #55 (T,wt=11): 126 (x v y) ^ (z ^ x) = z ^ x. [para(33(a,1),18(a,2)),rewrite(89(4))]. given #56 (A,wt=25): 43 x ^ (((y ^ (z v x)) v (z ^ (x v y))) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(26(a,1),5(a,1,1)),flip(a)]. given #57 (F,wt=25): 219 x ^ (((x v y) ^ z) v (y ^ (x v (z ^ (x v y))))) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),87(a,1,2,2,2,2))]. given #58 (F,wt=25): 249 x ^ ((y ^ (z v x)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z) # label(false). [para(2(a,1),90(a,1,2,1,2))]. given #59 (T,wt=11): 137 x ^ (y v (z v (x v u))) = x. [para(3(a,1),38(a,1,2))]. given #60 (T,wt=11): 150 x ^ (y v (z v (u v x))) = x. [para(3(a,1),49(a,1,2,2))]. given #61 (A,wt=25): 48 x ^ (((y ^ (x v z)) v (z ^ (y v x))) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(27(a,1),5(a,1,1)),flip(a)]. given #62 (F,wt=25): 250 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (z v x))))) = (y ^ x) v (x ^ z) # label(false). [para(2(a,1),90(a,1,2,2,2,2,2))]. given #63 (F,wt=25): 256 x ^ ((y ^ (z v x)) v (z ^ (x v ((z v x) ^ y)))) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),107(a,1,2,1))]. given #64 (T,wt=11): 182 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),57(a,1,2,2))]. given #65 (T,wt=11): 201 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),63(a,1,2))]. given #66 (A,wt=13): 51 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(16(a,1),5(a,1)),flip(a)]. given #67 (F,wt=25): 257 x ^ (((y v x) ^ z) v (y ^ (x v (z ^ (y v x))))) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),107(a,1,2,2,2,2))]. given #68 (F,wt=25): 296 x ^ ((y ^ (z v x)) v (z ^ (x v ((x v z) ^ y)))) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),216(a,1,2,1))]. given #69 (T,wt=11): 212 (x ^ y) v (z v x) = z v x. [para(37(a,1),20(a,2)),rewrite(117(4))]. given #70 (T,wt=11): 234 (x v y) ^ (z ^ y) = z ^ y. [para(33(a,1),50(a,2)),rewrite(89(4))]. given #71 (A,wt=13): 53 (x v y) ^ (x v (z v y)) = x v y. [para(13(a,1),16(a,1,2))]. given #72 (F,wt=25): 297 x ^ (((y v x) ^ z) v (y ^ (x v (z ^ (x v y))))) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),216(a,1,2,2,2,2))]. given #73 (F,wt=25): 353 x ^ ((y ^ (x v z)) v (z ^ (x v ((z v x) ^ y)))) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),217(a,1,2,1))]. given #74 (T,wt=11): 251 (x ^ y) v (y ^ x) = y ^ x. [para(16(a,1),90(a,1,2,1)),rewrite(16(2),16(2),25(1)),flip(a)]. given #75 (T,wt=11): 266 (x ^ y) v (z v y) = z v y. [para(37(a,1),55(a,2)),rewrite(117(4))]. given #76 (A,wt=13): 56 x v (y v (z ^ (x v y))) = x v y. [para(22(a,1),3(a,1)),flip(a)]. given #77 (F,wt=25): 354 x ^ (((x v y) ^ z) v (y ^ (x v (z ^ (y v x))))) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),217(a,1,2,2,2,2))]. given #78 (F,wt=13): 68 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(15(a,1),22(a,1,2))]. given #79 (T,wt=13): 85 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(31(a,1),5(a,2,2)),rewrite(15(3),5(2))]. given #80 (T,wt=13): 89 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),33(a,1,2)),rewrite(5(5))]. given #81 (A,wt=17): 58 x ^ ((y ^ x) v (z ^ x)) = (x ^ y) v (z ^ x). [para(22(a,1),9(a,1,2,1,2)),rewrite(5(4),6(3),33(7))]. given #82 (F,wt=13): 91 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),17(a,1,1))]. given #83 (F,wt=13): 92 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),17(a,1,2)),rewrite(3(3))]. given #84 (T,wt=13): 113 x v (y v (x v z)) = y v (x v z). [para(35(a,1),3(a,2,2)),rewrite(13(3),3(2))]. given #85 (T,wt=13): 117 x v (y v (z v x)) = y v (z v x). [para(3(a,1),37(a,1,2)),rewrite(3(5))]. given #86 (A,wt=25): 64 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ z) v (x ^ u)). [para(9(a,1),15(a,1,2)),flip(a)]. given #87 (F,wt=13): 123 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(13(a,1),18(a,1,2,1))]. given #88 (F,wt=13): 143 x ^ (y ^ (z v (x v u))) = y ^ x. [para(38(a,1),15(a,1,2)),flip(a)]. given #89 (T,wt=13): 151 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(49(a,1),5(a,1,1)),flip(a)]. given #90 (T,wt=13): 158 x ^ (y ^ (z v (u v x))) = y ^ x. [para(49(a,1),15(a,1,2)),flip(a)]. given #91 (A,wt=25): 65 x ^ (y ^ ((z ^ (u v x)) v (u ^ (x v z)))) = y ^ ((x ^ z) v (x ^ u)). [para(26(a,1),15(a,1,2)),flip(a)]. given #92 (F,wt=13): 165 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),19(a,1,2,2,1))]. given #93 (F,wt=13): 180 x v ((y ^ (z ^ x)) v u) = x v u. [para(57(a,1),3(a,1,1)),flip(a)]. given #94 (T,wt=13): 186 x v (y v (z ^ (u ^ x))) = y v x. [para(57(a,1),13(a,1,2)),flip(a)]. given #95 (T,wt=13): 198 x v ((y ^ (x ^ z)) v u) = x v u. [para(63(a,1),3(a,1,1)),flip(a)]. given #96 (A,wt=25): 66 x ^ (y ^ ((z ^ (x v u)) v (u ^ (z v x)))) = y ^ ((x ^ z) v (x ^ u)). [para(27(a,1),15(a,1,2)),flip(a)]. given #97 (F,wt=13): 202 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(9(a,1),63(a,1,2,2))]. given #98 (F,wt=13): 203 x v (y v (z ^ (x ^ u))) = y v x. [para(63(a,1),13(a,1,2)),flip(a)]. given #99 (T,wt=13): 242 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),21(a,1,2,2,1))]. given #100 (T,wt=13): 254 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(90(a,1),63(a,1,2,2))]. given #101 (A,wt=25): 70 x ^ (((y ^ (x v z)) v ((x v y) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(28(a,1),5(a,1,1)),flip(a)]. given #102 (F,wt=13): 260 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(22(a,1),107(a,1,2,1,1)),rewrite(22(5),73(6),35(6),5(5),86(4),5(6),4(8),33(8),2(8),23(8))]. given #103 (F,wt=13): 283 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),23(a,1,1))]. given #104 (T,wt=13): 284 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),23(a,1,2)),rewrite(5(3))]. given #105 (T,wt=13): 294 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(22(a,1),108(a,1,2,1,2)),rewrite(22(5),58(6),37(6),5(5),130(4),4(8),33(8),2(8),22(8))]. given #106 (A,wt=17): 73 x ^ ((y ^ x) v (x ^ z)) = (x ^ z) v (x ^ y). [para(7(a,1),28(a,1,2,1,2)),rewrite(15(4),18(4),31(6))]. given #107 (F,wt=13): 303 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(9(a,1),62(a,1,2)),rewrite(5(6),122(5),62(7))]. given #108 (F,wt=13): 314 x ^ (y ^ (z v (y ^ x))) = y ^ x. [back_rewrite(134),rewrite(304(5),85(5))]. given #109 (T,wt=13): 334 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(29(a,1),7(a,1,2))]. given #110 (T,wt=13): 358 (x ^ y) v (z ^ (y ^ x)) = y ^ x. [para(57(a,1),218(a,2)),rewrite(63(3),63(6),7(5),4(4),85(4),255(5))]. given #111 (A,wt=25): 77 x ^ (y ^ ((z ^ (x v u)) v ((x v z) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(28(a,1),15(a,1,2)),flip(a)]. given #112 (F,wt=13): 367 x v (y v (z ^ (y v x))) = x v y. [para(119(a,1),57(a,1,2,2)),rewrite(3(4))]. given #113 (F,wt=13): 373 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(13(a,1),126(a,1,1))]. given #114 (T,wt=13): 406 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),137(a,1,2,2))]. given #115 (T,wt=13): 418 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),150(a,1,2,2,2))]. given #116 (A,wt=25): 80 x ^ (((y ^ (z v x)) v (z ^ (y v x))) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(40(a,1),5(a,1,1)),flip(a)]. given #117 (F,wt=13): 445 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),182(a,1,2,2,2))]. given #118 (F,wt=13): 456 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(182(a,1),20(a,1,2)),rewrite(7(2)),flip(a)]. given #119 (T,wt=13): 505 (x ^ (y ^ z)) v (u v y) = u v y. [para(15(a,1),212(a,1,1))]. given #120 (T,wt=13): 520 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),234(a,1,1))]. given #121 (A,wt=25): 83 x ^ (y ^ ((z ^ (u v x)) v (u ^ (z v x)))) = y ^ ((x ^ z) v (x ^ u)). [para(40(a,1),15(a,1,2)),flip(a)]. given #122 (F,wt=13): 536 (x v y) ^ (z v (y v x)) = x v y. [para(119(a,1),234(a,1,2)),rewrite(4(4),119(7))]. given #123 (F,wt=13): 567 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),266(a,1,1))]. given #124 (T,wt=13): 634 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(58(a,1),19(a,1,2))]. given #125 (T,wt=13): 636 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(58(a,1),63(a,1,2,2))]. given #126 (A,wt=17): 86 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(9(a,1),31(a,1,2)),rewrite(9(10))]. given #127 (F,wt=13): 645 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(58(a,1),51(a,1,2))]. given #128 (F,wt=13): 972 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),254(a,1,2,2,2))]. given #129 (T,wt=13): 973 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),254(a,1,2))]. given #130 (T,wt=13): 1102 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(4(a,1),294(a,1,2,2))]. given #131 (A,wt=19): 93 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),17(a,1,1)),rewrite(3(5),3(8))]. given #132 (F,wt=13): 1177 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(4(a,1),303(a,1,2,1))]. given #133 (F,wt=13): 1235 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(4(a,1),334(a,1,2,1,2))]. given #134 (T,wt=13): 1560 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(4(a,1),634(a,1,2,1))]. given #135 (T,wt=13): 1648 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),972(a,1,2))]. given #136 (A,wt=17): 94 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(17(a,1),5(a,1,1)),flip(a)]. given #137 (F,wt=15): 96 (x v y) ^ (x v (z v (y v u))) = x v y. [para(13(a,1),17(a,1,2,2))]. given #138 (F,wt=15): 124 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(18(a,1),22(a,1,2)),rewrite(2(4))]. given #139 (T,wt=15): 125 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(18(a,1),15(a,1,2)),flip(a)]. given #140 (T,wt=15): 136 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),38(a,1,2,2))]. given #141 (A,wt=19): 95 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(13(a,1),17(a,1,1)),rewrite(3(4))]. given #142 (F,wt=15): 138 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(38(a,1),5(a,1)),flip(a)]. given #143 (F,wt=15): 152 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(49(a,1),5(a,1)),flip(a)]. given #144 (T,wt=15): 155 (x v y) ^ (z v (x v (u v y))) = x v y. [para(13(a,1),49(a,1,2,2))]. given #145 (T,wt=15): 170 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(19(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #146 (A,wt=17): 99 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(17(a,1),15(a,1,2)),flip(a)]. given #147 (F,wt=13): 2114 x ^ (((x v y) ^ (x v z)) v u) = x. [para(170(a,1),18(a,1)),rewrite(6(2)),flip(a)]. given #148 (F,wt=13): 2116 x ^ (((x v y) ^ (z v x)) v u) = x. [para(170(a,1),50(a,1)),rewrite(16(2)),flip(a)]. given #149 (T,wt=13): 2166 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),2114(a,1,2,1,1))]. given #150 (T,wt=13): 2167 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),2114(a,1,2))]. given #151 (A,wt=25): 101 x ^ (((y ^ (x v z)) v ((y v x) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(41(a,1),5(a,1,1)),flip(a)]. given #152 (F,wt=13): 2201 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),2116(a,1,2,1,1))]. given #153 (F,wt=13): 2202 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),2116(a,1,2))]. given #154 (T,wt=13): 2246 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),2166(a,1,2))]. given #155 (T,wt=13): 2321 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),2201(a,1,2))]. given #156 (A,wt=25): 106 x ^ (y ^ ((z ^ (x v u)) v ((z v x) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(41(a,1),15(a,1,2)),flip(a)]. given #157 (F,wt=15): 181 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(57(a,1),3(a,1)),flip(a)]. given #158 (F,wt=15): 188 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(15(a,1),57(a,1,2,2))]. given #159 (T,wt=15): 199 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(63(a,1),3(a,1)),flip(a)]. given #160 (T,wt=15): 200 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),63(a,1,2,2))]. given #161 (A,wt=25): 110 x ^ (((y ^ (z v x)) v ((x v y) ^ z)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(42(a,1),5(a,1,1)),flip(a)]. given #162 (F,wt=15): 210 x v (y v ((x ^ z) v u)) = y v (x v u). [para(20(a,1),13(a,1,2)),flip(a)]. given #163 (F,wt=15): 211 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(20(a,1),16(a,1,2)),rewrite(4(4))]. given #164 (T,wt=15): 225 x v (y v (z v (x ^ u))) = y v (z v x). [para(3(a,1),39(a,1,2)),rewrite(3(6))]. given #165 (T,wt=15): 227 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(39(a,1),16(a,1,2)),rewrite(4(4))]. given #166 (A,wt=25): 112 x ^ (y ^ ((z ^ (u v x)) v ((x v z) ^ u))) = y ^ ((x ^ z) v (x ^ u)). [para(42(a,1),15(a,1,2)),flip(a)]. given #167 (F,wt=15): 232 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(50(a,1),22(a,1,2)),rewrite(2(4))]. given #168 (F,wt=15): 233 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(50(a,1),15(a,1,2)),flip(a)]. given #169 (T,wt=15): 235 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(19(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #170 (T,wt=15): 247 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(21(a,1),20(a,1,2)),rewrite(20(3)),flip(a)]. given #171 (A,wt=19): 114 (x v y) ^ (x v (z ^ (x v y))) = x v ((x v y) ^ z). [para(35(a,1),26(a,1,2,1,2)),rewrite(3(5),6(6),2(4),4(9),6(9),2(8))]. given #172 (F,wt=15): 263 x v (y v ((z ^ x) v u)) = y v (x v u). [para(55(a,1),13(a,1,2)),flip(a)]. given #173 (F,wt=15): 264 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(55(a,1),16(a,1,2)),rewrite(4(4))]. given #174 (T,wt=15): 273 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(21(a,1),55(a,1,2)),rewrite(55(3)),flip(a)]. given #175 (T,wt=15): 274 x v (y v (z v (u ^ x))) = y v (z v x). [para(3(a,1),60(a,1,2)),rewrite(3(6))]. given #176 (A,wt=19): 115 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(35(a,1),41(a,1,2,2,1)),rewrite(3(3),6(4),4(9),6(9),2(8))]. given #177 (F,wt=15): 275 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(60(a,1),16(a,1,2)),rewrite(4(4))]. given #178 (F,wt=15): 289 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(15(a,1),23(a,1,2,2))]. given #179 (T,wt=15): 302 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(5(a,1),62(a,1,2)),rewrite(5(6))]. given #180 (T,wt=15): 304 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(62(a,1),22(a,1,2)),rewrite(2(4))]. given #181 (A,wt=19): 118 (x v y) ^ (y v (z ^ (x v y))) = y v ((x v y) ^ z). [para(37(a,1),26(a,1,2,1,2)),rewrite(3(5),38(6),2(4),4(9),16(9),2(8))]. given #182 (F,wt=15): 315 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(5(a,1),67(a,1,2)),rewrite(5(6))]. given #183 (F,wt=15): 317 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(67(a,1),22(a,1,2)),rewrite(2(4))]. given #184 (T,wt=13): 3252 x v ((y v x) ^ (y v z)) = x v y. [para(91(a,1),317(a,1,2)),rewrite(2(5),3(5),1948(4),91(8))]. given #185 (T,wt=13): 3294 x v ((x v y) ^ (y v z)) = x v y. [para(2(a,1),3252(a,1,2,1))]. given #186 (A,wt=19): 120 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(37(a,1),41(a,1,2,2,1)),rewrite(3(3),38(4),4(9),16(9),2(8))]. given #187 (F,wt=13): 3295 x v ((y v x) ^ (z v y)) = x v y. [para(2(a,1),3252(a,1,2,2))]. given #188 (F,wt=13): 3299 x v ((y v z) ^ (y v x)) = x v y. [para(4(a,1),3252(a,1,2))]. given #189 (T,wt=13): 3348 x v ((x v y) ^ (z v y)) = x v y. [para(2(a,1),3294(a,1,2,2))]. given #190 (T,wt=13): 3352 x v ((y v z) ^ (x v y)) = x v y. [para(4(a,1),3294(a,1,2))]. given #191 (A,wt=17): 121 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(18(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #192 (F,wt=13): 3385 x v ((y v z) ^ (z v x)) = x v z. [para(4(a,1),3295(a,1,2))]. given #193 (F,wt=13): 3502 x v ((y v z) ^ (x v z)) = x v z. [para(4(a,1),3348(a,1,2))]. given #194 (T,wt=15): 345 x v (y ^ (((x ^ z) v (x ^ u)) ^ v)) = x. [para(29(a,1),63(a,1,2,2))]. given #195 (T,wt=15): 361 (x v y) ^ ((y v x) ^ z) = (x v y) ^ z. [para(119(a,1),5(a,1,1)),flip(a)]. given #196 (A,wt=19): 122 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(9(a,1),18(a,2)),rewrite(64(8))]. given #197 (F,wt=15): 362 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(119(a,1),5(a,2,2)),rewrite(4(4))]. given #198 (F,wt=15): 369 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(126(a,1),5(a,1,1)),rewrite(5(2),5(5)),flip(a)]. given #199 (T,wt=15): 370 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(5(a,1),126(a,1,2)),rewrite(5(6))]. given #200 (T,wt=15): 384 (x ^ y) v ((y v z) ^ x) = (y v z) ^ x. [para(126(a,1),23(a,1,2)),rewrite(2(4))]. given #201 (A,wt=25): 127 x ^ ((((x v y) ^ z) v ((x v z) ^ y)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(69(a,1),5(a,1,1)),flip(a)]. given #202 (F,wt=15): 385 x ^ (y ^ ((x ^ (y v z)) v u)) = x ^ y. [para(62(a,1),126(a,1,2)),rewrite(4(5),5(5),62(8))]. given #203 (F,wt=15): 386 x ^ (y ^ ((x ^ (z v y)) v u)) = x ^ y. [para(67(a,1),126(a,1,2)),rewrite(4(5),5(5),67(8))]. given #204 (T,wt=15): 402 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(38(a,1),249(a,1,2,2,2,2)),rewrite(3(2),6(3),313(5)),flip(a)]. given #205 (T,wt=15): 403 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [para(49(a,1),249(a,1,2,2,2,2)),rewrite(3(2),38(3),332(5)),flip(a)]. given #206 (A,wt=17): 130 x ^ ((x ^ y) v (z ^ x)) = (z ^ x) v (x ^ y). [para(22(a,1),69(a,1,2,1,1)),rewrite(126(4),33(6))]. given #207 (F,wt=15): 407 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(137(a,1),5(a,1,1)),flip(a)]. given #208 (F,wt=15): 411 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(137(a,1),15(a,1,2)),flip(a)]. given #209 (T,wt=15): 419 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(150(a,1),5(a,1,1)),flip(a)]. given #210 (T,wt=15): 425 x ^ (y ^ (z v (u v (v v x)))) = y ^ x. [para(150(a,1),15(a,1,2)),flip(a)]. given #211 (A,wt=25): 131 x ^ (y ^ (((x v z) ^ u) v ((x v u) ^ z))) = y ^ ((x ^ z) v (x ^ u)). [para(69(a,1),15(a,1,2)),flip(a)]. given #212 (F,wt=15): 443 x v ((y ^ (z ^ (u ^ x))) v v) = x v v. [para(182(a,1),3(a,1,1)),flip(a)]. given #213 (F,wt=15): 447 x v (y v (z ^ (u ^ (v ^ x)))) = y v x. [para(182(a,1),13(a,1,2)),flip(a)]. given #214 (T,wt=15): 466 x v (y v (z ^ (u ^ (y v x)))) = x v y. [para(119(a,1),182(a,1,2,2,2)),rewrite(3(5))]. given #215 (T,wt=15): 469 x v ((y ^ (z ^ (x ^ u))) v v) = x v v. [para(201(a,1),3(a,1,1)),flip(a)]. given #216 (A,wt=25): 133 x ^ (((y ^ (z v x)) v ((y v x) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(79(a,1),5(a,1,1)),flip(a)]. given #217 (F,wt=15): 473 (x ^ y) v (z ^ (y ^ (x ^ u))) = y ^ x. [para(201(a,1),9(a,2)),rewrite(5(2),63(4),5(3),4(6),369(6),255(6))]. given #218 (F,wt=15): 474 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(9(a,1),201(a,1,2,2,2))]. given #219 (T,wt=15): 475 x v (y v (z ^ (u ^ (x ^ v)))) = y v x. [para(201(a,1),13(a,1,2)),flip(a)]. given #220 (T,wt=15): 479 x v (y ^ (z ^ ((u ^ x) v (x ^ v)))) = x. [para(90(a,1),201(a,1,2,2,2))]. given #221 (A,wt=25): 135 x ^ (y ^ ((z ^ (u v x)) v ((z v x) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(79(a,1),15(a,1,2)),flip(a)]. given #222 (F,wt=15): 484 (x ^ y) v (z ^ (u ^ (y ^ x))) = y ^ x. [back_rewrite(465),rewrite(478(6))]. given #223 (F,wt=15): 489 x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y. [para(51(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #224 (T,wt=15): 491 x ^ (y ^ (z v ((u v x) ^ y))) = x ^ y. [para(51(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #225 (T,wt=15): 499 (x ^ y) v (z v (x v u)) = z v (x v u). [para(212(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)]. given #226 (A,wt=19): 166 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(19(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #227 (F,wt=15): 500 (x ^ y) v (z v (u v x)) = z v (u v x). [para(3(a,1),212(a,1,2)),rewrite(3(6))]. given #228 (F,wt=15): 507 (x v y) ^ ((y ^ z) v x) = (y ^ z) v x. [para(212(a,1),17(a,1,2)),rewrite(4(4))]. given #229 (T,wt=15): 513 x v (y v ((x v (y ^ z)) ^ u)) = x v y. [para(39(a,1),212(a,1,2)),rewrite(2(5),3(5),39(8))]. given #230 (T,wt=15): 516 x v (y v ((x v (z ^ y)) ^ u)) = x v y. [para(60(a,1),212(a,1,2)),rewrite(2(5),3(5),60(8))]. given #231 (A,wt=19): 167 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(19(a,1),22(a,1,2)),rewrite(2(5))]. given #232 (F,wt=15): 518 (x v y) ^ (z ^ (y ^ u)) = z ^ (y ^ u). [para(212(a,1),126(a,1,1))]. given #233 (F,wt=15): 519 (x ^ y) v (z v (y v u)) = z v (y v u). [para(126(a,1),212(a,1,1))]. given #234 (T,wt=15): 521 (x v y) ^ (z ^ (u ^ y)) = z ^ (u ^ y). [para(5(a,1),234(a,1,2)),rewrite(5(6))]. given #235 (T,wt=15): 531 (x ^ y) v ((z v y) ^ x) = (z v y) ^ x. [para(234(a,1),23(a,1,2)),rewrite(2(4))]. given #236 (A,wt=17): 168 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(19(a,1),15(a,1,2)),flip(a)]. given #237 (F,wt=15): 532 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [para(62(a,1),234(a,1,2)),rewrite(4(5),5(5),62(8))]. given #238 (F,wt=15): 533 x ^ (y ^ (z v (x ^ (u v y)))) = x ^ y. [para(67(a,1),234(a,1,2)),rewrite(4(5),5(5),67(8))]. given #239 (T,wt=15): 542 (x ^ y) v (z v (u v y)) = z v (u v y). [para(234(a,1),212(a,1,1))]. given #240 (T,wt=15): 544 (x v y) ^ (x v (z v (u v y))) = x v y. [para(3(a,1),53(a,1,2,2))]. given #241 (A,wt=19): 169 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(15(a,1),19(a,1,2,2,1)),rewrite(5(5))]. given #242 (F,wt=15): 560 (x ^ y) v ((y ^ x) v z) = (y ^ x) v z. [para(251(a,1),3(a,1,1)),flip(a)]. given #243 (F,wt=15): 561 (x ^ y) v (z v (y ^ x)) = z v (x ^ y). [para(251(a,1),3(a,2,2)),rewrite(2(4))]. given #244 (T,wt=15): 566 x ^ (y ^ (z v (u v (y ^ x)))) = x ^ y. [para(251(a,1),137(a,1,2,2,2)),rewrite(5(5))]. given #245 (T,wt=15): 571 (x v y) ^ ((z ^ y) v x) = (z ^ y) v x. [para(266(a,1),17(a,1,2)),rewrite(4(4))]. given #246 (A,wt=25): 171 x ^ ((((x v y) ^ z) v ((z v x) ^ y)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(100(a,1),5(a,1,1)),flip(a)]. given #247 (F,wt=15): 574 x v (y v (z ^ ((x ^ u) v y))) = x v y. [para(20(a,1),266(a,1,2)),rewrite(2(5),3(5),20(8))]. given #248 (F,wt=15): 575 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(39(a,1),266(a,1,2)),rewrite(2(5),3(5),39(8))]. given #249 (T,wt=15): 578 x v (y v (z ^ ((u ^ x) v y))) = x v y. [para(55(a,1),266(a,1,2)),rewrite(2(5),3(5),55(8))]. given #250 (T,wt=15): 579 x v (y v (z ^ (x v (u ^ y)))) = x v y. [para(60(a,1),266(a,1,2)),rewrite(2(5),3(5),60(8))]. given #251 (A,wt=25): 175 x ^ (y ^ (((x v z) ^ u) v ((u v x) ^ z))) = y ^ ((x ^ z) v (x ^ u)). [para(100(a,1),15(a,1,2)),flip(a)]. given #252 (F,wt=15): 596 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(5(a,1),68(a,1,2,2))]. given #253 (F,wt=15): 627 (x v (y v (z v u))) ^ (v ^ z) = v ^ z. [para(137(a,1),89(a,1,2,2)),rewrite(137(9))]. given #254 (T,wt=15): 628 (x v (y v (z v u))) ^ (v ^ u) = v ^ u. [para(150(a,1),89(a,1,2,2)),rewrite(150(9))]. given #255 (T,wt=15): 643 x v (y ^ (z ^ ((x ^ u) v (v ^ x)))) = x. [para(58(a,1),201(a,1,2,2,2))]. given #256 (A,wt=25): 178 x ^ ((((y v x) ^ z) v ((x v z) ^ y)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(109(a,1),5(a,1,1)),flip(a)]. given #257 (F,wt=15): 654 (x v y) ^ (y v (z v (x v u))) = y v x. [para(13(a,1),91(a,1,2,2))]. given #258 (F,wt=15): 660 (x v y) ^ (y v (z v (u v x))) = x v y. [para(3(a,1),92(a,1,2,2))]. given #259 (T,wt=15): 678 (x v y) ^ (z v (y v (u v x))) = x v y. [para(92(a,1),234(a,1,2)),rewrite(4(5),92(9))]. given #260 (T,wt=15): 684 (x ^ (y ^ (z ^ u))) v (v v u) = v v u. [para(182(a,1),117(a,1,2,2)),rewrite(182(9))]. given #261 (A,wt=25): 179 x ^ (y ^ (((z v x) ^ u) v ((x v u) ^ z))) = y ^ ((x ^ u) v (x ^ z)). [para(109(a,1),15(a,1,2)),flip(a)]. given #262 (F,wt=15): 685 (x ^ (y ^ (z ^ u))) v (v v z) = v v z. [para(201(a,1),117(a,1,2,2)),rewrite(201(9))]. given #263 (F,wt=15): 712 x ^ (y v (z v (u v (v v (x v w))))) = x. [para(150(a,1),123(a,1,2)),rewrite(38(3)),flip(a)]. given #264 (T,wt=15): 722 (x v y) ^ (z v (y v (x v u))) = x v y. [para(91(a,1),123(a,2)),rewrite(3(3),655(8),4(5))]. given #265 (T,wt=15): 753 x ^ (y v (z v (u v (v v (w v x))))) = x. [para(150(a,1),151(a,1,2)),rewrite(49(3)),flip(a)]. given #266 (A,wt=21): 183 x ^ ((y ^ x) v (z ^ (u ^ x))) = (x ^ y) v (z ^ (u ^ x)). [para(57(a,1),9(a,1,2,1,2)),rewrite(5(5),5(4),6(3),89(9))]. given #267 (F,wt=15): 793 x ^ (y ^ (z v ((y ^ x) v u))) = x ^ y. [para(13(a,1),165(a,1,2,2))]. given #268 (F,wt=15): 797 x ^ (y ^ ((y ^ (x v z)) v u)) = x ^ y. [para(165(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #269 (T,wt=15): 799 x ^ (y ^ ((y ^ (z v x)) v u)) = x ^ y. [para(165(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #270 (T,wt=15): 828 x v (y ^ (z ^ (u ^ (v ^ (w ^ x))))) = x. [para(182(a,1),180(a,1,2)),rewrite(57(3)),flip(a)]. given #271 (A,wt=21): 184 x ^ ((y ^ (z ^ x)) v (u ^ x)) = (y ^ (z ^ x)) v (x ^ u). [para(57(a,1),9(a,1,2,2,2)),rewrite(5(4),5(3),6(2),89(8))]. given #272 (F,wt=15): 829 x v (y ^ (z ^ (u ^ (v ^ (x ^ w))))) = x. [para(201(a,1),180(a,1,2)),rewrite(57(3),5(3),5(2)),flip(a)]. given #273 (F,wt=15): 904 x v (y ^ ((z ^ (x ^ u)) v (x ^ v))) = x. [para(15(a,1),202(a,1,2,2,1))]. given #274 (T,wt=15): 905 x v (y ^ ((x ^ z) v (u ^ (x ^ v)))) = x. [para(15(a,1),202(a,1,2,2,2))]. given #275 (T,wt=15): 917 x v (y ^ ((z ^ (u ^ x)) v (x ^ v))) = x. [para(89(a,1),202(a,1,2,2,1))]. given #276 (A,wt=21): 190 x ^ ((y ^ (z ^ x)) v (x ^ u)) = (x ^ u) v (y ^ (z ^ x)). [para(57(a,1),28(a,1,2,2,1)),rewrite(5(4),5(3),6(2),89(9))]. given #277 (F,wt=15): 918 x v (y ^ ((x ^ z) v (u ^ (v ^ x)))) = x. [para(89(a,1),202(a,1,2,2,2))]. given #278 (F,wt=15): 949 x v (y v (z ^ ((y v x) ^ u))) = x v y. [para(15(a,1),242(a,1,2,2))]. given #279 (T,wt=15): 951 x v (y v ((y v (x ^ z)) ^ u)) = x v y. [para(242(a,1),20(a,1,2)),rewrite(20(3)),flip(a)]. given #280 (T,wt=15): 953 x v (y v ((y v (z ^ x)) ^ u)) = x v y. [para(242(a,1),55(a,1,2)),rewrite(55(3)),flip(a)]. given #281 (A,wt=17): 191 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(17(a,1),57(a,1,2,2)),rewrite(3(5),3(4))]. given #282 (F,wt=15): 979 x v (y ^ ((z ^ x) v (u ^ (x ^ v)))) = x. [para(15(a,1),254(a,1,2,2,2))]. given #283 (F,wt=15): 996 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(254(a,1),212(a,1,2)),rewrite(5(5),2(6),254(11))]. given #284 (T,wt=15): 1000 x v (y ^ ((z ^ x) v (u ^ (v ^ x)))) = x. [para(89(a,1),254(a,1,2,2,2))]. given #285 (T,wt=15): 1022 x ^ ((y ^ (z ^ u)) v (z ^ x)) = x ^ z. [para(15(a,1),260(a,1,2,1))]. given #286 (A,wt=17): 193 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(18(a,1),57(a,1,2,2))]. given #287 (F,wt=15): 1024 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(260(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #288 (F,wt=15): 1027 x ^ ((y ^ z) v (y ^ (u v x))) = x ^ y. [para(260(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #289 (T,wt=15): 1037 x ^ ((y ^ (z ^ u)) v (u ^ x)) = x ^ u. [para(89(a,1),260(a,1,2,1))]. given #290 (T,wt=15): 1054 (x ^ y) v (y ^ (z ^ (x ^ u))) = y ^ x. [para(15(a,1),283(a,1,2,2))]. given #291 (A,wt=21): 195 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(19(a,1),57(a,1,2,2))]. given #292 (F,wt=15): 1060 (x ^ y) v (y ^ (z ^ (u ^ x))) = y ^ x. [para(89(a,1),283(a,1,2,2))]. given #293 (F,wt=15): 1087 (x ^ y) v (z ^ (y ^ (u ^ x))) = x ^ y. [para(284(a,1),266(a,1,2)),rewrite(2(5),284(9))]. given #294 (T,wt=15): 1106 x ^ (y v ((y v z) ^ x)) = x ^ (y v z). [para(6(a,1),294(a,1,2,1))]. given #295 (T,wt=15): 1107 x ^ (y v ((z v y) ^ x)) = x ^ (z v y). [para(16(a,1),294(a,1,2,1))]. given #296 (A,wt=17): 208 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(20(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #297 (F,wt=19): 7424 x ^ ((x ^ y) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),1106(a,2)),rewrite(4(8),9(8),13(6),2(5),4102(6))]. given #298 (F,wt=19): 7425 x ^ ((x ^ y) v (z ^ (y v x))) = (x ^ z) v (x ^ y) # label(false). [para(26(a,1),1106(a,2)),rewrite(4(8),26(8),13(6),2(5),4159(6))]. given #299 (T,wt=15): 1112 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(294(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #300 (T,wt=15): 1119 x ^ ((y ^ z) v (z ^ (u v x))) = x ^ z. [para(294(a,1),50(a,1,2)),rewrite(50(3)),flip(a)]. given #301 (A,wt=17): 209 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),20(a,1,2,1))]. given #302 (F,wt=19): 7427 x ^ ((x ^ y) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(69(a,1),1106(a,2)),rewrite(4(8),69(8),13(6),2(5),124(5))]. given #303 (F,wt=19): 7428 x ^ ((x ^ y) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(109(a,1),1106(a,2)),rewrite(4(8),109(8),13(6),2(5),576(6))]. given #304 (T,wt=15): 1184 x ^ ((y ^ x) v (z ^ (y ^ u))) = x ^ y. [para(15(a,1),303(a,1,2,2))]. given #305 (T,wt=15): 1185 x ^ ((y ^ (x v z)) v (y ^ u)) = x ^ y. [para(303(a,1),18(a,1,2)),rewrite(18(3)),flip(a)]. given #306 (A,wt=17): 213 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(20(a,1),49(a,1,2,2))]. given #307 (F,wt=19): 7591 x ^ ((y ^ x) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),7428(a,1,2,1))]. ============================== PROOF ================================= % Proof 1 at 13.08 (+ 0.06) seconds: H2. % Length of proof is 44. % Level of proof is 11. % Maximum clause weight is 25. % Given clauses 307. 1 x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2). [goal]. 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [assumption]. 9 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [copy(8),flip(a)]. 10 c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2) # answer(H2). [deny(1)]. 11 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H2). [copy(10),rewrite(2(12))]. 13 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. 15 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. 16 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. 18 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 22 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 24 x ^ x = x. [para(7(a,1),6(a,1,2))]. 25 x v x = x. [para(6(a,1),7(a,1,2))]. 26 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (x ^ y) v (x ^ z) # label(false). [para(2(a,1),9(a,1,2,1,2))]. 28 x ^ ((y ^ (x v z)) v ((x v y) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),9(a,1,2,1)),rewrite(2(5))]. 33 x ^ (y ^ x) = y ^ x. [para(24(a,1),5(a,2,2)),rewrite(4(2))]. 37 x v (y v x) = y v x. [para(25(a,1),3(a,2,2)),rewrite(2(2))]. 39 x v (y v (x ^ z)) = y v x. [para(7(a,1),13(a,1,2)),flip(a)]. 41 x ^ ((y ^ (x v z)) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),26(a,1,2,1)),rewrite(2(5))]. 42 x ^ ((y ^ (z v x)) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),26(a,1,2,2))]. 50 x ^ ((y v x) ^ z) = x ^ z. [para(16(a,1),5(a,1,1)),flip(a)]. 55 x v ((y ^ x) v z) = x v z. [para(22(a,1),3(a,1,1)),flip(a)]. 58 x ^ ((y ^ x) v (z ^ x)) = (x ^ y) v (z ^ x). [para(22(a,1),9(a,1,2,1,2)),rewrite(5(4),6(3),33(7))]. 67 x ^ (y ^ (z v x)) = y ^ x. [para(16(a,1),15(a,1,2)),flip(a)]. 69 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ y) v (x ^ z) # label(false). [para(4(a,1),28(a,1,2,1))]. 89 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),33(a,1,2)),rewrite(5(5))]. 108 x ^ ((y ^ (z v x)) v (z ^ (x v (y ^ (z v x))))) = (y ^ x) v (x ^ z) # label(false). [para(33(a,1),41(a,1,2,2)),rewrite(2(7),67(11))]. 109 x ^ (((y v x) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),42(a,1,2,1))]. 117 x v (y v (z v x)) = y v (z v x). [para(3(a,1),37(a,1,2)),rewrite(3(5))]. 126 (x v y) ^ (z ^ x) = z ^ x. [para(33(a,1),18(a,2)),rewrite(89(4))]. 130 x ^ ((x ^ y) v (z ^ x)) = (z ^ x) v (x ^ y). [para(22(a,1),69(a,1,2,1,1)),rewrite(126(4),33(6))]. 266 (x ^ y) v (z v y) = z v y. [para(37(a,1),55(a,2)),rewrite(117(4))]. 294 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(22(a,1),108(a,1,2,1,2)),rewrite(22(5),58(6),37(6),5(5),130(4),4(8),33(8),2(8),22(8))]. 576 (x ^ y) v (z v ((u v x) ^ y)) = z v ((u v x) ^ y). [para(50(a,1),266(a,1,1))]. 1106 x ^ (y v ((y v z) ^ x)) = x ^ (y v z). [para(6(a,1),294(a,1,2,1))]. 7428 x ^ ((x ^ y) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(109(a,1),1106(a,2)),rewrite(4(8),109(8),13(6),2(5),576(6))]. 7591 x ^ ((y ^ x) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),7428(a,1,2,1))]. 7709 x ^ ((y ^ x) v (z ^ (y v x))) = (x ^ z) v (x ^ y) # label(false). [para(4(a,1),7591(a,1,2,2))]. 7711 $F # answer(H2). [back_rewrite(11),rewrite(7709(13),4(5),4(8),39(10),2(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=307. Generated=198458. Kept=7707. proofs=1. Usable=306. Sos=6787. Demods=7095. Limbo=2, Disabled=620. Hints=0. Weight_deleted=55640. Literals_deleted=0. Forward_subsumed=133263. Back_subsumed=186. Sos_limit_deleted=1847. Sos_displaced=0. Sos_removed=0. New_demodulators=7706 (6 lex), Back_demodulated=424. Back_unit_deleted=0. Demod_attempts=4004679. Demod_rewrites=688298. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.15. User_CPU=13.08, System_CPU=0.06, Wall_clock=13. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 9935 exit (max_proofs) Sat Aug 12 20:54:13 2006