============================== Prover9 =============================== Prover9 (32) version September-2006, September 2006. Process 26878 was started by mccune on cleo.thornwood, Wed Sep 13 14:38:40 2006 The command was "/home/mccune/LADR/bin/prover9 -f lt.in uc.in H65d.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 H65d.in formulas(sos). x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). end_of_list. formulas(goals). x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v y = y v x. [assumption]. (x v y) v z = x v (y v z). [assumption]. x ^ y = y ^ x. [assumption]. (x ^ y) ^ z = x ^ (y ^ z). [assumption]. x ^ (x v y) = x. [assumption]. x v (x ^ y) = x. [assumption]. x v x' = 1. [assumption]. x ^ x' = 0. [assumption]. x v y != 1 | x ^ y != 0 | x' = y. [assumption]. x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). [assumption]. (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [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, c3, ^, v, ' ]). After inverse_order: Function symbol precedence: lex([ 0, 1, c1, c2, c3, ^, 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 ^ u)))) = x ^ (y v (z ^ u)). [copy(11),flip(a)]. 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [deny(1)]. 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 ^ u)))) = x ^ (y v (z ^ u)). [copy(11),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 x v y = y v x. [assumption]. given #2 (I,wt=11): 3 (x v y) v z = x v (y v z). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 14 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 16 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=6): 8 x v x' = 1. [assumption]. given #8 (I,wt=6): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=14): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=21): 12 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)). [copy(11),flip(a)]. given #11 (I,wt=13): 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [deny(1)]. given #12 (F,wt=5): 26 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #13 (F,wt=5): 27 x v x = x. [para(6(a,1),7(a,1,2))]. given #14 (T,wt=5): 30 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #15 (T,wt=5): 33 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #16 (A,wt=11): 15 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #17 (F,wt=5): 62 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. given #18 (F,wt=4): 72 1' = 0. [hyper(10,a,33,a,b,62,a)]. given #19 (T,wt=5): 64 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. given #20 (T,wt=4): 75 0' = 1. [hyper(10,a,64,a,b,30,a)]. given #21 (A,wt=11): 17 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #22 (F,wt=5): 73 1 v x = 1. [para(62(a,1),6(a,1))]. given #23 (F,wt=5): 76 0 ^ x = 0. [para(64(a,1),6(a,1,2))]. given #24 (T,wt=5): 82 x v 1 = 1. [para(73(a,1),2(a,1)),flip(a)]. given #25 (T,wt=5): 85 x ^ 0 = 0. [para(76(a,1),4(a,1)),flip(a)]. given #26 (A,wt=7): 18 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #27 (F,wt=7): 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #28 (F,wt=7): 84 0 != x | x' = 1. [back_rewrite(63),rewrite(82(2)),xx(a)]. given #29 (T,wt=7): 87 1 != x | x' = 0. [back_rewrite(65),rewrite(85(4)),xx(b)]. given #30 (T,wt=8): 74 x v (x' v y) = 1. [back_rewrite(28),rewrite(73(5))]. given #31 (A,wt=13): 19 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #32 (F,wt=8): 77 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite(76(5))]. given #33 (F,wt=8): 83 x v (y v x') = 1. [back_rewrite(69),rewrite(82(5))]. given #34 (T,wt=8): 86 x ^ (y ^ x') = 0. [back_rewrite(80),rewrite(85(5))]. given #35 (T,wt=9): 52 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. given #36 (A,wt=11): 20 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #37 (F,wt=8): 125 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #38 (F,wt=8): 132 x ^ (y v x)' = 0. [para(2(a,1),125(a,1,2,1))]. given #39 (T,wt=9): 54 x ^ (y ^ x) = y ^ x. [para(26(a,1),5(a,2,2)),rewrite(4(2))]. given #40 (T,wt=9): 58 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. given #41 (A,wt=13): 21 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #42 (F,wt=9): 60 x v (y v x) = y v x. [para(27(a,1),3(a,2,2)),rewrite(2(2))]. given #43 (F,wt=9): 67 x ^ (y v (x v z)) = x. [para(15(a,1),6(a,1,2))]. given #44 (T,wt=9): 79 x v (y ^ (x ^ z)) = x. [para(17(a,1),7(a,1,2))]. given #45 (T,wt=9): 88 x ^ (y v (z v x)) = x. [para(3(a,1),18(a,1,2))]. given #46 (A,wt=11): 22 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #47 (F,wt=8): 176 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #48 (F,wt=8): 186 x v (y ^ x)' = 1. [para(4(a,1),176(a,1,2,1))]. given #49 (T,wt=9): 96 x v (y ^ (z ^ x)) = x. [para(5(a,1),24(a,1,2))]. given #50 (T,wt=10): 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #51 (A,wt=13): 23 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #52 (F,wt=10): 32 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #53 (F,wt=10): 55 1 != x | 0 != x | x' = x. [para(26(a,1),10(b,1)),rewrite(27(1)),flip(a),flip(b)]. given #54 (T,wt=10): 102 x v (y v (x' v z)) = 1. [para(74(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #55 (T,wt=10): 115 x ^ (y ^ (x' ^ z)) = 0. [para(77(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #56 (A,wt=13): 25 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #57 (F,wt=10): 117 x v (y v (z v x')) = 1. [para(3(a,1),83(a,1,2))]. given #58 (F,wt=10): 120 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),86(a,1,2))]. given #59 (T,wt=10): 130 x ^ ((x v y)' ^ z) = 0. [para(77(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #60 (T,wt=10): 131 x ^ (y ^ (x v z)') = 0. [para(86(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #61 (A,wt=14): 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #62 (F,wt=5): 265 x'' = x. [para(8(a,1),34(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #63 (F,wt=8): 283 x' v (y v x) = 1. [para(265(a,1),83(a,1,2,2))]. given #64 (T,wt=8): 284 x' ^ (y ^ x) = 0. [para(265(a,1),86(a,1,2,2))]. given #65 (T,wt=10): 136 x ^ (y v (x v z))' = 0. [para(15(a,1),125(a,1,2,1))]. given #66 (A,wt=20): 35 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #67 (F,wt=10): 137 x ^ (y v (z v x))' = 0. [para(3(a,1),132(a,1,2,1))]. given #68 (F,wt=10): 138 x ^ ((y v x)' ^ z) = 0. [para(132(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #69 (T,wt=10): 142 x ^ (y ^ (z v x)') = 0. [para(132(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #70 (T,wt=10): 180 x v ((x ^ y)' v z) = 1. [para(74(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #71 (A,wt=14): 36 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #72 (F,wt=10): 181 x v (y v (x ^ z)') = 1. [para(83(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #73 (F,wt=10): 189 x v (y ^ (x ^ z))' = 1. [para(17(a,1),176(a,1,2,1))]. given #74 (T,wt=10): 190 x v ((y ^ x)' v z) = 1. [para(186(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #75 (T,wt=10): 192 x v (y ^ (z ^ x))' = 1. [para(5(a,1),186(a,1,2,1))]. given #76 (A,wt=20): 37 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #77 (F,wt=10): 194 x v (y v (z ^ x)') = 1. [para(186(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #78 (F,wt=10): 207 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. given #79 (T,wt=10): 222 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),32(a,1,2,2,1))]. given #80 (T,wt=10): 285 x' v (y v (x v z)) = 1. [para(265(a,1),102(a,1,2,2,1))]. given #81 (A,wt=21): 40 x ^ (y v (x ^ ((z ^ u) v (x ^ y)))) = x ^ (y v (z ^ u)). [para(2(a,1),12(a,1,2,2,2))]. given #82 (F,wt=10): 286 x' ^ (y ^ (x ^ z)) = 0. [para(265(a,1),115(a,1,2,2,1))]. given #83 (F,wt=10): 287 x' v (y v (z v x)) = 1. [para(265(a,1),117(a,1,2,2,2))]. given #84 (T,wt=10): 288 x' ^ (y ^ (z ^ x)) = 0. [para(265(a,1),120(a,1,2,2,2))]. given #85 (T,wt=10): 579 (x ^ y)' v (z v x) = 1. [para(7(a,1),287(a,1,2,2))]. given #86 (A,wt=27): 41 x ^ (y v (z v (x ^ ((x ^ (y v z)) v (u ^ v))))) = x ^ (y v (z v (u ^ v))). [para(3(a,1),12(a,1,2)),rewrite(3(11))]. given #87 (F,wt=10): 582 (x ^ y)' v (z v y) = 1. [para(24(a,1),287(a,1,2,2))]. given #88 (F,wt=10): 593 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),288(a,1,2,2))]. given #89 (T,wt=10): 596 (x v y)' ^ (z ^ y) = 0. [para(18(a,1),288(a,1,2,2))]. given #90 (T,wt=11): 68 x v (y v (x ^ z)) = y v x. [para(7(a,1),15(a,1,2)),flip(a)]. given #91 (A,wt=21): 42 x ^ (y v (x ^ ((y ^ x) v (z ^ u)))) = x ^ (y v (z ^ u)). [para(4(a,1),12(a,1,2,2,2,1))]. given #92 (F,wt=11): 78 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. given #93 (F,wt=11): 89 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. given #94 (T,wt=11): 93 x ^ (y ^ (z v x)) = y ^ x. [para(18(a,1),17(a,1,2)),flip(a)]. given #95 (T,wt=11): 94 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. given #96 (A,wt=25): 43 x ^ ((y v (x ^ ((x ^ y) v (z ^ u)))) ^ v) = x ^ ((y v (z ^ u)) ^ v). [para(12(a,1),5(a,1,1)),rewrite(5(4)),flip(a)]. given #97 (F,wt=11): 98 x v (y v (z ^ x)) = y v x. [para(24(a,1),15(a,1,2)),flip(a)]. given #98 (F,wt=11): 145 (x v y) ^ (z ^ x) = z ^ x. [para(54(a,1),20(a,2)),rewrite(144(4))]. given #99 (T,wt=11): 157 (x v y) ^ (y v x) = x v y. [para(60(a,1),19(a,1,2))]. given #100 (T,wt=10): 965 (x v y) ^ (y v x)' = 0. [para(157(a,1),284(a,1,2)),rewrite(4(4))]. given #101 (A,wt=29): 44 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (y ^ z)) v (u ^ v)))))) = x ^ (y ^ (z v (u ^ v))). [para(12(a,1),5(a,1)),rewrite(5(4),5(7),5(10)),flip(a)]. given #102 (F,wt=11): 159 x ^ (y v (z v (x v u))) = x. [para(3(a,1),67(a,1,2))]. given #103 (F,wt=11): 165 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),79(a,1,2))]. given #104 (T,wt=11): 168 x ^ (y v (z v (u v x))) = x. [para(3(a,1),88(a,1,2,2))]. given #105 (T,wt=11): 183 (x ^ y) v (z v x) = z v x. [para(60(a,1),22(a,2)),rewrite(156(4))]. given #106 (A,wt=17): 45 x ^ (y v (x ^ ((x ^ y) v z))) = x ^ (y v z). [para(6(a,1),12(a,1,2,2,2,2)),rewrite(6(7))]. given #107 (F,wt=11): 200 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),96(a,1,2,2))]. given #108 (F,wt=11): 243 (x ^ y) v (y ^ x) = x ^ y. [para(54(a,1),25(a,1,2))]. given #109 (T,wt=10): 1212 (x ^ y) v (y ^ x)' = 1. [para(243(a,1),283(a,1,2)),rewrite(2(4))]. given #110 (T,wt=11): 307 x v y != 0 | (x v y)' = 1. [para(30(a,1),35(b,1)),rewrite(82(2),82(2)),xx(a)]. given #111 (A,wt=14): 57 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(39),rewrite(52(4))]. given #112 (F,wt=7): 1232 x' != 1 | 0 = x. [para(284(a,1),57(b,1)),rewrite(265(8),284(9)),flip(a),flip(c),xx(b)]. given #113 (F,wt=11): 308 x v y != 1 | (x v y)' = 0. [para(33(a,1),35(a,1,2)),rewrite(4(6),76(6)),xx(b)]. given #114 (T,wt=11): 439 x ^ y != 0 | (x ^ y)' = 1. [para(30(a,1),37(b,1,2)),rewrite(2(3),73(3)),xx(a)]. given #115 (T,wt=11): 440 x ^ y != 1 | (x ^ y)' = 0. [para(33(a,1),37(a,1)),rewrite(85(5),85(5)),xx(b)]. given #116 (A,wt=14): 61 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(38),rewrite(58(2))]. given #117 (F,wt=7): 1242 x' != 0 | 1 = x. [para(283(a,1),61(a,1)),rewrite(265(8),283(9)),flip(b),flip(c),xx(a)]. given #118 (F,wt=11): 761 (x v y) ^ (z ^ y) = z ^ y. [para(54(a,1),89(a,2)),rewrite(144(4))]. given #119 (T,wt=11): 814 (x ^ y) v (z v y) = z v y. [para(60(a,1),94(a,2)),rewrite(156(4))]. given #120 (T,wt=11): 1228 x v y != 0 | (y v x)' = 1. [para(2(a,1),307(a,1))]. given #121 (A,wt=20): 70 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(15(a,1),10(a,1))]. given #122 (F,wt=11): 1233 (x v y)' != 1 | x v y = 0. [para(593(a,1),57(b,1)),rewrite(265(10),593(12)),flip(a),xx(b)]. given #123 (F,wt=11): 1234 x v y != 1 | (y v x)' = 0. [para(2(a,1),308(a,1))]. given #124 (T,wt=11): 1236 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),439(a,1))]. given #125 (T,wt=11): 1238 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),440(a,1))]. given #126 (A,wt=20): 81 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(17(a,1),10(b,1))]. given #127 (F,wt=11): 1243 (x ^ y)' != 0 | x ^ y = 1. [para(579(a,1),61(a,1)),rewrite(265(10),579(12)),flip(b),xx(a)]. given #128 (F,wt=11): 1329 (x v y)' != 1 | y v x = 0. [para(2(a,1),1233(a,1,1))]. given #129 (T,wt=11): 1331 (x ^ y)' != 1 | x ^ y = 0. [para(25(a,1),1233(a,1,1)),rewrite(25(8))]. given #130 (T,wt=11): 1375 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),1243(a,1,1))]. given #131 (A,wt=13): 90 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(18(a,1),5(a,1)),flip(a)]. given #132 (F,wt=11): 1377 (x v y)' != 0 | x v y = 1. [para(19(a,1),1243(a,1,1)),rewrite(19(8))]. given #133 (F,wt=11): 1380 (x ^ y)' != 1 | y ^ x = 0. [para(243(a,1),1329(a,1,1)),rewrite(243(7))]. given #134 (T,wt=11): 1384 (x v y)' != 0 | y v x = 1. [para(157(a,1),1375(a,1,1)),rewrite(157(7))]. given #135 (T,wt=12): 100 x v (y v ((x v y)' v z)) = 1. [para(74(a,1),3(a,1)),flip(a)]. given #136 (A,wt=14): 91 x v y != 1 | 0 != y | y' = x v y. [para(18(a,1),10(b,1)),rewrite(60(2)),flip(b)]. given #137 (F,wt=12): 113 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(77(a,1),5(a,1)),flip(a)]. given #138 (F,wt=12): 116 x v (y v (z v (x v y)')) = 1. [para(83(a,1),3(a,1)),flip(a)]. given #139 (T,wt=12): 119 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(86(a,1),5(a,1)),flip(a)]. given #140 (T,wt=12): 133 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),125(a,1,2,1))]. given #141 (A,wt=13): 92 (x v y) ^ (x v (z v y)) = x v y. [para(15(a,1),18(a,1,2))]. given #142 (F,wt=12): 134 x ^ (y ^ ((x ^ y) v z)') = 0. [para(125(a,1),5(a,1)),flip(a)]. given #143 (F,wt=12): 139 x ^ (y ^ (z v (x ^ y))') = 0. [para(132(a,1),5(a,1)),flip(a)]. given #144 (T,wt=12): 141 (x v y) ^ (x v (z v y))' = 0. [para(15(a,1),132(a,1,2,1))]. given #145 (T,wt=12): 182 ((x ^ y) v z) ^ (x v z)' = 0. [para(22(a,1),132(a,1,2,1))]. given #146 (A,wt=13): 95 x v (y v (z ^ (x v y))) = x v y. [para(24(a,1),3(a,1)),flip(a)]. given #147 (F,wt=12): 185 x v (y v ((x v y) ^ z)') = 1. [para(176(a,1),3(a,1)),flip(a)]. given #148 (F,wt=12): 187 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),176(a,1,2,1))]. given #149 (T,wt=12): 191 x v (y v (z ^ (x v y))') = 1. [para(186(a,1),3(a,1)),flip(a)]. given #150 (T,wt=12): 195 (x ^ y) v (x ^ (z ^ y))' = 1. [para(17(a,1),186(a,1,2,1))]. given #151 (A,wt=14): 97 1 != x | y ^ x != 0 | x' = y ^ x. [para(24(a,1),10(a,1)),rewrite(54(4)),flip(a)]. given #152 (F,wt=12): 196 ((x v y) ^ z) v (x ^ z)' = 1. [para(20(a,1),186(a,1,2,1))]. given #153 (F,wt=12): 210 x v (y v (z v (x v z)')) = 1. [para(29(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #154 (T,wt=12): 212 x v (y v ((x ^ z) v y)') = 1. [para(29(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #155 (T,wt=12): 225 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(32(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #156 (A,wt=13): 99 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(17(a,1),24(a,1,2))]. given #157 (F,wt=12): 227 x ^ (y ^ ((x v z) ^ y)') = 0. [para(32(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #158 (F,wt=12): 229 x v (y v (z v (x' v u))) = 1. [para(3(a,1),102(a,1,2))]. given #159 (T,wt=12): 231 x v (y v ((x ^ z)' v u)) = 1. [para(102(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #160 (T,wt=12): 233 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),115(a,1,2))]. given #161 (A,wt=15): 101 x ^ (x' v y) != 0 | x' v y = x'. [para(74(a,1),10(a,1)),flip(c),xx(a)]. given #162 (F,wt=12): 235 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(115(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #163 (F,wt=12): 246 x v (y v (z v (u v x'))) = 1. [para(3(a,1),117(a,1,2,2))]. given #164 (T,wt=12): 248 x v (y v (z v (x ^ u)')) = 1. [para(117(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #165 (T,wt=12): 250 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),120(a,1,2,2))]. given #166 (A,wt=13): 103 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),19(a,1,1))]. given #167 (F,wt=12): 252 x ^ (y ^ (z ^ (x v u)')) = 0. [para(120(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #168 (F,wt=12): 256 x ^ ((y v (x v z))' ^ u) = 0. [para(15(a,1),130(a,1,2,1,1))]. given #169 (T,wt=12): 260 x ^ (y ^ (z v (x v u))') = 0. [para(15(a,1),131(a,1,2,2,1))]. given #170 (T,wt=12): 290 x v ((x v y)' v (z v y)) = 1. [para(15(a,1),283(a,1,2)),rewrite(15(5))]. given #171 (A,wt=13): 104 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),19(a,1,2)),rewrite(3(3))]. given #172 (F,wt=12): 294 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(17(a,1),284(a,1,2)),rewrite(17(5))]. given #173 (F,wt=12): 298 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),136(a,1,2,1))]. given #174 (T,wt=12): 350 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),137(a,1,2,1,2))]. given #175 (T,wt=12): 351 x ^ ((y v (z v x))' ^ u) = 0. [para(137(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #176 (A,wt=19): 105 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),19(a,1,1)),rewrite(3(5),3(8))]. given #177 (F,wt=12): 355 x ^ (y ^ (z v (u v x))') = 0. [para(137(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #178 (F,wt=12): 363 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(138(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #179 (T,wt=12): 367 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),142(a,1,2))]. given #180 (T,wt=12): 376 x v ((y ^ (x ^ z))' v u) = 1. [para(17(a,1),180(a,1,2,1,1))]. given #181 (A,wt=17): 106 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(19(a,1),5(a,1,1)),flip(a)]. given #182 (F,wt=12): 405 x v (y v (z ^ (x ^ u))') = 1. [para(17(a,1),181(a,1,2,2,1))]. given #183 (F,wt=12): 411 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),189(a,1,2,1))]. given #184 (T,wt=12): 416 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),190(a,1,2,1,1))]. given #185 (T,wt=12): 418 x v (y v ((z ^ x)' v u)) = 1. [para(190(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #186 (A,wt=19): 108 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(15(a,1),19(a,1,1)),rewrite(3(4))]. given #187 (F,wt=12): 425 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),192(a,1,2,1,2))]. given #188 (F,wt=12): 427 x v (y v (z ^ (u ^ x))') = 1. [para(192(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #189 (T,wt=12): 492 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),194(a,1,2))]. given #190 (T,wt=12): 501 x v (y v ((y v x)' v z)) = 1. [para(207(a,1),3(a,1,1)),rewrite(73(2),3(5)),flip(a)]. given #191 (A,wt=15): 109 (x v y) ^ (x v (z v (y v u))) = x v y. [para(15(a,1),19(a,1,2,2))]. given #192 (F,wt=12): 505 x v (y v (z v (z v x)')) = 1. [para(207(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #193 (F,wt=12): 507 x v (y v (y v (x ^ z))') = 1. [para(207(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #194 (T,wt=12): 511 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(222(a,1),5(a,1,1)),rewrite(76(2),5(5)),flip(a)]. given #195 (T,wt=12): 515 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(222(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #196 (A,wt=17): 110 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(19(a,1),17(a,1,2)),flip(a)]. given #197 (F,wt=12): 517 x ^ (y ^ (y ^ (x v z))') = 0. [para(222(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #198 (F,wt=12): 522 x' v (y v (z v (x v u))) = 1. [para(3(a,1),285(a,1,2))]. given #199 (T,wt=12): 572 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),286(a,1,2))]. given #200 (T,wt=12): 578 x' v (y v (z v (u v x))) = 1. [para(3(a,1),287(a,1,2,2))]. given #201 (A,wt=22): 112 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [back_rewrite(107),rewrite(111(4))]. given #202 (F,wt=12): 583 (x ^ (y ^ z))' v (u v y) = 1. [para(79(a,1),287(a,1,2,2))]. given #203 (F,wt=12): 585 (x ^ (y ^ z))' v (u v z) = 1. [para(96(a,1),287(a,1,2,2))]. given #204 (T,wt=12): 592 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),288(a,1,2,2))]. given #205 (T,wt=12): 600 (x v (y v z))' ^ (u ^ y) = 0. [para(67(a,1),288(a,1,2,2))]. given #206 (A,wt=15): 114 x v (x' ^ y) != 1 | x' ^ y = x'. [para(77(a,1),10(b,1)),flip(c),xx(b)]. given #207 (F,wt=12): 601 (x v (y v z))' ^ (u ^ z) = 0. [para(88(a,1),288(a,1,2,2))]. given #208 (F,wt=12): 606 (x ^ y)' v (z v (x v u)) = 1. [para(579(a,1),3(a,1,1)),rewrite(73(2),3(5)),flip(a)]. given #209 (T,wt=12): 607 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),579(a,1,2))]. given #210 (T,wt=12): 638 (x ^ y)' v (z v (y v u)) = 1. [para(582(a,1),3(a,1,1)),rewrite(73(2),3(5)),flip(a)]. given #211 (A,wt=15): 118 x ^ (y v x') != 0 | y v x' = x'. [para(83(a,1),10(a,1)),flip(c),xx(a)]. given #212 (F,wt=12): 639 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),582(a,1,2))]. given #213 (F,wt=12): 649 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(593(a,1),5(a,1,1)),rewrite(76(2),5(5)),flip(a)]. given #214 (T,wt=12): 650 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),593(a,1,2))]. given #215 (T,wt=12): 657 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(596(a,1),5(a,1,1)),rewrite(76(2),5(5)),flip(a)]. given #216 (A,wt=15): 121 x v (y ^ x') != 1 | y ^ x' = x'. [para(86(a,1),10(b,1)),flip(c),xx(b)]. given #217 (F,wt=12): 658 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),596(a,1,2))]. given #218 (F,wt=12): 672 (x v (y ^ z)) ^ (x v y)' = 0. [para(68(a,1),132(a,1,2,1))]. given #219 (T,wt=12): 675 x v (y v (x v (y ^ z))') = 1. [para(68(a,1),283(a,1,2)),rewrite(2(5),3(5))]. given #220 (T,wt=12): 741 (x ^ (y v z)) v (x ^ y)' = 1. [para(78(a,1),186(a,1,2,1))]. given #221 (A,wt=13): 123 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(52(a,1),5(a,2,2)),rewrite(17(3),5(2))]. given #222 (F,wt=12): 743 x ^ (y ^ (x ^ (y v z))') = 0. [para(78(a,1),284(a,1,2)),rewrite(4(5),5(5))]. given #223 (F,wt=12): 764 ((x v y) ^ z) v (y ^ z)' = 1. [para(89(a,1),186(a,1,2,1))]. given #224 (T,wt=12): 768 x ^ (y ^ ((z v x) ^ y)') = 0. [para(32(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #225 (T,wt=12): 775 x ^ (y ^ (y ^ (z v x))') = 0. [para(222(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #226 (A,wt=17): 124 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(20(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #227 (F,wt=12): 789 (x ^ (y v z)) v (x ^ z)' = 1. [para(93(a,1),186(a,1,2,1))]. given #228 (F,wt=12): 793 x ^ (y ^ (x ^ (z v y))') = 0. [para(93(a,1),284(a,1,2)),rewrite(4(5),5(5))]. given #229 (T,wt=12): 812 ((x ^ y) v z) ^ (y v z)' = 0. [para(94(a,1),132(a,1,2,1))]. given #230 (T,wt=12): 817 x v (y v ((z ^ x) v y)') = 1. [para(29(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #231 (A,wt=22): 126 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(20(a,1),10(b,1))]. given #232 (F,wt=12): 825 x v (y v (y v (z ^ x))') = 1. [para(207(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #233 (F,wt=12): 923 (x v (y ^ z)) ^ (x v z)' = 0. [para(98(a,1),132(a,1,2,1))]. given #234 (T,wt=12): 927 x v (y v (x v (z ^ y))') = 1. [para(98(a,1),283(a,1,2)),rewrite(2(5),3(5))]. given #235 (T,wt=12): 967 x v (y v (z ^ (y v x))') = 1. [para(157(a,1),192(a,1,2,1,2)),rewrite(3(5))]. given #236 (A,wt=13): 127 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(15(a,1),20(a,1,2,1))]. given #237 (F,wt=12): 969 x v (y v (z v (y v x)')) = 1. [para(157(a,1),194(a,1,2,2,1)),rewrite(3(5))]. given #238 (F,wt=12): 970 (x v y)' ^ (z ^ (y v x)) = 0. [para(157(a,1),288(a,1,2,2))]. given #239 (T,wt=12): 971 (x v y)' v (z v (y v x)) = 1. [para(157(a,1),582(a,1,1,1))]. given #240 (T,wt=12): 972 (x v y) ^ (y v (x v z))' = 0. [para(157(a,1),593(a,1,2)),rewrite(3(2),4(5))]. given #241 (A,wt=15): 128 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(20(a,1),17(a,1,2)),flip(a)]. given #242 (F,wt=12): 973 (x v y) ^ (z v (y v x))' = 0. [para(157(a,1),596(a,1,2)),rewrite(4(5))]. given #243 (F,wt=12): 977 (x v y) ^ ((y v x)' ^ z) = 0. [para(965(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #244 (T,wt=12): 979 (x v y) ^ (z ^ (y v x)') = 0. [para(965(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #245 (T,wt=12): 1214 x ^ (y ^ (z v (y ^ x))') = 0. [para(243(a,1),137(a,1,2,1,2)),rewrite(5(5))]. given #246 (A,wt=15): 129 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(20(a,1),24(a,1,2)),rewrite(2(4))]. given #247 (F,wt=12): 1215 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(243(a,1),142(a,1,2,2,1)),rewrite(5(5))]. given #248 (F,wt=12): 1217 (x ^ y)' v (z v (y ^ x)) = 1. [para(243(a,1),287(a,1,2,2))]. given #249 (T,wt=12): 1218 (x ^ y) v (y ^ (x ^ z))' = 1. [para(243(a,1),579(a,1,2)),rewrite(5(2),2(5))]. given #250 (T,wt=12): 1219 (x ^ y) v (z ^ (y ^ x))' = 1. [para(243(a,1),582(a,1,2)),rewrite(2(5))]. given #251 (A,wt=15): 135 x v (x v y)' != 1 | (x v y)' = x'. [para(125(a,1),10(b,1)),flip(c),xx(b)]. given #252 (F,wt=12): 1220 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(243(a,1),596(a,1,1,1))]. given #253 (F,wt=12): 1222 (x ^ y) v ((y ^ x)' v z) = 1. [para(1212(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #254 (T,wt=12): 1225 (x ^ y) v (z v (y ^ x)') = 1. [para(1212(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #255 (T,wt=12): 1469 (x v y) ^ (y v (z v x))' = 0. [para(2(a,1),133(a,1,2,1)),rewrite(3(3))]. given #256 (A,wt=15): 140 x v (y v x)' != 1 | (y v x)' = x'. [para(132(a,1),10(b,1)),flip(c),xx(b)]. given #257 (F,wt=12): 1476 ((x ^ y) v z) ^ (z v x)' = 0. [para(183(a,1),133(a,1,2,1))]. given #258 (F,wt=12): 1479 ((x ^ y) v z) ^ (z v y)' = 0. [para(814(a,1),133(a,1,2,1))]. given #259 (T,wt=12): 1503 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),134(a,1,2,2,1,1))]. given #260 (T,wt=12): 1545 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),182(a,1,1))]. given #261 (A,wt=13): 144 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),54(a,1,2)),rewrite(5(5))]. given #262 (F,wt=12): 1547 (x v y)' ^ ((x ^ z) v y) = 0. [para(182(a,1),4(a,1)),flip(a)]. given #263 (F,wt=12): 1549 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),182(a,1,2,1))]. given #264 (T,wt=12): 1554 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(24(a,1),182(a,1,2,1))]. given #265 (T,wt=12): 1603 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),185(a,1,2,2,1,1))]. given #266 (A,wt=13): 146 x v (y v (x v z)) = y v (x v z). [para(58(a,1),3(a,2,2)),rewrite(15(3),3(2))]. given #267 (F,wt=12): 1613 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),187(a,1,2,1)),rewrite(5(3))]. given #268 (F,wt=12): 1620 ((x v y) ^ z) v (z ^ x)' = 1. [para(145(a,1),187(a,1,2,1))]. given #269 (T,wt=12): 1622 ((x v y) ^ z) v (z ^ y)' = 1. [para(761(a,1),187(a,1,2,1))]. given #270 (T,wt=12): 1664 (x ^ y)' v ((x v z) ^ y) = 1. [para(196(a,1),2(a,1)),flip(a)]. given #271 (A,wt=13): 147 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. given #272 (F,wt=12): 1666 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),196(a,1,1))]. given #273 (F,wt=12): 1668 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),196(a,1,2,1))]. given #274 (T,wt=12): 1673 ((x v y) ^ (z v x)) v x' = 1. [para(18(a,1),196(a,1,2,1))]. given #275 (T,wt=12): 1712 x v (y v ((y ^ z) v x)') = 1. [para(212(a,1),15(a,1)),flip(a)]. given #276 (A,wt=19): 148 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(21(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #277 (F,wt=12): 1715 x v ((x ^ y) v (x ^ z))' = 1. [para(212(a,1),22(a,1)),flip(a)]. given #278 (F,wt=12): 1720 x v ((x ^ y) v (z ^ x))' = 1. [para(212(a,1),94(a,1)),flip(a)]. given #279 (T,wt=12): 1775 x ^ (y ^ ((y v z) ^ x)') = 0. [para(227(a,1),17(a,1)),flip(a)]. given #280 (T,wt=12): 1777 x ^ ((x v y) ^ (x v z))' = 0. [para(227(a,1),20(a,1)),flip(a)]. given #281 (A,wt=26): 149 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x' = y ^ ((x ^ y) v z). [para(21(a,1),10(b,1))]. given #282 (F,wt=12): 1782 x ^ ((x v y) ^ (z v x))' = 0. [para(227(a,1),89(a,1)),flip(a)]. given #283 (F,wt=12): 1920 x v ((y v x)' v (z v y)) = 1. [para(2(a,1),290(a,1,2,1,1))]. given #284 (T,wt=12): 1998 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),294(a,1,2,1,1))]. given #285 (T,wt=12): 2394 x v (y v ((z ^ y) v x)') = 1. [para(814(a,1),501(a,1,2)),rewrite(2(4))]. given #286 (A,wt=15): 150 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(15(a,1),21(a,1,2,2))]. given #287 (F,wt=12): 2450 x v ((y ^ x) v (x ^ z))' = 1. [para(507(a,1),94(a,1)),flip(a)]. given #288 (F,wt=12): 2471 x ^ (y ^ ((z v y) ^ x)') = 0. [para(761(a,1),511(a,1,2)),rewrite(4(4))]. given #289 (T,wt=12): 2546 x ^ ((y v x) ^ (x v z))' = 0. [para(517(a,1),89(a,1)),flip(a)]. given #290 (T,wt=12): 2881 (x v y)' ^ (x v (y ^ z)) = 0. [para(672(a,1),4(a,1)),flip(a)]. given #291 (A,wt=17): 151 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(21(a,1),17(a,1,2)),flip(a)]. given #292 (F,wt=12): 2918 (x ^ y)' v (x ^ (y v z)) = 1. [para(741(a,1),2(a,1)),flip(a)]. given #293 (F,wt=12): 2966 (x ^ y)' v ((z v x) ^ y) = 1. [para(764(a,1),2(a,1)),flip(a)]. given #294 (T,wt=12): 2968 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),764(a,1,1))]. given #295 (T,wt=12): 2970 ((x v y) ^ (y v z)) v y' = 1. [para(6(a,1),764(a,1,2,1))]. given #296 (A,wt=19): 152 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(17(a,1),21(a,1,2,2,1)),rewrite(5(5))]. given #297 (F,wt=12): 2975 ((x v y) ^ (z v y)) v y' = 1. [para(18(a,1),764(a,1,2,1))]. given #298 (F,wt=12): 3023 x ^ ((y v x) ^ (z v x))' = 0. [para(768(a,1),89(a,1)),flip(a)]. given #299 (T,wt=12): 3165 (x ^ y)' v (x ^ (z v y)) = 1. [para(789(a,1),2(a,1)),flip(a)]. given #300 (T,wt=12): 3223 (x v (y ^ z)) ^ (z v x)' = 0. [para(2(a,1),812(a,1,1))]. given #301 (A,wt=19): 153 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(21(a,1),24(a,1,2)),rewrite(2(5))]. given #302 (F,wt=12): 3224 (x v y)' ^ ((z ^ x) v y) = 0. [para(812(a,1),4(a,1)),flip(a)]. given #303 (F,wt=12): 3226 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(7(a,1),812(a,1,2,1))]. given #304 (T,wt=12): 3231 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(24(a,1),812(a,1,2,1))]. given #305 (T,wt=12): 3280 x v ((y ^ x) v (z ^ x))' = 1. [para(817(a,1),94(a,1)),flip(a)]. given #306 (A,wt=15): 154 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(21(a,1),20(a,1,2)),rewrite(20(3)),flip(a)]. given #307 (F,wt=12): 3363 (x v y)' ^ (x v (z ^ y)) = 0. [para(923(a,1),4(a,1)),flip(a)]. given #308 (F,wt=12): 3870 (x v y)' ^ ((y ^ z) v x) = 0. [para(1476(a,1),4(a,1)),flip(a)]. given #309 (T,wt=12): 3895 (x v y)' ^ ((z ^ y) v x) = 0. [para(1479(a,1),4(a,1)),flip(a)]. given #310 (T,wt=12): 3955 (x v y)' ^ (y v (x ^ z)) = 0. [para(1545(a,1),4(a,1)),flip(a)]. given #311 (A,wt=13): 156 x v (y v (z v x)) = y v (z v x). [para(3(a,1),60(a,1,2)),rewrite(3(5))]. given #312 (F,wt=12): 4007 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),1547(a,1,1,1))]. given #313 (F,wt=12): 4011 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(24(a,1),1547(a,1,1,1))]. given #314 (T,wt=12): 4157 (x ^ y)' v ((y v z) ^ x) = 1. [para(1620(a,1),2(a,1)),flip(a)]. given #315 (T,wt=12): 4180 (x ^ y)' v ((z v y) ^ x) = 1. [para(1622(a,1),2(a,1)),flip(a)]. given #316 (A,wt=15): 158 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),67(a,1,2,2))]. given #317 (F,wt=12): 4206 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),1664(a,1,2))]. given #318 (F,wt=12): 4208 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),1664(a,1,1,1))]. given #319 (T,wt=12): 4212 x' v ((x v y) ^ (z v x)) = 1. [para(18(a,1),1664(a,1,1,1))]. given #320 (T,wt=12): 5139 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),2966(a,1,2))]. given #321 (A,wt=18): 160 x v (y v z) != 1 | 0 != y | y' = x v (y v z). [para(67(a,1),10(b,1)),rewrite(146(3)),flip(b)]. given #322 (F,wt=12): 5141 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),2966(a,1,1,1))]. given #323 (F,wt=12): 5145 x' v ((y v x) ^ (z v x)) = 1. [para(18(a,1),2966(a,1,1,1))]. given #324 (T,wt=12): 5469 (x v y)' ^ (y v (z ^ x)) = 0. [para(3223(a,1),4(a,1)),flip(a)]. given #325 (T,wt=12): 5584 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(7(a,1),3224(a,1,1,1))]. given #326 (A,wt=13): 161 x ^ (y ^ (z v (x v u))) = y ^ x. [para(67(a,1),17(a,1,2)),flip(a)]. given #327 (F,wt=12): 5588 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(24(a,1),3224(a,1,1,1))]. given #328 (F,wt=13): 162 x v ((y ^ (x ^ z)) v u) = x v u. [para(79(a,1),3(a,1,1)),flip(a)]. given #329 (T,wt=13): 167 x v (y v (z ^ (x ^ u))) = y v x. [para(79(a,1),15(a,1,2)),flip(a)]. given #330 (T,wt=13): 169 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(88(a,1),5(a,1,1)),flip(a)]. given #331 (A,wt=15): 163 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(79(a,1),3(a,1)),flip(a)]. given #332 (F,wt=13): 173 x ^ (y ^ (z v (u v x))) = y ^ x. [para(88(a,1),17(a,1,2)),flip(a)]. given #333 (F,wt=13): 198 x v ((y ^ (z ^ x)) v u) = x v u. [para(96(a,1),3(a,1,1)),flip(a)]. given #334 (T,wt=13): 202 x v (y v (z ^ (u ^ x))) = y v x. [para(96(a,1),15(a,1,2)),flip(a)]. given #335 (T,wt=13): 213 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),23(a,1,2,2,1))]. given #336 (A,wt=15): 164 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),79(a,1,2,2))]. given #337 (F,wt=13): 236 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),25(a,1,1))]. given #338 (F,wt=13): 237 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),25(a,1,2)),rewrite(5(3))]. given #339 (T,wt=13): 275 x ^ (x ^ y)' != 0 | x ^ y = x. [para(176(a,1),34(a,1)),rewrite(4(6),265(11)),xx(a)]. given #340 (T,wt=13): 276 x ^ (y ^ x)' != 0 | y ^ x = x. [para(186(a,1),34(a,1)),rewrite(4(6),265(11)),xx(a)]. given #341 (A,wt=18): 166 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(79(a,1),10(a,1)),rewrite(123(5)),flip(a)]. given #342 (F,wt=13): 289 x' ^ (y v x) != 0 | y v x = x. [para(283(a,1),10(a,1)),rewrite(265(10)),flip(c),xx(a)]. given #343 (F,wt=13): 293 x' v (y ^ x) != 1 | y ^ x = x. [para(284(a,1),10(b,1)),rewrite(265(10)),flip(c),xx(b)]. given #344 (T,wt=13): 296 (x ^ y) v y' != 1 | x ^ y = y. [para(284(a,1),34(b,1)),rewrite(265(10)),flip(c),xx(b)]. given #345 (T,wt=13): 386 x v (x v y)' != 1 | x v y = x. [para(125(a,1),36(b,1)),rewrite(2(3),265(11)),xx(b)]. given #346 (A,wt=15): 170 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(88(a,1),5(a,1)),flip(a)]. given #347 (F,wt=13): 387 x v (y v x)' != 1 | y v x = x. [para(132(a,1),36(b,1)),rewrite(2(3),265(11)),xx(b)]. given #348 (F,wt=13): 396 (x v y) ^ y' != 0 | x v y = y. [para(283(a,1),36(a,1)),rewrite(265(10)),flip(c),xx(a)]. given #349 (T,wt=13): 946 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(15(a,1),145(a,1,1))]. given #350 (T,wt=13): 963 x v (y v (z ^ (y v x))) = x v y. [para(157(a,1),96(a,1,2,2)),rewrite(3(4))]. given #351 (A,wt=18): 171 x v (y v z) != 1 | 0 != z | z' = x v (y v z). [para(88(a,1),10(b,1)),rewrite(156(3)),flip(b)]. given #352 (F,wt=13): 974 (x v (y v z)) ^ (y v x) = y v x. [para(157(a,1),145(a,1,2)),rewrite(3(2),157(7))]. given #353 (F,wt=13): 1059 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),159(a,1,2,2))]. given #354 (T,wt=13): 1073 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(5(a,1),165(a,1,2,2))]. given #355 (T,wt=13): 1083 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),168(a,1,2,2,2))]. given #356 (A,wt=15): 172 (x v y) ^ (z v (x v (u v y))) = x v y. [para(15(a,1),88(a,1,2,2))]. given #357 (F,wt=13): 1110 (x ^ (y ^ z)) v (u v y) = u v y. [para(17(a,1),183(a,1,1))]. given #358 (F,wt=13): 1181 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),200(a,1,2,2,2))]. given #359 (T,wt=13): 1209 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(243(a,1),88(a,1,2,2)),rewrite(5(4))]. given #360 (T,wt=13): 1210 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(243(a,1),22(a,2)),rewrite(5(3),1204(6))]. given #361 (A,wt=17): 174 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(22(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #362 (F,wt=13): 1244 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),761(a,1,1))]. given #363 (F,wt=13): 1262 (x v (y v z)) ^ (z v y) = z v y. [para(157(a,1),761(a,1,2)),rewrite(157(7))]. given #364 (T,wt=13): 1269 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),814(a,1,1))]. given #365 (T,wt=13): 1289 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(243(a,1),814(a,1,2)),rewrite(243(7))]. given #366 (A,wt=17): 175 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),22(a,1,2,1))]. given #367 (F,wt=13): 1298 x' ^ (x v y) != 0 | x v y = x. [para(74(a,1),70(a,1)),rewrite(265(10)),flip(c),xx(a)]. given #368 (F,wt=13): 1343 x' v (x ^ y) != 1 | x ^ y = x. [para(77(a,1),81(b,1)),rewrite(265(10)),flip(c),xx(b)]. given #369 (T,wt=13): 1480 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),92(a,1,2)),rewrite(3(3))]. given #370 (T,wt=13): 1741 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),99(a,1,2)),rewrite(5(3))]. given #371 (A,wt=22): 177 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(22(a,1),10(a,1))]. given #372 (F,wt=13): 1953 (x v (y v z)) ^ (z v x) = z v x. [para(104(a,1),4(a,1)),flip(a)]. given #373 (F,wt=13): 4040 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(265(a,1),1549(a,1,2)),rewrite(4(6))]. given #374 (T,wt=13): 4062 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(265(a,1),1554(a,1,2)),rewrite(4(6))]. given #375 (T,wt=13): 4366 x v ((x' v y) ^ (x' v z)) = 1. [para(265(a,1),1668(a,1,2)),rewrite(2(6))]. given #376 (A,wt=15): 178 x v (y v ((x ^ z) v u)) = y v (x v u). [para(22(a,1),15(a,1,2)),flip(a)]. given #377 (F,wt=13): 4389 x v ((x' v y) ^ (z v x')) = 1. [para(265(a,1),1673(a,1,2)),rewrite(2(6))]. given #378 (F,wt=13): 5240 x v ((y v x') ^ (x' v z)) = 1. [para(265(a,1),2970(a,1,2)),rewrite(2(6))]. given #379 (T,wt=13): 5377 x v ((y v x') ^ (z v x')) = 1. [para(265(a,1),2975(a,1,2)),rewrite(2(6))]. given #380 (T,wt=13): 5618 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(265(a,1),3226(a,1,2)),rewrite(4(6))]. given #381 (A,wt=15): 179 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite(4(4))]. given #382 (F,wt=13): 5638 x ^ ((y ^ x') v (z ^ x')) = 0. [para(265(a,1),3231(a,1,2)),rewrite(4(6))]. given #383 (F,wt=13): 5716 x ^ (((x v y) ^ (x v z)) v u) = x. [para(154(a,1),20(a,1)),rewrite(6(2)),flip(a)]. given #384 (T,wt=13): 5731 x ^ (((x v y) ^ (z v x)) v u) = x. [para(154(a,1),89(a,1)),rewrite(18(2)),flip(a)]. given #385 (T,wt=13): 7204 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(237(a,1),2(a,1)),flip(a)]. given #386 (A,wt=17): 184 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(22(a,1),88(a,1,2,2))]. given #387 (F,wt=13): 7296 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),275(a,1,2,1))]. given #388 (F,wt=13): 7299 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),276(a,1,2,1))]. given #389 (T,wt=13): 7301 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),276(a,1,2,1)),rewrite(6(7)),flip(b)]. given #390 (T,wt=13): 7336 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),289(a,1,2))]. given #391 (A,wt=15): 188 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(176(a,1),10(a,1)),flip(c),xx(a)]. given #392 (F,wt=13): 7351 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),293(a,1,2))]. given #393 (F,wt=13): 7377 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),296(a,1,1))]. given #394 (T,wt=13): 7379 x v (y v x)' != 1 | x v y = x. [para(2(a,1),386(a,1,2,1))]. given #395 (T,wt=13): 7470 x v (x v y)' != 1 | y v x = x. [para(2(a,1),387(a,1,2,1))]. given #396 (A,wt=15): 193 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(186(a,1),10(a,1)),flip(c),xx(a)]. given #397 (F,wt=13): 7472 (x ^ y) v x' != 1 | x ^ y = x. [para(7(a,1),387(a,1,2,1)),rewrite(7(7)),flip(b)]. given #398 (F,wt=13): 7486 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),396(a,1,1))]. given #399 (T,wt=13): 8859 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),1298(a,1,2))]. given #400 (T,wt=13): 8864 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),1343(a,1,2))]. given #401 (A,wt=14): 197 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(21(a,1),186(a,1,2,1))]. given #402 (F,wt=13): 9377 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),5716(a,1,2,1,1))]. given #403 (F,wt=13): 9378 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),5716(a,1,2))]. given #404 (T,wt=13): 9473 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),5731(a,1,2,1,1))]. given #405 (T,wt=13): 9474 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),5731(a,1,2))]. given #406 (A,wt=15): 199 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(96(a,1),3(a,1)),flip(a)]. given #407 (F,wt=13): 9774 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),7301(a,1,1))]. given #408 (F,wt=13): 9824 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),7472(a,1,1))]. given #409 (T,wt=13): 9857 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),9377(a,1,2))]. given #410 (T,wt=13): 10050 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),9473(a,1,2))]. given #411 (A,wt=18): 201 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(96(a,1),10(a,1)),rewrite(144(5)),flip(a)]. given #412 (F,wt=14): 208 x v (y v (z v (x v (y v z))')) = 1. [para(29(a,1),3(a,1)),rewrite(3(3)),flip(a)]. given #413 (F,wt=14): 211 x v (y v (z v (y v (x v z))')) = 1. [para(15(a,1),29(a,1,2,2,1)),rewrite(3(5))]. given #414 (T,wt=14): 219 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(23(a,1),132(a,1,2,1))]. given #415 (T,wt=14): 223 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(32(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #416 (A,wt=15): 203 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(17(a,1),96(a,1,2,2))]. given #417 (F,wt=14): 226 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(17(a,1),32(a,1,2,2,1)),rewrite(5(5))]. given #418 (F,wt=14): 228 x v (y v (z v ((x v y)' v u))) = 1. [para(102(a,1),3(a,1)),flip(a)]. given #419 (T,wt=14): 232 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0. [para(115(a,1),5(a,1)),flip(a)]. given #420 (T,wt=14): 245 x v (y v (z v (u v (x v y)'))) = 1. [para(117(a,1),3(a,1)),flip(a)]. given #421 (A,wt=17): 204 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(19(a,1),96(a,1,2,2)),rewrite(3(5),3(4))]. given #422 (F,wt=14): 249 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0. [para(120(a,1),5(a,1)),flip(a)]. given #423 (F,wt=14): 253 (x v y) ^ ((x v (y v z))' ^ u) = 0. [para(3(a,1),130(a,1,2,1,1))]. given #424 (T,wt=14): 254 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0. [para(130(a,1),5(a,1)),flip(a)]. given #425 (T,wt=14): 257 (x v y) ^ (z ^ (x v (y v u))') = 0. [para(3(a,1),131(a,1,2,2,1))]. given #426 (A,wt=17): 205 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(20(a,1),96(a,1,2,2))]. Low Water (keep): wt=48, part=0.99, limit=42 given #427 (F,wt=14): 258 x ^ (y ^ (z ^ ((x ^ y) v u)')) = 0. [para(131(a,1),5(a,1)),flip(a)]. given #428 (F,wt=14): 262 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),34(b,1))]. given #429 (T,wt=14): 264 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),34(a,1)),rewrite(4(4),52(4)),flip(a)]. given #430 (T,wt=14): 268 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(24(a,1),34(a,1)),rewrite(4(4),54(4)),flip(a)]. Low Water (keep): wt=38, part=0.98, limit=37 given #431 (A,wt=21): 206 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(21(a,1),96(a,1,2,2))]. Low Water (keep): wt=37, part=0.98, limit=37 given #432 (F,wt=14): 271 x v y != 1 | 0 != x | (x v y)' = x. [para(58(a,1),34(a,1)),rewrite(4(5),6(5)),flip(b)]. given #433 (F,wt=14): 272 x v y != 1 | 0 != y | (x v y)' = y. [para(60(a,1),34(a,1)),rewrite(4(5),18(5)),flip(b)]. given #434 (T,wt=14): 291 x v (y v (y v ((x v y) ^ z))') = 1. [para(23(a,1),283(a,1,2)),rewrite(2(6),3(6))]. Low Water (keep): wt=35, part=0.98, limit=35 given #435 (T,wt=14): 295 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(21(a,1),284(a,1,2)),rewrite(4(6),5(6))]. given #436 (A,wt=19): 209 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(29(a,1),10(a,1)),flip(c),xx(a)]. given #437 (F,wt=14): 297 (x v y) ^ (z v (x v (y v u)))' = 0. [para(3(a,1),136(a,1,2,1,2))]. given #438 (F,wt=14): 299 x ^ (y ^ (z v ((x ^ y) v u))') = 0. [para(136(a,1),5(a,1)),flip(a)]. given #439 (T,wt=14): 328 x v y != 1 | 0 != y | (y v x)' = y. [para(60(a,1),35(a,1)),rewrite(4(5),6(5)),flip(b)]. given #440 (T,wt=14): 352 x ^ (y ^ (z v (u v (x ^ y)))') = 0. [para(137(a,1),5(a,1)),flip(a)]. given #441 (A,wt=19): 214 x v (y v (z v ((x v (y v z)) ^ u))) = x v (y v z). [para(23(a,1),3(a,1)),rewrite(3(2),3(4)),flip(a)]. given #442 (F,wt=14): 354 (x v y) ^ (z v (x v (u v y)))' = 0. [para(15(a,1),137(a,1,2,1,2))]. given #443 (F,wt=14): 356 ((x ^ y) v z) ^ (u v (x v z))' = 0. [para(22(a,1),137(a,1,2,1,2))]. given #444 (T,wt=14): 358 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0. [para(25(a,1),137(a,1,2,1,2)),rewrite(5(6),5(5))]. given #445 (T,wt=14): 360 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0. [para(138(a,1),5(a,1)),flip(a)]. given #446 (A,wt=26): 215 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | x' = y v ((x v y) ^ z). [para(23(a,1),10(a,1))]. Low Water (keep): wt=34, part=0.96, limit=34 given #447 (F,wt=14): 362 (x v y) ^ ((x v (z v y))' ^ u) = 0. [para(15(a,1),138(a,1,2,1,1))]. Low Water (keep): wt=33, part=0.95, limit=33 given #448 (F,wt=14): 364 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0. [para(22(a,1),138(a,1,2,1,1))]. given #449 (T,wt=14): 369 (x v y) ^ (z ^ (x v (u v y))') = 0. [para(15(a,1),142(a,1,2,2,1))]. given #450 (T,wt=14): 370 ((x ^ y) v z) ^ (u ^ (x v z)') = 0. [para(22(a,1),142(a,1,2,2,1))]. given #451 (A,wt=17): 216 x v (y v (z v ((x v z) ^ u))) = y v (x v z). [para(23(a,1),15(a,1,2)),flip(a)]. Low Water (keep): wt=32, part=0.94, limit=32 given #452 (F,wt=14): 373 x v (y v (((x v y) ^ z)' v u)) = 1. [para(180(a,1),3(a,1)),flip(a)]. given #453 (F,wt=14): 374 (x ^ y) v ((x ^ (y ^ z))' v u) = 1. [para(5(a,1),180(a,1,2,1,1))]. given #454 (T,wt=14): 402 x v (y v (z v ((x v y) ^ u)')) = 1. [para(181(a,1),3(a,1)),flip(a)]. Low Water (keep): wt=31, part=0.94, limit=31 given #455 (T,wt=14): 403 (x ^ y) v (z v (x ^ (y ^ u))') = 1. [para(5(a,1),181(a,1,2,2,1))]. given #456 (A,wt=19): 217 x v (y v (z v ((y v (x v z)) ^ u))) = x v (y v z). [para(15(a,1),23(a,1,2,2,1)),rewrite(3(5))]. given #457 (F,wt=14): 409 x v (y v (z ^ ((x v y) ^ u))') = 1. [para(189(a,1),3(a,1)),flip(a)]. given #458 (F,wt=14): 410 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1. [para(5(a,1),189(a,1,2,1,2))]. given #459 (T,wt=14): 415 x v (y v ((z ^ (x v y))' v u)) = 1. [para(190(a,1),3(a,1)),flip(a)]. given #460 (T,wt=14): 419 (x ^ y) v ((x ^ (z ^ y))' v u) = 1. [para(17(a,1),190(a,1,2,1,1))]. given #461 (A,wt=19): 218 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(23(a,1),18(a,1,2)),rewrite(4(5))]. given #462 (F,wt=14): 420 ((x v y) ^ z) v ((x ^ z)' v u) = 1. [para(20(a,1),190(a,1,2,1,1))]. given #463 (F,wt=14): 424 x v (y v (z ^ (u ^ (x v y)))') = 1. [para(192(a,1),3(a,1)),flip(a)]. given #464 (T,wt=14): 428 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1. [para(17(a,1),192(a,1,2,1,2))]. given #465 (T,wt=14): 429 x v (y v (z v (u ^ (x v y))')) = 1. [para(19(a,1),192(a,1,2,1,2)),rewrite(3(6),3(5))]. given #466 (A,wt=21): 220 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(23(a,1),88(a,1,2,2))]. given #467 (F,wt=14): 430 ((x v y) ^ z) v (u ^ (x ^ z))' = 1. [para(20(a,1),192(a,1,2,1,2))]. given #468 (F,wt=14): 458 1 != x | y ^ x != 0 | (x ^ y)' = x. [para(54(a,1),37(b,1)),rewrite(2(2),7(2)),flip(a)]. Low Water (keep): wt=30, part=0.91, limit=30 given #469 (T,wt=14): 494 (x ^ y) v (z v (x ^ (u ^ y))') = 1. [para(17(a,1),194(a,1,2,2,1))]. given #470 (T,wt=14): 495 ((x v y) ^ z) v (u v (x ^ z)') = 1. [para(20(a,1),194(a,1,2,2,1))]. given #471 (A,wt=15): 221 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(23(a,1),22(a,1,2)),rewrite(22(3)),flip(a)]. given #472 (F,wt=13): 12998 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(221(a,1),22(a,1)),rewrite(7(2)),flip(a)]. Low Water (keep): wt=29, part=0.90, limit=29 given #473 (F,wt=13): 13009 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(221(a,1),94(a,1)),rewrite(24(2)),flip(a)]. given #474 (T,wt=13): 13138 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),12998(a,1,2,1,1))]. given #475 (T,wt=13): 13139 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),12998(a,1,2))]. given #476 (A,wt=19): 224 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(32(a,1),10(b,1)),flip(c),xx(b)]. given #477 (F,wt=13): 13234 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),13009(a,1,2,1,1))]. given #478 (F,wt=13): 13235 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),13009(a,1,2))]. Low Water (keep): wt=28, part=0.87, limit=28 given #479 (T,wt=13): 13340 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(4(a,1),13138(a,1,2))]. Low Water (keep): wt=27, part=0.87, limit=27 given #480 (T,wt=13): 13523 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),13234(a,1,2))]. given #481 (A,wt=19): 230 x ^ (y v (x' v z)) != 0 | y v (x' v z) = x'. [para(102(a,1),10(a,1)),flip(c),xx(a)]. given #482 (F,wt=14): 502 x v (y v (z v (z v (x v y))')) = 1. [para(207(a,1),3(a,1)),flip(a)]. given #483 (F,wt=14): 503 x v (y v (z v (y v (z v x))')) = 1. [para(3(a,1),207(a,1,2,2,1)),rewrite(3(5))]. given #484 (T,wt=14): 506 x v (y v (z v (x v (z v y))')) = 1. [para(15(a,1),207(a,1,2,2,1)),rewrite(3(6))]. given #485 (T,wt=14): 512 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0. [para(222(a,1),5(a,1)),flip(a)]. given #486 (A,wt=19): 234 x v (y ^ (x' ^ z)) != 1 | y ^ (x' ^ z) = x'. [para(115(a,1),10(b,1)),flip(c),xx(b)]. given #487 (F,wt=14): 513 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0. [para(5(a,1),222(a,1,2,2,1)),rewrite(5(5))]. given #488 (F,wt=14): 516 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0. [para(17(a,1),222(a,1,2,2,1)),rewrite(5(6))]. given #489 (T,wt=14): 521 (x v y)' v (z v (x v (y v u))) = 1. [para(3(a,1),285(a,1,2,2))]. given #490 (T,wt=14): 571 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0. [para(5(a,1),286(a,1,2,2))]. given #491 (A,wt=19): 238 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),25(a,1,1)),rewrite(5(5),5(8))]. given #492 (F,wt=14): 581 (x v y)' v (z v (x v (u v y))) = 1. [para(15(a,1),287(a,1,2,2))]. given #493 (F,wt=14): 584 ((x ^ y) v z)' v (u v (x v z)) = 1. [para(22(a,1),287(a,1,2,2))]. given #494 (T,wt=14): 587 (x ^ (y ^ z))' v (u v (x ^ y)) = 1. [para(25(a,1),287(a,1,2,2))]. given #495 (T,wt=14): 595 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0. [para(17(a,1),288(a,1,2,2))]. given #496 (A,wt=22): 239 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [para(25(a,1),10(a,1)),rewrite(17(7),17(6),5(5),123(6),52(6))]. given #497 (F,wt=14): 597 (x v (y v z))' ^ (u ^ (x v y)) = 0. [para(19(a,1),288(a,1,2,2))]. given #498 (F,wt=14): 598 ((x v y) ^ z)' ^ (u ^ (x ^ z)) = 0. [para(20(a,1),288(a,1,2,2))]. given #499 (T,wt=14): 609 x v (((x v y) ^ z)' v (u v y)) = 1. [para(15(a,1),579(a,1,2)),rewrite(15(6))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 195 (0.00 of 7.76 sec). given #500 (T,wt=14): 610 x v (y v (((x ^ z) v y) ^ u)') = 1. [para(22(a,1),579(a,1,2)),rewrite(2(6),3(6))]. given #501 (A,wt=17): 240 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(25(a,1),15(a,1,2)),flip(a)]. given #502 (F,wt=14): 641 x v ((y ^ (x v z))' v (u v z)) = 1. [para(15(a,1),582(a,1,2)),rewrite(15(6))]. given #503 (F,wt=14): 642 (x ^ (y ^ z))' v (u v (x ^ z)) = 1. [para(17(a,1),582(a,1,1,1))]. given #504 (T,wt=14): 643 (x ^ y)' v (z v ((x v u) ^ y)) = 1. [para(20(a,1),582(a,1,1,1))]. given #505 (T,wt=14): 645 x v (y v (z ^ ((x ^ u) v y))') = 1. [para(22(a,1),582(a,1,2)),rewrite(2(6),3(6))]. given #506 (A,wt=19): 241 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(17(a,1),25(a,1,1)),rewrite(5(4))]. given #507 (F,wt=14): 652 x ^ (((x ^ y) v z)' ^ (u ^ y)) = 0. [para(17(a,1),593(a,1,2)),rewrite(17(6))]. Low Water (keep): wt=26, part=0.81, limit=26 given #508 (F,wt=14): 653 x ^ (y ^ (((x v z) ^ y) v u)') = 0. [para(20(a,1),593(a,1,2)),rewrite(4(6),5(6))]. given #509 (T,wt=14): 660 (x v (y v z))' ^ (u ^ (x v z)) = 0. [para(15(a,1),596(a,1,1,1))]. given #510 (T,wt=14): 661 x ^ ((y v (x ^ z))' ^ (u ^ z)) = 0. [para(17(a,1),596(a,1,2)),rewrite(17(6))]. given #511 (A,wt=15): 242 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(17(a,1),25(a,1,2,2))]. given #512 (F,wt=14): 662 x ^ (y ^ (z v ((x v u) ^ y))') = 0. [para(20(a,1),596(a,1,2)),rewrite(4(6),5(6))]. given #513 (F,wt=14): 664 (x v y)' ^ (z ^ ((x ^ u) v y)) = 0. [para(22(a,1),596(a,1,1,1))]. given #514 (T,wt=14): 678 (x v (y ^ z)) ^ (u v (x v y))' = 0. [para(68(a,1),137(a,1,2,1,2))]. given #515 (T,wt=14): 679 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0. [para(68(a,1),138(a,1,2,1,1))]. given #516 (A,wt=17): 244 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(25(a,1),88(a,1,2,2)),rewrite(5(5),5(4))]. given #517 (F,wt=14): 680 (x v (y ^ z)) ^ (u ^ (x v y)') = 0. [para(68(a,1),142(a,1,2,2,1))]. given #518 (F,wt=14): 682 (x v (y ^ z))' v (u v (x v y)) = 1. [para(68(a,1),287(a,1,2,2))]. Low Water (keep): wt=25, part=0.78, limit=25 given #519 (T,wt=14): 683 x v (y v ((x v (y ^ z)) ^ u)') = 1. [para(68(a,1),579(a,1,2)),rewrite(2(6),3(6))]. given #520 (T,wt=14): 684 x v (y v (z ^ (x v (y ^ u)))') = 1. [para(68(a,1),582(a,1,2)),rewrite(2(6),3(6))]. given #521 (A,wt=19): 247 x ^ (y v (z v x')) != 0 | y v (z v x') = x'. [para(117(a,1),10(a,1)),flip(c),xx(a)]. given #522 (F,wt=14): 685 (x v y)' ^ (z ^ (x v (y ^ u))) = 0. [para(68(a,1),596(a,1,1,1))]. given #523 (F,wt=14): 746 (x ^ (y v z)) v ((x ^ y)' v u) = 1. [para(78(a,1),190(a,1,2,1,1))]. given #524 (T,wt=14): 747 (x ^ (y v z)) v (u ^ (x ^ y))' = 1. [para(78(a,1),192(a,1,2,1,2))]. given #525 (T,wt=14): 750 (x ^ (y v z)) v (u v (x ^ y)') = 1. [para(78(a,1),194(a,1,2,2,1))]. given #526 (A,wt=19): 251 x v (y ^ (z ^ x')) != 1 | y ^ (z ^ x') = x'. [para(120(a,1),10(b,1)),flip(c),xx(b)]. given #527 (F,wt=14): 751 (x ^ (y v z))' ^ (u ^ (x ^ y)) = 0. [para(78(a,1),288(a,1,2,2))]. given #528 (F,wt=14): 752 (x ^ y)' v (z v (x ^ (y v u))) = 1. [para(78(a,1),582(a,1,1,1))]. given #529 (T,wt=14): 753 x ^ (y ^ ((x ^ (y v z)) v u)') = 0. [para(78(a,1),593(a,1,2)),rewrite(4(6),5(6))]. given #530 (T,wt=14): 754 x ^ (y ^ (z v (x ^ (y v u)))') = 0. [para(78(a,1),596(a,1,2)),rewrite(4(6),5(6))]. given #531 (A,wt=19): 255 x v ((x v y)' ^ z) != 1 | (x v y)' ^ z = x'. [para(130(a,1),10(b,1)),flip(c),xx(b)]. given #532 (F,wt=14): 771 ((x v y) ^ z) v ((y ^ z)' v u) = 1. [para(89(a,1),190(a,1,2,1,1))]. given #533 (F,wt=14): 772 ((x v y) ^ z) v (u ^ (y ^ z))' = 1. [para(89(a,1),192(a,1,2,1,2))]. given #534 (T,wt=14): 774 ((x v y) ^ z) v (u v (y ^ z)') = 1. [para(89(a,1),194(a,1,2,2,1))]. given #535 (T,wt=14): 776 ((x v y) ^ z)' ^ (u ^ (y ^ z)) = 0. [para(89(a,1),288(a,1,2,2))]. given #536 (A,wt=19): 259 x v (y ^ (x v z)') != 1 | y ^ (x v z)' = x'. [para(131(a,1),10(b,1)),flip(c),xx(b)]. given #537 (F,wt=14): 777 (x ^ y)' v (z v ((u v x) ^ y)) = 1. [para(89(a,1),582(a,1,1,1))]. Low Water (keep): wt=24, part=0.75, limit=24 given #538 (F,wt=14): 778 x ^ (y ^ (((z v x) ^ y) v u)') = 0. [para(89(a,1),593(a,1,2)),rewrite(4(6),5(6))]. given #539 (T,wt=14): 779 x ^ (y ^ (z v ((u v x) ^ y))') = 0. [para(89(a,1),596(a,1,2)),rewrite(4(6),5(6))]. given #540 (T,wt=14): 796 (x ^ (y v z)) v ((x ^ z)' v u) = 1. [para(93(a,1),190(a,1,2,1,1))]. given #541 (A,wt=20): 261 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),34(a,1))]. given #542 (F,wt=14): 797 (x ^ (y v z)) v (u ^ (x ^ z))' = 1. [para(93(a,1),192(a,1,2,1,2))]. given #543 (F,wt=14): 800 (x ^ (y v z)) v (u v (x ^ z)') = 1. [para(93(a,1),194(a,1,2,2,1))]. given #544 (T,wt=14): 801 (x ^ (y v z))' ^ (u ^ (x ^ z)) = 0. [para(93(a,1),288(a,1,2,2))]. given #545 (T,wt=14): 802 (x ^ y)' v (z v (x ^ (u v y))) = 1. [para(93(a,1),582(a,1,1,1))]. given #546 (A,wt=20): 263 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),34(b,1))]. given #547 (F,wt=14): 803 x ^ (y ^ ((x ^ (z v y)) v u)') = 0. [para(93(a,1),593(a,1,2)),rewrite(4(6),5(6))]. given #548 (F,wt=14): 804 x ^ (y ^ (z v (x ^ (u v y)))') = 0. [para(93(a,1),596(a,1,2)),rewrite(4(6),5(6))]. given #549 (T,wt=14): 821 ((x ^ y) v z) ^ (u v (y v z))' = 0. [para(94(a,1),137(a,1,2,1,2))]. given #550 (T,wt=14): 822 ((x ^ y) v z) ^ ((y v z)' ^ u) = 0. [para(94(a,1),138(a,1,2,1,1))]. given #551 (A,wt=20): 266 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(15(a,1),34(a,1))]. Low Water (keep): wt=23, part=0.70, limit=23 given #552 (F,wt=14): 823 ((x ^ y) v z) ^ (u ^ (y v z)') = 0. [para(94(a,1),142(a,1,2,2,1))]. given #553 (F,wt=14): 826 ((x ^ y) v z)' v (u v (y v z)) = 1. [para(94(a,1),287(a,1,2,2))]. given #554 (T,wt=14): 827 x v (y v (((z ^ x) v y) ^ u)') = 1. [para(94(a,1),579(a,1,2)),rewrite(2(6),3(6))]. given #555 (T,wt=14): 828 x v (y v (z ^ ((u ^ x) v y))') = 1. [para(94(a,1),582(a,1,2)),rewrite(2(6),3(6))]. given #556 (A,wt=20): 267 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(17(a,1),34(b,1))]. given #557 (F,wt=14): 829 (x v y)' ^ (z ^ ((u ^ x) v y)) = 0. [para(94(a,1),596(a,1,1,1))]. given #558 (F,wt=14): 930 (x v (y ^ z)) ^ (u v (x v z))' = 0. [para(98(a,1),137(a,1,2,1,2))]. given #559 (T,wt=14): 931 (x v (y ^ z)) ^ ((x v z)' ^ u) = 0. [para(98(a,1),138(a,1,2,1,1))]. given #560 (T,wt=14): 932 (x v (y ^ z)) ^ (u ^ (x v z)') = 0. [para(98(a,1),142(a,1,2,2,1))]. Low Water (keep): wt=22, part=0.68, limit=22 given #561 (A,wt=15): 269 x ^ (x' v y) != 0 | (x' v y)' = x. [para(74(a,1),34(a,1)),rewrite(4(6)),xx(a)]. given #562 (F,wt=14): 934 (x v (y ^ z))' v (u v (x v z)) = 1. [para(98(a,1),287(a,1,2,2))]. given #563 (F,wt=14): 935 x v (y v ((x v (z ^ y)) ^ u)') = 1. [para(98(a,1),579(a,1,2)),rewrite(2(6),3(6))]. given #564 (T,wt=14): 936 x v (y v (z ^ (x v (u ^ y)))') = 1. [para(98(a,1),582(a,1,2)),rewrite(2(6),3(6))]. given #565 (T,wt=14): 937 (x v y)' ^ (z ^ (x v (u ^ y))) = 0. [para(98(a,1),596(a,1,1,1))]. given #566 (A,wt=15): 270 x ^ (y v x') != 0 | (y v x')' = x. [para(83(a,1),34(a,1)),rewrite(4(6)),xx(a)]. given #567 (F,wt=14): 975 (x v (y v z)) ^ (z v (x v y))' = 0. [para(3(a,1),965(a,1,1))]. given #568 (F,wt=14): 976 (x v (y v z)) ^ (y v (z v x))' = 0. [para(3(a,1),965(a,1,2,1))]. given #569 (T,wt=14): 978 (x v (y v z)) ^ (x v (z v y))' = 0. [para(15(a,1),965(a,1,1)),rewrite(3(4))]. given #570 (T,wt=14): 1067 (x v (y v (z v u)))' ^ (v ^ z) = 0. [para(159(a,1),288(a,1,2,2))]. given #571 (A,wt=18): 273 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(79(a,1),34(a,1)),rewrite(4(5),123(5)),flip(a)]. given #572 (F,wt=14): 1068 x' v (y v (z v (u v (x v v)))) = 1. [para(159(a,1),582(a,1,1,1))]. given #573 (F,wt=14): 1069 x ^ (y v (z v (u v (x v v))))' = 0. [para(159(a,1),596(a,1,2)),rewrite(4(6))]. given #574 (T,wt=14): 1079 (x ^ (y ^ (z ^ u)))' v (v v z) = 1. [para(165(a,1),287(a,1,2,2))]. given #575 (T,wt=14): 1080 x v (y ^ (z ^ (u ^ (x ^ v))))' = 1. [para(165(a,1),582(a,1,2)),rewrite(2(6))]. given #576 (A,wt=22): 274 x v y != 1 | x ^ ((x ^ z) v y) != 0 | ((x ^ z) v y)' = x. [para(22(a,1),34(a,1)),rewrite(4(6))]. given #577 (F,wt=14): 1081 x' ^ (y ^ (z ^ (u ^ (x ^ v)))) = 0. [para(165(a,1),596(a,1,1,1))]. given #578 (F,wt=14): 1097 (x v (y v (z v u)))' ^ (v ^ u) = 0. [para(168(a,1),288(a,1,2,2))]. given #579 (T,wt=14): 1098 x' v (y v (z v (u v (v v x)))) = 1. [para(168(a,1),582(a,1,1,1))]. given #580 (T,wt=14): 1099 x ^ (y v (z v (u v (v v x))))' = 0. [para(168(a,1),596(a,1,2)),rewrite(4(6))]. given #581 (A,wt=18): 277 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x. [para(96(a,1),34(a,1)),rewrite(4(5),144(5)),flip(a)]. given #582 (F,wt=14): 1192 (x ^ (y ^ (z ^ u)))' v (v v u) = 1. [para(200(a,1),287(a,1,2,2))]. given #583 (F,wt=14): 1193 x v (y ^ (z ^ (u ^ (v ^ x))))' = 1. [para(200(a,1),582(a,1,2)),rewrite(2(6))]. given #584 (T,wt=14): 1194 x' ^ (y ^ (z ^ (u ^ (v ^ x)))) = 0. [para(200(a,1),596(a,1,1,1))]. given #585 (T,wt=14): 1223 (x ^ (y ^ z)) v (z ^ (x ^ y))' = 1. [para(5(a,1),1212(a,1,1))]. given #586 (A,wt=19): 278 x ^ (y v (x v y)') != 0 | (y v (x v y)')' = x. [para(29(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #587 (F,wt=14): 1224 (x ^ (y ^ z)) v (y ^ (z ^ x))' = 1. [para(5(a,1),1212(a,1,2,1))]. given #588 (F,wt=14): 1226 (x ^ (y ^ z)) v (x ^ (z ^ y))' = 1. [para(17(a,1),1212(a,1,1)),rewrite(5(4))]. given #589 (T,wt=14): 1230 1 != x | y ^ x != 0 | x' = x ^ y. [para(4(a,1),57(b,1))]. given #590 (T,wt=14): 1240 x v y != 1 | 0 != y | y' = y v x. [para(2(a,1),61(a,1))]. given #591 (A,wt=26): 279 x v y != 1 | x ^ (y v ((x v y) ^ z)) != 0 | (y v ((x v y) ^ z))' = x. [para(23(a,1),34(a,1)),rewrite(4(7))]. given #592 (F,wt=14): 1389 (x ^ (y v (z ^ x))) v (z ^ x)' = 1. [para(90(a,1),186(a,1,2,1))]. given #593 (F,wt=14): 1391 x ^ (y ^ (y ^ (z v (x ^ y)))') = 0. [para(90(a,1),284(a,1,2)),rewrite(4(6),5(6))]. given #594 (T,wt=14): 1418 x v (y v (z v ((x v z)' v u))) = 1. [para(100(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #595 (T,wt=14): 1420 x v (y v (((x ^ z) v y)' v u)) = 1. [para(100(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #596 (A,wt=19): 280 x ^ (y v (x' v z)) != 0 | (y v (x' v z))' = x. [para(102(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #597 (F,wt=14): 1424 x v (y v (((z ^ x) v y)' v u)) = 1. [para(100(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #598 (F,wt=14): 1427 x v y != 1 | 0 != x | x' = y v x. [para(2(a,1),91(a,1))]. given #599 (T,wt=14): 1436 x ^ (y ^ (z ^ ((x ^ z)' ^ u))) = 0. [para(113(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #600 (T,wt=14): 1438 x ^ (y ^ (((x v z) ^ y)' ^ u)) = 0. [para(113(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #601 (A,wt=22): 281 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ (y ^ z))' = x ^ y. [para(25(a,1),34(a,1)),rewrite(4(7),17(7),17(6),5(5),123(6),52(6))]. given #602 (F,wt=14): 1442 x ^ (y ^ (((z v x) ^ y)' ^ u)) = 0. [para(113(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #603 (F,wt=14): 1448 x v (y v (z v (u v (x v z)'))) = 1. [para(116(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #604 (T,wt=14): 1450 x v (y v (z v ((x ^ u) v y)')) = 1. [para(116(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #605 (T,wt=14): 1454 x v (y v (z v ((u ^ x) v y)')) = 1. [para(116(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #606 (A,wt=19): 282 x ^ (y v (z v x')) != 0 | (y v (z v x'))' = x. [para(117(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #607 (F,wt=10): 18666 x v y != 0 | y v x = 0. [para(103(a,1),282(a,1)),rewrite(207(7),72(5)),flip(b)]. given #608 (F,wt=10): 18669 x ^ y != 0 | y ^ x = 0. [para(243(a,1),18666(a,1)),rewrite(243(6))]. given #609 (T,wt=14): 1459 x ^ (y ^ (z ^ (u ^ (x ^ z)'))) = 0. [para(119(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #610 (T,wt=14): 1461 x ^ (y ^ (z ^ ((x v u) ^ y)')) = 0. [para(119(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #611 (A,wt=15): 292 (x v y) ^ y' != 0 | (x v y)' = y'. [para(283(a,1),34(a,1)),xx(a)]. given #612 (F,wt=14): 1465 x ^ (y ^ (z ^ ((u v x) ^ y)')) = 0. [para(119(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #613 (F,wt=14): 1472 (x v y) ^ (x v (z v (y v u)))' = 0. [para(15(a,1),133(a,1,2,1,2))]. given #614 (T,wt=14): 1475 (x v (y ^ z)) ^ (x v (u v y))' = 0. [para(183(a,1),133(a,1,2,1,2))]. given #615 (T,wt=14): 1478 (x v (y ^ z)) ^ (x v (u v z))' = 0. [para(814(a,1),133(a,1,2,1,2))]. given #616 (A,wt=19): 300 x v (y v (x v z))' != 1 | (y v (x v z))' = x'. [para(136(a,1),10(b,1)),flip(c),xx(b)]. given #617 (F,wt=14): 1493 x v (y v (z v (u ^ (x v z))')) = 1. [para(92(a,1),192(a,1,2,1,2)),rewrite(3(6),3(5))]. given #618 (F,wt=14): 1506 x ^ (y ^ (z ^ ((x ^ z) v u)')) = 0. [para(134(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #619 (T,wt=14): 1516 x ^ (y ^ (z ^ (u v (x ^ z))')) = 0. [para(139(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #620 (T,wt=14): 1525 (x v y) ^ (x v (z v (u v y)))' = 0. [para(3(a,1),141(a,1,2,1,2))]. given #621 (A,wt=20): 301 x v (y v z) != 1 | (z v x) ^ y != 0 | (z v x)' = y. [para(2(a,1),35(a,1)),rewrite(3(2))]. given #622 (F,wt=14): 1528 (x v (y ^ (z ^ u))) ^ (x v z)' = 0. [para(79(a,1),141(a,1,2,1,2))]. given #623 (F,wt=14): 1530 (x v (y ^ (z ^ u))) ^ (x v u)' = 0. [para(96(a,1),141(a,1,2,1,2))]. given #624 (T,wt=14): 1532 (x v ((x v y) ^ z)) ^ (x v y)' = 0. [para(23(a,1),141(a,1,2,1))]. given #625 (T,wt=14): 1542 (x v (y ^ z)) ^ (x v (z ^ y))' = 0. [para(243(a,1),141(a,1,2,1,2))]. given #626 (A,wt=20): 302 x v (y v z) != 1 | (y v x) ^ z != 0 | (x v y)' = z. [para(2(a,1),35(b,1,1))]. given #627 (F,wt=14): 1553 ((x ^ (y ^ z)) v u) ^ (y v u)' = 0. [para(17(a,1),182(a,1,1,1))]. given #628 (F,wt=14): 1555 ((x ^ y) v (z ^ (x ^ u))) ^ x' = 0. [para(79(a,1),182(a,1,2,1))]. given #629 (T,wt=14): 1557 ((x ^ y) v (z ^ (u ^ x))) ^ x' = 0. [para(96(a,1),182(a,1,2,1))]. given #630 (T,wt=14): 1566 ((x ^ y) v z) ^ (y v (u v z))' = 0. [para(145(a,1),182(a,1,1,1)),rewrite(3(4))]. given #631 (A,wt=26): 303 x v (y v (z v u)) != 1 | (x v (y v z)) ^ u != 0 | (x v (y v z))' = u. [para(3(a,1),35(a,1,2))]. given #632 (F,wt=14): 1575 (x v (y ^ (z v x))) ^ (z v x)' = 0. [para(95(a,1),132(a,1,2,1))]. given #633 (F,wt=14): 1578 x v (y v (y v (z ^ (x v y)))') = 1. [para(95(a,1),283(a,1,2)),rewrite(2(6),3(6))]. given #634 (T,wt=14): 1600 (x v (y ^ (x v z))) ^ (x v z)' = 0. [para(95(a,1),141(a,1,2,1))]. given #635 (T,wt=14): 1606 x v (y v (z v ((x v z) ^ u)')) = 1. [para(185(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. Low Water (keep): wt=21, part=0.61, limit=21 given #636 (A,wt=20): 304 x v (y v z) != 1 | z ^ (x v y) != 0 | (x v y)' = z. [para(4(a,1),35(b,1))]. given #637 (F,wt=14): 1616 (x ^ y) v (x ^ (z ^ (y ^ u)))' = 1. [para(17(a,1),187(a,1,2,1,2))]. given #638 (F,wt=14): 1619 (x ^ (y v z)) v (x ^ (u ^ y))' = 1. [para(145(a,1),187(a,1,2,1,2))]. given #639 (T,wt=14): 1621 (x ^ (y v z)) v (x ^ (u ^ z))' = 1. [para(761(a,1),187(a,1,2,1,2))]. given #640 (T,wt=14): 1632 (x ^ y) v (x ^ (z ^ (u ^ y)))' = 1. [para(5(a,1),195(a,1,2,1,2))]. given #641 (A,wt=18): 305 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),35(a,1,2)),rewrite(17(6),89(6))]. Low Water (keep): wt=20, part=0.60, limit=20 given #642 (F,wt=14): 1638 (x ^ ((x ^ y) v z)) v (x ^ y)' = 1. [para(21(a,1),195(a,1,2,1))]. given #643 (F,wt=14): 1639 (x ^ (y v (z v u))) v (x ^ z)' = 1. [para(67(a,1),195(a,1,2,1,2))]. given #644 (T,wt=14): 1640 (x ^ (y v (z v u))) v (x ^ u)' = 1. [para(88(a,1),195(a,1,2,1,2))]. given #645 (T,wt=14): 1646 (x ^ (y v z)) v (x ^ (z v y))' = 1. [para(157(a,1),195(a,1,2,1,2))]. given #646 (A,wt=18): 306 x v y != 1 | x v y != 0 | (x v y)' = x v y. [para(26(a,1),35(b,1)),rewrite(60(2),58(2))]. given #647 (F,wt=14): 1652 (x ^ (y v (x ^ z))) v (x ^ z)' = 1. [para(90(a,1),195(a,1,2,1))]. given #648 (F,wt=14): 1654 1 != x | x ^ y != 0 | x' = y ^ x. [para(4(a,1),97(b,1))]. given #649 (T,wt=14): 1670 ((x v (y v z)) ^ u) v (y ^ u)' = 1. [para(15(a,1),196(a,1,1,1))]. given #650 (T,wt=14): 1677 ((x v y) ^ (z v (x v u))) v x' = 1. [para(67(a,1),196(a,1,2,1))]. given #651 (A,wt=26): 309 x v (y v (z v u)) != 1 | (x v z) ^ (y v u) != 0 | (x v z)' = y v u. [para(15(a,1),35(a,1,2))]. given #652 (F,wt=14): 1678 ((x v y) ^ (z v (u v x))) v x' = 1. [para(88(a,1),196(a,1,2,1))]. given #653 (F,wt=14): 1687 ((x v y) ^ z) v (y ^ (u ^ z))' = 1. [para(183(a,1),196(a,1,1,1)),rewrite(5(4))]. given #654 (T,wt=14): 1696 x v (y v (z v (u v (x v u)'))) = 1. [para(3(a,1),210(a,1,2))]. given #655 (T,wt=14): 1698 x v (y v (z v ((x ^ u) v z)')) = 1. [para(210(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #656 (A,wt=20): 310 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(15(a,1),35(a,1))]. given #657 (F,wt=14): 1704 x v (y v (z v ((u ^ x) v z)')) = 1. [para(210(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #658 (F,wt=14): 1714 x v (y v ((z ^ (x ^ u)) v y)') = 1. [para(17(a,1),212(a,1,2,2,1,1))]. given #659 (T,wt=14): 1728 x ^ (y ^ (z ^ (u ^ (x ^ u)'))) = 0. [para(5(a,1),225(a,1,2))]. given #660 (T,wt=14): 1730 x ^ (y ^ (z ^ ((x v u) ^ z)')) = 0. [para(225(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #661 (A,wt=26): 311 x v (y v (z v u)) != 1 | (y v (x v z)) ^ u != 0 | (x v (y v z))' = u. [para(15(a,1),35(b,1,1)),rewrite(3(2))]. given #662 (F,wt=14): 1736 x ^ (y ^ (z ^ ((u v x) ^ z)')) = 0. [para(225(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #663 (F,wt=14): 1774 x ^ (y ^ ((z v (x v u)) ^ y)') = 0. [para(15(a,1),227(a,1,2,2,1,1))]. given #664 (T,wt=14): 1791 x v (y v (z v (u v (x' v v)))) = 1. [para(3(a,1),229(a,1,2,2))]. given #665 (T,wt=14): 1792 x v (y v (z v ((x ^ u)' v v))) = 1. [para(229(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #666 (A,wt=26): 312 x v (y v (z ^ u)) != 1 | z ^ ((x v y) ^ u) != 0 | (x v y)' = z ^ u. [para(17(a,1),35(b,1))]. given #667 (F,wt=14): 1797 x v (y v (z v ((u ^ x)' v v))) = 1. [para(229(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #668 (F,wt=14): 1802 x v (y v ((z ^ (x ^ u))' v v)) = 1. [para(17(a,1),231(a,1,2,2,1,1))]. given #669 (T,wt=14): 1811 x ^ (y ^ (z ^ (u ^ (x' ^ v)))) = 0. [para(5(a,1),233(a,1,2,2))]. given #670 (T,wt=14): 1812 x ^ (y ^ (z ^ ((x v u)' ^ v))) = 0. [para(233(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #671 (A,wt=22): 313 x v (y v z) != 1 | y v z != 0 | (y v z)' = x v (y v z). [para(18(a,1),35(b,1)),rewrite(156(3),146(3))]. given #672 (F,wt=14): 1817 x ^ (y ^ (z ^ ((u v x)' ^ v))) = 0. [para(233(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #673 (F,wt=14): 1826 x ^ (y ^ ((z v (x v u))' ^ v)) = 0. [para(15(a,1),235(a,1,2,2,1,1))]. given #674 (T,wt=14): 1836 x v (y v (z v (u v (v v x')))) = 1. [para(3(a,1),246(a,1,2,2,2))]. given #675 (T,wt=14): 1837 x v (y v (z v (u v (x ^ v)'))) = 1. [para(246(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #676 (A,wt=19): 315 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z. [para(74(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #677 (F,wt=14): 1842 x v (y v (z v (u v (v ^ x)'))) = 1. [para(246(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #678 (F,wt=14): 1847 x v (y v (z v (u ^ (x ^ v))')) = 1. [para(17(a,1),248(a,1,2,2,2,1))]. given #679 (T,wt=14): 1856 x ^ (y ^ (z ^ (u ^ (v ^ x')))) = 0. [para(5(a,1),250(a,1,2,2,2))]. given #680 (T,wt=14): 1857 x ^ (y ^ (z ^ (u ^ (x v v)'))) = 0. [para(250(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #681 (A,wt=23): 316 x v (y v ((x v y)' ^ z)) != 1 | (x v y)' ^ z = (x v y)'. [para(77(a,1),35(b,1)),flip(c),xx(b)]. given #682 (F,wt=14): 1862 x ^ (y ^ (z ^ (u ^ (v v x)'))) = 0. [para(250(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #683 (F,wt=14): 1878 (x v (y v z)) ^ (y v (x v z))' = 0. [para(103(a,1),182(a,1,1,1)),rewrite(3(2),3(4))]. given #684 (T,wt=14): 1880 (x ^ y)' v (((x v z) ^ y) v u) = 1. [para(196(a,1),103(a,1,1)),rewrite(62(8),1664(11))]. given #685 (T,wt=14): 1882 x v (y v (z v ((y v x)' v u))) = 1. [para(103(a,1),231(a,1,2,2,1,1)),rewrite(3(6))]. given #686 (A,wt=19): 317 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'. [para(83(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #687 (F,wt=14): 1883 x v (y v (z v (u v (y v x)'))) = 1. [para(103(a,1),248(a,1,2,2,2,1)),rewrite(3(6))]. given #688 (F,wt=14): 1887 x ^ (y ^ (z ^ (u v (x v v))')) = 0. [para(15(a,1),252(a,1,2,2,2,1))]. given #689 (T,wt=14): 1896 x ^ ((y v (z v (x v u)))' ^ v) = 0. [para(3(a,1),256(a,1,2,1,1))]. given #690 (T,wt=14): 1902 x ^ (y ^ ((z v (u v x))' ^ v)) = 0. [para(183(a,1),256(a,1,2,1,1,2)),rewrite(5(6))]. given #691 (A,wt=15): 318 (x v y) ^ x' != 0 | (x v y)' = x'. [para(83(a,1),35(a,1)),xx(a)]. given #692 (F,wt=14): 1908 x ^ (y ^ (z v (u v (x v v)))') = 0. [para(3(a,1),260(a,1,2,2,1))]. given #693 (F,wt=14): 1914 x ^ (y ^ (z ^ (u v (v v x))')) = 0. [para(183(a,1),260(a,1,2,2,1,2)),rewrite(5(6))]. given #694 (T,wt=14): 1921 x v ((x v y)' v (z v (y v u))) = 1. [para(290(a,1),3(a,1,1)),rewrite(73(2),3(6),3(5)),flip(a)]. given #695 (T,wt=14): 1923 x v ((x v y)' v (z v (u v y))) = 1. [para(3(a,1),290(a,1,2,2))]. given #696 (A,wt=23): 319 x v (y v (z ^ (x v y)')) != 1 | z ^ (x v y)' = (x v y)'. [para(86(a,1),35(b,1)),flip(c),xx(b)]. given #697 (F,wt=14): 1925 x v (y v ((x v z)' v (u v z))) = 1. [para(290(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #698 (F,wt=14): 1927 x v (y v (x v (z ^ (y ^ u)))') = 1. [para(79(a,1),290(a,1,2,2)),rewrite(2(5))]. given #699 (T,wt=14): 1928 x v (((x ^ y) v z)' v (u v z)) = 1. [para(290(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #700 (T,wt=14): 1930 x v (y v (x v (z ^ (u ^ y)))') = 1. [para(96(a,1),290(a,1,2,2)),rewrite(2(5))]. given #701 (A,wt=22): 320 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(52(a,1),35(b,1)),rewrite(23(4))]. given #702 (F,wt=14): 1939 x v (((y ^ x) v z)' v (u v z)) = 1. [para(290(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #703 (F,wt=14): 1945 x v ((y ^ z) v (x v (z ^ y))') = 1. [para(243(a,1),290(a,1,2,2)),rewrite(2(5))]. given #704 (T,wt=14): 1966 x v (y v (z v ((z v x)' v u))) = 1. [para(104(a,1),190(a,1,2,1,1)),rewrite(3(6),3(5))]. given #705 (T,wt=14): 1967 x v (y v (z v (u ^ (z v x))')) = 1. [para(104(a,1),192(a,1,2,1,2)),rewrite(3(6),3(5))]. given #706 (A,wt=32): 321 x v (y v ((x v (y v z)) ^ u)) != 1 | (x v y) ^ u != 0 | (x v y)' = (x v (y v z)) ^ u. [para(20(a,1),35(b,1)),rewrite(3(2),3(15))]. given #707 (F,wt=14): 1969 x v (y v (z v (u v (z v x)'))) = 1. [para(104(a,1),194(a,1,2,2,1)),rewrite(3(6),3(5))]. given #708 (F,wt=14): 1970 (x v (y v z))' ^ (u ^ (z v x)) = 0. [para(104(a,1),288(a,1,2,2))]. given #709 (T,wt=14): 1971 (x v y)' v (z v (y v (u v x))) = 1. [para(104(a,1),582(a,1,1,1))]. given #710 (T,wt=14): 1972 (x v y) ^ (y v (z v (x v u)))' = 0. [para(104(a,1),593(a,1,2)),rewrite(3(3),3(2),4(6))]. given #711 (A,wt=23): 322 x v (y v (x v (y v z))') != 1 | (x v (y v z))' = (x v y)'. [para(125(a,1),35(b,1)),rewrite(3(2),3(14)),flip(c),xx(b)]. given #712 (F,wt=14): 1973 (x v y) ^ (z v (y v (u v x)))' = 0. [para(104(a,1),596(a,1,2)),rewrite(4(6))]. given #713 (F,wt=14): 1985 x v ((y v x)' v (z v (u v y))) = 1. [para(100(a,1),104(a,1,1)),rewrite(3(7),3(6),62(8),100(11))]. given #714 (T,wt=14): 1986 x v (y v ((z v x)' v (u v z))) = 1. [para(116(a,1),104(a,1,1)),rewrite(3(7),3(6),62(8),116(11))]. given #715 (T,wt=14): 1988 x v (((y v x) ^ z)' v (u v y)) = 1. [para(185(a,1),104(a,1,1)),rewrite(3(7),62(8),185(11))]. given #716 (A,wt=23): 323 x v (y v (z v (x v y))') != 1 | (z v (x v y))' = (x v y)'. [para(132(a,1),35(b,1)),flip(c),xx(b)]. given #717 (F,wt=14): 1989 x v ((y ^ (z v x))' v (u v z)) = 1. [para(191(a,1),104(a,1,1)),rewrite(3(7),62(8),191(11))]. given #718 (F,wt=14): 1992 x v (((y ^ z) v x)' v (u v y)) = 1. [para(212(a,1),104(a,1,1)),rewrite(3(7),62(8),212(11))]. given #719 (T,wt=14): 1999 x ^ ((x ^ y)' ^ (z ^ (y ^ u))) = 0. [para(294(a,1),5(a,1,1)),rewrite(76(2),5(6),5(5)),flip(a)]. given #720 (T,wt=14): 2001 x ^ ((x ^ y)' ^ (z ^ (u ^ y))) = 0. [para(5(a,1),294(a,1,2,2))]. given #721 (A,wt=22): 324 x v y != 1 | z ^ (x v y) != 0 | (x v y)' = z ^ (x v y). [para(54(a,1),35(b,1)),rewrite(95(4))]. given #722 (F,wt=14): 2003 x ^ (y ^ ((x ^ z)' ^ (u ^ z))) = 0. [para(294(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #723 (F,wt=14): 2006 x ^ (((x v y) ^ z)' ^ (u ^ z)) = 0. [para(294(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #724 (T,wt=14): 2009 x ^ (y ^ (x ^ (z v (y v u)))') = 0. [para(67(a,1),294(a,1,2,2)),rewrite(4(5))]. given #725 (T,wt=14): 2010 x ^ (y ^ (x ^ (z v (u v y)))') = 0. [para(88(a,1),294(a,1,2,2)),rewrite(4(5))]. given #726 (A,wt=24): 325 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z. [para(58(a,1),35(a,1,2))]. given #727 (F,wt=14): 2017 x ^ (((y v x) ^ z)' ^ (u ^ z)) = 0. [para(294(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #728 (F,wt=14): 2021 x ^ ((y v z) ^ (x ^ (z v y))') = 0. [para(157(a,1),294(a,1,2,2)),rewrite(4(5))]. given #729 (T,wt=14): 2039 x ^ (y ^ (z v (u v (v v x)))') = 0. [para(183(a,1),298(a,1,2,1,2,2)),rewrite(5(6))]. given #730 (T,wt=14): 2043 x ^ ((y v (z v (u v x)))' ^ v) = 0. [para(350(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #731 (A,wt=36): 326 x v (y v (z ^ (((x v y) ^ z) v u))) != 1 | (x v y) ^ z != 0 | (x v y)' = z ^ (((x v y) ^ z) v u). [para(21(a,1),35(b,1))]. given #732 (F,wt=14): 2057 x ^ (y ^ (z v (u v (y ^ x)))') = 0. [para(243(a,1),350(a,1,2,1,2,2)),rewrite(5(6))]. given #733 (F,wt=14): 2074 x ^ (y ^ ((z v (y ^ x))' ^ u)) = 0. [para(243(a,1),351(a,1,2,1,1,2)),rewrite(5(6))]. given #734 (T,wt=14): 2121 x ^ (y ^ (z ^ (u v (y ^ x))')) = 0. [para(243(a,1),355(a,1,2,2,1,2)),rewrite(5(6))]. given #735 (T,wt=14): 2136 x ^ (y ^ (z ^ ((y ^ x)' ^ u))) = 0. [para(243(a,1),363(a,1,2,2,1,1)),rewrite(5(6))]. given #736 (A,wt=24): 327 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z. [para(60(a,1),35(a,1,2))]. given #737 (F,wt=14): 2151 x ^ (y ^ (z ^ (u ^ (y ^ x)'))) = 0. [para(243(a,1),367(a,1,2,2,2,1)),rewrite(5(6))]. given #738 (F,wt=14): 2158 x v ((y ^ (z ^ (x ^ u)))' v v) = 1. [para(5(a,1),376(a,1,2,1,1))]. given #739 (T,wt=14): 2163 x v (y v ((z ^ (u ^ x))' v v)) = 1. [para(145(a,1),376(a,1,2,1,1,2)),rewrite(3(6))]. given #740 (T,wt=14): 2166 x v (y v ((z ^ (y v x))' v u)) = 1. [para(103(a,1),376(a,1,2,1,1,2)),rewrite(3(6))]. given #741 (A,wt=28): 332 x v (y v z) != 1 | (x v y) ^ ((y ^ u) v z) != 0 | (x v y)' = (y ^ u) v z. [para(22(a,1),35(a,1,2))]. given #742 (F,wt=14): 2167 (x ^ (y ^ z))' v (u v (v v y)) = 1. [para(376(a,1),104(a,1,1)),rewrite(3(7),62(8),376(11))]. given #743 (F,wt=14): 2203 ((x ^ y) v z) ^ (x v (z v u))' = 0. [para(182(a,1),106(a,1,2)),rewrite(4(4),76(4)),flip(a)]. given #744 (T,wt=14): 2222 x v (y v (z ^ (u ^ (x ^ v)))') = 1. [para(5(a,1),405(a,1,2,2,1))]. given #745 (T,wt=14): 2227 x v (y v (z v (u ^ (v ^ x))')) = 1. [para(145(a,1),405(a,1,2,2,1,2)),rewrite(3(6))]. given #746 (A,wt=19): 333 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(176(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #747 (F,wt=14): 2229 x v (y v (z v (u ^ (y v x))')) = 1. [para(103(a,1),405(a,1,2,2,1,2)),rewrite(3(6))]. given #748 (F,wt=14): 2237 x v (y v (z ^ (u ^ (v ^ x)))') = 1. [para(145(a,1),411(a,1,2,1,2,2)),rewrite(3(6))]. given #749 (T,wt=14): 2239 x v (y v (z ^ (u ^ (y v x)))') = 1. [para(103(a,1),411(a,1,2,1,2,2)),rewrite(3(6))]. given #750 (T,wt=14): 2241 x v ((y ^ (z ^ (u ^ x)))' v v) = 1. [para(5(a,1),416(a,1,2,1,1,2))]. given #751 (A,wt=19): 334 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(186(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #752 (F,wt=14): 2258 (x ^ (y ^ z))' v (u v (v v z)) = 1. [para(416(a,1),104(a,1,1)),rewrite(3(7),62(8),416(11))]. given #753 (F,wt=14): 2294 (x ^ y)' v (z v (u v (x v v))) = 1. [para(579(a,1),108(a,1,1,2)),rewrite(82(2),3(5),62(8),607(11))]. given #754 (T,wt=14): 2295 (x ^ y)' v (z v (u v (y v v))) = 1. [para(582(a,1),108(a,1,1,2)),rewrite(82(2),3(5),62(8),639(11))]. given #755 (T,wt=14): 2301 (x ^ y) v (z v ((y ^ x)' v u)) = 1. [para(1212(a,1),108(a,1,1,2)),rewrite(82(2),62(8),1225(11))]. given #756 (A,wt=23): 336 (x v y) ^ (z v (y v z)') != 0 | (x v y)' = z v (y v z)'. [para(29(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #757 (F,wt=14): 2308 x v (y v (((y v x) ^ z)' v u)) = 1. [para(185(a,1),108(a,1,1)),rewrite(62(8),1603(11))]. given #758 (F,wt=14): 2314 x v (y v (((y ^ z) v x)' v u)) = 1. [para(212(a,1),108(a,1,1)),rewrite(62(8),1712(11))]. given #759 (T,wt=14): 2388 x v (y v ((y v (x ^ z))' v u)) = 1. [para(501(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #760 (T,wt=14): 2393 x v (y v ((y v (z ^ x))' v u)) = 1. [para(501(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #761 (A,wt=32): 337 x v (y v z) != 1 | (x v y) ^ (z v ((y v z) ^ u)) != 0 | (x v y)' = z v ((y v z) ^ u). [para(23(a,1),35(a,1,2))]. given #762 (F,wt=14): 2430 x v (y v (z v (u v (u v x)'))) = 1. [para(3(a,1),505(a,1,2))]. given #763 (F,wt=14): 2432 x v (y v (z v (z v (x ^ u))')) = 1. [para(505(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #764 (T,wt=14): 2437 x v (y v (z v (z v (u ^ x))')) = 1. [para(505(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #765 (T,wt=14): 2445 x v (y v (y v (z ^ (x ^ u)))') = 1. [para(17(a,1),507(a,1,2,2,1,2))]. given #766 (A,wt=27): 338 x v (y v (z ^ ((x v y) ^ z)')) != 1 | z ^ ((x v y) ^ z)' = (x v y)'. [para(32(a,1),35(b,1)),flip(c),xx(b)]. given #767 (F,wt=14): 2453 x v (y v (z v (z v (y v x))')) = 1. [para(103(a,1),507(a,1,2,2,1,2)),rewrite(3(6))]. given #768 (F,wt=14): 2454 x v ((x v (y ^ z))' v (u v y)) = 1. [para(507(a,1),104(a,1,1)),rewrite(3(7),62(8),507(11))]. given #769 (T,wt=14): 2456 x v (y v ((x v (y ^ z))' v u)) = 1. [para(507(a,1),108(a,1,1)),rewrite(62(8),675(11))]. given #770 (T,wt=14): 2462 x ^ (y ^ (z ^ ((z ^ x)' ^ u))) = 0. [para(511(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #771 (A,wt=23): 339 (x v y) ^ (z v (y' v u)) != 0 | (x v y)' = z v (y' v u). [para(102(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #772 (F,wt=14): 2464 x ^ (y ^ ((y ^ (x v z))' ^ u)) = 0. [para(511(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #773 (F,wt=14): 2469 x ^ (y ^ ((y ^ (z v x))' ^ u)) = 0. [para(511(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #774 (T,wt=14): 2473 (x v y)' ^ (((x ^ z) v y) ^ u) = 0. [para(182(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #775 (T,wt=14): 2480 x ^ (y ^ (z ^ (u ^ (u ^ x)'))) = 0. [para(5(a,1),515(a,1,2))]. given #776 (A,wt=19): 340 (x v y) ^ (x' v z) != 0 | (x v y)' = x' v z. [para(102(a,1),35(a,1)),xx(a)]. given #777 (F,wt=14): 2482 x ^ (y ^ (z ^ (z ^ (x v u))')) = 0. [para(515(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #778 (F,wt=14): 2487 x ^ (y ^ (z ^ (z ^ (u v x))')) = 0. [para(515(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #779 (T,wt=14): 2491 x ^ ((y ^ x)' ^ (z ^ (u ^ y))) = 0. [para(113(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6),5(5))]. given #780 (T,wt=14): 2492 x ^ (y ^ ((z ^ x)' ^ (u ^ z))) = 0. [para(119(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6),5(5))]. given #781 (A,wt=27): 341 x v (y v (z ^ ((x v y)' ^ u))) != 1 | z ^ ((x v y)' ^ u) = (x v y)'. [para(115(a,1),35(b,1)),flip(c),xx(b)]. given #782 (F,wt=14): 2493 x ^ (((y ^ x) v z)' ^ (u ^ y)) = 0. [para(134(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #783 (F,wt=14): 2494 x ^ ((y v (z ^ x))' ^ (u ^ z)) = 0. [para(139(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #784 (T,wt=14): 2495 x ^ (((y v z) ^ x)' ^ (u ^ y)) = 0. [para(227(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #785 (T,wt=14): 2496 (x v (y v z))' ^ (u ^ (v ^ y)) = 0. [para(256(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #786 (A,wt=23): 343 (x v y) ^ (z v (u v y')) != 0 | (x v y)' = z v (u v y'). [para(117(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #787 (F,wt=14): 2497 (x ^ y)' ^ (z ^ (y ^ (u ^ x))) = 0. [para(294(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6),5(5))]. given #788 (F,wt=14): 2498 (x v (y v z))' ^ (u ^ (v ^ z)) = 0. [para(351(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #789 (T,wt=14): 2541 x ^ (y ^ (y ^ (z v (x v u)))') = 0. [para(15(a,1),517(a,1,2,2,1,2))]. given #790 (T,wt=14): 2550 x ^ ((x ^ (y v z))' ^ (u ^ y)) = 0. [para(517(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #791 (A,wt=19): 344 (x v y) ^ (z v x') != 0 | (x v y)' = z v x'. [para(117(a,1),35(a,1)),xx(a)]. given #792 (F,wt=14): 2556 (x ^ y)' v (z v (u v (v v x))) = 1. [para(183(a,1),522(a,1,2,2,2))]. given #793 (F,wt=14): 2557 (x ^ y)' v (z v (u v (v v y))) = 1. [para(814(a,1),522(a,1,2,2,2))]. given #794 (T,wt=14): 2564 (x v y)' ^ (z ^ (u ^ (v ^ x))) = 0. [para(145(a,1),572(a,1,2,2,2))]. given #795 (T,wt=14): 2566 (x v y)' ^ (z ^ (u ^ (v ^ y))) = 0. [para(761(a,1),572(a,1,2,2,2))]. given #796 (A,wt=27): 345 x v (y v (z ^ (u ^ (x v y)'))) != 1 | z ^ (u ^ (x v y)') = (x v y)'. [para(120(a,1),35(b,1)),flip(c),xx(b)]. given #797 (F,wt=14): 2568 (x v y)' ^ (z ^ (u ^ (y v x))) = 0. [para(103(a,1),572(a,1,2,2,2))]. given #798 (F,wt=14): 2584 (x ^ y)' v (z v (u v (y ^ x))) = 1. [para(243(a,1),578(a,1,2,2,2))]. given #799 (T,wt=14): 2600 (x ^ (y ^ z))' v (u v (y v v)) = 1. [para(583(a,1),3(a,1,1)),rewrite(73(2),3(6)),flip(a)]. given #800 (T,wt=14): 2611 (x ^ (y ^ z))' v (u v (z v v)) = 1. [para(145(a,1),583(a,1,1,1,2))]. given #801 (A,wt=27): 346 x v (y v ((x v (y v z))' ^ u)) != 1 | (x v (y v z))' ^ u = (x v y)'. [para(130(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)]. given #802 (F,wt=14): 2613 (x ^ y) v (z ^ (y ^ (x ^ u)))' = 1. [para(243(a,1),583(a,1,2)),rewrite(5(2),2(6))]. given #803 (F,wt=14): 2617 (x ^ (y v z))' v (u v (z v y)) = 1. [para(103(a,1),583(a,1,1,1,2))]. given #804 (T,wt=14): 2641 (x ^ y) v (z ^ (u ^ (y ^ x)))' = 1. [para(243(a,1),585(a,1,2)),rewrite(2(6))]. given #805 (T,wt=14): 2677 (x v (y v z))' ^ (u ^ (y ^ v)) = 0. [para(600(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. given #806 (A,wt=27): 347 x v (y v (z ^ (x v (y v u))')) != 1 | z ^ (x v (y v u))' = (x v y)'. [para(131(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)]. given #807 (F,wt=14): 2687 (x v y) ^ (z v (y v (x v u)))' = 0. [para(157(a,1),600(a,1,2)),rewrite(3(2),4(6))]. given #808 (F,wt=14): 2689 (x v (y v z))' ^ (u ^ (z ^ v)) = 0. [para(183(a,1),600(a,1,1,1,2))]. given #809 (T,wt=14): 2704 (x v y)' ^ (z ^ (u ^ (y ^ v))) = 0. [para(79(a,1),601(a,1,1,1,2))]. given #810 (T,wt=14): 2716 (x v y) ^ (z v (u v (y v x)))' = 0. [para(157(a,1),601(a,1,2)),rewrite(4(6))]. given #811 (A,wt=19): 348 (x v y') ^ (z v y) != 0 | (x v y')' = z v y. [para(283(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #812 (F,wt=14): 2722 (x v (y ^ z))' ^ (u ^ (z ^ y)) = 0. [para(243(a,1),601(a,1,1,1,2))]. given #813 (F,wt=14): 2739 (x v y)' v (z v (y v (x v u))) = 1. [para(103(a,1),606(a,1,1,1)),rewrite(3(4))]. given #814 (T,wt=14): 2752 (x ^ (y ^ z))' v (u v (y ^ x)) = 1. [para(243(a,1),607(a,1,2,2)),rewrite(5(2))]. given #815 (T,wt=14): 2756 (x v y)' v (z v (u v (y v x))) = 1. [para(103(a,1),607(a,1,1,1))]. given #816 (A,wt=27): 349 x v (y v (z v (x v (y v u)))') != 1 | (z v (x v (y v u)))' = (x v y)'. [para(136(a,1),35(b,1)),rewrite(3(2),3(15)),flip(c),xx(b)]. given #817 (F,wt=14): 2794 (x ^ (y ^ z))' v (u v (z ^ y)) = 1. [para(243(a,1),639(a,1,2,2))]. given #818 (F,wt=14): 2805 (x v y)' ^ (z ^ (u ^ (x ^ v))) = 0. [para(5(a,1),649(a,1,2))]. given #819 (T,wt=14): 2813 (x v (y v z))' ^ (u ^ (y v x)) = 0. [para(103(a,1),649(a,1,2,2)),rewrite(3(2))]. given #820 (T,wt=14): 2846 (x ^ y)' ^ (z ^ (y ^ (x ^ u))) = 0. [para(243(a,1),657(a,1,1,1)),rewrite(5(4))]. given #821 (A,wt=19): 353 x v (y v (z v x))' != 1 | (y v (z v x))' = x'. [para(137(a,1),10(b,1)),flip(c),xx(b)]. given #822 (F,wt=14): 2850 (x v (y v z))' ^ (u ^ (z v y)) = 0. [para(103(a,1),657(a,1,2,2))]. given #823 (F,wt=14): 2871 (x ^ y)' ^ (z ^ (u ^ (y ^ x))) = 0. [para(243(a,1),658(a,1,1,1))]. given #824 (T,wt=14): 2892 (x v (y ^ z)) ^ (x v (z v u))' = 0. [para(145(a,1),672(a,1,1,2))]. given #825 (T,wt=14): 2899 (x v y)' ^ ((x v (y ^ z)) ^ u) = 0. [para(672(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #826 (A,wt=16): 357 (x v ((y v x) ^ z)) ^ (u v (y v x))' = 0. [para(23(a,1),137(a,1,2,1,2))]. given #827 (F,wt=14): 2903 x v (y v (z v (x v (z ^ u))')) = 1. [para(675(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #828 (F,wt=14): 2904 x v (y v ((x ^ z) v (y ^ u))') = 1. [para(675(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #829 (T,wt=14): 2909 x v (y v ((z ^ x) v (y ^ u))') = 1. [para(675(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #830 (T,wt=14): 2910 x v (y v (z v (x v (u ^ y))')) = 1. [para(145(a,1),675(a,1,2,2,1,2)),rewrite(3(5))]. given #831 (A,wt=27): 359 x v (y v (z v (u v (x v y)))') != 1 | (z v (u v (x v y)))' = (x v y)'. [para(137(a,1),35(b,1)),flip(c),xx(b)]. given #832 (F,wt=14): 2911 x v (y v (z v (x v (u ^ z))')) = 1. [para(761(a,1),675(a,1,2,2,1,2)),rewrite(3(5))]. given #833 (F,wt=14): 2913 x v ((y v (x ^ z))' v (u v y)) = 1. [para(675(a,1),104(a,1,1)),rewrite(3(7),62(8),675(11))]. given #834 (T,wt=14): 2930 (x ^ (y v z)) v (x ^ (z ^ u))' = 1. [para(183(a,1),741(a,1,1,2))]. given #835 (T,wt=14): 2935 (x ^ y)' v ((x ^ (y v z)) v u) = 1. [para(741(a,1),103(a,1,1)),rewrite(62(8),2918(11))]. given #836 (A,wt=19): 361 x v ((y v x)' ^ z) != 1 | (y v x)' ^ z = x'. [para(138(a,1),10(b,1)),flip(c),xx(b)]. given #837 (F,wt=14): 2950 x ^ (y ^ ((x ^ (y v z))' ^ u)) = 0. [para(743(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. given #838 (F,wt=14): 2952 x ^ (y ^ (z ^ (x ^ (z v u))')) = 0. [para(743(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #839 (T,wt=14): 2953 x ^ (y ^ ((x v z) ^ (y v u))') = 0. [para(743(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #840 (T,wt=14): 2958 x ^ (y ^ ((z v x) ^ (y v u))') = 0. [para(743(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #841 (A,wt=16): 365 (x v ((y v x) ^ z)) ^ ((y v x)' ^ u) = 0. [para(23(a,1),138(a,1,2,1,1))]. given #842 (F,wt=14): 2959 x ^ (y ^ (z ^ (x ^ (u v y))')) = 0. [para(183(a,1),743(a,1,2,2,1,2)),rewrite(5(5))]. given #843 (F,wt=14): 2961 x ^ (y ^ (z ^ (x ^ (u v z))')) = 0. [para(814(a,1),743(a,1,2,2,1,2)),rewrite(5(5))]. given #844 (T,wt=14): 2964 x ^ ((y ^ (x v z))' ^ (u ^ y)) = 0. [para(743(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #845 (T,wt=14): 2967 ((x v (y v z)) ^ u) v (z ^ u)' = 1. [para(3(a,1),764(a,1,1,1))]. given #846 (A,wt=27): 366 x v (y v ((z v (x v y))' ^ u)) != 1 | (z v (x v y))' ^ u = (x v y)'. [para(138(a,1),35(b,1)),flip(c),xx(b)]. given #847 (F,wt=14): 2979 ((x v y) ^ (z v (y v u))) v y' = 1. [para(67(a,1),764(a,1,2,1))]. given #848 (F,wt=14): 2980 ((x v y) ^ (z v (u v y))) v y' = 1. [para(88(a,1),764(a,1,2,1))]. given #849 (T,wt=14): 2995 (x ^ (y ^ z)) v (y ^ (x ^ z))' = 1. [para(243(a,1),764(a,1,1,1)),rewrite(5(2),5(4))]. given #850 (T,wt=14): 3000 (x ^ y)' v (((z v x) ^ y) v u) = 1. [para(764(a,1),103(a,1,1)),rewrite(62(8),2966(11))]. given #851 (A,wt=19): 368 x v (y ^ (z v x)') != 1 | y ^ (z v x)' = x'. [para(142(a,1),10(b,1)),flip(c),xx(b)]. given #852 (F,wt=14): 3009 x ^ (y ^ ((z v (u v x)) ^ y)') = 0. [para(3(a,1),768(a,1,2,2,1,1))]. given #853 (F,wt=14): 3034 x ^ (((y v z) ^ x)' ^ (u ^ z)) = 0. [para(768(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #854 (T,wt=14): 3036 x ^ (y ^ (y ^ (z v (u v x)))') = 0. [para(3(a,1),775(a,1,2,2,1,2))]. given #855 (T,wt=14): 3052 x ^ (y ^ (z ^ (z ^ (y ^ x))')) = 0. [para(243(a,1),775(a,1,2,2,1,2)),rewrite(5(6))]. Low Water (displace): id=11715, wt=34 Low Water (displace): id=11738, wt=33 given #856 (A,wt=16): 371 (x v ((y v x) ^ z)) ^ (u ^ (y v x)') = 0. [para(23(a,1),142(a,1,2,2,1))]. given #857 (F,wt=14): 3059 x ^ ((x ^ (y v z))' ^ (u ^ z)) = 0. [para(775(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. Low Water (displace): id=12263, wt=31 given #858 (F,wt=14): 3113 x ^ (y ^ (x ^ ((x ^ y) v z))') = 0. [para(124(a,1),225(a,1))]. given #859 (T,wt=14): 3189 (x ^ y)' v ((x ^ (z v y)) v u) = 1. [para(789(a,1),103(a,1,1)),rewrite(62(8),3165(11))]. given #860 (T,wt=14): 3199 x ^ (y ^ ((x ^ (z v y))' ^ u)) = 0. [para(793(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. Low Water (displace): id=12724, wt=30 given #861 (A,wt=27): 372 x v (y v (z ^ (u v (x v y))')) != 1 | z ^ (u v (x v y))' = (x v y)'. [para(142(a,1),35(b,1)),flip(c),xx(b)]. given #862 (F,wt=14): 3201 x ^ (y ^ ((x v z) ^ (u v y))') = 0. [para(793(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #863 (F,wt=14): 3209 x ^ (y ^ ((z v x) ^ (u v y))') = 0. [para(793(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. Low Water (displace): id=13132, wt=29 given #864 (T,wt=14): 3219 x ^ ((y ^ (z v x))' ^ (u ^ y)) = 0. [para(793(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6),5(6))]. given #865 (T,wt=14): 3225 ((x ^ (y ^ z)) v u) ^ (z v u)' = 0. [para(5(a,1),812(a,1,1,1))]. given #866 (A,wt=19): 375 x ^ ((x ^ y)' v z) != 0 | (x ^ y)' v z = x'. [para(180(a,1),10(a,1)),flip(c),xx(a)]. given #867 (F,wt=14): 3234 ((x ^ y) v (z ^ (y ^ u))) ^ y' = 0. [para(79(a,1),812(a,1,2,1))]. Low Water (displace): id=13072, wt=28 given #868 (F,wt=14): 3236 ((x ^ y) v (z ^ (u ^ y))) ^ y' = 0. [para(96(a,1),812(a,1,2,1))]. given #869 (T,wt=14): 3257 ((x ^ y) v z) ^ (y v (z v u))' = 0. [para(812(a,1),106(a,1,2)),rewrite(4(4),76(4)),flip(a)]. Low Water (displace): id=13702, wt=27 given #870 (T,wt=14): 3260 (x v y)' ^ (((z ^ x) v y) ^ u) = 0. [para(812(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #871 (A,wt=19): 377 x ^ ((x ^ y)' v z) != 0 | ((x ^ y)' v z)' = x. [para(180(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #872 (F,wt=14): 3266 x v (y v ((z ^ (u ^ x)) v y)') = 1. [para(5(a,1),817(a,1,2,2,1,1))]. given #873 (F,wt=14): 3286 x v (((y ^ z) v x)' v (u v z)) = 1. [para(817(a,1),104(a,1,1)),rewrite(3(7),62(8),817(11))]. given #874 (T,wt=14): 3290 x v (y v (((z ^ y) v x)' v u)) = 1. [para(817(a,1),108(a,1,1)),rewrite(62(8),2394(11))]. given #875 (T,wt=14): 3336 x v (y v (y v (z ^ (u ^ x)))') = 1. [para(5(a,1),825(a,1,2,2,1,2))]. given #876 (A,wt=23): 378 (x v y) ^ ((y ^ z)' v u) != 0 | (x v y)' = (y ^ z)' v u. [para(180(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #877 (F,wt=14): 3353 x v ((x v (y ^ z))' v (u v z)) = 1. [para(825(a,1),104(a,1,1)),rewrite(3(7),62(8),825(11))]. given #878 (F,wt=14): 3358 x v (y v ((x v (z ^ y))' v u)) = 1. [para(825(a,1),108(a,1,1)),rewrite(62(8),927(11))]. given #879 (T,wt=14): 3392 (x v y)' ^ ((x v (z ^ y)) ^ u) = 0. [para(923(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #880 (T,wt=14): 3399 x v (y v ((x ^ z) v (u ^ y))') = 1. [para(927(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. Low Water (displace): id=14858, wt=26 given #881 (A,wt=20): 379 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | x' = y ^ z. [para(5(a,1),36(b,1))]. given #882 (F,wt=14): 3407 x v (y v ((z ^ x) v (u ^ y))') = 1. [para(927(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #883 (F,wt=14): 3413 x v ((y v (z ^ x))' v (u v y)) = 1. [para(927(a,1),104(a,1,1)),rewrite(3(7),62(8),927(11))]. given #884 (T,wt=14): 3425 x v (y v (z ^ (y v (x ^ u)))') = 1. [para(967(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #885 (T,wt=14): 3430 x v (y v (z ^ (y v (u ^ x)))') = 1. [para(967(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #886 (A,wt=20): 380 x v (y v z) != 1 | (x v z) ^ y != 0 | y' = x v z. [para(15(a,1),36(a,1))]. given #887 (F,wt=14): 3467 x ^ ((x v y) ^ (z v (x v u)))' = 0. [para(127(a,1),227(a,1))]. given #888 (F,wt=14): 3483 x ^ (y ^ ((z v (y v u)) ^ x)') = 0. [para(127(a,1),515(a,1,2))]. given #889 (T,wt=14): 3486 x ^ ((y v (x v z)) ^ (x v u))' = 0. [para(127(a,1),517(a,1))]. given #890 (T,wt=14): 3499 x ^ ((y v x) ^ (z v (x v u)))' = 0. [para(127(a,1),768(a,1))]. Low Water (keep): wt=19, part=0.50, limit=19 given #891 (A,wt=20): 381 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z. [para(17(a,1),36(b,1))]. given #892 (F,wt=14): 3501 x ^ ((y v (x v z)) ^ (u v x))' = 0. [para(127(a,1),775(a,1))]. given #893 (F,wt=14): 3517 x v (y v (z v (y v (x ^ u))')) = 1. [para(969(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #894 (T,wt=14): 3522 x v (y v (z v (y v (u ^ x))')) = 1. [para(969(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #895 (T,wt=14): 3527 (x v y)' ^ (z ^ ((y v x) ^ u)) = 0. [para(970(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. given #896 (A,wt=22): 382 x v (y v z) != 1 | x v y != 0 | (x v (y v z))' = x v y. [para(19(a,1),36(b,1)),rewrite(2(4),15(4),15(3),3(2),146(3),58(3))]. given #897 (F,wt=14): 3551 (x v y) ^ ((y v (x v z))' ^ u) = 0. [para(972(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #898 (F,wt=14): 3554 (x v y) ^ (z ^ (y v (x v u))') = 0. [para(972(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #899 (T,wt=14): 3557 ((x ^ y) v z) ^ (z v (u v x))' = 0. [para(183(a,1),972(a,1,2,1,2))]. given #900 (T,wt=14): 3559 ((x ^ y) v z) ^ (z v (u v y))' = 0. [para(814(a,1),972(a,1,2,1,2))]. Low Water (displace): id=15497, wt=25 given #901 (A,wt=15): 383 x v (x' ^ y) != 1 | (x' ^ y)' = x. [para(77(a,1),36(b,1)),rewrite(2(3)),xx(b)]. given #902 (F,wt=14): 3582 x ^ (y ^ (z ^ (x ^ (y v u))')) = 0. [para(119(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #903 (F,wt=14): 3596 x ^ (y ^ (((y v z) ^ x)' ^ u)) = 0. [para(511(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #904 (T,wt=14): 3598 x ^ (y ^ ((y v z) ^ (x v u))') = 0. [para(517(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #905 (T,wt=14): 3609 x ^ (y ^ ((y v z) ^ (u v x))') = 0. [para(775(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #906 (A,wt=15): 384 x v (y ^ x') != 1 | (y ^ x')' = x. [para(86(a,1),36(b,1)),rewrite(2(3)),xx(b)]. given #907 (F,wt=14): 3622 (x v y) ^ ((z v (y v x))' ^ u) = 0. [para(973(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #908 (F,wt=14): 3625 (x v y) ^ (z ^ (u v (y v x))') = 0. [para(973(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #909 (T,wt=14): 3635 (x v y) ^ (z ^ ((y v x)' ^ u)) = 0. [para(977(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #910 (T,wt=14): 3640 (x v y) ^ ((y v (z v x))' ^ u) = 0. [para(977(a,1),106(a,1,2)),rewrite(4(3),76(3),3(4)),flip(a)]. given #911 (A,wt=22): 385 x v ((x v y) ^ z) != 1 | x ^ z != 0 | ((x v y) ^ z)' = x. [para(20(a,1),36(b,1)),rewrite(2(3))]. given #912 (F,wt=14): 3644 (x v y) ^ (z ^ (u ^ (y v x)')) = 0. [para(5(a,1),979(a,1,2))]. given #913 (F,wt=14): 3651 (x v y) ^ (z ^ (y v (u v x))') = 0. [para(979(a,1),106(a,1,2)),rewrite(4(3),76(3),3(4)),flip(a)]. given #914 (T,wt=14): 3657 x ^ (y ^ (z ^ (u v (z ^ x))')) = 0. [para(1214(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #915 (T,wt=14): 3659 x ^ (y ^ (z v (y ^ (x v u)))') = 0. [para(1214(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #916 (A,wt=26): 388 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | (y ^ ((x ^ y) v z))' = x. [para(21(a,1),36(b,1)),rewrite(2(4))]. given #917 (F,wt=14): 3664 x ^ (y ^ (z v (y ^ (u v x)))') = 0. [para(1214(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #918 (F,wt=14): 3671 x ^ (y ^ (z v ((y v u) ^ x))') = 0. [para(1214(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #919 (T,wt=14): 3746 x ^ (y ^ (z ^ (u ^ (z ^ x)'))) = 0. [para(1215(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #920 (T,wt=14): 3748 x ^ (y ^ (z ^ (y ^ (x v u))')) = 0. [para(1215(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #921 (A,wt=18): 389 x v (y v z) != 1 | 0 != y | (x v (y v z))' = y. [para(67(a,1),36(b,1)),rewrite(2(3),146(3)),flip(b)]. given #922 (F,wt=14): 3753 x ^ (y ^ (z ^ (y ^ (u v x))')) = 0. [para(1215(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #923 (F,wt=14): 3760 x ^ (y ^ (z ^ ((y v u) ^ x)')) = 0. [para(1215(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #924 (T,wt=14): 3762 (x ^ y)' v (z v ((y ^ x) v u)) = 1. [para(1217(a,1),3(a,1,1)),rewrite(73(2),3(6)),flip(a)]. given #925 (T,wt=14): 3774 (x ^ y) v ((y ^ (x ^ z))' v u) = 1. [para(1218(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #926 (A,wt=18): 390 x v (y v z) != 1 | 0 != z | (x v (y v z))' = z. [para(88(a,1),36(b,1)),rewrite(2(3),156(3)),flip(b)]. given #927 (F,wt=14): 3778 (x ^ y) v (z v (y ^ (x ^ u))') = 1. [para(1218(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #928 (F,wt=14): 3780 (x ^ y) v (y ^ (z ^ (x ^ u)))' = 1. [para(17(a,1),1218(a,1,2,1,2))]. given #929 (T,wt=14): 3783 ((x v y) ^ z) v (z ^ (u ^ x))' = 1. [para(145(a,1),1218(a,1,2,1,2))]. given #930 (T,wt=14): 3784 ((x v y) ^ z) v (z ^ (u ^ y))' = 1. [para(761(a,1),1218(a,1,2,1,2))]. Low Water (displace): id=16332, wt=24 given #931 (A,wt=19): 391 x v (y ^ (x ^ y)') != 1 | (y ^ (x ^ y)')' = x. [para(32(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #932 (F,wt=14): 3787 ((x v y) ^ z) v (z ^ (y v x))' = 1. [para(103(a,1),1218(a,1,2,1,2))]. given #933 (F,wt=14): 3793 (x ^ y) v ((z ^ (y ^ x))' v u) = 1. [para(1219(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #934 (T,wt=14): 3797 (x ^ y) v (z v (u ^ (y ^ x))') = 1. [para(1219(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #935 (T,wt=14): 3805 (x ^ (y v (z v u))) v (z ^ x)' = 1. [para(127(a,1),1219(a,1,2,1))]. given #936 (A,wt=19): 392 x v (y ^ (x' ^ z)) != 1 | (y ^ (x' ^ z))' = x. [para(115(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #937 (F,wt=14): 3828 (x ^ y) v (z v (u v (y ^ x)')) = 1. [para(3(a,1),1225(a,1,2))]. given #938 (F,wt=14): 3838 (x v y) ^ (y v (z v (u v x)))' = 0. [para(3(a,1),1469(a,1,2,1,2))]. given #939 (T,wt=14): 3841 ((x ^ (y ^ z)) v u) ^ (u v y)' = 0. [para(79(a,1),1469(a,1,2,1,2))]. given #940 (T,wt=14): 3843 ((x ^ (y ^ z)) v u) ^ (u v z)' = 0. [para(96(a,1),1469(a,1,2,1,2))]. given #941 (A,wt=19): 393 x v (y ^ (z ^ x')) != 1 | (y ^ (z ^ x'))' = x. [para(120(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #942 (F,wt=10): 23753 x ^ y != 1 | y ^ x = 1. [para(236(a,1),393(a,1)),rewrite(222(7),75(5)),flip(b)]. given #943 (F,wt=10): 23756 x v y != 1 | y v x = 1. [para(157(a,1),23753(a,1)),rewrite(157(6))]. given #944 (T,wt=14): 3854 ((x ^ y) v z) ^ (z v (y ^ x))' = 0. [para(243(a,1),1469(a,1,2,1,2))]. given #945 (T,wt=14): 3871 ((x ^ y) v z) ^ ((z v x)' ^ u) = 0. [para(1476(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. Low Water (keep): wt=18, part=0.50, limit=18 given #946 (A,wt=19): 394 x v ((x v y)' ^ z) != 1 | ((x v y)' ^ z)' = x. [para(130(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #947 (F,wt=14): 3875 ((x ^ y) v z) ^ (u ^ (z v x)') = 0. [para(1476(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #948 (F,wt=14): 3879 ((x ^ y) v z) ^ (z v (y v u))' = 0. [para(145(a,1),1476(a,1,1,1))]. given #949 (T,wt=14): 3884 (x v (y v z)) ^ (z v (y v x))' = 0. [para(103(a,1),1476(a,1,1,1)),rewrite(3(2))]. given #950 (T,wt=14): 3887 (x v y)' ^ (((y ^ z) v x) ^ u) = 0. [para(1476(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #951 (A,wt=19): 395 x v (y ^ (x v z)') != 1 | (y ^ (x v z)')' = x. [para(131(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #952 (F,wt=14): 3888 (x v y)' ^ (z ^ ((y ^ u) v x)) = 0. [para(1476(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #953 (F,wt=14): 3896 ((x ^ y) v z) ^ ((z v y)' ^ u) = 0. [para(1479(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #954 (T,wt=14): 3900 ((x ^ y) v z) ^ (u ^ (z v y)') = 0. [para(1479(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #955 (T,wt=14): 3920 (x v y)' ^ (((z ^ y) v x) ^ u) = 0. [para(1479(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #956 (A,wt=15): 397 (x ^ y) v y' != 1 | (x ^ y)' = y'. [para(284(a,1),36(b,1)),xx(b)]. given #957 (F,wt=14): 3921 (x v y)' ^ (z ^ ((u ^ y) v x)) = 0. [para(1479(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #958 (F,wt=14): 3930 x ^ (y ^ (((y ^ x) v z)' ^ u)) = 0. [para(1503(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. given #959 (T,wt=14): 3933 x ^ (y ^ (z v ((y ^ x) v u))') = 0. [para(15(a,1),1503(a,1,2,2,1))]. given #960 (T,wt=14): 3934 x ^ (y ^ (z ^ ((z ^ x) v u)')) = 0. [para(1503(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #961 (A,wt=17): 398 x v (y v (x v z))' != 1 | y v (x v z) = x. [para(136(a,1),36(b,1)),rewrite(2(4),265(13)),xx(b)]. given #962 (F,wt=14): 3936 x ^ (y ^ ((y ^ (x v z)) v u)') = 0. [para(1503(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #963 (F,wt=14): 3941 x ^ (y ^ ((y ^ (z v x)) v u)') = 0. [para(1503(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #964 (T,wt=14): 3947 x ^ (y ^ (((y v z) ^ x) v u)') = 0. [para(1503(a,1),128(a,1,2)),rewrite(85(2)),flip(a)]. given #965 (T,wt=14): 3956 (x v (y ^ z)) ^ ((y v x)' ^ u) = 0. [para(1545(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. Low Water (displace): id=16954, wt=23 given #966 (A,wt=17): 399 x v (y v (z v x))' != 1 | y v (z v x) = x. [para(137(a,1),36(b,1)),rewrite(2(4),265(13)),xx(b)]. given #967 (F,wt=14): 3960 (x v (y ^ z)) ^ (u ^ (y v x)') = 0. [para(1545(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #968 (F,wt=14): 3961 (x v (y ^ (z ^ u))) ^ (z v x)' = 0. [para(17(a,1),1545(a,1,1,2))]. given #969 (T,wt=14): 3962 ((x ^ (y ^ z)) v (y ^ u)) ^ y' = 0. [para(79(a,1),1545(a,1,2,1))]. given #970 (T,wt=14): 3964 ((x ^ (y ^ z)) v (z ^ u)) ^ z' = 0. [para(96(a,1),1545(a,1,2,1))]. given #971 (A,wt=19): 400 x v ((y v x)' ^ z) != 1 | ((y v x)' ^ z)' = x. [para(138(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #972 (F,wt=14): 3972 (x v (y ^ z)) ^ (z v (u v x))' = 0. [para(145(a,1),1545(a,1,1,2)),rewrite(3(4))]. given #973 (F,wt=14): 3976 (x v (y ^ z)) ^ (u v (z v x))' = 0. [para(761(a,1),1545(a,1,1,2)),rewrite(3(4))]. given #974 (T,wt=14): 3982 (x v y)' ^ ((y v (x ^ z)) ^ u) = 0. [para(1545(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #975 (T,wt=14): 3983 (x v y)' ^ (z ^ (y v (x ^ u))) = 0. [para(1545(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #976 (A,wt=19): 401 x v (y ^ (z v x)') != 1 | (y ^ (z v x)')' = x. [para(142(a,1),36(b,1)),rewrite(2(4)),xx(b)]. given #977 (F,wt=14): 4003 (x ^ y) v (y ^ (z ^ (u ^ x)))' = 1. [para(144(a,1),1218(a,1,2,1,2))]. given #978 (F,wt=14): 4004 (x v (y ^ (z ^ u))) ^ (u v x)' = 0. [para(144(a,1),1545(a,1,1,2))]. given #979 (T,wt=14): 4010 (x v y)' ^ ((z ^ (x ^ u)) v y) = 0. [para(17(a,1),1547(a,1,2,1))]. given #980 (T,wt=14): 4012 x' ^ ((x ^ y) v (z ^ (x ^ u))) = 0. [para(79(a,1),1547(a,1,1,1))]. given #981 (A,wt=19): 404 x ^ (y v (x ^ z)') != 0 | y v (x ^ z)' = x'. [para(181(a,1),10(a,1)),flip(c),xx(a)]. given #982 (F,wt=14): 4014 x' ^ ((x ^ y) v (z ^ (u ^ x))) = 0. [para(96(a,1),1547(a,1,1,1))]. given #983 (F,wt=14): 4022 (x v (y v z))' ^ ((u ^ x) v z) = 0. [para(145(a,1),1547(a,1,2,1)),rewrite(3(2))]. given #984 (T,wt=14): 4026 (x v (y v z))' ^ ((u ^ y) v z) = 0. [para(761(a,1),1547(a,1,2,1)),rewrite(3(2))]. given #985 (T,wt=14): 4030 (x v (y v z))' ^ ((x ^ u) v y) = 0. [para(1547(a,1),110(a,1,2)),rewrite(4(4),76(4)),flip(a)]. given #986 (A,wt=19): 406 x ^ (y v (x ^ z)') != 0 | (y v (x ^ z)')' = x. [para(181(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #987 (F,wt=14): 4032 (x v y)' ^ ((z ^ (u ^ x)) v y) = 0. [para(144(a,1),1547(a,1,2,1))]. given #988 (F,wt=14): 4036 ((x ^ y) v (x ^ z)) ^ (x' ^ u) = 0. [para(1549(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #989 (T,wt=14): 4038 ((x ^ y) v (x ^ z)) ^ (u ^ x') = 0. [para(1549(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #990 (T,wt=14): 4047 x' ^ (((x ^ y) v (x ^ z)) ^ u) = 0. [para(1549(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #991 (A,wt=23): 407 (x v y) ^ (z v (y ^ u)') != 0 | (x v y)' = z v (y ^ u)'. [para(181(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #992 (F,wt=14): 4048 x' ^ (y ^ ((x ^ z) v (x ^ u))) = 0. [para(1549(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #993 (F,wt=14): 4052 ((x ^ y) v (z ^ x)) ^ (x' ^ u) = 0. [para(1554(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #994 (T,wt=14): 4055 ((x ^ y) v (z ^ x)) ^ (u ^ x') = 0. [para(1554(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #995 (T,wt=14): 4056 ((x ^ (y ^ z)) v (u ^ y)) ^ y' = 0. [para(17(a,1),1554(a,1,1,1))]. given #996 (A,wt=19): 408 (x v y) ^ (x ^ z)' != 0 | (x v y)' = (x ^ z)'. [para(181(a,1),35(a,1)),xx(a)]. given #997 (F,wt=14): 4082 x' ^ (((x ^ y) v (z ^ x)) ^ u) = 0. [para(1554(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #998 (F,wt=14): 4083 x' ^ (y ^ ((x ^ z) v (u ^ x))) = 0. [para(1554(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #999 (T,wt=14): 4089 ((x ^ (y ^ z)) v (u ^ z)) ^ z' = 0. [para(144(a,1),1554(a,1,1,1))]. given #1000 (T,wt=14): 4095 x v (y v (z v ((z v x) ^ u)')) = 1. [para(1603(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1001 (A,wt=19): 412 x ^ (y ^ (x ^ z))' != 0 | (y ^ (x ^ z))' = x'. [para(189(a,1),10(a,1)),flip(c),xx(a)]. given #1002 (F,wt=14): 4097 x v (y v (z ^ ((y v x) ^ u))') = 1. [para(17(a,1),1603(a,1,2,2,1))]. given #1003 (F,wt=14): 4098 x v (y v ((y v (x ^ z)) ^ u)') = 1. [para(1603(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #1004 (T,wt=14): 4103 x v (y v ((y v (z ^ x)) ^ u)') = 1. [para(1603(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #1005 (T,wt=14): 4117 (x ^ y) v ((y ^ (z ^ x))' v u) = 1. [para(1613(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1006 (A,wt=17): 413 x ^ (y ^ (x ^ z))' != 0 | y ^ (x ^ z) = x. [para(189(a,1),34(a,1)),rewrite(4(7),265(13)),xx(a)]. given #1007 (F,wt=14): 4121 (x ^ y) v (z v (y ^ (u ^ x))') = 1. [para(1613(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1008 (F,wt=14): 4125 ((x v (y v z)) ^ u) v (u ^ y)' = 1. [para(67(a,1),1613(a,1,2,1,2))]. given #1009 (T,wt=14): 4126 ((x v (y v z)) ^ u) v (u ^ z)' = 1. [para(88(a,1),1613(a,1,2,1,2))]. given #1010 (T,wt=14): 4139 (x ^ (y ^ z))' v (u v (z ^ x)) = 1. [para(1613(a,1),104(a,1,1)),rewrite(62(8),1613(11))]. given #1011 (A,wt=23): 414 (x v y) ^ (z ^ (y ^ u))' != 0 | (x v y)' = (z ^ (y ^ u))'. [para(189(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #1012 (F,wt=14): 4158 ((x v y) ^ z) v ((z ^ x)' v u) = 1. [para(1620(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1013 (F,wt=14): 4161 ((x v y) ^ z) v (u v (z ^ x)') = 1. [para(1620(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1014 (T,wt=14): 4168 ((x v y) ^ z) v (z ^ (y ^ u))' = 1. [para(183(a,1),1620(a,1,1,1))]. given #1015 (T,wt=14): 4171 (x ^ y)' v (((y v z) ^ x) v u) = 1. [para(1620(a,1),103(a,1,1)),rewrite(62(8),4157(11))]. given #1016 (A,wt=19): 417 x ^ ((y ^ x)' v z) != 0 | (y ^ x)' v z = x'. [para(190(a,1),10(a,1)),flip(c),xx(a)]. given #1017 (F,wt=14): 4172 (x ^ y)' v (z v ((y v u) ^ x)) = 1. [para(1620(a,1),104(a,1,1)),rewrite(62(8),1620(11))]. given #1018 (F,wt=14): 4181 ((x v y) ^ z) v ((z ^ y)' v u) = 1. [para(1622(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1019 (T,wt=14): 4184 ((x v y) ^ z) v (u v (z ^ y)') = 1. [para(1622(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1020 (T,wt=14): 4198 (x ^ (y ^ z)) v (z ^ (y ^ x))' = 1. [para(243(a,1),1622(a,1,1,1)),rewrite(5(2))]. given #1021 (A,wt=16): 421 (x ^ ((y ^ x) v z)) v ((y ^ x)' v u) = 1. [para(21(a,1),190(a,1,2,1,1))]. given #1022 (F,wt=14): 4202 (x ^ y)' v (((z v y) ^ x) v u) = 1. [para(1622(a,1),103(a,1,1)),rewrite(62(8),4180(11))]. given #1023 (F,wt=14): 4203 (x ^ y)' v (z v ((u v y) ^ x)) = 1. [para(1622(a,1),104(a,1,1)),rewrite(62(8),1622(11))]. given #1024 (T,wt=14): 4209 (x ^ y)' v ((z v (x v u)) ^ y) = 1. [para(15(a,1),1664(a,1,2,1))]. given #1025 (T,wt=14): 4216 x' v ((x v y) ^ (z v (x v u))) = 1. [para(67(a,1),1664(a,1,1,1))]. given #1026 (A,wt=19): 422 x ^ ((y ^ x)' v z) != 0 | ((y ^ x)' v z)' = x. [para(190(a,1),34(a,1)),rewrite(4(7)),xx(a)]. given #1027 (F,wt=14): 4217 x' v ((x v y) ^ (z v (u v x))) = 1. [para(88(a,1),1664(a,1,1,1))]. given #1028 (F,wt=14): 4225 (x ^ (y ^ z))' v ((u v x) ^ z) = 1. [para(183(a,1),1664(a,1,2,1)),rewrite(5(2))]. given #1029 (T,wt=14): 4227 (x ^ (y ^ z))' v ((u v y) ^ z) = 1. [para(814(a,1),1664(a,1,2,1)),rewrite(5(2))]. given #1030 (T,wt=14): 4251 (x ^ ((x ^ y) v z)) v (y ^ x)' = 1. [para(147(a,1),186(a,1,2,1))]. given #1031 (A,wt=23): 423 (x v y) ^ ((z ^ y)' v u) != 0 | (x v y)' = (z ^ y)' v u. [para(190(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #1032 (F,wt=14): 4253 x ^ (y ^ (y ^ ((y ^ x) v z))') = 0. [para(147(a,1),284(a,1,2)),rewrite(4(6),5(6))]. given #1033 (F,wt=14): 4277 (x ^ ((y ^ x) v z)) v (x ^ y)' = 1. [para(147(a,1),195(a,1,2,1))]. given #1034 (T,wt=14): 4291 ((x ^ y) v z)' ^ (u ^ (y ^ x)) = 0. [para(147(a,1),592(a,1,2,2))]. given #1035 (T,wt=14): 4320 (x ^ (y v z)) v ((y ^ x)' v u) = 1. [para(1666(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1036 (A,wt=19): 426 x ^ (y ^ (z ^ x))' != 0 | (y ^ (z ^ x))' = x'. [para(192(a,1),10(a,1)),flip(c),xx(a)]. given #1037 (F,wt=14): 4324 (x ^ (y v z)) v (u v (y ^ x)') = 1. [para(1666(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1038 (F,wt=14): 4328 ((x v (y v z)) ^ (y v u)) v y' = 1. [para(67(a,1),1666(a,1,2,1))]. given #1039 (T,wt=14): 4329 ((x v (y v z)) ^ (z v u)) v z' = 1. [para(88(a,1),1666(a,1,2,1))]. given #1040 (T,wt=14): 4338 (x ^ (y v z)) v (z ^ (u ^ x))' = 1. [para(183(a,1),1666(a,1,1,2)),rewrite(5(4))]. given #1041 (A,wt=16): 431 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x))' = 1. [para(21(a,1),192(a,1,2,1,2))]. given #1042 (F,wt=14): 4340 (x ^ (y v z)) v (u ^ (z ^ x))' = 1. [para(814(a,1),1666(a,1,1,2)),rewrite(5(4))]. given #1043 (F,wt=14): 4344 (x ^ y)' v ((y ^ (x v z)) v u) = 1. [para(1666(a,1),103(a,1,1)),rewrite(62(8),4206(11))]. given #1044 (T,wt=14): 4346 (x ^ y)' v (z v (y ^ (x v u))) = 1. [para(1666(a,1),104(a,1,1)),rewrite(62(8),1666(11))]. given #1045 (T,wt=14): 4362 ((x v y) ^ (x v z)) v (x' v u) = 1. [para(1668(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1046 (A,wt=17): 432 x ^ (y ^ (z ^ x))' != 0 | y ^ (z ^ x) = x. [para(192(a,1),34(a,1)),rewrite(4(7),265(13)),xx(a)]. given #1047 (F,wt=14): 4364 ((x v y) ^ (x v z)) v (u v x') = 1. [para(1668(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1048 (F,wt=14): 4372 x' v (((x v y) ^ (x v z)) v u) = 1. [para(1668(a,1),103(a,1,1)),rewrite(62(8),4208(11))]. given #1049 (T,wt=14): 4373 x' v (y v ((x v z) ^ (x v u))) = 1. [para(1668(a,1),104(a,1,1)),rewrite(62(8),1668(11))]. given #1050 (T,wt=14): 4380 ((x v y) ^ (z v x)) v (x' v u) = 1. [para(1673(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1051 (A,wt=23): 433 (x v y) ^ (z ^ (u ^ y))' != 0 | (x v y)' = (z ^ (u ^ y))'. [para(192(a,1),35(a,1,2)),rewrite(82(2)),xx(a)]. given #1052 (F,wt=14): 4383 ((x v y) ^ (z v x)) v (u v x') = 1. [para(1673(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1053 (F,wt=14): 4384 ((x v (y v z)) ^ (u v y)) v y' = 1. [para(15(a,1),1673(a,1,1,1))]. given #1054 (T,wt=14): 4401 x' v (((x v y) ^ (z v x)) v u) = 1. [para(1673(a,1),103(a,1,1)),rewrite(62(8),4212(11))]. given #1055 (T,wt=14): 4402 x' v (y v ((x v z) ^ (u v x))) = 1. [para(1673(a,1),104(a,1,1)),rewrite(62(8),1673(11))]. given #1056 (A,wt=20): 434 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (y ^ x)' = z. [para(4(a,1),37(a,1,1))]. given #1057 (F,wt=14): 4410 x v (y v (z v ((z ^ u) v x)')) = 1. [para(1712(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1058 (F,wt=14): 4412 x v (y v ((z ^ (y ^ u)) v x)') = 1. [para(17(a,1),1712(a,1,2,2,1,1))]. given #1059 (T,wt=14): 4413 x v (y v ((y ^ z) v (x ^ u))') = 1. [para(1712(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #1060 (T,wt=14): 4418 x v (y v ((y ^ z) v (u ^ x))') = 1. [para(1712(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #1061 (A,wt=20): 435 (x ^ y) v z != 1 | y ^ (z ^ x) != 0 | (x ^ y)' = z. [para(4(a,1),37(b,1)),rewrite(5(6))]. given #1062 (F,wt=14): 4419 x v (y v (z v ((u ^ y) v x)')) = 1. [para(145(a,1),1712(a,1,2,2,1,1)),rewrite(3(5))]. given #1063 (F,wt=14): 4420 x v (y v (z v ((u ^ z) v x)')) = 1. [para(761(a,1),1712(a,1,2,2,1,1)),rewrite(3(5))]. given #1064 (T,wt=14): 4426 x v (y v ((z ^ (u ^ y)) v x)') = 1. [para(144(a,1),1712(a,1,2,2,1,1))]. given #1065 (T,wt=14): 4515 x v (((x ^ y) v (x ^ z))' v u) = 1. [para(1715(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1066 (A,wt=26): 436 (x ^ (y ^ z)) v u != 1 | x ^ (y ^ (z ^ u)) != 0 | (x ^ (y ^ z))' = u. [para(5(a,1),37(a,1,1)),rewrite(5(8),5(12))]. given #1067 (F,wt=14): 4519 x v (y v ((x ^ z) v (x ^ u))') = 1. [para(1715(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1068 (F,wt=14): 4520 x v ((y ^ (x ^ z)) v (x ^ u))' = 1. [para(17(a,1),1715(a,1,2,1,1))]. given #1069 (T,wt=14): 4521 x v ((x ^ y) v (z ^ (x ^ u)))' = 1. [para(17(a,1),1715(a,1,2,1,2))]. given #1070 (T,wt=14): 4531 ((x ^ y) v (x ^ z))' v (u v x) = 1. [para(1715(a,1),104(a,1,1)),rewrite(62(8),1715(11))]. given #1071 (A,wt=18): 437 x v y != 1 | z ^ x != 0 | (z ^ x)' = x v y. [para(6(a,1),37(b,1,2)),rewrite(15(3),94(3))]. given #1072 (F,wt=14): 4533 x v ((y ^ (z ^ x)) v (x ^ u))' = 1. [para(144(a,1),1715(a,1,2,1,1))]. given #1073 (F,wt=14): 4534 x v ((x ^ y) v (z ^ (u ^ x)))' = 1. [para(144(a,1),1715(a,1,2,1,2))]. given #1074 (T,wt=14): 4539 x v (((x ^ y) v (z ^ x))' v u) = 1. [para(1720(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1075 (T,wt=14): 4542 x v (y v (x v ((x v y) ^ z))') = 1. [para(6(a,1),1720(a,1,2,1,2)),rewrite(2(4),3(6))]. given #1076 (A,wt=18): 438 x ^ y != 1 | x ^ y != 0 | (x ^ y)' = x ^ y. [para(27(a,1),37(a,1)),rewrite(54(5),52(5))]. given #1077 (F,wt=14): 4544 x v (y v ((x ^ z) v (u ^ x))') = 1. [para(1720(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1078 (F,wt=14): 4545 x v ((y ^ (x ^ z)) v (u ^ x))' = 1. [para(17(a,1),1720(a,1,2,1,1))]. given #1079 (T,wt=14): 4569 ((x ^ y) v (z ^ x))' v (u v x) = 1. [para(1720(a,1),104(a,1,1)),rewrite(62(8),1720(11))]. given #1080 (T,wt=14): 4580 x v ((y ^ (z ^ x)) v (u ^ x))' = 1. [para(144(a,1),1720(a,1,2,1,1))]. given #1081 (A,wt=26): 441 x v ((y ^ z) v u) != 1 | y ^ (z ^ (x v u)) != 0 | (y ^ z)' = x v u. [para(15(a,1),37(a,1))]. given #1082 (F,wt=14): 4586 x ^ (y ^ (z ^ ((z v u) ^ x)')) = 0. [para(1775(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1083 (F,wt=14): 4592 x ^ (y ^ (z ^ ((u v y) ^ x)')) = 0. [para(183(a,1),1775(a,1,2,2,1,1)),rewrite(5(5))]. given #1084 (T,wt=14): 4594 x ^ (y ^ (z ^ ((u v z) ^ x)')) = 0. [para(814(a,1),1775(a,1,2,2,1,1)),rewrite(5(5))]. given #1085 (T,wt=14): 4603 x ^ (((x v y) ^ (x v z))' ^ u) = 0. [para(1777(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1086 (A,wt=26): 442 (x ^ (y ^ z)) v u != 1 | y ^ (x ^ (z ^ u)) != 0 | (y ^ (x ^ z))' = u. [para(17(a,1),37(a,1,1)),rewrite(5(7))]. given #1087 (F,wt=14): 4606 x ^ (y ^ ((x v z) ^ (x v u))') = 0. [para(1777(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1088 (F,wt=14): 4615 ((x v y) ^ (x v z))' ^ (u ^ x) = 0. [para(1777(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6))]. given #1089 (T,wt=14): 4689 x ^ ((x v y) ^ (z v (u v x)))' = 0. [para(3(a,1),1782(a,1,2,1,2))]. given #1090 (T,wt=14): 4690 x ^ (((x v y) ^ (z v x))' ^ u) = 0. [para(1782(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1091 (A,wt=26): 443 (x ^ y) v (z ^ u) != 1 | x ^ (z ^ (y ^ u)) != 0 | (x ^ y)' = z ^ u. [para(17(a,1),37(b,1,2))]. given #1092 (F,wt=14): 4694 x ^ (y ^ ((x v z) ^ (u v x))') = 0. [para(1782(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1093 (F,wt=14): 4715 ((x v y) ^ (z v x))' ^ (u ^ x) = 0. [para(1782(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6))]. given #1094 (T,wt=14): 4721 x v ((y v x)' v (z v (y v u))) = 1. [para(1920(a,1),3(a,1,1)),rewrite(73(2),3(6),3(5)),flip(a)]. given #1095 (T,wt=14): 4738 x v ((y ^ z) v ((z ^ y) v x)') = 1. [para(243(a,1),1920(a,1,2,2)),rewrite(2(5))]. given #1096 (A,wt=20): 444 (x ^ y) v z != 1 | y ^ (x ^ z) != 0 | (x ^ y)' = z. [para(17(a,1),37(b,1))]. given #1097 (F,wt=14): 4745 x ^ ((y ^ x)' ^ (z ^ (y ^ u))) = 0. [para(1998(a,1),5(a,1,1)),rewrite(76(2),5(6),5(5)),flip(a)]. given #1098 (F,wt=14): 4752 x ^ (y ^ ((z v (u v y)) ^ x)') = 0. [para(88(a,1),1998(a,1,2,2)),rewrite(4(5))]. given #1099 (T,wt=14): 4760 x ^ ((y v z) ^ ((z v y) ^ x)') = 0. [para(157(a,1),1998(a,1,2,2)),rewrite(4(5))]. given #1100 (T,wt=14): 4794 x v (y v ((z ^ y) v (x ^ u))') = 1. [para(2394(a,1),22(a,1,2)),rewrite(82(2)),flip(a)]. given #1101 (A,wt=22): 446 x ^ y != 1 | z ^ (x ^ y) != 0 | (x ^ y)' = z ^ (x ^ y). [para(24(a,1),37(a,1)),rewrite(144(6),123(6))]. given #1102 (F,wt=14): 4802 x v (y v ((z ^ y) v (u ^ x))') = 1. [para(2394(a,1),94(a,1,2)),rewrite(82(2)),flip(a)]. given #1103 (F,wt=14): 4894 x v (((y ^ x) v (x ^ z))' v u) = 1. [para(2450(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1104 (T,wt=14): 4898 x v (y v ((z ^ x) v (x ^ u))') = 1. [para(2450(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1105 (T,wt=14): 4900 x v ((y ^ x) v (z ^ (x ^ u)))' = 1. [para(17(a,1),2450(a,1,2,1,2))]. given #1106 (A,wt=23): 447 x ^ (y ^ ((x ^ y)' v z)) != 0 | (x ^ y)' v z = (x ^ y)'. [para(74(a,1),37(a,1)),flip(c),xx(a)]. given #1107 (F,wt=14): 4908 ((x ^ y) v (y ^ z))' v (u v y) = 1. [para(2450(a,1),104(a,1,1)),rewrite(62(8),2450(11))]. given #1108 (F,wt=14): 4910 x v ((y ^ x) v (z ^ (u ^ x)))' = 1. [para(144(a,1),2450(a,1,2,1,2))]. given #1109 (T,wt=14): 4914 x ^ (y ^ (((z v y) ^ x)' ^ u)) = 0. [para(2471(a,1),5(a,1,1)),rewrite(76(2),5(6)),flip(a)]. given #1110 (T,wt=14): 4918 x ^ (y ^ ((z v y) ^ (x v u))') = 0. [para(2471(a,1),20(a,1,2)),rewrite(85(2)),flip(a)]. given #1111 (A,wt=19): 449 (x ^ y) v (y' ^ z) != 1 | (x ^ y)' = y' ^ z. [para(77(a,1),37(b,1,2)),rewrite(85(8)),xx(b)]. given #1112 (F,wt=14): 4926 x ^ (y ^ ((z v y) ^ (u v x))') = 0. [para(2471(a,1),89(a,1,2)),rewrite(85(2)),flip(a)]. given #1113 (F,wt=14): 4943 x ^ ((y v (z v x)) ^ (x v u))' = 0. [para(3(a,1),2546(a,1,2,1,1))]. given #1114 (T,wt=14): 4944 x ^ (((y v x) ^ (x v z))' ^ u) = 0. [para(2546(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1115 (T,wt=14): 4948 x ^ (y ^ ((z v x) ^ (x v u))') = 0. [para(2546(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1116 (A,wt=23): 450 x ^ (y ^ (z v (x ^ y)')) != 0 | z v (x ^ y)' = (x ^ y)'. [para(83(a,1),37(a,1)),flip(c),xx(a)]. given #1117 (F,wt=14): 4958 ((x v y) ^ (y v z))' ^ (u ^ y) = 0. [para(2546(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6))]. given #1118 (F,wt=14): 4966 (x v y)' ^ (x v (z ^ (y ^ u))) = 0. [para(17(a,1),2881(a,1,2,2))]. given #1119 (T,wt=14): 4967 (x v y)' ^ (x v ((x v y) ^ z)) = 0. [para(58(a,1),2881(a,1,1,1))]. given #1120 (T,wt=14): 4968 (x v y)' ^ (y v ((x v y) ^ z)) = 0. [para(60(a,1),2881(a,1,1,1))]. given #1121 (A,wt=19): 451 (x ^ y) v (z ^ y') != 1 | (x ^ y)' = z ^ y'. [para(86(a,1),37(b,1,2)),rewrite(85(8)),xx(b)]. given #1122 (F,wt=14): 4976 (x v (y v z))' ^ (x v (u ^ y)) = 0. [para(145(a,1),2881(a,1,2,2))]. given #1123 (F,wt=14): 4979 (x v (y v z))' ^ (x v (u ^ z)) = 0. [para(761(a,1),2881(a,1,2,2))]. given #1124 (T,wt=14): 4984 (x v y)' ^ (x v (z ^ (u ^ y))) = 0. [para(144(a,1),2881(a,1,2,2))]. given #1125 (T,wt=14): 5109 (x ^ y)' v (x ^ (z v (y v u))) = 1. [para(15(a,1),2918(a,1,2,2))]. given #1126 (A,wt=15): 452 (x ^ y) v x' != 1 | (x ^ y)' = x'. [para(86(a,1),37(b,1)),xx(b)]. given #1127 (F,wt=14): 5111 (x ^ y)' v (x ^ ((x ^ y) v z)) = 1. [para(52(a,1),2918(a,1,1,1))]. given #1128 (F,wt=14): 5113 (x ^ y)' v (y ^ ((x ^ y) v z)) = 1. [para(54(a,1),2918(a,1,1,1))]. given #1129 (T,wt=14): 5121 (x ^ (y ^ z))' v (x ^ (u v y)) = 1. [para(183(a,1),2918(a,1,2,2))]. given #1130 (T,wt=14): 5124 (x ^ (y ^ z))' v (x ^ (u v z)) = 1. [para(814(a,1),2918(a,1,2,2))]. given #1131 (A,wt=24): 453 (x ^ y) v (y ^ z) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = y ^ z. [para(52(a,1),37(b,1,2))]. given #1132 (F,wt=14): 5138 (x ^ y)' v ((z v (u v x)) ^ y) = 1. [para(3(a,1),2966(a,1,2,1))]. given #1133 (F,wt=14): 5149 x' v ((y v x) ^ (z v (x v u))) = 1. [para(67(a,1),2966(a,1,1,1))]. given #1134 (T,wt=14): 5150 x' v ((y v x) ^ (z v (u v x))) = 1. [para(88(a,1),2966(a,1,1,1))]. given #1135 (T,wt=14): 5182 (x ^ (y v z)) v ((z ^ x)' v u) = 1. [para(2968(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1136 (A,wt=28): 454 (x ^ y) v ((y v z) ^ u) != 1 | x ^ (y ^ u) != 0 | (x ^ y)' = (y v z) ^ u. [para(20(a,1),37(b,1,2))]. given #1137 (F,wt=14): 5183 (x ^ (y v (z v u))) v (u ^ x)' = 1. [para(3(a,1),2968(a,1,1,2))]. given #1138 (F,wt=14): 5187 (x ^ (y v z)) v (u v (z ^ x)') = 1. [para(2968(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1139 (T,wt=14): 5192 (x ^ y) v (z ^ (y ^ (u ^ x)))' = 1. [para(79(a,1),2968(a,1,1,2)),rewrite(5(4),5(3))]. given #1140 (T,wt=14): 5193 ((x v (y v z)) ^ (u v z)) v z' = 1. [para(88(a,1),2968(a,1,2,1))]. given #1141 (A,wt=19): 455 (x ^ y) v (y v z)' != 1 | (y v z)' = (x ^ y)'. [para(125(a,1),37(b,1,2)),rewrite(85(8)),flip(c),xx(b)]. given #1142 (F,wt=14): 5215 (x ^ y)' v ((y ^ (z v x)) v u) = 1. [para(2968(a,1),103(a,1,1)),rewrite(62(8),5139(11))]. given #1143 (F,wt=14): 5217 (x ^ y)' v (z v (y ^ (u v x))) = 1. [para(2968(a,1),104(a,1,1)),rewrite(62(8),2968(11))]. given #1144 (T,wt=14): 5236 ((x v y) ^ (y v z)) v (y' v u) = 1. [para(2970(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1145 (T,wt=14): 5238 ((x v y) ^ (y v z)) v (u v y') = 1. [para(2970(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1146 (A,wt=19): 456 (x ^ y) v (z v y)' != 1 | (z v y)' = (x ^ y)'. [para(132(a,1),37(b,1,2)),rewrite(85(8)),flip(c),xx(b)]. given #1147 (F,wt=14): 5245 x' v (((y v x) ^ (x v z)) v u) = 1. [para(2970(a,1),103(a,1,1)),rewrite(62(8),5141(11))]. given #1148 (F,wt=14): 5246 x' v (y v ((z v x) ^ (x v u))) = 1. [para(2970(a,1),104(a,1,1)),rewrite(62(8),2970(11))]. given #1149 (T,wt=14): 5370 ((x v y) ^ (z v y)) v (y' v u) = 1. [para(2975(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1150 (T,wt=14): 5372 ((x v y) ^ (z v y)) v (u v y') = 1. [para(2975(a,1),15(a,1,2)),rewrite(82(2)),flip(a)]. given #1151 (A,wt=24): 457 (x ^ y) v (z ^ y) != 1 | x ^ (z ^ y) != 0 | (x ^ y)' = z ^ y. [para(54(a,1),37(b,1,2))]. given #1152 (F,wt=14): 5388 x' v (((y v x) ^ (z v x)) v u) = 1. [para(2975(a,1),103(a,1,1)),rewrite(62(8),5145(11))]. given #1153 (F,wt=14): 5389 x' v (y v ((z v x) ^ (u v x))) = 1. [para(2975(a,1),104(a,1,1)),rewrite(62(8),2975(11))]. given #1154 (T,wt=14): 5396 x ^ ((y v (z v x)) ^ (u v x))' = 0. [para(3(a,1),3023(a,1,2,1,1))]. given #1155 (T,wt=14): 5397 x ^ ((y v x) ^ (z v (u v x)))' = 0. [para(3(a,1),3023(a,1,2,1,2))]. given #1156 (A,wt=22): 459 (x ^ y) v z != 1 | x ^ y != 0 | (x ^ y)' = (x ^ y) v z. [para(58(a,1),37(a,1)),rewrite(21(8))]. given #1157 (F,wt=14): 5398 x ^ (((y v x) ^ (z v x))' ^ u) = 0. [para(3023(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1158 (F,wt=14): 5400 x ^ (y ^ (x ^ (z v (x ^ y)))') = 0. [para(7(a,1),3023(a,1,2,1,1)),rewrite(5(6))]. given #1159 (T,wt=14): 5404 x ^ (y ^ ((z v x) ^ (u v x))') = 0. [para(3023(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1160 (T,wt=14): 5425 ((x v y) ^ (z v y))' ^ (u ^ y) = 0. [para(3023(a,1),515(a,1,2,2,2,1)),rewrite(75(6),30(6))]. given #1161 (A,wt=32): 460 (x ^ y) v (z ^ ((y ^ z) v u)) != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z ^ ((y ^ z) v u). [para(21(a,1),37(b,1,2))]. given #1162 (F,wt=14): 5430 (x ^ y)' v (x ^ (z v (u v y))) = 1. [para(3(a,1),3165(a,1,2,2))]. given #1163 (F,wt=14): 5433 (x ^ y)' v (x ^ (z v (x ^ y))) = 1. [para(52(a,1),3165(a,1,1,1))]. given #1164 (T,wt=14): 5435 (x ^ y)' v (y ^ (z v (x ^ y))) = 1. [para(54(a,1),3165(a,1,1,1))]. given #1165 (T,wt=14): 5470 (x v (y ^ z)) ^ ((z v x)' ^ u) = 0. [para(3223(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1166 (A,wt=22): 461 x v (y ^ z) != 1 | y ^ z != 0 | (y ^ z)' = x v (y ^ z). [para(60(a,1),37(a,1)),rewrite(90(8))]. given #1167 (F,wt=14): 5473 (x v (y ^ z)) ^ (u ^ (z v x)') = 0. [para(3223(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1168 (F,wt=14): 5502 (x v y)' ^ ((y v (z ^ x)) ^ u) = 0. [para(3223(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #1169 (T,wt=14): 5503 (x v y)' ^ (z ^ (y v (u ^ x))) = 0. [para(3223(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #1170 (T,wt=14): 5559 x ^ (y ^ (x ^ ((y ^ x) v z))') = 0. [para(153(a,1),1503(a,1,2,2,1))]. given #1171 (A,wt=32): 465 (x ^ y) v z != 1 | x ^ (y ^ ((x ^ (y ^ u)) v z)) != 0 | (x ^ y)' = (x ^ (y ^ u)) v z. [para(22(a,1),37(a,1)),rewrite(5(6),5(15))]. given #1172 (F,wt=14): 5589 x' ^ ((y ^ x) v (z ^ (x ^ u))) = 0. [para(79(a,1),3224(a,1,1,1))]. given #1173 (F,wt=14): 5591 x' ^ ((y ^ x) v (z ^ (u ^ x))) = 0. [para(96(a,1),3224(a,1,1,1))]. given #1174 (T,wt=14): 5605 (x v (y v z))' ^ ((u ^ x) v y) = 0. [para(3224(a,1),110(a,1,2)),rewrite(4(4),76(4)),flip(a)]. given #1175 (T,wt=14): 5614 ((x ^ y) v (y ^ z)) ^ (y' ^ u) = 0. [para(3226(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1176 (A,wt=23): 466 x ^ (y ^ (x ^ (y ^ z))') != 0 | (x ^ (y ^ z))' = (x ^ y)'. [para(176(a,1),37(a,1)),rewrite(5(5),5(14)),flip(c),xx(a)]. given #1177 (F,wt=14): 5616 ((x ^ y) v (y ^ z)) ^ (u ^ y') = 0. [para(3226(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1178 (F,wt=14): 5624 x' ^ (((y ^ x) v (x ^ z)) ^ u) = 0. [para(3226(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #1179 (T,wt=14): 5625 x' ^ (y ^ ((z ^ x) v (x ^ u))) = 0. [para(3226(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #1180 (T,wt=14): 5632 ((x ^ y) v (z ^ y)) ^ (y' ^ u) = 0. [para(3231(a,1),5(a,1,1)),rewrite(76(2)),flip(a)]. given #1181 (A,wt=23): 467 x ^ (y ^ (z ^ (x ^ y))') != 0 | (z ^ (x ^ y))' = (x ^ y)'. [para(186(a,1),37(a,1)),flip(c),xx(a)]. given #1182 (F,wt=14): 5634 ((x ^ y) v (z ^ y)) ^ (u ^ y') = 0. [para(3231(a,1),17(a,1,2)),rewrite(85(2)),flip(a)]. given #1183 (F,wt=14): 5655 x' ^ (((y ^ x) v (z ^ x)) ^ u) = 0. [para(3231(a,1),511(a,1,2,2,1,1)),rewrite(75(6),62(6))]. given #1184 (T,wt=14): 5656 x' ^ (y ^ ((z ^ x) v (u ^ x))) = 0. [para(3231(a,1),515(a,1,2,2,2,1)),rewrite(75(6),4(6),62(6))]. given #1185 (T,wt=14): 5673 x v (((y ^ x) v (z ^ x))' v u) = 1. [para(3280(a,1),3(a,1,1)),rewrite(73(2)),flip(a)]. given #1186 (A,wt=27): 469 x ^ (y ^ (z v ((x ^ y) v z)')) != 0 | z v ((x ^ y) v z)' = (x ^ y)'. [par