============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13805 was started by mccune on cleo.thornwood, Mon Jun 19 16:51:26 2006 The command was "/home/mccune/bin/prover9 -f lt.in H39-H3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in 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. % Reading from file H39-H3.in clauses(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). end_of_list. clauses(goals). x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) # answer(H3). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). 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 (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). [input]. 8 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [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([ c1, c2, c3, ^, v ]). After inverse_order: Function symbol precedence: lex([ c1, c2, c3, ^, 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. ============================== 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 (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))) # label(H39). [copy(7),flip(a)]. 16 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [clausify]. 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 (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))) # label(H39). [copy(7),flip(a)]. given #8 (I,wt=23): 16 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [clausify]. given #9 (T,wt=5): 27 x ^ x = x. [para(14(a,1),13(a,1,2))]. given #10 (T,wt=5): 28 x v x = x. [para(13(a,1),14(a,1,2))]. given #11 (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 #12 (F,wt=7): 19 x ^ (y v x) = x. [para(9(a,1),13(a,1,2))]. given #13 (F,wt=7): 25 x v (y ^ x) = x. [para(11(a,1),14(a,1,2))]. given #14 (T,wt=9): 42 x ^ (x ^ y) = x ^ y. [para(27(a,1),12(a,1,1)),flip(a)]. given #15 (T,wt=9): 44 x ^ (y ^ x) = y ^ x. [para(27(a,1),12(a,2,2)),demod(11(2))]. given #16 (A,wt=11): 18 x ^ (y ^ z) = y ^ (x ^ z). [para(11(a,1),12(a,1,1)),demod(12(2))]. given #17 (F,wt=9): 45 x v (x v y) = x v y. [para(28(a,1),10(a,1,1)),flip(a)]. given #18 (F,wt=9): 47 x v (y v x) = y v x. [para(28(a,1),10(a,2,2)),demod(9(2))]. given #19 (T,wt=9): 48 x ^ (y v (x v z)) = x. [para(17(a,1),13(a,1,2))]. given #20 (T,wt=9): 50 x ^ (y v (z v x)) = x. [para(10(a,1),19(a,1,2))]. given #21 (A,wt=13): 20 (x v y) ^ (x v (y v z)) = x v y. [para(10(a,1),13(a,1,2))]. given #22 (F,wt=9): 56 x v (y ^ (z ^ x)) = x. [para(12(a,1),25(a,1,2))]. given #23 (F,wt=9): 63 x v (y ^ (x ^ z)) = x. [para(18(a,1),14(a,1,2))]. given #24 (T,wt=11): 21 x ^ ((x v y) ^ z) = x ^ z. [para(13(a,1),12(a,1,1)),flip(a)]. given #25 (T,wt=11): 23 x v ((x ^ y) v z) = x v z. [para(14(a,1),10(a,1,1)),flip(a)]. given #26 (A,wt=13): 22 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(13(a,1),12(a,1)),flip(a)]. given #27 (F,wt=11): 49 x v (y v (x ^ z)) = y v x. [para(14(a,1),17(a,1,2)),flip(a)]. given #28 (F,wt=11): 51 x ^ ((y v x) ^ z) = x ^ z. [para(19(a,1),12(a,1,1)),flip(a)]. given #29 (T,wt=11): 54 x v ((y ^ x) v z) = x v z. [para(25(a,1),10(a,1,1)),flip(a)]. given #30 (T,wt=11): 57 x v (y v (z ^ x)) = y v x. [para(25(a,1),17(a,1,2)),flip(a)]. given #31 (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 #32 (F,wt=11): 62 x ^ (y ^ (x v z)) = y ^ x. [para(13(a,1),18(a,1,2)),flip(a)]. given #33 (F,wt=11): 64 x ^ (y ^ (z v x)) = y ^ x. [para(19(a,1),18(a,1,2)),flip(a)]. given #34 (T,wt=11): 71 x ^ (y v (z v (x v u))) = x. [para(10(a,1),48(a,1,2))]. given #35 (T,wt=11): 75 x ^ (y v (z v (u v x))) = x. [para(10(a,1),50(a,1,2,2))]. given #36 (A,wt=13): 26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(12(a,1),14(a,1,2))]. given #37 (F,wt=11): 87 (x v y) ^ (y v x) = x v y. [para(47(a,1),20(a,1,2))]. given #38 (F,wt=11): 90 x v (y ^ (z ^ (u ^ x))) = x. [para(12(a,1),56(a,1,2,2))]. given #39 (T,wt=11): 97 x v (y ^ (z ^ (x ^ u))) = x. [para(12(a,1),63(a,1,2))]. given #40 (T,wt=11): 101 (x v y) ^ (z ^ x) = z ^ x. [para(44(a,1),21(a,2)),demod(61(4))]. given #41 (A,wt=21): 29 x ^ (y v (z ^ ((x ^ z) v u))) = x ^ (y v (z ^ (x v u))). [para(9(a,1),15(a,1,2,2,2))]. given #42 (F,wt=11): 108 (x ^ y) v (z v x) = z v x. [para(47(a,1),23(a,2)),demod(69(4))]. given #43 (F,wt=11): 125 (x v y) ^ (z ^ y) = z ^ y. [para(44(a,1),51(a,2)),demod(61(4))]. given #44 (T,wt=11): 136 (x ^ y) v (z v y) = z v y. [para(47(a,1),54(a,2)),demod(69(4))]. given #45 (T,wt=11): 200 (x ^ y) v (y ^ x) = x ^ y. [para(44(a,1),26(a,1,2))]. given #46 (A,wt=21): 30 x ^ ((y ^ (z v (x ^ y))) v u) = x ^ (u v (y ^ (x v z))). [para(9(a,1),15(a,1,2))]. given #47 (F,wt=25): 337 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ ((c1 ^ c2) v (c1 ^ c3)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [para(30(a,2),16(a,1,2,2)),demod(11(10),9(14))]. given #48 (F,wt=13): 52 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(19(a,1),12(a,1)),flip(a)]. given #49 (T,wt=13): 53 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),19(a,1,2))]. given #50 (T,wt=13): 55 x v (y v (z ^ (x v y))) = x v y. [para(25(a,1),10(a,1)),flip(a)]. given #51 (A,wt=21): 31 x ^ (y v (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (u v x))). [para(9(a,1),15(a,2,2,2,2))]. given #52 (F,wt=13): 59 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(42(a,1),12(a,2,2)),demod(18(3),12(2))]. given #53 (F,wt=13): 61 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(12(a,1),44(a,1,2)),demod(12(5))]. given #54 (T,wt=13): 65 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(18(a,1),25(a,1,2))]. given #55 (T,wt=13): 67 x v (y v (x v z)) = y v (x v z). [para(45(a,1),10(a,2,2)),demod(17(3),10(2))]. given #56 (A,wt=43): 38 x ^ (y v ((z v (u ^ (v v (x ^ u)))) ^ (w v (x ^ (z v (u ^ (x v v))))))) = x ^ (y v ((z v (u ^ (v v (x ^ u)))) ^ (x v w))). [para(15(a,1),15(a,1,2,2,2,2))]. given #57 (F,wt=13): 69 x v (y v (z v x)) = y v (z v x). [para(10(a,1),47(a,1,2)),demod(10(5))]. given #58 (F,wt=13): 72 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(48(a,1),12(a,1,1)),flip(a)]. given #59 (T,wt=13): 74 x ^ (y ^ (z v (x v u))) = y ^ x. [para(48(a,1),18(a,1,2)),flip(a)]. given #60 (T,wt=13): 76 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(50(a,1),12(a,1,1)),flip(a)]. given #61 (A,wt=39): 39 x ^ (y v ((z v (u ^ (x v v))) ^ (w v (x ^ (z v (u ^ (v v x))))))) = x ^ (y v ((z v (u ^ (x v v))) ^ (x v w))). [para(15(a,2),15(a,1,2,2,2,2)),demod(31(8))]. given #62 (F,wt=13): 79 x ^ (y ^ (z v (u v x))) = y ^ x. [para(50(a,1),18(a,1,2)),flip(a)]. given #63 (F,wt=13): 80 (x v y) ^ (y v (x v z)) = y v x. [para(9(a,1),20(a,1,1))]. given #64 (T,wt=13): 81 (x v y) ^ (y v (z v x)) = x v y. [para(9(a,1),20(a,1,2)),demod(10(3))]. given #65 (T,wt=13): 88 x v ((y ^ (z ^ x)) v u) = x v u. [para(56(a,1),10(a,1,1)),flip(a)]. given #66 (A,wt=29): 41 x ^ (y v (z ^ ((u ^ (v v (z ^ u))) v x))) = x ^ (y v (z ^ (x v (u ^ (z v v))))). [para(15(a,1),15(a,2,2,2)),demod(31(8))]. given #67 (F,wt=13): 91 x v (y v (z ^ (u ^ x))) = y v x. [para(56(a,1),17(a,1,2)),flip(a)]. given #68 (F,wt=13): 94 x v ((y ^ (x ^ z)) v u) = x v u. [para(63(a,1),10(a,1,1)),flip(a)]. given #69 (T,wt=13): 98 x v (y v (z ^ (x ^ u))) = y v x. [para(63(a,1),17(a,1,2)),flip(a)]. given #70 (T,wt=13): 110 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(11(a,1),22(a,1,2,2,1))]. given #71 (A,wt=15): 70 (x v y) ^ (z v (x v (y v u))) = x v y. [para(10(a,1),48(a,1,2,2))]. given #72 (F,wt=13): 152 x v (y v ((y v x) ^ z)) = x v y. [para(9(a,1),24(a,1,2,2,1))]. given #73 (F,wt=13): 181 x ^ (y v (z v (u v (x v v)))) = x. [para(10(a,1),71(a,1,2,2))]. given #74 (T,wt=13): 185 x ^ (y v (z v (u v (v v x)))) = x. [para(10(a,1),75(a,1,2,2,2))]. given #75 (T,wt=13): 197 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(11(a,1),26(a,1,1))]. given #76 (A,wt=15): 73 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(48(a,1),12(a,1)),flip(a)]. given #77 (F,wt=13): 198 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(11(a,1),26(a,1,2)),demod(12(3))]. given #78 (F,wt=13): 211 x v (y v (z ^ (y v x))) = x v y. [para(87(a,1),56(a,1,2,2)),demod(10(4))]. given #79 (T,wt=13): 214 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(12(a,1),90(a,1,2,2,2))]. given #80 (T,wt=13): 220 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(90(a,1),23(a,1,2)),demod(14(2)),flip(a)]. given #81 (A,wt=15): 77 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(50(a,1),12(a,1)),flip(a)]. given #82 (F,wt=13): 234 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),101(a,1,1))]. given #83 (F,wt=13): 241 (x v (y v z)) ^ (y v x) = y v x. [para(87(a,1),101(a,1,2)),demod(10(2),87(7))]. given #84 (T,wt=13): 271 (x ^ (y ^ z)) v (u v y) = u v y. [para(18(a,1),108(a,1,1))]. given #85 (T,wt=13): 279 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(10(a,1),125(a,1,1))]. given #86 (A,wt=15): 78 (x v y) ^ (z v (x v (u v y))) = x v y. [para(17(a,1),50(a,1,2,2))]. given #87 (F,wt=13): 294 (x v (y v z)) ^ (z v y) = z v y. [para(87(a,1),125(a,1,2)),demod(87(7))]. given #88 (F,wt=13): 298 (x ^ (y ^ z)) v (u v z) = u v z. [para(12(a,1),136(a,1,1))]. given #89 (T,wt=13): 320 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(200(a,1),50(a,1,2,2)),demod(12(4))]. given #90 (T,wt=13): 321 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(200(a,1),23(a,2)),demod(12(3),316(6))]. given #91 (A,wt=19): 82 (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 #92 (F,wt=13): 323 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(200(a,1),136(a,1,2)),demod(200(7))]. given #93 (F,wt=13): 430 (x v y) ^ (z v (y v x)) = x v y. [para(9(a,1),53(a,1,2)),demod(10(3))]. given #94 (T,wt=13): 511 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(11(a,1),65(a,1,2)),demod(12(3))]. given #95 (T,wt=13): 913 (x v (y v z)) ^ (z v x) = z v x. [para(81(a,1),11(a,1)),flip(a)]. given #96 (A,wt=17): 83 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(20(a,1),12(a,1,1)),flip(a)]. given #97 (F,wt=13): 1321 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(198(a,1),9(a,1)),flip(a)]. given #98 (F,wt=15): 85 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),20(a,1,2,2))]. given #99 (T,wt=15): 89 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(56(a,1),10(a,1)),flip(a)]. given #100 (T,wt=15): 92 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(18(a,1),56(a,1,2,2))]. given #101 (A,wt=19): 84 (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 #102 (F,wt=15): 95 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(63(a,1),10(a,1)),flip(a)]. given #103 (F,wt=15): 96 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(12(a,1),63(a,1,2,2))]. given #104 (T,wt=15): 100 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(21(a,1),25(a,1,2)),demod(9(4))]. given #105 (T,wt=15): 102 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(21(a,1),18(a,1,2)),flip(a)]. given #106 (A,wt=17): 86 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(20(a,1),18(a,1,2)),flip(a)]. given #107 (F,wt=15): 106 x v (y v ((x ^ z) v u)) = y v (x v u). [para(23(a,1),17(a,1,2)),flip(a)]. given #108 (F,wt=15): 107 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(23(a,1),19(a,1,2)),demod(11(4))]. given #109 (T,wt=15): 116 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(22(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #110 (T,wt=13): 2403 x ^ (((x v y) ^ (x v z)) v u) = x. [para(116(a,1),21(a,1)),demod(13(2)),flip(a)]. given #111 (A,wt=17): 93 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(20(a,1),56(a,1,2,2)),demod(10(5),10(4))]. given #112 (F,wt=13): 2404 x ^ (((x v y) ^ (z v x)) v u) = x. [para(116(a,1),51(a,1)),demod(19(2)),flip(a)]. given #113 (F,wt=13): 2457 x ^ (((y v x) ^ (x v z)) v u) = x. [para(9(a,1),2403(a,1,2,1,1))]. given #114 (T,wt=13): 2458 x ^ (y v ((x v z) ^ (x v u))) = x. [para(9(a,1),2403(a,1,2))]. given #115 (T,wt=13): 2557 x ^ (((y v x) ^ (z v x)) v u) = x. [para(9(a,1),2404(a,1,2,1,1))]. given #116 (A,wt=17): 99 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(21(a,1),12(a,1)),demod(12(2)),flip(a)]. given #117 (F,wt=13): 2558 x ^ (y v ((x v z) ^ (u v x))) = x. [para(9(a,1),2404(a,1,2))]. given #118 (F,wt=13): 2624 x ^ (y v ((z v x) ^ (x v u))) = x. [para(9(a,1),2457(a,1,2))]. given #119 (T,wt=13): 2704 x ^ (y v ((z v x) ^ (u v x))) = x. [para(9(a,1),2557(a,1,2))]. given #120 (T,wt=15): 118 x v (y v (z v (x ^ u))) = y v (z v x). [para(10(a,1),49(a,1,2)),demod(10(6))]. given #121 (A,wt=17): 103 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(21(a,1),56(a,1,2,2))]. given #122 (F,wt=15): 120 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(49(a,1),19(a,1,2)),demod(11(4))]. given #123 (F,wt=15): 124 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(51(a,1),25(a,1,2)),demod(9(4))]. given #124 (T,wt=15): 126 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(51(a,1),18(a,1,2)),flip(a)]. given #125 (T,wt=15): 130 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(22(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #126 (A,wt=17): 104 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 #127 (F,wt=15): 133 x v (y v ((z ^ x) v u)) = y v (x v u). [para(54(a,1),17(a,1,2)),flip(a)]. given #128 (F,wt=15): 134 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(54(a,1),19(a,1,2)),demod(11(4))]. given #129 (T,wt=13): 3605 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(321(a,1),134(a,1,2)),demod(11(5),12(5),2344(4),321(8))]. given #130 (T,wt=13): 3637 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(9(a,1),3605(a,1,2))]. given #131 (A,wt=17): 105 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(12(a,1),23(a,1,2,1))]. given #132 (F,wt=13): 3638 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(11(a,1),3605(a,1,2,1))]. given #133 (F,wt=13): 3639 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(11(a,1),3605(a,1,2,2))]. given #134 (T,wt=13): 3724 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(11(a,1),3637(a,1,2,1))]. given #135 (T,wt=13): 3725 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(11(a,1),3637(a,1,2,2))]. given #136 (A,wt=17): 109 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(23(a,1),50(a,1,2,2))]. given #137 (F,wt=13): 3854 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(11(a,1),3638(a,1,2,2))]. given #138 (F,wt=13): 4023 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(11(a,1),3724(a,1,2,2))]. given #139 (T,wt=15): 143 x v (y v (z v (u ^ x))) = y v (z v x). [para(10(a,1),57(a,1,2)),demod(10(6))]. given #140 (T,wt=15): 144 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(57(a,1),19(a,1,2)),demod(11(4))]. given #141 (A,wt=19): 111 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 #142 (F,wt=15): 158 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 #143 (F,wt=13): 4545 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(158(a,1),23(a,1)),demod(14(2)),flip(a)]. given #144 (T,wt=13): 4547 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(158(a,1),54(a,1)),demod(25(2)),flip(a)]. given #145 (T,wt=13): 4614 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(11(a,1),4545(a,1,2,1,1))]. given #146 (A,wt=19): 112 (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 #147 (F,wt=13): 4615 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(11(a,1),4545(a,1,2))]. given #148 (F,wt=13): 4674 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(11(a,1),4547(a,1,2,1,1))]. given #149 (T,wt=13): 4675 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(11(a,1),4547(a,1,2))]. given #150 (T,wt=13): 4786 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(11(a,1),4614(a,1,2))]. given #151 (A,wt=17): 113 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(22(a,1),18(a,1,2)),flip(a)]. given #152 (F,wt=13): 4987 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(11(a,1),4674(a,1,2))]. given #153 (F,wt=15): 160 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(24(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #154 (T,wt=15): 162 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(12(a,1),62(a,1,2)),demod(12(6))]. given #155 (T,wt=15): 163 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(62(a,1),25(a,1,2)),demod(9(4))]. given #156 (A,wt=19): 114 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 #157 (F,wt=15): 168 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(12(a,1),64(a,1,2)),demod(12(6))]. given #158 (F,wt=15): 170 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(64(a,1),25(a,1,2)),demod(9(4))]. given #159 (T,wt=13): 5892 x v ((y v x) ^ (y v z)) = x v y. [para(80(a,1),170(a,1,2)),demod(17(5),9(4),2174(4),80(8))]. given #160 (T,wt=13): 5972 x v ((x v y) ^ (y v z)) = x v y. [para(9(a,1),5892(a,1,2,1))]. given #161 (A,wt=21): 115 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(22(a,1),56(a,1,2,2))]. given #162 (F,wt=13): 5973 x v ((y v x) ^ (z v y)) = x v y. [para(9(a,1),5892(a,1,2,2))]. given #163 (F,wt=13): 5977 x v ((y v z) ^ (y v x)) = x v y. [para(11(a,1),5892(a,1,2))]. given #164 (T,wt=13): 6064 x v ((x v y) ^ (z v y)) = x v y. [para(9(a,1),5972(a,1,2,2))]. given #165 (T,wt=13): 6068 x v ((y v z) ^ (x v y)) = x v y. [para(11(a,1),5972(a,1,2))]. given #166 (A,wt=17): 117 x v (y v (z v ((x v y) ^ u))) = z v (x v y). [para(49(a,1),10(a,1)),flip(a)]. given #167 (F,wt=13): 6202 x v ((y v z) ^ (z v x)) = x v z. [para(11(a,1),5973(a,1,2))]. given #168 (F,wt=13): 6410 x v ((y v z) ^ (x v z)) = x v z. [para(11(a,1),6064(a,1,2))]. given #169 (T,wt=15): 173 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [para(22(a,1),64(a,2)),demod(29(8),18(8),12(7),99(8))]. given #170 (T,wt=15): 182 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(71(a,1),12(a,1,1)),flip(a)]. given #171 (A,wt=17): 119 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(12(a,1),49(a,1,2,2))]. given #172 (F,wt=15): 184 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(71(a,1),18(a,1,2)),flip(a)]. given #173 (F,wt=15): 186 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(75(a,1),12(a,1,1)),flip(a)]. given #174 (T,wt=15): 190 x ^ (y ^ (z v (u v (v v x)))) = y ^ x. [para(75(a,1),18(a,1,2)),flip(a)]. given #175 (T,wt=15): 202 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(18(a,1),26(a,1,2,2))]. given #176 (A,wt=17): 121 (x v (y ^ z)) ^ (u v (x v y)) = x v (y ^ z). [para(49(a,1),50(a,1,2,2))]. given #177 (F,wt=15): 207 (x v y) ^ ((y v x) ^ z) = (x v y) ^ z. [para(87(a,1),12(a,1,1)),flip(a)]. given #178 (F,wt=15): 212 x v ((y ^ (z ^ (u ^ x))) v v) = x v v. [para(90(a,1),10(a,1,1)),flip(a)]. given #179 (T,wt=15): 215 x v (y v (z ^ (u ^ (v ^ x)))) = y v x. [para(90(a,1),17(a,1,2)),flip(a)]. given #180 (T,wt=15): 226 x v (y v (z ^ (u ^ (y v x)))) = x v y. [para(87(a,1),90(a,1,2,2,2)),demod(10(5))]. given #181 (A,wt=17): 122 x ^ (y ^ ((z v (x ^ y)) ^ u)) = x ^ (y ^ u). [para(51(a,1),12(a,1)),demod(12(2)),flip(a)]. given #182 (F,wt=15): 227 x v ((y ^ (z ^ (x ^ u))) v v) = x v v. [para(97(a,1),10(a,1,1)),flip(a)]. given #183 (F,wt=15): 230 x v (y v (z ^ (u ^ (x ^ v)))) = y v x. [para(97(a,1),17(a,1,2)),flip(a)]. given #184 (T,wt=15): 232 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(101(a,1),12(a,1,1)),demod(12(2),12(5)),flip(a)]. given #185 (T,wt=15): 233 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(12(a,1),101(a,1,2)),demod(12(6))]. given #186 (A,wt=17): 123 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u. [para(17(a,1),51(a,1,2,1))]. given #187 (F,wt=15): 237 x ^ (y ^ ((x ^ (y v z)) v u)) = x ^ y. [para(62(a,1),101(a,1,2)),demod(11(5),12(5),62(8))]. given #188 (F,wt=15): 238 x ^ (y ^ ((x ^ (z v y)) v u)) = x ^ y. [para(64(a,1),101(a,1,2)),demod(11(5),12(5),64(8))]. given #189 (T,wt=15): 240 ((x v y) ^ z) v (z ^ x) = (x v y) ^ z. [para(101(a,1),26(a,1,2))]. given #190 (T,wt=15): 267 (x ^ y) v (z v (x v u)) = z v (x v u). [para(108(a,1),10(a,1,1)),demod(10(2),10(5)),flip(a)]. given #191 (A,wt=17): 127 ((x v y) ^ z) v (u ^ (y ^ z)) = (x v y) ^ z. [para(51(a,1),56(a,1,2,2))]. given #192 (F,wt=15): 268 (x ^ y) v (z v (u v x)) = z v (u v x). [para(10(a,1),108(a,1,2)),demod(10(6))]. given #193 (F,wt=15): 273 ((x ^ y) v z) ^ (z v x) = (x ^ y) v z. [para(108(a,1),20(a,1,2))]. given #194 (T,wt=15): 274 x v (y v ((x v (y ^ z)) ^ u)) = x v y. [para(49(a,1),108(a,1,2)),demod(9(5),10(5),49(8))]. given #195 (T,wt=15): 275 x v (y v ((x v (z ^ y)) ^ u)) = x v y. [para(57(a,1),108(a,1,2)),demod(9(5),10(5),57(8))]. given #196 (A,wt=17): 128 x ^ (y ^ (z ^ (x ^ u))) = y ^ (z ^ (x ^ u)). [para(56(a,1),51(a,1,2,1)),demod(18(4),12(3),12(2),12(7),12(6))]. given #197 (F,wt=15): 277 (x v y) ^ (z ^ (y ^ u)) = z ^ (y ^ u). [para(108(a,1),101(a,1,1))]. given #198 (F,wt=15): 278 (x ^ y) v (z v (y v u)) = z v (y v u). [para(101(a,1),108(a,1,1))]. given #199 (T,wt=15): 280 (x v y) ^ (z ^ (u ^ y)) = z ^ (u ^ y). [para(12(a,1),125(a,1,2)),demod(12(6))]. given #200 (T,wt=15): 283 x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y. [para(21(a,1),125(a,1,2)),demod(11(5),12(5),21(8))]. given #201 (A,wt=19): 129 (x v y) ^ (((x ^ z) v y) ^ u) = ((x ^ z) v y) ^ u. [para(23(a,1),51(a,1,2,1)),demod(18(5))]. given #202 (F,wt=15): 285 x ^ (y ^ (z v (x ^ (y v u)))) = y ^ x. [para(22(a,1),125(a,1,2)),demod(11(6),12(6),252(6),22(9))]. given #203 (F,wt=15): 287 x ^ (y ^ (z v ((u v x) ^ y))) = x ^ y. [para(51(a,1),125(a,1,2)),demod(11(5),12(5),51(8))]. given #204 (T,wt=15): 291 x ^ (y ^ (z v (x ^ (u v y)))) = x ^ y. [para(64(a,1),125(a,1,2)),demod(11(5),12(5),64(8))]. given #205 (T,wt=15): 293 ((x v y) ^ z) v (z ^ y) = (x v y) ^ z. [para(125(a,1),26(a,1,2))]. given #206 (A,wt=19): 131 (x v y) ^ ((x v (y ^ z)) ^ u) = (x v (y ^ z)) ^ u. [para(49(a,1),51(a,1,2,1)),demod(18(5))]. given #207 (F,wt=15): 297 (x ^ y) v (z v (u v y)) = z v (u v y). [para(125(a,1),108(a,1,1))]. given #208 (F,wt=15): 302 ((x ^ y) v z) ^ (z v y) = (x ^ y) v z. [para(136(a,1),20(a,1,2))]. given #209 (T,wt=15): 304 x v (y v (z ^ ((x ^ u) v y))) = x v y. [para(23(a,1),136(a,1,2)),demod(9(5),10(5),23(8))]. given #210 (T,wt=15): 306 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(49(a,1),136(a,1,2)),demod(9(5),10(5),49(8))]. given #211 (A,wt=17): 132 x v (y v ((z ^ (x v y)) v u)) = x v (y v u). [para(54(a,1),10(a,1)),demod(10(2)),flip(a)]. given #212 (F,wt=15): 308 x v (y v (z ^ ((u ^ x) v y))) = x v y. [para(54(a,1),136(a,1,2)),demod(9(5),10(5),54(8))]. given #213 (F,wt=15): 309 x v (y v (z ^ (x v (u ^ y)))) = x v y. [para(57(a,1),136(a,1,2)),demod(9(5),10(5),57(8))]. given #214 (T,wt=15): 315 (x ^ y) v ((y ^ x) v z) = (x ^ y) v z. [para(200(a,1),10(a,1,1)),flip(a)]. given #215 (T,wt=15): 316 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(200(a,1),10(a,2,2)),demod(9(4))]. given #216 (A,wt=17): 135 (x ^ y) v ((x ^ (z ^ y)) v u) = (x ^ y) v u. [para(18(a,1),54(a,1,2,1))]. given #217 (F,wt=15): 322 x ^ (y ^ (z v (u v (y ^ x)))) = x ^ y. [para(200(a,1),75(a,1,2,2,2)),demod(12(5))]. given #218 (F,wt=15): 421 x ^ (y ^ (z v (y ^ (u v x)))) = x ^ y. [para(52(a,1),64(a,2)),demod(31(8),18(8),12(7),122(8))]. given #219 (T,wt=15): 432 (x v y) ^ (x v (z v (u v y))) = x v y. [para(10(a,1),53(a,1,2,2))]. given #220 (T,wt=15): 503 (x v (y v (z v u))) ^ (v ^ z) = v ^ z. [para(71(a,1),61(a,1,2,2)),demod(71(9))]. given #221 (A,wt=17): 137 ((x ^ y) v z) ^ (u v (y v z)) = (x ^ y) v z. [para(54(a,1),50(a,1,2,2))]. given #222 (F,wt=15): 504 (x v (y v (z v u))) ^ (v ^ u) = v ^ u. [para(75(a,1),61(a,1,2,2)),demod(75(9))]. given #223 (F,wt=15): 505 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(61(a,1),26(a,1,2,2))]. given #224 (T,wt=15): 506 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(87(a,1),61(a,1,2,2)),demod(87(7))]. given #225 (T,wt=15): 685 (x ^ (y ^ (z ^ u))) v (v v u) = v v u. [para(90(a,1),69(a,1,2,2)),demod(90(9))]. given #226 (A,wt=17): 138 x v (y v (z v (x v u))) = y v (z v (x v u)). [para(50(a,1),54(a,1,2,1)),demod(17(4),10(3),10(2),10(7),10(6))]. given #227 (F,wt=15): 686 (x ^ (y ^ (z ^ u))) v (v v z) = v v z. [para(97(a,1),69(a,1,2,2)),demod(97(9))]. given #228 (F,wt=15): 696 x ^ (y v (z v (u v (v v (x v w))))) = x. [para(75(a,1),72(a,1,2)),demod(48(3)),flip(a)]. given #229 (T,wt=15): 697 (x v (y v (z v u))) ^ (z v y) = y v z. [para(87(a,1),72(a,2)),demod(10(3),506(7))]. given #230 (T,wt=15): 739 x ^ (y v (z v (u v (v v (w v x))))) = x. [para(75(a,1),76(a,1,2)),demod(50(3)),flip(a)]. given #231 (A,wt=19): 139 (x ^ y) v (((x v z) ^ y) v u) = ((x v z) ^ y) v u. [para(21(a,1),54(a,1,2,1)),demod(17(5))]. given #232 (F,wt=15): 904 (x v y) ^ (y v (z v (x v u))) = y v x. [para(17(a,1),80(a,1,2,2))]. given #233 (F,wt=15): 909 (x v y) ^ (y v (z v (u v x))) = y v x. [para(69(a,1),80(a,1,2,2))]. given #234 (T,wt=15): 930 (x v (y v (z v u))) ^ (z v x) = z v x. [para(81(a,1),101(a,1,2)),demod(10(3),10(2),81(9))]. given #235 (T,wt=15): 931 (x v (y v (z v u))) ^ (u v y) = u v y. [para(81(a,1),125(a,1,2)),demod(81(9))]. given #236 (A,wt=23): 140 (x ^ y) v ((y ^ ((x ^ y) v z)) v u) = (y ^ ((x ^ y) v z)) v u. [para(22(a,1),54(a,1,2,1)),demod(17(6))]. given #237 (F,wt=15): 957 x v (y ^ (z ^ (u ^ (v ^ (w ^ x))))) = x. [para(90(a,1),88(a,1,2)),demod(56(3)),flip(a)]. given #238 (F,wt=15): 958 x v (y ^ (z ^ (u ^ (v ^ (x ^ w))))) = x. [para(97(a,1),88(a,1,2)),demod(56(3),12(3),12(2)),flip(a)]. given #239 (T,wt=15): 1145 (x ^ (y ^ (z ^ u))) v (z ^ y) = y ^ z. [para(200(a,1),94(a,2)),demod(12(3),316(7))]. given #240 (T,wt=15): 1178 x ^ (y ^ (z v ((y ^ x) v u))) = x ^ y. [para(17(a,1),110(a,1,2,2))]. given #241 (A,wt=19): 141 (x v y) ^ (((z ^ x) v y) ^ u) = ((z ^ x) v y) ^ u. [para(54(a,1),51(a,1,2,1)),demod(18(5))]. given #242 (F,wt=15): 1183 x ^ (y ^ ((y ^ (x v z)) v u)) = x ^ y. [para(110(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #243 (F,wt=15): 1184 x ^ (y ^ ((y ^ (z v x)) v u)) = x ^ y. [para(110(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #244 (T,wt=15): 1204 (x v y) ^ (z v (y v (x v u))) = y v x. [para(9(a,1),70(a,1,1))]. given #245 (T,wt=15): 1205 (x v y) ^ (z v (y v (u v x))) = x v y. [para(9(a,1),70(a,1,2,2)),demod(10(3))]. given #246 (A,wt=19): 142 (x ^ y) v (((z v x) ^ y) v u) = ((z v x) ^ y) v u. [para(51(a,1),54(a,1,2,1)),demod(17(5))]. given #247 (F,wt=15): 1226 x v (y v (z ^ ((y v x) ^ u))) = x v y. [para(18(a,1),152(a,1,2,2))]. given #248 (F,wt=15): 1228 x v (y v ((y v (x ^ z)) ^ u)) = x v y. [para(152(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #249 (T,wt=15): 1230 x v (y v ((y v (z ^ x)) ^ u)) = x v y. [para(152(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #250 (T,wt=15): 1282 (x ^ y) v (y ^ (z ^ (x ^ u))) = y ^ x. [para(18(a,1),197(a,1,2,2))]. given #251 (A,wt=17): 145 (x ^ y) v (z v (x ^ (u ^ y))) = z v (x ^ y). [para(18(a,1),57(a,1,2,2))]. given #252 (F,wt=15): 1286 (x ^ y) v (y ^ (z ^ (u ^ x))) = y ^ x. [para(61(a,1),197(a,1,2,2))]. given #253 (F,wt=15): 1342 (x ^ (y ^ (z ^ u))) v (z ^ x) = z ^ x. [para(198(a,1),108(a,1,2)),demod(12(3),12(2),198(9))]. low water: id=5684, wt=51 low water: id=5603, wt=49 low water: id=5604, wt=47 low water: id=5764, wt=45 given #254 (T,wt=15): 1343 (x ^ (y ^ (z ^ u))) v (u ^ y) = u ^ y. [para(198(a,1),136(a,1,2)),demod(198(9))]. low water: id=5795, wt=43 low water: id=6191, wt=41 low water: id=6195, wt=39 low water: id=6196, wt=37 given #255 (T,wt=15): 1382 x v (y v (z ^ (y v (x ^ u)))) = x v y. [para(211(a,1),23(a,1,2)),demod(23(3)),flip(a)]. low water: id=6612, wt=35 given #256 (A,wt=17): 146 (x v (y ^ z)) ^ (u v (x v z)) = x v (y ^ z). [para(57(a,1),50(a,1,2,2))]. given #257 (F,wt=15): 1384 x v (y v (z ^ (y v (u ^ x)))) = x v y. [para(211(a,1),54(a,1,2)),demod(54(3)),flip(a)]. low water: id=6944, wt=33 given #258 (F,wt=15): 1514 (x v (y v (z v u))) ^ (u v x) = u v x. [para(69(a,1),241(a,1,1,2))]. given #259 (T,wt=15): 1559 (x v (y v (z v u))) ^ (u v z) = u v z. [para(87(a,1),279(a,1,2)),demod(87(8))]. given #260 (T,wt=15): 1590 (x v y) ^ (z v (u v (y v x))) = x v y. [para(9(a,1),78(a,1,2,2)),demod(10(3))]. given #261 (A,wt=23): 149 (x ^ ((y ^ x) v z)) v (u v (y ^ x)) = u v (x ^ ((y ^ x) v z)). [para(22(a,1),57(a,1,2,2))]. given #262 (F,wt=15): 1629 (x v y) ^ (y v (x ^ z)) = y v (x ^ z). [para(23(a,1),294(a,1,1))]. low water: id=7494, wt=31 given #263 (F,wt=15): 1630 (x v y) ^ ((y ^ z) v x) = (y ^ z) v x. [para(49(a,1),294(a,1,1))]. given #264 (T,wt=15): 1631 (x v y) ^ (y v (z ^ x)) = y v (z ^ x). [para(54(a,1),294(a,1,1))]. given #265 (T,wt=15): 1632 (x v y) ^ ((z ^ y) v x) = (z ^ y) v x. [para(57(a,1),294(a,1,1))]. given #266 (A,wt=19): 150 (x v y) ^ ((x v (z ^ y)) ^ u) = (x v (z ^ y)) ^ u. [para(57(a,1),51(a,1,2,1)),demod(18(5))]. given #267 (F,wt=15): 1660 (x ^ (y ^ (z ^ u))) v (u ^ z) = u ^ z. [para(200(a,1),298(a,1,2)),demod(200(8))]. low water: id=7910, wt=29 given #268 (F,wt=15): 1732 (x ^ (y ^ (z ^ u))) v (u ^ x) = x ^ u. [para(61(a,1),321(a,1,1,2))]. given #269 (T,wt=15): 1778 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(21(a,1),323(a,1,1))]. given #270 (T,wt=15): 1779 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [para(51(a,1),323(a,1,1))]. given #271 (A,wt=19): 153 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(24(a,1),10(a,1)),demod(10(2),10(4)),flip(a)]. given #272 (F,wt=15): 1780 (x ^ y) v ((y v z) ^ x) = (y v z) ^ x. [para(62(a,1),323(a,1,1))]. given #273 (F,wt=15): 1781 (x ^ y) v ((z v y) ^ x) = (z v y) ^ x. [para(64(a,1),323(a,1,1))]. given #274 (T,wt=15): 1808 (x v (y ^ z)) ^ (y v x) = x v (y ^ z). [para(23(a,1),430(a,1,2))]. given #275 (T,wt=15): 1809 (x v (y ^ z)) ^ (z v x) = x v (y ^ z). [para(54(a,1),430(a,1,2))]. given #276 (A,wt=17): 154 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(24(a,1),17(a,1,2)),flip(a)]. given #277 (F,wt=15): 1817 (x ^ y) v (z ^ (u ^ (y ^ x))) = x ^ y. [para(12(a,1),511(a,1,2))]. given #278 (F,wt=15): 1819 (x ^ (y v z)) v (y ^ x) = x ^ (y v z). [para(21(a,1),511(a,1,2))]. given #279 (T,wt=15): 1820 (x ^ y) v (z ^ (y ^ (x ^ u))) = x ^ y. [para(511(a,1),49(a,2)),demod(12(6),12(5),1772(8))]. given #280 (T,wt=15): 1821 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(51(a,1),511(a,1,2))]. low water: id=8589, wt=27 given #281 (A,wt=19): 155 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(17(a,1),24(a,1,2,2,1)),demod(10(5))]. given #282 (F,wt=15): 2014 (x ^ y) v (z ^ (y ^ (u ^ x))) = y ^ x. [para(11(a,1),92(a,1,1))]. given #283 (F,wt=15): 2264 x ^ (y ^ (((y v z) ^ x) v u)) = x ^ y. [para(110(a,1),102(a,1,2)),demod(62(3)),flip(a)]. given #284 (T,wt=15): 2271 x ^ (y ^ (z v ((y v u) ^ x))) = x ^ y. [para(320(a,1),102(a,1,2)),demod(62(3)),flip(a)]. given #285 (T,wt=15): 2333 x v (y v (((y ^ z) v x) ^ u)) = x v y. [para(152(a,1),106(a,1,2)),demod(49(3)),flip(a)]. given #286 (A,wt=19): 156 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(24(a,1),19(a,1,2)),demod(11(5))]. given #287 (F,wt=15): 2335 x v (y v (z ^ ((y ^ u) v x))) = x v y. [para(211(a,1),106(a,1,2)),demod(49(3)),flip(a)]. given #288 (F,wt=15): 2423 x ^ (((x v y) ^ (z v (x v u))) v v) = x. [para(116(a,1),72(a,1)),demod(48(3)),flip(a)]. given #289 (T,wt=15): 2425 x ^ (((x v y) ^ (z v (u v x))) v v) = x. [para(116(a,1),76(a,1)),demod(50(3)),flip(a)]. given #290 (T,wt=15): 2461 x ^ (((y v (x v z)) ^ (x v u)) v v) = x. [para(17(a,1),2403(a,1,2,1,1))]. given #291 (A,wt=21): 157 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(24(a,1),50(a,1,2,2))]. given #292 (F,wt=15): 2462 x ^ (y v (((x v z) ^ (x v u)) v v)) = x. [para(17(a,1),2403(a,1,2))]. given #293 (F,wt=15): 2477 x ^ (((y v (z v x)) ^ (x v u)) v v) = x. [para(69(a,1),2403(a,1,2,1,1))]. given #294 (T,wt=15): 2478 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(69(a,1),2403(a,1,2))]. given #295 (T,wt=15): 2563 x ^ (((y v (x v z)) ^ (u v x)) v v) = x. [para(17(a,1),2404(a,1,2,1,1))]. given #296 (A,wt=23): 159 (x v y) ^ ((y v ((x v y) ^ z)) ^ u) = (y v ((x v y) ^ z)) ^ u. [para(24(a,1),51(a,1,2,1)),demod(18(6))]. given #297 (F,wt=15): 2565 x ^ (y v (((x v z) ^ (u v x)) v v)) = x. [para(17(a,1),2404(a,1,2))]. given #298 (F,wt=15): 2589 x ^ (((y v (z v x)) ^ (u v x)) v v) = x. [para(69(a,1),2404(a,1,2,1,1))]. given #299 (T,wt=15): 2590 x ^ (y v (z v ((x v u) ^ (v v x)))) = x. [para(69(a,1),2404(a,1,2))]. given #300 (T,wt=15): 2629 x ^ (((y v x) ^ (z v (x v u))) v v) = x. [para(17(a,1),2457(a,1,2,1,2))]. given #301 (A,wt=17): 161 x ^ (y ^ (z ^ ((x ^ y) v u))) = z ^ (x ^ y). [para(62(a,1),12(a,1)),flip(a)]. given #302 (F,wt=15): 2630 x ^ (y v (((z v x) ^ (x v u)) v v)) = x. [para(17(a,1),2457(a,1,2))]. given #303 (F,wt=15): 2643 x ^ (((y v x) ^ (z v (u v x))) v v) = x. [para(69(a,1),2457(a,1,2,1,2))]. given #304 (T,wt=15): 2644 x ^ (y v (z v ((u v x) ^ (x v v)))) = x. [para(69(a,1),2457(a,1,2))]. given #305 (T,wt=15): 2666 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(17(a,1),2458(a,1,2,2,1))]. given #306 (A,wt=17): 164 (x ^ (y v z)) v (u ^ (x ^ y)) = x ^ (y v z). [para(62(a,1),56(a,1,2,2))]. given #307 (F,wt=15): 2667 x ^ (y v ((x v z) ^ (u v (x v v)))) = x. [para(17(a,1),2458(a,1,2,2,2))]. given #308 (F,wt=15): 2680 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(69(a,1),2458(a,1,2,2,1))]. given #309 (T,wt=15): 2681 x ^ (y v ((x v z) ^ (u v (v v x)))) = x. [para(69(a,1),2458(a,1,2,2,2))]. low water: id=9482, wt=25 given #310 (T,wt=15): 2710 x ^ (y v (((z v x) ^ (u v x)) v v)) = x. [para(17(a,1),2557(a,1,2))]. given #311 (A,wt=19): 165 (x ^ y) v ((x ^ (y v z)) v u) = (x ^ (y v z)) v u. [para(62(a,1),54(a,1,2,1)),demod(17(5))]. given #312 (F,wt=15): 2733 x ^ (y v (z v ((u v x) ^ (v v x)))) = x. [para(69(a,1),2557(a,1,2))]. given #313 (F,wt=15): 2846 x ^ (y v ((z v (x v u)) ^ (v v x))) = x. [para(17(a,1),2558(a,1,2,2,1))]. given #314 (T,wt=15): 2869 x ^ (y v ((z v (u v x)) ^ (v v x))) = x. [para(69(a,1),2558(a,1,2,2,1))]. given #315 (T,wt=15): 2906 x ^ (y v ((z v x) ^ (u v (x v v)))) = x. [para(17(a,1),2624(a,1,2,2,2))]. given #316 (A,wt=17): 167 x ^ (y ^ (z ^ (u v (x ^ y)))) = z ^ (x ^ y). [para(64(a,1),12(a,1)),flip(a)]. given #317 (F,wt=15): 2917 x ^ (y v ((z v x) ^ (u v (v v x)))) = x. [para(69(a,1),2624(a,1,2,2,2))]. given #318 (F,wt=15): 3304 x ^ (y ^ (((z v y) ^ x) v u)) = x ^ y. [para(110(a,1),126(a,1,2)),demod(64(3)),flip(a)]. given #319 (T,wt=15): 3312 x ^ (y ^ (z v ((u v y) ^ x))) = x ^ y. [para(320(a,1),126(a,1,2)),demod(64(3)),flip(a)]. given #320 (T,wt=15): 3513 x v (y v (((z ^ y) v x) ^ u)) = x v y. [para(152(a,1),133(a,1,2)),demod(57(3)),flip(a)]. given #321 (A,wt=17): 169 (x v y) ^ (z ^ (x v (u v y))) = z ^ (x v y). [para(17(a,1),64(a,1,2,2))]. given #322 (F,wt=15): 3516 x v (y v (z ^ ((u ^ y) v x))) = x v y. [para(211(a,1),133(a,1,2)),demod(57(3)),flip(a)]. given #323 (F,wt=15): 3644 x ^ ((y ^ (z ^ u)) v (z ^ x)) = x ^ z. [para(18(a,1),3605(a,1,2,1))]. given #324 (T,wt=15): 3646 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(3605(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #325 (T,wt=15): 3649 x ^ ((y ^ z) v (y ^ (u v x))) = x ^ y. [para(3605(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #326 (A,wt=17): 171 (x ^ (y v z)) v (u ^ (x ^ z)) = x ^ (y v z). [para(64(a,1),56(a,1,2,2))]. given #327 (F,wt=15): 3667 x ^ ((y ^ (z ^ u)) v (u ^ x)) = x ^ u. [para(61(a,1),3605(a,1,2,1))]. given #328 (F,wt=15): 3731 x ^ ((y ^ x) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),3637(a,1,2,2))]. given #329 (T,wt=15): 3732 x ^ ((y ^ (x v z)) v (y ^ u)) = x ^ y. [para(3637(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #330 (T,wt=15): 3733 x ^ ((y ^ (z v x)) v (y ^ u)) = x ^ y. [para(3637(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #331 (A,wt=19): 175 (x ^ y) v ((x ^ (z v y)) v u) = (x ^ (z v y)) v u. [para(64(a,1),54(a,1,2,1)),demod(17(5))]. given #332 (F,wt=15): 3745 x ^ ((y ^ x) v (z ^ (u ^ y))) = x ^ y. [para(61(a,1),3637(a,1,2,2))]. given #333 (F,wt=15): 3858 x ^ (y v ((y v z) ^ x)) = x ^ (y v z). [para(13(a,1),3638(a,1,2,1))]. given #334 (T,wt=15): 3859 x ^ (y v ((z v y) ^ x)) = x ^ (z v y). [para(19(a,1),3638(a,1,2,1))]. given #335 (T,wt=15): 3866 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(3638(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #336 (A,wt=23): 179 (x v ((y v x) ^ z)) ^ (u ^ (y v x)) = u ^ (x v ((y v x) ^ z)). [para(24(a,1),64(a,1,2,2))]. given #337 (F,wt=15): 3871 x ^ ((y ^ z) v (z ^ (u v x))) = x ^ z. [para(3638(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #338 (F,wt=15): 3985 x ^ ((y ^ (z ^ u)) v (x ^ z)) = x ^ z. [para(18(a,1),3639(a,1,2,1))]. given #339 (T,wt=15): 3987 x ^ ((y ^ z) v ((x v u) ^ y)) = x ^ y. [para(3639(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #340 (T,wt=15): 3988 x ^ ((y ^ z) v ((u v x) ^ y)) = x ^ y. [para(3639(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #341 (A,wt=17): 180 (x v y) ^ (z v (u v (x v (y v v)))) = x v y. [para(10(a,1),71(a,1,2,2,2))]. given #342 (F,wt=15): 3996 x ^ ((y ^ (z ^ u)) v (x ^ u)) = x ^ u. [para(61(a,1),3639(a,1,2,1))]. given #343 (F,wt=15): 4029 x ^ ((x ^ y) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),3724(a,1,2,2))]. given #344 (T,wt=15): 4030 x ^ (((x v y) ^ z) v (z ^ u)) = x ^ z. [para(3724(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #345 (T,wt=15): 4031 x ^ (((y v x) ^ z) v (z ^ u)) = x ^ z. [para(3724(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #346 (A,wt=17): 183 x ^ (y ^ (z v (u v ((x ^ y) v v)))) = x ^ y. [para(71(a,1),12(a,1)),flip(a)]. given #347 (F,wt=15): 4039 x ^ ((x ^ y) v (z ^ (u ^ y))) = x ^ y. [para(61(a,1),3724(a,1,2,2))]. given #348 (F,wt=15): 4069 x ^ ((y ^ (x v z)) v (u ^ y)) = x ^ y. [para(3725(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #349 (T,wt=15): 4070 x ^ ((y ^ (z v x)) v (u ^ y)) = x ^ y. [para(3725(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #350 (T,wt=15): 4208 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(13(a,1),3854(a,1,2,1))]. given #351 (A,wt=17): 187 x ^ (y ^ (z v (u v (v v (x ^ y))))) = x ^ y. [para(75(a,1),12(a,1)),flip(a)]. given #352 (F,wt=15): 4209 x ^ (y v (x ^ (z v y))) = x ^ (z v y). [para(19(a,1),3854(a,1,2,1))]. given #353 (F,wt=15): 4216 x ^ ((y ^ z) v ((x v u) ^ z)) = x ^ z. [para(3854(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #354 (T,wt=15): 4219 x ^ ((y ^ z) v ((u v x) ^ z)) = x ^ z. [para(3854(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #355 (T,wt=15): 4296 x ^ (((x v y) ^ z) v (u ^ z)) = x ^ z. [para(4023(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #356 (A,wt=17): 188 (x v y) ^ (z v (u v (x v (v v y)))) = x v y. [para(17(a,1),75(a,1,2,2,2))]. given #357 (F,wt=15): 4297 x ^ (((y v x) ^ z) v (u ^ z)) = x ^ z. [para(4023(a,1),51(a,1,2)),demod(51(3)),flip(a)]. given #358 (F,wt=15): 4564 x v (((x ^ y) v (z ^ (u ^ x))) ^ v) = x. [para(158(a,1),88(a,1)),demod(56(3)),flip(a)]. given #359 (T,wt=15): 4566 x v (((x ^ y) v (z ^ (x ^ u))) ^ v) = x. [para(158(a,1),94(a,1)),demod(63(3)),flip(a)]. given #360 (T,wt=15): 4618 x v (((y ^ (x ^ z)) v (x ^ u)) ^ v) = x. [para(18(a,1),4545(a,1,2,1,1))]. given #361 (A,wt=17): 189 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(75(a,1),25(a,1,2)),demod(9(4))]. given #362 (F,wt=15): 4619 x v (y ^ (((x ^ z) v (x ^ u)) ^ v)) = x. [para(18(a,1),4545(a,1,2))]. given #363 (F,wt=15): 4633 x v (((y ^ (z ^ x)) v (x ^ u)) ^ v) = x. [para(61(a,1),4545(a,1,2,1,1))]. given #364 (T,wt=15): 4634 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(61(a,1),4545(a,1,2))]. given #365 (T,wt=15): 4680 x v (((y ^ (x ^ z)) v (u ^ x)) ^ v) = x. [para(18(a,1),4547(a,1,2,1,1))]. given #366 (A,wt=19): 191 ((x ^ y) v z) ^ (u v (v v (x v z))) = (x ^ y) v z. [para(23(a,1),75(a,1,2,2,2))]. given #367 (F,wt=15): 4682 x v (y ^ (((x ^ z) v (u ^ x)) ^ v)) = x. [para(18(a,1),4547(a,1,2))]. given #368 (F,wt=15): 4710 x v (((y ^ (z ^ x)) v (u ^ x)) ^ v) = x. [para(61(a,1),4547(a,1,2,1,1))]. given #369 (T,wt=15): 4711 x v (y ^ (z ^ ((x ^ u) v (v ^ x)))) = x. [para(61(a,1),4547(a,1,2))]. given #370 (T,wt=15): 4791 x v (((y ^ x) v (z ^ (x ^ u))) ^ v) = x. [para(18(a,1),4614(a,1,2,1,2))]. given #371 (A,wt=19): 192 (x v (y ^ z)) ^ (u v (v v (x v y))) = x v (y ^ z). [para(49(a,1),75(a,1,2,2,2))]. given #372 (F,wt=15): 4792 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(18(a,1),4614(a,1,2))]. given #373 (F,wt=15): 4806 x v (((y ^ x) v (z ^ (u ^ x))) ^ v) = x. [para(61(a,1),4614(a,1,2,1,2))]. given #374 (T,wt=15): 4807 x v (y ^ (z ^ ((u ^ x) v (x ^ v)))) = x. [para(61(a,1),4614(a,1,2))]. given #375 (T,wt=15): 4886 x v (y ^ ((z ^ y) v x)) = x v (z ^ y). [para(112(a,1),211(a,1,2))]. given #376 (A,wt=21): 193 x v (y v (z v (u v (x v v)))) = y v (z v (u v (x v v))). [para(75(a,1),54(a,1,2,1)),demod(17(5),10(4),10(3),10(2),10(9),10(8),10(7))]. given #377 (F,wt=15): 4934 x v (y ^ ((z ^ (x ^ u)) v (x ^ v))) = x. [para(18(a,1),4615(a,1,2,2,1))]. given #378 (F,wt=15): 4935 x v (y ^ ((x ^ z) v (u ^ (x ^ v)))) = x. [para(18(a,1),4615(a,1,2,2,2))]. given #379 (T,wt=15): 4947 x v (y ^ ((z ^ (u ^ x)) v (x ^ v))) = x. [para(61(a,1),4615(a,1,2,2,1))]. given #380 (T,wt=15): 4948 x v (y ^ ((x ^ z) v (u ^ (v ^ x)))) = x. [para(61(a,1),4615(a,1,2,2,2))]. given #381 (A,wt=19): 194 ((x ^ y) v z) ^ (u v (v v (y v z))) = (x ^ y) v z. [para(54(a,1),75(a,1,2,2,2))]. given #382 (F,wt=15): 4993 x v (y ^ (((z ^ x) v (u ^ x)) ^ v)) = x. [para(18(a,1),4674(a,1,2))]. given #383 (F,wt=15): 5022 x v (y ^ (z ^ ((u ^ x) v (v ^ x)))) = x. [para(61(a,1),4674(a,1,2))]. given #384 (T,wt=15): 5095 x v (y ^ ((z ^ (x ^ u)) v (v ^ x))) = x. [para(18(a,1),4675(a,1,2,2,1))]. given #385 (T,wt=15): 5124 x v (y ^ ((z ^ (u ^ x)) v (v ^ x))) = x. [para(61(a,1),4675(a,1,2,2,1))]. given #386 (A,wt=19): 195 (x v (y ^ z)) ^ (u v (v v (x v z))) = x v (y ^ z). [para(57(a,1),75(a,1,2,2,2))]. given #387 (F,wt=15): 5200 x v (y ^ ((z ^ x) v (u ^ (x ^ v)))) = x. [para(18(a,1),4786(a,1,2,2,2))]. given #388 (F,wt=15): 5215 x v (y ^ ((z ^ x) v (u ^ (v ^ x)))) = x. [para(61(a,1),4786(a,1,2,2,2))]. given #389 (T,wt=15): 5980 x v ((y v x) ^ (z v (y v u))) = x v y. [para(17(a,1),5892(a,1,2,2))]. given #390 (T,wt=15): 5981 x v ((y v (x ^ z)) ^ (y v u)) = x v y. [para(5892(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #391 (A,wt=23): 196 (x v ((y v x) ^ z)) ^ (u v (v v (y v x))) = x v ((y v x) ^ z). [para(24(a,1),75(a,1,2,2,2))]. given #392 (F,wt=15): 5984 x v ((y v (z ^ x)) ^ (y v u)) = x v y. [para(5892(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #393 (F,wt=15): 5994 x v ((y v x) ^ (z v (u v y))) = x v y. [para(69(a,1),5892(a,1,2,2))]. given #394 (T,wt=15): 6047 x v (y ^ ((y ^ z) v x)) = x v (y ^ z). [para(3605(a,1),5892(a,1,2)),demod(11(3))]. given #395 (T,wt=15): 6070 x v ((x v y) ^ (z v (y v u))) = x v y. [para(17(a,1),5972(a,1,2,2))]. given #396 (A,wt=19): 199 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(12(a,1),26(a,1,1)),demod(12(5),12(8))]. given #397 (F,wt=15): 6071 x v (((x ^ y) v z) ^ (z v u)) = x v z. [para(5972(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #398 (F,wt=15): 6072 x v (((y ^ x) v z) ^ (z v u)) = x v z. [para(5972(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #399 (T,wt=15): 6077 x v ((x v y) ^ (z v (u v y))) = x v y. [para(69(a,1),5972(a,1,2,2))]. given #400 (T,wt=15): 6094 x v (y ^ (x v (y ^ z))) = x v (y ^ z). [para(3605(a,1),5972(a,1,2)),demod(11(3))]. given #401 (A,wt=19): 201 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(18(a,1),26(a,1,1)),demod(12(4))]. given #402 (F,wt=15): 6096 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(3638(a,1),5972(a,1,2)),demod(11(3))]. given #403 (F,wt=15): 6208 x v ((y v (x ^ z)) ^ (u v y)) = x v y. [para(5973(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #404 (T,wt=15): 6212 x v ((y v (z ^ x)) ^ (u v y)) = x v y. [para(5973(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #405 (T,wt=15): 6326 x v ((y v (z v u)) ^ (z v x)) = x v z. [para(17(a,1),5977(a,1,2,1))]. given #406 (A,wt=19): 204 x ^ (y ^ (z ^ (u v (v v (x ^ y))))) = x ^ (y ^ z). [para(26(a,1),75(a,1,2,2,2)),demod(12(6),12(5))]. given #407 (F,wt=15): 6328 x v ((y v z) ^ (y v (x ^ u))) = x v y. [para(5977(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #408 (F,wt=15): 6330 x v ((y v z) ^ (y v (u ^ x))) = x v y. [para(5977(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #409 (T,wt=15): 6342 x v ((y v (z v u)) ^ (u v x)) = x v u. [para(69(a,1),5977(a,1,2,1))]. given #410 (T,wt=15): 6416 x v (((x ^ y) v z) ^ (u v z)) = x v z. [para(6064(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #411 (A,wt=17): 205 (x v (y v z)) ^ (z v (x v y)) = x v (y v z). [para(10(a,1),87(a,1,1)),demod(10(7))]. given #412 (F,wt=15): 6419 x v (((y ^ x) v z) ^ (u v z)) = x v z. [para(6064(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #413 (F,wt=15): 6485 x v ((y v (z v u)) ^ (x v z)) = x v z. [para(17(a,1),6068(a,1,2,1))]. given #414 (T,wt=15): 6487 x v ((y v z) ^ ((x ^ u) v y)) = x v y. [para(6068(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #415 (T,wt=15): 6488 x v ((y v z) ^ ((u ^ x) v y)) = x v y. [para(6068(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #416 (A,wt=17): 206 (x v (y v z)) ^ (y v (z v x)) = x v (y v z). [para(10(a,1),87(a,1,2))]. given #417 (F,wt=15): 6494 x v ((y v (z v u)) ^ (x v u)) = x v u. [para(69(a,1),6068(a,1,2,1))]. given #418 (F,wt=15): 6597 x v ((y v z) ^ (z v (x ^ u))) = x v z. [para(6202(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #419 (T,wt=15): 6599 x v ((y v z) ^ (z v (u ^ x))) = x v z. [para(6202(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #420 (T,wt=15): 6686 x v ((y v z) ^ ((x ^ u) v z)) = x v z. [para(6410(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #421 (A,wt=17): 209 (x v (y v z)) ^ (x v (z v y)) = x v (y v z). [para(17(a,1),87(a,1,2)),demod(10(2),10(7))]. given #422 (F,wt=15): 6687 x v ((y v z) ^ ((u ^ x) v z)) = x v z. [para(6410(a,1),54(a,1,2)),demod(54(3)),flip(a)]. given #423 (F,wt=17): 213 x v (y v (z ^ (u ^ (v ^ (x v y))))) = x v y. [para(90(a,1),10(a,1)),flip(a)]. given #424 (T,wt=17): 216 x ^ (y ^ (z ^ (u ^ x))) = y ^ (z ^ (u ^ x)). [para(90(a,1),19(a,1,2)),demod(11(4))]. given #425 (T,wt=17): 217 (x ^ y) v (z ^ (u ^ (x ^ (v ^ y)))) = x ^ y. [para(18(a,1),90(a,1,2,2,2))]. given #426 (A,wt=19): 218 x v (y v (z v (u ^ (v ^ (x v y))))) = x v (y v z). [para(20(a,1),90(a,1,2,2,2)),demod(10(6),10(5))]. given #427 (F,wt=17): 228 x v (y v (z ^ (u ^ ((x v y) ^ v)))) = x v y. [para(97(a,1),10(a,1)),flip(a)]. given #428 (F,wt=17): 229 (x ^ y) v (z ^ (u ^ (x ^ (y ^ v)))) = x ^ y. [para(12(a,1),97(a,1,2,2,2))]. given #429 (T,wt=17): 231 (x v (y v z)) ^ (u ^ (x v y)) = u ^ (x v y). [para(10(a,1),101(a,1,1))]. given #430 (T,wt=17): 236 x ^ (y ^ ((y ^ ((x ^ y) v z)) v u)) = x ^ y. [para(22(a,1),101(a,1,2)),demod(11(6),12(6),22(10))]. given #431 (A,wt=19): 219 ((x v y) ^ z) v (u ^ (v ^ (x ^ z))) = (x v y) ^ z. [para(21(a,1),90(a,1,2,2,2))]. given #432 (F,wt=17): 239 (x ^ (y v z)) v (x ^ (u ^ y)) = x ^ (y v z). [para(101(a,1),26(a,1,2,2))]. given #433 (F,wt=17): 269 (x ^ (y ^ z)) v (u v (x ^ y)) = u v (x ^ y). [para(12(a,1),108(a,1,1))]. given #434 (T,wt=17): 272 (x v (y ^ z)) ^ (x v (u v y)) = x v (y ^ z). [para(108(a,1),20(a,1,2,2))]. given #435 (T,wt=17): 276 x v (y v ((y v ((x v y) ^ z)) ^ u)) = x v y. [para(24(a,1),108(a,1,2)),demod(9(6),10(6),24(10))]. given #436 (A,wt=23): 221 (x ^ ((y ^ x) v z)) v (u ^ (v ^ (y ^ x))) = x ^ ((y ^ x) v z). [para(22(a,1),90(a,1,2,2,2))]. given #437 (F,wt=17): 281 (x v (y v z)) ^ (u ^ (x v z)) = u ^ (x v z). [para(17(a,1),125(a,1,1))]. given #438 (F,wt=17): 292 (x ^ (y v z)) v (x ^ (u ^ z)) = x ^ (y v z). [para(125(a,1),26(a,1,2,2))]. given #439 (T,wt=17): 300 (x ^ (y ^ z)) v (u v (x ^ z)) = u v (x ^ z). [para(18(a,1),136(a,1,1))]. given #440 (T,wt=17): 301 (x v (y ^ z)) ^ (x v (u v z)) = x v (y ^ z). [para(136(a,1),20(a,1,2,2))]. given #441 (A,wt=21): 222 x ^ (y ^ (z ^ (u ^ (x ^ v)))) = y ^ (z ^ (u ^ (x ^ v))). [para(90(a,1),51(a,1,2,1)),demod(18(5),12(4),12(3),12(2),12(9),12(8),12(7))]. given #442 (F,wt=17): 310 x v (y v (z ^ (y v ((x v y) ^ u)))) = x v y. [para(24(a,1),136(a,1,2)),demod(9(6),10(6),24(10))]. given #443 (F,wt=17): 317 (x ^ (y ^ z)) v (z ^ (x ^ y)) = x ^ (y ^ z). [para(12(a,1),200(a,1,1)),demod(12(7))]. given #444 (T,wt=17): 318 (x ^ (y ^ z)) v (y ^ (z ^ x)) = x ^ (y ^ z). [para(12(a,1),200(a,1,2))]. given #445 (T,wt=17): 319 (x ^ (y ^ z)) v (x ^ (z ^ y)) = y ^ (x ^ z). [para(18(a,1),200(a,1,1)),demod(12(4))]. given #446 (A,wt=19): 223 ((x v y) ^ z) v (u ^ (v ^ (y ^ z))) = (x v y) ^ z. [para(51(a,1),90(a,1,2,2,2))]. given #447 (F,wt=17): 380 x ^ (y ^ ((x ^ (z v (y ^ x))) v u)) = x ^ y. [para(30(a,2),64(a,1,2)),demod(18(8),12(7),102(8),62(9))]. given #448 (F,wt=17): 416 x ^ (y ^ (z ^ (u v (x ^ z)))) = y ^ (x ^ z). [para(52(a,1),18(a,1,2)),flip(a)]. given #449 (T,wt=17): 423 x ^ (y ^ ((y ^ (z v (x ^ y))) v u)) = x ^ y. [para(52(a,1),101(a,1,2)),demod(11(6),12(6),52(10))]. given #450 (T,wt=17): 434 x v (y v (z v (u ^ (x v z)))) = x v (y v z). [para(53(a,1),56(a,1,2,2)),demod(10(5),10(4))]. given #451 (A,wt=19): 224 (x ^ (y v z)) v (u ^ (v ^ (x ^ y))) = x ^ (y v z). [para(62(a,1),90(a,1,2,2,2))]. given #452 (F,wt=17): 447 (x v (y ^ z)) ^ (x v (z ^ y)) = x v (y ^ z). [para(200(a,1),53(a,1,2,2))]. given #453 (F,wt=17): 456 x v (y v ((y v (z ^ (x v y))) ^ u)) = x v y. [para(55(a,1),108(a,1,2)),demod(9(6),10(6),55(10))]. given #454 (T,wt=17): 458 x v (y v (z ^ (y v (u ^ (x v y))))) = x v y. [para(55(a,1),136(a,1,2)),demod(9(6),10(6),55(10))]. given #455 (T,wt=17): 526 (x ^ (y v z)) v (x ^ (z v y)) = x ^ (y v z). [para(87(a,1),65(a,1,2,2))]. given #456 (A,wt=19): 225 (x ^ (y v z)) v (u ^ (v ^ (x ^ z))) = x ^ (y v z). [para(64(a,1),90(a,1,2,2,2))]. given #457 (F,wt=17): 691 x ^ (y ^ ((z v (x v u)) ^ v)) = y ^ (x ^ v). [para(72(a,1),18(a,1,2)),flip(a)]. given #458 (F,wt=17): 693 x ^ (y ^ (((z v (x v u)) ^ y) v v)) = x ^ y. [para(22(a,1),72(a,1,2)),demod(72(4)),flip(a)]. given #459 (T,wt=17): 701 x ^ (y ^ ((z v (u v x)) ^ v)) = x ^ (y ^ v). [para(108(a,1),72(a,1,2,1,2)),demod(12(5),12(7))]. given #460 (T,wt=17): 702 x ^ (y ^ (z v ((u v (x v v)) ^ y))) = x ^ y. [para(72(a,1),125(a,1,2)),demod(11(6),12(6),72(10))]. given #461 (A,wt=21): 242 x ^ ((y ^ ((x ^ y) v z)) v u) = x ^ (u v (y ^ (x v z))). [para(9(a,1),29(a,1,2))]. ============================== PROOF ================================= % Proof 1 at 14.30 (+ 0.11) seconds: H3. % Length of proof is 39. % Level of proof is 9. % Maximum clause weight is 23. % Given clauses 461. 7 x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (u v (x ^ z)))) # label(H39). [input]. 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 (z ^ (u v (x ^ z)))) = x ^ (y v (z ^ (x v u))) # label(H39). [copy(7),flip(a)]. 16 c1 ^ (c2 v (c3 ^ (c2 v (c1 ^ (c3 v (c1 ^ c2)))))) != c1 ^ (c2 v (c1 ^ c3)) # answer(H3). [clausify]. 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))]. 20 (x v y) ^ (x v (y v z)) = x v y. [para(10(a,1),13(a,1,2))]. 21 x ^ ((x v y) ^ z) = x ^ z. [para(13(a,1),12(a,1,1)),flip(a)]. 23 x v ((x ^ y) v z) = x v z. [para(14(a,1),10(a,1,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))]. 29 x ^ (y v (z ^ ((x ^ z) v u))) = x ^ (y v (z ^ (x v u))). [para(9(a,1),15(a,1,2,2,2))]. 44 x ^ (y ^ x) = y ^ x. [para(27(a,1),12(a,2,2)),demod(11(2))]. 54 x v ((y ^ x) v z) = x v z. [para(25(a,1),10(a,1,1)),flip(a)]. 64 x ^ (y ^ (z v x)) = y ^ x. [para(19(a,1),18(a,1,2)),flip(a)]. 80 (x v y) ^ (y v (x v z)) = y v x. [para(9(a,1),20(a,1,1))]. 100 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(21(a,1),25(a,1,2)),demod(9(4))]. 107 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(23(a,1),19(a,1,2)),demod(11(4))]. 134 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(54(a,1),19(a,1,2)),demod(11(4))]. 170 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(64(a,1),25(a,1,2)),demod(9(4))]. 200 (x ^ y) v (y ^ x) = x ^ y. [para(44(a,1),26(a,1,2))]. 242 x ^ ((y ^ ((x ^ y) v z)) v u) = x ^ (u v (y ^ (x v z))). [para(9(a,1),29(a,1,2))]. 316 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(200(a,1),10(a,2,2)),demod(9(4))]. 321 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(200(a,1),23(a,2)),demod(12(3),316(6))]. 2174 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(13(a,1),100(a,1,1))]. 2344 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(14(a,1),107(a,1,1))]. 3605 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(321(a,1),134(a,1,2)),demod(11(5),12(5),2344(4),321(8))]. 3638 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(11(a,1),3605(a,1,2,1))]. 5892 x v ((y v x) ^ (y v z)) = x v y. [para(80(a,1),170(a,1,2)),demod(17(5),9(4),2174(4),80(8))]. 5972 x v ((x v y) ^ (y v z)) = x v y. [para(9(a,1),5892(a,1,2,1))]. 6096 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(3638(a,1),5972(a,1,2)),demod(11(3))]. 12709 $F # answer(H3). [para(242(a,2),16(a,1,2,2)),demod(11(7),9(11),2344(12),9(12),54(12),6096(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=461. Generated=401184. Kept=12700. proofs=1. Usable=457. Sos=9996. Demods=9658. Denials=0. Limbo=0, Disabled=2255. Hints=0. Weight_deleted=14. Literals_deleted=0. Forward_subsumed=311450. Back_subsumed=234. Sos_limit_deleted=77019. Sos_displaced=1346. Sos_removed=0. New_demodulators=11460 (4 lex), Back_demodulated=667. Back_unit_deleted=0. Demod_attempts=6379765. Demod_rewrites=1024772. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=12.48. User_CPU=14.30, System_CPU=0.11, Wall_clock=15. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 13805 exit (max_proofs) Mon Jun 19 16:51:41 2006