============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4147 was started by mccune on cleo.thornwood, Wed Nov 22 11:32:42 2006 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_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 (F,wt=4): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #14 (T,wt=4): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #15 (T,wt=4): 50 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #16 (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 #17 (F,wt=2): 56 1' = 0. [hyper(10,a,35,a,b,50,a)]. given #18 (F,wt=3): 57 1 v x = 1. [para(50(a,1),6(a,1))]. given #19 (T,wt=3): 65 x v 1 = 1. [para(57(a,1),2(a,1)),flip(a)]. given #20 (T,wt=2): 68 0' = 1. [hyper(10,a,65,a,b,32,a)]. given #21 (A,wt=15): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #22 (F,wt=4): 53 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #23 (F,wt=3): 74 0 ^ x = 0. [para(53(a,1),6(a,1,2))]. given #24 (T,wt=3): 76 x ^ 0 = 0. [para(74(a,1),4(a,1)),flip(a)]. given #25 (T,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #26 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #27 (F,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #28 (F,wt=5): 48 c1 v c2 != 1 | c1 != 0 | c1' = c2. [para(13(a,1),10(b,1))]. given #29 (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 #30 (T,wt=5): 67 0 != x | x' = 1. [back_rewrite(51),rewrite(65(2)),xx(a)]. given #31 (A,wt=15): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #32 (F,wt=5): 80 1 != x | x' = 0. [back_rewrite(54),rewrite(76(4)),xx(b)]. given #33 (F,wt=5): 96 c1 ^ (c2 v (x ^ c1)) = c1. [para(4(a,1),49(a,1,2,2))]. given #34 (T,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #35 (T,wt=2): 117 c1 v c2 = c2. [para(13(a,1),26(a,1,2)),rewrite(2(3))]. given #36 (A,wt=13): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #37 (F,wt=4): 120 c2 v (c1 ^ x) = c2. [para(49(a,1),26(a,1,2)),rewrite(2(6),62(6),2(3),117(3)),flip(a)]. given #38 (F,wt=4): 122 c2 v (x ^ c1) = c2. [para(96(a,1),26(a,1,2)),rewrite(2(6),118(6),2(3),117(3)),flip(a)]. given #39 (T,wt=4): 123 c2 != 1 | c1 != 0 | c1' = c2. [back_rewrite(98),rewrite(117(3),120(12))]. given #40 (T,wt=7): 129 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite(76(2)),flip(a)]. given #41 (A,wt=15): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #42 (F,wt=3): 151 c1 ^ c2' = 0. [para(117(a,1),129(a,1,2,1))]. given #43 (F,wt=6): 159 c1 v c2' != 1 | c2' = c1'. [para(151(a,1),10(b,1)),flip(c),xx(b)]. given #44 (T,wt=7): 144 x ^ (y v x)' = 0. [para(2(a,1),129(a,1,2,1))]. given #45 (T,wt=7): 158 c1 ^ (c2' ^ x) = 0. [para(151(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #46 (A,wt=13): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #47 (F,wt=7): 160 c1 ^ (x ^ c2') = 0. [para(151(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #48 (F,wt=7): 172 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite(65(2)),flip(a)]. given #49 (T,wt=7): 183 x v (y ^ x)' = 1. [para(4(a,1),172(a,1,2,1))]. given #50 (T,wt=3): 193 c2 v c1' = 1. [para(13(a,1),183(a,1,2,1))]. given #51 (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 #52 (F,wt=6): 200 c2 ^ c1' != 0 | c2' = c1'. [para(193(a,1),10(a,1)),xx(a)]. given #53 (F,wt=7): 199 c2 v (c1' v x) = 1. [para(193(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #54 (T,wt=7): 202 c2 v (x v c1') = 1. [para(193(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #55 (T,wt=8): 46 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #56 (A,wt=15): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #57 (F,wt=4): 217 c1 ^ (c2 v x) = c1. [para(6(a,1),46(a,1,2)),rewrite(13(3)),flip(a)]. given #58 (F,wt=4): 223 c1 ^ (x v c2) = c1. [para(20(a,1),46(a,1,2)),rewrite(13(3)),flip(a)]. given #59 (T,wt=5): 226 c1 ^ (c2 v x)' = 0. [para(129(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #60 (T,wt=5): 228 c1 ^ (x v c2)' = 0. [para(144(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #61 (A,wt=11): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #62 (F,wt=7): 229 (c2 ^ x) v (c1 ^ x)' = 1. [para(46(a,1),183(a,1,2,1))]. given #63 (F,wt=5): 272 c2 v (c1 ^ x)' = 1. [para(229(a,1),24(a,1,2)),rewrite(2(3),57(3)),flip(a)]. given #64 (T,wt=5): 274 c2 v (x ^ c1)' = 1. [para(4(a,1),272(a,1,2,1))]. given #65 (T,wt=6): 263 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),229(a,1,2,1))]. given #66 (A,wt=11): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #67 (F,wt=6): 269 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),229(a,1,2,1))]. given #68 (F,wt=6): 284 c1' v (c2 ^ (c1 v x)) = 1. [para(263(a,1),2(a,1)),flip(a)]. given #69 (T,wt=6): 297 c1' v (c2 ^ (x v c1)) = 1. [para(269(a,1),2(a,1)),flip(a)]. given #70 (T,wt=7): 261 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),229(a,1,1))]. given #71 (A,wt=12): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #72 (F,wt=4): 324 c2 != 1 | c1 != 0 | c2' = c1. [para(117(a,1),36(a,1)),rewrite(4(6),13(6))]. given #73 (F,wt=4): 330 c2 ^ c1' != 0 | c2 = c1. [para(193(a,1),36(a,1)),rewrite(4(7),319(12)),flip(c),xx(a)]. given #74 (T,wt=7): 262 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),229(a,1,2,1))]. given #75 (T,wt=7): 311 (x ^ c2) v (x ^ c1)' = 1. [para(4(a,1),261(a,1,2,1))]. given #76 (A,wt=20): 37 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #77 (F,wt=7): 319 x'' = x. [para(8(a,1),36(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #78 (F,wt=8): 47 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite(4(4))]. given #79 (T,wt=8): 73 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #80 (T,wt=8): 84 1 != x | 0 != x | x' = x. [para(28(a,1),10(b,1)),rewrite(29(1)),flip(a),flip(b)]. given #81 (A,wt=12): 38 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #82 (F,wt=4): 401 c1 v c2' != 1 | c2 = c1. [para(151(a,1),38(b,1)),rewrite(2(4),319(12)),xx(b)]. given #83 (F,wt=8): 124 c1 v (c2 v x) = c2 v x. [para(117(a,1),3(a,1,1)),flip(a)]. given #84 (T,wt=8): 125 c2 v (x v c1) = x v c2. [para(117(a,1),3(a,2,2)),rewrite(2(4))]. given #85 (T,wt=7): 426 (x v c1) ^ (x v c2)' = 0. [para(125(a,1),144(a,1,2,1))]. given #86 (A,wt=20): 39 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #87 (F,wt=7): 434 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),426(a,1,1))]. given #88 (F,wt=7): 435 (x v c1) ^ (c2 v x)' = 0. [para(2(a,1),426(a,1,2,1))]. given #89 (T,wt=6): 479 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),435(a,1,2,1)),rewrite(2(4))]. given #90 (T,wt=6): 483 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),435(a,1,2,1)),rewrite(2(4))]. given #91 (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 #92 (F,wt=6): 488 c2' ^ (c1 v (c2 ^ x)) = 0. [para(479(a,1),4(a,1)),flip(a)]. given #93 (F,wt=6): 496 c2' ^ (c1 v (x ^ c2)) = 0. [para(483(a,1),4(a,1)),flip(a)]. given #94 (T,wt=7): 469 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),434(a,1,2,1))]. given #95 (T,wt=8): 126 c1 v (x v c2) = x v c2. [para(117(a,1),17(a,1,2)),flip(a)]. given #96 (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 #97 (F,wt=8): 127 (x v c1) ^ (x v c2) = x v c1. [para(117(a,1),21(a,1,2,2))]. given #98 (F,wt=8): 135 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x. [para(120(a,1),10(a,1)),rewrite(19(7),46(7))]. given #99 (T,wt=3): 565 c2 != 1 | c2' = 0. [para(9(a,1),135(b,1)),rewrite(9(12)),xx(b)]. given #100 (T,wt=8): 138 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),120(a,1,2))]. given #101 (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 #102 (F,wt=8): 140 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),122(a,1,2))]. given #103 (F,wt=8): 141 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1. [para(122(a,1),10(a,1)),rewrite(47(7))]. given #104 (T,wt=8): 224 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(46(a,1),26(a,1,2)),rewrite(2(5))]. given #105 (T,wt=8): 236 c2 v x != 1 | c1 != 0 | c1' = c2 v x. [para(217(a,1),10(b,1)),rewrite(124(4))]. given #106 (A,wt=11): 58 x v (x v y) = x v y. [para(50(a,1),12(a,1,2,2,2,1)),rewrite(57(4),32(4),50(4),50(4),50(5),50(5))]. given #107 (F,wt=3): 610 c1 != 0 | c1' = 1. [para(8(a,1),236(a,1)),rewrite(8(12)),xx(a)]. given #108 (F,wt=8): 238 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),217(a,1,2))]. given #109 (T,wt=8): 240 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),223(a,1,2))]. given #110 (T,wt=8): 242 x v c2 != 1 | c1 != 0 | c1' = x v c2. [para(223(a,1),10(b,1)),rewrite(126(4))]. given #111 (A,wt=9): 59 x v (x' v y) = 1. [back_rewrite(30),rewrite(57(5))]. given #112 (F,wt=5): 634 c1 ^ (c1' v c2') != 0. [ur(38,a,59,a,c,15,a(flip)),rewrite(4(7))]. given #113 (F,wt=8): 325 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2. [para(120(a,1),36(a,1)),rewrite(4(7),19(7),46(7))]. given #114 (T,wt=8): 326 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2. [para(122(a,1),36(a,1)),rewrite(4(7),47(7))]. given #115 (T,wt=8): 337 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2. [para(272(a,1),36(a,1)),rewrite(4(8),319(14)),xx(a)]. given #116 (A,wt=12): 60 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(40),rewrite(58(2))]. given #117 (F,wt=3): 648 c2 != 0 | c2' = 1. [para(193(a,1),60(a,1)),rewrite(193(12)),flip(b),xx(a)]. given #118 (F,wt=3): 649 c1' != 0 | c1 = 1. [para(284(a,1),60(a,1)),rewrite(319(10),284(15)),flip(b),xx(a)]. given #119 (T,wt=4): 647 c2 != 1 | c2 != 0 | c2' = c2. [para(120(a,1),60(a,1)),rewrite(120(12)),flip(b)]. given #120 (T,wt=8): 338 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2. [para(274(a,1),36(a,1)),rewrite(4(8),319(14)),xx(a)]. given #121 (A,wt=11): 61 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #122 (F,wt=8): 386 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(47(a,1),27(a,1,2))]. given #123 (F,wt=8): 391 (x ^ c1) v (x ^ c2) = x ^ c2. [para(73(a,1),26(a,1,2)),rewrite(2(5))]. given #124 (T,wt=8): 392 (c1 ^ x) v (x ^ c1) = c1 ^ x. [para(73(a,1),27(a,1,2))]. given #125 (T,wt=8): 407 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1. [para(217(a,1),38(b,1)),rewrite(2(4),124(4))]. given #126 (A,wt=13): 62 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #127 (F,wt=8): 408 x v c2 != 1 | c1 != 0 | (x v c2)' = c1. [para(223(a,1),38(b,1)),rewrite(2(4),126(4))]. given #128 (F,wt=8): 409 c1 v (c2 v x)' != 1 | c2 v x = c1. [para(226(a,1),38(b,1)),rewrite(2(5),319(14)),xx(b)]. given #129 (T,wt=8): 410 c1 v (x v c2)' != 1 | x v c2 = c1. [para(228(a,1),38(b,1)),rewrite(2(5),319(14)),xx(b)]. given #130 (T,wt=8): 421 c2 v (x v c1) = c2 v x. [para(125(a,2),2(a,1))]. given #131 (A,wt=20): 64 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #132 (F,wt=8): 431 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1. [para(125(a,1),37(a,1)),rewrite(4(8),217(8))]. given #133 (F,wt=8): 467 c2 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c2. [para(73(a,1),39(b,1)),rewrite(2(4),120(4))]. given #134 (T,wt=8): 534 (c1 v x) ^ (x v c2) = c1 v x. [para(126(a,1),21(a,1,2))]. given #135 (T,wt=8): 551 (x v c1) ^ (c2 v x) = x v c1. [para(2(a,1),127(a,1,2))]. given #136 (A,wt=9): 66 x v (y v x') = 1. [back_rewrite(63),rewrite(65(5))]. given #137 (F,wt=8): 564 c2 != 1 | x ^ c1 != 0 | c2' = c1 ^ x. [para(4(a,1),135(b,1))]. given #138 (F,wt=8): 591 c2 != 1 | c1 ^ x != 0 | c2' = x ^ c1. [para(4(a,1),141(b,1))]. given #139 (T,wt=8): 595 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),224(a,1,1))]. given #140 (T,wt=8): 596 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),224(a,1,2))]. given #141 (A,wt=13): 69 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #142 (F,wt=8): 597 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),224(a,1,1))]. given #143 (F,wt=6): 836 c1 ^ (c2 ^ (c1 v x))' = 0. [para(597(a,1),129(a,1,2,1))]. given #144 (T,wt=6): 841 c1 ^ (c2 ^ (x v c1))' = 0. [para(2(a,1),836(a,1,2,1,2))]. given #145 (T,wt=7): 839 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [para(597(a,1),61(a,1,2,2))]. given #146 (A,wt=11): 70 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #147 (F,wt=7): 854 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),839(a,1,2,2,2))]. given #148 (F,wt=7): 855 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(2(a,1),839(a,1,2))]. given #149 (T,wt=7): 877 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),854(a,1,2))]. given #150 (T,wt=8): 602 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(20(a,1),224(a,1,1))]. given #151 (A,wt=20): 72 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(19(a,1),10(b,1))]. given #152 (F,wt=8): 609 x v c2 != 1 | c1 != 0 | c1' = c2 v x. [para(2(a,1),236(a,1))]. given #153 (F,wt=8): 632 c2 v x != 1 | c1 != 0 | c1' = x v c2. [para(2(a,1),242(a,1))]. given #154 (T,wt=8): 641 c2 != 1 | c1 ^ x != 0 | (x ^ c1)' = c2. [para(4(a,1),326(b,1))]. given #155 (T,wt=8): 643 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),337(a,1,2,1))]. given #156 (A,wt=9): 75 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite(74(5))]. given #157 (F,wt=8): 650 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),338(a,1,2,1))]. given #158 (F,wt=8): 707 c2 v x != 1 | c1 != 0 | (x v c2)' = c1. [para(2(a,1),408(a,1))]. given #159 (T,wt=8): 709 c1 v (x v c2)' != 1 | c2 v x = c1. [para(2(a,1),409(a,1,2,1))]. given #160 (T,wt=8): 711 c1 v (c2 v x)' != 1 | x v c2 = c1. [para(2(a,1),410(a,1,2,1))]. given #161 (A,wt=9): 78 x ^ (y ^ x') = 0. [back_rewrite(71),rewrite(76(5))]. given #162 (F,wt=8): 720 c2 v x != 1 | c2 != 0 | c2' = c2 v x. [para(421(a,1),60(a,1)),rewrite(421(13)),flip(b)]. given #163 (F,wt=8): 732 c1' ^ (c2 v x) != 0 | c2 v x = c1. [para(199(a,1),64(a,1)),rewrite(319(13)),flip(c),xx(a)]. given #164 (T,wt=8): 757 (c1 v x) ^ (c2 v x) = c1 v x. [para(2(a,1),534(a,1,2))]. given #165 (T,wt=8): 758 (x v c2) ^ (c1 v x) = c1 v x. [para(534(a,1),4(a,1)),flip(a)]. given #166 (A,wt=11): 81 x ^ (x ^ y) = x ^ y. [para(28(a,1),5(a,1,1)),flip(a)]. given #167 (F,wt=8): 773 (c2 v x) ^ (x v c1) = x v c1. [para(551(a,1),4(a,1)),flip(a)]. given #168 (F,wt=8): 775 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(7(a,1),551(a,1,2)),rewrite(2(4),4(6),2(10))]. given #169 (T,wt=6): 1025 c2 v (c1 v (c2 ^ x))' = 1. [para(775(a,1),172(a,1,2,1))]. given #170 (T,wt=6): 1034 c2 v (c1 v (x ^ c2))' = 1. [para(4(a,1),1025(a,1,2,1,2))]. given #171 (A,wt=11): 83 x ^ (y ^ x) = y ^ x. [para(28(a,1),5(a,2,2)),rewrite(4(2))]. given #172 (F,wt=7): 1031 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(775(a,1),70(a,1,2,2))]. given #173 (F,wt=7): 1057 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),1031(a,1,2,2,2))]. given #174 (T,wt=7): 1058 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(4(a,1),1031(a,1,2))]. given #175 (T,wt=7): 1069 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(4(a,1),1057(a,1,2))]. given #176 (A,wt=12): 85 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(41),rewrite(81(4))]. given #177 (F,wt=3): 1107 c1 != 1 | c1' = 0. [para(151(a,1),85(b,1)),rewrite(151(12)),flip(a),xx(b)]. given #178 (F,wt=3): 1110 c2' != 1 | c2 = 0. [para(488(a,1),85(b,1)),rewrite(319(10),488(15)),flip(a),xx(b)]. given #179 (T,wt=4): 1105 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),85(b,1)),rewrite(13(11)),flip(a)]. given #180 (T,wt=8): 781 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(26(a,1),551(a,1,2)),rewrite(2(4),4(6),2(10))]. given #181 (A,wt=11): 86 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #182 (F,wt=8): 804 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(596(a,1),2(a,1)),flip(a)]. given #183 (F,wt=8): 928 c2' v (c1 ^ x) != 1 | c1 ^ x = c2. [para(158(a,1),72(b,1)),rewrite(319(13)),flip(c),xx(b)]. given #184 (T,wt=8): 980 x v c2 != 1 | c2 != 0 | c2' = c2 v x. [para(2(a,1),720(a,1))]. given #185 (T,wt=8): 982 x v c2 != 1 | c2 != 0 | c2' = x v c2. [para(62(a,1),720(a,1)),rewrite(62(14))]. given #186 (A,wt=13): 87 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #187 (F,wt=8): 983 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),732(a,1,2))]. given #188 (F,wt=8): 984 (c2 v x) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),732(a,1))]. given #189 (T,wt=8): 987 c1' ^ (x v c2) != 0 | x v c2 = c1. [para(62(a,1),732(a,1,2)),rewrite(62(12))]. given #190 (T,wt=8): 1108 c1 != 1 | c1 ^ x != 0 | c1' = c1 ^ x. [para(46(a,1),85(b,1)),rewrite(46(13)),flip(a)]. given #191 (A,wt=15): 88 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #192 (F,wt=8): 1109 c1 != 1 | x ^ c1 != 0 | c1' = x ^ c1. [para(73(a,1),85(b,1)),rewrite(73(13)),flip(a)]. given #193 (F,wt=8): 1151 (c1 ^ x) v c2' != 1 | c1 ^ x = c2. [para(2(a,1),928(a,1))]. given #194 (T,wt=8): 1152 c2' v (x ^ c1) != 1 | c1 ^ x = c2. [para(4(a,1),928(a,1,2))]. given #195 (T,wt=8): 1154 c2' v (x ^ c1) != 1 | x ^ c1 = c2. [para(73(a,1),928(a,1,2)),rewrite(73(11))]. given #196 (A,wt=15): 90 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #197 (F,wt=8): 1156 c2 v x != 1 | c2 != 0 | c2' = x v c2. [para(2(a,1),982(a,1))]. given #198 (F,wt=8): 1177 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),983(a,1))]. given #199 (T,wt=8): 1179 (x v c2) ^ c1' != 0 | x v c2 = c1. [para(62(a,1),984(a,1,1)),rewrite(62(12))]. given #200 (T,wt=8): 1180 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),987(a,1,2))]. given #201 (A,wt=13): 91 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #202 (F,wt=8): 1181 c1 != 1 | x ^ c1 != 0 | c1' = c1 ^ x. [para(4(a,1),1108(b,1))]. given #203 (F,wt=8): 1196 x ^ (c1 v (x ^ c2)) = x ^ c2. [para(781(a,1),88(a,1,2))]. given #204 (T,wt=8): 1200 c1 != 1 | c1 ^ x != 0 | c1' = x ^ c1. [para(4(a,1),1109(b,1))]. given #205 (T,wt=8): 1202 (x ^ c1) v c2' != 1 | c1 ^ x = c2. [para(4(a,1),1151(a,1,1))]. given #206 (A,wt=11): 93 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite(2(2))]. given #207 (F,wt=8): 1204 (x ^ c1) v c2' != 1 | x ^ c1 = c2. [para(73(a,1),1151(a,1,1)),rewrite(73(11))]. given #208 (F,wt=8): 1206 c2' v (c1 ^ x) != 1 | x ^ c1 = c2. [para(4(a,1),1154(a,1,2))]. given #209 (T,wt=8): 1227 (c2 v x) ^ c1' != 0 | x v c2 = c1. [para(2(a,1),1179(a,1,1))]. given #210 (T,wt=8): 1240 x ^ (c1 v (c2 ^ x)) = x ^ c2. [para(4(a,1),1196(a,1,2,2))]. given #211 (A,wt=12): 95 x v y != 1 | 0 != y | y' = x v y. [back_rewrite(89),rewrite(93(2))]. given #212 (F,wt=5): 1268 x' != 0 | 1 = x. [para(8(a,1),95(a,1)),rewrite(319(8),8(8)),flip(b),flip(c),xx(a)]. given #213 (F,wt=8): 1254 (c1 ^ x) v c2' != 1 | x ^ c1 = c2. [para(4(a,1),1204(a,1,1))]. given #214 (T,wt=9): 245 c1 ^ ((c2 v x)' ^ y) = 0. [para(226(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #215 (T,wt=9): 247 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),226(a,1,2,1))]. given #216 (A,wt=15): 102 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #217 (F,wt=9): 248 c1 ^ (x ^ (c2 v y)') = 0. [para(226(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #218 (F,wt=9): 249 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),228(a,1,2,1))]. given #219 (T,wt=9): 250 c1 ^ ((x v c2)' ^ y) = 0. [para(228(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #220 (T,wt=9): 252 c1 ^ (x ^ (y v c2)') = 0. [para(228(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #221 (A,wt=15): 103 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite(3(3))]. given #222 (F,wt=7): 1356 c1' v (x v c2) = 1. [para(193(a,1),103(a,1,1)),rewrite(50(7),193(9))]. given #223 (F,wt=9): 273 c2 v ((c1 ^ x)' v y) = 1. [para(272(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #224 (T,wt=9): 277 c2 v (x v (c1 ^ y)') = 1. [para(272(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #225 (T,wt=9): 278 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),272(a,1,2,1))]. given #226 (A,wt=21): 104 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #227 (F,wt=9): 279 c2 v ((x ^ c1)' v y) = 1. [para(274(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #228 (F,wt=9): 280 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),274(a,1,2,1))]. given #229 (T,wt=9): 283 c2 v (x v (y ^ c1)') = 1. [para(274(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #230 (T,wt=9): 296 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #231 (A,wt=19): 105 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #232 (F,wt=9): 356 x v y != 0 | (x v y)' = 1. [para(32(a,1),37(b,1)),rewrite(65(2),65(2)),xx(a)]. given #233 (F,wt=9): 357 x v y != 1 | (x v y)' = 0. [para(35(a,1),37(a,1,2)),rewrite(4(6),74(6)),xx(b)]. given #234 (T,wt=9): 446 x ^ y != 0 | (x ^ y)' = 1. [para(32(a,1),39(b,1,2)),rewrite(2(3),57(3)),xx(a)]. given #235 (T,wt=9): 447 x ^ y != 1 | (x ^ y)' = 0. [para(35(a,1),39(a,1)),rewrite(76(5),76(5)),xx(b)]. given #236 (A,wt=21): 106 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #237 (F,wt=9): 559 x v (c2 v (x v c1)') = 1. [para(127(a,1),183(a,1,2,1)),rewrite(3(6))]. given #238 (F,wt=9): 668 x ^ (c1 ^ (c2 ^ x)') = 0. [para(386(a,1),144(a,1,2,1)),rewrite(5(6))]. given #239 (T,wt=9): 681 x ^ (c1 ^ (x ^ c2)') = 0. [para(391(a,1),129(a,1,2,1)),rewrite(5(6))]. given #240 (T,wt=9): 765 x v (c2 v (c1 v x)') = 1. [para(534(a,1),183(a,1,2,1)),rewrite(3(6))]. given #241 (A,wt=13): 112 x v ((y ^ x) v z) = x v z. [para(26(a,1),3(a,1,1)),flip(a)]. given #242 (F,wt=9): 767 c2 v (x v (c1 v x)') = 1. [para(31(a,1),534(a,1,1)),rewrite(2(7),50(8),31(12))]. given #243 (F,wt=9): 783 c2 v (x v (x v c1)') = 1. [para(551(a,1),183(a,1,2,1)),rewrite(3(6))]. given #244 (T,wt=9): 794 x' v (y v x) = 1. [para(319(a,1),66(a,1,2,2))]. given #245 (T,wt=7): 1643 (c2 ^ x) v (x ^ c2)' = 1. [para(596(a,1),794(a,1,2)),rewrite(2(6))]. given #246 (A,wt=15): 113 x v (y v (z ^ (x v y))) = x v y. [para(26(a,1),3(a,1)),flip(a)]. given #247 (F,wt=8): 1644 c2 v (x ^ (c1 v (c2 ^ y)))' = 1. [para(1031(a,1),794(a,1,2)),rewrite(2(8))]. given #248 (F,wt=8): 1645 c2 v (x ^ (c1 v (y ^ c2)))' = 1. [para(1057(a,1),794(a,1,2)),rewrite(2(8))]. given #249 (T,wt=8): 1646 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1. [para(1058(a,1),794(a,1,2)),rewrite(2(8))]. given #250 (T,wt=8): 1647 c2 v ((c1 v (x ^ c2)) ^ y)' = 1. [para(1069(a,1),794(a,1,2)),rewrite(2(8))]. given #251 (A,wt=11): 114 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #252 (F,wt=8): 1670 x v (c2 ^ (x v c1)) = x v c1. [para(602(a,1),113(a,1,2))]. given #253 (F,wt=8): 1746 x v (c2 ^ (c1 v x)) = x v c1. [para(2(a,1),1670(a,1,2,2))]. given #254 (T,wt=9): 862 (c2 ^ (x v (c2 ^ (c1 v y)))) v c1' = 1. [para(839(a,1),229(a,1,2,1))]. given #255 (T,wt=9): 886 (c2 ^ (x v (c2 ^ (y v c1)))) v c1' = 1. [para(854(a,1),229(a,1,2,1))]. given #256 (A,wt=12): 115 1 != x | y ^ x != 0 | x' = y ^ x. [para(26(a,1),10(a,1)),rewrite(83(4)),flip(a)]. given #257 (F,wt=5): 1810 x' != 1 | 0 = x. [para(9(a,1),115(b,1)),rewrite(319(8),9(8)),flip(a),flip(c),xx(b)]. given #258 (F,wt=6): 1824 (c1 ^ (c1' v c2'))' != 1. [ur(1810,b,634,a(flip))]. given #259 (T,wt=9): 897 (c2 ^ ((c2 ^ (c1 v x)) v y)) v c1' = 1. [para(855(a,1),229(a,1,2,1))]. given #260 (T,wt=9): 907 (c2 ^ ((c2 ^ (x v c1)) v y)) v c1' = 1. [para(877(a,1),229(a,1,2,1))]. given #261 (A,wt=13): 118 x v (y v (z ^ x)) = y v x. [para(26(a,1),17(a,1,2)),flip(a)]. given #262 (F,wt=9): 973 x' ^ (y ^ x) = 0. [para(319(a,1),78(a,1,2,2))]. given #263 (F,wt=8): 1885 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(839(a,1),973(a,1,2)),rewrite(4(8))]. given #264 (T,wt=8): 1886 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(854(a,1),973(a,1,2)),rewrite(4(8))]. given #265 (T,wt=8): 1887 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(855(a,1),973(a,1,2)),rewrite(4(8))]. given #266 (A,wt=15): 119 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(19(a,1),26(a,1,2))]. given #267 (F,wt=8): 1888 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(877(a,1),973(a,1,2)),rewrite(4(8))]. given #268 (F,wt=9): 1064 (c1 v (x ^ (c1 v (c2 ^ y)))) ^ c2' = 0. [para(1031(a,1),435(a,1,2,1)),rewrite(2(7))]. given #269 (T,wt=9): 1078 (c1 v (x ^ (c1 v (y ^ c2)))) ^ c2' = 0. [para(1057(a,1),435(a,1,2,1)),rewrite(2(7))]. given #270 (T,wt=9): 1089 (c1 v ((c1 v (c2 ^ x)) ^ y)) ^ c2' = 0. [para(1058(a,1),435(a,1,2,1)),rewrite(2(7))]. given #271 (A,wt=23): 128 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(22(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #272 (F,wt=9): 1101 (c1 v ((c1 v (x ^ c2)) ^ y)) ^ c2' = 0. [para(1069(a,1),435(a,1,2,1)),rewrite(2(7))]. given #273 (F,wt=9): 1271 (x ^ y)' != 0 | x ^ y = 1. [para(172(a,1),95(a,1)),rewrite(319(10),172(11)),flip(b),xx(a)]. given #274 (T,wt=9): 1361 (c1 ^ x)' v (y v c2) = 1. [para(272(a,1),103(a,1,1)),rewrite(50(8),272(11))]. given #275 (T,wt=9): 1362 (x ^ c1)' v (y v c2) = 1. [para(274(a,1),103(a,1,1)),rewrite(50(8),274(11))]. given #276 (A,wt=20): 130 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(22(a,1),10(b,1))]. given #277 (F,wt=8): 2041 c2 != 1 | c2 ^ x != 0 | c2' = c2 ^ x. [para(120(a,1),130(a,1,2,1)),rewrite(7(4),120(13))]. given #278 (F,wt=8): 2052 c1 v x != 1 | c1 != 0 | c1' = c1 v x. [para(534(a,1),130(a,1,2)),rewrite(58(4),223(8),534(14))]. given #279 (T,wt=8): 2066 c2 != 1 | x ^ c2 != 0 | c2' = c2 ^ x. [para(4(a,1),2041(b,1))]. given #280 (T,wt=8): 2068 c2 != 1 | x ^ c2 != 0 | c2' = x ^ c2. [para(69(a,1),2041(b,1)),rewrite(69(14))]. given #281 (A,wt=17): 131 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(17(a,1),22(a,1,2,1))]. given #282 (F,wt=8): 2069 x v c1 != 1 | c1 != 0 | c1' = c1 v x. [para(2(a,1),2052(a,1))]. given #283 (F,wt=8): 2071 x v c1 != 1 | c1 != 0 | c1' = x v c1. [para(62(a,1),2052(a,1)),rewrite(62(14))]. given #284 (T,wt=8): 2073 c2 != 1 | c2 ^ x != 0 | c2' = x ^ c2. [para(4(a,1),2068(b,1))]. given #285 (T,wt=8): 2097 c1 v x != 1 | c1 != 0 | c1' = x v c1. [para(2(a,1),2071(a,1))]. given #286 (A,wt=21): 132 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(22(a,1),19(a,1,2)),flip(a)]. given #287 (F,wt=9): 1454 c1 ^ (x ^ (x ^ c2)') = 0. [para(4(a,1),296(a,1,2,2,1))]. given #288 (F,wt=9): 1510 x v y != 0 | (y v x)' = 1. [para(2(a,1),356(a,1))]. given #289 (T,wt=9): 1512 x v y != 1 | (y v x)' = 0. [para(2(a,1),357(a,1))]. given #290 (T,wt=9): 1514 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),446(a,1))]. given #291 (A,wt=15): 133 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(22(a,1),26(a,1,2)),rewrite(2(4))]. given #292 (F,wt=8): 2183 c1 ^ ((c2 v x) ^ (c1 v y))' = 0. [para(133(a,1),1887(a,1,2,1))]. given #293 (F,wt=8): 2184 c1 ^ ((c2 v x) ^ (y v c1))' = 0. [para(133(a,1),1888(a,1,2,1))]. given #294 (T,wt=8): 2196 c1 ^ ((x v c2) ^ (c1 v y))' = 0. [para(2(a,1),2183(a,1,2,1,1))]. given #295 (T,wt=8): 2197 c1 ^ ((c1 v x) ^ (c2 v y))' = 0. [para(4(a,1),2183(a,1,2,1))]. given #296 (A,wt=10): 134 c2 v ((c1 ^ x) v y) = c2 v y. [para(120(a,1),3(a,1,1)),flip(a)]. given #297 (F,wt=8): 2204 c1 ^ ((c2 v x) ^ (c2 v y))' = 0. [para(124(a,1),2183(a,1,2,1,2))]. given #298 (F,wt=8): 2206 c1 ^ ((c2 v x) ^ (y v c2))' = 0. [para(126(a,1),2183(a,1,2,1,2))]. given #299 (T,wt=8): 2209 c1 ^ ((x v c2) ^ (y v c1))' = 0. [para(2(a,1),2184(a,1,2,1,1))]. given #300 (T,wt=8): 2211 c1 ^ ((x v c1) ^ (c2 v y))' = 0. [para(4(a,1),2184(a,1,2,1))]. given #301 (A,wt=17): 136 c2 ^ ((c1 ^ x) v (c2 ^ ((c1 ^ x) v (y ^ c2)))) = c2 ^ ((c1 ^ x) v (c2 ^ y)). [para(120(a,1),12(a,1,2,2,2,2,2)),rewrite(19(8),46(8))]. given #302 (F,wt=8): 2221 c1 ^ ((c1 v x) ^ (y v c2))' = 0. [para(4(a,1),2196(a,1,2,1))]. given #303 (F,wt=8): 2227 c1 ^ ((x v c2) ^ (c2 v y))' = 0. [para(124(a,1),2196(a,1,2,1,2))]. given #304 (T,wt=8): 2229 c1 ^ ((x v c2) ^ (y v c2))' = 0. [para(126(a,1),2196(a,1,2,1,2))]. given #305 (T,wt=8): 2279 c1 ^ ((x v c1) ^ (y v c2))' = 0. [para(4(a,1),2209(a,1,2,1))]. given #306 (A,wt=10): 137 c2 v (x v (c1 ^ y)) = x v c2. [para(120(a,1),17(a,1,2)),flip(a)]. given #307 (F,wt=9): 1516 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),447(a,1))]. given #308 (F,wt=9): 1783 c1' v (c2 ^ (x v (c2 ^ (c1 v y)))) = 1. [para(862(a,1),2(a,1)),flip(a)]. given #309 (T,wt=9): 1796 c1' v (c2 ^ (x v (c2 ^ (y v c1)))) = 1. [para(886(a,1),2(a,1)),flip(a)]. given #310 (T,wt=9): 1813 (x v y)' != 1 | x v y = 0. [para(129(a,1),115(b,1)),rewrite(319(10),129(11)),flip(a),xx(b)]. given #311 (A,wt=10): 139 c2 v ((x ^ c1) v y) = c2 v y. [para(122(a,1),3(a,1,1)),flip(a)]. given #312 (F,wt=9): 1825 c1' v (c2 ^ ((c2 ^ (c1 v x)) v y)) = 1. [para(897(a,1),2(a,1)),flip(a)]. given #313 (F,wt=9): 1838 c1' v (c2 ^ ((c2 ^ (x v c1)) v y)) = 1. [para(907(a,1),2(a,1)),flip(a)]. given #314 (T,wt=9): 1953 c2' ^ (c1 v (x ^ (c1 v (c2 ^ y)))) = 0. [para(1064(a,1),4(a,1)),flip(a)]. given #315 (T,wt=9): 1963 c2' ^ (c1 v (x ^ (c1 v (y ^ c2)))) = 0. [para(1078(a,1),4(a,1)),flip(a)]. given #316 (A,wt=17): 142 c2 ^ ((x ^ c1) v (c2 ^ ((x ^ c1) v (y ^ c2)))) = c2 ^ ((x ^ c1) v (c2 ^ y)). [para(122(a,1),12(a,1,2,2,2,2,2)),rewrite(47(8))]. given #317 (F,wt=9): 1973 c2' ^ (c1 v ((c1 v (c2 ^ x)) ^ y)) = 0. [para(1089(a,1),4(a,1)),flip(a)]. given #318 (F,wt=9): 2011 c2' ^ (c1 v ((c1 v (x ^ c2)) ^ y)) = 0. [para(1101(a,1),4(a,1)),flip(a)]. given #319 (T,wt=9): 2021 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),1271(a,1,1))]. given #320 (T,wt=9): 2023 (x v y)' != 0 | x v y = 1. [para(21(a,1),1271(a,1,1)),rewrite(21(8))]. given #321 (A,wt=10): 143 c2 v (x v (y ^ c1)) = x v c2. [para(122(a,1),17(a,1,2)),flip(a)]. given #322 (F,wt=3): 2453 c2' != 0 | c2 = 1. [para(117(a,1),2023(a,1,1)),rewrite(117(7))]. given #323 (F,wt=9): 2244 ((c1 ^ x) v y) ^ (c2 v y)' = 0. [para(134(a,1),144(a,1,2,1))]. given #324 (T,wt=8): 2471 ((c1 ^ x) v (c2 ^ y)) ^ c2' = 0. [para(7(a,1),2244(a,1,2,1))]. given #325 (T,wt=8): 2477 ((c1 ^ x) v (y ^ c2)) ^ c2' = 0. [para(26(a,1),2244(a,1,2,1))]. given #326 (A,wt=13): 145 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),129(a,1,2,1))]. given #327 (F,wt=8): 2478 ((c1 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(120(a,1),2244(a,1,2,1))]. given #328 (F,wt=8): 2479 ((c1 ^ x) v (y ^ c1)) ^ c2' = 0. [para(122(a,1),2244(a,1,2,1))]. given #329 (T,wt=8): 2505 ((c2 ^ x) v (c1 ^ y)) ^ c2' = 0. [para(2(a,1),2471(a,1,1))]. given #330 (T,wt=8): 2506 c2' ^ ((c1 ^ x) v (c2 ^ y)) = 0. [para(2471(a,1),4(a,1)),flip(a)]. given #331 (A,wt=11): 146 x ^ ((x v y)' ^ z) = 0. [para(129(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #332 (F,wt=8): 2507 ((x ^ c1) v (c2 ^ y)) ^ c2' = 0. [para(4(a,1),2471(a,1,1,1))]. given #333 (F,wt=8): 2519 ((x ^ c2) v (c1 ^ y)) ^ c2' = 0. [para(2(a,1),2477(a,1,1))]. given #334 (T,wt=8): 2520 c2' ^ ((c1 ^ x) v (y ^ c2)) = 0. [para(2477(a,1),4(a,1)),flip(a)]. given #335 (T,wt=8): 2521 ((x ^ c1) v (y ^ c2)) ^ c2' = 0. [para(4(a,1),2477(a,1,1,1))]. given #336 (A,wt=13): 147 x ^ (y ^ ((x ^ y) v z)') = 0. [para(129(a,1),5(a,1)),flip(a)]. given #337 (F,wt=8): 2548 c2' ^ ((c1 ^ x) v (c1 ^ y)) = 0. [para(2478(a,1),4(a,1)),flip(a)]. given #338 (F,wt=8): 2549 ((x ^ c1) v (c1 ^ y)) ^ c2' = 0. [para(4(a,1),2478(a,1,1,1))]. given #339 (T,wt=8): 2560 c2' ^ ((c1 ^ x) v (y ^ c1)) = 0. [para(2479(a,1),4(a,1)),flip(a)]. given #340 (T,wt=7): 2682 c2' ^ (x ^ c1) = 0. [para(9(a,1),2560(a,1,2,1)),rewrite(53(6))]. given #341 (A,wt=14): 148 x v (x v y)' != 1 | (x v y)' = x'. [para(129(a,1),10(b,1)),flip(c),xx(b)]. given #342 (F,wt=3): 2698 c1' != 1 | c1 = 0. [para(284(a,1),148(a,1,2,1)),rewrite(56(4),2(4),53(4),284(11),56(6),319(8)),flip(b)]. given #343 (F,wt=8): 2561 ((x ^ c1) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2479(a,1,1,1))]. given #344 (T,wt=8): 2572 c2' ^ ((c2 ^ x) v (c1 ^ y)) = 0. [para(2505(a,1),4(a,1)),flip(a)]. given #345 (T,wt=8): 2573 ((c2 ^ x) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2505(a,1,1,2))]. given #346 (A,wt=11): 149 x ^ (y v (x v z))' = 0. [para(17(a,1),129(a,1,2,1))]. given #347 (F,wt=8): 2584 c2' ^ ((x ^ c1) v (c2 ^ y)) = 0. [para(4(a,1),2506(a,1,2,1))]. given #348 (F,wt=8): 2612 c2' ^ ((x ^ c2) v (c1 ^ y)) = 0. [para(2519(a,1),4(a,1)),flip(a)]. given #349 (T,wt=8): 2613 ((x ^ c2) v (y ^ c1)) ^ c2' = 0. [para(4(a,1),2519(a,1,1,2))]. given #350 (T,wt=8): 2624 c2' ^ ((x ^ c1) v (y ^ c2)) = 0. [para(4(a,1),2520(a,1,2,1))]. given #351 (A,wt=11): 150 x ^ (y ^ (x v z)') = 0. [para(129(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #352 (F,wt=8): 2660 c2' ^ ((x ^ c1) v (c1 ^ y)) = 0. [para(4(a,1),2548(a,1,2,1))]. given #353 (F,wt=8): 2679 c2' ^ ((x ^ c1) v (y ^ c1)) = 0. [para(4(a,1),2560(a,1,2,1))]. given #354 (T,wt=8): 2710 c2' ^ ((c2 ^ x) v (y ^ c1)) = 0. [para(4(a,1),2572(a,1,2,2))]. given #355 (T,wt=8): 2745 c2' ^ ((x ^ c2) v (y ^ c1)) = 0. [para(4(a,1),2612(a,1,2,2))]. given #356 (A,wt=15): 152 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),23(a,1,2,2,1))]. given #357 (F,wt=9): 2348 (x v (c1 ^ y)) ^ (x v c2)' = 0. [para(137(a,1),144(a,1,2,1))]. given #358 (F,wt=9): 2374 (x v y)' != 1 | y v x = 0. [para(2(a,1),1813(a,1,1))]. given #359 (T,wt=9): 2376 (x ^ y)' != 1 | x ^ y = 0. [para(27(a,1),1813(a,1,1)),rewrite(27(8))]. given #360 (T,wt=9): 2380 ((x ^ c1) v y) ^ (c2 v y)' = 0. [para(139(a,1),144(a,1,2,1))]. given #361 (A,wt=24): 153 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 #362 (F,wt=7): 2892 c2 ^ c1' != 0 | c1 v (c2 ^ c1') = c1. [para(297(a,1),153(a,1)),rewrite(4(7),319(12),4(15),2(17),775(18)),flip(c),xx(a)]. given #363 (F,wt=9): 2451 (x v y)' != 0 | y v x = 1. [para(2(a,1),2023(a,1,1))]. given #364 (T,wt=9): 2455 (x v (y ^ c1)) ^ (x v c2)' = 0. [para(143(a,1),144(a,1,2,1))]. given #365 (T,wt=9): 2467 (x v (c1 ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),2244(a,1,1))]. given #366 (A,wt=19): 154 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(17(a,1),23(a,1,2,2))]. given #367 (F,wt=9): 2468 ((c1 ^ x) v y) ^ (y v c2)' = 0. [para(2(a,1),2244(a,1,2,1))]. given #368 (F,wt=9): 2469 (c2 v x)' ^ ((c1 ^ y) v x) = 0. [para(2244(a,1),4(a,1)),flip(a)]. given #369 (T,wt=9): 2539 (x v y) ^ (y v x)' = 0. [para(62(a,1),145(a,1,2,1))]. given #370 (T,wt=9): 2839 (x v c2)' ^ (x v (c1 ^ y)) = 0. [para(2348(a,1),4(a,1)),flip(a)]. given #371 (A,wt=23): 155 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(23(a,1),19(a,1,2)),flip(a)]. given #372 (F,wt=9): 2852 (x ^ y)' != 1 | y ^ x = 0. [para(4(a,1),2376(a,1,1))]. given #373 (F,wt=9): 2855 (x v (y ^ c1)) ^ (c2 v x)' = 0. [para(2(a,1),2380(a,1,1))]. given #374 (T,wt=9): 2856 ((x ^ c1) v y) ^ (y v c2)' = 0. [para(2(a,1),2380(a,1,2,1))]. given #375 (T,wt=9): 2857 (c2 v x)' ^ ((y ^ c1) v x) = 0. [para(2380(a,1),4(a,1)),flip(a)]. given #376 (A,wt=19): 156 (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 #377 (F,wt=9): 2978 (x v c2)' ^ (x v (y ^ c1)) = 0. [para(2455(a,1),4(a,1)),flip(a)]. given #378 (F,wt=9): 2991 (c2 v x)' ^ (x v (c1 ^ y)) = 0. [para(2467(a,1),4(a,1)),flip(a)]. given #379 (T,wt=9): 3029 (x v c2)' ^ ((c1 ^ y) v x) = 0. [para(2468(a,1),4(a,1)),flip(a)]. given #380 (T,wt=9): 3186 (c2 v x)' ^ (x v (y ^ c1)) = 0. [para(2855(a,1),4(a,1)),flip(a)]. given #381 (A,wt=17): 157 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(23(a,1),22(a,1,2)),rewrite(22(3)),flip(a)]. given #382 (F,wt=9): 3216 (x v c2)' ^ ((y ^ c1) v x) = 0. [para(2856(a,1),4(a,1)),flip(a)]. given #383 (F,wt=9): 3238 (c2 v x)' ^ (y ^ c1) = 0. [para(2857(a,1),69(a,1,2)),rewrite(4(4),74(4)),flip(a)]. given #384 (T,wt=9): 3297 (x v c2)' ^ (y ^ c1) = 0. [para(2978(a,1),91(a,1,2)),rewrite(4(4),74(4)),flip(a)]. given #385 (T,wt=10): 167 c1 v (c2' ^ x) != 1 | c2' ^ x = c1'. [para(158(a,1),10(b,1)),flip(c),xx(b)]. given #386 (A,wt=11): 161 x ^ (y v (z v x))' = 0. [para(3(a,1),144(a,1,2,1))]. given #387 (F,wt=10): 179 c1 v (x ^ c2') != 1 | x ^ c2' = c1'. [para(160(a,1),10(b,1)),flip(c),xx(b)]. given #388 (F,wt=10): 210 c2 ^ (c1' v x) != 0 | c2' = c1' v x. [para(199(a,1),10(a,1)),xx(a)]. given #389 (T,wt=10): 214 c2 ^ (x v c1') != 0 | c2' = x v c1'. [para(202(a,1),10(a,1)),xx(a)]. given #390 (T,wt=10): 225 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),46(a,1,2)),rewrite(46(4)),flip(a)]. given #391 (A,wt=11): 162 x ^ ((y v x)' ^ z) = 0. [para(144(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #392 (F,wt=9): 3448 ((c2 v x) ^ y) v (c1 ^ y)' = 1. [para(225(a,1),183(a,1,2,1))]. given #393 (F,wt=8): 3491 ((c2 v x) ^ (c1 v y)) v c1' = 1. [para(6(a,1),3448(a,1,2,1))]. given #394 (T,wt=8): 3498 ((c2 v x) ^ (y v c1)) v c1' = 1. [para(20(a,1),3448(a,1,2,1))]. given #395 (T,wt=8): 3501 ((c2 v x) ^ (c2 v y)) v c1' = 1. [para(217(a,1),3448(a,1,2,1))]. given #396 (A,wt=13): 163 x ^ (y ^ (z v (x ^ y))') = 0. [para(144(a,1),5(a,1)),flip(a)]. given #397 (F,wt=8): 3502 ((c2 v x) ^ (y v c2)) v c1' = 1. [para(223(a,1),3448(a,1,2,1))]. given #398 (F,wt=8): 3537 c1' v ((c2 v x) ^ (c1 v y)) = 1. [para(3491(a,1),2(a,1)),flip(a)]. given #399 (T,wt=8): 3538 ((x v c2) ^ (c1 v y)) v c1' = 1. [para(2(a,1),3491(a,1,1,1))]. given #400 (T,wt=8): 3540 ((c1 v x) ^ (c2 v y)) v c1' = 1. [para(4(a,1),3491(a,1,1))]. given #401 (A,wt=14): 164 x v (y v x)' != 1 | (y v x)' = x'. [para(144(a,1),10(b,1)),flip(c),xx(b)]. given #402 (F,wt=8): 3554 c1' v ((c2 v x) ^ (y v c1)) = 1. [para(3498(a,1),2(a,1)),flip(a)]. given #403 (F,wt=8): 3555 ((x v c2) ^ (y v c1)) v c1' = 1. [para(2(a,1),3498(a,1,1,1))]. given #404 (T,wt=8): 3557 ((x v c1) ^ (c2 v y)) v c1' = 1. [para(4(a,1),3498(a,1,1))]. given #405 (T,wt=8): 3571 c1' v ((c2 v x) ^ (c2 v y)) = 1. [para(3501(a,1),2(a,1)),flip(a)]. given #406 (A,wt=13): 165 (x v y) ^ (x v (z v y))' = 0. [para(17(a,1),144(a,1,2,1))]. given #407 (F,wt=8): 3572 ((x v c2) ^ (c2 v y)) v c1' = 1. [para(2(a,1),3501(a,1,1,1))]. given #408 (F,wt=8): 3602 c1' v ((c2 v x) ^ (y v c2)) = 1. [para(3502(a,1),2(a,1)),flip(a)]. given #409 (T,wt=8): 3603 ((x v c2) ^ (y v c2)) v c1' = 1. [para(2(a,1),3502(a,1,1,1))]. given #410 (T,wt=8): 3616 c1' v ((x v c2) ^ (c1 v y)) = 1. [para(2(a,1),3537(a,1,2,1))]. given #411 (A,wt=11): 166 x ^ (y ^ (z v x)') = 0. [para(144(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #412 (F,wt=8): 3617 c1' v ((c1 v x) ^ (c2 v y)) = 1. [para(4(a,1),3537(a,1,2))]. given #413 (F,wt=8): 3628 ((c1 v x) ^ (y v c2)) v c1' = 1. [para(4(a,1),3538(a,1,1))]. given #414 (T,wt=8): 3665 c1' v ((x v c2) ^ (y v c1)) = 1. [para(2(a,1),3554(a,1,2,1))]. given #415 (T,wt=8): 3667 c1' v ((x v c1) ^ (c2 v y)) = 1. [para(4(a,1),3554(a,1,2))]. given #416 (A,wt=18): 168 c1 ^ (x v (c1 ^ ((c1 ^ x) v (c2' ^ (y ^ (c1 v x)))))) = c1 ^ x. [para(158(a,1),12(a,2,2,2)),rewrite(5(10),35(17))]. given #417 (F,wt=8): 3679 ((x v c1) ^ (y v c2)) v c1' = 1. [para(4(a,1),3555(a,1,1))]. given #418 (F,wt=8): 3703 c1' v ((x v c2) ^ (c2 v y)) = 1. [para(2(a,1),3571(a,1,2,1))]. given #419 (T,wt=8): 3753 c1' v ((x v c2) ^ (y v c2)) = 1. [para(2(a,1),3602(a,1,2,1))]. given #420 (T,wt=8): 3777 c1' v ((c1 v x) ^ (y v c2)) = 1. [para(4(a,1),3616(a,1,2))]. given #421 (A,wt=11): 169 c1 ^ (x ^ (c2' ^ y)) = 0. [para(158(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #422 (F,wt=8): 3826 c1' v ((x v c1) ^ (y v c2)) = 1. [para(4(a,1),3665(a,1,2))]. given #423 (F,wt=9): 3468 c1 ^ (((c1 v x) ^ (c2 v y)) v z) = c1. [para(225(a,1),157(a,1)),rewrite(217(12))]. given #424 (T,wt=9): 3486 (c1 ^ x)' v ((c2 v y) ^ x) = 1. [para(3448(a,1),2(a,1)),flip(a)]. given #425 (T,wt=9): 3487 ((x v c2) ^ y) v (c1 ^ y)' = 1. [para(2(a,1),3448(a,1,1,1))]. given #426 (A,wt=23): 170 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(24(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #427 (F,wt=9): 3489 (x ^ (c2 v y)) v (c1 ^ x)' = 1. [para(4(a,1),3448(a,1,1))]. given #428 (F,wt=7): 4101 (x ^ c1) v (c1 ^ x)' = 1. [para(81(a,1),3489(a,1,2,1)),rewrite(5(5),239(5))]. given #429 (T,wt=9): 3490 ((c2 v x) ^ y) v (y ^ c1)' = 1. [para(4(a,1),3448(a,1,2,1))]. given #430 (T,wt=9): 3513 (x ^ (c2 v y)) v (x ^ c1)' = 1. [para(69(a,1),3448(a,1,1)),rewrite(3(7),239(9))]. given #431 (A,wt=21): 171 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),24(a,1,2,1))]. given #432 (F,wt=9): 3915 c1 ^ (((x v c1) ^ (c2 v y)) v z) = c1. [para(2(a,1),3468(a,1,2,1,1))]. given #433 (F,wt=9): 3916 c1 ^ (((c1 v x) ^ (y v c2)) v z) = c1. [para(2(a,1),3468(a,1,2,1,2))]. given #434 (T,wt=9): 3917 c1 ^ (x v ((c1 v y) ^ (c2 v z))) = c1. [para(2(a,1),3468(a,1,2))]. given #435 (T,wt=9): 3918 c1 ^ (((c2 v x) ^ (c1 v y)) v z) = c1. [para(4(a,1),3468(a,1,2,1))]. given #436 (A,wt=20): 173 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(24(a,1),10(a,1))]. given #437 (F,wt=9): 3929 c1 ^ (((c2 v x) ^ (c2 v y)) v z) = c1. [para(124(a,1),3468(a,1,2,1,1))]. given #438 (F,wt=9): 3930 c1 ^ (((x v c2) ^ (c2 v y)) v z) = c1. [para(126(a,1),3468(a,1,2,1,1))]. given #439 (T,wt=9): 3944 (c1 ^ x)' v ((y v c2) ^ x) = 1. [para(2(a,1),3486(a,1,2,1))]. given #440 (T,wt=9): 3945 (x ^ c1)' v ((c2 v y) ^ x) = 1. [para(4(a,1),3486(a,1,1,1))]. given #441 (A,wt=21): 174 x v (y v ((x ^ z) v u)) = y v (x v u). [para(24(a,1),17(a,1,2)),flip(a)]. given #442 (F,wt=9): 3946 (c1 ^ x)' v (x ^ (c2 v y)) = 1. [para(4(a,1),3486(a,1,2))]. given #443 (F,wt=9): 3962 (x ^ c1)' v (x ^ (c2 v y)) = 1. [para(69(a,1),3486(a,1,2)),rewrite(3(4),239(6))]. given #444 (T,wt=9): 3988 (x ^ (y v c2)) v (c1 ^ x)' = 1. [para(4(a,1),3487(a,1,1))]. given #445 (T,wt=9): 3989 ((x v c2) ^ y) v (y ^ c1)' = 1. [para(4(a,1),3487(a,1,2,1))]. given #446 (A,wt=17): 175 x v ((y ^ (x ^ z)) v u) = x v u. [para(19(a,1),24(a,1,2,1))]. given #447 (F,wt=9): 4004 (x ^ (y v c2)) v (x ^ c1)' = 1. [para(69(a,1),3487(a,1,1)),rewrite(3(7),618(9))]. given #448 (F,wt=9): 4186 c1 ^ (((x v c1) ^ (y v c2)) v z) = c1. [para(2(a,1),3915(a,1,2,1,2))]. given #449 (T,wt=9): 4187 c1 ^ (x v ((y v c1) ^ (c2 v z))) = c1. [para(2(a,1),3915(a,1,2))]. given #450 (T,wt=9): 4189 c1 ^ (((c2 v x) ^ (y v c1)) v z) = c1. [para(4(a,1),3915(a,1,2,1))]. given #451 (A,wt=15): 176 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(24(a,1),20(a,1,2)),rewrite(4(4))]. given #452 (F,wt=8): 4767 c2 v ((c1 ^ x) v (c2 ^ y))' = 1. [para(176(a,1),1646(a,1,2,1))]. given #453 (F,wt=8): 4768 c2 v ((c1 ^ x) v (y ^ c2))' = 1. [para(176(a,1),1647(a,1,2,1))]. given #454 (T,wt=8): 4797 c2 v ((c2 ^ x) v (c1 ^ y))' = 1. [para(2(a,1),4767(a,1,2,1))]. given #455 (T,wt=8): 4799 c2 v ((x ^ c1) v (c2 ^ y))' = 1. [para(4(a,1),4767(a,1,2,1,1))]. given #456 (A,wt=11): 177 ((x ^ y) v z) ^ (x v z)' = 0. [para(24(a,1),144(a,1,2,1))]. given #457 (F,wt=8): 4806 c2 v ((c1 ^ x) v (y ^ c1))' = 1. [para(47(a,1),4767(a,1,2,1,2))]. given #458 (F,wt=8): 4812 c2 v ((x ^ c2) v (c1 ^ y))' = 1. [para(2(a,1),4768(a,1,2,1))]. given #459 (T,wt=8): 4814 c2 v ((x ^ c1) v (y ^ c2))' = 1. [para(4(a,1),4768(a,1,2,1,1))]. given #460 (T,wt=8): 4827 c2 v ((c2 ^ x) v (y ^ c1))' = 1. [para(4(a,1),4797(a,1,2,1,2))]. given #461 (A,wt=11): 178 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),160(a,1,2))]. given #462 (F,wt=8): 4834 c2 v ((x ^ c1) v (c1 ^ y))' = 1. [para(47(a,1),4797(a,1,2,1,1))]. given #463 (F,wt=8): 4847 c2 v ((x ^ c1) v (y ^ c1))' = 1. [para(47(a,1),4799(a,1,2,1,2))]. given #464 (T,wt=8): 4895 c2 v ((c1 ^ x) v (c1 ^ y))' = 1. [para(4(a,1),4806(a,1,2,1,2))]. given #465 (T,wt=8): 4908 c2 v ((x ^ c2) v (y ^ c1))' = 1. [para(4(a,1),4812(a,1,2,1,2))]. given #466 (A,wt=18): 180 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2' ^ (c1 v x)))))) = c1 ^ x. [para(160(a,1),12(a,2,2,2)),rewrite(5(10),35(17))]. given #467 (F,wt=9): 4215 c1 ^ (x v ((c1 v y) ^ (z v c2))) = c1. [para(2(a,1),3916(a,1,2))]. given #468 (F,wt=9): 4217 c1 ^ (((x v c2) ^ (c1 v y)) v z) = c1. [para(4(a,1),3916(a,1,2,1))]. given #469 (T,wt=9): 4227 c1 ^ (((c2 v x) ^ (y v c2)) v z) = c1. [para(124(a,1),3916(a,1,2,1,1))]. given #470 (T,wt=9): 4228 c1 ^ (((x v c2) ^ (y v c2)) v z) = c1. [para(126(a,1),3916(a,1,2,1,1))]. given #471 (A,wt=11): 181 x v ((x ^ y)' v z) = 1. [para(172(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #472 (F,wt=9): 4246 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(4(a,1),3917(a,1,2,2))]. given #473 (F,wt=9): 4256 c1 ^ (x v ((c2 v y) ^ (c2 v z))) = c1. [para(124(a,1),3917(a,1,2,2,1))]. given #474 (T,wt=9): 4257 c1 ^ (x v ((y v c2) ^ (c2 v z))) = c1. [para(126(a,1),3917(a,1,2,2,1))]. given #475 (T,wt=9): 4382 (x ^ c1)' v ((y v c2) ^ x) = 1. [para(4(a,1),3944(a,1,1,1))]. given #476 (A,wt=13): 182 x v (y v ((x v y) ^ z)') = 1. [para(172(a,1),3(a,1)),flip(a)]. given #477 (F,wt=9): 4383 (c1 ^ x)' v (x ^ (y v c2)) = 1. [para(4(a,1),3944(a,1,2))]. given #478 (F,wt=9): 4398 (x ^ c1)' v (x ^ (y v c2)) = 1. [para(69(a,1),3944(a,1,2)),rewrite(3(4),618(6))]. given #479 (T,wt=9): 4646 c1 ^ (x v ((y v c1) ^ (z v c2))) = c1. [para(2(a,1),4186(a,1,2))]. given #480 (T,wt=9): 4649 c1 ^ (((x v c2) ^ (y v c1)) v z) = c1. [para(4(a,1),4186(a,1,2,1))]. given #481 (A,wt=13): 184 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),172(a,1,2,1))]. given #482 (F,wt=9): 4679 c1 ^ (x v ((c2 v y) ^ (z v c1))) = c1. [para(4(a,1),4187(a,1,2,2))]. given #483 (F,wt=9): 5018 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(4(a,1),4215(a,1,2,2))]. given #484 (T,wt=9): 5027 c1 ^ (x v ((c2 v y) ^ (z v c2))) = c1. [para(124(a,1),4215(a,1,2,2,1))]. given #485 (T,wt=9): 5028 c1 ^ (x v ((y v c2) ^ (z v c2))) = c1. [para(126(a,1),4215(a,1,2,2,1))]. given #486 (A,wt=14): 185 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(172(a,1),10(a,1)),flip(c),xx(a)]. given #487 (F,wt=9): 5323 c1 ^ (x v ((y v c2) ^ (z v c1))) = c1. [para(4(a,1),4646(a,1,2,2))]. given #488 (F,wt=9): 5390 (x ^ y) v (y ^ x)' = 1. [para(69(a,1),184(a,1,2,1))]. given #489 (T,wt=10): 239 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(217(a,1),19(a,1,2)),flip(a)]. given #490 (T,wt=10): 241 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(223(a,1),5(a,1,1)),flip(a)]. given #491 (A,wt=11): 186 x v (y v (x ^ z)') = 1. [para(172(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #492 (F,wt=10): 244 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(223(a,1),19(a,1,2)),flip(a)]. given #493 (F,wt=10): 246 c1 v (c2 v x)' != 1 | (c2 v x)' = c1'. [para(226(a,1),10(b,1)),flip(c),xx(b)]. given #494 (T,wt=10): 251 c1 v (x v c2)' != 1 | (x v c2)' = c1'. [para(228(a,1),10(b,1)),flip(c),xx(b)]. given #495 (T,wt=10): 275 c2 ^ (c1 ^ x)' != 0 | (c1 ^ x)' = c2'. [para(272(a,1),10(a,1)),flip(c),xx(a)]. given #496 (A,wt=11): 187 x v (y ^ (x ^ z))' = 1. [para(19(a,1),172(a,1,2,1))]. given #497 (F,wt=10): 281 c2 ^ (x ^ c1)' != 0 | (x ^ c1)' = c2'. [para(274(a,1),10(a,1)),flip(c),xx(a)]. given #498 (F,wt=10): 285 (c2 ^ (c1 v x)) v (c1' v y) = 1. [para(263(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #499 (T,wt=10): 287 (c2 ^ (c1 v x)) v (y v c1') = 1. [para(263(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 87 (0.00 of 1.80 sec). given #500 (T,wt=10): 288 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(17(a,1),263(a,1,1,2))]. given #501 (A,wt=11): 188 x v ((y ^ x)' v z) = 1. [para(183(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #502 (F,wt=10): 298 (c2 ^ (x v c1)) v (c1' v y) = 1. [para(269(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #503 (F,wt=10): 299 (c2 ^ (x v (y v c1))) v c1' = 1. [para(3(a,1),269(a,1,1,2))]. given #504 (T,wt=10): 301 (c2 ^ (x v c1)) v (y v c1') = 1. [para(269(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #505 (T,wt=10): 302 c1' v ((c2 ^ (c1 v x)) v y) = 1. [para(284(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #506 (A,wt=13): 189 x v (y v (z ^ (x v y))') = 1. [para(183(a,1),3(a,1)),flip(a)]. given #507 (F,wt=10): 304 c1' v (x v (c2 ^ (c1 v y))) = 1. [para(284(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #508 (F,wt=10): 305 c1' v (c2 ^ (x v (c1 v y))) = 1. [para(17(a,1),284(a,1,2,2))]. given #509 (T,wt=10): 306 c1' v ((c2 ^ (x v c1)) v y) = 1. [para(297(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #510 (T,wt=10): 307 c1' v (c2 ^ (x v (y v c1))) = 1. [para(3(a,1),297(a,1,2,2))]. given #511 (A,wt=11): 190 x v (y ^ (z ^ x))' = 1. [para(5(a,1),183(a,1,2,1))]. given #512 (F,wt=10): 309 c1' v (x v (c2 ^ (y v c1))) = 1. [para(297(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #513 (F,wt=10): 332 c2 ^ (c1' v x) != 0 | (c1' v x)' = c2. [para(199(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #514 (T,wt=10): 333 c2 ^ (x v c1') != 0 | (x v c1')' = c2. [para(202(a,1),36(a,1)),rewrite(4(8)),xx(a)]. given #515 (T,wt=10): 367 (x v c2) ^ c1' != 0 | (x v c2)' = c1'. [para(193(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #516 (A,wt=14): 191 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(183(a,1),10(a,1)),flip(c),xx(a)]. given #517 (F,wt=10): 371 (c2 v x) ^ c1' != 0 | (c2 v x)' = c1'. [para(202(a,1),37(a,1)),xx(a)]. given #518 (F,wt=10): 403 c1 v (c2' ^ x) != 1 | (c2' ^ x)' = c1. [para(158(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #519 (T,wt=10): 404 c1 v (x ^ c2') != 1 | (x ^ c2')' = c1. [para(160(a,1),38(b,1)),rewrite(2(5)),xx(b)]. given #520 (T,wt=10): 453 (x ^ c1) v c2' != 1 | (x ^ c1)' = c2'. [para(151(a,1),39(b,1,2)),rewrite(76(9)),xx(b)]. given #521 (A,wt=25): 192 x v ((y ^ ((y ^ x) v (z ^ (y v x)))) v (y ^ (x v (y ^ z)))') = 1. [para(12(a,1),183(a,1,2,1)),rewrite(3(11))]. given #522 (F,wt=10): 457 (c1 ^ x) v c2' != 1 | (c1 ^ x)' = c2'. [para(160(a,1),39(b,1)),xx(b)]. given #523 (F,wt=10): 489 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0. [para(479(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #524 (T,wt=10): 491 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0. [para(479(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #525 (T,wt=10): 492 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0. [para(19(a,1),479(a,1,1,2))]. given #526 (A,wt=11): 194 x v (y v (z ^ x)') = 1. [para(183(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #527 (F,wt=10): 497 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0. [para(483(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #528 (F,wt=10): 498 (c1 v (x ^ (y ^ c2))) ^ c2' = 0. [para(5(a,1),483(a,1,1,2))]. given #529 (T,wt=10): 500 (c1 v (x ^ c2)) ^ (y ^ c2') = 0. [para(483(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #530 (T,wt=10): 516 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(488(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #531 (A,wt=13): 195 (x ^ y) v (x ^ (z ^ y))' = 1. [para(19(a,1),183(a,1,2,1))]. given #532 (F,wt=10): 517 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(488(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #533 (F,wt=10): 518 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(19(a,1),488(a,1,2,2))]. given #534 (T,wt=10): 521 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(496(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #535 (T,wt=10): 522 c2' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(5(a,1),496(a,1,2,2))]. given #536 (A,wt=15): 196 x v (y v (z v (x v y)')) = 1. [para(21(a,1),183(a,1,2,1)),rewrite(3(5),3(4))]. given #537 (F,wt=10): 523 c2' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(496(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #538 (F,wt=10): 832 c2 ^ (c1 v x) != 1 | c1 != 0 | c1' = c2 ^ (c1 v x). [para(597(a,1),10(a,1)),rewrite(69(12),4(9),13(9))]. given #539 (T,wt=10): 837 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (c1 v x))' = c1. [para(597(a,1),36(a,1)),rewrite(4(12),69(12),4(9),13(9))]. given #540 (T,wt=10): 842 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0. [para(836(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #541 (A,wt=11): 197 ((x v y) ^ z) v (x ^ z)' = 1. [para(22(a,1),183(a,1,2,1))]. given #542 (F,wt=10): 844 c1 ^ (c2 ^ (x v (c1 v y)))' = 0. [para(17(a,1),836(a,1,2,1,2))]. given #543 (F,wt=9): 6311 c1 ^ (c2 ^ (x v (c2 ^ (c1 v y))))' = 0. [para(597(a,1),844(a,1,2,1,2,2))]. given #544 (T,wt=9): 6312 c1 ^ (c2 ^ (x v (c2 ^ (y v c1))))' = 0. [para(602(a,1),844(a,1,2,1,2,2))]. given #545 (T,wt=9): 6318 c1 ^ (c2 ^ ((c2 ^ (c1 v x)) v y))' = 0. [para(2(a,1),6311(a,1,2,1,2))]. given #546 (A,wt=13): 198 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(23(a,1),183(a,1,2,1))]. given #547 (F,wt=9): 6331 c1 ^ (c2 ^ ((c2 ^ (x v c1)) v y))' = 0. [para(2(a,1),6312(a,1,2,1,2))]. given #548 (F,wt=10): 845 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0. [para(836(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #549 (T,wt=10): 846 c1 v (c2 ^ (c1 v x))' != 1 | c2 ^ (c1 v x) = c1. [para(836(a,1),38(b,1)),rewrite(2(7),319(18)),xx(b)]. given #550 (T,wt=10): 848 c1 ^ (c2 ^ (x v (y v c1)))' = 0. [para(3(a,1),841(a,1,2,1,2))]. given #551 (A,wt=14): 201 c2 ^ (c1' v (c2 ^ ((c2 ^ c1') v x))) = c2 ^ (c1' v (c2 ^ x)). [para(193(a,1),12(a,1,2,2,2,2,2)),rewrite(32(10))]. given #552 (F,wt=8): 6451 c2 ^ (c1' v (c2 ^ (c2 ^ c1')')) = c2. [para(8(a,1),201(a,1,2,2,2)),rewrite(4(6),50(6),2(5),193(5),4(3),50(3)),flip(a)]. given #553 (F,wt=7): 6495 c1' v (c2 ^ (c2 ^ c1')') = 1. [para(6451(a,1),26(a,1,2)),rewrite(2(12),62(12),2(4),193(4)),flip(a)]. given #554 (T,wt=5): 6498 c2 ^ (c2 ^ c1')' = c1. [hyper(72,a,6495,a,b,34,a),rewrite(319(3)),flip(a)]. given #555 (T,wt=4): 6505 c1 != 0 | c2 ^ c1' = c2. [para(6498(a,1),38(b,1)),rewrite(2(7),172(7),319(12)),xx(a)]. given #556 (A,wt=15): 203 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),25(a,1,2,2,1))]. given #557 (F,wt=5): 6504 c1 ^ (c2 ^ c1')' = c1. [para(6498(a,1),46(a,1,2)),rewrite(28(3)),flip(a)]. given #558 (F,wt=6): 6500 c1 != 0 | (c2 ^ c1')' = c2'. [para(6498(a,1),10(b,1)),rewrite(172(7)),flip(c),xx(a)]. given #559 (T,wt=8): 6503 c1 v (c2 ^ c1')' = (c2 ^ c1')'. [para(6498(a,1),26(a,1,2)),rewrite(2(7))]. given #560 (T,wt=7): 6583 c1 ^ (x v (c2 ^ c1')') = c1. [para(6503(a,1),61(a,1,2,2))]. given #561 (A,wt=24): 204 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 #562 (F,wt=7): 6616 c1 ^ ((c2 ^ c1')' v x) = c1. [para(2(a,1),6583(a,1,2))]. given #563 (F,wt=7): 6653 c1 v c2' != 1 | c2 ^ (c1 v c2') = c2. [para(496(a,1),204(b,1)),rewrite(2(4),319(12),2(15),4(17),597(18)),flip(c),xx(b)]. given #564 (T,wt=8): 6511 (c2 ^ c1')' != 1 | c1 != 0 | c2 ^ c1' = c1. [para(6498(a,1),115(b,1)),rewrite(319(16),6498(21)),flip(a)]. given #565 (T,wt=8): 6519 (c2 ^ c1')' v (x ^ c1)' = 1. [para(6498(a,1),190(a,1,2,1,2))]. given #566 (A,wt=23): 205 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 #567 (F,wt=8): 6600 c1 ^ (x v (c2 ^ c1')')' = 0. [para(6503(a,1),149(a,1,2,1,2))]. given #568 (F,wt=8): 6784 c1 ^ ((c2 ^ c1')' v x)' = 0. [para(6616(a,1),973(a,1,2)),rewrite(4(9))]. given #569 (T,wt=8): 6804 (x ^ c1)' v (c2 ^ c1')' = 1. [para(6519(a,1),2(a,1)),flip(a)]. given #570 (T,wt=8): 6806 (c2 ^ c1')' v (c1 ^ x)' = 1. [para(4(a,1),6519(a,1,2,1))]. given #571 (A,wt=19): 206 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(19(a,1),25(a,1,2,2))]. given #572 (F,wt=8): 6873 (c1 ^ x)' v (c2 ^ c1')' = 1. [para(4(a,1),6804(a,1,1,1))]. given #573 (F,wt=9): 6523 c1' v ((c2 v x) ^ (c2 ^ c1')') = 1. [para(6498(a,1),197(a,1,2,1)),rewrite(2(11))]. given #574 (T,wt=9): 6524 c1' v ((c2 ^ c1')' ^ (c1 v x)) = 1. [para(6498(a,1),198(a,1,1,2,1)),rewrite(6498(15),2(11))]. given #575 (T,wt=9): 6574 c1' v ((x v c2) ^ (c2 ^ c1')') = 1. [para(6504(a,1),3487(a,1,2,1)),rewrite(2(11))]. given #576 (A,wt=19): 207 (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 #577 (F,wt=9): 6575 c1' v ((c2 ^ c1')' ^ (c2 v x)) = 1. [para(6504(a,1),3489(a,1,2,1)),rewrite(2(11))]. given #578 (F,wt=9): 6576 c1' v ((c2 ^ c1')' ^ (x v c2)) = 1. [para(6504(a,1),3988(a,1,2,1)),rewrite(2(11))]. given #579 (T,wt=9): 6578 c1' v ((c1 v x) ^ (c2 ^ c1')') = 1. [para(6504(a,1),197(a,1,2,1)),rewrite(2(11))]. given #580 (T,wt=9): 6595 c1 ^ ((c2 v x) ^ (c2 ^ c1')')' = 0. [para(6503(a,1),2183(a,1,2,1,2))]. given #581 (A,wt=13): 208 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(25(a,1),144(a,1,2,1))]. given #582 (F,wt=9): 6596 c1 ^ ((x v c2) ^ (c2 ^ c1')')' = 0. [para(6503(a,1),2196(a,1,2,1,2))]. given #583 (F,wt=9): 6597 c1 ^ ((c2 ^ c1')' ^ (c2 v x))' = 0. [para(6503(a,1),2197(a,1,2,1,1))]. given #584 (T,wt=9): 6598 c1 ^ ((c2 ^ c1')' ^ (x v c2))' = 0. [para(6503(a,1),2221(a,1,2,1,1))]. given #585 (T,wt=9): 6613 c1' v (c2 ^ (x v (c2 ^ c1')')) = 1. [para(6503(a,1),288(a,1,1,2,2)),rewrite(2(11))]. given #586 (A,wt=17): 209 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 #587 (F,wt=9): 6615 c1 ^ (c2 ^ (x v (c2 ^ c1')'))' = 0. [para(6503(a,1),844(a,1,2,1,2,2))]. given #588 (F,wt=9): 6775 c1' v (c2 ^ ((c2 ^ c1')' v x)) = 1. [para(6616(a,1),229(a,1,2,1)),rewrite(2(11))]. given #589 (T,wt=9): 6942 c1' v ((c2 ^ c1')' ^ (x v c1)) = 1. [para(2(a,1),6524(a,1,2,2))]. given #590 (T,wt=9): 7073 c1' v ((x v c1) ^ (c2 ^ c1')') = 1. [para(2(a,1),6578(a,1,2,1))]. given #591 (A,wt=24): 211 c2 ^ (c1' v (x v (c2 ^ ((c2 ^ (c1' v x)) v y)))) = c2 ^ (c1' v (x v (c2 ^ y))). [para(199(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12),3(13),3(21))]. given #592 (F,wt=9): 7195 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z) = c2. [para(209(a,1),134(a,1)),rewrite(120(4)),flip(a)]. given #593 (F,wt=9): 7199 c2 v (((c2 ^ x) v (y ^ c1)) ^ z) = c2. [para(209(a,1),139(a,1)),rewrite(122(4)),flip(a)]. given #594 (T,wt=9): 7228 c1 ^ (c2 ^ ((c2 ^ c1')' v x))' = 0. [para(2(a,1),6615(a,1,2,1,2))]. given #595 (T,wt=9): 7304 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),7195(a,1,2,1))]. given #596 (A,wt=11): 212 c2 v (x v (c1' v y)) = 1. [para(199(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #597 (F,wt=9): 7306 c2 v (((x ^ c2) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),7195(a,1,2,1,1))]. given #598 (F,wt=9): 7307 c2 v (x ^ ((c2 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),7195(a,1,2))]. given #599 (T,wt=9): 7315 c2 v (((x ^ c1) v (c1 ^ y)) ^ z) = c2. [para(47(a,1),7195(a,1,2,1,1))]. given #600 (T,wt=9): 7345 c2 v (((x ^ c1) v (c2 ^ y)) ^ z) = c2. [para(2(a,1),7199(a,1,2,1))]. given #601 (A,wt=11): 213 c2 v (x v (y v c1')) = 1. [para(3(a,1),202(a,1,2))]. given #602 (F,wt=9): 7347 c2 v (((x ^ c2) v (y ^ c1)) ^ z) = c2. [para(4(a,1),7199(a,1,2,1,1))]. given #603 (F,wt=9): 7348 c2 v (x ^ ((c2 ^ y) v (z ^ c1))) = c2. [para(4(a,1),7199(a,1,2))]. given #604 (T,wt=9): 7356 c2 v (((x ^ c1) v (y ^ c1)) ^ z) = c2. [para(47(a,1),7199(a,1,2,1,1))]. given #605 (T,wt=9): 7398 c2 v (((c1 ^ x) v (y ^ c2)) ^ z) = c2. [para(4(a,1),7304(a,1,2,1,2))]. given #606 (A,wt=24): 215 c2 ^ (x v (c1' v (c2 ^ ((c2 ^ (x v c1')) v y)))) = c2 ^ (x v (c1' v (c2 ^ y))). [para(202(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12),3(13),3(21))]. given #607 (F,wt=9): 7399 c2 v (x ^ ((c1 ^ y) v (c2 ^ z))) = c2. [para(4(a,1),7304(a,1,2))]. given #608 (F,wt=9): 7407 c2 v (((c1 ^ x) v (y ^ c1)) ^ z) = c2. [para(47(a,1),7304(a,1,2,1,2))]. given #609 (T,wt=9): 7440 c2 v (x ^ ((y ^ c2) v (c1 ^ z))) = c2. [para(4(a,1),7306(a,1,2))]. given #610 (T,wt=9): 7486 c2 v (x ^ ((y ^ c1) v (c1 ^ z))) = c2. [para(47(a,1),7307(a,1,2,2,1))]. given #611 (A,wt=16): 216 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(46(a,1),5(a,2,2)),rewrite(19(5),5(4))]. given #612 (F,wt=9): 7516 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z) = c2. [para(4(a,1),7315(a,1,2,1,1))]. given #613 (F,wt=9): 7555 c2 v (((x ^ c1) v (y ^ c2)) ^ z) = c2. [para(4(a,1),7345(a,1,2,1,2))]. given #614 (T,wt=9): 7556 c2 v (x ^ ((y ^ c1) v (c2 ^ z))) = c2. [para(4(a,1),7345(a,1,2))]. given #615 (T,wt=9): 7599 c2 v (x ^ ((y ^ c2) v (z ^ c1))) = c2. [para(4(a,1),7347(a,1,2))]. given #616 (A,wt=11): 218 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | c1' = c2 ^ x. [para(46(a,1),10(b,1))]. given #617 (F,wt=9): 7645 c2 v (x ^ ((y ^ c1) v (z ^ c1))) = c2. [para(47(a,1),7348(a,1,2,2,1))]. given #618 (F,wt=9): 7713 c2 v (x ^ ((c1 ^ y) v (z ^ c2))) = c2. [para(4(a,1),7398(a,1,2))]. given #619 (T,wt=9): 7780 c2 v (x ^ ((c1 ^ y) v (z ^ c1))) = c2. [para(47(a,1),7399(a,1,2,2,2))]. given #620 (T,wt=9): 7881 c2 v (x ^ ((c1 ^ y) v (c1 ^ z))) = c2. [para(4(a,1),7486(a,1,2,2,1))]. given #621 (A,wt=20): 219 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 #622 (F,wt=9): 7976 c2 v (x ^ ((y ^ c1) v (z ^ c2))) = c2. [para(4(a,1),7555(a,1,2))]. given #623 (F,wt=10): 849 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0. [para(841(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #624 (T,wt=10): 851 c1 ^ (x ^ (c2 ^ (y v c1))') = 0. [para(841(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #625 (T,wt=10): 852 c1 v (c2 ^ (x v c1))' != 1 | c2 ^ (x v c1) = c1. [para(841(a,1),38(b,1)),rewrite(2(7),319(18)),xx(b)]. given #626 (A,wt=20): 220 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 #627 (F,wt=10): 916 c2 ^ (x v c1) != 1 | c1 != 0 | c1' = c2 ^ (x v c1). [para(602(a,1),10(a,1)),rewrite(91(12),4(9),13(9))]. given #628 (F,wt=10): 918 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (x v c1))' = c1. [para(602(a,1),36(a,1)),rewrite(4(12),91(12),4(9),13(9))]. given #629 (T,wt=10): 1022 c2 != 1 | c1 v (c2 ^ x) != 0 | c2' = c1 v (c2 ^ x). [para(775(a,1),10(b,1)),rewrite(17(6),7(5),117(3))]. given #630 (T,wt=10): 1027 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (c2 ^ x))' = c2. [para(775(a,1),38(b,1)),rewrite(2(6),17(6),7(5),117(3))]. given #631 (A,wt=17): 221 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 #632 (F,wt=10): 1033 c2 v ((c1 v (c2 ^ x))' v y) = 1. [para(1025(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #633 (F,wt=10): 1037 c2 v (x v (c1 v (c2 ^ y))') = 1. [para(1025(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #634 (T,wt=10): 1038 c2 v (c1 v (x ^ (c2 ^ y)))' = 1. [para(19(a,1),1025(a,1,2,1,2))]. given #635 (T,wt=9): 8512 c2 v (c1 v (x ^ (c1 v (c2 ^ y))))' = 1. [para(775(a,1),1038(a,1,2,1,2,2))]. given #636 (A,wt=16): 222 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(46(a,1),19(a,1,2)),flip(a)]. given #637 (F,wt=9): 8513 c2 v (c1 v (x ^ (c1 v (y ^ c2))))' = 1. [para(781(a,1),1038(a,1,2,1,2,2))]. given #638 (F,wt=9): 8520 c2 v (c1 v ((c1 v (c2 ^ x)) ^ y))' = 1. [para(4(a,1),8512(a,1,2,1,2))]. given #639 (T,wt=9): 8556 c2 v (c1 v ((c1 v (x ^ c2)) ^ y))' = 1. [para(4(a,1),8513(a,1,2,1,2))]. given #640 (T,wt=10): 1039 c2 ^ (c1 v (c2 ^ x))' != 0 | c1 v (c2 ^ x) = c2. [para(1025(a,1),36(a,1)),rewrite(4(10),319(18)),xx(a)]. given #641 (A,wt=12): 227 c1 ^ (x ^ ((c2 ^ x) v y)) = c1 ^ x. [para(23(a,1),46(a,1,2)),rewrite(46(4)),flip(a)]. given #642 (F,wt=10): 1042 c2 v ((c1 v (x ^ c2))' v y) = 1. [para(1034(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #643 (F,wt=10): 1043 c2 v (c1 v (x ^ (y ^ c2)))' = 1. [para(5(a,1),1034(a,1,2,1,2))]. given #644 (T,wt=10): 1046 c2 v (x v (c1 v (y ^ c2))') = 1. [para(1034(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #645 (T,wt=10): 1047 c2 ^ (c1 v (x ^ c2))' != 0 | c1 v (x ^ c2) = c2. [para(1034(a,1),36(a,1)),rewrite(4(10),319(18)),xx(a)]. given #646 (A,wt=15): 230 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),27(a,1,1))]. given #647 (F,wt=10): 1112 c2 != 1 | c1 v (x ^ c2) != 0 | c2' = c1 v (x ^ c2). [para(781(a,1),10(b,1)),rewrite(17(6),26(5),117(3))]. given #648 (F,wt=10): 1115 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (x ^ c2))' = c2. [para(781(a,1),38(b,1)),rewrite(2(6),17(6),26(5),117(3))]. given #649 (T,wt=10): 1246 x ^ (c1 v (c2 ^ (x v y))) = c2 ^ x. [para(1196(a,1),22(a,1,2)),rewrite(4(3),69(4),4(6)),flip(a)]. given #650 (T,wt=10): 1250 x ^ (c1 v (c2 ^ (y v x))) = c2 ^ x. [para(1196(a,1),87(a,1,2)),rewrite(4(3),91(4),4(6)),flip(a)]. given #651 (A,wt=15): 231 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),27(a,1,2)),rewrite(5(3))]. given #652 (F,wt=10): 1377 (c1 v (c2 ^ x))' v (y v c2) = 1. [para(1025(a,1),103(a,1,1)),rewrite(50(10),1025(15))]. given #653 (F,wt=10): 1378 (c1 v (x ^ c2))' v (y v c2) = 1. [para(1034(a,1),103(a,1,1)),rewrite(50(10),1034(15))]. given #654 (T,wt=10): 1753 x v (c2 ^ (c1 v (x ^ y))) = c1 v x. [para(1670(a,1),24(a,1,2)),rewrite(2(3),62(4),2(6)),flip(a)]. given #655 (T,wt=10): 1762 x v (c2 ^ (c1 v (y ^ x))) = c1 v x. [para(1670(a,1),112(a,1,2)),rewrite(2(3),118(4),2(6)),flip(a)]. given #656 (A,wt=21): 232 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(27(a,1),17(a,1,2)),flip(a)]. given #657 (F,wt=10): 2154 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(47(a,1),133(a,1,1)),rewrite(26(8)),flip(a)]. given #658 (F,wt=10): 2173 (c2 v x) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(775(a,1),133(a,1,1)),rewrite(26(12)),flip(a)]. given #659 (T,wt=10): 2174 (c2 v x) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(781(a,1),133(a,1,1)),rewrite(26(12)),flip(a)]. given #660 (T,wt=8): 9059 c2 v x != 1 | c2 != 0 | (c2 v x)' = c2. [para(2174(a,1),204(b,1)),rewrite(2(4),124(4),2(9),124(9),4(9),6(9),117(7),2(15),124(15),4(15),6(15),117(13))]. given #661 (A,wt=19): 233 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(19(a,1),27(a,1,2,2))]. given #662 (F,wt=8): 9066 x v c2 != 1 | c2 != 0 | (c2 v x)' = c2. [para(2(a,1),9059(a,1))]. given #663 (F,wt=8): 9068 x v c2 != 1 | c2 != 0 | (x v c2)' = c2. [para(62(a,1),9059(a,1)),rewrite(62(12))]. given #664 (T,wt=8): 9101 c2 v x != 1 | c2 != 0 | (x v c2)' = c2. [para(2(a,1),9068(a,1))]. given #665 (T,wt=10): 2249 (c1 ^ x) v (y v c2) = y v c2. [para(62(a,1),134(a,2)),rewrite(697(8))]. given #666 (A,wt=15): 235 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(27(a,1),144(a,1,2,1)),rewrite(5(5),5(4))]. given #667 (F,wt=10): 2385 (x ^ c1) v (y v c2) = y v c2. [para(62(a,1),139(a,2)),rewrite(697(8))]. given #668 (F,wt=10): 2542 (x v c1) ^ (x v (c2 ^ (c1 v y)))' = 0. [para(597(a,1),145(a,1,2,1,2))]. given #669 (T,wt=10): 2543 (x v c1) ^ (x v (c2 ^ (y v c1)))' = 0. [para(602(a,1),145(a,1,2,1,2))]. given #670 (T,wt=10): 2935 c1 v (c2 ^ x) != 1 | c1 != 0 | c1' = c1 v (x ^ c2). [para(136(a,1),153(a,1,2)),rewrite(13(5),775(7),58(6),13(9),13(15),13(17),781(19),58(18),781(17))]. given #671 (A,wt=11): 253 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #672 (F,wt=10): 3410 c1 v (x ^ c2') != 1 | c2' ^ x = c1'. [para(4(a,1),167(a,1,2))]. given #673 (F,wt=10): 3442 c1 v (c2' ^ x) != 1 | x ^ c2' = c1'. [para(4(a,1),179(a,1,2))]. given #674 (T,wt=10): 3443 c2 ^ (x v c1') != 0 | c2' = c1' v x. [para(2(a,1),210(a,1,2))]. given #675 (T,wt=10): 3446 c2 ^ (c1' v x) != 0 | c2' = x v c1'. [para(2(a,1),214(a,1,2))]. given #676 (A,wt=15): 254 x v (y v ((x v y)' v z)) = 1. [para(31(a,1),3(a,1,1)),rewrite(57(2),3(5)),flip(a)]. given #677 (F,wt=10): 3935 c1 ^ (((c1 v x) ^ (c2 v y)) v z)' = 0. [para(3468(a,1),973(a,1,2)),rewrite(4(9))]. given #678 (F,wt=10): 4203 c1 ^ (((x v c1) ^ (c2 v y)) v z)' = 0. [para(3915(a,1),973(a,1,2)),rewrite(4(9))]. given #679 (T,wt=10): 4233 c1 ^ (((c1 v x) ^ (y v c2)) v z)' = 0. [para(3916(a,1),973(a,1,2)),rewrite(4(9))]. given #680 (T,wt=10): 4261 c1 ^ (x v ((c1 v y) ^ (c2 v z)))' = 0. [para(3917(a,1),973(a,1,2)),rewrite(4(9))]. given #681 (A,wt=19): 255 x v (y v (z v (x v (y v z))')) = 1. [para(31(a,1),3(a,1)),rewrite(3(3)),flip(a)]. given #682 (F,wt=10): 4288 c1 ^ (((c2 v x) ^ (c1 v y)) v z)' = 0. [para(3918(a,1),973(a,1,2)),rewrite(4(9))]. given #683 (F,wt=10): 4328 c2 != 1 | c1 v (c2 ^ x) != 0 | c2' = c1 v (x ^ c2). [para(142(a,1),173(b,1)),rewrite(4(5),13(5),781(7),17(6),26(5),117(3),4(7),13(7),775(9),4(14),13(14),4(16),13(16),781(18),58(17))]. given #684 (T,wt=10): 4343 c1 ^ (((c2 v x) ^ (c2 v y)) v z)' = 0. [para(3929(a,1),973(a,1,2)),rewrite(4(9))]. given #685 (T,wt=10): 4369 c1 ^ (((x v c2) ^ (c2 v y)) v z)' = 0. [para(3930(a,1),973(a,1,2)),rewrite(4(9))]. given #686 (A,wt=18): 256 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(31(a,1),10(a,1)),flip(c),xx(a)]. given #687 (F,wt=10): 4662 c1 ^ (((x v c1) ^ (y v c2)) v z)' = 0. [para(4186(a,1),973(a,1,2)),rewrite(4(9))]. given #688 (F,wt=10): 4693 c1 ^ (x v ((y v c1) ^ (c2 v z)))' = 0. [para(4187(a,1),973(a,1,2)),rewrite(4(9))]. given #689 (T,wt=10): 4723 c1 ^ (((c2 v x) ^ (y v c1)) v z)' = 0. [para(4189(a,1),973(a,1,2)),rewrite(4(9))]. given #690 (T,wt=10): 4756 (c1 ^ x) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(597(a,1),176(a,1,1)),rewrite(20(12)),flip(a)]. given #691 (A,wt=15): 257 x v (y v (z v (x v z)')) = 1. [para(31(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #692 (F,wt=10): 4758 (c1 ^ x) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(602(a,1),176(a,1,1)),rewrite(20(12)),flip(a)]. given #693 (F,wt=8): 9486 c1 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c1. [para(4758(a,1),153(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 #694 (T,wt=8): 9492 c1 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c1. [para(4(a,1),9486(b,1))]. given #695 (T,wt=8): 9494 c1 != 1 | x ^ c1 != 0 | (x ^ c1)' = c1. [para(73(a,1),9486(b,1)),rewrite(73(11))]. given #696 (A,wt=19): 258 x v (y v (z v (y v (x v z))')) = 1. [para(17(a,1),31(a,1,2,2,1)),rewrite(3(5))]. given #697 (F,wt=8): 9497 c1 != 1 | c1 ^ x != 0 | (x ^ c1)' = c1. [para(4(a,1),9494(b,1))]. given #698 (F,wt=10): 4782 c2 ^ c1' != 0 | (c2 ^ c1') v (c2 ^ (x v c1)) = c1. [back_rewrite(2941),rewrite(4740(17))]. given #699 (T,wt=10): 4783 c2 ^ c1' != 0 | (c2 ^ c1') v (c2 ^ (c1 v x)) = c1. [back_rewrite(2940),rewrite(4740(17))]. given #700 (T,wt=10): 5032 c1 ^ (x v ((c1 v y) ^ (z v c2)))' = 0. [para(4215(a,1),973(a,1,2)),rewrite(4(9))]. given #701 (A,wt=13): 259 x v (y v ((x ^ z) v y)') = 1. [para(31(a,1),24(a,1,2)),rewrite(65(2)),flip(a)]. given #702 (F,wt=10): 5062 c1 ^ (((x v c2) ^ (c1 v y)) v z)' = 0. [para(4217(a,1),973(a,1,2)),rewrite(4(9))]. given #703 (F,wt=10): 5089 c1 ^ (((c2 v x) ^ (y v c2)) v z)' = 0. [para(4227(a,1),973(a,1,2)),rewrite(4(9))]. given #704 (T,wt=10): 5118 c1 ^ (((x v c2) ^ (y v c2)) v z)' = 0. [para(4228(a,1),973(a,1,2)),rewrite(4(9))]. given #705 (T,wt=10): 5153 c1 ^ (x v ((c2 v y) ^ (c1 v z)))' = 0. [para(4246(a,1),973(a,1,2)),rewrite(4(9))]. given #706 (A,wt=11): 260 (c2 ^ x) v ((c1 ^ x)' v y) = 1. [para(229(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #707 (F,wt=10): 5185 c1 ^ (x v ((c2 v y) ^ (c2 v z)))' = 0. [para(4256(a,1),973(a,1,2)),rewrite(4(9))]. given #708 (F,wt=10): 5216 c1 ^ (x v ((y v c2) ^ (c2 v z)))' = 0. [para(4257(a,1),973(a,1,2)),rewrite(4(9))]. given #709 (T,wt=10): 5336 c1 ^ (x v ((y v c1) ^ (z v c2)))' = 0. [para(4646(a,1),973(a,1,2)),rewrite(4(9))]. given #710 (T,wt=10): 5367 c1 ^ (((x v c2) ^ (y v c1)) v z)' = 0. [para(4649(a,1),973(a,1,2)),rewrite(4(9))]. given #711 (A,wt=16): 264 c2 ^ (x ^ (c1 ^ x)') != 0 | (c2 ^ x)' = (c1 ^ x)'. [para(229(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #712 (F,wt=10): 5393 (x ^ c2) v (x ^ (c1 v (c2 ^ y)))' = 1. [para(775(a,1),184(a,1,2,1,2))]. given #713 (F,wt=10): 5394 (x ^ c2) v (x ^ (c1 v (y ^ c2)))' = 1. [para(781(a,1),184(a,1,2,1,2))]. given #714 (T,wt=10): 5414 c1 ^ (x v ((c2 v y) ^ (z v c1)))' = 0. [para(4679(a,1),973(a,1,2)),rewrite(4(9))]. given #715 (T,wt=10): 5444 c1 ^ (x v ((y v c2) ^ (c1 v z)))' = 0. [para(5018(a,1),973(a,1,2)),rewrite(4(9))]. given #716 (A,wt=19): 265 (c2 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c1 v x)))))) v (c1 ^ (x v (c1 ^ y)))' = 1. [para(12(a,1),229(a,1,2,1))]. given #717 (F,wt=10): 5476 c1 ^ (x v ((c2 v y) ^ (z v c2)))' = 0. [para(5027(a,1),973(a,1,2)),rewrite(4(9))]. given #718 (F,wt=10): 5508 c1 ^ (x v ((y v c2) ^ (z v c2)))' = 0. [para(5028(a,1),973(a,1,2)),rewrite(4(9))]. given #719 (T,wt=10): 5544 c1 ^ (x v ((y v c2) ^ (z v c1)))' = 0. [para(5323(a,1),973(a,1,2)),rewrite(4(9))]. given #720 (T,wt=10): 5603 (x v c2) ^ (y ^ c1) = y ^ c1. [para(69(a,1),241(a,2)),rewrite(819(8))]. given #721 (A,wt=11): 266 (c2 ^ x) v (y v (c1 ^ x)') = 1. [para(229(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #722 (F,wt=10): 5667 c1 v (x v c2)' != 1 | (c2 v x)' = c1'. [para(2(a,1),246(a,1,2,1))]. given #723 (F,wt=10): 5669 c1 v (c2 v x)' != 1 | (x v c2)' = c1'. [para(2(a,1),251(a,1,2,1))]. given #724 (T,wt=10): 5671 c2 ^ (x ^ c1)' != 0 | (c1 ^ x)' = c2'. [para(4(a,1),275(a,1,2,1))]. given #725 (T,wt=10): 5680 c2 ^ (c1 ^ x)' != 0 | (x ^ c1)' = c2'. [para(4(a,1),281(a,1,2,1))]. given #726 (A,wt=15): 267 (x ^ (c2 ^ y)) v (c1 ^ (x ^ y))' = 1. [para(19(a,1),229(a,1,1))]. given #727 (F,wt=10): 5883 c2 ^ (x v c1') != 0 | (c1' v x)' = c2. [para(2(a,1),332(a,1,2))]. given #728 (F,wt=10): 5887 c2 ^ (c1' v x) != 0 | (x v c1')' = c2. [para(2(a,1),333(a,1,2))]. given #729 (T,wt=10): 5889 (c2 v x) ^ c1' != 0 | (x v c2)' = c1'. [para(2(a,1),367(a,1,1))]. given #730 (T,wt=10): 5891 c1' ^ (x v c2) != 0 | (x v c2)' = c1'. [para(4(a,1),367(a,1))]. given #731 (A,wt=15): 268 (c2 ^ (x ^ y)) v (x ^ (c1 ^ y))' = 1. [para(19(a,1),229(a,1,2,1))]. given #732 (F,wt=10): 5913 (x v c2) ^ c1' != 0 | (c2 v x)' = c1'. [para(2(a,1),371(a,1,1))]. given #733 (F,wt=10): 5914 c1' ^ (c2 v x) != 0 | (c2 v x)' = c1'. [para(4(a,1),371(a,1))]. given #734 (T,wt=10): 5916 c1 v (x ^ c2') != 1 | (c2' ^ x)' = c1. [para(4(a,1),403(a,1,2))]. given #735 (T,wt=10): 5918 c1 v (c2' ^ x) != 1 | (x ^ c2')' = c1. [para(4(a,1),404(a,1,2))]. given #736 (A,wt=12): 270 (c2 ^ ((c1 v x) ^ y)) v (c1 ^ y)' = 1. [para(22(a,1),229(a,1,2,1))]. given #737 (F,wt=8): 10205 (c2 ^ (c1 v x)) v (c1 ^ y)' = 1. [para(270(a,1),171(a,1,2)),rewrite(2(6),57(6)),flip(a)]. given #738 (F,wt=8): 10236 (c1 ^ x)' v (c2 ^ (c1 v y)) = 1. [para(10205(a,1),2(a,1)),flip(a)]. given #739 (T,wt=8): 10237 (c2 ^ (x v c1)) v (c1 ^ y)' = 1. [para(2(a,1),10205(a,1,1,2))]. given #740 (T,wt=8): 10239 (c2 ^ (c1 v x)) v (y ^ c1)' = 1. [para(4(a,1),10205(a,1,2,1))]. given #741 (A,wt=14): 271 (c2 ^ (x ^ ((c1 ^ x) v y))) v (c1 ^ x)' = 1. [para(23(a,1),229(a,1,2,1))]. given #742 (F,wt=8): 10253 (c1 ^ x)' v (c2 ^ (y v c1)) = 1. [para(2(a,1),10236(a,1,2,2))]. given #743 (F,wt=8): 10254 (x ^ c1)' v (c2 ^ (c1 v y)) = 1. [para(4(a,1),10236(a,1,1,1))]. given #744 (T,wt=8): 10266 (c2 ^ (x v c1)) v (y ^ c1)' = 1. [para(4(a,1),10237(a,1,2,1))]. given #745 (T,wt=8): 10342 (x ^ c1)' v (c2 ^ (y v c1)) = 1. [para(4(a,1),10253(a,1,1,1))]. given #746 (A,wt=20): 276 c2 ^ ((c1 ^ x)' v (c2 ^ ((c2 ^ (c1 ^ x)') v y))) = c2 ^ ((c1 ^ x)' v (c2 ^ y)). [para(272(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12))]. given #747 (F,wt=10): 5919 c2' v (x ^ c1) != 1 | (x ^ c1)' = c2'. [para(2(a,1),453(a,1))]. given #748 (F,wt=10): 5920 (c1 ^ x) v c2' != 1 | (x ^ c1)' = c2'. [para(4(a,1),453(a,1,1))]. given #749 (T,wt=10): 6014 c2' v (c1 ^ x) != 1 | (c1 ^ x)' = c2'. [para(2(a,1),457(a,1))]. given #750 (T,wt=10): 6015 (x ^ c1) v c2' != 1 | (c1 ^ x)' = c2'. [para(4(a,1),457(a,1,1))]. given #751 (A,wt=20): 282 c2 ^ ((x ^ c1)' v (c2 ^ ((c2 ^ (x ^ c1)') v y))) = c2 ^ ((x ^ c1)' v (c2 ^ y)). [para(274(a,1),12(a,1,2,2,2,2,2)),rewrite(32(12))]. given #752 (F,wt=10): 6213 c2 ^ (x v c1) != 1 | c1 != 0 | c1' = c2 ^ (c1 v x). [para(2(a,1),832(a,1,2))]. given #753 (F,wt=10): 6216 c2 ^ (x v c1) != 1 | c1 != 0 | (c2 ^ (c1 v x))' = c1. [para(2(a,1),837(a,1,2))]. given #754 (T,wt=10): 6217 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (x ^ c2))' = c1. [para(12(a,1),837(a,1)),rewrite(775(6),4(15),13(15),2(16),117(16),781(17),58(16),781(15))]. given #755 (T,wt=10): 6219 c1 v (c2 ^ x) != 1 | c1 != 0 | (c1 v (c2 ^ x))' = c1. [para(44(a,1),837(a,1)),rewrite(775(6),4(15),13(15),2(16),117(16),775(17),58(16),775(15))]. given #756 (A,wt=14): 286 c2 ^ ((c1 v x) ^ c1') != 0 | (c2 ^ (c1 v x))' = c1'. [para(263(a,1),10(a,1)),rewrite(5(10)),xx(a)]. given #757 (F,wt=10): 6220 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (x ^ c2))' = c1. [para(781(a,1),837(a,1)),rewrite(781(15))]. given #758 (F,wt=10): 6435 c1 v (c2 ^ (x v c1))' != 1 | c2 ^ (c1 v x) = c1. [para(2(a,1),846(a,1,2,1,2))]. given #759 (T,wt=10): 6436 c1 v (c1 v (c2 ^ x))' != 1 | c1 v (x ^ c2) = c1. [para(12(a,1),846(a,1,2,1)),rewrite(775(7),4(15),13(15),2(16),117(16),781(17),58(16),781(15))]. given #760 (T,wt=10): 6510 (c2 ^ c1')' v (x ^ c1) = (c2 ^ c1')'. [para(6498(a,1),114(a,1,2,2))]. given #761 (A,wt=11): 289 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),34(a,1,2,2,1))]. given #762 (F,wt=10): 6522 (x ^ (c2 ^ c1')') v (x ^ c1)' = 1. [para(6498(a,1),195(a,1,2,1,2))]. given #763 (F,wt=10): 6566 (c2 ^ c1')' != 1 | c1 != 0 | (c2 ^ c1')' = c1'. [para(6504(a,1),10(b,1)),rewrite(6503(7)),flip(c)]. given #764 (T,wt=10): 6599 (x v c1) ^ (x v (c2 ^ c1')')' = 0. [para(6503(a,1),145(a,1,2,1,2))]. given #765 (T,wt=10): 6602 c1 ^ (((c2 ^ c1')' ^ (c2 v x)) v y) = c1. [para(6503(a,1),3468(a,1,2,1,1))]. given #766 (A,wt=15): 290 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(34(a,1),5(a,1,1)),rewrite(74(2),5(5)),flip(a)]. given #767 (F,wt=10): 6604 c1 ^ (((c2 ^ c1')' ^ (x v c2)) v y) = c1. [para(6503(a,1),3916(a,1,2,1,1))]. given #768 (F,wt=10): 6605 c1 ^ (x v ((c2 ^ c1')' ^ (c2 v y))) = c1. [para(6503(a,1),3917(a,1,2,2,1))]. given #769 (T,wt=10): 6606 c1 ^ (((c2 v x) ^ (c2 ^ c1')') v y) = c1. [para(6503(a,1),3918(a,1,2,1,2))]. given #770 (T,wt=10): 6608 (c1 ^ x) v (c2 ^ c1')' = (c2 ^ c1')'. [para(6503(a,1),176(a,1,1)),rewrite(20(14)),flip(a)]. given #771 (A,wt=19): 291 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(34(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #772 (F,wt=10): 6609 c1 ^ (x v ((c2 ^ c1')' ^ (y v c2))) = c1. [para(6503(a,1),4215(a,1,2,2,1))]. given #773 (F,wt=10): 6610 c1 ^ (((x v c2) ^ (c2 ^ c1')') v y) = c1. [para(6503(a,1),4217(a,1,2,1,2))]. given #774 (T,wt=10): 6611 c1 ^ (x v ((c2 v y) ^ (c2 ^ c1')')) = c1. [para(6503(a,1),4246(a,1,2,2,2))]. given #775 (T,wt=10): 6612 c1 ^ (x v ((y v c2) ^ (c2 ^ c1')')) = c1. [para(6503(a,1),5018(a,1,2,2,2))]. given #776 (A,wt=18): 292 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(34(a,1),10(b,1)),flip(c),xx(b)]. given #777 (F,wt=10): 6614 ((c2 ^ c1')' ^ x) v (c1 ^ x)' = 1. [para(6503(a,1),197(a,1,1,1))]. given #778 (F,wt=10): 6686 c1 v c2' != 1 | (c1 v c2') ^ (c1 v (c2 ^ x)) = c2. [para(1953(a,1),204(b,1)),rewrite(2(4),319(12),2(15),2146(21)),flip(c),xx(b)]. given #779 (T,wt=10): 6687 c1 v c2' != 1 | (c1 v c2') ^ (c1 v (x ^ c2)) = c2. [para(1963(a,1),204(b,1)),rewrite(2(4),319(12),2(15),2146(21)),flip(c),xx(b)]. given #780 (T,wt=10): 6965 c1' ^ (c2 ^ c1')' != 0 | (c2 ^ c1')' = c1. [para(6574(a,1),130(a,1)),rewrite(319(16),2(18),193(18),50(21)),flip(c),xx(a)]. given #781 (A,wt=15): 293 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(34(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #782 (F,wt=10): 7324 c2 v (((c2 ^ x) v (c1 ^ y)) ^ z)' = 1. [para(7195(a,1),794(a,1,2)),rewrite(2(9))]. given #783 (F,wt=10): 7365 c2 v (((c2 ^ x) v (y ^ c1)) ^ z)' = 1. [para(7199(a,1),794(a,1,2)),rewrite(2(9))]. given #784 (T,wt=10): 7416 c2 v (((c1 ^ x) v (c2 ^ y)) ^ z)' = 1. [para(7304(a,1),794(a,1,2)),rewrite(2(9))]. given #785 (T,wt=10): 7456 c2 v (((x ^ c2) v (c1 ^ y)) ^ z)' = 1. [para(7306(a,1),794(a,1,2)),rewrite(2(9))]. given #786 (A,wt=19): 294 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(19(a,1),34(a,1,2,2,1)),rewrite(5(5))]. given #787 (F,wt=10): 7494 c2 v (x ^ ((c2 ^ y) v (c1 ^ z)))' = 1. [para(7307(a,1),794(a,1,2)),rewrite(2(9))]. given #788 (F,wt=10): 7532 c2 v (((x ^ c1) v (c1 ^ y)) ^ z)' = 1. [para(7315(a,1),794(a,1,2)),rewrite(2(9))]. given #789 (T,wt=10): 7572 c2 v (((x ^ c1) v (c2 ^ y)) ^ z)' = 1. [para(7345(a,1),794(a,1,2)),rewrite(2(9))]. given #790 (T,wt=10): 7615 c2 v (((x ^ c2) v (y ^ c1)) ^ z)' = 1. [para(7347(a,1),794(a,1,2)),rewrite(2(9))]. given #791 (A,wt=13): 295 x ^ (y ^ ((x v z) ^ y)') = 0. [para(34(a,1),22(a,1,2)),rewrite(76(2)),flip(a)]. given #792 (F,wt=10): 7653 c2 v (x ^ ((c2 ^ y) v (z ^ c1)))' = 1. [para(7348(a,1),794(a,1,2)),rewrite(2(9))]. given #793 (F,wt=10): 7690 c2 v (((x ^ c1) v (y ^ c1)) ^ z)' = 1. [para(7356(a,1),794(a,1,2)),rewrite(2(9))]. given #794 (T,wt=10): 7729 c2 v (((c1 ^ x) v (y ^ c2)) ^ z)' = 1. [para(7398(a,1),794(a,1,2)),rewrite(2(9))]. given #795 (T,wt=10): 7787 c2 v (x ^ ((c1 ^ y) v (c2 ^ z)))' = 1. [para(7399(a,1),794(a,1,2)),rewrite(2(9))]. given #796 (A,wt=14): 300 c2 ^ ((x v c1) ^ c1') != 0 | (c2 ^ (x v c1))' = c1'. [para(269(a,1),10(a,1)),rewrite(5(10)),xx(a)]. given #797 (F,wt=10): 7821 c2 v (((c1 ^ x) v (y ^ c1)) ^ z)' = 1. [para(7407(a,1),794(a,1,2)),rewrite(2(9))]. given #798 (F,wt=10): 7860 c2 v (x ^ ((y ^ c2) v (c1 ^ z)))' = 1. [para(7440(a,1),794(a,1,2)),rewrite(2(9))]. given #799 (T,wt=10): 7898 c2 v (x ^ ((y ^ c1) v (c1 ^ z)))' = 1. [para(7486(a,1),794(a,1,2)),rewrite(2(9))]. given #800 (T,wt=10): 7953 c2 v (((c1 ^ x) v (c1 ^ y)) ^ z)' = 1. [para(7516(a,1),794(a,1,2)),rewrite(2(9))]. given #801 (A,wt=11): 310 (x ^ c2) v ((c1 ^ x)' v y) = 1. [para(261(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #802 (F,wt=10): 7992 c2 v (((x ^ c1) v (y ^ c2)) ^ z)' = 1. [para(7555(a,1),794(a,1,2)),rewrite(2(9))]. given #803 (F,wt=10): 8027 c2 v (x ^ ((y ^ c1) v (c2 ^ z)))' = 1. [para(7556(a,1),794(a,1,2)),rewrite(2(9))]. given #804 (T,wt=10): 8064 c2 v (x ^ ((y ^ c2) v (z ^ c1)))' = 1. [para(7599(a,1),794(a,1,2)),rewrite(2(9))]. given #805 (T,wt=10): 8147 c2 v (x ^ ((y ^ c1) v (z ^ c1)))' = 1. [para(7645(a,1),794(a,1,2)),rewrite(2(9))]. given #806 (A,wt=15): 312 (x ^ (y ^ c2)) v (c1 ^ (x ^ y))' = 1. [para(5(a,1),261(a,1,1))]. given #807 (F,wt=10): 8184 c2 v (x ^ ((c1 ^ y) v (z ^ c2)))' = 1. [para(7713(a,1),794(a,1,2)),rewrite(2(9))]. given #808 (F,wt=10): 8220 c2 v (x ^ ((c1 ^ y) v (z ^ c1)))' = 1. [para(7780(a,1),794(a,1,2)),rewrite(2(9))]. given #809 (T,wt=10): 8255 c2 v (x ^ ((c1 ^ y) v (c1 ^ z)))' = 1. [para(7881(a,1),794(a,1,2)),rewrite(2(9))]. given #810 (T,wt=10): 8363 c2 v (x ^ ((y ^ c1) v (z ^ c2)))' = 1. [para(7976(a,1),794(a,1,2)),rewrite(2(9))]. given #811 (A,wt=16): 313 x ^ (c2 ^ (c1 ^ x)') != 0 | (c1 ^ x)' = (x ^ c2)'. [para(261(a,1),10(a,1)),rewrite(5(9)),flip(c),xx(a)]. given #812 (F,wt=10): 8402 c1 v (c2 ^ (c1 v x))' != 1 | c2 ^ (x v c1) = c1. [para(2(a,1),852(a,1,2,1,2))]. given #813 (F,wt=10): 8406 x ^ ((x ^ c1) v (c1 ^ y)) = x ^ c1. [para(220(a,1),23(a,1,2)),rewrite(6970(7))]. given #814 (T,wt=10): 8428 x ^ ((c1 ^ x) v (c1 ^ y)) = x ^ c1. [para(220(a,1),152(a,1,2)),rewrite(4740(7))]. given #815 (T,wt=10): 8449 c2 ^ (c1 v x) != 1 | c1 != 0 | c1' = c2 ^ (x v c1). [para(2(a,1),916(a,1,2))]. given #816 (A,wt=11): 314 (x ^ c2) v (y v (c1 ^ x)') = 1. [para(261(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #817 (F,wt=10): 8451 c2 ^ (c1 v x) != 1 | c1 != 0 | (c2 ^ (x v c1))' = c1. [para(2(a,1),918(a,1,2))]. given #818 (F,wt=10): 8453 c2 != 1 | c1 v (x ^ c2) != 0 | c2' = c1 v (c2 ^ x). [para(4(a,1),1022(b,1,2))]. given #819 (T,wt=10): 8456 c2 != 1 | c1 v (x ^ c2) != 0 | (c1 v (c2 ^ x))' = c2. [para(4(a,1),1027(b,1,2))]. given #820 (T,wt=10): 8458 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (c1 v x))' = c2. [para(597(a,1),1027(b,1)),rewrite(597(15))]. given #821 (A,wt=20): 315 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),36(a,1))]. given #822 (F,wt=10): 8459 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (x v c1))' = c2. [para(602(a,1),1027(b,1)),rewrite(602(15))]. given #823 (F,wt=10): 8593 c2 ^ (c1 v (x ^ c2))' != 0 | c1 v (c2 ^ x) = c2. [para(4(a,1),1039(a,1,2,1,2))]. given #824 (T,wt=10): 8597 c1 ^ ((c2 ^ x) v (x ^ y)) = c1 ^ x. [para(12(a,1),227(a,1,2)),rewrite(6970(6))]. given #825 (T,wt=10): 8639 (c1 ^ ((c2 ^ x) v y)) v (c1 ^ x)' = 1. [para(227(a,1),195(a,1,2,1))]. given #826 (A,wt=12): 316 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),36(b,1))]. Low Water (keep): wt=25, part=1.00, limit=25 given #827 (F,wt=10): 8666 c2 ^ (c1 v (c2 ^ x))' != 0 | c1 v (x ^ c2) = c2. [para(4(a,1),1047(a,1,2,1,2))]. given #828 (F,wt=10): 8700 c2 != 1 | c1 v (c2 ^ x) != 0 | (c1 v (x ^ c2))' = c2. [para(4(a,1),1115(b,1,2))]. given #829 (T,wt=10): 8783 (c2 ^ (c1 v x))' ^ (y ^ c1) = 0. [para(836(a,1),231(a,1,1)),rewrite(53(10),836(15))]. given #830 (T,wt=10): 8784 (c2 ^ (x v c1))' ^ (y ^ c1) = 0. [para(841(a,1),231(a,1,1)),rewrite(53(10),841(15))]. given #831 (A,wt=20): 317 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),36(b,1))]. given #832 (F,wt=10): 8876 c1 v ((c2 ^ c1')' ^ (x ^ c2)) = c1. [para(6498(a,1),231(a,1,1)),rewrite(6498(17))]. given #833 (F,wt=10): 9012 (x v c2) ^ (c1 v (c2 ^ y)) = c1 v (c2 ^ y). [para(2(a,1),2173(a,1,1))]. given #834 (T,wt=10): 9013 (c1 v (c2 ^ x)) ^ (c2 v y) = c1 v (c2 ^ x). [para(2173(a,1),4(a,1)),flip(a)]. given #835 (T,wt=8): 12172 (c2 v x)' ^ (c1 v (c2 ^ y)) = 0. [para(9013(a,1),973(a,1,2))]. given #836 (A,wt=12): 318 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),36(a,1)),rewrite(4(4),81(4)),flip(a)]. given #837 (F,wt=8): 12183 (x v c2)' ^ (c1 v (c2 ^ y)) = 0. [para(2(a,1),12172(a,1,1,1))]. given #838 (F,wt=8): 12184 (c1 v (c2 ^ x)) ^ (c2 v y)' = 0. [para(12172(a,1),4(a,1)),flip(a)]. given #839 (T,wt=8): 12185 (c2 v x)' ^ (c1 v (y ^ c2)) = 0. [para(4(a,1),12172(a,1,2,2))]. given #840 (T,wt=8): 12212 (c1 v (c2 ^ x)) ^ (y v c2)' = 0. [para(12183(a,1),4(a,1)),flip(a)]. given #841 (A,wt=20): 320 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(17(a,1),36(a,1))]. given #842 (F,wt=8): 12213 (x v c2)' ^ (c1 v (y ^ c2)) = 0. [para(4(a,1),12183(a,1,2,2))]. given #843 (F,wt=8): 12227 (c1 v (x ^ c2)) ^ (c2 v y)' = 0. [para(4(a,1),12184(a,1,1,2))]. given #844 (T,wt=8): 12255 (c1 v (x ^ c2)) ^ (y v c2)' = 0. [para(4(a,1),12212(a,1,1,2))]. given #845 (T,wt=10): 9039 (x v c2) ^ (c1 v (y ^ c2)) = c1 v (y ^ c2). [para(2(a,1),2174(a,1,1))]. given #846 (A,wt=20): 321 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(19(a,1),36(b,1))]. given #847 (F,wt=10): 9040 (c1 v (x ^ c2)) ^ (c2 v y) = c1 v (x ^ c2). [para(2174(a,1),4(a,1)),flip(a)]. Low Water (keep): wt=24, part=0.97, limit=24 given #848 (F,wt=10): 9159 (c1 v x) ^ (x v (c2 ^ (c1 v y)))' = 0. [para(2(a,1),2542(a,1,1))]. given #849 (T,wt=10): 9160 (x v c1) ^ ((c2 ^ (c1 v y)) v x)' = 0. [para(2(a,1),2542(a,1,2,1))]. given #850 (T,wt=10): 9174 (c1 v x) ^ (x v (c2 ^ (y v c1)))' = 0. [para(2(a,1),2543(a,1,1))]. given #851 (A,wt=24): 322 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),121(4))]. given #852 (F,wt=10): 9175 (x v c1) ^ ((c2 ^ (y v c1)) v x)' = 0. [para(2(a,1),2543(a,1,2,1))]. given #853 (F,wt=10): 9415 (c2 ^ (c1 v x)) v (c1 ^ y) = c2 ^ (c1 v x). [para(4756(a,1),2(a,1)),flip(a)]. given #854 (T,wt=10): 9417 (x ^ c1) v (c2 ^ (c1 v y)) = c2 ^ (c1 v y). [para(4(a,1),4756(a,1,1))]. given #855 (T,wt=10): 9467 (c2 ^ (x v c1)) v (c1 ^ y) = c2 ^ (x v c1). [para(4758(a,1),2(a,1)),flip(a)]. given #856 (A,wt=12): 323 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(26(a,1),36(a,1)),rewrite(4(4),83(4)),flip(a)]. given #857 (F,wt=10): 9470 (x ^ c1) v (c2 ^ (y v c1)) = c2 ^ (y v c1). [para(4(a,1),4758(a,1,1))]. given #858 (F,wt=10): 9751 (c2 ^ x) v (x ^ (c1 v (c2 ^ y)))' = 1. [para(4(a,1),5393(a,1,1))]. given #859 (T,wt=10): 9752 (x ^ c2) v ((c1 v (c2 ^ y)) ^ x)' = 1. [para(4(a,1),5393(a,1,2,1))]. given #860 (T,wt=10): 9766 (c2 ^ x) v (x ^ (c1 v (y ^ c2)))' = 1. [para(4(a,1),5394(a,1,1))]. given #861 (A,wt=20): 327 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 #862 (F,wt=8): 12827 c1 v x != 1 | c1 != 0 | (c1 v x)' = c1. [para(13(a,1),327(b,1,2,1)),rewrite(6(8),13(10))]. given #863 (F,wt=8): 12834 c2 != 1 | c2 ^ x != 0 | (c2 ^ x)' = c2. [para(386(a,1),327(b,1,2)),rewrite(122(4),81(7),386(12))]. given #864 (T,wt=8): 12872 x v c1 != 1 | c1 != 0 | (c1 v x)' = c1. [para(2(a,1),12827(a,1))]. given #865 (T,wt=8): 12874 x v c1 != 1 | c1 != 0 | (x v c1)' = c1. [para(62(a,1),12827(a,1)),rewrite(62(12))]. given #866 (A,wt=12): 328 x ^ (x ^ y)' != 0 | x ^ y = x. [para(172(a,1),36(a,1)),rewrite(4(6),319(11)),xx(a)]. given #867 (F,wt=8): 12876 c2 != 1 | x ^ c2 != 0 | (c2 ^ x)' = c2. [para(4(a,1),12834(b,1))]. given #868 (F,wt=8): 12878 c2 != 1 | x ^ c2 != 0 | (x ^ c2)' = c2. [para(69(a,1),12834(b,1)),rewrite(69(12))]. given #869 (T,wt=8): 12881 c1 v x != 1 | c1 != 0 | (x v c1)' = c1. [para(2(a,1),12874(a,1))]. given #870 (T,wt=8): 12888 c2 != 1 | c2 ^ x != 0 | (x ^ c2)' = c2. [para(4(a,1),12878(b,1))]. given #871 (A,wt=12): 329 x ^ (y ^ x)' != 0 | y ^ x = x. [para(183(a,1),36(a,1)),rewrite(4(6),319(11)),xx(a)]. given #872 (F,wt=10): 9767 (x ^ c2) v ((c1 v (y ^ c2)) ^ x)' = 1. [para(4(a,1),5394(a,1,2,1))]. given #873 (F,wt=10): 10112 c1' ^ (c2 v x) != 0 | (x v c2)' = c1'. [para(4(a,1),5889(a,1))]. given #874 (T,wt=10): 10165 c1' ^ (x v c2) != 0 | (c2 v x)' = c1'. [para(4(a,1),5913(a,1))]. given #875 (T,wt=10): 10427 c2' v (c1 ^ x) != 1 | (x ^ c1)' = c2'. [para(4(a,1),5919(a,1,2))]. given #876 (A,wt=24): 331 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 #877 (F,wt=9): 12959 c1 v c2' != 1 | (c2 ^ (c1 v c2'))' = c2'. [para(496(a,1),331(b,1)),rewrite(2(4),2(14),4(16),597(17)),xx(b)]. given #878 (F,wt=10): 10429 c2' v (x ^ c1) != 1 | (c1 ^ x)' = c2'. [para(4(a,1),6014(a,1,2))]. given #879 (T,wt=10): 10480 c1 v (x ^ c2) != 1 | c1 != 0 | (c1 v (c2 ^ x))' = c1. [para(4(a,1),6219(a,1,2))]. given #880 (T,wt=10): 10485 (x ^ c1) v (c2 ^ c1')' = (c2 ^ c1')'. [para(6510(a,1),2(a,1)),flip(a)]. given #881 (A,wt=24): 334 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),234(7))]. given #882 (F,wt=10): 10487 (c2 ^ c1')' v (c1 ^ x) = (c2 ^ c1')'. [para(4(a,1),6510(a,1,2))]. given #883 (F,wt=10): 10528 (x ^ c1)' v (x ^ (c2 ^ c1')') = 1. [para(6522(a,1),2(a,1)),flip(a)]. given #884 (T,wt=10): 10530 ((c2 ^ c1')' ^ x) v (x ^ c1)' = 1. [para(4(a,1),6522(a,1,1))]. given #885 (T,wt=10): 10531 (x ^ (c2 ^ c1')') v (c1 ^ x)' = 1. [para(4(a,1),6522(a,1,2,1))]. given #886 (A,wt=18): 335 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 #887 (F,wt=10): 10544 (c1 v x) ^ (x v (c2 ^ c1')')' = 0. [para(2(a,1),6599(a,1,1))]. given #888 (F,wt=10): 10545 (x v c1) ^ ((c2 ^ c1')' v x)' = 0. [para(2(a,1),6599(a,1,2,1))]. given #889 (T,wt=10): 10925 (c1 ^ x)' v ((c2 ^ c1')' ^ x) = 1. [para(6614(a,1),2(a,1)),flip(a)]. given #890 (T,wt=10): 11454 x ^ ((c1 ^ y) v (x ^ c1)) = x ^ c1. [para(2(a,1),8406(a,1,2))]. given #891 (A,wt=14): 336 c2 ^ (x ^ (c1 ^ x)') != 0 | c2 ^ x = c1 ^ x. [para(229(a,1),36(a,1)),rewrite(4(9),5(9),319(15)),flip(c),xx(a)]. given #892 (F,wt=10): 11455 x ^ ((x ^ c1) v (y ^ c1)) = x ^ c1. [para(4(a,1),8406(a,1,2,2))]. given #893 (F,wt=10): 11478 x ^ ((c1 ^ y) v (c1 ^ x)) = x ^ c1. [para(2(a,1),8428(a,1,2))]. given #894 (T,wt=10): 11479 x ^ ((c1 ^ x) v (y ^ c1)) = x ^ c1. [para(4(a,1),8428(a,1,2,2))]. given #895 (T,wt=10): 11519 c2 != 1 | c2 ^ (x v c1) != 0 | (c2 ^ (c1 v x))' = c2. [para(2(a,1),8458(b,1,2))]. given #896 (A,wt=12): 339 c2 ^ (c1' ^ (c1 v x)) != 0 | c2 ^ (c1 v x) = c1. [para(263(a,1),36(a,1)),rewrite(19(10),319(15)),flip(c),xx(a)]. given #897 (F,wt=9): 13409 c2 ^ c1' != 0 | c1 v (c2 ^ (c1' v x)) = c1. [para(1246(a,1),339(a,1,2)),rewrite(81(6),775(15))]. given #898 (F,wt=9): 13410 c2 ^ c1' != 0 | c1 v (c2 ^ (x v c1')) = c1. [para(1250(a,1),339(a,1,2)),rewrite(81(6),775(15))]. given #899 (T,wt=10): 11703 c2 != 1 | c2 ^ (c1 v x) != 0 | (c2 ^ (x v c1))' = c2. [para(2(a,1),8459(b,1,2))]. given #900 (T,wt=10): 11705 c1 ^ ((x ^ y) v (c2 ^ x)) = c1 ^ x. [para(2(a,1),8597(a,1,2))]. given #901 (A,wt=12): 340 c2 ^ (c1' ^ (x v c1)) != 0 | c2 ^ (x v c1) = c1. [para(269(a,1),36(a,1)),rewrite(19(10),319(15)),flip(c),xx(a)]. given #902 (F,wt=10): 11706 c1 ^ ((x ^ c2) v (x ^ y)) = c1 ^ x. [para(4(a,1),8597(a,1,2,1))]. given #903 (F,wt=10): 11707 c1 ^ ((c2 ^ x) v (y ^ x)) = c1 ^ x. [para(4(a,1),8597(a,1,2,2))]. given #904 (T,wt=10): 11763 (c1 ^ x)' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(8639(a,1),2(a,1)),flip(a)]. given #905 (T,wt=10): 11764 (c1 ^ (x v (c2 ^ y))) v (c1 ^ y)' = 1. [para(2(a,1),8639(a,1,1,2))]. given #906 (A,wt=14): 341 x ^ (c2 ^ (c1 ^ x)') != 0 | c1 ^ x = x ^ c2. [para(261(a,1),36(a,1)),rewrite(4(9),5(9),319(15)),xx(a)]. given #907 (F,wt=8): 13678 c1 v ((x ^ c1) v (c1 ^ y))' = 1. [para(7486(a,1),11764(a,1,1,2)),rewrite(13(3),6970(8))]. given #908 (F,wt=8): 13702 c1 v ((x ^ c1) v (y ^ c1))' = 1. [para(4(a,1),13678(a,1,2,1,2))]. given #909 (T,wt=10): 11766 (c1 ^ ((x ^ c2) v y)) v (c1 ^ x)' = 1. [para(4(a,1),8639(a,1,1,2,1))]. given #910 (T,wt=10): 11767 (c1 ^ ((c2 ^ x) v y)) v (x ^ c1)' = 1. [para(4(a,1),8639(a,1,2,1))]. given #911 (A,wt=11): 342 (c2 ^ x) v ((x ^ c1)' v y) = 1. [para(262(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #912 (F,wt=10): 11778 (c1 ^ ((x ^ c2) v y)) v (x ^ c1)' = 1. [para(73(a,1),8639(a,1,2,1)),rewrite(83(5))]. given #913 (F,wt=10): 12147 (c1 v (c2 ^ x)) ^ (y v c2) = c1 v (c2 ^ x). [para(9012(a,1),4(a,1)),flip(a)]. given #914 (T,wt=10): 12425 (c1 v (x ^ c2)) ^ (y v c2) = c1 v (x ^ c2). [para(9039(a,1),4(a,1)),flip(a)]. given #915 (T,wt=10): 12554 (c1 v x) ^ ((c2 ^ (c1 v y)) v x)' = 0. [para(2(a,1),9159(a,1,2,1))]. given #916 (A,wt=15): 343 (c2 ^ (x ^ y)) v (x ^ (y ^ c1))' = 1. [para(5(a,1),262(a,1,2,1))]. given #917 (F,wt=10): 12606 (c1 v x) ^ ((c2 ^ (y v c1)) v x)' = 0. [para(2(a,1),9174(a,1,2,1))]. given #918 (F,wt=10): 12664 (c2 ^ (c1 v x)) v (y ^ c1) = c2 ^ (c1 v x). [para(4(a,1),9415(a,1,2))]. given #919 (T,wt=10): 12689 (c2 ^ (x v c1)) v (y ^ c1) = c2 ^ (x v c1). [para(4(a,1),9467(a,1,2))]. given #920 (T,wt=10): 12734 (c2 ^ x) v ((c1 v (c2 ^ y)) ^ x)' = 1. [para(4(a,1),9751(a,1,2,1))]. given #921 (A,wt=16): 344 c2 ^ (x ^ (x ^ c1)') != 0 | (c2 ^ x)' = (x ^ c1)'. [para(262(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #922 (F,wt=10): 12754 c1 v ((c2 ^ c1')' ^ (c1 v (c2 ^ x)))' = 1. [para(6498(a,1),9751(a,1,1))]. given #923 (F,wt=10): 12796 (c2 ^ x) v ((c1 v (y ^ c2)) ^ x)' = 1. [para(4(a,1),9766(a,1,2,1))]. given #924 (T,wt=10): 12816 c1 v ((c2 ^ c1')' ^ (c1 v (x ^ c2)))' = 1. [para(6498(a,1),9766(a,1,1))]. given #925 (T,wt=10): 12962 x v c2 != 1 | 0 != x | (c2 v x)' = x. [para(758(a,1),331(b,1,2,2)),rewrite(17(8),124(8),20(7),758(12),17(10),124(10)),flip(b)]. given #926 (A,wt=11): 345 (c2 ^ x) v (y v (x ^ c1)') = 1. [para(262(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #927 (F,wt=10): 13121 (c1 ^ x)' v (x ^ (c2 ^ c1')') = 1. [para(4(a,1),10528(a,1,1,1))]. given #928 (F,wt=10): 13122 (x ^ c1)' v ((c2 ^ c1')' ^ x) = 1. [para(4(a,1),10528(a,1,2))]. given #929 (T,wt=10): 13228 (c1 v x) ^ ((c2 ^ c1')' v x)' = 0. [para(2(a,1),10544(a,1,2,1))]. given #930 (T,wt=10): 13293 x ^ ((y ^ c1) v (x ^ c1)) = x ^ c1. [para(4(a,1),11454(a,1,2,1))]. given #931 (A,wt=14): 346 c2 ^ (x ^ (x ^ c1)') != 0 | c2 ^ x = x ^ c1. [para(262(a,1),36(a,1)),rewrite(4(9),5(9),319(15)),flip(c),xx(a)]. given #932 (F,wt=10): 13361 x ^ ((y ^ c1) v (c1 ^ x)) = x ^ c1. [para(4(a,1),11478(a,1,2,1))]. given #933 (F,wt=10): 13411 c1 ^ ((x ^ y) v (c2 ^ y)) = c1 ^ y. [para(4(a,1),11705(a,1,2,1))]. given #934 (T,wt=10): 13412 c1 ^ ((x ^ y) v (x ^ c2)) = c1 ^ x. [para(4(a,1),11705(a,1,2,2))]. given #935 (T,wt=10): 13454 c2 ^ c1' != 0 | c2 ^ (c1 v ((c2 v x) ^ c1')) = c1. [para(157(a,1),340(a,1)),rewrite(2(14))]. given #936 (A,wt=11): 347 (x ^ c2) v ((x ^ c1)' v y) = 1. [para(311(a,1),3(a,1,1)),rewrite(57(2)),flip(a)]. given #937 (F,wt=10): 13455 c1 ^ ((x ^ c2) v (y ^ x)) = c1 ^ x. [para(4(a,1),11706(a,1,2,2))]. given #938 (F,wt=10): 13563 (c1 ^ x)' v (c1 ^ (y v (c2 ^ x))) = 1. [para(2(a,1),11763(a,1,2,2))]. Low Water (keep): wt=23, part=0.89, limit=23 given #939 (T,wt=10): 13564 (x ^ c1)' v (c1 ^ ((c2 ^ x) v y)) = 1. [para(4(a,1),11763(a,1,1,1))]. given #940 (T,wt=10): 13565 (c1 ^ x)' v (c1 ^ ((x ^ c2) v y)) = 1. [para(4(a,1),11763(a,1,2,2,1))]. given #941 (A,wt=16): 348 x ^ (c2 ^ (x ^ c1)') != 0 | (x ^ c2)' = (x ^ c1)'. [para(311(a,1),10(a,1)),rewrite(5(9)),xx(a)]. given #942 (F,wt=9): 14296 (c1 ^ x)' v (c1 ^ (x v y)) = 1. [para(133(a,1),13565(a,1,2,2)),rewrite(4(7),46(8))]. given #943 (F,wt=9): 14302 (c1 ^ x)' v (c1 ^ (y v x)) = 1. [para(2(a,1),14296(a,1,2,2))]. given #944 (T,wt=9): 14304 (x ^ c1)' v (c1 ^ (x v y)) = 1. [para(4(a,1),14296(a,1,1,1))]. given #945 (T,wt=9): 14337 (x ^ c1)' v (c1 ^ (y v x)) = 1. [para(4(a,1),14302(a,1,1,1))]. given #946 (A,wt=11): 349 (x ^ c2) v (y v (x ^ c1)') = 1. [para(311(a,1),17(a,1,2)),rewrite(65(2)),flip(a)]. given #947 (F,wt=9): 14403 (c1 ^ (x v y)) v (y ^ c1)' = 1. [para(14337(a,1),2(a,1)),flip(a)]. given #948 (F,wt=10): 13572 (x ^ c1)' v (c1 ^ ((x ^ c2) v y)) = 1. [para(73(a,1),11763(a,1,1,1)),rewrite(83(8))]. given #949 (T,wt=10): 13581 (c1 ^ x)' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(81(a,1),11763(a,1,1,1)),rewrite(19(8),46(8))]. given #950 (T,wt=10): 13623 (c1 ^ (x v (y ^ c2))) v (c1 ^ y)' = 1. [para(4(a,1),11764(a,1,1,2,2))]. given #951 (A,wt=14): 350 x ^ (c2 ^ (x ^ c1)') != 0 | x ^ c2 = x ^ c1. [para(311(a,1),36(a,1)),rewrite(4(9),5(9),319(15)),flip(c),xx(a)]. given #952 (F,wt=10): 13624 (c1 ^ (x v (c2 ^ y))) v (y ^ c1)' = 1. [para(4(a,1),11764(a,1,2,1))]. given #953 (F,wt=10): 13632 (c1 ^ (x v (y ^ c2))) v (y ^ c1)' = 1. [para(73(a,1),11764(a,1,2,1)),rewrite(83(5))]. given #954 (T,wt=10): 13897 c1 v ((c1 v (c2 ^ x)) ^ (c2 ^ c1')')' = 1. [para(6498(a,1),12734(a,1,1))]. given #955 (T,wt=10): 13951 c1 v ((c1 v (x ^ c2)) ^ (c2 ^ c1')')' = 1. [para(6498(a,1),12796(a,1,1))]. given #956 (A,wt=20): 351 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 #957 (F,wt=10): 14081 c1 ^ ((x ^ y) v (y ^ c2)) = c1 ^ y. [para(4(a,1),13411(a,1,2,2))]. Low Water (keep): wt=22, part=0.87, limit=22 given #958 (F,wt=10): 14230 (x ^ c1)' v (c1 ^ (y v (c2 ^ x))) = 1. [para(4(a,1),13563(a,1,1,1))]. given #959 (T,wt=10): 14231 (c1 ^ x)' v (c1 ^ (y v (x ^ c2))) = 1. [para(4(a,1),13563(a,1,2,2,2))]. given #960 (T,wt=10): 14237 (x ^ c1)' v (c1 ^ (y v (x ^ c1))) = 1. [para(47(a,1),13563(a,1,2,2,2)),rewrite(83(4))]. given #961 (A,wt=20): 352 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z. [para(2(a,1),37(b,1,1))]. given #962 (F,wt=10): 14238 (x ^ c1)' v (c1 ^ (y v (x ^ c2))) = 1. [para(73(a,1),13563(a,1,1,1)),rewrite(83(8))]. given #963 (F,wt=10): 14247 (c1 ^ x)' v (c1 ^ (y v (c1 ^ x))) = 1. [para(81(a,1),13563(a,1,1,1)),rewrite(19(8),46(8))]. given #964 (T,wt=10): 14430 (x ^ c1)' v (c1 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),13581(a,1,1,1))]. given #965 (T,wt=10): 14431 (c1 ^ x)' v (c1 ^ ((x ^ c1) v y)) = 1. [para(4(a,1),13581(a,1,2,2,1))]. given #966 (A,wt=20): 353 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z. [para(4(a,1),37(b,1))]. given #967 (F,wt=10): 14706 (c1 ^ x)' v (c1 ^ (y v (x ^ c1))) = 1. [para(4(a,1),14237(a,1,1,1))]. given #968 (F,wt=10): 14707 (x ^ c1)' v (c1 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),14237(a,1,2,2,2))]. given #969 (T,wt=10): 14986 (c1 ^ (x v (y ^ c1))) v (c1 ^ y)' = 1. [para(14706(a,1),2(a,1)),flip(a)]. given #970 (T,wt=10): 14997 (c1 ^ (x v (c1 ^ y))) v (y ^ c1)' = 1. [para(14707(a,1),2(a,1)),flip(a)]. given #971 (A,wt=16): 354 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),37(a,1,2)),rewrite(19(6),87(6))]. given #972 (F,wt=11): 362 x v c2 != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(117(a,1),37(a,1,2)),rewrite(4(8))]. given #973 (F,wt=11): 388 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | c1' = x ^ c2. [para(73(a,1),10(b,1))]. given #974 (T,wt=11): 405 c1 v (c2 ^ x) != 1 | c1 ^ x != 0 | (c2 ^ x)' = c1. [para(46(a,1),38(b,1)),rewrite(2(4))]. given #975 (T,wt=11): 416 c1 v (x ^ c2) != 1 | x ^ c1 != 0 | (x ^ c2)' = c1. [para(73(a,1),38(b,1)),rewrite(2(4))]. given #976 (A,wt=14): 355 (x v y) ^ y' != 0 | (x v y)' = y'. [para(8(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #977 (F,wt=11): 423 x v c2 != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(125(a,1),10(a,1))]. given #978 (F,wt=11): 438 (x v c1) ^ ((x v c2)' ^ y) = 0. [para(426(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #979 (T,wt=11): 440 (x v c1) ^ (y ^ (x v c2)') = 0. [para(426(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #980 (T,wt=11): 465 c1 v (c2 ^ x) != 1 | x ^ c1 != 0 | (c2 ^ x)' = c1. [para(47(a,1),39(b,1)),rewrite(2(4))]. given #981 (A,wt=20): 358 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(17(a,1),37(a,1))]. given #982 (F,wt=11): 470 (c1 v x) ^ ((x v c2)' ^ y) = 0. [para(434(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #983 (F,wt=11): 473 (c1 v x) ^ (y ^ (x v c2)') = 0. [para(434(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #984 (T,wt=11): 478 (x v c1) ^ ((c2 v x)' ^ y) = 0. [para(435(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #985 (T,wt=11): 482 (x v c1) ^ (y ^ (c2 v x)') = 0. [para(435(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #986 (A,wt=16): 359 x v y != 1 | x v y != 0 | (x v y)' = x v y. [para(28(a,1),37(b,1)),rewrite(93(2),58(2))]. given #987 (F,wt=11): 526 (c1 v x) ^ ((c2 v x)' ^ y) = 0. [para(469(a,1),5(a,1,1)),rewrite(74(2)),flip(a)]. given #988 (F,wt=11): 528 (c1 v x) ^ (y ^ (c2 v x)') = 0. [para(469(a,1),19(a,1,2)),rewrite(76(2)),flip(a)]. given #989 (T,wt=11): 536 x v c2 != 1 | c2 ^ (c1 v x) != 0 | (c1 v x)' = c2. [para(126(a,1),37(a,1)),rewrite(4(8))]. given #990 (T,wt=11): 701 (x v y) ^ (y v x) = x v y. [para(62(a,1),21(a,1,2))]. given #991 (A,wt=12): 360 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 #992 (F,wt=11): 702 (x v (y ^ z)) ^ (x v y)' = 0. [para(62(a,1),144(a,1,2,1))]. given #993 (F,wt=10): 15319 (c1 v ((c2 v x) ^ y)) ^ (c2 v x)' = 0. [para(124(a,1),702(a,1,2,1))]. given #994 (T,wt=10): 15320 (c1 v ((x v c2) ^ y)) ^ (x v c2)' = 0. [para(126(a,1),702(a,1,2,1))]. given #995 (T,wt=10): 15323 (c2 v ((x v c1) ^ y)) ^ (c2 v x)' = 0. [para(421(a,1),702(a,1,2,1))]. given #996 (A,wt=12): 363 x v c2 != 1 | c1 ^ y != 0 | (x v c2)' = c1 ^ y. [para(120(a,1),37(a,1,2)),rewrite(19(9),241(9))]. given #997 (F,wt=10): 15357 (c1 v ((x v c2) ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),15319(a,1,1,2,1))]. given #998 (F,wt=10): 15358 (c1 v ((c2 v x) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15319(a,1,2,1))]. given #999 (T,wt=10): 15359 (c2 v x)' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(15319(a,1),4(a,1)),flip(a)]. given #1000 (T,wt=10): 15360 (c1 v (x ^ (c2 v y))) ^ (c2 v y)' = 0. [para(4(a,1),15319(a,1,1,2))]. given #1001 (A,wt=18): 365 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(172(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1002 (F,wt=10): 15377 (x v c2)' ^ (c1 v ((x v c2) ^ y)) = 0. [para(15320(a,1),4(a,1)),flip(a)]. given #1003 (F,wt=9): 15504 (x v c2)' ^ (c2 v (x ^ y)) = 0. [para(176(a,1),15377(a,1,2,2)),rewrite(2(7),124(8))]. given #1004 (T,wt=9): 15508 (x v c2)' ^ (c2 v (y ^ x)) = 0. [para(4(a,1),15504(a,1,2,2))]. given #1005 (T,wt=9): 15529 (c2 v x)' ^ (c2 v (y ^ x)) = 0. [para(2(a,1),15508(a,1,1,1))]. given #1006 (A,wt=18): 366 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(183(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1007 (F,wt=9): 15531 (c2 v (x ^ y)) ^ (y v c2)' = 0. [para(15508(a,1),4(a,1)),flip(a)]. given #1008 (F,wt=10): 15378 (c1 v (x ^ (y v c2))) ^ (y v c2)' = 0. [para(4(a,1),15320(a,1,1,2))]. given #1009 (T,wt=10): 15390 (c2 v ((c1 v x) ^ y)) ^ (c2 v x)' = 0. [para(2(a,1),15323(a,1,1,2,1))]. given #1010 (T,wt=10): 15391 (c2 v ((x v c1) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15323(a,1,2,1))]. given #1011 (A,wt=20): 368 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(25(a,1),37(a,1)),rewrite(81(7))]. given #1012 (F,wt=10): 15393 (c2 v x)' ^ (c2 v ((x v c1) ^ y)) = 0. [para(15323(a,1),4(a,1)),flip(a)]. given #1013 (F,wt=10): 15394 (c2 v (x ^ (y v c1))) ^ (c2 v y)' = 0. [para(4(a,1),15323(a,1,1,2))]. given #1014 (T,wt=8): 15705 c2 ^ ((x v c2) ^ (c2 v y))' = 0. [para(3930(a,1),15394(a,1,1,2)),rewrite(2(3),117(3),3256(8))]. given #1015 (T,wt=8): 15740 c2 ^ ((x v c2) ^ (y v c2))' = 0. [para(2(a,1),15705(a,1,2,1,2))]. given #1016 (A,wt=14): 369 (x v c2) ^ (c1' v y) != 0 | (x v c2)' = c1' v y. [para(199(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1017 (F,wt=10): 15445 (c2 v x)' ^ (c1 v ((x v c2) ^ y)) = 0. [para(15357(a,1),4(a,1)),flip(a)]. given #1018 (F,wt=10): 15446 (c1 v (x ^ (y v c2))) ^ (c2 v y)' = 0. [para(4(a,1),15357(a,1,1,2))]. given #1019 (T,wt=10): 15458 (x v c2)' ^ (c1 v ((c2 v x) ^ y)) = 0. [para(15358(a,1),4(a,1)),flip(a)]. given #1020 (T,wt=10): 15459 (c1 v (x ^ (c2 v y))) ^ (y v c2)' = 0. [para(4(a,1),15358(a,1,1,2))]. given #1021 (A,wt=14): 370 (x v c2) ^ (y v c1') != 0 | (x v c2)' = y v c1'. [para(202(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1022 (F,wt=10): 15470 (c2 v x)' ^ (c1 v (y ^ (c2 v x))) = 0. [para(4(a,1),15359(a,1,2,2))]. given #1023 (F,wt=10): 15501 (x v c2)' ^ (c1 v (y ^ (x v c2))) = 0. [para(4(a,1),15377(a,1,2,2))]. given #1024 (T,wt=10): 15570 (c2 v x)' ^ (c2 v (y ^ (c2 v x))) = 0. [para(58(a,1),15529(a,1,1,1))]. given #1025 (T,wt=10): 15572 (c2 v x)' ^ (c2 v (y ^ (x v c1))) = 0. [para(421(a,1),15529(a,1,1,1))]. given #1026 (A,wt=22): 372 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'. [para(31(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1027 (F,wt=10): 15574 (x v c2)' ^ (c2 v (y ^ (x v c2))) = 0. [para(93(a,1),15529(a,1,1,1))]. given #1028 (F,wt=10): 15614 (c2 v ((c1 v x) ^ y)) ^ (x v c2)' = 0. [para(2(a,1),15390(a,1,2,1))]. given #1029 (T,wt=10): 15615 (c2 v x)' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(15390(a,1),4(a,1)),flip(a)]. given #1030 (T,wt=10): 15616 (c2 v (x ^ (c1 v y))) ^ (c2 v y)' = 0. [para(4(a,1),15390(a,1,1,2))]. given #1031 (A,wt=18): 373 (x v (c2 ^ y)) ^ (c1 ^ y)' != 0 | (x v (c2 ^ y))' = (c1 ^ y)'. [para(229(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1032 (F,wt=10): 15633 (x v c2)' ^ (c2 v ((x v c1) ^ y)) = 0. [para(15391(a,1),4(a,1)),flip(a)]. given #1033 (F,wt=10): 15634 (c2 v (x ^ (y v c1))) ^ (y v c2)' = 0. [para(4(a,1),15391(a,1,1,2))]. given #1034 (T,wt=10): 15649 (c2 v x)' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(58(a,1),15393(a,1,1,1)),rewrite(2(8),124(8))]. given #1035 (T,wt=10): 15772 (c2 v x)' ^ (c1 v (y ^ (x v c2))) = 0. [para(4(a,1),15445(a,1,2,2))]. given #1036 (A,wt=14): 374 (x v c2) ^ (c1 ^ y)' != 0 | (x v c2)' = (c1 ^ y)'. [para(272(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1037 (F,wt=10): 15775 (c2 v x)' ^ (c2 v ((x v c2) ^ y)) = 0. [para(207(a,1),15445(a,1,2,2)),rewrite(124(10))]. given #1038 (F,wt=10): 15786 (x v c2)' ^ (c1 v (y ^ (c2 v x))) = 0. [para(4(a,1),15458(a,1,2,2))]. given #1039 (T,wt=10): 15817 (x v c2)' ^ (c2 v (y ^ (c2 v x))) = 0. [para(2(a,1),15570(a,1,1,1))]. given #1040 (T,wt=10): 15818 (c2 v x)' ^ (c2 v (y ^ (x v c2))) = 0. [para(2(a,1),15570(a,1,2,2,2))]. given #1041 (A,wt=14): 375 (x v c2) ^ (y ^ c1)' != 0 | (x v c2)' = (y ^ c1)'. [para(274(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1042 (F,wt=10): 15836 (x v c2)' ^ (c2 v (y ^ (x v c1))) = 0. [para(2(a,1),15572(a,1,1,1))]. given #1043 (F,wt=10): 15837 (c2 v x)' ^ (c2 v (y ^ (c1 v x))) = 0. [para(2(a,1),15572(a,1,2,2,2))]. given #1044 (T,wt=10): 15897 (x v c2)' ^ (c2 v ((c1 v x) ^ y)) = 0. [para(15614(a,1),4(a,1)),flip(a)]. given #1045 (T,wt=10): 15898 (c2 v (x ^ (c1 v y))) ^ (y v c2)' = 0. [para(4(a,1),15614(a,1,1,2))]. given #1046 (A,wt=16): 376 (x v (c2 ^ (c1 v y))) ^ c1' != 0 | (x v (c2 ^ (c1 v y)))' = c1'. [para(263(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1047 (F,wt=10): 15949 (x v c2)' ^ (c2 v ((c2 v x) ^ y)) = 0. [para(2(a,1),15649(a,1,1,1))]. given #1048 (F,wt=10): 15984 (c2 v (x ^ (c2 v y))) ^ (y v c2)' = 0. [para(15817(a,1),4(a,1)),flip(a)]. given #1049 (T,wt=10): 15998 (c2 v (x ^ (y v c2))) ^ (c2 v y)' = 0. [para(15818(a,1),4(a,1)),flip(a)]. given #1050 (T,wt=10): 16010 (x v c2)' ^ (c2 v (y ^ (c1 v x))) = 0. [para(2(a,1),15836(a,1,2,2,2))]. given #1051 (A,wt=16): 377 (x v (c2 ^ (y v c1))) ^ c1' != 0 | (x v (c2 ^ (y v c1)))' = c1'. [para(269(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1052 (F,wt=11): 714 c2 v x != 1 | c2 ^ (x v c1) != 0 | c2' = x v c1. [para(421(a,1),10(a,1))]. given #1053 (F,wt=11): 716 c2 v x != 1 | c2 ^ (x v c1) != 0 | (x v c1)' = c2. [para(421(a,1),36(a,1)),rewrite(4(8))]. given #1054 (T,wt=11): 745 c2 v x != 1 | c2 ^ (c1 v x) != 0 | c2' = c1 v x. [para(124(a,1),64(a,1))]. given #1055 (T,wt=11): 823 (x ^ (y v z)) v (x ^ y)' = 1. [para(69(a,1),183(a,1,2,1))]. given #1056 (A,wt=18): 378 c2 ^ ((x v c1') ^ (c1 v y)) != 0 | (x v c1')' = c2 ^ (c1 v y). [para(284(a,1),37(a,1,2)),rewrite(65(2),19(11)),xx(a)]. given #1057 (F,wt=10): 16143 (c2 ^ ((x ^ c1) v y)) v (x ^ c1)' = 1. [para(47(a,1),823(a,1,2,1))]. given #1058 (F,wt=10): 16187 (x ^ c1)' v (c2 ^ ((x ^ c1) v y)) = 1. [para(16143(a,1),2(a,1)),flip(a)]. given #1059 (T,wt=10): 16188 (c2 ^ (x v (y ^ c1))) v (y ^ c1)' = 1. [para(2(a,1),16143(a,1,1,2))]. given #1060 (T,wt=10): 16190 (c2 ^ ((c1 ^ x) v y)) v (x ^ c1)' = 1. [para(4(a,1),16143(a,1,1,2,1))]. given #1061 (A,wt=18): 379 c2 ^ ((x v c1') ^ (y v c1)) != 0 | (x v c1')' = c2 ^ (y v c1). [para(297(a,1),37(a,1,2)),rewrite(65(2),19(11)),xx(a)]. given #1062 (F,wt=10): 16191 (c2 ^ ((x ^ c1) v y)) v (c1 ^ x)' = 1. [para(4(a,1),16143(a,1,2,1))]. given #1063 (F,wt=10): 16202 (x ^ c1)' v (c2 ^ (y v (x ^ c1))) = 1. [para(2(a,1),16187(a,1,2,2))]. given #1064 (T,wt=10): 16203 (c1 ^ x)' v (c2 ^ ((x ^ c1) v y)) = 1. [para(4(a,1),16187(a,1,1,1))]. given #1065 (T,wt=10): 16204 (x ^ c1)' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),16187(a,1,2,2,1))]. given #1066 (A,wt=18): 380 (x v (y ^ c2)) ^ (c1 ^ y)' != 0 | (x v (y ^ c2))' = (c1 ^ y)'. [para(261(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1067 (F,wt=10): 16213 (c2 ^ (x v (c1 ^ y))) v (y ^ c1)' = 1. [para(4(a,1),16188(a,1,1,2,2))]. given #1068 (F,wt=10): 16214 (c2 ^ (x v (y ^ c1))) v (c1 ^ y)' = 1. [para(4(a,1),16188(a,1,2,1))]. given #1069 (T,wt=10): 16227 (c2 ^ ((c1 ^ x) v y)) v (c1 ^ x)' = 1. [para(4(a,1),16190(a,1,2,1))]. given #1070 (T,wt=10): 16252 (c1 ^ x)' v (c2 ^ (y v (x ^ c1))) = 1. [para(4(a,1),16202(a,1,1,1))]. given #1071 (A,wt=18): 381 (x v (c2 ^ y)) ^ (y ^ c1)' != 0 | (x v (c2 ^ y))' = (y ^ c1)'. [para(262(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1072 (F,wt=10): 16253 (x ^ c1)' v (c2 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),16202(a,1,2,2,2))]. given #1073 (F,wt=10): 16258 (c1 ^ x)' v (c2 ^ ((c1 ^ x) v y)) = 1. [para(4(a,1),16203(a,1,2,2,1))]. given #1074 (T,wt=10): 16274 (c2 ^ (x v (c1 ^ y))) v (c1 ^ y)' = 1. [para(4(a,1),16213(a,1,2,1))]. given #1075 (T,wt=10): 16308 (c1 ^ x)' v (c2 ^ (y v (c1 ^ x))) = 1. [para(4(a,1),16252(a,1,2,2,2))]. given #1076 (A,wt=18): 382 (x v (y ^ c2)) ^ (y ^ c1)' != 0 | (x v (y ^ c2))' = (y ^ c1)'. [para(311(a,1),37(a,1,2)),rewrite(65(2)),xx(a)]. given #1077 (F,wt=11): 824 (x ^ y) v (y ^ x) = x ^ y. [para(69(a,1),27(a,1,2))]. given #1078 (F,wt=11): 835 (x v c1) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(597(a,1),21(a,1,2,2))]. given #1079 (T,wt=11): 856 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),839(a,1,2))]. given #1080 (T,wt=11): 860 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),839(a,1,2,2,2))]. given #1081 (A,wt=16): 383 c2 ^ (x ^ (y ^ c1)) = c1 ^ (x ^ y). [para(5(a,1),47(a,1,2)),rewrite(4(8))]. given #1082 (F,wt=10): 16405 c1 ^ (x v (c2 ^ (y v (c2 ^ (c1 v z))))) = c1. [para(597(a,1),860(a,1,2,2,2,2))]. given #1083 (F,wt=10): 16406 c1 ^ (x v (c2 ^ (y v (c2 ^ (z v c1))))) = c1. [para(602(a,1),860(a,1,2,2,2,2))]. Low Water (keep): wt=21, part=0.79, limit=21 given #1084 (T,wt=10): 16418 c1 ^ (x v (c2 ^ (y v (c2 ^ c1')'))) = c1. [para(6503(a,1),860(a,1,2,2,2,2))]. given #1085 (T,wt=10): 16452 c1 ^ (x v (c2 ^ ((c2 ^ (c1 v y)) v z))) = c1. [para(2(a,1),16405(a,1,2,2,2))]. given #1086 (A,wt=12): 385 (x ^ c2) v (x ^ (y ^ c1)) = x ^ c2. [para(47(a,1),27(a,1,2,2))]. given #1087 (F,wt=10): 16453 c1 ^ ((c2 ^ (x v (c2 ^ (c1 v y)))) v z) = c1. [para(2(a,1),16405(a,1,2))]. given #1088 (F,wt=10): 16495 c1 ^ (x v (c2 ^ ((c2 ^ (y v c1)) v z))) = c1. [para(2(a,1),16406(a,1,2,2,2))]. given #1089 (T,wt=10): 16496 c1 ^ ((c2 ^ (x v (c2 ^ (y v c1)))) v z) = c1. [para(2(a,1),16406(a,1,2))]. given #1090 (T,wt=10): 16537 c1 ^ (x v (c2 ^ ((c2 ^ c1')' v y))) = c1. [para(2(a,1),16418(a,1,2,2,2))]. given #1091 (A,wt=16): 387 c1 ^ (x ^ (y ^ c2)) = c1 ^ (x ^ y). [para(5(a,1),73(a,1,2)),rewrite(4(8))]. given #1092 (F,wt=10): 16538 c1 ^ ((c2 ^ (x v (c2 ^ c1')')) v y) = c1. [para(2(a,1),16418(a,1,2))]. given #1093 (F,wt=10): 16570 c1 ^ ((c2 ^ ((c2 ^ (c1 v x)) v y)) v z) = c1. [para(2(a,1),16452(a,1,2))]. given #1094 (T,wt=10): 16660 c1 ^ ((c2 ^ ((c2 ^ (x v c1)) v y)) v z) = c1. [para(2(a,1),16495(a,1,2))]. given #1095 (T,wt=10): 16739 c1 ^ ((c2 ^ ((c2 ^ c1')' v x)) v y) = c1. [para(2(a,1),16537(a,1,2))]. given #1096 (A,wt=20): 389 c1 ^ ((x ^ c2) v (c1 ^ ((x ^ c1) v (y ^ (c1 v (x ^ c2)))))) = c1 ^ ((x ^ c2) v (c1 ^ y)). [para(73(a,1),12(a,1,2,2,2,1))]. given #1097 (F,wt=11): 878 c1 ^ (x v (c2 ^ (y v (z v c1)))) = c1. [para(3(a,1),854(a,1,2,2,2))]. given #1098 (F,wt=11): 879 c1 ^ (x v (y v (c2 ^ (z v c1)))) = c1. [para(3(a,1),854(a,1,2))]. given #1099 (T,wt=11): 894 c1 ^ ((c2 ^ (x v (c1 v y))) v z) = c1. [para(17(a,1),855(a,1,2,1,2))]. given #1100 (T,wt=11): 895 c1 ^ (x v ((c2 ^ (c1 v y)) v z)) = c1. [para(17(a,1),855(a,1,2))]. given #1101 (A,wt=20): 390 c1 ^ (x v (c1 ^ ((c1 ^ x) v (y ^ (c2 ^ (c1 v x)))))) = c1 ^ (x v (y ^ c1)). [para(73(a,1),12(a,2,2,2)),rewrite(5(9))]. given #1102 (F,wt=11): 901 c1 ^ ((c2 ^ (x v (y v c1))) v z) = c1. [para(3(a,1),877(a,1,2,1,2))]. given #1103 (F,wt=11): 904 c1 ^ (x v ((c2 ^ (y v c1)) v z)) = c1. [para(17(a,1),877(a,1,2))]. given #1104 (T,wt=11): 917 (x v c1) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(602(a,1),21(a,1,2,2))]. given #1105 (T,wt=11): 1026 (x ^ c2) v (x ^ (c1 v (c2 ^ y))) = x ^ c2. [para(775(a,1),27(a,1,2,2))]. given #1106 (A,wt=20): 393 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z. [para(5(a,1),38(b,1))]. given #1107 (F,wt=11): 1059 c2 v (x ^ (y ^ (c1 v (c2 ^ z)))) = c2. [para(5(a,1),1031(a,1,2))]. given #1108 (F,wt=11): 1061 c2 v (x ^ (c1 v (y ^ (c2 ^ z)))) = c2. [para(19(a,1),1031(a,1,2,2,2))]. Low Water (keep): wt=20, part=0.76, limit=20 given #1109 (T,wt=10): 17211 c2 v (x ^ (c1 v (y ^ (c1 v (c2 ^ z))))) = c2. [para(775(a,1),1061(a,1,2,2,2,2))]. given #1110 (T,wt=10): 17212 c2 v (x ^ (c1 v (y ^ (c1 v (z ^ c2))))) = c2. [para(781(a,1),1061(a,1,2,2,2,2))]. given #1111 (A,wt=12): 394 x v y != 1 | 0 != x | (x v y)' = x. [para(6(a,1),38(b,1)),rewrite(2(2),58(2)),flip(b)]. given #1112 (F,wt=10): 17232 c2 v (x ^ (c1 v ((c1 v (c2 ^ y)) ^ z))) = c2. [para(4(a,1),17211(a,1,2,2,2))]. given #1113 (F,wt=10): 17233 c2 v ((c1 v (x ^ (c1 v (c2 ^ y)))) ^ z) = c2. [para(4(a,1),17211(a,1,2))]. given #1114 (T,wt=10): 17261 c2 v (x ^ (c1 v ((c1 v (y ^ c2)) ^ z))) = c2. [para(4(a,1),17212(a,1,2,2,2))]. given #1115 (T,wt=10): 17262 c2 v ((c1 v (x ^ (c1 v (y ^ c2)))) ^ z) = c2. [para(4(a,1),17212(a,1,2))]. given #1116 (A,wt=20): 395 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z. [para(17(a,1),38(a,1))]. given #1117 (F,wt=10): 17290 c2 v ((c1 v ((c1 v (c2 ^ x)) ^ y)) ^ z) = c2. [para(4(a,1),17232(a,1,2))]. given #1118 (F,wt=10): 17344 c2 v ((c1 v ((c1 v (x ^ c2)) ^ y)) ^ z) = c2. [para(4(a,1),17261(a,1,2))]. given #1119 (T,wt=11): 1070 c2 v (x ^ (c1 v (y ^ (z ^ c2)))) = c2. [para(5(a,1),1057(a,1,2,2,2))]. given #1120 (T,wt=11): 1071 c2 v (x ^ (y ^ (c1 v (z ^ c2)))) = c2. [para(5(a,1),1057(a,1,2))]. given #1121 (A,wt=20): 396 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z. [para(19(a,1),38(b,1))]. given #1122 (F,wt=11): 1085 c2 v ((c1 v (x ^ (c2 ^ y))) ^ z) = c2. [para(19(a,1),1058(a,1,2,1,2))]. given #1123 (F,wt=11): 1086 c2 v (x ^ ((c1 v (c2 ^ y)) ^ z)) = c2. [para(19(a,1),1058(a,1,2))]. given #1124 (T,wt=11): 1093 c2 v ((c1 v (x ^ (y ^ c2))) ^ z) = c2. [para(5(a,1),1069(a,1,2,1,2))]. given #1125 (T,wt=11): 1096 c2 v (x ^ ((c1 v (y ^ c2)) ^ z)) = c2. [para(19(a,1),1069(a,1,2))]. given #1126 (A,wt=24): 397 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),121(4))]. given #1127 (F,wt=11): 1114 (x ^ c2) v (x ^ (c1 v (y ^ c2))) = x ^ c2. [para(781(a,1),27(a,1,2,2))]. given #1128 (F,wt=11): 1164 ((x v y) ^ z) v (y ^ z)' = 1. [para(87(a,1),183(a,1,2,1))]. given #1129 (T,wt=11): 1231 (x ^ (y v z)) v (x ^ z)' = 1. [para(91(a,1),183(a,1,2,1))]. given #1130 (T,wt=11): 1306 (c1 v x) ^ (x v (c2 ^ (c1 v y))) = x v c1. [para(597(a,1),102(a,1,2,2))]. given #1131 (A,wt=20): 398 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 #1132 (F,wt=11): 1308 (c1 v x) ^ (x v (c2 ^ (y v c1))) = x v c1. [para(602(a,1),102(a,1,2,2))]. given #1133 (F,wt=11): 1353 (x ^ y)' v (z v x) = 1. [para(172(a,1),103(a,1,1)),rewrite(50(6),172(7))]. given #1134 (T,wt=11): 1355 (x ^ y)' v (z v y) = 1. [para(183(a,1),103(a,1,1)),rewrite(50(6),183(7))]. given #1135 (T,wt=11): 1357 c1' v (x v (y v c2)) = 1. [para(199(a,1),103(a,1,1)),rewrite(3(7),50(8),199(11))]. given #1136 (A,wt=12): 399 x v (x v y)' != 1 | x v y = x. [para(129(a,1),38(b,1)),rewrite(2(3),319(11)),xx(b)]. given #1137 (F,wt=7): 18087 c1' v (c1' v c2')' != 1. [ur(399,b,15,a)]. given #1138 (F,wt=8): 18090 (c1' v (c1' v c2')')' != 0. [ur(2451,b,18087,a),rewrite(2(9))]. given #1139 (T,wt=11): 1360 (c1 ^ x)' v (y v (c2 ^ x)) = 1. [para(229(a,1),103(a,1,1)),rewrite(50(9),229(13))]. given #1140 (T,wt=11): 1363 (c1 ^ x)' v (y v (x ^ c2)) = 1. [para(261(a,1),103(a,1,1)),rewrite(50(9),261(13))]. given #1141 (A,wt=24): 400 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z))' = x. [para(23(a,1),38(b,1)),rewrite(2(4))]. given #1142 (F,wt=9): 18164 c2 ^ c1' != 0 | (c1 v (c2 ^ c1'))' = c1'. [para(297(a,1),400(a,1)),rewrite(4(7),4(14),2(16),775(17)),xx(a)]. given #1143 (F,wt=11): 1364 (x ^ c1)' v (y v (c2 ^ x)) = 1. [para(262(a,1),103(a,1,1)),rewrite(50(9),262(13))]. given #1144 (T,wt=11): 1365 (x ^ c1)' v (y v (x ^ c2)) = 1. [para(311(a,1),103(a,1,1)),rewrite(50(9),311(13))]. given #1145 (T,wt=11): 1383 c1' v (x v (c2 v y)) = 1. [para(1356(a,1),3(a,1,1)),rewrite(57(2),3(6)),flip(a)]. given #1146 (A,wt=12): 402 x v (y v x)' != 1 | y v x = x. [para(144(a,1),38(b,1)),rewrite(2(3),319(11)),xx(b)]. given #1147 (F,wt=11): 1414 (c1 v x) ^ (c2 v (x v y))' = 0. [para(434(a,1),104(a,1,2)),rewrite(4(4),74(4),2(6)),flip(a)]. given #1148 (F,wt=11): 1538 x v (c2 v (c1 v (x ^ y))') = 1. [para(559(a,1),24(a,1,2)),rewrite(65(2),2(5)),flip(a)]. given #1149 (T,wt=11): 1551 x ^ (c1 ^ (c2 ^ (x v y))') = 0. [para(668(a,1),22(a,1,2)),rewrite(76(2)),flip(a)]. given #1150 (T,wt=11): 1560 x ^ (c1 ^ (c2 ^ (y v x))') = 0. [para(668(a,1),87(a,1,2)),rewrite(76(2)),flip(a)]. given #1151 (A,wt=24): 406 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),234(7))]. given #1152 (F,wt=11): 1598 ((x ^ y) v z) ^ (y v z)' = 0. [para(112(a,1),144(a,1,2,1))]. given #1153 (F,wt=11): 1618 x v (c2 v (c1 v (y ^ x))') = 1. [para(559(a,1),112(a,1,2)),rewrite(65(2),2(5)),flip(a)]. given #1154 (T,wt=11): 1855 (x v (y ^ z)) ^ (x v z)' = 0. [para(118(a,1),144(a,1,2,1))]. given #1155 (T,wt=11): 2124 c1 ^ (x ^ (c2 ^ (x v y))') = 0. [para(296(a,1),132(a,1,2)),rewrite(76(2)),flip(a)]. given #1156 (A,wt=14): 411 c2 ^ (c1' ^ (c1 v x)) != 0 | (c2 ^ (c1 v x))' = c1'. [para(263(a,1),38(a,1)),rewrite(19(10)),xx(a)]. given #1157 (F,wt=11): 2246 c2 v (x v ((c1 ^ y) v x)') = 1. [para(31(a,1),134(a,1,2)),rewrite(2(3),57(3)),flip(a)]. given #1158 (F,wt=11): 2359 x v (c2 v (x v (c1 ^ y))') = 1. [para(137(a,1),794(a,1,2)),rewrite(2(7),3(7))]. given #1159 (T,wt=11): 2382 c2 v (x v ((y ^ c1) v x)') = 1. [para(31(a,1),139(a,1,2)),rewrite(2(3),57(3)),flip(a)]. given #1160 (T,wt=11): 2465 x v (c2 v (x v (y ^ c1))') = 1. [para(143(a,1),794(a,1,2)),rewrite(2(7),3(7))]. given #1161 (A,wt=18): 412 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x. [para(34(a,1),38(b,1)),rewrite(2(4)),xx(b)]. given #1162 (F,wt=11): 2490 ((c1 ^ x) v (y ^ (c1 v (c2 ^ z)))) ^ c2' = 0. [para(1031(a,1),2244(a,1,2,1))]. given #1163 (F,wt=11): 2491 ((c1 ^ x) v (y ^ (c1 v (z ^ c2)))) ^ c2' = 0. [para(1057(a,1),2244(a,1,2,1))]. given #1164 (T,wt=11): 2492 ((c1 ^ x) v ((c1 v (c2 ^ y)) ^ z)) ^ c2' = 0. [para(1058(a,1),2244(a,1,2,1))]. given #1165 (T,wt=11): 2493 ((c1 ^ x) v ((c1 v (y ^ c2)) ^ z)) ^ c2' = 0. [para(1069(a,1),2244(a,1,2,1))]. given #1166 (A,wt=14): 413 c2 ^ (c1' ^ (x v c1)) != 0 | (c2 ^ (x v c1))' = c1'. [para(269(a,1),38(a,1)),rewrite(19(10)),xx(a)]. given #1167 (F,wt=11): 2535 (x v c1) ^ (x v (c2 v y))' = 0. [para(124(a,1),145(a,1,2,1,2))]. given #1168 (F,wt=11): 2536 (x v c1) ^ (x v (y v c2))' = 0. [para(126(a,1),145(a,1,2,1,2))]. given #1169 (T,wt=11): 2537 (x v (c1 ^ y)) ^ (x v (c2 ^ y))' = 0. [para(224(a,1),145(a,1,2,1,2))]. given #1170 (T,wt=10): 18867 ((x ^ c1)' v (c2 ^ (y v x)))' = 0. [hyper(368,a,14337,a,b,2537,a),rewrite(14337(7),56(2),14337(8),50(11)),flip(a)]. given #1171 (A,wt=12): 414 c2 ^ ((c1 v x) ^ c1') != 0 | c2 ^ (c1 v x) = c1. [para(284(a,1),38(a,1)),rewrite(5(10),319(15)),flip(c),xx(a)]. given #1172 (F,wt=9): 18962 (c2 ^ (x v y)) v (y ^ c1)' = 1. [hyper(2451,a,18867,a)]. given #1173 (F,wt=9): 18963 (x ^ c1)' v (c2 ^ (y v x)) = 1. [hyper(2023,a,18867,a)]. given #1174 (T,wt=9): 18991 (c2 ^ (x v y)) v (x ^ c1)' = 1. [para(2(a,1),18962(a,1,1,2))]. Low Water (keep): wt=19, part=0.68, limit=19 given #1175 (T,wt=9): 18994 (c2 ^ (x v y)) v (c1 ^ y)' = 1. [para(4(a,1),18962(a,1,2,1))]. given #1176 (A,wt=12): 415 c2 ^ ((x v c1) ^ c1') != 0 | c2 ^ (x v c1) = c1. [para(297(a,1),38(a,1)),rewrite(5(10),319(15)),flip(c),xx(a)]. given #1177 (F,wt=9): 19024 (x ^ c1)' v (c2 ^ (x v y)) = 1. [para(2(a,1),18963(a,1,2,2))]. given #1178 (F,wt=9): 19026 (c1 ^ x)' v (c2 ^ (y v x)) = 1. [para(4(a,1),18963(a,1,1,1))]. given #1179 (T,wt=9): 19036 (c2 ^ (x v y)) v (c1 ^ x)' = 1. [para(4(a,1),18991(a,1,2,1))]. given #1180 (T,wt=9): 19140 (c1 ^ x)' v (c2 ^ (x v y)) = 1. [para(4(a,1),19024(a,1,1,1))]. given #1181 (A,wt=16): 418 c1 v (x v (c2 v y)) = x v (c2 v y). [para(124(a,1),17(a,1,2)),flip(a)]. given #1182 (F,wt=10): 19055 (c2 ^ (x v (c2 ^ y))) v (c1 ^ y)' = 1. [para(46(a,1),18994(a,1,2,1))]. given #1183 (F,wt=10): 19057 (c2 ^ (x v (y ^ c2))) v (y ^ c1)' = 1. [para(73(a,1),18994(a,1,2,1))]. given #1184 (T,wt=10): 19149 (c1 ^ x)' v (c2 ^ (y v (c2 ^ x))) = 1. [para(46(a,1),19026(a,1,1,1))]. given #1185 (T,wt=10): 19150 (x ^ c1)' v (c2 ^ (y v (x ^ c2))) = 1. [para(73(a,1),19026(a,1,1,1))]. given #1186 (A,wt=12): 419 (x v c1) ^ (x v (c2 v y)) = x v c1. [para(124(a,1),21(a,1,2,2))]. given #1187 (F,wt=10): 19225 (c2 ^ ((c2 ^ x) v y)) v (c1 ^ x)' = 1. [para(46(a,1),19036(a,1,2,1))]. given #1188 (F,wt=10): 19227 (c2 ^ ((x ^ c2) v y)) v (x ^ c1)' = 1. [para(73(a,1),19036(a,1,2,1))]. given #1189 (T,wt=10): 19258 (c1 ^ x)' v (c2 ^ ((c2 ^ x) v y)) = 1. [para(46(a,1),19140(a,1,1,1))]. given #1190 (T,wt=10): 19259 (x ^ c1)' v (c2 ^ ((x ^ c2) v y)) = 1. [para(73(a,1),19140(a,1,1,1))]. given #1191 (A,wt=19): 420 x v (c2 v y) != 1 | (x v c1) ^ (c2 v y) != 0 | (x v c1)' = c2 v y. [para(124(a,1),37(a,1,2))]. given #1192 (F,wt=10): 19304 (c2 ^ (x v (y ^ c2))) v (c1 ^ y)' = 1. [para(4(a,1),19055(a,1,1,2,2))]. given #1193 (F,wt=10): 19305 (c2 ^ (x v (c2 ^ y))) v (y ^ c1)' = 1. [para(4(a,1),19055(a,1,2,1))]. given #1194 (T,wt=10): 19388 (x ^ c1)' v (c2 ^ (y v (c2 ^ x))) = 1. [para(4(a,1),19149(a,1,1,1))]. given #1195 (T,wt=10): 19389 (c1 ^ x)' v (c2 ^ (y v (x ^ c2))) = 1. [para(4(a,1),19149(a,1,2,2,2))]. Low Water (keep): wt=18, part=0.66, limit=18 given #1196 (A,wt=16): 422 c2 v (x v (y v c1)) = c2 v (x v y). [para(3(a,1),125(a,1,2)),rewrite(2(8))]. given #1197 (F,wt=10): 19471 (c2 ^ ((x ^ c2) v y)) v (c1 ^ x)' = 1. [para(4(a,1),19225(a,1,1,2,1))]. given #1198 (F,wt=10): 19472 (c2 ^ ((c2 ^ x) v y)) v (x ^ c1)' = 1. [para(4(a,1),19225(a,1,2,1))]. given #1199 (T,wt=10): 19556 (x ^ c1)' v (c2 ^ ((c2 ^ x) v y)) = 1. [para(4(a,1),19258(a,1,1,1))]. given #1200 (T,wt=10): 19557 (c1 ^ x)' v (c2 ^ ((x ^ c2) v y)) = 1. [para(4(a,1),19258(a,1,2,2,1))]. given #1201 (A,wt=19): 430 x v (y v c2) != 1 | (x v c2) ^ (y v c1) != 0 | (x v c2)' = y v c1. [para(125(a,1),37(a,1,2))]. given #1202 (F,wt=11): 2538 (x v (y ^ c1)) ^ (x v (y ^ c2))' = 0. [para(391(a,1),145(a,1,2,1,2))]. given #1203 (F,wt=11): 2540 (x v (y ^ c1)) ^ (x v (c2 ^ y))' = 0. [para(595(a,1),145(a,1,2,1,2))]. given #1204 (T,wt=11): 2651 c1 ^ (x ^ ((c2 ^ x) v y)') = 0. [para(147(a,1),46(a,1,2)),rewrite(4(3),74(3)),flip(a)]. given #1205 (T,wt=11): 2689 c2' ^ (x ^ (c1 ^ y)) = 0. [para(2682(a,1),5(a,1,1)),rewrite(74(2),5(6)),flip(a)]. given #1206 (A,wt=17): 432 x v (c2 v y) != 1 | c2 ^ (x v y) != 0 | (x v y)' = c2. [para(125(a,2),37(a,1,2)),rewrite(421(4),4(8))]. given #1207 (F,wt=11): 2690 c2' ^ (x ^ (y ^ c1)) = 0. [para(5(a,1),2682(a,1,2))]. given #1208 (F,wt=11): 2731 c1 ^ (x ^ (y v (c2 ^ x))') = 0. [para(224(a,1),149(a,1,2,1,2)),rewrite(5(7))]. given #1209 (T,wt=11): 2732 x ^ (c1 ^ (y v (x ^ c2))') = 0. [para(391(a,1),149(a,1,2,1,2)),rewrite(5(7))]. given #1210 (T,wt=11): 2733 x ^ (c1 ^ (y v (c2 ^ x))') = 0. [para(595(a,1),149(a,1,2,1,2)),rewrite(5(7))]. given #1211 (A,wt=15): 436 (x v (y v c1)) ^ (c2 v (x v y))' = 0. [para(3(a,1),426(a,1,1)),rewrite(2(6))]. given #1212 (F,wt=11): 2871 ((x ^ c1) v (y ^ (c1 v (c2 ^ z)))) ^ c2' = 0. [para(1031(a,1),2380(a,1,2,1))]. given #1213 (F,wt=11): 2872 ((x ^ c1) v (y ^ (c1 v (z ^ c2)))) ^ c2' = 0. [para(1057(a,1),2380(a,1,2,1))]. given #1214 (T,wt=11): 2873 ((x ^ c1) v ((c1 v (c2 ^ y)) ^ z)) ^ c2' = 0. [para(1058(a,1),2380(a,1,2,1))]. given #1215 (T,wt=11): 2874 ((x ^ c1) v ((c1 v (y ^ c2)) ^ z)) ^ c2' = 0. [para(1069(a,1),2380(a,1,2,1))]. given #1216 (A,wt=15): 437 (c1 v (x v y)) ^ (x v (y v c2))' = 0. [para(3(a,1),426(a,1,2,1)),rewrite(2(3))]. given #1217 (F,wt=11): 3004 ((x ^ (c1 v (c2 ^ y))) v (c1 ^ z)) ^ c2' = 0. [para(1031(a,1),2467(a,1,2,1))]. given #1218 (F,wt=11): 3005 ((x ^ (c1 v (y ^ c2))) v (c1 ^ z)) ^ c2' = 0. [para(1057(a,1),2467(a,1,2,1))]. given #1219 (T,wt=11): 3006 (((c1 v (c2 ^ x)) ^ y) v (c1 ^ z)) ^ c2' = 0. [para(1058(a,1),2467(a,1,2,1))]. given #1220 (T,wt=11): 3007 (((c1 v (x ^ c2)) ^ y) v (c1 ^ z)) ^ c2' = 0. [para(1069(a,1),2467(a,1,2,1))]. given #1221 (A,wt=16): 439 x v (c1 v (x v c2)') != 1 | (x v c2)' = (x v c1)'. [para(426(