============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27208 was started by mccune on cleo, Fri Apr 13 09:24:39 2007 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H42.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file lt.in formulas(sos). x v y = y v x. (x v y) v z = x v (y v z). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. end_of_list. % Reading from file uc.in formulas(sos). x v x' = 1. x ^ x' = 0. x v y != 1 | x ^ y != 0 | x' = y. end_of_list. % Reading from file H42.in assign(max_seconds,300). 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 (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 #14 (T,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #15 (T,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #16 (T,wt=5): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #17 (T,wt=5): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #18 (A,wt=11): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #19 (T,wt=5): 75 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #20 (T,wt=4): 84 1' = 0. [hyper(10,a,35,a,b,75,a)]. given #21 (T,wt=5): 77 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #22 (T,wt=4): 87 0' = 1. [hyper(10,a,77,a,b,32,a)]. given #23 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #24 (T,wt=5): 85 1 v x = 1. [para(75(a,1),6(a,1))]. given #25 (T,wt=5): 88 0 ^ x = 0. [para(77(a,1),6(a,1,2))]. given #26 (T,wt=5): 96 x v 1 = 1. [para(20(a,1),75(a,1)),flip(a)]. given #27 (T,wt=5): 99 x ^ 0 = 0. [para(88(a,1),4(a,1)),flip(a)]. given #28 (A,wt=13): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #29 (T,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #30 (T,wt=5): 114 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. given #31 (T,wt=7): 97 0 != x | x' = 1. [back_rewrite(76),rewrite(96(2)),xx(a)]. given #32 (T,wt=7): 101 1 != x | x' = 0. [back_rewrite(78),rewrite(99(4)),xx(b)]. given #33 (A,wt=11): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #34 (T,wt=8): 86 x v (x' v y) = 1. [back_rewrite(30),rewrite(85(5))]. given #35 (T,wt=8): 89 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(88(5))]. given #36 (T,wt=8): 98 x v (y v x') = 1. [back_rewrite(64),rewrite(96(5))]. given #37 (T,wt=8): 100 x ^ (y ^ x') = 0. [back_rewrite(81),rewrite(99(5))]. given #38 (A,wt=13): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #39 (F,wt=9): 130 c1 ^ (c1' v c2') != 0. [ur(10,a,86,a,c,15,a(flip))]. given #40 (T,wt=8): 125 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #41 (T,wt=6): 158 c1 ^ c2' = 0. [para(114(a,1),125(a,1,2,1))]. given #42 (T,wt=8): 153 x ^ (y v x)' = 0. [para(2(a,1),125(a,1,2,1))]. given #43 (T,wt=8): 159 c1 ^ (c2' ^ x) = 0. [para(158(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #44 (A,wt=11): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #45 (T,wt=8): 161 c1 ^ (x ^ c2') = 0. [para(158(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #46 (T,wt=8): 172 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #47 (T,wt=8): 183 x v (y ^ x)' = 1. [para(4(a,1),172(a,1,2,1))]. given #48 (T,wt=6): 191 c2 v c1' = 1. [para(13(a,1),183(a,1,2,1))]. given #49 (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 #50 (T,wt=8): 196 c2 v (c1' v x) = 1. [para(191(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #51 (T,wt=8): 198 c2 v (x v c1') = 1. [para(191(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #52 (T,wt=9): 59 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #53 (T,wt=7): 213 c1 ^ (c2 v x) = c1. [para(6(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #54 (A,wt=13): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #55 (T,wt=7): 216 c1 ^ (x v c2) = c1. [para(20(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #56 (T,wt=8): 220 c1 ^ (c2 v x)' = 0. [para(125(a,1),59(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #57 (T,wt=8): 221 c1 ^ (x v c2)' = 0. [para(153(a,1),59(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #58 (T,wt=9): 60 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite(4(4))]. given #59 (A,wt=10): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #60 (T,wt=7): 248 c2 v (x ^ c1) = c2. [para(60(a,1),7(a,1,2))]. given #61 (T,wt=7): 260 c2 v (c1 ^ x) = c2. [para(4(a,1),248(a,1,2))]. given #62 (T,wt=8): 251 c2 v (x ^ c1)' = 1. [para(60(a,1),172(a,1,2,1))]. given #63 (T,wt=8): 268 c2 v (c1 ^ x)' = 1. [para(4(a,1),251(a,1,2,1))]. given #64 (A,wt=10): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #65 (T,wt=9): 62 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #66 (T,wt=9): 66 x ^ (x ^ y) = x ^ y. [para(28(a,1),5(a,1,1)),flip(a)]. given #67 (T,wt=9): 68 x ^ (y ^ x) = y ^ x. [para(28(a,1),5(a,2,2)),rewrite(4(2))]. given #68 (T,wt=9): 71 x v (x v y) = x v y. [para(29(a,1),3(a,1,1)),flip(a)]. given #69 (A,wt=14): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #70 (T,wt=5): 298 x'' = x. [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #71 (T,wt=8): 319 x' v (y v x) = 1. [para(298(a,1),98(a,1,2,2))]. given #72 (T,wt=8): 320 x' ^ (y ^ x) = 0. [para(298(a,1),100(a,1,2,2))]. given #73 (T,wt=9): 73 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite(2(2))]. given #74 (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 #75 (T,wt=9): 80 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #76 (T,wt=9): 83 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #77 (T,wt=9): 90 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #78 (T,wt=9): 112 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #79 (A,wt=14): 38 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #80 (T,wt=9): 120 c1 v (c2 v x) = c2 v x. [para(114(a,1),3(a,1,1)),flip(a)]. given #81 (T,wt=9): 121 c2 v (x v c1) = x v c2. [para(114(a,1),3(a,2,2)),rewrite(2(4))]. given #82 (T,wt=9): 122 c1 v (x v c2) = x v c2. [para(114(a,1),17(a,1,2)),flip(a)]. given #83 (T,wt=9): 224 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),213(a,1,2))]. given #84 (A,wt=20): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #85 (T,wt=9): 235 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),216(a,1,2))]. given #86 (T,wt=9): 261 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),248(a,1,2))]. given #87 (T,wt=9): 266 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),260(a,1,2))]. given #88 (T,wt=9): 308 c2 ^ c1' != 0 | c2 = c1. [para(191(a,1),36(a,1)),rewrite(4(7),298(12)),flip(c),xx(a)]. given #89 (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 #90 (T,wt=9): 427 c1 v c2' != 1 | c2 = c1. [para(158(a,1),38(b,1)),rewrite(2(4),298(12)),xx(b)]. given #91 (T,wt=9): 446 c2 v (x v c1) = c2 v x. [para(121(a,2),2(a,1))]. given #92 (T,wt=10): 69 1 != x | 0 != x | x' = x. [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)]. given #93 (T,wt=10): 118 c2 != 1 | c1 != 0 | c1' = c2. [back_rewrite(61),rewrite(114(3))]. given #94 (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 #95 (T,wt=10): 133 x v (y v (x' v z)) = 1. [para(86(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #96 (T,wt=10): 136 x ^ (y ^ (x' ^ z)) = 0. [para(89(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #97 (T,wt=10): 137 x ^ ((x v y)' ^ z) = 0. [para(89(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #98 (T,wt=10): 139 x v (y v (z v x')) = 1. [para(3(a,1),98(a,1,2))]. given #99 (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 #100 (T,wt=10): 142 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),100(a,1,2))]. given #101 (T,wt=10): 144 x ^ (y ^ (x v z)') = 0. [para(100(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #102 (T,wt=10): 157 x ^ (y v (x v z))' = 0. [para(17(a,1),125(a,1,2,1))]. given #103 (T,wt=10): 162 x ^ (y v (z v x))' = 0. [para(3(a,1),153(a,1,2,1))]. given #104 (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 #105 (T,wt=10): 163 x ^ ((y v x)' ^ z) = 0. [para(153(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #106 (T,wt=10): 167 x ^ (y ^ (z v x)') = 0. [para(153(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #107 (T,wt=10): 169 c1 ^ (x ^ (c2' ^ y)) = 0. [para(159(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #108 (T,wt=10): 177 x v ((x ^ y)' v z) = 1. [para(86(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #109 (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 #110 (T,wt=10): 178 x v (y v (x ^ z)') = 1. [para(98(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #111 (T,wt=10): 180 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),161(a,1,2))]. given #112 (T,wt=10): 186 x v (y ^ (x ^ z))' = 1. [para(19(a,1),172(a,1,2,1))]. given #113 (T,wt=10): 187 x v ((y ^ x)' v z) = 1. [para(183(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #114 (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 #115 (T,wt=10): 189 x v (y ^ (z ^ x))' = 1. [para(5(a,1),183(a,1,2,1))]. given #116 (T,wt=10): 192 x v (y v (z ^ x)') = 1. [para(183(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #117 (T,wt=10): 209 c2 v (x v (c1' v y)) = 1. [para(196(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #118 (T,wt=10): 210 c2 v (x v (y v c1')) = 1. [para(3(a,1),198(a,1,2))]. given #119 (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 #120 (T,wt=10): 222 (c2 ^ x) v (c1 ^ x)' = 1. [para(59(a,1),183(a,1,2,1))]. given #121 (T,wt=10): 239 c1 ^ ((c2 v x)' ^ y) = 0. [para(220(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #122 (T,wt=10): 241 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),220(a,1,2,1))]. given #123 (T,wt=10): 242 c1 ^ (x ^ (c2 v y)') = 0. [para(220(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #124 (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 #125 (T,wt=10): 243 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),221(a,1,2,1))]. given #126 (T,wt=10): 244 c1 ^ ((x v c2)' ^ y) = 0. [para(221(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #127 (T,wt=10): 246 c1 ^ (x ^ (y v c2)') = 0. [para(221(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #128 (T,wt=10): 254 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #129 (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 #130 (T,wt=10): 267 c2 v ((x ^ c1)' v y) = 1. [para(251(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #131 (T,wt=10): 269 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),251(a,1,2,1))]. given #132 (T,wt=10): 271 c2 v (x v (y ^ c1)') = 1. [para(251(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #133 (T,wt=10): 272 c2 v ((c1 ^ x)' v y) = 1. [para(268(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #134 (A,wt=11): 63 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #135 (T,wt=10): 274 c2 v (x v (c1 ^ y)') = 1. [para(268(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #136 (T,wt=10): 275 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),268(a,1,2,1))]. given #137 (T,wt=10): 276 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),34(a,1,2,2,1))]. given #138 (T,wt=10): 282 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),59(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #139 (A,wt=20): 65 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #140 (T,wt=10): 302 c2 != 1 | c1 != 0 | c2' = c1. [para(114(a,1),36(a,1)),rewrite(4(6),13(6))]. given #141 (T,wt=10): 321 x' v (y v (x v z)) = 1. [para(319(a,1),3(a,1,1)),rewrite(85(2),3(4)),flip(a)]. given #142 (T,wt=8): 1869 c1' v (x v c2) = 1. [para(114(a,1),321(a,1,2,2))]. given #143 (T,wt=10): 322 x' v (y v (z v x)) = 1. [para(3(a,1),319(a,1,2))]. given #144 (A,wt=14): 70 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(41),rewrite(66(4))]. given #145 (T,wt=7): 1915 c1 != 1 | c1' = 0. [para(158(a,1),70(b,1)),rewrite(158(12)),flip(a),xx(b)]. given #146 (T,wt=7): 1917 x' != 1 | 0 = x. [para(320(a,1),70(b,1)),rewrite(298(8),320(9)),flip(a),flip(c),xx(b)]. given #147 (T,wt=10): 327 x' ^ (y ^ (x ^ z)) = 0. [para(320(a,1),5(a,1,1)),rewrite(88(2),5(4)),flip(a)]. given #148 (T,wt=10): 328 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),320(a,1,2))]. given #149 (A,wt=14): 74 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(40),rewrite(71(2))]. given #150 (F,wt=10): 1921 (c1 ^ (c1' v c2'))' != 1. [ur(1917,b,130,a(flip))]. given #151 (T,wt=7): 1964 c2 != 0 | c2' = 1. [para(191(a,1),74(a,1)),rewrite(191(12)),flip(b),xx(a)]. given #152 (T,wt=7): 1966 x' != 0 | 1 = x. [para(319(a,1),74(a,1)),rewrite(298(8),319(9)),flip(b),flip(c),xx(a)]. given #153 (T,wt=7): 1968 c1' != 0 | c1 = 1. [para(1869(a,1),74(a,1)),rewrite(298(10),1869(13)),flip(b),xx(a)]. given #154 (T,wt=8): 1936 c2' ^ (x ^ c1) = 0. [para(13(a,1),328(a,1,2,2))]. given #155 (A,wt=11): 79 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #156 (T,wt=7): 1976 c2' != 1 | c2 = 0. [para(1936(a,1),70(b,1)),rewrite(298(10),1936(13)),flip(a),xx(b)]. given #157 (T,wt=10): 393 (x ^ c2) v (x ^ c1)' = 1. [para(83(a,1),183(a,1,2,1))]. given #158 (T,wt=10): 394 x ^ (c1 ^ (x ^ c2)') = 0. [para(83(a,1),320(a,1,2)),rewrite(4(6),5(6))]. given #159 (T,wt=10): 449 (x v c1) ^ (x v c2)' = 0. [para(121(a,1),153(a,1,2,1))]. given #160 (A,wt=20): 82 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(19(a,1),10(b,1))]. given #161 (T,wt=10): 453 x v (c2 v (x v c1)') = 1. [para(121(a,1),319(a,1,2)),rewrite(2(6),3(6))]. given #162 (T,wt=10): 601 (x v c1) ^ (c2 v x)' = 0. [para(446(a,1),153(a,1,2,1))]. given #163 (T,wt=10): 603 c2 v (x v (x v c1)') = 1. [para(446(a,1),319(a,1,2)),rewrite(2(6),3(6))]. given #164 (T,wt=10): 1292 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),222(a,1,1))]. given #165 (A,wt=11): 91 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #166 (T,wt=10): 1293 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),222(a,1,2,1))]. given #167 (T,wt=10): 1294 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),222(a,1,2,1))]. given #168 (T,wt=10): 1298 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),222(a,1,2,1))]. given #169 (T,wt=10): 1792 c1 ^ (x ^ (x ^ c2)') = 0. [para(276(a,1),59(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #170 (A,wt=13): 92 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #171 (T,wt=10): 1803 x ^ (c1 ^ (c2 ^ x)') = 0. [para(282(a,1),19(a,1)),flip(a)]. given #172 (T,wt=10): 1805 c1 ^ (c2 ^ (c1 v x))' = 0. [para(282(a,1),22(a,1)),flip(a)]. given #173 (T,wt=10): 1874 c1' v (x v (c2 v y)) = 1. [para(120(a,1),321(a,1,2,2))]. given #174 (T,wt=10): 1875 c1' v (x v (y v c2)) = 1. [para(122(a,1),321(a,1,2,2))]. given #175 (A,wt=14): 93 x v y != 1 | 0 != y | y' = x v y. [para(20(a,1),10(b,1)),rewrite(73(2)),flip(b)]. given #176 (T,wt=10): 1889 (x ^ y)' v (z v x) = 1. [para(7(a,1),322(a,1,2,2))]. given #177 (T,wt=10): 1891 (x ^ y)' v (z v y) = 1. [para(26(a,1),322(a,1,2,2))]. given #178 (T,wt=10): 1895 (x ^ c1)' v (y v c2) = 1. [para(248(a,1),322(a,1,2,2))]. given #179 (T,wt=10): 1896 (c1 ^ x)' v (y v c2) = 1. [para(260(a,1),322(a,1,2,2))]. given #180 (A,wt=13): 94 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #181 (T,wt=10): 1913 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),70(b,1)),rewrite(13(11)),flip(a)]. given #182 (T,wt=10): 1925 c2' ^ (x ^ (y ^ c1)) = 0. [para(60(a,1),327(a,1,2,2))]. given #183 (T,wt=10): 1934 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),328(a,1,2,2))]. given #184 (T,wt=10): 1938 (x v y)' ^ (z ^ y) = 0. [para(20(a,1),328(a,1,2,2))]. given #185 (A,wt=11): 95 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #186 (T,wt=10): 1943 (c2 v x)' ^ (y ^ c1) = 0. [para(213(a,1),328(a,1,2,2))]. given #187 (T,wt=10): 1944 (x v c2)' ^ (y ^ c1) = 0. [para(216(a,1),328(a,1,2,2))]. given #188 (T,wt=10): 1965 c2 != 1 | c2 != 0 | c2' = c2. [para(248(a,1),74(a,1)),rewrite(248(12)),flip(b)]. given #189 (T,wt=10): 1969 c2' ^ (x ^ (c1 ^ y)) = 0. [para(1936(a,1),5(a,1,1)),rewrite(88(2),5(6)),flip(a)]. given #190 (A,wt=13): 102 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #191 (T,wt=10): 2019 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),449(a,1,1))]. given #192 (T,wt=10): 2089 x v (c2 v (c1 v x)') = 1. [para(2(a,1),453(a,1,2,2,1))]. given #193 (T,wt=10): 2108 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),601(a,1,1))]. given #194 (T,wt=10): 2109 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),601(a,1,2,1)),rewrite(2(4))]. given #195 (A,wt=13): 103 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite(3(3))]. given #196 (T,wt=10): 2112 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),601(a,1,2,1)),rewrite(2(4))]. given #197 (T,wt=10): 2124 c2 v (x v (c1 v x)') = 1. [para(2(a,1),603(a,1,2,2,1))]. given #198 (T,wt=10): 2127 c2 v (c1 v (c2 ^ x))' = 1. [para(603(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #199 (T,wt=10): 2177 c1 ^ (c2 ^ (x v c1))' = 0. [para(91(a,1),282(a,1))]. given #200 (A,wt=19): 104 (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 #201 (T,wt=10): 2194 c1' v (c2 ^ (c1 v x)) = 1. [para(1294(a,1),2(a,1)),flip(a)]. given #202 (T,wt=7): 2733 c1 != 0 | c1' = 1. [para(2194(a,1),55(b,1,2)),rewrite(13(9),319(9),4(6),75(6),2(5),191(5),2(3),85(3),4(6),75(6),13(16),319(16),4(13),75(13),2(12),191(12)),xx(a)]. given #203 (T,wt=10): 2206 c1' v (c2 ^ (x v c1)) = 1. [para(1298(a,1),2(a,1)),flip(a)]. given #204 (T,wt=10): 2587 c2' ^ (c1 v (c2 ^ x)) = 0. [para(2109(a,1),4(a,1)),flip(a)]. given #205 (A,wt=17): 105 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #206 (T,wt=10): 2648 c2' ^ (c1 v (x ^ c2)) = 0. [para(2112(a,1),4(a,1)),flip(a)]. given #207 (T,wt=10): 2670 c2 v (c1 v (x ^ c2))' = 1. [para(4(a,1),2127(a,1,2,1,2))]. given #208 (T,wt=11): 110 x v ((y ^ x) v z) = x v z. [para(26(a,1),3(a,1,1)),flip(a)]. given #209 (T,wt=11): 115 x v (y v (z ^ x)) = y v x. [para(26(a,1),17(a,1,2)),flip(a)]. given #210 (A,wt=19): 107 (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 #211 (T,wt=11): 123 (x v c1) ^ (x v c2) = x v c1. [para(114(a,1),21(a,1,2,2))]. given #212 (T,wt=11): 160 c1 v c2' != 1 | c2' = c1'. [para(158(a,1),10(b,1)),flip(c),xx(b)]. given #213 (T,wt=11): 197 c2 ^ c1' != 0 | c2' = c1'. [para(191(a,1),10(a,1)),xx(a)]. given #214 (T,wt=11): 217 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(59(a,1),26(a,1,2)),rewrite(2(5))]. given #215 (A,wt=15): 108 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #216 (T,wt=11): 218 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #217 (T,wt=11): 225 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(213(a,1),19(a,1,2)),flip(a)]. given #218 (T,wt=11): 236 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(216(a,1),5(a,1,1)),flip(a)]. given #219 (T,wt=11): 238 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(216(a,1),19(a,1,2)),flip(a)]. given #220 (A,wt=17): 109 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #221 (T,wt=11): 250 c2 v ((x ^ c1) v y) = c2 v y. [para(60(a,1),24(a,1,2,1))]. given #222 (T,wt=11): 253 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(60(a,1),27(a,1,2))]. given #223 (T,wt=11): 262 c2 v (x v (y ^ c1)) = x v c2. [para(248(a,1),17(a,1,2)),flip(a)]. given #224 (T,wt=11): 263 c2 v ((c1 ^ x) v y) = c2 v y. [para(260(a,1),3(a,1,1)),flip(a)]. given #225 (A,wt=13): 111 x v (y v (z ^ (x v y))) = x v y. [para(26(a,1),3(a,1)),flip(a)]. given #226 (T,wt=11): 265 c2 v (x v (c1 ^ y)) = x v c2. [para(260(a,1),17(a,1,2)),flip(a)]. given #227 (T,wt=11): 284 x ^ (y v (z v (x v u))) = x. [para(3(a,1),62(a,1,2))]. given #228 (T,wt=11): 292 (x v y) ^ (z ^ x) = z ^ x. [para(68(a,1),22(a,2)),rewrite(291(4))]. given #229 (T,wt=11): 293 (x ^ y) v (y ^ x) = x ^ y. [para(68(a,1),27(a,1,2))]. given #230 (A,wt=14): 113 1 != x | y ^ x != 0 | x' = y ^ x. [para(26(a,1),10(a,1)),rewrite(68(4)),flip(a)]. given #231 (T,wt=10): 3436 (x ^ y) v (y ^ x)' = 1. [para(293(a,1),319(a,1,2)),rewrite(2(4))]. given #232 (T,wt=11): 335 (x v y) ^ (y v x) = x v y. [para(73(a,1),21(a,1,2))]. given #233 (T,wt=10): 3500 (x v y) ^ (y v x)' = 0. [para(335(a,1),320(a,1,2)),rewrite(4(4))]. given #234 (T,wt=11): 336 (x ^ y) v (z v x) = z v x. [para(73(a,1),24(a,2)),rewrite(334(4))]. given #235 (A,wt=13): 116 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(19(a,1),26(a,1,2))]. given #236 (T,wt=11): 347 x v y != 0 | (x v y)' = 1. [para(32(a,1),37(b,1)),rewrite(96(2),96(2)),xx(a)]. given #237 (T,wt=11): 348 x v y != 1 | (x v y)' = 0. [para(35(a,1),37(a,1,2)),rewrite(4(6),88(6)),xx(b)]. given #238 (T,wt=7): 3619 c2 != 1 | c2' = 0. [para(114(a,1),348(a,1)),rewrite(114(6))]. given #239 (T,wt=11): 385 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),80(a,1,2))]. given #240 (A,wt=22): 119 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [back_rewrite(106),rewrite(117(4))]. given #241 (T,wt=11): 392 (x ^ c1) v (x ^ c2) = x ^ c2. [para(83(a,1),26(a,1,2)),rewrite(2(5))]. given #242 (T,wt=11): 395 x ^ (y v (z v (u v x))) = x. [para(3(a,1),90(a,1,2,2))]. given #243 (T,wt=11): 407 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),112(a,1,2,2))]. given #244 (T,wt=11): 462 (c1 v x) ^ (x v c2) = c1 v x. [para(122(a,1),21(a,1,2))]. given #245 (A,wt=17): 124 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(22(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #246 (T,wt=11): 465 c1 ^ (x v (y v (c2 v z))) = c1. [para(3(a,1),224(a,1,2))]. given #247 (T,wt=11): 476 x ^ y != 0 | (x ^ y)' = 1. [para(32(a,1),39(b,1,2)),rewrite(2(3),85(3)),xx(a)]. given #248 (T,wt=11): 477 x ^ y != 1 | (x ^ y)' = 0. [para(35(a,1),39(a,1)),rewrite(99(5),99(5)),xx(b)]. given #249 (T,wt=11): 523 c1 ^ (x v (y v (z v c2))) = c1. [para(3(a,1),235(a,1,2,2))]. given #250 (A,wt=22): 126 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(22(a,1),10(b,1))]. given #251 (T,wt=11): 530 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(5(a,1),261(a,1,2,2))]. given #252 (T,wt=11): 536 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(5(a,1),266(a,1,2))]. given #253 (T,wt=11): 600 (x v c1) ^ (c2 v x) = x v c1. [para(446(a,1),20(a,1,2))]. given #254 (T,wt=11): 2157 (x v y) ^ (z ^ y) = z ^ y. [para(68(a,1),91(a,2)),rewrite(291(4))]. given #255 (A,wt=13): 127 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),22(a,1,2,1))]. given #256 (T,wt=11): 2297 (x ^ y)' != 0 | x ^ y = 1. [para(172(a,1),93(a,1)),rewrite(298(10),172(11)),flip(b),xx(a)]. given #257 (T,wt=11): 2384 (c1 v x) ^ (c2 v x) = c1 v x. [para(120(a,1),94(a,1,2))]. given #258 (T,wt=11): 2429 (x v y)' != 1 | x v y = 0. [para(1934(a,1),70(b,1)),rewrite(298(10),1934(12)),flip(a),xx(b)]. given #259 (T,wt=11): 2838 (x ^ y) v (z v y) = z v y. [para(73(a,1),110(a,2)),rewrite(334(4))]. given #260 (A,wt=15): 128 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(22(a,1),19(a,1,2)),flip(a)]. given #261 (T,wt=11): 3010 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),217(a,1,1))]. given #262 (T,wt=11): 3011 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),217(a,1,2))]. given #263 (T,wt=11): 3083 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(68(a,1),218(a,2)),rewrite(291(7))]. given #264 (T,wt=11): 3133 (x v c2) ^ (y ^ c1) = y ^ c1. [para(68(a,1),236(a,2)),rewrite(291(7))]. given #265 (A,wt=15): 129 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(22(a,1),26(a,1,2)),rewrite(2(4))]. given #266 (T,wt=11): 3211 (x ^ c1) v (y v c2) = y v c2. [para(73(a,1),250(a,2)),rewrite(334(7))]. given #267 (T,wt=11): 3301 (c1 ^ x) v (y v c2) = y v c2. [para(73(a,1),263(a,2)),rewrite(334(7))]. given #268 (T,wt=11): 3615 x v y != 0 | (y v x)' = 1. [para(2(a,1),347(a,1))]. given #269 (T,wt=11): 3617 x v y != 1 | (y v x)' = 0. [para(2(a,1),348(a,1))]. given #270 (A,wt=12): 131 x v (y v ((x v y)' v z)) = 1. [para(86(a,1),3(a,1)),flip(a)]. given #271 (T,wt=11): 3766 (x v c2) ^ (c1 v x) = c1 v x. [para(462(a,1),4(a,1)),flip(a)]. given #272 (T,wt=11): 3870 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),476(a,1))]. given #273 (T,wt=11): 3874 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),477(a,1))]. given #274 (T,wt=11): 3990 (c2 v x) ^ (x v c1) = x v c1. [para(600(a,1),4(a,1)),flip(a)]. given #275 (A,wt=15): 132 x ^ (x' v y) != 0 | x' v y = x'. [para(86(a,1),10(a,1)),flip(c),xx(a)]. given #276 (T,wt=11): 4112 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),2297(a,1,1))]. given #277 (T,wt=11): 4114 (x v y)' != 0 | x v y = 1. [para(21(a,1),2297(a,1,1)),rewrite(21(8))]. given #278 (T,wt=7): 4503 c2' != 0 | c2 = 1. [para(114(a,1),4114(a,1,1)),rewrite(114(7))]. given #279 (T,wt=11): 4135 (x v y)' != 1 | y v x = 0. [para(2(a,1),2429(a,1,1))]. given #280 (A,wt=12): 134 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(89(a,1),5(a,1)),flip(a)]. given #281 (T,wt=11): 4137 (x ^ y)' != 1 | x ^ y = 0. [para(27(a,1),2429(a,1,1)),rewrite(27(8))]. given #282 (T,wt=7): 4528 c1' != 1 | c1 = 0. [para(13(a,1),4137(a,1,1)),rewrite(13(7))]. given #283 (T,wt=11): 4255 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(3011(a,1),2(a,1)),flip(a)]. given #284 (T,wt=11): 4501 (x v y)' != 0 | y v x = 1. [para(335(a,1),4112(a,1,1)),rewrite(335(7))]. given #285 (A,wt=15): 135 x v (x' ^ y) != 1 | x' ^ y = x'. [para(89(a,1),10(b,1)),flip(c),xx(b)]. given #286 (T,wt=11): 4506 (x ^ y)' != 1 | y ^ x = 0. [para(293(a,1),4135(a,1,1)),rewrite(293(7))]. given #287 (T,wt=12): 138 x v (y v (z v (x v y)')) = 1. [para(98(a,1),3(a,1)),flip(a)]. given #288 (T,wt=12): 141 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(100(a,1),5(a,1)),flip(a)]. given #289 (T,wt=12): 154 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),125(a,1,2,1))]. given #290 (A,wt=15): 140 x ^ (y v x') != 0 | y v x' = x'. [para(98(a,1),10(a,1)),flip(c),xx(a)]. given #291 (T,wt=12): 155 x ^ (y ^ ((x ^ y) v z)') = 0. [para(125(a,1),5(a,1)),flip(a)]. given #292 (T,wt=12): 164 x ^ (y ^ (z v (x ^ y))') = 0. [para(153(a,1),5(a,1)),flip(a)]. given #293 (T,wt=12): 166 (x v y) ^ (x v (z v y))' = 0. [para(17(a,1),153(a,1,2,1))]. given #294 (T,wt=12): 179 ((x ^ y) v z) ^ (x v z)' = 0. [para(24(a,1),153(a,1,2,1))]. given #295 (A,wt=15): 143 x v (y ^ x') != 1 | y ^ x' = x'. [para(100(a,1),10(b,1)),flip(c),xx(b)]. given #296 (T,wt=12): 182 x v (y v ((x v y) ^ z)') = 1. [para(172(a,1),3(a,1)),flip(a)]. given #297 (T,wt=12): 184 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),172(a,1,2,1))]. given #298 (T,wt=12): 188 x v (y v (z ^ (x v y))') = 1. [para(183(a,1),3(a,1)),flip(a)]. given #299 (T,wt=12): 193 (x ^ y) v (x ^ (z ^ y))' = 1. [para(19(a,1),183(a,1,2,1))]. given #300 (A,wt=13): 145 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),23(a,1,2,2,1))]. given #301 (T,wt=12): 194 ((x v y) ^ z) v (x ^ z)' = 1. [para(22(a,1),183(a,1,2,1))]. given #302 (T,wt=12): 257 x v (y v (z v (x v z)')) = 1. [para(31(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #303 (T,wt=12): 259 x v (y v ((x ^ z) v y)') = 1. [para(31(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #304 (T,wt=12): 279 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(34(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #305 (A,wt=19): 146 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 #306 (T,wt=12): 281 x ^ (y ^ ((x v z) ^ y)') = 0. [para(34(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #307 (T,wt=12): 324 x v ((x v y)' v (z v y)) = 1. [para(17(a,1),319(a,1,2)),rewrite(17(5))]. given #308 (T,wt=12): 330 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(19(a,1),320(a,1,2)),rewrite(19(5))]. given #309 (T,wt=12): 715 x v (y v (z v (x' v u))) = 1. [para(3(a,1),133(a,1,2))]. given #310 (A,wt=26): 147 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 #311 (T,wt=12): 717 x v (y v ((x ^ z)' v u)) = 1. [para(133(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #312 (T,wt=12): 724 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),136(a,1,2))]. given #313 (T,wt=12): 726 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(136(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #314 (T,wt=12): 735 x ^ ((y v (x v z))' ^ u) = 0. [para(17(a,1),137(a,1,2,1,1))]. given #315 (A,wt=15): 148 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(17(a,1),23(a,1,2,2))]. given #316 (T,wt=12): 741 x v (y v (z v (u v x'))) = 1. [para(3(a,1),139(a,1,2,2))]. given #317 (T,wt=12): 743 x v (y v (z v (x ^ u)')) = 1. [para(139(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #318 (T,wt=12): 804 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),142(a,1,2,2))]. given #319 (T,wt=12): 806 x ^ (y ^ (z ^ (x v u)')) = 0. [para(142(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #320 (A,wt=17): 149 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(23(a,1),19(a,1,2)),flip(a)]. given #321 (T,wt=12): 816 x ^ (y ^ (z v (x v u))') = 0. [para(17(a,1),144(a,1,2,2,1))]. given #322 (T,wt=12): 824 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),157(a,1,2,1))]. given #323 (T,wt=12): 832 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),162(a,1,2,1,2))]. given #324 (T,wt=12): 833 x ^ ((y v (z v x))' ^ u) = 0. [para(162(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #325 (A,wt=19): 150 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 #326 (T,wt=12): 837 x ^ (y ^ (z v (u v x))') = 0. [para(162(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #327 (T,wt=12): 845 (x v c1) ^ (y v (c2 v x))' = 0. [para(446(a,1),162(a,1,2,1,2))]. given #328 (T,wt=12): 887 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(163(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #329 (T,wt=12): 894 (x v c1) ^ ((c2 v x)' ^ y) = 0. [para(446(a,1),163(a,1,2,1,1))]. given #330 (A,wt=19): 151 (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 #331 (T,wt=12): 896 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),167(a,1,2))]. given #332 (T,wt=12): 906 (x v c1) ^ (y ^ (c2 v x)') = 0. [para(446(a,1),167(a,1,2,2,1))]. given #333 (T,wt=12): 908 c1 ^ (x ^ (y ^ (c2' ^ z))) = 0. [para(5(a,1),169(a,1,2))]. given #334 (T,wt=12): 918 x v ((y ^ (x ^ z))' v u) = 1. [para(19(a,1),177(a,1,2,1,1))]. given #335 (A,wt=15): 152 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(23(a,1),22(a,1,2)),rewrite(22(3)),flip(a)]. given #336 (T,wt=11): 6131 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(152(a,1),59(a,1)),rewrite(13(3),4(6)),flip(a)]. given #337 (T,wt=11): 6204 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),6131(a,1,2,1,2))]. given #338 (T,wt=11): 6205 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(2(a,1),6131(a,1,2))]. given #339 (T,wt=11): 6242 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),6204(a,1,2))]. given #340 (A,wt=15): 156 x v (x v y)' != 1 | (x v y)' = x'. [para(125(a,1),10(b,1)),flip(c),xx(b)]. given #341 (T,wt=12): 1036 x v (y v (z ^ (x ^ u))') = 1. [para(19(a,1),178(a,1,2,2,1))]. given #342 (T,wt=12): 1045 c1 ^ (x ^ (y ^ (z ^ c2'))) = 0. [para(5(a,1),180(a,1,2,2))]. given #343 (T,wt=12): 1054 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),186(a,1,2,1))]. given #344 (T,wt=12): 1063 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),187(a,1,2,1,1))]. given #345 (A,wt=15): 165 x v (y v x)' != 1 | (y v x)' = x'. [para(153(a,1),10(b,1)),flip(c),xx(b)]. given #346 (T,wt=12): 1065 x v (y v ((z ^ x)' v u)) = 1. [para(187(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #347 (T,wt=12): 1069 (c2 ^ x) v ((c1 ^ x)' v y) = 1. [para(59(a,1),187(a,1,2,1,1))]. given #348 (T,wt=12): 1072 (x ^ c2) v ((x ^ c1)' v y) = 1. [para(83(a,1),187(a,1,2,1,1))]. given #349 (T,wt=12): 1199 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),189(a,1,2,1,2))]. given #350 (A,wt=15): 168 c1 v (c2' ^ x) != 1 | c2' ^ x = c1'. [para(159(a,1),10(b,1)),flip(c),xx(b)]. given #351 (T,wt=12): 1201 x v (y v (z ^ (u ^ x))') = 1. [para(189(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #352 (T,wt=12): 1206 (c2 ^ x) v (y ^ (c1 ^ x))' = 1. [para(59(a,1),189(a,1,2,1,2))]. given #353 (T,wt=12): 1209 (x ^ c2) v (y ^ (x ^ c1))' = 1. [para(83(a,1),189(a,1,2,1,2))]. given #354 (T,wt=12): 1220 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),192(a,1,2))]. given #355 (A,wt=17): 170 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 #356 (T,wt=12): 1225 (c2 ^ x) v (y v (c1 ^ x)') = 1. [para(59(a,1),192(a,1,2,2,1))]. given #357 (T,wt=12): 1229 (x ^ c2) v (y v (x ^ c1)') = 1. [para(83(a,1),192(a,1,2,2,1))]. given #358 (T,wt=12): 1241 c2 v (x v (y v (c1' v z))) = 1. [para(3(a,1),209(a,1,2))]. given #359 (T,wt=12): 1251 c2 v (x v (y v (z v c1'))) = 1. [para(3(a,1),210(a,1,2,2))]. given #360 (A,wt=17): 171 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),24(a,1,2,1))]. given #361 (T,wt=12): 1301 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(62(a,1),222(a,1,2,1))]. given #362 (T,wt=12): 1304 (c2 ^ (x v (y v c1))) v c1' = 1. [para(90(a,1),222(a,1,2,1))]. given #363 (T,wt=12): 1317 c1 ^ ((x v (c2 v y))' ^ z) = 0. [para(17(a,1),239(a,1,2,1,1))]. given #364 (T,wt=12): 1318 c1 ^ (x ^ ((c2 v y)' ^ z)) = 0. [para(239(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #365 (A,wt=22): 173 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(24(a,1),10(a,1))]. given #366 (T,wt=12): 1324 c1 ^ (x v (y v (c2 v z)))' = 0. [para(3(a,1),241(a,1,2,1))]. given #367 (T,wt=12): 1326 c1 ^ (x ^ (y v (c2 v z))') = 0. [para(241(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #368 (T,wt=12): 1332 c1 ^ (x ^ (y ^ (c2 v z)')) = 0. [para(5(a,1),242(a,1,2))]. given #369 (T,wt=12): 1543 c1 ^ (x v (y v (z v c2)))' = 0. [para(3(a,1),243(a,1,2,1,2))]. given #370 (A,wt=15): 174 x v (y v ((x ^ z) v u)) = y v (x v u). [para(24(a,1),17(a,1,2)),flip(a)]. given #371 (T,wt=12): 1544 c1 ^ ((x v (y v c2))' ^ z) = 0. [para(243(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #372 (T,wt=12): 1546 c1 ^ (x ^ (y v (z v c2))') = 0. [para(243(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #373 (T,wt=12): 1553 c1 ^ (x ^ ((y v c2)' ^ z)) = 0. [para(244(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #374 (T,wt=12): 1559 c1 ^ (x ^ (y ^ (z v c2)')) = 0. [para(5(a,1),246(a,1,2))]. given #375 (A,wt=13): 175 x v ((y ^ (x ^ z)) v u) = x v u. [para(19(a,1),24(a,1,2,1))]. given #376 (T,wt=12): 1567 x v (y v ((y v x)' v z)) = 1. [para(254(a,1),3(a,1,1)),rewrite(85(2),3(5)),flip(a)]. given #377 (T,wt=12): 1571 x v (y v (z v (z v x)')) = 1. [para(254(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #378 (T,wt=12): 1573 x v (y v (y v (x ^ z))') = 1. [para(254(a,1),24(a,1,2)),rewrite(96(2)),flip(a)]. given #379 (T,wt=12): 1702 c2 v ((x ^ (y ^ c1))' v z) = 1. [para(5(a,1),267(a,1,2,1,1))]. given #380 (A,wt=15): 176 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(24(a,1),20(a,1,2)),rewrite(4(4))]. given #381 (T,wt=12): 1704 c2 v (x v ((y ^ c1)' v z)) = 1. [para(267(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #382 (T,wt=12): 1715 c2 v (x ^ (y ^ (z ^ c1)))' = 1. [para(5(a,1),269(a,1,2,1,2))]. given #383 (T,wt=12): 1717 c2 v (x v (y ^ (z ^ c1))') = 1. [para(269(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #384 (T,wt=12): 1724 c2 v (x v (y v (z ^ c1)')) = 1. [para(3(a,1),271(a,1,2))]. given #385 (A,wt=15): 181 c1 v (x ^ c2') != 1 | x ^ c2' = c1'. [para(161(a,1),10(b,1)),flip(c),xx(b)]. given #386 (T,wt=12): 1735 c2 v (x v ((c1 ^ y)' v z)) = 1. [para(272(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #387 (T,wt=12): 1736 c2 v ((x ^ (c1 ^ y))' v z) = 1. [para(19(a,1),272(a,1,2,1,1))]. given #388 (T,wt=12): 1751 (x v (y ^ z)) ^ (x v y)' = 0. [para(63(a,1),153(a,1,2,1))]. given #389 (T,wt=12): 1753 x v (y v (x v (y ^ z))') = 1. [para(63(a,1),319(a,1,2)),rewrite(2(5),3(5))]. given #390 (A,wt=15): 185 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(172(a,1),10(a,1)),flip(c),xx(a)]. given #391 (T,wt=12): 1766 c2 v (x v (y v (c1 ^ z)')) = 1. [para(3(a,1),274(a,1,2))]. given #392 (T,wt=12): 1768 c2 v (x v (y ^ (c1 ^ z))') = 1. [para(19(a,1),274(a,1,2,2,1))]. given #393 (T,wt=12): 1777 c2 v (x ^ (y ^ (c1 ^ z)))' = 1. [para(5(a,1),275(a,1,2,1))]. given #394 (T,wt=12): 1785 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(276(a,1),5(a,1,1)),rewrite(88(2),5(5)),flip(a)]. given #395 (A,wt=15): 190 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(183(a,1),10(a,1)),flip(c),xx(a)]. given #396 (T,wt=12): 1789 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(276(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #397 (T,wt=12): 1791 x ^ (y ^ (y ^ (x v z))') = 0. [para(276(a,1),22(a,1,2)),rewrite(99(2)),flip(a)]. given #398 (T,wt=12): 1799 c1 ^ (x ^ ((c2 ^ x)' ^ y)) = 0. [para(282(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #399 (T,wt=12): 1802 c1 ^ (x ^ (y ^ (c2 ^ y)')) = 0. [para(282(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #400 (A,wt=14): 195 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(23(a,1),183(a,1,2,1))]. given #401 (T,wt=12): 1867 x' v (y v (z v (x v u))) = 1. [para(3(a,1),321(a,1,2))]. given #402 (T,wt=12): 1888 x' v (y v (z v (u v x))) = 1. [para(3(a,1),322(a,1,2,2))]. given #403 (T,wt=12): 1900 (x ^ (y ^ z))' v (u v y) = 1. [para(80(a,1),322(a,1,2,2))]. given #404 (T,wt=12): 1901 (x ^ (y ^ z))' v (u v z) = 1. [para(112(a,1),322(a,1,2,2))]. given #405 (A,wt=13): 199 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),25(a,1,2,2,1))]. given #406 (T,wt=12): 1903 (x ^ (y ^ c1))' v (z v c2) = 1. [para(261(a,1),322(a,1,2,2))]. given #407 (T,wt=12): 1904 (x ^ (c1 ^ y))' v (z v c2) = 1. [para(266(a,1),322(a,1,2,2))]. given #408 (T,wt=12): 1906 (x v c1)' v (y v (c2 v x)) = 1. [para(446(a,1),322(a,1,2,2))]. given #409 (T,wt=12): 1923 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),327(a,1,2))]. given #410 (A,wt=19): 200 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 #411 (T,wt=12): 1933 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),328(a,1,2,2))]. given #412 (T,wt=12): 1942 (c2 ^ x)' ^ (y ^ (c1 ^ x)) = 0. [para(59(a,1),328(a,1,2,2))]. given #413 (T,wt=12): 1945 (x v (y v z))' ^ (u ^ y) = 0. [para(62(a,1),328(a,1,2,2))]. given #414 (T,wt=12): 1947 (x ^ c2)' ^ (y ^ (x ^ c1)) = 0. [para(83(a,1),328(a,1,2,2))]. given #415 (A,wt=26): 201 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 #416 (T,wt=12): 1948 (x v (y v z))' ^ (u ^ z) = 0. [para(90(a,1),328(a,1,2,2))]. given #417 (T,wt=12): 1950 (x v (c2 v y))' ^ (z ^ c1) = 0. [para(224(a,1),328(a,1,2,2))]. given #418 (T,wt=12): 1953 (x v (y v c2))' ^ (z ^ c1) = 0. [para(235(a,1),328(a,1,2,2))]. given #419 (T,wt=12): 1980 (x ^ (y v z)) v (x ^ y)' = 1. [para(79(a,1),183(a,1,2,1))]. given #420 (A,wt=17): 202 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 #421 (T,wt=12): 1981 x ^ (y ^ (x ^ (y v z))') = 0. [para(79(a,1),320(a,1,2)),rewrite(4(5),5(5))]. given #422 (T,wt=12): 2005 x ^ (c1 ^ ((x ^ c2)' ^ y)) = 0. [para(394(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #423 (T,wt=12): 2007 c1 ^ (x ^ (y ^ (y ^ c2)')) = 0. [para(394(a,1),5(a,2,2)),rewrite(19(7),5(6),99(9))]. given #424 (T,wt=12): 2010 x ^ (y ^ (c1 ^ (x ^ c2)')) = 0. [para(394(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #425 (A,wt=19): 203 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 #426 (T,wt=12): 2011 x ^ (c1 ^ (c2 ^ (x v y))') = 0. [para(394(a,1),22(a,1,2)),rewrite(99(2),4(5)),flip(a)]. given #427 (T,wt=12): 2022 (x v c1) ^ ((x v c2)' ^ y) = 0. [para(449(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #428 (T,wt=12): 2024 (x v c1) ^ (y ^ (x v c2)') = 0. [para(449(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #429 (T,wt=12): 2090 x v (c2 v ((x v c1)' v y)) = 1. [para(453(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #430 (A,wt=15): 204 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(19(a,1),25(a,1,2,2))]. given #431 (T,wt=12): 2092 c2 v (x v (y v (y v c1)')) = 1. [para(453(a,1),3(a,2,2)),rewrite(17(7),3(6),96(9))]. given #432 (T,wt=12): 2095 x v (y v (c2 v (x v c1)')) = 1. [para(453(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #433 (T,wt=12): 2096 x v (c2 v (c1 v (x ^ y))') = 1. [para(453(a,1),24(a,1,2)),rewrite(96(2),2(5)),flip(a)]. given #434 (T,wt=12): 2115 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0. [para(80(a,1),601(a,1,2,1)),rewrite(2(5))]. given #435 (A,wt=19): 205 (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 #436 (T,wt=12): 2116 (c1 v (x ^ (y ^ c2))) ^ c2' = 0. [para(112(a,1),601(a,1,2,1)),rewrite(2(5))]. given #437 (T,wt=12): 2125 c2 v (x v ((x v c1)' v y)) = 1. [para(603(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #438 (T,wt=12): 2137 (x ^ c2) v ((c1 ^ x)' v y) = 1. [para(1292(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #439 (T,wt=12): 2139 (x ^ c2) v (y v (c1 ^ x)') = 1. [para(1292(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #440 (A,wt=14): 206 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(25(a,1),153(a,1,2,1))]. given #441 (T,wt=12): 2154 ((x v y) ^ z) v (y ^ z)' = 1. [para(91(a,1),183(a,1,2,1))]. given #442 (T,wt=12): 2156 x ^ (y ^ ((z v x) ^ y)') = 0. [para(34(a,1),91(a,1,2)),rewrite(99(2)),flip(a)]. given #443 (T,wt=12): 2176 x ^ (y ^ (y ^ (z v x))') = 0. [para(276(a,1),91(a,1,2)),rewrite(99(2)),flip(a)]. given #444 (T,wt=12): 2179 x ^ (c1 ^ (c2 ^ (y v x))') = 0. [para(394(a,1),91(a,1,2)),rewrite(99(2),4(5)),flip(a)]. given #445 (A,wt=15): 207 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 #446 (T,wt=12): 2184 (c2 ^ x) v ((x ^ c1)' v y) = 1. [para(1293(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #447 (T,wt=12): 2186 (c2 ^ x) v (y v (x ^ c1)') = 1. [para(1293(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #448 (T,wt=12): 2195 (c2 ^ (c1 v x)) v (c1' v y) = 1. [para(1294(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #449 (T,wt=12): 2197 (c2 ^ (c1 v x)) v (y v c1') = 1. [para(1294(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #450 (A,wt=15): 208 c2 ^ (c1' v x) != 0 | c2' = c1' v x. [para(196(a,1),10(a,1)),xx(a)]. given #451 (T,wt=12): 2207 (c2 ^ (x v c1)) v (c1' v y) = 1. [para(1298(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #452 (T,wt=12): 2209 (c2 ^ (x v c1)) v (y v c1') = 1. [para(1298(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #453 (T,wt=12): 2218 c1 ^ (x ^ ((x ^ c2)' ^ y)) = 0. [para(1792(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #454 (T,wt=12): 2254 x ^ (c1 ^ ((c2 ^ x)' ^ y)) = 0. [para(1803(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #455 (A,wt=15): 211 c2 ^ (x v c1') != 0 | c2' = x v c1'. [para(198(a,1),10(a,1)),xx(a)]. given #456 (T,wt=12): 2255 x ^ (y ^ (c1 ^ (c2 ^ x)')) = 0. [para(1803(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #457 (T,wt=12): 2263 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0. [para(1805(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #458 (T,wt=12): 2265 c1 ^ (c2 ^ (x v (c1 v y)))' = 0. [para(17(a,1),1805(a,1,2,1,2))]. given #459 (T,wt=12): 2266 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0. [para(1805(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #460 (A,wt=13): 212 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(59(a,1),5(a,2,2)),rewrite(19(5),5(4))]. given #461 (T,wt=12): 2273 c1' v (x v (y v (c2 v z))) = 1. [para(3(a,1),1874(a,1,2))]. given #462 (T,wt=12): 2284 c1' v (x v (y v (z v c2))) = 1. [para(3(a,1),1875(a,1,2,2))]. given #463 (T,wt=12): 2302 (x ^ y)' v (z v (x v u)) = 1. [para(1889(a,1),3(a,1,1)),rewrite(85(2),3(5)),flip(a)]. given #464 (T,wt=12): 2303 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),1889(a,1,2))]. given #465 (A,wt=18): 214 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1' = c2 ^ x. [para(59(a,1),10(b,1))]. given #466 (T,wt=12): 2311 c2 v (x v ((x v c1) ^ y)') = 1. [para(446(a,1),1889(a,1,2)),rewrite(2(7),3(7))]. given #467 (T,wt=12): 2318 (x ^ y)' v (z v (y v u)) = 1. [para(1891(a,1),3(a,1,1)),rewrite(85(2),3(5)),flip(a)]. given #468 (T,wt=12): 2319 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),1891(a,1,2))]. given #469 (T,wt=12): 2327 (c1 ^ x)' v (y v (c2 ^ x)) = 1. [para(59(a,1),1891(a,1,1,1))]. given #470 (A,wt=13): 215 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(59(a,1),19(a,1,2)),flip(a)]. given #471 (T,wt=12): 2329 (x ^ c1)' v (y v (x ^ c2)) = 1. [para(83(a,1),1891(a,1,1,1))]. given #472 (T,wt=12): 2333 c2 v (x v (y ^ (x v c1))') = 1. [para(446(a,1),1891(a,1,2)),rewrite(2(7),3(7))]. given #473 (T,wt=12): 2347 (x ^ c1)' v (y v (c2 v z)) = 1. [para(1895(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #474 (T,wt=12): 2348 (x ^ c1)' v (y v (z v c2)) = 1. [para(3(a,1),1895(a,1,2))]. given #475 (A,wt=13): 219 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(23(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #476 (T,wt=12): 2357 (c1 ^ x)' v (y v (c2 v z)) = 1. [para(1896(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #477 (T,wt=12): 2358 (c1 ^ x)' v (y v (z v c2)) = 1. [para(3(a,1),1896(a,1,2))]. given #478 (T,wt=12): 2401 c2' ^ (x ^ (y ^ (c1 ^ z))) = 0. [para(1925(a,1),5(a,1,1)),rewrite(88(2),5(7),5(6)),flip(a)]. given #479 (T,wt=12): 2402 c2' ^ (x ^ (y ^ (z ^ c1))) = 0. [para(5(a,1),1925(a,1,2,2))]. given #480 (A,wt=14): 223 c2 v x != 1 | c1 != 0 | c1' = c2 v x. [para(213(a,1),10(b,1)),rewrite(120(4))]. given #481 (T,wt=12): 2411 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(1934(a,1),5(a,1,1)),rewrite(88(2),5(5)),flip(a)]. given #482 (T,wt=12): 2412 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),1934(a,1,2))]. given #483 (T,wt=12): 2417 c1 ^ (x ^ ((c2 ^ x) v y)') = 0. [para(59(a,1),1934(a,1,2)),rewrite(4(7),5(7))]. given #484 (T,wt=12): 2419 x ^ (c1 ^ ((x ^ c2) v y)') = 0. [para(83(a,1),1934(a,1,2)),rewrite(4(7),5(7))]. given #485 (A,wt=13): 226 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),27(a,1,1))]. given #486 (T,wt=12): 2435 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(1938(a,1),5(a,1,1)),rewrite(88(2),5(5)),flip(a)]. given #487 (T,wt=12): 2436 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),1938(a,1,2))]. given #488 (T,wt=12): 2443 c1 ^ (x ^ (y v (c2 ^ x))') = 0. [para(59(a,1),1938(a,1,2)),rewrite(4(7),5(7))]. given #489 (T,wt=12): 2445 x ^ (c1 ^ (y v (x ^ c2))') = 0. [para(83(a,1),1938(a,1,2)),rewrite(4(7),5(7))]. given #490 (A,wt=13): 227 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),27(a,1,2)),rewrite(5(3))]. given #491 (T,wt=12): 2449 (c2 v x)' ^ (y ^ (x v c1)) = 0. [para(446(a,1),1938(a,1,1,1))]. given #492 (T,wt=12): 2464 (x ^ (y v z)) v (x ^ z)' = 1. [para(95(a,1),183(a,1,2,1))]. given #493 (T,wt=12): 2467 x ^ (y ^ (x ^ (z v y))') = 0. [para(95(a,1),320(a,1,2)),rewrite(4(5),5(5))]. given #494 (T,wt=12): 2490 (c2 v x)' ^ (y ^ (c1 ^ z)) = 0. [para(1943(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #495 (A,wt=19): 228 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),27(a,1,1)),rewrite(5(5),5(8))]. Low Water (keep, True_semantics): wt=74 given #496 (T,wt=12): 2491 (c2 v x)' ^ (y ^ (z ^ c1)) = 0. [para(5(a,1),1943(a,1,2))]. given #497 (T,wt=12): 2499 (x v c2)' ^ (y ^ (c1 ^ z)) = 0. [para(1944(a,1),5(a,1,1)),rewrite(88(2),5(7)),flip(a)]. given #498 (T,wt=12): 2500 (x v c2)' ^ (y ^ (z ^ c1)) = 0. [para(5(a,1),1944(a,1,2))]. given #499 (T,wt=12): 2536 x v (y v (z v (y v x)')) = 1. [para(102(a,1),178(a,1,2,2,1)),rewrite(3(5))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 86 (0.00 of 4.20 sec). given #500 (A,wt=17): 230 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(27(a,1),17(a,1,2)),flip(a)]. Low Water (keep, True_semantics): wt=64 given #501 (T,wt=12): 2537 x v (y v (z ^ (y v x))') = 1. [para(102(a,1),186(a,1,2,1,2)),rewrite(3(5))]. given #502 (T,wt=12): 2543 (x v y)' ^ (z ^ (y v x)) = 0. [para(102(a,1),327(a,1,2,2))]. given #503 (T,wt=12): 2545 c1' v ((c2 ^ (c1 v x)) v y) = 1. [para(1294(a,1),102(a,1,1)),rewrite(75(10),2194(15))]. given #504 (T,wt=12): 2546 c1' v ((c2 ^ (x v c1)) v y) = 1. [para(1298(a,1),102(a,1,1)),rewrite(75(10),2206(15))]. given #505 (A,wt=19): 231 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(19(a,1),27(a,1,1)),rewrite(5(4))]. Low Water (keep, True_semantics): wt=56 given #506 (T,wt=12): 2547 (x v y)' v (z v (y v x)) = 1. [para(102(a,1),1889(a,1,1,1))]. given #507 (T,wt=12): 2550 (c1 v x) ^ ((x v c2)' ^ y) = 0. [para(2019(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. Low Water (keep, True_semantics): wt=55 given #508 (T,wt=12): 2553 (c1 v x) ^ (y ^ (x v c2)') = 0. [para(2019(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #509 (T,wt=12): 2561 x v (c2 v ((c1 v x)' v y)) = 1. [para(2089(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #510 (A,wt=15): 232 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(19(a,1),27(a,1,2,2))]. given #511 (T,wt=12): 2562 c2 v (x v (y v (c1 v y)')) = 1. [para(2089(a,1),3(a,2,2)),rewrite(17(7),3(6),96(9))]. given #512 (T,wt=12): 2564 x v (y v (c2 v (c1 v x)')) = 1. [para(2089(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #513 (T,wt=12): 2578 (c1 v x) ^ ((c2 v x)' ^ y) = 0. [para(2108(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #514 (T,wt=12): 2580 (c1 v x) ^ (y ^ (c2 v x)') = 0. [para(2108(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #515 (A,wt=22): 234 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [back_rewrite(229),rewrite(233(7))]. given #516 (T,wt=12): 2588 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0. [para(2109(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #517 (T,wt=12): 2590 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0. [para(2109(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #518 (T,wt=12): 2613 x v ((y v x)' v (z v y)) = 1. [para(31(a,1),103(a,1,1)),rewrite(3(6),75(7),31(9))]. given #519 (T,wt=12): 2617 (x v y) ^ (y v (z v x))' = 0. [para(103(a,1),320(a,1,2)),rewrite(4(5))]. given #520 (A,wt=14): 237 x v c2 != 1 | c1 != 0 | c1' = x v c2. [para(216(a,1),10(b,1)),rewrite(122(4))]. given #521 (T,wt=12): 2638 c2 v ((x v c1)' v (y v x)) = 1. [para(453(a,1),103(a,1,1)),rewrite(3(8),75(9),453(13))]. Low Water (keep, True_semantics): wt=50 given #522 (T,wt=12): 2639 x v ((x v c1)' v (y v c2)) = 1. [para(603(a,1),103(a,1,1)),rewrite(3(8),75(9),603(13))]. given #523 (T,wt=12): 2640 (c1 ^ x)' v (y v (x ^ c2)) = 1. [para(1292(a,1),103(a,1,1)),rewrite(75(9),1292(13))]. given #524 (T,wt=12): 2641 (x ^ c1)' v (y v (c2 ^ x)) = 1. [para(1293(a,1),103(a,1,1)),rewrite(75(9),1293(13))]. given #525 (A,wt=15): 240 c1 v (c2 v x)' != 1 | (c2 v x)' = c1'. [para(220(a,1),10(b,1)),flip(c),xx(b)]. given #526 (T,wt=12): 2642 c1' v (x v (c2 ^ (c1 v y))) = 1. [para(1294(a,1),103(a,1,1)),rewrite(75(10),1294(15))]. given #527 (T,wt=12): 2643 c1' v (x v (c2 ^ (y v c1))) = 1. [para(1298(a,1),103(a,1,1)),rewrite(75(10),1298(15))]. given #528 (T,wt=12): 2647 c2 v ((c1 v x)' v (y v x)) = 1. [para(2089(a,1),103(a,1,1)),rewrite(3(8),75(9),2089(13))]. given #529 (T,wt=12): 2649 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0. [para(2112(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #530 (A,wt=15): 245 c1 v (x v c2)' != 1 | (x v c2)' = c1'. [para(221(a,1),10(b,1)),flip(c),xx(b)]. given #531 (T,wt=12): 2651 (c1 v (x ^ c2)) ^ (y ^ c2') = 0. [para(2112(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #532 (T,wt=12): 2659 c2 v (x v ((c1 v x)' v y)) = 1. [para(2124(a,1),3(a,1,1)),rewrite(85(2),3(7)),flip(a)]. given #533 (T,wt=12): 2668 x v ((c1 v x)' v (y v c2)) = 1. [para(2124(a,1),103(a,1,1)),rewrite(3(8),75(9),2124(13))]. given #534 (T,wt=12): 2669 c2 v ((c1 v (c2 ^ x))' v y) = 1. [para(2127(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #535 (A,wt=13): 247 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(5(a,1),60(a,1,2)),rewrite(4(8))]. given #536 (T,wt=12): 2672 c2 v (x v (c1 v (c2 ^ y))') = 1. [para(2127(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #537 (T,wt=12): 2673 c2 v (c1 v (x ^ (c2 ^ y)))' = 1. [para(19(a,1),2127(a,1,2,1,2))]. given #538 (T,wt=12): 2683 (c1 v (c2 ^ x))' v (y v c2) = 1. [para(2127(a,1),103(a,1,1)),rewrite(75(10),2127(15))]. given #539 (T,wt=12): 2684 c1 ^ (c2 ^ (x v (y v c1)))' = 0. [para(3(a,1),2177(a,1,2,1,2))]. given #540 (A,wt=14): 249 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1. [para(60(a,1),10(b,1)),rewrite(248(4))]. given #541 (T,wt=12): 2685 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0. [para(2177(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #542 (T,wt=12): 2687 c1 ^ (x ^ (c2 ^ (y v c1))') = 0. [para(2177(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #543 (T,wt=12): 2725 c1' v (c2 ^ (x v (c1 v y))) = 1. [para(17(a,1),2194(a,1,2,2))]. given #544 (T,wt=12): 2735 c1' v (c2 ^ (x v (y v c1))) = 1. [para(3(a,1),2206(a,1,2,2))]. given #545 (A,wt=13): 252 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(60(a,1),27(a,1,2,2))]. given #546 (T,wt=12): 2744 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(2587(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #547 (T,wt=12): 2745 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(2587(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #548 (T,wt=12): 2746 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(19(a,1),2587(a,1,2,2))]. given #549 (T,wt=12): 2799 (c1 v x) ^ (c2 v (x v y))' = 0. [para(2019(a,1),105(a,1,2)),rewrite(4(4),88(4),2(6)),flip(a)]. given #550 (A,wt=14): 255 x v (y v (z v (x v (y v z))')) = 1. [para(31(a,1),3(a,1)),rewrite(3(3)),flip(a)]. Low Water (keep, True_semantics): wt=47 given #551 (T,wt=12): 2800 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(2648(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #552 (T,wt=12): 2801 c2' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(5(a,1),2648(a,1,2,2))]. given #553 (T,wt=12): 2802 c2' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(2648(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #554 (T,wt=12): 2812 c2 v ((c1 v (x ^ c2))' v y) = 1. [para(2670(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #555 (A,wt=19): 256 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 #556 (T,wt=12): 2813 c2 v (c1 v (x ^ (y ^ c2)))' = 1. [para(5(a,1),2670(a,1,2,1,2))]. given #557 (T,wt=12): 2815 c2 v (x v (c1 v (y ^ c2))') = 1. [para(2670(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #558 (T,wt=12): 2825 (c1 v (x ^ c2))' v (y v c2) = 1. [para(2670(a,1),103(a,1,1)),rewrite(75(10),2670(15))]. given #559 (T,wt=12): 2833 ((x ^ y) v z) ^ (y v z)' = 0. [para(110(a,1),153(a,1,2,1))]. given #560 (A,wt=14): 258 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 #561 (T,wt=12): 2836 x v (y v ((z ^ x) v y)') = 1. [para(31(a,1),110(a,1,2)),rewrite(96(2)),flip(a)]. given #562 (T,wt=12): 2861 x v (y v (y v (z ^ x))') = 1. [para(254(a,1),110(a,1,2)),rewrite(96(2)),flip(a)]. given #563 (T,wt=12): 2865 x v (c2 v (c1 v (y ^ x))') = 1. [para(453(a,1),110(a,1,2)),rewrite(96(2),2(5)),flip(a)]. Low Water (keep, True_semantics): wt=41 given #564 (T,wt=12): 2890 (x v (y ^ z)) ^ (x v z)' = 0. [para(115(a,1),153(a,1,2,1))]. given #565 (A,wt=14): 264 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x. [para(260(a,1),10(a,1)),rewrite(19(7),59(7))]. given #566 (T,wt=12): 2893 x v (y v (x v (z ^ y))') = 1. [para(115(a,1),319(a,1,2)),rewrite(2(5),3(5))]. given #567 (T,wt=12): 3003 x v (c2 v (y ^ (x v c1))') = 1. [para(123(a,1),189(a,1,2,1,2)),rewrite(3(7))]. given #568 (T,wt=12): 3004 x v (c2 v (y v (x v c1)')) = 1. [para(123(a,1),192(a,1,2,2,1)),rewrite(3(7))]. given #569 (T,wt=12): 3005 (x v c2)' ^ (y ^ (x v c1)) = 0. [para(123(a,1),328(a,1,2,2))]. given #570 (A,wt=15): 270 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'. [para(251(a,1),10(a,1)),flip(c),xx(a)]. given #571 (T,wt=12): 3007 (x v c1)' v (y v (x v c2)) = 1. [para(123(a,1),1891(a,1,1,1))]. given #572 (T,wt=12): 3008 (x v c1) ^ (x v (c2 v y))' = 0. [para(123(a,1),1934(a,1,2)),rewrite(3(3),4(7))]. given #573 (T,wt=12): 3009 (x v c1) ^ (y v (x v c2))' = 0. [para(123(a,1),1938(a,1,2)),rewrite(4(7))]. given #574 (T,wt=12): 3028 c1 ^ (x ^ (y ^ (c2 ^ x)')) = 0. [para(217(a,1),144(a,1,2,2,1)),rewrite(5(7))]. given #575 (A,wt=15): 273 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'. [para(268(a,1),10(a,1)),flip(c),xx(a)]. given #576 (T,wt=12): 3081 ((c2 v x) ^ y) v (c1 ^ y)' = 1. [para(218(a,1),183(a,1,2,1))]. Low Water (keep, True_semantics): wt=39 given #577 (T,wt=12): 3082 c1 ^ (x ^ ((c2 v y) ^ x)') = 0. [para(34(a,1),218(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #578 (T,wt=12): 3096 c1 ^ (x ^ (x ^ (c2 v y))') = 0. [para(276(a,1),218(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #579 (T,wt=12): 3108 (x ^ (c2 v y)) v (x ^ c1)' = 1. [para(225(a,1),183(a,1,2,1))]. Low Water (keep, True_semantics): wt=36 given #580 (A,wt=14): 277 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(34(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #581 (T,wt=12): 3109 x ^ (c1 ^ (x ^ (c2 v y))') = 0. [para(225(a,1),320(a,1,2)),rewrite(4(7),5(7))]. given #582 (T,wt=12): 3131 ((x v c2) ^ y) v (c1 ^ y)' = 1. [para(236(a,1),183(a,1,2,1))]. given #583 (T,wt=12): 3132 c1 ^ (x ^ ((y v c2) ^ x)') = 0. [para(34(a,1),236(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #584 (T,wt=12): 3147 c1 ^ (x ^ (x ^ (y v c2))') = 0. [para(276(a,1),236(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #585 (A,wt=19): 278 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(34(a,1),10(b,1)),flip(c),xx(b)]. Low Water (keep, True_semantics): wt=35 given #586 (T,wt=12): 3159 (x ^ (y v c2)) v (x ^ c1)' = 1. [para(238(a,1),183(a,1,2,1))]. given #587 (T,wt=12): 3160 x ^ (c1 ^ (x ^ (y v c2))') = 0. [para(238(a,1),320(a,1,2)),rewrite(4(7),5(7))]. given #588 (T,wt=12): 3207 ((x ^ c1) v y) ^ (c2 v y)' = 0. [para(250(a,1),153(a,1,2,1))]. given #589 (T,wt=12): 3209 c2 v (x v ((y ^ c1) v x)') = 1. [para(31(a,1),250(a,1,2)),rewrite(2(3),85(3)),flip(a)]. given #590 (A,wt=14): 280 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(19(a,1),34(a,1,2,2,1)),rewrite(5(5))]. given #591 (T,wt=12): 3225 c2 v (x v (x v (y ^ c1))') = 1. [para(254(a,1),250(a,1,2)),rewrite(2(3),85(3)),flip(a)]. given #592 (T,wt=12): 3249 x ^ (c1 ^ (y v (c2 ^ x))') = 0. [para(253(a,1),162(a,1,2,1,2)),rewrite(5(7))]. given #593 (T,wt=12): 3251 x ^ (c1 ^ (y ^ (c2 ^ x)')) = 0. [para(253(a,1),167(a,1,2,2,1)),rewrite(5(7))]. given #594 (T,wt=12): 3260 (c2 ^ x) v (x ^ (c1 ^ y))' = 1. [para(253(a,1),1889(a,1,2)),rewrite(5(3),2(7))]. given #595 (A,wt=15): 283 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),62(a,1,2,2))]. Low Water (keep, True_semantics): wt=34 given #596 (T,wt=12): 3261 (c2 ^ x) v (y ^ (x ^ c1))' = 1. [para(253(a,1),1891(a,1,2)),rewrite(2(7))]. given #597 (T,wt=12): 3263 (c2 ^ x)' ^ (y ^ (x ^ c1)) = 0. [para(253(a,1),1938(a,1,1,1))]. given #598 (T,wt=12): 3268 (x v (y ^ c1)) ^ (x v c2)' = 0. [para(262(a,1),153(a,1,2,1))]. given #599 (T,wt=12): 3270 x v (c2 v (x v (y ^ c1))') = 1. [para(262(a,1),319(a,1,2)),rewrite(2(7),3(7))]. given #600 (A,wt=13): 286 x ^ (y ^ (z v (x v u))) = y ^ x. [para(62(a,1),19(a,1,2)),flip(a)]. given #601 (T,wt=12): 3297 ((c1 ^ x) v y) ^ (c2 v y)' = 0. [para(263(a,1),153(a,1,2,1))]. given #602 (T,wt=12): 3299 c2 v (x v ((c1 ^ y) v x)') = 1. [para(31(a,1),263(a,1,2)),rewrite(2(3),85(3)),flip(a)]. given #603 (T,wt=12): 3315 c2 v (x v (x v (c1 ^ y))') = 1. [para(254(a,1),263(a,1,2)),rewrite(2(3),85(3)),flip(a)]. given #604 (T,wt=12): 3364 (x v (c1 ^ y)) ^ (x v c2)' = 0. [para(265(a,1),153(a,1,2,1))]. given #605 (A,wt=13): 287 x v (y v (x v z)) = y v (x v z). [para(62(a,1),26(a,1,2)),rewrite(2(3))]. given #606 (T,wt=12): 3366 x v (c2 v (x v (c1 ^ y))') = 1. [para(265(a,1),319(a,1,2)),rewrite(2(7),3(7))]. given #607 (T,wt=12): 3440 x ^ (y ^ (z v (y ^ x))') = 0. [para(293(a,1),162(a,1,2,1,2)),rewrite(5(5))]. Low Water (keep, True_semantics): wt=33 given #608 (T,wt=12): 3441 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(293(a,1),167(a,1,2,2,1)),rewrite(5(5))]. given #609 (T,wt=12): 3454 (x ^ y)' v (z v (y ^ x)) = 1. [para(293(a,1),322(a,1,2,2))]. given #610 (A,wt=18): 288 x v (y v z) != 1 | 0 != y | y' = x v (y v z). [back_rewrite(285),rewrite(287(3))]. given #611 (T,wt=12): 3455 (x ^ y) v (y ^ (x ^ z))' = 1. [para(293(a,1),1889(a,1,2)),rewrite(5(2),2(5))]. given #612 (T,wt=12): 3456 (x ^ y) v (z ^ (y ^ x))' = 1. [para(293(a,1),1891(a,1,2)),rewrite(2(5))]. given #613 (T,wt=12): 3458 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(293(a,1),1938(a,1,1,1))]. given #614 (T,wt=12): 3484 (x ^ y) v ((y ^ x)' v z) = 1. [para(3436(a,1),3(a,1,1)),rewrite(85(2)),flip(a)]. given #615 (A,wt=13): 289 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(66(a,1),5(a,2,2)),rewrite(19(3),5(2))]. given #616 (T,wt=12): 3487 (x ^ y) v (z v (y ^ x)') = 1. [para(3436(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #617 (T,wt=12): 3505 (x v y) ^ (y v (x v z))' = 0. [para(335(a,1),1934(a,1,2)),rewrite(3(2),4(5))]. given #618 (T,wt=12): 3506 (x v y) ^ (z v (y v x))' = 0. [para(335(a,1),1938(a,1,2)),rewrite(4(5))]. given #619 (T,wt=12): 3509 (x v y) ^ ((y v x)' ^ z) = 0. [para(3500(a,1),5(a,1,1)),rewrite(88(2)),flip(a)]. given #620 (A,wt=13): 291 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),68(a,1,2)),rewrite(5(5))]. given #621 (T,wt=12): 3511 (x v y) ^ (z ^ (y v x)') = 0. [para(3500(a,1),19(a,1,2)),rewrite(99(2)),flip(a)]. given #622 (T,wt=12): 3665 x ^ (c1 ^ (y ^ (x ^ c2)')) = 0. [para(392(a,1),144(a,1,2,2,1)),rewrite(5(7))]. given #623 (T,wt=12): 3775 x v (c2 v (y ^ (c1 v x))') = 1. [para(462(a,1),189(a,1,2,1,2)),rewrite(3(7))]. given #624 (T,wt=12): 3776 x v (c2 v (y v (c1 v x)')) = 1. [para(462(a,1),192(a,1,2,2,1)),rewrite(3(7))]. given #625 (A,wt=20): 294 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, True_semantics): wt=32 given #626 (T,wt=12): 3777 (x v c2)' ^ (y ^ (c1 v x)) = 0. [para(462(a,1),328(a,1,2,2))]. given #627 (T,wt=12): 3780 (c1 v x)' v (y v (x v c2)) = 1. [para(462(a,1),1891(a,1,1,1))]. Low Water (keep, True_semantics): wt=31 given #628 (T,wt=12): 3781 (c1 v x) ^ (x v (c2 v y))' = 0. [para(462(a,1),1934(a,1,2)),rewrite(3(3),4(7))]. given #629 (T,wt=12): 3782 (c1 v x) ^ (y v (x v c2))' = 0. [para(462(a,1),1938(a,1,2)),rewrite(4(7))]. given #630 (A,wt=14): 295 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),36(b,1))]. given #631 (T,wt=12): 4003 c2 v (x v (y v (x v c1)')) = 1. [para(600(a,1),192(a,1,2,2,1)),rewrite(3(7))]. given #632 (T,wt=12): 4007 (x v c1) ^ (c2 v (x v y))' = 0. [para(600(a,1),1934(a,1,2)),rewrite(3(3),4(7))]. given #633 (T,wt=12): 4125 c2 v (x v (y ^ (c1 v x))') = 1. [para(2384(a,1),189(a,1,2,1,2)),rewrite(3(7))]. given #634 (T,wt=12): 4126 c2 v (x v (y v (c1 v x)')) = 1. [para(2384(a,1),192(a,1,2,2,1)),rewrite(3(7))]. given #635 (A,wt=20): 296 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),36(b,1))]. given #636 (T,wt=12): 4127 (c2 v x)' ^ (y ^ (c1 v x)) = 0. [para(2384(a,1),328(a,1,2,2))]. given #637 (T,wt=12): 4129 (c1 v x)' v (y v (c2 v x)) = 1. [para(2384(a,1),1891(a,1,1,1))]. given #638 (T,wt=12): 4130 (c1 v x) ^ (y v (c2 v x))' = 0. [para(2384(a,1),1938(a,1,2)),rewrite(4(7))]. given #639 (T,wt=12): 4211 x ^ (y ^ ((y v z) ^ x)') = 0. [para(276(a,1),128(a,1,2)),rewrite(99(2)),flip(a)]. given #640 (A,wt=14): 297 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),36(a,1)),rewrite(4(4),66(4)),flip(a)]. given #641 (T,wt=12): 4213 c1 ^ (x ^ (c2 ^ (x v y))') = 0. [para(282(a,1),128(a,1,2)),rewrite(99(2)),flip(a)]. given #642 (T,wt=12): 4551 (c2 ^ x) v (c1 ^ (x ^ y))' = 1. [para(4255(a,1),1889(a,1,2)),rewrite(5(3),2(7))]. Low Water (keep, True_semantics): wt=30 given #643 (T,wt=12): 4616 (x v c1) ^ (x v (y v c2))' = 0. [para(122(a,1),154(a,1,2,1,2))]. given #644 (T,wt=12): 4623 ((x ^ y) v z) ^ (z v x)' = 0. [para(336(a,1),154(a,1,2,1))]. given #645 (A,wt=20): 299 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(17(a,1),36(a,1))]. given #646 (T,wt=12): 4626 ((x ^ y) v z) ^ (z v y)' = 0. [para(2838(a,1),154(a,1,2,1))]. Low Water (keep, True_semantics): wt=28 given #647 (T,wt=12): 4631 ((x ^ c1) v y) ^ (y v c2)' = 0. [para(3211(a,1),154(a,1,2,1))]. given #648 (T,wt=12): 4633 ((c1 ^ x) v y) ^ (y v c2)' = 0. [para(3301(a,1),154(a,1,2,1))]. given #649 (T,wt=12): 4637 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),155(a,1,2,2,1,1))]. given #650 (A,wt=20): 300 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(19(a,1),36(b,1))]. given #651 (T,wt=12): 4703 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),179(a,1,1))]. given #652 (T,wt=12): 4705 (x v y)' ^ ((x ^ z) v y) = 0. [para(179(a,1),4(a,1)),flip(a)]. Low Water (keep, True_semantics): wt=27 given #653 (T,wt=12): 4707 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),179(a,1,2,1))]. given #654 (T,wt=12): 4712 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(26(a,1),179(a,1,2,1))]. given #655 (A,wt=14): 301 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(26(a,1),36(a,1)),rewrite(4(4),68(4)),flip(a)]. given #656 (T,wt=12): 4716 ((c2 ^ x) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),179(a,1,2,1))]. given #657 (T,wt=12): 4717 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(260(a,1),179(a,1,2,1))]. given #658 (T,wt=12): 4755 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),182(a,1,2,2,1,1))]. given #659 (T,wt=12): 4770 c2 v (x v ((c1 v x) ^ y)') = 1. [para(182(a,1),2089(a,1,2,2,1)),rewrite(84(8),2(8),77(8),2(7))]. given #660 (A,wt=15): 303 x ^ (x' v y) != 0 | (x' v y)' = x. [para(86(a,1),36(a,1)),rewrite(4(6)),xx(a)]. given #661 (T,wt=12): 4775 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),184(a,1,2,1)),rewrite(5(3))]. given #662 (T,wt=12): 4778 (x ^ c2) v (x ^ (y ^ c1))' = 1. [para(60(a,1),184(a,1,2,1,2))]. given #663 (T,wt=12): 4791 ((x v y) ^ z) v (z ^ x)' = 1. [para(292(a,1),184(a,1,2,1))]. given #664 (T,wt=12): 4793 ((x v y) ^ z) v (z ^ y)' = 1. [para(2157(a,1),184(a,1,2,1))]. given #665 (A,wt=15): 304 x ^ (y v x') != 0 | (y v x')' = x. [para(98(a,1),36(a,1)),rewrite(4(6)),xx(a)]. given #666 (T,wt=12): 4795 ((c2 v x) ^ y) v (y ^ c1)' = 1. [para(3083(a,1),184(a,1,2,1))]. given #667 (T,wt=12): 4797 ((x v c2) ^ y) v (y ^ c1)' = 1. [para(3133(a,1),184(a,1,2,1))]. given #668 (T,wt=12): 4920 (x ^ y)' v ((x v z) ^ y) = 1. [para(194(a,1),2(a,1)),flip(a)]. given #669 (T,wt=12): 4921 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),194(a,1,1))]. given #670 (A,wt=22): 305 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 #671 (T,wt=12): 4922 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),194(a,1,2,1))]. given #672 (T,wt=12): 4926 ((x v y) ^ (z v x)) v x' = 1. [para(20(a,1),194(a,1,2,1))]. given #673 (T,wt=12): 4930 ((c1 v x) ^ (c2 v y)) v c1' = 1. [para(213(a,1),194(a,1,2,1))]. given #674 (T,wt=12): 4931 ((c1 v x) ^ (y v c2)) v c1' = 1. [para(216(a,1),194(a,1,2,1))]. given #675 (A,wt=13): 306 x ^ (x ^ y)' != 0 | x ^ y = x. [para(172(a,1),36(a,1)),rewrite(4(6),298(11)),xx(a)]. given #676 (T,wt=12): 5012 x v (y v ((y ^ z) v x)') = 1. [para(259(a,1),17(a,1)),flip(a)]. given #677 (T,wt=12): 5015 x v ((x ^ y) v (x ^ z))' = 1. [para(259(a,1),24(a,1)),flip(a)]. given #678 (T,wt=12): 5029 x v ((x ^ y) v (z ^ x))' = 1. [para(259(a,1),110(a,1)),flip(a)]. given #679 (T,wt=12): 5035 c2 v ((c2 ^ x) v (y ^ c1))' = 1. [para(259(a,1),250(a,1)),flip(a)]. given #680 (A,wt=13): 307 x ^ (y ^ x)' != 0 | y ^ x = x. [para(183(a,1),36(a,1)),rewrite(4(6),298(11)),xx(a)]. given #681 (T,wt=12): 5036 c2 v ((c2 ^ x) v (c1 ^ y))' = 1. [para(259(a,1),263(a,1)),flip(a)]. given #682 (T,wt=12): 5132 x ^ ((x v y) ^ (x v z))' = 0. [para(281(a,1),22(a,1)),flip(a)]. given #683 (T,wt=12): 5147 x ^ ((x v y) ^ (z v x))' = 0. [para(281(a,1),91(a,1)),flip(a)]. given #684 (T,wt=12): 5149 c1 ^ ((c1 v x) ^ (c2 v y))' = 0. [para(281(a,1),218(a,1)),flip(a)]. given #685 (A,wt=26): 309 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 #686 (T,wt=12): 5151 c1 ^ ((c1 v x) ^ (y v c2))' = 0. [para(281(a,1),236(a,1)),flip(a)]. given #687 (T,wt=12): 5213 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),330(a,1,2,1,1))]. given #688 (T,wt=12): 5222 c1 ^ ((c2 ^ x)' ^ (y ^ x)) = 0. [para(330(a,1),59(a,1,2)),rewrite(4(3),88(3)),flip(a)]. given #689 (T,wt=12): 5892 (c1 v (c2 ^ x)) ^ (y v c2)' = 0. [para(7(a,1),845(a,1,2,1,2)),rewrite(2(4))]. given #690 (A,wt=15): 310 c2 ^ (c1' v x) != 0 | (c1' v x)' = c2. [para(196(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #691 (T,wt=12): 5895 (x v c1) ^ (c2 v (y v x))' = 0. [para(17(a,1),845(a,1,2,1))]. given #692 (T,wt=12): 5896 (c1 v (x ^ c2)) ^ (y v c2)' = 0. [para(26(a,1),845(a,1,2,1,2)),rewrite(2(4))]. given #693 (T,wt=12): 5908 (c1 v (x ^ y)) ^ (c2 v x)' = 0. [para(63(a,1),845(a,1,2,1)),rewrite(2(3))]. given #694 (T,wt=12): 5912 (c1 v (x ^ y)) ^ (c2 v y)' = 0. [para(115(a,1),845(a,1,2,1)),rewrite(2(3))]. given #695 (A,wt=15): 311 c2 ^ (x v c1') != 0 | (x v c1')' = c2. [para(198(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #696 (T,wt=12): 6213 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(6131(a,1),320(a,1,2)),rewrite(4(8))]. given #697 (T,wt=12): 6250 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(6204(a,1),320(a,1,2)),rewrite(4(8))]. given #698 (T,wt=12): 6286 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(6205(a,1),320(a,1,2)),rewrite(4(8))]. given #699 (T,wt=12): 6320 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(6242(a,1),320(a,1,2)),rewrite(4(8))]. given #700 (A,wt=22): 312 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),289(6),66(6))]. given #701 (T,wt=12): 6695 (x ^ c2) v (y ^ (c1 ^ x))' = 1. [para(4(a,1),1206(a,1,1))]. given #702 (T,wt=12): 6696 (c2 ^ (c1 v x)) v (y ^ c1)' = 1. [para(6(a,1),1206(a,1,2,1,2))]. given #703 (T,wt=12): 6700 (c2 ^ x) v (c1 ^ (y ^ x))' = 1. [para(19(a,1),1206(a,1,2,1))]. given #704 (T,wt=12): 6701 (c2 ^ (x v c1)) v (y ^ c1)' = 1. [para(20(a,1),1206(a,1,2,1,2))]. given #705 (A,wt=19): 313 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 #706 (T,wt=12): 6722 (c2 ^ (x v y)) v (c1 ^ x)' = 1. [para(79(a,1),1206(a,1,2,1))]. given #707 (T,wt=12): 6727 (c2 ^ (x v y)) v (c1 ^ y)' = 1. [para(95(a,1),1206(a,1,2,1))]. given #708 (T,wt=12): 6755 (x ^ c2) v (x ^ (c1 ^ y))' = 1. [para(4(a,1),1209(a,1,2,1)),rewrite(5(5))]. Low Water (keep, True_semantics): wt=26 given #709 (T,wt=12): 6759 (c2 ^ (x v y)) v (x ^ c1)' = 1. [para(22(a,1),1209(a,1,2,1)),rewrite(4(3))]. given #710 (A,wt=14): 314 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2. [para(248(a,1),36(a,1)),rewrite(4(7),60(7))]. given #711 (T,wt=12): 6767 (c2 ^ (x v y)) v (y ^ c1)' = 1. [para(91(a,1),1209(a,1,2,1)),rewrite(4(3))]. given #712 (T,wt=12): 7235 c2 v (x v (c1 v (x ^ y))') = 1. [para(603(a,1),174(a,1,2)),rewrite(96(2),2(5)),flip(a)]. given #713 (T,wt=12): 7400 x v (y v ((z ^ y) v x)') = 1. [para(2838(a,1),1567(a,1,2)),rewrite(2(4))]. given #714 (T,wt=12): 7401 x v (c2 v ((y ^ c1) v x)') = 1. [para(3211(a,1),1567(a,1,2)),rewrite(2(6))]. given #715 (A,wt=14): 315 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2. [para(260(a,1),36(a,1)),rewrite(4(7),19(7),59(7))]. given #716 (T,wt=12): 7402 x v (c2 v ((c1 ^ y) v x)') = 1. [para(3301(a,1),1567(a,1,2)),rewrite(2(6))]. given #717 (T,wt=12): 7449 x v ((y ^ x) v (x ^ z))' = 1. [para(1573(a,1),110(a,1)),flip(a)]. given #718 (T,wt=12): 7453 c2 v ((x ^ c1) v (c2 ^ y))' = 1. [para(1573(a,1),250(a,1)),flip(a)]. given #719 (T,wt=12): 7454 c2 v ((c1 ^ x) v (c2 ^ y))' = 1. [para(1573(a,1),263(a,1)),flip(a)]. given #720 (A,wt=13): 316 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2. [para(251(a,1),36(a,1)),rewrite(4(8),298(14)),xx(a)]. given #721 (T,wt=12): 7620 (x v y)' ^ (x v (y ^ z)) = 0. [para(1751(a,1),4(a,1)),flip(a)]. given #722 (T,wt=12): 7741 x ^ (y ^ ((z v y) ^ x)') = 0. [para(2157(a,1),1785(a,1,2)),rewrite(4(4))]. given #723 (T,wt=12): 7743 x ^ (c1 ^ ((c2 v y) ^ x)') = 0. [para(3083(a,1),1785(a,1,2)),rewrite(4(6))]. given #724 (T,wt=12): 7744 x ^ (c1 ^ ((y v c2) ^ x)') = 0. [para(3133(a,1),1785(a,1,2)),rewrite(4(6))]. given #725 (A,wt=13): 317 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2. [para(268(a,1),36(a,1)),rewrite(4(8),298(14)),xx(a)]. given #726 (T,wt=12): 7802 x ^ ((c2 ^ x)' ^ (y ^ c1)) = 0. [para(282(a,1),1789(a,1,2,2,2,1)),rewrite(87(7),4(7),75(7),5(7))]. given #727 (T,wt=12): 7803 c1 ^ ((x ^ c2)' ^ (y ^ x)) = 0. [para(394(a,1),1789(a,1,2,2,2,1)),rewrite(87(7),32(7),5(7))]. given #728 (T,wt=12): 7806 x ^ ((x ^ c2)' ^ (y ^ c1)) = 0. [para(1792(a,1),1789(a,1,2,2,2,1)),rewrite(87(7),4(7),75(7),5(7))]. given #729 (T,wt=12): 7807 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0. [para(1805(a,1),1789(a,1,2,2,2,1)),rewrite(87(8),4(8),75(8))]. given #730 (A,wt=14): 318 x v y != 1 | 0 != x | (x v y)' = x. [para(71(a,1),36(a,1)),rewrite(4(5),6(5)),flip(b)]. given #731 (T,wt=12): 7808 (c2 ^ (x v c1))' ^ (y ^ c1) = 0. [para(2177(a,1),1789(a,1,2,2,2,1)),rewrite(87(8),4(8),75(8))]. given #732 (T,wt=12): 7846 x ^ ((y v x) ^ (x v z))' = 0. [para(1791(a,1),91(a,1)),flip(a)]. given #733 (T,wt=12): 7848 c1 ^ ((c2 v x) ^ (c1 v y))' = 0. [para(1791(a,1),218(a,1)),flip(a)]. given #734 (T,wt=12): 7850 c1 ^ ((x v c2) ^ (c1 v y))' = 0. [para(1791(a,1),236(a,1)),flip(a)]. given #735 (A,wt=13): 323 x' ^ (y v x) != 0 | y v x = x. [para(319(a,1),10(a,1)),rewrite(298(10)),flip(c),xx(a)]. given #736 (T,wt=12): 7876 c1 ^ (x ^ (c2 ^ (y v x))') = 0. [para(2157(a,1),1799(a,1,2)),rewrite(4(6))]. given #737 (T,wt=12): 7921 ((x v y) ^ (y v z)) v y' = 1. [para(20(a,1),195(a,1,1,2,1)),rewrite(20(5))]. given #738 (T,wt=12): 7923 ((c2 v x) ^ (c1 v y)) v c1' = 1. [para(213(a,1),195(a,1,1,2,1)),rewrite(213(9))]. given #739 (T,wt=12): 7924 ((x v c2) ^ (c1 v y)) v c1' = 1. [para(216(a,1),195(a,1,1,2,1)),rewrite(216(9))]. given #740 (A,wt=14): 325 x v (y v (y v ((x v y) ^ z))') = 1. [para(25(a,1),319(a,1,2)),rewrite(2(6),3(6))]. given #741 (T,wt=12): 7960 (x ^ (y v z)) v (z ^ x)' = 1. [para(336(a,1),195(a,1,1,2))]. given #742 (T,wt=12): 7970 (x ^ (y v c2)) v (c1 ^ x)' = 1. [para(3301(a,1),195(a,1,1,2))]. Low Water (keep, True_semantics): wt=25 given #743 (T,wt=12): 8271 c2 v (x v (c1 v (y ^ x))') = 1. [para(115(a,1),1906(a,1,2)),rewrite(2(3),2(7),3(7))]. given #744 (T,wt=12): 8446 (x ^ c2)' ^ (y ^ (c1 ^ x)) = 0. [para(4(a,1),1942(a,1,1,1))]. given #745 (A,wt=15): 326 (x v y) ^ y' != 0 | (x v y)' = y'. [para(319(a,1),36(a,1)),xx(a)]. given #746 (T,wt=12): 8756 (x ^ y)' v (x ^ (y v z)) = 1. [para(1980(a,1),2(a,1)),flip(a)]. given #747 (T,wt=12): 8935 c1 ^ (x ^ (y ^ (x ^ c2)')) = 0. [para(19(a,1),2007(a,1,2))]. given #748 (T,wt=12): 9406 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(26(a,1),206(a,1,1,2,1)),rewrite(26(5))]. given #749 (T,wt=12): 9408 ((x ^ c1) v (c2 ^ y)) ^ c2' = 0. [para(248(a,1),206(a,1,1,2,1)),rewrite(248(9))]. given #750 (A,wt=13): 329 x' v (y ^ x) != 1 | y ^ x = x. [para(320(a,1),10(b,1)),rewrite(298(10)),flip(c),xx(b)]. given #751 (T,wt=12): 9409 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0. [para(260(a,1),206(a,1,1,2,1)),rewrite(260(9))]. given #752 (T,wt=12): 9430 (x v (y ^ z)) ^ (z v x)' = 0. [para(292(a,1),206(a,1,1,2))]. given #753 (T,wt=12): 9436 (x v (y ^ c1)) ^ (c2 v x)' = 0. [para(3083(a,1),206(a,1,1,2))]. given #754 (T,wt=12): 9449 (x ^ y)' v ((z v x) ^ y) = 1. [para(2154(a,1),2(a,1)),flip(a)]. given #755 (A,wt=14): 331 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(23(a,1),320(a,1,2)),rewrite(4(6),5(6))]. given #756 (T,wt=12): 9455 ((x v y) ^ (z v y)) v y' = 1. [para(20(a,1),2154(a,1,2,1))]. given #757 (T,wt=12): 9460 ((x v c1) ^ (c2 v y)) v c1' = 1. [para(213(a,1),2154(a,1,2,1))]. Low Water (keep, True_semantics): wt=24 given #758 (T,wt=12): 9461 ((x v c1) ^ (y v c2)) v c1' = 1. [para(216(a,1),2154(a,1,2,1))]. given #759 (T,wt=12): 9571 x ^ ((y v x) ^ (z v x))' = 0. [para(2156(a,1),91(a,1)),flip(a)]. given #760 (A,wt=13): 332 (x ^ y) v y' != 1 | x ^ y = y. [para(320(a,1),36(b,1)),rewrite(298(10)),flip(c),xx(b)]. given #761 (T,wt=12): 9576 c1 ^ ((x v c1) ^ (c2 v y))' = 0. [para(2156(a,1),218(a,1)),flip(a)]. given #762 (T,wt=12): 9578 c1 ^ ((x v c1) ^ (y v c2))' = 0. [para(2156(a,1),236(a,1)),flip(a)]. given #763 (T,wt=12): 9629 c1 ^ ((c2 v x) ^ (y v c1))' = 0. [para(2176(a,1),218(a,1)),flip(a)]. given #764 (T,wt=12): 9631 c1 ^ ((x v c2) ^ (y v c1))' = 0. [para(2176(a,1),236(a,1)),flip(a)]. given #765 (A,wt=13): 334 x v (y v (z v x)) = y v (z v x). [para(3(a,1),73(a,1,2)),rewrite(3(5))]. given #766 (T,wt=12): 10082 x v (c2 v ((x v c1) ^ y)') = 1. [para(2311(a,1),17(a,1)),flip(a)]. given #767 (T,wt=12): 10083 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1. [para(2311(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #768 (T,wt=12): 10095 c2 v ((c1 v (x ^ c2)) ^ y)' = 1. [para(2311(a,1),110(a,1)),rewrite(2(6)),flip(a)]. given #769 (T,wt=12): 10320 c2 v (x ^ (c1 v (c2 ^ y)))' = 1. [para(2333(a,1),24(a,1)),rewrite(2(6)),flip(a)]. given #770 (A,wt=14): 337 x v y != 1 | 0 != y | (x v y)' = y. [para(73(a,1),36(a,1)),rewrite(4(5),20(5)),flip(b)]. given #771 (T,wt=12): 10332 c2 v (x ^ (c1 v (y ^ c2)))' = 1. [para(2333(a,1),110(a,1)),rewrite(2(6)),flip(a)]. given #772 (T,wt=12): 10549 c1 ^ (x ^ ((x ^ c2) v y)') = 0. [para(4(a,1),2417(a,1,2,2,1,1))]. given #773 (T,wt=12): 10552 x ^ (c1 ^ ((c2 ^ x) v y)') = 0. [para(2417(a,1),19(a,1)),flip(a)]. given #774 (T,wt=12): 10754 c1 ^ (x ^ (y v (x ^ c2))') = 0. [para(4(a,1),2443(a,1,2,2,1,2))]. given #775 (A,wt=20): 338 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 #776 (T,wt=12): 10919 (x ^ c2) v (c1 ^ (y ^ x))' = 1. [para(227(a,1),2327(a,1,2)),rewrite(2(7))]. given #777 (T,wt=12): 10954 (x ^ y)' v (x ^ (z v y)) = 1. [para(2464(a,1),2(a,1)),flip(a)]. given #778 (T,wt=12): 11361 c1' v ((c2 v x) ^ (c1 v y)) = 1. [para(129(a,1),2545(a,1,2))]. given #779 (T,wt=12): 11374 c1' v ((c2 v x) ^ (y v c1)) = 1. [para(129(a,1),2546(a,1,2))]. given #780 (A,wt=20): 339 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z. [para(2(a,1),37(b,1,1))]. given #781 (T,wt=12): 12242 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(176(a,1),2744(a,1,2))]. given #782 (T,wt=12): 12261 (c1 v x) ^ (c2 v (y v x))' = 0. [para(2(a,1),2799(a,1,2,1,2))]. given #783 (T,wt=12): 12266 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0. [para(24(a,1),2799(a,1,2,1))]. Low Water (keep, True_semantics): wt=23 given #784 (T,wt=12): 12272 (c1 v (x ^ c2)) ^ (c2 v y)' = 0. [para(110(a,1),2799(a,1,2,1))]. given #785 (A,wt=26): 340 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 #786 (T,wt=12): 12311 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(176(a,1),2800(a,1,2))]. given #787 (T,wt=12): 12390 (x v y)' ^ ((z ^ x) v y) = 0. [para(2833(a,1),4(a,1)),flip(a)]. given #788 (T,wt=12): 12395 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(26(a,1),2833(a,1,2,1))]. given #789 (T,wt=12): 12401 ((x ^ c2) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),2833(a,1,2,1))]. given #790 (A,wt=20): 341 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z. [para(4(a,1),37(b,1))]. given #791 (T,wt=12): 12402 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0. [para(260(a,1),2833(a,1,2,1))]. given #792 (T,wt=12): 12550 x v ((y ^ x) v (z ^ x))' = 1. [para(2836(a,1),110(a,1)),flip(a)]. given #793 (T,wt=12): 12560 c2 v ((x ^ c2) v (y ^ c1))' = 1. [para(2836(a,1),250(a,1)),flip(a)]. given #794 (T,wt=12): 12561 c2 v ((x ^ c2) v (c1 ^ y))' = 1. [para(2836(a,1),263(a,1)),flip(a)]. given #795 (A,wt=18): 342 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),37(a,1,2)),rewrite(19(6),91(6))]. given #796 (T,wt=12): 12634 c2 v ((x ^ c1) v (y ^ c2))' = 1. [para(2861(a,1),250(a,1)),flip(a)]. given #797 (T,wt=12): 12635 c2 v ((c1 ^ x) v (y ^ c2))' = 1. [para(2861(a,1),263(a,1)),flip(a)]. given #798 (T,wt=12): 12714 (x v y)' ^ (x v (z ^ y)) = 0. [para(2890(a,1),4(a,1)),flip(a)]. given #799 (T,wt=12): 12961 (c1 v (x ^ y)) ^ (x v c2)' = 0. [para(24(a,1),3009(a,1,2,1)),rewrite(2(3))]. given #800 (A,wt=26): 343 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 #801 (T,wt=12): 12967 (c1 v (x ^ y)) ^ (y v c2)' = 0. [para(110(a,1),3009(a,1,2,1)),rewrite(2(3))]. given #802 (T,wt=12): 12998 (c1 ^ x)' v ((c2 v y) ^ x) = 1. [para(3081(a,1),2(a,1)),flip(a)]. given #803 (T,wt=12): 12999 (x ^ (c2 v y)) v (c1 ^ x)' = 1. [para(4(a,1),3081(a,1,1))]. given #804 (T,wt=12): 13003 ((c2 v x) ^ (y v c1)) v c1' = 1. [para(20(a,1),3081(a,1,2,1))]. given #805 (A,wt=20): 344 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(17(a,1),37(a,1))]. given #806 (T,wt=12): 13005 ((c2 v x) ^ (c2 v y)) v c1' = 1. [para(213(a,1),3081(a,1,2,1))]. given #807 (T,wt=12): 13006 ((c2 v x) ^ (y v c2)) v c1' = 1. [para(216(a,1),3081(a,1,2,1))]. given #808 (T,wt=12): 13069 c1 ^ ((c2 v x) ^ (c2 v y))' = 0. [para(3082(a,1),218(a,1)),flip(a)]. given #809 (T,wt=12): 13070 c1 ^ ((c2 v x) ^ (y v c2))' = 0. [para(3082(a,1),236(a,1)),flip(a)]. given #810 (A,wt=26): 345 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 #811 (T,wt=12): 13088 c1 ^ ((x v c2) ^ (c2 v y))' = 0. [para(3096(a,1),236(a,1)),flip(a)]. given #812 (T,wt=12): 13096 (x ^ c1)' v (x ^ (c2 v y)) = 1. [para(3108(a,1),2(a,1)),flip(a)]. given #813 (T,wt=12): 13147 (c1 ^ x)' v ((y v c2) ^ x) = 1. [para(3131(a,1),2(a,1)),flip(a)]. given #814 (T,wt=12): 13151 ((x v c2) ^ (y v c1)) v c1' = 1. [para(20(a,1),3131(a,1,2,1))]. given #815 (A,wt=18): 346 x v y != 1 | x v y != 0 | (x v y)' = x v y. [para(28(a,1),37(b,1)),rewrite(73(2),71(2))]. given #816 (T,wt=12): 13153 ((x v c2) ^ (c2 v y)) v c1' = 1. [para(213(a,1),3131(a,1,2,1))]. given #817 (T,wt=12): 13154 ((x v c2) ^ (y v c2)) v c1' = 1. [para(216(a,1),3131(a,1,2,1))]. given #818 (T,wt=12): 13215 c1 ^ ((x v c2) ^ (y v c2))' = 0. [para(3132(a,1),236(a,1)),flip(a)]. given #819 (T,wt=12): 13243 (x ^ c1)' v (x ^ (y v c2)) = 1. [para(3159(a,1),2(a,1)),flip(a)]. given #820 (A,wt=26): 349 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 #821 (T,wt=12): 13273 (c2 v x)' ^ ((y ^ c1) v x) = 0. [para(3207(a,1),4(a,1)),flip(a)]. given #822 (T,wt=12): 13277 ((x ^ c1) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),3207(a,1,2,1))]. given #823 (T,wt=12): 13279 ((x ^ c1) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3207(a,1,2,1))]. given #824 (T,wt=12): 13280 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0. [para(260(a,1),3207(a,1,2,1))]. given #825 (A,wt=22): 350 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(334(3),287(3))]. given #826 (T,wt=12): 13325 c2 v ((x ^ c1) v (y ^ c1))' = 1. [para(3209(a,1),250(a,1)),flip(a)]. given #827 (T,wt=12): 13326 c2 v ((x ^ c1) v (c1 ^ y))' = 1. [para(3209(a,1),263(a,1)),flip(a)]. given #828 (T,wt=12): 13375 c2 v ((c1 ^ x) v (y ^ c1))' = 1. [para(3225(a,1),263(a,1)),flip(a)]. given #829 (T,wt=12): 13416 (c2 ^ x) v (x ^ (y ^ c1))' = 1. [para(4(a,1),3260(a,1,2,1,2))]. given #830 (A,wt=18): 352 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(114(a,1),37(a,1,2)),rewrite(4(8))]. given #831 (T,wt=12): 13508 (x v c2)' ^ (x v (y ^ c1)) = 0. [para(3268(a,1),4(a,1)),flip(a)]. given #832 (T,wt=12): 13616 (x v (c1 ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),3297(a,1,1))]. given #833 (T,wt=12): 13617 (c2 v x)' ^ ((c1 ^ y) v x) = 0. [para(3297(a,1),4(a,1)),flip(a)]. given #834 (T,wt=12): 13620 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),3297(a,1,2,1))]. given #835 (A,wt=32): 353 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 #836 (T,wt=12): 13622 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0. [para(248(a,1),3297(a,1,2,1))]. given #837 (T,wt=12): 13623 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(260(a,1),3297(a,1,2,1))]. given #838 (T,wt=12): 13667 c2 v ((c1 ^ x) v (c1 ^ y))' = 1. [para(3299(a,1),263(a,1)),flip(a)]. given #839 (T,wt=12): 13692 (x v c2)' ^ (x v (c1 ^ y)) = 0. [para(3364(a,1),4(a,1)),flip(a)]. given #840 (A,wt=19): 354 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z. [para(86(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #841 (T,wt=12): 13834 (x ^ c2) v (c1 ^ (x ^ y))' = 1. [para(247(a,1),3455(a,1,2,1))]. given #842 (T,wt=12): 13917 (c1 v x) ^ (x v (y v c2))' = 0. [para(122(a,1),3505(a,1,2,1,2))]. given #843 (T,wt=12): 14017 x v (c2 v ((c1 v x) ^ y)') = 1. [para(4(a,1),3775(a,1,2,2,1))]. given #844 (T,wt=12): 14874 (c2 ^ (c1 v x)) v (c1 ^ y)' = 1. [para(22(a,1),4551(a,1,2,1))]. given #845 (A,wt=23): 355 x v (y v ((x v y)' ^ z)) != 1 | (x v y)' ^ z = (x v y)'. [para(89(a,1),37(b,1)),flip(c),xx(b)]. given #846 (T,wt=12): 14879 (c2 ^ (x v c1)) v (c1 ^ y)' = 1. [para(91(a,1),4551(a,1,2,1))]. given #847 (T,wt=12): 14911 (x v y)' ^ ((y ^ z) v x) = 0. [para(4623(a,1),4(a,1)),flip(a)]. given #848 (T,wt=12): 15129 (x v y)' ^ ((z ^ y) v x) = 0. [para(4626(a,1),4(a,1)),flip(a)]. given #849 (T,wt=12): 15196 (x v c2)' ^ ((y ^ c1) v x) = 0. [para(4631(a,1),4(a,1)),flip(a)]. given #850 (A,wt=19): 356 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'. [para(98(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #851 (T,wt=12): 15216 (x v c2)' ^ ((c1 ^ y) v x) = 0. [para(4633(a,1),4(a,1)),flip(a)]. given #852 (T,wt=12): 15362 (x v y)' ^ (y v (x ^ z)) = 0. [para(4703(a,1),4(a,1)),flip(a)]. given #853 (T,wt=12): 15418 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),4705(a,1,1,1))]. given #854 (T,wt=12): 15422 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(26(a,1),4705(a,1,1,1))]. given #855 (A,wt=15): 357 (x v y) ^ x' != 0 | (x v y)' = x'. [para(98(a,1),37(a,1)),xx(a)]. given #856 (T,wt=12): 15426 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(248(a,1),4705(a,1,1,1))]. given #857 (T,wt=12): 15427 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(260(a,1),4705(a,1,1,1))]. given #858 (T,wt=12): 15725 (x ^ y)' v ((y v z) ^ x) = 1. [para(4791(a,1),2(a,1)),flip(a)]. given #859 (T,wt=12): 15751 (x ^ y)' v ((z v y) ^ x) = 1. [para(4793(a,1),2(a,1)),flip(a)]. given #860 (A,wt=23): 358 x v (y v (z ^ (x v y)')) != 1 | z ^ (x v y)' = (x v y)'. [para(100(a,1),37(b,1)),flip(c),xx(b)]. given #861 (T,wt=12): 15799 (x ^ c1)' v ((c2 v y) ^ x) = 1. [para(4795(a,1),2(a,1)),flip(a)]. given #862 (T,wt=12): 15813 (x ^ c1)' v ((y v c2) ^ x) = 1. [para(4797(a,1),2(a,1)),flip(a)]. given #863 (T,wt=12): 15823 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),4920(a,1,2))]. given #864 (T,wt=12): 15825 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),4920(a,1,1,1))]. given #865 (A,wt=36): 359 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 #866 (T,wt=12): 15829 x' v ((x v y) ^ (z v x)) = 1. [para(20(a,1),4920(a,1,1,1))]. given #867 (T,wt=12): 15834 c1' v ((c1 v x) ^ (c2 v y)) = 1. [para(213(a,1),4920(a,1,1,1))]. given #868 (T,wt=12): 15835 c1' v ((c1 v x) ^ (y v c2)) = 1. [para(216(a,1),4920(a,1,1,1))]. given #869 (T,wt=12): 16491 (x v c2)' ^ (c1 v (c2 ^ y)) = 0. [para(5892(a,1),4(a,1)),flip(a)]. given #870 (A,wt=23): 360 x v (y v (x v (y v z))') != 1 | (x v (y v z))' = (x v y)'. [para(125(a,1),37(b,1)),rewrite(3(2),3(14)),flip(c),xx(b)]. given #871 (T,wt=12): 16554 (x v c2)' ^ (c1 v (y ^ c2)) = 0. [para(5896(a,1),4(a,1)),flip(a)]. given #872 (T,wt=12): 16570 (c2 v x)' ^ (c1 v (x ^ y)) = 0. [para(5908(a,1),4(a,1)),flip(a)]. given #873 (T,wt=12): 16610 (c2 v x)' ^ (c1 v (y ^ x)) = 0. [para(5912(a,1),4(a,1)),flip(a)]. given #874 (T,wt=12): 16738 (x ^ c1)' v (c2 ^ (c1 v y)) = 1. [para(6696(a,1),2(a,1)),flip(a)]. given #875 (A,wt=23): 361 x v (y v (z v (x v y))') != 1 | (z v (x v y))' = (x v y)'. [para(153(a,1),37(b,1)),flip(c),xx(b)]. given #876 (T,wt=12): 16803 (x ^ c1)' v (c2 ^ (y v c1)) = 1. [para(6701(a,1),2(a,1)),flip(a)]. given #877 (T,wt=12): 16817 (c1 ^ x)' v (c2 ^ (x v y)) = 1. [para(6722(a,1),2(a,1)),flip(a)]. given #878 (T,wt=12): 16862 (c1 ^ x)' v (c2 ^ (y v x)) = 1. [para(6727(a,1),2(a,1)),flip(a)]. given #879 (T,wt=12): 16936 (x ^ c1)' v (c2 ^ (x v y)) = 1. [para(6759(a,1),2(a,1)),flip(a)]. given #880 (A,wt=28): 362 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 #881 (T,wt=12): 16952 (x ^ c1)' v (c2 ^ (y v x)) = 1. [para(6767(a,1),2(a,1)),flip(a)]. given #882 (T,wt=12): 17345 x' v ((y v x) ^ (x v z)) = 1. [para(7921(a,1),2(a,1)),flip(a)]. given #883 (T,wt=12): 17375 c1' v ((x v c2) ^ (c1 v y)) = 1. [para(7924(a,1),2(a,1)),flip(a)]. given #884 (T,wt=12): 17423 (x ^ y)' v (y ^ (z v x)) = 1. [para(7960(a,1),2(a,1)),flip(a)]. given #885 (A,wt=19): 363 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(172(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #886 (T,wt=12): 17518 (c1 ^ x)' v (x ^ (y v c2)) = 1. [para(7970(a,1),2(a,1)),flip(a)]. given #887 (T,wt=12): 17635 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(9406(a,1),4(a,1)),flip(a)]. given #888 (T,wt=12): 17653 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(9408(a,1),4(a,1)),flip(a)]. given #889 (T,wt=12): 17692 (x v y)' ^ (y v (z ^ x)) = 0. [para(9430(a,1),4(a,1)),flip(a)]. given #890 (A,wt=19): 364 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(183(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #891 (T,wt=12): 17783 (c2 v x)' ^ (x v (y ^ c1)) = 0. [para(9436(a,1),4(a,1)),flip(a)]. given #892 (T,wt=12): 17819 x' v ((y v x) ^ (z v x)) = 1. [para(20(a,1),9449(a,1,1,1))]. given #893 (T,wt=12): 17824 c1' v ((x v c1) ^ (c2 v y)) = 1. [para(213(a,1),9449(a,1,1,1))]. given #894 (T,wt=12): 17825 c1' v ((x v c1) ^ (y v c2)) = 1. [para(216(a,1),9449(a,1,1,1))]. Low Water (keep, True_semantics): wt=22 given #895 (A,wt=15): 365 (x v c2) ^ c1' != 0 | (x v c2)' = c1'. [para(191(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #896 (T,wt=12): 18284 c1' v ((c2 v x) ^ (c2 v y)) = 1. [para(120(a,1),11361(a,1,2,2))]. given #897 (T,wt=12): 18285 c1' v ((c2 v x) ^ (y v c2)) = 1. [para(122(a,1),11361(a,1,2,2))]. given #898 (T,wt=12): 18294 c1' v ((x v c2) ^ (y v c1)) = 1. [para(2(a,1),11374(a,1,2,1))]. given #899 (T,wt=12): 18510 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(60(a,1),12242(a,1,2,2))]. given #900 (A,wt=32): 366 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 #901 (T,wt=12): 18535 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0. [para(12266(a,1),4(a,1)),flip(a)]. given #902 (T,wt=12): 18547 (c2 v x)' ^ (c1 v (y ^ c2)) = 0. [para(12272(a,1),4(a,1)),flip(a)]. given #903 (T,wt=12): 18562 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(2(a,1),12311(a,1,2))]. given #904 (T,wt=12): 18563 c2' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(4(a,1),12311(a,1,2,1))]. given #905 (A,wt=22): 367 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(25(a,1),37(a,1)),rewrite(66(7))]. given #906 (T,wt=12): 18575 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(26(a,1),12390(a,1,1,1))]. given #907 (T,wt=12): 18579 c2' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(248(a,1),12390(a,1,1,1))]. given #908 (T,wt=12): 18912 (x v c2)' ^ (c1 v (x ^ y)) = 0. [para(12961(a,1),4(a,1)),flip(a)]. given #909 (T,wt=12): 18924 (x v c2)' ^ (c1 v (y ^ x)) = 0. [para(12967(a,1),4(a,1)),flip(a)]. given #910 (A,wt=19): 368 (x v c2) ^ (c1' v y) != 0 | (x v c2)' = c1' v y. [para(196(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #911 (T,wt=12): 18928 (c1 ^ x)' v (x ^ (c2 v y)) = 1. [para(4(a,1),12998(a,1,2))]. given #912 (T,wt=12): 19059 c1' v ((x v c2) ^ (c2 v y)) = 1. [para(213(a,1),13147(a,1,1,1))]. given #913 (T,wt=12): 19060 c1' v ((x v c2) ^ (y v c2)) = 1. [para(216(a,1),13147(a,1,1,1))]. given #914 (T,wt=12): 19130 c2' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(248(a,1),13273(a,1,1,1))]. given #915 (A,wt=19): 369 (x v c2) ^ (y v c1') != 0 | (x v c2)' = y v c1'. [para(198(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #916 (T,wt=12): 19131 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(260(a,1),13273(a,1,1,1))]. given #917 (T,wt=12): 19216 (c2 v x)' ^ (x v (c1 ^ y)) = 0. [para(13616(a,1),4(a,1)),flip(a)]. given #918 (T,wt=12): 19246 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(260(a,1),13617(a,1,1,1))]. given #919 (T,wt=12): 19321 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1. [para(14874(a,1),2(a,1)),flip(a)]. given #920 (A,wt=15): 370 (c2 v x) ^ c1' != 0 | (c2 v x)' = c1'. [para(198(a,1),37(a,1)),xx(a)]. given #921 (T,wt=12): 19333 (c1 ^ x)' v (c2 ^ (y v c1)) = 1. [para(14879(a,1),2(a,1)),flip(a)]. given #922 (T,wt=13): 387 x v (y v (z ^ (x ^ u))) = y v x. [para(80(a,1),17(a,1,2)),flip(a)]. given #923 (T,wt=13): 390 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(5(a,1),83(a,1,2)),rewrite(4(8))]. given #924 (T,wt=13): 396 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(90(a,1),5(a,1,1)),flip(a)]. given #925 (A,wt=23): 372 (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(96(2)),xx(a)]. given #926 (T,wt=13): 400 x ^ (y ^ (z v (u v x))) = y ^ x. [para(90(a,1),19(a,1,2)),flip(a)]. given #927 (T,wt=13): 405 x v ((y ^ (z ^ x)) v u) = x v u. [para(112(a,1),3(a,1,1)),flip(a)]. given #928 (T,wt=13): 409 x v (y v (z ^ (u ^ x))) = y v x. [para(112(a,1),17(a,1,2)),flip(a)]. given #929 (T,wt=13): 414 (c2 ^ x) v (y ^ (c1 ^ x)) = c2 ^ x. [para(59(a,1),112(a,1,2,2))]. given #930 (A,wt=18): 374 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y. [para(260(a,1),37(a,1,2)),rewrite(19(9),236(9))]. given #931 (T,wt=13): 417 (x ^ c2) v (y ^ (x ^ c1)) = x ^ c2. [para(83(a,1),112(a,1,2,2))]. Low Water (keep, True_semantics): wt=21 given #932 (T,wt=13): 426 x v (x v y)' != 1 | x v y = x. [para(125(a,1),38(b,1)),rewrite(2(3),298(11)),xx(b)]. given #933 (T,wt=13): 428 x v (y v x)' != 1 | y v x = x. [para(153(a,1),38(b,1)),rewrite(2(3),298(11)),xx(b)]. given #934 (T,wt=13): 434 c1 v (c2 v x)' != 1 | c2 v x = c1. [para(220(a,1),38(b,1)),rewrite(2(5),298(14)),xx(b)]. given #935 (A,wt=19): 375 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'. [para(251(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #936 (F,wt=11): 20835 c1' v (c1' v c2')' != 1. [ur(426,b,15,a)]. given #937 (F,wt=12): 20843 (c1' v (c1' v c2')')' != 0. [ur(4501,b,20835,a),rewrite(2(9))]. given #938 (T,wt=13): 435 c1 v (x v c2)' != 1 | x v c2 = c1. [para(221(a,1),38(b,1)),rewrite(2(5),298(14)),xx(b)]. given #939 (T,wt=13): 438 (x v y) ^ y' != 0 | x v y = y. [para(319(a,1),38(a,1)),rewrite(298(10)),flip(c),xx(a)]. given #940 (T,wt=13): 443 c1 v (x v (c2 v y)) = x v (c2 v y). [para(120(a,1),17(a,1,2)),flip(a)]. given #941 (T,wt=13): 444 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(120(a,1),21(a,1,2,2))]. given #942 (A,wt=19): 376 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'. [para(268(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #943 (T,wt=13): 447 c2 v (x v (y v c1)) = c2 v (x v y). [para(3(a,1),121(a,1,2)),rewrite(2(8))]. given #944 (T,wt=13): 458 (x v c1) ^ (y v (x v c2)) = x v c1. [para(121(a,1),90(a,1,2,2))]. given #945 (T,wt=13): 460 c1 v (x v (y v c2)) = x v (y v c2). [para(122(a,1),17(a,1,2)),flip(a)]. given #946 (T,wt=13): 461 (x v c1) ^ (x v (y v c2)) = x v c1. [para(122(a,1),21(a,1,2,2))]. given #947 (A,wt=27): 377 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 #948 (T,wt=13): 466 c1 ^ ((x v (c2 v y)) ^ z) = c1 ^ z. [para(224(a,1),5(a,1,1)),flip(a)]. given #949 (T,wt=13): 468 c1 ^ (x ^ (y v (c2 v z))) = x ^ c1. [para(224(a,1),19(a,1,2)),flip(a)]. given #950 (T,wt=13): 524 c1 ^ ((x v (y v c2)) ^ z) = c1 ^ z. [para(235(a,1),5(a,1,1)),flip(a)]. given #951 (T,wt=13): 526 c1 ^ (x ^ (y v (z v c2))) = x ^ c1. [para(235(a,1),19(a,1,2)),flip(a)]. given #952 (A,wt=22): 379 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y). [para(68(a,1),37(b,1)),rewrite(111(4))]. given #953 (T,wt=13): 529 c2 v ((x ^ (y ^ c1)) v z) = c2 v z. [para(261(a,1),3(a,1,1)),flip(a)]. given #954 (T,wt=13): 532 c2 v (x v (y ^ (z ^ c1))) = x v c2. [para(261(a,1),17(a,1,2)),flip(a)]. given #955 (T,wt=13): 535 c2 v ((x ^ (c1 ^ y)) v z) = c2 v z. [para(266(a,1),3(a,1,1)),flip(a)]. Low Water (keep, True_semantics): wt=20 given #956 (T,wt=13): 538 c2 v (x v (y ^ (c1 ^ z))) = x v c2. [para(266(a,1),17(a,1,2)),flip(a)]. given #957 (A,wt=24): 380 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z. [para(71(a,1),37(a,1,2))]. given #958 (T,wt=13): 598 c2 v (x v (c1 v y)) = c2 v (x v y). [para(446(a,1),3(a,1,1)),rewrite(3(3),3(7)),flip(a)]. given #959 (T,wt=13): 605 (x v c1) ^ (y v (c2 v x)) = x v c1. [para(446(a,1),90(a,1,2,2))]. given #960 (T,wt=13): 1823 x' ^ (x v y) != 0 | x v y = x. [para(86(a,1),65(a,1)),rewrite(298(10)),flip(c),xx(a)]. given #961 (T,wt=13): 1828 c1' ^ (c2 v x) != 0 | c2 v x = c1. [para(196(a,1),65(a,1)),rewrite(298(13)),flip(c),xx(a)]. given #962 (A,wt=19): 381 (x v y') ^ (z v y) != 0 | (x v y')' = z v y. [para(319(a,1),37(a,1,2)),rewrite(96(2)),xx(a)]. given #963 (T,wt=13): 1881 c1' ^ (x v c2) != 0 | x v c2 = c1. [para(1869(a,1),10(a,1)),rewrite(298(13)),flip(c),xx(a)]. given #964 (T,wt=13): 1883 (x v c2) ^ c1' != 0 | x v c2 = c1. [para(1869(a,1),38(a,1)),rewrite(298(13)),flip(c),xx(a)]. given #965 (T,wt=13): 1970 c2' v (x ^ c1) != 1 | x ^ c1 = c2. [para(1936(a,1),10(b,1)),rewrite(298(13)),flip(c),xx(b)]. given #966 (T,wt=13): 1971 (x ^ c1) v c2' != 1 | x ^ c1 = c2. [para(1936(a,1),36(b,1)),rewrite(298(13)),flip(c),xx(b)]. given #967 (A,wt=24): 382 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z. [para(73(a,1),37(a,1,2))]. given #968 (T,wt=13): 2037 x' v (x ^ y) != 1 | x ^ y = x. [para(89(a,1),82(b,1)),rewrite(298(10)),flip(c),xx(b)]. given #969 (T,wt=13): 2040 c2' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(159(a,1),82(b,1)),rewrite(298(13)),flip(c),xx(b)]. given #970 (T,wt=13): 2226 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(4(a,1),92(a,1,2,2,2))]. given #971 (T,wt=13): 2234 c1 ^ (x ^ (y v (c2 ^ x))) = c1 ^ x. [para(92(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #972 (A,wt=14): 383 x v y != 1 | 0 != y | (y v x)' = y. [para(73(a,1),37(a,1)),rewrite(4(5),6(5)),flip(b)]. given #973 (T,wt=13): 2367 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),94(a,1,2)),rewrite(3(3))]. given #974 (T,wt=13): 2519 (x v (y v z)) ^ (y v x) = x v y. [para(102(a,1),4(a,1)),flip(a)]. given #975 (T,wt=13): 2527 x v (y v (z ^ (y v x))) = x v y. [para(102(a,1),80(a,1,2,2)),rewrite(3(4))]. Low Water (displace, True_semantics): id=11740, wt=50 Low Water (displace, True_semantics): id=11554, wt=46 Low Water (displace, True_semantics): id=12352, wt=43 Low Water (displace, True_semantics): id=12498, wt=40 Low Water (displace, True_semantics): id=12387, wt=39 Low Water (displace, True_semantics): id=11608, wt=38 Low Water (displace, True_semantics): id=12727, wt=37 Low Water (displace, True_semantics): id=13019, wt=36 Low Water (displace, True_semantics): id=13107, wt=35 given #976 (T,wt=13): 2529 (c1 v x) ^ (x v (c2 v y)) = x v c1. [para(120(a,1),102(a,1,2,2))]. Low Water (displace, True_semantics): id=13368, wt=34 given #977 (A,wt=15): 384 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),80(a,1,2,2))]. given #978 (T,wt=13): 2530 (c1 v x) ^ (x v (y v c2)) = x v c1. [para(122(a,1),102(a,1,2,2))]. Low Water (displace, True_semantics): id=13403, wt=33 given #979 (T,wt=13): 2601 (x v (y v z)) ^ (z v x) = z v x. [para(103(a,1),4(a,1)),flip(a)]. given #980 (T,wt=13): 2998 x v (c2 v (y ^ (x v c1))) = x v c2. [para(123(a,1),112(a,1,2,2)),rewrite(3(6))]. Low Water (displace, True_semantics): id=13900, wt=32 Low Water (displace, True_semantics): id=14253, wt=31 given #981 (T,wt=13): 3012 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),217(a,1,1))]. Low Water (displace, True_semantics): id=14793, wt=30 given #982 (A,wt=18): 386 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(80(a,1),10(a,1)),rewrite(289(5)),flip(a)]. given #983 (T,wt=11): 22267 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(3012(a,1),44(a,2,2)),rewrite(71(8),3993(7),71(6),95(10))]. Low Water (displace, True_semantics): id=14817, wt=29 Low Water (displace, True_semantics): id=14959, wt=28 given #984 (T,wt=11): 22268 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(3012(a,1),53(a,1,2)),rewrite(95(5)),flip(a)]. Low Water (keep, True_semantics): wt=19 given #985 (T,wt=11): 22305 x v (c2 ^ (c1 v x)) = x v c1. [para(3012(a,1),2527(a,1,2))]. Low Water (displace, True_semantics): id=15415, wt=27 given #986 (T,wt=11): 22386 x v (c2 ^ (x v c1)) = x v c1. [para(2(a,1),22305(a,1,2,2))]. given #987 (A,wt=18): 388 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(80(a,1),36(a,1)),rewrite(4(5),289(5)),flip(a)]. given #988 (T,wt=13): 3017 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(20(a,1),217(a,1,1))]. given #989 (T,wt=13): 3060 (c1 v x) ^ (c2 v (x v y)) = c1 v x. [para(120(a,1),108(a,1,2))]. given #990 (T,wt=13): 3246 x ^ (c1 ^ (y v (c2 ^ x))) = x ^ c1. [para(253(a,1),90(a,1,2,2)),rewrite(5(6))]. given #991 (T,wt=13): 3387 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),284(a,1,2,2))]. given #992 (A,wt=18): 391 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1' = x ^ c2. [para(83(a,1),10(b,1))]. given #993 (T,wt=13): 3402 c1 ^ (x v (y v (z v (c2 v u)))) = c1. [para(284(a,1),236(a,1,2)),rewrite(216(4),3(5)),flip(a)]. given #994 (T,wt=13): 3405 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(17(a,1),292(a,1,1))]. given #995 (T,wt=13): 3411 x ^ (c1 ^ ((x ^ c2) v y)) = x ^ c1. [para(83(a,1),292(a,1,2)),rewrite(4(6),5(6),83(10))]. given #996 (T,wt=13): 3434 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(293(a,1),24(a,2)),rewrite(5(3),3429(6))]. given #997 (A,wt=15): 397 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(90(a,1),5(a,1)),flip(a)]. given #998 (T,wt=13): 3521 (x ^ (y ^ z)) v (u v y) = u v y. [para(19(a,1),336(a,1,1))]. given #999 (T,wt=13): 3529 c2 v (x v ((x v c1) ^ y)) = c2 v x. [para(446(a,1),336(a,1,2)),rewrite(17(6),2(5),446(10))]. given #1000 (T,wt=11): 22826 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(7(a,1),3529(a,2)),rewrite(2(7),24(10))]. given #1001 (T,wt=11): 22827 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(26(a,1),3529(a,2)),rewrite(2(7),110(10))]. given #1002 (A,wt=18): 398 x v (y v z) != 1 | 0 != z | z' = x v (y v z). [para(90(a,1),10(b,1)),rewrite(334(3)),flip(b)]. given #1003 (T,wt=11): 22899 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(4(a,1),22826(a,1,2))]. given #1004 (T,wt=11): 22951 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),22827(a,1,2))]. given #1005 (T,wt=13): 3552 (x ^ (c1 ^ y)) v (c2 ^ x) = c2 ^ x. [para(253(a,1),336(a,1,2)),rewrite(5(3),253(11))]. given #1006 (T,wt=13): 3562 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),116(a,1,2)),rewrite(5(3))]. given #1007 (A,wt=15): 399 (x v y) ^ (z v (x v (u v y))) = x v y. [para(17(a,1),90(a,1,2,2))]. Low Water (displace, True_semantics): id=16875, wt=26 given #1008 (T,wt=13): 3623 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(5(a,1),385(a,1,2,2))]. Low Water (keep, True_semantics): wt=18 given #1009 (T,wt=13): 3643 c2 v (x ^ (y ^ (z ^ (c1 ^ u)))) = c2. [para(385(a,1),250(a,1,2)),rewrite(248(4),5(5)),flip(a)]. given #1010 (T,wt=13): 3662 x ^ (c1 ^ (y v (x ^ c2))) = x ^ c1. [para(392(a,1),62(a,1,2,2)),rewrite(5(6))]. given #1011 (T,wt=13): 3678 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),395(a,1,2,2,2))]. given #1012 (A,wt=17): 401 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(24(a,1),90(a,1,2,2))]. given #1013 (T,wt=13): 3704 c1 ^ (x v (y v (z v (u v c2)))) = c1. [para(395(a,1),236(a,1,2)),rewrite(216(4)),flip(a)]. given #1014 (T,wt=13): 3718 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),407(a,1,2,2,2))]. given #1015 (T,wt=13): 3763 c2 v (x ^ (y ^ (z ^ (u ^ c1)))) = c2. [para(407(a,1),250(a,1,2)),rewrite(248(4)),flip(a)]. given #1016 (T,wt=13): 3769 x v (c2 v (y ^ (c1 v x))) = x v c2. [para(462(a,1),112(a,1,2,2)),rewrite(3(6))]. given #1017 (A,wt=21): 402 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(25(a,1),90(a,1,2,2))]. given #1018 (T,wt=13): 3783 (x v (c2 v y)) ^ (c1 v x) = c1 v x. [para(462(a,1),292(a,1,2)),rewrite(3(3),462(11))]. given #1019 (T,wt=13): 3991 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(7(a,1),600(a,1,2)),rewrite(2(4),4(6),2(10))]. given #1020 (T,wt=13): 3993 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(26(a,1),600(a,1,2)),rewrite(2(4),4(6),2(10))]. given #1021 (T,wt=13): 3997 c2 v (x v (y ^ (x v c1))) = c2 v x. [para(600(a,1),112(a,1,2,2)),rewrite(3(6))]. given #1022 (A,wt=17): 403 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(27(a,1),90(a,1,2,2)),rewrite(5(5),5(4))]. given #1023 (T,wt=13): 4011 (c2 v (x v y)) ^ (x v c1) = x v c1. [para(600(a,1),292(a,1,2)),rewrite(3(3),600(11))]. given #1024 (T,wt=13): 4018 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),2157(a,1,1))]. given #1025 (T,wt=13): 4052 (x v (y v z)) ^ (z v y) = z v y. [para(335(a,1),2157(a,1,2)),rewrite(335(7))]. given #1026 (T,wt=13): 4055 (x v (y v c2)) ^ (c1 v y) = c1 v y. [para(462(a,1),2157(a,1,2)),rewrite(462(11))]. Low Water (displace, True_semantics): id=17510, wt=25 given #1027 (A,wt=15): 406 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(112(a,1),3(a,1)),flip(a)]. given #1028 (T,wt=13): 4059 (x v (c2 v y)) ^ (y v c1) = y v c1. [para(600(a,1),2157(a,1,2)),rewrite(600(11))]. given #1029 (T,wt=13): 4120 c2 v (x v (y ^ (c1 v x))) = c2 v x. [para(2384(a,1),112(a,1,2,2)),rewrite(3(6))]. given #1030 (T,wt=13): 4134 (c1 v x) ^ (y v (c2 v x)) = c1 v x. [para(2384(a,1),2157(a,1,2)),rewrite(4(6),2384(11))]. given #1031 (T,wt=13): 4138 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),2838(a,1,1))]. given #1032 (A,wt=18): 408 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(112(a,1),10(a,1)),rewrite(291(5)),flip(a)]. given #1033 (T,wt=13): 4182 (x ^ (y ^ c1)) v (c2 ^ y) = c2 ^ y. [para(253(a,1),2838(a,1,2)),rewrite(253(11))]. given #1034 (T,wt=13): 4186 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(293(a,1),2838(a,1,2)),rewrite(293(7))]. given #1035 (T,wt=13): 4278 (x v (c2 v y)) ^ (z ^ c1) = z ^ c1. [para(17(a,1),3083(a,1,1))]. given #1036 (T,wt=13): 4289 (x v (y v c2)) ^ (z ^ c1) = z ^ c1. [para(3(a,1),3133(a,1,1))]. given #1037 (A,wt=15): 410 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(19(a,1),112(a,1,2,2))]. given #1038 (T,wt=13): 4402 (x ^ (y ^ c1)) v (z v c2) = z v c2. [para(5(a,1),3211(a,1,1))]. given #1039 (T,wt=13): 4424 (x ^ (c1 ^ y)) v (z v c2) = z v c2. [para(19(a,1),3301(a,1,1))]. given #1040 (T,wt=13): 4560 (c1 ^ (x ^ y)) v (c2 ^ x) = c2 ^ x. [para(4255(a,1),336(a,1,2)),rewrite(5(3),4255(11))]. given #1041 (T,wt=13): 4565 (x ^ (c1 ^ y)) v (c2 ^ y) = c2 ^ y. [para(4255(a,1),2838(a,1,2)),rewrite(4255(11))]. given #1042 (A,wt=17): 411 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(21(a,1),112(a,1,2,2)),rewrite(3(5),3(4))]. given #1043 (T,wt=13): 4876 c1 ^ (x ^ ((x ^ c2) v y)) = c1 ^ x. [para(145(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #1044 (T,wt=13): 5976 x ^ ((y ^ z) v (z ^ x)) = z ^ x. [para(151(a,1),53(a,1,2)),rewrite(95(4)),flip(a)]. given #1045 (T,wt=13): 6129 x ^ (((x v y) ^ (x v z)) v u) = x. [para(152(a,1),22(a,1)),rewrite(6(2)),flip(a)]. Low Water (displace, True_semantics): id=17940, wt=24 given #1046 (T,wt=13): 6155 x ^ (((x v y) ^ (z v x)) v u) = x. [para(152(a,1),91(a,1)),rewrite(20(2)),flip(a)]. given #1047 (A,wt=17): 412 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(22(a,1),112(a,1,2,2))]. given #1048 (T,wt=13): 6165 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(152(a,1),218(a,1)),rewrite(213(4)),flip(a)]. given #1049 (T,wt=13): 6167 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(152(a,1),236(a,1)),rewrite(216(4)),flip(a)]. given #1050 (T,wt=13): 6208 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(17(a,1),6131(a,1,2,1,2))]. given #1051 (T,wt=13): 6209 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(17(a,1),6131(a,1,2))]. given #1052 (A,wt=21): 413 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(23(a,1),112(a,1,2,2))]. given #1053 (T,wt=13): 6243 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(3(a,1),6204(a,1,2,1,2))]. given #1054 (T,wt=13): 6246 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(17(a,1),6204(a,1,2))]. given #1055 (T,wt=13): 6279 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),6205(a,1,2))]. given #1056 (T,wt=13): 6282 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),6205(a,1,2,2,2))]. given #1057 (A,wt=18): 415 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x. [para(112(a,1),36(a,1)),rewrite(4(5),291(5)),flip(a)]. given #1058 (T,wt=13): 6313 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(3(a,1),6242(a,1,2,2,2))]. given #1059 (T,wt=13): 6314 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(3(a,1),6242(a,1,2))]. given #1060 (T,wt=13): 6825 x v (c2 v ((x v c1) ^ y)) = x v c2. [para(114(a,1),170(a,2,2)),rewrite(2(6),120(7))]. given #1061 (T,wt=13): 7048 (c2 ^ x) v (c1 ^ (x ^ y)) = c2 ^ x. [para(253(a,1),171(a,1,2)),rewrite(27(6),4(7)),flip(a)]. given #1062 (A,wt=20): 418 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z. [para(5(a,1),38(b,1))]. given #1063 (T,wt=13): 7515 (x ^ c2) v (x ^ (c1 ^ y)) = x ^ c2. [para(392(a,1),176(a,1,1)),rewrite(5(5),2(8),6(9),5(5),2(8)),flip(a)]. given #1064 (T,wt=13): 7522 (c1 ^ (x ^ y)) v (x ^ c2) = c2 ^ x. [para(3011(a,1),176(a,1,1)),rewrite(5(5),5(9),2226(9),5(5)),flip(a)]. given #1065 (T,wt=13): 8813 c2 v (x v ((c1 v x) ^ y)) = c2 v x. [para(202(a,1),120(a,1)),rewrite(17(4),120(4)),flip(a)]. given #1066 (T,wt=13): 9705 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(207(a,1),24(a,1)),rewrite(7(2)),flip(a)]. given #1067 (A,wt=20): 419 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z. [para(17(a,1),38(a,1))]. given #1068 (T,wt=13): 9736 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(207(a,1),110(a,1)),rewrite(26(2)),flip(a)]. given #1069 (T,wt=13): 9738 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(207(a,1),250(a,1)),rewrite(248(4)),flip(a)]. given #1070 (T,wt=13): 9739 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(207(a,1),263(a,1)),rewrite(260(4)),flip(a)]. given #1071 (T,wt=13): 9949 (c2 ^ x) v (x ^ (c1 ^ y)) = c2 ^ x. [para(212(a,1),27(a,1,2))]. given #1072 (A,wt=20): 420 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z. [para(19(a,1),38(b,1))]. given #1073 (T,wt=13): 10277 x ^ (c1 ^ ((c2 ^ x) v y)) = x ^ c1. [para(145(a,1),215(a,1,2)),rewrite(83(4)),flip(a)]. Low Water (displace, True_semantics): id=18528, wt=23 given #1074 (T,wt=13): 10615 (c2 ^ x) v (x ^ (y ^ c1)) = x ^ c2. [para(60(a,1),226(a,1,2,2))]. given #1075 (T,wt=13): 10807 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(227(a,1),2(a,1)),flip(a)]. given #1076 (T,wt=13): 12084 (x ^ c2) v (c1 ^ (x ^ y)) = c2 ^ x. [para(247(a,1),226(a,1,2))]. given #1077 (A,wt=22): 421 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),287(3),71(3))]. given #1078 (T,wt=13): 12097 (c2 ^ x) v (c1 ^ (y ^ x)) = c2 ^ x. [para(247(a,1),232(a,1,2))]. given #1079 (T,wt=13): 12185 (x ^ c2) v (y ^ (c1 ^ x)) = x ^ c2. [para(4(a,1),252(a,1,2)),rewrite(5(5))]. given #1080 (T,wt=13): 13442 (c1 v x) ^ (y v (x v c2)) = c1 v x. [para(122(a,1),283(a,1,2,2))]. given #1081 (T,wt=13): 15264 (x ^ y) v x' != 1 | x ^ y = x. [para(89(a,1),300(b,1)),rewrite(298(10)),flip(c),xx(b)]. given #1082 (A,wt=22): 422 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 #1083 (T,wt=13): 15266 (c1 ^ x) v c2' != 1 | c1 ^ x = c2. [para(159(a,1),300(b,1)),rewrite(298(13)),flip(c),xx(b)]. given #1084 (T,wt=13): 15487 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(298(a,1),4707(a,1,2)),rewrite(4(6))]. given #1085 (T,wt=13): 15511 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(298(a,1),4712(a,1,2)),rewrite(4(6))]. given #1086 (T,wt=13): 15983 x v ((x' v y) ^ (x' v z)) = 1. [para(298(a,1),4922(a,1,2)),rewrite(2(6))]. given #1087 (A,wt=15): 423 x v (x' ^ y) != 1 | (x' ^ y)' = x. [para(89(a,1),38(b,1)),rewrite(2(3)),xx(b)]. given #1088 (T,wt=13): 16006 x v ((x' v y) ^ (z v x')) = 1. [para(298(a,1),4926(a,1,2)),rewrite(2(6))]. given #1089 (T,wt=13): 16065 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),306(a,1,2,1))]. given #1090 (T,wt=13): 16202 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),307(a,1,2,1))]. given #1091 (T,wt=13): 16203 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),307(a,1,2,1)),rewrite(6(7)),flip(b)]. given #1092 (A,wt=15): 424 x v (y ^ x') != 1 | (y ^ x')' = x. [para(100(a,1),38(b,1)),rewrite(2(3)),xx(b)]. given #1093 (T,wt=13): 16206 (c2 v x) ^ c1' != 0 | c2 v x = c1. [para(213(a,1),307(a,1,2,1)),rewrite(213(11)),flip(b)]. given #1094 (T,wt=13): 17102 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),316(a,1,2,1))]. given #1095 (T,wt=13): 17229 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),317(a,1,2,1))]. given #1096 (T,wt=13): 17330 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),323(a,1,2))]. given #1097 (A,wt=26): 425 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 #1098 (T,wt=13): 17348 x v ((y v x') ^ (x' v z)) = 1. [para(298(a,1),7921(a,1,2)),rewrite(2(6))]. given #1099 (T,wt=13): 17638 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(298(a,1),9406(a,1,2)),rewrite(4(6))]. given #1100 (T,wt=13): 17661 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),329(a,1,2))]. given #1101 (T,wt=13): 17920 x v ((y v x') ^ (z v x')) = 1. [para(298(a,1),9455(a,1,2)),rewrite(2(6))]. given #1102 (A,wt=15): 429 c1 v (c2' ^ x) != 1 | (c2' ^ x)' = c1. [para(159(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #1103 (T,wt=13): 18011 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),332(a,1,1))]. given #1104 (T,wt=13): 18626 x ^ ((y ^ x') v (z ^ x')) = 0. [para(298(a,1),12395(a,1,2)),rewrite(4(6))]. given #1105 (T,wt=13): 20222 (x ^ c2) v (c1 ^ (y ^ x)) = x ^ c2. [para(390(a,1),112(a,1,2))]. given #1106 (T,wt=13): 20741 (c2 ^ x) v (y ^ (x ^ c1)) = c2 ^ x. [para(4(a,1),414(a,1,2,2))]. given #1107 (A,wt=15): 430 c1 v (x ^ c2') != 1 | (x ^ c2')' = c1. [para(161(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #1108 (T,wt=13): 20792 (x ^ (y ^ c1)) v (y ^ c2) = y ^ c2. [para(417(a,1),2(a,1)),flip(a)]. given #1109 (T,wt=13): 20836 x v (y v x)' != 1 | x v y = x. [para(2(a,1),426(a,1,2,1))]. given #1110 (T,wt=13): 20839 x v (x v y)' != 1 | y v x = x. [para(2(a,1),428(a,1,2,1))]. given #1111 (T,wt=13): 20840 c1 v (x v c2)' != 1 | c2 v x = c1. [para(2(a,1),434(a,1,2,1))]. given #1112 (A,wt=18): 431 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x)' = c1. [para(59(a,1),38(b,1)),rewrite(2(4))]. given #1113 (T,wt=13): 20844 c1 v (c2 v x)' != 1 | x v c2 = c1. [para(2(a,1),435(a,1,2,1))]. given #1114 (T,wt=13): 20846 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),438(a,1,1))]. given #1115 (T,wt=13): 20858 (x v c1) ^ (c2 v (y v x)) = x v c1. [para(2(a,1),444(a,1,2)),rewrite(3(5))]. given #1116 (T,wt=13): 20862 (x v c1) ^ (c2 v (x v y)) = x v c1. [para(17(a,1),444(a,1,2))]. given #1117 (A,wt=14): 432 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1. [para(213(a,1),38(b,1)),rewrite(2(4),120(4))]. given #1118 (T,wt=13): 21005 x v (c2 v ((c1 v x) ^ y)) = x v c2. [para(460(a,1),170(a,1)),rewrite(2(5),122(10))]. given #1119 (T,wt=13): 21669 (c1 v x) ^ (c2 v (y v x)) = c1 v x. [para(598(a,1),90(a,1,2))]. given #1120 (T,wt=13): 21764 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),1823(a,1,2))]. given #1121 (T,wt=13): 21766 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),1828(a,1,2))]. given #1122 (A,wt=14): 433 x v c2 != 1 | c1 != 0 | (x v c2)' = c1. [para(216(a,1),38(b,1)),rewrite(2(4),122(4))]. given #1123 (T,wt=13): 21769 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),1881(a,1,2))]. given #1124 (T,wt=13): 21771 (c2 v x) ^ c1' != 0 | x v c2 = c1. [para(2(a,1),1883(a,1,1))]. given #1125 (T,wt=13): 21773 c2' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(4(a,1),1970(a,1,2))]. given #1126 (T,wt=13): 21775 (c1 ^ x) v c2' != 1 | x ^ c1 = c2. [para(4(a,1),1971(a,1,1))]. given #1127 (A,wt=19): 436 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x. [para(34(a,1),38(b,1)),rewrite(2(4)),xx(b)]. given #1128 (T,wt=13): 21777 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),2037(a,1,2))]. given #1129 (T,wt=13): 21779 c2' v (x ^ c1) != 1 | c1 ^ x = c2. [para(4(a,1),2040(a,1,2))]. given #1130 (T,wt=13): 21787 c1 ^ (x ^ (y v (x ^ c2))) = c1 ^ x. [para(2226(a,1),59(a,1,2)),rewrite(59(4)),flip(a)]. given #1131 (T,wt=13): 22009 (x v (y v c2)) ^ (c1 v x) = x v c1. [para(122(a,1),2519(a,1,1,2))]. given #1132 (A,wt=18): 437 x v (y v z) != 1 | 0 != y | (x v (y v z))' = y. [para(62(a,1),38(b,1)),rewrite(2(3),287(3)),flip(b)]. given #1133 (T,wt=13): 22265 x ^ (c1 v (c2 ^ (x v y))) = x ^ c2. [para(3012(a,1),42(a,1,2)),rewrite(148(8)),flip(a)]. given #1134 (T,wt=13): 22266 x ^ (c1 v (c2 ^ (y v x))) = x ^ c2. [para(3012(a,1),44(a,1,2)),rewrite(397(8)),flip(a)]. given #1135 (T,wt=13): 22392 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(22305(a,1),24(a,1,2)),rewrite(2(3),63(4)),flip(a)]. given #1136 (T,wt=13): 22397 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(22305(a,1),110(a,1,2)),rewrite(2(3),115(4)),flip(a)]. given #1137 (A,wt=15): 439 (x ^ y) v y' != 1 | (x ^ y)' = y'. [para(320(a,1),38(b,1)),xx(b)]. given #1138 (T,wt=13): 22766 (x ^ (y ^ c1)) v (c2 ^ x) = x ^ c2. [para(60(a,1),3434(a,1,1,2))]. given #1139 (T,wt=13): 22831 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(80(a,1),3529(a,2)),rewrite(2(9),175(12))]. given #1140 (T,wt=13): 22832 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(112(a,1),3529(a,2)),rewrite(2(9),405(12))]. given #1141 (T,wt=13): 22901 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(19(a,1),22826(a,1,2))]. given #1142 (A,wt=18): 440 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2)' = c1. [para(83(a,1),38(b,1)),rewrite(2(4))]. given #1143 (T,wt=13): 22931 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(291(a,1),22826(a,1,2))]. given #1144 (T,wt=13): 22953 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(19(a,1),22827(a,1,2))]. given #1145 (T,wt=13): 22984 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(291(a,1),22827(a,1,2))]. given #1146 (T,wt=13): 23008 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(19(a,1),22899(a,1,2,2,2))]. given #1147 (A,wt=18): 441 x v (y v z) != 1 | 0 != z | (x v (y v z))' = z. [para(90(a,1),38(b,1)),rewrite(2(3),334(3)),flip(b)]. given #1148 (T,wt=13): 23036 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(291(a,1),22899(a,1,2,2,2))]. given #1149 (T,wt=13): 23104 (c1 ^ (x ^ y)) v (c2 ^ y) = c2 ^ y. [para(4(a,1),3552(a,1,1)),rewrite(5(3))]. given #1150 (T,wt=13): 23354 (c2 v (x v y)) ^ (y v c1) = y v c1. [para(2(a,1),4011(a,1,1,2))]. given #1151 (T,wt=13): 23590 (x ^ (c1 ^ y)) v (y ^ c2) = c2 ^ y. [para(4(a,1),4565(a,1,2))]. given #1152 (A,wt=24): 445 x v (c2 v y) != 1 | (x v c1) ^ (c2 v y) != 0 | (x v c1)' = c2 v y. [para(120(a,1),37(a,1,2))]. given #1153 (T,wt=13): 23599 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(53(a,1),4876(a,1,2)),rewrite(7480(6))]. given #1154 (T,wt=13): 23617 x ^ ((y ^ x) v (z ^ y)) = y ^ x. [para(2(a,1),5976(a,1,2))]. given #1155 (T,wt=13): 23618 x ^ ((y ^ z) v (y ^ x)) = y ^ x. [para(4(a,1),5976(a,1,2,1))]. given #1156 (T,wt=13): 23619 x ^ ((y ^ z) v (x ^ z)) = z ^ x. [para(4(a,1),5976(a,1,2,2))]. given #1157 (A,wt=18): 448 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(121(a,1),10(a,1))]. given #1158 (T,wt=13): 23624 c1 ^ ((x ^ y) v (y ^ c2)) = y ^ c1. [para(5976(a,1),59(a,1,2)),rewrite(83(4)),flip(a)]. given #1159 (T,wt=13): 23648 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),6129(a,1,2,1,1))]. given #1160 (T,wt=13): 23649 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),6129(a,1,2))]. given #1161 (T,wt=13): 23654 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(6129(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1162 (A,wt=24): 454 x v (y v c2) != 1 | (x v c2) ^ (y v c1) != 0 | (x v c2)' = y v c1. [para(121(a,1),37(a,1,2))]. given #1163 (T,wt=13): 23656 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(120(a,1),6129(a,1,2,1,1))]. given #1164 (T,wt=13): 23657 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(122(a,1),6129(a,1,2,1,1))]. given #1165 (T,wt=13): 23680 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),6155(a,1,2,1,1))]. given #1166 (T,wt=13): 23681 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),6155(a,1,2))]. given #1167 (A,wt=14): 455 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1. [para(121(a,1),37(a,1)),rewrite(4(8),213(8))]. given #1168 (T,wt=13): 23686 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(6155(a,1),59(a,1,2)),rewrite(13(3)),flip(a)]. given #1169 (T,wt=13): 23689 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(120(a,1),6155(a,1,2,1,1))]. given #1170 (T,wt=13): 23690 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(122(a,1),6155(a,1,2,1,1))]. given #1171 (T,wt=13): 23717 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(2(a,1),6165(a,1,2,1,1))]. given #1172 (A,wt=20): 456 x v (c2 v y) != 1 | c2 ^ (x v y) != 0 | (x v y)' = c2. [para(121(a,2),37(a,1,2)),rewrite(446(4),4(8))]. given #1173 (T,wt=13): 23718 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(2(a,1),6165(a,1,2))]. given #1174 (T,wt=13): 23724 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(122(a,1),6165(a,1,2,1,1))]. given #1175 (T,wt=13): 23737 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(2(a,1),6167(a,1,2,1,1))]. given #1176 (T,wt=13): 23738 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(2(a,1),6167(a,1,2))]. given #1177 (A,wt=24): 463 x v (y v c2) != 1 | (x v c1) ^ (y v c2) != 0 | (x v c1)' = y v c2. [para(122(a,1),37(a,1,2))]. given #1178 (T,wt=13): 23744 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(122(a,1),6167(a,1,2,1,1))]. given #1179 (T,wt=13): 23773 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(129(a,1),6209(a,1,2,2))]. given #1180 (T,wt=13): 23796 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(129(a,1),6246(a,1,2,2))]. given #1181 (T,wt=13): 23887 (c1 ^ (x ^ y)) v (y ^ c2) = c2 ^ y. [para(4(a,1),7522(a,1,1,2))]. given #1182 (A,wt=18): 464 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x)' = c2. [para(122(a,1),37(a,1)),rewrite(4(8))]. given #1183 (T,wt=13): 23908 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),9705(a,1,2,1,1))]. given #1184 (T,wt=13): 23909 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),9705(a,1,2))]. given #1185 (T,wt=13): 23913 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(60(a,1),9705(a,1,2,1,1))]. given #1186 (T,wt=13): 23942 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),9736(a,1,2,1,1))]. Low Water (displace, True_semantics): id=19988, wt=22 given #1187 (A,wt=18): 467 x v (c2 v y) != 1 | c1 != 0 | c1' = x v (c2 v y). [para(224(a,1),10(b,1)),rewrite(443(5))]. given #1188 (T,wt=13): 23943 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),9736(a,1,2))]. given #1189 (T,wt=13): 23948 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(60(a,1),9736(a,1,2,1,1))]. given #1190 (T,wt=13): 23973 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(4(a,1),9738(a,1,2,1,1))]. given #1191 (T,wt=13): 23974 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(4(a,1),9738(a,1,2))]. given #1192 (A,wt=18): 469 x v (c2 v y) != 1 | c1 != 0 | (x v (c2 v y))' = c1. [para(224(a,1),38(b,1)),rewrite(2(5),443(5))]. given #1193 (T,wt=13): 23978 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(60(a,1),9738(a,1,2,1,1))]. given #1194 (T,wt=13): 23993 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),9739(a,1,2,1))]. given #1195 (T,wt=13): 23995 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),9739(a,1,2,1,1))]. given #1196 (T,wt=13): 23996 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),9739(a,1,2))]. given #1197 (A,wt=20): 470 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x)' = z. [para(4(a,1),39(a,1,1))]. given #1198 (T,wt=13): 24000 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(60(a,1),9739(a,1,2,1,1))]. given #1199 (T,wt=13): 24113 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),15264(a,1,1))]. given #1200 (T,wt=13): 24116 (x ^ c1) v c2' != 1 | c1 ^ x = c2. [para(4(a,1),15266(a,1,1))]. given #1201 (T,wt=13): 24130 c1 ^ ((c2' ^ x) v (c2' ^ y)) = 0. [hyper(318,a,1293,a,b,15487,a(flip)),rewrite(15487(9),4(10),77(12),298(11),15487(18))]. given #1202 (A,wt=20): 471 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y)' = z. [para(4(a,1),39(b,1)),rewrite(5(6))]. given #1203 (T,wt=13): 24149 c1 ^ ((c2' ^ x) v (y ^ c2')) = 0. [hyper(318,a,1293,a,b,15511,a(flip)),rewrite(15511(9),4(10),77(12),298(11),15511(18))]. given #1204 (T,wt=13): 24171 c2 v ((c1' v x) ^ (c1' v y)) = 1. [para(15983(a,1),2089(a,1,2,2,1)),rewrite(84(10),2(10),77(10),2(9))]. given #1205 (T,wt=13): 24196 c2 v ((c1' v x) ^ (y v c1')) = 1. [para(16006(a,1),2089(a,1,2,2,1)),rewrite(84(10),2(10),77(10),2(9))]. given #1206 (T,wt=13): 24205 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),16203(a,1,1))]. given #1207 (A,wt=26): 472 (x ^ (y ^ z)) v u != 1 | x ^ (y ^ (z ^ u)) != 0 | (x ^ (y ^ z))' = u. [para(5(a,1),39(a,1,1)),rewrite(5(8),5(12))]. given #1208 (T,wt=13): 24208 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(2(a,1),16206(a,1,1))]. given #1209 (T,wt=13): 24229 c2 v ((x v c1') ^ (c1' v y)) = 1. [para(17348(a,1),2089(a,1,2,2,1)),rewrite(84(10),2(10),77(10),2(9))]. given #1210 (T,wt=13): 24248 c1 ^ ((x ^ c2') v (c2' ^ y)) = 0. [hyper(318,a,1293,a,b,17638,a(flip)),rewrite(17638(9),4(10),77(12),298(11),17638(18))]. given #1211 (T,wt=13): 24269 c2 v ((x v c1') ^ (y v c1')) = 1. [para(17920(a,1),2089(a,1,2,2,1)),rewrite(84(10),2(10),77(10),2(9))]. given #1212 (A,wt=18): 473 x v y != 1 | z ^ x != 0 | (z ^ x)' = x v y. [para(6(a,1),39(b,1,2)),rewrite(17(3),110(3))]. given #1213 (T,wt=13): 24289 c1 ^ ((x ^ c2') v (y ^ c2')) = 0. [hyper(318,a,1293,a,b,18626,a(flip)),rewrite(18626(9),4(10),77(12),298(11),18626(18))]. given #1214 (T,wt=13): 24494 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(176(a,1),22901(a,1,2,2))]. given #1215 (T,wt=13): 24506 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(176(a,1),22953(a,1,2,2))]. given #1216 (T,wt=13): 24536 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(4(a,1),23599(a,1,2,1))]. given #1217 (A,wt=26): 474 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z)' = x v u. [para(17(a,1),39(a,1))]. given #1218 (T,wt=13): 24537 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(4(a,1),23599(a,1,2,2))]. given #1219 (T,wt=13): 24546 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(4(a,1),23617(a,1,2,1))]. given #1220 (T,wt=13): 24547 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(4(a,1),23617(a,1,2,2))]. given #1221 (T,wt=13): 24567 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(4(a,1),23618(a,1,2,2))]. given #1222 (A,wt=18): 475 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x