============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13993 was started by mccune on cleo.thornwood, Mon Jun 19 17:19:25 2006 The command was "/home/mccune/bin/prover9 -f LT.in LT-interp.outx". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file LT.in assign(age_part,1). assign(false_part,4). assign(true_part,1). assign(max_weight,25). assign(max_minutes,10). % assign(max_minutes, 10) -> assign(max_seconds, 600). clauses(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. clauses(sos). (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). end_of_list. clauses(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 terms(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 GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c7 ^ (c8 v (c9 ^ ((c7 ^ (c8 v c9)) v (c8 ^ c9)))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). end_of_list. ============================== end of process goals ================== ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x v y = y v x. [input]. 2 (x v y) v z = x v (y v z). [input]. 3 x ^ y = y ^ x. [input]. 4 (x ^ y) ^ z = x ^ (y ^ z). [input]. 5 x ^ (x v y) = x. [input]. 6 x v (x ^ y) = x. [input]. 7 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [input]. 8 c7 ^ (c8 v (c9 ^ ((c7 ^ (c8 v c9)) v (c8 ^ c9)))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [clausify]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). Auto_denials: no changes. Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c7, c8, c9, ^, v ]). After inverse_order: Function symbol precedence: lex([ c7, c8, c9, ^, v ]). 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; redundancy checks enabled. % Operation v is associative-commutative; redundancy checks enabled. % Operation ^ is commutative; redundancy checks enabled. % Operation ^ is associative-commutative; redundancy checks enabled. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [copy(8),demod(9(12))]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 9 x v y = y v x. [input]. 10 (x v y) v z = x v (y v z). [input]. 11 x ^ y = y ^ x. [input]. 12 (x ^ y) ^ z = x ^ (y ^ z). [input]. 13 x ^ (x v y) = x. [input]. 14 x v (x ^ y) = x. [input]. 15 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82) # label(false). [input]. 16 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [copy(8),demod(9(12))]. end_of_list. clauses(demodulators). 9 x v y = y v x. [input]. % (lex-dep) 10 (x v y) v z = x v (y v z). [input]. 11 x ^ y = y ^ x. [input]. % (lex-dep) 12 (x ^ y) ^ z = x ^ (y ^ z). [input]. 13 x ^ (x v y) = x. [input]. 14 x v (x ^ y) = x. [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 9 x v y = y v x. [input]. given #2 (I,wt=11): 10 (x v y) v z = x v (y v z). [input]. given #3 (I,wt=7): 11 x ^ y = y ^ x. [input]. given #4 (I,wt=11): 12 (x ^ y) ^ z = x ^ (y ^ z). [input]. given #5 (I,wt=7): 13 x ^ (x v y) = x. [input]. given #6 (I,wt=7): 14 x v (x ^ y) = x. [input]. given #7 (I,wt=21): 15 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82) # label(false). [input]. given #8 (I,wt=23): 16 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [copy(8),demod(9(12))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(9(a,1),16(a,1,2,2,2,2,2)),demod(9(10))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(9(a,1),16(a,1,2,2,2)),demod(9(12))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(9(a,1),16(a,1,2)),demod(9(14))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(9(a,1),16(a,2,2)),demod(9(21))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,1,2,2,2,1)),demod(11(6))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,1,2,2,2,2)),demod(11(11))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,1,2,2)),demod(11(13))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,1)),demod(11(15))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,2,2,2)),demod(11(20))]. not interpretable: c7 % Clause contains symbol not in interpretation: % 0 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)). [para(11(a,1),16(a,2)),demod(11(22))]. given #9 (F,wt=21): 29 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [para(15(a,1),9(a,1))]. given #10 (F,wt=21): 32 x ^ (((x v y) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),15(a,2,2,1)),flip(a)]. given #11 (F,wt=21): 37 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),29(a,1,2,1,2))]. given #12 (T,wt=5): 27 x ^ x = x. [para(14(a,1),13(a,1,2))]. given #13 (A,wt=11): 17 x v (y v z) = y v (x v z). [para(9(a,1),10(a,1,1)),demod(10(2))]. given #14 (F,wt=21): 38 x ^ ((y ^ (x v z)) v (z ^ (y v x))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),29(a,1,2,2,2))]. given #15 (F,wt=21): 39 x ^ ((y ^ (x v z)) v ((x v y) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),29(a,1,2,2))]. given #16 (F,wt=21): 41 x ^ (((y v x) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),32(a,1,2,1,1))]. given #17 (F,wt=21): 42 x ^ (((x v y) ^ z) v (y ^ (z v x))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),32(a,1,2,2,2))]. given #18 (T,wt=5): 28 x v x = x. [para(13(a,1),14(a,1,2))]. given #19 (A,wt=11): 18 x ^ (y ^ z) = y ^ (x ^ z). [para(11(a,1),12(a,1,1)),demod(12(2))]. given #20 (F,wt=21): 43 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),32(a,1,2,2))]. given #21 (F,wt=21): 48 x ^ ((y ^ (z v x)) v (z ^ (y v x))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),37(a,1,2,2,2))]. given #22 (F,wt=21): 49 x ^ ((y ^ (z v x)) v ((x v y) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),37(a,1,2,2))]. given #23 (F,wt=21): 62 x ^ ((y ^ (x v z)) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),38(a,1,2,2))]. given #24 (T,wt=7): 19 x ^ (y v x) = x. [para(9(a,1),13(a,1,2))]. given #25 (A,wt=13): 20 (x v y) ^ (x v (y v z)) = x v y. [para(10(a,1),13(a,1,2))]. given #26 (F,wt=21): 69 x ^ (((y v x) ^ z) v (y ^ (z v x))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),41(a,1,2,2,2))]. given #27 (F,wt=21): 70 x ^ (((y v x) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),41(a,1,2,2))]. given #28 (F,wt=21): 74 x ^ (((x v y) ^ z) v ((z v x) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),42(a,1,2,2))]. given #29 (F,wt=21): 96 x ^ ((y ^ (z v x)) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),48(a,1,2,2))]. given #30 (T,wt=7): 25 x v (y ^ x) = x. [para(11(a,1),14(a,1,2))]. given #31 (A,wt=11): 21 x ^ ((x v y) ^ z) = x ^ z. [para(13(a,1),12(a,1,1)),flip(a)]. given #32 (F,wt=21): 134 x ^ (((y v x) ^ z) v ((z v x) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),69(a,1,2,2))]. given #33 (F,wt=9): 52 x ^ (x ^ y) = x ^ y. [para(27(a,1),12(a,1,1)),flip(a)]. given #34 (F,wt=25): 178 x ^ (((x v y) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(52(a,1),32(a,1,2,1)),demod(21(11))]. given #35 (F,wt=25): 179 x ^ (((y v x) ^ z) v (y ^ (x v ((y v x) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(52(a,1),41(a,1,2,1)),demod(111(11))]. given #36 (T,wt=9): 54 x ^ (y ^ x) = y ^ x. [para(27(a,1),12(a,2,2)),demod(11(2))]. given #37 (A,wt=13): 22 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(13(a,1),12(a,1)),flip(a)]. given #38 (F,wt=25): 180 x ^ (((y v x) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),178(a,1,2,1,1))]. given #39 (F,wt=25): 181 x ^ (((x v y) ^ z) v (y ^ (x v ((y v x) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),178(a,1,2,2,2,2,1))]. given #40 (F,wt=25): 182 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v ((x v z) ^ y)))) # label(false). [para(11(a,1),178(a,1,2,1)),flip(a)]. given #41 (F,wt=25): 183 x ^ (((x v y) ^ z) v (y ^ (x v (z ^ (x v y))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),178(a,1,2,2,2,2))]. given #42 (T,wt=9): 60 x ^ (y v (x v z)) = x. [para(17(a,1),13(a,1,2))]. given #43 (A,wt=11): 23 x v ((x ^ y) v z) = x v z. [para(14(a,1),10(a,1,1)),flip(a)]. given #44 (F,wt=25): 186 (x ^ y) v (x ^ z) = x ^ ((y ^ (z v x)) v (z ^ (x v ((z v x) ^ y)))) # label(false). [para(11(a,1),179(a,1,2,1)),flip(a)]. given #45 (F,wt=25): 187 x ^ (((y v x) ^ z) v (y ^ (x v (z ^ (y v x))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),179(a,1,2,2,2,2))]. given #46 (F,wt=25): 191 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z) # label(false). [para(54(a,1),32(a,1,2,1)),demod(80(11))]. given #47 (F,wt=25): 192 x ^ ((y ^ (z v x)) v (z ^ (x v (y ^ (z v x))))) = (y ^ x) v (x ^ z) # label(false). [para(54(a,1),41(a,1,2,1)),demod(122(11))]. given #48 (T,wt=9): 77 x v (x v y) = x v y. [para(28(a,1),10(a,1,1)),flip(a)]. given #49 (A,wt=13): 24 x v (y v ((x v y) ^ z)) = x v y. [para(14(a,1),10(a,1)),flip(a)]. given #50 (F,wt=25): 203 x ^ ((y ^ (x v ((x v y) ^ z))) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),180(a,1,2))]. given #51 (F,wt=25): 204 (x ^ y) v (x ^ z) = x ^ ((y ^ (z v x)) v (z ^ (x v ((x v z) ^ y)))) # label(false). [para(11(a,1),180(a,1,2,1)),flip(a)]. given #52 (F,wt=25): 205 x ^ (((y v x) ^ z) v (y ^ (x v (z ^ (x v y))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),180(a,1,2,2,2,2))]. given #53 (F,wt=25): 208 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v ((z v x) ^ y)))) # label(false). [para(11(a,1),181(a,1,2,1)),flip(a)]. given #54 (T,wt=9): 79 x v (y v x) = y v x. [para(28(a,1),10(a,2,2)),demod(9(2))]. given #55 (A,wt=13): 26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(12(a,1),14(a,1,2))]. given #56 (F,wt=25): 209 x ^ (((x v y) ^ z) v (y ^ (x v (z ^ (y v x))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),181(a,1,2,2,2,2))]. given #57 (F,wt=25): 212 x ^ ((y ^ (x v z)) v (z ^ (x v ((x v z) ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(182(a,1),9(a,1))]. given #58 (F,wt=25): 237 x ^ ((y ^ (z v x)) v (z ^ (x v ((z v x) ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(186(a,1),9(a,1))]. given #59 (F,wt=25): 241 x ^ ((y ^ (z v x)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z) # label(false). [para(9(a,1),191(a,1,2,1,2))]. given #60 (T,wt=9): 81 x v (y ^ (x ^ z)) = x. [para(18(a,1),14(a,1,2))]. given #61 (A,wt=25): 40 x ^ (((y ^ (x v z)) v (z ^ (x v y))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(29(a,1),12(a,1,1)),flip(a)]. given #62 (F,wt=25): 242 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (z v x))))) = (y ^ x) v (x ^ z) # label(false). [para(9(a,1),191(a,1,2,2,2,2,2))]. given #63 (F,wt=25): 265 x ^ ((y ^ (x v (z ^ (x v y)))) v ((y v x) ^ z)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),203(a,1,2,1,2,2))]. given #64 (F,wt=25): 266 x ^ ((y ^ (x v ((x v y) ^ z))) v (z ^ (y v x))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),203(a,1,2,2))]. given #65 (F,wt=25): 267 x ^ ((y ^ (z v x)) v (z ^ (x v ((x v z) ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(204(a,1),9(a,1))]. given #66 (T,wt=9): 110 x ^ (y v (z v x)) = x. [para(10(a,1),19(a,1,2))]. given #67 (A,wt=25): 44 x ^ ((((x v y) ^ z) v (y ^ (x v z))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(32(a,1),12(a,1,1)),flip(a)]. given #68 (F,wt=25): 272 x ^ ((y ^ (x v z)) v (z ^ (x v ((z v x) ^ y)))) = (x ^ z) v (x ^ y) # label(false). [para(208(a,1),9(a,1))]. given #69 (F,wt=25): 293 x ^ ((y ^ (x v (z ^ (x v y)))) v (z ^ (y v x))) = (z ^ x) v (x ^ y) # label(false). [para(9(a,1),241(a,1,2))]. given #70 (F,wt=9): 150 x v (y ^ (z ^ x)) = x. [para(12(a,1),25(a,1,2))]. given #71 (F,wt=11): 61 x v (y v (x ^ z)) = y v x. [para(14(a,1),17(a,1,2)),flip(a)]. given #72 (T,wt=11): 80 x ^ (y ^ (x v z)) = y ^ x. [para(13(a,1),18(a,1,2)),flip(a)]. given #73 (A,wt=25): 50 x ^ (((y ^ (z v x)) v (z ^ (x v y))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(37(a,1),12(a,1,1)),flip(a)]. given #74 (F,wt=11): 111 x ^ ((y v x) ^ z) = x ^ z. [para(19(a,1),12(a,1,1)),flip(a)]. given #75 (F,wt=11): 122 x ^ (y ^ (z v x)) = y ^ x. [para(19(a,1),18(a,1,2)),flip(a)]. given #76 (F,wt=11): 148 x v ((y ^ x) v z) = x v z. [para(25(a,1),10(a,1,1)),flip(a)]. given #77 (F,wt=11): 157 x v (y v (z ^ x)) = y v x. [para(25(a,1),17(a,1,2)),flip(a)]. given #78 (T,wt=11): 168 (x ^ y) v (y ^ x) = x ^ y. [back_demod(153),demod(154(4))]. given #79 (A,wt=25): 63 x ^ (((y ^ (x v z)) v (z ^ (y v x))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(38(a,1),12(a,1,1)),flip(a)]. given #80 (F,wt=11): 193 (x v y) ^ (z ^ x) = z ^ x. [para(54(a,1),21(a,2)),demod(190(4))]. given #81 (F,wt=11): 220 x ^ (y v (z v (x v u))) = x. [para(10(a,1),60(a,1,2))]. given #82 (F,wt=11): 240 (x v y) ^ (y v x) = y v x. [para(183(a,1),187(a,1,2,2)),demod(27(3),27(4),77(3),11(3),19(3),13(3),14(3),27(6),11(5),19(5),27(6),11(5),13(5))]. given #83 (F,wt=11): 278 (x ^ y) v (z v x) = z v x. [para(79(a,1),23(a,2)),demod(277(4))]. given #84 (T,wt=11): 296 x v (y ^ (z ^ (x ^ u))) = x. [para(12(a,1),81(a,1,2))]. given #85 (A,wt=25): 67 x ^ (((y ^ (x v z)) v ((x v y) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(39(a,1),12(a,1,1)),flip(a)]. given #86 (F,wt=11): 336 x ^ (y v (z v (u v x))) = x. [para(10(a,1),110(a,1,2,2))]. given #87 (F,wt=11): 373 x v (y ^ (z ^ (u ^ x))) = x. [para(12(a,1),150(a,1,2,2))]. given #88 (F,wt=11): 432 (x v y) ^ (z ^ y) = z ^ y. [para(54(a,1),111(a,2)),demod(190(4))]. given #89 (F,wt=11): 459 (x ^ y) v (z v y) = z v y. [para(79(a,1),148(a,2)),demod(277(4))]. given #90 (T,wt=13): 112 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(19(a,1),12(a,1)),flip(a)]. given #91 (A,wt=25): 71 x ^ ((((y v x) ^ z) v (y ^ (x v z))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(41(a,1),12(a,1,1)),flip(a)]. given #92 (F,wt=13): 118 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),19(a,1,2))]. given #93 (F,wt=13): 126 (x v y) ^ (y v (x v z)) = y v x. [para(9(a,1),20(a,1,1))]. given #94 (F,wt=13): 127 (x v y) ^ (y v (z v x)) = x v y. [para(9(a,1),20(a,1,2)),demod(10(3))]. given #95 (F,wt=13): 149 x v (y v (z ^ (x v y))) = x v y. [para(25(a,1),10(a,1)),flip(a)]. given #96 (T,wt=13): 161 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(18(a,1),25(a,1,2))]. given #97 (A,wt=25): 75 x ^ ((((x v y) ^ z) v (y ^ (z v x))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(42(a,1),12(a,1,1)),flip(a)]. given #98 (F,wt=13): 171 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),21(a,1,2,1))]. given #99 (F,wt=13): 177 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(52(a,1),12(a,2,2)),demod(18(3),12(2))]. given #100 (F,wt=13): 190 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(12(a,1),54(a,1,2)),demod(12(5))]. given #101 (F,wt=13): 195 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(11(a,1),22(a,1,2,2,1))]. given #102 (T,wt=13): 224 x ^ (y ^ (z v (x v u))) = y ^ x. [para(60(a,1),18(a,1,2)),flip(a)]. given #103 (A,wt=25): 82 x ^ (y ^ ((z ^ (x v u)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(29(a,1),18(a,1,2)),flip(a)]. given #104 (F,wt=13): 225 x v (y v (x v z)) = y v (x v z). [para(60(a,1),25(a,1,2)),demod(9(3))]. given #105 (F,wt=13): 235 x v ((y ^ (x ^ z)) v u) = x v u. [para(18(a,1),23(a,1,2,1))]. given #106 (F,wt=13): 250 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [back_demod(188),demod(244(5),79(5))]. given #107 (F,wt=13): 257 x v (y v ((y v x) ^ z)) = x v y. [para(9(a,1),24(a,1,2,2,1))]. given #108 (T,wt=13): 277 x v (y v (z v x)) = y v (z v x). [para(10(a,1),79(a,1,2)),demod(10(5))]. given #109 (A,wt=25): 83 x ^ (y ^ (((x v z) ^ u) v (z ^ (x v u)))) = y ^ ((x ^ u) v (x ^ z)). [para(32(a,1),18(a,1,2)),flip(a)]. given #110 (F,wt=13): 280 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(11(a,1),26(a,1,1))]. given #111 (F,wt=13): 281 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(11(a,1),26(a,1,2)),demod(12(3))]. given #112 (F,wt=13): 299 (x ^ (y ^ z)) v (z ^ x) = x ^ z. [para(81(a,1),29(a,2)),demod(12(2),12(4),12(3),122(3),12(4),14(5),154(5))]. given #113 (F,wt=13): 300 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(29(a,1),81(a,1,2,2))]. given #114 (T,wt=13): 304 x v (y v (z ^ (x ^ u))) = y v x. [para(81(a,1),17(a,1,2)),flip(a)]. given #115 (A,wt=25): 84 x ^ (y ^ ((z ^ (u v x)) v (u ^ (x v z)))) = y ^ ((x ^ u) v (x ^ z)). [para(37(a,1),18(a,1,2)),flip(a)]. given #116 (F,wt=13): 314 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(191(a,1),81(a,1,2,2))]. given #117 (F,wt=13): 318 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(40(a,1),14(a,1,2))]. given #118 (F,wt=13): 335 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(81(a,1),266(a,2)),demod(12(2),12(4),14(5),14(4),11(3),52(3),12(4),9(5),14(5),154(5))]. given #119 (F,wt=13): 337 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(110(a,1),12(a,1,1)),flip(a)]. given #120 (T,wt=13): 346 x ^ (y ^ (z v (u v x))) = y ^ x. [para(110(a,1),18(a,1,2)),flip(a)]. given #121 (A,wt=25): 85 x ^ (y ^ ((z ^ (x v u)) v (u ^ (z v x)))) = y ^ ((x ^ u) v (x ^ z)). [para(38(a,1),18(a,1,2)),flip(a)]. given #122 (F,wt=13): 371 x v ((y ^ (z ^ x)) v u) = x v u. [para(150(a,1),10(a,1,1)),flip(a)]. given #123 (F,wt=13): 379 x v (y v (z ^ (u ^ x))) = y v x. [para(150(a,1),17(a,1,2)),flip(a)]. given #124 (F,wt=13): 406 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(29(a,1),80(a,1,2)),demod(12(6),170(5),80(7))]. given #125 (F,wt=13): 417 x ^ (y ^ (z v (y ^ x))) = y ^ x. [back_demod(231),demod(410(6))]. given #126 (T,wt=13): 440 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(29(a,1),122(a,1,2)),demod(12(6),170(5),80(7))]. given #127 (A,wt=25): 86 x ^ (y ^ ((z ^ (x v u)) v ((x v z) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(39(a,1),18(a,1,2)),flip(a)]. given #128 (F,wt=13): 483 (x ^ y) v (z ^ (y ^ x)) = y ^ x. [para(168(a,1),29(a,1,2,2,2)),demod(12(5),195(5),12(6),377(5),313(5),12(6),18(9),11(8),52(8),54(8),9(8),26(8))]. given #129 (F,wt=13): 486 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [back_demod(252),demod(480(5))]. given #130 (F,wt=13): 497 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),193(a,1,1))]. given #131 (F,wt=13): 523 x ^ (y v (z v (u v (x v v)))) = x. [para(10(a,1),220(a,1,2,2))]. given #132 (T,wt=13): 554 (x v (y v z)) ^ (y v x) = y v x. [para(240(a,1),21(a,2)),demod(10(3),548(6))]. given #133 (A,wt=25): 87 x ^ (y ^ (((z v x) ^ u) v (z ^ (x v u)))) = y ^ ((x ^ u) v (x ^ z)). [para(41(a,1),18(a,1,2)),flip(a)]. given #134 (F,wt=13): 556 x v (y v (z ^ (y v x))) = y v x. [para(240(a,1),191(a,2,2)),demod(17(4),9(3),77(3),79(3),17(8),9(7),77(7),79(7),25(8),240(6),9(5),25(5),27(3),17(5),9(4)),flip(a)]. given #135 (F,wt=13): 568 (x ^ (y ^ z)) v (u v y) = u v y. [para(18(a,1),278(a,1,1))]. given #136 (F,wt=13): 578 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(278(a,1),191(a,1,2,1,2)),demod(278(8),500(11),12(3),122(3),12(6),122(6)),flip(a)]. given #137 (F,wt=13): 591 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(12(a,1),296(a,1,2,2))]. given #138 (T,wt=13): 620 x ^ (y v (z v (u v (v v x)))) = x. [para(10(a,1),336(a,1,2,2,2))]. given #139 (A,wt=25): 88 x ^ (y ^ (((x v z) ^ u) v (z ^ (u v x)))) = y ^ ((x ^ u) v (x ^ z)). [para(42(a,1),18(a,1,2)),flip(a)]. given #140 (F,wt=13): 643 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(12(a,1),373(a,1,2,2,2))]. given #141 (F,wt=13): 663 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(10(a,1),432(a,1,1))]. given #142 (F,wt=13): 697 (x ^ (y ^ z)) v (u v z) = u v z. [para(12(a,1),459(a,1,1))]. given #143 (F,wt=13): 736 (x v y) ^ (z v (y v x)) = x v y. [para(9(a,1),118(a,1,2)),demod(10(3))]. given #144 (T,wt=13): 768 (x v (y v z)) ^ (z v x) = z v x. [para(127(a,1),11(a,1)),flip(a)]. given #145 (A,wt=25): 90 x ^ ((((x v y) ^ z) v ((x v z) ^ y)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(43(a,1),12(a,1,1)),flip(a)]. given #146 (F,wt=13): 951 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(9(a,1),250(a,1,2))]. given #147 (F,wt=13): 1102 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(11(a,1),300(a,1,2,2,2))]. given #148 (F,wt=13): 1155 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(11(a,1),314(a,1,2,2,2))]. given #149 (F,wt=13): 1156 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(11(a,1),314(a,1,2))]. given #150 (T,wt=13): 1187 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(11(a,1),318(a,1,2,1,2))]. given #151 (A,wt=17): 93 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(14(a,1),43(a,1,2,1,1)),demod(18(4),21(4),52(7))]. given #152 (F,wt=13): 1351 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(11(a,1),406(a,1,2,1))]. given #153 (F,wt=13): 1407 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(11(a,1),440(a,1,2,2))]. given #154 (F,wt=13): 1462 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(9(a,1),486(a,1,2))]. given #155 (F,wt=13): 1818 (x v (y v z)) ^ (z v y) = z v y. [para(736(a,1),11(a,1)),flip(a)]. given #156 (T,wt=13): 1938 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(11(a,1),1155(a,1,2))]. given #157 (A,wt=25): 94 x ^ (y ^ (((x v z) ^ u) v ((x v u) ^ z))) = y ^ ((x ^ u) v (x ^ z)). [para(43(a,1),18(a,1,2)),flip(a)]. given #158 (F,wt=15): 132 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),20(a,1,2,2))]. given #159 (F,wt=15): 172 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(21(a,1),18(a,1,2)),flip(a)]. given #160 (F,wt=15): 173 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(21(a,1),25(a,1,2)),demod(9(4))]. given #161 (F,wt=15): 197 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(17(a,1),22(a,1,2,2))]. given #162 (T,wt=15): 201 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(22(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #163 (A,wt=25): 97 x ^ (((y ^ (z v x)) v (z ^ (y v x))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(48(a,1),12(a,1,1)),flip(a)]. given #164 (F,wt=13): 2301 x ^ (((x v y) ^ (x v z)) v u) = x. [para(201(a,1),21(a,1)),demod(13(2)),flip(a)]. given #165 (F,wt=13): 2303 x ^ (((x v y) ^ (z v x)) v u) = x. [para(201(a,1),111(a,1)),demod(19(2)),flip(a)]. given #166 (F,wt=13): 2336 x ^ (((y v x) ^ (x v z)) v u) = x. [para(9(a,1),2301(a,1,2,1,1))]. given #167 (F,wt=13): 2337 x ^ (y v ((x v z) ^ (x v u))) = x. [para(9(a,1),2301(a,1,2))]. given #168 (T,wt=13): 2374 x ^ (((y v x) ^ (z v x)) v u) = x. [para(9(a,1),2303(a,1,2,1,1))]. given #169 (A,wt=25): 101 x ^ (y ^ ((z ^ (u v x)) v (u ^ (z v x)))) = y ^ ((x ^ u) v (x ^ z)). [para(48(a,1),18(a,1,2)),flip(a)]. given #170 (F,wt=13): 2375 x ^ (y v ((x v z) ^ (u v x))) = x. [para(9(a,1),2303(a,1,2))]. given #171 (F,wt=13): 2418 x ^ (y v ((z v x) ^ (x v u))) = x. [para(9(a,1),2336(a,1,2))]. given #172 (F,wt=13): 2488 x ^ (y v ((z v x) ^ (u v x))) = x. [para(9(a,1),2374(a,1,2))]. given #173 (F,wt=15): 219 (x v y) ^ (z v (x v (y v u))) = x v y. [para(10(a,1),60(a,1,2,2))]. given #174 (T,wt=15): 234 x v (y v ((x ^ z) v u)) = y v (x v u). [para(23(a,1),17(a,1,2)),flip(a)]. given #175 (A,wt=25): 102 x ^ (((y ^ (z v x)) v ((x v y) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(49(a,1),12(a,1,1)),flip(a)]. given #176 (F,wt=15): 236 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(23(a,1),19(a,1,2)),demod(11(4))]. given #177 (F,wt=15): 261 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(18(a,1),24(a,1,2,2))]. given #178 (F,wt=15): 263 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(24(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #179 (F,wt=15): 288 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(18(a,1),26(a,1,2,2))]. given #180 (T,wt=15): 295 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(12(a,1),81(a,1,2,2))]. given #181 (A,wt=25): 105 x ^ (y ^ ((z ^ (u v x)) v ((x v z) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(49(a,1),18(a,1,2)),flip(a)]. given #182 (F,wt=15): 331 x v (y ^ (((x ^ z) v (x ^ u)) ^ v)) = x. [para(40(a,1),81(a,1,2,2))]. given #183 (F,wt=15): 338 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(110(a,1),12(a,1)),flip(a)]. given #184 (F,wt=15): 344 (x v y) ^ (z v (x v (u v y))) = x v y. [para(17(a,1),110(a,1,2,2))]. given #185 (F,wt=15): 372 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(150(a,1),10(a,1)),flip(a)]. given #186 (T,wt=15): 382 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(18(a,1),150(a,1,2,2))]. given #187 (A,wt=25): 106 x ^ (((y ^ (x v z)) v ((y v x) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(62(a,1),12(a,1,1)),flip(a)]. given #188 (F,wt=15): 400 x v (y v (z v (x ^ u))) = y v (z v x). [para(10(a,1),61(a,1,2)),demod(10(6))]. given #189 (F,wt=15): 401 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(61(a,1),19(a,1,2)),demod(11(4))]. given #190 (F,wt=15): 405 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(12(a,1),80(a,1,2)),demod(12(6))]. given #191 (F,wt=15): 416 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [back_demod(248),demod(410(9))]. given #192 (T,wt=15): 418 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [back_demod(221),demod(410(9))]. given #193 (A,wt=25): 109 x ^ (y ^ ((z ^ (x v u)) v ((z v x) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(62(a,1),18(a,1,2)),flip(a)]. given #194 (F,wt=15): 430 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(111(a,1),18(a,1,2)),flip(a)]. given #195 (F,wt=15): 431 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(111(a,1),25(a,1,2)),demod(9(4))]. given #196 (F,wt=15): 433 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(22(a,1),111(a,1,2)),demod(111(3)),flip(a)]. given #197 (F,wt=15): 439 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(12(a,1),122(a,1,2)),demod(12(6))]. given #198 (T,wt=15): 450 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [back_demod(353),demod(442(9))]. given #199 (A,wt=19): 128 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(10(a,1),20(a,1,1)),demod(10(5),10(8))]. given #200 (F,wt=13): 3328 x v ((y v z) ^ (y v x)) = x v y. [para(126(a,1),450(a,1,2)),demod(17(5),9(4),2256(4),126(8))]. given #201 (F,wt=13): 3398 x v ((y v z) ^ (z v x)) = x v z. [para(9(a,1),3328(a,1,2,1))]. given #202 (F,wt=13): 3399 x v ((y v z) ^ (x v y)) = x v y. [para(9(a,1),3328(a,1,2,2))]. given #203 (F,wt=13): 3403 x v ((y v x) ^ (y v z)) = x v y. [para(11(a,1),3328(a,1,2))]. given #204 (T,wt=13): 3467 x v ((y v z) ^ (x v z)) = x v z. [para(9(a,1),3398(a,1,2,2))]. given #205 (A,wt=17): 129 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(20(a,1),12(a,1,1)),flip(a)]. given #206 (F,wt=13): 3471 x v ((y v x) ^ (z v y)) = x v y. [para(11(a,1),3398(a,1,2))]. given #207 (F,wt=13): 3558 x v ((x v y) ^ (y v z)) = x v y. [para(11(a,1),3399(a,1,2))]. given #208 (F,wt=13): 3645 x v ((x v y) ^ (z v y)) = x v y. [para(11(a,1),3467(a,1,2))]. given #209 (F,wt=15): 451 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [back_demod(339),demod(442(9))]. given #210 (T,wt=15): 453 x v (y v ((z ^ x) v u)) = y v (x v u). [para(148(a,1),17(a,1,2)),flip(a)]. given #211 (A,wt=19): 131 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(17(a,1),20(a,1,1)),demod(10(4))]. given #212 (F,wt=15): 455 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(148(a,1),19(a,1,2)),demod(11(4))]. given #213 (F,wt=15): 458 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(24(a,1),148(a,1,2)),demod(148(3)),flip(a)]. given #214 (F,wt=15): 467 x v (y v (z v (u ^ x))) = y v (z v x). [para(10(a,1),157(a,1,2)),demod(10(6))]. given #215 (F,wt=15): 469 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(157(a,1),19(a,1,2)),demod(11(4))]. given #216 (T,wt=15): 479 (x ^ y) v ((y ^ x) v z) = (x ^ y) v z. [para(168(a,1),10(a,1,1)),flip(a)]. given #217 (A,wt=17): 133 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(20(a,1),18(a,1,2)),flip(a)]. given #218 (F,wt=15): 480 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(168(a,1),10(a,2,2)),demod(9(4))]. given #219 (F,wt=15): 490 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(193(a,1),12(a,1,1)),demod(12(2),12(5)),flip(a)]. given #220 (F,wt=15): 491 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(12(a,1),193(a,1,2)),demod(12(6))]. given #221 (F,wt=15): 511 ((x v y) ^ z) v (z ^ x) = (x v y) ^ z. [para(193(a,1),26(a,1,2))]. given #222 (T,wt=15): 517 x ^ (y ^ ((x ^ (y v z)) v u)) = x ^ y. [para(80(a,1),193(a,1,2)),demod(11(5),12(5),80(8))]. given #223 (A,wt=25): 135 x ^ ((((y v x) ^ z) v (y ^ (z v x))) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(69(a,1),12(a,1,1)),flip(a)]. given #224 (F,wt=15): 520 x ^ (y ^ ((x ^ (z v y)) v u)) = x ^ y. [para(122(a,1),193(a,1,2)),demod(11(5),12(5),122(8))]. given #225 (F,wt=15): 524 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(220(a,1),12(a,1,1)),flip(a)]. given #226 (F,wt=15): 530 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(220(a,1),18(a,1,2)),flip(a)]. given #227 (F,wt=15): 541 (x v y) ^ ((y v x) ^ z) = (y v x) ^ z. [para(240(a,1),12(a,1,1)),flip(a)]. given #228 (T,wt=15): 548 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(240(a,1),18(a,1,2)),flip(a)]. given #229 (A,wt=25): 137 x ^ (y ^ (((z v x) ^ u) v (z ^ (u v x)))) = y ^ ((x ^ u) v (x ^ z)). [para(69(a,1),18(a,1,2)),flip(a)]. given #230 (F,wt=15): 558 (x ^ y) v (z v (x v u)) = z v (x v u). [para(278(a,1),10(a,1,1)),demod(10(2),10(5)),flip(a)]. given #231 (F,wt=15): 559 (x ^ y) v (z v (u v x)) = z v (u v x). [para(10(a,1),278(a,1,2)),demod(10(6))]. given #232 (F,wt=15): 574 ((x ^ y) v z) ^ (z v x) = (x ^ y) v z. [para(278(a,1),20(a,1,2))]. given #233 (F,wt=15): 583 x v (y v ((x v (y ^ z)) ^ u)) = x v y. [para(61(a,1),278(a,1,2)),demod(9(5),10(5),61(8))]. given #234 (T,wt=15): 584 x v (y v ((x v (z ^ y)) ^ u)) = x v y. [para(157(a,1),278(a,1,2)),demod(9(5),10(5),157(8))]. given #235 (A,wt=25): 138 x ^ ((((y v x) ^ z) v ((x v z) ^ y)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(70(a,1),12(a,1,1)),flip(a)]. given #236 (F,wt=15): 585 (x v y) ^ (z ^ (y ^ u)) = z ^ (y ^ u). [para(278(a,1),193(a,1,1))]. given #237 (F,wt=15): 586 (x ^ y) v (z v (y v u)) = z v (y v u). [para(193(a,1),278(a,1,1))]. given #238 (F,wt=15): 587 x ^ (y ^ (z v (u v (v v x)))) = x ^ y. [para(278(a,1),220(a,1,2,2,2)),demod(12(5))]. given #239 (F,wt=15): 588 x v ((y ^ (z ^ (x ^ u))) v v) = x v v. [para(296(a,1),10(a,1,1)),flip(a)]. given #240 (T,wt=15): 595 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(29(a,1),296(a,1,2,2,2))]. given #241 (A,wt=25): 140 x ^ (y ^ (((z v x) ^ u) v ((x v u) ^ z))) = y ^ ((x ^ u) v (x ^ z)). [para(70(a,1),18(a,1,2)),flip(a)]. given #242 (F,wt=15): 598 x v (y v (z ^ (u ^ (x ^ v)))) = y v x. [para(296(a,1),17(a,1,2)),flip(a)]. given #243 (F,wt=15): 603 x v (y ^ (z ^ ((u ^ x) v (x ^ v)))) = x. [para(191(a,1),296(a,1,2,2,2))]. given #244 (F,wt=15): 610 x v (y v (z ^ (u ^ (v ^ x)))) = x v y. [para(193(a,1),296(a,1,2,2,2)),demod(10(5))]. given #245 (F,wt=15): 611 x v (y v (z ^ (u ^ (y v x)))) = x v y. [para(240(a,1),296(a,1,2,2,2)),demod(10(5))]. given #246 (T,wt=15): 621 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(336(a,1),12(a,1,1)),flip(a)]. given #247 (A,wt=25): 142 x ^ ((((x v y) ^ z) v ((z v x) ^ y)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(74(a,1),12(a,1,1)),flip(a)]. given #248 (F,wt=15): 640 x ^ (y ^ (z v (u v (y ^ x)))) = x ^ y. [para(168(a,1),336(a,1,2,2,2)),demod(12(5))]. given #249 (F,wt=15): 641 x v ((y ^ (z ^ (u ^ x))) v v) = x v v. [para(373(a,1),10(a,1,1)),flip(a)]. given #250 (F,wt=15): 664 (x v y) ^ (z ^ (u ^ y)) = z ^ (u ^ y). [para(12(a,1),432(a,1,2)),demod(12(6))]. given #251 (F,wt=15): 673 x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y. [para(21(a,1),432(a,1,2)),demod(11(5),12(5),21(8))]. given #252 (T,wt=15): 679 ((x v y) ^ z) v (z ^ y) = (x v y) ^ z. [para(432(a,1),26(a,1,2))]. given #253 (A,wt=25): 144 x ^ (y ^ (((x v z) ^ u) v ((u v x) ^ z))) = y ^ ((x ^ u) v (x ^ z)). [para(74(a,1),18(a,1,2)),flip(a)]. given #254 (F,wt=15): 686 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [para(80(a,1),432(a,1,2)),demod(11(5),12(5),80(8))]. given #255 (F,wt=15): 688 x ^ (y ^ (z v ((u v x) ^ y))) = x ^ y. [para(111(a,1),432(a,1,2)),demod(11(5),12(5),111(8))]. given #256 (F,wt=15): 689 x ^ (y ^ (z v (x ^ (u v y)))) = x ^ y. [para(122(a,1),432(a,1,2)),demod(11(5),12(5),122(8))]. given #257 (F,wt=15): 694 (x ^ y) v (z v (u v y)) = z v (u v y). [para(432(a,1),278(a,1,1))]. given #258 (T,wt=15): 704 ((x ^ y) v z) ^ (z v y) = (x ^ y) v z. [para(459(a,1),20(a,1,2))]. given #259 (A,wt=25): 146 x ^ (((y ^ (z v x)) v ((y v x) ^ z)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(96(a,1),12(a,1,1)),flip(a)]. given #260 (F,wt=15): 708 x v (y v (z ^ ((x ^ u) v y))) = x v y. [para(23(a,1),459(a,1,2)),demod(9(5),10(5),23(8))]. given #261 (F,wt=15): 710 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(61(a,1),459(a,1,2)),demod(9(5),10(5),61(8))]. given #262 (F,wt=15): 714 x v (y v (z ^ ((u ^ x) v y))) = x v y. [para(148(a,1),459(a,1,2)),demod(9(5),10(5),148(8))]. given #263 (F,wt=15): 715 x v (y v (z ^ (x v (u ^ y)))) = x v y. [para(157(a,1),459(a,1,2)),demod(9(5),10(5),157(8))]. given #264 (T,wt=15): 738 (x v y) ^ (x v (z v (u v y))) = x v y. [para(10(a,1),118(a,1,2,2))]. given #265 (A,wt=25): 147 x ^ (y ^ ((z ^ (u v x)) v ((z v x) ^ u))) = y ^ ((x ^ u) v (x ^ z)). [para(96(a,1),18(a,1,2)),flip(a)]. given #266 (F,wt=15): 761 (x v y) ^ (y v (z v (x v u))) = y v x. [para(17(a,1),126(a,1,2,2))]. given #267 (F,wt=15): 766 (x v y) ^ (y v (z v (u v x))) = x v y. [para(10(a,1),127(a,1,2,2))]. given #268 (F,wt=15): 784 (x v (y v (z v u))) ^ (z v x) = z v x. [para(127(a,1),193(a,1,2)),demod(10(3),10(2),127(9))]. given #269 (F,wt=15): 788 (x v (y v (z v u))) ^ (u v y) = u v y. [para(127(a,1),432(a,1,2)),demod(127(9))]. given #270 (T,wt=15): 801 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(12(a,1),161(a,1,2,2))]. given #271 (A,wt=17): 154 x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x). [para(25(a,1),32(a,1,2,1,1)),demod(12(4),13(3),54(7))]. given #272 (F,wt=15): 837 (x v (y v (z v u))) ^ (z v y) = z v y. [para(240(a,1),171(a,2)),demod(10(3),548(7))]. given #273 (F,wt=15): 839 x ^ (y v (z v (u v (v v (x v w))))) = x. [para(336(a,1),171(a,1,2)),demod(60(3)),flip(a)]. given #274 (F,wt=15): 842 (x v (y v (z v u))) ^ (v ^ z) = v ^ z. [para(432(a,1),171(a,2)),demod(10(3),664(7))]. given #275 (F,wt=15): 851 (x v (y v (z v u))) ^ (v ^ u) = v ^ u. [para(336(a,1),190(a,1,2,2)),demod(336(9))]. given #276 (T,wt=15): 857 x ^ (y ^ (z v ((y ^ x) v u))) = x ^ y. [para(17(a,1),195(a,1,2,2))]. given #277 (A,wt=17): 169 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(21(a,1),12(a,1)),demod(12(2)),flip(a)]. given #278 (F,wt=15): 861 x ^ (y ^ ((y ^ (x v z)) v u)) = x ^ y. [para(195(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #279 (F,wt=15): 864 x ^ (y ^ ((y ^ (z v x)) v u)) = x ^ y. [para(195(a,1),111(a,1,2)),demod(111(3)),flip(a)]. given #280 (F,wt=15): 938 (x ^ (y ^ (z ^ u))) v (z ^ y) = y ^ z. [para(168(a,1),235(a,2)),demod(12(3),480(7))]. given #281 (F,wt=15): 942 x v (y ^ (z ^ (u ^ (v ^ (x ^ w))))) = x. [para(373(a,1),235(a,1,2)),demod(81(3)),flip(a)]. given #282 (T,wt=15): 945 (x ^ (y ^ (z ^ u))) v (v v z) = v v z. [para(459(a,1),235(a,2)),demod(12(3),694(7))]. given #283 (A,wt=19): 170 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(29(a,1),21(a,2)),demod(82(8))]. given #284 (F,wt=15): 958 x ^ ((x ^ y) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),250(a,1,2,2))]. given #285 (F,wt=15): 959 x ^ (((x v y) ^ z) v (z ^ u)) = x ^ z. [para(250(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #286 (F,wt=15): 963 x ^ (((y v x) ^ z) v (z ^ u)) = x ^ z. [para(250(a,1),111(a,1,2)),demod(111(3)),flip(a)]. given #287 (F,wt=15): 967 x ^ ((x ^ y) v (z ^ (u ^ y))) = x ^ y. [para(190(a,1),250(a,1,2,2))]. given #288 (T,wt=15): 975 x v (y v (z ^ ((y v x) ^ u))) = x v y. [para(18(a,1),257(a,1,2,2))]. given #289 (A,wt=25): 174 x ^ ((((y v x) ^ z) v ((z v x) ^ y)) ^ u) = ((x ^ z) v (x ^ y)) ^ u. [para(134(a,1),12(a,1,1)),flip(a)]. given #290 (F,wt=15): 977 x v (y v ((y v (x ^ z)) ^ u)) = x v y. [para(257(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #291 (F,wt=15): 982 x v (y v ((y v (z ^ x)) ^ u)) = x v y. [para(257(a,1),148(a,1,2)),demod(148(3)),flip(a)]. given #292 (F,wt=15): 994 (x ^ (y ^ (z ^ u))) v (v v u) = v v u. [para(373(a,1),277(a,1,2,2)),demod(373(9))]. given #293 (F,wt=15): 1015 (x ^ y) v (y ^ (z ^ (x ^ u))) = y ^ x. [para(18(a,1),280(a,1,2,2))]. given #294 (T,wt=15): 1027 (x ^ y) v (y ^ (z ^ (u ^ x))) = y ^ x. [para(190(a,1),280(a,1,2,2))]. given #295 (A,wt=25): 175 x ^ (y ^ (((z v x) ^ u) v ((u v x) ^ z))) = y ^ ((x ^ u) v (x ^ z)). [para(134(a,1),18(a,1,2)),flip(a)]. given #296 (F,wt=15): 1055 (x ^ (y ^ (z ^ u))) v (z ^ x) = z ^ x. [para(281(a,1),278(a,1,2)),demod(12(3),12(2),281(9))]. given #297 (F,wt=15): 1058 (x ^ (y ^ (z ^ u))) v (u ^ y) = u ^ y. [para(281(a,1),459(a,1,2)),demod(281(9))]. given #298 (F,wt=15): 1072 (x ^ (y ^ (z ^ u))) v (u ^ x) = x ^ u. [para(12(a,1),299(a,1,1,2))]. given #299 (F,wt=15): 1075 (x ^ y) v ((y v z) ^ x) = x ^ (y v z). [para(13(a,1),299(a,1,1,2))]. given #300 (T,wt=15): 1080 (x ^ y) v ((z v y) ^ x) = x ^ (z v y). [para(19(a,1),299(a,1,1,2))]. given #301 (A,wt=19): 196 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(22(a,1),12(a,1)),demod(12(2),12(4)),flip(a)]. given #302 (F,wt=15): 1105 x v (y ^ ((z ^ (x ^ u)) v (x ^ v))) = x. [para(18(a,1),300(a,1,2,2,1))]. given #303 (F,wt=15): 1106 x v (y ^ ((x ^ z) v (u ^ (x ^ v)))) = x. [para(18(a,1),300(a,1,2,2,2))]. given #304 (F,wt=15): 1121 x v (y ^ ((z ^ (u ^ x)) v (x ^ v))) = x. [para(190(a,1),300(a,1,2,2,1))]. given #305 (F,wt=15): 1122 x v (y ^ ((x ^ z) v (u ^ (v ^ x)))) = x. [para(190(a,1),300(a,1,2,2,2))]. given #306 (T,wt=15): 1162 x v (y ^ ((z ^ x) v (u ^ (x ^ v)))) = x. [para(18(a,1),314(a,1,2,2,2))]. given #307 (A,wt=17): 198 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(22(a,1),18(a,1,2)),flip(a)]. given #308 (F,wt=15): 1177 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(314(a,1),278(a,1,2)),demod(12(5),9(6),314(11))]. given #309 (F,wt=15): 1183 x v (y ^ ((z ^ x) v (u ^ (v ^ x)))) = x. [para(190(a,1),314(a,1,2,2,2))]. given #310 (F,wt=15): 1190 x v (((y ^ (x ^ z)) v (x ^ u)) ^ v) = x. [para(18(a,1),318(a,1,2,1,1))]. given #311 (F,wt=15): 1191 x v (((x ^ y) v (z ^ (x ^ u))) ^ v) = x. [para(18(a,1),318(a,1,2,1,2))]. given #312 (T,wt=15): 1206 x v (((y ^ (z ^ x)) v (x ^ u)) ^ v) = x. [para(190(a,1),318(a,1,2,1,1))]. given #313 (A,wt=19): 199 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(18(a,1),22(a,1,2,2,1)),demod(12(5))]. given #314 (F,wt=15): 1207 x v (((x ^ y) v (z ^ (u ^ x))) ^ v) = x. [para(190(a,1),318(a,1,2,1,2))]. given #315 (F,wt=15): 1238 x ^ (y v (z v (u v (v v (w v x))))) = x. [para(336(a,1),337(a,1,2)),demod(110(3)),flip(a)]. given #316 (F,wt=15): 1297 x v (y ^ (z ^ (u ^ (v ^ (w ^ x))))) = x. [para(373(a,1),371(a,1,2)),demod(150(3)),flip(a)]. given #317 (F,wt=15): 1357 x ^ ((y ^ (z ^ u)) v (z ^ x)) = x ^ z. [para(18(a,1),406(a,1,2,1))]. given #318 (T,wt=15): 1359 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(406(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #319 (A,wt=19): 200 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(22(a,1),25(a,1,2)),demod(9(5))]. given #320 (F,wt=15): 1364 x ^ ((y ^ z) v (y ^ (u v x))) = x ^ y. [para(406(a,1),111(a,1,2)),demod(111(3)),flip(a)]. given #321 (F,wt=15): 1374 x ^ ((y ^ (z ^ u)) v (u ^ x)) = x ^ u. [para(190(a,1),406(a,1,2,1))]. given #322 (F,wt=15): 1388 x ^ (y ^ (z v (y ^ (x v u)))) = y ^ x. [para(417(a,1),21(a,1,2)),demod(80(3)),flip(a)]. given #323 (F,wt=15): 1391 x ^ (y ^ (z v (y ^ (u v x)))) = y ^ x. [para(417(a,1),111(a,1,2)),demod(122(3)),flip(a)]. given #324 (T,wt=15): 1414 x ^ ((y ^ x) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),440(a,1,2,2))]. given #325 (A,wt=19): 223 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(60(a,1),42(a,1,2,2)),demod(9(3),77(3),9(4),11(9),13(9),9(8))]. given #326 (F,wt=15): 1415 x ^ ((y ^ (x v z)) v (y ^ u)) = x ^ y. [para(440(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #327 (F,wt=15): 1419 x ^ ((y ^ (z v x)) v (y ^ u)) = x ^ y. [para(440(a,1),111(a,1,2)),demod(111(3)),flip(a)]. given #328 (F,wt=15): 1426 x ^ ((y ^ x) v (z ^ (u ^ y))) = x ^ y. [para(190(a,1),440(a,1,2,2))]. given #329 (F,wt=15): 1446 (x ^ y) v (z ^ (u ^ (y ^ x))) = y ^ x. [para(12(a,1),483(a,1,2))]. given #330 (T,wt=15): 1455 (x ^ (y v z)) v (y ^ x) = (y v z) ^ x. [para(21(a,1),483(a,1,2))]. given #331 (A,wt=17): 232 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(23(a,1),10(a,1)),demod(10(2)),flip(a)]. given #332 (F,wt=15): 1458 (x ^ (y v z)) v (z ^ x) = (y v z) ^ x. [para(111(a,1),483(a,1,2))]. given #333 (F,wt=15): 1465 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(13(a,1),486(a,1,2,2)),demod(9(3))]. given #334 (F,wt=19): 8199 x ^ ((x ^ y) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(29(a,1),1465(a,1,2,2)),demod(17(6),1455(5),29(11))]. given #335 (F,wt=19): 8200 x ^ ((x ^ y) v ((y v x) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(37(a,1),1465(a,1,2,2)),demod(17(6),1458(5),37(11))]. given #336 (T,wt=15): 1469 x ^ (y v (x ^ (z v y))) = x ^ (z v y). [para(19(a,1),486(a,1,2,2)),demod(9(3))]. given #337 (A,wt=17): 233 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(12(a,1),23(a,1,2,1))]. given #338 (F,wt=19): 8230 (x ^ y) v (x ^ z) = x ^ ((y ^ x) v ((x v y) ^ z)) # label(false). [para(11(a,1),8199(a,1,2,1)),flip(a)]. given #339 (F,wt=19): 8232 x ^ ((x ^ y) v (z ^ (x v y))) = (x ^ y) v (z ^ x) # label(false). [para(54(a,1),8199(a,1,2,2)),demod(80(9))]. given #340 (F,wt=19): 8237 x ^ ((x ^ y) v (z ^ (y v x))) = (x ^ y) v (z ^ x) # label(false). [para(548(a,1),8199(a,1,2,2)),demod(122(9))]. given #341 (F,wt=19): 8238 (x ^ y) v (x ^ z) = x ^ ((y ^ x) v ((y v x) ^ z)) # label(false). [para(11(a,1),8200(a,1,2,1)),flip(a)]. given #342 (T,wt=15): 1471 x ^ (((x v y) ^ z) v (u ^ z)) = x ^ z. [para(486(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #343 (A,wt=17): 244 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(14(a,1),191(a,1,2,1,2)),demod(14(4),25(4),11(3),52(3),52(7))]. given #344 (F,wt=19): 8316 x ^ ((y ^ x) v ((x v y) ^ z)) = (y ^ x) v (x ^ z) # label(false). [para(11(a,1),8230(a,1,1)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 10.79 (+ 0.10) seconds. % Length of proof is 60. % Level of proof is 13. % Maximum clause weight is 25. % Given clauses 344. 8 c7 ^ (c8 v (c9 ^ ((c7 ^ (c8 v c9)) v (c8 ^ c9)))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [clausify]. 9 x v y = y v x. [input]. 10 (x v y) v z = x v (y v z). [input]. 11 x ^ y = y ^ x. [input]. 12 (x ^ y) ^ z = x ^ (y ^ z). [input]. 13 x ^ (x v y) = x. [input]. 14 x v (x ^ y) = x. [input]. 15 (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82) # label(false). [input]. 16 c7 ^ (c8 v (c9 ^ ((c8 ^ c9) v (c7 ^ (c8 v c9))))) != c7 ^ (c8 v (c7 ^ c9)) # label(H2). [copy(8),demod(9(12))]. 17 x v (y v z) = y v (x v z). [para(9(a,1),10(a,1,1)),demod(10(2))]. 18 x ^ (y ^ z) = y ^ (x ^ z). [para(11(a,1),12(a,1,1)),demod(12(2))]. 19 x ^ (y v x) = x. [para(9(a,1),13(a,1,2))]. 21 x ^ ((x v y) ^ z) = x ^ z. [para(13(a,1),12(a,1,1)),flip(a)]. 22 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(13(a,1),12(a,1)),flip(a)]. 25 x v (y ^ x) = x. [para(11(a,1),14(a,1,2))]. 26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(12(a,1),14(a,1,2))]. 27 x ^ x = x. [para(14(a,1),13(a,1,2))]. 28 x v x = x. [para(13(a,1),14(a,1,2))]. 29 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y) # label(false). [para(15(a,1),9(a,1))]. 32 x ^ (((x v y) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),15(a,2,2,1)),flip(a)]. 41 x ^ (((y v x) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y) # label(false). [para(9(a,1),32(a,1,2,1,1))]. 43 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),32(a,1,2,2))]. 52 x ^ (x ^ y) = x ^ y. [para(27(a,1),12(a,1,1)),flip(a)]. 54 x ^ (y ^ x) = y ^ x. [para(27(a,1),12(a,2,2)),demod(11(2))]. 61 x v (y v (x ^ z)) = y v x. [para(14(a,1),17(a,1,2)),flip(a)]. 77 x v (x v y) = x v y. [para(28(a,1),10(a,1,1)),flip(a)]. 80 x ^ (y ^ (x v z)) = y ^ x. [para(13(a,1),18(a,1,2)),flip(a)]. 81 x v (y ^ (x ^ z)) = x. [para(18(a,1),14(a,1,2))]. 93 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(14(a,1),43(a,1,2,1,1)),demod(18(4),21(4),52(7))]. 111 x ^ ((y v x) ^ z) = x ^ z. [para(19(a,1),12(a,1,1)),flip(a)]. 122 x ^ (y ^ (z v x)) = y ^ x. [para(19(a,1),18(a,1,2)),flip(a)]. 150 x v (y ^ (z ^ x)) = x. [para(12(a,1),25(a,1,2))]. 153 x ^ ((x ^ y) v (y ^ x)) = x ^ y. [para(25(a,1),29(a,2)),demod(12(3),19(2),14(3))]. 154 x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x). [para(25(a,1),32(a,1,2,1,1)),demod(12(4),13(3),54(7))]. 168 (x ^ y) v (y ^ x) = x ^ y. [back_demod(153),demod(154(4))]. 177 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(52(a,1),12(a,2,2)),demod(18(3),12(2))]. 178 x ^ (((x v y) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(52(a,1),32(a,1,2,1)),demod(21(11))]. 179 x ^ (((y v x) ^ z) v (y ^ (x v ((y v x) ^ z)))) = (x ^ z) v (x ^ y) # label(false). [para(52(a,1),41(a,1,2,1)),demod(111(11))]. 183 x ^ (((x v y) ^ z) v (y ^ (x v (z ^ (x v y))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),178(a,1,2,2,2,2))]. 187 x ^ (((y v x) ^ z) v (y ^ (x v (z ^ (y v x))))) = (x ^ z) v (x ^ y) # label(false). [para(11(a,1),179(a,1,2,2,2,2))]. 190 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(12(a,1),54(a,1,2)),demod(12(5))]. 191 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z) # label(false). [para(54(a,1),32(a,1,2,1)),demod(80(11))]. 195 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(11(a,1),22(a,1,2,2,1))]. 239 x ^ ((y ^ z) v (y ^ ((x ^ y) v (z ^ y)))) = x ^ y. [para(25(a,1),187(a,1,2,1,1)),demod(25(5),12(8),93(7),12(9),11(11),54(11),9(11),26(11))]. 240 (x v y) ^ (y v x) = y v x. [para(183(a,1),187(a,1,2,2)),demod(27(3),27(4),77(3),11(3),19(3),13(3),14(3),27(6),11(5),19(5),27(6),11(5),13(5))]. 247 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(25(a,1),191(a,1,2,1,2)),demod(25(4),25(4),11(3),54(3),54(7))]. 252 x ^ ((y ^ z) v ((x ^ y) v (z ^ y))) = x ^ y. [back_demod(239),demod(247(5))]. 313 x ^ ((y ^ x) v (z ^ (x ^ u))) = (y ^ x) v (z ^ (x ^ u)). [para(81(a,1),191(a,1,2,1,2)),demod(81(6),25(5),11(4),177(4),177(9))]. 377 x ^ ((x ^ y) v (z ^ (u ^ x))) = (x ^ y) v (z ^ (u ^ x)). [para(150(a,1),32(a,1,2,1,1)),demod(12(5),12(4),13(3),190(9))]. 480 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(168(a,1),10(a,2,2)),demod(9(4))]. 483 (x ^ y) v (z ^ (y ^ x)) = y ^ x. [para(168(a,1),29(a,1,2,2,2)),demod(12(5),195(5),12(6),377(5),313(5),12(6),18(9),11(8),52(8),54(8),9(8),26(8))]. 486 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [back_demod(252),demod(480(5))]. 548 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(240(a,1),18(a,1,2)),flip(a)]. 1455 (x ^ (y v z)) v (y ^ x) = (y v z) ^ x. [para(21(a,1),483(a,1,2))]. 1465 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(13(a,1),486(a,1,2,2)),demod(9(3))]. 8199 x ^ ((x ^ y) v ((x v y) ^ z)) = (x ^ y) v (x ^ z) # label(false). [para(29(a,1),1465(a,1,2,2)),demod(17(6),1455(5),29(11))]. 8230 (x ^ y) v (x ^ z) = x ^ ((y ^ x) v ((x v y) ^ z)) # label(false). [para(11(a,1),8199(a,1,2,1)),flip(a)]. 8316 x ^ ((y ^ x) v ((x v y) ^ z)) = (y ^ x) v (x ^ z) # label(false). [para(11(a,1),8230(a,1,1)),flip(a)]. 8385 x ^ ((y ^ x) v (z ^ (y v x))) = (y ^ x) v (z ^ x) # label(false). [para(548(a,1),8316(a,1,2,2)),demod(122(9))]. 8387 $F. [back_demod(16),demod(8385(13),9(9),61(10),9(6)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=344. Generated=253102. Kept=8378. proofs=1. Usable=336. Sos=7155. Demods=7274. Denials=0. Limbo=2, Disabled=893. Hints=0. Weight_deleted=77498. Literals_deleted=0. Forward_subsumed=163753. Back_subsumed=155. Sos_limit_deleted=3472. Sos_displaced=0. Sos_removed=0. New_demodulators=7924 (4 lex), Back_demodulated=730. Back_unit_deleted=0. Demod_attempts=5310687. Demod_rewrites=898971. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.45. User_CPU=10.79, System_CPU=0.10, Wall_clock=10. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13993 exit (max_proofs) Mon Jun 19 17:19:35 2006