============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 13671 was started by mccune on cleo.thornwood, Mon Jun 19 16:48:36 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H42.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 H42.in clauses(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (y v (u v (x ^ z))))) # label(H42). 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 ^ (x v u))) = x ^ (y v (z ^ (y v (u v (x ^ z))))) # label(H42). [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 ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (x v u))) # label(H42). [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=6): 19 x v x ' = 1. [input]. given #8 (I,wt=6): 20 x ^ x ' = 0. [input]. given #9 (I,wt=14): 21 x v y != 1 | x ^ y != 0 | x ' = y. [input]. given #10 (I,wt=23): 22 x ^ (y v (z ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (x v u))) # label(H42). [copy(10),flip(a)]. given #11 (I,wt=5): 23 c1 ^ c2 = c1. [clausify]. given #12 (I,wt=8): 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): 78 1 ^ x = x. [para(39(a,1),15(a,1)),flip(a)]. given #19 (T,wt=4): 86 1 ' = 0. [hyper(21,a,42,a,b,78,a)]. given #20 (T,wt=5): 84 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=4): 89 0 ' = 1. [hyper(21,a,84,a,b,39,a)]. given #23 (F,wt=5): 87 1 v x = 1. [para(78(a,1),17(a,1))]. given #24 (T,wt=5): 90 0 ^ x = 0. [para(84(a,1),17(a,1,2))]. given #25 (T,wt=5): 97 x v 1 = 1. [para(87(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): 100 x ^ 0 = 0. [para(90(a,1),15(a,1)),flip(a)]. given #28 (F,wt=7): 33 x v (y ^ x) = x. [para(15(a,1),18(a,1,2))]. given #29 (T,wt=5): 113 c1 v c2 = c2. [para(23(a,1),33(a,1,2)),demod(13(3))]. given #30 (T,wt=7): 99 0 != x | x ' = 1. [back_demod(79),demod(97(2)),xx(a)]. 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=7): 102 1 != x | x ' = 0. [back_demod(85),demod(100(4)),xx(b)]. given #33 (F,wt=8): 88 x v (x ' v y) = 1. [back_demod(37),demod(87(5))]. given #34 (T,wt=8): 91 x ^ (x ' ^ y) = 0. [back_demod(40),demod(90(5))]. given #35 (T,wt=8): 98 x v (y v x ') = 1. [back_demod(82),demod(97(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=9): 131 c1 ^ (c1 ' v c2 ') != 0. [ur(21,a,88,a,c,24,a(flip))]. given #38 (F,wt=8): 101 x ^ (y ^ x ') = 0. [back_demod(94),demod(100(5))]. given #39 (T,wt=8): 142 x ^ (x v y) ' = 0. [para(20(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #40 (T,wt=6): 157 c1 ^ c2 ' = 0. [para(113(a,1),142(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=8): 152 x ^ (y v x) ' = 0. [para(13(a,1),142(a,1,2,1))]. given #43 (F,wt=8): 158 c1 ^ (c2 ' ^ x) = 0. [para(157(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #44 (T,wt=8): 160 c1 ^ (x ^ c2 ') = 0. [para(157(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #45 (T,wt=9): 66 c1 ^ (c2 ^ x) = c1 ^ x. [para(23(a,1),16(a,1,1)),flip(a)]. 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): 180 c1 ^ (c2 v x) = c1. [para(17(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #48 (F,wt=7): 183 c1 ^ (x v c2) = c1. [para(27(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #49 (T,wt=8): 186 c1 ^ (c2 v x) ' = 0. [para(142(a,1),66(a,1,2)),demod(15(3),90(3)),flip(a)]. given #50 (T,wt=8): 188 c1 ^ (x v c2) ' = 0. [para(152(a,1),66(a,1,2)),demod(15(3),90(3)),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=8): 191 x v (x ^ y) ' = 1. [para(19(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #53 (F,wt=8): 224 x v (y ^ x) ' = 1. [para(15(a,1),191(a,1,2,1))]. given #54 (T,wt=6): 232 c2 v c1 ' = 1. [para(23(a,1),224(a,1,2,1))]. given #55 (T,wt=8): 238 c2 v (x v c1 ') = 1. [para(180(a,1),224(a,1,2,1)),demod(14(5))]. 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=8): 239 c2 v (c1 ' v x) = 1. [para(232(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #58 (F,wt=9): 67 c2 ^ (x ^ c1) = x ^ c1. [para(23(a,1),16(a,2,2)),demod(15(4))]. given #59 (T,wt=7): 255 c2 v (x ^ c1) = c2. [para(67(a,1),18(a,1,2))]. given #60 (T,wt=7): 261 c2 v (c1 ^ x) = c2. [para(15(a,1),255(a,1,2))]. given #61 (A,wt=10): 38 x v (y v (x v y) ') = 1. [para(19(a,1),14(a,1)),flip(a)]. given #62 (F,wt=8): 258 c2 v (x ^ c1) ' = 1. [para(67(a,1),191(a,1,2,1))]. given #63 (F,wt=8): 275 c2 v (c1 ^ x) ' = 1. [para(15(a,1),258(a,1,2,1))]. given #64 (T,wt=9): 69 x ^ (x ^ y) = x ^ y. [para(35(a,1),16(a,1,1)),flip(a)]. given #65 (T,wt=9): 71 x ^ (y ^ x) = y ^ x. [para(35(a,1),16(a,2,2)),demod(15(2))]. given #66 (A,wt=10): 41 x ^ (y ^ (x ^ y) ') = 0. [para(20(a,1),16(a,1)),flip(a)]. given #67 (F,wt=9): 74 x v (x v y) = x v y. [para(36(a,1),14(a,1,1)),flip(a)]. given #68 (F,wt=9): 76 x v (y v x) = y v x. [para(36(a,1),14(a,2,2)),demod(13(2))]. given #69 (T,wt=9): 80 x ^ (y v (x v z)) = x. [para(25(a,1),17(a,1,2))]. given #70 (T,wt=9): 93 x v (y ^ (x ^ z)) = x. [para(26(a,1),18(a,1,2))]. given #71 (A,wt=14): 43 x v y != 1 | y ^ x != 0 | y ' = x. [para(13(a,1),21(a,1))]. given #72 (F,wt=5): 312 x ' ' = x. [para(19(a,1),43(a,1)),demod(15(5),20(5)),xx(a),xx(b)]. given #73 (F,wt=8): 335 x ' v (y v x) = 1. [para(312(a,1),98(a,1,2,2))]. given #74 (T,wt=8): 336 x ' ^ (y ^ x) = 0. [para(312(a,1),101(a,1,2,2))]. given #75 (T,wt=9): 96 c1 ^ (x ^ c2) = x ^ c1. [para(23(a,1),26(a,1,2)),flip(a)]. given #76 (A,wt=20): 44 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y) ' = z. [para(14(a,1),21(a,1))]. given #77 (F,wt=9): 103 x ^ (y v (z v x)) = x. [para(14(a,1),27(a,1,2))]. given #78 (F,wt=9): 111 x v (y ^ (z ^ x)) = x. [para(16(a,1),33(a,1,2))]. given #79 (T,wt=9): 117 c1 v (c2 v x) = c2 v x. [para(113(a,1),14(a,1,1)),flip(a)]. given #80 (T,wt=9): 118 c2 v (x v c1) = x v c2. [para(113(a,1),14(a,2,2)),demod(13(4))]. given #81 (A,wt=14): 45 x v y != 1 | y ^ x != 0 | x ' = y. [para(15(a,1),21(b,1))]. given #82 (F,wt=9): 119 c1 v (x v c2) = x v c2. [para(113(a,1),25(a,1,2)),flip(a)]. given #83 (F,wt=9): 200 c1 ^ (x v (c2 v y)) = c1. [para(25(a,1),180(a,1,2))]. given #84 (T,wt=9): 202 c1 ^ (x v (y v c2)) = c1. [para(14(a,1),183(a,1,2))]. given #85 (T,wt=9): 262 c2 v (x ^ (y ^ c1)) = c2. [para(16(a,1),255(a,1,2))]. given #86 (A,wt=20): 46 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = z. [para(16(a,1),21(b,1))]. given #87 (F,wt=9): 267 c2 v (x ^ (c1 ^ y)) = c2. [para(26(a,1),261(a,1,2))]. given #88 (F,wt=9): 323 c2 ^ c1 ' != 0 | c2 = c1. [para(232(a,1),43(a,1)),demod(15(7),312(12)),flip(c),xx(a)]. given #89 (T,wt=9): 429 c2 v (x v c1) = c2 v x. [para(118(a,2),13(a,1))]. given #90 (T,wt=9): 450 c1 v c2 ' != 1 | c2 = c1. [para(157(a,1),45(b,1)),demod(13(4),312(12)),xx(b)]. given #91 (A,wt=23): 49 x ^ (y v (z ^ (y v ((x ^ z) v u)))) = x ^ (y v (z ^ (x v u))). [para(13(a,1),22(a,1,2,2,2,2))]. given #92 (F,wt=10): 72 1 != x | 0 != x | x ' = x. [para(35(a,1),21(b,1)),demod(36(1)),flip(a),flip(b)]. given #93 (F,wt=10): 116 c2 != 1 | c1 != 0 | c1 ' = c2. [back_demod(68),demod(113(3))]. given #94 (T,wt=10): 134 x v (y v (x ' v z)) = 1. [para(88(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #95 (T,wt=10): 137 x ^ (y ^ (x ' ^ z)) = 0. [para(91(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #96 (A,wt=23): 50 x ^ (y v (z ^ (u v ((x ^ z) v y)))) = x ^ (y v (z ^ (x v u))). [para(13(a,1),22(a,1,2,2,2)),demod(14(3))]. given #97 (F,wt=10): 139 x v (y v (z v x ')) = 1. [para(14(a,1),98(a,1,2))]. given #98 (F,wt=10): 147 x ^ ((x v y) ' ^ z) = 0. [para(91(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #99 (T,wt=10): 149 x ^ (y ^ (z ^ x ')) = 0. [para(16(a,1),101(a,1,2))]. given #100 (T,wt=10): 151 x ^ (y ^ (x v z) ') = 0. [para(101(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #101 (A,wt=23): 51 x ^ (y v (z ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (u v x))). [para(13(a,1),22(a,2,2,2,2))]. given #102 (F,wt=10): 156 x ^ (y v (x v z)) ' = 0. [para(25(a,1),142(a,1,2,1))]. given #103 (F,wt=10): 169 x ^ (y v (z v x)) ' = 0. [para(14(a,1),152(a,1,2,1))]. given #104 (T,wt=10): 170 x ^ ((y v x) ' ^ z) = 0. [para(152(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #105 (T,wt=10): 174 x ^ (y ^ (z v x) ') = 0. [para(152(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #106 (A,wt=17): 60 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)). [para(18(a,1),22(a,1,2,2,2,2)),demod(36(5))]. given #107 (F,wt=10): 176 c1 ^ (x ^ (c2 ' ^ y)) = 0. [para(158(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #108 (F,wt=10): 177 c1 ^ (x ^ (y ^ c2 ')) = 0. [para(16(a,1),160(a,1,2))]. given #109 (T,wt=10): 196 x v ((x ^ y) ' v z) = 1. [para(88(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #110 (T,wt=10): 197 x v (y v (x ^ z) ') = 1. [para(98(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #111 (A,wt=21): 61 x ^ (y v (x ' ^ (y v z))) = x ^ (y v (x ' ^ (x v z))). [para(20(a,1),22(a,1,2,2,2,2,2)),demod(42(3))]. given #112 (F,wt=10): 206 c1 ^ ((c2 v x) ' ^ y) = 0. [para(186(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #113 (F,wt=10): 208 c1 ^ (x v (c2 v y)) ' = 0. [para(25(a,1),186(a,1,2,1))]. given #114 (T,wt=10): 209 c1 ^ (x ^ (c2 v y) ') = 0. [para(186(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #115 (T,wt=10): 210 c1 ^ (x v (y v c2)) ' = 0. [para(14(a,1),188(a,1,2,1))]. given #116 (A,wt=40): 62 x v (y v (z ^ (y v (u v (x ^ z))))) != 1 | x ^ (y v (z ^ (x v u))) != 0 | x ' = y v (z ^ (y v (u v (x ^ z)))). [para(22(a,1),21(b,1))]. given #117 (F,wt=10): 211 c1 ^ ((x v c2) ' ^ y) = 0. [para(188(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #118 (F,wt=10): 213 c1 ^ (x ^ (y v c2) ') = 0. [para(188(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #119 (T,wt=10): 227 x v (y ^ (x ^ z)) ' = 1. [para(26(a,1),191(a,1,2,1))]. given #120 (T,wt=10): 228 x v ((y ^ x) ' v z) = 1. [para(224(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #121 (A,wt=32): 63 x v (y v (z ^ (x v u))) != 1 | x ^ (y v (z ^ (u v x))) != 0 | x ' = y v (z ^ (x v u)). [para(22(a,2),21(b,1)),demod(51(12))]. given #122 (F,wt=10): 230 x v (y ^ (z ^ x)) ' = 1. [para(16(a,1),224(a,1,2,1))]. given #123 (F,wt=10): 233 x v (y v (z ^ x) ') = 1. [para(224(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #124 (T,wt=10): 237 (c2 ^ x) v (c1 ^ x) ' = 1. [para(66(a,1),224(a,1,2,1))]. given #125 (T,wt=10): 241 c2 v (x v (c1 ' v y)) = 1. [para(238(a,1),14(a,1,1)),demod(87(2),14(6)),flip(a)]. given #126 (A,wt=49): 64 x ^ (y v ((z v (u ^ (z v (v v (x ^ u))))) ^ (y v (w v (x ^ (z v (u ^ (x v v)))))))) = x ^ (y v ((z v (u ^ (z v (v v (x ^ u))))) ^ (x v w))). [para(22(a,1),22(a,1,2,2,2,2,2))]. given #127 (F,wt=10): 242 c2 v (x v (y v c1 ')) = 1. [para(14(a,1),238(a,1,2))]. given #128 (F,wt=10): 268 x v (y v (y v x) ') = 1. [para(13(a,1),38(a,1,2,2,1))]. given #129 (T,wt=10): 274 c2 v ((x ^ c1) ' v y) = 1. [para(258(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #130 (T,wt=10): 276 c2 v (x ^ (y ^ c1)) ' = 1. [para(16(a,1),258(a,1,2,1))]. given #131 (A,wt=41): 65 x ^ (y v ((z v (u ^ (x v v))) ^ (y v (w v (x ^ (z v (u ^ (v v x)))))))) = x ^ (y v ((z v (u ^ (x v v))) ^ (x v w))). [para(22(a,2),22(a,1,2,2,2,2,2)),demod(51(9))]. given #132 (F,wt=10): 278 c2 v (x v (y ^ c1) ') = 1. [para(258(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #133 (F,wt=10): 279 c2 v ((c1 ^ x) ' v y) = 1. [para(275(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #134 (T,wt=10): 281 c2 v (x v (c1 ^ y) ') = 1. [para(275(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #135 (T,wt=10): 282 c2 v (x ^ (c1 ^ y)) ' = 1. [para(26(a,1),275(a,1,2,1))]. given #136 (A,wt=14): 73 1 != x | x ^ y != 0 | x ' = x ^ y. [back_demod(48),demod(69(4))]. given #137 (F,wt=7): 1779 c1 != 1 | c1 ' = 0. [para(157(a,1),73(b,1)),demod(157(12)),flip(a),xx(b)]. given #138 (F,wt=7): 1781 x ' != 1 | 0 = x. [para(336(a,1),73(b,1)),demod(312(8),336(9)),flip(a),flip(c),xx(b)]. given #139 (T,wt=10): 288 x ^ (y ^ (y ^ x) ') = 0. [para(15(a,1),41(a,1,2,2,1))]. given #140 (T,wt=10): 294 c1 ^ (x ^ (c2 ^ x) ') = 0. [para(41(a,1),66(a,1,2)),demod(15(3),90(3)),flip(a)]. given #141 (A,wt=14): 77 x v y != 1 | 0 != x | x ' = x v y. [back_demod(47),demod(74(2))]. given #142 (F,wt=10): 1785 (c1 ^ (c1 ' v c2 ')) ' != 1. [ur(1781,b,131,a(flip))]. given #143 (F,wt=7): 1821 c2 != 0 | c2 ' = 1. [para(232(a,1),77(a,1)),demod(232(12)),flip(b),xx(a)]. given #144 (T,wt=7): 1823 x ' != 0 | 1 = x. [para(335(a,1),77(a,1)),demod(312(8),335(9)),flip(b),flip(c),xx(a)]. given #145 (T,wt=10): 316 c2 != 1 | c1 != 0 | c2 ' = c1. [para(113(a,1),43(a,1)),demod(15(6),23(6))]. given #146 (A,wt=11): 81 x v (y v (x ^ z)) = y v x. [para(18(a,1),25(a,1,2)),flip(a)]. given #147 (F,wt=10): 337 x ' v (y v (x v z)) = 1. [para(335(a,1),14(a,1,1)),demod(87(2),14(4)),flip(a)]. given #148 (F,wt=8): 1847 c1 ' v (x v c2) = 1. [para(113(a,1),337(a,1,2,2))]. given #149 (T,wt=7): 1864 c1 ' != 0 | c1 = 1. [para(1847(a,1),77(a,1)),demod(312(10),1847(13)),flip(b),xx(a)]. given #150 (T,wt=10): 338 x ' v (y v (z v x)) = 1. [para(14(a,1),335(a,1,2))]. given #151 (A,wt=20): 83 x v (y v z) != 1 | y ^ (x v z) != 0 | y ' = x v z. [para(25(a,1),21(a,1))]. given #152 (F,wt=10): 343 x ' ^ (y ^ (x ^ z)) = 0. [para(336(a,1),16(a,1,1)),demod(90(2),16(4)),flip(a)]. given #153 (F,wt=10): 344 x ' ^ (y ^ (z ^ x)) = 0. [para(16(a,1),336(a,1,2))]. given #154 (T,wt=8): 1953 c2 ' ^ (x ^ c1) = 0. [para(23(a,1),344(a,1,2,2))]. given #155 (T,wt=7): 1986 c2 ' != 1 | c2 = 0. [para(1953(a,1),73(b,1)),demod(312(10),1953(13)),flip(a),xx(b)]. given #156 (A,wt=11): 92 x ^ (y ^ (x v z)) = y ^ x. [para(17(a,1),26(a,1,2)),flip(a)]. given #157 (F,wt=10): 352 (x ^ c2) v (x ^ c1) ' = 1. [para(96(a,1),224(a,1,2,1))]. given #158 (F,wt=10): 353 x ^ (c1 ^ (x ^ c2) ') = 0. [para(96(a,1),336(a,1,2)),demod(15(6),16(6))]. given #159 (T,wt=10): 432 (x v c1) ^ (x v c2) ' = 0. [para(118(a,1),152(a,1,2,1))]. given #160 (T,wt=10): 436 x v (c2 v (x v c1) ') = 1. [para(118(a,1),335(a,1,2)),demod(13(6),14(6))]. given #161 (A,wt=20): 95 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x ' = y ^ z. [para(26(a,1),21(b,1))]. given #162 (F,wt=10): 550 (x v c1) ^ (c2 v x) ' = 0. [para(429(a,1),152(a,1,2,1))]. given #163 (F,wt=10): 552 c2 v (x v (x v c1) ') = 1. [para(429(a,1),335(a,1,2)),demod(13(6),14(6))]. given #164 (T,wt=10): 1328 (x ^ c2) v (c1 ^ x) ' = 1. [para(15(a,1),237(a,1,1))]. given #165 (T,wt=10): 1329 (c2 ^ x) v (x ^ c1) ' = 1. [para(15(a,1),237(a,1,2,1))]. given #166 (A,wt=11): 104 x ^ ((y v x) ^ z) = x ^ z. [para(27(a,1),16(a,1,1)),flip(a)]. given #167 (F,wt=10): 1330 (c2 ^ (c1 v x)) v c1 ' = 1. [para(17(a,1),237(a,1,2,1))]. given #168 (F,wt=10): 1334 (c2 ^ (x v c1)) v c1 ' = 1. [para(27(a,1),237(a,1,2,1))]. given #169 (T,wt=10): 1777 c1 != 1 | c1 != 0 | c1 ' = c1. [para(23(a,1),73(b,1)),demod(23(11)),flip(a)]. given #170 (T,wt=10): 1793 c1 ^ (x ^ (x ^ c2) ') = 0. [para(288(a,1),66(a,1,2)),demod(15(3),90(3)),flip(a)]. given #171 (A,wt=13): 105 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(27(a,1),16(a,1)),flip(a)]. given #172 (F,wt=10): 1804 x ^ (c1 ^ (c2 ^ x) ') = 0. [para(294(a,1),26(a,1)),flip(a)]. given #173 (F,wt=10): 1806 c1 ^ (c2 ^ (c1 v x)) ' = 0. [para(294(a,1),29(a,1)),flip(a)]. given #174 (T,wt=10): 1822 c2 != 1 | c2 != 0 | c2 ' = c2. [para(255(a,1),77(a,1)),demod(255(12)),flip(b)]. given #175 (T,wt=10): 1851 c1 ' v (x v (c2 v y)) = 1. [para(117(a,1),337(a,1,2,2))]. given #176 (A,wt=14): 106 x v y != 1 | 0 != y | y ' = x v y. [para(27(a,1),21(b,1)),demod(76(2)),flip(b)]. given #177 (F,wt=10): 1853 c1 ' v (x v (y v c2)) = 1. [para(119(a,1),337(a,1,2,2))]. given #178 (F,wt=10): 1866 (x ^ y) ' v (z v x) = 1. [para(18(a,1),338(a,1,2,2))]. given #179 (T,wt=10): 1869 (x ^ y) ' v (z v y) = 1. [para(33(a,1),338(a,1,2,2))]. given #180 (T,wt=10): 1873 (x ^ c1) ' v (y v c2) = 1. [para(255(a,1),338(a,1,2,2))]. given #181 (A,wt=13): 107 (x v y) ^ (x v (z v y)) = x v y. [para(25(a,1),27(a,1,2))]. given #182 (F,wt=10): 1874 (c1 ^ x) ' v (y v c2) = 1. [para(261(a,1),338(a,1,2,2))]. given #183 (F,wt=10): 1942 c2 ' ^ (x ^ (y ^ c1)) = 0. [para(67(a,1),343(a,1,2,2))]. given #184 (T,wt=10): 1951 (x v y) ' ^ (z ^ x) = 0. [para(17(a,1),344(a,1,2,2))]. given #185 (T,wt=10): 1955 (x v y) ' ^ (z ^ y) = 0. [para(27(a,1),344(a,1,2,2))]. given #186 (A,wt=11): 108 x ^ (y ^ (z v x)) = y ^ x. [para(27(a,1),26(a,1,2)),flip(a)]. given #187 (F,wt=10): 1960 (c2 v x) ' ^ (y ^ c1) = 0. [para(180(a,1),344(a,1,2,2))]. given #188 (F,wt=10): 1961 (x v c2) ' ^ (y ^ c1) = 0. [para(183(a,1),344(a,1,2,2))]. given #189 (T,wt=10): 1979 c2 ' ^ (x ^ (c1 ^ y)) = 0. [para(1953(a,1),16(a,1,1)),demod(90(2),16(6)),flip(a)]. given #190 (T,wt=10): 2029 (c1 v x) ^ (x v c2) ' = 0. [para(13(a,1),432(a,1,1))]. given #191 (A,wt=11): 109 x v ((y ^ x) v z) = x v z. [para(33(a,1),14(a,1,1)),flip(a)]. given #192 (F,wt=10): 2040 x v (c2 v (c1 v x) ') = 1. [para(13(a,1),436(a,1,2,2,1))]. given #193 (F,wt=10): 2118 (c1 v x) ^ (c2 v x) ' = 0. [para(13(a,1),550(a,1,1))]. given #194 (T,wt=10): 2119 (c1 v (c2 ^ x)) ^ c2 ' = 0. [para(18(a,1),550(a,1,2,1)),demod(13(4))]. given #195 (T,wt=10): 2122 (c1 v (x ^ c2)) ^ c2 ' = 0. [para(33(a,1),550(a,1,2,1)),demod(13(4))]. given #196 (A,wt=13): 110 x v (y v (z ^ (x v y))) = x v y. [para(33(a,1),14(a,1)),flip(a)]. given #197 (F,wt=10): 2134 c2 v (x v (c1 v x) ') = 1. [para(13(a,1),552(a,1,2,2,1))]. given #198 (F,wt=10): 2137 c2 v (c1 v (c2 ^ x)) ' = 1. [para(552(a,1),31(a,1)),demod(13(6)),flip(a)]. given #199 (T,wt=10): 2196 c1 ^ (c2 ^ (x v c1)) ' = 0. [para(104(a,1),294(a,1))]. given #200 (T,wt=10): 2204 c1 ' v (c2 ^ (c1 v x)) = 1. [para(1330(a,1),13(a,1)),flip(a)]. given #201 (A,wt=14): 112 1 != x | y ^ x != 0 | x ' = y ^ x. [para(33(a,1),21(a,1)),demod(71(4)),flip(a)]. given #202 (F,wt=7): 2720 c1 != 0 | c1 ' = 1. [para(2204(a,1),62(b,1,2)),demod(23(9),335(9),15(6),78(6),13(5),232(5),13(3),87(3),15(6),78(6),23(16),335(16),15(13),78(13),13(12),232(12)),xx(a)]. given #203 (F,wt=10): 2216 c1 ' v (c2 ^ (x v c1)) = 1. [para(1334(a,1),13(a,1)),flip(a)]. given #204 (T,wt=10): 2579 c2 v (c1 v (x ^ c2)) ' = 1. [para(109(a,1),552(a,1)),demod(13(5))]. given #205 (T,wt=10): 2620 c2 ' ^ (c1 v (c2 ^ x)) = 0. [para(2119(a,1),15(a,1)),flip(a)]. given #206 (A,wt=11): 114 x v (y v (z ^ x)) = y v x. [para(33(a,1),25(a,1,2)),flip(a)]. given #207 (F,wt=10): 2631 c2 ' ^ (c1 v (x ^ c2)) = 0. [para(2122(a,1),15(a,1)),flip(a)]. given #208 (F,wt=11): 129 (x v c1) ^ (x v c2) = x v c1. [para(113(a,1),28(a,1,2,2))]. given #209 (T,wt=11): 159 c1 v c2 ' != 1 | c2 ' = c1 '. [para(157(a,1),21(b,1)),flip(c),xx(b)]. given #210 (T,wt=11): 184 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(66(a,1),33(a,1,2)),demod(13(5))]. given #211 (A,wt=13): 115 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(26(a,1),33(a,1,2))]. given #212 (F,wt=11): 185 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(29(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #213 (F,wt=11): 201 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(180(a,1),26(a,1,2)),flip(a)]. given #214 (T,wt=11): 203 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(183(a,1),16(a,1,1)),flip(a)]. given #215 (T,wt=11): 205 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(183(a,1),26(a,1,2)),flip(a)]. given #216 (A,wt=13): 120 (x v y) ^ (y v (x v z)) = y v x. [para(13(a,1),28(a,1,1))]. given #217 (F,wt=11): 240 c2 ^ c1 ' != 0 | c2 ' = c1 '. [para(232(a,1),21(a,1)),xx(a)]. given #218 (F,wt=11): 257 c2 v ((x ^ c1) v y) = c2 v y. [para(67(a,1),31(a,1,2,1))]. given #219 (T,wt=11): 260 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(67(a,1),34(a,1,2))]. given #220 (T,wt=11): 263 c2 v (x v (y ^ c1)) = x v c2. [para(255(a,1),25(a,1,2)),flip(a)]. given #221 (A,wt=13): 121 (x v y) ^ (y v (z v x)) = x v y. [para(13(a,1),28(a,1,2)),demod(14(3))]. given #222 (F,wt=11): 264 c2 v ((c1 ^ x) v y) = c2 v y. [para(261(a,1),14(a,1,1)),flip(a)]. given #223 (F,wt=11): 266 c2 v (x v (c1 ^ y)) = x v c2. [para(261(a,1),25(a,1,2)),flip(a)]. given #224 (T,wt=11): 286 (x v y) ^ (z ^ x) = z ^ x. [para(71(a,1),29(a,2)),demod(285(4))]. given #225 (T,wt=11): 287 (x ^ y) v (y ^ x) = x ^ y. [para(71(a,1),34(a,1,2))]. given #226 (A,wt=19): 122 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(14(a,1),28(a,1,1)),demod(14(5),14(8))]. given #227 (F,wt=10): 3304 (x ^ y) v (y ^ x) ' = 1. [para(287(a,1),335(a,1,2)),demod(13(4))]. given #228 (F,wt=11): 298 (x v y) ^ (y v x) = x v y. [para(76(a,1),28(a,1,2))]. given #229 (T,wt=10): 3378 (x v y) ^ (y v x) ' = 0. [para(298(a,1),336(a,1,2)),demod(15(4))]. given #230 (T,wt=11): 299 (x ^ y) v (z v x) = z v x. [para(76(a,1),31(a,2)),demod(297(4))]. given #231 (A,wt=17): 123 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(28(a,1),16(a,1,1)),flip(a)]. given #232 (F,wt=11): 301 x ^ (y v (z v (x v u))) = x. [para(14(a,1),80(a,1,2))]. given #233 (F,wt=11): 305 x v (y ^ (z ^ (x ^ u))) = x. [para(16(a,1),93(a,1,2))]. given #234 (T,wt=11): 351 (x ^ c1) v (x ^ c2) = x ^ c2. [para(96(a,1),33(a,1,2)),demod(13(5))]. given #235 (T,wt=11): 360 x v y != 0 | (x v y) ' = 1. [para(39(a,1),44(b,1)),demod(97(2),97(2)),xx(a)]. given #236 (A,wt=19): 125 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(25(a,1),28(a,1,1)),demod(14(4))]. given #237 (F,wt=11): 364 x v y != 1 | (x v y) ' = 0. [para(42(a,1),44(a,1,2)),demod(15(6),90(6)),xx(b)]. given #238 (F,wt=7): 3612 c2 != 1 | c2 ' = 0. [para(113(a,1),364(a,1)),demod(113(6))]. given #239 (T,wt=11): 401 x ^ (y v (z v (u v x))) = x. [para(14(a,1),103(a,1,2,2))]. given #240 (T,wt=11): 413 x v (y ^ (z ^ (u ^ x))) = x. [para(16(a,1),111(a,1,2,2))]. given #241 (A,wt=15): 126 (x v y) ^ (x v (z v (y v u))) = x v y. [para(25(a,1),28(a,1,2,2))]. given #242 (F,wt=11): 468 (c1 v x) ^ (x v c2) = c1 v x. [para(119(a,1),28(a,1,2))]. given #243 (F,wt=11): 471 c1 ^ (x v (y v (c2 v z))) = c1. [para(14(a,1),200(a,1,2))]. given #244 (T,wt=11): 476 c1 ^ (x v (y v (z v c2))) = c1. [para(14(a,1),202(a,1,2,2))]. given #245 (T,wt=11): 482 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(16(a,1),262(a,1,2,2))]. given #246 (A,wt=17): 127 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(28(a,1),26(a,1,2)),flip(a)]. given #247 (F,wt=11): 492 x ^ y != 0 | (x ^ y) ' = 1. [para(39(a,1),46(b,1,2)),demod(13(3),87(3)),xx(a)]. given #248 (F,wt=11): 494 x ^ y != 1 | (x ^ y) ' = 0. [para(42(a,1),46(a,1)),demod(100(5),100(5)),xx(b)]. given #249 (T,wt=11): 542 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(16(a,1),267(a,1,2))]. given #250 (T,wt=11): 549 (x v c1) ^ (c2 v x) = x v c1. [para(429(a,1),27(a,1,2))]. given #251 (A,wt=22): 130 x v (y v z) != 1 | x v y != 0 | (x v y) ' = x v (y v z). [back_demod(124),demod(128(4))]. given #252 (F,wt=11): 2176 (x v y) ^ (z ^ y) = z ^ y. [para(71(a,1),104(a,2)),demod(285(4))]. given #253 (F,wt=11): 2298 (x ^ y) ' != 0 | x ^ y = 1. [para(191(a,1),106(a,1)),demod(312(10),191(11)),flip(b),xx(a)]. given #254 (T,wt=11): 2383 (c1 v x) ^ (c2 v x) = c1 v x. [para(117(a,1),107(a,1,2))]. given #255 (T,wt=11): 2439 (x v y) ' != 1 | x v y = 0. [para(1951(a,1),73(b,1)),demod(312(10),1951(12)),flip(a),xx(b)]. given #256 (A,wt=12): 132 x v (y v ((x v y) ' v z)) = 1. [para(88(a,1),14(a,1)),flip(a)]. given #257 (F,wt=11): 2549 (x ^ y) v (z v y) = z v y. [para(76(a,1),109(a,2)),demod(297(4))]. given #258 (F,wt=11): 2848 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(15(a,1),184(a,1,1))]. given #259 (T,wt=11): 2849 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(15(a,1),184(a,1,2))]. given #260 (T,wt=11): 2933 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(71(a,1),185(a,2)),demod(285(7))]. given #261 (A,wt=15): 133 x ^ (x ' v y) != 0 | x ' v y = x '. [para(88(a,1),21(a,1)),flip(c),xx(a)]. given #262 (F,wt=11): 2986 (x v c2) ^ (y ^ c1) = y ^ c1. [para(71(a,1),203(a,2)),demod(285(7))]. given #263 (F,wt=11): 3070 (x ^ c1) v (y v c2) = y v c2. [para(76(a,1),257(a,2)),demod(297(7))]. given #264 (T,wt=11): 3218 (c1 ^ x) v (y v c2) = y v c2. [para(76(a,1),264(a,2)),demod(297(7))]. given #265 (T,wt=11): 3536 x v y != 0 | (y v x) ' = 1. [para(13(a,1),360(a,1))]. given #266 (A,wt=12): 135 x ^ (y ^ ((x ^ y) ' ^ z)) = 0. [para(91(a,1),16(a,1)),flip(a)]. given #267 (F,wt=11): 3610 x v y != 1 | (y v x) ' = 0. [para(13(a,1),364(a,1))]. given #268 (F,wt=11): 3733 (x v c2) ^ (c1 v x) = c1 v x. [para(468(a,1),15(a,1)),flip(a)]. given #269 (T,wt=11): 3829 x ^ y != 0 | (y ^ x) ' = 1. [para(15(a,1),492(a,1))]. given #270 (T,wt=11): 3833 x ^ y != 1 | (y ^ x) ' = 0. [para(15(a,1),494(a,1))]. given #271 (A,wt=15): 136 x v (x ' ^ y) != 1 | x ' ^ y = x '. [para(91(a,1),21(b,1)),flip(c),xx(b)]. given #272 (F,wt=11): 3851 (c2 v x) ^ (x v c1) = x v c1. [para(549(a,1),15(a,1)),flip(a)]. given #273 (F,wt=11): 3932 (x ^ y) ' != 0 | y ^ x = 1. [para(15(a,1),2298(a,1,1))]. given #274 (T,wt=11): 3934 (x v y) ' != 0 | x v y = 1. [para(28(a,1),2298(a,1,1)),demod(28(8))]. given #275 (T,wt=7): 4189 c2 ' != 0 | c2 = 1. [para(113(a,1),3934(a,1,1)),demod(113(7))]. given #276 (A,wt=12): 138 x v (y v (z v (x v y) ')) = 1. [para(98(a,1),14(a,1)),flip(a)]. given #277 (F,wt=11): 3954 (x v y) ' != 1 | y v x = 0. [para(13(a,1),2439(a,1,1))]. given #278 (F,wt=11): 3956 (x ^ y) ' != 1 | x ^ y = 0. [para(34(a,1),2439(a,1,1)),demod(34(8))]. given #279 (T,wt=7): 4210 c1 ' != 1 | c1 = 0. [para(23(a,1),3956(a,1,1)),demod(23(7))]. given #280 (T,wt=11): 4042 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(2849(a,1),13(a,1)),flip(a)]. given #281 (A,wt=15): 140 x ^ (y v x ') != 0 | y v x ' = x '. [para(98(a,1),21(a,1)),flip(c),xx(a)]. given #282 (F,wt=11): 4187 (x v y) ' != 0 | y v x = 1. [para(298(a,1),3932(a,1,1)),demod(298(7))]. given #283 (F,wt=11): 4209 (x ^ y) ' != 1 | y ^ x = 0. [para(287(a,1),3954(a,1,1)),demod(287(7))]. given #284 (T,wt=12): 148 x ^ (y ^ (z ^ (x ^ y) ')) = 0. [para(101(a,1),16(a,1)),flip(a)]. given #285 (T,wt=12): 153 (x v y) ^ (x v (y v z)) ' = 0. [para(14(a,1),142(a,1,2,1))]. given #286 (A,wt=17): 141 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(29(a,1),16(a,1)),demod(16(2)),flip(a)]. given #287 (F,wt=12): 154 x ^ (y ^ ((x ^ y) v z) ') = 0. [para(142(a,1),16(a,1)),flip(a)]. given #288 (F,wt=12): 171 x ^ (y ^ (z v (x ^ y)) ') = 0. [para(152(a,1),16(a,1)),flip(a)]. given #289 (T,wt=12): 173 (x v y) ^ (x v (z v y)) ' = 0. [para(25(a,1),152(a,1,2,1))]. given #290 (T,wt=12): 198 ((x ^ y) v z) ^ (x v z) ' = 0. [para(31(a,1),152(a,1,2,1))]. given #291 (A,wt=22): 143 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x ' = (x v y) ^ z. [para(29(a,1),21(b,1))]. given #292 (F,wt=12): 223 x v (y v ((x v y) ^ z) ') = 1. [para(191(a,1),14(a,1)),flip(a)]. given #293 (F,wt=12): 225 (x ^ y) v (x ^ (y ^ z)) ' = 1. [para(16(a,1),191(a,1,2,1))]. given #294 (T,wt=12): 229 x v (y v (z ^ (x v y)) ') = 1. [para(224(a,1),14(a,1)),flip(a)]. given #295 (T,wt=12): 234 (x ^ y) v (x ^ (z ^ y)) ' = 1. [para(26(a,1),224(a,1,2,1))]. given #296 (A,wt=13): 144 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(25(a,1),29(a,1,2,1))]. given #297 (F,wt=12): 235 ((x v y) ^ z) v (x ^ z) ' = 1. [para(29(a,1),224(a,1,2,1))]. given #298 (F,wt=12): 271 x v (y v (z v (x v z) ')) = 1. [para(38(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #299 (T,wt=12): 273 x v (y v ((x ^ z) v y) ') = 1. [para(38(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #300 (T,wt=12): 291 x ^ (y ^ (z ^ (x ^ z) ')) = 0. [para(41(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #301 (A,wt=15): 145 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(29(a,1),26(a,1,2)),flip(a)]. given #302 (F,wt=12): 293 x ^ (y ^ ((x v z) ^ y) ') = 0. [para(41(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #303 (F,wt=12): 340 x v ((x v y) ' v (z v y)) = 1. [para(25(a,1),335(a,1,2)),demod(25(5))]. given #304 (T,wt=12): 346 x ^ ((x ^ y) ' ^ (z ^ y)) = 0. [para(26(a,1),336(a,1,2)),demod(26(5))]. given #305 (T,wt=12): 613 x v (y v (z v (x ' v u))) = 1. [para(14(a,1),134(a,1,2))]. given #306 (A,wt=15): 146 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(29(a,1),33(a,1,2)),demod(13(4))]. given #307 (F,wt=12): 615 x v (y v ((x ^ z) ' v u)) = 1. [para(134(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #308 (F,wt=12): 622 x ^ (y ^ (z ^ (x ' ^ u))) = 0. [para(16(a,1),137(a,1,2))]. given #309 (T,wt=12): 624 x ^ (y ^ ((x v z) ' ^ u)) = 0. [para(137(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #310 (T,wt=12): 741 x v (y v (z v (u v x '))) = 1. [para(14(a,1),139(a,1,2,2))]. given #311 (A,wt=15): 150 x v (y ^ x ') != 1 | y ^ x ' = x '. [para(101(a,1),21(b,1)),flip(c),xx(b)]. given #312 (F,wt=12): 743 x v (y v (z v (x ^ u) ')) = 1. [para(139(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #313 (F,wt=12): 752 x ^ ((y v (x v z)) ' ^ u) = 0. [para(25(a,1),147(a,1,2,1,1))]. given #314 (T,wt=12): 758 x ^ (y ^ (z ^ (u ^ x '))) = 0. [para(16(a,1),149(a,1,2,2))]. given #315 (T,wt=12): 760 x ^ (y ^ (z ^ (x v u) ')) = 0. [para(149(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #316 (A,wt=15): 155 x v (x v y) ' != 1 | (x v y) ' = x '. [para(142(a,1),21(b,1)),flip(c),xx(b)]. given #317 (F,wt=12): 769 x ^ (y ^ (z v (x v u)) ') = 0. [para(25(a,1),151(a,1,2,2,1))]. given #318 (F,wt=12): 833 x ^ (y v (z v (x v u))) ' = 0. [para(14(a,1),156(a,1,2,1))]. given #319 (T,wt=12): 841 x ^ (y v (z v (u v x))) ' = 0. [para(14(a,1),169(a,1,2,1,2))]. given #320 (T,wt=12): 842 x ^ ((y v (z v x)) ' ^ u) = 0. [para(169(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #321 (A,wt=13): 161 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(15(a,1),30(a,1,2,2,1))]. given #322 (F,wt=12): 846 x ^ (y ^ (z v (u v x)) ') = 0. [para(169(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #323 (F,wt=12): 853 (x v c1) ^ (y v (c2 v x)) ' = 0. [para(429(a,1),169(a,1,2,1,2))]. given #324 (T,wt=12): 859 x ^ (y ^ ((z v x) ' ^ u)) = 0. [para(170(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #325 (T,wt=12): 865 (x v c1) ^ ((c2 v x) ' ^ y) = 0. [para(429(a,1),170(a,1,2,1,1))]. given #326 (A,wt=19): 162 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(30(a,1),16(a,1)),demod(16(2),16(4)),flip(a)]. given #327 (F,wt=12): 868 x ^ (y ^ (z ^ (u v x) ')) = 0. [para(16(a,1),174(a,1,2))]. given #328 (F,wt=12): 877 (x v c1) ^ (y ^ (c2 v x) ') = 0. [para(429(a,1),174(a,1,2,2,1))]. given #329 (T,wt=12): 917 c1 ^ (x ^ (y ^ (c2 ' ^ z))) = 0. [para(16(a,1),176(a,1,2))]. given #330 (T,wt=12): 924 c1 ^ (x ^ (y ^ (z ^ c2 '))) = 0. [para(16(a,1),177(a,1,2,2))]. given #331 (A,wt=26): 163 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 #332 (F,wt=12): 934 x v ((y ^ (x ^ z)) ' v u) = 1. [para(26(a,1),196(a,1,2,1,1))]. given #333 (F,wt=12): 943 x v (y v (z ^ (x ^ u)) ') = 1. [para(26(a,1),197(a,1,2,2,1))]. given #334 (T,wt=12): 1061 c1 ^ ((x v (c2 v y)) ' ^ z) = 0. [para(25(a,1),206(a,1,2,1,1))]. given #335 (T,wt=12): 1062 c1 ^ (x ^ ((c2 v y) ' ^ z)) = 0. [para(206(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #336 (A,wt=15): 164 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(25(a,1),30(a,1,2,2))]. given #337 (F,wt=12): 1067 c1 ^ (x v (y v (c2 v z))) ' = 0. [para(14(a,1),208(a,1,2,1))]. given #338 (F,wt=12): 1069 c1 ^ (x ^ (y v (c2 v z)) ') = 0. [para(208(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #339 (T,wt=12): 1074 c1 ^ (x ^ (y ^ (c2 v z) ')) = 0. [para(16(a,1),209(a,1,2))]. given #340 (T,wt=12): 1081 c1 ^ (x v (y v (z v c2))) ' = 0. [para(14(a,1),210(a,1,2,1,2))]. given #341 (A,wt=17): 165 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(30(a,1),26(a,1,2)),flip(a)]. given #342 (F,wt=12): 1082 c1 ^ ((x v (y v c2)) ' ^ z) = 0. [para(210(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #343 (F,wt=12): 1084 c1 ^ (x ^ (y v (z v c2)) ') = 0. [para(210(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #344 (T,wt=12): 1204 c1 ^ (x ^ ((y v c2) ' ^ z)) = 0. [para(211(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #345 (T,wt=12): 1210 c1 ^ (x ^ (y ^ (z v c2) ')) = 0. [para(16(a,1),213(a,1,2))]. given #346 (A,wt=19): 166 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(26(a,1),30(a,1,2,2,1)),demod(16(5))]. given #347 (F,wt=12): 1220 x v (y ^ (z ^ (x ^ u))) ' = 1. [para(16(a,1),227(a,1,2,1))]. given #348 (F,wt=12): 1230 x v ((y ^ (z ^ x)) ' v u) = 1. [para(16(a,1),228(a,1,2,1,1))]. given #349 (T,wt=12): 1232 x v (y v ((z ^ x) ' v u)) = 1. [para(228(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #350 (T,wt=12): 1236 (c2 ^ x) v ((c1 ^ x) ' v y) = 1. [para(66(a,1),228(a,1,2,1,1))]. given #351 (A,wt=19): 167 (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 #352 (F,wt=12): 1238 (x ^ c2) v ((x ^ c1) ' v y) = 1. [para(96(a,1),228(a,1,2,1,1))]. given #353 (F,wt=12): 1286 x v (y ^ (z ^ (u ^ x))) ' = 1. [para(16(a,1),230(a,1,2,1,2))]. given #354 (T,wt=12): 1288 x v (y v (z ^ (u ^ x)) ') = 1. [para(230(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #355 (T,wt=12): 1293 (c2 ^ x) v (y ^ (c1 ^ x)) ' = 1. [para(66(a,1),230(a,1,2,1,2))]. given #356 (A,wt=15): 168 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(30(a,1),29(a,1,2)),demod(29(3)),flip(a)]. given #357 (F,wt=11): 6559 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(168(a,1),66(a,1)),demod(23(3),15(6)),flip(a)]. given #358 (F,wt=11): 6638 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(13(a,1),6559(a,1,2,1,2))]. given #359 (T,wt=11): 6639 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(13(a,1),6559(a,1,2))]. given #360 (T,wt=11): 6682 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(13(a,1),6638(a,1,2))]. given #361 (A,wt=15): 172 x v (y v x) ' != 1 | (y v x) ' = x '. [para(152(a,1),21(b,1)),flip(c),xx(b)]. given #362 (F,wt=12): 1295 (x ^ c2) v (y ^ (x ^ c1)) ' = 1. [para(96(a,1),230(a,1,2,1,2))]. given #363 (F,wt=12): 1307 x v (y v (z v (u ^ x) ')) = 1. [para(14(a,1),233(a,1,2))]. given #364 (T,wt=12): 1312 (c2 ^ x) v (y v (c1 ^ x) ') = 1. [para(66(a,1),233(a,1,2,2,1))]. given #365 (T,wt=12): 1314 (x ^ c2) v (y v (x ^ c1) ') = 1. [para(96(a,1),233(a,1,2,2,1))]. given #366 (A,wt=15): 175 c1 v (c2 ' ^ x) != 1 | c2 ' ^ x = c1 '. [para(158(a,1),21(b,1)),flip(c),xx(b)]. given #367 (F,wt=12): 1337 (c2 ^ (x v (c1 v y))) v c1 ' = 1. [para(80(a,1),237(a,1,2,1))]. given #368 (F,wt=12): 1340 (c2 ^ (x v (y v c1))) v c1 ' = 1. [para(103(a,1),237(a,1,2,1))]. given #369 (T,wt=12): 1352 c2 v (x v (y v (c1 ' v z))) = 1. [para(14(a,1),241(a,1,2))]. given #370 (T,wt=12): 1565 c2 v (x v (y v (z v c1 '))) = 1. [para(14(a,1),242(a,1,2,2))]. given #371 (A,wt=15): 178 c1 v (x ^ c2 ') != 1 | x ^ c2 ' = c1 '. [para(160(a,1),21(b,1)),flip(c),xx(b)]. given #372 (F,wt=12): 1575 x v (y v ((y v x) ' v z)) = 1. [para(268(a,1),14(a,1,1)),demod(87(2),14(5)),flip(a)]. given #373 (F,wt=12): 1579 x v (y v (z v (z v x) ')) = 1. [para(268(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #374 (T,wt=12): 1581 x v (y v (y v (x ^ z)) ') = 1. [para(268(a,1),31(a,1,2)),demod(97(2)),flip(a)]. given #375 (T,wt=12): 1590 c2 v ((x ^ (y ^ c1)) ' v z) = 1. [para(16(a,1),274(a,1,2,1,1))]. given #376 (A,wt=13): 179 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(66(a,1),16(a,2,2)),demod(26(5),16(4))]. given #377 (F,wt=12): 1592 c2 v (x v ((y ^ c1) ' v z)) = 1. [para(274(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #378 (F,wt=12): 1603 c2 v (x ^ (y ^ (z ^ c1))) ' = 1. [para(16(a,1),276(a,1,2,1,2))]. given #379 (T,wt=12): 1605 c2 v (x v (y ^ (z ^ c1)) ') = 1. [para(276(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #380 (T,wt=12): 1734 c2 v (x v (y v (z ^ c1) ')) = 1. [para(14(a,1),278(a,1,2))]. given #381 (A,wt=18): 181 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1 ' = c2 ^ x. [para(66(a,1),21(b,1))]. given #382 (F,wt=12): 1745 c2 v (x v ((c1 ^ y) ' v z)) = 1. [para(279(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #383 (F,wt=12): 1746 c2 v ((x ^ (c1 ^ y)) ' v z) = 1. [para(26(a,1),279(a,1,2,1,1))]. given #384 (T,wt=12): 1757 c2 v (x v (y v (c1 ^ z) ')) = 1. [para(14(a,1),281(a,1,2))]. given #385 (T,wt=12): 1759 c2 v (x v (y ^ (c1 ^ z)) ') = 1. [para(26(a,1),281(a,1,2,2,1))]. given #386 (A,wt=13): 182 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(66(a,1),26(a,1,2)),flip(a)]. given #387 (F,wt=12): 1768 c2 v (x ^ (y ^ (c1 ^ z))) ' = 1. [para(16(a,1),282(a,1,2,1))]. given #388 (F,wt=12): 1786 x ^ (y ^ ((y ^ x) ' ^ z)) = 0. [para(288(a,1),16(a,1,1)),demod(90(2),16(5)),flip(a)]. given #389 (T,wt=12): 1790 x ^ (y ^ (z ^ (z ^ x) ')) = 0. [para(288(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #390 (T,wt=12): 1792 x ^ (y ^ (y ^ (x v z)) ') = 0. [para(288(a,1),29(a,1,2)),demod(100(2)),flip(a)]. given #391 (A,wt=13): 187 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(30(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #392 (F,wt=12): 1800 c1 ^ (x ^ ((c2 ^ x) ' ^ y)) = 0. [para(294(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #393 (F,wt=12): 1803 c1 ^ (x ^ (y ^ (c2 ^ y) ')) = 0. [para(294(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #394 (T,wt=12): 1829 (x v (y ^ z)) ^ (x v y) ' = 0. [para(81(a,1),152(a,1,2,1))]. given #395 (T,wt=12): 1831 x v (y v (x v (y ^ z)) ') = 1. [para(81(a,1),335(a,1,2)),demod(13(5),14(5))]. given #396 (A,wt=17): 189 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(31(a,1),14(a,1)),demod(14(2)),flip(a)]. given #397 (F,wt=12): 1845 x ' v (y v (z v (x v u))) = 1. [para(14(a,1),337(a,1,2))]. given #398 (F,wt=12): 1865 x ' v (y v (z v (u v x))) = 1. [para(14(a,1),338(a,1,2,2))]. given #399 (T,wt=12): 1875 (x ^ (y ^ z)) ' v (u v y) = 1. [para(93(a,1),338(a,1,2,2))]. given #400 (T,wt=12): 1879 (x ^ (y ^ z)) ' v (u v z) = 1. [para(111(a,1),338(a,1,2,2))]. given #401 (A,wt=17): 190 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(16(a,1),31(a,1,2,1))]. given #402 (F,wt=12): 1881 (x ^ (y ^ c1)) ' v (z v c2) = 1. [para(262(a,1),338(a,1,2,2))]. given #403 (F,wt=12): 1882 (x ^ (c1 ^ y)) ' v (z v c2) = 1. [para(267(a,1),338(a,1,2,2))]. given #404 (T,wt=12): 1883 (x v c1) ' v (y v (c2 v x)) = 1. [para(429(a,1),338(a,1,2,2))]. given #405 (T,wt=12): 1940 x ' ^ (y ^ (z ^ (x ^ u))) = 0. [para(16(a,1),343(a,1,2))]. given #406 (A,wt=22): 192 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x ' = (x ^ z) v y. [para(31(a,1),21(a,1))]. given #407 (F,wt=12): 1950 x ' ^ (y ^ (z ^ (u ^ x))) = 0. [para(16(a,1),344(a,1,2,2))]. given #408 (F,wt=12): 1959 (c2 ^ x) ' ^ (y ^ (c1 ^ x)) = 0. [para(66(a,1),344(a,1,2,2))]. given #409 (T,wt=12): 1962 (x v (y v z)) ' ^ (u ^ y) = 0. [para(80(a,1),344(a,1,2,2))]. given #410 (T,wt=12): 1964 (x ^ c2) ' ^ (y ^ (x ^ c1)) = 0. [para(96(a,1),344(a,1,2,2))]. given #411 (A,wt=15): 193 x v (y v ((x ^ z) v u)) = y v (x v u). [para(31(a,1),25(a,1,2)),flip(a)]. given #412 (F,wt=12): 1965 (x v (y v z)) ' ^ (u ^ z) = 0. [para(103(a,1),344(a,1,2,2))]. given #413 (F,wt=12): 1967 (x v (c2 v y)) ' ^ (z ^ c1) = 0. [para(200(a,1),344(a,1,2,2))]. given #414 (T,wt=12): 1968 (x v (y v c2)) ' ^ (z ^ c1) = 0. [para(202(a,1),344(a,1,2,2))]. given #415 (T,wt=12): 1990 (x ^ (y v z)) v (x ^ y) ' = 1. [para(92(a,1),224(a,1,2,1))]. given #416 (A,wt=13): 194 x v ((y ^ (x ^ z)) v u) = x v u. [para(26(a,1),31(a,1,2,1))]. given #417 (F,wt=12): 1991 x ^ (y ^ (x ^ (y v z)) ') = 0. [para(92(a,1),336(a,1,2)),demod(15(5),16(5))]. given #418 (F,wt=12): 2015 x ^ (c1 ^ ((x ^ c2) ' ^ y)) = 0. [para(353(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #419 (T,wt=12): 2017 c1 ^ (x ^ (y ^ (y ^ c2) ')) = 0. [para(353(a,1),16(a,2,2)),demod(26(7),16(6),100(9))]. given #420 (T,wt=12): 2020 x ^ (y ^ (c1 ^ (x ^ c2) ')) = 0. [para(353(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #421 (A,wt=15): 195 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(31(a,1),27(a,1,2)),demod(15(4))]. given #422 (F,wt=12): 2021 x ^ (c1 ^ (c2 ^ (x v y)) ') = 0. [para(353(a,1),29(a,1,2)),demod(100(2),15(5)),flip(a)]. given #423 (F,wt=12): 2032 (x v c1) ^ ((x v c2) ' ^ y) = 0. [para(432(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #424 (T,wt=12): 2034 (x v c1) ^ (y ^ (x v c2) ') = 0. [para(432(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #425 (T,wt=12): 2041 x v (c2 v ((x v c1) ' v y)) = 1. [para(436(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #426 (A,wt=14): 199 c2 v x != 1 | c1 != 0 | c1 ' = c2 v x. [para(180(a,1),21(b,1)),demod(117(4))]. given #427 (F,wt=12): 2043 c2 v (x v (y v (y v c1) ')) = 1. [para(436(a,1),14(a,2,2)),demod(25(7),14(6),97(9))]. given #428 (F,wt=12): 2046 x v (y v (c2 v (x v c1) ')) = 1. [para(436(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #429 (T,wt=12): 2047 x v (c2 v (c1 v (x ^ y)) ') = 1. [para(436(a,1),31(a,1,2)),demod(97(2),13(5)),flip(a)]. given #430 (T,wt=12): 2125 (c1 v (x ^ (c2 ^ y))) ^ c2 ' = 0. [para(93(a,1),550(a,1,2,1)),demod(13(5))]. given #431 (A,wt=14): 204 x v c2 != 1 | c1 != 0 | c1 ' = x v c2. [para(183(a,1),21(b,1)),demod(119(4))]. given #432 (F,wt=12): 2126 (c1 v (x ^ (y ^ c2))) ^ c2 ' = 0. [para(111(a,1),550(a,1,2,1)),demod(13(5))]. given #433 (F,wt=12): 2135 c2 v (x v ((x v c1) ' v y)) = 1. [para(552(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #434 (T,wt=12): 2147 (x ^ c2) v ((c1 ^ x) ' v y) = 1. [para(1328(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #435 (T,wt=12): 2149 (x ^ c2) v (y v (c1 ^ x) ') = 1. [para(1328(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #436 (A,wt=15): 207 c1 v (c2 v x) ' != 1 | (c2 v x) ' = c1 '. [para(186(a,1),21(b,1)),flip(c),xx(b)]. given #437 (F,wt=12): 2157 (c2 ^ x) v ((x ^ c1) ' v y) = 1. [para(1329(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #438 (F,wt=12): 2159 (c2 ^ x) v (y v (x ^ c1) ') = 1. [para(1329(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #439 (T,wt=12): 2175 ((x v y) ^ z) v (y ^ z) ' = 1. [para(104(a,1),224(a,1,2,1))]. given #440 (T,wt=12): 2177 x ^ (y ^ ((z v x) ^ y) ') = 0. [para(41(a,1),104(a,1,2)),demod(100(2)),flip(a)]. given #441 (A,wt=15): 212 c1 v (x v c2) ' != 1 | (x v c2) ' = c1 '. [para(188(a,1),21(b,1)),flip(c),xx(b)]. given #442 (F,wt=12): 2195 x ^ (y ^ (y ^ (z v x)) ') = 0. [para(288(a,1),104(a,1,2)),demod(100(2)),flip(a)]. given #443 (F,wt=12): 2199 x ^ (c1 ^ (c2 ^ (y v x)) ') = 0. [para(353(a,1),104(a,1,2)),demod(100(2),15(5)),flip(a)]. given #444 (T,wt=12): 2205 (c2 ^ (c1 v x)) v (c1 ' v y) = 1. [para(1330(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #445 (T,wt=12): 2207 (c2 ^ (c1 v x)) v (y v c1 ') = 1. [para(1330(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #446 (A,wt=13): 214 x v (y v ((y v x) ^ z)) = x v y. [para(13(a,1),32(a,1,2,2,1))]. given #447 (F,wt=12): 2217 (c2 ^ (x v c1)) v (c1 ' v y) = 1. [para(1334(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #448 (F,wt=12): 2219 (c2 ^ (x v c1)) v (y v c1 ') = 1. [para(1334(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #449 (T,wt=12): 2228 c1 ^ (x ^ ((x ^ c2) ' ^ y)) = 0. [para(1793(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #450 (T,wt=12): 2264 x ^ (c1 ^ ((c2 ^ x) ' ^ y)) = 0. [para(1804(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #451 (A,wt=19): 215 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(32(a,1),14(a,1)),demod(14(2),14(4)),flip(a)]. given #452 (F,wt=12): 2265 x ^ (y ^ (c1 ^ (c2 ^ x) ')) = 0. [para(1804(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #453 (F,wt=12): 2273 c1 ^ ((c2 ^ (c1 v x)) ' ^ y) = 0. [para(1806(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #454 (T,wt=12): 2275 c1 ^ (c2 ^ (x v (c1 v y))) ' = 0. [para(25(a,1),1806(a,1,2,1,2))]. given #455 (T,wt=12): 2276 c1 ^ (x ^ (c2 ^ (c1 v y)) ') = 0. [para(1806(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #456 (A,wt=26): 216 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 #457 (F,wt=12): 2283 c1 ' v (x v (y v (c2 v z))) = 1. [para(14(a,1),1851(a,1,2))]. given #458 (F,wt=12): 2302 c1 ' v (x v (y v (z v c2))) = 1. [para(14(a,1),1853(a,1,2,2))]. given #459 (T,wt=12): 2312 (x ^ y) ' v (z v (x v u)) = 1. [para(1866(a,1),14(a,1,1)),demod(87(2),14(5)),flip(a)]. given #460 (T,wt=12): 2313 (x ^ y) ' v (z v (u v x)) = 1. [para(14(a,1),1866(a,1,2))]. given #461 (A,wt=17): 217 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(32(a,1),25(a,1,2)),flip(a)]. given #462 (F,wt=12): 2320 c2 v (x v ((x v c1) ^ y) ') = 1. [para(429(a,1),1866(a,1,2)),demod(13(7),14(7))]. given #463 (F,wt=12): 2328 (x ^ y) ' v (z v (y v u)) = 1. [para(1869(a,1),14(a,1,1)),demod(87(2),14(5)),flip(a)]. given #464 (T,wt=12): 2329 (x ^ y) ' v (z v (u v y)) = 1. [para(14(a,1),1869(a,1,2))]. given #465 (T,wt=12): 2335 (c1 ^ x) ' v (y v (c2 ^ x)) = 1. [para(66(a,1),1869(a,1,1,1))]. given #466 (A,wt=19): 218 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(25(a,1),32(a,1,2,2,1)),demod(14(5))]. given #467 (F,wt=12): 2338 (x ^ c1) ' v (y v (x ^ c2)) = 1. [para(96(a,1),1869(a,1,1,1))]. given #468 (F,wt=12): 2341 c2 v (x v (y ^ (x v c1)) ') = 1. [para(429(a,1),1869(a,1,2)),demod(13(7),14(7))]. given #469 (T,wt=12): 2357 (x ^ c1) ' v (y v (c2 v z)) = 1. [para(1873(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #470 (T,wt=12): 2358 (x ^ c1) ' v (y v (z v c2)) = 1. [para(14(a,1),1873(a,1,2))]. given #471 (A,wt=15): 219 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(26(a,1),32(a,1,2,2))]. given #472 (F,wt=12): 2401 (c1 ^ x) ' v (y v (c2 v z)) = 1. [para(1874(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #473 (F,wt=12): 2402 (c1 ^ x) ' v (y v (z v c2)) = 1. [para(14(a,1),1874(a,1,2))]. given #474 (T,wt=12): 2411 c2 ' ^ (x ^ (y ^ (c1 ^ z))) = 0. [para(1942(a,1),16(a,1,1)),demod(90(2),16(7),16(6)),flip(a)]. given #475 (T,wt=12): 2412 c2 ' ^ (x ^ (y ^ (z ^ c1))) = 0. [para(16(a,1),1942(a,1,2,2))]. given #476 (A,wt=19): 220 (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 #477 (F,wt=12): 2421 (x v y) ' ^ (z ^ (x ^ u)) = 0. [para(1951(a,1),16(a,1,1)),demod(90(2),16(5)),flip(a)]. given #478 (F,wt=12): 2422 (x v y) ' ^ (z ^ (u ^ x)) = 0. [para(16(a,1),1951(a,1,2))]. given #479 (T,wt=12): 2427 c1 ^ (x ^ ((c2 ^ x) v y) ') = 0. [para(66(a,1),1951(a,1,2)),demod(15(7),16(7))]. given #480 (T,wt=12): 2429 x ^ (c1 ^ ((x ^ c2) v y) ') = 0. [para(96(a,1),1951(a,1,2)),demod(15(7),16(7))]. given #481 (A,wt=14): 221 (x v ((y v x) ^ z)) ^ (y v x) ' = 0. [para(32(a,1),152(a,1,2,1))]. given #482 (F,wt=12): 2445 (x v y) ' ^ (z ^ (y ^ u)) = 0. [para(1955(a,1),16(a,1,1)),demod(90(2),16(5)),flip(a)]. given #483 (F,wt=12): 2446 (x v y) ' ^ (z ^ (u ^ y)) = 0. [para(16(a,1),1955(a,1,2))]. given #484 (T,wt=12): 2451 c1 ^ (x ^ (y v (c2 ^ x)) ') = 0. [para(66(a,1),1955(a,1,2)),demod(15(7),16(7))]. given #485 (T,wt=12): 2455 x ^ (c1 ^ (y v (x ^ c2)) ') = 0. [para(96(a,1),1955(a,1,2)),demod(15(7),16(7))]. given #486 (A,wt=15): 222 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 #487 (F,wt=12): 2457 (c2 v x) ' ^ (y ^ (x v c1)) = 0. [para(429(a,1),1955(a,1,1,1))]. given #488 (F,wt=12): 2475 (x ^ (y v z)) v (x ^ z) ' = 1. [para(108(a,1),224(a,1,2,1))]. given #489 (T,wt=12): 2477 x ^ (y ^ (x ^ (z v y)) ') = 0. [para(108(a,1),336(a,1,2)),demod(15(5),16(5))]. given #490 (T,wt=12): 2500 (c2 v x) ' ^ (y ^ (c1 ^ z)) = 0. [para(1960(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #491 (A,wt=15): 226 x ^ (x ^ y) ' != 0 | (x ^ y) ' = x '. [para(191(a,1),21(a,1)),flip(c),xx(a)]. given #492 (F,wt=12): 2501 (c2 v x) ' ^ (y ^ (z ^ c1)) = 0. [para(16(a,1),1960(a,1,2))]. given #493 (F,wt=12): 2509 (x v c2) ' ^ (y ^ (c1 ^ z)) = 0. [para(1961(a,1),16(a,1,1)),demod(90(2),16(7)),flip(a)]. given #494 (T,wt=12): 2510 (x v c2) ' ^ (y ^ (z ^ c1)) = 0. [para(16(a,1),1961(a,1,2))]. given #495 (T,wt=12): 2527 (c1 v x) ^ ((x v c2) ' ^ y) = 0. [para(2029(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #496 (A,wt=15): 231 x ^ (y ^ x) ' != 0 | (y ^ x) ' = x '. [para(224(a,1),21(a,1)),flip(c),xx(a)]. given #497 (F,wt=12): 2530 (c1 v x) ^ (y ^ (x v c2) ') = 0. [para(2029(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #498 (F,wt=12): 2545 ((x ^ y) v z) ^ (y v z) ' = 0. [para(109(a,1),152(a,1,2,1))]. given #499 (T,wt=12): 2548 x v (y v ((z ^ x) v y) ') = 1. [para(38(a,1),109(a,1,2)),demod(97(2)),flip(a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 87 (0.00 of 3.91 sec). given #500 (T,wt=12): 2573 x v (y v (y v (z ^ x)) ') = 1. [para(268(a,1),109(a,1,2)),demod(97(2)),flip(a)]. given #501 (A,wt=14): 236 (x ^ ((y ^ x) v z)) v (y ^ x) ' = 1. [para(30(a,1),224(a,1,2,1))]. given #502 (F,wt=12): 2577 x v (c2 v (c1 v (y ^ x)) ') = 1. [para(436(a,1),109(a,1,2)),demod(97(2),13(5)),flip(a)]. given #503 (F,wt=12): 2594 x v (c2 v ((c1 v x) ' v y)) = 1. [para(2040(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #504 (T,wt=12): 2595 c2 v (x v (y v (c1 v y) ')) = 1. [para(2040(a,1),14(a,2,2)),demod(25(7),14(6),97(9))]. given #505 (T,wt=12): 2597 x v (y v (c2 v (c1 v x) ')) = 1. [para(2040(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #506 (A,wt=15): 243 c2 ^ (x v c1 ') != 0 | c2 ' = x v c1 '. [para(238(a,1),21(a,1)),xx(a)]. given #507 (F,wt=12): 2611 (c1 v x) ^ ((c2 v x) ' ^ y) = 0. [para(2118(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #508 (F,wt=12): 2613 (c1 v x) ^ (y ^ (c2 v x) ') = 0. [para(2118(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #509 (T,wt=12): 2621 (c1 v (c2 ^ x)) ^ (c2 ' ^ y) = 0. [para(2119(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #510 (T,wt=12): 2623 (c1 v (c2 ^ x)) ^ (y ^ c2 ') = 0. [para(2119(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #511 (A,wt=13): 244 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(15(a,1),34(a,1,1))]. given #512 (F,wt=12): 2632 (c1 v (x ^ c2)) ^ (c2 ' ^ y) = 0. [para(2122(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #513 (F,wt=12): 2634 (c1 v (x ^ c2)) ^ (y ^ c2 ') = 0. [para(2122(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #514 (T,wt=12): 2678 c2 v (x v ((c1 v x) ' v y)) = 1. [para(2134(a,1),14(a,1,1)),demod(87(2),14(7)),flip(a)]. given #515 (T,wt=12): 2687 c2 v ((c1 v (c2 ^ x)) ' v y) = 1. [para(2137(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #516 (A,wt=13): 245 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(15(a,1),34(a,1,2)),demod(16(3))]. given #517 (F,wt=12): 2689 c2 v (x v (c1 v (c2 ^ y)) ') = 1. [para(2137(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #518 (F,wt=12): 2690 c2 v (c1 v (x ^ (c2 ^ y))) ' = 1. [para(26(a,1),2137(a,1,2,1,2))]. given #519 (T,wt=12): 2700 c1 ^ (c2 ^ (x v (y v c1))) ' = 0. [para(14(a,1),2196(a,1,2,1,2))]. given #520 (T,wt=12): 2701 c1 ^ ((c2 ^ (x v c1)) ' ^ y) = 0. [para(2196(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #521 (A,wt=19): 246 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(16(a,1),34(a,1,1)),demod(16(5),16(8))]. given #522 (F,wt=12): 2703 c1 ^ (x ^ (c2 ^ (y v c1)) ') = 0. [para(2196(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #523 (F,wt=12): 2710 c1 ' v ((c2 ^ (c1 v x)) v y) = 1. [para(2204(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #524 (T,wt=12): 2711 c1 ' v (x v (c2 ^ (c1 v y))) = 1. [para(2204(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #525 (T,wt=12): 2712 c1 ' v (c2 ^ (x v (c1 v y))) = 1. [para(25(a,1),2204(a,1,2,2))]. given #526 (A,wt=17): 248 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(34(a,1),25(a,1,2)),flip(a)]. given #527 (F,wt=12): 2739 c1 ' v ((c2 ^ (x v c1)) v y) = 1. [para(2216(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #528 (F,wt=12): 2740 c1 ' v (c2 ^ (x v (y v c1))) = 1. [para(14(a,1),2216(a,1,2,2))]. given #529 (T,wt=12): 2741 c1 ' v (x v (c2 ^ (y v c1))) = 1. [para(2216(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #530 (T,wt=12): 2750 c2 v ((c1 v (x ^ c2)) ' v y) = 1. [para(2579(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #531 (A,wt=19): 249 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(26(a,1),34(a,1,1)),demod(16(4))]. given #532 (F,wt=12): 2751 c2 v (c1 v (x ^ (y ^ c2))) ' = 1. [para(16(a,1),2579(a,1,2,1,2))]. given #533 (F,wt=12): 2753 c2 v (x v (c1 v (y ^ c2)) ') = 1. [para(2579(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #534 (T,wt=12): 2763 c2 ' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(2620(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #535 (T,wt=12): 2764 c2 ' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(2620(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #536 (A,wt=15): 250 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(26(a,1),34(a,1,2,2))]. given #537 (F,wt=12): 2765 c2 ' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(26(a,1),2620(a,1,2,2))]. given #538 (F,wt=12): 2780 (x v (y ^ z)) ^ (x v z) ' = 0. [para(114(a,1),152(a,1,2,1))]. given #539 (T,wt=12): 2783 x v (y v (x v (z ^ y)) ') = 1. [para(114(a,1),335(a,1,2)),demod(13(5),14(5))]. given #540 (T,wt=12): 2816 c2 ' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(2631(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #541 (A,wt=22): 252 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y) ' = x ^ (y ^ z). [back_demod(247),demod(251(7))]. given #542 (F,wt=12): 2817 c2 ' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(16(a,1),2631(a,1,2,2))]. given #543 (F,wt=12): 2818 c2 ' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(2631(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #544 (T,wt=12): 2840 x v (c2 v (y ^ (x v c1)) ') = 1. [para(129(a,1),230(a,1,2,1,2)),demod(14(7))]. given #545 (T,wt=12): 2841 x v (c2 v (y v (x v c1) ')) = 1. [para(129(a,1),233(a,1,2,2,1)),demod(14(7))]. given #546 (A,wt=15): 253 c2 ^ (c1 ' v x) != 0 | c2 ' = c1 ' v x. [para(239(a,1),21(a,1)),xx(a)]. given #547 (F,wt=12): 2842 (x v c2) ' ^ (y ^ (x v c1)) = 0. [para(129(a,1),344(a,1,2,2))]. given #548 (F,wt=12): 2844 (x v c1) ' v (y v (x v c2)) = 1. [para(129(a,1),1869(a,1,1,1))]. given #549 (T,wt=12): 2845 (x v c1) ^ (x v (c2 v y)) ' = 0. [para(129(a,1),1951(a,1,2)),demod(14(3),15(7))]. given #550 (T,wt=12): 2846 (x v c1) ^ (y v (x v c2)) ' = 0. [para(129(a,1),1955(a,1,2)),demod(15(7))]. given #551 (A,wt=13): 254 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(16(a,1),67(a,1,2)),demod(15(8))]. given #552 (F,wt=12): 2864 c1 ^ (x ^ (y ^ (c2 ^ x) ')) = 0. [para(184(a,1),151(a,1,2,2,1)),demod(16(7))]. given #553 (F,wt=12): 2932 ((c2 v x) ^ y) v (c1 ^ y) ' = 1. [para(185(a,1),224(a,1,2,1))]. given #554 (T,wt=12): 2934 c1 ^ (x ^ ((c2 v y) ^ x) ') = 0. [para(41(a,1),185(a,1,2)),demod(15(3),90(3)),flip(a)]. given #555 (T,wt=12): 2947 c1 ^ (x ^ (x ^ (c2 v y)) ') = 0. [para(288(a,1),185(a,1,2)),demod(15(3),90(3)),flip(a)]. given #556 (A,wt=14): 256 c2 != 1 | x ^ c1 != 0 | c2 ' = x ^ c1. [para(67(a,1),21(b,1)),demod(255(4))]. given #557 (F,wt=12): 2960 (x ^ (c2 v y)) v (x ^ c1) ' = 1. [para(201(a,1),224(a,1,2,1))]. given #558 (F,wt=12): 2961 x ^ (c1 ^ (x ^ (c2 v y)) ') = 0. [para(201(a,1),336(a,1,2)),demod(15(7),16(7))]. given #559 (T,wt=12): 2985 ((x v c2) ^ y) v (c1 ^ y) ' = 1. [para(203(a,1),224(a,1,2,1))]. given #560 (T,wt=12): 2987 c1 ^ (x ^ ((y v c2) ^ x) ') = 0. [para(41(a,1),203(a,1,2)),demod(15(3),90(3)),flip(a)]. given #561 (A,wt=13): 259 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(67(a,1),34(a,1,2,2))]. given #562 (F,wt=12): 3001 c1 ^ (x ^ (x ^ (y v c2)) ') = 0. [para(288(a,1),203(a,1,2)),demod(15(3),90(3)),flip(a)]. given #563 (F,wt=12): 3014 (x ^ (y v c2)) v (x ^ c1) ' = 1. [para(205(a,1),224(a,1,2,1))]. given #564 (T,wt=12): 3015 x ^ (c1 ^ (x ^ (y v c2)) ') = 0. [para(205(a,1),336(a,1,2)),demod(15(7),16(7))]. given #565 (T,wt=12): 3053 x v (y v (z v (y v x) ')) = 1. [para(120(a,1),197(a,1,2,2,1)),demod(14(5))]. given #566 (A,wt=14): 265 c2 != 1 | c1 ^ x != 0 | c2 ' = c1 ^ x. [para(261(a,1),21(a,1)),demod(26(7),66(7))]. given #567 (F,wt=12): 3056 x v (y v (z ^ (y v x)) ') = 1. [para(120(a,1),227(a,1,2,1,2)),demod(14(5))]. given #568 (F,wt=12): 3060 (x v y) ' ^ (z ^ (y v x)) = 0. [para(120(a,1),343(a,1,2,2))]. given #569 (T,wt=12): 3062 (x v y) ' v (z v (y v x)) = 1. [para(120(a,1),1866(a,1,1,1))]. given #570 (T,wt=12): 3067 ((x ^ c1) v y) ^ (c2 v y) ' = 0. [para(257(a,1),152(a,1,2,1))]. given #571 (A,wt=14): 269 x v (y v (z v (x v (y v z)) ')) = 1. [para(38(a,1),14(a,1)),demod(14(3)),flip(a)]. given #572 (F,wt=12): 3069 c2 v (x v ((y ^ c1) v x) ') = 1. [para(38(a,1),257(a,1,2)),demod(13(3),87(3)),flip(a)]. given #573 (F,wt=12): 3085 c2 v (x v (x v (y ^ c1)) ') = 1. [para(268(a,1),257(a,1,2)),demod(13(3),87(3)),flip(a)]. given #574 (T,wt=12): 3108 x ^ (c1 ^ (y v (c2 ^ x)) ') = 0. [para(260(a,1),169(a,1,2,1,2)),demod(16(7))]. given #575 (T,wt=12): 3109 x ^ (c1 ^ (y ^ (c2 ^ x) ')) = 0. [para(260(a,1),174(a,1,2,2,1)),demod(16(7))]. given #576 (A,wt=19): 270 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 #577 (F,wt=12): 3117 (x ^ c1) ' v (y v (c2 ^ x)) = 1. [para(260(a,1),338(a,1,2,2))]. given #578 (F,wt=12): 3120 (c2 ^ x) v (x ^ (c1 ^ y)) ' = 1. [para(260(a,1),1866(a,1,2)),demod(16(3),13(7))]. given #579 (T,wt=12): 3121 (c2 ^ x) v (y ^ (x ^ c1)) ' = 1. [para(260(a,1),1869(a,1,2)),demod(13(7))]. given #580 (T,wt=12): 3123 (c2 ^ x) ' ^ (y ^ (x ^ c1)) = 0. [para(260(a,1),1955(a,1,1,1))]. given #581 (A,wt=14): 272 x v (y v (z v (y v (x v z)) ')) = 1. [para(25(a,1),38(a,1,2,2,1)),demod(14(5))]. given #582 (F,wt=12): 3126 (x v (y ^ c1)) ^ (x v c2) ' = 0. [para(263(a,1),152(a,1,2,1))]. given #583 (F,wt=12): 3128 x v (c2 v (x v (y ^ c1)) ') = 1. [para(263(a,1),335(a,1,2)),demod(13(7),14(7))]. given #584 (T,wt=12): 3168 x v ((y v x) ' v (z v y)) = 1. [para(38(a,1),121(a,1,1)),demod(14(6),78(7),38(9))]. given #585 (T,wt=12): 3171 (x v y) ^ (y v (z v x)) ' = 0. [para(121(a,1),336(a,1,2)),demod(15(5))]. given #586 (A,wt=15): 277 c2 ^ (x ^ c1) ' != 0 | (x ^ c1) ' = c2 '. [para(258(a,1),21(a,1)),flip(c),xx(a)]. given #587 (F,wt=12): 3189 c2 v ((x v c1) ' v (y v x)) = 1. [para(436(a,1),121(a,1,1)),demod(14(8),78(9),436(13))]. given #588 (F,wt=12): 3192 x v ((x v c1) ' v (y v c2)) = 1. [para(552(a,1),121(a,1,1)),demod(14(8),78(9),552(13))]. given #589 (T,wt=12): 3193 (c1 ^ x) ' v (y v (x ^ c2)) = 1. [para(1328(a,1),121(a,1,1)),demod(78(9),1328(13))]. given #590 (T,wt=12): 3199 c2 v ((c1 v x) ' v (y v x)) = 1. [para(2040(a,1),121(a,1,1)),demod(14(8),78(9),2040(13))]. given #591 (A,wt=15): 280 c2 ^ (c1 ^ x) ' != 0 | (c1 ^ x) ' = c2 '. [para(275(a,1),21(a,1)),flip(c),xx(a)]. given #592 (F,wt=12): 3201 x v ((c1 v x) ' v (y v c2)) = 1. [para(2134(a,1),121(a,1,1)),demod(14(8),78(9),2134(13))]. given #593 (F,wt=12): 3202 (c1 v (c2 ^ x)) ' v (y v c2) = 1. [para(2137(a,1),121(a,1,1)),demod(78(10),2137(15))]. given #594 (T,wt=12): 3203 (c1 v (x ^ c2)) ' v (y v c2) = 1. [para(2579(a,1),121(a,1,1)),demod(78(10),2579(15))]. given #595 (T,wt=12): 3215 ((c1 ^ x) v y) ^ (c2 v y) ' = 0. [para(264(a,1),152(a,1,2,1))]. given #596 (A,wt=13): 283 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(69(a,1),16(a,2,2)),demod(26(3),16(2))]. given #597 (F,wt=12): 3217 c2 v (x v ((c1 ^ y) v x) ') = 1. [para(38(a,1),264(a,1,2)),demod(13(3),87(3)),flip(a)]. given #598 (F,wt=12): 3233 c2 v (x v (x v (c1 ^ y)) ') = 1. [para(268(a,1),264(a,1,2)),demod(13(3),87(3)),flip(a)]. given #599 (T,wt=12): 3248 (x v (c1 ^ y)) ^ (x v c2) ' = 0. [para(266(a,1),152(a,1,2,1))]. given #600 (T,wt=12): 3250 x v (c2 v (x v (c1 ^ y)) ') = 1. [para(266(a,1),335(a,1,2)),demod(13(7),14(7))]. given #601 (A,wt=13): 285 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(16(a,1),71(a,1,2)),demod(16(5))]. given #602 (F,wt=12): 3308 x ^ (y ^ (z v (y ^ x)) ') = 0. [para(287(a,1),169(a,1,2,1,2)),demod(16(5))]. given #603 (F,wt=12): 3309 x ^ (y ^ (z ^ (y ^ x) ')) = 0. [para(287(a,1),174(a,1,2,2,1)),demod(16(5))]. given #604 (T,wt=12): 3320 (x ^ y) ' v (z v (y ^ x)) = 1. [para(287(a,1),338(a,1,2,2))]. given #605 (T,wt=12): 3323 (x ^ y) v (y ^ (x ^ z)) ' = 1. [para(287(a,1),1866(a,1,2)),demod(16(2),13(5))]. given #606 (A,wt=14): 289 x ^ (y ^ (z ^ (x ^ (y ^ z)) ')) = 0. [para(41(a,1),16(a,1)),demod(16(3)),flip(a)]. given #607 (F,wt=12): 3324 (x ^ y) v (z ^ (y ^ x)) ' = 1. [para(287(a,1),1869(a,1,2)),demod(13(5))]. given #608 (F,wt=12): 3326 (x ^ y) ' ^ (z ^ (y ^ x)) = 0. [para(287(a,1),1955(a,1,1,1))]. given #609 (T,wt=12): 3361 (x ^ y) v ((y ^ x) ' v z) = 1. [para(3304(a,1),14(a,1,1)),demod(87(2)),flip(a)]. given #610 (T,wt=12): 3364 (x ^ y) v (z v (y ^ x) ') = 1. [para(3304(a,1),25(a,1,2)),demod(97(2)),flip(a)]. given #611 (A,wt=19): 290 x v (y ^ (x ^ y) ') != 1 | y ^ (x ^ y) ' = x '. [para(41(a,1),21(b,1)),flip(c),xx(b)]. given #612 (F,wt=12): 3384 (x v y) ^ (y v (x v z)) ' = 0. [para(298(a,1),1951(a,1,2)),demod(14(2),15(5))]. given #613 (F,wt=12): 3385 (x v y) ^ (z v (y v x)) ' = 0. [para(298(a,1),1955(a,1,2)),demod(15(5))]. given #614 (T,wt=12): 3388 (x v y) ^ ((y v x) ' ^ z) = 0. [para(3378(a,1),16(a,1,1)),demod(90(2)),flip(a)]. given #615 (T,wt=12): 3390 (x v y) ^ (z ^ (y v x) ') = 0. [para(3378(a,1),26(a,1,2)),demod(100(2)),flip(a)]. given #616 (A,wt=14): 292 x ^ (y ^ (z ^ (y ^ (x ^ z)) ')) = 0. [para(26(a,1),41(a,1,2,2,1)),demod(16(5))]. given #617 (F,wt=12): 3468 (c1 v x) ^ (c2 v (x v y)) ' = 0. [para(2029(a,1),123(a,1,2)),demod(15(4),90(4),13(6)),flip(a)]. given #618 (F,wt=12): 3527 x ^ (c1 ^ (y ^ (x ^ c2) ')) = 0. [para(351(a,1),151(a,1,2,2,1)),demod(16(7))]. given #619 (T,wt=12): 3744 x v (c2 v (y ^ (c1 v x)) ') = 1. [para(468(a,1),230(a,1,2,1,2)),demod(14(7))]. given #620 (T,wt=12): 3745 x v (c2 v (y v (c1 v x) ')) = 1. [para(468(a,1),233(a,1,2,2,1)),demod(14(7))]. given #621 (A,wt=13): 295 x v (y v (x v z)) = y v (x v z). [para(74(a,1),14(a,2,2)),demod(25(3),14(2))]. given #622 (F,wt=12): 3746 (x v c2) ' ^ (y ^ (c1 v x)) = 0. [para(468(a,1),344(a,1,2,2))]. given #623 (F,wt=12): 3749 (c1 v x) ' v (y v (x v c2)) = 1. [para(468(a,1),1869(a,1,1,1))]. low water: id=6145, wt=52 given #624 (T,wt=12): 3750 (c1 v x) ^ (x v (c2 v y)) ' = 0. [para(468(a,1),1951(a,1,2)),demod(14(3),15(7))]. low water: id=6161, wt=50 low water: id=6022, wt=48 low water: id=6064, wt=46 given #625 (T,wt=12): 3751 (c1 v x) ^ (y v (x v c2)) ' = 0. [para(468(a,1),1955(a,1,2)),demod(15(7))]. low water: id=6372, wt=45 given #626 (A,wt=13): 297 x v (y v (z v x)) = y v (z v x). [para(14(a,1),76(a,1,2)),demod(14(5))]. low water: id=6131, wt=44 low water: id=6570, wt=43 low water: id=6620, wt=42 low water: id=6371, wt=41 given #627 (F,wt=12): 3864 c2 v (x v (y v (x v c1) ')) = 1. [para(549(a,1),233(a,1,2,2,1)),demod(14(7))]. given #628 (F,wt=12): 3868 (x v c1) ^ (c2 v (x v y)) ' = 0. [para(549(a,1),1951(a,1,2)),demod(14(3),15(7))]. low water: id=6562, wt=40 given #629 (T,wt=12): 3945 c2 v (x v (y ^ (c1 v x)) ') = 1. [para(2383(a,1),230(a,1,2,1,2)),demod(14(7))]. given #630 (T,wt=12): 3946 c2 v (x v (y v (c1 v x) ')) = 1. [para(2383(a,1),233(a,1,2,2,1)),demod(14(7))]. given #631 (A,wt=15): 300 (x v y) ^ (z v (x v (y v u))) = x v y. [para(14(a,1),80(a,1,2,2))]. low water: id=6569, wt=39 low water: id=6607, wt=38 low water: id=6361, wt=37 low water: id=6579, wt=36 low water: id=6632, wt=35 given #632 (F,wt=12): 3947 (c2 v x) ' ^ (y ^ (c1 v x)) = 0. [para(2383(a,1),344(a,1,2,2))]. given #633 (F,wt=12): 3949 (c1 v x) ' v (y v (c2 v x)) = 1. [para(2383(a,1),1869(a,1,1,1))]. given #634 (T,wt=12): 3950 (c1 v x) ^ (y v (c2 v x)) ' = 0. [para(2383(a,1),1955(a,1,2)),demod(15(7))]. given #635 (T,wt=12): 4233 (c2 ^ x) v (c1 ^ (x ^ y)) ' = 1. [para(4042(a,1),1866(a,1,2)),demod(16(3),13(7))]. low water: id=7066, wt=34 given #636 (A,wt=18): 302 x v (y v z) != 1 | 0 != y | y ' = x v (y v z). [para(80(a,1),21(b,1)),demod(295(3)),flip(b)]. given #637 (F,wt=12): 4273 (x v c1) ^ (x v (y v c2)) ' = 0. [para(119(a,1),153(a,1,2,1,2))]. low water: id=7199, wt=33 given #638 (F,wt=12): 4280 ((x ^ y) v z) ^ (z v x) ' = 0. [para(299(a,1),153(a,1,2,1))]. given #639 (T,wt=12): 4283 ((x ^ y) v z) ^ (z v y) ' = 0. [para(2549(a,1),153(a,1,2,1))]. low water: id=7300, wt=32 low water: id=7447, wt=31 given #640 (T,wt=12): 4287 ((x ^ c1) v y) ^ (y v c2) ' = 0. [para(3070(a,1),153(a,1,2,1))]. given #641 (A,wt=13): 303 x ^ (y ^ (z v (x v u))) = y ^ x. [para(80(a,1),26(a,1,2)),flip(a)]. low water: id=7157, wt=30 low water: id=7735, wt=29 given #642 (F,wt=12): 4289 ((c1 ^ x) v y) ^ (y v c2) ' = 0. [para(3218(a,1),153(a,1,2,1))]. given #643 (F,wt=12): 4375 x ^ (y ^ ((y ^ x) v z) ') = 0. [para(15(a,1),154(a,1,2,2,1,1))]. low water: id=7898, wt=28 given #644 (T,wt=12): 4441 (x v (y ^ z)) ^ (y v x) ' = 0. [para(13(a,1),198(a,1,1))]. low water: id=8080, wt=27 given #645 (T,wt=12): 4443 (x v y) ' ^ ((x ^ z) v y) = 0. [para(198(a,1),15(a,1)),flip(a)]. given #646 (A,wt=15): 304 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(16(a,1),93(a,1,2,2))]. given #647 (F,wt=12): 4445 ((x ^ y) v (x ^ z)) ^ x ' = 0. [para(18(a,1),198(a,1,2,1))]. given #648 (F,wt=12): 4450 ((x ^ y) v (z ^ x)) ^ x ' = 0. [para(33(a,1),198(a,1,2,1))]. given #649 (T,wt=12): 4454 ((c2 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(255(a,1),198(a,1,2,1))]. given #650 (T,wt=12): 4455 ((c2 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(261(a,1),198(a,1,2,1))]. given #651 (A,wt=18): 306 1 != x | y ^ (x ^ z) != 0 | x ' = y ^ (x ^ z). [para(93(a,1),21(a,1)),demod(283(5)),flip(a)]. given #652 (F,wt=12): 4559 x v (y v ((y v x) ^ z) ') = 1. [para(13(a,1),223(a,1,2,2,1,1))]. given #653 (F,wt=12): 4574 c2 v (x v ((c1 v x) ^ y) ') = 1. [para(223(a,1),2040(a,1,2,2,1)),demod(86(8),13(8),84(8),13(7))]. given #654 (T,wt=12): 4579 (x ^ y) v (y ^ (z ^ x)) ' = 1. [para(15(a,1),225(a,1,2,1)),demod(16(3))]. low water: id=8414, wt=26 given #655 (T,wt=12): 4582 (x ^ c2) v (x ^ (y ^ c1)) ' = 1. [para(67(a,1),225(a,1,2,1,2))]. given #656 (A,wt=13): 307 x v (y v (z ^ (x ^ u))) = y v x. [para(93(a,1),25(a,1,2)),flip(a)]. given #657 (F,wt=12): 4593 ((x v y) ^ z) v (z ^ x) ' = 1. [para(286(a,1),225(a,1,2,1))]. given #658 (F,wt=12): 4597 ((x v y) ^ z) v (z ^ y) ' = 1. [para(2176(a,1),225(a,1,2,1))]. given #659 (T,wt=12): 4599 ((c2 v x) ^ y) v (y ^ c1) ' = 1. [para(2933(a,1),225(a,1,2,1))]. given #660 (T,wt=12): 4601 ((x v c2) ^ y) v (y ^ c1) ' = 1. [para(2986(a,1),225(a,1,2,1))]. given #661 (A,wt=20): 308 x v (y v z) != 1 | z ^ (x v y) != 0 | z ' = x v y. [para(14(a,1),43(a,1))]. given #662 (F,wt=12): 4729 (x ^ y) ' v ((x v z) ^ y) = 1. [para(235(a,1),13(a,1)),flip(a)]. low water: id=8387, wt=25 given #663 (F,wt=12): 4730 (x ^ (y v z)) v (y ^ x) ' = 1. [para(15(a,1),235(a,1,1))]. given #664 (T,wt=12): 4731 ((x v y) ^ (x v z)) v x ' = 1. [para(17(a,1),235(a,1,2,1))]. given #665 (T,wt=12): 4735 ((x v y) ^ (z v x)) v x ' = 1. [para(27(a,1),235(a,1,2,1))]. given #666 (A,wt=14): 309 x v y != 1 | x ^ y != 0 | y ' = x. [para(15(a,1),43(b,1))]. low water: id=8939, wt=24 given #667 (F,wt=12): 4739 ((c1 v x) ^ (c2 v y)) v c1 ' = 1. [para(180(a,1),235(a,1,2,1))]. given #668 (F,wt=12): 4740 ((c1 v x) ^ (y v c2)) v c1 ' = 1. [para(183(a,1),235(a,1,2,1))]. given #669 (T,wt=12): 4819 x v (y v ((y ^ z) v x) ') = 1. [para(273(a,1),25(a,1)),flip(a)]. given #670 (T,wt=12): 4822 x v ((x ^ y) v (x ^ z)) ' = 1. [para(273(a,1),31(a,1)),flip(a)]. given #671 (A,wt=20): 310 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z) ' = x. [para(16(a,1),43(b,1))]. given #672 (F,wt=12): 4834 x v ((x ^ y) v (z ^ x)) ' = 1. [para(273(a,1),109(a,1)),flip(a)]. given #673 (F,wt=12): 4837 c2 v ((c2 ^ x) v (y ^ c1)) ' = 1. [para(273(a,1),257(a,1)),flip(a)]. given #674 (T,wt=12): 4839 c2 v ((c2 ^ x) v (c1 ^ y)) ' = 1. [para(273(a,1),264(a,1)),flip(a)]. given #675 (T,wt=12): 4895 x ^ (y ^ ((y v z) ^ x) ') = 0. [para(288(a,1),145(a,1,2)),demod(100(2)),flip(a)]. given #676 (A,wt=14): 311 1 != x | x ^ y != 0 | (x ^ y) ' = x. [para(18(a,1),43(a,1)),demod(15(4),69(4)),flip(a)]. given #677 (F,wt=12): 4897 c1 ^ (x ^ (c2 ^ (x v y)) ') = 0. [para(294(a,1),145(a,1,2)),demod(100(2)),flip(a)]. given #678 (F,wt=12): 4929 x ^ ((x v y) ^ (x v z)) ' = 0. [para(293(a,1),29(a,1)),flip(a)]. given #679 (T,wt=12): 4944 x ^ ((x v y) ^ (z v x)) ' = 0. [para(293(a,1),104(a,1)),flip(a)]. given #680 (T,wt=12): 4945 c1 ^ ((c1 v x) ^ (c2 v y)) ' = 0. [para(293(a,1),185(a,1)),flip(a)]. given #681 (A,wt=20): 313 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z) ' = y. [para(25(a,1),43(a,1))]. given #682 (F,wt=12): 4947 c1 ^ ((c1 v x) ^ (y v c2)) ' = 0. [para(293(a,1),203(a,1)),flip(a)]. given #683 (F,wt=12): 5009 x ^ ((y ^ x) ' ^ (z ^ y)) = 0. [para(15(a,1),346(a,1,2,1,1))]. low water: id=9169, wt=23 given #684 (T,wt=12): 5018 c1 ^ ((c2 ^ x) ' ^ (y ^ x)) = 0. [para(346(a,1),66(a,1,2)),demod(15(3),90(3)),flip(a)]. given #685 (T,wt=12): 5507 (c1 v (c2 ^ x)) ^ (y v c2) ' = 0. [para(18(a,1),853(a,1,2,1,2)),demod(13(4))]. given #686 (A,wt=20): 314 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z ' = x ^ y. [para(26(a,1),43(b,1))]. given #687 (F,wt=12): 5510 (x v c1) ^ (c2 v (y v x)) ' = 0. [para(25(a,1),853(a,1,2,1))]. given #688 (F,wt=12): 5511 (c1 v (x ^ c2)) ^ (y v c2) ' = 0. [para(33(a,1),853(a,1,2,1,2)),demod(13(4))]. given #689 (T,wt=12): 5523 (c1 v (x ^ y)) ^ (c2 v x) ' = 0. [para(81(a,1),853(a,1,2,1)),demod(13(3))]. given #690 (T,wt=12): 5529 (c1 v (x ^ y)) ^ (c2 v y) ' = 0. [para(114(a,1),853(a,1,2,1)),demod(13(3))]. given #691 (A,wt=14): 315 1 != x | y ^ x != 0 | (y ^ x) ' = x. [para(33(a,1),43(a,1)),demod(15(4),71(4)),flip(a)]. given #692 (F,wt=12): 6503 (x ^ c2) v (y ^ (c1 ^ x)) ' = 1. [para(15(a,1),1293(a,1,1))]. given #693 (F,wt=12): 6504 (c2 ^ (c1 v x)) v (y ^ c1) ' = 1. [para(17(a,1),1293(a,1,2,1,2))]. given #694 (T,wt=12): 6508 (c2 ^ x) v (c1 ^ (y ^ x)) ' = 1. [para(26(a,1),1293(a,1,2,1))]. given #695 (T,wt=12): 6509 (c2 ^ (x v c1)) v (y ^ c1) ' = 1. [para(27(a,1),1293(a,1,2,1,2))]. given #696 (A,wt=15): 317 x ^ (x ' v y) != 0 | (x ' v y) ' = x. [para(88(a,1),43(a,1)),demod(15(6)),xx(a)]. given #697 (F,wt=12): 6529 (c2 ^ (x v y)) v (c1 ^ x) ' = 1. [para(92(a,1),1293(a,1,2,1))]. given #698 (F,wt=12): 6534 (c2 ^ (x v y)) v (c1 ^ y) ' = 1. [para(108(a,1),1293(a,1,2,1))]. given #699 (T,wt=12): 6647 c1 ^ ((c2 ^ (c1 v x)) v y) ' = 0. [para(6559(a,1),336(a,1,2)),demod(15(8))]. given #700 (T,wt=12): 6690 c1 ^ ((c2 ^ (x v c1)) v y) ' = 0. [para(6638(a,1),336(a,1,2)),demod(15(8))]. given #701 (A,wt=15): 318 x ^ (y v x ') != 0 | (y v x ') ' = x. [para(98(a,1),43(a,1)),demod(15(6)),xx(a)]. given #702 (F,wt=12): 6732 c1 ^ (x v (c2 ^ (c1 v y))) ' = 0. [para(6639(a,1),336(a,1,2)),demod(15(8))]. given #703 (F,wt=12): 6769 c1 ^ (x v (c2 ^ (y v c1))) ' = 0. [para(6682(a,1),336(a,1,2)),demod(15(8))]. given #704 (T,wt=12): 6815 (x ^ c2) v (x ^ (c1 ^ y)) ' = 1. [para(15(a,1),1295(a,1,2,1)),demod(16(5))]. given #705 (T,wt=12): 6819 (c2 ^ (x v y)) v (x ^ c1) ' = 1. [para(29(a,1),1295(a,1,2,1)),demod(15(3))]. given #706 (A,wt=22): 319 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 #707 (F,wt=12): 6826 (c2 ^ (x v y)) v (y ^ c1) ' = 1. [para(104(a,1),1295(a,1,2,1)),demod(15(3))]. given #708 (F,wt=12): 6989 x v (y v ((z ^ y) v x) ') = 1. [para(2549(a,1),1575(a,1,2)),demod(13(4))]. given #709 (T,wt=12): 6990 x v (c2 v ((y ^ c1) v x) ') = 1. [para(3070(a,1),1575(a,1,2)),demod(13(6))]. given #710 (T,wt=12): 6991 x v (c2 v ((c1 ^ y) v x) ') = 1. [para(3218(a,1),1575(a,1,2)),demod(13(6))]. given #711 (A,wt=26): 320 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 #712 (F,wt=12): 7028 x v ((y ^ x) v (x ^ z)) ' = 1. [para(1581(a,1),109(a,1)),flip(a)]. given #713 (F,wt=12): 7031 c2 v ((x ^ c1) v (c2 ^ y)) ' = 1. [para(1581(a,1),257(a,1)),flip(a)]. given #714 (T,wt=12): 7033 c2 v ((c1 ^ x) v (c2 ^ y)) ' = 1. [para(1581(a,1),264(a,1)),flip(a)]. low water: id=9813, wt=22 given #715 (T,wt=12): 7206 x ^ (y ^ ((z v y) ^ x) ') = 0. [para(2176(a,1),1786(a,1,2)),demod(15(4))]. given #716 (A,wt=13): 321 x ^ (x ^ y) ' != 0 | x ^ y = x. [para(191(a,1),43(a,1)),demod(15(6),312(11)),xx(a)]. given #717 (F,wt=12): 7207 x ^ (c1 ^ ((c2 v y) ^ x) ') = 0. [para(2933(a,1),1786(a,1,2)),demod(15(6))]. given #718 (F,wt=12): 7208 x ^ (c1 ^ ((y v c2) ^ x) ') = 0. [para(2986(a,1),1786(a,1,2)),demod(15(6))]. given #719 (T,wt=12): 7227 x ^ ((c2 ^ x) ' ^ (y ^ c1)) = 0. [para(294(a,1),1790(a,1,2,2,2,1)),demod(89(7),15(7),78(7),16(7))]. given #720 (T,wt=12): 7228 c1 ^ ((x ^ c2) ' ^ (y ^ x)) = 0. [para(353(a,1),1790(a,1,2,2,2,1)),demod(89(7),39(7),16(7))]. given #721 (A,wt=13): 322 x ^ (y ^ x) ' != 0 | y ^ x = x. [para(224(a,1),43(a,1)),demod(15(6),312(11)),xx(a)]. given #722 (F,wt=12): 7231 x ^ ((x ^ c2) ' ^ (y ^ c1)) = 0. [para(1793(a,1),1790(a,1,2,2,2,1)),demod(89(7),15(7),78(7),16(7))]. given #723 (F,wt=12): 7232 (c2 ^ (c1 v x)) ' ^ (y ^ c1) = 0. [para(1806(a,1),1790(a,1,2,2,2,1)),demod(89(8),15(8),78(8))]. given #724 (T,wt=12): 7233 (c2 ^ (x v c1)) ' ^ (y ^ c1) = 0. [para(2196(a,1),1790(a,1,2,2,2,1)),demod(89(8),15(8),78(8))]. given #725 (T,wt=12): 7268 x ^ ((y v x) ^ (x v z)) ' = 0. [para(1792(a,1),104(a,1)),flip(a)]. given #726 (A,wt=15): 324 c2 ^ (x v c1 ') != 0 | (x v c1 ') ' = c2. [para(238(a,1),43(a,1)),demod(15(8)),xx(a)]. given #727 (F,wt=12): 7270 c1 ^ ((c2 v x) ^ (c1 v y)) ' = 0. [para(1792(a,1),185(a,1)),flip(a)]. given #728 (F,wt=12): 7272 c1 ^ ((x v c2) ^ (c1 v y)) ' = 0. [para(1792(a,1),203(a,1)),flip(a)]. given #729 (T,wt=12): 7363 c1 ^ (x ^ (c2 ^ (y v x)) ') = 0. [para(2176(a,1),1800(a,1,2)),demod(15(6))]. given #730 (T,wt=12): 7403 (x v y) ' ^ (x v (y ^ z)) = 0. [para(1829(a,1),15(a,1)),flip(a)]. given #731 (A,wt=22): 325 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z)) ' = x ^ y. [para(34(a,1),43(a,1)),demod(15(7),26(7),26(6),16(5),283(6),69(6))]. given #732 (F,wt=12): 7453 c2 v (x v (c1 v (x ^ y)) ') = 1. [para(1831(a,1),2040(a,1,2,2,1)),demod(86(8),13(8),84(8),13(7))]. given #733 (F,wt=12): 7841 c2 v (x v (c1 v (y ^ x)) ') = 1. [para(114(a,1),1883(a,1,2)),demod(13(3),13(7),14(7))]. given #734 (T,wt=12): 7946 (x ^ c2) ' ^ (y ^ (c1 ^ x)) = 0. [para(15(a,1),1959(a,1,1,1))]. given #735 (T,wt=12): 8192 (x ^ y) ' v (x ^ (y v z)) = 1. [para(1990(a,1),13(a,1)),flip(a)]. given #736 (A,wt=15): 326 c2 ^ (c1 ' v x) != 0 | (c1 ' v x) ' = c2. [para(239(a,1),43(a,1)),demod(15(8)),xx(a)]. given #737 (F,wt=12): 8335 c1 ^ (x ^ (y ^ (x ^ c2) ')) = 0. [para(26(a,1),2017(a,1,2))]. given #738 (F,wt=12): 8540 (x ^ y) ' v ((z v x) ^ y) = 1. [para(2175(a,1),13(a,1)),flip(a)]. given #739 (T,wt=12): 8542 (x ^ (y v z)) v (z ^ x) ' = 1. [para(15(a,1),2175(a,1,1))]. given #740 (T,wt=12): 8544 ((x v y) ^ (y v z)) v y ' = 1. [para(17(a,1),2175(a,1,2,1))]. given #741 (A,wt=14): 327 c2 != 1 | x ^ c1 != 0 | (x ^ c1) ' = c2. [para(255(a,1),43(a,1)),demod(15(7),67(7))]. given #742 (F,wt=12): 8549 ((x v y) ^ (z v y)) v y ' = 1. [para(27(a,1),2175(a,1,2,1))]. low water: id=10202, wt=21 given #743 (F,wt=12): 8554 ((x v c1) ^ (c2 v y)) v c1 ' = 1. [para(180(a,1),2175(a,1,2,1))]. given #744 (T,wt=12): 8555 ((x v c1) ^ (y v c2)) v c1 ' = 1. [para(183(a,1),2175(a,1,2,1))]. given #745 (T,wt=12): 8638 x ^ ((y v x) ^ (z v x)) ' = 0. [para(2177(a,1),104(a,1)),flip(a)]. given #746 (A,wt=14): 328 c2 != 1 | c1 ^ x != 0 | (c1 ^ x) ' = c2. [para(261(a,1),43(a,1)),demod(15(7),26(7),66(7))]. given #747 (F,wt=12): 8642 c1 ^ ((x v c1) ^ (c2 v y)) ' = 0. [para(2177(a,1),185(a,1)),flip(a)]. given #748 (F,wt=12): 8644 c1 ^ ((x v c1) ^ (y v c2)) ' = 0. [para(2177(a,1),203(a,1)),flip(a)]. given #749 (T,wt=12): 8684 c1 ^ ((c2 v x) ^ (y v c1)) ' = 0. [para(2195(a,1),185(a,1)),flip(a)]. given #750 (T,wt=12): 8686 c1 ^ ((x v c2) ^ (y v c1)) ' = 0. [para(2195(a,1),203(a,1)),flip(a)]. given #751 (A,wt=19): 329 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 #752 (F,wt=12): 9063 x v (c2 v ((x v c1) ^ y) ') = 1. [para(2320(a,1),25(a,1)),flip(a)]. given #753 (F,wt=12): 9064 c2 v ((c1 v (c2 ^ x)) ^ y) ' = 1. [para(2320(a,1),31(a,1)),demod(13(6)),flip(a)]. given #754 (T,wt=12): 9069 c2 v ((c1 v (x ^ c2)) ^ y) ' = 1. [para(2320(a,1),109(a,1)),demod(13(6)),flip(a)]. given #755 (T,wt=12): 9240 c2 v (x ^ (c1 v (c2 ^ y))) ' = 1. [para(2341(a,1),31(a,1)),demod(13(6)),flip(a)]. given #756 (A,wt=13): 330 c2 ^ (x ^ c1) ' != 0 | x ^ c1 = c2. [para(258(a,1),43(a,1)),demod(15(8),312(14)),xx(a)]. given #757 (F,wt=12): 9242 c2 v (x ^ (c1 v (y ^ c2))) ' = 1. [para(2341(a,1),109(a,1)),demod(13(6)),flip(a)]. given #758 (F,wt=12): 9377 c1 ^ (x ^ ((x ^ c2) v y) ') = 0. [para(15(a,1),2427(a,1,2,2,1,1))]. given #759 (T,wt=12): 9379 x ^ (c1 ^ ((c2 ^ x) v y) ') = 0. [para(2427(a,1),26(a,1)),flip(a)]. given #760 (T,wt=12): 9411 ((x ^ y) v (y ^ z)) ^ y ' = 0. [para(33(a,1),221(a,1,1,2,1)),demod(33(5))]. given #761 (A,wt=13): 331 c2 ^ (c1 ^ x) ' != 0 | c1 ^ x = c2. [para(275(a,1),43(a,1)),demod(15(8),312(14)),xx(a)]. given #762 (F,wt=12): 9413 ((x ^ c1) v (c2 ^ y)) ^ c2 ' = 0. [para(255(a,1),221(a,1,1,2,1)),demod(255(9))]. given #763 (F,wt=12): 9414 ((c1 ^ x) v (c2 ^ y)) ^ c2 ' = 0. [para(261(a,1),221(a,1,1,2,1)),demod(261(9))]. given #764 (T,wt=12): 9429 (x v (y ^ z)) ^ (z v x) ' = 0. [para(286(a,1),221(a,1,1,2))]. given #765 (T,wt=12): 9434 (x v (y ^ c1)) ^ (c2 v x) ' = 0. [para(2933(a,1),221(a,1,1,2))]. given #766 (A,wt=14): 332 x v y != 1 | 0 != x | (x v y) ' = x. [para(74(a,1),43(a,1)),demod(15(5),17(5)),flip(b)]. given #767 (F,wt=12): 9515 c1 ^ (x ^ (y v (x ^ c2)) ') = 0. [para(15(a,1),2451(a,1,2,2,1,2))]. given #768 (F,wt=12): 9617 (x ^ y) ' v (x ^ (z v y)) = 1. [para(2475(a,1),13(a,1)),flip(a)]. given #769 (T,wt=12): 9738 (x v y) ' ^ ((z ^ x) v y) = 0. [para(2545(a,1),15(a,1)),flip(a)]. given #770 (T,wt=12): 9743 ((x ^ y) v (z ^ y)) ^ y ' = 0. [para(33(a,1),2545(a,1,2,1))]. given #771 (A,wt=14): 333 x v y != 1 | 0 != y | (x v y) ' = y. [para(76(a,1),43(a,1)),demod(15(5),27(5)),flip(b)]. given #772 (F,wt=12): 9748 (c1 v x) ^ (c2 v (y v x)) ' = 0. [para(180(a,1),2545(a,1,1,1)),demod(14(5))]. given #773 (F,wt=12): 9750 ((x ^ c2) v (y ^ c1)) ^ c2 ' = 0. [para(255(a,1),2545(a,1,2,1))]. given #774 (T,wt=12): 9751 ((x ^ c2) v (c1 ^ y)) ^ c2 ' = 0. [para(261(a,1),2545(a,1,2,1))]. given #775 (T,wt=12): 9830 x v ((y ^ x) v (z ^ x)) ' = 1. [para(2548(a,1),109(a,1)),flip(a)]. given #776 (A,wt=18): 334 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z)) ' = x. [para(93(a,1),43(a,1)),demod(15(5),283(5)),flip(a)]. given #777 (F,wt=12): 9836 c2 v ((x ^ c2) v (y ^ c1)) ' = 1. [para(2548(a,1),257(a,1)),flip(a)]. given #778 (F,wt=12): 9838 c2 v ((x ^ c2) v (c1 ^ y)) ' = 1. [para(2548(a,1),264(a,1)),flip(a)]. low water: id=10572, wt=20 given #779 (T,wt=12): 9882 c2 v ((x ^ c1) v (y ^ c2)) ' = 1. [para(2573(a,1),257(a,1)),flip(a)]. given #780 (T,wt=12): 9885 c2 v ((c1 ^ x) v (y ^ c2)) ' = 1. [para(2573(a,1),264(a,1)),flip(a)]. given #781 (A,wt=13): 339 x ' ^ (y v x) != 0 | y v x = x. [para(335(a,1),21(a,1)),demod(312(10)),flip(c),xx(a)]. given #782 (F,wt=12): 9914 ((c2 v x) ^ (c1 v y)) v c1 ' = 1. [para(180(a,1),236(a,1,1,2,1)),demod(180(9))]. given #783 (F,wt=12): 9915 ((x v c2) ^ (c1 v y)) v c1 ' = 1. [para(183(a,1),236(a,1,1,2,1)),demod(183(9))]. given #784 (T,wt=12): 9937 (x ^ (y v c2)) v (c1 ^ x) ' = 1. [para(3218(a,1),236(a,1,1,2))]. given #785 (T,wt=12): 10103 (x ^ c2) v (c1 ^ (y ^ x)) ' = 1. [para(245(a,1),2335(a,1,2)),demod(13(7))]. given #786 (A,wt=14): 341 x v (y v (y v ((x v y) ^ z)) ') = 1. [para(32(a,1),335(a,1,2)),demod(13(6),14(6))]. given #787 (F,wt=12): 10169 c1 ' v ((c2 v x) ^ (c1 v y)) = 1. [para(146(a,1),2710(a,1,2))]. given #788 (F,wt=12): 10228 c1 ' v ((c2 v x) ^ (y v c1)) = 1. [para(146(a,1),2739(a,1,2))]. given #789 (T,wt=12): 10272 c2 ' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(195(a,1),2763(a,1,2))]. given #790 (T,wt=12): 10318 (x v y) ' ^ (x v (z ^ y)) = 0. [para(2780(a,1),15(a,1)),flip(a)]. given #791 (A,wt=15): 342 (x v y) ^ y ' != 0 | (x v y) ' = y '. [para(335(a,1),43(a,1)),xx(a)]. given #792 (F,wt=12): 10426 c2 ' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(195(a,1),2816(a,1,2))]. given #793 (F,wt=12): 10480 (c1 v (x ^ y)) ^ (x v c2) ' = 0. [para(31(a,1),2846(a,1,2,1)),demod(13(3))]. given #794 (T,wt=12): 10481 (c1 v (x ^ y)) ^ (y v c2) ' = 0. [para(109(a,1),2846(a,1,2,1)),demod(13(3))]. given #795 (T,wt=12): 10542 (c1 ^ x) ' v ((c2 v y) ^ x) = 1. [para(2932(a,1),13(a,1)),flip(a)]. given #796 (A,wt=13): 345 x ' v (y ^ x) != 1 | y ^ x = x. [para(336(a,1),21(b,1)),demod(312(10)),flip(c),xx(b)]. given #797 (F,wt=12): 10543 (x ^ (c2 v y)) v (c1 ^ x) ' = 1. [para(15(a,1),2932(a,1,1))]. given #798 (F,wt=12): 10547 ((c2 v x) ^ (y v c1)) v c1 ' = 1. [para(27(a,1),2932(a,1,2,1))]. given #799 (T,wt=12): 10549 ((c2 v x) ^ (c2 v y)) v c1 ' = 1. [para(180(a,1),2932(a,1,2,1))]. given #800 (T,wt=12): 10550 ((c2 v x) ^ (y v c2)) v c1 ' = 1. [para(183(a,1),2932(a,1,2,1))]. given #801 (A,wt=14): 347 x ^ (y ^ (y ^ ((x ^ y) v z)) ') = 0. [para(30(a,1),336(a,1,2)),demod(15(6),16(6))]. given #802 (F,wt=12): 10581 c1 ^ ((c2 v x) ^ (c2 v y)) ' = 0. [para(2934(a,1),185(a,1)),flip(a)]. given #803 (F,wt=12): 10582 c1 ^ ((c2 v x) ^ (y v c2)) ' = 0. [para(2934(a,1),203(a,1)),flip(a)]. given #804 (T,wt=12): 10588 c1 ^ ((x v c2) ^ (c2 v y)) ' = 0. [para(2947(a,1),203(a,1)),flip(a)]. given #805 (T,wt=12): 10597 (x ^ c1) ' v (x ^ (c2 v y)) = 1. [para(2960(a,1),13(a,1)),flip(a)]. given #806 (A,wt=13): 348 (x ^ y) v y ' != 1 | x ^ y = y. [para(336(a,1),43(b,1)),demod(312(10)),flip(c),xx(b)]. given #807 (F,wt=12): 10613 (c1 ^ x) ' v ((y v c2) ^ x) = 1. [para(2985(a,1),13(a,1)),flip(a)]. given #808 (F,wt=12): 10617 ((x v c2) ^ (y v c1)) v c1 ' = 1. [para(27(a,1),2985(a,1,2,1))]. given #809 (T,wt=12): 10619 ((x v c2) ^ (c2 v y)) v c1 ' = 1. [para(180(a,1),2985(a,1,2,1))]. given #810 (T,wt=12): 10620 ((x v c2) ^ (y v c2)) v c1 ' = 1. [para(183(a,1),2985(a,1,2,1))]. given #811 (A,wt=13): 349 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(16(a,1),96(a,1,2)),demod(15(8))]. given #812 (F,wt=12): 10648 c1 ^ ((x v c2) ^ (y v c2)) ' = 0. [para(2987(a,1),203(a,1)),flip(a)]. given #813 (F,wt=12): 10691 (x ^ c1) ' v (x ^ (y v c2)) = 1. [para(3014(a,1),13(a,1)),flip(a)]. given #814 (T,wt=12): 10747 (c2 v x) ' ^ ((y ^ c1) v x) = 0. [para(3067(a,1),15(a,1)),flip(a)]. given #815 (T,wt=12): 10751 ((x ^ c1) v (y ^ c2)) ^ c2 ' = 0. [para(33(a,1),3067(a,1,2,1))]. given #816 (A,wt=18): 350 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1 ' = x ^ c2. [para(96(a,1),21(b,1))]. given #817 (F,wt=12): 10753 ((x ^ c1) v (y ^ c1)) ^ c2 ' = 0. [para(255(a,1),3067(a,1,2,1))]. given #818 (F,wt=12): 10754 ((x ^ c1) v (c1 ^ y)) ^ c2 ' = 0. [para(261(a,1),3067(a,1,2,1))]. given #819 (T,wt=12): 10786 c2 v ((x ^ c1) v (y ^ c1)) ' = 1. [para(3069(a,1),257(a,1)),flip(a)]. given #820 (T,wt=12): 10787 c2 v ((x ^ c1) v (c1 ^ y)) ' = 1. [para(3069(a,1),264(a,1)),flip(a)]. given #821 (A,wt=20): 354 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 #822 (F,wt=12): 10793 c2 v ((c1 ^ x) v (y ^ c1)) ' = 1. [para(3085(a,1),264(a,1)),flip(a)]. given #823 (F,wt=12): 10822 (c2 ^ x) v (x ^ (y ^ c1)) ' = 1. [para(15(a,1),3120(a,1,2,1,2))]. given #824 (T,wt=12): 10847 (x v c2) ' ^ (x v (y ^ c1)) = 0. [para(3126(a,1),15(a,1)),flip(a)]. given #825 (T,wt=12): 10980 (x v (c1 ^ y)) ^ (c2 v x) ' = 0. [para(13(a,1),3215(a,1,1))]. given #826 (A,wt=20): 355 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y) ' = z. [para(13(a,1),44(b,1,1))]. given #827 (F,wt=12): 10981 (c2 v x) ' ^ ((c1 ^ y) v x) = 0. [para(3215(a,1),15(a,1)),flip(a)]. given #828 (F,wt=12): 10984 ((c1 ^ x) v (y ^ c2)) ^ c2 ' = 0. [para(33(a,1),3215(a,1,2,1))]. given #829 (T,wt=12): 10986 ((c1 ^ x) v (y ^ c1)) ^ c2 ' = 0. [para(255(a,1),3215(a,1,2,1))]. given #830 (T,wt=12): 10987 ((c1 ^ x) v (c1 ^ y)) ^ c2 ' = 0. [para(261(a,1),3215(a,1,2,1))]. given #831 (A,wt=26): 356 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z)) ' = u. [para(14(a,1),44(a,1,2))]. given #832 (F,wt=12): 11010 c2 v ((c1 ^ x) v (c1 ^ y)) ' = 1. [para(3217(a,1),264(a,1)),flip(a)]. given #833 (F,wt=12): 11023 (x v c2) ' ^ (x v (c1 ^ y)) = 0. [para(3248(a,1),15(a,1)),flip(a)]. given #834 (T,wt=12): 11116 (x ^ c2) v (c1 ^ (x ^ y)) ' = 1. [para(254(a,1),3323(a,1,2,1))]. given #835 (T,wt=12): 11159 (c1 v x) ^ (x v (y v c2)) ' = 0. [para(119(a,1),3384(a,1,2,1,2))]. given #836 (A,wt=20): 357 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y) ' = z. [para(15(a,1),44(b,1))]. given #837 (F,wt=12): 11195 (c1 v (c2 ^ x)) ^ (c2 v y) ' = 0. [para(31(a,1),3468(a,1,2,1))]. given #838 (F,wt=12): 11196 (c1 v (x ^ c2)) ^ (c2 v y) ' = 0. [para(109(a,1),3468(a,1,2,1))]. given #839 (T,wt=12): 11210 x v (c2 v ((c1 v x) ^ y) ') = 1. [para(15(a,1),3744(a,1,2,2,1))]. given #840 (T,wt=12): 11306 (c2 ^ (c1 v x)) v (c1 ^ y) ' = 1. [para(29(a,1),4233(a,1,2,1))]. given #841 (A,wt=18): 358 x v y != 1 | y ^ z != 0 | (x v y) ' = y ^ z. [para(18(a,1),44(a,1,2)),demod(26(6),104(6))]. given #842 (F,wt=12): 11307 (c2 ^ (x v c1)) v (c1 ^ y) ' = 1. [para(104(a,1),4233(a,1,2,1))]. given #843 (F,wt=12): 11337 (x v y) ' ^ ((y ^ z) v x) = 0. [para(4280(a,1),15(a,1)),flip(a)]. given #844 (T,wt=12): 11360 (x v y) ' ^ ((z ^ y) v x) = 0. [para(4283(a,1),15(a,1)),flip(a)]. given #845 (T,wt=12): 11404 (x v c2) ' ^ ((y ^ c1) v x) = 0. [para(4287(a,1),15(a,1)),flip(a)]. given #846 (A,wt=18): 359 x v y != 1 | x v y != 0 | (x v y) ' = x v y. [para(35(a,1),44(b,1)),demod(76(2),74(2))]. given #847 (F,wt=12): 11471 (x v c2) ' ^ ((c1 ^ y) v x) = 0. [para(4289(a,1),15(a,1)),flip(a)]. given #848 (F,wt=12): 11505 (x v y) ' ^ (y v (x ^ z)) = 0. [para(4441(a,1),15(a,1)),flip(a)]. given #849 (T,wt=12): 11540 x ' ^ ((x ^ y) v (x ^ z)) = 0. [para(18(a,1),4443(a,1,1,1))]. given #850 (T,wt=12): 11544 x ' ^ ((x ^ y) v (z ^ x)) = 0. [para(33(a,1),4443(a,1,1,1))]. given #851 (A,wt=26): 361 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z) ' = y v u. [para(25(a,1),44(a,1,2))]. given #852 (F,wt=12): 11548 c2 ' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(255(a,1),4443(a,1,1,1))]. given #853 (F,wt=12): 11549 c2 ' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(261(a,1),4443(a,1,1,1))]. given #854 (T,wt=12): 11735 (x ^ y) ' v ((y v z) ^ x) = 1. [para(4593(a,1),13(a,1)),flip(a)]. given #855 (T,wt=12): 11759 (x ^ y) ' v ((z v y) ^ x) = 1. [para(4597(a,1),13(a,1)),flip(a)]. given #856 (A,wt=20): 362 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x) ' = z. [para(25(a,1),44(a,1))]. given #857 (F,wt=12): 11791 (x ^ c1) ' v ((c2 v y) ^ x) = 1. [para(4599(a,1),13(a,1)),flip(a)]. given #858 (F,wt=12): 11804 (x ^ c1) ' v ((y v c2) ^ x) = 1. [para(4601(a,1),13(a,1)),flip(a)]. given #859 (T,wt=12): 11817 (x ^ y) ' v (y ^ (x v z)) = 1. [para(15(a,1),4729(a,1,2))]. given #860 (T,wt=12): 11819 x ' v ((x v y) ^ (x v z)) = 1. [para(17(a,1),4729(a,1,1,1))]. given #861 (A,wt=26): 363 x v (y v (z v u)) != 1 | (y v (x v z)) ^ u != 0 | (x v (y v z)) ' = u. [para(25(a,1),44(b,1,1)),demod(14(2))]. given #862 (F,wt=12): 11823 x ' v ((x v y) ^ (z v x)) = 1. [para(27(a,1),4729(a,1,1,1))]. given #863 (F,wt=12): 11826 c1 ' v ((c1 v x) ^ (c2 v y)) = 1. [para(180(a,1),4729(a,1,1,1))]. given #864 (T,wt=12): 11827 c1 ' v ((c1 v x) ^ (y v c2)) = 1. [para(183(a,1),4729(a,1,1,1))]. given #865 (T,wt=12): 12182 (x v c2) ' ^ (c1 v (c2 ^ y)) = 0. [para(5507(a,1),15(a,1)),flip(a)]. given #866 (A,wt=26): 365 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 #867 (F,wt=12): 12221 (x v c2) ' ^ (c1 v (y ^ c2)) = 0. [para(5511(a,1),15(a,1)),flip(a)]. given #868 (F,wt=12): 12233 (c2 v x) ' ^ (c1 v (x ^ y)) = 0. [para(5523(a,1),15(a,1)),flip(a)]. given #869 (T,wt=12): 12257 (c2 v x) ' ^ (c1 v (y ^ x)) = 0. [para(5529(a,1),15(a,1)),flip(a)]. given #870 (T,wt=12): 12291 (x ^ c1) ' v (c2 ^ (c1 v y)) = 1. [para(6504(a,1),13(a,1)),flip(a)]. given #871 (A,wt=22): 366 x v (y v z) != 1 | y v z != 0 | (y v z) ' = x v (y v z). [para(27(a,1),44(b,1)),demod(297(3),295(3))]. given #872 (F,wt=12): 12317 (x ^ c1) ' v (c2 ^ (y v c1)) = 1. [para(6509(a,1),13(a,1)),flip(a)]. given #873 (F,wt=12): 12328 (c1 ^ x) ' v (c2 ^ (x v y)) = 1. [para(6529(a,1),13(a,1)),flip(a)]. given #874 (T,wt=12): 12350 (c1 ^ x) ' v (c2 ^ (y v x)) = 1. [para(6534(a,1),13(a,1)),flip(a)]. given #875 (T,wt=12): 12409 (x ^ c1) ' v (c2 ^ (x v y)) = 1. [para(6819(a,1),13(a,1)),flip(a)]. given #876 (A,wt=18): 368 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1) ' = c2. [para(113(a,1),44(a,1,2)),demod(15(8))]. given #877 (F,wt=12): 12422 (x ^ c1) ' v (c2 ^ (y v x)) = 1. [para(6826(a,1),13(a,1)),flip(a)]. given #878 (F,wt=12): 12683 (x ^ y) ' v (y ^ (z v x)) = 1. [para(15(a,1),8540(a,1,2))]. given #879 (T,wt=12): 12684 x ' v ((y v x) ^ (x v z)) = 1. [para(17(a,1),8540(a,1,1,1))]. given #880 (T,wt=12): 12688 x ' v ((y v x) ^ (z v x)) = 1. [para(27(a,1),8540(a,1,1,1))]. given #881 (A,wt=19): 369 (x v y) ^ (y ' v z) != 0 | (x v y) ' = y ' v z. [para(88(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #882 (F,wt=12): 12691 c1 ' v ((x v c1) ^ (c2 v y)) = 1. [para(180(a,1),8540(a,1,1,1))]. given #883 (F,wt=12): 12692 c1 ' v ((x v c1) ^ (y v c2)) = 1. [para(183(a,1),8540(a,1,1,1))]. given #884 (T,wt=12): 12899 x ' ^ ((y ^ x) v (x ^ z)) = 0. [para(9411(a,1),15(a,1)),flip(a)]. given #885 (T,wt=12): 12915 c2 ' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(9413(a,1),15(a,1)),flip(a)]. given #886 (A,wt=23): 370 x v (y v ((x v y) ' ^ z)) != 1 | (x v y) ' ^ z = (x v y) '. [para(91(a,1),44(b,1)),flip(c),xx(b)]. given #887 (F,wt=12): 12937 (x v y) ' ^ (y v (z ^ x)) = 0. [para(9429(a,1),15(a,1)),flip(a)]. given #888 (F,wt=12): 12987 (c2 v x) ' ^ (x v (y ^ c1)) = 0. [para(9434(a,1),15(a,1)),flip(a)]. given #889 (T,wt=12): 13037 x ' ^ ((y ^ x) v (z ^ x)) = 0. [para(33(a,1),9738(a,1,1,1))]. given #890 (T,wt=12): 13039 c2 ' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(255(a,1),9738(a,1,1,1))]. given #891 (A,wt=19): 371 (x v y) ^ (z v y ') != 0 | (x v y) ' = z v y '. [para(98(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #892 (F,wt=12): 13040 c2 ' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(261(a,1),9738(a,1,1,1))]. given #893 (F,wt=12): 13133 c1 ' v ((x v c2) ^ (c1 v y)) = 1. [para(9915(a,1),13(a,1)),flip(a)]. given #894 (T,wt=12): 13141 (c1 ^ x) ' v (x ^ (y v c2)) = 1. [para(9937(a,1),13(a,1)),flip(a)]. given #895 (T,wt=12): 13182 c1 ' v ((c2 v x) ^ (c2 v y)) = 1. [para(117(a,1),10169(a,1,2,2))]. given #896 (A,wt=15): 372 (x v y) ^ x ' != 0 | (x v y) ' = x '. [para(98(a,1),44(a,1)),xx(a)]. given #897 (F,wt=12): 13183 c1 ' v ((c2 v x) ^ (y v c2)) = 1. [para(119(a,1),10169(a,1,2,2))]. given #898 (F,wt=12): 13191 c1 ' v ((x v c2) ^ (y v c1)) = 1. [para(13(a,1),10228(a,1,2,1))]. given #899 (T,wt=12): 13197 c2 ' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(67(a,1),10272(a,1,2,2))]. given #900 (T,wt=12): 13231 c2 ' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(15(a,1),10426(a,1,2,1))]. given #901 (A,wt=32): 373 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 #902 (F,wt=12): 13242 (x v c2) ' ^ (c1 v (x ^ y)) = 0. [para(10480(a,1),15(a,1)),flip(a)]. given #903 (F,wt=12): 13252 (x v c2) ' ^ (c1 v (y ^ x)) = 0. [para(10481(a,1),15(a,1)),flip(a)]. given #904 (T,wt=12): 13254 (c1 ^ x) ' v (x ^ (c2 v y)) = 1. [para(15(a,1),10542(a,1,2))]. given #905 (T,wt=12): 13345 c1 ' v ((x v c2) ^ (c2 v y)) = 1. [para(180(a,1),10613(a,1,1,1))]. given #906 (A,wt=23): 374 x v (y v (z ^ (x v y) ')) != 1 | z ^ (x v y) ' = (x v y) '. [para(101(a,1),44(b,1)),flip(c),xx(b)]. given #907 (F,wt=12): 13346 c1 ' v ((x v c2) ^ (y v c2)) = 1. [para(183(a,1),10613(a,1,1,1))]. given #908 (F,wt=12): 13384 c2 ' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(255(a,1),10747(a,1,1,1))]. given #909 (T,wt=12): 13385 c2 ' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(261(a,1),10747(a,1,1,1))]. given #910 (T,wt=12): 13418 (c2 v x) ' ^ (x v (c1 ^ y)) = 0. [para(10980(a,1),15(a,1)),flip(a)]. given #911 (A,wt=23): 375 x v (y v (x v (y v z)) ') != 1 | (x v (y v z)) ' = (x v y) '. [para(142(a,1),44(b,1)),demod(14(2),14(14)),flip(c),xx(b)]. given #912 (F,wt=12): 13422 c2 ' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(261(a,1),10981(a,1,1,1))]. given #913 (F,wt=12): 13447 (c2 v x) ' ^ (c1 v (c2 ^ y)) = 0. [para(11195(a,1),15(a,1)),flip(a)]. given #914 (T,wt=12): 13456 (c2 v x) ' ^ (c1 v (y ^ c2)) = 0. [para(11196(a,1),15(a,1)),flip(a)]. given #915 (T,wt=12): 13468 (c1 ^ x) ' v (c2 ^ (c1 v y)) = 1. [para(11306(a,1),13(a,1)),flip(a)]. given #916 (A,wt=36): 376 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 #917 (F,wt=12): 13478 (c1 ^ x) ' v (c2 ^ (y v c1)) = 1. [para(11307(a,1),13(a,1)),flip(a)]. given #918 (F,wt=13): 402 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(103(a,1),16(a,1,1)),flip(a)]. given #919 (T,wt=13): 406 x ^ (y ^ (z v (u v x))) = y ^ x. [para(103(a,1),26(a,1,2)),flip(a)]. given #920 (T,wt=13): 411 x v ((y ^ (z ^ x)) v u) = x v u. [para(111(a,1),14(a,1,1)),flip(a)]. given #921 (A,wt=23): 377 x v (y v (z v (x v y)) ') != 1 | (z v (x v y)) ' = (x v y) '. [para(152(a,1),44(b,1)),flip(c),xx(b)]. given #922 (F,wt=13): 415 x v (y v (z ^ (u ^ x))) = y v x. [para(111(a,1),25(a,1,2)),flip(a)]. given #923 (F,wt=13): 420 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x. [para(66(a,1),111(a,1,2,2))]. given #924 (T,wt=13): 422 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2. [para(96(a,1),111(a,1,2,2))]. given #925 (T,wt=13): 425 c1 v (x v (c2 v y)) = x v (c2 v y). [para(117(a,1),25(a,1,2)),flip(a)]. given #926 (A,wt=28): 378 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 #927 (F,wt=13): 426 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(117(a,1),28(a,1,2,2))]. given #928 (F,wt=13): 430 c2 v (x v (y v c1)) = c2 v (x v y). [para(14(a,1),118(a,1,2)),demod(13(8))]. given #929 (T,wt=13): 441 (x v c1) ^ (y v (x v c2)) = x v c1. [para(118(a,1),103(a,1,2,2))]. given #930 (T,wt=13): 449 x v (x v y) ' != 1 | x v y = x. [para(142(a,1),45(b,1)),demod(13(3),312(11)),xx(b)]. given #931 (A,wt=32): 379 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 #932 (F,wt=11): 13605 c1 ' v (c1 ' v c2 ') ' != 1. [ur(449,b,24,a)]. given #933 (F,wt=12): 13607 (c1 ' v (c1 ' v c2 ') ') ' != 0. [ur(4187,b,13605,a),demod(13(9))]. given #934 (T,wt=13): 452 x v (y v x) ' != 1 | y v x = x. [para(152(a,1),45(b,1)),demod(13(3),312(11)),xx(b)]. given #935 (T,wt=13): 457 c1 v (c2 v x) ' != 1 | c2 v x = c1. [para(186(a,1),45(b,1)),demod(13(5),312(14)),xx(b)]. given #936 (A,wt=22): 380 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 #937 (F,wt=13): 458 c1 v (x v c2) ' != 1 | x v c2 = c1. [para(188(a,1),45(b,1)),demod(13(5),312(14)),xx(b)]. given #938 (F,wt=13): 461 (x v y) ^ y ' != 0 | x v y = y. [para(335(a,1),45(a,1)),demod(312(10)),flip(c),xx(a)]. given #939 (T,wt=13): 466 c1 v (x v (y v c2)) = x v (y v c2). [para(119(a,1),25(a,1,2)),flip(a)]. given #940 (T,wt=13): 467 (x v c1) ^ (x v (y v c2)) = x v c1. [para(119(a,1),28(a,1,2,2))]. given #941 (A,wt=19): 381 (x v y) ^ (y ^ z) ' != 0 | (x v y) ' = (y ^ z) '. [para(191(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #942 (F,wt=13): 472 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z. [para(200(a,1),16(a,1,1)),flip(a)]. given #943 (F,wt=13): 474 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1. [para(200(a,1),26(a,1,2)),flip(a)]. given #944 (T,wt=13): 477 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z. [para(202(a,1),16(a,1,1)),flip(a)]. given #945 (T,wt=13): 479 c1 ^ (x ^ (y v (z v c2))) = x ^ c1. [para(202(a,1),26(a,1,2)),flip(a)]. given #946 (A,wt=19): 382 (x v y) ^ (z ^ y) ' != 0 | (x v y) ' = (z ^ y) '. [para(224(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #947 (F,wt=13): 481 c2 v ((x ^ (y ^ c1)) v z) = c2 v z. [para(262(a,1),14(a,1,1)),flip(a)]. given #948 (F,wt=13): 484 c2 v (x v (y ^ (z ^ c1))) = x v c2. [para(262(a,1),25(a,1,2)),flip(a)]. given #949 (T,wt=13): 541 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z. [para(267(a,1),14(a,1,1)),flip(a)]. given #950 (T,wt=13): 544 c2 v (x v (y ^ (c1 ^ z))) = x v c2. [para(267(a,1),25(a,1,2)),flip(a)]. given #951 (A,wt=15): 383 (x v c2) ^ c1 ' != 0 | (x v c2) ' = c1 '. [para(232(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #952 (F,wt=13): 547 c2 v (x v (c1 v y)) = c2 v (x v y). [para(429(a,1),14(a,1,1)),demod(14(3),14(7)),flip(a)]. given #953 (F,wt=13): 554 (x v c1) ^ (y v (c2 v x)) = x v c1. [para(429(a,1),103(a,1,2,2))]. given #954 (T,wt=13): 1858 c1 ' ^ (x v c2) != 0 | x v c2 = c1. [para(1847(a,1),21(a,1)),demod(312(13)),flip(c),xx(a)]. given #955 (T,wt=13): 1860 (x v c2) ^ c1 ' != 0 | x v c2 = c1. [para(1847(a,1),45(a,1)),demod(312(13)),flip(c),xx(a)]. given #956 (A,wt=19): 384 (x v c2) ^ (y v c1 ') != 0 | (x v c2) ' = y v c1 '. [para(238(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #957 (F,wt=13): 1894 x ' ^ (x v y) != 0 | x v y = x. [para(88(a,1),83(a,1)),demod(312(10)),flip(c),xx(a)]. given #958 (F,wt=13): 1899 c1 ' ^ (c2 v x) != 0 | c2 v x = c1. [para(239(a,1),83(a,1)),demod(312(13)),flip(c),xx(a)]. given #959 (T,wt=13): 1980 c2 ' v (x ^ c1) != 1 | x ^ c1 = c2. [para(1953(a,1),21(b,1)),demod(312(13)),flip(c),xx(b)]. given #960 (T,wt=13): 1981 (x ^ c1) v c2 ' != 1 | x ^ c1 = c2. [para(1953(a,1),43(b,1)),demod(312(13)),flip(c),xx(b)]. given #961 (A,wt=15): 385 (c2 v x) ^ c1 ' != 0 | (c2 v x) ' = c1 '. [para(238(a,1),44(a,1)),xx(a)]. given #962 (F,wt=13): 2065 x ' v (x ^ y) != 1 | x ^ y = x. [para(91(a,1),95(b,1)),demod(312(10)),flip(c),xx(b)]. given #963 (F,wt=13): 2069 c2 ' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(158(a,1),95(b,1)),demod(312(13)),flip(c),xx(b)]. given #964 (T,wt=13): 2236 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(15(a,1),105(a,1,2,2,2))]. given #965 (T,wt=13): 2243 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x. [para(105(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #966 (A,wt=19): 387 (x v c2) ^ (c1 ' v y) != 0 | (x v c2) ' = c1 ' v y. [para(239(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #967 (F,wt=13): 2367 (x v y) ^ (z v (y v x)) = x v y. [para(13(a,1),107(a,1,2)),demod(14(3))]. given #968 (F,wt=13): 2642 x v (y v (z ^ (y v x))) = x v y. [para(13(a,1),110(a,1,2,2,2))]. given #969 (T,wt=13): 2834 x v (c2 v (y ^ (x v c1))) = x v c2. [para(129(a,1),111(a,1,2,2)),demod(14(6))]. given #970 (T,wt=13): 2850 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(17(a,1),184(a,1,1))]. given #971 (A,wt=18): 389 x v c2 != 1 | c1 ^ y != 0 | (x v c2) ' = c1 ^ y. [para(261(a,1),44(a,1,2)),demod(26(9),203(9))]. given #972 (F,wt=11): 13684 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(2850(a,1),51(a,2,2)),demod(74(8),3854(7),74(6),108(10))]. given #973 (F,wt=11): 13685 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(2850(a,1),60(a,1,2)),demod(108(5)),flip(a)]. given #974 (T,wt=11): 13708 x v (c2 ^ (c1 v x)) = x v c1. [para(2850(a,1),2642(a,1,2))]. given #975 (T,wt=11): 13715 x v (c2 ^ (x v c1)) = x v c1. [para(13(a,1),13708(a,1,2,2))]. given #976 (A,wt=23): 390 (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(97(2)),xx(a)]. given #977 (F,wt=13): 2855 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(27(a,1),184(a,1,1))]. low water: id=10967, wt=19 given #978 (F,wt=13): 2883 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(15(a,1),115(a,1,2)),demod(16(3))]. given #979 (T,wt=13): 3037 (x v (y v z)) ^ (y v x) = x v y. [para(120(a,1),15(a,1)),flip(a)]. given #980 (T,wt=13): 3045 (c1 v x) ^ (x v (c2 v y)) = x v c1. [para(117(a,1),120(a,1,2,2))]. given #981 (A,wt=19): 391 (x v c2) ^ (y ^ c1) ' != 0 | (x v c2) ' = (y ^ c1) '. [para(258(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #982 (F,wt=13): 3047 (c1 v x) ^ (x v (y v c2)) = x v c1. [para(119(a,1),120(a,1,2,2))]. given #983 (F,wt=13): 3105 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1. [para(260(a,1),103(a,1,2,2)),demod(16(6))]. given #984 (T,wt=13): 3154 (x v (y v z)) ^ (z v x) = z v x. [para(121(a,1),15(a,1)),flip(a)]. given #985 (T,wt=13): 3274 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(25(a,1),286(a,1,1))]. given #986 (A,wt=19): 392 (x v c2) ^ (c1 ^ y) ' != 0 | (x v c2) ' = (c1 ^ y) '. [para(275(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #987 (F,wt=13): 3280 x ^ (c1 ^ ((x ^ c2) v y)) = x ^ c1. [para(96(a,1),286(a,1,2)),demod(15(6),16(6),96(10))]. given #988 (F,wt=13): 3302 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(287(a,1),31(a,2)),demod(16(3),3297(6))]. given #989 (T,wt=13): 3400 (x ^ (y ^ z)) v (u v y) = u v y. [para(26(a,1),299(a,1,1))]. given #990 (T,wt=13): 3406 c2 v (x v ((x v c1) ^ y)) = c2 v x. [para(429(a,1),299(a,1,2)),demod(25(6),13(5),429(10))]. given #991 (A,wt=22): 393 x v y != 1 | z ^ (x v y) != 0 | (x v y) ' = z ^ (x v y). [para(71(a,1),44(b,1)),demod(110(4))]. given #992 (F,wt=11): 13779 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(18(a,1),3406(a,2)),demod(13(7),31(10))]. given #993 (F,wt=11): 13780 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(33(a,1),3406(a,2)),demod(13(7),109(10))]. given #994 (T,wt=11): 13789 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(15(a,1),13779(a,1,2))]. given #995 (T,wt=11): 13797 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(15(a,1),13780(a,1,2))]. given #996 (A,wt=27): 394 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 #997 (F,wt=13): 3418 (x ^ (c1 ^ y)) v (c2 ^ x) = c2 ^ x. [para(260(a,1),299(a,1,2)),demod(16(3),260(11))]. given #998 (F,wt=13): 3476 x ^ (y v (z v (u v (x v v)))) = x. [para(14(a,1),301(a,1,2,2))]. given #999 (T,wt=13): 3493 c1 ^ (x v (y v (z v (c2 v u)))) = c1. [para(301(a,1),203(a,1,2)),demod(183(4),14(5)),flip(a)]. given #1000 (T,wt=13): 3498 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(16(a,1),305(a,1,2,2))]. given #1001 (A,wt=24): 395 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y) ' = y v z. [para(74(a,1),44(a,1,2))]. given #1002 (F,wt=13): 3515 c2 v (x ^ (y ^ (z ^ (c1 ^ u)))) = c2. [para(305(a,1),257(a,1,2)),demod(255(4),16(5)),flip(a)]. given #1003 (F,wt=13): 3524 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1. [para(351(a,1),80(a,1,2,2)),demod(16(6))]. given #1004 (T,wt=13): 3613 x ^ (y v (z v (u v (v v x)))) = x. [para(14(a,1),401(a,1,2,2,2))]. given #1005 (T,wt=13): 3641 c1 ^ (x v (y v (z v (u v c2)))) = c1. [para(401(a,1),203(a,1,2)),demod(183(4)),flip(a)]. given #1006 (A,wt=24): 396 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z) ' = y v z. [para(76(a,1),44(a,1,2))]. given #1007 (F,wt=13): 3653 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(16(a,1),413(a,1,2,2,2))]. given #1008 (F,wt=13): 3692 c2 v (x ^ (y ^ (z ^ (u ^ c1)))) = c2. [para(413(a,1),257(a,1,2)),demod(255(4)),flip(a)]. given #1009 (T,wt=13): 3708 (c1 v x) ^ (c2 v (x v y)) = c1 v x. [para(117(a,1),126(a,1,2))]. given #1010 (T,wt=13): 3738 x v (c2 v (y ^ (c1 v x))) = x v c2. [para(468(a,1),111(a,1,2,2)),demod(14(6))]. given #1011 (A,wt=14): 397 x v y != 1 | 0 != y | (y v x) ' = y. [para(76(a,1),44(a,1)),demod(15(5),17(5)),flip(b)]. given #1012 (F,wt=13): 3753 (x v (c2 v y)) ^ (c1 v x) = c1 v x. [para(468(a,1),286(a,1,2)),demod(14(3),468(11))]. given #1013 (F,wt=13): 3852 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(18(a,1),549(a,1,2)),demod(13(4),15(6),13(10))]. given #1014 (T,wt=13): 3854 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(33(a,1),549(a,1,2)),demod(13(4),15(6),13(10))]. given #1015 (T,wt=13): 3858 c2 v (x v (y ^ (x v c1))) = c2 v x. [para(549(a,1),111(a,1,2,2)),demod(14(6))]. given #1016 (A,wt=19): 400 (x v y ') ^ (z v y) != 0 | (x v y ') ' = z v y. [para(335(a,1),44(a,1,2)),demod(97(2)),xx(a)]. given #1017 (F,wt=13): 3873 (c2 v (x v y)) ^ (x v c1) = x v c1. [para(549(a,1),286(a,1,2)),demod(14(3),549(11))]. given #1018 (F,wt=13): 3889 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(14(a,1),2176(a,1,1))]. given #1019 (T,wt=13): 3922 (x v (y v z)) ^ (z v y) = z v y. [para(298(a,1),2176(a,1,2)),demod(298(7))]. given #1020 (T,wt=13): 3926 (x v (y v c2)) ^ (c1 v y) = c1 v y. [para(468(a,1),2176(a,1,2)),demod(468(11))]. given #1021 (A,wt=15): 403 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(103(a,1),16(a,1)),flip(a)]. given #1022 (F,wt=13): 3929 (x v (c2 v y)) ^ (y v c1) = y v c1. [para(549(a,1),2176(a,1,2)),demod(549(11))]. given #1023 (F,wt=13): 3940 c2 v (x v (y ^ (c1 v x))) = c2 v x. [para(2383(a,1),111(a,1,2,2)),demod(14(6))]. given #1024 (T,wt=13): 3953 (c1 v x) ^ (y v (c2 v x)) = c1 v x. [para(2383(a,1),2176(a,1,2)),demod(15(6),2383(11))]. given #1025 (T,wt=13): 3974 (x ^ (y ^ z)) v (u v z) = u v z. [para(16(a,1),2549(a,1,1))]. given #1026 (A,wt=18): 404 x v (y v z) != 1 | 0 != z | z ' = x v (y v z). [para(103(a,1),21(b,1)),demod(297(3)),flip(b)]. given #1027 (F,wt=13): 4005 (x ^ (y ^ c1)) v (c2 ^ y) = c2 ^ y. [para(260(a,1),2549(a,1,2)),demod(260(11))]. given #1028 (F,wt=13): 4008 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(287(a,1),2549(a,1,2)),demod(287(7))]. given #1029 (T,wt=13): 4066 (x v (c2 v y)) ^ (z ^ c1) = z ^ c1. [para(25(a,1),2933(a,1,1))]. given #1030 (T,wt=13): 4081 (x v (y v c2)) ^ (z ^ c1) = z ^ c1. [para(14(a,1),2986(a,1,1))]. given #1031 (A,wt=15): 405 (x v y) ^ (z v (x v (u v y))) = x v y. [para(25(a,1),103(a,1,2,2))]. given #1032 (F,wt=13): 4093 (x ^ (y ^ c1)) v (z v c2) = z v c2. [para(16(a,1),3070(a,1,1))]. given #1033 (F,wt=13): 4114 (x ^ (c1 ^ y)) v (z v c2) = z v c2. [para(26(a,1),3218(a,1,1))]. given #1034 (T,wt=13): 4236 (c1 ^ (x ^ y)) v (c2 ^ x) = c2 ^ x. [para(4042(a,1),299(a,1,2)),demod(16(3),4042(11))]. given #1035 (T,wt=13): 4246 (x ^ (c1 ^ y)) v (c2 ^ y) = c2 ^ y. [para(4042(a,1),2549(a,1,2)),demod(4042(11))]. given #1036 (A,wt=17): 407 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(31(a,1),103(a,1,2,2))]. given #1037 (F,wt=13): 5434 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x. [para(161(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #1038 (F,wt=13): 6320 x ^ ((y ^ z) v (z ^ x)) = z ^ x. [para(167(a,1),60(a,1,2)),demod(108(4)),flip(a)]. given #1039 (T,wt=13): 6558 x ^ (((x v y) ^ (x v z)) v u) = x. [para(168(a,1),29(a,1)),demod(17(2)),flip(a)]. given #1040 (T,wt=13): 6581 x ^ (((x v y) ^ (z v x)) v u) = x. [para(168(a,1),104(a,1)),demod(27(2)),flip(a)]. low water: id=11584, wt=18 given #1041 (A,wt=21): 408 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(32(a,1),103(a,1,2,2))]. given #1042 (F,wt=13): 6591 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(168(a,1),185(a,1)),demod(180(4)),flip(a)]. given #1043 (F,wt=13): 6593 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(168(a,1),203(a,1)),demod(183(4)),flip(a)]. given #1044 (T,wt=13): 6642 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(25(a,1),6559(a,1,2,1,2))]. given #1045 (T,wt=13): 6643 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(25(a,1),6559(a,1,2))]. given #1046 (A,wt=17): 409 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(34(a,1),103(a,1,2,2)),demod(16(5),16(4))]. given #1047 (F,wt=13): 6683 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(14(a,1),6638(a,1,2,1,2))]. given #1048 (F,wt=13): 6686 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(25(a,1),6638(a,1,2))]. given #1049 (T,wt=13): 6725 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(14(a,1),6639(a,1,2))]. given #1050 (T,wt=13): 6728 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(25(a,1),6639(a,1,2,2,2))]. given #1051 (A,wt=15): 412 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(111(a,1),14(a,1)),flip(a)]. given #1052 (F,wt=13): 6762 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(14(a,1),6682(a,1,2,2,2))]. given #1053 (F,wt=13): 6763 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(14(a,1),6682(a,1,2))]. given #1054 (T,wt=13): 7052 (c2 ^ x) v (x ^ (c1 ^ y)) = c2 ^ x. [para(179(a,1),34(a,1,2))]. given #1055 (T,wt=13): 7174 x ^ (c1 ^ ((c2 ^ x) v y)) = x ^ c1. [para(161(a,1),182(a,1,2)),demod(96(4)),flip(a)]. given #1056 (A,wt=18): 414 1 != x | y ^ (z ^ x) != 0 | x ' = y ^ (z ^ x). [para(111(a,1),21(a,1)),demod(285(5)),flip(a)]. given #1057 (F,wt=13): 7472 x v (c2 v ((x v c1) ^ y)) = x v c2. [para(113(a,1),189(a,2,2)),demod(13(6),117(7))]. given #1058 (F,wt=13): 7754 (c2 ^ x) v (c1 ^ (x ^ y)) = c2 ^ x. [para(260(a,1),190(a,1,2)),demod(34(6),15(7)),flip(a)]. given #1059 (T,wt=13): 8383 (x ^ c2) v (x ^ (c1 ^ y)) = x ^ c2. [para(351(a,1),195(a,1,1)),demod(16(5),13(8),17(9),16(5),13(8)),flip(a)]. given #1060 (T,wt=13): 8389 (c1 ^ (x ^ y)) v (x ^ c2) = c2 ^ x. [para(2849(a,1),195(a,1,1)),demod(16(5),16(9),2236(9),16(5)),flip(a)]. given #1061 (A,wt=15): 416 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(26(a,1),111(a,1,2,2))]. given #1062 (F,wt=13): 8998 c2 v (x v ((c1 v x) ^ y)) = c2 v x. [para(217(a,1),117(a,1)),demod(25(4),117(4)),flip(a)]. given #1063 (F,wt=13): 9541 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(222(a,1),31(a,1)),demod(18(2)),flip(a)]. given #1064 (T,wt=13): 9551 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(222(a,1),109(a,1)),demod(33(2)),flip(a)]. given #1065 (T,wt=13): 9553 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(222(a,1),257(a,1)),demod(255(4)),flip(a)]. given #1066 (A,wt=17): 417 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(28(a,1),111(a,1,2,2)),demod(14(5),14(4))]. given #1067 (F,wt=13): 9554 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(222(a,1),264(a,1)),demod(261(4)),flip(a)]. given #1068 (F,wt=13): 10021 (c2 ^ x) v (x ^ (y ^ c1)) = x ^ c2. [para(67(a,1),244(a,1,2,2))]. given #1069 (T,wt=13): 10046 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(245(a,1),13(a,1)),flip(a)]. given #1070 (T,wt=13): 10528 (x ^ c2) v (c1 ^ (x ^ y)) = c2 ^ x. [para(254(a,1),244(a,1,2))]. given #1071 (A,wt=17): 418 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(29(a,1),111(a,1,2,2))]. given #1072 (F,wt=13): 10533 (c2 ^ x) v (c1 ^ (y ^ x)) = c2 ^ x. [para(254(a,1),250(a,1,2))]. given #1073 (F,wt=13): 10653 (x ^ c2) v (y ^ (c1 ^ x)) = x ^ c2. [para(15(a,1),259(a,1,2)),demod(16(5))]. given #1074 (T,wt=13): 11278 (c1 v x) ^ (y v (x v c2)) = c1 v x. [para(119(a,1),300(a,1,2,2))]. given #1075 (T,wt=13): 11589 (c2 ^ x) v (y ^ (x ^ c1)) = c2 ^ x. [para(67(a,1),304(a,1,2,2))]. given #1076 (A,wt=21): 419 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(30(a,1),111(a,1,2,2))]. given #1077 (F,wt=13): 11607 x ^ ((x ' ^ y) v (x ' ^ z)) = 0. [para(312(a,1),4445(a,1,2)),demod(15(6))]. given #1078 (F,wt=13): 11622 x ^ ((x ' ^ y) v (z ^ x ')) = 0. [para(312(a,1),4450(a,1,2)),demod(15(6))]. given #1079 (T,wt=13): 11899 x v ((x ' v y) ^ (x ' v z)) = 1. [para(312(a,1),4731(a,1,2)),demod(13(6))]. given #1080 (T,wt=13): 11916 x v ((x ' v y) ^ (z v x ')) = 1. [para(312(a,1),4735(a,1,2)),demod(13(6))]. given #1081 (A,wt=18): 421 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x)) ' = x. [para(111(a,1),43(a,1)),demod(15(5),285(5)),flip(a)]. given #1082 (F,wt=13): 12188 (x ^ y) v x ' != 1 | x ^ y = x. [para(91(a,1),314(b,1)),demod(312(10)),flip(c),xx(b)]. given #1083 (F,wt=13): 12189 (c1 ^ x) v c2 ' != 1 | c1 ^ x = c2. [para(158(a,1),314(b,1)),demod(312(13)),flip(c),xx(b)]. given #1084 (T,wt=13): 12526 x ^ (y ^ x) ' != 0 | x ^ y = x. [para(15(a,1),321(a,1,2,1))]. given #1085 (T,wt=13): 12557 x ^ (x ^ y) ' != 0 | y ^ x = x. [para(15(a,1),322(a,1,2,1))]. given #1086 (A,wt=14): 427 c2 v x != 1 | c1 != 0 | (c2 v x) ' = c1. [para(117(a,1),43(a,1)),demod(15(8),180(8))]. given #1087 (F,wt=13): 12558 (x v y) ^ x ' != 0 | x v y = x. [para(17(a,1),322(a,1,2,1)),demod(17(7)),flip(b)]. given #1088 (F,wt=13): 12559 (c2 v x) ^ c1 ' != 0 | c2 v x = c1. [para(180(a,1),322(a,1,2,1)),demod(180(11)),flip(b)]. given #1089 (T,wt=13): 12770 x v ((y v x ') ^ (x ' v z)) = 1. [para(312(a,1),8544(a,1,2)),demod(13(6))]. given #1090 (T,wt=13): 12779 x v ((y v x ') ^ (z v x ')) = 1. [para(312(a,1),8549(a,1,2)),demod(13(6))]. given #1091 (A,wt=24): 428 x v (c2 v y) != 1 | (x v c1) ^ (c2 v y) != 0 | (x v c1) ' = c2 v y. [para(117(a,1),44(a,1,2))]. given #1092 (F,wt=13): 12877 c2 ^ (c1 ^ x) ' != 0 | x ^ c1 = c2. [para(15(a,1),330(a,1,2,1))]. given #1093 (F,wt=13): 12902 x ^ ((y ^ x ') v (x ' ^ z)) = 0. [para(312(a,1),9411(a,1,2)),demod(15(6))]. given #1094 (T,wt=13): 12908 c2 ^ (x ^ c1) ' != 0 | c1 ^ x = c2. [para(15(a,1),331(a,1,2,1))]. given #1095 (T,wt=13): 13068 x ^ ((y ^ x ') v (z ^ x ')) = 0. [para(312(a,1),9743(a,1,2)),demod(15(6))]. given #1096 (A,wt=18): 431 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2 ' = x v c1. [para(118(a,1),21(a,1))]. given #1097 (F,wt=13): 13121 x ' ^ (x v y) != 0 | y v x = x. [para(13(a,1),339(a,1,2))]. given #1098 (F,wt=13): 13280 x ' v (x ^ y) != 1 | y ^ x = x. [para(15(a,1),345(a,1,2))]. given #1099 (T,wt=13): 13341 (x ^ y) v x ' != 1 | y ^ x = x. [para(15(a,1),348(a,1,1))]. given #1100 (T,wt=13): 13381 (x ^ c2) v (c1 ^ (y ^ x)) = x ^ c2. [para(349(a,1),111(a,1,2))]. given #1101 (A,wt=24): 437 x v (y v c2) != 1 | (x v c2) ^ (y v c1) != 0 | (x v c2) ' = y v c1. [para(118(a,1),44(a,1,2))]. given #1102 (F,wt=13): 13589 (x ^ (y ^ c1)) v (y ^ c2) = y ^ c2. [para(422(a,1),13(a,1)),flip(a)]. given #1103 (F,wt=13): 13597 (x v c1) ^ (c2 v (y v x)) = x v c1. [para(13(a,1),426(a,1,2)),demod(14(5))]. given #1104 (T,wt=13): 13598 (x v c1) ^ (c2 v (x v y)) = x v c1. [para(25(a,1),426(a,1,2))]. given #1105 (T,wt=13): 13606 x v (y v x) ' != 1 | x v y = x. [para(13(a,1),449(a,1,2,1))]. given #1106 (A,wt=14): 438 x v c2 != 1 | c1 != 0 | (c2 v x) ' = c1. [para(118(a,1),44(a,1)),demod(15(8),180(8))]. given #1107 (F,wt=13): 13608 x v (x v y) ' != 1 | y v x = x. [para(13(a,1),452(a,1,2,1))]. given #1108 (F,wt=13): 13609 c1 v (x v c2) ' != 1 | c2 v x = c1. [para(13(a,1),457(a,1,2,1))]. given #1109 (T,wt=13): 13610 c1 v (c2 v x) ' != 1 | x v c2 = c1. [para(13(a,1),458(a,1,2,1))]. given #1110 (T,wt=13): 13611 (x v y) ^ x ' != 0 | y v x = x. [para(13(a,1),461(a,1,1))]. given #1111 (A,wt=20): 439 x v (c2 v y) != 1 | c2 ^ (x v y) != 0 | (x v y) ' = c2. [para(118(a,2),44(a,1,2)),demod(429(4),15(8))]. given #1112 (F,wt=13): 13613 x v (c2 v ((c1 v x) ^ y)) = x v c2. [para(466(a,1),189(a,1)),demod(13(5),119(10))]. given #1113 (F,wt=13): 13624 (c1 v x) ^ (c2 v (y v x)) = c1 v x. [para(547(a,1),103(a,1,2))]. given #1114 (T,wt=13): 13630 c1 ' ^ (c2 v x) != 0 | x v c2 = c1. [para(13(a,1),1858(a,1,2))]. given #1115 (T,wt=13): 13631 (c2 v x) ^ c1 ' != 0 | x v c2 = c1. [para(13(a,1),1860(a,1,1))]. given #1116 (A,wt=20): 442 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x ' = y ^ z. [para(16(a,1),45(b,1))]. given #1117 (F,wt=13): 13632 x ' ^ (y v x) != 0 | x v y = x. [para(13(a,1),1894(a,1,2))]. given #1118 (F,wt=13): 13633 c1 ' ^ (x v c2) != 0 | c2 v x = c1. [para(13(a,1),1899(a,1,2))]. given #1119 (T,wt=13): 13634 c2 ' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(15(a,1),1980(a,1,2))]. given #1120 (T,wt=13): 13635 (c1 ^ x) v c2 ' != 1 | x ^ c1 = c2. [para(15(a,1),1981(a,1,1))]. given #1121 (A,wt=20): 443 x v (y v z) != 1 | (x v z) ^ y != 0 | y ' = x v z. [para(25(a,1),45(a,1))]. given #1122 (F,wt=13): 13636 x ' v (y ^ x) != 1 | x ^ y = x. [para(15(a,1),2065(a,1,2))]. given #1123 (F,wt=13): 13637 c2 ' v (x ^ c1) != 1 | c1 ^ x = c2. [para(15(a,1),2069(a,1,2))]. given #1124 (T,wt=13): 13639 c1 ^ (x ^ (y v (x ^ c2))) = c1 ^ x. [para(2236(a,1),66(a,1,2)),demod(66(4)),flip(a)]. given #1125 (T,wt=13): 13682 x ^ (c1 v (c2 ^ (x v y))) = x ^ c2. [para(2850(a,1),49(a,1,2)),demod(164(8)),flip(a)]. given #1126 (A,wt=20): 444 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y) ' = z. [para(26(a,1),45(b,1))]. given #1127 (F,wt=13): 13683 x ^ (c1 v (c2 ^ (y v x))) = x ^ c2. [para(2850(a,1),51(a,1,2)),demod(403(8)),flip(a)]. given #1128 (F,wt=13): 13718 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(13708(a,1),31(a,1,2)),demod(13(3),81(4)),flip(a)]. given #1129 (T,wt=13): 13721 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(13708(a,1),109(a,1,2)),demod(13(3),114(4)),flip(a)]. given #1130 (T,wt=13): 13751 (x v (y v c2)) ^ (c1 v x) = x v c1. [para(119(a,1),3037(a,1,1,2))]. given #1131 (A,wt=22): 445 x v (y v z) != 1 | x v y != 0 | (x v (y v z)) ' = x v y. [para(28(a,1),45(b,1)),demod(13(4),25(4),25(3),14(2),295(3),74(3))]. given #1132 (F,wt=13): 13775 (x ^ (y ^ c1)) v (c2 ^ x) = x ^ c2. [para(67(a,1),3302(a,1,1,2))]. given #1133 (F,wt=13): 13782 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(93(a,1),3406(a,2)),demod(13(9),194(12))]. given #1134 (T,wt=13): 13784 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(111(a,1),3406(a,2)),demod(13(9),411(12))]. given #1135 (T,wt=13): 13791 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(26(a,1),13779(a,1,2))]. given #1136 (A,wt=15): 446 x v (x ' ^ y) != 1 | (x ' ^ y) ' = x. [para(91(a,1),45(b,1)),demod(13(3)),xx(b)]. given #1137 (F,wt=13): 13794 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(285(a,1),13779(a,1,2))]. given #1138 (F,wt=13): 13799 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(26(a,1),13780(a,1,2))]. given #1139 (T,wt=13): 13802 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(285(a,1),13780(a,1,2))]. given #1140 (T,wt=13): 13806 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(26(a,1),13789(a,1,2,2,2))]. given #1141 (A,wt=22): 447 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 #1142 (F,wt=13): 13809 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(285(a,1),13789(a,1,2,2,2))]. given #1143 (F,wt=13): 13819 (c1 ^ (x ^ y)) v (c2 ^ y) = c2 ^ y. [para(15(a,1),3418(a,1,1)),demod(16(3))]. given #1144 (T,wt=13): 13888 (c2 v (x v y)) ^ (y v c1) = y v c1. [para(13(a,1),3873(a,1,1,2))]. given #1145 (T,wt=13): 13910 (x ^ (c1 ^ y)) v (y ^ c2) = c2 ^ y. [para(15(a,1),4246(a,1,2))]. given #1146 (A,wt=15): 448 x v (y ^ x ') != 1 | (y ^ x ') ' = x. [para(101(a,1),45(b,1)),demod(13(3)),xx(b)]. given #1147 (F,wt=13): 13918 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(60(a,1),5434(a,1,2)),demod(8359(6))]. given #1148 (F,wt=13): 13923 x ^ ((y ^ x) v (z ^ y)) = y ^ x. [para(13(a,1),6320(a,1,2))]. given #1149 (T,wt=13): 13924 x ^ ((y ^ z) v (y ^ x)) = y ^ x. [para(15(a,1),6320(a,1,2,1))]. given #1150 (T,wt=13): 13925 x ^ ((y ^ z) v (x ^ z)) = z ^ x. [para(15(a,1),6320(a,1,2,2))]. given #1151 (A,wt=26): 451 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 #1152 (F,wt=13): 13928 c1 ^ ((x ^ y) v (y ^ c2)) = y ^ c1. [para(6320(a,1),66(a,1,2)),demod(96(4)),flip(a)]. given #1153 (F,wt=13): 13934 x ^ (((y v x) ^ (x v z)) v u) = x. [para(13(a,1),6558(a,1,2,1,1))]. given #1154 (T,wt=13): 13935 x ^ (y v ((x v z) ^ (x v u))) = x. [para(13(a,1),6558(a,1,2))]. given #1155 (T,wt=13): 13938 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(6558(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #1156 (A,wt=15): 453 c1 v (c2 ' ^ x) != 1 | (c2 ' ^ x) ' = c1. [para(158(a,1),45(b,1)),demod(13(5)),xx(b)]. given #1157 (F,wt=13): 13940 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(117(a,1),6558(a,1,2,1,1))]. given #1158 (F,wt=13): 13941 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(119(a,1),6558(a,1,2,1,1))]. given #1159 (T,wt=13): 13951 x ^ (((y v x) ^ (z v x)) v u) = x. [para(13(a,1),6581(a,1,2,1,1))]. given #1160 (T,wt=13): 13952 x ^ (y v ((x v z) ^ (u v x))) = x. [para(13(a,1),6581(a,1,2))]. given #1161 (A,wt=15): 454 c1 v (x ^ c2 ') != 1 | (x ^ c2 ') ' = c1. [para(160(a,1),45(b,1)),demod(13(5)),xx(b)]. given #1162 (F,wt=13): 13955 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(6581(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #1163 (F,wt=13): 13957 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(117(a,1),6581(a,1,2,1,1))]. given #1164 (T,wt=13): 13958 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(119(a,1),6581(a,1,2,1,1))]. given #1165 (T,wt=13): 13966 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(13(a,1),6591(a,1,2,1,1))]. given #1166 (A,wt=18): 455 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x) ' = c1. [para(66(a,1),45(b,1)),demod(13(4))]. given #1167 (F,wt=13): 13967 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(13(a,1),6591(a,1,2))]. given #1168 (F,wt=13): 13971 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(119(a,1),6591(a,1,2,1,1))]. given #1169 (T,wt=13): 13977 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(13(a,1),6593(a,1,2,1,1))]. given #1170 (T,wt=13): 13978 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(13(a,1),6593(a,1,2))]. given #1171 (A,wt=14): 456 x v c2 != 1 | c1 != 0 | (x v c2) ' = c1. [para(183(a,1),45(b,1)),demod(13(4),119(4))]. given #1172 (F,wt=13): 13982 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(119(a,1),6593(a,1,2,1,1))]. given #1173 (F,wt=13): 13992 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(146(a,1),6643(a,1,2,2))]. given #1174 (T,wt=13): 13995 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(146(a,1),6686(a,1,2,2))]. given #1175 (T,wt=13): 14021 (c1 ^ (x ^ y)) v (y ^ c2) = c2 ^ y. [para(15(a,1),8389(a,1,1,2))]. given #1176 (A,wt=19): 459 x v (y ^ (x ^ y) ') != 1 | (y ^ (x ^ y) ') ' = x. [para(41(a,1),45(b,1)),demod(13(4)),xx(b)]. given #1177 (F,wt=13): 14029 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(15(a,1),9541(a,1,2,1,1))]. given #1178 (F,wt=13): 14030 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(15(a,1),9541(a,1,2))]. given #1179 (T,wt=13): 14033 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(67(a,1),9541(a,1,2,1,1))]. given #1180 (T,wt=13): 14044 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(15(a,1),9551(a,1,2,1,1))]. given #1181 (A,wt=18): 460 x v (y v z) != 1 | 0 != y | (x v (y v z)) ' = y. [para(80(a,1),45(b,1)),demod(13(3),295(3)),flip(b)]. given #1182 (F,wt=13): 14045 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(15(a,1),9551(a,1,2))]. given #1183 (F,wt=13): 14048 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(67(a,1),9551(a,1,2,1,1))]. given #1184 (T,wt=13): 14057 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(15(a,1),9553(a,1,2,1,1))]. given #1185 (T,wt=13): 14058 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(15(a,1),9553(a,1,2))]. given #1186 (A,wt=15): 462 (x ^ y) v y ' != 1 | (x ^ y) ' = y '. [para(336(a,1),45(b,1)),xx(b)]. given #1187 (F,wt=13): 14061 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(67(a,1),9553(a,1,2,1,1))]. given #1188 (F,wt=13): 14068 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(13(a,1),9554(a,1,2,1))]. given #1189 (T,wt=13): 14069 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(15(a,1),9554(a,1,2,1,1))]. given #1190 (T,wt=13): 14070 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(15(a,1),9554(a,1,2))]. given #1191 (A,wt=18): 463 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2) ' = c1. [para(96(a,1),45(b,1)),demod(13(4))]. given #1192 (F,wt=13): 14073 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(67(a,1),9554(a,1,2,1,1))]. given #1193 (F,wt=13): 14097 c1 ^ ((c2 ' ^ x) v (c2 ' ^ y)) = 0. [hyper(332,a,1329,a,b,11607,a(flip)),demod(11607(9),15(10),84(12),312(11),11607(18))]. given #1194 (T,wt=13): 14109 c1 ^ ((c2 ' ^ x) v (y ^ c2 ')) = 0. [hyper(332,a,1329,a,b,11622,a(flip)),demod(11622(9),15(10),84(12),312(11),11622(18))]. given #1195 (T,wt=13): 14123 c2 v ((c1 ' v x) ^ (c1 ' v y)) = 1. [para(11899(a,1),2040(a,1,2,2,1)),demod(86(10),13(10),84(10),13(9))]. given #1196 (A,wt=18): 464 x v (y v z) != 1 | 0 != z | (x v (y v z)) ' = z. [para(103(a,1),45(b,1)),demod(13(3),297(3)),flip(b)]. given #1197 (F,wt=13): 14135 c2 v ((c1 ' v x) ^ (y v c1 ')) = 1. [para(11916(a,1),2040(a,1,2,2,1)),demod(86(10),13(10),84(10),13(9))]. given #1198 (F,wt=13): 14137 (x ^ y) v y ' != 1 | y ^ x = y. [para(15(a,1),12188(a,1,1))]. given #1199 (T,wt=13): 14138 (x ^ c1) v c2 ' != 1 | c1 ^ x = c2. [para(15(a,1),12189(a,1,1))]. given #1200 (T,wt=13): 14139 (x v y) ^ y ' != 0 | y v x = y. [para(13(a,1),12558(a,1,1))]. given #1201 (A,wt=24): 469 x v (y v c2) != 1 | (x v c1) ^ (y v c2) != 0 | (x v c1) ' = y v c2. [para(119(a,1),44(a,1,2))]. given #1202 (F,wt=13): 14140 (x v c2) ^ c1 ' != 0 | c2 v x = c1. [para(13(a,1),12559(a,1,1))]. given #1203 (F,wt=13): 14150 c2 v ((x v c1 ') ^ (c1 ' v y)) = 1. [para(12770(a,1),2040(a,1,2,2,1)),demod(86(10),13(10),84(10),13(9))]. given #1204 (T,wt=13): 14160 c2 v ((x v c1 ') ^ (y v c1 ')) = 1. [para(12779(a,1),2040(a,1,2,2,1)),demod(86(10),13(10),84(10),13(9))]. given #1205 (T,wt=13): 14167 c1 ^ ((x ^ c2 ') v (c2 ' ^ y)) = 0. [hyper(332,a,1329,a,b,12902,a(flip)),demod(12902(9),15(10),84(12),312(11),12902(18))]. given #1206 (A,wt=18): 470 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x) ' = c2. [para(119(a,1),44(a,1)),demod(15(8))]. given #1207 (F,wt=13): 14177 c1 ^ ((x ^ c2 ') v (y ^ c2 ')) = 0. [hyper(332,a,1329,a,b,13068,a(flip)),demod(13068(9),15(10),84(12),312(11),13068(18))]. given #1208 (F,wt=13): 14209 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(195(a,1),13791(a,1,2,2))]. given #1209 (T,wt=13): 14211 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(195(a,1),13799(a,1,2,2))]. given #1210 (T,wt=13): 14215 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(15(a,1),13918(a,1,2,1))]. given #1211 (A,wt=18): 473 x v (c2 v y) != 1 | c1 != 0 | c1 ' = x v (c2 v y). [para(200(a,1),21(b,1)),demod(425(5))]. given #1212 (F,wt=13): 14216 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(15(a,1),13918(a,1,2,2))]. given #1213 (F,wt=13): 14219 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(15(a,1),13923(a,1,2,1))]. given #1214 (T,wt=13): 14220 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(15(a,1),13923(a,1,2,2))]. given #1215 (T,wt=13): 14227 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(15(a,1),13924(a,1,2,2))]. given #1216 (A,wt=18): 475 x v (c2 v y) != 1 | c1 != 0 | (x v (c2 v y)) ' = c1. [para(200(a,1),45(b,1)),demod(13(5),425(5))]. given #1217 (F,wt=13): 14230 c1 ^ ((x ^ y) v (x ^ c2)) = x ^ c1. [para(13924(a,1),66(a,1,2)),demod(96(4)),flip(a)]. given #1218 (F,wt=13): 14231 x ^ ((y ^ c1) v (c2 ^ x)) = c2 ^ x. [para(67(a,1),13924(a,1,2,1))]. given #1219 (T,wt=13): 14244 c1 ^ ((x ^ y) v (c2 ^ y)) = y ^ c1. [para(13925(a,1),66(a,1,2)),demod(96(4)),flip(a)]. given #1220 (T,wt=13): 14254 x ^ (y v ((z v x) ^ (x v u))) = x. [para(13(a,1),13934(a,1,2))]. given #1221 (A,wt=18): 478 x v (y v c2) != 1 | c1 != 0 | c1 ' = x v (y v c2). [para(202(a,1),21(b,1)),demod(466(5))]. given #1222 (F,wt=13): 14266 c1 ^ (x v ((c2 v y) ^ (c2 v z))) = c1. [para(13935(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #1223 (F,wt=13): 14267 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(119(a,1),13935(a,1,2,2,1))]. given #1224 (T,wt=13): 14298 x ^ (y v ((z v x) ^ (u v x))) = x. [para(13(a,1),13951(a,1,2))]. given #1225 (T,wt=13): 14305 c1 ^ (x v ((c2 v y) ^ (z v c2))) = c1. [para(13952(a,1),66(a,1,2)),demod(23(3)),flip(a)]. given #1226 (A,wt=18): 480 x v (y v c2) != 1 | c1 != 0 | (x v (y v c2)) ' = c1. [para(202(a,1),45(b,1)),demod(13(5),466(5))]. given #1227 (F,wt=13): 14306 c1 ^ (x v ((y v c2) ^ (z v c1))) = c1. [para(119(a,1),13952(a,1,2,2,1))]. given #1228 (F,wt=13): 14324 c1 ^ (x v ((y v c1) ^ (c2 v z))) = c1. [para(13(a,1),13966(a,1,2))]. given #1229 (T,wt=13): 14330 c1 ^ (x v ((y v c2) ^ (c2 v z))) = c1. [para(119(a,1),13967(a,1,2,2,1))]. given #1230 (T,wt=13): 14338 c1 ^ (x v ((y v c1) ^ (z v c2))) = c1. [para(13(a,1),13977(a,1,2))]. given #1231 (A,wt=18): 483 c2 != 1 | c1 ^ (x ^ y) != 0 | c2 ' = x ^ (y ^ c1). [para(262(a,1),21(a,1)),demod(254(8))]. given #1232