============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27307 was started by mccune on cleo, Fri Apr 13 09:27:23 2007 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H7b.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 H7b.in assign(max_seconds,60). assign(max_weight,25). assign(constant_weight,0). assign(nest_penalty,2). formulas(sos). x ^ (y v (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7). 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 (x ^ z)) = x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) # label(H7). [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 (x ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)). [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]. 12 x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)). [copy(11),flip(a)]. 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=15): 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=15): 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=5): 8 x v x' = 1. [assumption]. given #8 (I,wt=5): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=12): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=23): 12 x ^ (y v (x ^ ((x ^ y) v (z ^ (x v y))))) = x ^ (y v (x ^ z)). [copy(11),flip(a)]. given #11 (I,wt=2): 13 c1 ^ c2 = c1. [deny(1)]. given #12 (I,wt=5): 15 c1' v c2' != c1'. [copy(14),flip(a)]. given #13 (A,wt=15): 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=4): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #15 (T,wt=4): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #16 (T,wt=4): 54 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #17 (T,wt=2): 60 1' = 0. [hyper(10,a,35,a,b,54,a)]. given #18 (A,wt=15): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #19 (T,wt=3): 61 1 v x = 1. [para(54(a,1),6(a,1))]. given #20 (T,wt=3): 70 x v 1 = 1. [para(61(a,1),2(a,1)),flip(a)]. given #21 (T,wt=2): 73 0' = 1. [hyper(10,a,70,a,b,32,a)]. given #22 (T,wt=4): 57 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #23 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #24 (T,wt=3): 74 0 ^ x = 0. [para(57(a,1),6(a,1,2))]. given #25 (T,wt=3): 85 x ^ 0 = 0. [para(74(a,1),4(a,1)),flip(a)]. given #26 (T,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #27 (T,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #28 (A,wt=15): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #29 (T,wt=5): 48 c1 v c2 != 1 | c1 != 0 | c1' = c2. [para(13(a,1),10(b,1))]. given #30 (T,wt=5): 49 c1 ^ (c2 v (c1 ^ x)) = c1. [para(13(a,1),12(a,1,2,2,2,1)),rewrite(6(10),2(4),6(5)),flip(a)]. given #31 (T,wt=5): 71 0 != x | x' = 1. [back_rewrite(55),rewrite(70(2)),xx(a)]. given #32 (T,wt=5): 88 1 != x | x' = 0. [back_rewrite(58),rewrite(85(4)),xx(b)]. given #33 (A,wt=13): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #34 (T,wt=5): 99 c1 ^ (c2 v (x ^ c1)) = c1. [para(4(a,1),49(a,1,2,2))]. given #35 (T,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #36 (T,wt=2): 120 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. given #37 (T,wt=4): 124 c2 v (c1 ^ x) = c2. [para(49(a,1),26(a,1,2)),rewrite(2(6),51(6),2(3),120(3)),flip(a)]. given #38 (A,wt=15): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #39 (T,wt=4): 126 c2 v (x ^ c1) = c2. [para(99(a,1),26(a,1,2)),rewrite(2(6),121(6),2(3),120(3)),flip(a)]. given #40 (T,wt=4): 127 c2 != 1 | c1 != 0 | c1' = c2. [back_rewrite(101),rewrite(120(3),124(12))]. given #41 (T,wt=7): 106 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(85(2)),flip(a)]. given #42 (T,wt=3): 155 c1 ^ c2' = 0. [para(120(a,1),106(a,1,2,1))]. given #43 (A,wt=13): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #44 (T,wt=6): 157 c1 v c2' != 1 | c2' = c1'. [para(155(a,1),10(b,1)),flip(c),xx(b)]. given #45 (T,wt=7): 148 x ^ (y v x)' = 0. [para(2(a,1),106(a,1,2,1))]. given #46 (T,wt=7): 156 c1 ^ (c2' ^ x) = 0. [para(155(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #47 (T,wt=7): 158 c1 ^ (x ^ c2') = 0. [para(155(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #48 (A,wt=15): 25 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #49 (T,wt=7): 161 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(70(2)),flip(a)]. given #50 (T,wt=7): 188 x v (y ^ x)' = 1. [para(4(a,1),161(a,1,2,1))]. given #51 (T,wt=3): 198 c2 v c1' = 1. [para(13(a,1),188(a,1,2,1))]. given #52 (T,wt=6): 205 c2 ^ c1' != 0 | c2' = c1'. [para(198(a,1),10(a,1)),xx(a)]. given #53 (A,wt=15): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #54 (T,wt=7): 204 c2 v (c1' v x) = 1. [para(198(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #55 (T,wt=7): 207 c2 v (x v c1') = 1. [para(198(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #56 (T,wt=8): 46 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #57 (T,wt=4): 221 c1 ^ (c2 v x) = c1. [para(6(a,1),46(a,1,2)),rewrite(13(3)),flip(a)]. given #58 (A,wt=11): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #59 (T,wt=4): 227 c1 ^ (x v c2) = c1. [para(20(a,1),46(a,1,2)),rewrite(13(3)),flip(a)]. given #60 (T,wt=5): 231 c1 ^ (c2 v x)' = 0. [para(106(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #61 (T,wt=5): 232 c1 ^ (x v c2)' = 0. [para(148(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #62 (T,wt=7): 233 (c2 ^ x) v (c1 ^ x)' = 1. [para(46(a,1),188(a,1,2,1))]. given #63 (A,wt=11): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #64 (T,wt=5): 270 c2 v (c1 ^ x)' = 1. [para(233(a,1),24(a,1,2)),rewrite(2(3),61(3)),flip(a)]. given #65 (T,wt=5): 280 c2 v (x ^ c1)' = 1. [para(4(a,1),270(a,1,2,1))]. given #66 (T,wt=6): 261 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),233(a,1,2,1))]. given #67 (T,wt=6): 267 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),233(a,1,2,1))]. given #68 (A,wt=12): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #69 (T,wt=4): 309 c2 != 1 | c1 != 0 | c2' = c1. [para(120(a,1),36(a,1)),rewrite(4(6),13(6))]. given #70 (T,wt=4): 316 c2 ^ c1' != 0 | c2 = c1. [para(198(a,1),36(a,1)),rewrite(4(7),304(12)),flip(c),xx(a)]. given #71 (T,wt=6): 290 c1' v (c2 ^ (c1 v x)) = 1. [para(261(a,1),2(a,1)),flip(a)]. given #72 (T,wt=6): 295 c1' v (c2 ^ (x v c1)) = 1. [para(267(a,1),2(a,1)),flip(a)]. given #73 (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 #74 (T,wt=7): 259 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),233(a,1,1))]. given #75 (T,wt=7): 260 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),233(a,1,2,1))]. given #76 (T,wt=7): 304 x'' = x. [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #77 (T,wt=7): 362 (x ^ c2) v (x ^ c1)' = 1. [para(4(a,1),259(a,1,2,1))]. given #78 (A,wt=12): 38 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #79 (T,wt=4): 387 c1 v c2' != 1 | c2 = c1. [para(155(a,1),38(b,1)),rewrite(2(4),304(12)),xx(b)]. given #80 (T,wt=8): 47 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite(4(4))]. given #81 (T,wt=7): 406 (x ^ c1) v (c1 ^ x)' = 1. [para(47(a,1),233(a,1,1)),rewrite(86(6))]. given #82 (T,wt=8): 69 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #83 (A,wt=20): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #84 (T,wt=8): 89 1 != x | 0 != x | x' = x. [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)]. given #85 (T,wt=8): 128 c1 v (c2 v x) = c2 v x. [para(120(a,1),3(a,1,1)),flip(a)]. given #86 (T,wt=8): 129 c2 v (x v c1) = x v c2. [para(120(a,1),3(a,2,2)),rewrite(2(4))]. given #87 (T,wt=7): 455 (x v c1) ^ (x v c2)' = 0. [para(129(a,1),148(a,1,2,1))]. given #88 (A,wt=23): 42 x ^ (y v (x ^ ((x ^ y) v (z ^ (y v x))))) = x ^ (y v (x ^ z)). [para(2(a,1),12(a,1,2,2,2,2,2))]. given #89 (T,wt=7): 463 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),455(a,1,1))]. given #90 (T,wt=7): 464 (x v c1) ^ (c2 v x)' = 0. [para(2(a,1),455(a,1,2,1))]. given #91 (T,wt=6): 494 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),464(a,1,2,1)),rewrite(2(4))]. given #92 (T,wt=6): 498 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),464(a,1,2,1)),rewrite(2(4))]. given #93 (A,wt=23): 43 x ^ (y v (x ^ ((y ^ x) v (z ^ (x v y))))) = x ^ (y v (x ^ z)). [para(4(a,1),12(a,1,2,2,2,1))]. given #94 (T,wt=6): 503 c2' ^ (c1 v (c2 ^ x)) = 0. [para(494(a,1),4(a,1)),flip(a)]. given #95 (T,wt=6): 511 c2' ^ (c1 v (x ^ c2)) = 0. [para(498(a,1),4(a,1)),flip(a)]. given #96 (T,wt=7): 484 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),463(a,1,2,1))]. given #97 (T,wt=8): 130 c1 v (x v c2) = x v c2. [para(120(a,1),17(a,1,2)),flip(a)]. given #98 (A,wt=23): 44 x ^ (y v (x ^ ((x ^ y) v ((x v y) ^ z)))) = x ^ (y v (x ^ z)). [para(4(a,1),12(a,1,2,2,2,2))]. given #99 (T,wt=8): 131 (x v c1) ^ (x v c2) = x v c1. [para(120(a,1),21(a,1,2,2))]. given #100 (T,wt=8): 133 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x. [para(124(a,1),10(a,1)),rewrite(19(7),46(7))]. given #101 (T,wt=3): 579 c2 != 1 | c2' = 0. [para(9(a,1),133(b,1)),rewrite(9(12)),xx(b)]. given #102 (T,wt=8): 136 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),124(a,1,2))]. given #103 (A,wt=11): 50 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #104 (T,wt=8): 144 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),126(a,1,2))]. given #105 (T,wt=8): 145 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1. [para(126(a,1),10(a,1)),rewrite(47(7))]. given #106 (T,wt=8): 229 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(46(a,1),26(a,1,2)),rewrite(2(5))]. given #107 (T,wt=8): 234 c2 v x != 1 | c1 != 0 | c1' = c2 v x. [para(221(a,1),10(b,1)),rewrite(128(4))]. given #108 (A,wt=13): 51 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #109 (T,wt=3): 627 c1 != 0 | c1' = 1. [para(8(a,1),234(a,1)),rewrite(8(12)),xx(a)]. given #110 (T,wt=8): 236 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),221(a,1,2))]. given #111 (T,wt=8): 245 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),227(a,1,2))]. given #112 (T,wt=8): 247 x v c2 != 1 | c1 != 0 | c1' = x v c2. [para(227(a,1),10(b,1)),rewrite(130(4))]. given #113 (A,wt=20): 53 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #114 (T,wt=8): 310 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2. [para(124(a,1),36(a,1)),rewrite(4(7),19(7),46(7))]. given #115 (T,wt=8): 311 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2. [para(126(a,1),36(a,1)),rewrite(4(7),47(7))]. given #116 (T,wt=8): 322 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2. [para(270(a,1),36(a,1)),rewrite(4(8),304(14)),xx(a)]. given #117 (T,wt=8): 323 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2. [para(280(a,1),36(a,1)),rewrite(4(8),304(14)),xx(a)]. given #118 (A,wt=11): 62 x v (x v y) = x v y. [para(54(a,1),12(a,1,2,2,2,1)),rewrite(61(4),32(4),54(4),54(4),54(5),54(5))]. given #119 (T,wt=8): 393 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1. [para(221(a,1),38(b,1)),rewrite(2(4),128(4))]. given #120 (T,wt=8): 394 x v c2 != 1 | c1 != 0 | (x v c2)' = c1. [para(227(a,1),38(b,1)),rewrite(2(4),130(4))]. given #121 (T,wt=8): 395 c1 v (c2 v x)' != 1 | c2 v x = c1. [para(231(a,1),38(b,1)),rewrite(2(5),304(14)),xx(b)]. given #122 (T,wt=8): 396 c1 v (x v c2)' != 1 | x v c2 = c1. [para(232(a,1),38(b,1)),rewrite(2(5),304(14)),xx(b)]. given #123 (A,wt=9): 63 x v (x' v y) = 1. [back_rewrite(30),rewrite(61(5))]. given #124 (F,wt=5): 704 c1 ^ (c1' v c2') != 0. [ur(38,a,63,a,c,15,a(flip)),rewrite(4(7))]. given #125 (T,wt=8): 405 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(47(a,1),27(a,1,2))]. given #126 (T,wt=8): 416 (x ^ c1) v (x ^ c2) = x ^ c2. [para(69(a,1),26(a,1,2)),rewrite(2(5))]. given #127 (T,wt=8): 417 (c1 ^ x) v (x ^ c1) = c1 ^ x. [para(69(a,1),27(a,1,2))]. given #128 (T,wt=8): 445 c2 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c2. [para(69(a,1),39(b,1)),rewrite(2(4),124(4))]. given #129 (A,wt=12): 64 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(40),rewrite(62(2))]. given #130 (T,wt=3): 753 c2 != 0 | c2' = 1. [para(198(a,1),64(a,1)),rewrite(198(12)),flip(b),xx(a)]. given #131 (T,wt=3): 754 c1' != 0 | c1 = 1. [para(290(a,1),64(a,1)),rewrite(304(10),290(15)),flip(b),xx(a)]. given #132 (T,wt=4): 752 c2 != 1 | c2 != 0 | c2' = c2. [para(124(a,1),64(a,1)),rewrite(124(12)),flip(b)]. given #133 (T,wt=8): 450 c2 v (x v c1) = c2 v x. [para(129(a,2),2(a,1))]. given #134 (A,wt=13): 65 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #135 (T,wt=8): 460 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1. [para(129(a,1),37(a,1)),rewrite(4(8),221(8))]. given #136 (T,wt=8): 552 (c1 v x) ^ (x v c2) = c1 v x. [para(130(a,1),21(a,1,2))]. given #137 (T,wt=8): 565 (x v c1) ^ (c2 v x) = x v c1. [para(2(a,1),131(a,1,2))]. given #138 (T,wt=8): 578 c2 != 1 | x ^ c1 != 0 | c2' = c1 ^ x. [para(4(a,1),133(b,1))]. given #139 (A,wt=11): 66 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #140 (T,wt=8): 606 c2 != 1 | c1 ^ x != 0 | c2' = x ^ c1. [para(4(a,1),145(b,1))]. given #141 (T,wt=8): 610 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),229(a,1,1))]. given #142 (T,wt=8): 611 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),229(a,1,2))]. given #143 (T,wt=8): 612 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),229(a,1,1))]. given #144 (A,wt=20): 68 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(19(a,1),10(b,1))]. given #145 (T,wt=6): 845 c1 ^ (c2 ^ (c1 v x))' = 0. [para(612(a,1),106(a,1,2,1))]. given #146 (T,wt=6): 885 c1 ^ (c2 ^ (x v c1))' = 0. [para(2(a,1),845(a,1,2,1,2))]. given #147 (T,wt=7): 848 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(612(a,1),50(a,1,2,2))]. given #148 (T,wt=7): 900 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),848(a,1,2,2,2))]. given #149 (A,wt=9): 72 x v (y v x') = 1. [back_rewrite(52),rewrite(70(5))]. given #150 (T,wt=7): 901 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(2(a,1),848(a,1,2))]. given #151 (T,wt=7): 914 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),900(a,1,2))]. given #152 (T,wt=8): 617 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(20(a,1),229(a,1,1))]. given #153 (T,wt=8): 626 x v c2 != 1 | c1 != 0 | c1' = c2 v x. [para(2(a,1),234(a,1))]. given #154 (A,wt=9): 75 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(74(5))]. given #155 (T,wt=8): 658 c2 v x != 1 | c1 != 0 | c1' = x v c2. [para(2(a,1),247(a,1))]. given #156 (T,wt=8): 671 c1' ^ (c2 v x) != 0 | c2 v x = c1. [para(204(a,1),53(a,1)),rewrite(304(13)),flip(c),xx(a)]. given #157 (T,wt=8): 690 c2 != 1 | c1 ^ x != 0 | (x ^ c1)' = c2. [para(4(a,1),311(b,1))]. given #158 (T,wt=8): 692 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),322(a,1,2,1))]. given #159 (A,wt=11): 76 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #160 (T,wt=8): 694 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),323(a,1,2,1))]. given #161 (T,wt=8): 698 c2 v x != 1 | c1 != 0 | (x v c2)' = c1. [para(2(a,1),394(a,1))]. given #162 (T,wt=8): 700 c1 v (x v c2)' != 1 | c2 v x = c1. [para(2(a,1),395(a,1,2,1))]. given #163 (T,wt=8): 702 c1 v (c2 v x)' != 1 | x v c2 = c1. [para(2(a,1),396(a,1,2,1))]. given #164 (A,wt=13): 77 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #165 (T,wt=8): 764 c2 v x != 1 | c2 != 0 | c2' = c2 v x. [para(450(a,1),64(a,1)),rewrite(450(13)),flip(b)]. given #166 (T,wt=8): 777 (c1 v x) ^ (c2 v x) = c1 v x. [para(2(a,1),552(a,1,2))]. given #167 (T,wt=8): 778 (x v c2) ^ (c1 v x) = c1 v x. [para(552(a,1),4(a,1)),flip(a)]. given #168 (T,wt=8): 793 (c2 v x) ^ (x v c1) = x v c1. [para(565(a,1),4(a,1)),flip(a)]. given #169 (A,wt=15): 78 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #170 (T,wt=8): 795 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(7(a,1),565(a,1,2)),rewrite(2(4),4(6),2(10))]. given #171 (T,wt=6): 1066 c2 v (c1 v (c2 ^ x))' = 1. [para(795(a,1),161(a,1,2,1))]. given #172 (T,wt=6): 1075 c2 v (c1 v (x ^ c2))' = 1. [para(4(a,1),1066(a,1,2,1,2))]. given #173 (T,wt=7): 1072 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(795(a,1),66(a,1,2,2))]. given #174 (A,wt=11): 79 x ^ (x ^ y) = x ^ y. [para(7(a,1),20(a,1,2)),rewrite(4(2))]. given #175 (T,wt=7): 1092 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),1072(a,1,2,2,2))]. given #176 (T,wt=7): 1093 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(4(a,1),1072(a,1,2))]. given #177 (T,wt=7): 1110 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(4(a,1),1092(a,1,2))]. given #178 (T,wt=8): 801 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(26(a,1),565(a,1,2)),rewrite(2(4),4(6),2(10))]. given #179 (A,wt=15): 81 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #180 (T,wt=8): 827 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(611(a,1),2(a,1)),flip(a)]. given #181 (T,wt=8): 859 c2' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(156(a,1),68(b,1)),rewrite(304(13)),flip(c),xx(b)]. given #182 (T,wt=3): 1193 c2' != 1 | c2 = 0. [para(9(a,1),859(a,1,2)),rewrite(2(4),57(4),9(8)),flip(b)]. given #183 (T,wt=8): 977 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),671(a,1,2))]. given #184 (A,wt=13): 82 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #185 (T,wt=7): 1207 c2' ^ (x ^ c2) = 0. [para(511(a,1),82(a,1,2)),rewrite(4(4),74(4)),flip(a)]. given #186 (T,wt=8): 978 (c2 v x) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),671(a,1))]. given #187 (T,wt=8): 981 c1' ^ (x v c2) != 0 | x v c2 = c1. [para(51(a,1),671(a,1,2)),rewrite(51(12))]. given #188 (T,wt=8): 1016 x v c2 != 1 | c2 != 0 | c2' = c2 v x. [para(2(a,1),764(a,1))]. given #189 (A,wt=12): 84 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(41),rewrite(79(4))]. given #190 (T,wt=3): 1228 c1 != 1 | c1' = 0. [para(155(a,1),84(b,1)),rewrite(155(12)),flip(a),xx(b)]. given #191 (T,wt=4): 1226 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),84(b,1)),rewrite(13(11)),flip(a)]. given #192 (T,wt=8): 1018 x v c2 != 1 | c2 != 0 | c2' = x v c2. [para(51(a,1),764(a,1)),rewrite(51(14))]. given #193 (T,wt=8): 1157 x ^ (c1 v (c2 ^ x)) = x ^ c2. [para(801(a,1),42(a,1,2,2,2,2)),rewrite(4(9),69(9),17(12),416(11),20(10),20(7),4(9),86(9),5(9),795(8)),flip(a)]. given #194 (A,wt=11): 86 x ^ (y ^ x) = x ^ y. [back_rewrite(83),rewrite(85(2),57(3))]. given #195 (T,wt=8): 1159 x ^ (c1 v (x ^ c2)) = x ^ c2. [para(801(a,1),78(a,1,2))]. given #196 (T,wt=8): 1191 (c1 ^ x) v c2' != 1 | c1 ^ x = c2. [para(2(a,1),859(a,1))]. given #197 (T,wt=8): 1192 c2' v (x ^ c1) != 1 | c1 ^ x = c2. [para(4(a,1),859(a,1,2))]. given #198 (T,wt=8): 1195 c2' v (x ^ c1) != 1 | x ^ c1 = c2. [para(69(a,1),859(a,1,2)),rewrite(69(11))]. given #199 (A,wt=9): 87 x ^ (y ^ x') = 0. [back_rewrite(67),rewrite(85(5))]. given #200 (T,wt=8): 1197 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),977(a,1))]. given #201 (T,wt=8): 1214 c2' v (x ^ c2) != 1 | x ^ c2 = c2. [para(1207(a,1),10(b,1)),rewrite(304(13)),flip(c),xx(b)]. given #202 (T,wt=8): 1216 (x ^ c2) v c2' != 1 | x ^ c2 = c2. [para(1207(a,1),36(b,1)),rewrite(304(13)),flip(c),xx(b)]. given #203 (T,wt=8): 1222 (x v c2) ^ c1' != 0 | x v c2 = c1. [para(51(a,1),978(a,1,1)),rewrite(51(12))]. given #204 (A,wt=11): 91 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite(2(2))]. given #205 (T,wt=8): 1223 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),981(a,1,2))]. given #206 (T,wt=8): 1229 c1 != 1 | c1 ^ x != 0 | c1' = c1 ^ x. [para(46(a,1),84(b,1)),rewrite(46(13)),flip(a)]. given #207 (T,wt=8): 1230 c1 != 1 | x ^ c1 != 0 | c1' = x ^ c1. [para(69(a,1),84(b,1)),rewrite(69(13)),flip(a)]. given #208 (T,wt=8): 1231 c2 v x != 1 | c2 != 0 | c2' = x v c2. [para(2(a,1),1018(a,1))]. given #209 (A,wt=12): 93 x v y != 1 | 0 != y | y' = x v y. [back_rewrite(80),rewrite(91(2))]. given #210 (T,wt=5): 1289 x' != 0 | 1 = x. [para(8(a,1),93(a,1)),rewrite(304(8),8(8)),flip(b),flip(c),xx(a)]. given #211 (T,wt=8): 1261 (x ^ c1) v c2' != 1 | c1 ^ x = c2. [para(4(a,1),1191(a,1,1))]. given #212 (T,wt=8): 1263 (x ^ c1) v c2' != 1 | x ^ c1 = c2. [para(69(a,1),1191(a,1,1)),rewrite(69(11))]. given #213 (T,wt=8): 1265 c2' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(4(a,1),1195(a,1,2))]. given #214 (A,wt=15): 94 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #215 (T,wt=8): 1277 c2' v (c2 ^ x) != 1 | x ^ c2 = c2. [para(4(a,1),1214(a,1,2))]. given #216 (T,wt=8): 1279 (c2 ^ x) v c2' != 1 | x ^ c2 = c2. [para(4(a,1),1216(a,1,1))]. given #217 (T,wt=8): 1281 (c2 v x) ^ c1' != 0 | x v c2 = c1. [para(2(a,1),1222(a,1,1))]. given #218 (T,wt=8): 1284 c1 != 1 | x ^ c1 != 0 | c1' = c1 ^ x. [para(4(a,1),1229(b,1))]. given #219 (A,wt=15): 95 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite(3(3))]. given #220 (T,wt=7): 1335 c1' v (x v c2) = 1. [para(198(a,1),95(a,1,1)),rewrite(54(7),198(9))]. given #221 (T,wt=8): 1286 c1 != 1 | c1 ^ x != 0 | c1' = x ^ c1. [para(4(a,1),1230(b,1))]. given #222 (T,wt=8): 1299 (c1 ^ x) v c2' != 1 | x ^ c1 = c2. [para(4(a,1),1263(a,1,1))]. given #223 (T,wt=8): 1321 (c2 ^ x) v c2' != 1 | c2 ^ x = c2. [para(22(a,1),1279(a,1,1)),rewrite(4(12),22(12))]. given #224 (A,wt=21): 96 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #225 (T,wt=8): 1366 (x ^ c2) v c2' != 1 | c2 ^ x = c2. [para(4(a,1),1321(a,1,1))]. given #226 (T,wt=8): 1394 c2' v (x ^ c2) != 1 | c2 ^ x = c2. [para(2(a,1),1366(a,1))]. given #227 (T,wt=9): 250 c1 ^ ((c2 v x)' ^ y) = 0. [para(231(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #228 (T,wt=9): 252 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),231(a,1,2,1))]. given #229 (A,wt=19): 97 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #230 (T,wt=9): 253 c1 ^ (x ^ (c2 v y)') = 0. [para(231(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #231 (T,wt=9): 254 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),232(a,1,2,1))]. given #232 (T,wt=9): 255 c1 ^ ((x v c2)' ^ y) = 0. [para(232(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #233 (T,wt=9): 257 c1 ^ (x ^ (y v c2)') = 0. [para(232(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #234 (A,wt=21): 98 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #235 (T,wt=9): 278 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #236 (T,wt=9): 279 c2 v ((c1 ^ x)' v y) = 1. [para(270(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #237 (T,wt=9): 283 c2 v (x v (c1 ^ y)') = 1. [para(270(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #238 (T,wt=9): 284 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),270(a,1,2,1))]. given #239 (A,wt=23): 105 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(22(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #240 (T,wt=9): 285 c2 v ((x ^ c1)' v y) = 1. [para(280(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #241 (T,wt=9): 286 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),280(a,1,2,1))]. given #242 (T,wt=9): 289 c2 v (x v (y ^ c1)') = 1. [para(280(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #243 (T,wt=9): 338 x v y != 0 | (x v y)' = 1. [para(32(a,1),37(b,1)),rewrite(70(2),70(2)),xx(a)]. given #244 (A,wt=20): 107 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(22(a,1),10(b,1))]. given #245 (T,wt=8): 1585 c2 != 1 | c2 ^ x != 0 | c2' = c2 ^ x. [para(124(a,1),107(a,1,2,1)),rewrite(7(4),124(13))]. given #246 (T,wt=8): 1596 c1 v x != 1 | c1 != 0 | c1' = c1 v x. [para(552(a,1),107(a,1,2)),rewrite(62(4),227(8),552(14))]. given #247 (T,wt=8): 1609 c2 != 1 | x ^ c2 != 0 | c2' = c2 ^ x. [para(4(a,1),1585(b,1))]. given #248 (T,wt=8): 1611 c2 != 1 | x ^ c2 != 0 | c2' = x ^ c2. [para(65(a,1),1585(b,1)),rewrite(65(14))]. given #249 (A,wt=17): 108 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),22(a,1,2,1))]. given #250 (T,wt=8): 1612 x v c1 != 1 | c1 != 0 | c1' = c1 v x. [para(2(a,1),1596(a,1))]. given #251 (T,wt=8): 1614 x v c1 != 1 | c1 != 0 | c1' = x v c1. [para(51(a,1),1596(a,1)),rewrite(51(14))]. given #252 (T,wt=8): 1616 c2 != 1 | c2 ^ x != 0 | c2' = x ^ c2. [para(4(a,1),1611(b,1))]. given #253 (T,wt=8): 1639 c1 v x != 1 | c1 != 0 | c1' = x v c1. [para(2(a,1),1614(a,1))]. given #254 (A,wt=21): 109 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(22(a,1),19(a,1,2)),flip(a)]. given #255 (T,wt=9): 339 x v y != 1 | (x v y)' = 0. [para(35(a,1),37(a,1,2)),rewrite(4(6),74(6)),xx(b)]. given #256 (T,wt=9): 423 x ^ y != 0 | (x ^ y)' = 1. [para(32(a,1),39(b,1,2)),rewrite(2(3),61(3)),xx(a)]. given #257 (T,wt=9): 424 x ^ y != 1 | (x ^ y)' = 0. [para(35(a,1),39(a,1)),rewrite(85(5),85(5)),xx(b)]. given #258 (T,wt=9): 573 x v (c2 v (x v c1)') = 1. [para(131(a,1),188(a,1,2,1)),rewrite(3(6))]. given #259 (A,wt=13): 115 x v ((y ^ x) v z) = x v z. [para(26(a,1),3(a,1,1)),flip(a)]. given #260 (T,wt=9): 718 x ^ (c1 ^ (c2 ^ x)') = 0. [para(405(a,1),148(a,1,2,1)),rewrite(5(6))]. given #261 (T,wt=9): 734 x ^ (c1 ^ (x ^ c2)') = 0. [para(416(a,1),106(a,1,2,1)),rewrite(5(6))]. given #262 (T,wt=9): 786 x v (c2 v (c1 v x)') = 1. [para(552(a,1),188(a,1,2,1)),rewrite(3(6))]. given #263 (T,wt=9): 787 c2 v (x v (c1 v x)') = 1. [para(31(a,1),552(a,1,1)),rewrite(2(7),54(8),31(12))]. given #264 (A,wt=15): 116 x v (y v (z ^ (x v y))) = x v y. [para(26(a,1),3(a,1)),flip(a)]. given #265 (T,wt=8): 1795 x v (c2 ^ (x v c1)) = x v c1. [para(617(a,1),116(a,1,2))]. given #266 (T,wt=7): 1818 c1 v c2' != 1 | c2 ^ (c1 v c2') = c2. [para(1795(a,1),1277(a,1)),rewrite(2(4),2(10),4(12))]. given #267 (T,wt=8): 1804 x v (c2 ^ (c1 v x)) = x v c1. [para(2(a,1),1795(a,1,2,2))]. given #268 (T,wt=9): 804 c2 v (x v (x v c1)') = 1. [para(565(a,1),188(a,1,2,1)),rewrite(3(6))]. given #269 (A,wt=11): 117 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #270 (T,wt=9): 908 (c2 ^ (x v (c2 ^ (c1 v y)))) v c1' = 1. [para(848(a,1),233(a,1,2,1))]. given #271 (T,wt=9): 923 (c2 ^ (x v (c2 ^ (y v c1)))) v c1' = 1. [para(900(a,1),233(a,1,2,1))]. given #272 (T,wt=9): 934 x' v (y v x) = 1. [para(304(a,1),72(a,1,2,2))]. given #273 (T,wt=8): 1912 c2 v (x ^ (c1 v (c2 ^ y)))' = 1. [para(1072(a,1),934(a,1,2)),rewrite(2(8))]. given #274 (A,wt=12): 118 1 != x | x ^ y != 0 | x' = y ^ x. [para(26(a,1),10(a,1)),rewrite(86(4)),flip(a)]. given #275 (T,wt=8): 1913 c2 v (x ^ (c1 v (y ^ c2)))' = 1. [para(1092(a,1),934(a,1,2)),rewrite(2(8))]. given #276 (T,wt=8): 1914 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1. [para(1093(a,1),934(a,1,2)),rewrite(2(8))]. given #277 (T,wt=8): 1915 c2 v ((c1 v (x ^ c2)) ^ y)' = 1. [para(1110(a,1),934(a,1,2)),rewrite(2(8))]. given #278 (T,wt=9): 942 (c2 ^ ((c2 ^ (c1 v x)) v y)) v c1' = 1. [para(901(a,1),233(a,1,2,1))]. given #279 (A,wt=25): 119 x ^ ((y ^ x) v (x ^ ((x ^ y) v (z ^ x)))) = x ^ ((y ^ x) v (x ^ z)). [para(26(a,1),12(a,1,2,2,2,2,2)),rewrite(86(3))]. given #280 (T,wt=9): 953 (c2 ^ ((c2 ^ (x v c1)) v y)) v c1' = 1. [para(914(a,1),233(a,1,2,1))]. given #281 (T,wt=9): 1100 (c1 v (x ^ (c1 v (c2 ^ y)))) ^ c2' = 0. [para(1072(a,1),464(a,1,2,1)),rewrite(2(7))]. given #282 (T,wt=9): 1120 (c1 v (x ^ (c1 v (y ^ c2)))) ^ c2' = 0. [para(1092(a,1),464(a,1,2,1)),rewrite(2(7))]. given #283 (T,wt=9): 1132 (c1 v ((c1 v (c2 ^ x)) ^ y)) ^ c2' = 0. [para(1093(a,1),464(a,1,2,1)),rewrite(2(7))]. given #284 (A,wt=13): 121 x v (y v (z ^ x)) = y v x. [para(26(a,1),17(a,1,2)),flip(a)]. given #285 (T,wt=9): 1146 (c1 v ((c1 v (x ^ c2)) ^ y)) ^ c2' = 0. [para(1110(a,1),464(a,1,2,1)),rewrite(2(7))]. given #286 (T,wt=9): 1250 (x ^ y) v (y ^ x)' = 1. [para(86(a,1),188(a,1,2,1))]. given #287 (T,wt=9): 1269 x' ^ (y ^ x) = 0. [para(304(a,1),87(a,1,2,2))]. given #288 (T,wt=5): 2088 x' != 1 | 0 = x. [para(1269(a,1),84(b,1)),rewrite(304(8),1269(9)),flip(a),flip(c),xx(b)]. given #289 (A,wt=15): 122 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(19(a,1),26(a,1,2))]. given #290 (F,wt=6): 2095 (c1 ^ (c1' v c2'))' != 1. [ur(2088,b,704,a(flip))]. given #291 (T,wt=8): 2082 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(848(a,1),1269(a,1,2)),rewrite(4(8))]. given #292 (T,wt=8): 2083 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(900(a,1),1269(a,1,2)),rewrite(4(8))]. given #293 (T,wt=8): 2084 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(901(a,1),1269(a,1,2)),rewrite(4(8))]. given #294 (T,wt=8): 2085 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(914(a,1),1269(a,1,2)),rewrite(4(8))]. given #295 (A,wt=15): 125 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(22(a,1),26(a,1,2)),rewrite(2(4))]. given #296 (T,wt=8): 2196 c1 ^ ((c2 v x) ^ (c1 v y))' = 0. [para(125(a,1),2084(a,1,2,1))]. given #297 (T,wt=8): 2197 c1 ^ ((c2 v x) ^ (y v c1))' = 0. [para(125(a,1),2085(a,1,2,1))]. given #298 (T,wt=8): 2208 c1 ^ ((x v c2) ^ (c1 v y))' = 0. [para(2(a,1),2196(a,1,2,1,1))]. given #299 (T,wt=8): 2209 c1 ^ ((c1 v x) ^ (c2 v y))' = 0. [para(4(a,1),2196(a,1,2,1))]. given #300 (A,wt=10): 132 c2 v ((c1 ^ x) v y) = c2 v y. [para(124(a,1),3(a,1,1)),flip(a)]. given #301 (T,wt=8): 2217 c1 ^ ((c2 v x) ^ (c2 v y))' = 0. [para(128(a,1),2196(a,1,2,1,2))]. given #302 (T,wt=8): 2218 c1 ^ ((c2 v x) ^ (y v c2))' = 0. [para(130(a,1),2196(a,1,2,1,2))]. given #303 (T,wt=8): 2220 c1 ^ ((x v c2) ^ (y v c1))' = 0. [para(2(a,1),2197(a,1,2,1,1))]. given #304 (T,wt=8): 2222 c1 ^ ((x v c1) ^ (c2 v y))' = 0. [para(4(a,1),2197(a,1,2,1))]. given #305 (A,wt=17): 134 c2 ^ ((c1 ^ x) v (c2 ^ ((c1 ^ x) v (y ^ c2)))) = c2 ^ ((c1 ^ x) v (c2 ^ y)). [para(124(a,1),12(a,1,2,2,2,2,2)),rewrite(19(8),46(8))]. given #306 (T,wt=8): 2231 c1 ^ ((c1 v x) ^ (y v c2))' = 0. [para(4(a,1),2208(a,1,2,1))]. given #307 (T,wt=8): 2238 c1 ^ ((x v c2) ^ (c2 v y))' = 0. [para(128(a,1),2208(a,1,2,1,2))]. given #308 (T,wt=8): 2239 c1 ^ ((x v c2) ^ (y v c2))' = 0. [para(130(a,1),2208(a,1,2,1,2))]. given #309 (T,wt=8): 2285 c1 ^ ((x v c1) ^ (y v c2))' = 0. [para(4(a,1),2220(a,1,2,1))]. given #310 (A,wt=10): 135 c2 v (x v (c1 ^ y)) = x v c2. [para(124(a,1),17(a,1,2)),flip(a)]. given #311 (T,wt=9): 1293 (x ^ y)' != 0 | x ^ y = 1. [para(161(a,1),93(a,1)),rewrite(304(10),161(11)),flip(b),xx(a)]. given #312 (T,wt=9): 1340 (c1 ^ x)' v (y v c2) = 1. [para(270(a,1),95(a,1,1)),rewrite(54(8),270(11))]. given #313 (T,wt=9): 1341 (x ^ c1)' v (y v c2) = 1. [para(280(a,1),95(a,1,1)),rewrite(54(8),280(11))]. given #314 (T,wt=9): 1490 c1 ^ (x ^ (x ^ c2)') = 0. [para(4(a,1),278(a,1,2,2,1))]. given #315 (A,wt=15): 137 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),23(a,1,2,2,1))]. given #316 (T,wt=9): 1578 x v y != 0 | (y v x)' = 1. [para(2(a,1),338(a,1))]. given #317 (T,wt=9): 1673 x v y != 1 | (y v x)' = 0. [para(2(a,1),339(a,1))]. given #318 (T,wt=9): 1675 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),423(a,1))]. given #319 (T,wt=9): 1677 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),424(a,1))]. given #320 (A,wt=24): 138 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 #321 (T,wt=7): 2428 c2 ^ c1' != 0 | c1 v (c2 ^ c1') = c1. [para(295(a,1),138(a,1)),rewrite(4(7),304(12),4(15),2(17),795(18)),flip(c),xx(a)]. given #322 (T,wt=9): 1878 c1' v (c2 ^ (x v (c2 ^ (c1 v y)))) = 1. [para(908(a,1),2(a,1)),flip(a)]. given #323 (T,wt=9): 1891 c1' v (c2 ^ (x v (c2 ^ (y v c1)))) = 1. [para(923(a,1),2(a,1)),flip(a)]. given #324 (T,wt=9): 1961 c1' v (c2 ^ ((c2 ^ (c1 v x)) v y)) = 1. [para(942(a,1),2(a,1)),flip(a)]. given #325 (A,wt=19): 139 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(17(a,1),23(a,1,2,2))]. given #326 (T,wt=9): 1984 c1' v (c2 ^ ((c2 ^ (x v c1)) v y)) = 1. [para(953(a,1),2(a,1)),flip(a)]. given #327 (T,wt=9): 1997 c2' ^ (c1 v (x ^ (c1 v (c2 ^ y)))) = 0. [para(1100(a,1),4(a,1)),flip(a)]. given #328 (T,wt=9): 2008 c2' ^ (c1 v (x ^ (c1 v (y ^ c2)))) = 0. [para(1120(a,1),4(a,1)),flip(a)]. given #329 (T,wt=9): 2019 c2' ^ (c1 v ((c1 v (c2 ^ x)) ^ y)) = 0. [para(1132(a,1),4(a,1)),flip(a)]. given #330 (A,wt=23): 140 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(23(a,1),19(a,1,2)),flip(a)]. given #331 (T,wt=9): 2052 c2' ^ (c1 v ((c1 v (x ^ c2)) ^ y)) = 0. [para(1146(a,1),4(a,1)),flip(a)]. given #332 (T,wt=9): 2252 ((c1 ^ x) v y) ^ (c2 v y)' = 0. [para(132(a,1),148(a,1,2,1))]. given #333 (T,wt=8): 2613 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0. [para(7(a,1),2252(a,1,2,1))]. given #334 (T,wt=8): 2619 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),2252(a,1,2,1))]. given #335 (A,wt=17): 141 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=8): 2620 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(124(a,1),2252(a,1,2,1))]. given #337 (T,wt=8): 2621 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0. [para(126(a,1),2252(a,1,2,1))]. given #338 (T,wt=8): 2648 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(2(a,1),2613(a,1,1))]. given #339 (T,wt=8): 2649 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(2613(a,1),4(a,1)),flip(a)]. given #340 (A,wt=19): 142 (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 #341 (T,wt=8): 2650 ((x ^ c1) v (c2 ^ y)) ^ c2' = 0. [para(4(a,1),2613(a,1,1,1))]. given #342 (T,wt=8): 2665 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0. [para(2(a,1),2619(a,1,1))]. given #343 (T,wt=8): 2666 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(2619(a,1),4(a,1)),flip(a)]. given #344 (T,wt=8): 2667 ((x ^ c1) v (y ^ c2)) ^ c2' = 0. [para(4(a,1),2619(a,1,1,1))]. given #345 (A,wt=10): 143 c2 v ((x ^ c1) v y) = c2 v y. [para(126(a,1),3(a,1,1)),flip(a)]. given #346 (T,wt=8): 2715 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(2620(a,1),4(a,1)),flip(a)]. given #347 (T,wt=8): 2716 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0. [para(4(a,1),2620(a,1,1,1))]. given #348 (T,wt=8): 2730 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(2621(a,1),4(a,1)),flip(a)]. given #349 (T,wt=7): 2900 c2' ^ (x ^ c1) = 0. [para(9(a,1),2730(a,1,2,1)),rewrite(57(6))]. given #350 (A,wt=17): 146 c2 ^ ((x ^ c1) v (c2 ^ ((x ^ c1) v (y ^ c2)))) = c2 ^ ((x ^ c1) v (c2 ^ y)). [para(126(a,1),12(a,1,2,2,2,2,2)),rewrite(47(8))]. given #351 (T,wt=8): 2731 ((x ^ c1) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2621(a,1,1,1))]. given #352 (T,wt=8): 2745 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(2648(a,1),4(a,1)),flip(a)]. given #353 (T,wt=8): 2746 ((c2 ^ x) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2648(a,1,1,2))]. given #354 (T,wt=8): 2760 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(4(a,1),2649(a,1,2,1))]. given #355 (A,wt=10): 147 c2 v (x v (y ^ c1)) = x v c2. [para(126(a,1),17(a,1,2)),flip(a)]. given #356 (T,wt=8): 2818 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(2665(a,1),4(a,1)),flip(a)]. given #357 (T,wt=8): 2819 ((x ^ c2) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2665(a,1,1,2))]. given #358 (T,wt=8): 2833 c2' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(4(a,1),2666(a,1,2,1))]. given #359 (T,wt=8): 2875 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(4(a,1),2715(a,1,2,1))]. given #360 (A,wt=13): 149 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),106(a,1,2,1))]. given #361 (T,wt=8): 2898 c2' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(4(a,1),2730(a,1,2,1))]. given #362 (T,wt=8): 2944 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(4(a,1),2745(a,1,2,2))]. given #363 (T,wt=8): 2989 c2' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(4(a,1),2818(a,1,2,2))]. given #364 (T,wt=9): 2348 (x v (c1 ^ y)) ^ (x v c2)' = 0. [para(135(a,1),148(a,1,2,1))]. given #365 (A,wt=11): 150 x ^ ((x v y)' ^ z) = 0. [para(106(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #366 (T,wt=9): 2360 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),1293(a,1,1))]. given #367 (T,wt=9): 2362 (x v y)' != 0 | x v y = 1. [para(21(a,1),1293(a,1,1)),rewrite(21(8))]. given #368 (T,wt=3): 3099 c2' != 0 | c2 = 1. [para(120(a,1),2362(a,1,1)),rewrite(120(7))]. given #369 (T,wt=9): 2608 (x v (c1 ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),2252(a,1,1))]. given #370 (A,wt=13): 151 x ^ (y ^ ((x ^ y) v z)') = 0. [para(106(a,1),5(a,1)),flip(a)]. given #371 (T,wt=9): 2609 ((c1 ^ x) v y) ^ (y v c2)' = 0. [para(2(a,1),2252(a,1,2,1))]. given #372 (T,wt=9): 2610 (c2 v x)' ^ ((c1 ^ y) v x) = 0. [para(2252(a,1),4(a,1)),flip(a)]. given #373 (T,wt=7): 3179 (c2 v x)' != 1 | c2 v x = 0. [para(2610(a,1),84(b,1)),rewrite(304(12),2610(17)),flip(a),xx(b)]. given #374 (T,wt=7): 3190 (x v c2)' != 1 | c2 v x = 0. [para(2(a,1),3179(a,1,1))]. given #375 (A,wt=14): 152 x v (x v y)' != 1 | (x v y)' = x'. [para(106(a,1),10(b,1)),flip(c),xx(b)]. given #376 (T,wt=3): 3196 c1' != 1 | c1 = 0. [para(290(a,1),152(a,1,2,1)),rewrite(60(4),2(4),57(4),290(11),60(6),304(8)),flip(b)]. given #377 (T,wt=7): 3192 (x v c2)' != 1 | x v c2 = 0. [para(51(a,1),3179(a,1,1)),rewrite(51(10))]. given #378 (T,wt=7): 3198 (c1 ^ x)' != 1 | c1 ^ x = 0. [para(1340(a,1),152(a,1,2,1)),rewrite(60(5),2(5),57(5),1340(11),60(7),304(10)),flip(b)]. given #379 (T,wt=7): 3199 (x ^ c1)' != 1 | x ^ c1 = 0. [para(1341(a,1),152(a,1,2,1)),rewrite(60(5),2(5),57(5),1341(11),60(7),304(10)),flip(b)]. given #380 (A,wt=11): 153 x ^ (y v (x v z))' = 0. [para(17(a,1),106(a,1,2,1))]. given #381 (T,wt=7): 3200 (c2 v x)' != 1 | x v c2 = 0. [para(2(a,1),3192(a,1,1))]. given #382 (T,wt=7): 3201 (x ^ c1)' != 1 | c1 ^ x = 0. [para(4(a,1),3198(a,1,1))]. given #383 (T,wt=7): 3204 (c1 ^ x)' != 1 | x ^ c1 = 0. [para(4(a,1),3199(a,1,1))]. given #384 (T,wt=9): 2611 ((x ^ c1) v y) ^ (c2 v y)' = 0. [para(4(a,1),2252(a,1,1,1))]. given #385 (A,wt=11): 154 x ^ (y ^ (x v z)') = 0. [para(106(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #386 (T,wt=9): 2977 (x v (y ^ c1)) ^ (x v c2)' = 0. [para(147(a,1),148(a,1,2,1))]. given #387 (T,wt=9): 3036 (x v y) ^ (y v x)' = 0. [para(51(a,1),149(a,1,2,1))]. given #388 (T,wt=9): 3077 (x v c2)' ^ (x v (c1 ^ y)) = 0. [para(2348(a,1),4(a,1)),flip(a)]. given #389 (T,wt=9): 3097 (x v y)' != 0 | y v x = 1. [para(2(a,1),2362(a,1,1))]. given #390 (A,wt=23): 159 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 #391 (T,wt=9): 3101 (c2 v x)' ^ (x v (c1 ^ y)) = 0. [para(2608(a,1),4(a,1)),flip(a)]. given #392 (T,wt=9): 3102 (x v (y ^ c1)) ^ (c2 v x)' = 0. [para(4(a,1),2608(a,1,1,2))]. given #393 (T,wt=9): 3150 (x v c2)' ^ ((c1 ^ y) v x) = 0. [para(2609(a,1),4(a,1)),flip(a)]. given #394 (T,wt=9): 3151 ((x ^ c1) v y) ^ (y v c2)' = 0. [para(4(a,1),2609(a,1,1,1))]. given #395 (A,wt=21): 160 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),24(a,1,2,1))]. given #396 (T,wt=9): 3164 (c2 v x)' ^ ((y ^ c1) v x) = 0. [para(4(a,1),2610(a,1,2,1))]. given #397 (T,wt=9): 3258 (x v c2)' ^ (x v (y ^ c1)) = 0. [para(2977(a,1),4(a,1)),flip(a)]. given #398 (T,wt=9): 3330 (c2 v x)' ^ (x v (y ^ c1)) = 0. [para(4(a,1),3101(a,1,2,2))]. given #399 (T,wt=9): 3383 (x v c2)' ^ ((y ^ c1) v x) = 0. [para(4(a,1),3150(a,1,2,1))]. given #400 (A,wt=20): 162 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(24(a,1),10(a,1))]. given #401 (T,wt=9): 3439 (c2 v x)' ^ (y ^ c1) = 0. [para(3164(a,1),65(a,1,2)),rewrite(4(4),74(4)),flip(a)]. given #402 (T,wt=9): 3463 (x v c2)' ^ (y ^ c1) = 0. [para(3258(a,1),82(a,1,2)),rewrite(4(4),74(4)),flip(a)]. given #403 (T,wt=10): 173 c1 v (c2' ^ x) != 1 | c2' ^ x = c1'. [para(156(a,1),10(b,1)),flip(c),xx(b)]. given #404 (T,wt=10): 177 c1 v (x ^ c2') != 1 | x ^ c2' = c1'. [para(158(a,1),10(b,1)),flip(c),xx(b)]. given #405 (A,wt=21): 163 x v (y v ((x ^ z) v u)) = y v (x v u). [para(24(a,1),17(a,1,2)),flip(a)]. given #406 (T,wt=10): 214 c2 ^ (c1' v x) != 0 | c2' = c1' v x. [para(204(a,1),10(a,1)),xx(a)]. given #407 (T,wt=10): 218 c2 ^ (x v c1') != 0 | c2' = x v c1'. [para(207(a,1),10(a,1)),xx(a)]. given #408 (T,wt=10): 228 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),46(a,1,2)),rewrite(46(4)),flip(a)]. given #409 (T,wt=9): 3600 ((c2 v x) ^ y) v (c1 ^ y)' = 1. [para(228(a,1),188(a,1,2,1))]. given #410 (A,wt=17): 164 x v ((y ^ (x ^ z)) v u) = x v u. [para(19(a,1),24(a,1,2,1))]. given #411 (T,wt=8): 3628 ((c2 v x) ^ (c1 v y)) v c1' = 1. [para(6(a,1),3600(a,1,2,1))]. given #412 (T,wt=8): 3635 ((c2 v x) ^ (y v c1)) v c1' = 1. [para(20(a,1),3600(a,1,2,1))]. given #413 (T,wt=8): 3638 ((c2 v x) ^ (c2 v y)) v c1' = 1. [para(221(a,1),3600(a,1,2,1))]. given #414 (T,wt=8): 3639 ((c2 v x) ^ (y v c2)) v c1' = 1. [para(227(a,1),3600(a,1,2,1))]. given #415 (A,wt=15): 165 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(24(a,1),20(a,1,2)),rewrite(4(4))]. given #416 (T,wt=8): 3706 c1' v ((c2 v x) ^ (c1 v y)) = 1. [para(3628(a,1),2(a,1)),flip(a)]. given #417 (T,wt=8): 3707 ((x v c2) ^ (c1 v y)) v c1' = 1. [para(2(a,1),3628(a,1,1,1))]. given #418 (T,wt=8): 3709 ((c1 v x) ^ (c2 v y)) v c1' = 1. [para(4(a,1),3628(a,1,1))]. given #419 (T,wt=8): 3724 c1' v ((c2 v x) ^ (y v c1)) = 1. [para(3635(a,1),2(a,1)),flip(a)]. given #420 (A,wt=11): 166 x ^ (y v (z v x))' = 0. [para(3(a,1),148(a,1,2,1))]. given #421 (T,wt=8): 3725 ((x v c2) ^ (y v c1)) v c1' = 1. [para(2(a,1),3635(a,1,1,1))]. given #422 (T,wt=8): 3727 ((x v c1) ^ (c2 v y)) v c1' = 1. [para(4(a,1),3635(a,1,1))]. given #423 (T,wt=8): 3742 c1' v ((c2 v x) ^ (c2 v y)) = 1. [para(3638(a,1),2(a,1)),flip(a)]. given #424 (T,wt=8): 3743 ((x v c2) ^ (c2 v y)) v c1' = 1. [para(2(a,1),3638(a,1,1,1))]. given #425 (A,wt=11): 167 x ^ ((y v x)' ^ z) = 0. [para(148(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #426 (T,wt=8): 3759 c1' v ((c2 v x) ^ (y v c2)) = 1. [para(3639(a,1),2(a,1)),flip(a)]. given #427 (T,wt=8): 3760 ((x v c2) ^ (y v c2)) v c1' = 1. [para(2(a,1),3639(a,1,1,1))]. given #428 (T,wt=8): 3808 c2 v ((c1 ^ x) v (c2 ^ y))' = 1. [para(165(a,1),1914(a,1,2,1))]. given #429 (T,wt=8): 3809 c2 v ((c1 ^ x) v (y ^ c2))' = 1. [para(165(a,1),1915(a,1,2,1))]. given #430 (A,wt=13): 168 x ^ (y ^ (z v (x ^ y))') = 0. [para(148(a,1),5(a,1)),flip(a)]. given #431 (T,wt=8): 3832 c1' v ((x v c2) ^ (c1 v y)) = 1. [para(2(a,1),3706(a,1,2,1))]. given #432 (T,wt=8): 3833 c1' v ((c1 v x) ^ (c2 v y)) = 1. [para(4(a,1),3706(a,1,2))]. given #433 (T,wt=8): 3844 ((c1 v x) ^ (y v c2)) v c1' = 1. [para(4(a,1),3707(a,1,1))]. given #434 (T,wt=8): 3872 c1' v ((x v c2) ^ (y v c1)) = 1. [para(2(a,1),3724(a,1,2,1))]. given #435 (A,wt=14): 169 x v (y v x)' != 1 | (y v x)' = x'. [para(148(a,1),10(b,1)),flip(c),xx(b)]. given #436 (T,wt=8): 3874 c1' v ((x v c1) ^ (c2 v y)) = 1. [para(4(a,1),3724(a,1,2))]. given #437 (T,wt=8): 3921 ((x v c1) ^ (y v c2)) v c1' = 1. [para(4(a,1),3725(a,1,1))]. given #438 (T,wt=8): 3947 c1' v ((x v c2) ^ (c2 v y)) = 1. [para(2(a,1),3742(a,1,2,1))]. given #439 (T,wt=8): 3987 c1' v ((x v c2) ^ (y v c2)) = 1. [para(2(a,1),3759(a,1,2,1))]. given #440 (A,wt=13): 170 (x v y) ^ (x v (z v y))' = 0. [para(17(a,1),148(a,1,2,1))]. given #441 (T,wt=8): 4011 c2 v ((c2 ^ x) v (c1 ^ y))' = 1. [para(2(a,1),3808(a,1,2,1))]. given #442 (T,wt=8): 4013 c2 v ((x ^ c1) v (c2 ^ y))' = 1. [para(4(a,1),3808(a,1,2,1,1))]. given #443 (T,wt=8): 4020 c2 v ((c1 ^ x) v (y ^ c1))' = 1. [para(47(a,1),3808(a,1,2,1,2))]. given #444 (T,wt=8): 4025 c2 v ((x ^ c2) v (c1 ^ y))' = 1. [para(2(a,1),3809(a,1,2,1))]. given #445 (A,wt=11): 171 x ^ (y ^ (z v x)') = 0. [para(148(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #446 (T,wt=8): 4027 c2 v ((x ^ c1) v (y ^ c2))' = 1. [para(4(a,1),3809(a,1,2,1,1))]. given #447 (T,wt=8): 4053 c1' v ((c1 v x) ^ (y v c2)) = 1. [para(4(a,1),3832(a,1,2))]. given #448 (T,wt=8): 4084 c1' v ((x v c1) ^ (y v c2)) = 1. [para(4(a,1),3872(a,1,2))]. given #449 (T,wt=8): 4174 c2 v ((c2 ^ x) v (y ^ c1))' = 1. [para(4(a,1),4011(a,1,2,1,2))]. given #450 (A,wt=11): 172 ((x ^ y) v z) ^ (x v z)' = 0. [para(24(a,1),148(a,1,2,1))]. given #451 (T,wt=8): 4181 c2 v ((x ^ c1) v (c1 ^ y))' = 1. [para(47(a,1),4011(a,1,2,1,1))]. given #452 (T,wt=8): 4195 c2 v ((x ^ c1) v (y ^ c1))' = 1. [para(47(a,1),4013(a,1,2,1,2))]. given #453 (T,wt=8): 4203 c2 v ((c1 ^ x) v (c1 ^ y))' = 1. [para(4(a,1),4020(a,1,2,1,2))]. given #454 (T,wt=8): 4217 c2 v ((x ^ c2) v (y ^ c1))' = 1. [para(4(a,1),4025(a,1,2,1,2))]. given #455 (A,wt=18): 174 c1 ^ (x v (c1 ^ ((c1 ^ x) v (c2' ^ (y ^ (c1 v x)))))) = c1 ^ x. [para(156(a,1),12(a,2,2,2)),rewrite(5(10),35(17))]. given #456 (T,wt=9): 3618 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(228(a,1),141(a,1)),rewrite(221(12))]. given #457 (T,wt=9): 3623 (c1 ^ x)' v ((c2 v y) ^ x) = 1. [para(3600(a,1),2(a,1)),flip(a)]. given #458 (T,wt=9): 3624 ((x v c2) ^ y) v (c1 ^ y)' = 1. [para(2(a,1),3600(a,1,1,1))]. given #459 (T,wt=9): 3626 (x ^ (c2 v y)) v (c1 ^ x)' = 1. [para(4(a,1),3600(a,1,1))]. given #460 (A,wt=11): 175 c1 ^ (x ^ (c2' ^ y)) = 0. [para(156(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #461 (T,wt=9): 3627 ((c2 v x) ^ y) v (y ^ c1)' = 1. [para(4(a,1),3600(a,1,2,1))]. given #462 (T,wt=9): 3650 (x ^ (c2 v y)) v (x ^ c1)' = 1. [para(65(a,1),3600(a,1,1)),rewrite(3(7),237(9))]. given #463 (T,wt=9): 4093 (x ^ y)' != 1 | x ^ y = 0. [para(161(a,1),169(a,1,2,1)),rewrite(60(4),2(4),57(4),161(7),60(6),304(8)),flip(b)]. given #464 (T,wt=9): 4409 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(2(a,1),3618(a,1,2,1,1))]. given #465 (A,wt=11): 176 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),158(a,1,2))]. given #466 (T,wt=9): 4410 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(2(a,1),3618(a,1,2,1,2))]. given #467 (T,wt=9): 4411 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(2(a,1),3618(a,1,2))]. given #468 (T,wt=9): 4412 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(4(a,1),3618(a,1,2,1))]. given #469 (T,wt=9): 4423 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(128(a,1),3618(a,1,2,1,1))]. given #470 (A,wt=18): 178 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2' ^ (c1 v x)))))) = c1 ^ x. [para(158(a,1),12(a,2,2,2)),rewrite(5(10),35(17))]. given #471 (T,wt=9): 4424 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(130(a,1),3618(a,1,2,1,1))]. given #472 (T,wt=9): 4438 (c1 ^ x)' v ((y v c2) ^ x) = 1. [para(2(a,1),3623(a,1,2,1))]. given #473 (T,wt=9): 4439 (x ^ c1)' v ((c2 v y) ^ x) = 1. [para(4(a,1),3623(a,1,1,1))]. given #474 (T,wt=9): 4440 (c1 ^ x)' v (x ^ (c2 v y)) = 1. [para(4(a,1),3623(a,1,2))]. given #475 (A,wt=15): 179 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),25(a,1,2,2,1))]. given #476 (T,wt=9): 4456 (x ^ c1)' v (x ^ (c2 v y)) = 1. [para(65(a,1),3623(a,1,2)),rewrite(3(4),237(6))]. given #477 (T,wt=9): 4482 (x ^ (y v c2)) v (c1 ^ x)' = 1. [para(4(a,1),3624(a,1,1))]. given #478 (T,wt=9): 4483 ((x v c2) ^ y) v (y ^ c1)' = 1. [para(4(a,1),3624(a,1,2,1))]. given #479 (T,wt=9): 4498 (x ^ (y v c2)) v (x ^ c1)' = 1. [para(65(a,1),3624(a,1,1)),rewrite(3(7),644(9))]. given #480 (A,wt=24): 180 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 #481 (T,wt=9): 4602 (x ^ y)' != 1 | y ^ x = 0. [para(4(a,1),4093(a,1,1))]. given #482 (T,wt=9): 4604 (x v y)' != 1 | x v y = 0. [para(21(a,1),4093(a,1,1)),rewrite(21(8))]. given #483 (T,wt=9): 4605 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(2(a,1),4409(a,1,2,1,2))]. given #484 (T,wt=9): 4606 c1 ^ (x v ((y v c1) ^ (c2 v z))) = c1. [para(2(a,1),4409(a,1,2))]. given #485 (A,wt=23): 181 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 #486 (T,wt=9): 4608 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(4(a,1),4409(a,1,2,1))]. given #487 (T,wt=9): 4642 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(2(a,1),4410(a,1,2))]. given #488 (T,wt=9): 4644 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(4(a,1),4410(a,1,2,1))]. given #489 (T,wt=9): 4654 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(128(a,1),4410(a,1,2,1,1))]. given #490 (A,wt=19): 182 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(19(a,1),25(a,1,2,2))]. given #491 (T,wt=9): 4655 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(130(a,1),4410(a,1,2,1,1))]. given #492 (T,wt=9): 4673 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(4(a,1),4411(a,1,2,2))]. given #493 (T,wt=9): 4683 c1 ^ (x v ((c2 v y) ^ (c2 v z))) = c1. [para(128(a,1),4411(a,1,2,2,1))]. given #494 (T,wt=9): 4684 c1 ^ (x v ((y v c2) ^ (c2 v z))) = c1. [para(130(a,1),4411(a,1,2,2,1))]. given #495 (A,wt=19): 183 (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 #496 (T,wt=9): 4797 (x ^ c1)' v ((y v c2) ^ x) = 1. [para(4(a,1),4438(a,1,1,1))]. given #497 (T,wt=9): 4798 (c1 ^ x)' v (x ^ (y v c2)) = 1. [para(4(a,1),4438(a,1,2))]. given #498 (T,wt=9): 4813 (x ^ c1)' v (x ^ (y v c2)) = 1. [para(65(a,1),4438(a,1,2)),rewrite(3(4),644(6))]. given #499 (T,wt=9): 5123 (x v y)' != 1 | y v x = 0. [para(2(a,1),4604(a,1,1))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 72 (0.00 of 2.04 sec). given #500 (A,wt=17): 184 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 #501 (T,wt=9): 5125 c1 ^ (x v ((y v c1) ^ (z v c2))) = c1. [para(2(a,1),4605(a,1,2))]. given #502 (T,wt=9): 5128 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(4(a,1),4605(a,1,2,1))]. given #503 (T,wt=9): 5159 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(4(a,1),4606(a,1,2,2))]. given #504 (T,wt=9): 5254 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(4(a,1),4642(a,1,2,2))]. given #505 (A,wt=13): 185 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(25(a,1),148(a,1,2,1))]. given #506 (T,wt=9): 5263 c1 ^ (x v ((c2 v y) ^ (z v c2))) = c1. [para(128(a,1),4642(a,1,2,2,1))]. given #507 (T,wt=9): 5264 c1 ^ (x v ((y v c2) ^ (z v c2))) = c1. [para(130(a,1),4642(a,1,2,2,1))]. given #508 (T,wt=9): 5652 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(184(a,1),132(a,1)),rewrite(124(4)),flip(a)]. given #509 (T,wt=9): 5657 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(184(a,1),143(a,1)),rewrite(126(4)),flip(a)]. given #510 (A,wt=11): 186 x v ((x ^ y)' v z) = 1. [para(161(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #511 (T,wt=9): 5681 c1 ^ (x v ((y v c2) ^ (z v c1))) = c1. [para(4(a,1),5125(a,1,2,2))]. given #512 (T,wt=9): 5899 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),5652(a,1,2,1))]. given #513 (T,wt=9): 5901 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),5652(a,1,2,1,1))]. given #514 (T,wt=9): 5902 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),5652(a,1,2))]. given #515 (A,wt=13): 187 x v (y v ((x v y) ^ z)') = 1. [para(161(a,1),3(a,1)),flip(a)]. given #516 (T,wt=9): 5911 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(47(a,1),5652(a,1,2,1,1))]. given #517 (T,wt=9): 5940 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),5657(a,1,2,1))]. given #518 (T,wt=9): 5942 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(4(a,1),5657(a,1,2,1,1))]. given #519 (T,wt=9): 5943 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(4(a,1),5657(a,1,2))]. given #520 (A,wt=13): 189 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),161(a,1,2,1))]. given #521 (T,wt=9): 5952 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(47(a,1),5657(a,1,2,1,1))]. given #522 (T,wt=9): 6020 c2 v (((c1 ^ x) v (y ^ c2)) ^ z) = c2. [para(4(a,1),5899(a,1,2,1,2))]. given #523 (T,wt=9): 6021 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(4(a,1),5899(a,1,2))]. given #524 (T,wt=9): 6030 c2 v (((c1 ^ x) v (y ^ c1)) ^ z) = c2. [para(47(a,1),5899(a,1,2,1,2))]. given #525 (A,wt=14): 190 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(161(a,1),10(a,1)),flip(c),xx(a)]. given #526 (T,wt=9): 6060 c2 v (x ^ ((y ^ c2) v (c1 ^ z))) = c2. [para(4(a,1),5901(a,1,2))]. given #527 (T,wt=9): 6107 c2 v (x ^ ((y ^ c1) v (c1 ^ z))) = c2. [para(47(a,1),5902(a,1,2,2,1))]. given #528 (T,wt=9): 6163 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),5911(a,1,2,1,1))]. given #529 (T,wt=9): 6202 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(4(a,1),5940(a,1,2,1,2))]. given #530 (A,wt=11): 191 x v (y v (x ^ z)') = 1. [para(161(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #531 (T,wt=9): 6203 c2 v (x ^ ((y ^ c1) v (c2 ^ z))) = c2. [para(4(a,1),5940(a,1,2))]. given #532 (T,wt=9): 6241 c2 v (x ^ ((y ^ c2) v (z ^ c1))) = c2. [para(4(a,1),5942(a,1,2))]. given #533 (T,wt=9): 6288 c2 v (x ^ ((y ^ c1) v (z ^ c1))) = c2. [para(47(a,1),5943(a,1,2,2,1))]. given #534 (T,wt=9): 6369 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(4(a,1),6020(a,1,2))]. given #535 (A,wt=11): 192 x v (y ^ (x ^ z))' = 1. [para(19(a,1),161(a,1,2,1))]. given #536 (T,wt=9): 6414 c2 v (x ^ ((c1 ^ y) v (z ^ c1))) = c2. [para(47(a,1),6021(a,1,2,2,2))]. given #537 (T,wt=9): 6519 c2 v (x ^ ((c1 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),6107(a,1,2,2,1))]. given #538 (T,wt=9): 6593 c2 v (x ^ ((y ^ c1) v (z ^ c2))) = c2. [para(4(a,1),6202(a,1,2))]. given #539 (T,wt=10): 237 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(221(a,1),19(a,1,2)),flip(a)]. given #540 (A,wt=11): 193 x v ((y ^ x)' v z) = 1. [para(188(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #541 (T,wt=10): 246 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(227(a,1),5(a,1,1)),flip(a)]. given #542 (T,wt=10): 249 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(227(a,1),19(a,1,2)),flip(a)]. given #543 (T,wt=10): 251 c1 v (c2 v x)' != 1 | (c2 v x)' = c1'. [para(231(a,1),10(b,1)),flip(c),xx(b)]. given #544 (T,wt=10): 256 c1 v (x v c2)' != 1 | (x v c2)' = c1'. [para(232(a,1),10(b,1)),flip(c),xx(b)]. given #545 (A,wt=13): 194 x v (y v (z ^ (x v y))') = 1. [para(188(a,1),3(a,1)),flip(a)]. given #546 (T,wt=10): 281 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'. [para(270(a,1),10(a,1)),flip(c),xx(a)]. given #547 (T,wt=10): 287 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'. [para(280(a,1),10(a,1)),flip(c),xx(a)]. given #548 (T,wt=10): 291 (c2 ^ (c1 v x)) v (c1' v y) = 1. [para(261(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #549 (T,wt=10): 293 (c2 ^ (c1 v x)) v (y v c1') = 1. [para(261(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #550 (A,wt=11): 195 x v (y ^ (z ^ x))' = 1. [para(5(a,1),188(a,1,2,1))]. given #551 (T,wt=10): 294 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(17(a,1),261(a,1,1,2))]. given #552 (T,wt=10): 296 (c2 ^ (x v c1)) v (c1' v y) = 1. [para(267(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #553 (T,wt=10): 297 (c2 ^ (x v (y v c1))) v c1' = 1. [para(3(a,1),267(a,1,1,2))]. given #554 (T,wt=10): 299 (c2 ^ (x v c1)) v (y v c1') = 1. [para(267(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #555 (A,wt=14): 196 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(188(a,1),10(a,1)),flip(c),xx(a)]. given #556 (T,wt=10): 318 c2 ^ (c1' v x) != 0 | (c1' v x)' = c2. [para(204(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #557 (T,wt=10): 319 c2 ^ (x v c1') != 0 | (x v c1')' = c2. [para(207(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #558 (T,wt=10): 326 c1' v ((c2 ^ (c1 v x)) v y) = 1. [para(290(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #559 (T,wt=10): 327 c1' v (x v (c2 ^ (c1 v y))) = 1. [para(290(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #560 (A,wt=25): 197 x v ((y ^ ((y ^ x) v (z ^ (y v x)))) v (y ^ (x v (y ^ z)))') = 1. [para(12(a,1),188(a,1,2,1)),rewrite(3(11))]. given #561 (T,wt=10): 328 c1' v (c2 ^ (x v (c1 v y))) = 1. [para(17(a,1),290(a,1,2,2))]. given #562 (T,wt=10): 329 c1' v ((c2 ^ (x v c1)) v y) = 1. [para(295(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #563 (T,wt=10): 330 c1' v (c2 ^ (x v (y v c1))) = 1. [para(3(a,1),295(a,1,2,2))]. given #564 (T,wt=10): 331 c1' v (x v (c2 ^ (y v c1))) = 1. [para(295(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #565 (A,wt=11): 199 x v (y v (z ^ x)') = 1. [para(188(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #566 (T,wt=10): 349 (x v c2) ^ c1' != 0 | (x v c2)' = c1'. [para(198(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #567 (T,wt=10): 352 (c2 v x) ^ c1' != 0 | (c2 v x)' = c1'. [para(207(a,1),37(a,1)),xx(a)]. given #568 (T,wt=10): 389 c1 v (c2' ^ x) != 1 | (c2' ^ x)' = c1. [para(156(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #569 (T,wt=10): 390 c1 v (x ^ c2') != 1 | (x ^ c2')' = c1. [para(158(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #570 (A,wt=13): 200 (x ^ y) v (x ^ (z ^ y))' = 1. [para(19(a,1),188(a,1,2,1))]. given #571 (T,wt=10): 431 (x ^ c1) v c2' != 1 | (x ^ c1)' = c2'. [para(155(a,1),39(b,1,2)),rewrite(85(9)),xx(b)]. given #572 (T,wt=10): 435 (c1 ^ x) v c2' != 1 | (c1 ^ x)' = c2'. [para(158(a,1),39(b,1)),xx(b)]. given #573 (T,wt=10): 504 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0. [para(494(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #574 (T,wt=10): 506 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0. [para(494(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #575 (A,wt=15): 201 x v (y v (z v (x v y)')) = 1. [para(21(a,1),188(a,1,2,1)),rewrite(3(5),3(4))]. given #576 (T,wt=10): 507 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0. [para(19(a,1),494(a,1,1,2))]. given #577 (T,wt=10): 512 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0. [para(498(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #578 (T,wt=10): 513 (c1 v (x ^ (y ^ c2))) ^ c2' = 0. [para(5(a,1),498(a,1,1,2))]. given #579 (T,wt=10): 515 (c1 v (x ^ c2)) ^ (y ^ c2') = 0. [para(498(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #580 (A,wt=11): 202 ((x v y) ^ z) v (x ^ z)' = 1. [para(22(a,1),188(a,1,2,1))]. given #581 (T,wt=10): 533 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(503(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #582 (T,wt=10): 534 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(503(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #583 (T,wt=10): 535 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(19(a,1),503(a,1,2,2))]. given #584 (T,wt=10): 538 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(511(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #585 (A,wt=13): 203 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(23(a,1),188(a,1,2,1))]. given #586 (T,wt=10): 539 c2' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(5(a,1),511(a,1,2,2))]. given #587 (T,wt=10): 541 c2' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(511(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #588 (T,wt=10): 841 c2 ^ (c1 v x) != 1 | c1 != 0 | c1' = c2 ^ (c1 v x). [para(612(a,1),10(a,1)),rewrite(65(12),4(9),13(9))]. given #589 (T,wt=10): 846 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (c1 v x))' = c1. [para(612(a,1),36(a,1)),rewrite(4(12),65(12),4(9),13(9))]. given #590 (A,wt=14): 206 c2 ^ (c1' v (c2 ^ ((c2 ^ c1') v x))) = c2 ^ (c1' v (c2 ^ x)). [para(198(a,1),12(a,1,2,2,2,2,2)),rewrite(32(10))]. given #591 (T,wt=8): 7663 c2 ^ (c1' v (c2 ^ (c2 ^ c1')')) = c2. [para(8(a,1),206(a,1,2,2,2)),rewrite(4(6),54(6),2(5),198(5),4(3),54(3)),flip(a)]. given #592 (T,wt=7): 7711 c1' v (c2 ^ (c2 ^ c1')') = 1. [para(7663(a,1),26(a,1,2)),rewrite(2(12),51(12),2(4),198(4)),flip(a)]. given #593 (T,wt=5): 7714 c2 ^ (c2 ^ c1')' = c1. [hyper(68,a,7711,a,b,34,a),rewrite(304(3)),flip(a)]. given #594 (T,wt=4): 7721 c1 != 0 | c2 ^ c1' = c2. [para(7714(a,1),38(b,1)),rewrite(2(7),161(7),304(12)),xx(a)]. given #595 (A,wt=15): 208 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),27(a,1,1))]. given #596 (T,wt=5): 7720 c1 ^ (c2 ^ c1')' = c1. [para(7714(a,1),46(a,1,2)),rewrite(28(3)),flip(a)]. given #597 (T,wt=6): 7716 c1 != 0 | (c2 ^ c1')' = c2'. [para(7714(a,1),10(b,1)),rewrite(161(7)),flip(c),xx(a)]. given #598 (T,wt=8): 7719 c1 v (c2 ^ c1')' = (c2 ^ c1')'. [para(7714(a,1),26(a,1,2)),rewrite(2(7))]. given #599 (T,wt=7): 7789 c1 ^ (x v (c2 ^ c1')') = c1. [para(7719(a,1),50(a,1,2,2))]. given #600 (A,wt=15): 209 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),27(a,1,2)),rewrite(5(3))]. given #601 (T,wt=7): 7821 c1 ^ ((c2 ^ c1')' v x) = c1. [para(2(a,1),7789(a,1,2))]. given #602 (T,wt=8): 7734 (c2 ^ c1')' v (x ^ c1)' = 1. [para(7714(a,1),195(a,1,2,1,2))]. given #603 (T,wt=8): 7774 (c2 ^ c1')' != 1 | c1 != 0 | c2 ^ c1' = c1. [para(7720(a,1),38(b,1)),rewrite(2(7),7719(7),304(16))]. given #604 (T,wt=8): 7807 c1 ^ (x v (c2 ^ c1')')' = 0. [para(7719(a,1),153(a,1,2,1,2))]. given #605 (A,wt=21): 210 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(27(a,1),17(a,1,2)),flip(a)]. given #606 (T,wt=8): 7982 c1 ^ ((c2 ^ c1')' v x)' = 0. [para(7821(a,1),1269(a,1,2)),rewrite(4(9))]. given #607 (T,wt=8): 8002 (x ^ c1)' v (c2 ^ c1')' = 1. [para(7734(a,1),2(a,1)),flip(a)]. given #608 (T,wt=8): 8004 (c2 ^ c1')' v (c1 ^ x)' = 1. [para(4(a,1),7734(a,1,2,1))]. given #609 (T,wt=8): 8056 (c1 ^ x)' v (c2 ^ c1')' = 1. [para(4(a,1),8002(a,1,1,1))]. given #610 (A,wt=19): 211 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(19(a,1),27(a,1,2,2))]. given #611 (T,wt=9): 7738 c1' v ((c2 v x) ^ (c2 ^ c1')') = 1. [para(7714(a,1),202(a,1,2,1)),rewrite(2(11))]. given #612 (T,wt=9): 7739 c1' v ((c2 ^ c1')' ^ (c1 v x)) = 1. [para(7714(a,1),203(a,1,1,2,1)),rewrite(7714(15),2(11))]. given #613 (T,wt=9): 7780 c1' v ((x v c2) ^ (c2 ^ c1')') = 1. [para(7720(a,1),3624(a,1,2,1)),rewrite(2(11))]. given #614 (T,wt=9): 7781 c1' v ((c2 ^ c1')' ^ (c2 v x)) = 1. [para(7720(a,1),3626(a,1,2,1)),rewrite(2(11))]. given #615 (A,wt=15): 213 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(27(a,1),148(a,1,2,1)),rewrite(5(5),5(4))]. given #616 (T,wt=9): 7782 c1' v ((c2 ^ c1')' ^ (x v c2)) = 1. [para(7720(a,1),4482(a,1,2,1)),rewrite(2(11))]. given #617 (T,wt=9): 7784 c1' v ((c1 v x) ^ (c2 ^ c1')') = 1. [para(7720(a,1),202(a,1,2,1)),rewrite(2(11))]. given #618 (T,wt=9): 7801 c1 ^ ((c2 v x) ^ (c2 ^ c1')')' = 0. [para(7719(a,1),2196(a,1,2,1,2))]. given #619 (T,wt=9): 7802 c1 ^ ((x v c2) ^ (c2 ^ c1')')' = 0. [para(7719(a,1),2208(a,1,2,1,2))]. given #620 (A,wt=24): 215 c2 ^ (c1' v (x v (c2 ^ ((c2 ^ (c1' v x)) v y)))) = c2 ^ (c1' v (x v (c2 ^ y))). [para(204(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12),3(13),3(21))]. given #621 (T,wt=9): 7803 c1 ^ ((c2 ^ c1')' ^ (c2 v x))' = 0. [para(7719(a,1),2209(a,1,2,1,1))]. given #622 (T,wt=9): 7804 c1 ^ ((c2 ^ c1')' ^ (x v c2))' = 0. [para(7719(a,1),2231(a,1,2,1,1))]. given #623 (T,wt=9): 7819 c1' v (c2 ^ (x v (c2 ^ c1')')) = 1. [para(7719(a,1),294(a,1,1,2,2)),rewrite(2(11))]. given #624 (T,wt=9): 7972 c1' v (c2 ^ ((c2 ^ c1')' v x)) = 1. [para(7821(a,1),233(a,1,2,1)),rewrite(2(11))]. given #625 (A,wt=11): 216 c2 v (x v (c1' v y)) = 1. [para(204(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #626 (T,wt=9): 8122 c1' v ((c2 ^ c1')' ^ (x v c1)) = 1. [para(2(a,1),7739(a,1,2,2))]. given #627 (T,wt=9): 8187 c1' v ((x v c1) ^ (c2 ^ c1')') = 1. [para(2(a,1),7784(a,1,2,1))]. given #628 (T,wt=10): 886 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0. [para(845(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #629 (T,wt=10): 888 c1 ^ (c2 ^ (x v (c1 v y)))' = 0. [para(17(a,1),845(a,1,2,1,2))]. given #630 (A,wt=11): 217 c2 v (x v (y v c1')) = 1. [para(3(a,1),207(a,1,2))]. given #631 (T,wt=9): 8343 c1 ^ (c2 ^ (x v (c2 ^ (c1 v y))))' = 0. [para(612(a,1),888(a,1,2,1,2,2))]. given #632 (T,wt=9): 8345 c1 ^ (c2 ^ (x v (c2 ^ (y v c1))))' = 0. [para(617(a,1),888(a,1,2,1,2,2))]. given #633 (T,wt=9): 8348 c1 ^ (c2 ^ (x v (c2 ^ c1')'))' = 0. [para(7719(a,1),888(a,1,2,1,2,2))]. given #634 (T,wt=9): 8357 c1 ^ (c2 ^ ((c2 ^ (c1 v x)) v y))' = 0. [para(2(a,1),8343(a,1,2,1,2))]. given #635 (A,wt=24): 219 c2 ^ (x v (c1' v (c2 ^ ((c2 ^ (x v c1')) v y)))) = c2 ^ (x v (c1' v (c2 ^ y))). [para(207(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12),3(13),3(21))]. given #636 (T,wt=9): 8371 c1 ^ (c2 ^ ((c2 ^ (x v c1)) v y))' = 0. [para(2(a,1),8345(a,1,2,1,2))]. given #637 (T,wt=9): 8385 c1 ^ (c2 ^ ((c2 ^ c1')' v x))' = 0. [para(2(a,1),8348(a,1,2,1,2))]. given #638 (T,wt=10): 889 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0. [para(845(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #639 (T,wt=10): 890 c1 v (c2 ^ (c1 v x))' != 1 | c2 ^ (c1 v x) = c1. [para(845(a,1),38(b,1)),rewrite(2(7),304(18)),xx(b)]. given #640 (A,wt=16): 220 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(46(a,1),5(a,2,2)),rewrite(19(5),5(4))]. given #641 (T,wt=10): 893 c1 ^ (c2 ^ (x v (y v c1)))' = 0. [para(3(a,1),885(a,1,2,1,2))]. given #642 (T,wt=10): 894 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0. [para(885(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #643 (T,wt=10): 896 c1 ^ (x ^ (c2 ^ (y v c1))') = 0. [para(885(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #644 (T,wt=10): 897 c1 v (c2 ^ (x v c1))' != 1 | c2 ^ (x v c1) = c1. [para(885(a,1),38(b,1)),rewrite(2(7),304(18)),xx(b)]. given #645 (A,wt=11): 222 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1' = c2 ^ x. [para(46(a,1),10(b,1))]. given #646 (T,wt=10): 963 c2 ^ (x v c1) != 1 | c1 != 0 | c1' = c2 ^ (x v c1). [para(617(a,1),10(a,1)),rewrite(82(12),4(9),13(9))]. given #647 (T,wt=10): 965 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (x v c1))' = c1. [para(617(a,1),36(a,1)),rewrite(4(12),82(12),4(9),13(9))]. given #648 (T,wt=10): 1063 c2 != 1 | c1 v (c2 ^ x) != 0 | c2' = c1 v (c2 ^ x). [para(795(a,1),10(b,1)),rewrite(17(6),7(5),120(3))]. given #649 (T,wt=10): 1068 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (c2 ^ x))' = c2. [para(795(a,1),38(b,1)),rewrite(2(6),17(6),7(5),120(3))]. given #650 (A,wt=20): 223 c1 ^ ((c2 ^ x) v (c1 ^ ((c1 ^ x) v (y ^ (c1 v (c2 ^ x)))))) = c1 ^ ((c2 ^ x) v (c1 ^ y)). [para(46(a,1),12(a,1,2,2,2,1))]. given #651 (T,wt=10): 1074 c2 v ((c1 v (c2 ^ x))' v y) = 1. [para(1066(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #652 (T,wt=10): 1078 c2 v (x v (c1 v (c2 ^ y))') = 1. [para(1066(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #653 (T,wt=10): 1079 c2 v (c1 v (x ^ (c2 ^ y)))' = 1. [para(19(a,1),1066(a,1,2,1,2))]. given #654 (T,wt=9): 8673 c2 v (c1 v (x ^ (c1 v (c2 ^ y))))' = 1. [para(795(a,1),1079(a,1,2,1,2,2))]. given #655 (A,wt=20): 224 c1 ^ (x v (c1 ^ ((c1 ^ x) v (c2 ^ (y ^ (c1 v x)))))) = c1 ^ (x v (c1 ^ y)). [para(46(a,1),12(a,2,2,2)),rewrite(5(9))]. given #656 (T,wt=9): 8674 c2 v (c1 v (x ^ (c1 v (y ^ c2))))' = 1. [para(801(a,1),1079(a,1,2,1,2,2))]. given #657 (T,wt=9): 8681 c2 v (c1 v ((c1 v (c2 ^ x)) ^ y))' = 1. [para(4(a,1),8673(a,1,2,1,2))]. given #658 (T,wt=9): 8739 c2 v (c1 v ((c1 v (x ^ c2)) ^ y))' = 1. [para(4(a,1),8674(a,1,2,1,2))]. given #659 (T,wt=10): 1080 c2 ^ (c1 v (c2 ^ x))' != 0 | c1 v (c2 ^ x) = c2. [para(1066(a,1),36(a,1)),rewrite(4(10),304(18)),xx(a)]. given #660 (A,wt=17): 225 c1 ^ (x v (c2 ^ ((c2 ^ x) v (y ^ (c2 v x))))) = c1 ^ (x v (c2 ^ y)). [para(12(a,1),46(a,1,2)),rewrite(46(7)),flip(a)]. given #661 (T,wt=10): 1083 c2 v ((c1 v (x ^ c2))' v y) = 1. [para(1075(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #662 (T,wt=10): 1084 c2 v (c1 v (x ^ (y ^ c2)))' = 1. [para(5(a,1),1075(a,1,2,1,2))]. given #663 (T,wt=10): 1087 c2 v (x v (c1 v (y ^ c2))') = 1. [para(1075(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #664 (T,wt=10): 1088 c2 ^ (c1 v (x ^ c2))' != 0 | c1 v (x ^ c2) = c2. [para(1075(a,1),36(a,1)),rewrite(4(10),304(18)),xx(a)]. given #665 (A,wt=16): 226 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(46(a,1),19(a,1,2)),flip(a)]. given #666 (T,wt=10): 1152 c2 != 1 | c1 v (x ^ c2) != 0 | c2' = c1 v (x ^ c2). [para(801(a,1),10(b,1)),rewrite(17(6),26(5),120(3))]. given #667 (T,wt=10): 1155 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (x ^ c2))' = c2. [para(801(a,1),38(b,1)),rewrite(2(6),17(6),26(5),120(3))]. given #668 (T,wt=10): 1238 x ^ (c1 v (c2 ^ (x v y))) = c2 ^ x. [para(1157(a,1),22(a,1,2)),rewrite(4(3),65(4)),flip(a)]. given #669 (T,wt=10): 1247 x ^ (c1 v (c2 ^ (y v x))) = c2 ^ x. [para(1157(a,1),77(a,1,2)),rewrite(4(3),82(4)),flip(a)]. given #670 (A,wt=12): 230 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(23(a,1),46(a,1,2)),rewrite(46(4)),flip(a)]. given #671 (T,wt=10): 1356 (c1 v (c2 ^ x))' v (y v c2) = 1. [para(1066(a,1),95(a,1,1)),rewrite(54(10),1066(15))]. given #672 (T,wt=10): 1357 (c1 v (x ^ c2))' v (y v c2) = 1. [para(1075(a,1),95(a,1,1)),rewrite(54(10),1075(15))]. given #673 (T,wt=10): 1811 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(1795(a,1),24(a,1,2)),rewrite(2(3),51(4),2(6)),flip(a)]. given #674 (T,wt=9): 8993 c1 v c2' != 1 | c2 ^ (c1 v (c2' ^ x)) = c2. [para(1811(a,1),1277(a,1)),rewrite(4(13))]. given #675 (A,wt=11): 238 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #676 (T,wt=10): 1821 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(1795(a,1),115(a,1,2)),rewrite(2(3),121(4),2(6)),flip(a)]. given #677 (T,wt=9): 9047 c1 v c2' != 1 | c2 ^ (c1 v (x ^ c2')) = c2. [para(1821(a,1),1277(a,1)),rewrite(4(13))]. given #678 (T,wt=10): 2165 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(47(a,1),125(a,1,1)),rewrite(26(8)),flip(a)]. given #679 (T,wt=10): 2186 (c2 v x) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(795(a,1),125(a,1,1)),rewrite(26(12)),flip(a)]. given #680 (A,wt=15): 239 x v (y v ((x v y)' v z)) = 1. [para(31(a,1),3(a,1,1)),rewrite(61(2),3(5)),flip(a)]. given #681 (T,wt=10): 2187 (c2 v x) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(801(a,1),125(a,1,1)),rewrite(26(12)),flip(a)]. given #682 (T,wt=8): 9151 c2 v x != 1 | c2 != 0 | (c2 v x)' = c2. [para(2187(a,1),180(b,1)),rewrite(2(4),128(4),2(9),128(9),4(9),6(9),120(7),2(15),128(15),4(15),6(15),120(13))]. given #683 (T,wt=8): 9160 x v c2 != 1 | c2 != 0 | (c2 v x)' = c2. [para(2(a,1),9151(a,1))]. given #684 (T,wt=8): 9162 x v c2 != 1 | c2 != 0 | (x v c2)' = c2. [para(51(a,1),9151(a,1)),rewrite(51(12))]. given #685 (A,wt=19): 240 x v (y v (z v (x v (y v z))')) = 1. [para(31(a,1),3(a,1)),rewrite(3(3)),flip(a)]. given #686 (T,wt=8): 9165 c2 v x != 1 | c2 != 0 | (x v c2)' = c2. [para(2(a,1),9162(a,1))]. given #687 (T,wt=10): 2257 (c1 ^ x) v (y v c2) = y v c2. [para(51(a,1),132(a,2)),rewrite(630(8))]. given #688 (T,wt=10): 2472 c1 v (c2 ^ x) != 1 | c1 != 0 | c1' = c1 v (x ^ c2). [para(134(a,1),138(a,1,2)),rewrite(13(5),795(7),62(6),13(9),13(15),13(17),801(19),62(18),801(17))]. given #689 (T,wt=10): 2864 (x ^ c1) v (y v c2) = y v c2. [para(51(a,1),143(a,2)),rewrite(630(8))]. given #690 (A,wt=18): 241 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 #691 (T,wt=10): 3040 (x v c1) ^ (x v (c2 ^ (c1 v y)))' = 0. [para(612(a,1),149(a,1,2,1,2))]. given #692 (T,wt=10): 3041 (x v c1) ^ (x v (c2 ^ (y v c1)))' = 0. [para(617(a,1),149(a,1,2,1,2))]. given #693 (T,wt=10): 3525 c2 != 1 | c1 v (c2 ^ x) != 0 | c2' = c1 v (x ^ c2). [para(146(a,1),162(b,1)),rewrite(4(5),13(5),801(7),17(6),26(5),120(3),4(7),13(7),795(9),4(14),13(14),4(16),13(16),801(18),62(17))]. given #694 (T,wt=10): 3545 c1 v (x ^ c2') != 1 | c2' ^ x = c1'. [para(4(a,1),173(a,1,2))]. given #695 (A,wt=15): 242 x v (y v (z v (x v z)')) = 1. [para(31(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #696 (T,wt=10): 3547 c1 v (c2' ^ x) != 1 | x ^ c2' = c1'. [para(4(a,1),177(a,1,2))]. given #697 (T,wt=10): 3595 c2 ^ (x v c1') != 0 | c2' = c1' v x. [para(2(a,1),214(a,1,2))]. given #698 (T,wt=10): 3598 c2 ^ (c1' v x) != 0 | c2' = x v c1'. [para(2(a,1),218(a,1,2))]. given #699 (T,wt=10): 3793 (c1 ^ x) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(612(a,1),165(a,1,1)),rewrite(20(12)),flip(a)]. given #700 (A,wt=19): 243 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 #701 (T,wt=10): 3795 (c1 ^ x) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(617(a,1),165(a,1,1)),rewrite(20(12)),flip(a)]. given #702 (T,wt=8): 9370 c1 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c1. [para(3795(a,1),138(a,1)),rewrite(4(5),19(5),46(5),2(5),7(5),4(3),13(3),4(7),19(7),46(7),4(15),19(15),46(15),2(15),7(15),4(13),13(13))]. given #703 (T,wt=8): 9377 c1 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c1. [para(4(a,1),9370(b,1))]. given #704 (T,wt=8): 9379 c1 != 1 | x ^ c1 != 0 | (x ^ c1)' = c1. [para(69(a,1),9370(b,1)),rewrite(69(11))]. given #705 (A,wt=13): 244 x v (y v ((x ^ z) v y)') = 1. [para(31(a,1),24(a,1,2)),rewrite(70(2)),flip(a)]. given #706 (T,wt=8): 9382 c1 != 1 | c1 ^ x != 0 | (x ^ c1)' = c1. [para(4(a,1),9379(b,1))]. given #707 (T,wt=10): 3818 c2 ^ c1' != 0 | (c2 ^ c1') v (c2 ^ (x v c1)) = c1. [back_rewrite(2491),rewrite(3776(17))]. given #708 (T,wt=10): 3819 c2 ^ c1' != 0 | (c2 ^ c1') v (c2 ^ (c1 v x)) = c1. [back_rewrite(2484),rewrite(3776(17))]. given #709 (T,wt=10): 4430 c1 ^ (((c1 v x) ^ (c2 v y)) v z)' = 0. [para(3618(a,1),1269(a,1,2)),rewrite(4(9))]. given #710 (A,wt=11): 258 (c2 ^ x) v ((c1 ^ x)' v y) = 1. [para(233(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #711 (T,wt=10): 4623 c1 ^ (((x v c1) ^ (c2 v y)) v z)' = 0. [para(4409(a,1),1269(a,1,2)),rewrite(4(9))]. given #712 (T,wt=10): 4661 c1 ^ (((c1 v x) ^ (y v c2)) v z)' = 0. [para(4410(a,1),1269(a,1,2)),rewrite(4(9))]. given #713 (T,wt=10): 4689 c1 ^ (x v ((c1 v y) ^ (c2 v z)))' = 0. [para(4411(a,1),1269(a,1,2)),rewrite(4(9))]. given #714 (T,wt=10): 4717 c1 ^ (((c2 v x) ^ (c1 v y)) v z)' = 0. [para(4412(a,1),1269(a,1,2)),rewrite(4(9))]. given #715 (A,wt=16): 262 c2 ^ (x ^ (c1 ^ x)') != 0 | (c2 ^ x)' = (c1 ^ x)'. [para(233(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #716 (T,wt=10): 4741 c1 ^ (((c2 v x) ^ (c2 v y)) v z)' = 0. [para(4423(a,1),1269(a,1,2)),rewrite(4(9))]. given #717 (T,wt=10): 4785 c1 ^ (((x v c2) ^ (c2 v y)) v z)' = 0. [para(4424(a,1),1269(a,1,2)),rewrite(4(9))]. given #718 (T,wt=10): 5051 c1 v c2' != 1 | (c1 v c2') ^ (c1 v (c2 ^ x)) = c2. [para(1997(a,1),180(b,1)),rewrite(2(4),304(12),2(15),2156(21)),flip(c),xx(b)]. given #719 (T,wt=10): 5052 c1 v c2' != 1 | (c1 v c2') ^ (c1 v (x ^ c2)) = c2. [para(2008(a,1),180(b,1)),rewrite(2(4),304(12),2(15),2156(21)),flip(c),xx(b)]. given #720 (A,wt=19): 263 (c2 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c1 v x)))))) v (c1 ^ (x v (c1 ^ y)))' = 1. [para(12(a,1),233(a,1,2,1))]. given #721 (T,wt=10): 5142 c1 ^ (((x v c1) ^ (y v c2)) v z)' = 0. [para(4605(a,1),1269(a,1,2)),rewrite(4(9))]. given #722 (T,wt=10): 5174 c1 ^ (x v ((y v c1) ^ (c2 v z)))' = 0. [para(4606(a,1),1269(a,1,2)),rewrite(4(9))]. given #723 (T,wt=10): 5237 c1 ^ (((c2 v x) ^ (y v c1)) v z)' = 0. [para(4608(a,1),1269(a,1,2)),rewrite(4(9))]. given #724 (T,wt=10): 5269 c1 ^ (x v ((c1 v y) ^ (z v c2)))' = 0. [para(4642(a,1),1269(a,1,2)),rewrite(4(9))]. given #725 (A,wt=11): 264 (c2 ^ x) v (y v (c1 ^ x)') = 1. [para(233(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #726 (T,wt=10): 5300 c1 ^ (((x v c2) ^ (c1 v y)) v z)' = 0. [para(4644(a,1),1269(a,1,2)),rewrite(4(9))]. given #727 (T,wt=10): 5327 c1 ^ (((c2 v x) ^ (y v c2)) v z)' = 0. [para(4654(a,1),1269(a,1,2)),rewrite(4(9))]. given #728 (T,wt=10): 5384 c1 ^ (((x v c2) ^ (y v c2)) v z)' = 0. [para(4655(a,1),1269(a,1,2)),rewrite(4(9))]. given #729 (T,wt=10): 5413 c1 ^ (x v ((c2 v y) ^ (c1 v z)))' = 0. [para(4673(a,1),1269(a,1,2)),rewrite(4(9))]. given #730 (A,wt=15): 265 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y))' = 1. [para(19(a,1),233(a,1,1))]. given #731 (T,wt=10): 5445 c1 ^ (x v ((c2 v y) ^ (c2 v z)))' = 0. [para(4683(a,1),1269(a,1,2)),rewrite(4(9))]. given #732 (T,wt=10): 5476 c1 ^ (x v ((y v c2) ^ (c2 v z)))' = 0. [para(4684(a,1),1269(a,1,2)),rewrite(4(9))]. given #733 (T,wt=10): 5695 c1 ^ (x v ((y v c1) ^ (z v c2)))' = 0. [para(5125(a,1),1269(a,1,2)),rewrite(4(9))]. given #734 (T,wt=10): 5726 c1 ^ (((x v c2) ^ (y v c1)) v z)' = 0. [para(5128(a,1),1269(a,1,2)),rewrite(4(9))]. given #735 (A,wt=15): 266 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y))' = 1. [para(19(a,1),233(a,1,2,1))]. given #736 (T,wt=10): 5758 c1 ^ (x v ((c2 v y) ^ (z v c1)))' = 0. [para(5159(a,1),1269(a,1,2)),rewrite(4(9))]. given #737 (T,wt=10): 5788 c1 ^ (x v ((y v c2) ^ (c1 v z)))' = 0. [para(5254(a,1),1269(a,1,2)),rewrite(4(9))]. given #738 (T,wt=10): 5851 c1 ^ (x v ((c2 v y) ^ (z v c2)))' = 0. [para(5263(a,1),1269(a,1,2)),rewrite(4(9))]. given #739 (T,wt=10): 5883 c1 ^ (x v ((y v c2) ^ (z v c2)))' = 0. [para(5264(a,1),1269(a,1,2)),rewrite(4(9))]. given #740 (A,wt=12): 268 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y)' = 1. [para(22(a,1),233(a,1,2,1))]. given #741 (T,wt=8): 10145 (c2 ^ (c1 v x)) v (c1 ^ y)' = 1. [para(268(a,1),160(a,1,2)),rewrite(2(6),61(6)),flip(a)]. given #742 (T,wt=8): 10177 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1. [para(10145(a,1),2(a,1)),flip(a)]. given #743 (T,wt=8): 10178 (c2 ^ (x v c1)) v (c1 ^ y)' = 1. [para(2(a,1),10145(a,1,1,2))]. given #744 (T,wt=8): 10180 (c2 ^ (c1 v x)) v (y ^ c1)' = 1. [para(4(a,1),10145(a,1,2,1))]. given #745 (A,wt=14): 269 (c2 ^ (x ^ ((c1 ^ x) v y))) v (c1 ^ x)' = 1. [para(23(a,1),233(a,1,2,1))]. given #746 (T,wt=8): 10194 (c1 ^ x)' v (c2 ^ (y v c1)) = 1. [para(2(a,1),10177(a,1,2,2))]. given #747 (T,wt=8): 10195 (x ^ c1)' v (c2 ^ (c1 v y)) = 1. [para(4(a,1),10177(a,1,1,1))]. given #748 (T,wt=8): 10207 (c2 ^ (x v c1)) v (y ^ c1)' = 1. [para(4(a,1),10178(a,1,2,1))]. given #749 (T,wt=8): 10283 (x ^ c1)' v (c2 ^ (y v c1)) = 1. [para(4(a,1),10194(a,1,1,1))]. given #750 (A,wt=11): 271 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),34(a,1,2,2,1))]. given #751 (T,wt=10): 5919 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z)' = 1. [para(5652(a,1),934(a,1,2)),rewrite(2(9))]. given #752 (T,wt=10): 5960 c2 v (((c2 ^ x) v (y ^ c1)) ^ z)' = 1. [para(5657(a,1),934(a,1,2)),rewrite(2(9))]. given #753 (T,wt=10): 6003 c1 ^ (x v ((y v c2) ^ (z v c1)))' = 0. [para(5681(a,1),1269(a,1,2)),rewrite(4(9))]. given #754 (T,wt=10): 6038 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z)' = 1. [para(5899(a,1),934(a,1,2)),rewrite(2(9))]. given #755 (A,wt=15): 272 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(34(a,1),5(a,1,1)),rewrite(74(2),5(5)),flip(a)]. given #756 (T,wt=10): 6076 c2 v (((x ^ c2) v (c1 ^ y)) ^ z)' = 1. [para(5901(a,1),934(a,1,2)),rewrite(2(9))]. given #757 (T,wt=10): 6115 c2 v (x ^ ((c2 ^ y) v (c1 ^ z)))' = 1. [para(5902(a,1),934(a,1,2)),rewrite(2(9))]. given #758 (T,wt=10): 6179 c2 v (((x ^ c1) v (c1 ^ y)) ^ z)' = 1. [para(5911(a,1),934(a,1,2)),rewrite(2(9))]. given #759 (T,wt=10): 6219 c2 v (((x ^ c1) v (c2 ^ y)) ^ z)' = 1. [para(5940(a,1),934(a,1,2)),rewrite(2(9))]. given #760 (A,wt=19): 273 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(34(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #761 (T,wt=10): 6257 c2 v (((x ^ c2) v (y ^ c1)) ^ z)' = 1. [para(5942(a,1),934(a,1,2)),rewrite(2(9))]. given #762 (T,wt=10): 6296 c2 v (x ^ ((c2 ^ y) v (z ^ c1)))' = 1. [para(5943(a,1),934(a,1,2)),rewrite(2(9))]. given #763 (T,wt=10): 6323 (x ^ c2) v (x ^ (c1 v (c2 ^ y)))' = 1. [para(795(a,1),189(a,1,2,1,2))]. given #764 (T,wt=10): 6324 (x ^ c2) v (x ^ (c1 v (y ^ c2)))' = 1. [para(801(a,1),189(a,1,2,1,2))]. given #765 (A,wt=18): 274 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(34(a,1),10(b,1)),flip(c),xx(b)]. given #766 (T,wt=10): 6346 c2 v (((x ^ c1) v (y ^ c1)) ^ z)' = 1. [para(5952(a,1),934(a,1,2)),rewrite(2(9))]. given #767 (T,wt=10): 6385 c2 v (((c1 ^ x) v (y ^ c2)) ^ z)' = 1. [para(6020(a,1),934(a,1,2)),rewrite(2(9))]. given #768 (T,wt=10): 6422 c2 v (x ^ ((c1 ^ y) v (c2 ^ z)))' = 1. [para(6021(a,1),934(a,1,2)),rewrite(2(9))]. given #769 (T,wt=10): 6455 c2 v (((c1 ^ x) v (y ^ c1)) ^ z)' = 1. [para(6030(a,1),934(a,1,2)),rewrite(2(9))]. given #770 (A,wt=15): 275 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(34(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #771 (T,wt=10): 6499 c2 v (x ^ ((y ^ c2) v (c1 ^ z)))' = 1. [para(6060(a,1),934(a,1,2)),rewrite(2(9))]. given #772 (T,wt=10): 6537 c2 v (x ^ ((y ^ c1) v (c1 ^ z)))' = 1. [para(6107(a,1),934(a,1,2)),rewrite(2(9))]. given #773 (T,wt=10): 6570 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z)' = 1. [para(6163(a,1),934(a,1,2)),rewrite(2(9))]. given #774 (T,wt=10): 6609 c2 v (((x ^ c1) v (y ^ c2)) ^ z)' = 1. [para(6202(a,1),934(a,1,2)),rewrite(2(9))]. given #775 (A,wt=19): 276 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(19(a,1),34(a,1,2,2,1)),rewrite(5(5))]. given #776 (T,wt=10): 6656 c2 v (x ^ ((y ^ c1) v (c2 ^ z)))' = 1. [para(6203(a,1),934(a,1,2)),rewrite(2(9))]. given #777 (T,wt=10): 6693 c2 v (x ^ ((y ^ c2) v (z ^ c1)))' = 1. [para(6241(a,1),934(a,1,2)),rewrite(2(9))]. given #778 (T,wt=10): 6730 c2 v (x ^ ((y ^ c1) v (z ^ c1)))' = 1. [para(6288(a,1),934(a,1,2)),rewrite(2(9))]. given #779 (T,wt=10): 6767 c2 v (x ^ ((c1 ^ y) v (z ^ c2)))' = 1. [para(6369(a,1),934(a,1,2)),rewrite(2(9))]. given #780 (A,wt=13): 277 x ^ (y ^ ((x v z) ^ y)') = 0. [para(34(a,1),22(a,1,2)),rewrite(85(2)),flip(a)]. given #781 (T,wt=10): 6812 c2 v (x ^ ((c1 ^ y) v (z ^ c1)))' = 1. [para(6414(a,1),934(a,1,2)),rewrite(2(9))]. given #782 (T,wt=10): 6849 c2 v (x ^ ((c1 ^ y) v (c1 ^ z)))' = 1. [para(6519(a,1),934(a,1,2)),rewrite(2(9))]. given #783 (T,wt=10): 6886 c2 v (x ^ ((y ^ c1) v (z ^ c2)))' = 1. [para(6593(a,1),934(a,1,2)),rewrite(2(9))]. given #784 (T,wt=10): 6962 (x v c2) ^ (y ^ c1) = y ^ c1. [para(65(a,1),246(a,2)),rewrite(766(8))]. given #785 (A,wt=20): 282 c2 ^ ((c1 ^ x)' v (c2 ^ ((c2 ^ (c1 ^ x)') v y))) = c2 ^ ((c1 ^ x)' v (c2 ^ y)). [para(270(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12))]. given #786 (T,wt=10): 7014 c1 v (x v c2)' != 1 | (c2 v x)' = c1'. [para(2(a,1),251(a,1,2,1))]. given #787 (T,wt=10): 7016 c1 v (c2 v x)' != 1 | (x v c2)' = c1'. [para(2(a,1),256(a,1,2,1))]. given #788 (T,wt=10): 7043 c2 ^ (x ^ c1)' != 0 | (c1 ^ x)' = c2'. [para(4(a,1),281(a,1,2,1))]. given #789 (T,wt=10): 7045 c2 ^ (c1 ^ x)' != 0 | (x ^ c1)' = c2'. [para(4(a,1),287(a,1,2,1))]. given #790 (A,wt=20): 288 c2 ^ ((x ^ c1)' v (c2 ^ ((c2 ^ (x ^ c1)') v y))) = c2 ^ ((x ^ c1)' v (c2 ^ y)). [para(280(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12))]. given #791 (T,wt=10): 7183 c2 ^ (x v c1') != 0 | (c1' v x)' = c2. [para(2(a,1),318(a,1,2))]. given #792 (T,wt=10): 7187 c2 ^ (c1' v x) != 0 | (x v c1')' = c2. [para(2(a,1),319(a,1,2))]. given #793 (T,wt=10): 7349 (c2 v x) ^ c1' != 0 | (x v c2)' = c1'. [para(2(a,1),349(a,1,1))]. given #794 (T,wt=10): 7351 c1' ^ (x v c2) != 0 | (x v c2)' = c1'. [para(4(a,1),349(a,1))]. given #795 (A,wt=14): 292 c2 ^ ((c1 v x) ^ c1') != 0 | (c2 ^ (c1 v x))' = c1'. [para(261(a,1),10(a,1)),rewrite(5(10)),xx(a)]. given #796 (T,wt=10): 7352 (x v c2) ^ c1' != 0 | (c2 v x)' = c1'. [para(2(a,1),352(a,1,1))]. given #797 (T,wt=10): 7353 c1' ^ (c2 v x) != 0 | (c2 v x)' = c1'. [para(4(a,1),352(a,1))]. given #798 (T,wt=10): 7355 c1 v (x ^ c2') != 1 | (c2' ^ x)' = c1. [para(4(a,1),389(a,1,2))]. given #799 (T,wt=10): 7357 c1 v (c2' ^ x) != 1 | (x ^ c2')' = c1. [para(4(a,1),390(a,1,2))]. given #800 (A,wt=14): 298 c2 ^ ((x v c1) ^ c1') != 0 | (c2 ^ (x v c1))' = c1'. [para(267(a,1),10(a,1)),rewrite(5(10)),xx(a)]. given #801 (T,wt=10): 7417 c2' v (x ^ c1) != 1 | (x ^ c1)' = c2'. [para(2(a,1),431(a,1))]. given #802 (T,wt=10): 7418 (c1 ^ x) v c2' != 1 | (x ^ c1)' = c2'. [para(4(a,1),431(a,1,1))]. given #803 (T,wt=10): 7420 c2' v (c1 ^ x) != 1 | (c1 ^ x)' = c2'. [para(2(a,1),435(a,1))]. given #804 (T,wt=10): 7421 (x ^ c1) v c2' != 1 | (c1 ^ x)' = c2'. [para(4(a,1),435(a,1,1))]. given #805 (A,wt=20): 300 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),36(a,1))]. given #806 (T,wt=10): 7652 c2 ^ (x v c1) != 1 | c1 != 0 | c1' = c2 ^ (c1 v x). [para(2(a,1),841(a,1,2))]. given #807 (T,wt=10): 7655 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (c1 v x))' = c1. [para(2(a,1),846(a,1,2))]. given #808 (T,wt=10): 7656 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (x ^ c2))' = c1. [para(12(a,1),846(a,1)),rewrite(795(6),4(15),13(15),2(16),120(16),801(17),62(16),801(15))]. given #809 (T,wt=10): 7658 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (c2 ^ x))' = c1. [para(44(a,1),846(a,1)),rewrite(795(6),4(15),13(15),2(16),120(16),795(17),62(16),795(15))]. given #810 (A,wt=12): 301 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),36(b,1))]. given #811 (T,wt=10): 7659 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (x ^ c2))' = c1. [para(801(a,1),846(a,1)),rewrite(801(15))]. given #812 (T,wt=10): 7727 (c2 ^ c1')' v (x ^ c1) = (c2 ^ c1')'. [para(7714(a,1),117(a,1,2,2))]. given #813 (T,wt=10): 7737 (x ^ (c2 ^ c1')') v (x ^ c1)' = 1. [para(7714(a,1),200(a,1,2,1,2))]. given #814 (T,wt=10): 7771 (c2 ^ c1')' != 1 | c1 != 0 | (c2 ^ c1')' = c1'. [para(7720(a,1),10(b,1)),rewrite(7719(7)),flip(c)]. given #815 (A,wt=20): 302 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),36(b,1))]. given #816 (T,wt=10): 7806 (x v c1) ^ (x v (c2 ^ c1')')' = 0. [para(7719(a,1),149(a,1,2,1,2))]. given #817 (T,wt=10): 7810 (c1 ^ x) v (c2 ^ c1')' = (c2 ^ c1')'. [para(7719(a,1),165(a,1,1)),rewrite(20(14)),flip(a)]. given #818 (T,wt=10): 7811 c1 ^ (((c2 ^ c1')' ^ (c2 v x)) v y) = c1. [para(7719(a,1),3618(a,1,2,1,1))]. given #819 (T,wt=10): 7812 c1 ^ (((c2 ^ c1')' ^ (x v c2)) v y) = c1. [para(7719(a,1),4410(a,1,2,1,1))]. given #820 (A,wt=12): 303 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),36(a,1)),rewrite(4(4),79(4)),flip(a)]. given #821 (T,wt=10): 7813 c1 ^ (x v ((c2 ^ c1')' ^ (c2 v y))) = c1. [para(7719(a,1),4411(a,1,2,2,1))]. given #822 (T,wt=10): 7814 c1 ^ (((c2 v x) ^ (c2 ^ c1')') v y) = c1. [para(7719(a,1),4412(a,1,2,1,2))]. given #823 (T,wt=10): 7815 c1 ^ (x v ((c2 ^ c1')' ^ (y v c2))) = c1. [para(7719(a,1),4642(a,1,2,2,1))]. given #824 (T,wt=10): 7816 c1 ^ (((x v c2) ^ (c2 ^ c1')') v y) = c1. [para(7719(a,1),4644(a,1,2,1,2))]. given #825 (A,wt=20): 305 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(17(a,1),36(a,1))]. given #826 (T,wt=10): 7817 c1 ^ (x v ((c2 v y) ^ (c2 ^ c1')')) = c1. [para(7719(a,1),4673(a,1,2,2,2))]. given #827 (T,wt=10): 7818 c1 ^ (x v ((y v c2) ^ (c2 ^ c1')')) = c1. [para(7719(a,1),5254(a,1,2,2,2))]. given #828 (T,wt=10): 7820 ((c2 ^ c1')' ^ x) v (c1 ^ x)' = 1. [para(7719(a,1),202(a,1,1,1))]. Low Water (keep, True_semantics): wt=25 given #829 (T,wt=10): 7875 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0. [para(845(a,1),209(a,1,1)),rewrite(57(10),845(15))]. given #830 (A,wt=20): 306 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(19(a,1),36(b,1))]. given #831 (T,wt=10): 7876 (c2 ^ (x v c1))' ^ (y ^ c1) = 0. [para(885(a,1),209(a,1,1)),rewrite(57(10),885(15))]. given #832 (T,wt=10): 7965 c1 v ((c2 ^ c1')' ^ (x ^ c2)) = c1. [para(7714(a,1),209(a,1,1)),rewrite(7714(17))]. given #833 (T,wt=10): 8145 c1' ^ (c2 ^ c1')' != 0 | (c2 ^ c1')' = c1. [para(7780(a,1),107(a,1)),rewrite(304(16),2(18),198(18),54(21)),flip(c),xx(a)]. given #834 (T,wt=10): 8466 c1 v (c2 ^ (x v c1))' != 1 | c2 ^ (c1 v x) = c1. [para(2(a,1),890(a,1,2,1,2))]. given #835 (A,wt=24): 307 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [para(21(a,1),36(b,1)),rewrite(2(4),17(4),17(3),3(2),123(4))]. given #836 (T,wt=10): 8467 c1 v (c1 v (c2 ^ x))' != 1 | c1 v (x ^ c2) = c1. [para(12(a,1),890(a,1,2,1)),rewrite(795(7),4(15),13(15),2(16),120(16),801(17),62(16),801(15))]. given #837 (T,wt=10): 8521 c1 v (c2 ^ (c1 v x))' != 1 | c2 ^ (x v c1) = c1. [para(2(a,1),897(a,1,2,1,2))]. given #838 (T,wt=10): 8569 c2 ^ (c1 v x) != 1 | c1 != 0 | c1' = c2 ^ (x v c1). [para(2(a,1),963(a,1,2))]. given #839 (T,wt=10): 8571 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (x v c1))' = c1. [para(2(a,1),965(a,1,2))]. given #840 (A,wt=12): 308 1 != x | x ^ y != 0 | (y ^ x)' = x. [para(26(a,1),36(a,1)),rewrite(4(4),86(4)),flip(a)]. given #841 (T,wt=10): 8573 c2 != 1 | c1 v (x ^ c2) != 0 | c2' = c1 v (c2 ^ x). [para(4(a,1),1063(b,1,2))]. given #842 (T,wt=10): 8576 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (c2 ^ x))' = c2. [para(4(a,1),1068(b,1,2))]. given #843 (T,wt=10): 8578 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (c1 v x))' = c2. [para(612(a,1),1068(b,1)),rewrite(612(15))]. given #844 (T,wt=10): 8579 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (x v c1))' = c2. [para(617(a,1),1068(b,1)),rewrite(617(15))]. given #845 (A,wt=20): 312 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x. [para(24(a,1),36(a,1)),rewrite(4(6))]. given #846 (T,wt=8): 12207 c1 v x != 1 | c1 != 0 | (c1 v x)' = c1. [para(13(a,1),312(b,1,2,1)),rewrite(6(8),13(10))]. given #847 (T,wt=8): 12214 c2 != 1 | c2 ^ x != 0 | (c2 ^ x)' = c2. [para(405(a,1),312(b,1,2)),rewrite(126(4),79(7),405(12))]. given #848 (T,wt=8): 12288 x v c1 != 1 | c1 != 0 | (c1 v x)' = c1. [para(2(a,1),12207(a,1))]. given #849 (T,wt=8): 12290 x v c1 != 1 | c1 != 0 | (x v c1)' = c1. [para(51(a,1),12207(a,1)),rewrite(51(12))]. given #850 (A,wt=24): 313 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x. [para(25(a,1),36(a,1)),rewrite(4(7))]. given #851 (T,wt=8): 12292 c2 != 1 | x ^ c2 != 0 | (c2 ^ x)' = c2. [para(4(a,1),12214(b,1))]. given #852 (T,wt=8): 12294 c2 != 1 | x ^ c2 != 0 | (x ^ c2)' = c2. [para(65(a,1),12214(b,1)),rewrite(65(12))]. given #853 (T,wt=8): 12297 c1 v x != 1 | c1 != 0 | (x v c1)' = c1. [para(2(a,1),12290(a,1))]. given #854 (T,wt=8): 12510 c2 != 1 | c2 ^ x != 0 | (x ^ c2)' = c2. [para(4(a,1),12294(b,1))]. given #855 (A,wt=12): 314 x ^ (x ^ y)' != 0 | x ^ y = x. [para(161(a,1),36(a,1)),rewrite(4(6),304(11)),xx(a)]. Low Water (keep, True_semantics): wt=24 given #856 (T,wt=9): 12304 c1 v c2' != 1 | (c2 ^ (c1 v c2'))' = c2'. [para(511(a,1),313(b,1)),rewrite(2(4),2(14),4(16),612(17)),xx(b)]. given #857 (T,wt=10): 8694 x ^ ((x ^ c1) v (c1 ^ y)) = x ^ c1. [para(224(a,1),23(a,1,2)),rewrite(5495(7))]. given #858 (T,wt=10): 8712 x ^ ((c1 ^ x) v (c1 ^ y)) = x ^ c1. [para(224(a,1),137(a,1,2)),rewrite(3776(7))]. given #859 (T,wt=10): 8776 c2 ^ (c1 v (x ^ c2))' != 0 | c1 v (c2 ^ x) = c2. [para(4(a,1),1080(a,1,2,1,2))]. given #860 (A,wt=12): 315 x ^ (y ^ x)' != 0 | y ^ x = x. [para(188(a,1),36(a,1)),rewrite(4(6),304(11)),xx(a)]. given #861 (T,wt=10): 8834 c2 ^ (c1 v (c2 ^ x))' != 0 | c1 v (x ^ c2) = c2. [para(4(a,1),1088(a,1,2,1,2))]. given #862 (T,wt=10): 8859 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (x ^ c2))' = c2. [para(4(a,1),1155(b,1,2))]. given #863 (T,wt=10): 8922 c1 ^ ((c2 ^ x) v (x ^ y)) = c1 ^ x. [para(12(a,1),230(a,1,2)),rewrite(5495(6))]. given #864 (T,wt=10): 8963 (c1 ^ ((c2 ^ x) v y)) v (c1 ^ x)' = 1. [para(230(a,1),200(a,1,2,1))]. given #865 (A,wt=24): 317 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),212(7))]. given #866 (T,wt=10): 9089 (x v c2) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(2(a,1),2186(a,1,1))]. given #867 (T,wt=10): 9090 (c1 v (c2 ^ x)) ^ (c2 v y) = c1 v (c2 ^ x). [para(2186(a,1),4(a,1)),flip(a)]. given #868 (T,wt=8): 12755 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0. [para(9090(a,1),1269(a,1,2))]. given #869 (T,wt=8): 12762 (x v c2)' ^ (c1 v (c2 ^ y)) = 0. [para(2(a,1),12755(a,1,1,1))]. given #870 (A,wt=18): 320 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 #871 (T,wt=8): 12763 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0. [para(12755(a,1),4(a,1)),flip(a)]. given #872 (T,wt=8): 12764 (c2 v x)' ^ (c1 v (y ^ c2)) = 0. [para(4(a,1),12755(a,1,2,2))]. given #873 (T,wt=8): 12785 (c1 v (c2 ^ x)) ^ (y v c2)' = 0. [para(12762(a,1),4(a,1)),flip(a)]. given #874 (T,wt=8): 12786 (x v c2)' ^ (c1 v (y ^ c2)) = 0. [para(4(a,1),12762(a,1,2,2))]. given #875 (A,wt=14): 321 c2 ^ (x ^ (c1 ^ x)') != 0 | c2 ^ x = c1 ^ x. [para(233(a,1),36(a,1)),rewrite(4(9),5(9),304(15)),flip(c),xx(a)]. given #876 (T,wt=8): 12816 (c1 v (x ^ c2)) ^ (c2 v y)' = 0. [para(4(a,1),12763(a,1,1,2))]. given #877 (T,wt=8): 12847 (c1 v (x ^ c2)) ^ (y v c2)' = 0. [para(4(a,1),12785(a,1,1,2))]. given #878 (T,wt=10): 9132 (x v c2) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(2(a,1),2187(a,1,1))]. given #879 (T,wt=10): 9133 (c1 v (x ^ c2)) ^ (c2 v y) = c1 v (x ^ c2). [para(2187(a,1),4(a,1)),flip(a)]. given #880 (A,wt=12): 324 c2 ^ (c1' ^ (c1 v x)) != 0 | c2 ^ (c1 v x) = c1. [para(261(a,1),36(a,1)),rewrite(19(10),304(15)),flip(c),xx(a)]. given #881 (T,wt=9): 12951 c2 ^ c1' != 0 | c1 v (c2 ^ (c1' v x)) = c1. [para(1238(a,1),324(a,1,2)),rewrite(79(6),795(15))]. given #882 (T,wt=9): 12952 c2 ^ c1' != 0 | c1 v (c2 ^ (x v c1')) = c1. [para(1247(a,1),324(a,1,2)),rewrite(79(6),795(15))]. given #883 (T,wt=10): 9245 (c1 v x) ^ (x v (c2 ^ (c1 v y)))' = 0. [para(2(a,1),3040(a,1,1))]. given #884 (T,wt=10): 9246 (x v c1) ^ ((c2 ^ (c1 v y)) v x)' = 0. [para(2(a,1),3040(a,1,2,1))]. given #885 (A,wt=12): 325 c2 ^ (c1' ^ (x v c1)) != 0 | c2 ^ (x v c1) = c1. [para(267(a,1),36(a,1)),rewrite(19(10),304(15)),flip(c),xx(a)]. given #886 (T,wt=10): 9260 (c1 v x) ^ (x v (c2 ^ (y v c1)))' = 0. [para(2(a,1),3041(a,1,1))]. given #887 (T,wt=10): 9261 (x v c1) ^ ((c2 ^ (y v c1)) v x)' = 0. [para(2(a,1),3041(a,1,2,1))]. given #888 (T,wt=10): 9305 (c2 ^ (c1 v x)) v (c1 ^ y) = c2 ^ (c1 v x). [para(3793(a,1),2(a,1)),flip(a)]. given #889 (T,wt=10): 9307 (x ^ c1) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(4(a,1),3793(a,1,1))]. given #890 (A,wt=20): 332 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 #891 (T,wt=10): 9352 (c2 ^ (x v c1)) v (c1 ^ y) = c2 ^ (x v c1). [para(3795(a,1),2(a,1)),flip(a)]. given #892 (T,wt=10): 9355 (x ^ c1) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(4(a,1),3795(a,1,1))]. given #893 (T,wt=10): 10527 (c2 ^ x) v (x ^ (c1 v (c2 ^ y)))' = 1. [para(4(a,1),6323(a,1,1))]. given #894 (T,wt=10): 10528 (x ^ c2) v ((c1 v (c2 ^ y)) ^ x)' = 1. [para(4(a,1),6323(a,1,2,1))]. given #895 (A,wt=20): 333 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z. [para(2(a,1),37(b,1,1))]. given #896 (T,wt=10): 10542 (c2 ^ x) v (x ^ (c1 v (y ^ c2)))' = 1. [para(4(a,1),6324(a,1,1))]. given #897 (T,wt=10): 10543 (x ^ c2) v ((c1 v (y ^ c2)) ^ x)' = 1. [para(4(a,1),6324(a,1,2,1))]. given #898 (T,wt=10): 10975 c1' ^ (c2 v x) != 0 | (x v c2)' = c1'. [para(4(a,1),7349(a,1))]. given #899 (T,wt=10): 10979 c1' ^ (x v c2) != 0 | (c2 v x)' = c1'. [para(4(a,1),7352(a,1))]. given #900 (A,wt=20): 334 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z. [para(4(a,1),37(b,1))]. given #901 (T,wt=10): 10987 c2' v (c1 ^ x) != 1 | (x ^ c1)' = c2'. [para(4(a,1),7417(a,1,2))]. given #902 (T,wt=10): 10989 c2' v (x ^ c1) != 1 | (c1 ^ x)' = c2'. [para(4(a,1),7420(a,1,2))]. given #903 (T,wt=10): 11168 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (c2 ^ x))' = c1. [para(4(a,1),7658(a,1,2))]. given #904 (T,wt=10): 11207 (x ^ c1) v (c2 ^ c1')' = (c2 ^ c1')'. [para(7727(a,1),2(a,1)),flip(a)]. given #905 (A,wt=16): 335 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),37(a,1,2)),rewrite(19(6),77(6))]. given #906 (T,wt=10): 11209 (c2 ^ c1')' v (c1 ^ x) = (c2 ^ c1')'. [para(4(a,1),7727(a,1,2))]. given #907 (T,wt=10): 11231 (x ^ c1)' v (x ^ (c2 ^ c1')') = 1. [para(7737(a,1),2(a,1)),flip(a)]. given #908 (T,wt=10): 11233 ((c2 ^ c1')' ^ x) v (x ^ c1)' = 1. [para(4(a,1),7737(a,1,1))]. given #909 (T,wt=10): 11234 (x ^ (c2 ^ c1')') v (c1 ^ x)' = 1. [para(4(a,1),7737(a,1,2,1))]. given #910 (A,wt=14): 336 (x v y) ^ y' != 0 | (x v y)' = y'. [para(8(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #911 (T,wt=10): 11475 (c1 v x) ^ (x v (c2 ^ c1')')' = 0. [para(2(a,1),7806(a,1,1))]. given #912 (T,wt=10): 11476 (x v c1) ^ ((c2 ^ c1')' v x)' = 0. [para(2(a,1),7806(a,1,2,1))]. given #913 (T,wt=10): 11983 (c1 ^ x)' v ((c2 ^ c1')' ^ x) = 1. [para(7820(a,1),2(a,1)),flip(a)]. given #914 (T,wt=10): 12197 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (c1 v x))' = c2. [para(2(a,1),8578(b,1,2))]. given #915 (A,wt=20): 337 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(17(a,1),37(a,1))]. given #916 (T,wt=10): 12200 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (x v c1))' = c2. [para(2(a,1),8579(b,1,2))]. given #917 (T,wt=10): 12307 x v c2 != 1 | 0 != x | (c2 v x)' = x. [para(778(a,1),313(b,1,2,2)),rewrite(17(8),128(8),20(7),778(12),17(10),128(10)),flip(b)]. given #918 (T,wt=10): 12516 x ^ ((c1 ^ y) v (x ^ c1)) = x ^ c1. [para(2(a,1),8694(a,1,2))]. given #919 (T,wt=10): 12517 x ^ ((x ^ c1) v (y ^ c1)) = x ^ c1. [para(4(a,1),8694(a,1,2,2))]. given #920 (A,wt=16): 340 x v y != 1 | x v y != 0 | (x v y)' = x v y. [para(28(a,1),37(b,1)),rewrite(91(2),62(2))]. given #921 (T,wt=10): 12537 x ^ ((c1 ^ y) v (c1 ^ x)) = x ^ c1. [para(2(a,1),8712(a,1,2))]. given #922 (T,wt=10): 12538 x ^ ((c1 ^ x) v (y ^ c1)) = x ^ c1. [para(4(a,1),8712(a,1,2,2))]. given #923 (T,wt=10): 12600 c1 ^ ((x ^ y) v (c2 ^ x)) = c1 ^ x. [para(2(a,1),8922(a,1,2))]. given #924 (T,wt=10): 12601 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(4(a,1),8922(a,1,2,1))]. given #925 (A,wt=12): 341 x v y != 1 | 0 != y | (x v y)' = y. [para(29(a,1),37(a,1,2)),rewrite(4(5),20(5)),flip(b)]. given #926 (T,wt=10): 12602 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(4(a,1),8922(a,1,2,2))]. given #927 (T,wt=10): 12646 (c1 ^ x)' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(8963(a,1),2(a,1)),flip(a)]. Low Water (keep, True_semantics): wt=23 given #928 (T,wt=10): 12647 (c1 ^ (x v (c2 ^ y))) v (c1 ^ y)' = 1. [para(2(a,1),8963(a,1,1,2))]. given #929 (T,wt=8): 14422 c1 v ((x ^ c1) v (c1 ^ y))' = 1. [para(6107(a,1),12647(a,1,1,2)),rewrite(13(3),5495(8))]. given #930 (A,wt=11): 343 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(120(a,1),37(a,1,2)),rewrite(4(8))]. given #931 (T,wt=8): 14446 c1 v ((x ^ c1) v (y ^ c1))' = 1. [para(4(a,1),14422(a,1,2,1,2))]. given #932 (T,wt=10): 12648 (c1 ^ ((x ^ c2) v y)) v (c1 ^ x)' = 1. [para(4(a,1),8963(a,1,1,2,1))]. given #933 (T,wt=10): 12649 (c1 ^ ((c2 ^ x) v y)) v (x ^ c1)' = 1. [para(4(a,1),8963(a,1,2,1))]. given #934 (T,wt=10): 12662 (c1 ^ ((x ^ c2) v y)) v (x ^ c1)' = 1. [para(65(a,1),8963(a,1,1,2,1)),rewrite(237(10))]. given #935 (A,wt=12): 344 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y. [para(124(a,1),37(a,1,2)),rewrite(19(9),246(9))]. given #936 (T,wt=10): 12728 (c1 v (c2 ^ x)) ^ (y v c2) = c1 v (c2 ^ x). [para(9089(a,1),4(a,1)),flip(a)]. given #937 (T,wt=10): 12921 (c1 v (x ^ c2)) ^ (y v c2) = c1 v (x ^ c2). [para(9132(a,1),4(a,1)),flip(a)]. given #938 (T,wt=10): 12965 (c1 v x) ^ ((c2 ^ (c1 v y)) v x)' = 0. [para(2(a,1),9245(a,1,2,1))]. given #939 (T,wt=10): 13007 c2 ^ c1' != 0 | c2 ^ (c1 v ((c2 v x) ^ c1')) = c1. [para(141(a,1),325(a,1)),rewrite(2(14))]. given #940 (A,wt=20): 346 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(25(a,1),37(a,1)),rewrite(79(7))]. given #941 (T,wt=10): 13020 (c1 v x) ^ ((c2 ^ (y v c1)) v x)' = 0. [para(2(a,1),9260(a,1,2,1))]. given #942 (T,wt=10): 13063 (c2 ^ (c1 v x)) v (y ^ c1) = c2 ^ (c1 v x). [para(4(a,1),9305(a,1,2))]. given #943 (T,wt=10): 13235 (c2 ^ (x v c1)) v (y ^ c1) = c2 ^ (x v c1). [para(4(a,1),9352(a,1,2))]. given #944 (T,wt=10): 13268 (c2 ^ x) v ((c1 v (c2 ^ y)) ^ x)' = 1. [para(4(a,1),10527(a,1,2,1))]. given #945 (A,wt=18): 347 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(161(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #946 (T,wt=10): 13288 c1 v ((c2 ^ c1')' ^ (c1 v (c2 ^ x)))' = 1. [para(7714(a,1),10527(a,1,1))]. given #947 (T,wt=10): 13522 (c2 ^ x) v ((c1 v (y ^ c2)) ^ x)' = 1. [para(4(a,1),10542(a,1,2,1))]. given #948 (T,wt=10): 13542 c1 v ((c2 ^ c1')' ^ (c1 v (x ^ c2)))' = 1. [para(7714(a,1),10542(a,1,1))]. given #949 (T,wt=10): 13796 (c1 ^ x)' v (x ^ (c2 ^ c1')') = 1. [para(4(a,1),11231(a,1,1,1))]. given #950 (A,wt=18): 348 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(188(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #951 (T,wt=10): 13797 (x ^ c1)' v ((c2 ^ c1')' ^ x) = 1. [para(4(a,1),11231(a,1,2))]. Low Water (keep, True_semantics): wt=22 given #952 (T,wt=10): 13897 (c1 v x) ^ ((c2 ^ c1')' v x)' = 0. [para(2(a,1),11475(a,1,2,1))]. given #953 (T,wt=10): 14059 x ^ ((y ^ c1) v (x ^ c1)) = x ^ c1. [para(4(a,1),12516(a,1,2,1))]. given #954 (T,wt=10): 14104 x ^ ((y ^ c1) v (c1 ^ x)) = x ^ c1. [para(4(a,1),12537(a,1,2,1))]. given #955 (A,wt=14): 350 (x v c2) ^ (c1' v y) != 0 | (x v c2)' = c1' v y. [para(204(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #956 (T,wt=10): 14148 c1 ^ ((x ^ y) v (c2 ^ y)) = c1 ^ y. [para(4(a,1),12600(a,1,2,1))]. given #957 (T,wt=10): 14149 c1 ^ ((x ^ y) v (x ^ c2)) = c1 ^ x. [para(4(a,1),12600(a,1,2,2))]. given #958 (T,wt=10): 14189 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(4(a,1),12601(a,1,2,2))]. given #959 (T,wt=10): 14309 (c1 ^ x)' v (c1 ^ (y v (c2 ^ x))) = 1. [para(2(a,1),12646(a,1,2,2))]. given #960 (A,wt=14): 351 (x v c2) ^ (y v c1') != 0 | (x v c2)' = y v c1'. [para(207(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #961 (T,wt=10): 14310 (x ^ c1)' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(4(a,1),12646(a,1,1,1))]. given #962 (T,wt=10): 14311 (c1 ^ x)' v (c1 ^ ((x ^ c2) v y)) = 1. [para(4(a,1),12646(a,1,2,2,1))]. given #963 (T,wt=9): 15006 (c1 ^ x)' v (c1 ^ (x v y)) = 1. [para(125(a,1),14311(a,1,2,2)),rewrite(4(7),46(8))]. given #964 (T,wt=9): 15009 (c1 ^ x)' v (c1 ^ (y v x)) = 1. [para(2(a,1),15006(a,1,2,2))]. given #965 (A,wt=22): 353 (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(70(2)),xx(a)]. given #966 (T,wt=9): 15012 (x ^ c1)' v (c1 ^ (x v y)) = 1. [para(4(a,1),15006(a,1,1,1))]. given #967 (T,wt=9): 15043 (x ^ c1)' v (c1 ^ (y v x)) = 1. [para(4(a,1),15009(a,1,1,1))]. given #968 (T,wt=9): 15108 (c1 ^ (x v y)) v (y ^ c1)' = 1. [para(15043(a,1),2(a,1)),flip(a)]. given #969 (T,wt=10): 14318 (c1 ^ x)' v (c1 ^ ((x ^ c1) v y)) = 1. [para(47(a,1),12646(a,1,2,2,1)),rewrite(86(4))]. given #970 (A,wt=18): 354 (x v (c2 ^ y)) ^ (c1 ^ y)' != 0 | (x v (c2 ^ y))' = (c1 ^ y)'. [para(233(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #971 (T,wt=10): 14323 (x ^ c1)' v (c1 ^ ((x ^ c2) v y)) = 1. [para(65(a,1),12646(a,1,2,2,1)),rewrite(237(5))]. given #972 (T,wt=10): 14330 (c1 ^ x)' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(79(a,1),12646(a,1,1,1)),rewrite(19(8),46(8))]. given #973 (T,wt=10): 14369 (c1 ^ (x v (y ^ c2))) v (c1 ^ y)' = 1. [para(4(a,1),12647(a,1,1,2,2))]. given #974 (T,wt=10): 14370 (c1 ^ (x v (c2 ^ y))) v (y ^ c1)' = 1. [para(4(a,1),12647(a,1,2,1))]. given #975 (A,wt=14): 355 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'. [para(270(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #976 (T,wt=10): 14379 (c1 ^ (x v (y ^ c1))) v (c1 ^ y)' = 1. [para(47(a,1),12647(a,1,1,2,2)),rewrite(86(9))]. given #977 (T,wt=10): 14383 (c1 ^ (x v (y ^ c2))) v (y ^ c1)' = 1. [para(65(a,1),12647(a,1,1,2,2)),rewrite(237(10))]. given #978 (T,wt=10): 14635 c1 v ((c1 v (c2 ^ x)) ^ (c2 ^ c1')')' = 1. [para(7714(a,1),13268(a,1,1))]. given #979 (T,wt=10): 14700 c1 v ((c1 v (x ^ c2)) ^ (c2 ^ c1')')' = 1. [para(7714(a,1),13522(a,1,1))]. given #980 (A,wt=14): 356 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'. [para(280(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #981 (T,wt=10): 14817 c1 ^ ((x ^ y) v (y ^ c2)) = c1 ^ y. [para(4(a,1),14148(a,1,2,2))]. given #982 (T,wt=10): 14945 (x ^ c1)' v (c1 ^ (y v (c2 ^ x))) = 1. [para(4(a,1),14309(a,1,1,1))]. given #983 (T,wt=10): 14946 (c1 ^ x)' v (c1 ^ (y v (x ^ c2))) = 1. [para(4(a,1),14309(a,1,2,2,2))]. given #984 (T,wt=10): 14951 (c1 ^ x)' v (c1 ^ (y v (x ^ c1))) = 1. [para(47(a,1),14309(a,1,2,2,2)),rewrite(86(4))]. given #985 (A,wt=16): 357 (x v (c2 ^ (c1 v y))) ^ c1' != 0 | (x v (c2 ^ (c1 v y)))' = c1'. [para(261(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #986 (T,wt=10): 14953 (x ^ c1)' v (c1 ^ (y v (x ^ c2))) = 1. [para(65(a,1),14309(a,1,2,2,2)),rewrite(237(5))]. given #987 (T,wt=10): 14960 (c1 ^ x)' v (c1 ^ (y v (c1 ^ x))) = 1. [para(79(a,1),14309(a,1,1,1)),rewrite(19(8),46(8))]. given #988 (T,wt=10): 15145 (x ^ c1)' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),14330(a,1,1,1))]. given #989 (T,wt=10): 15279 (x ^ c1)' v (c1 ^ (y v (x ^ c1))) = 1. [para(4(a,1),14951(a,1,1,1))]. given #990 (A,wt=16): 358 (x v (c2 ^ (y v c1))) ^ c1' != 0 | (x v (c2 ^ (y v c1)))' = c1'. [para(267(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #991 (T,wt=10): 15293 (x ^ c1)' v (c1 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),14960(a,1,1,1))]. given #992 (T,wt=10): 15325 (c1 ^ (x v (c1 ^ y))) v (y ^ c1)' = 1. [para(15293(a,1),2(a,1)),flip(a)]. given #993 (T,wt=11): 361 (x ^ c2) v ((c1 ^ x)' v y) = 1. [para(259(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #994 (T,wt=11): 365 (x ^ c2) v (y v (c1 ^ x)') = 1. [para(259(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #995 (A,wt=18): 359 c2 ^ ((x v c1') ^ (c1 v y)) != 0 | (x v c1')' = c2 ^ (c1 v y). [para(290(a,1),37(a,1,2)),rewrite(70(2),19(11)),xx(a)]. given #996 (T,wt=11): 368 (c2 ^ x) v ((x ^ c1)' v y) = 1. [para(260(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #997 (T,wt=11): 371 (c2 ^ x) v (y v (x ^ c1)') = 1. [para(260(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #998 (T,wt=11): 374 (x ^ c2) v ((x ^ c1)' v y) = 1. [para(362(a,1),3(a,1,1)),rewrite(61(2)),flip(a)]. given #999 (T,wt=11): 376 (x ^ c2) v (y v (x ^ c1)') = 1. [para(362(a,1),17(a,1,2)),rewrite(70(2)),flip(a)]. given #1000 (A,wt=18): 360 c2 ^ ((x v c1') ^ (y v c1)) != 0 | (x v c1')' = c2 ^ (y v c1). [para(295(a,1),37(a,1,2)),rewrite(70(2),19(11)),xx(a)]. given #1001 (T,wt=11): 392 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x)' = c1. [para(46(a,1),38(b,1)),rewrite(2(4))]. given #1002 (T,wt=11): 413 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1' = x ^ c2. [para(69(a,1),10(b,1))]. given #1003 (T,wt=11): 418 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2)' = c1. [para(69(a,1),38(b,1)),rewrite(2(4))]. given #1004 (T,wt=11): 443 c1 v (c2 ^ x) != 1 | x ^ c1 != 0 | (c2 ^ x)' = c1. [para(47(a,1),39(b,1)),rewrite(2(4))]. given #1005 (A,wt=15): 363 (x ^ (y ^ c2)) v (c1 ^ (x ^ y))' = 1. [para(5(a,1),259(a,1,1))]. given #1006 (T,wt=11): 452 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(129(a,1),10(a,1))]. given #1007 (T,wt=11): 467 (x v c1) ^ ((x v c2)' ^ y) = 0. [para(455(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #1008 (T,wt=11): 469 (x v c1) ^ (y ^ (x v c2)') = 0. [para(455(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #1009 (T,wt=11): 485 (c1 v x) ^ ((x v c2)' ^ y) = 0. [para(463(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #1010 (A,wt=16): 364 x ^ (c2 ^ (c1 ^ x)') != 0 | (c1 ^ x)' = (x ^ c2)'. [para(259(a,1),10(a,1)),rewrite(5(9)),flip(c),xx(a)]. given #1011 (T,wt=11): 488 (c1 v x) ^ (y ^ (x v c2)') = 0. [para(463(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #1012 (T,wt=11): 493 (x v c1) ^ ((c2 v x)' ^ y) = 0. [para(464(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #1013 (T,wt=11): 497 (x v c1) ^ (y ^ (c2 v x)') = 0. [para(464(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #1014 (T,wt=11): 544 (c1 v x) ^ ((c2 v x)' ^ y) = 0. [para(484(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #1015 (A,wt=14): 366 x ^ (c2 ^ (c1 ^ x)') != 0 | c1 ^ x = x ^ c2. [para(259(a,1),36(a,1)),rewrite(4(9),5(9),304(15)),xx(a)]. given #1016 (T,wt=11): 546 (c1 v x) ^ (y ^ (c2 v x)') = 0. [para(484(a,1),19(a,1,2)),rewrite(85(2)),flip(a)]. given #1017 (T,wt=11): 554 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x)' = c2. [para(130(a,1),37(a,1)),rewrite(4(8))]. given #1018 (T,wt=11): 634 (x v y) ^ (y v x) = x v y. [para(51(a,1),21(a,1,2))]. given #1019 (T,wt=11): 636 (x v (y ^ z)) ^ (x v y)' = 0. [para(51(a,1),148(a,1,2,1))]. given #1020 (A,wt=18): 367 (x v (y ^ c2)) ^ (c1 ^ y)' != 0 | (x v (y ^ c2))' = (c1 ^ y)'. [para(259(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #1021 (T,wt=10): 15592 (c1 v ((c2 v x) ^ y)) ^ (c2 v x)' = 0. [para(128(a,1),636(a,1,2,1))]. given #1022 (T,wt=10): 15593 (c1 v ((x v c2) ^ y)) ^ (x v c2)' = 0. [para(130(a,1),636(a,1,2,1))]. given #1023 (T,wt=10): 15596 (c2 v ((x v c1) ^ y)) ^ (c2 v x)' = 0. [para(450(a,1),636(a,1,2,1))]. given #1024 (T,wt=10): 15632 (c1 v ((x v c2) ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),15592(a,1,1,2,1))]. given #1025 (A,wt=15): 369 (c2 ^ (x ^ y)) v (x ^ (y ^ c1))' = 1. [para(5(a,1),260(a,1,2,1))]. given #1026 (T,wt=10): 15633 (c1 v ((c2 v x) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15592(a,1,2,1))]. given #1027 (T,wt=10): 15634 (c2 v x)' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(15592(a,1),4(a,1)),flip(a)]. given #1028 (T,wt=10): 15635 (c1 v (x ^ (c2 v y))) ^ (c2 v y)' = 0. [para(4(a,1),15592(a,1,1,2))]. given #1029 (T,wt=10): 15652 (x v c2)' ^ (c1 v ((x v c2) ^ y)) = 0. [para(15593(a,1),4(a,1)),flip(a)]. given #1030 (A,wt=16): 370 c2 ^ (x ^ (x ^ c1)') != 0 | (c2 ^ x)' = (x ^ c1)'. [para(260(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #1031 (T,wt=9): 15779 (x v c2)' ^ (c2 v (x ^ y)) = 0. [para(165(a,1),15652(a,1,2,2)),rewrite(2(7),128(8))]. given #1032 (T,wt=9): 15784 (x v c2)' ^ (c2 v (y ^ x)) = 0. [para(4(a,1),15779(a,1,2,2))]. given #1033 (T,wt=9): 15805 (c2 v x)' ^ (c2 v (y ^ x)) = 0. [para(2(a,1),15784(a,1,1,1))]. given #1034 (T,wt=9): 15807 (c2 v (x ^ y)) ^ (y v c2)' = 0. [para(15784(a,1),4(a,1)),flip(a)]. given #1035 (A,wt=14): 372 c2 ^ (x ^ (x ^ c1)') != 0 | c2 ^ x = x ^ c1. [para(260(a,1),36(a,1)),rewrite(4(9),5(9),304(15)),flip(c),xx(a)]. given #1036 (T,wt=10): 15653 (c1 v (x ^ (y v c2))) ^ (y v c2)' = 0. [para(4(a,1),15593(a,1,1,2))]. given #1037 (T,wt=10): 15665 (c2 v ((c1 v x) ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),15596(a,1,1,2,1))]. given #1038 (T,wt=10): 15666 (c2 v ((x v c1) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15596(a,1,2,1))]. given #1039 (T,wt=10): 15668 (c2 v x)' ^ (c2 v ((x v c1) ^ y)) = 0. [para(15596(a,1),4(a,1)),flip(a)]. given #1040 (A,wt=18): 373 (x v (c2 ^ y)) ^ (y ^ c1)' != 0 | (x v (c2 ^ y))' = (y ^ c1)'. [para(260(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #1041 (T,wt=10): 15669 (c2 v (x ^ (y v c1))) ^ (c2 v y)' = 0. [para(4(a,1),15596(a,1,1,2))]. given #1042 (T,wt=8): 15982 c2 ^ ((x v c2) ^ (c2 v y))' = 0. [para(4424(a,1),15669(a,1,1,2)),rewrite(2(3),120(3),2772(8))]. given #1043 (T,wt=8): 16016 c2 ^ ((x v c2) ^ (y v c2))' = 0. [para(2(a,1),15982(a,1,2,1,2))]. given #1044 (T,wt=10): 15718 (c2 v x)' ^ (c1 v ((x v c2) ^ y)) = 0. [para(15632(a,1),4(a,1)),flip(a)]. given #1045 (A,wt=16): 375 x ^ (c2 ^ (x ^ c1)') != 0 | (x ^ c2)' = (x ^ c1)'. [para(362(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #1046 (T,wt=10): 15719 (c1 v (x ^ (y v c2))) ^ (c2 v y)' = 0. [para(4(a,1),15632(a,1,1,2))]. given #1047 (T,wt=10): 15735 (x v c2)' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(15633(a,1),4(a,1)),flip(a)]. given #1048 (T,wt=10): 15736 (c1 v (x ^ (c2 v y))) ^ (y v c2)' = 0. [para(4(a,1),15633(a,1,1,2))]. given #1049 (T,wt=10): 15747 (c2 v x)' ^ (c1 v (y ^ (c2 v x))) = 0. [para(4(a,1),15634(a,1,2,2))]. given #1050 (A,wt=14): 377 x ^ (c2 ^ (x ^ c1)') != 0 | x ^ c2 = x ^ c1. [para(362(a,1),36(a,1)),rewrite(4(9),5(9),304(15)),flip(c),xx(a)]. given #1051 (T,wt=10): 15776 (x v c2)' ^ (c1 v (y ^ (x v c2))) = 0. [para(4(a,1),15652(a,1,2,2))]. given #1052 (T,wt=10): 15847 (c2 v x)' ^ (c2 v (y ^ (c2 v x))) = 0. [para(62(a,1),15805(a,1,1,1))]. given #1053 (T,wt=10): 15848 (c2 v x)' ^ (c2 v (y ^ (x v c1))) = 0. [para(450(a,1),15805(a,1,1,1))]. given #1054 (T,wt=10): 15850 (x v c2)' ^ (c2 v (y ^ (x v c2))) = 0. [para(91(a,1),15805(a,1,1,1))]. given #1055 (A,wt=18): 378 (x v (y ^ c2)) ^ (y ^ c1)' != 0 | (x v (y ^ c2))' = (y ^ c1)'. [para(362(a,1),37(a,1,2)),rewrite(70(2)),xx(a)]. given #1056 (T,wt=10): 15889 (c2 v ((c1 v x) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15665(a,1,2,1))]. given #1057 (T,wt=10): 15890 (c2 v x)' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(15665(a,1),4(a,1)),flip(a)]. given #1058 (T,wt=10): 15891 (c2 v (x ^ (c1 v y))) ^ (c2 v y)' = 0. [para(4(a,1),15665(a,1,1,2))]. given #1059 (T,wt=10): 15908 (x v c2)' ^ (c2 v ((x v c1) ^ y)) = 0. [para(15666(a,1),4(a,1)),flip(a)]. given #1060 (A,wt=20): 379 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z. [para(5(a,1),38(b,1))]. given #1061 (T,wt=10): 15909 (c2 v (x ^ (y v c1))) ^ (y v c2)' = 0. [para(4(a,1),15666(a,1,1,2))]. given #1062 (T,wt=10): 15924 (c2 v x)' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(62(a,1),15668(a,1,1,1)),rewrite(2(8),128(8))]. given #1063 (T,wt=10): 16047 (c2 v x)' ^ (c1 v (y ^ (x v c2))) = 0. [para(4(a,1),15718(a,1,2,2))]. given #1064 (T,wt=10): 16050 (c2 v x)' ^ (c2 v ((x v c2) ^ y)) = 0. [para(183(a,1),15718(a,1,2,2)),rewrite(128(10))]. given #1065 (A,wt=12): 380 x v y != 1 | 0 != x | (x v y)' = x. [para(6(a,1),38(b,1)),rewrite(2(2),62(2)),flip(b)]. given #1066 (T,wt=10): 16063 (x v c2)' ^ (c1 v (y ^ (c2 v x))) = 0. [para(4(a,1),15735(a,1,2,2))]. given #1067 (T,wt=10): 16097 (x v c2)' ^ (c2 v (y ^ (c2 v x))) = 0. [para(2(a,1),15847(a,1,1,1))]. given #1068 (T,wt=10): 16098 (c2 v x)' ^ (c2 v (y ^ (x v c2))) = 0. [para(2(a,1),15847(a,1,2,2,2))]. given #1069 (T,wt=10): 16117 (x v c2)' ^ (c2 v (y ^ (x v c1))) = 0. [para(2(a,1),15848(a,1,1,1))]. given #1070 (A,wt=20): 381 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z. [para(17(a,1),38(a,1))]. given #1071 (T,wt=10): 16118 (c2 v x)' ^ (c2 v (y ^ (c1 v x))) = 0. [para(2(a,1),15848(a,1,2,2,2))]. given #1072 (T,wt=10): 16179 (x v c2)' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(15889(a,1),4(a,1)),flip(a)]. given #1073 (T,wt=10): 16180 (c2 v (x ^ (c1 v y))) ^ (y v c2)' = 0. [para(4(a,1),15889(a,1,1,2))]. given #1074 (T,wt=10): 16313 (x v c2)' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(2(a,1),15924(a,1,1,1))]. given #1075 (A,wt=20): 382 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z. [para(19(a,1),38(b,1))]. given #1076 (T,wt=10): 16350 (c2 v (x ^ (c2 v y))) ^ (y v c2)' = 0. [para(16097(a,1),4(a,1)),flip(a)]. given #1077 (T,wt=10): 16362 (c2 v (x ^ (y v c2))) ^ (c2 v y)' = 0. [para(16098(a,1),4(a,1)),flip(a)]. given #1078 (T,wt=10): 16371 (x v c2)' ^ (c2 v (y ^ (c1 v x))) = 0. [para(2(a,1),16117(a,1,2,2,2))]. given #1079 (T,wt=11): 685 c2 v x != 1 | c2 ^ (c1 v x) != 0 | c2' = c1 v x. [para(128(a,1),53(a,1))]. given #1080 (A,wt=24): 383 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),123(4))]. given #1081 (T,wt=11): 757 c2 v x != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(450(a,1),10(a,1))]. given #1082 (T,wt=11): 759 c2 v x != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(450(a,1),36(a,1)),rewrite(4(8))]. given #1083 (T,wt=11): 770 (x ^ (y v z)) v (x ^ y)' = 1. [para(65(a,1),188(a,1,2,1))]. given #1084 (T,wt=10): 16601 (c2 ^ ((x ^ c1) v y)) v (x ^ c1)' = 1. [para(47(a,1),770(a,1,2,1))]. given #1085 (A,wt=20): 384 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 #1086 (T,wt=10): 16640 (x ^ c1)' v (c2 ^ ((x ^ c1) v y)) = 1. [para(16601(a,1),2(a,1)),flip(a)]. given #1087 (T,wt=10): 16641 (c2 ^ (x v (y ^ c1))) v (y ^ c1)' = 1. [para(2(a,1),16601(a,1,1,2))]. given #1088 (T,wt=10): 16643 (c2 ^ ((c1 ^ x) v y)) v (x ^ c1)' = 1. [para(4(a,1),16601(a,1,1,2,1))]. given #1089 (T,wt=10): 16644 (c2 ^ ((x ^ c1) v y)) v (c1 ^ x)' = 1. [para(4(a,1),16601(a,1,2,1))]. given #1090 (A,wt=24): 385 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))]. Low Water (keep, True_semantics): wt=21 given #1091 (T,wt=9): 16737 c2 ^ c1' != 0 | (c1 v (c2 ^ c1'))' = c1'. [para(295(a,1),385(a,1)),rewrite(4(7),4(14),2(16),795(17)),xx(a)]. given #1092 (T,wt=10): 16689 (x ^ c1)' v (c2 ^ (y v (x ^ c1))) = 1. [para(2(a,1),16640(a,1,2,2))]. given #1093 (T,wt=10): 16690 (c1 ^ x)' v (c2 ^ ((x ^ c1) v y)) = 1. [para(4(a,1),16640(a,1,1,1))]. given #1094 (T,wt=10): 16691 (x ^ c1)' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),16640(a,1,2,2,1))]. given #1095 (A,wt=12): 386 x v (x v y)' != 1 | x v y = x. [para(106(a,1),38(b,1)),rewrite(2(3),304(11)),xx(b)]. given #1096 (F,wt=7): 16845 c1' v (c1' v c2')' != 1. [ur(386,b,15,a)]. given #1097 (F,wt=8): 16849 (c1' v (c1' v c2')')' != 0. [ur(3097,b,16845,a),rewrite(2(9))]. given #1098 (T,wt=10): 16700 (c2 ^ (x v (c1 ^ y))) v (y ^ c1)' = 1. [para(4(a,1),16641(a,1,1,2,2))]. given #1099 (T,wt=10): 16701 (c2 ^ (x v (y ^ c1))) v (c1 ^ y)' = 1. [para(4(a,1),16641(a,1,2,1))]. given #1100 (T,wt=10): 16714 (c2 ^ ((c1 ^ x) v y)) v (c1 ^ x)' = 1. [para(4(a,1),16643(a,1,2,1))]. given #1101 (T,wt=10): 16828 (c1 ^ x)' v (c2 ^ (y v (x ^ c1))) = 1. [para(4(a,1),16689(a,1,1,1))]. given #1102 (A,wt=12): 388 x v (y v x)' != 1 | y v x = x. [para(148(a,1),38(b,1)),rewrite(2(3),304(11)),xx(b)]. given #1103 (T,wt=10): 16829 (x ^ c1)' v (c2 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),16689(a,1,2,2,2))]. given #1104 (T,wt=10): 16835 (c1 ^ x)' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),16690(a,1,2,2,1))]. given #1105 (T,wt=10): 16854 (c2 ^ (x v (c1 ^ y))) v (c1 ^ y)' = 1. [para(4(a,1),16700(a,1,2,1))]. given #1106 (T,wt=10): 16888 (c1 ^ x)' v (c2 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),16828(a,1,2,2,2))]. given #1107 (A,wt=24): 391 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [para(27(a,1),38(a,1)),rewrite(4(7),19(7),19(6),5(5),212(7))]. given #1108 (T,wt=11): 771 (x ^ y) v (y ^ x) = x ^ y. [para(65(a,1),27(a,1,2))]. given #1109 (T,wt=11): 844 (x v c1) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(612(a,1),21(a,1,2,2))]. given #1110 (T,wt=11): 902 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),848(a,1,2))]. given #1111 (T,wt=11): 906 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),848(a,1,2,2,2))]. given #1112 (A,wt=18): 397 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x. [para(34(a,1),38(b,1)),rewrite(2(4)),xx(b)]. given #1113 (T,wt=10): 17004 c1 ^ (x v (c2 ^ (y v (c2 ^ (c1 v z))))) = c1. [para(612(a,1),906(a,1,2,2,2,2))]. given #1114 (T,wt=10): 17005 c1 ^ (x v (c2 ^ (y v (c2 ^ (z v c1))))) = c1. [para(617(a,1),906(a,1,2,2,2,2))]. given #1115 (T,wt=10): 17017 c1 ^ (x v (c2 ^ (y v (c2 ^ c1')'))) = c1. [para(7719(a,1),906(a,1,2,2,2,2))]. given #1116 (T,wt=10): 17043 c1 ^ (x v (c2 ^ ((c2 ^ (c1 v y)) v z))) = c1. [para(2(a,1),17004(a,1,2,2,2))]. given #1117 (A,wt=14): 398 c2 ^ (c1' ^ (c1 v x)) != 0 | (c2 ^ (c1 v x))' = c1'. [para(261(a,1),38(a,1)),rewrite(19(10)),xx(a)]. given #1118 (T,wt=10): 17044 c1 ^ ((c2 ^ (x v (c2 ^ (c1 v y)))) v z) = c1. [para(2(a,1),17004(a,1,2))]. given #1119 (T,wt=10): 17084 c1 ^ (x v (c2 ^ ((c2 ^ (y v c1)) v z))) = c1. [para(2(a,1),17005(a,1,2,2,2))]. given #1120 (T,wt=10): 17085 c1 ^ ((c2 ^ (x v (c2 ^ (y v c1)))) v z) = c1. [para(2(a,1),17005(a,1,2))]. given #1121 (T,wt=10): 17125 c1 ^ (x v (c2 ^ ((c2 ^ c1')' v y))) = c1. [para(2(a,1),17017(a,1,2,2,2))]. given #1122 (A,wt=14): 399 c2 ^ (c1' ^ (x v c1)) != 0 | (c2 ^ (x v c1))' = c1'. [para(267(a,1),38(a,1)),rewrite(19(10)),xx(a)]. given #1123 (T,wt=10): 17126 c1 ^ ((c2 ^ (x v (c2 ^ c1')')) v y) = c1. [para(2(a,1),17017(a,1,2))]. given #1124 (T,wt=10): 17158 c1 ^ ((c2 ^ ((c2 ^ (c1 v x)) v y)) v z) = c1. [para(2(a,1),17043(a,1,2))]. given #1125 (T,wt=10): 17239 c1 ^ ((c2 ^ ((c2 ^ (x v c1)) v y)) v z) = c1. [para(2(a,1),17084(a,1,2))]. Low Water (keep, True_semantics): wt=20 given #1126 (T,wt=10): 17317 c1 ^ ((c2 ^ ((c2 ^ c1')' v x)) v y) = c1. [para(2(a,1),17125(a,1,2))]. given #1127 (A,wt=12): 400 c2 ^ ((c1 v x) ^ c1') != 0 | c2 ^ (c1 v x) = c1. [para(290(a,1),38(a,1)),rewrite(5(10),304(15)),flip(c),xx(a)]. given #1128 (T,wt=11): 915 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(3(a,1),900(a,1,2,2,2))]. given #1129 (T,wt=11): 916 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(3(a,1),900(a,1,2))]. given #1130 (T,wt=11): 939 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(17(a,1),901(a,1,2,1,2))]. given #1131 (T,wt=11): 940 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(17(a,1),901(a,1,2))]. given #1132 (A,wt=12): 401 c2 ^ ((x v c1) ^ c1') != 0 | c2 ^ (x v c1) = c1. [para(295(a,1),38(a,1)),rewrite(5(10),304(15)),flip(c),xx(a)]. given #1133 (T,wt=11): 947 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(3(a,1),914(a,1,2,1,2))]. given #1134 (T,wt=11): 950 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(17(a,1),914(a,1,2))]. given #1135 (T,wt=11): 964 (x v c1) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(617(a,1),21(a,1,2,2))]. given #1136 (T,wt=11): 1007 ((x v y) ^ z) v (y ^ z)' = 1. [para(77(a,1),188(a,1,2,1))]. given #1137 (A,wt=16): 402 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(5(a,1),47(a,1,2)),rewrite(4(8))]. given #1138 (T,wt=11): 1067 (x ^ c2) v (x ^ (c1 v (c2 ^ y))) = x ^ c2. [para(795(a,1),27(a,1,2,2))]. given #1139 (T,wt=11): 1094 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(5(a,1),1072(a,1,2))]. given #1140 (T,wt=11): 1096 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(19(a,1),1072(a,1,2,2,2))]. given #1141 (T,wt=10): 17849 c2 v (x ^ (c1 v (y ^ (c1 v (c2 ^ z))))) = c2. [para(795(a,1),1096(a,1,2,2,2,2))]. given #1142 (A,wt=12): 404 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(47(a,1),27(a,1,2,2))]. given #1143 (T,wt=10): 17850 c2 v (x ^ (c1 v (y ^ (c1 v (z ^ c2))))) = c2. [para(801(a,1),1096(a,1,2,2,2,2))]. given #1144 (T,wt=10): 17871 c2 v (x ^ (c1 v ((c1 v (c2 ^ y)) ^ z))) = c2. [para(4(a,1),17849(a,1,2,2,2))]. given #1145 (T,wt=10): 17872 c2 v ((c1 v (x ^ (c1 v (c2 ^ y)))) ^ z) = c2. [para(4(a,1),17849(a,1,2))]. given #1146 (T,wt=10): 17909 c2 v (x ^ (c1 v ((c1 v (y ^ c2)) ^ z))) = c2. [para(4(a,1),17850(a,1,2,2,2))]. given #1147 (A,wt=16): 412 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(5(a,1),69(a,1,2)),rewrite(4(8))]. given #1148 (T,wt=10): 17910 c2 v ((c1 v (x ^ (c1 v (y ^ c2)))) ^ z) = c2. [para(4(a,1),17850(a,1,2))]. given #1149 (T,wt=10): 17940 c2 v ((c1 v ((c1 v (c2 ^ x)) ^ y)) ^ z) = c2. [para(4(a,1),17871(a,1,2))]. given #1150 (T,wt=10): 17997 c2 v ((c1 v ((c1 v (x ^ c2)) ^ y)) ^ z) = c2. [para(4(a,1),17909(a,1,2))]. given #1151 (T,wt=11): 1111 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(5(a,1),1092(a,1,2,2,2))]. given #1152 (A,wt=20): 414 c1 ^ ((x ^ c2) v (c1 ^ ((x ^ c1) v (y ^ (c1 v (x ^ c2)))))) = c1 ^ ((x ^ c2) v (c1 ^ y)). [para(69(a,1),12(a,1,2,2,2,1))]. given #1153 (T,wt=11): 1112 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(5(a,1),1092(a,1,2))]. given #1154 (T,wt=11): 1128 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(19(a,1),1093(a,1,2,1,2))]. given #1155 (T,wt=11): 1129 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(19(a,1),1093(a,1,2))]. given #1156 (T,wt=11): 1138 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(5(a,1),1110(a,1,2,1,2))]. given #1157 (A,wt=20): 415 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2 ^ (c1 v x)))))) = c1 ^ (x v (y ^ c1)). [para(69(a,1),12(a,2,2,2)),rewrite(5(9))]. given #1158 (T,wt=11): 1141 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(19(a,1),1110(a,1,2))]. given #1159 (T,wt=11): 1154 (x ^ c2) v (x ^ (c1 v (y ^ c2))) = x ^ c2. [para(801(a,1),27(a,1,2,2))]. given #1160 (T,wt=11): 1203 (x ^ (y v z)) v (x ^ z)' = 1. [para(82(a,1),188(a,1,2,1))]. given #1161 (T,wt=11): 1314 (c1 v x) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(612(a,1),94(a,1,2,2))]. given #1162 (A,wt=20): 419 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x)' = z. [para(4(a,1),39(a,1,1))]. given #1163 (T,wt=11): 1315 (c1 v x) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(617(a,1),94(a,1,2,2))]. given #1164 (T,wt=11): 1332 (x ^ y)' v (z v x) = 1. [para(161(a,1),95(a,1,1)),rewrite(54(6),161(7))]. given #1165 (T,wt=11): 1334 (x ^ y)' v (z v y) = 1. [para(188(a,1),95(a,1,1)),rewrite(54(6),188(7))]. given #1166 (T,wt=11): 1337 c1' v (x v (y v c2)) = 1. [para(204(a,1),95(a,1,1)),rewrite(3(7),54(8),204(11))]. given #1167 (A,wt=20): 420 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y)' = z. [para(4(a,1),39(b,1)),rewrite(5(6))]. given #1168 (T,wt=11): 1339 (c1 ^ x)' v (y v (c2 ^ x)) = 1. [para(233(a,1),95(a,1,1)),rewrite(54(9),233(13))]. given #1169 (T,wt=11): 1342 (c1 ^ x)' v (y v (x ^ c2)) = 1. [para(259(a,1),95(a,1,1)),rewrite(54(9),259(13))]. given #1170 (T,wt=11): 1343 (x ^ c1)' v (y v (c2 ^ x)) = 1. [para(260(a,1),95(a,1,1)),rewrite(54(9),260(13))]. given #1171 (T,wt=11): 1344 (x ^ c1)' v (y v (x ^ c2)) = 1. [para(362(a,1),95(a,1,1)),rewrite(54(9),362(13))]. given #1172 (A,wt=16): 421 x v y != 1 | z ^ x != 0 | (z ^ x)' = x v y. [para(6(a,1),39(b,1,2)),rewrite(17(3),115(3))]. given #1173 (T,wt=11): 1362 c1' v (x v (c2 v y)) = 1. [para(1335(a,1),3(a,1,1)),rewrite(61(2),3(6)),flip(a)]. given #1174 (T,wt=11): 1374 (c1 v x) ^ (c2 v (x v y))' = 0. [para(463(a,1),96(a,1,2)),rewrite(4(4),74(4),2(6)),flip(a)]. given #1175 (T,wt=11): 1670 c1 ^ (x ^ (c2 ^ (x v y))') = 0. [para(278(a,1),109(a,1,2)),rewrite(85(2)),flip(a)]. given #1176 (T,wt=11): 1685 x v (c2 v (c1 v (x ^ y))') = 1. [para(573(a,1),24(a,1,2)),rewrite(70(2),2(5)),flip(a)]. given #1177 (A,wt=14): 422 (x ^ y) v y' != 1 | (x ^ y)' = y'. [para(9(a,1),39(b,1,2)),rewrite(85(7)),xx(b)]. given #1178 (T,wt=11): 1702 ((x ^ y) v z) ^ (y v z)' = 0. [para(115(a,1),148(a,1,2,1))]. given #1179 (T,wt=11): 1723 x v (c2 v (c1 v (y ^ x))') = 1. [para(573(a,1),115(a,1,2)),rewrite(70(2),2(5)),flip(a)]. given #1180 (T,wt=11): 1729 x ^ (c1 ^ (c2 ^ (x v y))') = 0. [para(718(a,1),22(a,1,2)),rewrite(85(2)),flip(a)]. given #1181 (T,wt=11): 1738 x ^ (c1 ^ (c2 ^ (y v x))') = 0. [para(718(a,1),77(a,1,2)),rewrite(85(2)),flip(a)]. given #1182 (A,wt=20): 425 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y)' = z. [para(19(a,1),39(b,1))]. given #1183 (T,wt=11): 2033 (x v (y ^ z)) ^ (x v z)' = 0. [para(121(a,1),148(a,1,2,1))]. given #1184 (T,wt=11): 2254 c2 v (x v ((c1 ^ y) v x)') = 1. [para(31(a,1),132(a,1,2)),rewrite(2(3),61(3)),flip(a)]. given #1185 (T,wt=11): 2359 x v (c2 v (x v (c1 ^ y))') = 1. [para(135(a,1),934(a,1,2)),rewrite(2(7),3(7))]. Low Water (keep, True_semantics): wt=19 given #1186 (T,wt=11): 2438 c1 v (x ^ c2) != 1 | c1 ^ x != 0 | c1' = x ^ c2. [para(229(a,1),138(a,1,2,2)),rewrite(86(4),229(17),86(15))]. given #1187 (A,wt=12): 427 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(28(a,1),39(b,1,2)),rewrite(2(2),26(2)),flip(a)]. given #1188 (T,wt=11): 2632 ((c1 ^ x) v (y ^ (c1 v (c2 ^ z)))) ^ c2' = 0. [para(1072(a,1),2252(a,1,2,1))]. given #1189 (T,wt=11): 2633 ((c1 ^ x) v (y ^ (c1 v (z ^ c2)))) ^ c2' = 0. [para(1092(a,1),2252(a,1,2,1))]. given #1190 (T,wt=11): 2634 ((c1 ^ x) v ((c1 v (c2 ^ y)) ^ z)) ^ c2' = 0. [para(1093(a,1),2252(a,1,2,1))]. given #1191 (T,wt=11): 2635 ((c1 ^ x) v ((c1 v (y ^ c2)) ^ z)) ^ c2' = 0. [para(1110(a,1),2252(a,1,2,1))]. given #1192 (A,wt=16): 428 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x ^ y. [para(29(a,1),39(a,1)),rewrite(86(5),86(5))]. given #1193 (T,wt=11): 2793 c1 ^ ((c1 v x) ^ ((c2 ^ (c1 v x)) v y))' = 0. [para(142(a,1),2084(a,1,2,1))]. given #1194 (T,wt=8): 19382 (c2 ^ c1')' ^ (c1 v (x ^ c2)) = c1. [back_rewrite(14716),rewrite(19380(13)),xx(a)]. given #1195 (T,wt=8): 19383 (c2 ^ c1')' ^ (c1 v (c2 ^ x)) = c1. [back_rewrite(14662),rewrite(19380(13)),xx(a)]. given #1196 (T,wt=8): 19384 (c1 v (x ^ c2)) ^ (c2 ^ c1')' = c1. [para(19382(a,1),4(a,1)),flip(a)]. given #1197 (A,wt=20): 429 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y)' = (x ^ y) v z. [para(23(a,1),39(b,1)),rewrite(62(4))]. given #1198 (T,wt=8): 19409 (c1 v (c2 ^ x)) ^ (c2 ^ c1')' = c1. [para(19383(a,1),4(a,1)),flip(a)]. given #1199 (T,wt=9): 19380 c1 ^ ((c2 ^ c1')' ^ (c1 v x))' = 0. [para(7719(a,1),2793(a,1,2,1,1)),rewrite(7719(14),7714(13))]. given #1200 (T,wt=9): 19445 c1 != 0 | (c1 v (c2 ^ c1'))' = (c2 ^ c1')'. [para(19409(a,1),336(a,1))]. given #1201 (T,wt=9): 19449 c1 ^ ((c2 ^ c1')' ^ (x v c1))' = 0. [para(2(a,1),19380(a,1,2,1,2))]. given #1202 (A,wt=18): 430 (x ^ y) v (y v z)' != 1 | (y v z)' = (x ^ y)'. [para(106(a,1),39(b,1,2)),rewrite(85(8)),flip(c),xx(b)]. given #1203 (T,wt=9): 19450 c1 ^ ((c1 v x) ^ (c2 ^ c1')')' = 0. [para(4(a,1),19380(a,1,2,1))]. given #1204 (T,wt=9): 19461 c1 ^ ((x v c1) ^ (c2 ^ c1')')' = 0. [para(4(a,1),19449(a,1,2,1))]. given #1205 (T,wt=11): 2794 c1 ^ ((x v c1) ^ ((c2 ^ (x v c1)) v y))' = 0. [para(142(a,1),2085(a,1,2,1))]. given #1206 (T,wt=11): 2861 c2 v (x v ((y ^ c1) v x)') = 1. [para(31(a,1),143(a,1,2)),rewrite(2(3),61(3)),flip(a)]. given #1207 (A,wt=18): 432 (x ^ y) v (z v y)' != 1 | (z v y)' = (x ^ y)'. [para(148(a,1),39(b,1,2)),rewrite(85(8)),flip(c),xx(b)]. given #1208 (T,wt=11): 2909 c2' ^ (x ^ (c1 ^ y)) = 0. [para(2900(a,1),5(a,1,1)),rewrite(74(2),5(6)),flip(a)]. given #1209 (T,wt=11): 2910 c2' ^ (x ^ (y ^ c1)) = 0. [para(5(a,1),2900(a,1,2))]. given #1210 (T,wt=11): 2987 x v (c2 v (x v (y ^ c1))') = 1. [para(147(a,1),934(a,1,2)),rewrite(2(7),3(7))]. given #1211 (T,wt=11): 3033 (x v c1) ^ (x v (c2 v y))' = 0. [para(128(a,1),149(a,1,2,1,2))]. given #1212 (A,wt=14): 433 (x ^ c1) v (c2' ^ y) != 1 | (x ^ c1)' = c2' ^ y. [para(156(a,1),39(b,1,2)),rewrite(85(10)),xx(b)]. given #1213 (T,wt=11): 3034 (x v c1) ^ (x v (y v c2))' = 0. [para(130(a,1),149(a,1,2,1,2))]. given #1214 (T,wt=11): 3035 (x v (c1 ^ y)) ^ (x v (c2 ^ y))' = 0. [para(229(a,1),149(a,1,2,1,2))]. given #1215 (T,wt=10): 19571 ((x ^ c1)' v (c2 ^ (y v x)))' = 0. [hyper(346,a,15043,a,b,3035,a),rewrite(15043(7),60(2),15043(8),54(11)),flip(a)]. given #1216 (T,wt=9): 19661 (c2 ^ (x v y)) v (y ^ c1)' = 1. [hyper(3097,a,19571,a)]. given #1217 (A,wt=14): 434 (x ^ c1) v (y ^ c2') != 1 | (x ^ c1)' = y ^ c2'. [para(158(a,1),39(b,1,2)),rewrite(85(10)),xx(b)]. given #1