============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13678 was started by mccune on cleo.thornwood, Mon Jun 19 16:49:49 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H78b.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in clauses(sos). x v y = y v x. (x v y) v z = x v (y v z). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. end_of_list. % Reading from file uc.in clauses(sos). x v x ' = 1. x ^ x ' = 0. x v y != 1 | x ^ y != 0 | x ' = y. end_of_list. % Reading from file H78b.in terms(weights). weight(x ') = weight(x). weight(x v (y v (z v u))) = 1000. weight(x ^ (y ^ (z ^ u))) = 1000. end_of_list. clauses(sos). x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (y ^ (x v u))))) # label(H78). end_of_list. formulas(goals). (all x all y (x ^ y = x -> x ' v y ' = x ')). end_of_list. ============================== end of input ========================== ============================== PROCESS GOALS ========================= % Each goal formula was negated; the result (to be placed in sos): clauses(negated_goals). c1 ^ c2 = c1. c1 ' != c1 ' v c2 '. 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 v x ' = 1. [input]. 8 x ^ x ' = 0. [input]. 9 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 10 x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (y ^ (x v u))))) # label(H78). [input]. 11 c1 ^ c2 = c1. [clausify]. 12 c1 ' != c1 ' v c2 '. [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([ 0, 1, c1, c2, ^, v, ' ]). After inverse_order: Function symbol precedence: lex([ 0, 1, c1, c2, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) 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). 13 x v y = y v x. [input]. 14 (x v y) v z = x v (y v z). [input]. 15 x ^ y = y ^ x. [input]. 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. 17 x ^ (x v y) = x. [input]. 18 x v (x ^ y) = x. [input]. 19 x v x ' = 1. [input]. 20 x ^ x ' = 0. [input]. 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. 22 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (y v u))) # label(H78). [copy(10),flip(a)]. 23 c1 ^ c2 = c1. [clausify]. 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. end_of_list. clauses(demodulators). 13 x v y = y v x. [input]. % (lex-dep) 14 (x v y) v z = x v (y v z). [input]. 15 x ^ y = y ^ x. [input]. % (lex-dep) 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. 17 x ^ (x v y) = x. [input]. 18 x v (x ^ y) = x. [input]. 19 x v x ' = 1. [input]. 20 x ^ x ' = 0. [input]. 23 c1 ^ c2 = c1. [clausify]. 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): 13 x v y = y v x. [input]. given #2 (I,wt=11): 14 (x v y) v z = x v (y v z). [input]. given #3 (I,wt=7): 15 x ^ y = y ^ x. [input]. given #4 (I,wt=11): 16 (x ^ y) ^ z = x ^ (y ^ z). [input]. given #5 (I,wt=7): 17 x ^ (x v y) = x. [input]. given #6 (I,wt=7): 18 x v (x ^ y) = x. [input]. given #7 (I,wt=5): 19 x v x ' = 1. [input]. given #8 (I,wt=5): 20 x ^ x ' = 0. [input]. given #9 (I,wt=13): 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=23): 22 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (y v u))) # label(H78). [copy(10),flip(a)]. given #11 (I,wt=5): 23 c1 ^ c2 = c1. [clausify]. given #12 (I,wt=5): 24 c1 ' v c2 ' != c1 '. [copy(12),flip(a)]. given #13 (F,wt=5): 35 x ^ x = x. [para(18(a,1),17(a,1,2))]. given #14 (T,wt=5): 36 x v x = x. [para(17(a,1),18(a,1,2))]. given #15 (T,wt=5): 39 x ^ 1 = x. [para(19(a,1),17(a,1,2))]. given #16 (A,wt=11): 25 x v (y v z) = y v (x v z). [para(13(a,1),14(a,1,1)),demod(14(2))]. given #17 (F,wt=5): 42 x v 0 = x. [para(20(a,1),18(a,1,2))]. given #18 (F,wt=5): 76 1 ^ x = x. [para(39(a,1),15(a,1)),flip(a)]. given #19 (T,wt=3): 84 1 ' = 0. [hyper(21,a,42,a,b,76,a)]. given #20 (T,wt=5): 82 0 v x = x. [para(42(a,1),13(a,1)),flip(a)]. given #21 (A,wt=11): 26 x ^ (y ^ z) = y ^ (x ^ z). [para(15(a,1),16(a,1,1)),demod(16(2))]. given #22 (F,wt=3): 87 0 ' = 1. [hyper(21,a,82,a,b,39,a)]. given #23 (F,wt=5): 85 1 v x = 1. [para(76(a,1),17(a,1))]. given #24 (T,wt=5): 88 0 ^ x = 0. [para(82(a,1),17(a,1,2))]. given #25 (T,wt=5): 95 x v 1 = 1. [para(85(a,1),13(a,1)),flip(a)]. given #26 (A,wt=7): 27 x ^ (y v x) = x. [para(13(a,1),17(a,1,2))]. given #27 (F,wt=5): 98 x ^ 0 = 0. [para(88(a,1),15(a,1)),flip(a)]. given #28 (F,wt=6): 97 0 != x | x ' = 1. [back_demod(77),demod(95(2)),xx(a)]. given #29 (T,wt=6): 100 1 != x | x ' = 0. [back_demod(83),demod(98(4)),xx(b)]. given #30 (T,wt=7): 33 x v (y ^ x) = x. [para(15(a,1),18(a,1,2))]. given #31 (A,wt=13): 28 (x v y) ^ (x v (y v z)) = x v y. [para(14(a,1),17(a,1,2))]. given #32 (F,wt=5): 111 c1 v c2 = c2. [para(23(a,1),33(a,1,2)),demod(13(3))]. given #33 (F,wt=7): 86 x v (x ' v y) = 1. [back_demod(37),demod(85(5))]. given #34 (T,wt=7): 89 x ^ (x ' ^ y) = 0. [back_demod(40),demod(88(5))]. given #35 (T,wt=7): 96 x v (y v x ') = 1. [back_demod(80),demod(95(5))]. given #36 (A,wt=11): 29 x ^ ((x v y) ^ z) = x ^ z. [para(17(a,1),16(a,1,1)),flip(a)]. given #37 (F,wt=7): 123 c1 ^ (c1 ' v c2 ') != 0. [ur(21,a,86,a,c,24,a(flip))]. given #38 (F,wt=7): 99 x ^ (y ^ x ') = 0. [back_demod(92),demod(98(5))]. given #39 (T,wt=7): 127 x ^ (x v y) ' = 0. [para(20(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #40 (T,wt=5): 139 c1 ^ c2 ' = 0. [para(111(a,1),127(a,1,2,1))]. given #41 (A,wt=13): 30 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(17(a,1),16(a,1)),flip(a)]. given #42 (F,wt=7): 134 x ^ (y v x) ' = 0. [para(13(a,1),127(a,1,2,1))]. given #43 (F,wt=7): 140 c1 ^ (c2 ' ^ x) = 0. [para(139(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #44 (T,wt=7): 142 c1 ^ (x ^ c2 ') = 0. [para(139(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #45 (T,wt=8): 141 c1 v c2 ' != 1 | c2 ' = c1 '. [para(139(a,1),21(b,1)),flip(c),xx(b)]. given #46 (A,wt=11): 31 x v ((x ^ y) v z) = x v z. [para(18(a,1),14(a,1,1)),flip(a)]. given #47 (F,wt=7): 157 x v (x ^ y) ' = 1. [para(19(a,1),31(a,1,2)),demod(95(2)),flip(a)]. given #48 (F,wt=7): 165 x v (y ^ x) ' = 1. [para(15(a,1),157(a,1,2,1))]. given #49 (T,wt=5): 173 c2 v c1 ' = 1. [para(23(a,1),165(a,1,2,1))]. given #50 (T,wt=7): 178 c2 v (c1 ' v x) = 1. [para(173(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #51 (A,wt=13): 32 x v (y v ((x v y) ^ z)) = x v y. [para(18(a,1),14(a,1)),flip(a)]. given #52 (F,wt=7): 180 c2 v (x v c1 ') = 1. [para(173(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #53 (F,wt=8): 179 c2 ^ c1 ' != 0 | c2 ' = c1 '. [para(173(a,1),21(a,1)),xx(a)]. given #54 (T,wt=9): 38 x v (y v (x v y) ') = 1. [para(19(a,1),14(a,1)),flip(a)]. given #55 (T,wt=9): 41 x ^ (y ^ (x ^ y) ') = 0. [para(20(a,1),16(a,1)),flip(a)]. given #56 (A,wt=13): 34 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(16(a,1),18(a,1,2))]. given #57 (F,wt=9): 66 c1 ^ (c2 ^ x) = c1 ^ x. [para(23(a,1),16(a,1,1)),flip(a)]. given #58 (F,wt=7): 198 c1 ^ (c2 v x) = c1. [para(17(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #59 (T,wt=7): 200 c1 ^ (x v c2) = c1. [para(27(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #60 (T,wt=7): 203 c1 ^ (c2 v x) ' = 0. [para(127(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #61 (A,wt=13): 43 x v y != 1 | y ^ x != 0 | y ' = x. [para(13(a,1),21(a,1))]. given #62 (F,wt=3): 223 x ' ' = x. [para(19(a,1),43(a,1)),demod(15(5),20(5)),xx(a),xx(b)]. given #63 (F,wt=7): 205 c1 ^ (x v c2) ' = 0. [para(134(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #64 (T,wt=7): 238 x ' v (y v x) = 1. [para(223(a,1),96(a,1,2,2))]. given #65 (T,wt=7): 239 x ' ^ (y ^ x) = 0. [para(223(a,1),99(a,1,2,2))]. given #66 (A,wt=19): 44 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y) ' = z. [para(14(a,1),21(a,1))]. given #67 (F,wt=8): 233 c2 ^ c1 ' != 0 | c2 = c1. [para(173(a,1),43(a,1)),demod(15(7),223(12)),flip(c),xx(a)]. given #68 (F,wt=9): 67 c2 ^ (x ^ c1) = x ^ c1. [para(23(a,1),16(a,2,2)),demod(15(4))]. given #69 (T,wt=7): 283 c2 v (x ^ c1) = c2. [para(67(a,1),18(a,1,2))]. given #70 (T,wt=7): 286 c2 v (x ^ c1) ' = 1. [para(67(a,1),157(a,1,2,1))]. given #71 (A,wt=13): 45 x v y != 1 | y ^ x != 0 | x ' = y. [para(15(a,1),21(b,1))]. given #72 (F,wt=7): 289 c2 v (c1 ^ x) = c2. [para(15(a,1),283(a,1,2))]. given #73 (F,wt=7): 295 c2 v (c1 ^ x) ' = 1. [para(15(a,1),286(a,1,2,1))]. given #74 (T,wt=8): 309 c1 v c2 ' != 1 | c2 = c1. [para(139(a,1),45(b,1)),demod(13(4),223(12)),xx(b)]. given #75 (T,wt=9): 69 x ^ (x ^ y) = x ^ y. [para(35(a,1),16(a,1,1)),flip(a)]. given #76 (A,wt=19): 46 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(16(a,1),21(b,1))]. given #77 (F,wt=9): 70 x ^ (y ^ x) = y ^ x. [para(35(a,1),16(a,2,2)),demod(15(2))]. given #78 (F,wt=9): 71 1 != x | 0 != x | x ' = x. [para(35(a,1),21(b,1)),demod(36(1)),flip(a),flip(b)]. given #79 (T,wt=9): 73 x v (x v y) = x v y. [para(36(a,1),14(a,1,1)),flip(a)]. given #80 (T,wt=9): 74 x v (y v x) = y v x. [para(36(a,1),14(a,2,2)),demod(13(2))]. given #81 (A,wt=23): 49 x ^ (y v (z ^ (u v (y ^ (u v x))))) = x ^ (y v (z ^ (y v u))). [para(13(a,1),22(a,1,2,2,2,2,2))]. given #82 (F,wt=9): 78 x ^ (y v (x v z)) = x. [para(25(a,1),17(a,1,2))]. given #83 (F,wt=9): 91 x v (y ^ (x ^ z)) = x. [para(26(a,1),18(a,1,2))]. given #84 (T,wt=9): 94 c1 ^ (x ^ c2) = x ^ c1. [para(23(a,1),26(a,1,2)),flip(a)]. given #85 (T,wt=9): 101 x ^ (y v (z v x)) = x. [para(14(a,1),27(a,1,2))]. given #86 (A,wt=23): 50 x ^ (y v (z ^ (u v (y ^ (x v u))))) = x ^ (y v (z ^ (u v y))). [para(13(a,1),22(a,2,2,2,2))]. given #87 (F,wt=9): 109 x v (y ^ (z ^ x)) = x. [para(16(a,1),33(a,1,2))]. given #88 (F,wt=9): 114 c2 != 1 | c1 != 0 | c1 ' = c2. [back_demod(68),demod(111(3))]. given #89 (T,wt=9): 119 c1 v (c2 v x) = c2 v x. [para(111(a,1),14(a,1,1)),flip(a)]. given #90 (T,wt=9): 120 c2 v (x v c1) = x v c2. [para(111(a,1),14(a,2,2)),demod(13(4))]. given #91 (A,wt=23): 55 x ^ (y v ((z v (y ^ (x v z))) ^ u)) = x ^ (y v (u ^ (y v z))). [para(15(a,1),22(a,1,2,2))]. given #92 (F,wt=9): 121 c1 v (x v c2) = x v c2. [para(111(a,1),25(a,1,2)),flip(a)]. given #93 (F,wt=9): 131 x ^ ((x v y) ' ^ z) = 0. [para(89(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #94 (T,wt=9): 133 x ^ (y ^ (x v z) ') = 0. [para(99(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #95 (T,wt=9): 138 x ^ (y v (x v z)) ' = 0. [para(25(a,1),127(a,1,2,1))]. given #96 (A,wt=39): 61 x v (y v (z ^ (u v (y ^ (x v u))))) != 1 | x ^ (y v (z ^ (y v u))) != 0 | x ' = y v (z ^ (u v (y ^ (x v u)))). [para(22(a,1),21(b,1))]. given #97 (F,wt=9): 148 x ^ (y v (z v x)) ' = 0. [para(14(a,1),134(a,1,2,1))]. given #98 (F,wt=9): 149 x ^ ((y v x) ' ^ z) = 0. [para(134(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #99 (T,wt=9): 153 x ^ (y ^ (z v x) ') = 0. [para(134(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #100 (T,wt=9): 161 x v ((x ^ y) ' v z) = 1. [para(86(a,1),31(a,1,2)),demod(95(2)),flip(a)]. given #101 (A,wt=31): 62 x v (y v (z ^ (y v u))) != 1 | x ^ (y v (z ^ (u v y))) != 0 | x ' = y v (z ^ (y v u)). [para(22(a,2),21(b,1)),demod(50(12))]. given #102 (F,wt=9): 162 x v (y v (x ^ z) ') = 1. [para(96(a,1),31(a,1,2)),demod(95(2)),flip(a)]. given #103 (F,wt=9): 168 x v (y ^ (x ^ z)) ' = 1. [para(26(a,1),157(a,1,2,1))]. given #104 (T,wt=9): 169 x v ((y ^ x) ' v z) = 1. [para(165(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #105 (T,wt=9): 171 x v (y ^ (z ^ x)) ' = 1. [para(16(a,1),165(a,1,2,1))]. given #106 (A,wt=43): 63 x ^ (y v (z ^ ((u ^ (v v (x ^ (y v v)))) v (y ^ (x v (u ^ (x v v))))))) = x ^ (y v (z ^ (y v (u ^ (v v (x ^ (y v v))))))). [para(22(a,1),22(a,1,2,2,2,2))]. given #107 (F,wt=9): 174 x v (y v (z ^ x) ') = 1. [para(165(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #108 (F,wt=9): 189 x v (y v (y v x) ') = 1. [para(13(a,1),38(a,1,2,2,1))]. given #109 (T,wt=9): 192 x ^ (y ^ (y ^ x) ') = 0. [para(15(a,1),41(a,1,2,2,1))]. given #110 (T,wt=9): 206 (c2 ^ x) v (c1 ^ x) ' = 1. [para(66(a,1),165(a,1,2,1))]. given #111 (A,wt=35): 64 x ^ (y v (z ^ ((u ^ (x v v)) v (y ^ (x v (u ^ (v v x))))))) = x ^ (y v (z ^ (y v (u ^ (x v v))))). [para(22(a,2),22(a,1,2,2,2,2)),demod(50(8))]. given #112 (F,wt=9): 207 c1 ^ (x ^ (c2 ^ x) ') = 0. [para(41(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #113 (F,wt=9): 209 c1 ^ (x v (c2 v y)) = c1. [para(25(a,1),198(a,1,2))]. given #114 (T,wt=9): 211 c1 ^ (x v (y v c2)) = c1. [para(14(a,1),200(a,1,2))]. given #115 (T,wt=9): 215 c1 ^ ((c2 v x) ' ^ y) = 0. [para(203(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #116 (A,wt=17): 65 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)). [para(22(a,2),22(a,1,2,2)),demod(27(2),36(1),33(2)),flip(a)]. given #117 (F,wt=9): 217 c1 ^ (x v (c2 v y)) ' = 0. [para(25(a,1),203(a,1,2,1))]. given #118 (F,wt=9): 218 c1 ^ (x ^ (c2 v y) ') = 0. [para(203(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #119 (T,wt=9): 227 c2 != 1 | c1 != 0 | c2 ' = c1. [para(111(a,1),43(a,1)),demod(15(6),23(6))]. given #120 (T,wt=9): 240 c1 ^ (x v (y v c2)) ' = 0. [para(14(a,1),205(a,1,2,1))]. given #121 (A,wt=13): 72 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(48),demod(69(4))]. given #122 (F,wt=6): 1156 c1 != 1 | c1 ' = 0. [para(139(a,1),72(b,1)),demod(139(12)),flip(a),xx(b)]. given #123 (F,wt=6): 1158 x ' != 1 | 0 = x. [para(239(a,1),72(b,1)),demod(223(8),239(9)),flip(a),flip(c),xx(b)]. given #124 (T,wt=9): 241 c1 ^ ((x v c2) ' ^ y) = 0. [para(205(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #125 (T,wt=9): 243 c1 ^ (x ^ (y v c2) ') = 0. [para(205(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #126 (A,wt=13): 75 x v y != 1 | 0 != x | x ' = x v y. [back_demod(47),demod(73(2))]. given #127 (F,wt=7): 1162 (c1 ^ (c1 ' v c2 ')) ' != 1. [ur(1158,b,123,a(flip))]. given #128 (F,wt=6): 1173 c2 != 0 | c2 ' = 1. [para(173(a,1),75(a,1)),demod(173(12)),flip(b),xx(a)]. given #129 (T,wt=6): 1174 x ' != 0 | 1 = x. [para(238(a,1),75(a,1)),demod(223(8),238(9)),flip(b),flip(c),xx(a)]. given #130 (T,wt=9): 290 c2 v (x ^ (y ^ c1)) = c2. [para(16(a,1),283(a,1,2))]. given #131 (A,wt=11): 79 x v (y v (x ^ z)) = y v x. [para(18(a,1),25(a,1,2)),flip(a)]. given #132 (F,wt=9): 294 c2 v ((x ^ c1) ' v y) = 1. [para(286(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #133 (F,wt=9): 296 c2 v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),286(a,1,2,1))]. given #134 (T,wt=9): 298 c2 v (x v (y ^ c1) ') = 1. [para(286(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #135 (T,wt=9): 325 c2 v (x ^ (c1 ^ y)) = c2. [para(26(a,1),289(a,1,2))]. given #136 (A,wt=19): 81 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(25(a,1),21(a,1))]. given #137 (F,wt=9): 328 c2 v ((c1 ^ x) ' v y) = 1. [para(295(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #138 (F,wt=9): 330 c2 v (x v (c1 ^ y) ') = 1. [para(295(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #139 (T,wt=9): 331 c2 v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),295(a,1,2,1))]. given #140 (T,wt=9): 447 (x ^ c2) v (x ^ c1) ' = 1. [para(94(a,1),165(a,1,2,1))]. given #141 (A,wt=11): 90 x ^ (y ^ (x v z)) = y ^ x. [para(17(a,1),26(a,1,2)),flip(a)]. given #142 (F,wt=9): 448 x ^ (c1 ^ (x ^ c2) ') = 0. [para(94(a,1),239(a,1,2)),demod(15(6),16(6))]. given #143 (F,wt=9): 502 c2 v (x v c1) = c2 v x. [para(120(a,2),13(a,1))]. given #144 (T,wt=9): 504 (x v c1) ^ (x v c2) ' = 0. [para(120(a,1),134(a,1,2,1))]. given #145 (T,wt=9): 505 x v (c2 v (x v c1) ') = 1. [para(120(a,1),238(a,1,2)),demod(13(6),14(6))]. given #146 (A,wt=19): 93 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(26(a,1),21(b,1))]. given #147 (F,wt=9): 962 c1 ^ (x ^ (x ^ c2) ') = 0. [para(192(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #148 (F,wt=9): 968 (x ^ c2) v (c1 ^ x) ' = 1. [para(15(a,1),206(a,1,1))]. given #149 (T,wt=9): 969 (c2 ^ x) v (x ^ c1) ' = 1. [para(15(a,1),206(a,1,2,1))]. given #150 (T,wt=9): 970 (c2 ^ (c1 v x)) v c1 ' = 1. [para(17(a,1),206(a,1,2,1))]. given #151 (A,wt=11): 102 x ^ ((y v x) ^ z) = x ^ z. [para(27(a,1),16(a,1,1)),flip(a)]. given #152 (F,wt=9): 974 (c2 ^ (x v c1)) v c1 ' = 1. [para(27(a,1),206(a,1,2,1))]. given #153 (F,wt=9): 1066 x ^ (c1 ^ (c2 ^ x) ') = 0. [para(207(a,1),26(a,1)),flip(a)]. given #154 (T,wt=9): 1067 c1 ^ (c2 ^ (c1 v x)) ' = 0. [para(207(a,1),29(a,1)),flip(a)]. given #155 (T,wt=9): 1154 c1 != 1 | c1 != 0 | c1 ' = c1. [para(23(a,1),72(b,1)),demod(23(11)),flip(a)]. given #156 (A,wt=13): 103 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(27(a,1),16(a,1)),flip(a)]. given #157 (F,wt=9): 1175 c2 != 1 | c2 != 0 | c2 ' = c2. [para(283(a,1),75(a,1)),demod(283(12)),flip(b)]. given #158 (F,wt=9): 1366 (x v c1) ^ (c2 v x) ' = 0. [para(502(a,1),134(a,1,2,1))]. given #159 (T,wt=9): 1368 c2 v (x v (x v c1) ') = 1. [para(502(a,1),238(a,1,2)),demod(13(6),14(6))]. given #160 (T,wt=9): 1384 (c1 v x) ^ (x v c2) ' = 0. [para(13(a,1),504(a,1,1))]. given #161 (A,wt=13): 104 x v y != 1 | 0 != y | y ' = x v y. [para(27(a,1),21(b,1)),demod(74(2)),flip(b)]. given #162 (F,wt=6): 1618 c1 ' != 0 | c1 = 1. [para(173(a,1),104(a,1)),demod(223(10),173(12)),flip(b),xx(a)]. given #163 (F,wt=9): 1392 x v (c2 v (c1 v x) ') = 1. [para(13(a,1),505(a,1,2,2,1))]. given #164 (T,wt=9): 1491 c1 ' v (c2 ^ (c1 v x)) = 1. [para(970(a,1),13(a,1)),flip(a)]. given #165 (T,wt=9): 1526 c1 ^ (c2 ^ (x v c1)) ' = 0. [para(102(a,1),207(a,1))]. given #166 (A,wt=13): 105 (x v y) ^ (x v (z v y)) = x v y. [para(25(a,1),27(a,1,2))]. given #167 (F,wt=9): 1531 c1 ' v (c2 ^ (x v c1)) = 1. [para(974(a,1),13(a,1)),flip(a)]. given #168 (F,wt=9): 1580 (c1 v x) ^ (c2 v x) ' = 0. [para(13(a,1),1366(a,1,1))]. given #169 (T,wt=9): 1581 (c1 v (c2 ^ x)) ^ c2 ' = 0. [para(18(a,1),1366(a,1,2,1)),demod(13(4))]. given #170 (T,wt=9): 1584 (c1 v (x ^ c2)) ^ c2 ' = 0. [para(33(a,1),1366(a,1,2,1)),demod(13(4))]. given #171 (A,wt=11): 106 x ^ (y ^ (z v x)) = y ^ x. [para(27(a,1),26(a,1,2)),flip(a)]. given #172 (F,wt=9): 1593 c2 v (x v (c1 v x) ') = 1. [para(13(a,1),1368(a,1,2,2,1))]. given #173 (F,wt=9): 1594 c2 v (c1 v (c2 ^ x)) ' = 1. [para(1368(a,1),31(a,1)),demod(13(6)),flip(a)]. given #174 (T,wt=9): 1705 c2 ' ^ (c1 v (c2 ^ x)) = 0. [para(1581(a,1),15(a,1)),flip(a)]. given #175 (T,wt=6): 1777 c2 ' != 1 | c2 = 0. [para(1705(a,1),72(b,1)),demod(223(10),1705(15)),flip(a),xx(b)]. given #176 (A,wt=11): 107 x v ((y ^ x) v z) = x v z. [para(33(a,1),14(a,1,1)),flip(a)]. given #177 (F,wt=9): 1713 c2 ' ^ (c1 v (x ^ c2)) = 0. [para(1584(a,1),15(a,1)),flip(a)]. given #178 (F,wt=9): 1750 c2 v (c1 v (x ^ c2)) ' = 1. [para(15(a,1),1594(a,1,2,1,2))]. given #179 (T,wt=10): 256 x v y != 0 | (x v y) ' = 1. [para(39(a,1),44(b,1)),demod(95(2),95(2)),xx(a)]. given #180 (T,wt=10): 258 x v y != 1 | (x v y) ' = 0. [para(42(a,1),44(a,1,2)),demod(15(6),88(6)),xx(b)]. given #181 (A,wt=13): 108 x v (y v (z ^ (x v y))) = x v y. [para(33(a,1),14(a,1)),flip(a)]. given #182 (F,wt=6): 1849 c2 != 1 | c2 ' = 0. [para(111(a,1),258(a,1)),demod(111(6))]. given #183 (F,wt=10): 338 x ^ y != 0 | (x ^ y) ' = 1. [para(39(a,1),46(b,1,2)),demod(13(3),85(3)),xx(a)]. given #184 (T,wt=6): 1885 c1 != 0 | c1 ' = 1. [para(23(a,1),338(a,1)),demod(23(6))]. given #185 (T,wt=10): 340 x ^ y != 1 | (x ^ y) ' = 0. [para(42(a,1),46(a,1)),demod(98(5),98(5)),xx(b)]. given #186 (A,wt=13): 110 1 != x | y ^ x != 0 | x ' = y ^ x. [para(33(a,1),21(a,1)),demod(70(4)),flip(a)]. given #187 (F,wt=10): 1617 (x ^ y) ' != 0 | x ^ y = 1. [para(157(a,1),104(a,1)),demod(223(10),157(11)),flip(b),xx(a)]. given #188 (F,wt=10): 1845 x v y != 0 | (y v x) ' = 1. [para(13(a,1),256(a,1))]. given #189 (T,wt=10): 1847 x v y != 1 | (y v x) ' = 0. [para(13(a,1),258(a,1))]. given #190 (T,wt=10): 1884 x ^ y != 0 | (y ^ x) ' = 1. [para(15(a,1),338(a,1))]. given #191 (A,wt=11): 112 x v (y v (z ^ x)) = y v x. [para(33(a,1),25(a,1,2)),flip(a)]. given #192 (F,wt=10): 1889 x ^ y != 1 | (y ^ x) ' = 0. [para(15(a,1),340(a,1))]. given #193 (F,wt=10): 1897 (x v y) ' != 1 | x v y = 0. [para(127(a,1),110(b,1)),demod(223(10),127(11)),flip(a),xx(b)]. given #194 (T,wt=10): 1916 (x ^ y) ' != 0 | y ^ x = 1. [para(15(a,1),1617(a,1,1))]. given #195 (T,wt=10): 1918 (x v y) ' != 0 | x v y = 1. [para(28(a,1),1617(a,1,1)),demod(28(8))]. given #196 (A,wt=13): 113 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(26(a,1),33(a,1,2))]. given #197 (F,wt=6): 1973 c2 ' != 0 | c2 = 1. [para(111(a,1),1918(a,1,1)),demod(111(7))]. given #198 (F,wt=10): 1965 (x v y) ' != 1 | y v x = 0. [para(13(a,1),1897(a,1,1))]. given #199 (T,wt=10): 1967 (x ^ y) ' != 1 | x ^ y = 0. [para(34(a,1),1897(a,1,1)),demod(34(8))]. given #200 (T,wt=6): 2015 c1 ' != 1 | c1 = 0. [para(23(a,1),1967(a,1,1)),demod(23(7))]. given #201 (A,wt=13): 115 (x v y) ^ (y v (x v z)) = y v x. [para(13(a,1),28(a,1,1))]. given #202 (F,wt=10): 1971 (x v y) ' != 0 | y v x = 1. [para(13(a,1),1918(a,1,1))]. given #203 (F,wt=10): 2014 (x ^ y) ' != 1 | y ^ x = 0. [para(15(a,1),1967(a,1,1))]. given #204 (T,wt=11): 122 (x v c1) ^ (x v c2) = x v c1. [para(111(a,1),28(a,1,2,2))]. given #205 (T,wt=11): 135 (x v y) ^ (x v (y v z)) ' = 0. [para(14(a,1),127(a,1,2,1))]. given #206 (A,wt=13): 116 (x v y) ^ (y v (z v x)) = x v y. [para(13(a,1),28(a,1,2)),demod(14(3))]. given #207 (F,wt=7): 2073 c1 ' v (x v c2) = 1. [para(173(a,1),116(a,1,1)),demod(76(7),173(9))]. given #208 (F,wt=9): 2062 (x v y) ^ (y v x) ' = 0. [para(74(a,1),135(a,1,2,1))]. given #209 (T,wt=9): 2071 (x ^ y) ' v (z v x) = 1. [para(157(a,1),116(a,1,1)),demod(76(6),157(7))]. given #210 (T,wt=9): 2072 (x ^ y) ' v (z v y) = 1. [para(165(a,1),116(a,1,1)),demod(76(6),165(7))]. given #211 (A,wt=17): 117 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(28(a,1),16(a,1,1)),flip(a)]. given #212 (F,wt=9): 2077 (x ^ c1) ' v (y v c2) = 1. [para(286(a,1),116(a,1,1)),demod(76(8),286(11))]. given #213 (F,wt=9): 2079 (c1 ^ x) ' v (y v c2) = 1. [para(295(a,1),116(a,1,1)),demod(76(8),295(11))]. given #214 (T,wt=11): 136 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(127(a,1),16(a,1)),flip(a)]. given #215 (T,wt=11): 150 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(134(a,1),16(a,1)),flip(a)]. given #216 (A,wt=17): 118 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(28(a,1),26(a,1,2)),flip(a)]. given #217 (F,wt=11): 152 (x v y) ^ (x v (z v y)) ' = 0. [para(25(a,1),134(a,1,2,1))]. given #218 (F,wt=11): 163 ((x ^ y) v z) ^ (x v z) ' = 0. [para(31(a,1),134(a,1,2,1))]. given #219 (T,wt=11): 164 x v (y v ((x v y) ^ z) ') = 1. [para(157(a,1),14(a,1)),flip(a)]. given #220 (T,wt=11): 166 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(16(a,1),157(a,1,2,1))]. given #221 (A,wt=12): 124 x ^ (x ' v y) != 0 | x ' v y = x '. [para(86(a,1),21(a,1)),flip(c),xx(a)]. given #222 (F,wt=9): 2343 (x ^ y) v (y ^ x) ' = 1. [para(70(a,1),166(a,1,2,1))]. given #223 (F,wt=11): 170 x v (y v (z ^ (x v y)) ') = 1. [para(165(a,1),14(a,1)),flip(a)]. given #224 (T,wt=11): 175 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(26(a,1),165(a,1,2,1))]. given #225 (T,wt=11): 176 ((x v y) ^ z) v (x ^ z) ' = 1. [para(29(a,1),165(a,1,2,1))]. given #226 (A,wt=12): 125 x v (x ' ^ y) != 1 | x ' ^ y = x '. [para(89(a,1),21(b,1)),flip(c),xx(b)]. given #227 (F,wt=10): 2490 c2 != 1 | c2 ' ^ (x ^ c1) = c2 '. [para(290(a,1),125(a,1))]. given #228 (F,wt=11): 191 x v (y v ((x ^ z) v y) ') = 1. [para(38(a,1),31(a,1,2)),demod(95(2)),flip(a)]. given #229 (T,wt=11): 194 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(41(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #230 (T,wt=11): 201 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(66(a,1),33(a,1,2)),demod(13(5))]. given #231 (A,wt=12): 126 x ^ (y v x ') != 0 | y v x ' = x '. [para(96(a,1),21(a,1)),flip(c),xx(a)]. given #232 (F,wt=11): 202 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(29(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #233 (F,wt=11): 210 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(198(a,1),26(a,1,2)),flip(a)]. given #234 (T,wt=11): 212 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(200(a,1),16(a,1,1)),flip(a)]. given #235 (T,wt=11): 214 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(200(a,1),26(a,1,2)),flip(a)]. given #236 (A,wt=21): 128 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(29(a,1),21(b,1))]. given #237 (F,wt=11): 285 c2 v ((x ^ c1) v y) = c2 v y. [para(67(a,1),31(a,1,2,1))]. given #238 (F,wt=11): 288 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(67(a,1),34(a,1,2))]. given #239 (T,wt=11): 291 c2 v (x v (y ^ c1)) = x v c2. [para(283(a,1),25(a,1,2)),flip(a)]. given #240 (T,wt=11): 322 c2 v ((c1 ^ x) v y) = c2 v y. [para(289(a,1),14(a,1,1)),flip(a)]. given #241 (A,wt=13): 129 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(25(a,1),29(a,1,2,1))]. given #242 (F,wt=11): 324 c2 v (x v (c1 ^ y)) = x v c2. [para(289(a,1),25(a,1,2)),flip(a)]. given #243 (F,wt=11): 372 (x ^ y) v (y ^ x) = x ^ y. [para(70(a,1),34(a,1,2))]. given #244 (T,wt=11): 377 (x v y) ^ (y v x) = x v y. [para(74(a,1),28(a,1,2))]. given #245 (T,wt=11): 446 (x ^ c1) v (x ^ c2) = x ^ c2. [para(94(a,1),33(a,1,2)),demod(13(5))]. given #246 (A,wt=15): 130 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(29(a,1),33(a,1,2)),demod(13(4))]. given #247 (F,wt=11): 620 (c1 v x) ^ (x v c2) = c1 v x. [para(121(a,1),28(a,1,2))]. given #248 (F,wt=11): 627 x ^ ((y v (x v z)) ' ^ u) = 0. [para(25(a,1),131(a,1,2,1,1))]. given #249 (T,wt=11): 634 x ^ (y ^ (z v (x v u)) ') = 0. [para(25(a,1),133(a,1,2,2,1))]. given #250 (T,wt=11): 723 x ^ ((y v (z v x)) ' ^ u) = 0. [para(148(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #251 (A,wt=12): 132 x v (y ^ x ') != 1 | y ^ x ' = x '. [para(99(a,1),21(b,1)),flip(c),xx(b)]. given #252 (F,wt=11): 726 x ^ (y ^ (z v (u v x)) ') = 0. [para(148(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #253 (F,wt=11): 750 x v ((y ^ (x ^ z)) ' v u) = 1. [para(26(a,1),161(a,1,2,1,1))]. given #254 (T,wt=11): 782 x v (y v (z ^ (x ^ u)) ') = 1. [para(26(a,1),162(a,1,2,2,1))]. given #255 (T,wt=11): 797 x v ((y ^ (z ^ x)) ' v u) = 1. [para(16(a,1),169(a,1,2,1,1))]. given #256 (A,wt=12): 137 x v (x v y) ' != 1 | (x v y) ' = x '. [para(127(a,1),21(b,1)),flip(c),xx(b)]. given #257 (F,wt=11): 802 (c2 ^ x) v ((c1 ^ x) ' v y) = 1. [para(66(a,1),169(a,1,2,1,1))]. given #258 (F,wt=11): 806 (x ^ c2) v ((x ^ c1) ' v y) = 1. [para(94(a,1),169(a,1,2,1,1))]. given #259 (T,wt=11): 814 x v (y v (z ^ (u ^ x)) ') = 1. [para(171(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #260 (T,wt=11): 817 (c2 ^ x) v (y ^ (c1 ^ x)) ' = 1. [para(66(a,1),171(a,1,2,1,2))]. given #261 (A,wt=13): 143 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(15(a,1),30(a,1,2,2,1))]. given #262 (F,wt=11): 820 (x ^ c2) v (y ^ (x ^ c1)) ' = 1. [para(94(a,1),171(a,1,2,1,2))]. given #263 (F,wt=11): 939 (c2 ^ x) v (y v (c1 ^ x) ') = 1. [para(66(a,1),174(a,1,2,2,1))]. given #264 (T,wt=11): 944 (x ^ c2) v (y v (x ^ c1) ') = 1. [para(94(a,1),174(a,1,2,2,1))]. given #265 (T,wt=11): 951 x v (y v (y v (x ^ z)) ') = 1. [para(189(a,1),31(a,1,2)),demod(95(2)),flip(a)]. given #266 (A,wt=25): 144 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x ' = y ^ ((x ^ y) v z). [para(30(a,1),21(b,1))]. given #267 (F,wt=11): 961 x ^ (y ^ (y ^ (x v z)) ') = 0. [para(192(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #268 (F,wt=11): 979 (c2 ^ (x v (c1 v y))) v c1 ' = 1. [para(78(a,1),206(a,1,2,1))]. given #269 (T,wt=11): 980 (c2 ^ (x v (y v c1))) v c1 ' = 1. [para(101(a,1),206(a,1,2,1))]. given #270 (T,wt=11): 1080 c1 ^ ((x v (c2 v y)) ' ^ z) = 0. [para(25(a,1),215(a,1,2,1,1))]. given #271 (A,wt=15): 145 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(25(a,1),30(a,1,2,2))]. given #272 (F,wt=11): 1140 c1 ^ (x ^ (y v (c2 v z)) ') = 0. [para(217(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #273 (F,wt=11): 1147 c1 ^ ((x v (y v c2)) ' ^ z) = 0. [para(240(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #274 (T,wt=11): 1149 c1 ^ (x ^ (y v (z v c2)) ') = 0. [para(240(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #275 (T,wt=11): 1187 (x v (y ^ z)) ^ (x v y) ' = 0. [para(79(a,1),134(a,1,2,1))]. given #276 (A,wt=19): 146 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(30(a,1),33(a,1,2)),demod(13(5))]. given #277 (F,wt=11): 1189 x v (y v (x v (y ^ z)) ') = 1. [para(79(a,1),238(a,1,2)),demod(13(5),14(5))]. given #278 (F,wt=11): 1211 c2 v ((x ^ (y ^ c1)) ' v z) = 1. [para(16(a,1),294(a,1,2,1,1))]. given #279 (T,wt=11): 1224 c2 v (x v (y ^ (z ^ c1)) ') = 1. [para(296(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #280 (T,wt=11): 1299 c2 v ((x ^ (c1 ^ y)) ' v z) = 1. [para(26(a,1),328(a,1,2,1,1))]. given #281 (A,wt=15): 147 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(30(a,1),29(a,1,2)),demod(29(3)),flip(a)]. given #282 (F,wt=11): 1312 c2 v (x v (y ^ (c1 ^ z)) ') = 1. [para(26(a,1),330(a,1,2,2,1))]. given #283 (F,wt=11): 1346 (x ^ (y v z)) v (x ^ y) ' = 1. [para(90(a,1),165(a,1,2,1))]. given #284 (T,wt=11): 1347 x ^ (y ^ (x ^ (y v z)) ') = 0. [para(90(a,1),239(a,1,2)),demod(15(5),16(5))]. given #285 (T,wt=11): 1358 x ^ (c1 ^ (c2 ^ (x v y)) ') = 0. [para(448(a,1),29(a,1,2)),demod(98(2),15(5)),flip(a)]. given #286 (A,wt=12): 151 x v (y v x) ' != 1 | (y v x) ' = x '. [para(134(a,1),21(b,1)),flip(c),xx(b)]. given #287 (F,wt=11): 1365 (x v c1) ^ (c2 v x) = x v c1. [para(502(a,1),27(a,1,2))]. given #288 (F,wt=11): 1376 (x v c1) ^ (y v (c2 v x)) ' = 0. [para(502(a,1),148(a,1,2,1,2))]. given #289 (T,wt=11): 1377 (x v c1) ^ ((c2 v x) ' ^ y) = 0. [para(502(a,1),149(a,1,2,1,1))]. given #290 (T,wt=11): 1378 (x v c1) ^ (y ^ (c2 v x) ') = 0. [para(502(a,1),153(a,1,2,2,1))]. given #291 (A,wt=12): 154 c1 v (c2 ' ^ x) != 1 | c2 ' ^ x = c1 '. [para(140(a,1),21(b,1)),flip(c),xx(b)]. given #292 (F,wt=10): 3928 c1 != 1 | c2 ' ^ (x ^ c1) = c1 '. [para(109(a,1),154(a,1))]. given #293 (F,wt=11): 1387 (x v c1) ^ ((x v c2) ' ^ y) = 0. [para(504(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #294 (T,wt=11): 1389 (x v c1) ^ (y ^ (x v c2) ') = 0. [para(504(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #295 (T,wt=11): 1394 x v (c2 v (c1 v (x ^ y)) ') = 1. [para(505(a,1),31(a,1,2)),demod(95(2),13(5)),flip(a)]. given #296 (A,wt=12): 155 c1 v (x ^ c2 ') != 1 | x ^ c2 ' = c1 '. [para(142(a,1),21(b,1)),flip(c),xx(b)]. given #297 (F,wt=11): 1467 (x ^ c2) v ((c1 ^ x) ' v y) = 1. [para(968(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #298 (F,wt=11): 1469 (x ^ c2) v (y v (c1 ^ x) ') = 1. [para(968(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #299 (T,wt=11): 1479 (c2 ^ x) v ((x ^ c1) ' v y) = 1. [para(969(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #300 (T,wt=11): 1481 (c2 ^ x) v (y v (x ^ c1) ') = 1. [para(969(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #301 (A,wt=17): 156 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(16(a,1),31(a,1,2,1))]. given #302 (F,wt=11): 1492 (c2 ^ (c1 v x)) v (c1 ' v y) = 1. [para(970(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #303 (F,wt=11): 1494 (c2 ^ (c1 v x)) v (y v c1 ') = 1. [para(970(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #304 (T,wt=11): 1510 ((x v y) ^ z) v (y ^ z) ' = 1. [para(102(a,1),165(a,1,2,1))]. given #305 (T,wt=11): 1512 x ^ (y ^ ((z v x) ^ y) ') = 0. [para(41(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #306 (A,wt=21): 158 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x ' = (x ^ z) v y. [para(31(a,1),21(a,1))]. given #307 (F,wt=11): 1524 x ^ (y ^ (y ^ (z v x)) ') = 0. [para(192(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #308 (F,wt=11): 1528 x ^ (c1 ^ (c2 ^ (y v x)) ') = 0. [para(448(a,1),102(a,1,2)),demod(98(2),15(5)),flip(a)]. given #309 (T,wt=11): 1532 (c2 ^ (x v c1)) v (c1 ' v y) = 1. [para(974(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #310 (T,wt=11): 1534 (c2 ^ (x v c1)) v (y v c1 ') = 1. [para(974(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #311 (A,wt=13): 159 x v ((y ^ (x ^ z)) v u) = x v u. [para(26(a,1),31(a,1,2,1))]. given #312 (F,wt=11): 1549 c1 ^ ((c2 ^ (c1 v x)) ' ^ y) = 0. [para(1067(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #313 (F,wt=11): 1551 c1 ^ (c2 ^ (x v (c1 v y))) ' = 0. [para(25(a,1),1067(a,1,2,1,2))]. given #314 (T,wt=11): 1552 c1 ^ (x ^ (c2 ^ (c1 v y)) ') = 0. [para(1067(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #315 (T,wt=11): 1589 (c1 v (x ^ (c2 ^ y))) ^ c2 ' = 0. [para(91(a,1),1366(a,1,2,1)),demod(13(5))]. given #316 (A,wt=15): 160 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(31(a,1),27(a,1,2)),demod(15(4))]. given #317 (F,wt=11): 1590 (c1 v (x ^ (y ^ c2))) ^ c2 ' = 0. [para(109(a,1),1366(a,1,2,1)),demod(13(5))]. given #318 (F,wt=11): 1605 (c1 v x) ^ ((x v c2) ' ^ y) = 0. [para(1384(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #319 (T,wt=11): 1608 (c1 v x) ^ (y ^ (x v c2) ') = 0. [para(1384(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #320 (T,wt=11): 1639 c1 ' v ((c2 ^ (c1 v x)) v y) = 1. [para(1491(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #321 (A,wt=12): 167 x ^ (x ^ y) ' != 0 | (x ^ y) ' = x '. [para(157(a,1),21(a,1)),flip(c),xx(a)]. given #322 (F,wt=11): 1640 c1 ' v (x v (c2 ^ (c1 v y))) = 1. [para(1491(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #323 (F,wt=11): 1641 c1 ' v (c2 ^ (x v (c1 v y))) = 1. [para(25(a,1),1491(a,1,2,2))]. given #324 (T,wt=11): 1652 c1 ^ (c2 ^ (x v (y v c1))) ' = 0. [para(14(a,1),1526(a,1,2,1,2))]. given #325 (T,wt=11): 1653 c1 ^ ((c2 ^ (x v c1)) ' ^ y) = 0. [para(1526(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #326 (A,wt=12): 172 x ^ (y ^ x) ' != 0 | (y ^ x) ' = x '. [para(165(a,1),21(a,1)),flip(c),xx(a)]. given #327 (F,wt=11): 1655 c1 ^ (x ^ (c2 ^ (y v c1)) ') = 0. [para(1526(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #328 (F,wt=11): 1672 (c1 v x) ^ (c2 v x) = c1 v x. [para(119(a,1),105(a,1,2))]. given #329 (T,wt=11): 1687 c1 ' v ((c2 ^ (x v c1)) v y) = 1. [para(1531(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #330 (T,wt=11): 1688 c1 ' v (c2 ^ (x v (y v c1))) = 1. [para(14(a,1),1531(a,1,2,2))]. given #331 (A,wt=13): 177 (x ^ ((y ^ x) v z)) v (y ^ x) ' = 1. [para(30(a,1),165(a,1,2,1))]. given #332 (F,wt=11): 1689 c1 ' v (x v (c2 ^ (y v c1))) = 1. [para(1531(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #333 (F,wt=11): 1699 (c1 v x) ^ ((c2 v x) ' ^ y) = 0. [para(1580(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #334 (T,wt=11): 1701 (c1 v x) ^ (y ^ (c2 v x) ') = 0. [para(1580(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #335 (T,wt=11): 1706 (c1 v (c2 ^ x)) ^ (c2 ' ^ y) = 0. [para(1581(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #336 (A,wt=12): 181 c2 ^ (c1 ' v x) != 0 | c2 ' = c1 ' v x. [para(178(a,1),21(a,1)),xx(a)]. given #337 (F,wt=11): 1708 (c1 v (c2 ^ x)) ^ (y ^ c2 ') = 0. [para(1581(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #338 (F,wt=11): 1714 (c1 v (x ^ c2)) ^ (c2 ' ^ y) = 0. [para(1584(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #339 (T,wt=11): 1716 (c1 v (x ^ c2)) ^ (y ^ c2 ') = 0. [para(1584(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #340 (T,wt=11): 1723 (x ^ (y v z)) v (x ^ z) ' = 1. [para(106(a,1),165(a,1,2,1))]. given #341 (A,wt=13): 182 x v (y v ((y v x) ^ z)) = x v y. [para(13(a,1),32(a,1,2,2,1))]. given #342 (F,wt=11): 1725 x ^ (y ^ (x ^ (z v y)) ') = 0. [para(106(a,1),239(a,1,2)),demod(15(5),16(5))]. given #343 (F,wt=11): 1749 c2 v ((c1 v (c2 ^ x)) ' v y) = 1. [para(1594(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #344 (T,wt=11): 1752 c2 v (x v (c1 v (c2 ^ y)) ') = 1. [para(1594(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #345 (T,wt=11): 1753 c2 v (c1 v (x ^ (c2 ^ y))) ' = 1. [para(26(a,1),1594(a,1,2,1,2))]. given #346 (A,wt=25): 183 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x ' = y v ((x v y) ^ z). [para(32(a,1),21(a,1))]. given #347 (F,wt=11): 1764 c2 ' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(1705(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #348 (F,wt=11): 1765 c2 ' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(1705(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #349 (T,wt=7): 4947 c2 ' ^ (x ^ c1) = 0. [para(20(a,1),1765(a,1,2,2,2)),demod(13(5),82(5))]. given #350 (T,wt=11): 1766 c2 ' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(26(a,1),1705(a,1,2,2))]. given #351 (A,wt=15): 184 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(26(a,1),32(a,1,2,2))]. given #352 (F,wt=11): 1784 ((x ^ y) v z) ^ (y v z) ' = 0. [para(107(a,1),134(a,1,2,1))]. given #353 (F,wt=11): 1786 x v (y v ((z ^ x) v y) ') = 1. [para(38(a,1),107(a,1,2)),demod(95(2)),flip(a)]. given #354 (T,wt=11): 1805 x v (y v (y v (z ^ x)) ') = 1. [para(189(a,1),107(a,1,2)),demod(95(2)),flip(a)]. given #355 (T,wt=11): 1809 x v (c2 v (c1 v (y ^ x)) ') = 1. [para(505(a,1),107(a,1,2)),demod(95(2),13(5)),flip(a)]. given #356 (A,wt=19): 185 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(32(a,1),27(a,1,2)),demod(15(5))]. given #357 (F,wt=11): 1818 c2 ' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(1713(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #358 (F,wt=11): 1819 c2 ' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(16(a,1),1713(a,1,2,2))]. given #359 (T,wt=11): 1820 c2 ' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(1713(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #360 (T,wt=11): 1831 c2 v ((c1 v (x ^ c2)) ' v y) = 1. [para(1750(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #361 (A,wt=13): 186 (x v ((y v x) ^ z)) ^ (y v x) ' = 0. [para(32(a,1),134(a,1,2,1))]. given #362 (F,wt=11): 1832 c2 v (c1 v (x ^ (y ^ c2))) ' = 1. [para(16(a,1),1750(a,1,2,1,2))]. given #363 (F,wt=11): 1834 c2 v (x v (c1 v (y ^ c2)) ') = 1. [para(1750(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #364 (T,wt=11): 1931 (x v (y ^ z)) ^ (x v z) ' = 0. [para(112(a,1),134(a,1,2,1))]. given #365 (T,wt=11): 1934 x v (y v (x v (z ^ y)) ') = 1. [para(112(a,1),238(a,1,2)),demod(13(5),14(5))]. given #366 (A,wt=15): 187 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(32(a,1),31(a,1,2)),demod(31(3)),flip(a)]. given #367 (F,wt=11): 2026 x v (y v (z ^ (y v x)) ') = 1. [para(115(a,1),168(a,1,2,1,2)),demod(14(5))]. given #368 (F,wt=11): 2051 x v (c2 v (y ^ (x v c1)) ') = 1. [para(122(a,1),171(a,1,2,1,2)),demod(14(7))]. given #369 (T,wt=11): 2058 (x v y) ^ (y v (x v z)) ' = 0. [para(13(a,1),135(a,1,1))]. given #370 (T,wt=11): 2059 (x v y) ^ (y v (z v x)) ' = 0. [para(13(a,1),135(a,1,2,1)),demod(14(3))]. given #371 (A,wt=12): 188 c2 ^ (x v c1 ') != 0 | c2 ' = x v c1 '. [para(180(a,1),21(a,1)),xx(a)]. given #372 (F,wt=11): 2063 (x v c1) ^ (x v (c2 v y)) ' = 0. [para(119(a,1),135(a,1,2,1,2))]. given #373 (F,wt=11): 2064 (x v c1) ^ (x v (y v c2)) ' = 0. [para(121(a,1),135(a,1,2,1,2))]. given #374 (T,wt=11): 2085 (x ^ (y ^ z)) ' v (u v y) = 1. [para(168(a,1),116(a,1,1)),demod(76(7),168(9))]. given #375 (T,wt=11): 2086 (x ^ (y ^ z)) ' v (u v z) = 1. [para(171(a,1),116(a,1,1)),demod(76(7),171(9))]. given #376 (A,wt=16): 190 x ^ (y v (x v y) ') != 0 | y v (x v y) ' = x '. [para(38(a,1),21(a,1)),flip(c),xx(a)]. given #377 (F,wt=11): 2088 (c1 ^ x) ' v (y v (c2 ^ x)) = 1. [para(206(a,1),116(a,1,1)),demod(76(9),206(13))]. given #378 (F,wt=11): 2092 (x ^ (y ^ c1)) ' v (z v c2) = 1. [para(296(a,1),116(a,1,1)),demod(76(9),296(13))]. given #379 (T,wt=11): 2094 (x ^ (c1 ^ y)) ' v (z v c2) = 1. [para(331(a,1),116(a,1,1)),demod(76(9),331(13))]. given #380 (T,wt=11): 2095 (x ^ c1) ' v (y v (x ^ c2)) = 1. [para(447(a,1),116(a,1,1)),demod(76(9),447(13))]. given #381 (A,wt=16): 193 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(41(a,1),21(b,1)),flip(c),xx(b)]. given #382 (F,wt=11): 2099 (c1 ^ x) ' v (y v (x ^ c2)) = 1. [para(968(a,1),116(a,1,1)),demod(76(9),968(13))]. given #383 (F,wt=11): 2100 (x ^ c1) ' v (y v (c2 ^ x)) = 1. [para(969(a,1),116(a,1,1)),demod(76(9),969(13))]. given #384 (T,wt=11): 2101 (c1 v (c2 ^ x)) ' v (y v c2) = 1. [para(1594(a,1),116(a,1,1)),demod(76(10),1594(15))]. given #385 (T,wt=11): 2103 (c1 v (x ^ c2)) ' v (y v c2) = 1. [para(1750(a,1),116(a,1,1)),demod(76(10),1750(15))]. given #386 (A,wt=13): 195 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(15(a,1),34(a,1,1))]. given #387 (F,wt=11): 2121 (x v y) ^ ((y v x) ' ^ z) = 0. [para(2062(a,1),16(a,1,1)),demod(88(2)),flip(a)]. given #388 (F,wt=11): 2123 (x v y) ^ (z ^ (y v x) ') = 0. [para(2062(a,1),26(a,1,2)),demod(98(2)),flip(a)]. given #389 (T,wt=11): 2141 c2 v (x v ((x v c1) ^ y) ') = 1. [para(502(a,1),2071(a,1,2)),demod(13(7),14(7))]. given #390 (T,wt=11): 2163 c2 v (x v (y ^ (x v c1)) ') = 1. [para(502(a,1),2072(a,1,2)),demod(13(7),14(7))]. given #391 (A,wt=13): 196 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(15(a,1),34(a,1,2)),demod(16(3))]. given #392 (F,wt=9): 5913 (x v y) ' ^ (z ^ x) = 0. [para(127(a,1),196(a,1,1)),demod(82(6),127(7))]. given #393 (F,wt=9): 5915 (x v y) ' ^ (z ^ y) = 0. [para(134(a,1),196(a,1,1)),demod(82(6),134(7))]. given #394 (T,wt=9): 5919 (c2 v x) ' ^ (y ^ c1) = 0. [para(203(a,1),196(a,1,1)),demod(82(8),203(11))]. given #395 (T,wt=9): 5920 (x v c2) ' ^ (y ^ c1) = 0. [para(205(a,1),196(a,1,1)),demod(82(8),205(11))]. given #396 (A,wt=17): 197 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(34(a,1),25(a,1,2)),flip(a)]. given #397 (F,wt=11): 2188 (c1 v x) ^ (c2 v (x v y)) ' = 0. [para(1384(a,1),117(a,1,2)),demod(15(4),88(4),13(6)),flip(a)]. given #398 (F,wt=11): 2215 x ^ (y ^ ((y ^ x) v z) ') = 0. [para(15(a,1),136(a,1,2,2,1,1))]. given #399 (T,wt=11): 2218 c1 ^ (x ^ ((c2 ^ x) v y) ') = 0. [para(136(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #400 (T,wt=11): 2230 x ^ (y ^ (z v (y ^ x)) ') = 0. [para(15(a,1),150(a,1,2,2,1,2))]. given #401 (A,wt=17): 199 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1 ' = c2 ^ x. [para(66(a,1),21(b,1))]. given #402 (F,wt=11): 2233 c1 ^ (x ^ (y v (c2 ^ x)) ') = 0. [para(150(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #403 (F,wt=11): 2262 (x v y) ^ (z v (y v x)) ' = 0. [para(13(a,1),152(a,1,2,1)),demod(14(3))]. given #404 (T,wt=11): 2268 (x v (y ^ c1)) ^ (x v c2) ' = 0. [para(283(a,1),152(a,1,2,1,2))]. given #405 (T,wt=11): 2270 (x v (c1 ^ y)) ^ (x v c2) ' = 0. [para(289(a,1),152(a,1,2,1,2))]. given #406 (A,wt=13): 204 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(30(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #407 (F,wt=11): 2286 (x v (y ^ z)) ^ (y v x) ' = 0. [para(13(a,1),163(a,1,1))]. given #408 (F,wt=11): 2287 ((x ^ y) v z) ^ (z v x) ' = 0. [para(13(a,1),163(a,1,2,1))]. given #409 (T,wt=11): 2289 (x v y) ' ^ ((x ^ z) v y) = 0. [para(163(a,1),15(a,1)),flip(a)]. given #410 (T,wt=11): 2291 ((x ^ y) v (x ^ z)) ^ x ' = 0. [para(18(a,1),163(a,1,2,1))]. given #411 (A,wt=13): 208 c2 v x != 1 | c1 != 0 | c1 ' = c2 v x. [para(198(a,1),21(b,1)),demod(119(4))]. given #412 (F,wt=11): 2296 ((x ^ y) v (z ^ x)) ^ x ' = 0. [para(33(a,1),163(a,1,2,1))]. given #413 (F,wt=11): 2301 ((x ^ c1) v y) ^ (c2 v y) ' = 0. [para(67(a,1),163(a,1,1,1))]. given #414 (T,wt=11): 2302 ((c2 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(283(a,1),163(a,1,2,1))]. given #415 (T,wt=11): 2304 ((c2 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(289(a,1),163(a,1,2,1))]. given #416 (A,wt=13): 213 x v c2 != 1 | c1 != 0 | c1 ' = x v c2. [para(200(a,1),21(b,1)),demod(121(4))]. given #417 (F,wt=11): 2324 x v (y v ((y v x) ^ z) ') = 1. [para(13(a,1),164(a,1,2,2,1,1))]. given #418 (F,wt=11): 2337 c2 v (x v ((c1 v x) ^ y) ') = 1. [para(164(a,1),1392(a,1,2,2,1)),demod(84(8),13(8),82(8),13(7))]. given #419 (T,wt=11): 2338 (x ^ y) v (y ^ (x ^ z)) ' = 1. [para(15(a,1),166(a,1,1))]. given #420 (T,wt=11): 2339 (x ^ y) v (y ^ (z ^ x)) ' = 1. [para(15(a,1),166(a,1,2,1)),demod(16(3))]. given #421 (A,wt=12): 216 c1 v (c2 v x) ' != 1 | (c2 v x) ' = c1 '. [para(203(a,1),21(b,1)),flip(c),xx(b)]. given #422 (F,wt=11): 2342 (x ^ c2) v (x ^ (y ^ c1)) ' = 1. [para(67(a,1),166(a,1,2,1,2))]. given #423 (F,wt=11): 2362 (x ^ y) v ((y ^ x) ' v z) = 1. [para(2343(a,1),14(a,1,1)),demod(85(2)),flip(a)]. given #424 (T,wt=11): 2365 (x ^ y) v (z v (y ^ x) ') = 1. [para(2343(a,1),25(a,1,2)),demod(95(2)),flip(a)]. given #425 (T,wt=11): 2379 (x ^ y) ' v (z v (y ^ x)) = 1. [para(2343(a,1),116(a,1,1)),demod(76(7),2343(9))]. given #426 (A,wt=19): 219 x v (y v z) != 1 | z ^ (x v y) != 0 | z ' = x v y. [para(14(a,1),43(a,1))]. given #427 (F,wt=11): 2393 c2 v (x v (y ^ (c1 v x)) ') = 1. [para(170(a,1),1392(a,1,2,2,1)),demod(84(8),13(8),82(8),13(7))]. given #428 (F,wt=11): 2394 (x ^ y) v (z ^ (y ^ x)) ' = 1. [para(15(a,1),175(a,1,2,1)),demod(16(3))]. given #429 (T,wt=11): 2400 (x ^ (c2 v y)) v (x ^ c1) ' = 1. [para(198(a,1),175(a,1,2,1,2))]. given #430 (T,wt=11): 2401 (x ^ (y v c2)) v (x ^ c1) ' = 1. [para(200(a,1),175(a,1,2,1,2))]. given #431 (A,wt=13): 220 x v y != 1 | x ^ y != 0 | y ' = x. [para(15(a,1),43(b,1))]. given #432 (F,wt=11): 2434 (x ^ y) ' v ((x v z) ^ y) = 1. [para(176(a,1),13(a,1)),flip(a)]. given #433 (F,wt=11): 2435 (x ^ (y v z)) v (y ^ x) ' = 1. [para(15(a,1),176(a,1,1))]. given #434 (T,wt=11): 2436 ((x v y) ^ z) v (z ^ x) ' = 1. [para(15(a,1),176(a,1,2,1))]. given #435 (T,wt=11): 2438 ((x v y) ^ (x v z)) v x ' = 1. [para(17(a,1),176(a,1,2,1))]. given #436 (A,wt=19): 221 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z) ' = x. [para(16(a,1),43(b,1))]. given #437 (F,wt=11): 2443 ((x v y) ^ (z v x)) v x ' = 1. [para(27(a,1),176(a,1,2,1))]. given #438 (F,wt=11): 2447 ((c1 v x) ^ (c2 v y)) v c1 ' = 1. [para(198(a,1),176(a,1,2,1))]. given #439 (T,wt=11): 2448 ((c1 v x) ^ (y v c2)) v c1 ' = 1. [para(200(a,1),176(a,1,2,1))]. given #440 (T,wt=11): 2458 ((c2 v x) ^ y) v (c1 ^ y) ' = 1. [para(119(a,1),176(a,1,1,1))]. given #441 (A,wt=13): 222 1 != x | x ^ y != 0 | (x ^ y) ' = x. [para(18(a,1),43(a,1)),demod(15(4),69(4)),flip(a)]. given #442 (F,wt=11): 2464 ((x v c2) ^ y) v (c1 ^ y) ' = 1. [para(121(a,1),176(a,1,1,1))]. given #443 (F,wt=11): 2495 x v (y v ((y ^ z) v x) ') = 1. [para(191(a,1),25(a,1)),flip(a)]. given #444 (T,wt=11): 2497 x v ((x ^ y) v (x ^ z)) ' = 1. [para(191(a,1),31(a,1)),flip(a)]. given #445 (T,wt=11): 2501 c2 v (x v ((y ^ c1) v x) ') = 1. [para(67(a,1),191(a,1,2,2,1,1))]. given #446 (A,wt=19): 224 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z) ' = y. [para(25(a,1),43(a,1))]. given #447 (F,wt=11): 2511 c2 v (x v ((c1 ^ y) v x) ') = 1. [para(191(a,1),1392(a,1,2,2,1)),demod(84(8),13(8),82(8),13(7))]. given #448 (F,wt=11): 2512 x v ((x ^ y) v (z ^ x)) ' = 1. [para(191(a,1),107(a,1)),flip(a)]. given #449 (T,wt=11): 2516 x ^ (y ^ ((y v z) ^ x) ') = 0. [para(194(a,1),26(a,1)),flip(a)]. given #450 (T,wt=11): 2517 x ^ ((x v y) ^ (x v z)) ' = 0. [para(194(a,1),29(a,1)),flip(a)]. given #451 (A,wt=19): 225 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z ' = x ^ y. [para(26(a,1),43(b,1))]. given #452 (F,wt=11): 2518 c1 ^ (x ^ ((c2 v y) ^ x) ') = 0. [para(194(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #453 (F,wt=11): 2527 c1 ^ (x ^ ((y v c2) ^ x) ') = 0. [para(121(a,1),194(a,1,2,2,1,1))]. given #454 (T,wt=11): 2532 x ^ ((x v y) ^ (z v x)) ' = 0. [para(194(a,1),102(a,1)),flip(a)]. given #455 (T,wt=11): 2534 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(15(a,1),201(a,1,1))]. given #456 (A,wt=13): 226 1 != x | y ^ x != 0 | (y ^ x) ' = x. [para(33(a,1),43(a,1)),demod(15(4),70(4)),flip(a)]. given #457 (F,wt=11): 2535 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(15(a,1),201(a,1,2))]. given #458 (F,wt=11): 2585 c1 ^ (x ^ (x ^ (c2 v y)) ') = 0. [para(192(a,1),202(a,1,2)),demod(15(3),88(3)),flip(a)]. given #459 (T,wt=11): 2599 c1 ^ ((c1 v x) ^ (c2 v y)) ' = 0. [para(202(a,1),194(a,1))]. given #460 (T,wt=11): 2600 x ^ (c1 ^ (x ^ (c2 v y)) ') = 0. [para(210(a,1),239(a,1,2)),demod(15(7),16(7))]. given #461 (A,wt=12): 228 x ^ (x ' v y) != 0 | (x ' v y) ' = x. [para(86(a,1),43(a,1)),demod(15(6)),xx(a)]. given #462 (F,wt=11): 2628 c1 ^ (x ^ (x ^ (y v c2)) ') = 0. [para(192(a,1),212(a,1,2)),demod(15(3),88(3)),flip(a)]. given #463 (F,wt=11): 2641 c1 ^ ((c1 v x) ^ (y v c2)) ' = 0. [para(212(a,1),194(a,1))]. given #464 (T,wt=11): 2643 x ^ (c1 ^ (x ^ (y v c2)) ') = 0. [para(214(a,1),239(a,1,2)),demod(15(7),16(7))]. given #465 (T,wt=11): 2726 c2 v (x v (x v (y ^ c1)) ') = 1. [para(189(a,1),285(a,1,2)),demod(13(3),85(3)),flip(a)]. given #466 (A,wt=12): 229 x ^ (y v x ') != 0 | (y v x ') ' = x. [para(96(a,1),43(a,1)),demod(15(6)),xx(a)]. given #467 (F,wt=11): 2739 c2 v ((c2 ^ x) v (y ^ c1)) ' = 1. [para(285(a,1),191(a,1))]. given #468 (F,wt=11): 2758 x ^ (c1 ^ (y v (c2 ^ x)) ') = 0. [para(288(a,1),148(a,1,2,1,2)),demod(16(7))]. given #469 (T,wt=11): 2766 (c2 ^ x) v (x ^ (c1 ^ y)) ' = 1. [para(288(a,1),2071(a,1,2)),demod(16(3),13(7))]. given #470 (T,wt=11): 2767 (c2 ^ x) v (y ^ (x ^ c1)) ' = 1. [para(288(a,1),2072(a,1,2)),demod(13(7))]. given #471 (A,wt=21): 230 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y) ' = x. [para(31(a,1),43(a,1)),demod(15(6))]. given #472 (F,wt=11): 2772 x v (c2 v (x v (y ^ c1)) ') = 1. [para(291(a,1),238(a,1,2)),demod(13(7),14(7))]. given #473 (F,wt=11): 2800 ((c1 ^ x) v y) ^ (c2 v y) ' = 0. [para(322(a,1),134(a,1,2,1))]. given #474 (T,wt=11): 2817 c2 v (x v (x v (c1 ^ y)) ') = 1. [para(189(a,1),322(a,1,2)),demod(13(3),85(3)),flip(a)]. given #475 (T,wt=11): 2830 c2 v ((c2 ^ x) v (c1 ^ y)) ' = 1. [para(322(a,1),191(a,1))]. given #476 (A,wt=12): 231 x ^ (x ^ y) ' != 0 | x ^ y = x. [para(157(a,1),43(a,1)),demod(15(6),223(11)),xx(a)]. given #477 (F,wt=11): 2859 x v (c2 v (x v (c1 ^ y)) ') = 1. [para(324(a,1),238(a,1,2)),demod(13(7),14(7))]. given #478 (F,wt=11): 2926 x ^ (c1 ^ (y v (x ^ c2)) ') = 0. [para(446(a,1),138(a,1,2,1,2)),demod(16(7))]. given #479 (T,wt=11): 2953 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(67(a,1),130(a,1,1)),demod(33(8)),flip(a)]. given #480 (T,wt=11): 2954 (x v y) ^ (z ^ x) = z ^ x. [para(70(a,1),130(a,1,1)),demod(33(5)),flip(a)]. given #481 (A,wt=12): 232 x ^ (y ^ x) ' != 0 | y ^ x = x. [para(165(a,1),43(a,1)),demod(15(6),223(11)),xx(a)]. given #482 (F,wt=11): 3020 (x v c2) ^ (c1 v x) = c1 v x. [para(620(a,1),15(a,1)),flip(a)]. given #483 (F,wt=11): 3030 x v (c2 v (y ^ (c1 v x)) ') = 1. [para(620(a,1),171(a,1,2,1,2)),demod(14(7))]. given #484 (T,wt=11): 3210 (x ^ c2) v (y ^ (c1 ^ x)) ' = 1. [para(15(a,1),817(a,1,1))]. given #485 (T,wt=11): 3211 (c2 ^ x) v (c1 ^ (x ^ y)) ' = 1. [para(15(a,1),817(a,1,2,1)),demod(16(5))]. given #486 (A,wt=12): 234 c2 ^ (c1 ' v x) != 0 | (c1 ' v x) ' = c2. [para(178(a,1),43(a,1)),demod(15(8)),xx(a)]. given #487 (F,wt=11): 3212 (c2 ^ (c1 v x)) v (y ^ c1) ' = 1. [para(17(a,1),817(a,1,2,1,2))]. given #488 (F,wt=11): 3214 (c2 ^ x) v (c1 ^ (y ^ x)) ' = 1. [para(26(a,1),817(a,1,2,1))]. given #489 (T,wt=11): 3215 (c2 ^ (x v c1)) v (y ^ c1) ' = 1. [para(27(a,1),817(a,1,2,1,2))]. given #490 (T,wt=11): 3238 (c2 ^ (x v y)) v (c1 ^ x) ' = 1. [para(90(a,1),817(a,1,2,1))]. given #491 (A,wt=25): 235 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z)) ' = x. [para(32(a,1),43(a,1)),demod(15(7))]. given #492 (F,wt=11): 3243 (c2 ^ (x v y)) v (c1 ^ y) ' = 1. [para(106(a,1),817(a,1,2,1))]. given #493 (F,wt=11): 3290 (x ^ c2) v (x ^ (c1 ^ y)) ' = 1. [para(15(a,1),820(a,1,2,1)),demod(16(5))]. given #494 (T,wt=11): 3292 (c2 ^ (x v y)) v (x ^ c1) ' = 1. [para(29(a,1),820(a,1,2,1)),demod(15(3))]. given #495 (T,wt=11): 3302 (c2 ^ (x v y)) v (y ^ c1) ' = 1. [para(102(a,1),820(a,1,2,1)),demod(15(3))]. given #496 (A,wt=12): 236 c2 ^ (x v c1 ') != 0 | (x v c1 ') ' = c2. [para(180(a,1),43(a,1)),demod(15(8)),xx(a)]. given #497 (F,wt=11): 3362 x v ((y ^ x) v (x ^ z)) ' = 1. [para(951(a,1),107(a,1)),flip(a)]. given #498 (F,wt=11): 3364 c2 v ((x ^ c1) v (c2 ^ y)) ' = 1. [para(951(a,1),285(a,1)),flip(a)]. given #499 (T,wt=11): 3365 c2 v ((c1 ^ x) v (c2 ^ y)) ' = 1. [para(951(a,1),322(a,1)),flip(a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 437 (0.00 of 4.20 sec). given #500 (T,wt=11): 3441 x ^ ((y v x) ^ (x v z)) ' = 0. [para(961(a,1),102(a,1)),flip(a)]. given #501 (A,wt=16): 237 x ^ (y v (x v y) ') != 0 | (y v (x v y) ') ' = x. [para(38(a,1),43(a,1)),demod(15(7)),xx(a)]. given #502 (F,wt=11): 3442 c1 ^ ((c2 v x) ^ (c1 v y)) ' = 0. [para(961(a,1),202(a,1)),flip(a)]. given #503 (F,wt=11): 3444 c1 ^ ((x v c2) ^ (c1 v y)) ' = 0. [para(961(a,1),212(a,1)),flip(a)]. given #504 (T,wt=11): 3533 (x v y) ' ^ (x v (y ^ z)) = 0. [para(1187(a,1),15(a,1)),flip(a)]. given #505 (T,wt=11): 3652 c2 v (x v (c1 v (x ^ y)) ') = 1. [para(1189(a,1),1392(a,1,2,2,1)),demod(84(8),13(8),82(8),13(7))]. given #506 (A,wt=12): 242 c1 v (x v c2) ' != 1 | (x v c2) ' = c1 '. [para(205(a,1),21(b,1)),flip(c),xx(b)]. given #507 (F,wt=11): 3698 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(147(a,1),66(a,1)),demod(23(3),15(6)),flip(a)]. given #508 (F,wt=11): 3760 (x ^ y) ' v (x ^ (y v z)) = 1. [para(1346(a,1),13(a,1)),flip(a)]. given #509 (T,wt=11): 3800 c1 ^ (x ^ (c2 ^ (x v y)) ') = 0. [para(1347(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #510 (T,wt=11): 3839 (c2 v x) ^ (x v c1) = x v c1. [para(1365(a,1),15(a,1)),flip(a)]. given #511 (A,wt=12): 244 x ' ^ (y v x) != 0 | y v x = x. [para(238(a,1),21(a,1)),demod(223(10)),flip(c),xx(a)]. given #512 (F,wt=11): 3876 (c1 v x) ^ (y v (c2 v x)) ' = 0. [para(13(a,1),1376(a,1,1))]. given #513 (F,wt=11): 3877 (x v c1) ^ (y v (x v c2)) ' = 0. [para(13(a,1),1376(a,1,2,1,2))]. given #514 (T,wt=11): 3878 (x v c1) ^ (c2 v (x v y)) ' = 0. [para(13(a,1),1376(a,1,2,1)),demod(14(5))]. given #515 (T,wt=11): 3879 (c1 v (c2 ^ x)) ^ (y v c2) ' = 0. [para(18(a,1),1376(a,1,2,1,2)),demod(13(4))]. given #516 (A,wt=13): 245 x v (y v (y v ((x v y) ^ z)) ') = 1. [para(32(a,1),238(a,1,2)),demod(13(6),14(6))]. given #517 (F,wt=11): 3881 (x v c1) ^ (c2 v (y v x)) ' = 0. [para(25(a,1),1376(a,1,2,1))]. given #518 (F,wt=11): 3882 (c1 v (x ^ c2)) ^ (y v c2) ' = 0. [para(33(a,1),1376(a,1,2,1,2)),demod(13(4))]. given #519 (T,wt=11): 3890 (c1 v (x ^ y)) ^ (c2 v x) ' = 0. [para(79(a,1),1376(a,1,2,1)),demod(13(3))]. given #520 (T,wt=11): 3896 (c1 v (x ^ y)) ^ (c2 v y) ' = 0. [para(112(a,1),1376(a,1,2,1)),demod(13(3))]. given #521 (A,wt=12): 246 (x v y) ^ y ' != 0 | (x v y) ' = y '. [para(238(a,1),43(a,1)),xx(a)]. given #522 (F,wt=11): 4074 (x ^ y) ' v ((z v x) ^ y) = 1. [para(1510(a,1),13(a,1)),flip(a)]. given #523 (F,wt=11): 4076 (x ^ (y v z)) v (z ^ x) ' = 1. [para(15(a,1),1510(a,1,1))]. given #524 (T,wt=11): 4077 ((x v y) ^ z) v (z ^ y) ' = 1. [para(15(a,1),1510(a,1,2,1))]. given #525 (T,wt=11): 4079 ((x v y) ^ (y v z)) v y ' = 1. [para(17(a,1),1510(a,1,2,1))]. given #526 (A,wt=12): 247 x ' v (y ^ x) != 1 | y ^ x = x. [para(239(a,1),21(b,1)),demod(223(10)),flip(c),xx(b)]. given #527 (F,wt=11): 4084 ((x v y) ^ (z v y)) v y ' = 1. [para(27(a,1),1510(a,1,2,1))]. given #528 (F,wt=11): 4090 ((x v c1) ^ (c2 v y)) v c1 ' = 1. [para(198(a,1),1510(a,1,2,1))]. given #529 (T,wt=11): 4091 ((x v c1) ^ (y v c2)) v c1 ' = 1. [para(200(a,1),1510(a,1,2,1))]. given #530 (T,wt=11): 4154 x ^ (y ^ ((z v y) ^ x) ') = 0. [para(1512(a,1),26(a,1)),flip(a)]. given #531 (A,wt=13): 248 x ^ (y ^ (y ^ ((x ^ y) v z)) ') = 0. [para(30(a,1),239(a,1,2)),demod(15(6),16(6))]. given #532 (F,wt=11): 4171 x ^ ((y v x) ^ (z v x)) ' = 0. [para(1512(a,1),102(a,1)),flip(a)]. given #533 (F,wt=11): 4176 c1 ^ ((x v c1) ^ (c2 v y)) ' = 0. [para(1512(a,1),202(a,1)),flip(a)]. given #534 (T,wt=11): 4178 c1 ^ ((x v c1) ^ (y v c2)) ' = 0. [para(1512(a,1),212(a,1)),flip(a)]. given #535 (T,wt=11): 4250 c1 ^ ((c2 v x) ^ (y v c1)) ' = 0. [para(1524(a,1),202(a,1)),flip(a)]. given #536 (A,wt=12): 249 (x ^ y) v y ' != 1 | x ^ y = y. [para(239(a,1),43(b,1)),demod(223(10)),flip(c),xx(b)]. given #537 (F,wt=11): 4252 c1 ^ ((x v c2) ^ (y v c1)) ' = 0. [para(1524(a,1),212(a,1)),flip(a)]. given #538 (F,wt=11): 4264 c1 ^ (x ^ (c2 ^ (y v x)) ') = 0. [para(1528(a,1),26(a,1)),flip(a)]. given #539 (T,wt=11): 4393 (x ^ y) v (z v x) = z v x. [para(74(a,1),160(a,1,1)),demod(27(5)),flip(a)]. given #540 (T,wt=11): 4401 (c1 ^ x) v (y v c2) = y v c2. [para(121(a,1),160(a,1,1)),demod(27(8)),flip(a)]. given #541 (A,wt=19): 250 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x) ' = y. [para(13(a,1),44(a,1)),demod(14(2))]. given #542 (F,wt=11): 4485 c1 ' v ((c2 v x) ^ (c1 v y)) = 1. [para(130(a,1),1639(a,1,2))]. given #543 (F,wt=11): 4588 c1 ' v ((c2 v x) ^ (y v c1)) = 1. [para(130(a,1),1687(a,1,2))]. given #544 (T,wt=11): 4607 ((c2 v x) ^ (c1 v y)) v c1 ' = 1. [para(198(a,1),177(a,1,1,2,1)),demod(198(9))]. given #545 (T,wt=11): 4608 ((x v c2) ^ (c1 v y)) v c1 ' = 1. [para(200(a,1),177(a,1,1,2,1)),demod(200(9))]. given #546 (A,wt=19): 251 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y) ' = z. [para(13(a,1),44(b,1,1))]. given #547 (F,wt=11): 4692 (x ^ y) ' v (x ^ (z v y)) = 1. [para(1723(a,1),13(a,1)),flip(a)]. given #548 (F,wt=11): 4946 c2 ' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(160(a,1),1764(a,1,2))]. given #549 (T,wt=11): 5023 (x v (y ^ z)) ^ (z v x) ' = 0. [para(13(a,1),1784(a,1,1))]. given #550 (T,wt=11): 5024 ((x ^ y) v z) ^ (z v y) ' = 0. [para(13(a,1),1784(a,1,2,1))]. given #551 (A,wt=19): 252 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y) ' = z. [para(15(a,1),44(b,1))]. given #552 (F,wt=11): 5025 (x v y) ' ^ ((z ^ x) v y) = 0. [para(1784(a,1),15(a,1)),flip(a)]. given #553 (F,wt=11): 5027 ((x ^ y) v (y ^ z)) ^ y ' = 0. [para(18(a,1),1784(a,1,2,1))]. given #554 (T,wt=11): 5031 ((x ^ y) v (z ^ y)) ^ y ' = 0. [para(33(a,1),1784(a,1,2,1))]. given #555 (T,wt=11): 5038 (c1 v x) ^ (c2 v (y v x)) ' = 0. [para(198(a,1),1784(a,1,1,1)),demod(14(5))]. given #556 (A,wt=17): 253 x v y != 1 | y ^ z != 0 | (x v y) ' = y ^ z. [para(18(a,1),44(a,1,2)),demod(26(6),102(6))]. given #557 (F,wt=11): 5040 ((x ^ c2) v (y ^ c1)) ^ c2 ' = 0. [para(283(a,1),1784(a,1,2,1))]. given #558 (F,wt=11): 5042 ((x ^ c2) v (c1 ^ y)) ^ c2 ' = 0. [para(289(a,1),1784(a,1,2,1))]. given #559 (T,wt=11): 5099 x v (y v ((z ^ y) v x) ') = 1. [para(1786(a,1),25(a,1)),flip(a)]. given #560 (T,wt=11): 5121 x v ((y ^ x) v (z ^ x)) ' = 1. [para(1786(a,1),107(a,1)),flip(a)]. given #561 (A,wt=17): 254 x v y != 1 | x v y != 0 | (x v y) ' = x v y. [para(35(a,1),44(b,1)),demod(74(2),73(2))]. given #562 (F,wt=11): 5129 c2 v ((x ^ c2) v (y ^ c1)) ' = 1. [para(1786(a,1),285(a,1)),flip(a)]. given #563 (F,wt=11): 5130 c2 v ((x ^ c2) v (c1 ^ y)) ' = 1. [para(1786(a,1),322(a,1)),flip(a)]. given #564 (T,wt=11): 5169 c2 v ((x ^ c1) v (y ^ c2)) ' = 1. [para(1805(a,1),285(a,1)),flip(a)]. given #565 (T,wt=11): 5170 c2 v ((c1 ^ x) v (y ^ c2)) ' = 1. [para(1805(a,1),322(a,1)),flip(a)]. given #566 (A,wt=13): 255 x v y != 1 | 0 != y | (x v y) ' = y. [para(36(a,1),44(a,1,2)),demod(15(5),27(5)),flip(b)]. given #567 (F,wt=11): 5181 c2 v (x v (c1 v (y ^ x)) ') = 1. [para(1809(a,1),25(a,1)),flip(a)]. given #568 (F,wt=11): 5271 c2 ' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(160(a,1),1818(a,1,2))]. given #569 (T,wt=11): 5307 ((x ^ c1) v (c2 ^ y)) ^ c2 ' = 0. [para(283(a,1),186(a,1,1,2,1)),demod(283(9))]. given #570 (T,wt=11): 5309 ((c1 ^ x) v (c2 ^ y)) ^ c2 ' = 0. [para(289(a,1),186(a,1,1,2,1)),demod(289(9))]. given #571 (A,wt=19): 257 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x) ' = z. [para(25(a,1),44(a,1))]. given #572 (F,wt=11): 5357 (x v y) ' ^ (x v (z ^ y)) = 0. [para(1931(a,1),15(a,1)),flip(a)]. given #573 (F,wt=11): 5542 x v (c2 v ((x v c1) ^ y) ') = 1. [para(15(a,1),2051(a,1,2,2,1))]. given #574 (T,wt=11): 5570 (c1 v x) ^ (x v (c2 v y)) ' = 0. [para(119(a,1),2058(a,1,2,1,2))]. given #575 (T,wt=11): 5571 (c1 v x) ^ (x v (y v c2)) ' = 0. [para(121(a,1),2058(a,1,2,1,2))]. given #576 (A,wt=25): 259 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y) ' = z ^ u. [para(26(a,1),44(b,1))]. given #577 (F,wt=11): 5586 ((x ^ c1) v y) ^ (y v c2) ' = 0. [para(283(a,1),2059(a,1,2,1,2))]. given #578 (F,wt=11): 5588 ((c1 ^ x) v y) ^ (y v c2) ' = 0. [para(289(a,1),2059(a,1,2,1,2))]. given #579 (T,wt=11): 5879 c2 v ((c1 v (c2 ^ x)) ^ y) ' = 1. [para(2141(a,1),31(a,1)),demod(13(6)),flip(a)]. given #580 (T,wt=11): 5890 c2 v ((c1 v (x ^ c2)) ^ y) ' = 1. [para(2141(a,1),107(a,1)),demod(13(6)),flip(a)]. given #581 (A,wt=17): 261 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1) ' = c2. [para(111(a,1),44(a,1,2)),demod(15(8))]. given #582 (F,wt=11): 5894 c2 v (x ^ (c1 v (c2 ^ y))) ' = 1. [para(2163(a,1),31(a,1)),demod(13(6)),flip(a)]. given #583 (F,wt=11): 5904 c2 v (x ^ (c1 v (y ^ c2))) ' = 1. [para(2163(a,1),107(a,1)),demod(13(6)),flip(a)]. given #584 (T,wt=11): 5933 (x v (y v z)) ' ^ (u ^ y) = 0. [para(138(a,1),196(a,1,1)),demod(82(7),138(9))]. given #585 (T,wt=11): 5936 (x v (y v z)) ' ^ (u ^ z) = 0. [para(148(a,1),196(a,1,1)),demod(82(7),148(9))]. given #586 (A,wt=16): 262 (x v y) ^ (y ' v z) != 0 | (x v y) ' = y ' v z. [para(86(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #587 (F,wt=11): 5941 (x v (c2 v y)) ' ^ (z ^ c1) = 0. [para(217(a,1),196(a,1,1)),demod(82(9),217(13))]. given #588 (F,wt=11): 5942 (x v (y v c2)) ' ^ (z ^ c1) = 0. [para(240(a,1),196(a,1,1)),demod(82(9),240(13))]. given #589 (T,wt=11): 5946 (x v c2) ' ^ (y ^ (x v c1)) = 0. [para(504(a,1),196(a,1,1)),demod(82(9),504(13))]. given #590 (T,wt=11): 5948 (c2 ^ (c1 v x)) ' ^ (y ^ c1) = 0. [para(1067(a,1),196(a,1,1)),demod(82(10),1067(15))]. given #591 (A,wt=20): 263 x v (y v ((x v y) ' ^ z)) != 1 | (x v y) ' ^ z = (x v y) '. [para(89(a,1),44(b,1)),flip(c),xx(b)]. given #592 (F,wt=11): 5950 (c2 v x) ' ^ (y ^ (x v c1)) = 0. [para(1366(a,1),196(a,1,1)),demod(82(9),1366(13))]. given #593 (F,wt=11): 5951 (x v c2) ' ^ (y ^ (c1 v x)) = 0. [para(1384(a,1),196(a,1,1)),demod(82(9),1384(13))]. given #594 (T,wt=11): 5953 (c2 ^ (x v c1)) ' ^ (y ^ c1) = 0. [para(1526(a,1),196(a,1,1)),demod(82(10),1526(15))]. given #595 (T,wt=11): 5956 (c2 v x) ' ^ (y ^ (c1 v x)) = 0. [para(1580(a,1),196(a,1,1)),demod(82(9),1580(13))]. given #596 (A,wt=16): 264 (x v y) ^ (z v y ') != 0 | (x v y) ' = z v y '. [para(96(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #597 (F,wt=11): 5963 (x v y) ' ^ (z ^ (y v x)) = 0. [para(2062(a,1),196(a,1,1)),demod(82(7),2062(9))]. given #598 (F,wt=11): 5998 (x ^ c2) v (c1 ^ (y ^ x)) ' = 1. [para(196(a,1),2088(a,1,2)),demod(13(7))]. given #599 (T,wt=11): 6003 x ^ (c1 ^ ((x ^ c2) v y) ') = 0. [para(94(a,1),5913(a,1,2)),demod(15(7),16(7))]. given #600 (T,wt=11): 6042 (c1 v x) ^ (y v (x v c2)) ' = 0. [para(620(a,1),5915(a,1,2)),demod(15(7))]. given #601 (A,wt=12): 265 (x v y) ^ x ' != 0 | (x v y) ' = x '. [para(96(a,1),44(a,1)),xx(a)]. given #602 (F,wt=11): 6117 (c1 v (c2 ^ x)) ^ (c2 v y) ' = 0. [para(31(a,1),2188(a,1,2,1))]. given #603 (F,wt=11): 6122 (c1 v (x ^ c2)) ^ (c2 v y) ' = 0. [para(107(a,1),2188(a,1,2,1))]. given #604 (T,wt=11): 6135 c1 ^ (x ^ ((x ^ c2) v y) ') = 0. [para(2215(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #605 (T,wt=11): 6152 x ^ (c1 ^ ((c2 ^ x) v y) ') = 0. [para(2218(a,1),26(a,1)),flip(a)]. given #606 (A,wt=31): 266 x v (y v ((x v (y v z)) ^ u)) != 1 | (x v y) ^ u != 0 | (x v y) ' = (x v (y v z)) ^ u. [para(29(a,1),44(b,1)),demod(14(2),14(15))]. given #607 (F,wt=11): 6153 c1 ^ ((c2 ^ (c1 v x)) v y) ' = 0. [para(2218(a,1),29(a,1)),flip(a)]. given #608 (F,wt=11): 6164 c1 ^ ((c2 ^ (x v c1)) v y) ' = 0. [para(2218(a,1),102(a,1)),flip(a)]. given #609 (T,wt=11): 6174 c1 ^ (x ^ (y v (x ^ c2)) ') = 0. [para(2230(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #610 (T,wt=11): 6211 c1 ^ (x v (c2 ^ (c1 v y))) ' = 0. [para(2233(a,1),29(a,1)),flip(a)]. given #611 (A,wt=20): 267 x v (y v (z ^ (x v y) ')) != 1 | z ^ (x v y) ' = (x v y) '. [para(99(a,1),44(b,1)),flip(c),xx(b)]. given #612 (F,wt=11): 6222 c1 ^ (x v (c2 ^ (y v c1))) ' = 0. [para(2233(a,1),102(a,1)),flip(a)]. given #613 (F,wt=11): 6233 (x v (y ^ c1)) ^ (c2 v x) ' = 0. [para(285(a,1),2262(a,1,2,1))]. given #614 (T,wt=11): 6234 (x v (c1 ^ y)) ^ (c2 v x) ' = 0. [para(322(a,1),2262(a,1,2,1))]. given #615 (T,wt=11): 6241 (x v c2) ' ^ (x v (y ^ c1)) = 0. [para(2268(a,1),15(a,1)),flip(a)]. given #616 (A,wt=20): 268 x v (y v (x v (y v z)) ') != 1 | (x v (y v z)) ' = (x v y) '. [para(127(a,1),44(b,1)),demod(14(2),14(14)),flip(c),xx(b)]. given #617 (F,wt=11): 6250 (x v c2) ' ^ (x v (c1 ^ y)) = 0. [para(2270(a,1),15(a,1)),flip(a)]. given #618 (F,wt=11): 6259 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(27(a,1),204(a,2)),demod(102(10))]. given #619 (T,wt=11): 6315 (x v y) ' ^ (y v (x ^ z)) = 0. [para(2286(a,1),15(a,1)),flip(a)]. given #620 (T,wt=11): 6355 (x v y) ' ^ ((y ^ z) v x) = 0. [para(2287(a,1),15(a,1)),flip(a)]. given #621 (A,wt=35): 269 x v (y v (z ^ (((x v y) ^ z) v u))) != 1 | (x v y) ^ z != 0 | (x v y) ' = z ^ (((x v y) ^ z) v u). [para(30(a,1),44(b,1))]. given #622 (F,wt=11): 6372 x ' ^ ((x ^ y) v (x ^ z)) = 0. [para(18(a,1),2289(a,1,1,1))]. given #623 (F,wt=11): 6376 x ' ^ ((x ^ y) v (z ^ x)) = 0. [para(33(a,1),2289(a,1,1,1))]. given #624 (T,wt=11): 6381 (c2 v x) ' ^ ((y ^ c1) v x) = 0. [para(67(a,1),2289(a,1,2,1))]. given #625 (T,wt=11): 6382 c2 ' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(283(a,1),2289(a,1,1,1))]. given #626 (A,wt=20): 270 x v (y v (z v (x v y)) ') != 1 | (z v (x v y)) ' = (x v y) '. [para(134(a,1),44(b,1)),flip(c),xx(b)]. given #627 (F,wt=11): 6383 c2 ' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(289(a,1),2289(a,1,1,1))]. given #628 (F,wt=11): 6425 x ^ ((x ' ^ y) v (x ' ^ z)) = 0. [para(223(a,1),2291(a,1,2)),demod(15(6))]. given #629 (T,wt=11): 6445 x ^ ((x ' ^ y) v (z ^ x ')) = 0. [para(223(a,1),2296(a,1,2)),demod(15(6))]. given #630 (T,wt=11): 6446 ((x ^ c1) v (y ^ c2)) ^ c2 ' = 0. [para(67(a,1),2296(a,1,1,1))]. given #631 (A,wt=27): 271 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y) ' = (y ^ u) v z. [para(31(a,1),44(a,1,2))]. given #632 (F,wt=11): 6485 ((x ^ c1) v (y ^ c1)) ^ c2 ' = 0. [para(283(a,1),2301(a,1,2,1))]. given #633 (F,wt=11): 6487 ((x ^ c1) v (c1 ^ y)) ^ c2 ' = 0. [para(289(a,1),2301(a,1,2,1))]. given #634 (T,wt=11): 6560 x v (c2 v ((c1 v x) ^ y) ') = 1. [para(2337(a,1),25(a,1)),flip(a)]. given #635 (T,wt=11): 6579 (c2 ^ x) v (x ^ (y ^ c1)) ' = 1. [para(67(a,1),2338(a,1,2,1,2))]. given #636 (A,wt=16): 272 (x v y) ^ (y ^ z) ' != 0 | (x v y) ' = (y ^ z) '. [para(157(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #637 (F,wt=11): 6599 ((c2 v x) ^ y) v (y ^ c1) ' = 1. [para(198(a,1),2339(a,1,2,1,2))]. given #638 (F,wt=11): 6600 ((x v c2) ^ y) v (y ^ c1) ' = 1. [para(200(a,1),2339(a,1,2,1,2))]. given #639 (T,wt=11): 6857 (x ^ (c2 v y)) v (c1 ^ x) ' = 1. [para(202(a,1),2394(a,1,2,1))]. given #640 (T,wt=11): 6858 (x ^ (y v c2)) v (c1 ^ x) ' = 1. [para(212(a,1),2394(a,1,2,1))]. given #641 (A,wt=16): 273 (x v y) ^ (z ^ y) ' != 0 | (x v y) ' = (z ^ y) '. [para(165(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #642 (F,wt=11): 6865 (x ^ c1) ' v (x ^ (c2 v y)) = 1. [para(2400(a,1),13(a,1)),flip(a)]. given #643 (F,wt=11): 6879 (x ^ c1) ' v (x ^ (y v c2)) = 1. [para(2401(a,1),13(a,1)),flip(a)]. given #644 (T,wt=11): 6959 (x ^ y) ' v ((y v z) ^ x) = 1. [para(15(a,1),2434(a,1,1,1))]. given #645 (T,wt=11): 6960 (x ^ y) ' v (y ^ (x v z)) = 1. [para(15(a,1),2434(a,1,2))]. given #646 (A,wt=12): 274 (x v c2) ^ c1 ' != 0 | (x v c2) ' = c1 '. [para(173(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #647 (F,wt=11): 6962 x ' v ((x v y) ^ (x v z)) = 1. [para(17(a,1),2434(a,1,1,1))]. given #648 (F,wt=11): 6966 x ' v ((x v y) ^ (z v x)) = 1. [para(27(a,1),2434(a,1,1,1))]. given #649 (T,wt=11): 6971 c1 ' v ((c1 v x) ^ (c2 v y)) = 1. [para(198(a,1),2434(a,1,1,1))]. given #650 (T,wt=11): 6972 c1 ' v ((c1 v x) ^ (y v c2)) = 1. [para(200(a,1),2434(a,1,1,1))]. given #651 (A,wt=16): 275 (x v c2) ^ (c1 ' v y) != 0 | (x v c2) ' = c1 ' v y. [para(178(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #652 (F,wt=11): 6978 (c1 ^ x) ' v ((c2 v y) ^ x) = 1. [para(119(a,1),2434(a,1,2,1))]. given #653 (F,wt=11): 6983 (c1 ^ x) ' v ((y v c2) ^ x) = 1. [para(121(a,1),2434(a,1,2,1))]. given #654 (T,wt=11): 7101 x v ((x ' v y) ^ (x ' v z)) = 1. [para(223(a,1),2438(a,1,2)),demod(13(6))]. given #655 (T,wt=11): 7282 x v ((x ' v y) ^ (z v x ')) = 1. [para(223(a,1),2443(a,1,2)),demod(13(6))]. given #656 (A,wt=31): 276 x v (y v z) != 1 | (x v y) ^ (z v ((y v z) ^ u)) != 0 | (x v y) ' = z v ((y v z) ^ u). [para(32(a,1),44(a,1,2))]. given #657 (F,wt=11): 7287 ((c2 v x) ^ (y v c1)) v c1 ' = 1. [para(119(a,1),2443(a,1,1,1))]. given #658 (F,wt=11): 7289 ((x v c2) ^ (y v c1)) v c1 ' = 1. [para(121(a,1),2443(a,1,1,1))]. given #659 (T,wt=11): 7329 ((c2 v x) ^ (c2 v y)) v c1 ' = 1. [para(119(a,1),2447(a,1,1,1))]. given #660 (T,wt=11): 7330 ((x v c2) ^ (c2 v y)) v c1 ' = 1. [para(121(a,1),2447(a,1,1,1))]. given #661 (A,wt=21): 277 x v y != 1 | (x v y) ^ z != 0 | (x v y) ' = (x v y) ^ z. [para(32(a,1),44(a,1)),demod(69(7))]. given #662 (F,wt=11): 7350 ((c2 v x) ^ (y v c2)) v c1 ' = 1. [para(119(a,1),2448(a,1,1,1))]. given #663 (F,wt=11): 7351 ((x v c2) ^ (y v c2)) v c1 ' = 1. [para(121(a,1),2448(a,1,1,1))]. given #664 (T,wt=11): 7448 x v (c2 v ((y ^ c1) v x) ') = 1. [para(67(a,1),2495(a,1,2,2,1,1))]. given #665 (T,wt=11): 7466 c2 v ((c1 ^ x) v (c1 ^ y)) ' = 1. [hyper(222,a,2497,a(flip),b,1580,a),demod(2497(8),76(11),223(10),2497(16))]. given #666 (A,wt=16): 278 (x v c2) ^ (y v c1 ') != 0 | (x v c2) ' = y v c1 '. [para(180(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #667 (F,wt=11): 7489 c2 v ((x ^ c1) v (y ^ c1)) ' = 1. [para(2501(a,1),285(a,1)),flip(a)]. given #668 (F,wt=11): 7490 c2 v ((x ^ c1) v (c1 ^ y)) ' = 1. [para(2501(a,1),322(a,1)),flip(a)]. given #669 (T,wt=11): 7655 x v (c2 v ((c1 ^ y) v x) ') = 1. [para(2511(a,1),25(a,1)),flip(a)]. given #670 (T,wt=11): 7661 c2 v ((c1 ^ x) v (y ^ c1)) ' = 1. [para(2511(a,1),285(a,1)),flip(a)]. given #671 (A,wt=12): 279 (c2 v x) ^ c1 ' != 0 | (c2 v x) ' = c1 '. [para(180(a,1),44(a,1)),xx(a)]. given #672 (F,wt=11): 7726 x ^ (c1 ^ ((c2 v y) ^ x) ') = 0. [para(119(a,1),2516(a,1,2,2,1,1))]. given #673 (F,wt=11): 7729 x ^ (c1 ^ ((y v c2) ^ x) ') = 0. [para(121(a,1),2516(a,1,2,2,1,1))]. given #674 (T,wt=11): 7751 c1 ^ ((c2 v x) ^ (c2 v y)) ' = 0. [para(2517(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #675 (T,wt=11): 7861 c1 ^ ((c2 v x) ^ (y v c2)) ' = 0. [para(2518(a,1),212(a,1)),flip(a)]. given #676 (A,wt=20): 280 (x v y) ^ (z v (y v z) ') != 0 | (x v y) ' = z v (y v z) '. [para(38(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #677 (F,wt=11): 7872 c1 ^ ((x v c2) ^ (c2 v y)) ' = 0. [para(2527(a,1),202(a,1)),flip(a)]. given #678 (F,wt=11): 7873 c1 ^ ((x v c2) ^ (y v c2)) ' = 0. [para(2527(a,1),212(a,1)),flip(a)]. given #679 (T,wt=11): 7955 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(2535(a,1),13(a,1)),flip(a)]. given #680 (T,wt=11): 8167 (c2 v x) ' ^ ((c1 ^ y) v x) = 0. [para(2800(a,1),15(a,1)),flip(a)]. given #681 (A,wt=24): 281 x v (y v (z ^ ((x v y) ^ z) ')) != 1 | z ^ ((x v y) ^ z) ' = (x v y) '. [para(41(a,1),44(b,1)),flip(c),xx(b)]. given #682 (F,wt=11): 8171 ((c1 ^ x) v (y ^ c2)) ^ c2 ' = 0. [para(33(a,1),2800(a,1,2,1))]. given #683 (F,wt=11): 8174 ((c1 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(283(a,1),2800(a,1,2,1))]. given #684 (T,wt=11): 8176 ((c1 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(289(a,1),2800(a,1,2,1))]. given #685 (T,wt=11): 8249 (x v c2) ^ (y ^ c1) = y ^ c1. [para(13(a,1),2953(a,1,1))]. given #686 (A,wt=16): 282 (x v y ') ^ (z v y) != 0 | (x v y ') ' = z v y. [para(238(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #687 (F,wt=11): 8281 (x v y) ^ (z ^ y) = z ^ y. [para(13(a,1),2954(a,1,1))]. low water: id=5935, wt=59 low water: id=5934, wt=57 low water: id=5901, wt=53 low water: id=5899, wt=49 low water: id=6614, wt=47 low water: id=6027, wt=45 low water: id=6391, wt=44 low water: id=6198, wt=43 low water: id=6077, wt=41 low water: id=6771, wt=39 given #688 (F,wt=11): 8369 (x ^ c2) v (c1 ^ (x ^ y)) ' = 1. [para(15(a,1),3210(a,1,2,1)),demod(16(5))]. given #689 (T,wt=11): 8379 (c2 ^ (c1 v x)) v (c1 ^ y) ' = 1. [para(29(a,1),3211(a,1,2,1))]. low water: id=6669, wt=38 given #690 (T,wt=11): 8383 (c2 ^ (x v c1)) v (c1 ^ y) ' = 1. [para(102(a,1),3211(a,1,2,1))]. low water: id=7173, wt=37 given #691 (A,wt=13): 284 c2 != 1 | x ^ c1 != 0 | c2 ' = x ^ c1. [para(67(a,1),21(b,1)),demod(283(4))]. given #692 (F,wt=11): 8404 (x ^ c1) ' v (c2 ^ (c1 v y)) = 1. [para(3212(a,1),13(a,1)),flip(a)]. given #693 (F,wt=11): 8455 (x ^ c1) ' v (c2 ^ (y v c1)) = 1. [para(3215(a,1),13(a,1)),flip(a)]. given #694 (T,wt=11): 8472 (c1 ^ x) ' v (c2 ^ (x v y)) = 1. [para(3238(a,1),13(a,1)),flip(a)]. low water: id=6114, wt=36 low water: id=7198, wt=35 low water: id=7216, wt=33 given #695 (T,wt=11): 8616 (c1 ^ x) ' v (c2 ^ (y v x)) = 1. [para(3243(a,1),13(a,1)),flip(a)]. low water: id=7472, wt=32 low water: id=7622, wt=31 given #696 (A,wt=13): 287 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(67(a,1),34(a,1,2,2))]. given #697 (F,wt=11): 8676 (x ^ c1) ' v (c2 ^ (x v y)) = 1. [para(3292(a,1),13(a,1)),flip(a)]. given #698 (F,wt=11): 8694 (x ^ c1) ' v (c2 ^ (y v x)) = 1. [para(3302(a,1),13(a,1)),flip(a)]. given #699 (T,wt=11): 8865 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(13(a,1),3698(a,1,2))]. low water: id=7857, wt=29 given #700 (T,wt=11): 8967 (c1 v (x ^ y)) ^ (x v c2) ' = 0. [para(31(a,1),3877(a,1,2,1)),demod(13(3))]. given #701 (A,wt=13): 292 c2 != 1 | x ^ c1 != 0 | (x ^ c1) ' = c2. [para(283(a,1),43(a,1)),demod(15(7),67(7))]. given #702 (F,wt=11): 8969 (c1 v (x ^ y)) ^ (y v c2) ' = 0. [para(107(a,1),3877(a,1,2,1)),demod(13(3))]. given #703 (F,wt=11): 8987 (x v c2) ' ^ (c1 v (c2 ^ y)) = 0. [para(3879(a,1),15(a,1)),flip(a)]. given #704 (T,wt=11): 9040 (x v c2) ' ^ (c1 v (y ^ c2)) = 0. [para(3882(a,1),15(a,1)),flip(a)]. given #705 (T,wt=11): 9055 (c2 v x) ' ^ (c1 v (x ^ y)) = 0. [para(3890(a,1),15(a,1)),flip(a)]. low water: id=8061, wt=28 given #706 (A,wt=12): 297 c2 ^ (x ^ c1) ' != 0 | (x ^ c1) ' = c2 '. [para(286(a,1),21(a,1)),flip(c),xx(a)]. given #707 (F,wt=11): 9087 (c2 v x) ' ^ (c1 v (y ^ x)) = 0. [para(3896(a,1),15(a,1)),flip(a)]. low water: id=8133, wt=27 given #708 (F,wt=11): 9128 (x ^ y) ' v ((z v y) ^ x) = 1. [para(15(a,1),4074(a,1,1,1))]. given #709 (T,wt=11): 9129 (x ^ y) ' v (y ^ (z v x)) = 1. [para(15(a,1),4074(a,1,2))]. given #710 (T,wt=11): 9130 x ' v ((y v x) ^ (x v z)) = 1. [para(17(a,1),4074(a,1,1,1))]. given #711 (A,wt=12): 299 c2 ^ (x ^ c1) ' != 0 | x ^ c1 = c2. [para(286(a,1),43(a,1)),demod(15(8),223(14)),xx(a)]. given #712 (F,wt=11): 9134 x ' v ((y v x) ^ (z v x)) = 1. [para(27(a,1),4074(a,1,1,1))]. given #713 (F,wt=11): 9139 c1 ' v ((x v c1) ^ (c2 v y)) = 1. [para(198(a,1),4074(a,1,1,1))]. given #714 (T,wt=11): 9140 c1 ' v ((x v c1) ^ (y v c2)) = 1. [para(200(a,1),4074(a,1,1,1))]. given #715 (T,wt=11): 9270 x v ((y v x ') ^ (x ' v z)) = 1. [para(223(a,1),4079(a,1,2)),demod(13(6))]. given #716 (A,wt=16): 300 (x v c2) ^ (y ^ c1) ' != 0 | (x v c2) ' = (y ^ c1) '. [para(286(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #717 (F,wt=11): 9295 x v ((y v x ') ^ (z v x ')) = 1. [para(223(a,1),4084(a,1,2)),demod(13(6))]. given #718 (F,wt=11): 9471 (x ^ y) v (z v y) = z v y. [para(15(a,1),4393(a,1,1))]. low water: id=8512, wt=25 given #719 (T,wt=11): 9476 (x ^ c1) v (y v c2) = y v c2. [para(67(a,1),4393(a,1,1))]. given #720 (T,wt=11): 9635 c1 ' v ((x v c2) ^ (c1 v y)) = 1. [para(13(a,1),4485(a,1,2,1))]. given #721 (A,wt=19): 301 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x ' = y ^ z. [para(16(a,1),45(b,1))]. given #722 (F,wt=11): 9641 c1 ' v ((c2 v x) ^ (c2 v y)) = 1. [para(119(a,1),4485(a,1,2,2))]. given #723 (F,wt=11): 9642 c1 ' v ((c2 v x) ^ (y v c2)) = 1. [para(121(a,1),4485(a,1,2,2))]. given #724 (T,wt=11): 9649 c1 ' v ((x v c2) ^ (y v c1)) = 1. [para(13(a,1),4588(a,1,2,1))]. given #725 (T,wt=11): 9854 c2 ' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(15(a,1),4946(a,1,2,1))]. given #726 (A,wt=13): 302 x v y != 1 | 0 != x | (x v y) ' = x. [para(17(a,1),45(b,1)),demod(13(2),73(2)),flip(b)]. given #727 (F,wt=11): 9861 c2 ' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(67(a,1),4946(a,1,2,2))]. given #728 (F,wt=11): 9873 (x v y) ' ^ (y v (z ^ x)) = 0. [para(5023(a,1),15(a,1)),flip(a)]. given #729 (T,wt=11): 9939 (x v y) ' ^ ((z ^ y) v x) = 0. [para(5024(a,1),15(a,1)),flip(a)]. given #730 (T,wt=11): 10022 x ' ^ ((y ^ x) v (x ^ z)) = 0. [para(18(a,1),5025(a,1,1,1))]. low water: id=8855, wt=24 given #731 (A,wt=19): 303 x v (y v z) != 1 | (x v z) ^ y != 0 | y ' = x v z. [para(25(a,1),45(a,1))]. given #732 (F,wt=11): 10026 x ' ^ ((y ^ x) v (z ^ x)) = 0. [para(33(a,1),5025(a,1,1,1))]. given #733 (F,wt=11): 10030 c2 ' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(283(a,1),5025(a,1,1,1))]. given #734 (T,wt=11): 10031 c2 ' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(289(a,1),5025(a,1,1,1))]. given #735 (T,wt=11): 10069 x ^ ((y ^ x ') v (x ' ^ z)) = 0. [para(223(a,1),5027(a,1,2)),demod(15(6))]. given #736 (A,wt=19): 304 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z. [para(26(a,1),45(b,1))]. given #737 (F,wt=11): 10088 x ^ ((y ^ x ') v (z ^ x ')) = 0. [para(223(a,1),5031(a,1,2)),demod(15(6))]. given #738 (F,wt=11): 10260 c2 ' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(15(a,1),5271(a,1,2,1))]. given #739 (T,wt=11): 10397 (x v c2) ' ^ ((y ^ c1) v x) = 0. [para(5586(a,1),15(a,1)),flip(a)]. given #740 (T,wt=11): 10414 (x v c2) ' ^ ((c1 ^ y) v x) = 0. [para(5588(a,1),15(a,1)),flip(a)]. given #741 (A,wt=12): 305 x v (x ' ^ y) != 1 | (x ' ^ y) ' = x. [para(89(a,1),45(b,1)),demod(13(3)),xx(b)]. given #742 (F,wt=11): 10542 (c2 v x) ' ^ (c1 v (c2 ^ y)) = 0. [para(6117(a,1),15(a,1)),flip(a)]. given #743 (F,wt=11): 10554 (c2 v x) ' ^ (c1 v (y ^ c2)) = 0. [para(6122(a,1),15(a,1)),flip(a)]. given #744 (T,wt=11): 10603 (c2 v x) ' ^ (x v (y ^ c1)) = 0. [para(6233(a,1),15(a,1)),flip(a)]. given #745 (T,wt=11): 10632 (c2 v x) ' ^ (x v (c1 ^ y)) = 0. [para(6234(a,1),15(a,1)),flip(a)]. given #746 (A,wt=21): 306 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z) ' = x. [para(29(a,1),45(b,1)),demod(13(3))]. given #747 (F,wt=11): 10661 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(13(a,1),6259(a,1,2))]. given #748 (F,wt=11): 10800 c2 ' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(283(a,1),6381(a,1,1,1))]. given #749 (T,wt=11): 10801 c2 ' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(289(a,1),6381(a,1,1,1))]. given #750 (T,wt=11): 10838 c1 ^ ((c2 ' ^ x) v (c2 ' ^ y)) = 0. [para(6425(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #751 (A,wt=12): 307 x v (y ^ x ') != 1 | (y ^ x ') ' = x. [para(99(a,1),45(b,1)),demod(13(3)),xx(b)]. given #752 (F,wt=11): 10863 c1 ^ ((c2 ' ^ x) v (y ^ c2 ')) = 0. [para(6445(a,1),66(a,1,2)),demod(15(3),88(3)),flip(a)]. given #753 (F,wt=11): 10915 (x ^ c1) ' v ((c2 v y) ^ x) = 1. [para(6599(a,1),13(a,1)),flip(a)]. given #754 (T,wt=11): 10923 (x ^ c1) ' v ((y v c2) ^ x) = 1. [para(6600(a,1),13(a,1)),flip(a)]. given #755 (T,wt=11): 10931 (c1 ^ x) ' v (x ^ (c2 v y)) = 1. [para(6857(a,1),13(a,1)),flip(a)]. given #756 (A,wt=12): 308 x v (x v y) ' != 1 | x v y = x. [para(127(a,1),45(b,1)),demod(13(3),223(11)),xx(b)]. given #757 (F,wt=7): 12023 c1 ' v (c1 ' v c2 ') ' != 1. [ur(308,b,24,a)]. given #758 (F,wt=7): 12026 (c1 ' v (c1 ' v c2 ') ') ' != 0. [ur(1971,b,12023,a),demod(13(9))]. given #759 (T,wt=11): 10959 (c1 ^ x) ' v (x ^ (y v c2)) = 1. [para(6858(a,1),13(a,1)),flip(a)]. given #760 (T,wt=11): 11076 c1 ' v ((x v c2) ^ (c2 v y)) = 1. [para(121(a,1),6971(a,1,2,1))]. given #761 (A,wt=25): 310 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z)) ' = x. [para(30(a,1),45(b,1)),demod(13(4))]. given #762 (F,wt=11): 11082 c1 ' v ((x v c2) ^ (y v c2)) = 1. [para(121(a,1),6972(a,1,2,1))]. given #763 (F,wt=11): 11152 c2 v ((c1 ' v x) ^ (c1 ' v y)) = 1. [hyper(222,a,7101,a(flip),b,1580,a),demod(7101(9),76(12),223(11),7101(18))]. given #764 (T,wt=11): 11172 c2 v ((c1 ' v x) ^ (y v c1 ')) = 1. [hyper(222,a,7282,a(flip),b,1580,a),demod(7282(9),76(12),223(11),7282(18))]. given #765 (T,wt=11): 11283 c2 ' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(289(a,1),8167(a,1,1,1))]. given #766 (A,wt=12): 311 x v (y v x) ' != 1 | y v x = x. [para(134(a,1),45(b,1)),demod(13(3),223(11)),xx(b)]. given #767 (F,wt=11): 11415 (c1 ^ x) ' v (c2 ^ (c1 v y)) = 1. [para(8379(a,1),13(a,1)),flip(a)]. given #768 (F,wt=11): 11427 (c1 ^ x) ' v (c2 ^ (y v c1)) = 1. [para(8383(a,1),13(a,1)),flip(a)]. given #769 (T,wt=11): 11547 (x v c2) ' ^ (c1 v (x ^ y)) = 0. [para(8967(a,1),15(a,1)),flip(a)]. given #770 (T,wt=11): 11561 (x v c2) ' ^ (c1 v (y ^ x)) = 0. [para(8969(a,1),15(a,1)),flip(a)]. given #771 (A,wt=12): 312 c1 v (c2 ' ^ x) != 1 | (c2 ' ^ x) ' = c1. [para(140(a,1),45(b,1)),demod(13(5)),xx(b)]. given #772 (F,wt=11): 11711 c2 v ((x v c1 ') ^ (c1 ' v y)) = 1. [para(9270(a,1),1392(a,1,2,2,1)),demod(84(10),13(10),82(10),13(9))]. given #773 (F,wt=11): 11739 c2 v ((x v c1 ') ^ (y v c1 ')) = 1. [para(9295(a,1),1392(a,1,2,2,1)),demod(84(10),13(10),82(10),13(9))]. given #774 (T,wt=11): 11878 c1 ^ ((x ^ c2 ') v (c2 ' ^ y)) = 0. [hyper(302,a,969,a,b,10069,a(flip)),demod(10069(9),15(10),82(12),223(11),10069(18))]. given #775 (T,wt=11): 11900 c1 ^ ((x ^ c2 ') v (y ^ c2 ')) = 0. [hyper(302,a,969,a,b,10088,a(flip)),demod(10088(9),15(10),82(12),223(11),10088(18))]. given #776 (A,wt=12): 313 c1 v (x ^ c2 ') != 1 | (x ^ c2 ') ' = c1. [para(142(a,1),45(b,1)),demod(13(5)),xx(b)]. given #777 (F,wt=12): 318 c1 v (c2 v x) ' != 1 | c2 v x = c1. [para(203(a,1),45(b,1)),demod(13(5),223(14)),xx(b)]. given #778 (F,wt=12): 319 c1 v (x v c2) ' != 1 | x v c2 = c1. [para(205(a,1),45(b,1)),demod(13(5),223(14)),xx(b)]. given #779 (T,wt=12): 320 (x v y) ^ y ' != 0 | x v y = y. [para(238(a,1),45(a,1)),demod(223(10)),flip(c),xx(a)]. given #780 (T,wt=12): 321 (x ^ y) v y ' != 1 | (x ^ y) ' = y '. [para(239(a,1),45(b,1)),xx(b)]. given #781 (A,wt=16): 314 x v (y ^ (x ^ y) ') != 1 | (y ^ (x ^ y) ') ' = x. [para(41(a,1),45(b,1)),demod(13(4)),xx(b)]. given #782 (F,wt=12): 329 c2 ^ (c1 ^ x) ' != 0 | (c1 ^ x) ' = c2 '. [para(295(a,1),21(a,1)),flip(c),xx(a)]. given #783 (F,wt=12): 332 c2 ^ (c1 ^ x) ' != 0 | c1 ^ x = c2. [para(295(a,1),43(a,1)),demod(15(8),223(14)),xx(a)]. given #784 (T,wt=12): 348 (x ^ y) v x ' != 1 | (x ^ y) ' = x '. [para(99(a,1),46(b,1)),xx(b)]. given #785 (T,wt=12): 350 (x ^ c1) v c2 ' != 1 | (x ^ c1) ' = c2 '. [para(139(a,1),46(b,1,2)),demod(98(9)),xx(b)]. given #786 (A,wt=17): 315 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x) ' = c1. [para(66(a,1),45(b,1)),demod(13(4))]. given #787 (F,wt=12): 356 (c1 ^ x) v c2 ' != 1 | (c1 ^ x) ' = c2 '. [para(142(a,1),46(b,1)),xx(b)]. given #788 (F,wt=12): 1255 x ' ^ (x v y) != 0 | x v y = x. [para(86(a,1),81(a,1)),demod(223(10)),flip(c),xx(a)]. given #789 (T,wt=12): 1260 c1 ' ^ (c2 v x) != 0 | c2 v x = c1. [para(178(a,1),81(a,1)),demod(223(13)),flip(c),xx(a)]. given #790 (T,wt=12): 1411 x ' v (x ^ y) != 1 | x ^ y = x. [para(89(a,1),93(b,1)),demod(223(10)),flip(c),xx(b)]. given #791 (A,wt=13): 316 c2 v x != 1 | c1 != 0 | (c2 v x) ' = c1. [para(198(a,1),45(b,1)),demod(13(4),119(4))]. given #792 (F,wt=12): 1417 c2 ' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(140(a,1),93(b,1)),demod(223(13)),flip(c),xx(b)]. given #793 (F,wt=12): 2109 c1 ' ^ (x v c2) != 0 | x v c2 = c1. [para(2073(a,1),21(a,1)),demod(223(13)),flip(c),xx(a)]. given #794 (T,wt=12): 2111 (x v c2) ^ c1 ' != 0 | x v c2 = c1. [para(2073(a,1),45(a,1)),demod(223(13)),flip(c),xx(a)]. given #795 (T,wt=12): 2353 x ^ (y v x ') != 0 | x ' v y = x '. [para(13(a,1),124(a,1,2))]. given #796 (A,wt=13): 317 x v c2 != 1 | c1 != 0 | (x v c2) ' = c1. [para(200(a,1),45(b,1)),demod(13(4),121(4))]. given #797 (F,wt=12): 2486 x v (y ^ x ') != 1 | x ' ^ y = x '. [para(15(a,1),125(a,1,2))]. given #798 (F,wt=12): 2572 x ^ (x ' v y) != 0 | y v x ' = x '. [para(13(a,1),126(a,1,2))]. given #799 (T,wt=12): 3070 x v (x ' ^ y) != 1 | y ^ x ' = x '. [para(15(a,1),132(a,1,2))]. given #800 (T,wt=12): 3137 x v (y v x) ' != 1 | (x v y) ' = x '. [para(13(a,1),137(a,1,2,1))]. given #801 (A,wt=13): 323 c2 != 1 | c1 ^ x != 0 | c2 ' = c1 ^ x. [para(289(a,1),21(a,1)),demod(26(7),66(7))]. given #802 (F,wt=12): 3823 x v (x v y) ' != 1 | (y v x) ' = x '. [para(13(a,1),151(a,1,2,1))]. given #803 (F,wt=12): 3872 c2 ^ c1 ' != 0 | c1 v (c2 ^ c1 ') = c1. [back_demod(3409),demod(3840(14))]. given #804 (T,wt=12): 3926 c1 v (x ^ c2 ') != 1 | c2 ' ^ x = c1 '. [para(15(a,1),154(a,1,2))]. given #805 (T,wt=12): 3957 c1 v (c2 ' ^ x) != 1 | x ^ c2 ' = c1 '. [para(15(a,1),155(a,1,2))]. given #806 (A,wt=13): 326 c2 != 1 | c1 ^ x != 0 | (c1 ^ x) ' = c2. [para(289(a,1),43(a,1)),demod(15(7),26(7),66(7))]. given #807 (F,wt=12): 4487 x ^ (y ^ x) ' != 0 | (x ^ y) ' = x '. [para(15(a,1),167(a,1,2,1))]. given #808 (F,wt=12): 4525 x ^ (x ^ y) ' != 0 | (y ^ x) ' = x '. [para(15(a,1),172(a,1,2,1))]. given #809 (T,wt=12): 4672 c2 ^ (x v c1 ') != 0 | c2 ' = c1 ' v x. [para(13(a,1),181(a,1,2))]. given #810 (T,wt=12): 4905 c1 v c2 ' != 1 | c2 ^ (c1 v c2 ') = c2. [para(1713(a,1),183(b,1)),demod(13(4),223(12),13(15),15(17),2536(18)),flip(c),xx(b)]. given #811 (A,wt=17): 327 x v c2 != 1 | c1 ^ y != 0 | (x v c2) ' = c1 ^ y. [para(289(a,1),44(a,1,2)),demod(26(9),212(9))]. given #812 (F,wt=12): 4952 c2 ' v (x ^ c1) != 1 | x ^ c1 = c2. [para(4947(a,1),21(b,1)),demod(223(13)),flip(c),xx(b)]. given #813 (F,wt=12): 4953 (x ^ c1) v c2 ' != 1 | x ^ c1 = c2. [para(4947(a,1),43(b,1)),demod(223(13)),flip(c),xx(b)]. given #814 (T,wt=12): 5614 c2 ^ (c1 ' v x) != 0 | c2 ' = x v c1 '. [para(13(a,1),188(a,1,2))]. given #815 (T,wt=12): 6644 c1 v (x v c2) ' != 1 | (c2 v x) ' = c1 '. [para(13(a,1),216(a,1,2,1))]. given #816 (A,wt=16): 333 (x v c2) ^ (c1 ^ y) ' != 0 | (x v c2) ' = (c1 ^ y) '. [para(295(a,1),44(a,1,2)),demod(95(2)),xx(a)]. given #817 (F,wt=12): 6893 x ' ^ (y v x) != 0 | (y v x) ' = x '. [para(238(a,1),220(a,1)),xx(a)]. given #818 (F,wt=12): 6894 x ' v (y ^ x) != 1 | (y ^ x) ' = x '. [para(239(a,1),220(b,1)),xx(b)]. given #819 (T,wt=12): 6896 c1 ' ^ (x v c2) != 0 | (x v c2) ' = c1 '. [para(2073(a,1),220(a,1)),xx(a)]. given #820 (T,wt=12): 6925 c2 ' v (x ^ c1) != 1 | (x ^ c1) ' = c2 '. [para(4947(a,1),220(b,1)),xx(b)]. given #821 (A,wt=19): 334 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x) ' = z. [para(15(a,1),46(a,1,1))]. given #822 (F,wt=12): 7120 x ' v (x ^ y) != 1 | (x ^ y) ' = x '. [para(99(a,1),221(b,1)),xx(b)]. given #823 (F,wt=12): 7124 c2 ' v (c1 ^ x) != 1 | (c1 ^ x) ' = c2 '. [para(142(a,1),221(b,1)),xx(b)]. given #824 (T,wt=12): 7770 (x ^ y) v x ' != 1 | x ^ y = x. [para(89(a,1),225(b,1)),demod(223(10)),flip(c),xx(b)]. given #825 (T,wt=12): 7772 (c1 ^ x) v c2 ' != 1 | c1 ^ x = c2. [para(140(a,1),225(b,1)),demod(223(13)),flip(c),xx(b)]. given #826 (A,wt=19): 335 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y) ' = z. [para(15(a,1),46(b,1)),demod(16(6))]. given #827 (F,wt=12): 8020 x ^ (y v x ') != 0 | (x ' v y) ' = x. [para(13(a,1),228(a,1,2))]. given #828 (F,wt=12): 8022 x ' ^ (x v y) != 0 | (x v y) ' = x '. [para(223(a,1),228(a,1,2,1)),demod(223(7))]. given #829 (T,wt=12): 8077 x ^ (x ' v y) != 0 | (y v x ') ' = x. [para(13(a,1),229(a,1,2))]. given #830 (T,wt=12): 8225 x ^ (y ^ x) ' != 0 | x ^ y = x. [para(15(a,1),231(a,1,2,1))]. given #831 (A,wt=17): 336 x v y != 1 | z ^ x != 0 | (z ^ x) ' = x v y. [para(17(a,1),46(b,1,2)),demod(25(3),107(3))]. given #832 (F,wt=12): 8328 x ^ (x ^ y) ' != 0 | y ^ x = x. [para(15(a,1),232(a,1,2,1))]. given #833 (F,wt=12): 8329 (x v y) ^ x ' != 0 | x v y = x. [para(17(a,1),232(a,1,2,1)),demod(17(7)),flip(b)]. given #834 (T,wt=12): 8332 (c2 v x) ^ c1 ' != 0 | c2 v x = c1. [para(198(a,1),232(a,1,2,1)),demod(198(11)),flip(b)]. given #835 (T,wt=12): 8392 c2 ^ (x v c1 ') != 0 | (c1 ' v x) ' = c2. [para(13(a,1),234(a,1,2))]. given #836 (A,wt=17): 337 x ^ y != 1 | x ^ y != 0 | (x ^ y) ' = x ^ y. [para(36(a,1),46(a,1)),demod(70(5),69(5))]. given #837 (F,wt=12): 8517 c1 v c2 ' != 1 | (c2 ^ (c1 v c2 ')) ' = c2 '. [para(1713(a,1),235(b,1)),demod(13(4),13(14),15(16),2536(17)),xx(b)]. given #838 (F,wt=12): 8707 c2 ^ (c1 ' v x) != 0 | (x v c1 ') ' = c2. [para(13(a,1),236(a,1,2))]. given #839 (T,wt=12): 8863 c1 v (c2 v x) ' != 1 | (x v c2) ' = c1 '. [para(13(a,1),242(a,1,2,1))]. given #840 (T,wt=12): 8950 x ' ^ (x v y) != 0 | y v x = x. [para(13(a,1),244(a,1,2))]. given #841 (A,wt=25): 339 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z) ' = x v u. [para(25(a,1),46(a,1))]. given #842 (F,wt=12): 9124 (x v y) ^ x ' != 0 | (y v x) ' = x '. [para(13(a,1),246(a,1,1))]. given #843 (F,wt=12): 9275 x ' v (x ^ y) != 1 | y ^ x = x. [para(15(a,1),247(a,1,2))]. given #844 (T,wt=12): 9456 (x ^ y) v x ' != 1 | y ^ x = x. [para(15(a,1),249(a,1,1))]. given #845 (T,wt=12): 9673 (x v y) ^ y ' != 0 | (y v x) ' = y '. [para(96(a,1),251(a,1)),xx(a)]. given #846 (A,wt=19): 341 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y) ' = z. [para(26(a,1),46(b,1))]. given #847 (F,wt=12): 9676 (c2 v x) ^ c1 ' != 0 | (x v c2) ' = c1 '. [para(173(a,1),251(a,1,2)),demod(95(2)),xx(a)]. given #848 (F,wt=12): 9680 (x v c2) ^ c1 ' != 0 | (c2 v x) ' = c1 '. [para(180(a,1),251(a,1)),xx(a)]. given #849 (T,wt=12): 9979 c1 ' ^ (c2 v x) != 0 | (c2 v x) ' = c1 '. [para(180(a,1),252(a,1)),xx(a)]. given #850 (T,wt=12): 11595 c2 ^ (c1 ^ x) ' != 0 | (x ^ c1) ' = c2 '. [para(15(a,1),297(a,1,2,1))]. given #851 (A,wt=20): 343 x ^ (y ^ ((x ^ y) ' v z)) != 0 | (x ^ y) ' v z = (x ^ y) '. [para(86(a,1),46(a,1)),flip(c),xx(a)]. given #852 (F,wt=12): 11662 c2 ^ (c1 ^ x) ' != 0 | x ^ c1 = c2. [para(15(a,1),299(a,1,2,1))]. given #853 (F,wt=12): 11912 x v (y ^ x ') != 1 | (x ' ^ y) ' = x. [para(15(a,1),305(a,1,2))]. given #854 (T,wt=12): 11992 x v (x ' ^ y) != 1 | (y ^ x ') ' = x. [para(15(a,1),307(a,1,2))]. given #855 (T,wt=12): 12024 x v (y v x) ' != 1 | x v y = x. [para(13(a,1),308(a,1,2,1))]. given #856 (A,wt=16): 344 (x ^ y) v (y ' ^ z) != 1 | (x ^ y) ' = y ' ^ z. [para(89(a,1),46(b,1,2)),demod(98(8)),xx(b)]. given #857 (F,wt=12): 12048 c2 ^ c1 ' != 0 | (c1 v (c2 ^ c1 ')) ' = c1 '. [para(1531(a,1),310(a,1)),demod(15(7),15(14),13(16),3840(17)),xx(a)]. given #858 (F,wt=12): 12066 x v (x v y) ' != 1 | y v x = x. [para(13(a,1),311(a,1,2,1))]. given #859 (T,wt=12): 12079 c1 v (x ^ c2 ') != 1 | (c2 ' ^ x) ' = c1. [para(15(a,1),312(a,1,2))]. given #860 (T,wt=12): 12099 c1 v (c2 ' ^ x) != 1 | (x ^ c2 ') ' = c1. [para(15(a,1),313(a,1,2))]. given #861 (A,wt=20): 345 x ^ (y ^ (z v (x ^ y) ')) != 0 | z v (x ^ y) ' = (x ^ y) '. [para(96(a,1),46(a,1)),flip(c),xx(a)]. given #862 (F,wt=12): 12100 c1 v (x v c2) ' != 1 | c2 v x = c1. [para(13(a,1),318(a,1,2,1))]. given #863 (F,wt=12): 12102 c1 v (c2 v x) ' != 1 | x v c2 = c1. [para(13(a,1),319(a,1,2,1))]. given #864 (T,wt=12): 12104 (x v y) ^ x ' != 0 | y v x = x. [para(13(a,1),320(a,1,1))]. given #865 (T,wt=12): 12105 (x ^ y) v x ' != 1 | (y ^ x) ' = x '. [para(15(a,1),321(a,1,1))]. given #866 (A,wt=27): 346 (x ^ y) v ((y v z) ^ u) != 1 | x ^ (y ^ u) != 0 | (x ^ y) ' = (y v z) ^ u. [para(29(a,1),46(b,1,2))]. given #867 (F,wt=12): 12107 c2 ^ (x ^ c1) ' != 0 | (c1 ^ x) ' = c2 '. [para(15(a,1),329(a,1,2,1))]. given #868 (F,wt=12): 12109 c2 ^ (x ^ c1) ' != 0 | c1 ^ x = c2. [para(15(a,1),332(a,1,2,1))]. given #869 (T,wt=12): 12111 (x ^ y) v y ' != 1 | (y ^ x) ' = y '. [para(15(a,1),348(a,1,1))]. given #870 (T,wt=12): 12113 (c1 ^ x) v c2 ' != 1 | (x ^ c1) ' = c2 '. [para(15(a,1),350(a,1,1))]. given #871 (A,wt=16): 347 (x ^ y) v (z ^ y ') != 1 | (x ^ y) ' = z ^ y '. [para(99(a,1),46(b,1,2)),demod(98(8)),xx(b)]. given #872 (F,wt=12): 12115 (x ^ c1) v c2 ' != 1 | (c1 ^ x) ' = c2 '. [para(15(a,1),356(a,1,1))]. given #873 (F,wt=12): 12117 x ' ^ (y v x) != 0 | x v y = x. [para(13(a,1),1255(a,1,2))]. given #874 (T,wt=12): 12119 c1 ' ^ (x v c2) != 0 | c2 v x = c1. [para(13(a,1),1260(a,1,2))]. given #875 (T,wt=12): 12121 x ' v (y ^ x) != 1 | x ^ y = x. [para(15(a,1),1411(a,1,2))]. given #876 (A,wt=16): 349 (x ^ y) v (y v z) ' != 1 | (y v z) ' = (x ^ y) '. [para(127(a,1),46(b,1,2)),demod(98(8)),flip(c),xx(b)]. given #877 (F,wt=12): 12124 c2 ' v (x ^ c1) != 1 | c1 ^ x = c2. [para(15(a,1),1417(a,1,2))]. given #878 (F,wt=12): 12126 c1 ' ^ (c2 v x) != 0 | x v c2 = c1. [para(13(a,1),2109(a,1,2))]. given #879 (T,wt=12): 12128 (c2 v x) ^ c1 ' != 0 | x v c2 = c1. [para(13(a,1),2111(a,1,1))]. given #880 (T,wt=12): 12145 c2 ' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(15(a,1),4952(a,1,2))]. given #881 (A,wt=31): 351 (x ^ y) v (z ^ ((y ^ z) v u)) != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z ^ ((y ^ z) v u). [para(30(a,1),46(b,1,2))]. given #882 (F,wt=12): 12147 (c1 ^ x) v c2 ' != 1 | x ^ c1 = c2. [para(15(a,1),4953(a,1,1))]. given #883 (F,wt=12): 12152 x ' ^ (x v y) != 0 | (y v x) ' = x '. [para(13(a,1),6893(a,1,2))]. given #884 (T,wt=12): 12154 x ' v (x ^ y) != 1 | (y ^ x) ' = x '. [para(15(a,1),6894(a,1,2))]. given #885 (T,wt=12): 12156 c1 ' ^ (c2 v x) != 0 | (x v c2) ' = c1 '. [para(13(a,1),6896(a,1,2))]. given #886 (A,wt=21): 352 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y) ' = (x ^ y) v z. [para(30(a,1),46(b,1)),demod(73(4))]. given #887 (F,wt=12): 12158 c2 ' v (c1 ^ x) != 1 | (x ^ c1) ' = c2 '. [para(15(a,1),6925(a,1,2))]. given #888 (F,wt=12): 12187 x ' v (y ^ x) != 1 | (x ^ y) ' = x '. [para(15(a,1),7120(a,1,2))]. given #889 (T,wt=12): 12189 c2 ' v (x ^ c1) != 1 | (c1 ^ x) ' = c2 '. [para(15(a,1),7124(a,1,2))]. given #890 (T,wt=12): 12191 (x ^ y) v y ' != 1 | y ^ x = y. [para(15(a,1),7770(a,1,1))]. given #891 (A,wt=16): 353 (x ^ y) v (z v y) ' != 1 | (z v y) ' = (x ^ y) '. [para(134(a,1),46(b,1,2)),demod(98(8)),flip(c),xx(b)]. given #892 (F,wt=12): 12193 (x ^ c1) v c2 ' != 1 | c1 ^ x = c2. [para(15(a,1),7772(a,1,1))]. given #893 (F,wt=12): 12207 x ' ^ (y v x) != 0 | (x v y) ' = x '. [para(223(a,1),8020(a,1,2,2)),demod(223(7))]. given #894 (T,wt=12): 12279 (x v y) ^ y ' != 0 | y v x = y. [para(13(a,1),8329(a,1,1))]. given #895 (T,wt=12): 12281 (x v c2) ^ c1 ' != 0 | c2 v x = c1. [para(13(a,1),8332(a,1,1))]. given #896 (A,wt=16): 354 (x ^ c1) v (c2 ' ^ y) != 1 | (x ^ c1) ' = c2 ' ^ y. [para(140(a,1),46(b,1,2)),demod(98(10)),xx(b)]. given #897 (F,wt=12): 12296 c1 ' ^ (x v c2) != 0 | (c2 v x) ' = c1 '. [para(15(a,1),9680(a,1))]. given #898 (F,wt=13): 375 1 != x | y ^ x != 0 | (x ^ y) ' = x. [para(70(a,1),46(b,1)),demod(13(2),18(2)),flip(a)]. given #899 (T,wt=13): 379 x v y != 1 | 0 != y | (y v x) ' = y. [para(74(a,1),44(a,1)),demod(15(5),17(5)),flip(b)]. given #900 (T,wt=13): 443 x ^ (y ^ (z v (x v u))) = y ^ x. [para(78(a,1),26(a,1,2)),flip(a)]. given #901 (A,wt=16): 355 (x ^ c1) v (y ^ c2 ') != 1 | (x ^ c1) ' = y ^ c2 '. [para(142(a,1),46(b,1,2)),demod(98(10)),xx(b)]. given #902 (F,wt=13): 444 x v (y v (z ^ (x ^ u))) = y v x. [para(91(a,1),25(a,1,2)),flip(a)]. given #903 (F,wt=13): 451 c2 != 1 | x ^ c1 != 0 | (c1 ^ x) ' = c2. [para(94(a,1),46(b,1)),demod(13(4),289(4))]. given #904 (T,wt=13): 452 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(101(a,1),16(a,1,1)),flip(a)]. given #905 (T,wt=13): 454 x ^ (y ^ (z v (u v x))) = y ^ x. [para(101(a,1),26(a,1,2)),flip(a)]. given #906 (A,wt=31): 357 (x ^ y) v z != 1 | x ^ (y ^ ((x ^ (y ^ u)) v z)) != 0 | (x ^ y) ' = (x ^ (y ^ u)) v z. [para(31(a,1),46(a,1)),demod(16(6),16(15))]. given #907 (F,wt=13): 490 x v ((y ^ (z ^ x)) v u) = x v u. [para(109(a,1),14(a,1,1)),flip(a)]. given #908 (F,wt=13): 492 x v (y v (z ^ (u ^ x))) = y v x. [para(109(a,1),25(a,1,2)),flip(a)]. given #909 (T,wt=13): 495 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x. [para(66(a,1),109(a,1,2,2))]. given #910 (T,wt=13): 496 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2. [para(94(a,1),109(a,1,2,2))]. given #911 (A,wt=20): 358 x ^ (y ^ (x ^ (y ^ z)) ') != 0 | (x ^ (y ^ z)) ' = (x ^ y) '. [para(157(a,1),46(a,1)),demod(16(5),16(14)),flip(c),xx(a)]. given #912 (F,wt=13): 499 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(119(a,1),28(a,1,2,2))]. given #913 (F,wt=13): 507 x v c2 != 1 | c1 != 0 | (c2 v x) ' = c1. [para(120(a,1),44(a,1)),demod(15(8),198(8))]. given #914 (T,wt=13): 509 (x v c1) ^ (y v (x v c2)) = x v c1. [para(120(a,1),101(a,1,2,2))]. given #915 (T,wt=13): 619 (x v c1) ^ (x v (y v c2)) = x v c1. [para(121(a,1),28(a,1,2,2))]. given #916 (A,wt=20): 359 x ^ (y ^ (z ^ (x ^ y)) ') != 0 | (z ^ (x ^ y)) ' = (x ^ y) '. [para(165(a,1),46(a,1)),flip(c),xx(a)]. given #917 (F,wt=13): 625 (x v y) ^ ((x v (y v z)) ' ^ u) = 0. [para(14(a,1),131(a,1,2,1,1))]. given #918 (F,wt=13): 632 (x v y) ^ (z ^ (x v (y v u)) ') = 0. [para(14(a,1),133(a,1,2,2,1))]. given #919 (T,wt=13): 640 x ^ (y ^ (z v ((x ^ y) v u)) ') = 0. [para(138(a,1),16(a,1)),flip(a)]. given #920 (T,wt=13): 724 x ^ (y ^ (z v (u v (x ^ y))) ') = 0. [para(148(a,1),16(a,1)),flip(a)]. given #921 (A,wt=35): 360 (x ^ y) v z != 1 | x ^ (y ^ (z v (((x ^ y) v z) ^ u))) != 0 | (x ^ y) ' = z v (((x ^ y) v z) ^ u). [para(32(a,1),46(a,1))]. given #922 (F,wt=13): 727 ((x ^ y) v z) ^ (u v (x v z)) ' = 0. [para(31(a,1),148(a,1,2,1,2))]. given #923 (F,wt=13): 732 (x v y) ^ ((x v (z v y)) ' ^ u) = 0. [para(25(a,1),149(a,1,2,1,1))]. given #924 (T,wt=13): 733 ((x ^ y) v z) ^ ((x v z) ' ^ u) = 0. [para(31(a,1),149(a,1,2,1,1))]. given #925 (T,wt=13): 740 (x v y) ^ (z ^ (x v (u v y)) ') = 0. [para(25(a,1),153(a,1,2,2,1))]. given #926 (A,wt=24): 361 x ^ (y ^ (z v ((x ^ y) v z) ')) != 0 | z v ((x ^ y) v z) ' = (x ^ y) '. [para(38(a,1),46(a,1)),flip(c),xx(a)]. given #927 (F,wt=13): 741 ((x ^ y) v z) ^ (u ^ (x v z) ') = 0. [para(31(a,1),153(a,1,2,2,1))]. given #928 (F,wt=13): 748 (x ^ y) v ((x ^ (y ^ z)) ' v u) = 1. [para(16(a,1),161(a,1,2,1,1))]. given #929 (T,wt=13): 780 (x ^ y) v (z v (x ^ (y ^ u)) ') = 1. [para(16(a,1),162(a,1,2,2,1))]. given #930 (T,wt=13): 790 x v (y v (z ^ ((x v y) ^ u)) ') = 1. [para(168(a,1),14(a,1)),flip(a)]. given #931 (A,wt=20): 362 (x ^ y) v (z ^ (y ^ z) ') != 1 | (x ^ y) ' = z ^ (y ^ z) '. [para(41(a,1),46(b,1,2)),demod(98(9)),xx(b)]. given #932 (F,wt=13): 799 (x ^ y) v ((x ^ (z ^ y)) ' v u) = 1. [para(26(a,1),169(a,1,2,1,1))]. low water: id=9844, wt=23 given #933 (F,wt=13): 800 ((x v y) ^ z) v ((x ^ z) ' v u) = 1. [para(29(a,1),169(a,1,2,1,1))]. given #934 (T,wt=13): 812 x v (y v (z ^ (u ^ (x v y))) ') = 1. [para(171(a,1),14(a,1)),flip(a)]. given #935 (T,wt=13): 815 ((x v y) ^ z) v (u ^ (x ^ z)) ' = 1. [para(29(a,1),171(a,1,2,1,2))]. given #936 (A,wt=23): 363 (x ^ c1) v (c2 ^ y) != 1 | x ^ (c1 ^ y) != 0 | (x ^ c1) ' = c2 ^ y. [para(66(a,1),46(b,1,2))]. given #937 (F,wt=13): 936 (x ^ y) v (z v (x ^ (u ^ y)) ') = 1. [para(26(a,1),174(a,1,2,2,1))]. given #938 (F,wt=13): 937 ((x v y) ^ z) v (u v (x ^ z) ') = 1. [para(29(a,1),174(a,1,2,2,1))]. given #939 (T,wt=13): 972 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y)) ' = 1. [para(26(a,1),206(a,1,1))]. given #940 (T,wt=13): 973 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),206(a,1,2,1))]. given #941 (A,wt=17): 364 c2 v x != 1 | y ^ c1 != 0 | (y ^ c1) ' = c2 v x. [para(198(a,1),46(b,1,2)),demod(25(5),285(5))]. given #942 (F,wt=13): 975 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y) ' = 1. [para(29(a,1),206(a,1,2,1))]. given #943 (F,wt=13): 1075 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z. [para(209(a,1),16(a,1,1)),flip(a)]. given #944 (T,wt=13): 1076 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1. [para(209(a,1),26(a,1,2)),flip(a)]. given #945 (T,wt=13): 1077 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z. [para(211(a,1),16(a,1,1)),flip(a)]. given #946 (A,wt=16): 366 (x ^ c1) v (c2 v y) ' != 1 | (c2 v y) ' = (x ^ c1) '. [para(203(a,1),46(b,1,2)),demod(98(10)),flip(c),xx(b)]. given #947 (F,wt=13): 1078 c1 ^ (x ^ (y v (z v c2))) = x ^ c1. [para(211(a,1),26(a,1,2)),flip(a)]. given #948 (F,wt=13): 1088 x ' ^ (x v (y ^ x ')) = x ' ^ (x v y). [para(19(a,1),65(a,1,2,2,2)),demod(39(3)),flip(a)]. low water: id=10059, wt=21 given #949 (T,wt=13): 1099 c1 ' ^ (c2 v (x ^ c1 ')) = c1 ' ^ (c2 v x). [para(173(a,1),65(a,1,2,2,2)),demod(39(5)),flip(a)]. given #950 (T,wt=13): 1152 1 != x | y ^ x != 0 | x ' = x ^ y. [para(15(a,1),72(b,1))]. given #951 (A,wt=16): 367 (x ^ c1) v (y v c2) ' != 1 | (y v c2) ' = (x ^ c1) '. [para(205(a,1),46(b,1,2)),demod(98(10)),flip(c),xx(b)]. given #952 (F,wt=13): 1157 c1 != 1 | c1 ^ x != 0 | c1 ' = c1 ^ x. [para(66(a,1),72(b,1)),demod(66(13)),flip(a)]. given #953 (F,wt=13): 1159 c1 != 1 | x ^ c1 != 0 | c1 ' = x ^ c1. [para(94(a,1),72(b,1)),demod(94(13)),flip(a)]. given #954 (T,wt=13): 1170 x v y != 1 | 0 != y | y ' = y v x. [para(13(a,1),75(a,1))]. given #955 (T,wt=13): 1176 c2 v ((x ^ (y ^ c1)) v z) = c2 v z. [para(290(a,1),14(a,1,1)),flip(a)]. given #956 (A,wt=16): 368 (x ^ y ') v (z ^ y) != 1 | (x ^ y ') ' = z ^ y. [para(239(a,1),46(b,1,2)),demod(98(8)),xx(b)]. given #957 (F,wt=13): 1177 c2 v (x v (y ^ (z ^ c1))) = x v c2. [para(290(a,1),25(a,1,2)),flip(a)]. given #958 (F,wt=13): 1200 (x v (y ^ z)) ^ (u v (x v y)) ' = 0. [para(79(a,1),148(a,1,2,1,2))]. given #959 (T,wt=13): 1201 (x v (y ^ z)) ^ ((x v y) ' ^ u) = 0. [para(79(a,1),149(a,1,2,1,1))]. given #960 (T,wt=13): 1202 (x v (y ^ z)) ^ (u ^ (x v y) ') = 0. [para(79(a,1),153(a,1,2,2,1))]. given #961 (A,wt=23): 369 (x ^ c2) v (y ^ c1) != 1 | x ^ (y ^ c1) != 0 | (x ^ c2) ' = y ^ c1. [para(67(a,1),46(b,1,2))]. given #962 (F,wt=13): 1243 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z. [para(325(a,1),14(a,1,1)),flip(a)]. given #963 (F,wt=13): 1244 c2 v (x v (y ^ (c1 ^ z))) = x v c2. [para(325(a,1),25(a,1,2)),flip(a)]. given #964 (T,wt=13): 1333 (x ^ (y ^ c2)) v (c1 ^ (x ^ y)) ' = 1. [para(16(a,1),447(a,1,1)),demod(15(6))]. given #965 (T,wt=13): 1334 (c2 ^ (x ^ y)) v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),447(a,1,2,1)),demod(15(3))]. given #966 (A,wt=17): 370 c1 v (c2 ^ x) != 1 | x ^ c1 != 0 | (c2 ^ x) ' = c1. [para(67(a,1),46(b,1)),demod(13(4))]. given #967 (F,wt=13): 1353 (x ^ (y v z)) v ((x ^ y) ' v u) = 1. [para(90(a,1),169(a,1,2,1,1))]. given #968 (F,wt=13): 1354 (x ^ (y v z)) v (u ^ (x ^ y)) ' = 1. [para(90(a,1),171(a,1,2,1,2))]. given #969 (T,wt=13): 1355 (x ^ (y v z)) v (u v (x ^ y) ') = 1. [para(90(a,1),174(a,1,2,2,1))]. given #970 (T,wt=13): 1356 (c2 ^ (x ^ (c1 v y))) v (x ^ c1) ' = 1. [para(90(a,1),206(a,1,2,1))]. given #971 (A,wt=23): 371 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = y ^ z. [para(69(a,1),46(b,1,2))]. given #972 (F,wt=13): 1370 (x v c1) ^ (y v (c2 v x)) = x v c1. [para(502(a,1),101(a,1,2,2))]. given #973 (F,wt=13): 1382 c2 v x != 1 | c2 != 0 | c2 ' = c2 v x. [para(502(a,1),75(a,1)),demod(502(13)),flip(b)]. given #974 (T,wt=13): 1385 (x v (y v c1)) ^ (c2 v (x v y)) ' = 0. [para(14(a,1),504(a,1,1)),demod(13(6))]. given #975 (T,wt=13): 1386 (c1 v (x v y)) ^ (x v (y v c2)) ' = 0. [para(14(a,1),504(a,1,2,1)),demod(13(3))]. given #976 (A,wt=21): 373 x v y != 1 | z ^ (x v y) != 0 | (x v y) ' = z ^ (x v y). [para(70(a,1),44(b,1)),demod(108(4))]. given #977 (F,wt=13): 1520 ((x v y) ^ z) v ((y ^ z) ' v u) = 1. [para(102(a,1),169(a,1,2,1,1))]. given #978 (F,wt=13): 1521 ((x v y) ^ z) v (u ^ (y ^ z)) ' = 1. [para(102(a,1),171(a,1,2,1,2))]. given #979 (T,wt=13): 1523 ((x v y) ^ z) v (u v (y ^ z) ') = 1. [para(102(a,1),174(a,1,2,2,1))]. given #980 (T,wt=13): 1525 (c2 ^ ((x v c1) ^ y)) v (c1 ^ y) ' = 1. [para(102(a,1),206(a,1,2,1))]. given #981 (A,wt=23): 374 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z ^ y. [para(70(a,1),46(b,1,2))]. given #982 (F,wt=13): 1556 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(15(a,1),103(a,1,2,2,2))]. low water: id=10444, wt=20 given #983 (F,wt=13): 1560 (x ^ (y v (z ^ x))) v (z ^ x) ' = 1. [para(103(a,1),165(a,1,2,1))]. given #984 (T,wt=13): 1561 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x. [para(103(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #985 (T,wt=13): 1562 x ^ (y ^ (y ^ (z v (x ^ y))) ') = 0. [para(103(a,1),239(a,1,2)),demod(15(6),16(6))]. given #986 (A,wt=23): 376 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y) ' = y v z. [para(73(a,1),44(a,1,2))]. given #987 (F,wt=13): 1583 (c1 v (x v y)) ^ (x v (c2 v y)) ' = 0. [para(25(a,1),1366(a,1,2,1)),demod(13(3))]. given #988 (F,wt=13): 1585 (c1 v ((c2 ^ x) v y)) ^ (c2 v y) ' = 0. [para(31(a,1),1366(a,1,2,1)),demod(13(5))]. given #989 (T,wt=13): 1591 (c1 v (x v (c2 ^ y))) ^ (x v c2) ' = 0. [para(79(a,1),1366(a,1,2,1)),demod(13(5))]. given #990 (T,wt=13): 1607 (x v (c1 v y)) ^ (c2 v (x v y)) ' = 0. [para(25(a,1),1384(a,1,1)),demod(13(6))]. given #991 (A,wt=23): 378 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z) ' = y v z. [para(74(a,1),44(a,1,2))]. given #992 (F,wt=13): 1614 x v y != 1 | 0 != x | x ' = y v x. [para(13(a,1),104(a,1))]. given #993 (F,wt=13): 1659 (x v y) ^ (z v (y v x)) = x v y. [para(13(a,1),105(a,1,2)),demod(14(3))]. given #994 (T,wt=13): 1732 (x ^ (y v z)) v ((x ^ z) ' v u) = 1. [para(106(a,1),169(a,1,2,1,1))]. given #995 (T,wt=13): 1733 (x ^ (y v z)) v (u ^ (x ^ z)) ' = 1. [para(106(a,1),171(a,1,2,1,2))]. given #996 (A,wt=21): 380 x v (y ^ z) != 1 | y ^ z != 0 | (y ^ z) ' = x v (y ^ z). [para(74(a,1),46(a,1)),demod(103(8))]. given #997 (F,wt=13): 1734 (x ^ (y v z)) v (u v (x ^ z) ') = 1. [para(106(a,1),174(a,1,2,2,1))]. given #998 (F,wt=13): 1735 (c2 ^ (x ^ (y v c1))) v (x ^ c1) ' = 1. [para(106(a,1),206(a,1,2,1))]. given #999 (T,wt=13): 1799 ((x ^ y) v z) ^ (u v (y v z)) ' = 0. [para(107(a,1),148(a,1,2,1,2))]. given #1000 (T,wt=13): 1800 ((x ^ y) v z) ^ ((y v z) ' ^ u) = 0. [para(107(a,1),149(a,1,2,1,1))]. given #1001 (A,wt=23): 381 x ^ (y v (z ^ (u v (y ^ (u v x))))) = x ^ (y v (z ^ (u v y))). [para(13(a,1),49(a,2,2,2,2))]. given #1002 (F,wt=13): 1801 ((x ^ y) v z) ^ (u ^ (y v z) ') = 0. [para(107(a,1),153(a,1,2,2,1))]. given #1003 (F,wt=13): 1813 (c1 v ((x ^ c2) v y)) ^ (c2 v y) ' = 0. [para(107(a,1),1366(a,1,2,1)),demod(13(5))]. given #1004 (T,wt=13): 1850 x v (y v (z ^ (y v x))) = x v y. [para(13(a,1),108(a,1,2,2,2))]. given #1005 (T,wt=13): 1853 (x v (y ^ (z v x))) ^ (z v x) ' = 0. [para(108(a,1),134(a,1,2,1))]. given #1006 (A,wt=29): 382 x ^ (y v (z ^ (u v (v v (y ^ (u v (v v x))))))) = x ^ (y v (z ^ (y v (u v v)))). [para(14(a,1),49(a,1,2,2,2,2,2)),demod(14(5))]. given #1007 (F,wt=13): 1856 x v (y v (y v (z ^ (x v y))) ') = 1. [para(108(a,1),238(a,1,2)),demod(13(6),14(6))]. given #1008 (F,wt=13): 1893 1 != x | x ^ y != 0 | x ' = y ^ x. [para(15(a,1),110(b,1))]. given #1009 (T,wt=13): 1945 (x v (y ^ z)) ^ (u v (x v z)) ' = 0. [para(112(a,1),148(a,1,2,1,2))]. given #1010 (T,wt=13): 1946 (x v (y ^ z)) ^ ((x v z) ' ^ u) = 0. [para(112(a,1),149(a,1,2,1,1))]. given #1011 (A,wt=31): 383 x ^ (y v (z v (u ^ (v v ((y v z) ^ (v v x)))))) = x ^ (y v (z v (u ^ (y v (z v v))))). [para(14(a,1),49(a,1,2)),demod(14(11),14(13))]. given #1012 (F,wt=13): 1947 (x v (y ^ z)) ^ (u ^ (x v z) ') = 0. [para(112(a,1),153(a,1,2,2,1))]. given #1013 (F,wt=13): 1957 (c1 v (x v (y ^ c2))) ^ (x v c2) ' = 0. [para(112(a,1),1366(a,1,2,1)),demod(13(5))]. given #1014 (T,wt=13): 1974 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(15(a,1),113(a,1,2)),demod(16(3))]. given #1015 (T,wt=13): 2019 (x v (y v z)) ^ (y v x) = x v y. [para(115(a,1),15(a,1)),flip(a)]. given #1016 (A,wt=23): 384 x ^ (y v (z ^ (u v ((u v x) ^ y)))) = x ^ (y v (z ^ (y v u))). [para(15(a,1),49(a,1,2,2,2,2))]. given #1017 (F,wt=13): 2023 (c1 v x) ^ (x v (c2 v y)) = x v c1. [para(119(a,1),115(a,1,2,2))]. given #1018 (F,wt=13): 2024 (c1 v x) ^ (x v (y v c2)) = x v c1. [para(121(a,1),115(a,1,2,2))]. given #1019 (T,wt=13): 2048 x v (c2 v (y ^ (x v c1))) = x v c2. [para(122(a,1),109(a,1,2,2)),demod(14(6))]. given #1020 (T,wt=13): 2065 (x v (y v z)) ^ (z v x) = z v x. [para(116(a,1),15(a,1)),flip(a)]. given #1021 (A,wt=23): 385 x ^ (y v ((z v (y ^ (z v x))) ^ u)) = x ^ (y v (u ^ (y v z))). [para(15(a,1),49(a,1,2,2))]. given #1022 (F,wt=13): 2119 (x v (y v z)) ^ (z v (x v y)) ' = 0. [para(14(a,1),2062(a,1,1))]. given #1023 (F,wt=13): 2120 (x v (y v z)) ^ (y v (z v x)) ' = 0. [para(14(a,1),2062(a,1,2,1))]. given #1024 (T,wt=13): 2122 (x v (y v z)) ^ (x v (z v y)) ' = 0. [para(25(a,1),2062(a,1,1)),demod(14(4))]. given #1025 (T,wt=13): 2126 (x ^ (y ^ z)) ' v (u v (x ^ y)) = 1. [para(16(a,1),2071(a,1,1,1))]. given #1026 (A,wt=27): 386 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v) = x ^ ((y v (z ^ (y v u))) ^ v). [para(49(a,1),16(a,1,1)),demod(16(5)),flip(a)]. given #1027 (F,wt=13): 2128 x v (y v (((x ^ z) v y) ^ u) ') = 1. [para(31(a,1),2071(a,1,2)),demod(13(6),14(6))]. given #1028 (F,wt=13): 2139 x v (y v ((x v (y ^ z)) ^ u) ') = 1. [para(79(a,1),2071(a,1,2)),demod(13(6),14(6))]. given #1029 (T,wt=13): 2142 x v (y v (((z ^ x) v y) ^ u) ') = 1. [para(107(a,1),2071(a,1,2)),demod(13(6),14(6))]. given #1030 (T,wt=13): 2144 x v (y v ((x v (z ^ y)) ^ u) ') = 1. [para(112(a,1),2071(a,1,2)),demod(13(6),14(6))]. given #1031 (A,wt=29): 387 x ^ (y ^ (z v (u ^ (v v (z ^ (v v (x ^ y))))))) = x ^ (y ^ (z v (u ^ (z v v)))). [para(49(a,1),16(a,1)),demod(16(5)),flip(a)]. given #1032 (F,wt=13): 2146 (x ^ (y ^ z)) ' v (u v (x ^ z)) = 1. [para(26(a,1),2072(a,1,1,1))]. given #1033 (F,wt=13): 2147 (x ^ y) ' v (z v ((x v u) ^ y)) = 1. [para(29(a,1),2072(a,1,1,1))]. given #1034 (T,wt=13): 2149 x v (y v (z ^ ((x ^ u) v y)) ') = 1. [para(31(a,1),2072(a,1,2)),demod(13(6),14(6))]. given #1035 (T,wt=13): 2160 x v (y v (z ^ (x v (y ^ u))) ') = 1. [para(79(a,1),2072(a,1,2)),demod(13(6),14(6))]. given #1036 (A,wt=31): 388 x ^ ((y ^ z) v (u ^ ((y ^ z) v v))) = x ^ ((y ^ z) v (u ^ (v v (y ^ (z ^ (v v x)))))). [para(16(a,1),49(a,1,2,2,2,2)),flip(a)]. given #1037 (F,wt=13): 2162 (x ^ y) ' v (z v (x ^ (y v u))) = 1. [para(90(a,1),2072(a,1,1,1))]. given #1038 (F,wt=13): 2164 (x ^ y) ' v (z v ((u v x) ^ y)) = 1. [para(102(a,1),2072(a,1,1,1))]. given #1039 (T,wt=13): 2166 (x ^ y) ' v (z v (x ^ (u v y))) = 1. [para(106(a,1),2072(a,1,1,1))]. given #1040 (T,wt=13): 2167 x v (y v (z ^ ((u ^ x) v y)) ') = 1. [para(107(a,1),2072(a,1,2)),demod(13(6),14(6))]. given #1041 (A,wt=27): 389 x ^ (y v (z ^ (u ^ (v v (y ^ (v v x)))))) = x ^ (y v (z ^ (u ^ (y v v)))). [para(16(a,1),49(a,1,2,2)),demod(16(10))]. given #1042 (F,wt=13): 2169 x v (y v (z ^ (x v (u ^ y))) ') = 1. [para(112(a,1),2072(a,1,2)),demod(13(6),14(6))]. given #1043 (F,wt=13): 2217 x ^ (y ^ (((x v z) ^ y) v u) ') = 0. [para(136(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #1044 (T,wt=13): 2227 x ^ (y ^ (((z v x) ^ y) v u) ') = 0. [para(136(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #1045 (T,wt=13): 2232 x ^ (y ^ (z v ((x v u) ^ y)) ') = 0. [para(150(a,1),29(a,1,2)),demod(98(2)),flip(a)]. given #1046 (A,wt=21): 390 x ^ (y ^ (z v (u ^ (z v x)))) = x ^ (y ^ (z v (u ^ x))). [para(18(a,1),49(a,1,2,2,2,2,2)),demod(33(3),16(4),16(9)),flip(a)]. given #1047 (F,wt=13): 2242 x ^ (y ^ (z v ((u v x) ^ y)) ') = 0. [para(150(a,1),102(a,1,2)),demod(98(2)),flip(a)]. given #1048 (F,wt=13): 2266 (x v ((x v y) ^ z)) ^ (x v y) ' = 0. [para(32(a,1),152(a,1,2,1))]. given #1049 (T,wt=13): 2272 (x v (y ^ (z ^ u))) ^ (x v z) ' = 0. [para(91(a,1),152(a,1,2,1,2))]. given #1050 (T,wt=13): 2273 (x v (y ^ (z ^ u))) ^ (x v u) ' = 0. [para(109(a,1),152(a,1,2,1,2))]. given #1051 (A,wt=39): 391 x v (y v (z ^ (u v (y ^ (u v x))))) != 1 | x ^ (y v (z ^ (y v u))) != 0 | x ' = y v (z ^ (u v (y ^ (u v x)))). [para(49(a,1),21(b,1))]. given #1052 (F,wt=13): 2275 (x v (y ^ (z ^ c1))) ^ (x v c2) ' = 0. [para(290(a,1),152(a,1,2,1,2))]. given #1053 (F,wt=13): 2277 (x v (y ^ (c1 ^ z))) ^ (x v c2) ' = 0. [para(325(a,1),152(a,1,2,1,2))]. given #1054 (T,wt=13): 2278 (x v (y v c1)) ^ (x v (c2 v y)) ' = 0. [para(502(a,1),152(a,1,2,1,2))]. given #1055 (T,wt=13): 2282 (x v (y ^ (x v z))) ^ (x v z) ' = 0. [para(108(a,1),152(a,1,2,1))]. given #1056 (A,wt=23): 392 (x v (y ^ (x v z))) ^ (x v (y ^ (z v x))) = x v (y ^ (x v z)). [para(49(a,2),35(a,1)),demod(78(8))]. given #1057 (F,wt=13): 2295 ((x ^ (y ^ z)) v u) ^ (y v u) ' = 0. [para(26(a,1),163(a,1,1,1))]. given #1058 (F,wt=13): 2307 ((x ^ y) v (z ^ (x ^ u))) ^ x ' = 0. [para(91(a,1),163(a,1,2,1))]. given #1059 (T,wt=13): 2308 ((x ^ y) v (z ^ (u ^ x))) ^ x ' = 0. [para(109(a,1),163(a,1,2,1))]. given #1060 (T,wt=13): 2311 ((c2 ^ x) v (y ^ (z ^ c1))) ^ c2 ' = 0. [para(290(a,1),163(a,1,2,1))]. given #1061 (A,wt=29): 394 (x v y) ^ (z v (u ^ (v v (z ^ (x v (v v y)))))) = (x v y) ^ (z v (u ^ (z v v))). [para(25(a,1),49(a,1,2,2,2,2,2))]. given #1062 (F,wt=13): 2313 ((c2 ^ x) v (y ^ (c1 ^ z))) ^ c2 ' = 0. [para(325(a,1),163(a,1,2,1))]. given #1063 (F,wt=13): 2314 ((c2 ^ x) v (y v c1)) ^ (c2 v y) ' = 0. [para(502(a,1),163(a,1,2,1))]. given #1064 (T,wt=13): 2320 (x v (y v z)) ^ (y v (x v z)) ' = 0. [para(115(a,1),163(a,1,1,1)),demod(14(2),14(4))]. given #1065 (T,wt=13): 2321 ((x ^ y) v z) ^ (x v (z v u)) ' = 0. [para(163(a,1),117(a,1,2)),demod(15(4),88(4)),flip(a)]. given #1066 (A,wt=29): 395 x ^ (y v (z ^ (u v (v v (y ^ (u v (v v x))))))) = x ^ (y v (z ^ (u v (y v v)))). [para(25(a,1),49(a,2,2,2,2)),demod(14(3),14(5))]. given #1067 (F,wt=13): 2352 (x ^ (y v z)) v (x ^ (z v y)) ' = 1. [para(115(a,1),166(a,1,2,1,2))]. given #1068 (F,wt=13): 2363 (x ^ (y ^ z)) v (z ^ (x ^ y)) ' = 1. [para(16(a,1),2343(a,1,1))]. given #1069 (T,wt=13): 2364 (x ^ (y ^ z)) v (y ^ (z ^ x)) ' = 1. [para(16(a,1),2343(a,1,2,1))]. given #1070 (T,wt=13): 2366 (x ^ (y ^ z)) v (x ^ (z ^ y)) ' = 1. [para(26(a,1),2343(a,1,1)),demod(16(4))]. given #1071 (A,wt=27): 396 x ^ (y ^ (z v (u ^ (v v (z ^ (v v x)))))) = y ^ (x ^ (z v (u ^ (z v v)))). [para(49(a,1),26(a,1,2)),flip(a)]. given #1072 (F,wt=13): 2398 (x ^ ((x ^ y) v z)) v (x ^ y) ' = 1. [para(30(a,1),175(a,1,2,1))]. given #1073 (F,wt=13): 2399 (x ^ (c2 ^ y)) v (x ^ (c1 ^ y)) ' = 1. [para(66(a,1),175(a,1,2,1,2))]. given #1074 (T,wt=13): 2404 (x ^ (y v (z v u))) v (x ^ z) ' = 1. [para(78(a,1),175(a,1,2,1,2))]. given #1075 (T,wt=13): 2405 (x ^ (y ^ c2)) v (x ^ (y ^ c1)) ' = 1. [para(94(a,1),175(a,1,2,1,2))]. given #1076 (A,wt=19): 397 x ^ ((y v z) ^ (y v (x ^ (z v y)))) = x ^ (y v z). [para(49(a,2),27(a,1)),demod(381(10),16(6))]. given #1077 (F,wt=11): 13670 x ^ (c1 v (x ^ c2)) = x ^ c2. [para(111(a,1),397(a,1,2,1)),demod(13(5),111(5),3842(6),111(8))]. given #1078 (F,wt=11): 13672 x ^ (c1 v (c2 ^ x)) = x ^ c2. [para(15(a,1),13670(a,1,2,2))]. given #1079 (T,wt=13): 2406 (x ^ (y v (z v u))) v (x ^ u) ' = 1. [para(101(a,1),175(a,1,2,1,2))]. given #1080 (T,wt=13): 2418 (x ^ (y v (c2 v z))) v (x ^ c1) ' = 1. [para(209(a,1),175(a,1,2,1,2))]. given #1081 (A,wt=33): 398 x v ((y ^ (z v (x ^ (z v u)))) v (u ^ (x v (y ^ (x v z))))) = x v (y ^ (z v (x ^ (z v u)))). [para(49(a,1),33(a,1,2)),demod(14(10))]. given #1082 (F,wt=13): 2419 (x ^ (y v (z v c2))) v (x ^ c1) ' = 1. [para(211(a,1),175(a,1,2,1,2))]. given #1083 (F,wt=13): 2426 (x ^ (y v (x ^ z))) v (x ^ z) ' = 1. [para(103(a,1),175(a,1,2,1))]. given #1084 (T,wt=13): 2429 (x ^ (y v c2)) v (x ^ (y v c1)) ' = 1. [para(122(a,1),175(a,1,2,1,2))]. given #1085 (T,wt=13): 2440 ((x v (y v z)) ^ u) v (y ^ u) ' = 1. [para(25(a,1),176(a,1,1,1))]. given #1086 (A,wt=25): 399 x v ((y ^ (x v z)) v (u ^ (x v (y ^ (z v x))))) = x v (y ^ (x v z)). [para(49(a,2),33(a,1,2)),demod(381(9),14(8))]. given #1087 (F,wt=13): 2454 ((x v y) ^ (z v (x v u))) v x ' = 1. [para(78(a,1),176(a,1,2,1))]. given #1088 (F,wt=13): 2455 ((c1 v x) ^ (y ^ c2)) v (y ^ c1) ' = 1. [para(94(a,1),176(a,1,2,1))]. given #1089 (T,wt=13): 2456 ((x v y) ^ (z v (u v x))) v x ' = 1. [para(101(a,1),176(a,1,2,1))]. given #1090 (T,wt=13): 2470 ((c1 v x) ^ (y v (c2 v z))) v c1 ' = 1. [para(209(a,1),176(a,1,2,1))]. given #1091 (A,wt=25): 400 x ^ (y v ((y v z) ^ (z v (u v (y ^ (z v (u v x))))))) = x ^ (y v z). [para(28(a,1),49(a,2,2,2)),demod(14(4),14(6),73(11))]. given #1092 (F,wt=13): 2471 ((c1 v x) ^ (y v (z v c2))) v c1 ' = 1. [para(211(a,1),176(a,1,2,1))]. given #1093 (F,wt=13): 2480 (x ^ y) ' v (((x v z) ^ y) v u) = 1. [para(176(a,1),115(a,1,1)),demod(76(8),2434(11))]. given #1094 (T,wt=13): 2496 x v (y v ((z ^ (x ^ u)) v y) ') = 1. [para(26(a,1),191(a,1,2,2,1,1))]. given #1095 (T,wt=13): 2515 x ^ (y ^ ((z v (x v u)) ^ y) ') = 0. [para(25(a,1),194(a,1,2,2,1,1))]. given #1096 (A,wt=21): 401 c2 ^ (x v (y ^ (c1 v (x ^ c2)))) = c2 ^ (x v (y ^ (x v c1))). [para(111(a,1),49(a,1,2,2,2,2,2))]. given #1097 (F,wt=13): 2536 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(17(a,1),201(a,1,1))]. given #1098 (F,wt=11): 13794 x v (c2 ^ (c1 v x)) = x v c1. [para(2536(a,1),1850(a,1,2))]. given #1099 (T,wt=11): 13804 x v (c2 ^ (x v c1)) = x v c1. [para(13(a,1),13794(a,1,2,2))]. given #1100 (T,wt=13): 2541 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(27(a,1),201(a,1,1))]. given #1101 (A,wt=23): 402 x ^ (y v (z ^ (y ' v (u v (y ^ (y ' v (u v x))))))) = x ^ (y v z). [para(86(a,1),49(a,2,2,2,2)),demod(14(5),14(7),39(12))]. given #1102 (F,wt=13): 2565 (x v (c1 ^ y)) ^ (x v (c2 ^ y)) ' = 0. [para(201(a,1),135(a,1,2,1,2))]. given #1103 (F,wt=13): 2581 ((c2 v x) ^ y) v ((c1 ^ y) ' v z) = 1. [para(202(a,1),169(a,1,2,1,1))]. given #1104 (T,wt=13): 2582 ((c2 v x) ^ y) v (z ^ (c1 ^ y)) ' = 1. [para(202(a,1),171(a,1,2,1,2))]. given #1105 (T,wt=13): 2584 ((c2 v x) ^ y) v (z v (c1 ^ y) ') = 1. [para(202(a,1),174(a,1,2,2,1))]. given #1106 (A,wt=23): 403 x ^ (y v (z ^ (u v (y ' v (y ^ (u v (y ' v x))))))) = x ^ (y v z). [para(96(a,1),49(a,2,2,2,2)),demod(14(5),14(7),39(12))]. given #1107 (F,wt=13): 2594 (c1 ^ x) ' v (y v ((c2 v z) ^ x)) = 1. [para(202(a,1),2072(a,1,1,1))]. given #1108 (F,wt=13): 2595 c1 ^ (x ^ (((c2 v y) ^ x) v z) ') = 0. [para(136(a,1),202(a,1,2)),demod(15(3),88(3)),flip(a)]. given #1109 (T,wt=13): 2596 c1 ^ (x ^ (y v ((c2 v z) ^ x)) ') = 0. [para(150(a,1),202(a,1,2)),demod(15(3),88(3)),flip(a)]. given #1110 (T,wt=13): 2605 (x ^ (c2 v y)) v ((x ^ c1) ' v z) = 1. [para(210(a,1),169(a,1,2,1,1))]. given #1111 (A,wt=25): 404 x ^ (y v (z ^ (u v (y ^ (u v (x v v)))))) = x ^ (y v (z ^ (y v u))). [para(49(a,1),29(a,1,2)),demod(29(6)),flip(a)]. given #1112 (F,wt=13): 2606 (x ^ (c2 v y)) v (z ^ (x ^ c1)) ' = 1. [para(210(a,1),171(a,1,2,1,2))]. given #1113 (F,wt=13): 2607 (x ^ (c2 v y)) v (z v (x ^ c1) ') = 1. [para(210(a,1),174(a,1,2,2,1))]. given #1114 (T,wt=13): 2613 (x ^ c1) ' v (y v (x ^ (c2 v z))) = 1. [para(210(a,1),2072(a,1,1,1))]. given #1115 (T,wt=13): 2624 ((x v c2) ^ y) v ((c1 ^ y) ' v z) = 1. [para(212(a,1),169(a,1,2,1,1))]. given #1116 (A,wt=35): 405 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ ((x ^ (y v (z ^ (y v u)))) v v)) = x ^ (y v (z ^ (u v y))). [para(49(a,1),30(a,1,2,2,1)),demod(381(18))]. given #1117 (F,wt=13): 2625 ((x v c2) ^ y) v (z ^ (c1 ^ y)) ' = 1. [para(212(a,1),171(a,1,2,1,2))]. given #1118 (F,wt=13): 2627 ((x v c2) ^ y) v (z v (c1 ^ y) ') = 1. [para(212(a,1),174(a,1,2,2,1))]. given #1119 (T,wt=13): 2636 (c1 ^ x) ' v (y v ((z v c2) ^ x)) = 1. [para(212(a,1),2072(a,1,1,1))]. given #1120 (T,wt=13): 2637 c1 ^ (x ^ (((y v c2) ^ x) v z) ') = 0. [para(136(a,1),212(a,1,2)),demod(15(3),88(3)),flip(a)]. given #1121 (A,wt=31): 406 x ^ ((y v (z ^ (y v u))) ^ ((x ^ (y v (z ^ (u v y)))) v v)) = x ^ (y v (z ^ (y v u))). [para(49(a,2),30(a,1,2,2,1)),demod(381(9))]. given #1122 (F,wt=13): 2638 c1 ^ (x ^ (y v ((z v c2) ^ x)) ') = 0. [para(150(a,1),212(a,1,2)),demod(15(3),88(3)),flip(a)]. given #1123 (F,wt=13): 2642 c1 ^ (x ^ ((y v (c2 v z)) ^ x) ') = 0. [para(194(a,1),212(a,1,2)),demod(15(3),88(3),14(5)),flip(a)]. given #1124 (T,wt=13): 2648 (x ^ (y v c2)) v ((x ^ c1) ' v z) = 1. [para(214(a,1),169(a,1,2,1,1))]. given #1125 (T,wt=13): 2649 (x ^ (y v c2)) v (z ^ (x ^ c1)) ' = 1. [para(214(a,1),171(a,1,2,1,2))]. given #1126 (A,wt=35): 407 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ ((x ^ (y v (z ^ (u v y)))) v v)) = x ^ (y v (z ^ (y v u))). [para(49(a,1),30(a,2)),demod(381(11))]. given #1127 (F,wt=13): 2650 (x ^ (y v c2)) v (z v (x ^ c1) ') = 1. [para(214(a,1),174(a,1,2,2,1))]. given #1128 (F,wt=13): 2656 (x ^ c1) ' v (y v (x ^ (z v c2))) = 1. [para(214(a,1),2072(a,1,1,1))]. given #1129 (T,wt=13): 2675 x ' v y != 1 | x ' ^ y != 0 | x = y. [para(238(a,1),128(a,1,2,1)),demod(76(3),223(10),238(11),76(10))]. given #1130 (T,wt=9): 14012 x ' != 1 | x ' != 0 | x ' = x. [para(35(a,1),2675(b,1)),demod(36(3)),flip(c)]. given #1131 (A,wt=31): 408 ((x ^ y) v z) ^ (u v (v ^ (u v x))) = ((x ^ y) v z) ^ (u v (v ^ (x v (u ^ (x v z))))). [para(31(a,1),49(a,1,2,2,2,2,2)),flip(a)]. given #1132 (F,wt=12): 14015 x ' v (x ' v y) ' != 1 | (x ' v y) ' = x. [para(127(a,1),2675(b,1)),flip(c),xx(b)]. given #1133 (F,wt=12): 14016 x ' v (y v x ') ' != 1 | (y v x ') ' = x. [para(134(a,1),2675(b,1)),flip(c),xx(b)]. given #1134 (T,wt=12): 14017 x ' ^ (x ' ^ y) ' != 0 | (x ' ^ y) ' = x. [para(157(a,1),2675(a,1)),flip(c),xx(a)]. given #1135 (T,wt=12): 14018 x ' ^ (y ^ x ') ' != 0 | (y ^ x ') ' = x. [para(165(a,1),2675(a,1)),flip(c),xx(a)]. given #1136 (A,wt=31): 409 x ^ (y v (z ^ ((y ^ u) v (v v (y ^ ((y ^ u) v (v v x))))))) = x ^ (y v (z ^ (y v v))). [para(31(a,1),49(a,2,2,2,2)),demod(14(5),14(7))]. given #1137 (F,wt=12): 14038 x ' v (y v x ') ' != 1 | (x ' v y) ' = x. [para(13(a,1),14015(a,1,2,1))]. given #1138 (F,wt=12): 14040 x ' v (x ' v y) ' != 1 | (y v x ') ' = x. [para(13(a,1),14016(a,1,2,1))]. given #1139 (T,wt=12): 14041 x ' ^ (y ^ x ') ' != 0 | (x ' ^ y) ' = x. [para(15(a,1),14017(a,1,2,1))]. given #1140 (T,wt=12): 14043 x ' ^ (x ' ^ y) ' != 0 | (y ^ x ') ' = x. [para(15(a,1),14018(a,1,2,1))]. given #1141 (A,wt=23): 410 x v ((y ^ (z v (x ^ (z v u)))) v (u ^ (x v (y ^ (x v z)))) ') = 1. [para(49(a,1),165(a,1,2,1)),demod(14(11))]. given #1142 (F,wt=13): 2677 c2 != 1 | c2 ^ x != 0 | c2 ' = c2 ^ x. [para(283(a,1),128(a,1,2,1)),demod(18(4),283(13))]. given #1143 (F,wt=13): 2720 ((x ^ c1) v y) ^ (z v (c2 v y)) ' = 0. [para(285(a,1),148(a,1,2,1,2))]. given #1144 (T,wt=13): 2721 ((x ^ c1) v y) ^ ((c2 v y) ' ^ z) = 0. [para(285(a,1),149(a,1,2,1,1))]. given #1145 (T,wt=13): 2722 ((x ^ c1) v y) ^ (z ^ (c2 v y) ') = 0. [para(285(a,1),153(a,1,2,2,1))]. given #1146 (A,wt=19): 411 x v ((y ^ (x v z)) v (u ^ (x v (y ^ (z v x)))) ') = 1. [para(49(a,2),165(a,1,2,1)),demod(381(9),14(9))]. given #1147 (F,wt=13): 2735 c2 v (x v (((y ^ c1) v x) ^ z) ') = 1. [para(285(a,1),2071(a,1,2)),demod(13(8),14(8))]. given #1148 (F,wt=13): 2736 c2 v (x v (y ^ ((z ^ c1) v x)) ') = 1. [para(285(a,1),2072(a,1,2)),demod(13(8),14(8))]. given #1149 (T,wt=13): 2740 c2 v (x v ((y ^ (c1 ^ z)) v x) ') = 1. [para(191(a,1),285(a,1,2)),demod(13(3),85(3),16(5)),flip(a)]. given #1150 (T,wt=13): 2750 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1. [para(288(a,1),101(a,1,2,2)),demod(16(6))]. given #1151 (A,wt=23): 412 x ^ (c2 v (y ^ (c1 ' v (z v (c2 ^ (c1 ' v (z v x))))))) = x ^ (c2 v y). [para(178(a,1),49(a,2,2,2,2)),demod(14(9),14(11),39(17))]. given #1152 (F,wt=13): 2768 (x v (y ^ c1)) ^ (x v (c2 ^ y)) ' = 0. [para(288(a,1),152(a,1,2,1,2))]. given #1153 (F,wt=13): 2781 (x v (y ^ c1)) ^ (z v (x v c2)) ' = 0. [para(291(a,1),148(a,1,2,1,2))]. given #1154 (T,wt=13): 2782 (x v (y ^ c1)) ^ ((x v c2) ' ^ z) = 0. [para(291(a,1),149(a,1,2,1,1))]. given #1155 (T,wt=13): 2783 (x v (y ^ c1)) ^ (z ^ (x v c2) ') = 0. [para(291(a,1),153(a,1,2,2,1))]. given #1156 (A,wt=35): 413 (x v ((y v x) ^ z)) ^ (u v (v ^ (u v y))) = (x v ((y v x) ^ z)) ^ (u v (v ^ (y v (u ^ (y v x))))). [para(32(a,1),49(a,1,2,2,2,2,2)),flip(a)]. given #1157 (F,wt=13): 2787 x v c2 != 1 | c2 != 0 | c2 ' = x v c2. [para(291(a,1),75(a,1)),demod(291(14)),flip(b)]. given #1158 (F,wt=13): 2794 x v (c2 v ((x v (y ^ c1)) ^ z) ') = 1. [para(291(a,1),2071(a,1,2)),demod(13(8),14(8))]. given #1159 (T,wt=13): 2795 x v (c2 v (y ^ (x v (z ^ c1))) ') = 1. [para(291(a,1),2072(a,1,2)),demod(13(8),14(8))]. given #1160 (T,wt=13): 2811 ((c1 ^ x) v y) ^ (z v (c2 v y)) ' = 0. [para(322(a,1),148(a,1,2,1,2))]. given #1161 (A,wt=35): 414 x ^ (y v (z ^ (u v (((y v u) ^ v) v (y ^ (u v (((y v u) ^ v) v x))))))) = x ^ (y v (z ^ (y v u))). [para(32(a,1),49(a,2,2,2,2)),demod(14(7),14(9))]. given #1162 (F,wt=13): 2812 ((c1 ^ x) v y) ^ ((c2 v y) ' ^ z) = 0. [para(322(a,1),149(a,1,2,1,1))]. given #1163 (F,wt=13): 2813 ((c1 ^ x) v y) ^ (z ^ (c2 v y) ') = 0. [para(322(a,1),153(a,1,2,2,1))]. given #1164 (T,wt=13): 2826 c2 v (x v (((c1 ^ y) v x) ^ z) ') = 1. [para(322(a,1),2071(a,1,2)),demod(13(8),14(8))]. given #1165 (T,wt=13): 2827 c2 v (x v (y ^ ((c1 ^ z) v x)) ') = 1. [para(322(a,1),2072(a,1,2)),demod(13(8),14(8))]. given #1166 (A,wt=23): 415 x ^ (c2 v (y ^ (z v (c1 ' v (c2 ^ (z v (c1 ' v x))))))) = x ^ (c2 v y). [para(180(a,1),49(a,2,2,2,2)),demod(14(9),14(11),39(17))]. given #1167 (F,wt=13): 2840 x ^ (y ^ (y ^ (z v (x v u))) ') = 0. [para(192(a,1),129(a,1,2)),demod(98(2)),flip(a)]. given #1168 (F,wt=13): 2842 x ^ (c1 ^ (c2 ^ (y v (x v z))) ') = 0. [para(448(a,1),129(a,1,2)),demod(98(2),15(6)),flip(a)]. low water: id=11771, wt=19 given #1169 (T,wt=13): 2855 x ^ ((x v y) ^ (z v (x v u))) ' = 0. [para(129(a,1),194(a,1))]. given #1170 (T,wt=13): 2868 (x v (c1 ^ y)) ^ (z v (x v c2)) ' = 0. [para(324(a,1),148(a,1,2,1,2))]. given #1171 (A,wt=27): 416 x ^ (y v (z ^ (u v ((y v u) ' v (y ^ (u v ((y v u) ' v x))))))) = x ^ (y v z). [para(38(a,1),49(a,2,2,2,2)),demod(14(7),14(9),39(14))]. given #1172 (F,wt=13): 2869 (x v (c1 ^ y)) ^ ((x v c2) ' ^ z) = 0. [para(324(a,1),149(a,1,2,1,1))]. given #1173 (F,wt=13): 2870 (x v (c1 ^ y)) ^ (z ^ (x v c2) ') = 0. [para(324(a,1),153(a,1,2,2,1))]. given #1174 (T,wt=13): 2881 x v (c2 v ((x v (c1 ^ y)) ^ z) ') = 1. [para(324(a,1),2071(a,1,2)),demod(13(8),14(8))]. given #1175 (T,wt=13): 2882 x v (c2 v (y ^ (x v (c1 ^ z))) ') = 1. [para(324(a,1),2072(a,1,2)),demod(13(8),14(8))]. given #1176 (A,wt=25): 417 x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ (x ^ (y v (z ^ (y v u)))) ') = 0. [para(49(a,1),41(a,1,2,2,1))]. given #1177 (F,wt=13): 2891 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(372(a,1),31(a,2)),demod(16(3),2886(6))]. given #1178 (F,wt=13): 2908 (x v (y ^ z)) ^ (x v (z ^ y)) ' = 0. [para(372(a,1),152(a,1,2,1,2))]. given #1179 (T,wt=13): 2923 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1. [para(446(a,1),78(a,1,2,2)),demod(16(6))]. given #1180 (T,wt=13): 2931 (x v (y ^ c1)) ^ (x v (y ^ c2)) ' = 0. [para(446(a,1),135(a,1,2,1,2))]. given #1181 (A,wt=21): 418 x ^ ((y v (z ^ (y v u))) ^ (x ^ (y v (z ^ (u v y)))) ') = 0. [para(49(a,2),41(a,1,2,2,1)),demod(381(9))]. given #1182 (F,wt=13): 3027 x v (c2 v (y ^ (c1 v x))) = x v c2. [para(620(a,1),109(a,1,2,2)),demod(14(6))]. given #1183 (F,wt=13): 3037 (c1 v x) ^ (c2 v (x v y)) = c1 v x. [para(620(a,1),117(a,1,2)),demod(28(6),13(7)),flip(a)]. given #1184 (T,wt=13): 3038 (x ^ (y v c2)) v (x ^ (c1 v y)) ' = 1. [para(620(a,1),175(a,1,2,1,2))]. given #1185 (T,wt=13): 3040 c1 v x != 1 | c1 != 0 | c1 ' = c1 v x. [para(620(a,1),128(a,1,2)),demod(73(4),200(8),620(14))]. given #1186 (A,wt=35): 419 (x ^ (y v (z ^ (y v u)))) v (x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v)) = x ^ (y v (z ^ (u v y))). [para(49(a,1),34(a,1,1)),demod(381(18))]. given #1187 (F,wt=13): 3060 (x v c1) ^ ((y v (c2 v x)) ' ^ z) = 0. [para(502(a,1),723(a,1,2,1,1,2))]. given #1188 (F,wt=13): 3077 (x v c1) ^ (y ^ (z v (c2 v x)) ') = 0. [para(502(a,1),726(a,1,2,2,1,2))]. given #1189 (T,wt=13): 3112 (c2 ^ x) v ((y ^ (c1 ^ x)) ' v z) = 1. [para(66(a,1),797(a,1,2,1,1,2))]. given #1190 (T,wt=13): 3115 (x ^ c2) v ((y ^ (x ^ c1)) ' v z) = 1. [para(94(a,1),797(a,1,2,1,1,2))]. given #1191 (A,wt=31): 420 (x ^ (y v (z ^ (u v y)))) v (x ^ ((y v (z ^ (y v u))) ^ v)) = x ^ (y v (z ^ (y v u))). [para(49(a,2),34(a,1,1)),demod(381(6))]. given #1192 (F,wt=13): 3146 (c2 ^ (x v (c1 v y))) v (c1 ' v z) = 1. [para(78(a,1),802(a,1,2,1,1))]. given #1193 (F,wt=13): 3147 (c2 ^ (x v (y v c1))) v (c1 ' v z) = 1. [para(101(a,1),802(a,1,2,1,1))]. given #1194 (T,wt=13): 3187 (c2 ^ x) v (y v (z ^ (c1 ^ x)) ') = 1. [para(66(a,1),814(a,1,2,2,1,2))]. given #1195 (T,wt=13): 3191 (x ^ c2) v (y v (z ^ (x ^ c1)) ') = 1. [para(94(a,1),814(a,1,2,2,1,2))]. given #1196 (A,wt=35): 421 (x ^ (y v (z ^ (u v y)))) v (x ^ ((y v (z ^ (u v (y ^ (u v x))))) ^ v)) = x ^ (y v (z ^ (y v u))). [para(49(a,1),34(a,2)),demod(381(6))]. given #1197 (F,wt=13): 3218 (c2 ^ ((x ^ c1) v y)) v (x ^ c1) ' = 1. [para(30(a,1),817(a,1,2,1))]. given #1198 (F,wt=13): 3221 (c2 ^ (x v (c1 v y))) v (z ^ c1) ' = 1. [para(78(a,1),817(a,1,2,1,2))]. given #1199 (T,wt=13): 3222 (c2 ^ (x v (y v c1))) v (z ^ c1) ' = 1. [para(101(a,1),817(a,1,2,1,2))]. given #1200 (T,wt=13): 3241 (c2 ^ (x v (y ^ c1))) v (y ^ c1) ' = 1. [para(103(a,1),817(a,1,2,1))]. given #1201 (A,wt=31): 422 x ^ ((y ^ z) v (u ^ ((y ^ (z ^ v)) v (y ^ (z ^ ((y ^ (z ^ v)) v x)))))) = x ^ (y ^ z). [para(34(a,1),49(a,2,2,2,2)),demod(16(8),33(16))]. given #1202 (F,wt=13): 3244 (x ^ (c1 ^ y)) ' v (z v (c2 ^ y)) = 1. [para(817(a,1),116(a,1,1)),demod(76(10),817(15))]. given #1203 (F,wt=13): 3251 (x ^ ((x ^ y) v z)) v (y ^ x) ' = 1. [para(143(a,1),165(a,1,2,1))]. given #1204 (T,wt=13): 3252 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x. [para(143(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #1205 (T,wt=13): 3253 x ^ (y ^ (y ^ ((y ^ x) v z)) ') = 0. [para(143(a,1),239(a,1,2)),demod(15(6),16(6))]. given #1206 (A,wt=23): 423 c1 ^ (x v (y ^ (z v (x ^ (z v c2))))) = c1 ^ (x v (y ^ (x v z))). [para(49(a,1),66(a,1,2)),demod(66(7)),flip(a)]. given #1207 (F,wt=13): 3275 (x v y) ' ^ (((x ^ z) v y) ^ u) = 0. [para(163(a,1),143(a,1,2,2,1)),demod(82(6),2289(11))]. given #1208 (F,wt=13): 3277 (x ^ ((y ^ x) v z)) v (x ^ y) ' = 1. [para(143(a,1),175(a,1,2,1))]. given #1209 (T,wt=13): 3289 (c2 ^ ((c1 ^ x) v y)) v (x ^ c1) ' = 1. [para(143(a,1),817(a,1,2,1))]. given #1210 (T,wt=13): 3303 (x ^ (y ^ c1)) ' v (z v (y ^ c2)) = 1. [para(820(a,1),116(a,1,1)),demod(76(10),820(15))]. given #1211 (A,wt=31): 424 x v ((y ^ (x v z)) v u) != 1 | u ^ (x v (y ^ (z v x))) != 0 | u ' = x v (y ^ (x v z)). [para(49(a,2),43(b,1)),demod(14(4),381(12))]. given #1212 (F,wt=13): 3304 (c2 ^ (x v (y v z))) v (y ^ c1) ' = 1. [para(129(a,1),820(a,1,2,1)),dem