============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 11521 was started by mccune on cleo.thornwood, Sat Aug 12 21:05:41 2006 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H42.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in formulas(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 formulas(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 formulas(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 NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y (x ^ y = x -> x' v y' = x')). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v y = y v x. [assumption]. (x v y) v z = x v (y v z). [assumption]. x ^ y = y ^ x. [assumption]. (x ^ y) ^ z = x ^ (y ^ z). [assumption]. x ^ (x v y) = x. [assumption]. x v (x ^ y) = x. [assumption]. x v x' = 1. [assumption]. x ^ x' = 0. [assumption]. x v y != 1 | x ^ y != 0 | x' = y. [assumption]. x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (y v (u v (x ^ z))))) # label(H42). [assumption]. c1 ^ c2 = c1. [deny(1)]. c1' != c1' v c2'. [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= 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; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. 12 x ^ (y v (z ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 c1 ^ c2 = c1. [deny(1)]. 15 c1' v c2' != c1'. [copy(14),flip(a)]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. % (lex-dep) 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 13 c1 ^ c2 = c1. [deny(1)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 x v y = y v x. [assumption]. given #2 (I,wt=11): 3 (x v y) v z = x v (y v z). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 16 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 18 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=6): 8 x v x' = 1. [assumption]. given #8 (I,wt=6): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=14): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=23): 12 x ^ (y v (z ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. given #11 (I,wt=5): 13 c1 ^ c2 = c1. [deny(1)]. given #12 (I,wt=8): 15 c1' v c2' != c1'. [copy(14),flip(a)]. given #13 (F,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #14 (T,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #15 (T,wt=5): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #16 (A,wt=11): 17 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #17 (F,wt=5): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #18 (F,wt=5): 71 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #19 (T,wt=4): 79 1' = 0. [hyper(10,a,35,a,b,71,a)]. given #20 (T,wt=5): 77 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #21 (A,wt=11): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #22 (F,wt=4): 82 0' = 1. [hyper(10,a,77,a,b,32,a)]. given #23 (F,wt=5): 80 1 v x = 1. [para(71(a,1),6(a,1))]. given #24 (T,wt=5): 83 0 ^ x = 0. [para(77(a,1),6(a,1,2))]. given #25 (T,wt=5): 90 x v 1 = 1. [para(80(a,1),2(a,1)),flip(a)]. given #26 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #27 (F,wt=5): 93 x ^ 0 = 0. [para(83(a,1),4(a,1)),flip(a)]. given #28 (F,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #29 (T,wt=5): 106 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. given #30 (T,wt=7): 92 0 != x | x' = 1. [back_rewrite(72),rewrite(90(2)),xx(a)]. given #31 (A,wt=13): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #32 (F,wt=7): 95 1 != x | x' = 0. [back_rewrite(78),rewrite(93(4)),xx(b)]. given #33 (F,wt=8): 81 x v (x' v y) = 1. [back_rewrite(30),rewrite(80(5))]. given #34 (T,wt=8): 84 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(83(5))]. given #35 (T,wt=8): 91 x v (y v x') = 1. [back_rewrite(75),rewrite(90(5))]. given #36 (A,wt=11): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #37 (F,wt=9): 124 c1 ^ (c1' v c2') != 0. [ur(10,a,81,a,c,15,a(flip))]. given #38 (F,wt=8): 94 x ^ (y ^ x') = 0. [back_rewrite(87),rewrite(93(5))]. given #39 (T,wt=8): 135 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #40 (T,wt=6): 150 c1 ^ c2' = 0. [para(106(a,1),135(a,1,2,1))]. given #41 (A,wt=13): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #42 (F,wt=8): 145 x ^ (y v x)' = 0. [para(2(a,1),135(a,1,2,1))]. given #43 (F,wt=8): 151 c1 ^ (c2' ^ x) = 0. [para(150(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #44 (T,wt=8): 153 c1 ^ (x ^ c2') = 0. [para(150(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #45 (T,wt=9): 59 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #46 (A,wt=11): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #47 (F,wt=7): 173 c1 ^ (c2 v x) = c1. [para(6(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #48 (F,wt=7): 176 c1 ^ (x v c2) = c1. [para(20(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #49 (T,wt=8): 179 c1 ^ (c2 v x)' = 0. [para(135(a,1),59(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #50 (T,wt=8): 181 c1 ^ (x v c2)' = 0. [para(145(a,1),59(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #51 (A,wt=13): 25 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #52 (F,wt=8): 184 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #53 (F,wt=8): 217 x v (y ^ x)' = 1. [para(4(a,1),184(a,1,2,1))]. given #54 (T,wt=6): 225 c2 v c1' = 1. [para(13(a,1),217(a,1,2,1))]. given #55 (T,wt=8): 231 c2 v (x v c1') = 1. [para(173(a,1),217(a,1,2,1)),rewrite(3(5))]. given #56 (A,wt=13): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #57 (F,wt=8): 232 c2 v (c1' v x) = 1. [para(225(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #58 (F,wt=9): 60 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite(4(4))]. given #59 (T,wt=7): 248 c2 v (x ^ c1) = c2. [para(60(a,1),7(a,1,2))]. given #60 (T,wt=7): 254 c2 v (c1 ^ x) = c2. [para(4(a,1),248(a,1,2))]. given #61 (A,wt=10): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #62 (F,wt=8): 251 c2 v (x ^ c1)' = 1. [para(60(a,1),184(a,1,2,1))]. given #63 (F,wt=8): 268 c2 v (c1 ^ x)' = 1. [para(4(a,1),251(a,1,2,1))]. given #64 (T,wt=9): 62 x ^ (x ^ y) = x ^ y. [para(28(a,1),5(a,1,1)),flip(a)]. given #65 (T,wt=9): 64 x ^ (y ^ x) = y ^ x. [para(28(a,1),5(a,2,2)),rewrite(4(2))]. given #66 (A,wt=10): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #67 (F,wt=9): 67 x v (x v y) = x v y. [para(29(a,1),3(a,1,1)),flip(a)]. given #68 (F,wt=9): 69 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite(2(2))]. given #69 (T,wt=9): 73 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #70 (T,wt=9): 86 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #71 (A,wt=14): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #72 (F,wt=5): 305 x'' = x. [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #73 (F,wt=8): 328 x' v (y v x) = 1. [para(305(a,1),91(a,1,2,2))]. given #74 (T,wt=8): 329 x' ^ (y ^ x) = 0. [para(305(a,1),94(a,1,2,2))]. given #75 (T,wt=9): 89 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #76 (A,wt=20): 37 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #77 (F,wt=9): 96 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #78 (F,wt=9): 104 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #79 (T,wt=9): 110 c1 v (c2 v x) = c2 v x. [para(106(a,1),3(a,1,1)),flip(a)]. given #80 (T,wt=9): 111 c2 v (x v c1) = x v c2. [para(106(a,1),3(a,2,2)),rewrite(2(4))]. given #81 (A,wt=14): 38 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #82 (F,wt=9): 112 c1 v (x v c2) = x v c2. [para(106(a,1),17(a,1,2)),flip(a)]. given #83 (F,wt=9): 193 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),173(a,1,2))]. given #84 (T,wt=9): 195 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),176(a,1,2))]. given #85 (T,wt=9): 255 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),248(a,1,2))]. given #86 (A,wt=20): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #87 (F,wt=9): 260 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),254(a,1,2))]. given #88 (F,wt=9): 316 c2 ^ c1' != 0 | c2 = c1. [para(225(a,1),36(a,1)),rewrite(4(7),305(12)),flip(c),xx(a)]. given #89 (T,wt=9): 422 c2 v (x v c1) = c2 v x. [para(111(a,2),2(a,1))]. given #90 (T,wt=9): 443 c1 v c2' != 1 | c2 = c1. [para(150(a,1),38(b,1)),rewrite(2(4),305(12)),xx(b)]. given #91 (A,wt=23): 42 x ^ (y v (z ^ (y v ((x ^ z) v u)))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2,2,2))]. given #92 (F,wt=10): 65 1 != x | 0 != x | x' = x. [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)]. given #93 (F,wt=10): 109 c2 != 1 | c1 != 0 | c1' = c2. [back_rewrite(61),rewrite(106(3))]. given #94 (T,wt=10): 127 x v (y v (x' v z)) = 1. [para(81(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #95 (T,wt=10): 130 x ^ (y ^ (x' ^ z)) = 0. [para(84(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #96 (A,wt=23): 43 x ^ (y v (z ^ (u v ((x ^ z) v y)))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2,2)),rewrite(3(3))]. given #97 (F,wt=10): 132 x v (y v (z v x')) = 1. [para(3(a,1),91(a,1,2))]. given #98 (F,wt=10): 140 x ^ ((x v y)' ^ z) = 0. [para(84(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #99 (T,wt=10): 142 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),94(a,1,2))]. given #100 (T,wt=10): 144 x ^ (y ^ (x v z)') = 0. [para(94(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #101 (A,wt=23): 44 x ^ (y v (z ^ (y v (u v (x ^ z))))) = x ^ (y v (z ^ (u v x))). [para(2(a,1),12(a,2,2,2,2))]. given #102 (F,wt=10): 149 x ^ (y v (x v z))' = 0. [para(17(a,1),135(a,1,2,1))]. given #103 (F,wt=10): 162 x ^ (y v (z v x))' = 0. [para(3(a,1),145(a,1,2,1))]. given #104 (T,wt=10): 163 x ^ ((y v x)' ^ z) = 0. [para(145(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #105 (T,wt=10): 167 x ^ (y ^ (z v x)') = 0. [para(145(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #106 (A,wt=17): 53 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)). [para(7(a,1),12(a,1,2,2,2,2)),rewrite(29(5))]. given #107 (F,wt=10): 169 c1 ^ (x ^ (c2' ^ y)) = 0. [para(151(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #108 (F,wt=10): 170 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),153(a,1,2))]. given #109 (T,wt=10): 189 x v ((x ^ y)' v z) = 1. [para(81(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #110 (T,wt=10): 190 x v (y v (x ^ z)') = 1. [para(91(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #111 (A,wt=21): 54 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))). [para(9(a,1),12(a,1,2,2,2,2,2)),rewrite(35(3))]. given #112 (F,wt=10): 199 c1 ^ ((c2 v x)' ^ y) = 0. [para(179(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #113 (F,wt=10): 201 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),179(a,1,2,1))]. given #114 (T,wt=10): 202 c1 ^ (x ^ (c2 v y)') = 0. [para(179(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #115 (T,wt=10): 203 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),181(a,1,2,1))]. given #116 (A,wt=40): 55 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(12(a,1),10(b,1))]. given #117 (F,wt=10): 204 c1 ^ ((x v c2)' ^ y) = 0. [para(181(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #118 (F,wt=10): 206 c1 ^ (x ^ (y v c2)') = 0. [para(181(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #119 (T,wt=10): 220 x v (y ^ (x ^ z))' = 1. [para(19(a,1),184(a,1,2,1))]. given #120 (T,wt=10): 221 x v ((y ^ x)' v z) = 1. [para(217(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #121 (A,wt=32): 56 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(12(a,2),10(b,1)),rewrite(44(12))]. given #122 (F,wt=10): 223 x v (y ^ (z ^ x))' = 1. [para(5(a,1),217(a,1,2,1))]. given #123 (F,wt=10): 226 x v (y v (z ^ x)') = 1. [para(217(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #124 (T,wt=10): 230 (c2 ^ x) v (c1 ^ x)' = 1. [para(59(a,1),217(a,1,2,1))]. given #125 (T,wt=10): 234 c2 v (x v (c1' v y)) = 1. [para(231(a,1),3(a,1,1)),rewrite(80(2),3(6)),flip(a)]. given #126 (A,wt=49): 57 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(12(a,1),12(a,1,2,2,2,2,2))]. given #127 (F,wt=10): 235 c2 v (x v (y v c1')) = 1. [para(3(a,1),231(a,1,2))]. given #128 (F,wt=10): 261 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #129 (T,wt=10): 267 c2 v ((x ^ c1)' v y) = 1. [para(251(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #130 (T,wt=10): 269 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),251(a,1,2,1))]. given #131 (A,wt=41): 58 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(12(a,2),12(a,1,2,2,2,2,2)),rewrite(44(9))]. given #132 (F,wt=10): 271 c2 v (x v (y ^ c1)') = 1. [para(251(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #133 (F,wt=10): 272 c2 v ((c1 ^ x)' v y) = 1. [para(268(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #134 (T,wt=10): 274 c2 v (x v (c1 ^ y)') = 1. [para(268(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #135 (T,wt=10): 275 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),268(a,1,2,1))]. given #136 (A,wt=14): 66 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(41),rewrite(62(4))]. given #137 (F,wt=7): 1772 c1 != 1 | c1' = 0. [para(150(a,1),66(b,1)),rewrite(150(12)),flip(a),xx(b)]. given #138 (F,wt=7): 1774 x' != 1 | 0 = x. [para(329(a,1),66(b,1)),rewrite(305(8),329(9)),flip(a),flip(c),xx(b)]. given #139 (T,wt=10): 281 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),34(a,1,2,2,1))]. given #140 (T,wt=10): 287 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),59(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #141 (A,wt=14): 70 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(40),rewrite(67(2))]. given #142 (F,wt=10): 1778 (c1 ^ (c1' v c2'))' != 1. [ur(1774,b,124,a(flip))]. given #143 (F,wt=7): 1814 c2 != 0 | c2' = 1. [para(225(a,1),70(a,1)),rewrite(225(12)),flip(b),xx(a)]. given #144 (T,wt=7): 1816 x' != 0 | 1 = x. [para(328(a,1),70(a,1)),rewrite(305(8),328(9)),flip(b),flip(c),xx(a)]. given #145 (T,wt=10): 309 c2 != 1 | c1 != 0 | c2' = c1. [para(106(a,1),36(a,1)),rewrite(4(6),13(6))]. given #146 (A,wt=11): 74 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #147 (F,wt=10): 330 x' v (y v (x v z)) = 1. [para(328(a,1),3(a,1,1)),rewrite(80(2),3(4)),flip(a)]. given #148 (F,wt=8): 1840 c1' v (x v c2) = 1. [para(106(a,1),330(a,1,2,2))]. given #149 (T,wt=7): 1857 c1' != 0 | c1 = 1. [para(1840(a,1),70(a,1)),rewrite(305(10),1840(13)),flip(b),xx(a)]. given #150 (T,wt=10): 331 x' v (y v (z v x)) = 1. [para(3(a,1),328(a,1,2))]. given #151 (A,wt=20): 76 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #152 (F,wt=10): 336 x' ^ (y ^ (x ^ z)) = 0. [para(329(a,1),5(a,1,1)),rewrite(83(2),5(4)),flip(a)]. given #153 (F,wt=10): 337 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),329(a,1,2))]. given #154 (T,wt=8): 1946 c2' ^ (x ^ c1) = 0. [para(13(a,1),337(a,1,2,2))]. given #155 (T,wt=7): 1979 c2' != 1 | c2 = 0. [para(1946(a,1),66(b,1)),rewrite(305(10),1946(13)),flip(a),xx(b)]. given #156 (A,wt=11): 85 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #157 (F,wt=10): 345 (x ^ c2) v (x ^ c1)' = 1. [para(89(a,1),217(a,1,2,1))]. given #158 (F,wt=10): 346 x ^ (c1 ^ (x ^ c2)') = 0. [para(89(a,1),329(a,1,2)),rewrite(4(6),5(6))]. given #159 (T,wt=10): 425 (x v c1) ^ (x v c2)' = 0. [para(111(a,1),145(a,1,2,1))]. given #160 (T,wt=10): 429 x v (c2 v (x v c1)') = 1. [para(111(a,1),328(a,1,2)),rewrite(2(6),3(6))]. given #161 (A,wt=20): 88 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(19(a,1),10(b,1))]. given #162 (F,wt=10): 543 (x v c1) ^ (c2 v x)' = 0. [para(422(a,1),145(a,1,2,1))]. given #163 (F,wt=10): 545 c2 v (x v (x v c1)') = 1. [para(422(a,1),328(a,1,2)),rewrite(2(6),3(6))]. given #164 (T,wt=10): 1321 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),230(a,1,1))]. given #165 (T,wt=10): 1322 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),230(a,1,2,1))]. given #166 (A,wt=11): 97 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #167 (F,wt=10): 1323 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),230(a,1,2,1))]. given #168 (F,wt=10): 1327 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),230(a,1,2,1))]. given #169 (T,wt=10): 1770 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),66(b,1)),rewrite(13(11)),flip(a)]. given #170 (T,wt=10): 1786 c1 ^ (x ^ (x ^ c2)') = 0. [para(281(a,1),59(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #171 (A,wt=13): 98 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #172 (F,wt=10): 1797 x ^ (c1 ^ (c2 ^ x)') = 0. [para(287(a,1),19(a,1)),flip(a)]. given #173 (F,wt=10): 1799 c1 ^ (c2 ^ (c1 v x))' = 0. [para(287(a,1),22(a,1)),flip(a)]. given #174 (T,wt=10): 1815 c2 != 1 | c2 != 0 | c2' = c2. [para(248(a,1),70(a,1)),rewrite(248(12)),flip(b)]. given #175 (T,wt=10): 1844 c1' v (x v (c2 v y)) = 1. [para(110(a,1),330(a,1,2,2))]. given #176 (A,wt=14): 99 x v y != 1 | 0 != y | y' = x v y. [para(20(a,1),10(b,1)),rewrite(69(2)),flip(b)]. given #177 (F,wt=10): 1846 c1' v (x v (y v c2)) = 1. [para(112(a,1),330(a,1,2,2))]. given #178 (F,wt=10): 1859 (x ^ y)' v (z v x) = 1. [para(7(a,1),331(a,1,2,2))]. given #179 (T,wt=10): 1862 (x ^ y)' v (z v y) = 1. [para(26(a,1),331(a,1,2,2))]. given #180 (T,wt=10): 1866 (x ^ c1)' v (y v c2) = 1. [para(248(a,1),331(a,1,2,2))]. given #181 (A,wt=13): 100 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #182 (F,wt=10): 1867 (c1 ^ x)' v (y v c2) = 1. [para(254(a,1),331(a,1,2,2))]. given #183 (F,wt=10): 1935 c2' ^ (x ^ (y ^ c1)) = 0. [para(60(a,1),336(a,1,2,2))]. given #184 (T,wt=10): 1944 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),337(a,1,2,2))]. given #185 (T,wt=10): 1948 (x v y)' ^ (z ^ y) = 0. [para(20(a,1),337(a,1,2,2))]. given #186 (A,wt=11): 101 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #187 (F,wt=10): 1953 (c2 v x)' ^ (y ^ c1) = 0. [para(173(a,1),337(a,1,2,2))]. given #188 (F,wt=10): 1954 (x v c2)' ^ (y ^ c1) = 0. [para(176(a,1),337(a,1,2,2))]. given #189 (T,wt=10): 1972 c2' ^ (x ^ (c1 ^ y)) = 0. [para(1946(a,1),5(a,1,1)),rewrite(83(2),5(6)),flip(a)]. given #190 (T,wt=10): 2022 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),425(a,1,1))]. given #191 (A,wt=11): 102 x v ((y ^ x) v z) = x v z. [para(26(a,1),3(a,1,1)),flip(a)]. given #192 (F,wt=10): 2033 x v (c2 v (c1 v x)') = 1. [para(2(a,1),429(a,1,2,2,1))]. given #193 (F,wt=10): 2111 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),543(a,1,1))]. given #194 (T,wt=10): 2112 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),543(a,1,2,1)),rewrite(2(4))]. given #195 (T,wt=10): 2115 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),543(a,1,2,1)),rewrite(2(4))]. given #196 (A,wt=13): 103 x v (y v (z ^ (x v y))) = x v y. [para(26(a,1),3(a,1)),flip(a)]. given #197 (F,wt=10): 2127 c2 v (x v (c1 v x)') = 1. [para(2(a,1),545(a,1,2,2,1))]. given #198 (F,wt=10): 2130 c2 v (c1 v (c2 ^ x))' = 1. [para(545(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #199 (T,wt=10): 2189 c1 ^ (c2 ^ (x v c1))' = 0. [para(97(a,1),287(a,1))]. given #200 (T,wt=10): 2197 c1' v (c2 ^ (c1 v x)) = 1. [para(1323(a,1),2(a,1)),flip(a)]. given #201 (A,wt=14): 105 1 != x | y ^ x != 0 | x' = y ^ x. [para(26(a,1),10(a,1)),rewrite(64(4)),flip(a)]. given #202 (F,wt=7): 2713 c1 != 0 | c1' = 1. [para(2197(a,1),55(b,1,2)),rewrite(13(9),328(9),4(6),71(6),2(5),225(5),2(3),80(3),4(6),71(6),13(16),328(16),4(13),71(13),2(12),225(12)),xx(a)]. given #203 (F,wt=10): 2209 c1' v (c2 ^ (x v c1)) = 1. [para(1327(a,1),2(a,1)),flip(a)]. given #204 (T,wt=10): 2572 c2 v (c1 v (x ^ c2))' = 1. [para(102(a,1),545(a,1)),rewrite(2(5))]. given #205 (T,wt=10): 2613 c2' ^ (c1 v (c2 ^ x)) = 0. [para(2112(a,1),4(a,1)),flip(a)]. given #206 (A,wt=11): 107 x v (y v (z ^ x)) = y v x. [para(26(a,1),17(a,1,2)),flip(a)]. given #207 (F,wt=10): 2624 c2' ^ (c1 v (x ^ c2)) = 0. [para(2115(a,1),4(a,1)),flip(a)]. given #208 (F,wt=11): 122 (x v c1) ^ (x v c2) = x v c1. [para(106(a,1),21(a,1,2,2))]. given #209 (T,wt=11): 152 c1 v c2' != 1 | c2' = c1'. [para(150(a,1),10(b,1)),flip(c),xx(b)]. given #210 (T,wt=11): 177 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(59(a,1),26(a,1,2)),rewrite(2(5))]. given #211 (A,wt=13): 108 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(19(a,1),26(a,1,2))]. given #212 (F,wt=11): 178 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #213 (F,wt=11): 194 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(173(a,1),19(a,1,2)),flip(a)]. given #214 (T,wt=11): 196 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(176(a,1),5(a,1,1)),flip(a)]. given #215 (T,wt=11): 198 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(176(a,1),19(a,1,2)),flip(a)]. given #216 (A,wt=13): 113 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #217 (F,wt=11): 233 c2 ^ c1' != 0 | c2' = c1'. [para(225(a,1),10(a,1)),xx(a)]. given #218 (F,wt=11): 250 c2 v ((x ^ c1) v y) = c2 v y. [para(60(a,1),24(a,1,2,1))]. given #219 (T,wt=11): 253 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(60(a,1),27(a,1,2))]. given #220 (T,wt=11): 256 c2 v (x v (y ^ c1)) = x v c2. [para(248(a,1),17(a,1,2)),flip(a)]. given #221 (A,wt=13): 114 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite(3(3))]. given #222 (F,wt=11): 257 c2 v ((c1 ^ x) v y) = c2 v y. [para(254(a,1),3(a,1,1)),flip(a)]. given #223 (F,wt=11): 259 c2 v (x v (c1 ^ y)) = x v c2. [para(254(a,1),17(a,1,2)),flip(a)]. given #224 (T,wt=11): 279 (x v y) ^ (z ^ x) = z ^ x. [para(64(a,1),22(a,2)),rewrite(278(4))]. given #225 (T,wt=11): 280 (x ^ y) v (y ^ x) = x ^ y. [para(64(a,1),27(a,1,2))]. given #226 (A,wt=19): 115 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),21(a,1,1)),rewrite(3(5),3(8))]. given #227 (F,wt=10): 3297 (x ^ y) v (y ^ x)' = 1. [para(280(a,1),328(a,1,2)),rewrite(2(4))]. given #228 (F,wt=11): 291 (x v y) ^ (y v x) = x v y. [para(69(a,1),21(a,1,2))]. given #229 (T,wt=10): 3371 (x v y) ^ (y v x)' = 0. [para(291(a,1),329(a,1,2)),rewrite(4(4))]. given #230 (T,wt=11): 292 (x ^ y) v (z v x) = z v x. [para(69(a,1),24(a,2)),rewrite(290(4))]. given #231 (A,wt=17): 116 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #232 (F,wt=11): 294 x ^ (y v (z v (x v u))) = x. [para(3(a,1),73(a,1,2))]. given #233 (F,wt=11): 298 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),86(a,1,2))]. given #234 (T,wt=11): 344 (x ^ c1) v (x ^ c2) = x ^ c2. [para(89(a,1),26(a,1,2)),rewrite(2(5))]. given #235 (T,wt=11): 353 x v y != 0 | (x v y)' = 1. [para(32(a,1),37(b,1)),rewrite(90(2),90(2)),xx(a)]. given #236 (A,wt=19): 118 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(17(a,1),21(a,1,1)),rewrite(3(4))]. given #237 (F,wt=11): 357 x v y != 1 | (x v y)' = 0. [para(35(a,1),37(a,1,2)),rewrite(4(6),83(6)),xx(b)]. given #238 (F,wt=7): 3605 c2 != 1 | c2' = 0. [para(106(a,1),357(a,1)),rewrite(106(6))]. given #239 (T,wt=11): 394 x ^ (y v (z v (u v x))) = x. [para(3(a,1),96(a,1,2,2))]. given #240 (T,wt=11): 406 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),104(a,1,2,2))]. given #241 (A,wt=15): 119 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #242 (F,wt=11): 461 (c1 v x) ^ (x v c2) = c1 v x. [para(112(a,1),21(a,1,2))]. given #243 (F,wt=11): 464 c1 ^ (x v (y v (c2 v z))) = c1. [para(3(a,1),193(a,1,2))]. given #244 (T,wt=11): 469 c1 ^ (x v (y v (z v c2))) = c1. [para(3(a,1),195(a,1,2,2))]. given #245 (T,wt=11): 475 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(5(a,1),255(a,1,2,2))]. given #246 (A,wt=17): 120 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #247 (F,wt=11): 485 x ^ y != 0 | (x ^ y)' = 1. [para(32(a,1),39(b,1,2)),rewrite(2(3),80(3)),xx(a)]. given #248 (F,wt=11): 487 x ^ y != 1 | (x ^ y)' = 0. [para(35(a,1),39(a,1)),rewrite(93(5),93(5)),xx(b)]. given #249 (T,wt=11): 535 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(5(a,1),260(a,1,2))]. given #250 (T,wt=11): 542 (x v c1) ^ (c2 v x) = x v c1. [para(422(a,1),20(a,1,2))]. given #251 (A,wt=22): 123 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [back_rewrite(117),rewrite(121(4))]. given #252 (F,wt=11): 2169 (x v y) ^ (z ^ y) = z ^ y. [para(64(a,1),97(a,2)),rewrite(278(4))]. given #253 (F,wt=11): 2291 (x ^ y)' != 0 | x ^ y = 1. [para(184(a,1),99(a,1)),rewrite(305(10),184(11)),flip(b),xx(a)]. given #254 (T,wt=11): 2376 (c1 v x) ^ (c2 v x) = c1 v x. [para(110(a,1),100(a,1,2))]. given #255 (T,wt=11): 2432 (x v y)' != 1 | x v y = 0. [para(1944(a,1),66(b,1)),rewrite(305(10),1944(12)),flip(a),xx(b)]. given #256 (A,wt=12): 125 x v (y v ((x v y)' v z)) = 1. [para(81(a,1),3(a,1)),flip(a)]. given #257 (F,wt=11): 2542 (x ^ y) v (z v y) = z v y. [para(69(a,1),102(a,2)),rewrite(290(4))]. given #258 (F,wt=11): 2841 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),177(a,1,1))]. given #259 (T,wt=11): 2842 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),177(a,1,2))]. given #260 (T,wt=11): 2926 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(64(a,1),178(a,2)),rewrite(278(7))]. given #261 (A,wt=15): 126 x ^ (x' v y) != 0 | x' v y = x'. [para(81(a,1),10(a,1)),flip(c),xx(a)]. given #262 (F,wt=11): 2979 (x v c2) ^ (y ^ c1) = y ^ c1. [para(64(a,1),196(a,2)),rewrite(278(7))]. given #263 (F,wt=11): 3063 (x ^ c1) v (y v c2) = y v c2. [para(69(a,1),250(a,2)),rewrite(290(7))]. given #264 (T,wt=11): 3211 (c1 ^ x) v (y v c2) = y v c2. [para(69(a,1),257(a,2)),rewrite(290(7))]. given #265 (T,wt=11): 3529 x v y != 0 | (y v x)' = 1. [para(2(a,1),353(a,1))]. given #266 (A,wt=12): 128 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(84(a,1),5(a,1)),flip(a)]. given #267 (F,wt=11): 3603 x v y != 1 | (y v x)' = 0. [para(2(a,1),357(a,1))]. given #268 (F,wt=11): 3726 (x v c2) ^ (c1 v x) = c1 v x. [para(461(a,1),4(a,1)),flip(a)]. given #269 (T,wt=11): 3822 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),485(a,1))]. given #270 (T,wt=11): 3826 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),487(a,1))]. given #271 (A,wt=15): 129 x v (x' ^ y) != 1 | x' ^ y = x'. [para(84(a,1),10(b,1)),flip(c),xx(b)]. given #272 (F,wt=11): 3844 (c2 v x) ^ (x v c1) = x v c1. [para(542(a,1),4(a,1)),flip(a)]. given #273 (F,wt=11): 3925 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),2291(a,1,1))]. given #274 (T,wt=11): 3927 (x v y)' != 0 | x v y = 1. [para(21(a,1),2291(a,1,1)),rewrite(21(8))]. given #275 (T,wt=7): 4182 c2' != 0 | c2 = 1. [para(106(a,1),3927(a,1,1)),rewrite(106(7))]. given #276 (A,wt=12): 131 x v (y v (z v (x v y)')) = 1. [para(91(a,1),3(a,1)),flip(a)]. given #277 (F,wt=11): 3947 (x v y)' != 1 | y v x = 0. [para(2(a,1),2432(a,1,1))]. given #278 (F,wt=11): 3949 (x ^ y)' != 1 | x ^ y = 0. [para(27(a,1),2432(a,1,1)),rewrite(27(8))]. given #279 (T,wt=7): 4203 c1' != 1 | c1 = 0. [para(13(a,1),3949(a,1,1)),rewrite(13(7))]. given #280 (T,wt=11): 4035 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(2842(a,1),2(a,1)),flip(a)]. given #281 (A,wt=15): 133 x ^ (y v x') != 0 | y v x' = x'. [para(91(a,1),10(a,1)),flip(c),xx(a)]. given #282 (F,wt=11): 4180 (x v y)' != 0 | y v x = 1. [para(291(a,1),3925(a,1,1)),rewrite(291(7))]. given #283 (F,wt=11): 4202 (x ^ y)' != 1 | y ^ x = 0. [para(280(a,1),3947(a,1,1)),rewrite(280(7))]. given #284 (T,wt=12): 141 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(94(a,1),5(a,1)),flip(a)]. given #285 (T,wt=12): 146 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),135(a,1,2,1))]. given #286 (A,wt=17): 134 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(22(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #287 (F,wt=12): 147 x ^ (y ^ ((x ^ y) v z)') = 0. [para(135(a,1),5(a,1)),flip(a)]. given #288 (F,wt=12): 164 x ^ (y ^ (z v (x ^ y))') = 0. [para(145(a,1),5(a,1)),flip(a)]. given #289 (T,wt=12): 166 (x v y) ^ (x v (z v y))' = 0. [para(17(a,1),145(a,1,2,1))]. given #290 (T,wt=12): 191 ((x ^ y) v z) ^ (x v z)' = 0. [para(24(a,1),145(a,1,2,1))]. given #291 (A,wt=22): 136 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(22(a,1),10(b,1))]. given #292 (F,wt=12): 216 x v (y v ((x v y) ^ z)') = 1. [para(184(a,1),3(a,1)),flip(a)]. given #293 (F,wt=12): 218 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),184(a,1,2,1))]. given #294 (T,wt=12): 222 x v (y v (z ^ (x v y))') = 1. [para(217(a,1),3(a,1)),flip(a)]. given #295 (T,wt=12): 227 (x ^ y) v (x ^ (z ^ y))' = 1. [para(19(a,1),217(a,1,2,1))]. given #296 (A,wt=13): 137 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),22(a,1,2,1))]. given #297 (F,wt=12): 228 ((x v y) ^ z) v (x ^ z)' = 1. [para(22(a,1),217(a,1,2,1))]. given #298 (F,wt=12): 264 x v (y v (z v (x v z)')) = 1. [para(31(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #299 (T,wt=12): 266 x v (y v ((x ^ z) v y)') = 1. [para(31(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #300 (T,wt=12): 284 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(34(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #301 (A,wt=15): 138 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(22(a,1),19(a,1,2)),flip(a)]. given #302 (F,wt=12): 286 x ^ (y ^ ((x v z) ^ y)') = 0. [para(34(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #303 (F,wt=12): 333 x v ((x v y)' v (z v y)) = 1. [para(17(a,1),328(a,1,2)),rewrite(17(5))]. given #304 (T,wt=12): 339 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(19(a,1),329(a,1,2)),rewrite(19(5))]. given #305 (T,wt=12): 606 x v (y v (z v (x' v u))) = 1. [para(3(a,1),127(a,1,2))]. given #306 (A,wt=15): 139 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(22(a,1),26(a,1,2)),rewrite(2(4))]. given #307 (F,wt=12): 608 x v (y v ((x ^ z)' v u)) = 1. [para(127(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #308 (F,wt=12): 615 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),130(a,1,2))]. given #309 (T,wt=12): 617 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(130(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #310 (T,wt=12): 734 x v (y v (z v (u v x'))) = 1. [para(3(a,1),132(a,1,2,2))]. given #311 (A,wt=15): 143 x v (y ^ x') != 1 | y ^ x' = x'. [para(94(a,1),10(b,1)),flip(c),xx(b)]. given #312 (F,wt=12): 736 x v (y v (z v (x ^ u)')) = 1. [para(132(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #313 (F,wt=12): 745 x ^ ((y v (x v z))' ^ u) = 0. [para(17(a,1),140(a,1,2,1,1))]. given #314 (T,wt=12): 751 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),142(a,1,2,2))]. given #315 (T,wt=12): 753 x ^ (y ^ (z ^ (x v u)')) = 0. [para(142(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #316 (A,wt=15): 148 x v (x v y)' != 1 | (x v y)' = x'. [para(135(a,1),10(b,1)),flip(c),xx(b)]. given #317 (F,wt=12): 762 x ^ (y ^ (z v (x v u))') = 0. [para(17(a,1),144(a,1,2,2,1))]. given #318 (F,wt=12): 826 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),149(a,1,2,1))]. given #319 (T,wt=12): 834 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),162(a,1,2,1,2))]. given #320 (T,wt=12): 835 x ^ ((y v (z v x))' ^ u) = 0. [para(162(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #321 (A,wt=13): 154 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),23(a,1,2,2,1))]. given #322 (F,wt=12): 839 x ^ (y ^ (z v (u v x))') = 0. [para(162(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #323 (F,wt=12): 846 (x v c1) ^ (y v (c2 v x))' = 0. [para(422(a,1),162(a,1,2,1,2))]. given #324 (T,wt=12): 852 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(163(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #325 (T,wt=12): 858 (x v c1) ^ ((c2 v x)' ^ y) = 0. [para(422(a,1),163(a,1,2,1,1))]. given #326 (A,wt=19): 155 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(23(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #327 (F,wt=12): 861 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),167(a,1,2))]. given #328 (F,wt=12): 870 (x v c1) ^ (y ^ (c2 v x)') = 0. [para(422(a,1),167(a,1,2,2,1))]. given #329 (T,wt=12): 910 c1 ^ (x ^ (y ^ (c2' ^ z))) = 0. [para(5(a,1),169(a,1,2))]. given #330 (T,wt=12): 917 c1 ^ (x ^ (y ^ (z ^ c2'))) = 0. [para(5(a,1),170(a,1,2,2))]. given #331 (A,wt=26): 156 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x' = y ^ ((x ^ y) v z). [para(23(a,1),10(b,1))]. given #332 (F,wt=12): 927 x v ((y ^ (x ^ z))' v u) = 1. [para(19(a,1),189(a,1,2,1,1))]. given #333 (F,wt=12): 936 x v (y v (z ^ (x ^ u))') = 1. [para(19(a,1),190(a,1,2,2,1))]. given #334 (T,wt=12): 1054 c1 ^ ((x v (c2 v y))' ^ z) = 0. [para(17(a,1),199(a,1,2,1,1))]. given #335 (T,wt=12): 1055 c1 ^ (x ^ ((c2 v y)' ^ z)) = 0. [para(199(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #336 (A,wt=15): 157 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(17(a,1),23(a,1,2,2))]. given #337 (F,wt=12): 1060 c1 ^ (x v (y v (c2 v z)))' = 0. [para(3(a,1),201(a,1,2,1))]. given #338 (F,wt=12): 1062 c1 ^ (x ^ (y v (c2 v z))') = 0. [para(201(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #339 (T,wt=12): 1067 c1 ^ (x ^ (y ^ (c2 v z)')) = 0. [para(5(a,1),202(a,1,2))]. given #340 (T,wt=12): 1074 c1 ^ (x v (y v (z v c2)))' = 0. [para(3(a,1),203(a,1,2,1,2))]. given #341 (A,wt=17): 158 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(23(a,1),19(a,1,2)),flip(a)]. given #342 (F,wt=12): 1075 c1 ^ ((x v (y v c2))' ^ z) = 0. [para(203(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #343 (F,wt=12): 1077 c1 ^ (x ^ (y v (z v c2))') = 0. [para(203(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #344 (T,wt=12): 1197 c1 ^ (x ^ ((y v c2)' ^ z)) = 0. [para(204(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #345 (T,wt=12): 1203 c1 ^ (x ^ (y ^ (z v c2)')) = 0. [para(5(a,1),206(a,1,2))]. given #346 (A,wt=19): 159 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(19(a,1),23(a,1,2,2,1)),rewrite(5(5))]. given #347 (F,wt=12): 1213 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),220(a,1,2,1))]. given #348 (F,wt=12): 1223 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),221(a,1,2,1,1))]. given #349 (T,wt=12): 1225 x v (y v ((z ^ x)' v u)) = 1. [para(221(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #350 (T,wt=12): 1229 (c2 ^ x) v ((c1 ^ x)' v y) = 1. [para(59(a,1),221(a,1,2,1,1))]. given #351 (A,wt=19): 160 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(23(a,1),26(a,1,2)),rewrite(2(5))]. given #352 (F,wt=12): 1231 (x ^ c2) v ((x ^ c1)' v y) = 1. [para(89(a,1),221(a,1,2,1,1))]. given #353 (F,wt=12): 1279 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),223(a,1,2,1,2))]. given #354 (T,wt=12): 1281 x v (y v (z ^ (u ^ x))') = 1. [para(223(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #355 (T,wt=12): 1286 (c2 ^ x) v (y ^ (c1 ^ x))' = 1. [para(59(a,1),223(a,1,2,1,2))]. given #356 (A,wt=15): 161 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(23(a,1),22(a,1,2)),rewrite(22(3)),flip(a)]. given #357 (F,wt=11): 6552 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(161(a,1),59(a,1)),rewrite(13(3),4(6)),flip(a)]. given #358 (F,wt=11): 6631 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),6552(a,1,2,1,2))]. given #359 (T,wt=11): 6632 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(2(a,1),6552(a,1,2))]. given #360 (T,wt=11): 6675 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),6631(a,1,2))]. given #361 (A,wt=15): 165 x v (y v x)' != 1 | (y v x)' = x'. [para(145(a,1),10(b,1)),flip(c),xx(b)]. given #362 (F,wt=12): 1288 (x ^ c2) v (y ^ (x ^ c1))' = 1. [para(89(a,1),223(a,1,2,1,2))]. given #363 (F,wt=12): 1300 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),226(a,1,2))]. given #364 (T,wt=12): 1305 (c2 ^ x) v (y v (c1 ^ x)') = 1. [para(59(a,1),226(a,1,2,2,1))]. given #365 (T,wt=12): 1307 (x ^ c2) v (y v (x ^ c1)') = 1. [para(89(a,1),226(a,1,2,2,1))]. given #366 (A,wt=15): 168 c1 v (c2' ^ x) != 1 | c2' ^ x = c1'. [para(151(a,1),10(b,1)),flip(c),xx(b)]. given #367 (F,wt=12): 1330 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(73(a,1),230(a,1,2,1))]. given #368 (F,wt=12): 1333 (c2 ^ (x v (y v c1))) v c1' = 1. [para(96(a,1),230(a,1,2,1))]. given #369 (T,wt=12): 1345 c2 v (x v (y v (c1' v z))) = 1. [para(3(a,1),234(a,1,2))]. given #370 (T,wt=12): 1558 c2 v (x v (y v (z v c1'))) = 1. [para(3(a,1),235(a,1,2,2))]. given #371 (A,wt=15): 171 c1 v (x ^ c2') != 1 | x ^ c2' = c1'. [para(153(a,1),10(b,1)),flip(c),xx(b)]. given #372 (F,wt=12): 1568 x v (y v ((y v x)' v z)) = 1. [para(261(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #373 (F,wt=12): 1572 x v (y v (z v (z v x)')) = 1. [para(261(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #374 (T,wt=12): 1574 x v (y v (y v (x ^ z))') = 1. [para(261(a,1),24(a,1,2)),rewrite(90(2)),flip(a)]. given #375 (T,wt=12): 1583 c2 v ((x ^ (y ^ c1))' v z) = 1. [para(5(a,1),267(a,1,2,1,1))]. given #376 (A,wt=13): 172 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(59(a,1),5(a,2,2)),rewrite(19(5),5(4))]. given #377 (F,wt=12): 1585 c2 v (x v ((y ^ c1)' v z)) = 1. [para(267(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #378 (F,wt=12): 1596 c2 v (x ^ (y ^ (z ^ c1)))' = 1. [para(5(a,1),269(a,1,2,1,2))]. given #379 (T,wt=12): 1598 c2 v (x v (y ^ (z ^ c1))') = 1. [para(269(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #380 (T,wt=12): 1727 c2 v (x v (y v (z ^ c1)')) = 1. [para(3(a,1),271(a,1,2))]. given #381 (A,wt=18): 174 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1' = c2 ^ x. [para(59(a,1),10(b,1))]. given #382 (F,wt=12): 1738 c2 v (x v ((c1 ^ y)' v z)) = 1. [para(272(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #383 (F,wt=12): 1739 c2 v ((x ^ (c1 ^ y))' v z) = 1. [para(19(a,1),272(a,1,2,1,1))]. given #384 (T,wt=12): 1750 c2 v (x v (y v (c1 ^ z)')) = 1. [para(3(a,1),274(a,1,2))]. given #385 (T,wt=12): 1752 c2 v (x v (y ^ (c1 ^ z))') = 1. [para(19(a,1),274(a,1,2,2,1))]. given #386 (A,wt=13): 175 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(59(a,1),19(a,1,2)),flip(a)]. given #387 (F,wt=12): 1761 c2 v (x ^ (y ^ (c1 ^ z)))' = 1. [para(5(a,1),275(a,1,2,1))]. given #388 (F,wt=12): 1779 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(281(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #389 (T,wt=12): 1783 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(281(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #390 (T,wt=12): 1785 x ^ (y ^ (y ^ (x v z))') = 0. [para(281(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #391 (A,wt=13): 180 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(23(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #392 (F,wt=12): 1793 c1 ^ (x ^ ((c2 ^ x)' ^ y)) = 0. [para(287(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #393 (F,wt=12): 1796 c1 ^ (x ^ (y ^ (c2 ^ y)')) = 0. [para(287(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #394 (T,wt=12): 1822 (x v (y ^ z)) ^ (x v y)' = 0. [para(74(a,1),145(a,1,2,1))]. given #395 (T,wt=12): 1824 x v (y v (x v (y ^ z))') = 1. [para(74(a,1),328(a,1,2)),rewrite(2(5),3(5))]. given #396 (A,wt=17): 182 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(24(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #397 (F,wt=12): 1838 x' v (y v (z v (x v u))) = 1. [para(3(a,1),330(a,1,2))]. given #398 (F,wt=12): 1858 x' v (y v (z v (u v x))) = 1. [para(3(a,1),331(a,1,2,2))]. given #399 (T,wt=12): 1868 (x ^ (y ^ z))' v (u v y) = 1. [para(86(a,1),331(a,1,2,2))]. given #400 (T,wt=12): 1872 (x ^ (y ^ z))' v (u v z) = 1. [para(104(a,1),331(a,1,2,2))]. given #401 (A,wt=17): 183 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),24(a,1,2,1))]. given #402 (F,wt=12): 1874 (x ^ (y ^ c1))' v (z v c2) = 1. [para(255(a,1),331(a,1,2,2))]. given #403 (F,wt=12): 1875 (x ^ (c1 ^ y))' v (z v c2) = 1. [para(260(a,1),331(a,1,2,2))]. given #404 (T,wt=12): 1876 (x v c1)' v (y v (c2 v x)) = 1. [para(422(a,1),331(a,1,2,2))]. given #405 (T,wt=12): 1933 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),336(a,1,2))]. given #406 (A,wt=22): 185 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(24(a,1),10(a,1))]. given #407 (F,wt=12): 1943 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),337(a,1,2,2))]. given #408 (F,wt=12): 1952 (c2 ^ x)' ^ (y ^ (c1 ^ x)) = 0. [para(59(a,1),337(a,1,2,2))]. given #409 (T,wt=12): 1955 (x v (y v z))' ^ (u ^ y) = 0. [para(73(a,1),337(a,1,2,2))]. given #410 (T,wt=12): 1957 (x ^ c2)' ^ (y ^ (x ^ c1)) = 0. [para(89(a,1),337(a,1,2,2))]. given #411 (A,wt=15): 186 x v (y v ((x ^ z) v u)) = y v (x v u). [para(24(a,1),17(a,1,2)),flip(a)]. given #412 (F,wt=12): 1958 (x v (y v z))' ^ (u ^ z) = 0. [para(96(a,1),337(a,1,2,2))]. given #413 (F,wt=12): 1960 (x v (c2 v y))' ^ (z ^ c1) = 0. [para(193(a,1),337(a,1,2,2))]. given #414 (T,wt=12): 1961 (x v (y v c2))' ^ (z ^ c1) = 0. [para(195(a,1),337(a,1,2,2))]. given #415 (T,wt=12): 1983 (x ^ (y v z)) v (x ^ y)' = 1. [para(85(a,1),217(a,1,2,1))]. given #416 (A,wt=13): 187 x v ((y ^ (x ^ z)) v u) = x v u. [para(19(a,1),24(a,1,2,1))]. given #417 (F,wt=12): 1984 x ^ (y ^ (x ^ (y v z))') = 0. [para(85(a,1),329(a,1,2)),rewrite(4(5),5(5))]. given #418 (F,wt=12): 2008 x ^ (c1 ^ ((x ^ c2)' ^ y)) = 0. [para(346(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #419 (T,wt=12): 2010 c1 ^ (x ^ (y ^ (y ^ c2)')) = 0. [para(346(a,1),5(a,2,2)),rewrite(19(7),5(6),93(9))]. given #420 (T,wt=12): 2013 x ^ (y ^ (c1 ^ (x ^ c2)')) = 0. [para(346(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #421 (A,wt=15): 188 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(24(a,1),20(a,1,2)),rewrite(4(4))]. given #422 (F,wt=12): 2014 x ^ (c1 ^ (c2 ^ (x v y))') = 0. [para(346(a,1),22(a,1,2)),rewrite(93(2),4(5)),flip(a)]. given #423 (F,wt=12): 2025 (x v c1) ^ ((x v c2)' ^ y) = 0. [para(425(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #424 (T,wt=12): 2027 (x v c1) ^ (y ^ (x v c2)') = 0. [para(425(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #425 (T,wt=12): 2034 x v (c2 v ((x v c1)' v y)) = 1. [para(429(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #426 (A,wt=14): 192 c2 v x != 1 | c1 != 0 | c1' = c2 v x. [para(173(a,1),10(b,1)),rewrite(110(4))]. given #427 (F,wt=12): 2036 c2 v (x v (y v (y v c1)')) = 1. [para(429(a,1),3(a,2,2)),rewrite(17(7),3(6),90(9))]. given #428 (F,wt=12): 2039 x v (y v (c2 v (x v c1)')) = 1. [para(429(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #429 (T,wt=12): 2040 x v (c2 v (c1 v (x ^ y))') = 1. [para(429(a,1),24(a,1,2)),rewrite(90(2),2(5)),flip(a)]. given #430 (T,wt=12): 2118 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0. [para(86(a,1),543(a,1,2,1)),rewrite(2(5))]. given #431 (A,wt=14): 197 x v c2 != 1 | c1 != 0 | c1' = x v c2. [para(176(a,1),10(b,1)),rewrite(112(4))]. given #432 (F,wt=12): 2119 (c1 v (x ^ (y ^ c2))) ^ c2' = 0. [para(104(a,1),543(a,1,2,1)),rewrite(2(5))]. given #433 (F,wt=12): 2128 c2 v (x v ((x v c1)' v y)) = 1. [para(545(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #434 (T,wt=12): 2140 (x ^ c2) v ((c1 ^ x)' v y) = 1. [para(1321(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #435 (T,wt=12): 2142 (x ^ c2) v (y v (c1 ^ x)') = 1. [para(1321(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #436 (A,wt=15): 200 c1 v (c2 v x)' != 1 | (c2 v x)' = c1'. [para(179(a,1),10(b,1)),flip(c),xx(b)]. given #437 (F,wt=12): 2150 (c2 ^ x) v ((x ^ c1)' v y) = 1. [para(1322(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #438 (F,wt=12): 2152 (c2 ^ x) v (y v (x ^ c1)') = 1. [para(1322(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #439 (T,wt=12): 2168 ((x v y) ^ z) v (y ^ z)' = 1. [para(97(a,1),217(a,1,2,1))]. given #440 (T,wt=12): 2170 x ^ (y ^ ((z v x) ^ y)') = 0. [para(34(a,1),97(a,1,2)),rewrite(93(2)),flip(a)]. given #441 (A,wt=15): 205 c1 v (x v c2)' != 1 | (x v c2)' = c1'. [para(181(a,1),10(b,1)),flip(c),xx(b)]. given #442 (F,wt=12): 2188 x ^ (y ^ (y ^ (z v x))') = 0. [para(281(a,1),97(a,1,2)),rewrite(93(2)),flip(a)]. given #443 (F,wt=12): 2192 x ^ (c1 ^ (c2 ^ (y v x))') = 0. [para(346(a,1),97(a,1,2)),rewrite(93(2),4(5)),flip(a)]. given #444 (T,wt=12): 2198 (c2 ^ (c1 v x)) v (c1' v y) = 1. [para(1323(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #445 (T,wt=12): 2200 (c2 ^ (c1 v x)) v (y v c1') = 1. [para(1323(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #446 (A,wt=13): 207 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),25(a,1,2,2,1))]. given #447 (F,wt=12): 2210 (c2 ^ (x v c1)) v (c1' v y) = 1. [para(1327(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #448 (F,wt=12): 2212 (c2 ^ (x v c1)) v (y v c1') = 1. [para(1327(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #449 (T,wt=12): 2221 c1 ^ (x ^ ((x ^ c2)' ^ y)) = 0. [para(1786(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #450 (T,wt=12): 2257 x ^ (c1 ^ ((c2 ^ x)' ^ y)) = 0. [para(1797(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #451 (A,wt=19): 208 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(25(a,1),3(a,1)),rewrite(3(2),3(4)),flip(a)]. given #452 (F,wt=12): 2258 x ^ (y ^ (c1 ^ (c2 ^ x)')) = 0. [para(1797(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #453 (F,wt=12): 2266 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0. [para(1799(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #454 (T,wt=12): 2268 c1 ^ (c2 ^ (x v (c1 v y)))' = 0. [para(17(a,1),1799(a,1,2,1,2))]. given #455 (T,wt=12): 2269 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0. [para(1799(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #456 (A,wt=26): 209 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x' = y v ((x v y) ^ z). [para(25(a,1),10(a,1))]. given #457 (F,wt=12): 2276 c1' v (x v (y v (c2 v z))) = 1. [para(3(a,1),1844(a,1,2))]. given #458 (F,wt=12): 2295 c1' v (x v (y v (z v c2))) = 1. [para(3(a,1),1846(a,1,2,2))]. given #459 (T,wt=12): 2305 (x ^ y)' v (z v (x v u)) = 1. [para(1859(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #460 (T,wt=12): 2306 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),1859(a,1,2))]. given #461 (A,wt=17): 210 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(25(a,1),17(a,1,2)),flip(a)]. given #462 (F,wt=12): 2313 c2 v (x v ((x v c1) ^ y)') = 1. [para(422(a,1),1859(a,1,2)),rewrite(2(7),3(7))]. given #463 (F,wt=12): 2321 (x ^ y)' v (z v (y v u)) = 1. [para(1862(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #464 (T,wt=12): 2322 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),1862(a,1,2))]. given #465 (T,wt=12): 2328 (c1 ^ x)' v (y v (c2 ^ x)) = 1. [para(59(a,1),1862(a,1,1,1))]. given #466 (A,wt=19): 211 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(17(a,1),25(a,1,2,2,1)),rewrite(3(5))]. given #467 (F,wt=12): 2331 (x ^ c1)' v (y v (x ^ c2)) = 1. [para(89(a,1),1862(a,1,1,1))]. given #468 (F,wt=12): 2334 c2 v (x v (y ^ (x v c1))') = 1. [para(422(a,1),1862(a,1,2)),rewrite(2(7),3(7))]. given #469 (T,wt=12): 2350 (x ^ c1)' v (y v (c2 v z)) = 1. [para(1866(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #470 (T,wt=12): 2351 (x ^ c1)' v (y v (z v c2)) = 1. [para(3(a,1),1866(a,1,2))]. given #471 (A,wt=15): 212 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(19(a,1),25(a,1,2,2))]. given #472 (F,wt=12): 2394 (c1 ^ x)' v (y v (c2 v z)) = 1. [para(1867(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #473 (F,wt=12): 2395 (c1 ^ x)' v (y v (z v c2)) = 1. [para(3(a,1),1867(a,1,2))]. given #474 (T,wt=12): 2404 c2' ^ (x ^ (y ^ (c1 ^ z))) = 0. [para(1935(a,1),5(a,1,1)),rewrite(83(2),5(7),5(6)),flip(a)]. given #475 (T,wt=12): 2405 c2' ^ (x ^ (y ^ (z ^ c1))) = 0. [para(5(a,1),1935(a,1,2,2))]. given #476 (A,wt=19): 213 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(25(a,1),20(a,1,2)),rewrite(4(5))]. given #477 (F,wt=12): 2414 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(1944(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #478 (F,wt=12): 2415 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),1944(a,1,2))]. given #479 (T,wt=12): 2420 c1 ^ (x ^ ((c2 ^ x) v y)') = 0. [para(59(a,1),1944(a,1,2)),rewrite(4(7),5(7))]. given #480 (T,wt=12): 2422 x ^ (c1 ^ ((x ^ c2) v y)') = 0. [para(89(a,1),1944(a,1,2)),rewrite(4(7),5(7))]. given #481 (A,wt=14): 214 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(25(a,1),145(a,1,2,1))]. given #482 (F,wt=12): 2438 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(1948(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #483 (F,wt=12): 2439 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),1948(a,1,2))]. given #484 (T,wt=12): 2444 c1 ^ (x ^ (y v (c2 ^ x))') = 0. [para(59(a,1),1948(a,1,2)),rewrite(4(7),5(7))]. given #485 (T,wt=12): 2448 x ^ (c1 ^ (y v (x ^ c2))') = 0. [para(89(a,1),1948(a,1,2)),rewrite(4(7),5(7))]. given #486 (A,wt=15): 215 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(25(a,1),24(a,1,2)),rewrite(24(3)),flip(a)]. given #487 (F,wt=12): 2450 (c2 v x)' ^ (y ^ (x v c1)) = 0. [para(422(a,1),1948(a,1,1,1))]. given #488 (F,wt=12): 2468 (x ^ (y v z)) v (x ^ z)' = 1. [para(101(a,1),217(a,1,2,1))]. given #489 (T,wt=12): 2470 x ^ (y ^ (x ^ (z v y))') = 0. [para(101(a,1),329(a,1,2)),rewrite(4(5),5(5))]. given #490 (T,wt=12): 2493 (c2 v x)' ^ (y ^ (c1 ^ z)) = 0. [para(1953(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #491 (A,wt=15): 219 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(184(a,1),10(a,1)),flip(c),xx(a)]. given #492 (F,wt=12): 2494 (c2 v x)' ^ (y ^ (z ^ c1)) = 0. [para(5(a,1),1953(a,1,2))]. given #493 (F,wt=12): 2502 (x v c2)' ^ (y ^ (c1 ^ z)) = 0. [para(1954(a,1),5(a,1,1)),rewrite(83(2),5(7)),flip(a)]. given #494 (T,wt=12): 2503 (x v c2)' ^ (y ^ (z ^ c1)) = 0. [para(5(a,1),1954(a,1,2))]. given #495 (T,wt=12): 2520 (c1 v x) ^ ((x v c2)' ^ y) = 0. [para(2022(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #496 (A,wt=15): 224 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(217(a,1),10(a,1)),flip(c),xx(a)]. given #497 (F,wt=12): 2523 (c1 v x) ^ (y ^ (x v c2)') = 0. [para(2022(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #498 (F,wt=12): 2538 ((x ^ y) v z) ^ (y v z)' = 0. [para(102(a,1),145(a,1,2,1))]. given #499 (T,wt=12): 2541 x v (y v ((z ^ x) v y)') = 1. [para(31(a,1),102(a,1,2)),rewrite(90(2)),flip(a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 87 (0.00 of 3.83 sec). given #500 (T,wt=12): 2566 x v (y v (y v (z ^ x))') = 1. [para(261(a,1),102(a,1,2)),rewrite(90(2)),flip(a)]. given #501 (A,wt=14): 229 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(23(a,1),217(a,1,2,1))]. given #502 (F,wt=12): 2570 x v (c2 v (c1 v (y ^ x))') = 1. [para(429(a,1),102(a,1,2)),rewrite(90(2),2(5)),flip(a)]. given #503 (F,wt=12): 2587 x v (c2 v ((c1 v x)' v y)) = 1. [para(2033(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #504 (T,wt=12): 2588 c2 v (x v (y v (c1 v y)')) = 1. [para(2033(a,1),3(a,2,2)),rewrite(17(7),3(6),90(9))]. given #505 (T,wt=12): 2590 x v (y v (c2 v (c1 v x)')) = 1. [para(2033(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #506 (A,wt=15): 236 c2 ^ (x v c1') != 0 | c2' = x v c1'. [para(231(a,1),10(a,1)),xx(a)]. given #507 (F,wt=12): 2604 (c1 v x) ^ ((c2 v x)' ^ y) = 0. [para(2111(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #508 (F,wt=12): 2606 (c1 v x) ^ (y ^ (c2 v x)') = 0. [para(2111(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #509 (T,wt=12): 2614 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0. [para(2112(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #510 (T,wt=12): 2616 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0. [para(2112(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #511 (A,wt=13): 237 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),27(a,1,1))]. given #512 (F,wt=12): 2625 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0. [para(2115(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #513 (F,wt=12): 2627 (c1 v (x ^ c2)) ^ (y ^ c2') = 0. [para(2115(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #514 (T,wt=12): 2671 c2 v (x v ((c1 v x)' v y)) = 1. [para(2127(a,1),3(a,1,1)),rewrite(80(2),3(7)),flip(a)]. given #515 (T,wt=12): 2680 c2 v ((c1 v (c2 ^ x))' v y) = 1. [para(2130(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #516 (A,wt=13): 238 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),27(a,1,2)),rewrite(5(3))]. given #517 (F,wt=12): 2682 c2 v (x v (c1 v (c2 ^ y))') = 1. [para(2130(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #518 (F,wt=12): 2683 c2 v (c1 v (x ^ (c2 ^ y)))' = 1. [para(19(a,1),2130(a,1,2,1,2))]. given #519 (T,wt=12): 2693 c1 ^ (c2 ^ (x v (y v c1)))' = 0. [para(3(a,1),2189(a,1,2,1,2))]. given #520 (T,wt=12): 2694 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0. [para(2189(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #521 (A,wt=19): 239 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),27(a,1,1)),rewrite(5(5),5(8))]. given #522 (F,wt=12): 2696 c1 ^ (x ^ (c2 ^ (y v c1))') = 0. [para(2189(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #523 (F,wt=12): 2703 c1' v ((c2 ^ (c1 v x)) v y) = 1. [para(2197(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #524 (T,wt=12): 2704 c1' v (x v (c2 ^ (c1 v y))) = 1. [para(2197(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #525 (T,wt=12): 2705 c1' v (c2 ^ (x v (c1 v y))) = 1. [para(17(a,1),2197(a,1,2,2))]. given #526 (A,wt=17): 241 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(27(a,1),17(a,1,2)),flip(a)]. given #527 (F,wt=12): 2732 c1' v ((c2 ^ (x v c1)) v y) = 1. [para(2209(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #528 (F,wt=12): 2733 c1' v (c2 ^ (x v (y v c1))) = 1. [para(3(a,1),2209(a,1,2,2))]. given #529 (T,wt=12): 2734 c1' v (x v (c2 ^ (y v c1))) = 1. [para(2209(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #530 (T,wt=12): 2743 c2 v ((c1 v (x ^ c2))' v y) = 1. [para(2572(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #531 (A,wt=19): 242 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(19(a,1),27(a,1,1)),rewrite(5(4))]. given #532 (F,wt=12): 2744 c2 v (c1 v (x ^ (y ^ c2)))' = 1. [para(5(a,1),2572(a,1,2,1,2))]. given #533 (F,wt=12): 2746 c2 v (x v (c1 v (y ^ c2))') = 1. [para(2572(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #534 (T,wt=12): 2756 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(2613(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #535 (T,wt=12): 2757 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(2613(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #536 (A,wt=15): 243 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(19(a,1),27(a,1,2,2))]. given #537 (F,wt=12): 2758 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(19(a,1),2613(a,1,2,2))]. given #538 (F,wt=12): 2773 (x v (y ^ z)) ^ (x v z)' = 0. [para(107(a,1),145(a,1,2,1))]. given #539 (T,wt=12): 2776 x v (y v (x v (z ^ y))') = 1. [para(107(a,1),328(a,1,2)),rewrite(2(5),3(5))]. given #540 (T,wt=12): 2809 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(2624(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #541 (A,wt=22): 245 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [back_rewrite(240),rewrite(244(7))]. given #542 (F,wt=12): 2810 c2' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(5(a,1),2624(a,1,2,2))]. given #543 (F,wt=12): 2811 c2' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(2624(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #544 (T,wt=12): 2833 x v (c2 v (y ^ (x v c1))') = 1. [para(122(a,1),223(a,1,2,1,2)),rewrite(3(7))]. given #545 (T,wt=12): 2834 x v (c2 v (y v (x v c1)')) = 1. [para(122(a,1),226(a,1,2,2,1)),rewrite(3(7))]. given #546 (A,wt=15): 246 c2 ^ (c1' v x) != 0 | c2' = c1' v x. [para(232(a,1),10(a,1)),xx(a)]. given #547 (F,wt=12): 2835 (x v c2)' ^ (y ^ (x v c1)) = 0. [para(122(a,1),337(a,1,2,2))]. given #548 (F,wt=12): 2837 (x v c1)' v (y v (x v c2)) = 1. [para(122(a,1),1862(a,1,1,1))]. given #549 (T,wt=12): 2838 (x v c1) ^ (x v (c2 v y))' = 0. [para(122(a,1),1944(a,1,2)),rewrite(3(3),4(7))]. given #550 (T,wt=12): 2839 (x v c1) ^ (y v (x v c2))' = 0. [para(122(a,1),1948(a,1,2)),rewrite(4(7))]. given #551 (A,wt=13): 247 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(5(a,1),60(a,1,2)),rewrite(4(8))]. given #552 (F,wt=12): 2857 c1 ^ (x ^ (y ^ (c2 ^ x)')) = 0. [para(177(a,1),144(a,1,2,2,1)),rewrite(5(7))]. given #553 (F,wt=12): 2925 ((c2 v x) ^ y) v (c1 ^ y)' = 1. [para(178(a,1),217(a,1,2,1))]. given #554 (T,wt=12): 2927 c1 ^ (x ^ ((c2 v y) ^ x)') = 0. [para(34(a,1),178(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #555 (T,wt=12): 2940 c1 ^ (x ^ (x ^ (c2 v y))') = 0. [para(281(a,1),178(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #556 (A,wt=14): 249 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1. [para(60(a,1),10(b,1)),rewrite(248(4))]. given #557 (F,wt=12): 2953 (x ^ (c2 v y)) v (x ^ c1)' = 1. [para(194(a,1),217(a,1,2,1))]. given #558 (F,wt=12): 2954 x ^ (c1 ^ (x ^ (c2 v y))') = 0. [para(194(a,1),329(a,1,2)),rewrite(4(7),5(7))]. given #559 (T,wt=12): 2978 ((x v c2) ^ y) v (c1 ^ y)' = 1. [para(196(a,1),217(a,1,2,1))]. given #560 (T,wt=12): 2980 c1 ^ (x ^ ((y v c2) ^ x)') = 0. [para(34(a,1),196(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #561 (A,wt=13): 252 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(60(a,1),27(a,1,2,2))]. given #562 (F,wt=12): 2994 c1 ^ (x ^ (x ^ (y v c2))') = 0. [para(281(a,1),196(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #563 (F,wt=12): 3007 (x ^ (y v c2)) v (x ^ c1)' = 1. [para(198(a,1),217(a,1,2,1))]. given #564 (T,wt=12): 3008 x ^ (c1 ^ (x ^ (y v c2))') = 0. [para(198(a,1),329(a,1,2)),rewrite(4(7),5(7))]. given #565 (T,wt=12): 3046 x v (y v (z v (y v x)')) = 1. [para(113(a,1),190(a,1,2,2,1)),rewrite(3(5))]. given #566 (A,wt=14): 258 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x. [para(254(a,1),10(a,1)),rewrite(19(7),59(7))]. given #567 (F,wt=12): 3049 x v (y v (z ^ (y v x))') = 1. [para(113(a,1),220(a,1,2,1,2)),rewrite(3(5))]. given #568 (F,wt=12): 3053 (x v y)' ^ (z ^ (y v x)) = 0. [para(113(a,1),336(a,1,2,2))]. given #569 (T,wt=12): 3055 (x v y)' v (z v (y v x)) = 1. [para(113(a,1),1859(a,1,1,1))]. given #570 (T,wt=12): 3060 ((x ^ c1) v y) ^ (c2 v y)' = 0. [para(250(a,1),145(a,1,2,1))]. given #571 (A,wt=14): 262 x v (y v (z v (x v (y v z))')) = 1. [para(31(a,1),3(a,1)),rewrite(3(3)),flip(a)]. given #572 (F,wt=12): 3062 c2 v (x v ((y ^ c1) v x)') = 1. [para(31(a,1),250(a,1,2)),rewrite(2(3),80(3)),flip(a)]. given #573 (F,wt=12): 3078 c2 v (x v (x v (y ^ c1))') = 1. [para(261(a,1),250(a,1,2)),rewrite(2(3),80(3)),flip(a)]. given #574 (T,wt=12): 3101 x ^ (c1 ^ (y v (c2 ^ x))') = 0. [para(253(a,1),162(a,1,2,1,2)),rewrite(5(7))]. given #575 (T,wt=12): 3102 x ^ (c1 ^ (y ^ (c2 ^ x)')) = 0. [para(253(a,1),167(a,1,2,2,1)),rewrite(5(7))]. given #576 (A,wt=19): 263 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(31(a,1),10(a,1)),flip(c),xx(a)]. given #577 (F,wt=12): 3110 (x ^ c1)' v (y v (c2 ^ x)) = 1. [para(253(a,1),331(a,1,2,2))]. given #578 (F,wt=12): 3113 (c2 ^ x) v (x ^ (c1 ^ y))' = 1. [para(253(a,1),1859(a,1,2)),rewrite(5(3),2(7))]. given #579 (T,wt=12): 3114 (c2 ^ x) v (y ^ (x ^ c1))' = 1. [para(253(a,1),1862(a,1,2)),rewrite(2(7))]. given #580 (T,wt=12): 3116 (c2 ^ x)' ^ (y ^ (x ^ c1)) = 0. [para(253(a,1),1948(a,1,1,1))]. given #581 (A,wt=14): 265 x v (y v (z v (y v (x v z))')) = 1. [para(17(a,1),31(a,1,2,2,1)),rewrite(3(5))]. given #582 (F,wt=12): 3119 (x v (y ^ c1)) ^ (x v c2)' = 0. [para(256(a,1),145(a,1,2,1))]. given #583 (F,wt=12): 3121 x v (c2 v (x v (y ^ c1))') = 1. [para(256(a,1),328(a,1,2)),rewrite(2(7),3(7))]. given #584 (T,wt=12): 3161 x v ((y v x)' v (z v y)) = 1. [para(31(a,1),114(a,1,1)),rewrite(3(6),71(7),31(9))]. given #585 (T,wt=12): 3164 (x v y) ^ (y v (z v x))' = 0. [para(114(a,1),329(a,1,2)),rewrite(4(5))]. given #586 (A,wt=15): 270 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'. [para(251(a,1),10(a,1)),flip(c),xx(a)]. given #587 (F,wt=12): 3182 c2 v ((x v c1)' v (y v x)) = 1. [para(429(a,1),114(a,1,1)),rewrite(3(8),71(9),429(13))]. given #588 (F,wt=12): 3185 x v ((x v c1)' v (y v c2)) = 1. [para(545(a,1),114(a,1,1)),rewrite(3(8),71(9),545(13))]. given #589 (T,wt=12): 3186 (c1 ^ x)' v (y v (x ^ c2)) = 1. [para(1321(a,1),114(a,1,1)),rewrite(71(9),1321(13))]. given #590 (T,wt=12): 3192 c2 v ((c1 v x)' v (y v x)) = 1. [para(2033(a,1),114(a,1,1)),rewrite(3(8),71(9),2033(13))]. given #591 (A,wt=15): 273 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'. [para(268(a,1),10(a,1)),flip(c),xx(a)]. given #592 (F,wt=12): 3194 x v ((c1 v x)' v (y v c2)) = 1. [para(2127(a,1),114(a,1,1)),rewrite(3(8),71(9),2127(13))]. given #593 (F,wt=12): 3195 (c1 v (c2 ^ x))' v (y v c2) = 1. [para(2130(a,1),114(a,1,1)),rewrite(71(10),2130(15))]. given #594 (T,wt=12): 3196 (c1 v (x ^ c2))' v (y v c2) = 1. [para(2572(a,1),114(a,1,1)),rewrite(71(10),2572(15))]. given #595 (T,wt=12): 3208 ((c1 ^ x) v y) ^ (c2 v y)' = 0. [para(257(a,1),145(a,1,2,1))]. given #596 (A,wt=13): 276 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(62(a,1),5(a,2,2)),rewrite(19(3),5(2))]. given #597 (F,wt=12): 3210 c2 v (x v ((c1 ^ y) v x)') = 1. [para(31(a,1),257(a,1,2)),rewrite(2(3),80(3)),flip(a)]. given #598 (F,wt=12): 3226 c2 v (x v (x v (c1 ^ y))') = 1. [para(261(a,1),257(a,1,2)),rewrite(2(3),80(3)),flip(a)]. given #599 (T,wt=12): 3241 (x v (c1 ^ y)) ^ (x v c2)' = 0. [para(259(a,1),145(a,1,2,1))]. given #600 (T,wt=12): 3243 x v (c2 v (x v (c1 ^ y))') = 1. [para(259(a,1),328(a,1,2)),rewrite(2(7),3(7))]. given #601 (A,wt=13): 278 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),64(a,1,2)),rewrite(5(5))]. given #602 (F,wt=12): 3301 x ^ (y ^ (z v (y ^ x))') = 0. [para(280(a,1),162(a,1,2,1,2)),rewrite(5(5))]. given #603 (F,wt=12): 3302 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(280(a,1),167(a,1,2,2,1)),rewrite(5(5))]. given #604 (T,wt=12): 3313 (x ^ y)' v (z v (y ^ x)) = 1. [para(280(a,1),331(a,1,2,2))]. given #605 (T,wt=12): 3316 (x ^ y) v (y ^ (x ^ z))' = 1. [para(280(a,1),1859(a,1,2)),rewrite(5(2),2(5))]. given #606 (A,wt=14): 282 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(34(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #607 (F,wt=12): 3317 (x ^ y) v (z ^ (y ^ x))' = 1. [para(280(a,1),1862(a,1,2)),rewrite(2(5))]. given #608 (F,wt=12): 3319 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(280(a,1),1948(a,1,1,1))]. given #609 (T,wt=12): 3354 (x ^ y) v ((y ^ x)' v z) = 1. [para(3297(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #610 (T,wt=12): 3357 (x ^ y) v (z v (y ^ x)') = 1. [para(3297(a,1),17(a,1,2)),rewrite(90(2)),flip(a)]. given #611 (A,wt=19): 283 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(34(a,1),10(b,1)),flip(c),xx(b)]. given #612 (F,wt=12): 3377 (x v y) ^ (y v (x v z))' = 0. [para(291(a,1),1944(a,1,2)),rewrite(3(2),4(5))]. given #613 (F,wt=12): 3378 (x v y) ^ (z v (y v x))' = 0. [para(291(a,1),1948(a,1,2)),rewrite(4(5))]. given #614 (T,wt=12): 3381 (x v y) ^ ((y v x)' ^ z) = 0. [para(3371(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #615 (T,wt=12): 3383 (x v y) ^ (z ^ (y v x)') = 0. [para(3371(a,1),19(a,1,2)),rewrite(93(2)),flip(a)]. given #616 (A,wt=14): 285 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(19(a,1),34(a,1,2,2,1)),rewrite(5(5))]. given #617 (F,wt=12): 3461 (c1 v x) ^ (c2 v (x v y))' = 0. [para(2022(a,1),116(a,1,2)),rewrite(4(4),83(4),2(6)),flip(a)]. given #618 (F,wt=12): 3520 x ^ (c1 ^ (y ^ (x ^ c2)')) = 0. [para(344(a,1),144(a,1,2,2,1)),rewrite(5(7))]. given #619 (T,wt=12): 3737 x v (c2 v (y ^ (c1 v x))') = 1. [para(461(a,1),223(a,1,2,1,2)),rewrite(3(7))]. given #620 (T,wt=12): 3738 x v (c2 v (y v (c1 v x)')) = 1. [para(461(a,1),226(a,1,2,2,1)),rewrite(3(7))]. given #621 (A,wt=13): 288 x v (y v (x v z)) = y v (x v z). [para(67(a,1),3(a,2,2)),rewrite(17(3),3(2))]. given #622 (F,wt=12): 3739 (x v c2)' ^ (y ^ (c1 v x)) = 0. [para(461(a,1),337(a,1,2,2))]. given #623 (F,wt=12): 3742 (c1 v x)' v (y v (x v c2)) = 1. [para(461(a,1),1862(a,1,1,1))]. low water: id=6138, wt=52 given #624 (T,wt=12): 3743 (c1 v x) ^ (x v (c2 v y))' = 0. [para(461(a,1),1944(a,1,2)),rewrite(3(3),4(7))]. low water: id=6154, wt=50 low water: id=6015, wt=48 low water: id=6057, wt=46 given #625 (T,wt=12): 3744 (c1 v x) ^ (y v (x v c2))' = 0. [para(461(a,1),1948(a,1,2)),rewrite(4(7))]. low water: id=6365, wt=45 given #626 (A,wt=13): 290 x v (y v (z v x)) = y v (z v x). [para(3(a,1),69(a,1,2)),rewrite(3(5))]. low water: id=6124, wt=44 low water: id=6563, wt=43 low water: id=6613, wt=42 low water: id=6364, wt=41 given #627 (F,wt=12): 3857 c2 v (x v (y v (x v c1)')) = 1. [para(542(a,1),226(a,1,2,2,1)),rewrite(3(7))]. given #628 (F,wt=12): 3861 (x v c1) ^ (c2 v (x v y))' = 0. [para(542(a,1),1944(a,1,2)),rewrite(3(3),4(7))]. low water: id=6555, wt=40 given #629 (T,wt=12): 3938 c2 v (x v (y ^ (c1 v x))') = 1. [para(2376(a,1),223(a,1,2,1,2)),rewrite(3(7))]. given #630 (T,wt=12): 3939 c2 v (x v (y v (c1 v x)')) = 1. [para(2376(a,1),226(a,1,2,2,1)),rewrite(3(7))]. given #631 (A,wt=15): 293 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),73(a,1,2,2))]. low water: id=6562, wt=39 low water: id=6600, wt=38 low water: id=6354, wt=37 low water: id=6572, wt=36 low water: id=6625, wt=35 given #632 (F,wt=12): 3940 (c2 v x)' ^ (y ^ (c1 v x)) = 0. [para(2376(a,1),337(a,1,2,2))]. given #633 (F,wt=12): 3942 (c1 v x)' v (y v (c2 v x)) = 1. [para(2376(a,1),1862(a,1,1,1))]. given #634 (T,wt=12): 3943 (c1 v x) ^ (y v (c2 v x))' = 0. [para(2376(a,1),1948(a,1,2)),rewrite(4(7))]. given #635 (T,wt=12): 4226 (c2 ^ x) v (c1 ^ (x ^ y))' = 1. [para(4035(a,1),1859(a,1,2)),rewrite(5(3),2(7))]. low water: id=7059, wt=34 given #636 (A,wt=18): 295 x v (y v z) != 1 | 0 != y | y' = x v (y v z). [para(73(a,1),10(b,1)),rewrite(288(3)),flip(b)]. given #637 (F,wt=12): 4266 (x v c1) ^ (x v (y v c2))' = 0. [para(112(a,1),146(a,1,2,1,2))]. low water: id=7192, wt=33 given #638 (F,wt=12): 4273 ((x ^ y) v z) ^ (z v x)' = 0. [para(292(a,1),146(a,1,2,1))]. given #639 (T,wt=12): 4276 ((x ^ y) v z) ^ (z v y)' = 0. [para(2542(a,1),146(a,1,2,1))]. low water: id=7293, wt=32 low water: id=7440, wt=31 given #640 (T,wt=12): 4280 ((x ^ c1) v y) ^ (y v c2)' = 0. [para(3063(a,1),146(a,1,2,1))]. given #641 (A,wt=13): 296 x ^ (y ^ (z v (x v u))) = y ^ x. [para(73(a,1),19(a,1,2)),flip(a)]. low water: id=7150, wt=30 low water: id=7728, wt=29 given #642 (F,wt=12): 4282 ((c1 ^ x) v y) ^ (y v c2)' = 0. [para(3211(a,1),146(a,1,2,1))]. given #643 (F,wt=12): 4368 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),147(a,1,2,2,1,1))]. low water: id=7891, wt=28 given #644 (T,wt=12): 4434 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),191(a,1,1))]. low water: id=8073, wt=27 given #645 (T,wt=12): 4436 (x v y)' ^ ((x ^ z) v y) = 0. [para(191(a,1),4(a,1)),flip(a)]. given #646 (A,wt=15): 297 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),86(a,1,2,2))]. given #647 (F,wt=12): 4438 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),191(a,1,2,1))]. given #648 (F,wt=12): 4443 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(26(a,1),191(a,1,2,1))]. given #649 (T,wt=12): 4447 ((c2 ^ x) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),191(a,1,2,1))]. given #650 (T,wt=12): 4448 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),191(a,1,2,1))]. given #651 (A,wt=18): 299 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(86(a,1),10(a,1)),rewrite(276(5)),flip(a)]. given #652 (F,wt=12): 4552 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),216(a,1,2,2,1,1))]. given #653 (F,wt=12): 4567 c2 v (x v ((c1 v x) ^ y)') = 1. [para(216(a,1),2033(a,1,2,2,1)),rewrite(79(8),2(8),77(8),2(7))]. given #654 (T,wt=12): 4572 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),218(a,1,2,1)),rewrite(5(3))]. low water: id=8407, wt=26 given #655 (T,wt=12): 4575 (x ^ c2) v (x ^ (y ^ c1))' = 1. [para(60(a,1),218(a,1,2,1,2))]. given #656 (A,wt=13): 300 x v (y v (z ^ (x ^ u))) = y v x. [para(86(a,1),17(a,1,2)),flip(a)]. given #657 (F,wt=12): 4586 ((x v y) ^ z) v (z ^ x)' = 1. [para(279(a,1),218(a,1,2,1))]. given #658 (F,wt=12): 4590 ((x v y) ^ z) v (z ^ y)' = 1. [para(2169(a,1),218(a,1,2,1))]. given #659 (T,wt=12): 4592 ((c2 v x) ^ y) v (y ^ c1)' = 1. [para(2926(a,1),218(a,1,2,1))]. given #660 (T,wt=12): 4594 ((x v c2) ^ y) v (y ^ c1)' = 1. [para(2979(a,1),218(a,1,2,1))]. given #661 (A,wt=20): 301 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),36(a,1))]. given #662 (F,wt=12): 4722 (x ^ y)' v ((x v z) ^ y) = 1. [para(228(a,1),2(a,1)),flip(a)]. low water: id=8380, wt=25 given #663 (F,wt=12): 4723 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),228(a,1,1))]. given #664 (T,wt=12): 4724 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),228(a,1,2,1))]. given #665 (T,wt=12): 4728 ((x v y) ^ (z v x)) v x' = 1. [para(20(a,1),228(a,1,2,1))]. given #666 (A,wt=14): 302 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),36(b,1))]. low water: id=8932, wt=24 given #667 (F,wt=12): 4732 ((c1 v x) ^ (c2 v y)) v c1' = 1. [para(173(a,1),228(a,1,2,1))]. given #668 (F,wt=12): 4733 ((c1 v x) ^ (y v c2)) v c1' = 1. [para(176(a,1),228(a,1,2,1))]. given #669 (T,wt=12): 4812 x v (y v ((y ^ z) v x)') = 1. [para(266(a,1),17(a,1)),flip(a)]. given #670 (T,wt=12): 4815 x v ((x ^ y) v (x ^ z))' = 1. [para(266(a,1),24(a,1)),flip(a)]. given #671 (A,wt=20): 303 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),36(b,1))]. given #672 (F,wt=12): 4827 x v ((x ^ y) v (z ^ x))' = 1. [para(266(a,1),102(a,1)),flip(a)]. given #673 (F,wt=12): 4830 c2 v ((c2 ^ x) v (y ^ c1))' = 1. [para(266(a,1),250(a,1)),flip(a)]. given #674 (T,wt=12): 4832 c2 v ((c2 ^ x) v (c1 ^ y))' = 1. [para(266(a,1),257(a,1)),flip(a)]. given #675 (T,wt=12): 4888 x ^ (y ^ ((y v z) ^ x)') = 0. [para(281(a,1),138(a,1,2)),rewrite(93(2)),flip(a)]. given #676 (A,wt=14): 304 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),36(a,1)),rewrite(4(4),62(4)),flip(a)]. given #677 (F,wt=12): 4890 c1 ^ (x ^ (c2 ^ (x v y))') = 0. [para(287(a,1),138(a,1,2)),rewrite(93(2)),flip(a)]. given #678 (F,wt=12): 4922 x ^ ((x v y) ^ (x v z))' = 0. [para(286(a,1),22(a,1)),flip(a)]. given #679 (T,wt=12): 4937 x ^ ((x v y) ^ (z v x))' = 0. [para(286(a,1),97(a,1)),flip(a)]. given #680 (T,wt=12): 4938 c1 ^ ((c1 v x) ^ (c2 v y))' = 0. [para(286(a,1),178(a,1)),flip(a)]. given #681 (A,wt=20): 306 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(17(a,1),36(a,1))]. given #682 (F,wt=12): 4940 c1 ^ ((c1 v x) ^ (y v c2))' = 0. [para(286(a,1),196(a,1)),flip(a)]. given #683 (F,wt=12): 5002 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),339(a,1,2,1,1))]. low water: id=9162, wt=23 given #684 (T,wt=12): 5011 c1 ^ ((c2 ^ x)' ^ (y ^ x)) = 0. [para(339(a,1),59(a,1,2)),rewrite(4(3),83(3)),flip(a)]. given #685 (T,wt=12): 5500 (c1 v (c2 ^ x)) ^ (y v c2)' = 0. [para(7(a,1),846(a,1,2,1,2)),rewrite(2(4))]. given #686 (A,wt=20): 307 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(19(a,1),36(b,1))]. given #687 (F,wt=12): 5503 (x v c1) ^ (c2 v (y v x))' = 0. [para(17(a,1),846(a,1,2,1))]. given #688 (F,wt=12): 5504 (c1 v (x ^ c2)) ^ (y v c2)' = 0. [para(26(a,1),846(a,1,2,1,2)),rewrite(2(4))]. given #689 (T,wt=12): 5516 (c1 v (x ^ y)) ^ (c2 v x)' = 0. [para(74(a,1),846(a,1,2,1)),rewrite(2(3))]. given #690 (T,wt=12): 5522 (c1 v (x ^ y)) ^ (c2 v y)' = 0. [para(107(a,1),846(a,1,2,1)),rewrite(2(3))]. given #691 (A,wt=14): 308 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(26(a,1),36(a,1)),rewrite(4(4),64(4)),flip(a)]. given #692 (F,wt=12): 6496 (x ^ c2) v (y ^ (c1 ^ x))' = 1. [para(4(a,1),1286(a,1,1))]. given #693 (F,wt=12): 6497 (c2 ^ (c1 v x)) v (y ^ c1)' = 1. [para(6(a,1),1286(a,1,2,1,2))]. given #694 (T,wt=12): 6501 (c2 ^ x) v (c1 ^ (y ^ x))' = 1. [para(19(a,1),1286(a,1,2,1))]. given #695 (T,wt=12): 6502 (c2 ^ (x v c1)) v (y ^ c1)' = 1. [para(20(a,1),1286(a,1,2,1,2))]. given #696 (A,wt=15): 310 x ^ (x' v y) != 0 | (x' v y)' = x. [para(81(a,1),36(a,1)),rewrite(4(6)),xx(a)]. given #697 (F,wt=12): 6522 (c2 ^ (x v y)) v (c1 ^ x)' = 1. [para(85(a,1),1286(a,1,2,1))]. given #698 (F,wt=12): 6527 (c2 ^ (x v y)) v (c1 ^ y)' = 1. [para(101(a,1),1286(a,1,2,1))]. given #699 (T,wt=12): 6640 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(6552(a,1),329(a,1,2)),rewrite(4(8))]. given #700 (T,wt=12): 6683 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(6631(a,1),329(a,1,2)),rewrite(4(8))]. given #701 (A,wt=15): 311 x ^ (y v x') != 0 | (y v x')' = x. [para(91(a,1),36(a,1)),rewrite(4(6)),xx(a)]. given #702 (F,wt=12): 6725 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(6632(a,1),329(a,1,2)),rewrite(4(8))]. given #703 (F,wt=12): 6762 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(6675(a,1),329(a,1,2)),rewrite(4(8))]. given #704 (T,wt=12): 6808 (x ^ c2) v (x ^ (c1 ^ y))' = 1. [para(4(a,1),1288(a,1,2,1)),rewrite(5(5))]. given #705 (T,wt=12): 6812 (c2 ^ (x v y)) v (x ^ c1)' = 1. [para(22(a,1),1288(a,1,2,1)),rewrite(4(3))]. given #706 (A,wt=22): 312 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x. [para(24(a,1),36(a,1)),rewrite(4(6))]. given #707 (F,wt=12): 6819 (c2 ^ (x v y)) v (y ^ c1)' = 1. [para(97(a,1),1288(a,1,2,1)),rewrite(4(3))]. given #708 (F,wt=12): 6982 x v (y v ((z ^ y) v x)') = 1. [para(2542(a,1),1568(a,1,2)),rewrite(2(4))]. given #709 (T,wt=12): 6983 x v (c2 v ((y ^ c1) v x)') = 1. [para(3063(a,1),1568(a,1,2)),rewrite(2(6))]. given #710 (T,wt=12): 6984 x v (c2 v ((c1 ^ y) v x)') = 1. [para(3211(a,1),1568(a,1,2)),rewrite(2(6))]. given #711 (A,wt=26): 313 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x. [para(25(a,1),36(a,1)),rewrite(4(7))]. given #712 (F,wt=12): 7021 x v ((y ^ x) v (x ^ z))' = 1. [para(1574(a,1),102(a,1)),flip(a)]. given #713 (F,wt=12): 7024 c2 v ((x ^ c1) v (c2 ^ y))' = 1. [para(1574(a,1),250(a,1)),flip(a)]. given #714 (T,wt=12): 7026 c2 v ((c1 ^ x) v (c2 ^ y))' = 1. [para(1574(a,1),257(a,1)),flip(a)]. low water: id=9806, wt=22 given #715 (T,wt=12): 7199 x ^ (y ^ ((z v y) ^ x)') = 0. [para(2169(a,1),1779(a,1,2)),rewrite(4(4))]. given #716 (A,wt=13): 314 x ^ (x ^ y)' != 0 | x ^ y = x. [para(184(a,1),36(a,1)),rewrite(4(6),305(11)),xx(a)]. given #717 (F,wt=12): 7200 x ^ (c1 ^ ((c2 v y) ^ x)') = 0. [para(2926(a,1),1779(a,1,2)),rewrite(4(6))]. given #718 (F,wt=12): 7201 x ^ (c1 ^ ((y v c2) ^ x)') = 0. [para(2979(a,1),1779(a,1,2)),rewrite(4(6))]. given #719 (T,wt=12): 7220 x ^ ((c2 ^ x)' ^ (y ^ c1)) = 0. [para(287(a,1),1783(a,1,2,2,2,1)),rewrite(82(7),4(7),71(7),5(7))]. given #720 (T,wt=12): 7221 c1 ^ ((x ^ c2)' ^ (y ^ x)) = 0. [para(346(a,1),1783(a,1,2,2,2,1)),rewrite(82(7),32(7),5(7))]. given #721 (A,wt=13): 315 x ^ (y ^ x)' != 0 | y ^ x = x. [para(217(a,1),36(a,1)),rewrite(4(6),305(11)),xx(a)]. given #722 (F,wt=12): 7224 x ^ ((x ^ c2)' ^ (y ^ c1)) = 0. [para(1786(a,1),1783(a,1,2,2,2,1)),rewrite(82(7),4(7),71(7),5(7))]. given #723 (F,wt=12): 7225 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0. [para(1799(a,1),1783(a,1,2,2,2,1)),rewrite(82(8),4(8),71(8))]. given #724 (T,wt=12): 7226 (c2 ^ (x v c1))' ^ (y ^ c1) = 0. [para(2189(a,1),1783(a,1,2,2,2,1)),rewrite(82(8),4(8),71(8))]. given #725 (T,wt=12): 7261 x ^ ((y v x) ^ (x v z))' = 0. [para(1785(a,1),97(a,1)),flip(a)]. given #726 (A,wt=15): 317 c2 ^ (x v c1') != 0 | (x v c1')' = c2. [para(231(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #727 (F,wt=12): 7263 c1 ^ ((c2 v x) ^ (c1 v y))' = 0. [para(1785(a,1),178(a,1)),flip(a)]. given #728 (F,wt=12): 7265 c1 ^ ((x v c2) ^ (c1 v y))' = 0. [para(1785(a,1),196(a,1)),flip(a)]. given #729 (T,wt=12): 7356 c1 ^ (x ^ (c2 ^ (y v x))') = 0. [para(2169(a,1),1793(a,1,2)),rewrite(4(6))]. given #730 (T,wt=12): 7396 (x v y)' ^ (x v (y ^ z)) = 0. [para(1822(a,1),4(a,1)),flip(a)]. given #731 (A,wt=22): 318 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z))' = x ^ y. [para(27(a,1),36(a,1)),rewrite(4(7),19(7),19(6),5(5),276(6),62(6))]. given #732 (F,wt=12): 7446 c2 v (x v (c1 v (x ^ y))') = 1. [para(1824(a,1),2033(a,1,2,2,1)),rewrite(79(8),2(8),77(8),2(7))]. given #733 (F,wt=12): 7834 c2 v (x v (c1 v (y ^ x))') = 1. [para(107(a,1),1876(a,1,2)),rewrite(2(3),2(7),3(7))]. given #734 (T,wt=12): 7939 (x ^ c2)' ^ (y ^ (c1 ^ x)) = 0. [para(4(a,1),1952(a,1,1,1))]. given #735 (T,wt=12): 8185 (x ^ y)' v (x ^ (y v z)) = 1. [para(1983(a,1),2(a,1)),flip(a)]. given #736 (A,wt=15): 319 c2 ^ (c1' v x) != 0 | (c1' v x)' = c2. [para(232(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #737 (F,wt=12): 8328 c1 ^ (x ^ (y ^ (x ^ c2)')) = 0. [para(19(a,1),2010(a,1,2))]. given #738 (F,wt=12): 8533 (x ^ y)' v ((z v x) ^ y) = 1. [para(2168(a,1),2(a,1)),flip(a)]. given #739 (T,wt=12): 8535 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),2168(a,1,1))]. given #740 (T,wt=12): 8537 ((x v y) ^ (y v z)) v y' = 1. [para(6(a,1),2168(a,1,2,1))]. given #741 (A,wt=14): 320 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2. [para(248(a,1),36(a,1)),rewrite(4(7),60(7))]. given #742 (F,wt=12): 8542 ((x v y) ^ (z v y)) v y' = 1. [para(20(a,1),2168(a,1,2,1))]. low water: id=10195, wt=21 given #743 (F,wt=12): 8547 ((x v c1) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2168(a,1,2,1))]. given #744 (T,wt=12): 8548 ((x v c1) ^ (y v c2)) v c1' = 1. [para(176(a,1),2168(a,1,2,1))]. given #745 (T,wt=12): 8631 x ^ ((y v x) ^ (z v x))' = 0. [para(2170(a,1),97(a,1)),flip(a)]. given #746 (A,wt=14): 321 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2. [para(254(a,1),36(a,1)),rewrite(4(7),19(7),59(7))]. given #747 (F,wt=12): 8635 c1 ^ ((x v c1) ^ (c2 v y))' = 0. [para(2170(a,1),178(a,1)),flip(a)]. given #748 (F,wt=12): 8637 c1 ^ ((x v c1) ^ (y v c2))' = 0. [para(2170(a,1),196(a,1)),flip(a)]. given #749 (T,wt=12): 8677 c1 ^ ((c2 v x) ^ (y v c1))' = 0. [para(2188(a,1),178(a,1)),flip(a)]. given #750 (T,wt=12): 8679 c1 ^ ((x v c2) ^ (y v c1))' = 0. [para(2188(a,1),196(a,1)),flip(a)]. given #751 (A,wt=19): 322 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x. [para(31(a,1),36(a,1)),rewrite(4(7)),xx(a)]. given #752 (F,wt=12): 9056 x v (c2 v ((x v c1) ^ y)') = 1. [para(2313(a,1),17(a,1)),flip(a)]. given #753 (F,wt=12): 9057 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1. [para(2313(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #754 (T,wt=12): 9062 c2 v ((c1 v (x ^ c2)) ^ y)' = 1. [para(2313(a,1),102(a,1)),rewrite(2(6)),flip(a)]. given #755 (T,wt=12): 9233 c2 v (x ^ (c1 v (c2 ^ y)))' = 1. [para(2334(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #756 (A,wt=13): 323 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2. [para(251(a,1),36(a,1)),rewrite(4(8),305(14)),xx(a)]. given #757 (F,wt=12): 9235 c2 v (x ^ (c1 v (y ^ c2)))' = 1. [para(2334(a,1),102(a,1)),rewrite(2(6)),flip(a)]. given #758 (F,wt=12): 9370 c1 ^ (x ^ ((x ^ c2) v y)') = 0. [para(4(a,1),2420(a,1,2,2,1,1))]. given #759 (T,wt=12): 9372 x ^ (c1 ^ ((c2 ^ x) v y)') = 0. [para(2420(a,1),19(a,1)),flip(a)]. given #760 (T,wt=12): 9404 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(26(a,1),214(a,1,1,2,1)),rewrite(26(5))]. given #761 (A,wt=13): 324 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2. [para(268(a,1),36(a,1)),rewrite(4(8),305(14)),xx(a)]. given #762 (F,wt=12): 9406 ((x ^ c1) v (c2 ^ y)) ^ c2' = 0. [para(248(a,1),214(a,1,1,2,1)),rewrite(248(9))]. given #763 (F,wt=12): 9407 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0. [para(254(a,1),214(a,1,1,2,1)),rewrite(254(9))]. given #764 (T,wt=12): 9422 (x v (y ^ z)) ^ (z v x)' = 0. [para(279(a,1),214(a,1,1,2))]. given #765 (T,wt=12): 9427 (x v (y ^ c1)) ^ (c2 v x)' = 0. [para(2926(a,1),214(a,1,1,2))]. given #766 (A,wt=14): 325 x v y != 1 | 0 != x | (x v y)' = x. [para(67(a,1),36(a,1)),rewrite(4(5),6(5)),flip(b)]. given #767 (F,wt=12): 9508 c1 ^ (x ^ (y v (x ^ c2))') = 0. [para(4(a,1),2444(a,1,2,2,1,2))]. given #768 (F,wt=12): 9610 (x ^ y)' v (x ^ (z v y)) = 1. [para(2468(a,1),2(a,1)),flip(a)]. given #769 (T,wt=12): 9731 (x v y)' ^ ((z ^ x) v y) = 0. [para(2538(a,1),4(a,1)),flip(a)]. given #770 (T,wt=12): 9736 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(26(a,1),2538(a,1,2,1))]. given #771 (A,wt=14): 326 x v y != 1 | 0 != y | (x v y)' = y. [para(69(a,1),36(a,1)),rewrite(4(5),20(5)),flip(b)]. given #772 (F,wt=12): 9741 (c1 v x) ^ (c2 v (y v x))' = 0. [para(173(a,1),2538(a,1,1,1)),rewrite(3(5))]. given #773 (F,wt=12): 9743 ((x ^ c2) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),2538(a,1,2,1))]. given #774 (T,wt=12): 9744 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),2538(a,1,2,1))]. given #775 (T,wt=12): 9823 x v ((y ^ x) v (z ^ x))' = 1. [para(2541(a,1),102(a,1)),flip(a)]. given #776 (A,wt=18): 327 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(86(a,1),36(a,1)),rewrite(4(5),276(5)),flip(a)]. given #777 (F,wt=12): 9829 c2 v ((x ^ c2) v (y ^ c1))' = 1. [para(2541(a,1),250(a,1)),flip(a)]. given #778 (F,wt=12): 9831 c2 v ((x ^ c2) v (c1 ^ y))' = 1. [para(2541(a,1),257(a,1)),flip(a)]. low water: id=10565, wt=20 given #779 (T,wt=12): 9875 c2 v ((x ^ c1) v (y ^ c2))' = 1. [para(2566(a,1),250(a,1)),flip(a)]. given #780 (T,wt=12): 9878 c2 v ((c1 ^ x) v (y ^ c2))' = 1. [para(2566(a,1),257(a,1)),flip(a)]. given #781 (A,wt=13): 332 x' ^ (y v x) != 0 | y v x = x. [para(328(a,1),10(a,1)),rewrite(305(10)),flip(c),xx(a)]. given #782 (F,wt=12): 9907 ((c2 v x) ^ (c1 v y)) v c1' = 1. [para(173(a,1),229(a,1,1,2,1)),rewrite(173(9))]. given #783 (F,wt=12): 9908 ((x v c2) ^ (c1 v y)) v c1' = 1. [para(176(a,1),229(a,1,1,2,1)),rewrite(176(9))]. given #784 (T,wt=12): 9930 (x ^ (y v c2)) v (c1 ^ x)' = 1. [para(3211(a,1),229(a,1,1,2))]. given #785 (T,wt=12): 10096 (x ^ c2) v (c1 ^ (y ^ x))' = 1. [para(238(a,1),2328(a,1,2)),rewrite(2(7))]. given #786 (A,wt=14): 334 x v (y v (y v ((x v y) ^ z))') = 1. [para(25(a,1),328(a,1,2)),rewrite(2(6),3(6))]. given #787 (F,wt=12): 10162 c1' v ((c2 v x) ^ (c1 v y)) = 1. [para(139(a,1),2703(a,1,2))]. given #788 (F,wt=12): 10221 c1' v ((c2 v x) ^ (y v c1)) = 1. [para(139(a,1),2732(a,1,2))]. given #789 (T,wt=12): 10265 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(188(a,1),2756(a,1,2))]. given #790 (T,wt=12): 10311 (x v y)' ^ (x v (z ^ y)) = 0. [para(2773(a,1),4(a,1)),flip(a)]. given #791 (A,wt=15): 335 (x v y) ^ y' != 0 | (x v y)' = y'. [para(328(a,1),36(a,1)),xx(a)]. given #792 (F,wt=12): 10419 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(188(a,1),2809(a,1,2))]. given #793 (F,wt=12): 10473 (c1 v (x ^ y)) ^ (x v c2)' = 0. [para(24(a,1),2839(a,1,2,1)),rewrite(2(3))]. given #794 (T,wt=12): 10474 (c1 v (x ^ y)) ^ (y v c2)' = 0. [para(102(a,1),2839(a,1,2,1)),rewrite(2(3))]. given #795 (T,wt=12): 10535 (c1 ^ x)' v ((c2 v y) ^ x) = 1. [para(2925(a,1),2(a,1)),flip(a)]. given #796 (A,wt=13): 338 x' v (y ^ x) != 1 | y ^ x = x. [para(329(a,1),10(b,1)),rewrite(305(10)),flip(c),xx(b)]. given #797 (F,wt=12): 10536 (x ^ (c2 v y)) v (c1 ^ x)' = 1. [para(4(a,1),2925(a,1,1))]. given #798 (F,wt=12): 10540 ((c2 v x) ^ (y v c1)) v c1' = 1. [para(20(a,1),2925(a,1,2,1))]. given #799 (T,wt=12): 10542 ((c2 v x) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2925(a,1,2,1))]. given #800 (T,wt=12): 10543 ((c2 v x) ^ (y v c2)) v c1' = 1. [para(176(a,1),2925(a,1,2,1))]. given #801 (A,wt=14): 340 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(23(a,1),329(a,1,2)),rewrite(4(6),5(6))]. given #802 (F,wt=12): 10574 c1 ^ ((c2 v x) ^ (c2 v y))' = 0. [para(2927(a,1),178(a,1)),flip(a)]. given #803 (F,wt=12): 10575 c1 ^ ((c2 v x) ^ (y v c2))' = 0. [para(2927(a,1),196(a,1)),flip(a)]. given #804 (T,wt=12): 10581 c1 ^ ((x v c2) ^ (c2 v y))' = 0. [para(2940(a,1),196(a,1)),flip(a)]. given #805 (T,wt=12): 10590 (x ^ c1)' v (x ^ (c2 v y)) = 1. [para(2953(a,1),2(a,1)),flip(a)]. given #806 (A,wt=13): 341 (x ^ y) v y' != 1 | x ^ y = y. [para(329(a,1),36(b,1)),rewrite(305(10)),flip(c),xx(b)]. given #807 (F,wt=12): 10606 (c1 ^ x)' v ((y v c2) ^ x) = 1. [para(2978(a,1),2(a,1)),flip(a)]. given #808 (F,wt=12): 10610 ((x v c2) ^ (y v c1)) v c1' = 1. [para(20(a,1),2978(a,1,2,1))]. given #809 (T,wt=12): 10612 ((x v c2) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2978(a,1,2,1))]. given #810 (T,wt=12): 10613 ((x v c2) ^ (y v c2)) v c1' = 1. [para(176(a,1),2978(a,1,2,1))]. given #811 (A,wt=13): 342 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(5(a,1),89(a,1,2)),rewrite(4(8))]. given #812 (F,wt=12): 10641 c1 ^ ((x v c2) ^ (y v c2))' = 0. [para(2980(a,1),196(a,1)),flip(a)]. given #813 (F,wt=12): 10684 (x ^ c1)' v (x ^ (y v c2)) = 1. [para(3007(a,1),2(a,1)),flip(a)]. given #814 (T,wt=12): 10740 (c2 v x)' ^ ((y ^ c1) v x) = 0. [para(3060(a,1),4(a,1)),flip(a)]. given #815 (T,wt=12): 10744 ((x ^ c1) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),3060(a,1,2,1))]. given #816 (A,wt=18): 343 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1' = x ^ c2. [para(89(a,1),10(b,1))]. given #817 (F,wt=12): 10746 ((x ^ c1) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3060(a,1,2,1))]. given #818 (F,wt=12): 10747 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),3060(a,1,2,1))]. given #819 (T,wt=12): 10779 c2 v ((x ^ c1) v (y ^ c1))' = 1. [para(3062(a,1),250(a,1)),flip(a)]. given #820 (T,wt=12): 10780 c2 v ((x ^ c1) v (c1 ^ y))' = 1. [para(3062(a,1),257(a,1)),flip(a)]. given #821 (A,wt=20): 347 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x)' = y. [para(2(a,1),37(a,1)),rewrite(3(2))]. given #822 (F,wt=12): 10786 c2 v ((c1 ^ x) v (y ^ c1))' = 1. [para(3078(a,1),257(a,1)),flip(a)]. given #823 (F,wt=12): 10815 (c2 ^ x) v (x ^ (y ^ c1))' = 1. [para(4(a,1),3113(a,1,2,1,2))]. given #824 (T,wt=12): 10840 (x v c2)' ^ (x v (y ^ c1)) = 0. [para(3119(a,1),4(a,1)),flip(a)]. given #825 (T,wt=12): 10973 (x v (c1 ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),3208(a,1,1))]. given #826 (A,wt=20): 348 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z. [para(2(a,1),37(b,1,1))]. given #827 (F,wt=12): 10974 (c2 v x)' ^ ((c1 ^ y) v x) = 0. [para(3208(a,1),4(a,1)),flip(a)]. given #828 (F,wt=12): 10977 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),3208(a,1,2,1))]. given #829 (T,wt=12): 10979 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3208(a,1,2,1))]. given #830 (T,wt=12): 10980 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),3208(a,1,2,1))]. given #831 (A,wt=26): 349 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z))' = u. [para(3(a,1),37(a,1,2))]. given #832 (F,wt=12): 11003 c2 v ((c1 ^ x) v (c1 ^ y))' = 1. [para(3210(a,1),257(a,1)),flip(a)]. given #833 (F,wt=12): 11016 (x v c2)' ^ (x v (c1 ^ y)) = 0. [para(3241(a,1),4(a,1)),flip(a)]. given #834 (T,wt=12): 11109 (x ^ c2) v (c1 ^ (x ^ y))' = 1. [para(247(a,1),3316(a,1,2,1))]. given #835 (T,wt=12): 11152 (c1 v x) ^ (x v (y v c2))' = 0. [para(112(a,1),3377(a,1,2,1,2))]. given #836 (A,wt=20): 350 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z. [para(4(a,1),37(b,1))]. given #837 (F,wt=12): 11188 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0. [para(24(a,1),3461(a,1,2,1))]. given #838 (F,wt=12): 11189 (c1 v (x ^ c2)) ^ (c2 v y)' = 0. [para(102(a,1),3461(a,1,2,1))]. given #839 (T,wt=12): 11203 x v (c2 v ((c1 v x) ^ y)') = 1. [para(4(a,1),3737(a,1,2,2,1))]. given #840 (T,wt=12): 11299 (c2 ^ (c1 v x)) v (c1 ^ y)' = 1. [para(22(a,1),4226(a,1,2,1))]. given #841 (A,wt=18): 351 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),37(a,1,2)),rewrite(19(6),97(6))]. given #842 (F,wt=12): 11300 (c2 ^ (x v c1)) v (c1 ^ y)' = 1. [para(97(a,1),4226(a,1,2,1))]. given #843 (F,wt=12): 11330 (x v y)' ^ ((y ^ z) v x) = 0. [para(4273(a,1),4(a,1)),flip(a)]. given #844 (T,wt=12): 11353 (x v y)' ^ ((z ^ y) v x) = 0. [para(4276(a,1),4(a,1)),flip(a)]. given #845 (T,wt=12): 11397 (x v c2)' ^ ((y ^ c1) v x) = 0. [para(4280(a,1),4(a,1)),flip(a)]. given #846 (A,wt=18): 352 x v y != 1 | x v y != 0 | (x v y)' = x v y. [para(28(a,1),37(b,1)),rewrite(69(2),67(2))]. given #847 (F,wt=12): 11464 (x v c2)' ^ ((c1 ^ y) v x) = 0. [para(4282(a,1),4(a,1)),flip(a)]. given #848 (F,wt=12): 11498 (x v y)' ^ (y v (x ^ z)) = 0. [para(4434(a,1),4(a,1)),flip(a)]. given #849 (T,wt=12): 11533 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),4436(a,1,1,1))]. given #850 (T,wt=12): 11537 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(26(a,1),4436(a,1,1,1))]. given #851 (A,wt=26): 354 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z)' = y v u. [para(17(a,1),37(a,1,2))]. given #852 (F,wt=12): 11541 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(248(a,1),4436(a,1,1,1))]. given #853 (F,wt=12): 11542 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(254(a,1),4436(a,1,1,1))]. given #854 (T,wt=12): 11728 (x ^ y)' v ((y v z) ^ x) = 1. [para(4586(a,1),2(a,1)),flip(a)]. given #855 (T,wt=12): 11752 (x ^ y)' v ((z v y) ^ x) = 1. [para(4590(a,1),2(a,1)),flip(a)]. given #856 (A,wt=20): 355 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(17(a,1),37(a,1))]. given #857 (F,wt=12): 11784 (x ^ c1)' v ((c2 v y) ^ x) = 1. [para(4592(a,1),2(a,1)),flip(a)]. given #858 (F,wt=12): 11797 (x ^ c1)' v ((y v c2) ^ x) = 1. [para(4594(a,1),2(a,1)),flip(a)]. given #859 (T,wt=12): 11810 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),4722(a,1,2))]. given #860 (T,wt=12): 11812 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),4722(a,1,1,1))]. given #861 (A,wt=26): 356 x v (y v (z v u)) != 1 | (y v (x v z)) ^ u != 0 | (x v (y v z))' = u. [para(17(a,1),37(b,1,1)),rewrite(3(2))]. given #862 (F,wt=12): 11816 x' v ((x v y) ^ (z v x)) = 1. [para(20(a,1),4722(a,1,1,1))]. given #863 (F,wt=12): 11819 c1' v ((c1 v x) ^ (c2 v y)) = 1. [para(173(a,1),4722(a,1,1,1))]. given #864 (T,wt=12): 11820 c1' v ((c1 v x) ^ (y v c2)) = 1. [para(176(a,1),4722(a,1,1,1))]. given #865 (T,wt=12): 12175 (x v c2)' ^ (c1 v (c2 ^ y)) = 0. [para(5500(a,1),4(a,1)),flip(a)]. given #866 (A,wt=26): 358 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y)' = z ^ u. [para(19(a,1),37(b,1))]. given #867 (F,wt=12): 12214 (x v c2)' ^ (c1 v (y ^ c2)) = 0. [para(5504(a,1),4(a,1)),flip(a)]. given #868 (F,wt=12): 12226 (c2 v x)' ^ (c1 v (x ^ y)) = 0. [para(5516(a,1),4(a,1)),flip(a)]. given #869 (T,wt=12): 12250 (c2 v x)' ^ (c1 v (y ^ x)) = 0. [para(5522(a,1),4(a,1)),flip(a)]. given #870 (T,wt=12): 12284 (x ^ c1)' v (c2 ^ (c1 v y)) = 1. [para(6497(a,1),2(a,1)),flip(a)]. given #871 (A,wt=22): 359 x v (y v z) != 1 | y v z != 0 | (y v z)' = x v (y v z). [para(20(a,1),37(b,1)),rewrite(290(3),288(3))]. given #872 (F,wt=12): 12310 (x ^ c1)' v (c2 ^ (y v c1)) = 1. [para(6502(a,1),2(a,1)),flip(a)]. given #873 (F,wt=12): 12321 (c1 ^ x)' v (c2 ^ (x v y)) = 1. [para(6522(a,1),2(a,1)),flip(a)]. given #874 (T,wt=12): 12343 (c1 ^ x)' v (c2 ^ (y v x)) = 1. [para(6527(a,1),2(a,1)),flip(a)]. given #875 (T,wt=12): 12402 (x ^ c1)' v (c2 ^ (x v y)) = 1. [para(6812(a,1),2(a,1)),flip(a)]. given #876 (A,wt=18): 361 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(106(a,1),37(a,1,2)),rewrite(4(8))]. given #877 (F,wt=12): 12415 (x ^ c1)' v (c2 ^ (y v x)) = 1. [para(6819(a,1),2(a,1)),flip(a)]. given #878 (F,wt=12): 12676 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),8533(a,1,2))]. given #879 (T,wt=12): 12677 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),8533(a,1,1,1))]. given #880 (T,wt=12): 12681 x' v ((y v x) ^ (z v x)) = 1. [para(20(a,1),8533(a,1,1,1))]. given #881 (A,wt=19): 362 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z. [para(81(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #882 (F,wt=12): 12684 c1' v ((x v c1) ^ (c2 v y)) = 1. [para(173(a,1),8533(a,1,1,1))]. given #883 (F,wt=12): 12685 c1' v ((x v c1) ^ (y v c2)) = 1. [para(176(a,1),8533(a,1,1,1))]. given #884 (T,wt=12): 12892 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(9404(a,1),4(a,1)),flip(a)]. given #885 (T,wt=12): 12908 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(9406(a,1),4(a,1)),flip(a)]. given #886 (A,wt=23): 363 x v (y v ((x v y)' ^ z)) != 1 | (x v y)' ^ z = (x v y)'. [para(84(a,1),37(b,1)),flip(c),xx(b)]. given #887 (F,wt=12): 12930 (x v y)' ^ (y v (z ^ x)) = 0. [para(9422(a,1),4(a,1)),flip(a)]. given #888 (F,wt=12): 12980 (c2 v x)' ^ (x v (y ^ c1)) = 0. [para(9427(a,1),4(a,1)),flip(a)]. given #889 (T,wt=12): 13030 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(26(a,1),9731(a,1,1,1))]. given #890 (T,wt=12): 13032 c2' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(248(a,1),9731(a,1,1,1))]. given #891 (A,wt=19): 364 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'. [para(91(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #892 (F,wt=12): 13033 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(254(a,1),9731(a,1,1,1))]. given #893 (F,wt=12): 13126 c1' v ((x v c2) ^ (c1 v y)) = 1. [para(9908(a,1),2(a,1)),flip(a)]. given #894 (T,wt=12): 13134 (c1 ^ x)' v (x ^ (y v c2)) = 1. [para(9930(a,1),2(a,1)),flip(a)]. given #895 (T,wt=12): 13175 c1' v ((c2 v x) ^ (c2 v y)) = 1. [para(110(a,1),10162(a,1,2,2))]. given #896 (A,wt=15): 365 (x v y) ^ x' != 0 | (x v y)' = x'. [para(91(a,1),37(a,1)),xx(a)]. given #897 (F,wt=12): 13176 c1' v ((c2 v x) ^ (y v c2)) = 1. [para(112(a,1),10162(a,1,2,2))]. given #898 (F,wt=12): 13184 c1' v ((x v c2) ^ (y v c1)) = 1. [para(2(a,1),10221(a,1,2,1))]. given #899 (T,wt=12): 13190 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(60(a,1),10265(a,1,2,2))]. given #900 (T,wt=12): 13224 c2' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(4(a,1),10419(a,1,2,1))]. given #901 (A,wt=32): 366 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(22(a,1),37(b,1)),rewrite(3(2),3(15))]. given #902 (F,wt=12): 13235 (x v c2)' ^ (c1 v (x ^ y)) = 0. [para(10473(a,1),4(a,1)),flip(a)]. given #903 (F,wt=12): 13245 (x v c2)' ^ (c1 v (y ^ x)) = 0. [para(10474(a,1),4(a,1)),flip(a)]. given #904 (T,wt=12): 13247 (c1 ^ x)' v (x ^ (c2 v y)) = 1. [para(4(a,1),10535(a,1,2))]. given #905 (T,wt=12): 13338 c1' v ((x v c2) ^ (c2 v y)) = 1. [para(173(a,1),10606(a,1,1,1))]. given #906 (A,wt=23): 367 x v (y v (z ^ (x v y)')) != 1 | z ^ (x v y)' = (x v y)'. [para(94(a,1),37(b,1)),flip(c),xx(b)]. given #907 (F,wt=12): 13339 c1' v ((x v c2) ^ (y v c2)) = 1. [para(176(a,1),10606(a,1,1,1))]. given #908 (F,wt=12): 13377 c2' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(248(a,1),10740(a,1,1,1))]. given #909 (T,wt=12): 13378 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(254(a,1),10740(a,1,1,1))]. given #910 (T,wt=12): 13411 (c2 v x)' ^ (x v (c1 ^ y)) = 0. [para(10973(a,1),4(a,1)),flip(a)]. given #911 (A,wt=23): 368 x v (y v (x v (y v z))') != 1 | (x v (y v z))' = (x v y)'. [para(135(a,1),37(b,1)),rewrite(3(2),3(14)),flip(c),xx(b)]. given #912 (F,wt=12): 13415 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(254(a,1),10974(a,1,1,1))]. given #913 (F,wt=12): 13440 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0. [para(11188(a,1),4(a,1)),flip(a)]. given #914 (T,wt=12): 13449 (c2 v x)' ^ (c1 v (y ^ c2)) = 0. [para(11189(a,1),4(a,1)),flip(a)]. given #915 (T,wt=12): 13461 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1. [para(11299(a,1),2(a,1)),flip(a)]. given #916 (A,wt=36): 369 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(23(a,1),37(b,1))]. given #917 (F,wt=12): 13471 (c1 ^ x)' v (c2 ^ (y v c1)) = 1. [para(11300(a,1),2(a,1)),flip(a)]. given #918 (F,wt=13): 395 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(96(a,1),5(a,1,1)),flip(a)]. given #919 (T,wt=13): 399 x ^ (y ^ (z v (u v x))) = y ^ x. [para(96(a,1),19(a,1,2)),flip(a)]. given #920 (T,wt=13): 404 x v ((y ^ (z ^ x)) v u) = x v u. [para(104(a,1),3(a,1,1)),flip(a)]. given #921 (A,wt=23): 370 x v (y v (z v (x v y))') != 1 | (z v (x v y))' = (x v y)'. [para(145(a,1),37(b,1)),flip(c),xx(b)]. given #922 (F,wt=13): 408 x v (y v (z ^ (u ^ x))) = y v x. [para(104(a,1),17(a,1,2)),flip(a)]. given #923 (F,wt=13): 413 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x. [para(59(a,1),104(a,1,2,2))]. given #924 (T,wt=13): 415 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2. [para(89(a,1),104(a,1,2,2))]. given #925 (T,wt=13): 418 c1 v (x v (c2 v y)) = x v (c2 v y). [para(110(a,1),17(a,1,2)),flip(a)]. given #926 (A,wt=28): 371 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y)' = (y ^ u) v z. [para(24(a,1),37(a,1,2))]. given #927 (F,wt=13): 419 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(110(a,1),21(a,1,2,2))]. given #928 (F,wt=13): 423 c2 v (x v (y v c1)) = c2 v (x v y). [para(3(a,1),111(a,1,2)),rewrite(2(8))]. given #929 (T,wt=13): 434 (x v c1) ^ (y v (x v c2)) = x v c1. [para(111(a,1),96(a,1,2,2))]. given #930 (T,wt=13): 442 x v (x v y)' != 1 | x v y = x. [para(135(a,1),38(b,1)),rewrite(2(3),305(11)),xx(b)]. given #931 (A,wt=32): 372 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(25(a,1),37(a,1,2))]. given #932 (F,wt=11): 13598 c1' v (c1' v c2')' != 1. [ur(442,b,15,a)]. given #933 (F,wt=12): 13600 (c1' v (c1' v c2')')' != 0. [ur(4180,b,13598,a),rewrite(2(9))]. given #934 (T,wt=13): 445 x v (y v x)' != 1 | y v x = x. [para(145(a,1),38(b,1)),rewrite(2(3),305(11)),xx(b)]. given #935 (T,wt=13): 450 c1 v (c2 v x)' != 1 | c2 v x = c1. [para(179(a,1),38(b,1)),rewrite(2(5),305(14)),xx(b)]. given #936 (A,wt=22): 373 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(25(a,1),37(a,1)),rewrite(62(7))]. given #937 (F,wt=13): 451 c1 v (x v c2)' != 1 | x v c2 = c1. [para(181(a,1),38(b,1)),rewrite(2(5),305(14)),xx(b)]. given #938 (F,wt=13): 454 (x v y) ^ y' != 0 | x v y = y. [para(328(a,1),38(a,1)),rewrite(305(10)),flip(c),xx(a)]. given #939 (T,wt=13): 459 c1 v (x v (y v c2)) = x v (y v c2). [para(112(a,1),17(a,1,2)),flip(a)]. given #940 (T,wt=13): 460 (x v c1) ^ (x v (y v c2)) = x v c1. [para(112(a,1),21(a,1,2,2))]. given #941 (A,wt=19): 374 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(184(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #942 (F,wt=13): 465 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z. [para(193(a,1),5(a,1,1)),flip(a)]. given #943 (F,wt=13): 467 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1. [para(193(a,1),19(a,1,2)),flip(a)]. given #944 (T,wt=13): 470 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z. [para(195(a,1),5(a,1,1)),flip(a)]. given #945 (T,wt=13): 472 c1 ^ (x ^ (y v (z v c2))) = x ^ c1. [para(195(a,1),19(a,1,2)),flip(a)]. given #946 (A,wt=19): 375 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(217(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #947 (F,wt=13): 474 c2 v ((x ^ (y ^ c1)) v z) = c2 v z. [para(255(a,1),3(a,1,1)),flip(a)]. given #948 (F,wt=13): 477 c2 v (x v (y ^ (z ^ c1))) = x v c2. [para(255(a,1),17(a,1,2)),flip(a)]. given #949 (T,wt=13): 534 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z. [para(260(a,1),3(a,1,1)),flip(a)]. given #950 (T,wt=13): 537 c2 v (x v (y ^ (c1 ^ z))) = x v c2. [para(260(a,1),17(a,1,2)),flip(a)]. given #951 (A,wt=15): 376 (x v c2) ^ c1' != 0 | (x v c2)' = c1'. [para(225(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #952 (F,wt=13): 540 c2 v (x v (c1 v y)) = c2 v (x v y). [para(422(a,1),3(a,1,1)),rewrite(3(3),3(7)),flip(a)]. given #953 (F,wt=13): 547 (x v c1) ^ (y v (c2 v x)) = x v c1. [para(422(a,1),96(a,1,2,2))]. given #954 (T,wt=13): 1851 c1' ^ (x v c2) != 0 | x v c2 = c1. [para(1840(a,1),10(a,1)),rewrite(305(13)),flip(c),xx(a)]. given #955 (T,wt=13): 1853 (x v c2) ^ c1' != 0 | x v c2 = c1. [para(1840(a,1),38(a,1)),rewrite(305(13)),flip(c),xx(a)]. given #956 (A,wt=19): 377 (x v c2) ^ (y v c1') != 0 | (x v c2)' = y v c1'. [para(231(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #957 (F,wt=13): 1887 x' ^ (x v y) != 0 | x v y = x. [para(81(a,1),76(a,1)),rewrite(305(10)),flip(c),xx(a)]. given #958 (F,wt=13): 1892 c1' ^ (c2 v x) != 0 | c2 v x = c1. [para(232(a,1),76(a,1)),rewrite(305(13)),flip(c),xx(a)]. given #959 (T,wt=13): 1973 c2' v (x ^ c1) != 1 | x ^ c1 = c2. [para(1946(a,1),10(b,1)),rewrite(305(13)),flip(c),xx(b)]. given #960 (T,wt=13): 1974 (x ^ c1) v c2' != 1 | x ^ c1 = c2. [para(1946(a,1),36(b,1)),rewrite(305(13)),flip(c),xx(b)]. given #961 (A,wt=15): 378 (c2 v x) ^ c1' != 0 | (c2 v x)' = c1'. [para(231(a,1),37(a,1)),xx(a)]. given #962 (F,wt=13): 2058 x' v (x ^ y) != 1 | x ^ y = x. [para(84(a,1),88(b,1)),rewrite(305(10)),flip(c),xx(b)]. given #963 (F,wt=13): 2062 c2' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(151(a,1),88(b,1)),rewrite(305(13)),flip(c),xx(b)]. given #964 (T,wt=13): 2229 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(4(a,1),98(a,1,2,2,2))]. given #965 (T,wt=13): 2236 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x. [para(98(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #966 (A,wt=19): 380 (x v c2) ^ (c1' v y) != 0 | (x v c2)' = c1' v y. [para(232(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #967 (F,wt=13): 2360 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),100(a,1,2)),rewrite(3(3))]. given #968 (F,wt=13): 2635 x v (y v (z ^ (y v x))) = x v y. [para(2(a,1),103(a,1,2,2,2))]. given #969 (T,wt=13): 2827 x v (c2 v (y ^ (x v c1))) = x v c2. [para(122(a,1),104(a,1,2,2)),rewrite(3(6))]. given #970 (T,wt=13): 2843 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),177(a,1,1))]. given #971 (A,wt=18): 382 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y. [para(254(a,1),37(a,1,2)),rewrite(19(9),196(9))]. given #972 (F,wt=11): 13677 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(2843(a,1),44(a,2,2)),rewrite(67(8),3847(7),67(6),101(10))]. given #973 (F,wt=11): 13678 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(2843(a,1),53(a,1,2)),rewrite(101(5)),flip(a)]. given #974 (T,wt=11): 13701 x v (c2 ^ (c1 v x)) = x v c1. [para(2843(a,1),2635(a,1,2))]. given #975 (T,wt=11): 13708 x v (c2 ^ (x v c1)) = x v c1. [para(2(a,1),13701(a,1,2,2))]. given #976 (A,wt=23): 383 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'. [para(31(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #977 (F,wt=13): 2848 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(20(a,1),177(a,1,1))]. low water: id=10960, wt=19 given #978 (F,wt=13): 2876 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),108(a,1,2)),rewrite(5(3))]. given #979 (T,wt=13): 3030 (x v (y v z)) ^ (y v x) = x v y. [para(113(a,1),4(a,1)),flip(a)]. given #980 (T,wt=13): 3038 (c1 v x) ^ (x v (c2 v y)) = x v c1. [para(110(a,1),113(a,1,2,2))]. given #981 (A,wt=19): 384 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'. [para(251(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #982 (F,wt=13): 3040 (c1 v x) ^ (x v (y v c2)) = x v c1. [para(112(a,1),113(a,1,2,2))]. given #983 (F,wt=13): 3098 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1. [para(253(a,1),96(a,1,2,2)),rewrite(5(6))]. given #984 (T,wt=13): 3147 (x v (y v z)) ^ (z v x) = z v x. [para(114(a,1),4(a,1)),flip(a)]. given #985 (T,wt=13): 3267 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),279(a,1,1))]. given #986 (A,wt=19): 385 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'. [para(268(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #987 (F,wt=13): 3273 x ^ (c1 ^ ((x ^ c2) v y)) = x ^ c1. [para(89(a,1),279(a,1,2)),rewrite(4(6),5(6),89(10))]. given #988 (F,wt=13): 3295 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(280(a,1),24(a,2)),rewrite(5(3),3290(6))]. given #989 (T,wt=13): 3393 (x ^ (y ^ z)) v (u v y) = u v y. [para(19(a,1),292(a,1,1))]. given #990 (T,wt=13): 3399 c2 v (x v ((x v c1) ^ y)) = c2 v x. [para(422(a,1),292(a,1,2)),rewrite(17(6),2(5),422(10))]. given #991 (A,wt=22): 386 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y). [para(64(a,1),37(b,1)),rewrite(103(4))]. given #992 (F,wt=11): 13772 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(7(a,1),3399(a,2)),rewrite(2(7),24(10))]. given #993 (F,wt=11): 13773 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(26(a,1),3399(a,2)),rewrite(2(7),102(10))]. given #994 (T,wt=11): 13782 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(4(a,1),13772(a,1,2))]. given #995 (T,wt=11): 13790 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),13773(a,1,2))]. given #996 (A,wt=27): 387 x v (y v (z ^ ((x v y) ^ z)')) != 1 | z ^ ((x v y) ^ z)' = (x v y)'. [para(34(a,1),37(b,1)),flip(c),xx(b)]. given #997 (F,wt=13): 3411 (x ^ (c1 ^ y)) v (c2 ^ x) = c2 ^ x. [para(253(a,1),292(a,1,2)),rewrite(5(3),253(11))]. given #998 (F,wt=13): 3469 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),294(a,1,2,2))]. given #999 (T,wt=13): 3486 c1 ^ (x v (y v (z v (c2 v u)))) = c1. [para(294(a,1),196(a,1,2)),rewrite(176(4),3(5)),flip(a)]. given #1000 (T,wt=13): 3491 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(5(a,1),298(a,1,2,2))]. given #1001 (A,wt=24): 388 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z. [para(67(a,1),37(a,1,2))]. given #1002 (F,wt=13): 3508 c2 v (x ^ (y ^ (z ^ (c1 ^ u)))) = c2. [para(298(a,1),250(a,1,2)),rewrite(248(4),5(5)),flip(a)]. given #1003 (F,wt=13): 3517 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1. [para(344(a,1),73(a,1,2,2)),rewrite(5(6))]. given #1004 (T,wt=13): 3606 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),394(a,1,2,2,2))]. given #1005 (T,wt=13): 3634 c1 ^ (x v (y v (z v (u v c2)))) = c1. [para(394(a,1),196(a,1,2)),rewrite(176(4)),flip(a)]. given #1006 (A,wt=24): 389 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z. [para(69(a,1),37(a,1,2))]. given #1007 (F,wt=13): 3646 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),406(a,1,2,2,2))]. given #1008 (F,wt=13): 3685 c2 v (x ^ (y ^ (z ^ (u ^ c1)))) = c2. [para(406(a,1),250(a,1,2)),rewrite(248(4)),flip(a)]. given #1009 (T,wt=13): 3701 (c1 v x) ^ (c2 v (x v y)) = c1 v x. [para(110(a,1),119(a,1,2))]. given #1010 (T,wt=13): 3731 x v (c2 v (y ^ (c1 v x))) = x v c2. [para(461(a,1),104(a,1,2,2)),rewrite(3(6))]. given #1011 (A,wt=14): 390 x v y != 1 | 0 != y | (y v x)' = y. [para(69(a,1),37(a,1)),rewrite(4(5),6(5)),flip(b)]. given #1012 (F,wt=13): 3746 (x v (c2 v y)) ^ (c1 v x) = c1 v x. [para(461(a,1),279(a,1,2)),rewrite(3(3),461(11))]. given #1013 (F,wt=13): 3845 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(7(a,1),542(a,1,2)),rewrite(2(4),4(6),2(10))]. given #1014 (T,wt=13): 3847 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(26(a,1),542(a,1,2)),rewrite(2(4),4(6),2(10))]. given #1015 (T,wt=13): 3851 c2 v (x v (y ^ (x v c1))) = c2 v x. [para(542(a,1),104(a,1,2,2)),rewrite(3(6))]. given #1016 (A,wt=19): 393 (x v y') ^ (z v y) != 0 | (x v y')' = z v y. [para(328(a,1),37(a,1,2)),rewrite(90(2)),xx(a)]. given #1017 (F,wt=13): 3866 (c2 v (x v y)) ^ (x v c1) = x v c1. [para(542(a,1),279(a,1,2)),rewrite(3(3),542(11))]. given #1018 (F,wt=13): 3882 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),2169(a,1,1))]. given #1019 (T,wt=13): 3915 (x v (y v z)) ^ (z v y) = z v y. [para(291(a,1),2169(a,1,2)),rewrite(291(7))]. given #1020 (T,wt=13): 3919 (x v (y v c2)) ^ (c1 v y) = c1 v y. [para(461(a,1),2169(a,1,2)),rewrite(461(11))]. given #1021 (A,wt=15): 396 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(96(a,1),5(a,1)),flip(a)]. given #1022 (F,wt=13): 3922 (x v (c2 v y)) ^ (y v c1) = y v c1. [para(542(a,1),2169(a,1,2)),rewrite(542(11))]. given #1023 (F,wt=13): 3933 c2 v (x v (y ^ (c1 v x))) = c2 v x. [para(2376(a,1),104(a,1,2,2)),rewrite(3(6))]. given #1024 (T,wt=13): 3946 (c1 v x) ^ (y v (c2 v x)) = c1 v x. [para(2376(a,1),2169(a,1,2)),rewrite(4(6),2376(11))]. given #1025 (T,wt=13): 3967 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),2542(a,1,1))]. given #1026 (A,wt=18): 397 x v (y v z) != 1 | 0 != z | z' = x v (y v z). [para(96(a,1),10(b,1)),rewrite(290(3)),flip(b)]. given #1027 (F,wt=13): 3998 (x ^ (y ^ c1)) v (c2 ^ y) = c2 ^ y. [para(253(a,1),2542(a,1,2)),rewrite(253(11))]. given #1028 (F,wt=13): 4001 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(280(a,1),2542(a,1,2)),rewrite(280(7))]. given #1029 (T,wt=13): 4059 (x v (c2 v y)) ^ (z ^ c1) = z ^ c1. [para(17(a,1),2926(a,1,1))]. given #1030 (T,wt=13): 4074 (x v (y v c2)) ^ (z ^ c1) = z ^ c1. [para(3(a,1),2979(a,1,1))]. given #1031 (A,wt=15): 398 (x v y) ^ (z v (x v (u v y))) = x v y. [para(17(a,1),96(a,1,2,2))]. given #1032 (F,wt=13): 4086 (x ^ (y ^ c1)) v (z v c2) = z v c2. [para(5(a,1),3063(a,1,1))]. given #1033 (F,wt=13): 4107 (x ^ (c1 ^ y)) v (z v c2) = z v c2. [para(19(a,1),3211(a,1,1))]. given #1034 (T,wt=13): 4229 (c1 ^ (x ^ y)) v (c2 ^ x) = c2 ^ x. [para(4035(a,1),292(a,1,2)),rewrite(5(3),4035(11))]. given #1035 (T,wt=13): 4239 (x ^ (c1 ^ y)) v (c2 ^ y) = c2 ^ y. [para(4035(a,1),2542(a,1,2)),rewrite(4035(11))]. given #1036 (A,wt=17): 400 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(24(a,1),96(a,1,2,2))]. given #1037 (F,wt=13): 5427 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x. [para(154(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #1038 (F,wt=13): 6313 x ^ ((y ^ z) v (z ^ x)) = z ^ x. [para(160(a,1),53(a,1,2)),rewrite(101(4)),flip(a)]. given #1039 (T,wt=13): 6551 x ^ (((x v y) ^ (x v z)) v u) = x. [para(161(a,1),22(a,1)),rewrite(6(2)),flip(a)]. given #1040 (T,wt=13): 6574 x ^ (((x v y) ^ (z v x)) v u) = x. [para(161(a,1),97(a,1)),rewrite(20(2)),flip(a)]. low water: id=11577, wt=18 given #1041 (A,wt=21): 401 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(25(a,1),96(a,1,2,2))]. given #1042 (F,wt=13): 6584 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(161(a,1),178(a,1)),rewrite(173(4)),flip(a)]. given #1043 (F,wt=13): 6586 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(161(a,1),196(a,1)),rewrite(176(4)),flip(a)]. given #1044 (T,wt=13): 6635 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(17(a,1),6552(a,1,2,1,2))]. given #1045 (T,wt=13): 6636 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(17(a,1),6552(a,1,2))]. given #1046 (A,wt=17): 402 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(27(a,1),96(a,1,2,2)),rewrite(5(5),5(4))]. given #1047 (F,wt=13): 6676 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(3(a,1),6631(a,1,2,1,2))]. given #1048 (F,wt=13): 6679 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(17(a,1),6631(a,1,2))]. given #1049 (T,wt=13): 6718 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),6632(a,1,2))]. given #1050 (T,wt=13): 6721 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),6632(a,1,2,2,2))]. given #1051 (A,wt=15): 405 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(104(a,1),3(a,1)),flip(a)]. given #1052 (F,wt=13): 6755 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(3(a,1),6675(a,1,2,2,2))]. given #1053 (F,wt=13): 6756 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(3(a,1),6675(a,1,2))]. given #1054 (T,wt=13): 7045 (c2 ^ x) v (x ^ (c1 ^ y)) = c2 ^ x. [para(172(a,1),27(a,1,2))]. given #1055 (T,wt=13): 7167 x ^ (c1 ^ ((c2 ^ x) v y)) = x ^ c1. [para(154(a,1),175(a,1,2)),rewrite(89(4)),flip(a)]. given #1056 (A,wt=18): 407 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(104(a,1),10(a,1)),rewrite(278(5)),flip(a)]. given #1057 (F,wt=13): 7465 x v (c2 v ((x v c1) ^ y)) = x v c2. [para(106(a,1),182(a,2,2)),rewrite(2(6),110(7))]. given #1058 (F,wt=13): 7747 (c2 ^ x) v (c1 ^ (x ^ y)) = c2 ^ x. [para(253(a,1),183(a,1,2)),rewrite(27(6),4(7)),flip(a)]. given #1059 (T,wt=13): 8376 (x ^ c2) v (x ^ (c1 ^ y)) = x ^ c2. [para(344(a,1),188(a,1,1)),rewrite(5(5),2(8),6(9),5(5),2(8)),flip(a)]. given #1060 (T,wt=13): 8382 (c1 ^ (x ^ y)) v (x ^ c2) = c2 ^ x. [para(2842(a,1),188(a,1,1)),rewrite(5(5),5(9),2229(9),5(5)),flip(a)]. given #1061 (A,wt=15): 409 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(19(a,1),104(a,1,2,2))]. given #1062 (F,wt=13): 8991 c2 v (x v ((c1 v x) ^ y)) = c2 v x. [para(210(a,1),110(a,1)),rewrite(17(4),110(4)),flip(a)]. given #1063 (F,wt=13): 9534 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(215(a,1),24(a,1)),rewrite(7(2)),flip(a)]. given #1064 (T,wt=13): 9544 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(215(a,1),102(a,1)),rewrite(26(2)),flip(a)]. given #1065 (T,wt=13): 9546 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(215(a,1),250(a,1)),rewrite(248(4)),flip(a)]. given #1066 (A,wt=17): 410 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(21(a,1),104(a,1,2,2)),rewrite(3(5),3(4))]. given #1067 (F,wt=13): 9547 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(215(a,1),257(a,1)),rewrite(254(4)),flip(a)]. given #1068 (F,wt=13): 10014 (c2 ^ x) v (x ^ (y ^ c1)) = x ^ c2. [para(60(a,1),237(a,1,2,2))]. given #1069 (T,wt=13): 10039 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(238(a,1),2(a,1)),flip(a)]. given #1070 (T,wt=13): 10521 (x ^ c2) v (c1 ^ (x ^ y)) = c2 ^ x. [para(247(a,1),237(a,1,2))]. given #1071 (A,wt=17): 411 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(22(a,1),104(a,1,2,2))]. given #1072 (F,wt=13): 10526 (c2 ^ x) v (c1 ^ (y ^ x)) = c2 ^ x. [para(247(a,1),243(a,1,2))]. given #1073 (F,wt=13): 10646 (x ^ c2) v (y ^ (c1 ^ x)) = x ^ c2. [para(4(a,1),252(a,1,2)),rewrite(5(5))]. given #1074 (T,wt=13): 11271 (c1 v x) ^ (y v (x v c2)) = c1 v x. [para(112(a,1),293(a,1,2,2))]. given #1075 (T,wt=13): 11582 (c2 ^ x) v (y ^ (x ^ c1)) = c2 ^ x. [para(60(a,1),297(a,1,2,2))]. given #1076 (A,wt=21): 412 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(23(a,1),104(a,1,2,2))]. given #1077 (F,wt=13): 11600 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(305(a,1),4438(a,1,2)),rewrite(4(6))]. given #1078 (F,wt=13): 11615 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(305(a,1),4443(a,1,2)),rewrite(4(6))]. given #1079 (T,wt=13): 11892 x v ((x' v y) ^ (x' v z)) = 1. [para(305(a,1),4724(a,1,2)),rewrite(2(6))]. given #1080 (T,wt=13): 11909 x v ((x' v y) ^ (z v x')) = 1. [para(305(a,1),4728(a,1,2)),rewrite(2(6))]. given #1081 (A,wt=18): 414 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x. [para(104(a,1),36(a,1)),rewrite(4(5),278(5)),flip(a)]. given #1082 (F,wt=13): 12181 (x ^ y) v x' != 1 | x ^ y = x. [para(84(a,1),307(b,1)),rewrite(305(10)),flip(c),xx(b)]. given #1083 (F,wt=13): 12182 (c1 ^ x) v c2' != 1 | c1 ^ x = c2. [para(151(a,1),307(b,1)),rewrite(305(13)),flip(c),xx(b)]. given #1084 (T,wt=13): 12519 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),314(a,1,2,1))]. given #1085 (T,wt=13): 12550 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),315(a,1,2,1))]. given #1086 (A,wt=14): 420 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1. [para(110(a,1),36(a,1)),rewrite(4(8),173(8))]. given #1087 (F,wt=13): 12551 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),315(a,1,2,1)),rewrite(6(7)),flip(b)]. given #1088 (F,wt=13): 12552 (c2 v x) ^ c1' != 0 | c2 v x = c1. [para(173(a,1),315(a,1,2,1)),rewrite(173(11)),flip(b)]. given #1089 (T,wt=13): 12763 x v ((y v x') ^ (x' v z)) = 1. [para(305(a,1),8537(a,1,2)),rewrite(2(6))]. given #1090 (T,wt=13): 12772 x v ((y v x') ^ (z v x')) = 1. [para(305(a,1),8542(a,1,2)),rewrite(2(6))]. given #1091 (A,wt=24): 421 x v (c2 v y) != 1 | (x v c1) ^ (c2 v y) != 0 | (x v c1)' = c2 v y. [para(110(a,1),37(a,1,2))]. given #1092 (F,wt=13): 12870 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),323(a,1,2,1))]. given #1093 (F,wt=13): 12895 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(305(a,1),9404(a,1,2)),rewrite(4(6))]. given #1094 (T,wt=13): 12901 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),324(a,1,2,1))]. given #1095 (T,wt=13): 13061 x ^ ((y ^ x') v (z ^ x')) = 0. [para(305(a,1),9736(a,1,2)),rewrite(4(6))]. given #1096 (A,wt=18): 424 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(111(a,1),10(a,1))]. given #1097 (F,wt=13): 13114 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),332(a,1,2))]. given #1098 (F,wt=13): 13273 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),338(a,1,2))]. given #1099 (T,wt=13): 13334 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),341(a,1,1))]. given #1100 (T,wt=13): 13374 (x ^ c2) v (c1 ^ (y ^ x)) = x ^ c2. [para(342(a,1),104(a,1,2))]. given #1101 (A,wt=24): 430 x v (y v c2) != 1 | (x v c2) ^ (y v c1) != 0 | (x v c2)' = y v c1. [para(111(a,1),37(a,1,2))]. given #1102 (F,wt=13): 13582 (x ^ (y ^ c1)) v (y ^ c2) = y ^ c2. [para(415(a,1),2(a,1)),flip(a)]. given #1103 (F,wt=13): 13590 (x v c1) ^ (c2 v (y v x)) = x v c1. [para(2(a,1),419(a,1,2)),rewrite(3(5))]. given #1104 (T,wt=13): 13591 (x v c1) ^ (c2 v (x v y)) = x v c1. [para(17(a,1),419(a,1,2))]. given #1105 (T,wt=13): 13599 x v (y v x)' != 1 | x v y = x. [para(2(a,1),442(a,1,2,1))]. given #1106 (A,wt=14): 431 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1. [para(111(a,1),37(a,1)),rewrite(4(8),173(8))]. given #1107 (F,wt=13): 13601 x v (x v y)' != 1 | y v x = x. [para(2(a,1),445(a,1,2,1))]. given #1108 (F,wt=13): 13602 c1 v (x v c2)' != 1 | c2 v x = c1. [para(2(a,1),450(a,1,2,1))]. given #1109 (T,wt=13): 13603 c1 v (c2 v x)' != 1 | x v c2 = c1. [para(2(a,1),451(a,1,2,1))]. given #1110 (T,wt=13): 13604 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),454(a,1,1))]. given #1111 (A,wt=20): 432 x v (c2 v y) != 1 | c2 ^ (x v y) != 0 | (x v y)' = c2. [para(111(a,2),37(a,1,2)),rewrite(422(4),4(8))]. given #1112 (F,wt=13): 13606 x v (c2 v ((c1 v x) ^ y)) = x v c2. [para(459(a,1),182(a,1)),rewrite(2(5),112(10))]. given #1113 (F,wt=13): 13617 (c1 v x) ^ (c2 v (y v x)) = c1 v x. [para(540(a,1),96(a,1,2))]. given #1114 (T,wt=13): 13623 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),1851(a,1,2))]. given #1115 (T,wt=13): 13624 (c2 v x) ^ c1' != 0 | x v c2 = c1. [para(2(a,1),1853(a,1,1))]. given #1116 (A,wt=20): 435 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z. [para(5(a,1),38(b,1))]. given #1117 (F,wt=13): 13625 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),1887(a,1,2))]. given #1118 (F,wt=13): 13626 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),1892(a,1,2))]. given #1119 (T,wt=13): 13627 c2' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(4(a,1),1973(a,1,2))]. given #1120 (T,wt=13): 13628 (c1 ^ x) v c2' != 1 | x ^ c1 = c2. [para(4(a,1),1974(a,1,1))]. given #1121 (A,wt=20): 436 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z. [para(17(a,1),38(a,1))]. given #1122 (F,wt=13): 13629 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),2058(a,1,2))]. given #1123 (F,wt=13): 13630 c2' v (x ^ c1) != 1 | c1 ^ x = c2. [para(4(a,1),2062(a,1,2))]. given #1124 (T,wt=13): 13632 c1 ^ (x ^ (y v (x ^ c2))) = c1 ^ x. [para(2229(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #1125 (T,wt=13): 13675 x ^ (c1 v (c2 ^ (x v y))) = x ^ c2. [para(2843(a,1),42(a,1,2)),rewrite(157(8)),flip(a)]. given #1126 (A,wt=20): 437 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z. [para(19(a,1),38(b,1))]. given #1127 (F,wt=13): 13676 x ^ (c1 v (c2 ^ (y v x))) = x ^ c2. [para(2843(a,1),44(a,1,2)),rewrite(396(8)),flip(a)]. given #1128 (F,wt=13): 13711 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(13701(a,1),24(a,1,2)),rewrite(2(3),74(4)),flip(a)]. given #1129 (T,wt=13): 13714 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(13701(a,1),102(a,1,2)),rewrite(2(3),107(4)),flip(a)]. given #1130 (T,wt=13): 13744 (x v (y v c2)) ^ (c1 v x) = x v c1. [para(112(a,1),3030(a,1,1,2))]. given #1131 (A,wt=22): 438 x v (y v z) != 1 | x v y != 0 | (x v (y v z))' = x v y. [para(21(a,1),38(b,1)),rewrite(2(4),17(4),17(3),3(2),288(3),67(3))]. given #1132 (F,wt=13): 13768 (x ^ (y ^ c1)) v (c2 ^ x) = x ^ c2. [para(60(a,1),3295(a,1,1,2))]. given #1133 (F,wt=13): 13775 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(86(a,1),3399(a,2)),rewrite(2(9),187(12))]. given #1134 (T,wt=13): 13777 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(104(a,1),3399(a,2)),rewrite(2(9),404(12))]. given #1135 (T,wt=13): 13784 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(19(a,1),13772(a,1,2))]. given #1136 (A,wt=15): 439 x v (x' ^ y) != 1 | (x' ^ y)' = x. [para(84(a,1),38(b,1)),rewrite(2(3)),xx(b)]. given #1137 (F,wt=13): 13787 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(278(a,1),13772(a,1,2))]. given #1138 (F,wt=13): 13792 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(19(a,1),13773(a,1,2))]. given #1139 (T,wt=13): 13795 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(278(a,1),13773(a,1,2))]. given #1140 (T,wt=13): 13799 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(19(a,1),13782(a,1,2,2,2))]. given #1141 (A,wt=22): 440 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z)' = x. [para(22(a,1),38(b,1)),rewrite(2(3))]. given #1142 (F,wt=13): 13802 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(278(a,1),13782(a,1,2,2,2))]. given #1143 (F,wt=13): 13812 (c1 ^ (x ^ y)) v (c2 ^ y) = c2 ^ y. [para(4(a,1),3411(a,1,1)),rewrite(5(3))]. given #1144 (T,wt=13): 13881 (c2 v (x v y)) ^ (y v c1) = y v c1. [para(2(a,1),3866(a,1,1,2))]. given #1145 (T,wt=13): 13903 (x ^ (c1 ^ y)) v (y ^ c2) = c2 ^ y. [para(4(a,1),4239(a,1,2))]. given #1146 (A,wt=15): 441 x v (y ^ x') != 1 | (y ^ x')' = x. [para(94(a,1),38(b,1)),rewrite(2(3)),xx(b)]. given #1147 (F,wt=13): 13911 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(53(a,1),5427(a,1,2)),rewrite(8352(6))]. given #1148 (F,wt=13): 13916 x ^ ((y ^ x) v (z ^ y)) = y ^ x. [para(2(a,1),6313(a,1,2))]. given #1149 (T,wt=13): 13917 x ^ ((y ^ z) v (y ^ x)) = y ^ x. [para(4(a,1),6313(a,1,2,1))]. given #1150 (T,wt=13): 13918 x ^ ((y ^ z) v (x ^ z)) = z ^ x. [para(4(a,1),6313(a,1,2,2))]. given #1151 (A,wt=26): 444 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z))' = x. [para(23(a,1),38(b,1)),rewrite(2(4))]. given #1152 (F,wt=13): 13921 c1 ^ ((x ^ y) v (y ^ c2)) = y ^ c1. [para(6313(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1153 (F,wt=13): 13927 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),6551(a,1,2,1,1))]. given #1154 (T,wt=13): 13928 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),6551(a,1,2))]. given #1155 (T,wt=13): 13931 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(6551(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1156 (A,wt=15): 446 c1 v (c2' ^ x) != 1 | (c2' ^ x)' = c1. [para(151(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #1157 (F,wt=13): 13933 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(110(a,1),6551(a,1,2,1,1))]. given #1158 (F,wt=13): 13934 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(112(a,1),6551(a,1,2,1,1))]. given #1159 (T,wt=13): 13944 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),6574(a,1,2,1,1))]. given #1160 (T,wt=13): 13945 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),6574(a,1,2))]. given #1161 (A,wt=15): 447 c1 v (x ^ c2') != 1 | (x ^ c2')' = c1. [para(153(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #1162 (F,wt=13): 13948 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(6574(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1163 (F,wt=13): 13950 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(110(a,1),6574(a,1,2,1,1))]. given #1164 (T,wt=13): 13951 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(112(a,1),6574(a,1,2,1,1))]. given #1165 (T,wt=13): 13959 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(2(a,1),6584(a,1,2,1,1))]. given #1166 (A,wt=18): 448 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x)' = c1. [para(59(a,1),38(b,1)),rewrite(2(4))]. given #1167 (F,wt=13): 13960 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(2(a,1),6584(a,1,2))]. given #1168 (F,wt=13): 13964 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(112(a,1),6584(a,1,2,1,1))]. given #1169 (T,wt=13): 13970 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(2(a,1),6586(a,1,2,1,1))]. given #1170 (T,wt=13): 13971 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(2(a,1),6586(a,1,2))]. given #1171 (A,wt=14): 449 x v c2 != 1 | c1 != 0 | (x v c2)' = c1. [para(176(a,1),38(b,1)),rewrite(2(4),112(4))]. given #1172 (F,wt=13): 13975 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(112(a,1),6586(a,1,2,1,1))]. given #1173 (F,wt=13): 13985 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(139(a,1),6636(a,1,2,2))]. given #1174 (T,wt=13): 13988 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(139(a,1),6679(a,1,2,2))]. given #1175 (T,wt=13): 14014 (c1 ^ (x ^ y)) v (y ^ c2) = c2 ^ y. [para(4(a,1),8382(a,1,1,2))]. given #1176 (A,wt=19): 452 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x. [para(34(a,1),38(b,1)),rewrite(2(4)),xx(b)]. given #1177 (F,wt=13): 14022 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),9534(a,1,2,1,1))]. given #1178 (F,wt=13): 14023 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),9534(a,1,2))]. given #1179 (T,wt=13): 14026 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(60(a,1),9534(a,1,2,1,1))]. given #1180 (T,wt=13): 14037 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),9544(a,1,2,1,1))]. given #1181 (A,wt=18): 453 x v (y v z) != 1 | 0 != y | (x v (y v z))' = y. [para(73(a,1),38(b,1)),rewrite(2(3),288(3)),flip(b)]. given #1182 (F,wt=13): 14038 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),9544(a,1,2))]. given #1183 (F,wt=13): 14041 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(60(a,1),9544(a,1,2,1,1))]. given #1184 (T,wt=13): 14050 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(4(a,1),9546(a,1,2,1,1))]. given #1185 (T,wt=13): 14051 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(4(a,1),9546(a,1,2))]. given #1186 (A,wt=15): 455 (x ^ y) v y' != 1 | (x ^ y)' = y'. [para(329(a,1),38(b,1)),xx(b)]. given #1187 (F,wt=13): 14054 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(60(a,1),9546(a,1,2,1,1))]. given #1188 (F,wt=13): 14061 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),9547(a,1,2,1))]. given #1189 (T,wt=13): 14062 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),9547(a,1,2,1,1))]. given #1190 (T,wt=13): 14063 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),9547(a,1,2))]. given #1191 (A,wt=18): 456 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2)' = c1. [para(89(a,1),38(b,1)),rewrite(2(4))]. given #1192 (F,wt=13): 14066 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(60(a,1),9547(a,1,2,1,1))]. given #1193 (F,wt=13): 14090 c1 ^ ((c2' ^ x) v (c2' ^ y)) = 0. [hyper(325,a,1322,a,b,11600,a(flip)),rewrite(11600(9),4(10),77(12),305(11),11600(18))]. given #1194 (T,wt=13): 14102 c1 ^ ((c2' ^ x) v (y ^ c2')) = 0. [hyper(325,a,1322,a,b,11615,a(flip)),rewrite(11615(9),4(10),77(12),305(11),11615(18))]. given #1195 (T,wt=13): 14116 c2 v ((c1' v x) ^ (c1' v y)) = 1. [para(11892(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1196 (A,wt=18): 457 x v (y v z) != 1 | 0 != z | (x v (y v z))' = z. [para(96(a,1),38(b,1)),rewrite(2(3),290(3)),flip(b)]. given #1197 (F,wt=13): 14128 c2 v ((c1' v x) ^ (y v c1')) = 1. [para(11909(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1198 (F,wt=13): 14130 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),12181(a,1,1))]. given #1199 (T,wt=13): 14131 (x ^ c1) v c2' != 1 | c1 ^ x = c2. [para(4(a,1),12182(a,1,1))]. given #1200 (T,wt=13): 14132 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),12551(a,1,1))]. given #1201 (A,wt=24): 462 x v (y v c2) != 1 | (x v c1) ^ (y v c2) != 0 | (x v c1)' = y v c2. [para(112(a,1),37(a,1,2))]. given #1202 (F,wt=13): 14133 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(2(a,1),12552(a,1,1))]. given #1203 (F,wt=13): 14143 c2 v ((x v c1') ^ (c1' v y)) = 1. [para(12763(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1204 (T,wt=13): 14153 c2 v ((x v c1') ^ (y v c1')) = 1. [para(12772(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1205 (T,wt=13): 14160 c1 ^ ((x ^ c2') v (c2' ^ y)) = 0. [hyper(325,a,1322,a,b,12895,a(flip)),rewrite(12895(9),4(10),77(12),305(11),12895(18))]. given #1206 (A,wt=18): 463 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x)' = c2. [para(112(a,1),37(a,1)),rewrite(4(8))]. given #1207 (F,wt=13): 14170 c1 ^ ((x ^ c2') v (y ^ c2')) = 0. [hyper(325,a,1322,a,b,13061,a(flip)),rewrite(13061(9),4(10),77(12),305(11),13061(18))]. given #1208 (F,wt=13): 14202 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(188(a,1),13784(a,1,2,2))]. given #1209 (T,wt=13): 14204 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(188(a,1),13792(a,1,2,2))]. given #1210 (T,wt=13): 14208 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(4(a,1),13911(a,1,2,1))]. given #1211 (A,wt=18): 466 x v (c2 v y) != 1 | c1 != 0 | c1' = x v (c2 v y). [para(193(a,1),10(b,1)),rewrite(418(5))]. given #1212 (F,wt=13): 14209 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(4(a,1),13911(a,1,2,2))]. given #1213 (F,wt=13): 14212 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(4(a,1),13916(a,1,2,1))]. given #1214 (T,wt=13): 14213 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(4(a,1),13916(a,1,2,2))]. given #1215 (T,wt=13): 14220 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(4(a,1),13917(a,1,2,2))]. given #1216 (A,wt=18): 468 x v (c2 v y) != 1 | c1 != 0 | (x v (c2 v y))' = c1. [para(193(a,1),38(b,1)),rewrite(2(5),418(5))]. given #1217 (F,wt=13): 14223 c1 ^ ((x ^ y) v (x ^ c2)) = x ^ c1. [para(13917(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1218 (F,wt=13): 14224 x ^ ((y ^ c1) v (c2 ^ x)) = c2 ^ x. [para(60(a,1),13917(a,1,2,1))]. given #1219 (T,wt=13): 14237 c1 ^ ((x ^ y) v (c2 ^ y)) = y ^ c1. [para(13918(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1220 (T,wt=13): 14247 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),13927(a,1,2))]. given #1221 (A,wt=18): 471 x v (y v c2) != 1 | c1 != 0 | c1' = x v (y v c2). [para(195(a,1),10(b,1)),rewrite(459(5))]. given #1222 (F,wt=13): 14259 c1 ^ (x v ((c2 v y) ^ (c2 v z))) = c1. [para(13928(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1223 (F,wt=13): 14260 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(112(a,1),13928(a,1,2,2,1))]. given #1224 (T,wt=13): 14291 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),13944(a,1,2))]. given #1225 (T,wt=13): 14298 c1 ^ (x v ((c2 v y) ^ (z v c2))) = c1. [para(13945(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1226 (A,wt=18): 473 x v (y v c2) != 1 | c1 != 0 | (x v (y v c2))' = c1. [para(195(a,1),38(b,1)),rewrite(2(5),459(5))]. given #1227 (F,wt=13): 14299 c1 ^ (x v ((y v c2) ^ (z v c1))) = c1. [para(112(a,1),13945(a,1,2,2,1))]. given #1228 (F,wt=13): 14317 c1 ^ (x v ((y v c1) ^ (c2 v z))) = c1. [para(2(a,1),13959(a,1,2))]. given #1229 (T,wt=13): 14323 c1 ^ (x v ((y v c2) ^ (c2 v z))) = c1. [para(112(a,1),13960(a,1,2,2,1))]. given #1230 (T,wt=13): 14331 c1 ^ (x v ((y v c1) ^ (z v c2))) = c1. [para(2(a,1),13970(a,1,2))]. given #1231 (A,wt=18): 476 c2 != 1 | c1 ^ (x ^ y) != 0 | c2' = x ^ (y ^ c1). [para(255(a,1),10(a,1)),rewrite(247(8))]. given #1232 (F,wt=13): 14337 c1 ^ (x v ((y v c2) ^ (z v c2))) = c1. [para(112(a,1),13971(a,1,2,2,1))]. given #1233 (F,wt=13): 14349 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(4(a,1),14022(a,1,2))]. given #1234 (T,wt=13): 14360 c2 v (x ^ ((y ^ c1) v (c2 ^ z))) = c2. [para(60(a,1),14023(a,1,2,2,1))]. given #1235 (T,wt=13): 14376 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),14037(a,1,2))]. given #1236 (A,wt=18): 478 c2 != 1 | c1 ^ (x ^ y) != 0 | (x ^ (y ^ c1))' = c2. [para(255(a,1),36(a,1)),rewrit