============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13995 was started by mccune on cleo.thornwood, Mon Jun 19 17:19:35 2006 The command was "/home/mccune/bin/prover9 -t 7200 -f LT.in". ============================== 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. % From the command line: assign(max_seconds, 7200). ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal clause was negated; the result (to be placed in sos): clauses(negated_goals). c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # 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 c1 ^ (c2 v (c3 ^ ((c1 ^ (c2 v c3)) v (c2 ^ c3)))) != c1 ^ (c2 v (c1 ^ c3)) # 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([ 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 (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y))) # label(H82). [input]. 16 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # 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). [input]. given #8 (I,wt=23): 16 c1 ^ (c2 v (c3 ^ ((c2 ^ c3) v (c1 ^ (c2 v c3))))) != c1 ^ (c2 v (c1 ^ c3)) # label(H2). [copy(8),demod(9(12))]. given #9 (F,wt=5): 27 x ^ x = x. [para(14(a,1),13(a,1,2))]. given #10 (F,wt=5): 28 x v x = x. [para(13(a,1),14(a,1,2))]. given #11 (F,wt=7): 19 x ^ (y v x) = x. [para(9(a,1),13(a,1,2))]. given #12 (T,wt=7): 25 x v (y ^ x) = x. [para(11(a,1),14(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=9): 37 x ^ (x ^ y) = x ^ y. [para(27(a,1),12(a,1,1)),flip(a)]. given #15 (F,wt=9): 39 x ^ (y ^ x) = y ^ x. [para(27(a,1),12(a,2,2)),demod(11(2))]. given #16 (F,wt=9): 42 x v (x v y) = x v y. [para(28(a,1),10(a,1,1)),flip(a)]. given #17 (F,wt=9): 44 x v (y v x) = y v x. [para(28(a,1),10(a,2,2)),demod(9(2))]. given #18 (T,wt=9): 45 x ^ (y v (z v x)) = x. [para(10(a,1),19(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=9): 50 x v (y ^ (z ^ x)) = x. [para(12(a,1),25(a,1,2))]. given #21 (F,wt=9): 51 x ^ (y v (x v z)) = x. [para(17(a,1),13(a,1,2))]. given #22 (F,wt=9): 69 x v (y ^ (x ^ z)) = x. [para(18(a,1),14(a,1,2))]. given #23 (F,wt=11): 21 x ^ ((x v y) ^ z) = x ^ z. [para(13(a,1),12(a,1,1)),flip(a)]. given #24 (T,wt=11): 23 x v ((x ^ y) v z) = x v z. [para(14(a,1),10(a,1,1)),flip(a)]. 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=11): 46 x ^ ((y v x) ^ z) = x ^ z. [para(19(a,1),12(a,1,1)),flip(a)]. given #27 (F,wt=11): 48 x v ((y ^ x) v z) = x v z. [para(25(a,1),10(a,1,1)),flip(a)]. given #28 (F,wt=11): 52 x v (y v (x ^ z)) = y v x. [para(14(a,1),17(a,1,2)),flip(a)]. given #29 (F,wt=11): 54 x v (y v (z ^ x)) = y v x. [para(25(a,1),17(a,1,2)),flip(a)]. given #30 (T,wt=11): 63 x ^ (y v (z v (u v x))) = x. [para(10(a,1),45(a,1,2,2))]. given #31 (A,wt=13): 22 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(13(a,1),12(a,1)),flip(a)]. given #32 (F,wt=11): 66 x ^ (y ^ (z v x)) = x ^ y. [para(14(a,1),45(a,1,2,2)),demod(12(3))]. given #33 (F,wt=11): 68 x ^ (y ^ (x v z)) = y ^ x. [para(13(a,1),18(a,1,2)),flip(a)]. given #34 (F,wt=11): 76 x v (y ^ (z ^ (u ^ x))) = x. [para(12(a,1),50(a,1,2,2))]. given #35 (F,wt=11): 80 x ^ (y v (z v (x v u))) = x. [para(10(a,1),51(a,1,2))]. given #36 (T,wt=11): 87 x v (y ^ (z ^ (x ^ u))) = x. [para(12(a,1),69(a,1,2))]. given #37 (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 #38 (F,wt=11): 92 (x v y) ^ (z ^ x) = z ^ x. [para(39(a,1),21(a,2)),demod(58(4))]. given #39 (F,wt=11): 99 (x ^ y) v (z v x) = z v x. [para(44(a,1),23(a,2)),demod(62(4))]. given #40 (F,wt=11): 106 (x v y) ^ (y v x) = x v y. [para(44(a,1),20(a,1,2))]. given #41 (F,wt=11): 112 (x v y) ^ (z ^ y) = z ^ y. [para(39(a,1),46(a,2)),demod(58(4))]. given #42 (T,wt=11): 120 (x ^ y) v (z v y) = z v y. [para(44(a,1),48(a,2)),demod(62(4))]. given #43 (A,wt=13): 26 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(12(a,1),14(a,1,2))]. given #44 (F,wt=11): 278 (x ^ y) v (y ^ x) = x ^ y. [para(39(a,1),26(a,1,2))]. given #45 (F,wt=13): 47 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(19(a,1),12(a,1)),flip(a)]. given #46 (F,wt=13): 49 x v (y v (z ^ (x v y))) = x v y. [para(25(a,1),10(a,1)),flip(a)]. given #47 (F,wt=13): 53 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),19(a,1,2))]. given #48 (T,wt=13): 56 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(37(a,1),12(a,2,2)),demod(18(3),12(2))]. given #49 (A,wt=21): 29 x ^ ((y ^ (x v z)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [para(15(a,1),9(a,1))]. given #50 (F,wt=13): 58 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(12(a,1),39(a,1,2)),demod(12(5))]. given #51 (F,wt=13): 60 x v (y v (x v z)) = y v (x v z). [para(42(a,1),10(a,2,2)),demod(17(3),10(2))]. given #52 (F,wt=13): 62 x v (y v (z v x)) = y v (z v x). [para(10(a,1),44(a,1,2)),demod(10(5))]. given #53 (F,wt=13): 64 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(45(a,1),12(a,1,1)),flip(a)]. given #54 (T,wt=13): 70 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(18(a,1),25(a,1,2))]. given #55 (A,wt=21): 32 x ^ (((x v y) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y). [para(11(a,1),15(a,2,2,1)),flip(a)]. given #56 (F,wt=13): 71 x ^ (y ^ (z v (u v x))) = y ^ x. [para(45(a,1),18(a,1,2)),flip(a)]. given #57 (F,wt=13): 74 x v ((y ^ (z ^ x)) v u) = x v u. [para(50(a,1),10(a,1,1)),flip(a)]. given #58 (F,wt=13): 77 x v (y v (z ^ (u ^ x))) = y v x. [para(50(a,1),17(a,1,2)),flip(a)]. given #59 (F,wt=13): 81 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(51(a,1),12(a,1,1)),flip(a)]. given #60 (T,wt=13): 83 x ^ (y ^ (z v (x v u))) = y ^ x. [para(51(a,1),18(a,1,2)),flip(a)]. given #61 (A,wt=15): 65 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(45(a,1),12(a,1)),flip(a)]. given #62 (F,wt=13): 84 x v ((y ^ (x ^ z)) v u) = x v u. [para(69(a,1),10(a,1,1)),flip(a)]. given #63 (F,wt=13): 88 x v (y v (z ^ (x ^ u))) = y v x. [para(69(a,1),17(a,1,2)),flip(a)]. given #64 (F,wt=13): 101 (x v y) ^ (y v (x v z)) = y v x. [para(9(a,1),20(a,1,1))]. given #65 (F,wt=13): 102 (x v y) ^ (y v (z v x)) = x v y. [para(9(a,1),20(a,1,2)),demod(10(3))]. given #66 (T,wt=13): 141 x ^ (y v (z v (u v (v v x)))) = x. [para(10(a,1),63(a,1,2,2,2))]. given #67 (A,wt=15): 67 (x v y) ^ (z v (x v (u v y))) = x v y. [para(17(a,1),45(a,1,2,2))]. given #68 (F,wt=13): 147 x ^ (y v (z v (u v (x v v)))) = x. [para(63(a,1),21(a,1,2)),demod(13(2)),flip(a)]. given #69 (F,wt=13): 153 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(11(a,1),22(a,1,2,2,1))]. given #70 (F,wt=13): 182 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(12(a,1),76(a,1,2,2,2))]. given #71 (F,wt=13): 187 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(76(a,1),23(a,1,2)),demod(14(2)),flip(a)]. given #72 (T,wt=13): 202 x v (y v ((y v x) ^ z)) = x v y. [para(9(a,1),24(a,1,2,2,1))]. given #73 (A,wt=17): 72 (x ^ y) v (x ^ z) = x ^ ((y ^ x) v (z ^ x)). [back_demod(41),demod(68(7))]. given #74 (F,wt=13): 216 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),92(a,1,1))]. given #75 (F,wt=13): 225 (x ^ (y ^ z)) v (u v y) = u v y. [para(18(a,1),99(a,1,1))]. given #76 (F,wt=13): 239 x v (y v (z ^ (y v x))) = x v y. [para(106(a,1),50(a,1,2,2)),demod(10(4))]. given #77 (F,wt=13): 241 (x v (y v z)) ^ (y v x) = y v x. [para(106(a,1),92(a,1,2)),demod(10(2),106(7))]. given #78 (T,wt=13): 242 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(10(a,1),112(a,1,1))]. given #79 (A,wt=17): 73 (x ^ y) v (x ^ z) = x ^ ((z ^ x) v (y ^ x)). [back_demod(40),demod(68(7))]. given #80 (F,wt=13): 258 (x v (y v z)) ^ (z v y) = z v y. [para(106(a,1),112(a,1,2)),demod(106(7))]. given #81 (F,wt=13): 259 (x ^ (y ^ z)) v (u v z) = u v z. [para(12(a,1),120(a,1,1))]. given #82 (F,wt=13): 275 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(11(a,1),26(a,1,1))]. given #83 (F,wt=13): 276 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(11(a,1),26(a,1,2)),demod(12(3))]. given #84 (T,wt=13): 290 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(278(a,1),45(a,1,2,2)),demod(12(4))]. given #85 (A,wt=15): 75 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(50(a,1),10(a,1)),flip(a)]. given #86 (F,wt=13): 292 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(278(a,1),23(a,2)),demod(12(3),287(6))]. given #87 (F,wt=13): 294 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(278(a,1),120(a,1,2)),demod(278(7))]. given #88 (F,wt=13): 317 (x v y) ^ (z v (y v x)) = x v y. [para(9(a,1),53(a,1,2)),demod(10(3))]. given #89 (F,wt=13): 352 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(29(a,1),69(a,1,2,2))]. given #90 (T,wt=13): 359 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(29(a,1),66(a,1,2)),demod(12(6),355(5),11(7),68(7))]. given #91 (A,wt=15): 78 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(18(a,1),50(a,1,2,2))]. given #92 (F,wt=13): 360 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(29(a,1),68(a,1,2)),demod(12(6),355(5),68(7))]. given #93 (F,wt=13): 410 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(11(a,1),70(a,1,2)),demod(12(3))]. given #94 (F,wt=13): 624 (x v (y v z)) ^ (z v x) = z v x. [para(102(a,1),11(a,1)),flip(a)]. given #95 (F,wt=13): 1076 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(276(a,1),9(a,1)),flip(a)]. given #96 (T,wt=13): 1198 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(11(a,1),352(a,1,2,2,1))]. given #97 (A,wt=15): 79 (x v y) ^ (z v (x v (y v u))) = x v y. [para(10(a,1),51(a,1,2,2))]. given #98 (F,wt=13): 1199 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(11(a,1),352(a,1,2,2,2))]. given #99 (F,wt=13): 1200 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(11(a,1),352(a,1,2))]. given #100 (F,wt=13): 1227 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(11(a,1),359(a,1,2,1))]. given #101 (F,wt=13): 1228 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(11(a,1),359(a,1,2,2))]. given #102 (T,wt=13): 1295 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(11(a,1),360(a,1,2,1))]. given #103 (A,wt=15): 82 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(51(a,1),12(a,1)),flip(a)]. given #104 (F,wt=13): 1296 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(11(a,1),360(a,1,2,2))]. given #105 (F,wt=13): 1397 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(11(a,1),1198(a,1,2,2,2))]. given #106 (F,wt=13): 1398 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(11(a,1),1198(a,1,2))]. given #107 (F,wt=13): 1462 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(11(a,1),1199(a,1,2))]. given #108 (T,wt=13): 1520 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(11(a,1),1227(a,1,2,2))]. given #109 (A,wt=15): 85 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(69(a,1),10(a,1)),flip(a)]. given #110 (F,wt=13): 1602 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(11(a,1),1295(a,1,2,2))]. given #111 (F,wt=13): 1672 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(11(a,1),1397(a,1,2))]. given #112 (F,wt=15): 86 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(12(a,1),69(a,1,2,2))]. given #113 (F,wt=15): 91 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(21(a,1),25(a,1,2)),demod(9(4))]. given #114 (T,wt=15): 93 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(21(a,1),18(a,1,2)),flip(a)]. given #115 (A,wt=17): 89 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(10(a,1),21(a,1,2,1))]. given #116 (F,wt=15): 97 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(23(a,1),19(a,1,2)),demod(11(4))]. given #117 (F,wt=15): 98 x v (y v ((x ^ z) v u)) = y v (x v u). [para(23(a,1),17(a,1,2)),flip(a)]. given #118 (F,wt=15): 105 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),20(a,1,2,2))]. given #119 (F,wt=15): 110 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(46(a,1),25(a,1,2)),demod(9(4))]. given #120 (T,wt=15): 113 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(46(a,1),18(a,1,2)),flip(a)]. given #121 (A,wt=17): 90 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(21(a,1),12(a,1)),demod(12(2)),flip(a)]. given #122 (F,wt=15): 118 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(48(a,1),19(a,1,2)),demod(11(4))]. given #123 (F,wt=15): 119 x v (y v ((z ^ x) v u)) = y v (x v u). [para(48(a,1),17(a,1,2)),flip(a)]. given #124 (F,wt=15): 128 x v (y v (z v (x ^ u))) = y v (z v x). [para(10(a,1),52(a,1,2)),demod(10(6))]. given #125 (F,wt=15): 130 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(52(a,1),19(a,1,2)),demod(11(4))]. given #126 (T,wt=15): 133 x v (y v (z v (u ^ x))) = y v (z v x). [para(10(a,1),54(a,1,2)),demod(10(6))]. given #127 (A,wt=17): 94 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(21(a,1),50(a,1,2,2))]. given #128 (F,wt=15): 134 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(54(a,1),19(a,1,2)),demod(11(4))]. given #129 (F,wt=15): 142 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(63(a,1),12(a,1,1)),flip(a)]. given #130 (F,wt=15): 146 x ^ (y ^ (z v (u v (v v x)))) = y ^ x. [para(63(a,1),18(a,1,2)),flip(a)]. given #131 (F,wt=15): 159 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(22(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #132 (T,wt=13): 2576 x ^ (((x v y) ^ (x v z)) v u) = x. [para(159(a,1),21(a,1)),demod(13(2)),flip(a)]. given #133 (A,wt=17): 95 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 #134 (F,wt=13): 2577 x ^ (((x v y) ^ (z v x)) v u) = x. [para(159(a,1),46(a,1)),demod(19(2)),flip(a)]. given #135 (F,wt=13): 2619 x ^ (((y v x) ^ (x v z)) v u) = x. [para(9(a,1),2576(a,1,2,1,1))]. given #136 (F,wt=13): 2620 x ^ (y v ((x v z) ^ (x v u))) = x. [para(9(a,1),2576(a,1,2))]. given #137 (F,wt=13): 2713 x ^ (((y v x) ^ (z v x)) v u) = x. [para(9(a,1),2577(a,1,2,1,1))]. given #138 (T,wt=13): 2714 x ^ (y v ((x v z) ^ (u v x))) = x. [para(9(a,1),2577(a,1,2))]. given #139 (A,wt=17): 96 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(12(a,1),23(a,1,2,1))]. given #140 (F,wt=13): 2756 x ^ (y v ((z v x) ^ (x v u))) = x. [para(9(a,1),2619(a,1,2))]. given #141 (F,wt=13): 2823 x ^ (y v ((z v x) ^ (u v x))) = x. [para(9(a,1),2713(a,1,2))]. given #142 (F,wt=15): 160 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(22(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #143 (F,wt=15): 164 x ^ (y ^ (z ^ (u v x))) = x ^ (y ^ z). [para(12(a,1),66(a,1,2))]. given #144 (T,wt=15): 165 (x ^ (y v z)) v (z ^ x) = x ^ (y v z). [para(66(a,1),25(a,1,2))]. given #145 (A,wt=17): 100 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(23(a,1),45(a,1,2,2))]. given #146 (F,wt=13): 3119 x v ((y v z) ^ (y v x)) = x v y. [para(101(a,1),165(a,1,1)),demod(10(5),1879(4),101(8))]. given #147 (F,wt=13): 3208 x v ((y v z) ^ (z v x)) = x v z. [para(9(a,1),3119(a,1,2,1))]. given #148 (F,wt=13): 3209 x v ((y v z) ^ (x v y)) = x v y. [para(9(a,1),3119(a,1,2,2))]. given #149 (F,wt=13): 3213 x v ((y v x) ^ (y v z)) = x v y. [para(11(a,1),3119(a,1,2))]. given #150 (T,wt=13): 3279 x v ((y v z) ^ (x v z)) = x v z. [para(9(a,1),3208(a,1,2,2))]. given #151 (A,wt=19): 103 (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 #152 (F,wt=13): 3283 x v ((y v x) ^ (z v y)) = x v y. [para(11(a,1),3208(a,1,2))]. given #153 (F,wt=13): 3373 x v ((x v y) ^ (y v z)) = x v y. [para(11(a,1),3209(a,1,2))]. given #154 (F,wt=13): 3455 x v ((x v y) ^ (z v y)) = x v y. [para(11(a,1),3279(a,1,2))]. given #155 (F,wt=15): 175 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(12(a,1),68(a,1,2)),demod(12(6))]. given #156 (T,wt=15): 176 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(68(a,1),25(a,1,2)),demod(9(4))]. given #157 (A,wt=19): 104 (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 #158 (F,wt=15): 180 x v ((y ^ (z ^ (u ^ x))) v v) = x v v. [para(76(a,1),10(a,1,1)),flip(a)]. given #159 (F,wt=15): 184 x v (y v (z ^ (u ^ (v ^ x)))) = y v x. [para(76(a,1),17(a,1,2)),flip(a)]. given #160 (F,wt=15): 195 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(80(a,1),12(a,1,1)),flip(a)]. given #161 (F,wt=15): 197 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(80(a,1),18(a,1,2)),flip(a)]. given #162 (T,wt=15): 198 x v ((y ^ (z ^ (x ^ u))) v v) = x v v. [para(87(a,1),10(a,1,1)),flip(a)]. given #163 (A,wt=17): 107 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(20(a,1),18(a,1,2)),flip(a)]. given #164 (F,wt=15): 201 x v (y v (z ^ (u ^ (x ^ v)))) = y v x. [para(87(a,1),17(a,1,2)),flip(a)]. given #165 (F,wt=15): 208 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 #166 (F,wt=15): 210 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(24(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #167 (F,wt=15): 214 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(92(a,1),12(a,1,1)),demod(12(2),12(5)),flip(a)]. given #168 (T,wt=15): 215 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(12(a,1),92(a,1,2)),demod(12(6))]. given #169 (A,wt=17): 108 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(20(a,1),50(a,1,2,2)),demod(10(5),10(4))]. given #170 (F,wt=15): 219 x ^ (y ^ ((y ^ (z v x)) v u)) = x ^ y. [para(66(a,1),92(a,1,2)),demod(11(5),12(5),66(8))]. given #171 (F,wt=15): 220 x ^ (y ^ ((x ^ (y v z)) v u)) = x ^ y. [para(68(a,1),92(a,1,2)),demod(11(5),12(5),68(8))]. given #172 (F,wt=15): 221 (x ^ y) v (z v (x v u)) = z v (x v u). [para(99(a,1),10(a,1,1)),demod(10(2),10(5)),flip(a)]. given #173 (F,wt=15): 222 (x ^ y) v (z v (u v x)) = z v (u v x). [para(10(a,1),99(a,1,2)),demod(10(6))]. given #174 (T,wt=15): 227 ((x ^ y) v z) ^ (z v x) = (x ^ y) v z. [para(99(a,1),20(a,1,2))]. given #175 (A,wt=17): 109 x ^ (y ^ ((z v (x ^ y)) ^ u)) = x ^ (y ^ u). [para(46(a,1),12(a,1)),demod(12(2)),flip(a)]. given #176 (F,wt=15): 228 x v (y v ((x v (y ^ z)) ^ u)) = x v y. [para(52(a,1),99(a,1,2)),demod(9(5),10(5),52(8))]. given #177 (F,wt=15): 229 x v (y v ((x v (z ^ y)) ^ u)) = x v y. [para(54(a,1),99(a,1,2)),demod(9(5),10(5),54(8))]. given #178 (F,wt=15): 231 (x v y) ^ (z ^ (y ^ u)) = z ^ (y ^ u). [para(99(a,1),92(a,1,1))]. given #179 (F,wt=15): 232 (x ^ y) v (z v (y v u)) = z v (y v u). [para(92(a,1),99(a,1,1))]. given #180 (T,wt=15): 235 (x v y) ^ ((y v x) ^ z) = (x v y) ^ z. [para(106(a,1),12(a,1,1)),flip(a)]. given #181 (A,wt=17): 111 (x v y) ^ ((x v (z v y)) ^ u) = (x v y) ^ u. [para(17(a,1),46(a,1,2,1))]. given #182 (F,wt=15): 240 x v (y v (z ^ (u ^ (y v x)))) = x v y. [para(106(a,1),76(a,1,2,2,2)),demod(10(5))]. given #183 (F,wt=15): 243 (x v y) ^ (z ^ (u ^ y)) = z ^ (u ^ y). [para(12(a,1),112(a,1,2)),demod(12(6))]. given #184 (F,wt=15): 246 x ^ (y ^ (z v ((x v u) ^ y))) = x ^ y. [para(21(a,1),112(a,1,2)),demod(11(5),12(5),21(8))]. given #185 (F,wt=15): 248 x ^ (y ^ (z v ((u v x) ^ y))) = x ^ y. [para(46(a,1),112(a,1,2)),demod(11(5),12(5),46(8))]. given #186 (T,wt=15): 253 x ^ (y ^ (z v (y ^ (u v x)))) = x ^ y. [para(66(a,1),112(a,1,2)),demod(11(5),12(5),66(8))]. given #187 (A,wt=17): 114 ((x v y) ^ z) v (u ^ (y ^ z)) = (x v y) ^ z. [para(46(a,1),50(a,1,2,2))]. given #188 (F,wt=15): 254 x ^ (y ^ (z v (x ^ (y v u)))) = x ^ y. [para(68(a,1),112(a,1,2)),demod(11(5),12(5),68(8))]. given #189 (F,wt=15): 257 (x ^ y) v (z v (u v y)) = z v (u v y). [para(112(a,1),99(a,1,1))]. given #190 (F,wt=15): 263 x v (y v (z ^ ((x ^ u) v y))) = x v y. [para(23(a,1),120(a,1,2)),demod(9(5),10(5),23(8))]. given #191 (F,wt=15): 265 ((x ^ y) v z) ^ (z v y) = (x ^ y) v z. [para(120(a,1),20(a,1,2))]. given #192 (T,wt=15): 267 x v (y v (z ^ ((u ^ x) v y))) = x v y. [para(48(a,1),120(a,1,2)),demod(9(5),10(5),48(8))]. given #193 (A,wt=17): 115 x ^ (y ^ (z ^ (x ^ u))) = y ^ (z ^ (x ^ u)). [para(50(a,1),46(a,1,2,1)),demod(18(4),12(3),12(2),12(7),12(6))]. given #194 (F,wt=15): 268 x v (y v (z ^ (x v (y ^ u)))) = x v y. [para(52(a,1),120(a,1,2)),demod(9(5),10(5),52(8))]. given #195 (F,wt=15): 269 x v (y v (z ^ (x v (u ^ y)))) = x v y. [para(54(a,1),120(a,1,2)),demod(9(5),10(5),54(8))]. given #196 (F,wt=15): 280 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(18(a,1),26(a,1,2,2))]. given #197 (F,wt=15): 283 ((x v y) ^ z) v (z ^ x) = (x v y) ^ z. [para(92(a,1),26(a,1,2))]. given #198 (T,wt=15): 285 ((x v y) ^ z) v (z ^ y) = (x v y) ^ z. [para(112(a,1),26(a,1,2))]. given #199 (A,wt=19): 116 (x v y) ^ (((x ^ z) v y) ^ u) = ((x ^ z) v y) ^ u. [para(23(a,1),46(a,1,2,1)),demod(18(5))]. given #200 (F,wt=15): 286 (x ^ y) v ((y ^ x) v z) = (x ^ y) v z. [para(278(a,1),10(a,1,1)),flip(a)]. given #201 (F,wt=15): 287 (x ^ y) v (z v (y ^ x)) = z v (y ^ x). [para(278(a,1),10(a,2,2)),demod(9(4))]. given #202 (F,wt=15): 293 x ^ (y ^ (z v (u v (y ^ x)))) = x ^ y. [para(278(a,1),63(a,1,2,2,2)),demod(12(5))]. given #203 (F,wt=15): 319 (x v y) ^ (x v (z v (u v y))) = x v y. [para(10(a,1),53(a,1,2,2))]. given #204 (T,wt=15): 366 x v (y ^ (z ^ ((x ^ u) v (x ^ v)))) = x. [para(29(a,1),87(a,1,2,2,2))]. given #205 (A,wt=17): 117 x v (y v ((z ^ (x v y)) v u)) = x v (y v u). [para(48(a,1),10(a,1)),demod(10(2)),flip(a)]. given #206 (F,wt=15): 379 (x v (y v (z v u))) ^ (v ^ u) = v ^ u. [para(63(a,1),58(a,1,2,2)),demod(63(9))]. given #207 (F,wt=15): 380 (x v (y v (z v u))) ^ (v ^ z) = v ^ z. [para(80(a,1),58(a,1,2,2)),demod(80(9))]. given #208 (F,wt=15): 381 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(106(a,1),58(a,1,2,2)),demod(106(7))]. given #209 (F,wt=15): 382 (x ^ y) v (x ^ (z ^ (u ^ y))) = x ^ y. [para(58(a,1),26(a,1,2,2))]. given #210 (T,wt=15): 383 (x ^ (y ^ (z ^ u))) v (v v u) = v v u. [para(76(a,1),62(a,1,2,2)),demod(76(9))]. given #211 (A,wt=17): 121 ((x ^ y) v z) ^ (u v (y v z)) = (x ^ y) v z. [para(48(a,1),45(a,1,2,2))]. given #212 (F,wt=15): 384 (x ^ (y ^ (z ^ u))) v (v v z) = v v z. [para(87(a,1),62(a,1,2,2)),demod(87(9))]. given #213 (F,wt=15): 396 x ^ (y v (z v (u v (v v (w v x))))) = x. [para(63(a,1),64(a,1,2)),demod(45(3)),flip(a)]. given #214 (F,wt=15): 399 x ^ (y v (z v (u v (v v (x v w))))) = x. [para(80(a,1),64(a,1,2)),demod(45(3),10(3),10(2)),flip(a)]. given #215 (F,wt=15): 433 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [back_demod(345),demod(412(9))]. given #216 (T,wt=15): 492 x v (y ^ (z ^ (u ^ (v ^ (w ^ x))))) = x. [para(76(a,1),74(a,1,2)),demod(50(3)),flip(a)]. given #217 (A,wt=17): 122 x v (y v (z v (x v u))) = y v (z v (x v u)). [para(45(a,1),48(a,1,2,1)),demod(17(4),10(3),10(2),10(7),10(6))]. given #218 (F,wt=15): 493 x v (y ^ (z ^ (u ^ (v ^ (x ^ w))))) = x. [para(87(a,1),74(a,1,2)),demod(50(3),12(3),12(2)),flip(a)]. given #219 (F,wt=15): 541 (x v (y v (z v u))) ^ (z v y) = y v z. [para(106(a,1),81(a,2)),demod(10(3),381(7))]. given #220 (F,wt=15): 588 (x ^ (y ^ (z ^ u))) v (z ^ y) = y ^ z. [para(278(a,1),84(a,2)),demod(12(3),287(7))]. given #221 (F,wt=15): 616 (x v y) ^ (y v (z v (x v u))) = y v x. [para(17(a,1),101(a,1,2,2))]. given #222 (T,wt=15): 620 (x v y) ^ (y v (z v (u v x))) = y v x. [para(62(a,1),101(a,1,2,2))]. given #223 (A,wt=17): 123 (x ^ y) v ((x ^ (z ^ y)) v u) = (x ^ y) v u. [para(18(a,1),48(a,1,2,1))]. given #224 (F,wt=15): 640 (x v (y v (z v u))) ^ (z v x) = z v x. [para(102(a,1),92(a,1,2)),demod(10(3),10(2),102(9))]. given #225 (F,wt=15): 641 (x v (y v (z v u))) ^ (u v y) = u v y. [para(102(a,1),112(a,1,2)),demod(102(9))]. given #226 (F,wt=15): 679 (x v y) ^ (z v (y v (u v x))) = y v x. [para(9(a,1),67(a,1,1))]. given #227 (F,wt=15): 680 (x v y) ^ (z v (u v (y v x))) = x v y. [para(9(a,1),67(a,1,2,2)),demod(10(3))]. given #228 (T,wt=15): 714 x ^ (y ^ (z v ((y ^ x) v u))) = x ^ y. [para(17(a,1),153(a,1,2,2))]. given #229 (A,wt=19): 124 (x ^ y) v (((x v z) ^ y) v u) = ((x v z) ^ y) v u. [para(21(a,1),48(a,1,2,1)),demod(17(5))]. given #230 (F,wt=15): 718 x ^ (y ^ ((y ^ (x v z)) v u)) = x ^ y. [para(153(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #231 (F,wt=15): 770 x v (y v (z ^ ((y v x) ^ u))) = x v y. [para(18(a,1),202(a,1,2,2))]. given #232 (F,wt=15): 771 x v (y v ((y v (x ^ z)) ^ u)) = x v y. [para(202(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #233 (F,wt=15): 773 x v (y v ((y v (z ^ x)) ^ u)) = x v y. [para(202(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #234 (T,wt=15): 899 x v (y v (z ^ (y v (x ^ u)))) = x v y. [para(239(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #235 (A,wt=19): 125 (x v y) ^ (((z ^ x) v y) ^ u) = ((z ^ x) v y) ^ u. [para(48(a,1),46(a,1,2,1)),demod(18(5))]. given #236 (F,wt=15): 901 x v (y v (z ^ (y v (u ^ x)))) = x v y. [para(239(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #237 (F,wt=15): 916 x v (y ^ ((y ^ z) v x)) = x v (y ^ z). [para(72(a,1),239(a,1,2)),demod(11(4),713(5),37(4))]. given #238 (F,wt=15): 928 (x v (y v (z v u))) ^ (u v x) = u v x. [para(62(a,1),241(a,1,1,2))]. given #239 (F,wt=15): 949 (x v (y v (z v u))) ^ (u v z) = u v z. [para(106(a,1),242(a,1,2)),demod(106(8))]. given #240 (T,wt=15): 1007 (x v y) ^ (y v (x ^ z)) = y v (x ^ z). [para(23(a,1),258(a,1,1))]. given #241 (A,wt=19): 126 (x ^ y) v (((z v x) ^ y) v u) = ((z v x) ^ y) v u. [para(46(a,1),48(a,1,2,1)),demod(17(5))]. given #242 (F,wt=15): 1008 (x v y) ^ (y v (z ^ x)) = y v (z ^ x). [para(48(a,1),258(a,1,1))]. given #243 (F,wt=15): 1009 (x v y) ^ ((y ^ z) v x) = (y ^ z) v x. [para(52(a,1),258(a,1,1))]. given #244 (F,wt=15): 1010 (x v y) ^ ((z ^ y) v x) = (z ^ y) v x. [para(54(a,1),258(a,1,1))]. given #245 (F,wt=15): 1036 (x ^ (y ^ (z ^ u))) v (u ^ z) = u ^ z. [para(278(a,1),259(a,1,2)),demod(278(8))]. given #246 (T,wt=15): 1064 (x ^ y) v (y ^ (z ^ (x ^ u))) = y ^ x. [para(18(a,1),275(a,1,2,2))]. given #247 (A,wt=17): 127 x v (y v (z v ((x v y) ^ u))) = z v (x v y). [para(52(a,1),10(a,1)),flip(a)]. given #248 (F,wt=15): 1068 (x ^ y) v (y ^ (z ^ (u ^ x))) = y ^ x. [para(58(a,1),275(a,1,2,2))]. given #249 (F,wt=15): 1093 (x ^ (y ^ (z ^ u))) v (z ^ x) = z ^ x. [para(276(a,1),99(a,1,2)),demod(12(3),12(2),276(9))]. given #250 (F,wt=15): 1094 (x ^ (y ^ (z ^ u))) v (u ^ y) = u ^ y. [para(276(a,1),120(a,1,2)),demod(276(9))]. given #251 (F,wt=15): 1121 x ^ (y ^ (z v (y ^ (x v u)))) = x ^ y. [para(290(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #252 (T,wt=15): 1141 x v (y ^ (x v (y ^ z))) = x v (y ^ z). [back_demod(827),demod(1118(5),37(4))]. given #253 (A,wt=17): 129 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(12(a,1),52(a,1,2,2))]. given #254 (F,wt=15): 1161 (x ^ (y ^ (z ^ u))) v (u ^ x) = x ^ u. [para(58(a,1),292(a,1,1,2))]. given #255 (F,wt=15): 1173 (x ^ y) v (y ^ (x v z)) = y ^ (x v z). [para(21(a,1),294(a,1,1))]. given #256 (F,wt=15): 1175 (x ^ y) v (y ^ (z v x)) = y ^ (z v x). [para(46(a,1),294(a,1,1))]. given #257 (F,wt=15): 1176 (x ^ y) v ((y v z) ^ x) = (y v z) ^ x. [para(68(a,1),294(a,1,1))]. given #258 (T,wt=15): 1190 (x v (y ^ z)) ^ (y v x) = x v (y ^ z). [para(23(a,1),317(a,1,2))]. given #259 (A,wt=17): 131 (x v (y ^ z)) ^ (u v (x v y)) = x v (y ^ z). [para(52(a,1),45(a,1,2,2))]. given #260 (F,wt=15): 1191 (x v (y ^ z)) ^ (z v x) = x v (y ^ z). [para(48(a,1),317(a,1,2))]. given #261 (F,wt=15): 1192 (x v y) ^ (z v (y v (x v u))) = x v y. [para(317(a,1),68(a,2)),demod(10(6),10(5),1004(8))]. given #262 (F,wt=15): 1203 x v (y ^ ((z ^ (x ^ u)) v (x ^ v))) = x. [para(18(a,1),352(a,1,2,2,1))]. given #263 (F,wt=15): 1204 x v (y ^ ((x ^ z) v (u ^ (x ^ v)))) = x. [para(18(a,1),352(a,1,2,2,2))]. given #264 (T,wt=15): 1211 x v (y ^ (((x ^ z) v (x ^ u)) ^ v)) = x. [para(352(a,1),99(a,1,2)),demod(12(5),9(6),352(11))]. given #265 (A,wt=19): 132 (x v y) ^ ((x v (y ^ z)) ^ u) = (x v (y ^ z)) ^ u. [para(52(a,1),46(a,1,2,1)),demod(18(5))]. given #266 (F,wt=15): 1216 x v (y ^ ((z ^ (u ^ x)) v (x ^ v))) = x. [para(58(a,1),352(a,1,2,2,1))]. given #267 (F,wt=15): 1217 x v (y ^ ((x ^ z) v (u ^ (v ^ x)))) = x. [para(58(a,1),352(a,1,2,2,2))]. given #268 (F,wt=15): 1234 x ^ ((y ^ x) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),359(a,1,2,2))]. given #269 (F,wt=15): 1235 x ^ ((y ^ (x v z)) v (y ^ u)) = x ^ y. [para(359(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #270 (T,wt=15): 1237 x ^ ((y ^ (z v x)) v (y ^ u)) = x ^ y. [para(359(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #271 (A,wt=17): 135 (x v (y ^ z)) ^ (u v (x v z)) = x v (y ^ z). [para(54(a,1),45(a,1,2,2))]. given #272 (F,wt=15): 1243 x ^ ((y ^ x) v (z ^ (u ^ y))) = x ^ y. [para(58(a,1),359(a,1,2,2))]. given #273 (F,wt=15): 1264 (x ^ y) v (z ^ (y ^ (u ^ x))) = y ^ x. [para(11(a,1),78(a,1,1))]. given #274 (F,wt=15): 1265 (x ^ y) v (z ^ (u ^ (y ^ x))) = x ^ y. [para(11(a,1),78(a,1,2,2)),demod(12(3))]. given #275 (F,wt=15): 1301 x ^ ((y ^ (z ^ u)) v (z ^ x)) = x ^ z. [para(18(a,1),360(a,1,2,1))]. given #276 (T,wt=15): 1303 x ^ ((y ^ z) v (y ^ (x v u))) = x ^ y. [para(360(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #277 (A,wt=17): 136 (x ^ y) v (z v (x ^ (u ^ y))) = z v (x ^ y). [para(18(a,1),54(a,1,2,2))]. given #278 (F,wt=15): 1304 x ^ ((y ^ z) v (y ^ (u v x))) = x ^ y. [para(360(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #279 (F,wt=15): 1309 x ^ ((y ^ (z ^ u)) v (u ^ x)) = x ^ u. [para(58(a,1),360(a,1,2,1))]. given #280 (F,wt=15): 1332 (x ^ (y v z)) v (y ^ x) = x ^ (y v z). [para(21(a,1),410(a,1,2))]. given #281 (F,wt=15): 1333 (x ^ y) v (z ^ (y ^ (x ^ u))) = x ^ y. [para(410(a,1),52(a,2)),demod(12(6),12(5),1168(8))]. given #282 (T,wt=15): 1371 (x ^ y) v ((z v y) ^ x) = (z v y) ^ x. [para(19(a,1),1076(a,1,1,2))]. given #283 (A,wt=19): 139 (x v y) ^ ((x v (z ^ y)) ^ u) = (x v (z ^ y)) ^ u. [para(54(a,1),46(a,1,2,1)),demod(18(5))]. given #284 (F,wt=15): 1400 x v (y ^ (z ^ ((u ^ x) v (x ^ v)))) = x. [para(12(a,1),1198(a,1,2))]. given #285 (F,wt=15): 1407 x v (y ^ ((z ^ x) v (u ^ (x ^ v)))) = x. [para(18(a,1),1198(a,1,2,2,2))]. given #286 (F,wt=15): 1419 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(1198(a,1),99(a,1,2)),demod(12(5),9(6),1198(11))]. given #287 (F,wt=15): 1426 x v (y ^ ((z ^ x) v (u ^ (v ^ x)))) = x. [para(58(a,1),1198(a,1,2,2,2))]. given #288 (T,wt=15): 1464 x v (y ^ (z ^ ((x ^ u) v (v ^ x)))) = x. [para(12(a,1),1199(a,1,2))]. given #289 (A,wt=17): 143 x ^ (y ^ (z v (u v (v v (x ^ y))))) = x ^ y. [para(63(a,1),12(a,1)),flip(a)]. given #290 (F,wt=15): 1468 x v (y ^ ((z ^ (x ^ u)) v (v ^ x))) = x. [para(18(a,1),1199(a,1,2,2,1))]. given #291 (F,wt=15): 1476 x v (y ^ (((x ^ z) v (u ^ x)) ^ v)) = x. [para(1199(a,1),99(a,1,2)),demod(12(5),9(6),1199(11))]. given #292 (F,wt=15): 1481 x v (y ^ ((z ^ (u ^ x)) v (v ^ x))) = x. [para(58(a,1),1199(a,1,2,2,1))]. given #293 (F,wt=15): 1497 x v (((y ^ (x ^ z)) v (x ^ u)) ^ v) = x. [para(18(a,1),1200(a,1,2,1,1))]. given #294 (T,wt=15): 1498 x v (((x ^ y) v (z ^ (x ^ u))) ^ v) = x. [para(18(a,1),1200(a,1,2,1,2))]. given #295 (A,wt=17): 144 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(63(a,1),25(a,1,2)),demod(9(4))]. given #296 (F,wt=15): 1507 x v (((y ^ (z ^ x)) v (x ^ u)) ^ v) = x. [para(58(a,1),1200(a,1,2,1,1))]. given #297 (F,wt=15): 1508 x v (((x ^ y) v (z ^ (u ^ x))) ^ v) = x. [para(58(a,1),1200(a,1,2,1,2))]. given #298 (F,wt=15): 1526 x ^ ((x ^ y) v (z ^ (y ^ u))) = x ^ y. [para(18(a,1),1227(a,1,2,2))]. given #299 (F,wt=15): 1527 x ^ (((x v y) ^ z) v (z ^ u)) = x ^ z. [para(1227(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #300 (T,wt=15): 1528 x ^ (((y v x) ^ z) v (z ^ u)) = x ^ z. [para(1227(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #301 (A,wt=17): 145 (x v y) ^ (z v (u v (x v (v v y)))) = x v y. [para(17(a,1),63(a,1,2,2,2))]. given #302 (F,wt=15): 1532 x ^ ((x ^ y) v (z ^ (u ^ y))) = x ^ y. [para(58(a,1),1227(a,1,2,2))]. given #303 (F,wt=15): 1547 x ^ (y v ((y v z) ^ x)) = x ^ (y v z). [para(13(a,1),1228(a,1,2,2)),demod(9(3))]. given #304 (F,wt=15): 1548 x ^ (y v ((z v y) ^ x)) = x ^ (z v y). [para(19(a,1),1228(a,1,2,2)),demod(9(3))]. given #305 (F,wt=15): 1554 x ^ ((y ^ (x v z)) v (u ^ y)) = x ^ y. [para(1228(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #306 (T,wt=15): 1557 x ^ ((y ^ (z v x)) v (u ^ y)) = x ^ y. [para(1228(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #307 (A,wt=19): 148 ((x ^ y) v z) ^ (u v (v v (x v z))) = (x ^ y) v z. [para(23(a,1),63(a,1,2,2,2))]. given #308 (F,wt=15): 1609 x ^ ((y ^ z) v (z ^ (x v u))) = x ^ z. [para(1295(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #309 (F,wt=15): 1610 x ^ ((y ^ z) v (z ^ (u v x))) = x ^ z. [para(1295(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #310 (F,wt=15): 1651 x ^ ((y ^ (z ^ u)) v (x ^ z)) = x ^ z. [para(18(a,1),1296(a,1,2,1))]. given #311 (F,wt=15): 1653 x ^ ((y ^ z) v ((x v u) ^ y)) = x ^ y. [para(1296(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #312 (T,wt=15): 1654 x ^ ((y ^ z) v ((u v x) ^ y)) = x ^ y. [para(1296(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #313 (A,wt=21): 149 x v (y v (z v (u v (x v v)))) = y v (z v (u v (x v v))). [para(63(a,1),48(a,1,2,1)),demod(17(5),10(4),10(3),10(2),10(9),10(8),10(7))]. given #314 (F,wt=15): 1658 x ^ ((y ^ (z ^ u)) v (x ^ u)) = x ^ u. [para(58(a,1),1296(a,1,2,1))]. given #315 (F,wt=15): 1673 x v (y ^ (z ^ ((u ^ x) v (v ^ x)))) = x. [para(12(a,1),1397(a,1,2))]. given #316 (F,wt=15): 1693 x v (y ^ (((z ^ x) v (u ^ x)) ^ v)) = x. [para(1397(a,1),99(a,1,2)),demod(12(5),9(6),1397(11))]. given #317 (F,wt=15): 1714 x v (((y ^ x) v (z ^ (x ^ u))) ^ v) = x. [para(18(a,1),1398(a,1,2,1,2))]. given #318 (T,wt=15): 1728 x v (((y ^ x) v (z ^ (u ^ x))) ^ v) = x. [para(58(a,1),1398(a,1,2,1,2))]. given #319 (A,wt=19): 150 ((x ^ y) v z) ^ (u v (v v (y v z))) = (x ^ y) v z. [para(48(a,1),63(a,1,2,2,2))]. given #320 (F,wt=15): 1744 x v (((y ^ (x ^ z)) v (u ^ x)) ^ v) = x. [para(18(a,1),1462(a,1,2,1,1))]. given #321 (F,wt=15): 1753 x v (((y ^ (z ^ x)) v (u ^ x)) ^ v) = x. [para(58(a,1),1462(a,1,2,1,1))]. given #322 (F,wt=15): 1762 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(13(a,1),1520(a,1,2,2)),demod(9(3))]. given #323 (F,wt=15): 1763 x ^ (y v (x ^ (z v y))) = x ^ (z v y). [para(19(a,1),1520(a,1,2,2)),demod(9(3))]. given #324 (T,wt=15): 1769 x ^ (((x v y) ^ z) v (u ^ z)) = x ^ z. [para(1520(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #325 (A,wt=19): 151 (x v (y ^ z)) ^ (u v (v v (x v y))) = x v (y ^ z). [para(52(a,1),63(a,1,2,2,2))]. given #326 (F,wt=15): 1772 x ^ (((y v x) ^ z) v (u ^ z)) = x ^ z. [para(1520(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #327 (F,wt=15): 1819 x ^ ((y ^ z) v ((x v u) ^ z)) = x ^ z. [para(1602(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #328 (F,wt=15): 1820 x ^ ((y ^ z) v ((u v x) ^ z)) = x ^ z. [para(1602(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #329 (F,wt=15): 1924 x ^ (y ^ (((y v z) ^ x) v u)) = x ^ y. [para(153(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #330 (T,wt=15): 1932 x ^ (y ^ (z v ((y v u) ^ x))) = x ^ y. [para(290(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #331 (A,wt=19): 152 (x v (y ^ z)) ^ (u v (v v (x v z))) = x v (y ^ z). [para(54(a,1),63(a,1,2,2,2))]. given #332 (F,wt=15): 2042 x v (y v (((y ^ z) v x) ^ u)) = x v y. [para(202(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #333 (F,wt=15): 2045 x v (y v (z ^ ((y ^ u) v x))) = x v y. [para(239(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #334 (F,wt=15): 2141 x ^ (y ^ ((x ^ (z v y)) v u)) = y ^ x. [para(22(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #335 (F,wt=15): 2146 x ^ (y ^ (z v (x ^ (u v y)))) = y ^ x. [para(47(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #336 (T,wt=15): 2150 x ^ (y ^ (((z v y) ^ x) v u)) = y ^ x. [para(153(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #337 (A,wt=19): 154 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 #338 (F,wt=15): 2155 x ^ (y ^ (z v ((u v y) ^ x))) = y ^ x. [para(290(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #339 (F,wt=15): 2336 x v (y v (((z ^ y) v x) ^ u)) = x v y. [para(202(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #340 (F,wt=15): 2338 x v (y v (z ^ ((u ^ y) v x))) = x v y. [para(239(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #341 (F,wt=15): 2584 x ^ (((x v y) ^ (z v (u v x))) v v) = x. [para(159(a,1),64(a,1)),demod(45(3)),flip(a)]. given #342 (T,wt=15): 2587 x ^ (((x v y) ^ (z v (x v u))) v v) = x. [para(159(a,1),81(a,1)),demod(51(3)),flip(a)]. given #343 (A,wt=19): 155 (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 #344 (F,wt=15): 2624 x ^ (((y v (x v z)) ^ (x v u)) v v) = x. [para(17(a,1),2576(a,1,2,1,1))]. given #345 (F,wt=15): 2625 x ^ (y v (((x v z) ^ (x v u)) v v)) = x. [para(17(a,1),2576(a,1,2))]. given #346 (F,wt=15): 2638 x ^ (((y v (z v x)) ^ (x v u)) v v) = x. [para(62(a,1),2576(a,1,2,1,1))]. given #347 (F,wt=15): 2639 x ^ (y v (z v ((x v u) ^ (x v v)))) = x. [para(62(a,1),2576(a,1,2))]. given #348 (T,wt=15): 2719 x ^ (((y v (x v z)) ^ (u v x)) v v) = x. [para(17(a,1),2577(a,1,2,1,1))]. given #349 (A,wt=17): 156 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(22(a,1),18(a,1,2)),flip(a)]. given #350 (F,wt=15): 2721 x ^ (y v (((x v z) ^ (u v x)) v v)) = x. [para(17(a,1),2577(a,1,2))]. given #351 (F,wt=15): 2738 x ^ (((y v (z v x)) ^ (u v x)) v v) = x. [para(62(a,1),2577(a,1,2,1,1))]. given #352 (F,wt=15): 2739 x ^ (y v (z v ((x v u) ^ (v v x)))) = x. [para(62(a,1),2577(a,1,2))]. given #353 (F,wt=15): 2762 x ^ (((y v x) ^ (z v (x v u))) v v) = x. [para(17(a,1),2619(a,1,2,1,2))]. given #354 (T,wt=15): 2763 x ^ (y v (((z v x) ^ (x v u)) v v)) = x. [para(17(a,1),2619(a,1,2))]. given #355 (A,wt=19): 157 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 #356 (F,wt=15): 2774 x ^ (((y v x) ^ (z v (u v x))) v v) = x. [para(62(a,1),2619(a,1,2,1,2))]. given #357 (F,wt=15): 2775 x ^ (y v (z v ((u v x) ^ (x v v)))) = x. [para(62(a,1),2619(a,1,2))]. given #358 (F,wt=15): 2793 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(17(a,1),2620(a,1,2,2,1))]. given #359 (F,wt=15): 2794 x ^ (y v ((x v z) ^ (u v (x v v)))) = x. [para(17(a,1),2620(a,1,2,2,2))]. given #360 (T,wt=15): 2804 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(62(a,1),2620(a,1,2,2,1))]. given #361 (A,wt=21): 158 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(22(a,1),50(a,1,2,2))]. given #362 (F,wt=15): 2805 x ^ (y v ((x v z) ^ (u v (v v x)))) = x. [para(62(a,1),2620(a,1,2,2,2))]. given #363 (F,wt=15): 2829 x ^ (y v (((z v x) ^ (u v x)) v v)) = x. [para(17(a,1),2713(a,1,2))]. given #364 (F,wt=15): 2845 x ^ (y v (z v ((u v x) ^ (v v x)))) = x. [para(62(a,1),2713(a,1,2))]. given #365 (F,wt=15): 2859 x ^ (y v ((z v (x v u)) ^ (v v x))) = x. [para(17(a,1),2714(a,1,2,2,1))]. given #366 (T,wt=15): 2874 x ^ (y v ((z v (u v x)) ^ (v v x))) = x. [para(62(a,1),2714(a,1,2,2,1))]. given #367 (A,wt=23): 161 (x ^ y) v ((y ^ ((x ^ y) v z)) v u) = (y ^ ((x ^ y) v z)) v u. [para(22(a,1),48(a,1,2,1)),demod(17(6))]. given #368 (F,wt=15): 2949 x ^ (y v ((z v x) ^ (u v (x v v)))) = x. [para(17(a,1),2756(a,1,2,2,2))]. given #369 (F,wt=15): 2958 x ^ (y v ((z v x) ^ (u v (v v x)))) = x. [para(62(a,1),2756(a,1,2,2,2))]. given #370 (F,wt=15): 3215 x v ((y v (z v u)) ^ (z v x)) = x v z. [para(17(a,1),3119(a,1,2,1))]. given #371 (F,wt=15): 3217 x v ((y v z) ^ (y v (x ^ u))) = x v y. [para(3119(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #372 (T,wt=15): 3219 x v ((y v z) ^ (y v (u ^ x))) = x v y. [para(3119(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #373 (A,wt=23): 162 (x ^ ((y ^ x) v z)) v (u v (y ^ x)) = u v (x ^ ((y ^ x) v z)). [para(22(a,1),54(a,1,2,2))]. given #374 (F,wt=15): 3230 x v ((y v (z v u)) ^ (u v x)) = x v u. [para(62(a,1),3119(a,1,2,1))]. given #375 (F,wt=15): 3284 x v (y ^ ((z ^ y) v x)) = x v (z ^ y). [para(25(a,1),3208(a,1,2,1))]. given #376 (F,wt=15): 3290 x v ((y v z) ^ (z v (x ^ u))) = x v z. [para(3208(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #377 (F,wt=15): 3293 x v ((y v z) ^ (z v (u ^ x))) = x v z. [para(3208(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #378 (T,wt=15): 3375 x v ((y v (z v u)) ^ (x v z)) = x v z. [para(17(a,1),3209(a,1,2,1))]. given #379 (A,wt=17): 163 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(66(a,1),12(a,1)),demod(12(2)),flip(a)]. given #380 (F,wt=15): 3377 x v ((y v z) ^ ((x ^ u) v y)) = x v y. [para(3209(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #381 (F,wt=15): 3378 x v ((y v z) ^ ((u ^ x) v y)) = x v y. [para(3209(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #382 (F,wt=15): 3381 x v ((y v (z v u)) ^ (x v u)) = x v u. [para(62(a,1),3209(a,1,2,1))]. given #383 (F,wt=15): 3404 x v ((y v x) ^ (z v (y v u))) = x v y. [para(17(a,1),3213(a,1,2,2))]. given #384 (T,wt=15): 3405 x v ((y v (x ^ z)) ^ (y v u)) = x v y. [para(3213(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #385 (A,wt=17): 166 (x v y) ^ (z ^ (x v (u v y))) = (x v y) ^ z. [para(17(a,1),66(a,1,2,2))]. given #386 (F,wt=15): 3406 x v ((y v (z ^ x)) ^ (y v u)) = x v y. [para(3213(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #387 (F,wt=15): 3414 x v ((y v x) ^ (z v (u v y))) = x v y. [para(62(a,1),3213(a,1,2,2))]. given #388 (F,wt=15): 3456 x v (y ^ (x v (z ^ y))) = x v (z ^ y). [para(25(a,1),3279(a,1,2,1))]. given #389 (F,wt=15): 3462 x v ((y v z) ^ ((x ^ u) v z)) = x v z. [para(3279(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #390 (T,wt=15): 3464 x v ((y v z) ^ ((u ^ x) v z)) = x v z. [para(3279(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #391 (A,wt=17): 167 (x ^ (y v z)) v (u ^ (z ^ x)) = x ^ (y v z). [para(66(a,1),50(a,1,2,2))]. given #392 (F,wt=15): 3523 x v ((y v (x ^ z)) ^ (u v y)) = x v y. [para(3283(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #393 (F,wt=15): 3524 x v ((y v (z ^ x)) ^ (u v y)) = x v y. [para(3283(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #394 (F,wt=15): 3581 x v ((x v y) ^ (z v (y v u))) = x v y. [para(17(a,1),3373(a,1,2,2))]. given #395 (F,wt=15): 3582 x v (((x ^ y) v z) ^ (z v u)) = x v z. [para(3373(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #396 (T,wt=15): 3583 x v (((y ^ x) v z) ^ (z v u)) = x v z. [para(3373(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #397 (A,wt=19): 168 ((x ^ y) v z) ^ (u ^ (x v z)) = ((x ^ y) v z) ^ u. [para(23(a,1),66(a,1,2,2))]. given #398 (F,wt=15): 3586 x v ((x v y) ^ (z v (u v y))) = x v y. [para(62(a,1),3373(a,1,2,2))]. given #399 (F,wt=15): 3608 x v (((x ^ y) v z) ^ (u v z)) = x v z. [para(3455(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #400 (F,wt=15): 3609 x v (((y ^ x) v z) ^ (u v z)) = x v z. [para(3455(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #401 (F,wt=17): 174 x ^ (y ^ (z ^ ((x ^ y) v u))) = z ^ (x ^ y). [para(68(a,1),12(a,1)),flip(a)]. given #402 (T,wt=17): 177 (x ^ (y v z)) v (u ^ (x ^ y)) = x ^ (y v z). [para(68(a,1),50(a,1,2,2))]. given #403 (A,wt=19): 169 (x ^ (y v z)) v ((z ^ x) v u) = (x ^ (y v z)) v u. [para(66(a,1),48(a,1,2,1))]. given #404 (F,wt=17): 181 x v (y v (z ^ (u ^ (v ^ (x v y))))) = x v y. [para(76(a,1),10(a,1)),flip(a)]. given #405 (F,wt=17): 183 x ^ (y ^ (z ^ (u ^ x))) = y ^ (z ^ (u ^ x)). [para(76(a,1),19(a,1,2)),demod(11(4))]. given #406 (F,wt=17): 185 (x ^ y) v (z ^ (u ^ (x ^ (v ^ y)))) = x ^ y. [para(18(a,1),76(a,1,2,2,2))]. given #407 (F,wt=17): 194 (x v y) ^ (z v (u v (x v (y v v)))) = x v y. [para(10(a,1),80(a,1,2,2,2))]. given #408 (T,wt=17): 196 x ^ (y ^ (z v (u v ((x ^ y) v v)))) = x ^ y. [para(80(a,1),12(a,1)),flip(a)]. given #409 (A,wt=19): 170 ((x ^ y) v z) ^ (u ^ (y v z)) = ((x ^ y) v z) ^ u. [para(48(a,1),66(a,1,2,2))]. given #410 (F,wt=17): 199 x v (y v (z ^ (u ^ ((x v y) ^ v)))) = x v y. [para(87(a,1),10(a,1)),flip(a)]. given #411 (F,wt=17): 200 (x ^ y) v (z ^ (u ^ (x ^ (y ^ v)))) = x ^ y. [para(12(a,1),87(a,1,2,2,2))]. given #412 (F,wt=17): 205 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 #413 (F,wt=17): 213 (x v (y v z)) ^ (u ^ (x v y)) = u ^ (x v y). [para(10(a,1),92(a,1,1))]. given #414 (T,wt=17): 218 x ^ (y ^ ((y ^ ((x ^ y) v z)) v u)) = x ^ y. [para(22(a,1),92(a,1,2)),demod(11(6),12(6),22(10))]. given #415 (A,wt=19): 171 (x v (y ^ z)) ^ (u ^ (x v y)) = (x v (y ^ z)) ^ u. [para(52(a,1),66(a,1,2,2))]. given #416 (F,wt=17): 223 (x ^ (y ^ z)) v (u v (x ^ y)) = u v (x ^ y). [para(12(a,1),99(a,1,1))]. given #417 (F,wt=17): 226 (x v (y ^ z)) ^ (x v (u v y)) = x v (y ^ z). [para(99(a,1),20(a,1,2,2))]. given #418 (F,wt=17): 230 x v (y v ((y v ((x v y) ^ z)) ^ u)) = x v y. [para(24(a,1),99(a,1,2)),demod(9(6),10(6),24(10))]. given #419 (F,wt=17): 233 (x v (y v z)) ^ (z v (x v y)) = x v (y v z). [para(10(a,1),106(a,1,1)),demod(10(7))]. given #420 (T,wt=17): 234 (x v (y v z)) ^ (y v (z v x)) = x v (y v z). [para(10(a,1),106(a,1,2))]. given #421 (A,wt=19): 173 (x v (y ^ z)) ^ (u ^ (x v z)) = (x v (y ^ z)) ^ u. [para(54(a,1),66(a,1,2,2))]. given #422 (F,wt=17): 237 (x v (y v z)) ^ (x v (z v y)) = x v (y v z). [para(17(a,1),106(a,1,2)),demod(10(2),10(7))]. given #423 (F,wt=17): 244 (x v (y v z)) ^ (u ^ (x v z)) = u ^ (x v z). [para(17(a,1),112(a,1,1))]. given #424 (F,wt=17): 252 x ^ (y ^ (z v (y ^ ((x ^ y) v u)))) = x ^ y. [para(22(a,1),112(a,1,2)),demod(11(6),12(6),22(10))]. given #425 (F,wt=17): 261 (x ^ (y ^ z)) v (u v (x ^ z)) = u v (x ^ z). [para(18(a,1),120(a,1,1))]. given #426 (T,wt=17): 264 (x v (y ^ z)) ^ (x v (u v z)) = x v (y ^ z). [para(120(a,1),20(a,1,2,2))]. given #427 (A,wt=19): 178 (x ^ y) v ((x ^ (y v z)) v u) = (x ^ (y v z)) v u. [para(68(a,1),48(a,1,2,1)),demod(17(5))]. given #428 (F,wt=17): 274 x v (y v (z ^ (y v ((x v y) ^ u)))) = x v y. [para(24(a,1),120(a,1,2)),demod(9(6),10(6),24(10))]. given #429 (F,wt=17): 282 (x ^ (y v z)) v (x ^ (u ^ y)) = x ^ (y v z). [para(92(a,1),26(a,1,2,2))]. given #430 (F,wt=17): 284 (x ^ (y v z)) v (x ^ (u ^ z)) = x ^ (y v z). [para(112(a,1),26(a,1,2,2))]. given #431 (F,wt=17): 288 (x ^ (y ^ z)) v (z ^ (x ^ y)) = x ^ (y ^ z). [para(12(a,1),278(a,1,1)),demod(12(7))]. given #432 (T,wt=17): 289 (x ^ (y ^ z)) v (y ^ (z ^ x)) = x ^ (y ^ z). [para(12(a,1),278(a,1,2))]. given #433 (A,wt=19): 186 ((x v y) ^ z) v (u ^ (v ^ (x ^ z))) = (x v y) ^ z. [para(21(a,1),76(a,1,2,2,2))]. given #434 (F,wt=17): 291 (x ^ (y ^ z)) v (x ^ (z ^ y)) = y ^ (x ^ z). [para(18(a,1),278(a,1,1)),demod(12(4))]. given #435 (F,wt=17): 297 x ^ (y ^ (z ^ (u v (x ^ z)))) = y ^ (x ^ z). [para(47(a,1),18(a,1,2)),flip(a)]. given #436 (F,wt=17): 303 x ^ (y ^ ((y ^ (z v (x ^ y))) v u)) = x ^ y. [para(47(a,1),92(a,1,2)),demod(11(6),12(6),47(10))]. given #437 (F,wt=17): 304 x ^ (y ^ (z v (y ^ (u v (x ^ y))))) = x ^ y. [para(47(a,1),112(a,1,2)),demod(11(6),12(6),47(10))]. given #438 (T,wt=17): 308 x v (y v (z v (u ^ (x v z)))) = y v (x v z). [para(49(a,1),17(a,1,2)),flip(a)]. given #439 (A,wt=19): 188 x v (y v (z v (u ^ (v ^ (x v y))))) = x v (y v z). [para(20(a,1),76(a,1,2,2,2)),demod(10(6),10(5))]. given #440 (F,wt=17): 314 x v (y v ((y v (z ^ (x v y))) ^ u)) = x v y. [para(49(a,1),99(a,1,2)),demod(9(6),10(6),49(10))]. given #441 (F,wt=17): 316 x v (y v (z ^ (y v (u ^ (x v y))))) = x v y. [para(49(a,1),120(a,1,2)),demod(9(6),10(6),49(10))]. given #442 (F,wt=17): 333 (x v (y ^ z)) ^ (x v (z ^ y)) = x v (y ^ z). [para(278(a,1),53(a,1,2,2))]. given #443 (F,wt=17): 344 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(29(a,1),37(a,1,2)),demod(29(10))]. given #444 (T,wt=17): 376 (x ^ y) v (x ^ ((y ^ z) v (y ^ u))) = x ^ y. [para(29(a,1),26(a,1,2,2))]. given #445 (A,wt=21): 189 x ^ (y ^ (z ^ (u ^ (x ^ v)))) = y ^ (z ^ (u ^ (x ^ v))). [para(76(a,1),46(a,1,2,1)),demod(18(5),12(4),12(3),12(2),12(9),12(8),12(7))]. given #446 (F,wt=17): 388 x ^ (y ^ ((z v (u v x)) ^ v)) = y ^ (x ^ v). [para(64(a,1),18(a,1,2)),flip(a)]. given #447 (F,wt=17): 397 x ^ (y ^ (((z v (u v x)) ^ y) v v)) = x ^ y. [para(22(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #448 (F,wt=17): 401 x ^ (y ^ (z v ((u v (v v x)) ^ y))) = x ^ y. [para(64(a,1),112(a,1,2)),demod(11(6),12(6),64(10))]. given #449 (F,wt=17): 404 x ^ (y ^ ((z v (y ^ x)) ^ u)) = x ^ (y ^ u). [para(278(a,1),64(a,1,2,1,2)),demod(12(5),12(7))]. given #450 (T,wt=17): 406 (x v (y v z)) ^ (u ^ (z ^ v)) = u ^ (z ^ v). [para(56(a,1),64(a,2)),demod(115(6))]. given #451 (A,wt=19): 190 ((x v y) ^ z) v (u ^ (v ^ (y ^ z))) = (x v y) ^ z. [para(46(a,1),76(a,1,2,2,2))]. given #452 (F,wt=17): 408 (x v (y v z)) ^ (u ^ (v ^ z)) = u ^ (v ^ z). [para(58(a,1),64(a,2)),demod(183(6))]. given #453 (F,wt=17): 409 x ^ ((y v (z v (u v (v v x)))) ^ w) = x ^ w. [para(64(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #454 (F,wt=17): 426 (x ^ (y v z)) v (x ^ (z v y)) = x ^ (y v z). [para(106(a,1),70(a,1,2,2))]. given #455 (F,wt=17): 441 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),39(7))]. given #456 (T,wt=17): 458 x ^ (y ^ (z ^ (u v (v v x)))) = y ^ (z ^ x). [para(12(a,1),71(a,1,2)),demod(12(7))]. given #457 (A,wt=23): 191 (x ^ ((y ^ x) v z)) v (u ^ (v ^ (y ^ x))) = x ^ ((y ^ x) v z). [para(22(a,1),76(a,1,2,2,2))]. given #458 (F,wt=17): 469 x ^ (y ^ ((x ^ (z v (u v y))) v v)) = x ^ y. [para(71(a,1),92(a,1,2)),demod(11(6),12(6),71(10))]. given #459 (F,wt=17): 470 x ^ (y ^ (z v (x ^ (u v (v v y))))) = x ^ y. [para(71(a,1),112(a,1,2)),demod(11(6),12(6),71(10))]. given #460 (F,wt=17): 473 x ^ (y ^ (z ^ (u v (y ^ x)))) = z ^ (x ^ y). [para(278(a,1),71(a,1,2,2,2)),demod(12(5))]. given #461 (F,wt=17): 475 x ^ (y ^ (z v (u v (v v (w v x))))) = y ^ x. [para(71(a,1),64(a,1,2)),demod(71(4)),flip(a)]. given #462 (T,wt=17): 480 x v (y v ((z ^ (u ^ x)) v v)) = y v (x v v). [para(74(a,1),17(a,1,2)),flip(a)]. given #463 (A,wt=19): 192 (x ^ (y v z)) v (u ^ (v ^ (z ^ x))) = x ^ (y v z). [para(66(a,1),76(a,1,2,2,2))]. given #464 (F,wt=17): 494 x v (y v (((z ^ (u ^ x)) v y) ^ v)) = x v y. [para(24(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #465 (F,wt=17): 495 x v (y v ((z ^ (y v x)) v u)) = x v (y v u). [para(106(a,1),74(a,1,2,1,2)),demod(10(5),10(7))]. given #466 (F,wt=17): 497 x v (y v (z ^ ((u ^ (v ^ x)) v y))) = x v y. [para(74(a,1),120(a,1,2)),demod(9(6),10(6),74(10))]. given #467 (F,wt=17): 501 (x ^ (y ^ z)) v (u v (z v v)) = u v (z v v). [para(60(a,1),74(a,2)),demod(122(6))]. given #468 (T,wt=17): 502 (x ^ (y ^ z)) v (u v (v v z)) = u v (v v z). [para(62(a,1),74(a,2)),demod(144(6))]. given #469 (A,wt=19): 193 (x ^ (y v z)) v (u ^ (v ^ (x ^ y))) = x ^ (y v z). [para(68(a,1),76(a,1,2,2,2))]. given #470 (F,wt=17): 507 x v ((y ^ (z ^ (u ^ (v ^ x)))) v w) = x v w. [para(74(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #471 (F,wt=17): 508 x v (y v (z v (u ^ (v ^ x)))) = y v (z v x). [para(10(a,1),77(a,1,2)),demod(10(7))]. given #472 (F,wt=17): 520 x v (y v ((x v (z ^ (u ^ y))) ^ v)) = x v y. [para(77(a,1),99(a,1,2)),demod(9(6),10(6),77(10))]. given #473 (F,wt=17): 523 x v (y v (z ^ (x v (u ^ (v ^ y))))) = x v y. [para(77(a,1),120(a,1,2)),demod(9(6),10(6),77(10))]. given #474 (T,wt=17): 531 x v (y v (z ^ (u ^ (v ^ (w ^ x))))) = y v x. [para(77(a,1),74(a,1,2)),demod(77(4)),flip(a)]. given #475 (A,wt=19): 203 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 #476 (F,wt=17): 535 x ^ (y ^ ((z v (x v u)) ^ v)) = y ^ (x ^ v). [para(81(a,1),18(a,1,2)),flip(a)]. given #477 (F,wt=17): 539 x ^ (y ^ (((z v (x v u)) ^ y) v v)) = x ^ y. [para(22(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #478 (F,wt=17): 542 x ^ (y ^ (z v ((u v (x v v)) ^ y))) = x ^ y. [para(81(a,1),112(a,1,2)),demod(11(6),12(6),81(10))]. given #479 (F,wt=17): 544 (x v (y v z)) ^ (u ^ (y ^ v)) = u ^ (y ^ v). [para(56(a,1),81(a,2)),demod(115(6))]. given #480 (T,wt=17): 546 (x v (y v z)) ^ (u ^ (v ^ y)) = u ^ (v ^ y). [para(58(a,1),81(a,2)),demod(183(6))]. given #481 (A,wt=19): 204 (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 #482 (F,wt=17): 547 x ^ ((y v (z v (u v (x v v)))) ^ w) = x ^ w. [para(81(a,1),64(a,1,2)),demod(64(4),10(4),10(3)),flip(a)]. given #483 (F,wt=17): 549 x ^ (y ^ (z v (u v (v v (x v w))))) = y ^ x. [para(71(a,1),81(a,1,2)),demod(83(4)),flip(a)]. given #484 (F,wt=17): 554 x ^ (y ^ (z ^ (u v (x v v)))) = y ^ (z ^ x). [para(12(a,1),83(a,1,2)),demod(12(7))]. given #485 (F,wt=17): 559 x ^ (y ^ ((x ^ (z v (y v u))) v v)) = x ^ y. [para(83(a,1),92(a,1,2)),demod(11(6),12(6),83(10))]. given #486 (T,wt=17): 560 x ^ (y ^ (z v (x ^ (u v (y v v))))) = x ^ y. [para(83(a,1),112(a,1,2)),demod(11(6),12(6),83(10))]. given #487 (A,wt=19): 206 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 #488 (F,wt=17): 562 (x v y) ^ (z v (x v (u v (y v v)))) = x v y. [para(53(a,1),83(a,2)),demod(10(6),10(5),18(9),111(9))]. given #489 (F,wt=17): 570 x ^ (y ^ (z v (u v ((x v v) ^ y)))) = x ^ y. [para(65(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #490 (F,wt=17): 571 x ^ (y ^ (z v (u v ((v v x) ^ y)))) = x ^ y. [para(65(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #491 (F,wt=17): 580 x v (y v ((z ^ (x ^ u)) v v)) = y v (x v v). [para(84(a,1),17(a,1,2)),flip(a)]. given #492 (T,wt=17): 585 x v (y v (((z ^ (x ^ u)) v y) ^ v)) = x v y. [para(24(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #493 (A,wt=21): 207 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(24(a,1),45(a,1,2,2))]. given #494 (F,wt=17): 587 x v (y v (z ^ ((u ^ (x ^ v)) v y))) = x v y. [para(84(a,1),120(a,1,2)),demod(9(6),10(6),84(10))]. given #495 (F,wt=17): 590 x v ((y ^ ((x ^ z) v (x ^ u))) v v) = x v v. [para(29(a,1),84(a,1,2,1,2))]. given #496 (F,wt=17): 591 (x ^ (y ^ z)) v (u v (y v v)) = u v (y v v). [para(60(a,1),84(a,2)),demod(122(6))]. given #497 (F,wt=17): 592 (x ^ (y ^ z)) v (u v (v v y)) = u v (v v y). [para(62(a,1),84(a,2)),demod(144(6))]. given #498 (T,wt=17): 595 x v ((y ^ (z ^ (u ^ (x ^ v)))) v w) = x v w. [para(84(a,1),74(a,1,2)),demod(74(4),12(4),12(3)),flip(a)]. given #499 (A,wt=23): 209 (x v y) ^ ((y v ((x v y) ^ z)) ^ u) = (y v ((x v y) ^ z)) ^ u. [para(24(a,1),46(a,1,2,1)),demod(18(6))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 41 (0.00 of 14.65 sec). given #500 (F,wt=17): 596 x v (y v (z ^ (u ^ (v ^ (x ^ w))))) = y v x. [para(77(a,1),84(a,1,2)),demod(88(4)),flip(a)]. given #501 (F,wt=17): 598 x v (y v (z v (u ^ (x ^ v)))) = y v (z v x). [para(10(a,1),88(a,1,2)),demod(10(7))]. given #502 (F,wt=17): 604 x v (y v ((x v (z ^ (y ^ u))) ^ v)) = x v y. [para(88(a,1),99(a,1,2)),demod(9(6),10(6),88(10))]. given #503 (F,wt=17): 606 x v (y v (z ^ (x v (u ^ (y ^ v))))) = x v y. [para(88(a,1),120(a,1,2)),demod(9(6),10(6),88(10))]. given #504 (T,wt=17): 608 x v (y v (z ^ ((x ^ u) v (x ^ v)))) = y v x. [para(29(a,1),88(a,1,2,2,2))]. given #505 (A,wt=23): 211 (x v ((y v x) ^ z)) ^ (u v (v v (y v x))) = x v ((y v x) ^ z). [para(24(a,1),63(a,1,2,2,2))]. given #506 (F,wt=17): 610 (x ^ y) v (z ^ (x ^ (u ^ (y ^ v)))) = x ^ y. [para(70(a,1),88(a,2)),demod(12(6),12(5),17(9),123(9))]. given #507 (F,wt=17): 614 (x v y) ^ ((y v (x v z)) ^ u) = (y v x) ^ u. [para(101(a,1),12(a,1,1)),flip(a)]. given #508 (F,wt=17): 617 (x v y) ^ (z ^ (y v (x v u))) = z ^ (y v x). [para(101(a,1),18(a,1,2)),flip(a)]. given #509 (F,wt=17): 625 (x v y) ^ ((y v (z v x)) ^ u) = (x v y) ^ u. [para(102(a,1),12(a,1,1)),flip(a)]. given #510 (T,wt=17): 629 x v (y v (z v (u ^ (z v x)))) = x v (y v z). [para(102(a,1),50(a,1,2,2)),demod(10(5),10(4))]. given #511 (A,wt=23): 212 (x v ((y v x) ^ z)) ^ (u ^ (y v x)) = (x v ((y v x) ^ z)) ^ u. [para(24(a,1),66(a,1,2,2))]. given #512 (F,wt=17): 643 ((x ^ y) v z) ^ (z v (y ^ x)) = (x ^ y) v z. [para(278(a,1),102(a,1,2,2))]. given #513 (F,wt=17): 645 (x v (y v z)) ^ (u ^ (z v x)) = u ^ (z v x). [para(102(a,1),58(a,1,2,2)),demod(102(9))]. given #514 (F,wt=17): 667 x ^ (y ^ (z v (u v (v v (y ^ x))))) = x ^ y. [para(278(a,1),141(a,1,2,2,2,2)),demod(12(6))]. given #515 (F,wt=17): 670 (x v (y v (z v (u v v)))) ^ (w ^ v) = w ^ v. [para(141(a,1),58(a,1,2,2)),demod(141(11))]. given #516 (T,wt=17): 671 x ^ (y v (z v (u v (v v (w v (v6 v x)))))) = x. [para(141(a,1),64(a,1,2)),demod(45(3)),flip(a)]. given #517 (A,wt=19): 247 (x v y) ^ (z ^ ((x ^ u) v y)) = z ^ ((x ^ u) v y). [para(23(a,1),112(a,1,1))]. given #518 (F,wt=17): 676 x ^ (y v (z v (u v (v v (w v (x v v6)))))) = x. [para(141(a,1),81(a,1,2)),demod(51(3)),flip(a)]. given #519 (F,wt=17): 682 (x v y) ^ (z v (x v (u v (v v y)))) = x v y. [para(10(a,1),67(a,1,2,2,2))]. given #520 (F,wt=17): 685 ((x ^ y) v z) ^ (x v (u v z)) = (x ^ y) v z. [para(23(a,1),67(a,1,2))]. given #521 (F,wt=17): 687 ((x ^ y) v z) ^ (y v (u v z)) = (x ^ y) v z. [para(48(a,1),67(a,1,2))]. given #522 (T,wt=17): 708 (x v (y v (z v (u v v)))) ^ (w ^ u) = w ^ u. [para(147(a,1),58(a,1,2,2)),demod(147(11))]. given #523 (A,wt=19): 249 (x v y) ^ (z ^ ((u ^ x) v y)) = z ^ ((u ^ x) v y). [para(48(a,1),112(a,1,1))]. given #524 (F,wt=17): 710 x ^ (y ^ (((y ^ x) v z) ^ u)) = x ^ (y ^ u). [para(153(a,1),12(a,1,1)),demod(12(2),12(6)),flip(a)]. given #525 (F,wt=17): 715 x ^ (y ^ (z ^ ((z ^ x) v u))) = y ^ (x ^ z). [para(153(a,1),18(a,1,2)),flip(a)]. given #526 (F,wt=17): 722 (x ^ y) v (z v (u ^ (y ^ x))) = (x ^ y) v z. [para(153(a,1),76(a,1,2,2)),demod(10(5))]. given #527 (F,wt=17): 723 x ^ (y ^ ((y ^ ((y ^ x) v z)) v u)) = x ^ y. [para(153(a,1),92(a,1,2)),demod(11(6),12(6),153(10))]. given #528 (T,wt=17): 724 x ^ (y ^ (z v (y ^ ((y ^ x) v u)))) = x ^ y. [para(153(a,1),112(a,1,2)),demod(11(6),12(6),153(10))]. given #529 (A,wt=19): 250 (x v y) ^ (z ^ (x v (y ^ u))) = z ^ (x v (y ^ u)). [para(52(a,1),112(a,1,1))]. given #530 (F,wt=17): 726 ((x ^ y) v z) ^ (u ^ (y ^ x)) = u ^ (y ^ x). [para(153(a,1),58(a,1,2,2)),demod(12(6),183(6),153(9))]. given #531 (F,wt=17): 727 x ^ (y ^ ((y ^ (z v (u v x))) v v)) = x ^ y. [para(153(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #532 (F,wt=17): 733 x ^ (y ^ ((y ^ (z v (x v u))) v v)) = x ^ y. [para(153(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #533 (F,wt=17): 743 x v (y v (z ^ (u ^ (v ^ (y v x))))) = x v y. [para(106(a,1),182(a,1,2,2,2,2)),demod(10(6))]. given #534 (T,wt=17): 748 (x ^ (y ^ (z ^ (u ^ v)))) v (w v v) = w v v. [para(182(a,1),62(a,1,2,2)),demod(182(11))]. given #535 (A,wt=19): 251 (x v y) ^ (z ^ (x v (u ^ y))) = z ^ (x v (u ^ y)). [para(54(a,1),112(a,1,1))]. given #536 (F,wt=17): 751 x v (y ^ (z ^ (u ^ (v ^ (w ^ (v6 ^ x)))))) = x. [para(182(a,1),74(a,1,2)),demod(50(3)),flip(a)]. given #537 (F,wt=17): 754 x v (y ^ (z ^ (u ^ (v ^ (w ^ (x ^ v6)))))) = x. [para(182(a,1),84(a,1,2)),demod(69(3)),flip(a)]. given #538 (F,wt=17): 761 x v (y ^ (z ^ (u ^ ((x ^ v) v (x ^ w))))) = x. [para(29(a,1),187(a,1,2,2,2,2))]. given #539 (F,wt=17): 762 (x ^ (y ^ (z ^ (u ^ v)))) v (w v u) = w v u. [para(187(a,1),62(a,1,2,2)),demod(187(11))]. given #540 (T,wt=17): 763 x v (y v (((y v x) ^ z) v u)) = x v (y v u). [para(202(a,1),10(a,1,1)),demod(10(2),10(6)),flip(a)]. given #541 (A,wt=21): 255 x ^ (y ^ (z ^ (u ^ (v ^ x)))) = y ^ (z ^ (u ^ (v ^ x))). [para(76(a,1),112(a,1,1))]. given #542 (F,wt=17): 775 (x v y) ^ (z ^ (u v (y v x))) = (x v y) ^ z. [para(202(a,1),63(a,1,2,2)),demod(12(5))]. given #543 (F,wt=17): 777 x v (y v ((y v ((y v x) ^ z)) ^ u)) = x v y. [para(202(a,1),99(a,1,2)),demod(17(6),9(5),202(10))]. given #544 (F,wt=17): 779 x v (y v (z ^ (y v ((y v x) ^ u)))) = x v y. [para(202(a,1),120(a,1,2)),demod(17(6),9(5),202(10))]. given #545 (F,wt=17): 782 ((x v y) ^ z) v (u v (y v x)) = u v (y v x). [para(202(a,1),62(a,1,2,2)),demod(10(6),144(6),202(9))]. given #546 (T,wt=17): 787 x v (y v ((y v (z ^ (u ^ x))) ^ v)) = x v y. [para(202(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #547 (A,wt=23): 256 (x v y) ^ (z ^ (y v ((x v y) ^ u))) = z ^ (y v ((x v y) ^ u)). [para(24(a,1),112(a,1,1))]. given #548 (F,wt=17): 788 x v (y v ((y v (z ^ (x ^ u))) ^ v)) = x v y. [para(202(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #549 (F,wt=17): 852 x ^ (y ^ (z v (((x v u) ^ y) v v))) = x ^ y. [para(21(a,1),216(a,1,2)),demod(11(6),12(6),21(9))]. given #550 (F,wt=17): 853 x ^ (y ^ (z v (((u v x) ^ y) v v))) = x ^ y. [para(46(a,1),216(a,1,2)),demod(11(6),12(6),46(9))]. given #551 (F,wt=17): 855 x ^ (y ^ (z v ((y ^ (u v x)) v v))) = x ^ y. [para(66(a,1),216(a,1,2)),demod(11(6),12(6),66(9))]. given #552 (T,wt=17): 856 x ^ (y ^ (z v ((x ^ (y v u)) v v))) = x ^ y. [para(68(a,1),216(a,1,2)),demod(11(6),12(6),68(9))]. given #553 (A,wt=19): 262 (x ^ y) v (z v ((x v u) ^ y)) = z v ((x v u) ^ y). [para(21(a,1),120(a,1,1))]. given #554 (F,wt=17): 868 (x v (y v (z v (u v v)))) ^ (u v y) = u v y. [para(102(a,1),216(a,1,2)),demod(10(3),10(2),102(10))]. given #555 (F,wt=17): 873 x v (y v (z ^ (((x ^ u) v y) ^ v))) = x v y. [para(23(a,1),225(a,1,2)),demod(9(6),10(6),23(9))]. given #556 (F,wt=17): 875 x v (y v (z ^ (((u ^ x) v y) ^ v))) = x v y. [para(48(a,1),225(a,1,2)),demod(9(6),10(6),48(9))]. given #557 (F,wt=17): 876 x v (y v (z ^ ((x v (y ^ u)) ^ v))) = x v y. [para(52(a,1),225(a,1,2)),demod(9(6),10(6),52(9))]. given #558 (T,wt=17): 877 x v (y v (z ^ ((x v (u ^ y)) ^ v))) = x v y. [para(54(a,1),225(a,1,2)),demod(9(6),10(6),54(9))]. given #559 (A,wt=19): 266 (x ^ y) v (z v ((u v x) ^ y)) = z v ((u v x) ^ y). [para(46(a,1),120(a,1,1))]. given #560 (F,wt=17): 881 (x ^ ((y ^ z) v (y ^ u))) v (v v y) = v v y. [para(29(a,1),225(a,1,1,2))]. given #561 (F,wt=17): 889 (x ^ (y v z)) v (u v (z v y)) = u v (z v y). [para(101(a,1),225(a,1,1,2))]. given #562 (F,wt=17): 904 x v (y v ((y v (z ^ (y v x))) ^ u)) = x v y. [para(239(a,1),99(a,1,2)),demod(17(6),9(5),239(10))]. given #563 (F,wt=17): 906 x v (y v (z ^ (y v (u ^ (y v x))))) = x v y. [para(239(a,1),120(a,1,2)),demod(17(6),9(5),239(10))]. given #564 (T,wt=17): 911 x v (y v (z ^ (y v (u ^ (v ^ x))))) = x v y. [para(239(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #565 (A,wt=21): 270 x v (y v (z v (u v (v v x)))) = y v (z v (u v (v v x))). [para(63(a,1),120(a,1,1))]. given #566 (F,wt=17): 912 x v (y v (z ^ (y v (u ^ (x ^ v))))) = x v y. [para(239(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #567 (F,wt=17): 920 (x v (y v z)) ^ ((y v x) ^ u) = (y v x) ^ u. [para(241(a,1),12(a,1,1)),flip(a)]. given #568 (F,wt=17): 922 (x v (y v z)) ^ (u ^ (y v x)) = u ^ (y v x). [para(241(a,1),18(a,1,2)),flip(a)]. given #569 (F,wt=17): 923 x v (y v (z v (u ^ (y v x)))) = x v (y v z). [para(241(a,1),69(a,1,2,2)),demod(10(5),10(4))]. given #570 (T,wt=17): 925 (x v (y v z)) ^ ((z ^ u) v x) = (z ^ u) v x. [para(99(a,1),241(a,1,1,2))]. given #571 (A,wt=23): 271 (x ^ y) v (z v (y ^ ((x ^ y) v u))) = z v (y ^ ((x ^ y) v u)). [para(22(a,1),120(a,1,1))]. given #572 (F,wt=17): 926 (x v (y v z)) ^ ((u ^ z) v x) = (u ^ z) v x. [para(120(a,1),241(a,1,1,2))]. given #573 (F,wt=17): 943 x ^ (y ^ (z v (u v (y ^ (v v x))))) = x ^ y. [para(66(a,1),242(a,1,2)),demod(11(6),12(6),66(9))]. given #574 (F,wt=17): 944 x ^ (y ^ (z v (u v (x ^ (y v v))))) = x ^ y. [para(68(a,1),242(a,1,2)),demod(11(6),12(6),68(9))]. given #575 (F,wt=17): 953 (x v (y ^ z)) ^ (u ^ (z ^ y)) = u ^ (z ^ y). [para(278(a,1),242(a,1,1,2))]. given #576 (T,wt=17): 964 (x v (y v (z v (u v v)))) ^ (v v z) = v v z. [para(102(a,1),242(a,1,2)),demod(102(10))]. given #577 (A,wt=19): 272 (x ^ y) v (z v (y ^ (u v x))) = z v (y ^ (u v x)). [para(66(a,1),120(a,1,1))]. given #578 (F,wt=17): 1004 (x v (y v z)) ^ ((z v y) ^ u) = (z v y) ^ u. [para(258(a,1),12(a,1,1)),flip(a)]. given #579 (F,wt=17): 1006 (x v (y v z)) ^ (u ^ (z v y)) = u ^ (z v y). [para(258(a,1),18(a,1,2)),flip(a)]. given #580 (F,wt=17): 1014 (x v (y v (z v (u v v)))) ^ (u v z) = u v z. [para(258(a,1),81(a,2)),demod(10(5),10(4),1006(9))]. given #581 (F,wt=17): 1023 x v (y v (z ^ (u ^ ((x ^ v) v y)))) = x v y. [para(23(a,1),259(a,1,2)),demod(9(6),10(6),23(9))]. given #582 (T,wt=17): 1027 x v (y v (z ^ (u ^ ((v ^ x) v y)))) = x v y. [para(48(a,1),259(a,1,2)),demod(9(6),10(6),48(9))]. given #583 (A,wt=19): 273 (x ^ y) v (z v (x ^ (y v u))) = z v (x ^ (y v u)). [para(68(a,1),120(a,1,1))]. given #584 (F,wt=17): 1028 x v (y v (z ^ (u ^ (x v (y ^ v))))) = x v y. [para(52(a,1),259(a,1,2)),demod(9(6),10(6),52(9))]. given #585 (F,wt=17): 1029 x v (y v (z ^ (u ^ (x v (v ^ y))))) = x v y. [para(54(a,1),259(a,1,2)),demod(9(6),10(6),54(9))]. given #586 (F,wt=17): 1059 (x ^ y) v ((y ^ (x ^ z)) v u) = (y ^ x) v u. [para(275(a,1),10(a,1,1)),flip(a)]. given #587 (F,wt=17): 1062 (x ^ y) v (z v (y ^ (x ^ u))) = z v (y ^ x). [para(275(a,1),17(a,1,2)),flip(a)]. given #588 (T,wt=17): 1065 ((x v y) ^ z) v (z ^ (u ^ x)) = z ^ (x v y). [para(92(a,1),275(a,1,2,2))]. given #589 (A,wt=19): 277 (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 #590 (F,wt=17): 1066 ((x v y) ^ z) v (z ^ (u ^ y)) = z ^ (x v y). [para(112(a,1),275(a,1,2,2))]. given #591 (F,wt=17): 1067 (x ^ y) v (y ^ ((x ^ z) v (x ^ u))) = y ^ x. [para(29(a,1),275(a,1,2,2))]. given #592 (F,wt=17): 1070 ((x v y) ^ z) v (z ^ (y v x)) = z ^ (x v y). [para(101(a,1),275(a,1,2,2))]. given #593 (F,wt=17): 1072 (x v (y ^ z)) ^ ((z ^ y) v x) = (z ^ y) v x. [para(275(a,1),241(a,1,1,2))]. given #594 (T,wt=17): 1077 (x ^ y) v ((y ^ (z ^ x)) v u) = (x ^ y) v u. [para(276(a,1),10(a,1,1)),flip(a)]. given #595 (A,wt=19): 279 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(18(a,1),26(a,1,1)),demod(12(4))]. given #596 (F,wt=17): 1081 x ^ (y ^ (z ^ (u v (z ^ x)))) = x ^ (y ^ z). [para(276(a,1),45(a,1,2,2)),demod(12(5),12(4))]. given #597 (F,wt=17): 1099 (x ^ (y ^ z)) v (u v (z ^ x)) = u v (z ^ x). [para(276(a,1),62(a,1,2,2)),demod(276(9))]. given #598 (F,wt=17): 1113 (x ^ (y ^ (z ^ (u ^ v)))) v (u ^ y) = u ^ y. [para(276(a,1),225(a,1,2)),demod(12(3),12(2),276(10))]. given #599 (F,wt=17): 1115 (x ^ (y ^ (z ^ (u ^ v)))) v (v ^ z) = v ^ z. [para(276(a,1),259(a,1,2)),demod(276(10))]. given #600 (T,wt=17): 1125 x ^ (y ^ ((y ^ (z v (y ^ x))) v u)) = x ^ y. [para(290(a,1),92(a,1,2)),demod(11(6),12(6),290(10))]. given #601 (A,wt=19): 281 x ^ (y ^ (z ^ (u v (v v (x ^ y))))) = x ^ (y ^ z). [para(26(a,1),63(a,1,2,2,2)),demod(12(6),12(5))]. given #602 (F,wt=17): 1126 x ^ (y ^ (z v (y ^ (u v (y ^ x))))) = x ^ y. [para(290(a,1),112(a,1,2)),demod(11(6),12(6),290(10))]. given #603 (F,wt=17): 1128 x ^ (y ^ (z v (y ^ (u v (v v x))))) = x ^ y. [para(290(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #604 (F,wt=17): 1133 x ^ (y ^ (z v (y ^ (u v (x v v))))) = x ^ y. [para(290(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #605 (F,wt=17): 1153 (x ^ (y ^ z)) v ((y ^ x) v u) = (x ^ y) v u. [para(292(a,1),10(a,1,1)),flip(a)]. given #606 (T,wt=17): 1158 (x ^ (y ^ z)) v ((z v u) ^ x) = x ^ (z v u). [para(92(a,1),292(a,1,1,2))]. given #607 (A,wt=19): 295 x ^ (y ^ (z ^ (u v (x ^ (y ^ z))))) = x ^ (y ^ z). [para(47(a,1),12(a,1)),demod(12(2),12(4)),flip(a)]. given #608 (F,wt=17): 1159 (x ^ (y ^ z)) v ((u v z) ^ x) = x ^ (u v z). [para(112(a,1),292(a,1,1,2))]. given #609 (F,wt=17): 1160 (x ^ ((y ^ z) v (y ^ u))) v (y ^ x) = x ^ y. [para(29(a,1),292(a,1,1,2))]. given #610 (F,wt=17): 1162 (x ^ (y v z)) v ((z v y) ^ x) = x ^ (z v y). [para(101(a,1),292(a,1,1,2))]. given #611 (F,wt=17): 1168 (x ^ (y ^ z)) v ((z ^ y) v u) = (z ^ y) v u. [para(294(a,1),10(a,1,1)),flip(a)]. given #612 (T,wt=17): 1171 (x ^ (y ^ z)) v (u v (z ^ y)) = u v (z ^ y). [para(294(a,1),17(a,1,2)),flip(a)]. given #613 (A,wt=19): 296 (x ^ y) v (y ^ (z v (x ^ y))) = y ^ (z v (x ^ y)). [para(47(a,1),25(a,1,2)),demod(9(5))]. given #614 (F,wt=17): 1181 (x ^ (y ^ (z ^ (u ^ v)))) v (u ^ z) = u ^ z. [para(294(a,1),84(a,2)),demod(12(5),12(4),1171(9))]. given #615 (F,wt=17): 1187 (x v y) ^ ((z v (y v x)) ^ u) = (x v y) ^ u. [para(317(a,1),12(a,1,1)),flip(a)]. given #616 (F,wt=17): 1194 (x v y) ^ (z v (u v (y v (x v v)))) = x v y. [para(317(a,1),83(a,2)),demod(10(6),10(5),1004(9))]. given #617 (F,wt=17): 1196 (x v (y v (z v (u v v)))) ^ (v v u) = v v u. [para(317(a,1),242(a,1,2)),demod(317(10))]. given #618 (T,wt=17): 1215 x v (y ^ ((x ^ z) v ((x ^ u) v (x ^ v)))) = x. [para(29(a,1),352(a,1,2,2,1)),demod(10(5))]. given #619 (A,wt=19): 298 x ^ (y ^ (z ^ (u v (y ^ (x ^ z))))) = x ^ (y ^ z). [para(18(a,1),47(a,1,2,2,2)),demod(12(5))]. given #620 (F,wt=17): 1221 x v (y ^ (z ^ (((x ^ u) v (x ^ v)) ^ w))) = x. [para(352(a,1),225(a,1,2)),demod(12(5),9(7),352(12))]. given #621 (F,wt=17): 1229 x ^ (((y ^ x) v (y ^ z)) ^ u) = x ^ (y ^ u). [para(359(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #622 (F,wt=17): 1232 x ^ (y ^ ((z ^ x) v (z ^ u))) = y ^ (x ^ z). [para(359(a,1),18(a,1,2)),flip(a)]. given #623 (F,wt=17): 1240 x ^ (((y v z) ^ x) v (u ^ y)) = x ^ (y v z). [para(92(a,1),359(a,1,2,2))]. given #624 (T,wt=17): 1241 x ^ (((y v z) ^ x) v (u ^ z)) = x ^ (y v z). [para(112(a,1),359(a,1,2,2))]. given #625 (A,wt=21): 299 (x ^ (y v (z ^ x))) v (u ^ (z ^ x)) = x ^ (y v (z ^ x)). [para(47(a,1),50(a,1,2,2))]. given #626 (F,wt=17): 1242 x ^ ((y ^ x) v ((y ^ z) v (y ^ u))) = x ^ y. [para(29(a,1),359(a,1,2,2))]. given #627 (F,wt=17): 1244 x ^ ((y ^ (z v (u v x))) v (y ^ v)) = x ^ y. [para(359(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #628 (F,wt=17): 1250 x ^ ((y ^ (z v (x v u))) v (y ^ v)) = x ^ y. [para(359(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #629 (F,wt=17): 1267 (x ^ y) v (z ^ (x ^ (u ^ (v ^ y)))) = x ^ y. [para(12(a,1),78(a,1,2,2,2))]. given #630 (T,wt=17): 1268 (x ^ (y v z)) v (u ^ (x ^ z)) = x ^ (y v z). [para(19(a,1),78(a,1,2,2,2))]. given #631 (A,wt=23): 300 (x ^ y) v ((y ^ (z v (x ^ y))) v u) = (y ^ (z v (x ^ y))) v u. [para(47(a,1),48(a,1,2,1)),demod(17(6))]. given #632 (F,wt=17): 1271 ((x v y) ^ z) v (x ^ (u ^ z)) = (x v y) ^ z. [para(21(a,1),78(a,1,2))]. given #633 (F,wt=17): 1274 ((x v y) ^ z) v (y ^ (u ^ z)) = (x v y) ^ z. [para(46(a,1),78(a,1,2))]. given #634 (F,wt=17): 1297 x ^ (((y ^ z) v (y ^ x)) ^ u) = x ^ (y ^ u). [para(360(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #635 (F,wt=17): 1300 x ^ (y ^ ((z ^ u) v (z ^ x))) = y ^ (x ^ z). [para(360(a,1),18(a,1,2)),flip(a)]. given #636 (T,wt=17): 1306 x ^ ((y ^ z) v ((z v u) ^ x)) = x ^ (z v u). [para(92(a,1),360(a,1,2,1))]. given #637 (A,wt=23): 301 (x ^ (y v (z ^ x))) v (u v (z ^ x)) = u v (x ^ (y v (z ^ x))). [para(47(a,1),54(a,1,2,2))]. given #638 (F,wt=17): 1307 x ^ ((y ^ z) v ((u v z) ^ x)) = x ^ (u v z). [para(112(a,1),360(a,1,2,1))]. given #639 (F,wt=17): 1308 x ^ ((y ^ z) v ((y ^ u) v (y ^ x))) = x ^ y. [para(29(a,1),360(a,1,2,1)),demod(10(5))]. given #640 (F,wt=17): 1310 x ^ ((y ^ z) v (y ^ (u v (v v x)))) = x ^ y. [para(360(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #641 (F,wt=17): 1314 x ^ ((y ^ z) v (y ^ (u v (x v v)))) = x ^ y. [para(360(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #642 (T,wt=17): 1328 (x ^ y) v ((z ^ (y ^ x)) v u) = (x ^ y) v u. [para(410(a,1),10(a,1,1)),flip(a)]. given #643 (A,wt=23): 302 (x ^ (y v (z ^ x))) v (u ^ (v ^ (z ^ x))) = x ^ (y v (z ^ x)). [para(47(a,1),76(a,1,2,2,2))]. given #644 (F,wt=17): 1336 (x ^ y) v (z ^ (u ^ (y ^ (x ^ v)))) = x ^ y. [para(410(a,1),88(a,2)),demod(12(6),12(5),1168(9))]. given #645 (F,wt=17): 1339 (x ^ (y ^ (z ^ (u ^ v)))) v (v ^ u) = v ^ u. [para(410(a,1),259(a,1,2)),demod(410(10))]. given #646 (F,wt=17): 1342 (x v (y v z)) ^ ((z v x) ^ u) = (z v x) ^ u. [para(624(a,1),12(a,1,1)),flip(a)]. given #647 (F,wt=17): 1367 (x v y) ^ (z v (y v (u v (x v v)))) = x v y. [back_demod(654),demod(1342(9))]. given #648 (T,wt=17): 1368 (x ^ (y ^ z)) v ((z ^ x) v u) = (z ^ x) v u. [para(1076(a,1),10(a,1,1)),flip(a)]. given #649 (A,wt=23): 305 (x ^ y) v (z v (y ^ (u v (x ^ y)))) = z v (y ^ (u v (x ^ y))). [para(47(a,1),120(a,1,1))]. given #650 (F,wt=17): 1394 (x ^ y) v (z ^ (y ^ (u ^ (x ^ v)))) = x ^ y. [back_demod(1106),demod(1368(9))]. given #651 (F,wt=17): 1395 x v ((y ^ ((z ^ x) v (x ^ u))) v v) = x v v. [para(1198(a,1),10(a,1,1)),flip(a)]. given #652 (F,wt=17): 1401 x v (y v (z ^ (x v ((x v y) ^ u)))) = x v y. [para(13(a,1),1198(a,1,2,2,1)),demod(10(6))]. given #653 (F,wt=17): 1403 x v (y v (z ^ ((u ^ x) v (x ^ v)))) = y v x. [para(1198(a,1),17(a,1,2)),flip(a)]. given #654 (T,wt=17): 1425 x v (y ^ ((z ^ x) v ((x ^ u) v (x ^ v)))) = x. [para(29(a,1),1198(a,1,2,2,2))]. given #655 (A,wt=19): 306 x v (y v (z v (u ^ (x v (y v z))))) = x v (y v z). [para(49(a,1),10(a,1)),demod(10(2),10(4)),flip(a)]. given #656 (F,wt=17): 1427 (x ^ ((y ^ z) v (z ^ u))) v (v v z) = v v z. [para(1198(a,1),62(a,1,2,2)),demod(1198(11))]. given #657 (F,wt=17): 1432 x v (y ^ (z ^ (((u ^ x) v (x ^ v)) ^ w))) = x. [para(1198(a,1),225(a,1,2)),demod(12(5),9(7),1198(12))]. given #658 (F,wt=17): 1436 x v (y ^ (z ^ (u ^ ((v ^ x) v (x ^ w))))) = x. [para(1198(a,1),259(a,1,2)),demod(9(7),1198(12))]. given #659 (F,wt=17): 1441 ((x ^ y) v z) ^ (x v (z v u)) = (x ^ y) v z. [para(23(a,1),79(a,1,2))]. given #660 (T,wt=17): 1442 ((x ^ y) v z) ^ (y v (z v u)) = (x ^ y) v z. [para(48(a,1),79(a,1,2))]. given #661 (A,wt=19): 307 (x v y) ^ (y v (z ^ (x v y))) = y v (z ^ (x v y)). [para(49(a,1),19(a,1,2)),demod(11(5))]. given #662 (F,wt=17): 1444 ((x ^ y) v z) ^ (u v (z v x)) = (x ^ y) v z. [para(99(a,1),79(a,1,2,2))]. given #663 (F,wt=17): 1446 ((x ^ y) v z) ^ (u v (z v y)) = (x ^ y) v z. [para(120(a,1),79(a,1,2,2))]. given #664 (F,wt=17): 1460 x v ((y ^ ((x ^ z) v (u ^ x))) v v) = x v v. [para(1199(a,1),10(a,1,1)),flip(a)]. given #665 (F,wt=17): 1466 x v (y v (z ^ ((x ^ u) v (v ^ x)))) = y v x. [para(1199(a,1),17(a,1,2)),flip(a)]. given #666 (T,wt=17): 1480 x v (y ^ ((x ^ z) v ((x ^ u) v (v ^ x)))) = x. [para(29(a,1),1199(a,1,2,2,1)),demod(10(5))]. given #667 (A,wt=19): 309 x v (y v (z v (u ^ (y v (x v z))))) = x v (y v z). [para(17(a,1),49(a,1,2,2,2)),demod(10(5))]. given #668 (F,wt=17): 1482 (x ^ ((y ^ z) v (u ^ y))) v (v v y) = v v y. [para(1199(a,1),62(a,1,2,2)),demod(1199(11))]. given #669 (F,wt=17): 1487 x v (y ^ (z ^ (((x ^ u) v (v ^ x)) ^ w))) = x. [para(1199(a,1),225(a,1,2)),demod(12(5),9(7),1199(12))]. given #670 (F,wt=17): 1489 x v (y ^ (z ^ (u ^ ((x ^ v) v (w ^ x))))) = x. [para(1199(a,1),259(a,1,2)),demod(9(7),1199(12))]. given #671 (F,wt=17): 1491 x v ((((x ^ y) v (x ^ z)) ^ u) v v) = x v v. [para(1200(a,1),10(a,1,1)),flip(a)]. given #672 (T,wt=17): 1495 x v (y v (((x ^ z) v (x ^ u)) ^ v)) = y v x. [para(1200(a,1),17(a,1,2)),flip(a)]. given #673 (A,wt=21): 310 (x v (y ^ (z v x))) ^ (u v (z v x)) = x v (y ^ (z v x)). [para(49(a,1),45(a,1,2,2))]. given #674 (F,wt=17): 1506 x v (((x ^ y) v ((x ^ z) v (x ^ u))) ^ v) = x. [para(29(a,1),1200(a,1,2,1,1)),demod(10(5))]. given #675 (F,wt=17): 1509 (((x ^ y) v (x ^ z)) ^ u) v (v v x) = v v x. [para(1200(a,1),62(a,1,2,2)),demod(1200(11))]. given #676 (F,wt=17): 1521 x ^ (((x ^ y) v (y ^ z)) ^ u) = x ^ (y ^ u). [para(1227(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #677 (F,wt=17): 1524 x ^ (y ^ ((x ^ z) v (z ^ u))) = y ^ (x ^ z). [para(1227(a,1),18(a,1,2)),flip(a)]. given #678 (T,wt=17): 1529 x ^ ((x ^ (y v z)) v (u ^ y)) = x ^ (y v z). [para(92(a,1),1227(a,1,2,2))]. given #679 (A,wt=23): 311 (x v y) ^ ((y v (z ^ (x v y))) ^ u) = (y v (z ^ (x v y))) ^ u. [para(49(a,1),46(a,1,2,1)),demod(18(6))]. given #680 (F,wt=17): 1530 x ^ ((x ^ (y v z)) v (u ^ z)) = x ^ (y v z). [para(112(a,1),1227(a,1,2,2))]. given #681 (F,wt=17): 1531 x ^ ((x ^ y) v ((y ^ z) v (y ^ u))) = x ^ y. [para(29(a,1),1227(a,1,2,2))]. given #682 (F,wt=17): 1533 x ^ (((y v (z v x)) ^ u) v (u ^ v)) = x ^ u. [para(1227(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #683 (F,wt=17): 1534 x ^ (((y v (x v z)) ^ u) v (u ^ v)) = x ^ u. [para(1227(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #684 (T,wt=17): 1544 x ^ (((y ^ x) v (z ^ y)) ^ u) = x ^ (y ^ u). [para(1228(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #685 (A,wt=23): 312 (x v (y ^ (z v x))) ^ (u v (v v (z v x))) = x v (y ^ (z v x)). [para(49(a,1),63(a,1,2,2,2))]. given #686 (F,wt=17): 1550 x ^ (y ^ ((z ^ x) v (u ^ z))) = y ^ (x ^ z). [para(1228(a,1),18(a,1,2)),flip(a)]. given #687 (F,wt=17): 1567 x ^ ((y ^ (z v (u v x))) v (v ^ y)) = x ^ y. [para(1228(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #688 (F,wt=17): 1574 x ^ ((y ^ (z v (x v u))) v (v ^ y)) = x ^ y. [para(1228(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #689 (F,wt=17): 1603 x ^ (((y ^ z) v (z ^ x)) ^ u) = x ^ (z ^ u). [para(1295(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #690 (T,wt=17): 1606 x ^ (y ^ ((z ^ u) v (u ^ x))) = y ^ (x ^ u). [para(1295(a,1),18(a,1,2)),flip(a)]. given #691 (A,wt=23): 313 (x v (y ^ (z v x))) ^ (u ^ (z v x)) = (x v (y ^ (z v x))) ^ u. [para(49(a,1),66(a,1,2,2))]. given #692 (F,wt=17): 1614 x ^ ((y ^ z) v (z ^ (u v (v v x)))) = x ^ z. [para(1295(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #693 (F,wt=17): 1617 x ^ ((y ^ z) v (z ^ (u v (x v v)))) = x ^ z. [para(1295(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #694 (F,wt=17): 1647 x ^ (((y ^ z) v (x ^ y)) ^ u) = x ^ (y ^ u). [para(1296(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #695 (F,wt=17): 1650 x ^ (y ^ ((z ^ u) v (x ^ z))) = y ^ (x ^ z). [para(1296(a,1),18(a,1,2)),flip(a)]. given #696 (T,wt=17): 1655 x ^ ((y ^ z) v (x ^ (z v u))) = x ^ (z v u). [para(92(a,1),1296(a,1,2,1))]. given #697 (A,wt=23): 315 (x v y) ^ (z ^ (y v (u ^ (x v y)))) = z ^ (y v (u ^ (x v y))). [para(49(a,1),112(a,1,1))]. given #698 (F,wt=17): 1656 x ^ ((y ^ z) v (x ^ (u v z))) = x ^ (u v z). [para(112(a,1),1296(a,1,2,1))]. given #699 (F,wt=17): 1657 x ^ ((y ^ z) v ((y ^ u) v (x ^ y))) = x ^ y. [para(29(a,1),1296(a,1,2,1)),demod(10(5))]. given #700 (F,wt=17): 1659 x ^ ((y ^ z) v ((u v (v v x)) ^ y)) = x ^ y. [para(1296(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #701 (F,wt=17): 1660 x ^ ((y ^ z) v ((u v (x v v)) ^ y)) = x ^ y. [para(1296(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #702 (T,wt=17): 1670 x v ((y ^ ((z ^ x) v (u ^ x))) v v) = x v v. [para(1397(a,1),10(a,1,1)),flip(a)]. given #703 (A,wt=19): 318 (x v (y v z)) ^ (x v (y v (u v z))) = x v (y v z). [para(10(a,1),53(a,1,1)),demod(10(5),10(8))]. given #704 (F,wt=17): 1674 x v (y v (z ^ (x v (u ^ (x v y))))) = x v y. [para(13(a,1),1397(a,1,2,2,1)),demod(10(6))]. given #705 (F,wt=17): 1676 x v (y v (z ^ ((u ^ x) v (v ^ x)))) = y v x. [para(1397(a,1),17(a,1,2)),flip(a)]. given #706 (F,wt=17): 1698 (x ^ ((y ^ z) v (u ^ z))) v (v v z) = v v z. [para(1397(a,1),62(a,1,2,2)),demod(1397(11))]. given #707 (F,wt=17): 1702 x v (y ^ (z ^ (((u ^ x) v (v ^ x)) ^ w))) = x. [para(1397(a,1),225(a,1,2)),demod(12(5),9(7),1397(12))]. given #708 (T,wt=17): 1703 x v (y ^ (z ^ (u ^ ((v ^ x) v (w ^ x))))) = x. [para(1397(a,1),259(a,1,2)),demod(9(7),1397(12))]. given #709 (A,wt=19): 320 (x v (y v z)) ^ (y v (u v (x v z))) = y v (x v z). [para(17(a,1),53(a,1,1))]. given #710 (F,wt=17): 1705 x v ((((y ^ x) v (x ^ z)) ^ u) v v) = x v v. [para(1398(a,1),10(a,1,1)),flip(a)]. given #711 (F,wt=17): 1708 x v (y v ((x v ((x v y) ^ z)) ^ u)) = x v y. [para(13(a,1),1398(a,1,2,1,1)),demod(10(6))]. given #712 (F,wt=17): 1710 x v (y v (((z ^ x) v (x ^ u)) ^ v)) = y v x. [para(1398(a,1),17(a,1,2)),flip(a)]. given #713 (F,wt=17): 1727 x v (((y ^ x) v ((x ^ z) v (x ^ u))) ^ v) = x. [para(29(a,1),1398(a,1,2,1,2))]. given #714 (T,wt=17): 1729 (((x ^ y) v (y ^ z)) ^ u) v (v v y) = v v y. [para(1398(a,1),62(a,1,2,2)),demod(1398(11))]. given #715 (A,wt=19): 321 (x v y) ^ (x v (z ^ (u ^ y))) = x v (z ^ (u ^ y)). [para(50(a,1),53(a,1,2,2)),demod(11(5))]. given #716 (F,wt=17): 1738 x v ((((x ^ y) v (z ^ x)) ^ u) v v) = x v v. [para(1462(a,1),10(a,1,1)),flip(a)]. given #717 (F,wt=17): 1742 x v (y v (((x ^ z) v (u ^ x)) ^ v)) = y v x. [para(1462(a,1),17(a,1,2)),flip(a)]. given #718 (F,wt=17): 1752 x v (((x ^ y) v ((x ^ z) v (u ^ x))) ^ v) = x. [para(29(a,1),1462(a,1,2,1,1)),demod(10(5))]. given #719 (F,wt=17): 1754 (((x ^ y) v (z ^ x)) ^ u) v (v v x) = v v x. [para(1462(a,1),62(a,1,2,2)),demod(1462(11))]. given #720 (T,wt=17): 1760 x ^ (((x ^ y) v (z ^ y)) ^ u) = x ^ (y ^ u). [para(1520(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #721 (A,wt=19): 322 (x v y) ^ (x v (z ^ (y ^ u))) = x v (z ^ (y ^ u)). [para(69(a,1),53(a,1,2,2)),demod(11(5))]. given #722 (F,wt=17): 1765 x ^ (y ^ ((x ^ z) v (u ^ z))) = y ^ (x ^ z). [para(1520(a,1),18(a,1,2)),flip(a)]. given #723 (F,wt=17): 1781 x ^ (((y v (z v x)) ^ u) v (v ^ u)) = x ^ u. [para(1520(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #724 (F,wt=17): 1784 x ^ (((y v (x v z)) ^ u) v (v ^ u)) = x ^ u. [para(1520(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #725 (F,wt=17): 1814 x ^ (((y ^ z) v (x ^ z)) ^ u) = x ^ (z ^ u). [para(1602(a,1),12(a,1,1)),demod(12(2)),flip(a)]. given #726 (T,wt=17): 1816 x ^ (y ^ ((z ^ u) v (x ^ u))) = y ^ (x ^ u). [para(1602(a,1),18(a,1,2)),flip(a)]. given #727 (A,wt=21): 323 (x v (y v z)) ^ (x v ((y ^ u) v z)) = x v ((y ^ u) v z). [para(23(a,1),53(a,1,2,2)),demod(11(6))]. given #728 (F,wt=17): 1822 x ^ ((y ^ z) v ((u v (v v x)) ^ z)) = x ^ z. [para(1602(a,1),64(a,1,2)),demod(64(4)),flip(a)]. given #729 (F,wt=17): 1823 x ^ ((y ^ z) v ((u v (x v v)) ^ z)) = x ^ z. [para(1602(a,1),81(a,1,2)),demod(81(4)),flip(a)]. given #730 (F,wt=17): 1831 x v ((((y ^ x) v (z ^ x)) ^ u) v v) = x v v. [para(1672(a,1),10(a,1,1)),flip(a)]. given #731 (F,wt=17): 1833 x v (y v ((x v (z ^ (x v y))) ^ u)) = x v y. [para(13(a,1),1672(a,1,2,1,1)),demod(10(6))]. given #732 (T,wt=17): 1835 x v (y v (((z ^ x) v (u ^ x)) ^ v)) = y v x. [para(1672(a,1),17(a,1,2)),flip(a)]. given #733 (A,wt=21): 324 (x v (y v z)) ^ (x v ((u ^ y) v z)) = x v ((u ^ y) v z). [para(48(a,1),53(a,1,2,2)),demod(11(6))]. given #734 (F,wt=17): 1852 (((x ^ y) v (z ^ y)) ^ u) v (v v y) = v v y. [para(1672(a,1),62(a,1,2,2)),demod(1672(11))]. given #735 (F,wt=17): 1858 ((x v y) ^ z) v (x ^ (z ^ u)) = (x v y) ^ z. [para(21(a,1),86(a,1,2))]. given #736 (F,wt=17): 1859 ((x v y) ^ z) v (y ^ (z ^ u)) = (x v y) ^ z. [para(46(a,1),86(a,1,2))]. given #737 (F,wt=17): 1861 ((x v y) ^ z) v (u ^ (z ^ x)) = (x v y) ^ z. [para(92(a,1),86(a,1,2,2))]. given #738 (T,wt=17): 1863 ((x v y) ^ z) v (u ^ (z ^ y)) = (x v y) ^ z. [para(112(a,1),86(a,1,2,2))]. given #739 (A,wt=21): 325 (x v (y v z)) ^ (x v (y v (z ^ u))) = x v (y v (z ^ u)). [para(52(a,1),53(a,1,2,2)),demod(11(6))]. given #740 (F,wt=17): 1879 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(13(a,1),91(a,1,1))]. given #741 (F,wt=17): 1880 x v ((x v y) ^ (z v x)) = (x v y) ^ (z v x). [para(19(a,1),91(a,1,1))]. given #742 (F,wt=17): 1886 (x ^ (y ^ z)) v ((x v u) ^ y) = (x v u) ^ y. [para(91(a,1),23(a,2)),demod(12(3),262(7))]. given #743 (F,wt=17): 1893 (x ^ (y ^ z)) v ((u v x) ^ z) = (u v x) ^ z. [para(99(a,1),91(a,1,2,1)),demod(12(2),99(8))]. given #744 (T,wt=17): 1894 (x ^ (y ^ z)) v ((u v y) ^ z) = (u v y) ^ z. [para(120(a,1),91(a,1,2,1)),demod(12(2),120(8))]. given #745 (A,wt=21): 326 (x v (y v z)) ^ (x v (y v (u ^ z))) = x v (y v (u ^ z)). [para(54(a,1),53(a,1,2,2)),demod(11(6))]. given #746 (F,wt=17): 1908 (x ^ (y ^ z)) v (y ^ (x ^ z)) = y ^ (x ^ z). [para(275(a,1),91(a,1,2,1)),demod(12(2),12(4),275(9),12(7))]. given #747 (F,wt=17): 1939 (x ^ (y v z)) v (x ^ (y ^ u)) = x ^ (y v z). [para(93(a,1),86(a,1,2))]. given #748 (F,wt=17): 1994 (x v (y v z)) ^ ((x ^ u) v y) = (x ^ u) v y. [para(97(a,1),21(a,2)),demod(10(3),247(7))]. given #749 (F,wt=17): 2000 (x v (y v z)) ^ ((u ^ x) v z) = (u ^ x) v z. [para(92(a,1),97(a,1,2,1)),demod(10(2),92(8))]. given #750 (T,wt=17): 2001 (x v (y v z)) ^ ((u ^ y) v z) = (u ^ y) v z. [para(112(a,1),97(a,1,2,1)),demod(10(2),112(8))]. given #751 (A,wt=19): 327 x v (y v (z v (u ^ (v ^ (x v z))))) = x v (y v z). [para(53(a,1),76(a,1,2,2,2)),demod(10(6),10(5))]. given #752 (F,wt=17): 2007 (x v (y v z)) ^ (y v (x v z)) = y v (x v z). [para(101(a,1),97(a,1,2,1)),demod(10(2),10(4),101(9),10(7))]. given #753 (F,wt=17): 2047 (x v (y ^ z)) ^ (x v (y v u)) = x v (y ^ z). [para(98(a,1),79(a,1,2))]. given #754 (F,wt=17): 2050 (x v y) ^ (x v (z v (u v (y v v)))) = x v y. [para(10(a,1),105(a,1,2,2))]. given #755 (F,wt=17): 2054 (x v (y ^ z)) ^ (x v (z v u)) = x v (y ^ z). [para(48(a,1),105(a,1,2,2))]. given #756 (T,wt=17): 2059 (x v y) ^ (x v (z v (u v (v v y)))) = x v y. [para(62(a,1),105(a,1,2,2,2))]. given #757 (A,wt=23): 328 (x v y) ^ (x v (z ^ (u ^ (v ^ y)))) = x v (z ^ (u ^ (v ^ y))). [para(76(a,1),53(a,1,2,2)),demod(11(6))]. given #758 (F,wt=17): 2082 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(13(a,1),110(a,1,1))]. given #759 (F,wt=17): 2083 x v ((y v x) ^ (z v x)) = (y v x) ^ (z v x). [para(19(a,1),110(a,1,1))]. given #760 (F,wt=17): 2090 (x ^ (y ^ z)) v ((u v x) ^ y) = (u v x) ^ y. [para(110(a,1),23(a,2)),demod(12(3),266(7))]. given #761 (F,wt=17): 2130 (x v (y v z)) ^ ((y ^ u) v z) = (y ^ u) v z. [para(97(a,1),110(a,1,1)),demod(25(8)),flip(a)]. given #762 (T,wt=17): 2149 x ^ (y ^ (z v (u v (x ^ (v v y))))) = y ^ x. [para(65(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #763 (A,wt=23): 329 (x v y) ^ (x v (z ^ (u ^ (y ^ v)))) = x v (z ^ (u ^ (y ^ v))). [para(87(a,1),53(a,1,2,2)),demod(11(6))]. given #764 (F,wt=17): 2162 x ^ (y ^ (z v ((x ^ (u v y)) v v))) = y ^ x. [para(82(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #765 (F,wt=17): 2163 (x ^ (y v z)) v (x ^ (z ^ u)) = x ^ (y v z). [para(113(a,1),86(a,1,2))]. given #766 (F,wt=17): 2167 x ^ (((x ^ y) v z) ^ (u ^ y)) = x ^ (u ^ y). [para(39(a,1),90(a,2,2)),demod(58(5))]. given #767 (F,wt=17): 2183 x ^ (((y ^ x) v z) ^ (u ^ y)) = x ^ (u ^ y). [para(58(a,1),90(a,2)),demod(183(6))]. given #768 (T,wt=17): 2232 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(14(a,1),118(a,1,1))]. given #769 (A,wt=25): 330 (x v (y v z)) ^ (x v (z v ((y v z) ^ u))) = x v (z v ((y v z) ^ u)). [para(24(a,1),53(a,1,2,2)),demod(11(7))]. given #770 (F,wt=17): 2233 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(25(a,1),118(a,1,1))]. given #771 (F,wt=17): 2239 (x v (y v z)) ^ ((u ^ x) v y) = (u ^ x) v y. [para(118(a,1),21(a,2)),demod(10(3),249(7))]. given #772 (F,wt=17): 2287 (x ^ (y ^ z)) v ((y v u) ^ z) = (y v u) ^ z. [para(91(a,1),118(a,1,1)),demod(19(8)),flip(a)]. given #773 (F,wt=17): 2355 (x v (y v z)) ^ (x v (y ^ u)) = x v (y ^ u). [para(130(a,1),21(a,2)),demod(10(3),250(7))]. given #774 (T,wt=17): 2360 (x v (y v z)) ^ (x v (u ^ y)) = x v (u ^ y). [para(92(a,1),130(a,1,2,2)),demod(92(8))]. given #775 (A,wt=19): 331 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(24(a,1),53(a,1,2)),demod(11(5))]. given #776 (F,wt=17): 2362 (x v (y v z)) ^ (x v (u ^ z)) = x v (u ^ z). [para(112(a,1),130(a,1,2,2)),demod(112(8))]. given #777 (F,wt=17): 2393 (x v (y v z)) ^ (y v (z ^ u)) = y v (z ^ u). [para(130(a,1),110(a,1,1)),demod(25(8)),flip(a)]. given #778 (F,wt=17): 2412 (x ^ (y v z)) v (u ^ (y ^ x)) = (y v z) ^ x. [para(11(a,1),94(a,1,1))]. given #779 (F,wt=17): 2497 (x v (y v z)) ^ (y v (u ^ z)) = y v (u ^ z). [para(134(a,1),110(a,1,1)),demod(25(8)),flip(a)]. given #780 (T,wt=17): 2608 x ^ (y ^ (((x v z) ^ (y v u)) v v)) = x ^ y. [para(159(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #781 (A,wt=21): 332 (x v (y ^ z)) ^ (x v (y ^ (z ^ u))) = x v (y ^ (z ^ u)). [para(26(a,1),53(a,1,2,2)),demod(11(6))]. given #782 (F,wt=17): 2612 x ^ (y ^ (((x v z) ^ (u v y)) v v)) = y ^ x. [para(159(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #783 (F,wt=17): 2618 x ^ (((x v y) ^ (z v (u v (v v x)))) v w) = x. [para(159(a,1),142(a,1)),demod(63(4)),flip(a)]. given #784 (F,wt=17): 2621 x ^ ((((x v y) ^ (x v z)) v u) ^ v) = x ^ v. [para(2576(a,1),12(a,1,1)),flip(a)]. given #785 (F,wt=17): 2626 x ^ (y ^ (((x v z) ^ (x v u)) v v)) = y ^ x. [para(2576(a,1),18(a,1,2)),flip(a)]. given #786 (T,wt=17): 2637 (((x v y) ^ (x v z)) v u) ^ (v ^ x) = v ^ x. [para(2576(a,1),58(a,1,2,2)),demod(2576(11))]. given #787 (A,wt=25): 334 (x v (y v z)) ^ (x v (z v (u ^ (y v z)))) = x v (z v (u ^ (y v z))). [para(49(a,1),53(a,1,2,2)),demod(11(7))]. given #788 (F,wt=17): 2643 x ^ (y v (z v (((x v u) ^ (x v v)) v w))) = x. [para(2576(a,1),242(a,1,2)),demod(11(7),2576(12))]. given #789 (F,wt=17): 2648 x ^ (y ^ ((x ^ ((x ^ y) v z)) v u)) = x ^ y. [para(360(a,1),2576(a,1,2,1)),demod(11(4),12(6))]. given #790 (F,wt=17): 2661 x v (((x v y) ^ z) v (u v y)) = x v (u v y). [para(44(a,1),95(a,2,2)),demod(62(5))]. given #791 (F,wt=17): 2674 x v (((y v x) ^ z) v (u v y)) = x v (u v y). [para(62(a,1),95(a,2)),demod(144(6))]. given #792 (T,wt=17): 2716 x ^ ((((x v y) ^ (z v x)) v u) ^ v) = x ^ v. [para(2577(a,1),12(a,1,1)),flip(a)]. given #793 (A,wt=19): 335 (x v y) ^ (x v (z ^ (x v y))) = x v (z ^ (x v y)). [para(49(a,1),53(a,1,2)),demod(11(5))]. given #794 (F,wt=17): 2722 x ^ (y ^ (((x v z) ^ (u v x)) v v)) = y ^ x. [para(2577(a,1),18(a,1,2)),flip(a)]. given #795 (F,wt=17): 2737 (((x v y) ^ (z v x)) v u) ^ (v ^ x) = v ^ x. [para(2577(a,1),58(a,1,2,2)),demod(2577(11))]. given #796 (F,wt=17): 2744 x ^ (y v (z v (((x v u) ^ (v v x)) v w))) = x. [para(2577(a,1),242(a,1,2)),demod(11(7),2577(12))]. given #797 (F,wt=17): 2758 x ^ ((((y v x) ^ (x v z)) v u) ^ v) = x ^ v. [para(2619(a,1),12(a,1,1)),flip(a)]. given #798 (T,wt=17): 2764 x ^ (y ^ (((z v x) ^ (x v u)) v v)) = y ^ x. [para(2619(a,1),18(a,1,2)),flip(a)]. given #799 (A,wt=21): 336 x ^ ((y ^ (z v x)) v (z ^ (x v y))) = (x ^ z) v (x ^ y). [para(9(a,1),29(a,1,2,1,2))]. given #800 (F,wt=17): 2773 (((x v y) ^ (y v z)) v u) ^ (v ^ y) = v ^ y. [para(2619(a,1),58(a,1,2,2)),demod(2619(11))]. given #801 (F,wt=17): 2779 x ^ (y v (z v (((u v x) ^ (x v v)) v w))) = x. [para(2619(a,1),242(a,1,2)),demod(11(7),2619(12))]. given #802 (F,wt=17): 2781 x ^ (y ^ ((x ^ (z v (x ^ y))) v u)) = x ^ y. [para(360(a,1),2619(a,1,2,1)),demod(11(4),12(6))]. given #803 (F,wt=17): 2790 x ^ ((y v ((x v z) ^ (x v u))) ^ v) = x ^ v. [para(2620(a,1),12(a,1,1)),flip(a)]. given #804 (T,wt=17): 2795 x ^ (y ^ (z v ((x v u) ^ (x v v)))) = y ^ x. [para(2620(a,1),18(a,1,2)),flip(a)]. given #805 (A,wt=21): 337 x ^ ((y ^ (x v z)) v (z ^ (y v x))) = (x ^ z) v (x ^ y). [para(9(a,1),29(a,1,2,2,2))]. given #806 (F,wt=17): 2803 (x v ((y v z) ^ (y v u))) ^ (v ^ y) = v ^ y. [para(2620(a,1),58(a,1,2,2)),demod(2620(11))]. given #807 (F,wt=17): 2809 x ^ (y v (z v (u v ((x v v) ^ (x v w))))) = x. [para(2620(a,1),242(a,1,2)),demod(11(7),2620(12))]. given #808 (F,wt=17): 2814 x ^ (y ^ (z v (x ^ ((x ^ y) v u)))) = x ^ y. [para(360(a,1),2620(a,1,2,2)),demod(11(4),12(6))]. given #809 (F,wt=17): 2824 x ^ ((((y v x) ^ (z v x)) v u) ^ v) = x ^ v. [para(2713(a,1),12(a,1,1)),flip(a)]. given #810 (T,wt=17): 2830 x ^ (y ^ (((z v x) ^ (u v x)) v v)) = y ^ x. [para(2713(a,1),18(a,1,2)),flip(a)]. given #811 (A,wt=21): 338 x ^ ((y ^ (x v z)) v ((x v y) ^ z)) = (x ^ z) v (x ^ y). [para(11(a,1),29(a,1,2,2))]. given #812 (F,wt=17): 2844 (((x v y) ^ (z v y)) v u) ^ (v ^ y) = v ^ y. [para(2713(a,1),58(a,1,2,2)),demod(2713(11))]. given #813 (F,wt=17): 2849 x ^ (y v (z v (((u v x) ^ (v v x)) v w))) = x. [para(2713(a,1),242(a,1,2)),demod(11(7),2713(12))]. given #814 (F,wt=17): 2856 x ^ ((y v ((x v z) ^ (u v x))) ^ v) = x ^ v. [para(2714(a,1),12(a,1,1)),flip(a)]. given #815 (F,wt=17): 2861 x ^ (y ^ (z v ((x v u) ^ (v v x)))) = y ^ x. [para(2714(a,1),18(a,1,2)),flip(a)]. given #816 (T,wt=17): 2873 (x v ((y v z) ^ (u v y))) ^ (v ^ y) = v ^ y. [para(2714(a,1),58(a,1,2,2)),demod(2714(11))]. given #817 (A,wt=25): 339 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 #818 (F,wt=17): 2879 x ^ (y v (z v (u v ((x v v) ^ (w v x))))) = x. [para(2714(a,1),242(a,1,2)),demod(11(7),2714(12))]. given #819 (F,wt=17): 2945 x ^ ((y v ((z v x) ^ (x v u))) ^ v) = x ^ v. [para(2756(a,1),12(a,1,1)),flip(a)]. given #820 (F,wt=17): 2950 x ^ (y ^ (z v ((u v x) ^ (x v v)))) = y ^ x. [para(2756(a,1),18(a,1,2)),flip(a)]. given #821 (F,wt=17): 2957 (x v ((y v z) ^ (z v u))) ^ (v ^ z) = v ^ z. [para(2756(a,1),58(a,1,2,2)),demod(2756(11))]. given #822 (T,wt=17): 2962 x ^ (y v (z v (u v ((v v x) ^ (x v w))))) = x. [para(2756(a,1),242(a,1,2)),demod(11(7),2756(12))]. given #823 (A,wt=25): 347 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 #824 (F,wt=17): 2964 x ^ (y ^ (z v (x ^ (u v (x ^ y))))) = x ^ y. [para(360(a,1),2756(a,1,2,2)),demod(11(4),12(6))]. given #825 (F,wt=17): 2972 x ^ ((y v ((z v x) ^ (u v x))) ^ v) = x ^ v. [para(2823(a,1),12(a,1,1)),flip(a)]. given #826 (F,wt=17): 2977 x ^ (y ^ (z v ((u v x) ^ (v v x)))) = y ^ x. [para(2823(a,1),18(a,1,2)),flip(a)]. given #827 (F,wt=17): 2989 (x v ((y v z) ^ (u v z))) ^ (v ^ z) = v ^ z. [para(2823(a,1),58(a,1,2,2)),demod(2823(11))]. given #828 (T,wt=17): 2993 x ^ (y v (z v (u v ((v v x) ^ (w v x))))) = x. [para(2823(a,1),242(a,1,2)),demod(11(7),2823(12))]. given #829 (A,wt=19): 355 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(29(a,1),21(a,2)),demod(347(8))]. given #830 (F,wt=17): 3033 x ^ (y ^ (((z v x) ^ (y v u)) v v)) = x ^ y. [para(160(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #831 (F,wt=17): 3036 x ^ (y ^ (((z v x) ^ (u v y)) v v)) = y ^ x. [para(160(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #832 (F,wt=17): 3042 x ^ (((y v x) ^ (z v (u v (v v x)))) v w) = x. [para(160(a,1),142(a,1)),demod(63(4)),flip(a)]. given #833 (F,wt=17): 3048 (x ^ (y v z)) v (z ^ (u ^ x)) = x ^ (y v z). [para(164(a,1),50(a,1,2))]. given #834 (T,wt=17): 3071 (x ^ (y v z)) v (z ^ (x ^ u)) = x ^ (y v z). [para(164(a,1),78(a,1,2))]. given #835 (A,wt=19): 356 (x v y) ^ ((y ^ z) v (y ^ u)) = (y ^ z) v (y ^ u). [para(29(a,1),46(a,2)),demod(347(8))]. given #836 (F,wt=17): 3103 (x ^ y) v (z ^ (u ^ (v ^ (y ^ x)))) = x ^ y. [para(76(a,1),165(a,1,1,2)),demod(12(5),12(4),12(3),76(10))]. given #837 (F,wt=17): 3105 (x ^ y) v (z ^ (u ^ (y ^ (v ^ x)))) = x ^ y. [para(87(a,1),165(a,1,1,2)),demod(12(5),12(4),12(3),87(10))]. given #838 (F,wt=17): 3107 (x ^ (y ^ z)) v (y ^ (u v x)) = y ^ (u v x). [para(165(a,1),99(a,1,2)),demod(12(2),165(9))]. given #839 (F,wt=17): 3108 (x ^ (y ^ z)) v (z ^ (u v y)) = z ^ (u v y). [para(165(a,1),120(a,1,2)),demod(165(9))]. given #840 (T,wt=17): 3109 (x ^ (y ^ z)) v (z ^ (y ^ x)) = x ^ (y ^ z). [para(278(a,1),165(a,1,1,2)),demod(12(4),278(8))]. given #841 (A,wt=25): 362 (x ^ y) v (z ^ (u ^ (v ^ x))) = x ^ ((z ^ (u ^ (v ^ x))) v (y ^ x)). [para(76(a,1),29(a,1,2,2,2)),demod(12(5),12(4),12(3),13(2),183(11)),flip(a)]. given #842 (F,wt=17): 3210 x v (((y v z) ^ (y v x)) v u) = x v (y v u). [para(3119(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #843 (F,wt=17): 3225 x v ((y v z) ^ ((z ^ u) v x)) = x v (z ^ u). [para(99(a,1),3119(a,1,2,1))]. given #844 (F,wt=17): 3226 x v ((y v z) ^ ((u ^ z) v x)) = x v (u ^ z). [para(120(a,1),3119(a,1,2,1))]. given #845 (F,wt=17): 3231 x v ((y v z) ^ (y v (u ^ (v ^ x)))) = x v y. [para(3119(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #846 (T,wt=17): 3234 x v ((y v z) ^ (y v (u ^ (x ^ v)))) = x v y. [para(3119(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #847 (A,wt=25): 368 (x ^ y) v (z ^ (u ^ (x ^ v))) = x ^ ((z ^ (u ^ (v ^ x))) v (y ^ x)). [para(87(a,1),29(a,1,2,2,2)),demod(12(5),12(4),12(3),68(3),115(11)),flip(a)]. given #848 (F,wt=17): 3280 x v (((y v z) ^ (z v x)) v u) = x v (z v u). [para(3208(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #849 (F,wt=17): 3312 x v ((y v z) ^ (z v (u ^ (v ^ x)))) = x v z. [para(3208(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #850 (F,wt=17): 3318 x v ((y v z) ^ (z v (u ^ (x ^ v)))) = x v z. [para(3208(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #851 (F,wt=17): 3370 x v (((y v z) ^ (x v y)) v u) = x v (y v u). [para(3209(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #852 (T,wt=17): 3374 x v (y v ((z v u) ^ (x v z))) = y v (x v z). [para(3209(a,1),17(a,1,2)),flip(a)]. given #853 (A,wt=23): 370 (x ^ y) v ((y v z) ^ u) = (y v z) ^ ((u ^ (z v y)) v (x ^ y)). [para(92(a,1),29(a,2,1)),demod(10(4),54(4),10(6),12(7),13(6)),flip(a)]. given #854 (F,wt=17): 3379 x v ((y v z) ^ (x v (z ^ u))) = x v (z ^ u). [para(99(a,1),3209(a,1,2,1))]. given #855 (F,wt=17): 3380 x v ((y v z) ^ (x v (u ^ z))) = x v (u ^ z). [para(120(a,1),3209(a,1,2,1))]. given #856 (F,wt=17): 3382 x v ((y v z) ^ ((u ^ (v ^ x)) v y)) = x v y. [para(3209(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #857 (F,wt=17): 3383 x v ((y v z) ^ ((u ^ (x ^ v)) v y)) = x v y. [para(3209(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #858 (T,wt=17): 3399 x v (((y v x) ^ (y v z)) v u) = x v (y v u). [para(3213(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #859 (A,wt=23): 371 ((x v y) ^ z) v (u ^ x) = (x v y) ^ ((u ^ x) v (z ^ (y v x))). [para(92(a,1),29(a,2,2)),demod(10(4),12(5),13(4),10(5),54(5)),flip(a)]. given #860 (F,wt=17): 3410 x v (((y ^ z) v x) ^ (u v y)) = x v (y ^ z). [para(99(a,1),3213(a,1,2,2))]. given #861 (F,wt=17): 3411 x v (((y ^ z) v x) ^ (u v z)) = x v (y ^ z). [para(120(a,1),3213(a,1,2,2))]. given #862 (F,wt=17): 3415 x v ((y v (z ^ (u ^ x))) ^ (y v v)) = x v y. [para(3213(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #863 (F,wt=17): 3417 x v ((y v (z ^ (x ^ u))) ^ (y v v)) = x v y. [para(3213(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #864 (T,wt=17): 3453 x v (((y v z) ^ (x v z)) v u) = x v (z v u). [para(3279(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #865 (A,wt=21): 378 x ^ (y ^ ((x ^ z) v (x ^ u))) = y ^ ((x ^ z) v (x ^ u)). [para(29(a,1),56(a,1,2,2)),demod(29(11))]. given #866 (F,wt=17): 3457 x v (y v ((z v u) ^ (x v u))) = y v (x v u). [para(3279(a,1),17(a,1,2)),flip(a)]. given #867 (F,wt=17): 3473 x v ((y v z) ^ ((u ^ (v ^ x)) v z)) = x v z. [para(3279(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #868 (F,wt=17): 3476 x v ((y v z) ^ ((u ^ (x ^ v)) v z)) = x v z. [para(3279(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #869 (F,wt=17): 3517 x v (((y v x) ^ (z v y)) v u) = x v (y v u). [para(3283(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #870 (T,wt=17): 3530 x v ((y v (z ^ (u ^ x))) ^ (v v y)) = x v y. [para(3283(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #871 (A,wt=19): 385 x ^ (y ^ ((z v (u v (x ^ y))) ^ v)) = x ^ (y ^ v). [para(64(a,1),12(a,1)),demod(12(2)),flip(a)]. given #872 (F,wt=17): 3532 x v ((y v (z ^ (x ^ u))) ^ (v v y)) = x v y. [para(3283(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #873 (F,wt=17): 3576 x v (((x v y) ^ (y v z)) v u) = x v (y v u). [para(3373(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #874 (F,wt=17): 3579 x v (y v ((x v z) ^ (z v u))) = y v (x v z). [para(3373(a,1),17(a,1,2)),flip(a)]. given #875 (F,wt=17): 3584 x v ((x v (y ^ z)) ^ (u v y)) = x v (y ^ z). [para(99(a,1),3373(a,1,2,2))]. given #876 (T,wt=17): 3585 x v ((x v (y ^ z)) ^ (u v z)) = x v (y ^ z). [para(120(a,1),3373(a,1,2,2))]. given #877 (A,wt=19): 386 (x ^ y) v ((z v (u v x)) ^ y) = (z v (u v x)) ^ y. [para(64(a,1),25(a,1,2)),demod(9(5))]. given #878 (F,wt=17): 3587 x v (((y ^ (z ^ x)) v u) ^ (u v v)) = x v u. [para(3373(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #879 (F,wt=17): 3588 x v (((y ^ (x ^ z)) v u) ^ (u v v)) = x v u. [para(3373(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #880 (F,wt=17): 3603 x v (((x v y) ^ (z v y)) v u) = x v (y v u). [para(3455(a,1),10(a,1,1)),demod(10(2)),flip(a)]. given #881 (F,wt=17): 3605 x v (y v ((x v z) ^ (u v z))) = y v (x v z). [para(3455(a,1),17(a,1,2)),flip(a)]. given #882 (T,wt=17): 3610 x v (((y ^ (z ^ x)) v u) ^ (v v u)) = x v u. [para(3455(a,1),74(a,1,2)),demod(74(4)),flip(a)]. given #883 (A,wt=19): 387 (x v y) ^ ((z v (x v (u v y))) ^ v) = (x v y) ^ v. [para(17(a,1),64(a,1,2,1,2))]. given #884 (F,wt=17): 3611 x v (((y ^ (x ^ z)) v u) ^ (v v u)) = x v u. [para(3455(a,1),84(a,1,2)),demod(84(4)),flip(a)]. given #885 (F,wt=17): 3653 (x ^ (y ^ z)) v (x ^ (y v u)) = x ^ (y v u). [para(176(a,1),23(a,2)),demod(12(3),273(7))]. given #886 (F,wt=17): 3656 (x ^ (y ^ z)) v (x ^ (u v y)) = x ^ (u v y). [para(99(a,1),176(a,1,2,2)),demod(99(8))]. given #887 (F,wt=17): 3658 (x ^ (y ^ z)) v (x ^ (u v z)) = x ^ (u v z). [para(120(a,1),176(a,1,2,2)),demod(120(8))]. given #888 (T,wt=17): 3675 (x ^ (y ^ z)) v (y ^ (z v u)) = y ^ (z v u). [para(176(a,1),118(a,1,1)),demod(19(8)),flip(a)]. given #889 (A,wt=21): 389 ((x v (y v z)) ^ u) v (v ^ (z ^ u)) = (x v (y v z)) ^ u. [para(64(a,1),50(a,1,2,2))]. given #890 (F,wt=17): 3711 x v (y v (z v ((z v x) ^ u))) = x v (y v z). [para(202(a,1),104(a,1,1,2)),demod(10(6),104(9)),flip(a)]. given #891 (F,wt=17): 3718 (x ^ y) v (z v (y ^ (u ^ x))) = (x ^ y) v z. [para(276(a,1),104(a,1,1,2)),demod(101(9)),flip(a)]. given #892 (F,wt=17): 3853 x ^ (((x v y) ^ (z v (u v (x v v)))) v w) = x. [para(195(a,1),159(a,1)),demod(80(11))]. given #893 (F,wt=17): 3860 x ^ (((y v x) ^ (z v (u v (x v v)))) v w) = x. [para(195(a,1),160(a,1)),demod(80(11))]. given #894 (T,wt=17): 3989 x v (y v (((x ^ z) v (y ^ u)) ^ v)) = x v y. [para(208(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #895 (A,wt=21): 390 ((x ^ y) v z) ^ ((u v (x v z)) ^ v) = ((x ^ y) v z) ^ v. [para(23(a,1),64(a,1,2,1,2))]. given #896 (F,wt=17): 3993 x v (y v (((x ^ z) v (u ^ y)) ^ v)) = x v y. [para(208(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #897 (F,wt=17): 4016 x v (((x ^ y) v (z ^ (u ^ (v ^ x)))) ^ w) = x. [para(208(a,1),180(a,1)),demod(76(4)),flip(a)]. given #898 (F,wt=17): 4017 x v (((x ^ y) v (z ^ (u ^ (x ^ v)))) ^ w) = x. [para(208(a,1),198(a,1)),demod(87(4)),flip(a)]. given #899 (F,wt=17): 4041 x v (y v (((z ^ x) v (y ^ u)) ^ v)) = x v y. [para(210(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #900 (T,wt=17): 4044 x v (y v (((z ^ x) v (u ^ y)) ^ v)) = x v y. [para(210(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #901 (A,wt=23): 391 (x ^ y) v (((z v (u v x)) ^ y) v v) = ((z v (u v x)) ^ y) v v. [para(64(a,1),48(a,1,2,1)),demod(17(6))]. given #902 (F,wt=17): 4066 x v (((y ^ x) v (z ^ (u ^ (v ^ x)))) ^ w) = x. [para(210(a,1),180(a,1)),demod(76(4)),flip(a)]. given #903 (F,wt=17): 4067 x v (((y ^ x) v (z ^ (u ^ (x ^ v)))) ^ w) = x. [para(210(a,1),198(a,1)),demod(87(4)),flip(a)]. given #904 (F,wt=17): 4069 ((x v y) ^ z) v (z ^ (x ^ u)) = (x v y) ^ z. [para(214(a,1),26(a,1,2))]. given #905 (F,wt=17): 4119 (x ^ (y ^ z)) v (x ^ (z v u)) = (z v u) ^ x. [para(215(a,1),292(a,1,1))]. given #906 (T,wt=17): 4235 x ^ (y ^ (((y v z) ^ (u v x)) v v)) = x ^ y. [para(219(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #907 (A,wt=21): 392 ((x ^ y) v z) ^ ((u v (y v z)) ^ v) = ((x ^ y) v z) ^ v. [para(48(a,1),64(a,1,2,1,2))]. given #908 (F,wt=17): 4238 x ^ (y ^ (((z v y) ^ (u v x)) v v)) = y ^ x. [para(219(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #909 (F,wt=17): 4245 x ^ (((y v (z v (u v x))) ^ (v v x)) v w) = x. [para(219(a,1),142(a,1)),demod(63(4)),flip(a)]. given #910 (F,wt=17): 4254 x ^ (((y v (z v (x v u))) ^ (v v x)) v w) = x. [para(219(a,1),195(a,1)),demod(80(4)),flip(a)]. given #911 (F,wt=17): 4297 ((x ^ y) v z) ^ (z v (x v u)) = (x ^ y) v z. [para(221(a,1),20(a,1,2))]. given #912 (T,wt=17): 4300 (x ^ (y ^ z)) v (u v (y ^ x)) = u v (y ^ x). [para(275(a,1),221(a,1,2,2)),demod(12(2),275(9))]. given #913 (A,wt=21): 393 (x v (y ^ z)) ^ ((u v (x v y)) ^ v) = (x v (y ^ z)) ^ v. [para(52(a,1),64(a,1,2,1,2))]. given #914 (F,wt=17): 4340 ((x ^ y) v z) ^ (z v (u v x)) = (x ^ y) v z. [para(222(a,1),20(a,1,2))]. given #915 (F,wt=17): 4354 (x v (y v z)) ^ (x v (z ^ u)) = x v (z ^ u). [para(222(a,1),241(a,1,1))]. given #916 (F,wt=17): 4413 x v (y v (z ^ (u ^ ((y ^ v) v x)))) = x v y. [para(227(a,1),76(a,1,2,2,2)),demod(10(6))]. given #917 (F,wt=17): 4414 (x v (y v z)) ^ ((y ^ u) v x) = (y ^ u) v x. [para(227(a,1),92(a,1,2)),demod(10(2),227(9))]. given #918 (T,wt=17): 4415 ((x ^ y) v z) ^ (z v (y v u)) = (x ^ y) v z. [para(92(a,1),227(a,1,1,1)),demod(92(8))]. given #919 (A,wt=23): 394 ((x v (y v z)) ^ u) v (v v (z ^ u)) = v v ((x v (y v z)) ^ u). [para(64(a,1),54(a,1,2,2))]. given #920 (F,wt=17): 4417 (x v (y v z)) ^ ((z ^ u) v y) = (z ^ u) v y. [para(227(a,1),112(a,1,2)),demod(227(9))]. given #921 (F,wt=17): 4418 ((x ^ y) v z) ^ (z v (u v y)) = (x ^ y) v z. [para(112(a,1),227(a,1,1,1)),demod(112(8))]. given #922 (F,wt=17): 4424 (x v (y v z)) ^ (z v (y v x)) = x v (y v z). [para(101(a,1),227(a,1,1,1)),demod(10(2),101(9),10(7))]. given #923 (F,wt=17): 4460 x ^ ((y v (x ^ z)) ^ (u ^ z)) = x ^ (u ^ z). [para(39(a,1),109(a,2,2)),demod(58(5))]. given #924 (T,wt=17): 4472 x ^ ((y v (z ^ x)) ^ (u ^ z)) = x ^ (u ^ z). [para(58(a,1),109(a,2)),demod(183(6))]. given #925 (A,wt=21): 395 (x v (y ^ z)) ^ ((u v (x v z)) ^ v) = (x v (y ^ z)) ^ v. [para(54(a,1),64(a,1,2,1,2))]. given #926 (F,wt=17): 4638 ((x v y) ^ z) v (z ^ (y ^ u)) = (x v y) ^ z. [para(231(a,1),26(a,1,2))]. given #927 (F,wt=17): 4707 ((x v y) ^ z) v ((y v x) ^ z) = (x v y) ^ z. [para(235(a,1),25(a,1,2))]. given #928 (F,wt=17): 4713 (x v y) ^ (z v (u v (v v (y v x)))) = x v y. [para(63(a,1),235(a,1,2)),demod(106(3)),flip(a)]. given #929 (F,wt=17): 4731 x v (y v (z ^ (u ^ ((y v x) ^ v)))) = x v y. [para(235(a,1),187(a,1,2,2,2)),demod(10(6))]. given #930 (T,wt=17): 4773 (x v (y ^ z)) ^ (u v (y v x)) = x v (y ^ z). [para(100(a,1),235(a,1,2)),demod(106(5)),flip(a)]. given #931 (A,wt=23): 398 ((x v (y v z)) ^ u) v (v ^ (w ^ (z ^ u))) = (x v (y v z)) ^ u. [para(64(a,1),76(a,1,2,2,2))]. given #932 (F,wt=17): 4823 (x v (y v z)) ^ ((x ^ u) v z) = (x ^ u) v z. [para(97(a,1),111(a,2)),demod(247(7))]. given #933 (F,wt=17): 4862 x v (y v (z ^ (u ^ (y v (x ^ v))))) = x v y. [para(240(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #934 (F,wt=17): 4863 x v (y v (z ^ (u ^ (y v (v ^ x))))) = x v y. [para(240(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #935 (F,wt=17): 4876 x v (y v (z ^ (u ^ ((v ^ y) v x)))) = x v y. [para(240(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #936 (T,wt=17): 4984 x ^ (y ^ (z v ((x v u) ^ (y v v)))) = x ^ y. [para(246(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #937 (A,wt=25): 400 (x v ((y v x) ^ z)) ^ ((u v (y v x)) ^ v) = (x v ((y v x) ^ z)) ^ v. [para(24(a,1),64(a,1,2,1,2))]. given #938 (F,wt=17): 4987 x ^ (y ^ (z v ((x v u) ^ (v v y)))) = y ^ x. [para(246(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #939 (F,wt=17): 4993 x ^ (y v ((x v z) ^ (u v (v v (w v x))))) = x. [para(246(a,1),142(a,1)),demod(63(4)),flip(a)]. given #940 (F,wt=17): 4996 x ^ (y v ((x v z) ^ (u v (v v (x v w))))) = x. [para(246(a,1),195(a,1)),demod(80(4)),flip(a)]. given #941 (F,wt=17): 5028 x ^ (y ^ (z v ((u v x) ^ (y v v)))) = x ^ y. [para(248(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #942 (T,wt=17): 5031 x ^ (y ^ (z v ((u v x) ^ (v v y)))) = y ^ x. [para(248(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #943 (A,wt=23): 402 (x ^ y) v (z v ((u v (v v x)) ^ y)) = z v ((u v (v v x)) ^ y). [para(64(a,1),120(a,1,1))]. given #944 (F,wt=17): 5036 x ^ (y v ((z v x) ^ (u v (v v (w v x))))) = x. [para(248(a,1),142(a,1)),demod(63(4)),flip(a)]. given #945 (F,wt=17): 5039 x ^ (y v ((z v x) ^ (u v (v v (x v w))))) = x. [para(248(a,1),195(a,1)),demod(80(4)),flip(a)]. given #946 (F,wt=17): 5063 x ^ (y ^ (z v ((y v u) ^ (v v x)))) = x ^ y. [para(253(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #947 (F,wt=17): 5066 x ^ (y ^ (z v ((u v y) ^ (v v x)))) = y ^ x. [para(253(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #948 (T,wt=17): 5073 x ^ (y v ((z v (u v (v v x))) ^ (w v x))) = x. [para(253(a,1),142(a,1)),demod(63(4)),flip(a)]. given #949 (A,wt=21): 403 x ^ (y ^ (z ^ ((u v (x ^ y)) ^ v))) = x ^ (y ^ (z ^ v)). [para(26(a,1),64(a,1,2,1,2)),demod(12(6),12(5),12(9),12(8))]. given #950 (F,wt=17): 5080 x ^ (y v ((z v (u v (x v v))) ^ (w v x))) = x. [para(253(a,1),195(a,1)),demod(80(4)),flip(a)]. given #951 (F,wt=17): 5293 x v (y v (z ^ ((x ^ u) v (y ^ v)))) = x v y. [para(263(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #952 (F,wt=17): 5297 x v (y v (z ^ ((x ^ u) v (v ^ y)))) = x v y. [para(263(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #953 (F,wt=17): 5318 x v (y ^ ((x ^ z) v (u ^ (v ^ (w ^ x))))) = x. [para(263(a,1),180(a,1)),demod(76(4)),flip(a)]. given #954 (T,wt=17): 5319 x v (y ^ ((x ^ z) v (u ^ (v ^ (x ^ w))))) = x. [para(263(a,1),198(a,1)),demod(87(4)),flip(a)]. given #955 (A,wt=25): 405 (x v (y ^ (z v x))) ^ ((u v (z v x)) ^ v) = (x v (y ^ (z v x))) ^ v. [para(49(a,1),64(a,1,2,1,2))]. given #956 (F,wt=17): 5327 (x v y) ^ (y v (z v (u v (v v x)))) = x v y. [para(63(a,1),265(a,1,1,1)),demod(63(10))]. given #957 (F,wt=17): 5329 (x v y) ^ (y v (z v (u v (x v v)))) = x v y. [para(80(a,1),265(a,1,1,1)),demod(80(10))]. given #958 (F,wt=17): 5330 (x v (y v z)) ^ ((u ^ y) v x) = (u ^ y) v x. [para(265(a,1),92(a,1,2)),demod(10(2),265(9))]. given #959 (F,wt=17): 5332 (x v (y v z)) ^ ((u ^ z) v y) = (u ^ z) v y. [para(265(a,1),112(a,1,2)),demod(265(9))]. given #960 (T,wt=17): 5431 x v (y v (z ^ ((u ^ x) v (y ^ v)))) = x v y. [para(267(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #961 (A,wt=21): 407 (x v (y v z)) ^ ((z ^ u) v (z ^ v)) = (z ^ u) v (z ^ v). [para(29(a,1),64(a,2)),demod(347(9))]. given #962 (F,wt=17): 5434 x v (y v (z ^ ((u ^ x) v (v ^ y)))) = x v y. [para(267(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #963 (F,wt=17): 5454 x v (y ^ ((z ^ x) v (u ^ (v ^ (w ^ x))))) = x. [para(267(a,1),180(a,1)),demod(76(4)),flip(a)]. given #964 (F,wt=17): 5455 x v (y ^ ((z ^ x) v (u ^ (v ^ (x ^ w))))) = x. [para(267(a,1),198(a,1)),demod(87(4)),flip(a)]. given #965 (F,wt=17): 5465 (x ^ y) v (x ^ (z ^ (u ^ (y ^ v)))) = x ^ y. [para(115(a,1),26(a,1,2,2))]. given #966 (T,wt=17): 5469 (x ^ y) v (y ^ (z ^ (u ^ (x ^ v)))) = y ^ x. [para(115(a,1),275(a,1,2,2))]. given #967 (A,wt=19): 411 (x ^ (y ^ z)) v (x ^ (y ^ (u ^ z))) = x ^ (y ^ z). [para(12(a,1),70(a,1,1)),demod(12(5),12(8))]. given #968 (F,wt=17): 5471 (x ^ (y ^ (z ^ (u ^ v)))) v (u ^ x) = x ^ u. [para(115(a,1),292(a,1,1,2))]. given #969 (F,wt=17): 5472 x v (y ^ ((z ^ (u ^ (x ^ v))) v (x ^ w))) = x. [para(115(a,1),352(a,1,2,2,1))]. given #970 (F,wt=17): 5473 x ^ ((y ^ x) v (z ^ (u ^ (y ^ v)))) = x ^ y. [para(115(a,1),359(a,1,2,2))]. given #971 (F,wt=17): 5474 x ^ ((y ^ (z ^ (u ^ v))) v (u ^ x)) = x ^ u. [para(115(a,1),360(a,1,2,1))]. given #972 (T,wt=17): 5477 x v (y ^ ((z ^ (u ^ (x ^ v))) v (w ^ x))) = x. [para(115(a,1),1199(a,1,2,2,1))]. given #973 (A,wt=19): 414 (x ^ (y ^ z)) v (y ^ (u ^ (x ^ z))) = y ^ (x ^ z). [para(18(a,1),70(a,1,1))]. given #974 (F,wt=17): 5478 x v (((y ^ (z ^ (x ^ u))) v (x ^ v)) ^ w) = x. [para(115(a,1),1200(a,1,2,1,1))]. given #975 (F,wt=17): 5479 x ^ ((x ^ y) v (z ^ (u ^ (y ^ v)))) = x ^ y. [para(115(a,1),1227(a,1,2,2))]. given #976 (F,wt=17): 5480 x ^ ((y ^ (z ^ (u ^ v))) v (x ^ u)) = x ^ u. [para(115(a,1),1296(a,1,2,1))]. given #977 (F,wt=17): 5481 x v (((y ^ (z ^ (x ^ u))) v (v ^ x)) ^ w) = x. [para(115(a,1),1462(a,1,2,1,1))]. given #978 (T,wt=17): 5571 (x ^ y) v (x ^ (z ^ (u ^ (v ^ y)))) = x ^ y. [para(58(a,1),280(a,1,2,2,2))]. given #979 (A,wt=21): 416 (x ^ (y ^ z)) v (x ^ ((y v u) ^ z)) = x ^ ((y v u) ^ z). [para(21(a,1),70(a,1,2,2)),demod(9(6))]. given #980 (F,wt=17): 5610 x ^ (y ^ (z v (u v ((y v v) ^ x)))) = x ^ y. [para(283(a,1),63(a,1,2,2,2)),demod(12(6))]. given #981 (F,wt=17): 5612 (x ^ (y ^ z)) v ((y v u) ^ x) = (y v u) ^ x. [para(283(a,1),99(a,1,2)),demod(12(2),283(9))]. given #982 (F,wt=17): 5614 (x ^ (y ^ z)) v ((z v u) ^ y) = (z v u) ^ y. [para(283(a,1),120(a,1,2)),demod(283(9))]. given #983 (F,wt=17): 5657 x ^ (y ^ (z v (u v ((v v y) ^ x)))) = x ^ y. [para(285(a,1),63(a,1,2,2,2)),demod(12(6))]. given #984 (T,wt=17): 5658 (x ^ y) v (y ^ (z ^ (u ^ (v ^ x)))) = x ^ y. [para(76(a,1),285(a,1,1,1)),demod(76(10))]. given #985 (A,wt=21): 417 (x ^ (y v z)) v (x ^ (y v (z v u))) = x ^ (y v (z v u)). [para(20(a,1),70(a,1,2,2)),demod(9(6))]. given #986 (F,wt=17): 5661 (x ^ (y ^ z)) v ((u v y) ^ x) = (u v y) ^ x. [para(285(a,1),99(a,1,2)),demod(12(2),285(9))]. given #987 (F,wt=17): 5663 (x ^ (y ^ z)) v ((u v z) ^ y) = (u v z) ^ y. [para(285(a,1),120(a,1,2)),demod(285(9))]. given #988 (F,wt=17): 5752 (x v (y v z)) ^ (y v (x ^ u)) = y v (x ^ u). [para(241(a,1),116(a,1,2)),demod(241(11))]. given #989 (F,wt=17): 5762 (x v (y v z)) ^ (z v (x ^ u)) = z v (x ^ u). [para(624(a,1),116(a,1,2)),demod(624(11))]. given #990 (T,wt=17): 5792 ((x ^ y) v z) ^ ((y ^ x) v z) = (x ^ y) v z. [para(286(a,1),19(a,1,2))]. given #991 (A,wt=21): 418 (x ^ (y ^ z)) v (x ^ ((u v y) ^ z)) = x ^ ((u v y) ^ z). [para(46(a,1),70(a,1,2,2)),demod(9(6))]. given #992 (F,wt=17): 5805 x ^ (y ^ (z ^ ((y ^ x) v u))) = z ^ (x ^ y). [para(286(a,1),83(a,1,2,2)),demod(12(5))]. given #993 (F,wt=17): 5812 x ^ (y ^ (z v (u v ((y ^ x) v v)))) = x ^ y. [para(286(a,1),147(a,1,2,2,2)),demod(12(6))]. given #994 (F,wt=17): 5915 x ^ (y ^ (z v (u v (y ^ (x v v))))) = x ^ y. [para(293(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #995 (F,wt=17): 5967 x v (y ^ (z ^ ((u ^ (x ^ v)) v (x ^ w)))) = x. [para(18(a,1),366(a,1,2,2,2,1))]. given #996 (T,wt=17): 5968 x v (y ^ (z ^ ((x ^ u) v (v ^ (x ^ w))))) = x. [para(18(a,1),366(a,1,2,2,2,2))]. given #997 (A,wt=19): 419 x ^ (y ^ (z ^ (u v (v v (x ^ z))))) = x ^ (y ^ z). [para(70(a,1),63(a,1,2,2,2)),demod(12(6),12(5))]. given #998 (F,wt=17): 5975 x v (y ^ (z ^ ((u ^ (v ^ x)) v (x ^ w)))) = x. [para(58(a,1),366(a,1,2,2,2,1))]. given #999 (F,wt=17): 5976 x v (y ^ (z ^ ((x ^ u) v (v ^ (w ^ x))))) = x. [para(58(a,1),366(a,1,2,2,2,2))]. given #1000 (F,wt=17): 6007 x v ((y ^ (x v z)) v (u v z)) = x v (u v z). [para(44(a,1),117(a,2,2)),demod(62(5))]. given #1001 (F,wt=17): 6014 x v ((y ^ (z v x)) v (u v z)) = x v (u v z). [para(62(a,1),117(a,2)),demod(144(6))]. given #1002 (T,wt=17): 6353 (x v (y ^ z)) ^ (u v (z v x)) = x v (y ^ z). [para(121(a,1),235(a,1,2)),demod(106(5)),flip(a)]. given #1003 (A,wt=23): 420 (x ^ y) v (x ^ (z v (u v (v v y)))) = x ^ (z v (u v (v v y))). [para(63(a,1),70(a,1,2,2)),demod(9(6))]. given #1004 (F,wt=17): 6467 (x ^ (y ^ z)) v (y ^ (u v z)) = y ^ (u v z). [para(433(a,1),118(a,1,1)),demod(19(8)),flip(a)]. given #1005 (F,wt=17): 6533 (x v (y v (z v (u v v)))) ^ (u v x) = u v x. [para(122(a,1),241(a,1,1,2))]. given #1006 (F,wt=17): 6539 x ^ (((y v (z v (x v u))) ^ (x v v)) v w) = x. [para(122(a,1),2576(a,1,2,1,1))]. given #1007 (F,wt=17): 6541 x ^ (y v ((z v (u v (x v v))) ^ (x v w))) = x. [para(122(a,1),2620(a,1,2,2,1))]. given #1008 (T,wt=17): 6542 x v ((y v (z v (u v v))) ^ (u v x)) = x v u. [para(122(a,1),3119(a,1,2,1))]. given #1009 (A,wt=25): 421 (x ^ (y ^ z)) v (x ^ (z ^ ((y ^ z) v u))) = x ^ (z ^ ((y ^ z) v u)). [para(22(a,1),70(a,1,2,2)),demod(9(7))]. given #1010 (F,wt=17): 6543 x v ((y v (z v (u v v))) ^ (x v u)) = x v u. [para(122(a,1),3209(a,1,2,1))]. given #1011 (F,wt=17): 6544 x v ((y v x) ^ (z v (u v (y v v)))) = x v y. [para(122(a,1),3213(a,1,2,2))]. given #1012 (F,wt=17): 6547 x v ((x v y) ^ (z v (u v (y v v)))) = x v y. [para(122(a,1),3373(a,1,2,2))]. given #1013 (F,wt=17): 6578 (x v (y v (z v (u v v)))) ^ (v v y) = y v v. [para(62(a,1),541(a,1,1,2,2))]. given #1014 (T,wt=17): 6612 (x ^ (y ^ z)) v (y ^ (x v u)) = (x v u) ^ y. [para(21(a,1),588(a,1,1))]. given #1015 (A,wt=19): 422 (x ^ y) v (x ^ ((x ^ y) v z)) = x ^ ((x ^ y) v z). [para(22(a,1),70(a,1,2)),demod(9(5))]. given #1016 (F,wt=17): 6616 (x ^ (y ^ (z ^ (u ^ v)))) v (v ^ y) = y ^ v. [para(58(a,1),588(a,1,1,2,2))]. given #1017 (F,wt=17): 6696 (x v y) ^ (z v (y v (u v (v v x)))) = x v y. [para(620(a,1),111(a,1,2)),demod(10(3),317(4),10(6)),flip(a)]. given #1018 (F,wt=17): 6720 (x ^ (y ^ z)) v ((x v u) ^ z) = (x v u) ^ z. [para(91(a,1),123(a,2)),demod(262(7))]. given #1019 (F,wt=17): 6766 (x v (y v (z v (u v v)))) ^ (v v x) = v v x. [para(62(a,1),640(a,1,1,2,2))]. given #1020 (T,wt=17): 6806 (x v (y v z)) ^ (z v (u ^ x)) = z v (u ^ x). [para(48(a,1),641(a,1,1))]. given #1021 (A,wt=21): 423 (x ^ (y ^ (z v u))) v (x ^ (u ^ y)) = x ^ (y ^ (z v u)). [para(66(a,1),70(a,1,2,2))]. given #1022 (F,wt=17): 6824 (x v y) ^ (z v (u v (y v (v v x)))) = x v y. [para(641(a,1),165(a,1,2)),demod(9(8),14(8)),flip(a)]. given #1023 (F,wt=17): 6889 x ^ (y ^ (z v ((y ^ (x v u)) v v))) = x ^ y. [para(714(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #1024 (F,wt=17): 6897 x ^ (y ^ (z v (((y v u) ^ x) v v))) = x ^ y. [para(714(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #1025 (F,wt=17): 6899 x ^ (y ^ (z v (((u v y) ^ x) v v))) = y ^ x. [para(714(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #1026 (T,wt=17): 6932 (x ^ (y ^ z)) v (z ^ (x v u)) = z ^ (x v u). [para(1076(a,1),124(a,1,2)),demod(1076(11))]. given #1027 (A,wt=21): 424 (x ^ (y ^ z)) v (x ^ (y ^ (z v u))) = x ^ (y ^ (z v u)). [para(68(a,1),70(a,1,2,2)),demod(9(6))]. given #1028 (F,wt=17): 6993 x ^ (y ^ (((y v z) ^ (x v u)) v v)) = x ^ y. [para(718(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #1029 (F,wt=17): 6995 x ^ (y ^ (((z v y) ^ (x v u)) v v)) = y ^ x. [para(718(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #1030 (F,wt=17): 6999 x ^ (((y v (z v (u v x))) ^ (x v v)) v w) = x. [para(718(a,1),142(a,1)),demod(63(4)),flip(a)]. given #1031 (F,wt=17): 7020 x v (y v (z ^ ((y v (x ^ u)) ^ v))) = x v y. [para(770(a,1),23(a,1,2)),demod(23(3)),flip(a)]. given #1032 (T,wt=17): 7021 x v (y v (z ^ ((y v (u ^ x)) ^ v))) = x v y. [para(770(a,1),48(a,1,2)),demod(48(3)),flip(a)]. given #1033 (A,wt=23): 425 (x ^ y) v (x ^ (z v (u v (y v v)))) = x ^ (z v (u v (y v v))). [para(80(a,1),70(a,1,2,2)),demod(9(6))]. given #1034 (F,wt=17): 7031 x v (y v (z ^ (((y ^ u) v x) ^ v))) = x v y. [para(770(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #1035 (F,wt=17): 7033 x v (y v (z ^ (((u ^ y) v x) ^ v))) = x v y. [para(770(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #1036 (F,wt=17): 7076 x v (y v (((y ^ z) v (x ^ u)) ^ v)) = x v y. [para(771(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #1037 (F,wt=17): 7079 x v (y v (((z ^ y) v (x ^ u)) ^ v)) = x v y. [para(771(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #1038 (T,wt=17): 7090 x v (((y ^ (z ^ (u ^ x))) v (x ^ v)) ^ w) = x. [para(771(a,1),180(a,1)),demod(76(4)),flip(a)]. given #1039 (A,wt=25): 427 (x ^ (y ^ z)) v (x ^ (z ^ (u v (y ^ z)))) = x ^ (z ^ (u v (y ^ z))). [para(47(a,1),70(a,1,2,2)),demod(9(7))]. given #1040 (F,wt=17): 7128 x v (y v (((y ^ z) v (u ^ x)) ^ v)) = x v y. [para(773(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #1041 (F,wt=17): 7130 x v (y v (((z ^ y) v (u ^ x)) ^ v)) = x v y. [para(773(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #1042 (F,wt=17): 7138 x v (((y ^ (z ^ (u ^ x))) v (v ^ x)) ^ w) = x. [para(773(a,1),180(a,1)),demod(76(4)),flip(a)]. given #1043 (F,wt=17): 7171 x v (y v (z ^ ((y ^ u) v (x ^ v)))) = x v y. [para(899(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #1044 (T,wt=17): 7174 x v (y v (z ^ ((u ^ y) v (x ^ v)))) = x v y. [para(899(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #1045 (A,wt=19): 428 (x ^ y) v (x ^ (z v (x ^ y))) = x ^ (z v (x ^ y)). [para(47(a,1),70(a,1,2)),demod(9(5))]. given #1046 (F,wt=17): 7185 x v (y ^ ((z ^ (u ^ (v ^ x))) v (x ^ w))) = x. [para(899(a,1),180(a,1)),demod(76(4)),flip(a)]. given #1047 (F,wt=17): 7208 (x v (y v z)) ^ (y v (u ^ x)) = y v (u ^ x). [para(241(a,1),125(a,1,2)),demod(241(11))]. given #1048 (F,wt=17): 7232 x v (y v (z ^ ((y ^ u) v (v ^ x)))) = x v y. [para(901(a,1),98(a,1,2)),demod(52(3)),flip(a)]. given #1049 (F,wt=17): 7233 x v (y v (z ^ ((u ^ y) v (v ^ x)))) = x v y. [para(901(a,1),119(a,1,2)),demod(54(3)),flip(a)]. given #1050 (T,wt=17): 7239 x v (y ^ ((z ^ (u ^ (v ^ x))) v (w ^ x))) = x. [para(901(a,1),180(a,1)),demod(76(4)),flip(a)]. given #1051 (A,wt=21): 429 (x v (y ^ z)) ^ (x v (y ^ (u ^ z))) = x v (y ^ (u ^ z)). [para(70(a,1),53(a,1,2,2)),demod(11(6))]. given #1052 (F,wt=17): 7247 x v (y ^ ((y ^ z) v (x ^ u))) = x v (y ^ z). [para(916(a,1),23(a,1,2)),demod(23(4)),flip(a)]. given #1053 (F,wt=17): 7249 x v (y ^ ((y ^ z) v (u ^ x))) = x v (y ^ z). [para(916(a,1),48(a,1,2)),demod(48(4)),flip(a)]. given #1054 (F,wt=17): 7251 x v ((y v z) ^ ((u ^ y) v x)) = x v (u ^ y). [para(92(a,1),916(a,1,2,2,1)),demod(92(8))]. given #1055 (F,wt=17): 7292 (x v (y v z)) ^ (z v (y ^ u)) = z v (y ^ u). [para(221(a,1),928(a,1,1))]. given #1056 (T,wt=17): 7295 (x v (y v z)) ^ (z v (u ^ y)) = z v (u ^ y). [para(232(a,1),928(a,1,1))]. given #1057 (A,wt=21): 430 (x ^ (y v z)) v (x ^ (y v (u v z))) = x ^ (y v (u v z)). [para(53(a,1),70(a,1,2,2)),demod(9(6))]. given #1058 (F,wt=17): 7381 (x ^ (y ^ z)) v (z ^ (u v x)) = z ^ (u v x). [para(1076(a,1),126(a,1,2)),demod(1076(11))]. given #1059 (F,wt=17): 7506 (x ^ (y ^ z)) v (z ^ (y v u)) = z ^ (y v u). [para(21(a,1),1036(a,1,1,2))]. given #1060 (F,wt=17): 7548 x v (y v (z v ((y v x) ^ u))) = z v (y v x). [para(127(a,1),17(a,1)),flip(a)]. given #1061 (F,wt=17): 7572 (x ^ y) v (z ^ (y ^ (u ^ (v ^ x)))) = x ^ y. [para(1068(a,1),134(a,1,1)),demod(12(8),1526(7),39(2)),flip(a)]. given #1062 (T,wt=17): 7585 (x ^ (y ^ (z ^ (u ^ v)))) v (v ^ x) = v ^ x. [para(58(a,1),1093(a,1,1,2,2))]. given #1063 (A,wt=21): 431 x ^ (y ^ (z ^ ((u v (x ^ z)) ^ v))) = x ^ (y ^ (z ^ v)). [para(70(a,1),64(a,1,2,1,2)),demod(12(6),12(5),12(9),12(8))]. given #1064 (F,wt=17): 7648 x ^ (y ^ (z v ((y v u) ^ (x v v)))) = x ^ y. [para(1121(a,1),93(a,1,2)),demod(68(3)),flip(a)]. given #1065 (F,wt=17): 7650 x ^ (y ^ (z v ((u v y) ^ (x v v)))) = y ^ x. [para(1121(a,1),113(a,1,2)),demod(66(3)),flip(a)]. given #1066 (F,wt=17): 7652 x ^ (y v ((z v (u v (v v x))) ^ (x v w))) = x. [para(1121(a,1),142(a,1)),demod(63(4)),flip(a)]. given #1067 (F,wt=17): 7661 x v (y ^ ((x ^ z) v (y ^ u))) = x v (y ^ u). [para(1141(a,1),23(a,1,2)),demod(23(4)),flip(a)]. given #1068 (T,wt=17): 7662 x v (y ^ ((z ^ x) v (y ^ u))) = x v (y ^ u). [para(1141(a,1),48(a,1,2)),demod(48(4)),flip(a)]. given #1069 (A,wt=25): 432 (x ^ (y ^ z)) v (x ^ ((u v (v v y)) ^ z)) = x ^ ((u v (v v y)) ^ z). [para(64(a,1),70(a,1,2,2)),demod(9(7))]. given #1070 (F,wt=17): 7663 x v ((y v z) ^ (x v (u ^ y))) = x v (u ^ y). [para(92(a,1),1141(a,1,2,2,2)),demod(92(8))]. given #1071 (F,wt=17): 7757 (x ^ (y v z)) v (y ^ (x ^ u)) = x ^ (y v z). [para(1173(a,1),1007(a,1,1)),demod(12(6),13(8),12(6)),flip(a)]. given #1072 (F,wt=17): 7758 (x v (y ^ z)) ^ (y v (x v u)) = x v (y ^ z). [para(1007(a,1),1173(a,1,1)),demod(10(6),14(8),10(6)),flip(a)]. given #1073 (F,wt=17): 7759 (x v (y ^ z)) ^ (z v (x v u)) = x v (y ^ z). [para(1008(a,1),1173(a,1,1)),demod(10(6),14(8),10(6)),flip(a)]. given #1074 (T,wt=17): 7808 (x v (y ^ z)) ^ (z v (u v x)) = x v (y ^ z). [para(92(a,1),1190(a,1,1,2)),demod(10(4),92(8))]. given #1075 (A,wt=19): 434 (x ^ y) v (x ^ (z v (u v y))) = x ^ (z v (u v y)). [back_demod(357),demod(413(11))]. given #1076 (F,wt=17): 7886 x v (y ^ ((z ^ (x ^ u)) v (v ^ (x ^ w)))) = x. [para(18(a,1),1203(a,1,2,2,2))]. given #1077 (F,wt=17): 7890 x v (y ^ (((z ^ (x ^ u)) v (x ^ v)) ^ w)) = x. [para(1203(a,1),99(a,1,2)),demod(12(6),9(7),1203(13))]. given #1078 (F,wt=17): 7894 x v (y ^ ((z ^ (x ^ u)) v (v ^ (w ^ x)))) = x. [para(58(a,1),1203(a,1,2,2,2))]. given #1079 (F,wt=17): 7915 x v (y ^ (((x ^ z) v (u ^ (x ^ v))) ^ w)) = x. [para(1204(a,1),99(a,1,2)),demod(12(6),9(7),1204(13))]. given #1080 (T,wt=17): 7919 x v (y ^ ((z ^ (u ^ x)) v (v ^ (x ^ w)))) = x. [para(58(a,1),1204(a,1,2,2,1))]. given #1081 (A,wt=19): 435 (x ^ y) v (x ^ (z v (y v u))) = x ^ (z v (y v u)). [back_demod(364),demod(415(11))]. given #1082 (F,wt=17): 7943 x v (y ^ (((z ^ (u ^ x)) v (x ^ v)) ^ w)) = x. [para(58(a,1),1211(a,1,2,2,1,1))]. given #1083 (F,wt=17): 7944 x v (y ^ (((x ^ z) v (u ^ (v ^ x))) ^ w)) = x. [para(58(a,1),1211(a,1,2,2,1,2))]. given #1084 (F,wt=17): 7983 x v (y ^ ((z ^ (u ^ x)) v (v ^ (w ^ x)))) = x. [para(58(a,1),1216(a,1,2,2,2))]. given #1085 (F,wt=17): 8022 x ^ ((y ^ (x v z)) v (u ^ (y ^ v))) = x ^ y. [para(1234(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #1086 (T,wt=17): 8023 x ^ (((y v z) ^ x) v (y ^ u)) = x ^ (y v z). [para(21(a,1),1234(a,1,2,2))]. given #1087 (A,wt=21): 436 x ^ (((y v x) ^ z) v (y ^ (x v z))) = (x ^ z) v (x ^ y). [para(9(a,1),32(a,1,2,1,1))]. given #1088 (F,wt=17): 8024 x ^ ((y ^ (z v x)) v (u ^ (y ^ v))) = x ^ y. [para(1234(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #1089 (F,wt=17): 8025 x ^ (((y v z) ^ x) v (z ^ u)) = x ^ (y v z). [para(46(a,1),1234(a,1,2,2))]. given #1090 (F,wt=17): 8028 x ^ ((y ^ x) v (z ^ (u ^ (v ^ y)))) = x ^ y. [para(58(a,1),1234(a,1,2,2,2))]. given #1091 (F,wt=17): 8085 x ^ ((y ^ (x v z)) v (u ^ (v ^ y))) = x ^ y. [para(58(a,1),1235(a,1,2,2))]. given #1092 (T,wt=17): 8100 x ^ (y v ((y v z) ^ (x v u))) = x ^ (y v z). [para(3119(a,1),1235(a,1,2)),demod(9(4))]. given #1093 (A,wt=21): 437 x ^ (((x v y) ^ z) v (y ^ (z v x))) = (x ^ z) v (x ^ y). [para(9(a,1),32(a,1,2,2,2))]. given #1094 (F,wt=17): 8101 x ^ (y v ((z v y) ^ (x v u))) = x ^ (z v y). [para(3208(a,1),1235(a,1,2)),demod(9(4))]. given #1095 (F,wt=17): 8128 x ^ ((y ^ (z v x)) v (u ^ (v ^ y))) = x ^ y. [para(58(a,1),1237(a,1,2,2))]. given #1096 (F,wt=17): 8140 x ^ (y v ((y v z) ^ (u v x))) = x ^ (y v z). [para(3119(a,1),1237(a,1,2)),demod(9(4))]. given #1097 (F,wt=17): 8141 x ^ (y v ((z v y) ^ (u v x))) = x ^ (z v y). [para(3208(a,1),1237(a,1,2)),demod(9(4))]. given #1098 (T,wt=17): 8217 (x ^ (y v z)) v (y ^ (u ^ x)) = (y v z) ^ x. [para(21(a,1),1264(a,1,2))]. given #1099 (A,wt=21): 438 x ^ (((x v y) ^ z) v ((x v z) ^ y)) = (x ^ z) v (x ^ y). [para(11(a,1),32(a,1,2,2))]. given #1100 (F,wt=17): 8241 x ^ ((y ^ (z ^ u)) v (z ^ (x v v))) = x ^ z. [para(1301(a,1),21(a,1,2)),demod(21(3)),flip(a)]. given #1101 (F,wt=17): 8242 x ^ ((y ^ z) v ((y v u) ^ x)) = x ^ (y v u). [para(21(a,1),1301(a,1,2,1))]. given #1102 (F,wt=17): 8243 x ^ ((y ^ (z ^ u)) v (z ^ (v v x))) = x ^ z. [para(1301(a,1),46(a,1,2)),demod(46(3)),flip(a)]. given #1103 (F,wt=17): 8244 x ^ ((y ^ z) v ((u v y) ^ x)) = x ^ (u v y). [para(46(a,1),1301(a,1,2,1))]. given #1104 (T,wt=17): 8247 x ^ ((y ^ (z ^ (u ^ v))) v (v ^ x)) = x ^ v. [para(58(a,1),1301(a,1,2,1,2))]. given #1105 (A,wt=25): 439 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 #1106 (F,wt=17): 8296 x ^ ((y ^ (z ^ u)) v (u ^ (x v v))) = x ^ u. [para(58(a,1),1303(a,1,2,1))]. given #1107 (F,wt=17): 8338 x ^ ((y ^ (z ^ u)) v (u ^ (v v x))) = x ^ u. [para(58(a,1),1304(a,1,2,1))]. given #1108 (F,wt=17): 8485 x v (y ^ (z ^ ((u ^ x) v (v ^ (x ^ w))))) = x. [para(18(a,1),1400(a,1,2,2,2,2))]. given #1109 (F,wt=17): 8490 x v (y ^ (z ^ ((u ^ x) v (v ^ (w ^ x))))) = x. [para(58(a,1),1400(a,1,2,2,2,2))]. given #1110 (T,wt=17): 8506 x v (y ^ (((z ^ x) v (u ^ (x ^ v))) ^ w)) = x. [para(1407(a,1),99(a,1,2)),demod(12(6),9(7),1407(13))]. given #1111 (A,wt=25): 443 x ^ (((x v y) ^ z) v (y ^ (x v ((x v y) ^ z)))) = (x ^ z) v (x ^ y). [para(37(a,1),32(a,1,2,1)),demod(21(11))]. given #1112 (F,wt=17): 8529 x v (y ^ (((z ^ x) v (u ^ (v ^ x))) ^ w)) = x. [para(58(a,1),1419(a,1,2,2,1,2))]. given #1113 (F,wt=17): 8556 x v (y ^ (z ^ ((u ^ (x ^ v)) v (w ^ x)))) = x. [para(18(a,1),1464(a,1,2,2,2,1))]. given #1114 (F,wt=17): 8561 x v (y ^ (z ^ ((u ^ (v ^ x)) v (w ^ x)))) = x. [para(58(a,1),1464(a,1,2,2,2,1))]. given #1115 (F,wt=17): 8577 x v (y ^ (((z ^ (x ^ u)) v (v ^ x)) ^ w)) = x. [para(1468(a,1),99(a,1,2)),demod(12(6),9(7),1468(13))]. given #1116 (T,wt=17): 8600 x v (y ^ (((z ^ (u ^ x)) v (v ^ x)) ^ w)) = x. [para(58(a,1),1476(a,1,2,2,1,1))]. given #1117 (A,wt=25): 444 x ^ ((y ^ (x v z)) v (z ^ (x v (y ^ (x v z))))) = (y ^ x) v (x ^ z). [para(39(a,1),32(a,1,2,1)),demod(68(11))]. given #1118 (F,wt=17): 8625 x v (((y ^ (x ^ z)) v (u ^ (x ^ v))) ^ w) = x. [para(18(a,1),1497(a,1,2,1,2))]. given #1119 (F,wt=17): 8632 x v (((y ^ (x ^ z)) v (u ^ (v ^ x))) ^ w) = x. [para(58(a,1),1497(a,1,2,1,2))]. given #1120 (F,wt=17): 8651 x v (((y ^ (z ^ x)) v (u ^ (x ^ v))) ^ w) = x. [para(58(a,1),1498(a,1,2,1,1))]. given #1121 (F,wt=17): 8672 x v ((y v (z v (u v v))) ^ (v v x)) = x v v. [para(144(a,1),3119(a,1,2,1))]. given #1122 (T,wt=17): 8673 x v ((y v (z v (u v v))) ^ (x v v)) = x v v. [para(144(a,1),3209(a,1,2,1))]. given #1123 (A,wt=25): 446 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 #1124 (F,wt=17): 8674 x v ((y v x) ^ (z v (u v (v v y)))) = x v y. [para(144(a,1),3213(a,1,2,2))]. given #1125 (F,wt=17): 8