============================== Prover9 =============================== Prover9 (32) version September-2006, September 2006. Process 27018 was started by mccune on cleo.thornwood, Wed Sep 13 14:41:39 2006 The command was "/home/mccune/LADR/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')) # label(goal). [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): 6574 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): 6656 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),6574(a,1,2,1,2))]. given #359 (T,wt=11): 6657 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(2(a,1),6574(a,1,2))]. given #360 (T,wt=11): 6700 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),6656(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 95 (0.00 of 4.13 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))]. Low Water (keep): wt=72, part=0.99, limit=62 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)]. Low Water (keep): wt=57, part=0.98, limit=56 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))]. Low Water (keep): wt=53, part=0.97, limit=53 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)]. Low Water (keep): wt=51, part=0.96, limit=50 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)]. Low Water (keep): wt=50, part=0.96, limit=50 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))]. Low Water (keep): wt=46, part=0.94, limit=46 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))]. Low Water (keep): wt=42, part=0.93, limit=42 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))]. Low Water (keep): wt=40, part=0.92, limit=40 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))]. Low Water (keep): wt=39, part=0.92, limit=39 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))]. Low Water (keep): wt=36, part=0.90, limit=36 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))]. Low Water (keep): wt=35, part=0.89, limit=35 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)]. Low Water (keep): wt=34, part=0.89, limit=34 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)]. Low Water (keep): wt=33, part=0.88, limit=33 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))]. 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))]. 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))]. 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))]. 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))]. 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))]. 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))]. Low Water (keep): wt=32, part=0.86, limit=32 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))]. 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))]. 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))]. 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)]. 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 (keep): wt=31, part=0.85, limit=31 given #644 (T,wt=12): 4434 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),191(a,1,1))]. 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)]. Low Water (keep): wt=30, part=0.84, limit=30 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))]. 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))]. Low Water (keep): wt=29, part=0.82, limit=29 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 (keep): wt=28, part=0.81, limit=28 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))]. Low Water (keep): wt=27, part=0.80, limit=27 given #666 (A,wt=14): 302 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),36(b,1))]. 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))]. 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): 6517 (x ^ c2) v (y ^ (c1 ^ x))' = 1. [para(4(a,1),1286(a,1,1))]. given #693 (F,wt=12): 6518 (c2 ^ (c1 v x)) v (y ^ c1)' = 1. [para(6(a,1),1286(a,1,2,1,2))]. given #694 (T,wt=12): 6522 (c2 ^ x) v (c1 ^ (y ^ x))' = 1. [para(19(a,1),1286(a,1,2,1))]. given #695 (T,wt=12): 6523 (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): 6544 (c2 ^ (x v y)) v (c1 ^ x)' = 1. [para(85(a,1),1286(a,1,2,1))]. given #698 (F,wt=12): 6549 (c2 ^ (x v y)) v (c1 ^ y)' = 1. [para(101(a,1),1286(a,1,2,1))]. given #699 (T,wt=12): 6665 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(6574(a,1),329(a,1,2)),rewrite(4(8))]. given #700 (T,wt=12): 6708 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(6656(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): 6750 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(6657(a,1),329(a,1,2)),rewrite(4(8))]. given #703 (F,wt=12): 6787 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(6700(a,1),329(a,1,2)),rewrite(4(8))]. given #704 (T,wt=12): 6833 (x ^ c2) v (x ^ (c1 ^ y))' = 1. [para(4(a,1),1288(a,1,2,1)),rewrite(5(5))]. Low Water (keep): wt=26, part=0.74, limit=26 given #705 (T,wt=12): 6837 (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): 6845 (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): 7018 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): 7019 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): 7020 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): 7059 x v ((y ^ x) v (x ^ z))' = 1. [para(1574(a,1),102(a,1)),flip(a)]. given #713 (F,wt=12): 7062 c2 v ((x ^ c1) v (c2 ^ y))' = 1. [para(1574(a,1),250(a,1)),flip(a)]. given #714 (T,wt=12): 7064 c2 v ((c1 ^ x) v (c2 ^ y))' = 1. [para(1574(a,1),257(a,1)),flip(a)]. given #715 (T,wt=12): 7274 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): 7275 x ^ (c1 ^ ((c2 v y) ^ x)') = 0. [para(2926(a,1),1779(a,1,2)),rewrite(4(6))]. given #718 (F,wt=12): 7276 x ^ (c1 ^ ((y v c2) ^ x)') = 0. [para(2979(a,1),1779(a,1,2)),rewrite(4(6))]. given #719 (T,wt=12): 7298 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): 7299 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): 7302 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): 7303 (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): 7304 (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): 7342 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): 7344 c1 ^ ((c2 v x) ^ (c1 v y))' = 0. [para(1785(a,1),178(a,1)),flip(a)]. given #728 (F,wt=12): 7346 c1 ^ ((x v c2) ^ (c1 v y))' = 0. [para(1785(a,1),196(a,1)),flip(a)]. given #729 (T,wt=12): 7451 c1 ^ (x ^ (c2 ^ (y v x))') = 0. [para(2169(a,1),1793(a,1,2)),rewrite(4(6))]. given #730 (T,wt=12): 7494 (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): 7549 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): 7982 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): 8121 (x ^ c2)' ^ (y ^ (c1 ^ x)) = 0. [para(4(a,1),1952(a,1,1,1))]. Low Water (keep): wt=25, part=0.72, limit=25 given #735 (T,wt=12): 8410 (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): 8588 c1 ^ (x ^ (y ^ (x ^ c2)')) = 0. [para(19(a,1),2010(a,1,2))]. given #738 (F,wt=12): 8914 (x ^ y)' v ((z v x) ^ y) = 1. [para(2168(a,1),2(a,1)),flip(a)]. given #739 (T,wt=12): 8916 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),2168(a,1,1))]. given #740 (T,wt=12): 8918 ((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): 8923 ((x v y) ^ (z v y)) v y' = 1. [para(20(a,1),2168(a,1,2,1))]. given #743 (F,wt=12): 8928 ((x v c1) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2168(a,1,2,1))]. given #744 (T,wt=12): 8929 ((x v c1) ^ (y v c2)) v c1' = 1. [para(176(a,1),2168(a,1,2,1))]. given #745 (T,wt=12): 9035 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): 9039 c1 ^ ((x v c1) ^ (c2 v y))' = 0. [para(2170(a,1),178(a,1)),flip(a)]. given #748 (F,wt=12): 9041 c1 ^ ((x v c1) ^ (y v c2))' = 0. [para(2170(a,1),196(a,1)),flip(a)]. given #749 (T,wt=12): 9090 c1 ^ ((c2 v x) ^ (y v c1))' = 0. [para(2188(a,1),178(a,1)),flip(a)]. given #750 (T,wt=12): 9092 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): 9708 x v (c2 v ((x v c1) ^ y)') = 1. [para(2313(a,1),17(a,1)),flip(a)]. given #753 (F,wt=12): 9709 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): 9720 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): 10018 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): 10029 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): 10314 c1 ^ (x ^ ((x ^ c2) v y)') = 0. [para(4(a,1),2420(a,1,2,2,1,1))]. given #759 (T,wt=12): 10317 x ^ (c1 ^ ((c2 ^ x) v y)') = 0. [para(2420(a,1),19(a,1)),flip(a)]. given #760 (T,wt=12): 10376 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(26(a,1),214(a,1,1,2,1)),rewrite(26(5))]. Low Water (keep): wt=24, part=0.70, limit=24 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): 10378 ((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): 10379 ((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): 10401 (x v (y ^ z)) ^ (z v x)' = 0. [para(279(a,1),214(a,1,1,2))]. given #765 (T,wt=12): 10406 (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): 10520 c1 ^ (x ^ (y v (x ^ c2))') = 0. [para(4(a,1),2444(a,1,2,2,1,2))]. given #768 (F,wt=12): 10702 (x ^ y)' v (x ^ (z v y)) = 1. [para(2468(a,1),2(a,1)),flip(a)]. given #769 (T,wt=12): 10933 (x v y)' ^ ((z ^ x) v y) = 0. [para(2538(a,1),4(a,1)),flip(a)]. given #770 (T,wt=12): 10938 ((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): 10943 (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): 10945 ((x ^ c2) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),2538(a,1,2,1))]. given #774 (T,wt=12): 10946 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),2538(a,1,2,1))]. given #775 (T,wt=12): 11058 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): 11064 c2 v ((x ^ c2) v (y ^ c1))' = 1. [para(2541(a,1),250(a,1)),flip(a)]. given #778 (F,wt=12): 11066 c2 v ((x ^ c2) v (c1 ^ y))' = 1. [para(2541(a,1),257(a,1)),flip(a)]. given #779 (T,wt=12): 11135 c2 v ((x ^ c1) v (y ^ c2))' = 1. [para(2566(a,1),250(a,1)),flip(a)]. given #780 (T,wt=12): 11138 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): 11172 ((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): 11173 ((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): 11211 (x ^ (y v c2)) v (c1 ^ x)' = 1. [para(3211(a,1),229(a,1,1,2))]. given #785 (T,wt=12): 11573 (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): 11724 c1' v ((c2 v x) ^ (c1 v y)) = 1. [para(139(a,1),2703(a,1,2))]. given #788 (F,wt=12): 11842 c1' v ((c2 v x) ^ (y v c1)) = 1. [para(139(a,1),2732(a,1,2))]. given #789 (T,wt=12): 11995 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(188(a,1),2756(a,1,2))]. given #790 (T,wt=12): 12090 (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): 12246 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(188(a,1),2809(a,1,2))]. given #793 (F,wt=12): 12391 (c1 v (x ^ y)) ^ (x v c2)' = 0. [para(24(a,1),2839(a,1,2,1)),rewrite(2(3))]. Low Water (keep): wt=23, part=0.67, limit=23 given #794 (T,wt=12): 12397 (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): 12503 (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): 12504 (x ^ (c2 v y)) v (c1 ^ x)' = 1. [para(4(a,1),2925(a,1,1))]. given #798 (F,wt=12): 12508 ((c2 v x) ^ (y v c1)) v c1' = 1. [para(20(a,1),2925(a,1,2,1))]. given #799 (T,wt=12): 12510 ((c2 v x) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2925(a,1,2,1))]. given #800 (T,wt=12): 12511 ((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): 12574 c1 ^ ((c2 v x) ^ (c2 v y))' = 0. [para(2927(a,1),178(a,1)),flip(a)]. given #803 (F,wt=12): 12575 c1 ^ ((c2 v x) ^ (y v c2))' = 0. [para(2927(a,1),196(a,1)),flip(a)]. given #804 (T,wt=12): 12593 c1 ^ ((x v c2) ^ (c2 v y))' = 0. [para(2940(a,1),196(a,1)),flip(a)]. given #805 (T,wt=12): 12603 (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): 12636 (c1 ^ x)' v ((y v c2) ^ x) = 1. [para(2978(a,1),2(a,1)),flip(a)]. given #808 (F,wt=12): 12640 ((x v c2) ^ (y v c1)) v c1' = 1. [para(20(a,1),2978(a,1,2,1))]. given #809 (T,wt=12): 12642 ((x v c2) ^ (c2 v y)) v c1' = 1. [para(173(a,1),2978(a,1,2,1))]. given #810 (T,wt=12): 12643 ((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): 12706 c1 ^ ((x v c2) ^ (y v c2))' = 0. [para(2980(a,1),196(a,1)),flip(a)]. given #813 (F,wt=12): 12781 (x ^ c1)' v (x ^ (y v c2)) = 1. [para(3007(a,1),2(a,1)),flip(a)]. given #814 (T,wt=12): 12899 (c2 v x)' ^ ((y ^ c1) v x) = 0. [para(3060(a,1),4(a,1)),flip(a)]. given #815 (T,wt=12): 12903 ((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): 12905 ((x ^ c1) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3060(a,1,2,1))]. given #818 (F,wt=12): 12906 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0. [para(254(a,1),3060(a,1,2,1))]. given #819 (T,wt=12): 12975 c2 v ((x ^ c1) v (y ^ c1))' = 1. [para(3062(a,1),250(a,1)),flip(a)]. given #820 (T,wt=12): 12976 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): 12996 c2 v ((c1 ^ x) v (y ^ c1))' = 1. [para(3078(a,1),257(a,1)),flip(a)]. given #823 (F,wt=12): 13053 (c2 ^ x) v (x ^ (y ^ c1))' = 1. [para(4(a,1),3113(a,1,2,1,2))]. given #824 (T,wt=12): 13123 (x v c2)' ^ (x v (y ^ c1)) = 0. [para(3119(a,1),4(a,1)),flip(a)]. given #825 (T,wt=12): 13406 (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): 13407 (c2 v x)' ^ ((c1 ^ y) v x) = 0. [para(3208(a,1),4(a,1)),flip(a)]. given #828 (F,wt=12): 13410 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),3208(a,1,2,1))]. given #829 (T,wt=12): 13412 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3208(a,1,2,1))]. given #830 (T,wt=12): 13413 ((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): 13461 c2 v ((c1 ^ x) v (c1 ^ y))' = 1. [para(3210(a,1),257(a,1)),flip(a)]. given #833 (F,wt=12): 13488 (x v c2)' ^ (x v (c1 ^ y)) = 0. [para(3241(a,1),4(a,1)),flip(a)]. given #834 (T,wt=12): 13656 (x ^ c2) v (c1 ^ (x ^ y))' = 1. [para(247(a,1),3316(a,1,2,1))]. given #835 (T,wt=12): 13753 (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): 13823 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0. [para(24(a,1),3461(a,1,2,1))]. given #838 (F,wt=12): 13827 (c1 v (x ^ c2)) ^ (c2 v y)' = 0. [para(102(a,1),3461(a,1,2,1))]. given #839 (T,wt=12): 13851 x v (c2 v ((c1 v x) ^ y)') = 1. [para(4(a,1),3737(a,1,2,2,1))]. given #840 (T,wt=12): 14123 (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): 14129 (c2 ^ (x v c1)) v (c1 ^ y)' = 1. [para(97(a,1),4226(a,1,2,1))]. given #843 (F,wt=12): 14173 (x v y)' ^ ((y ^ z) v x) = 0. [para(4273(a,1),4(a,1)),flip(a)]. given #844 (T,wt=12): 14202 (x v y)' ^ ((z ^ y) v x) = 0. [para(4276(a,1),4(a,1)),flip(a)]. given #845 (T,wt=12): 14267 (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): 14363 (x v c2)' ^ ((c1 ^ y) v x) = 0. [para(4282(a,1),4(a,1)),flip(a)]. given #848 (F,wt=12): 14408 (x v y)' ^ (y v (x ^ z)) = 0. [para(4434(a,1),4(a,1)),flip(a)]. given #849 (T,wt=12): 14461 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),4436(a,1,1,1))]. given #850 (T,wt=12): 14465 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): 14469 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(248(a,1),4436(a,1,1,1))]. given #853 (F,wt=12): 14470 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(254(a,1),4436(a,1,1,1))]. given #854 (T,wt=12): 14922 (x ^ y)' v ((y v z) ^ x) = 1. [para(4586(a,1),2(a,1)),flip(a)]. given #855 (T,wt=12): 14954 (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): 15009 (x ^ c1)' v ((c2 v y) ^ x) = 1. [para(4592(a,1),2(a,1)),flip(a)]. given #858 (F,wt=12): 15029 (x ^ c1)' v ((y v c2) ^ x) = 1. [para(4594(a,1),2(a,1)),flip(a)]. given #859 (T,wt=12): 15292 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),4722(a,1,2))]. given #860 (T,wt=12): 15294 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): 15298 x' v ((x v y) ^ (z v x)) = 1. [para(20(a,1),4722(a,1,1,1))]. given #863 (F,wt=12): 15303 c1' v ((c1 v x) ^ (c2 v y)) = 1. [para(173(a,1),4722(a,1,1,1))]. given #864 (T,wt=12): 15304 c1' v ((c1 v x) ^ (y v c2)) = 1. [para(176(a,1),4722(a,1,1,1))]. given #865 (T,wt=12): 16272 (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): 16405 (x v c2)' ^ (c1 v (y ^ c2)) = 0. [para(5504(a,1),4(a,1)),flip(a)]. given #868 (F,wt=12): 16421 (c2 v x)' ^ (c1 v (x ^ y)) = 0. [para(5516(a,1),4(a,1)),flip(a)]. given #869 (T,wt=12): 16462 (c2 v x)' ^ (c1 v (y ^ x)) = 0. [para(5522(a,1),4(a,1)),flip(a)]. given #870 (T,wt=12): 16551 (x ^ c1)' v (c2 ^ (c1 v y)) = 1. [para(6518(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): 16616 (x ^ c1)' v (c2 ^ (y v c1)) = 1. [para(6523(a,1),2(a,1)),flip(a)]. given #873 (F,wt=12): 16633 (c1 ^ x)' v (c2 ^ (x v y)) = 1. [para(6544(a,1),2(a,1)),flip(a)]. given #874 (T,wt=12): 16678 (c1 ^ x)' v (c2 ^ (y v x)) = 1. [para(6549(a,1),2(a,1)),flip(a)]. given #875 (T,wt=12): 16787 (x ^ c1)' v (c2 ^ (x v y)) = 1. [para(6837(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): 16819 (x ^ c1)' v (c2 ^ (y v x)) = 1. [para(6845(a,1),2(a,1)),flip(a)]. given #878 (F,wt=12): 17337 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),8914(a,1,2))]. given #879 (T,wt=12): 17338 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),8914(a,1,1,1))]. given #880 (T,wt=12): 17342 x' v ((y v x) ^ (z v x)) = 1. [para(20(a,1),8914(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): 17347 c1' v ((x v c1) ^ (c2 v y)) = 1. [para(173(a,1),8914(a,1,1,1))]. given #883 (F,wt=12): 17348 c1' v ((x v c1) ^ (y v c2)) = 1. [para(176(a,1),8914(a,1,1,1))]. given #884 (T,wt=12): 17745 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(10376(a,1),4(a,1)),flip(a)]. Low Water (keep): wt=22, part=0.61, limit=22 given #885 (T,wt=12): 17768 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(10378(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): 17800 (x v y)' ^ (y v (z ^ x)) = 0. [para(10401(a,1),4(a,1)),flip(a)]. given #888 (F,wt=12): 17891 (c2 v x)' ^ (x v (y ^ c1)) = 0. [para(10406(a,1),4(a,1)),flip(a)]. given #889 (T,wt=12): 17980 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(26(a,1),10933(a,1,1,1))]. given #890 (T,wt=12): 17984 c2' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(248(a,1),10933(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): 17985 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(254(a,1),10933(a,1,1,1))]. given #893 (F,wt=12): 18203 c1' v ((x v c2) ^ (c1 v y)) = 1. [para(11173(a,1),2(a,1)),flip(a)]. given #894 (T,wt=12): 18216 (c1 ^ x)' v (x ^ (y v c2)) = 1. [para(11211(a,1),2(a,1)),flip(a)]. given #895 (T,wt=12): 18295 c1' v ((c2 v x) ^ (c2 v y)) = 1. [para(110(a,1),11724(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): 18296 c1' v ((c2 v x) ^ (y v c2)) = 1. [para(112(a,1),11724(a,1,2,2))]. given #898 (F,wt=12): 18305 c1' v ((x v c2) ^ (y v c1)) = 1. [para(2(a,1),11842(a,1,2,1))]. given #899 (T,wt=12): 18318 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(60(a,1),11995(a,1,2,2))]. given #900 (T,wt=12): 18374 c2' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(4(a,1),12246(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): 18392 (x v c2)' ^ (c1 v (x ^ y)) = 0. [para(12391(a,1),4(a,1)),flip(a)]. given #903 (F,wt=12): 18404 (x v c2)' ^ (c1 v (y ^ x)) = 0. [para(12397(a,1),4(a,1)),flip(a)]. given #904 (T,wt=12): 18408 (c1 ^ x)' v (x ^ (c2 v y)) = 1. [para(4(a,1),12503(a,1,2))]. given #905 (T,wt=12): 18569 c1' v ((x v c2) ^ (c2 v y)) = 1. [para(173(a,1),12636(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): 18570 c1' v ((x v c2) ^ (y v c2)) = 1. [para(176(a,1),12636(a,1,1,1))]. given #908 (F,wt=12): 18698 c2' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(248(a,1),12899(a,1,1,1))]. given #909 (T,wt=12): 18699 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(254(a,1),12899(a,1,1,1))]. given #910 (T,wt=12): 18812 (c2 v x)' ^ (x v (c1 ^ y)) = 0. [para(13406(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): 18897 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(254(a,1),13407(a,1,1,1))]. given #913 (F,wt=12): 19000 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0. [para(13823(a,1),4(a,1)),flip(a)]. given #914 (T,wt=12): 19012 (c2 v x)' ^ (c1 v (y ^ c2)) = 0. [para(13827(a,1),4(a,1)),flip(a)]. given #915 (T,wt=12): 19029 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1. [para(14123(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): 19141 (c1 ^ x)' v (c2 ^ (y v c1)) = 1. [para(14129(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))]. Low Water (keep): wt=21, part=0.57, limit=21 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): 20674 c1' v (c1' v c2')' != 1. [ur(442,b,15,a)]. given #933 (F,wt=12): 20680 (c1' v (c1' v c2')')' != 0. [ur(4180,b,20674,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)]. Low Water (keep): wt=20, part=0.54, limit=20 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): 21859 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): 21860 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): 21896 x v (c2 ^ (c1 v x)) = x v c1. [para(2843(a,1),2635(a,1,2))]. given #975 (T,wt=11): 21975 x v (c2 ^ (x v c1)) = x v c1. [para(2(a,1),21896(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))]. 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))]. Low Water (keep): wt=19, part=0.51, limit=19 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))]. Low Water (displace): id=11740, wt=51 Low Water (displace): id=11646, wt=50 Low Water (displace): id=11819, wt=48 Low Water (displace): id=12023, wt=46 Low Water (displace): id=11809, wt=44 Low Water (displace): id=11886, wt=43 Low Water (displace): id=11897, wt=42 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)]. Low Water (displace): id=11888, wt=41 Low Water (displace): id=11894, wt=40 given #985 (T,wt=13): 3267 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),279(a,1,1))]. Low Water (displace): id=11839, wt=39 Low Water (displace): id=12077, wt=38 Low Water (displace): id=12915, wt=37 Low Water (displace): id=12874, wt=36 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))]. Low Water (displace): id=13231, wt=35 Low Water (displace): id=13370, wt=34 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))]. Low Water (displace): id=13600, wt=33 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))]. Low Water (displace): id=13733, wt=32 Low Water (displace): id=14318, wt=31 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): 22366 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(7(a,1),3399(a,2)),rewrite(2(7),24(10))]. Low Water (displace): id=14647, wt=30 given #993 (F,wt=11): 22367 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(26(a,1),3399(a,2)),rewrite(2(7),102(10))]. Low Water (displace): id=14577, wt=29 Low Water (displace): id=15167, wt=28 given #994 (T,wt=11): 22440 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(4(a,1),22366(a,1,2))]. Low Water (displace): id=15454, wt=27 given #995 (T,wt=11): 22492 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),22367(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))]. Low Water (keep): wt=18, part=0.50, limit=18 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))]. Low Water (displace): id=16691, wt=26 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))]. Low Water (displace): id=17245, wt=25 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): 6325 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): 6573 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): 6599 x ^ (((x v y) ^ (z v x)) v u) = x. [para(161(a,1),97(a,1)),rewrite(20(2)),flip(a)]. 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): 6609 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): 6611 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): 6660 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(17(a,1),6574(a,1,2,1,2))]. given #1045 (T,wt=13): 6661 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(17(a,1),6574(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): 6701 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(3(a,1),6656(a,1,2,1,2))]. given #1048 (F,wt=13): 6704 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(17(a,1),6656(a,1,2))]. given #1049 (T,wt=13): 6743 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),6657(a,1,2))]. given #1050 (T,wt=13): 6746 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),6657(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): 6780 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(3(a,1),6700(a,1,2,2,2))]. given #1053 (F,wt=13): 6781 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(3(a,1),6700(a,1,2))]. given #1054 (T,wt=13): 7085 (c2 ^ x) v (x ^ (c1 ^ y)) = c2 ^ x. [para(172(a,1),27(a,1,2))]. given #1055 (T,wt=13): 7238 x ^ (c1 ^ ((c2 ^ x) v y)) = x ^ c1. [para(154(a,1),175(a,1,2)),rewrite(89(4)),flip(a)]. Low Water (displace): id=17722, wt=24 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): 7569 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): 7885 (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): 8658 (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): 8664 (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): 9618 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): 10576 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): 10606 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): 10608 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): 10610 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): 11390 (c2 ^ x) v (x ^ (y ^ c1)) = x ^ c2. [para(60(a,1),237(a,1,2,2))]. given #1069 (T,wt=13): 11462 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(238(a,1),2(a,1)),flip(a)]. given #1070 (T,wt=13): 12463 (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): 12474 (c2 ^ x) v (c1 ^ (y ^ x)) = c2 ^ x. [para(247(a,1),243(a,1,2))]. given #1073 (F,wt=13): 12715 (x ^ c2) v (y ^ (c1 ^ x)) = x ^ c2. [para(4(a,1),252(a,1,2)),rewrite(5(5))]. given #1074 (T,wt=13): 14048 (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): 14528 (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): 14585 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(305(a,1),4438(a,1,2)),rewrite(4(6))]. given #1078 (F,wt=13): 14610 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(305(a,1),4443(a,1,2)),rewrite(4(6))]. given #1079 (T,wt=13): 15440 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): 15468 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): 16289 (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): 16291 (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): 17030 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),314(a,1,2,1))]. given #1085 (T,wt=13): 17090 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): 17091 (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): 17094 (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): 17499 x v ((y v x') ^ (x' v z)) = 1. [para(305(a,1),8918(a,1,2)),rewrite(2(6))]. given #1090 (T,wt=13): 17516 x v ((y v x') ^ (z v x')) = 1. [para(305(a,1),8923(a,1,2)),rewrite(2(6))]. Low Water (displace): id=18384, wt=23 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): 17714 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),323(a,1,2,1))]. given #1093 (F,wt=13): 17750 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(305(a,1),10376(a,1,2)),rewrite(4(6))]. given #1094 (T,wt=13): 17760 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),324(a,1,2,1))]. given #1095 (T,wt=13): 18036 x ^ ((y ^ x') v (z ^ x')) = 0. [para(305(a,1),10938(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): 18185 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),332(a,1,2))]. given #1098 (F,wt=13): 18447 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),338(a,1,2))]. given #1099 (T,wt=13): 18563 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),341(a,1,1))]. given #1100 (T,wt=13): 18631 (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): 20473 (x ^ (y ^ c1)) v (y ^ c2) = y ^ c2. [para(415(a,1),2(a,1)),flip(a)]. given #1103 (F,wt=13): 20532 (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): 20536 (x v c1) ^ (c2 v (x v y)) = x v c1. [para(17(a,1),419(a,1,2))]. given #1105 (T,wt=13): 20675 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): 20681 x v (x v y)' != 1 | y v x = x. [para(2(a,1),445(a,1,2,1))]. given #1108 (F,wt=13): 20682 c1 v (x v c2)' != 1 | c2 v x = c1. [para(2(a,1),450(a,1,2,1))]. given #1109 (T,wt=13): 20684 c1 v (c2 v x)' != 1 | x v c2 = c1. [para(2(a,1),451(a,1,2,1))]. given #1110 (T,wt=13): 20686 (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): 20697 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): 21368 (c1 v x) ^ (c2 v (y v x)) = c1 v x. [para(540(a,1),96(a,1,2))]. given #1114 (T,wt=13): 21463 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),1851(a,1,2))]. given #1115 (T,wt=13): 21465 (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): 21468 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),1887(a,1,2))]. given #1118 (F,wt=13): 21470 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),1892(a,1,2))]. given #1119 (T,wt=13): 21472 c2' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(4(a,1),1973(a,1,2))]. given #1120 (T,wt=13): 21474 (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): 21476 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),2058(a,1,2))]. given #1123 (F,wt=13): 21478 c2' v (x ^ c1) != 1 | c1 ^ x = c2. [para(4(a,1),2062(a,1,2))]. given #1124 (T,wt=13): 21485 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): 21857 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): 21858 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): 21981 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(21896(a,1),24(a,1,2)),rewrite(2(3),74(4)),flip(a)]. given #1129 (T,wt=13): 21985 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(21896(a,1),102(a,1,2)),rewrite(2(3),107(4)),flip(a)]. given #1130 (T,wt=13): 22118 (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): 22321 (x ^ (y ^ c1)) v (c2 ^ x) = x ^ c2. [para(60(a,1),3295(a,1,1,2))]. given #1133 (F,wt=13): 22370 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): 22372 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): 22442 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(19(a,1),22366(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): 22472 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(278(a,1),22366(a,1,2))]. given #1138 (F,wt=13): 22494 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(19(a,1),22367(a,1,2))]. given #1139 (T,wt=13): 22525 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(278(a,1),22367(a,1,2))]. given #1140 (T,wt=13): 22546 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(19(a,1),22440(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): 22574 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(278(a,1),22440(a,1,2,2,2))]. given #1143 (F,wt=13): 22642 (c1 ^ (x ^ y)) v (c2 ^ y) = c2 ^ y. [para(4(a,1),3411(a,1,1)),rewrite(5(3))]. given #1144 (T,wt=13): 23012 (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): 23252 (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): 23265 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(53(a,1),5427(a,1,2)),rewrite(8624(6))]. given #1148 (F,wt=13): 23282 x ^ ((y ^ x) v (z ^ y)) = y ^ x. [para(2(a,1),6325(a,1,2))]. given #1149 (T,wt=13): 23283 x ^ ((y ^ z) v (y ^ x)) = y ^ x. [para(4(a,1),6325(a,1,2,1))]. given #1150 (T,wt=13): 23284 x ^ ((y ^ z) v (x ^ z)) = z ^ x. [para(4(a,1),6325(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): 23289 c1 ^ ((x ^ y) v (y ^ c2)) = y ^ c1. [para(6325(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1153 (F,wt=13): 23313 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),6573(a,1,2,1,1))]. given #1154 (T,wt=13): 23314 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),6573(a,1,2))]. given #1155 (T,wt=13): 23319 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(6573(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): 23321 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(110(a,1),6573(a,1,2,1,1))]. given #1158 (F,wt=13): 23322 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(112(a,1),6573(a,1,2,1,1))]. given #1159 (T,wt=13): 23345 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),6599(a,1,2,1,1))]. given #1160 (T,wt=13): 23346 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),6599(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): 23351 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(6599(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1163 (F,wt=13): 23354 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(110(a,1),6599(a,1,2,1,1))]. given #1164 (T,wt=13): 23355 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(112(a,1),6599(a,1,2,1,1))]. given #1165 (T,wt=13): 23381 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(2(a,1),6609(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): 23382 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(2(a,1),6609(a,1,2))]. given #1168 (F,wt=13): 23388 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(112(a,1),6609(a,1,2,1,1))]. given #1169 (T,wt=13): 23401 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(2(a,1),6611(a,1,2,1,1))]. given #1170 (T,wt=13): 23402 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(2(a,1),6611(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): 23408 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(112(a,1),6611(a,1,2,1,1))]. given #1173 (F,wt=13): 23437 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(139(a,1),6661(a,1,2,2))]. given #1174 (T,wt=13): 23461 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(139(a,1),6704(a,1,2,2))]. given #1175 (T,wt=13): 23582 (c1 ^ (x ^ y)) v (y ^ c2) = c2 ^ y. [para(4(a,1),8664(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): 23607 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),10576(a,1,2,1,1))]. given #1178 (F,wt=13): 23608 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),10576(a,1,2))]. given #1179 (T,wt=13): 23612 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(60(a,1),10576(a,1,2,1,1))]. Low Water (displace): id=19727, wt=22 given #1180 (T,wt=13): 23639 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),10606(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): 23640 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),10606(a,1,2))]. given #1183 (F,wt=13): 23645 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(60(a,1),10606(a,1,2,1,1))]. given #1184 (T,wt=13): 23670 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(4(a,1),10608(a,1,2,1,1))]. given #1185 (T,wt=13): 23671 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(4(a,1),10608(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): 23675 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(60(a,1),10608(a,1,2,1,1))]. given #1188 (F,wt=13): 23691 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),10610(a,1,2,1))]. given #1189 (T,wt=13): 23693 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),10610(a,1,2,1,1))]. given #1190 (T,wt=13): 23694 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),10610(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): 23698 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(60(a,1),10610(a,1,2,1,1))]. given #1193 (F,wt=13): 23814 c1 ^ ((c2' ^ x) v (c2' ^ y)) = 0. [hyper(325,a,1322,a,b,14585,a(flip)),rewrite(14585(9),4(10),77(12),305(11),14585(18))]. given #1194 (T,wt=13): 23833 c1 ^ ((c2' ^ x) v (y ^ c2')) = 0. [hyper(325,a,1322,a,b,14610,a(flip)),rewrite(14610(9),4(10),77(12),305(11),14610(18))]. given #1195 (T,wt=13): 23855 c2 v ((c1' v x) ^ (c1' v y)) = 1. [para(15440(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): 23879 c2 v ((c1' v x) ^ (y v c1')) = 1. [para(15468(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1198 (F,wt=13): 23886 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),16289(a,1,1))]. given #1199 (T,wt=13): 23888 (x ^ c1) v c2' != 1 | c1 ^ x = c2. [para(4(a,1),16291(a,1,1))]. given #1200 (T,wt=13): 23892 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),17091(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): 23894 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(2(a,1),17094(a,1,1))]. given #1203 (F,wt=13): 23912 c2 v ((x v c1') ^ (c1' v y)) = 1. [para(17499(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1204 (T,wt=13): 23934 c2 v ((x v c1') ^ (y v c1')) = 1. [para(17516(a,1),2033(a,1,2,2,1)),rewrite(79(10),2(10),77(10),2(9))]. given #1205 (T,wt=13): 23952 c1 ^ ((x ^ c2') v (c2' ^ y)) = 0. [hyper(325,a,1322,a,b,17750,a(flip)),rewrite(17750(9),4(10),77(12),305(11),17750(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): 23969 c1 ^ ((x ^ c2') v (y ^ c2')) = 0. [hyper(325,a,1322,a,b,18036,a(flip)),rewrite(18036(9),4(10),77(12),305(11),18036(18))]. given #1208 (F,wt=13): 24171 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(188(a,1),22442(a,1,2,2))]. given #1209 (T,wt=13): 24184 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(188(a,1),22494(a,1,2,2))]. given #1210 (T,wt=13): 24216 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(4(a,1),23265(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): 24217 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(4(a,1),23265(a,1,2,2))]. given #1213 (F,wt=13): 24226 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(4(a,1),23282(a,1,2,1))]. given #1214 (T,wt=13): 24227 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(4(a,1),23282(a,1,2,2))]. given #1215 (T,wt=13): 24247 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(4(a,1),23283(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): 24252 c1 ^ ((x ^ y) v (x ^ c2)) = x ^ c1. [para(23283(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1218 (F,wt=13): 24253 x ^ ((y ^ c1) v (c2 ^ x)) = c2 ^ x. [para(60(a,1),23283(a,1,2,1))]. given #1219 (T,wt=13): 24284 c1 ^ ((x ^ y) v (c2 ^ y)) = y ^ c1. [para(23284(a,1),59(a,1,2)),rewrite(89(4)),flip(a)]. given #1220 (T,wt=13): 24317 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),23313(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): 24346 c1 ^ (x v ((c2 v y) ^ (c2 v z)))