============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5147 was started by mccune on cleo, Tue Nov 3 09:46:37 2009 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 assign(max_seconds,600). 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(non_clause) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, c3, ^, v, ' ]). After inverse_order: Function symbol precedence: function_order([ 0, 1, c1, c2, c3, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % 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. kept: 2 x v y = y v x. [assumption]. kept: 3 (x v y) v z = x v (y v z). [assumption]. % Operation ^ is commutative; C redundancy checks enabled. kept: 4 x ^ y = y ^ x. [assumption]. kept: 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. kept: 6 x ^ (x v y) = x. [assumption]. kept: 7 x v (x ^ y) = x. [assumption]. kept: 8 x v x' = 1. [assumption]. kept: 9 x ^ x' = 0. [assumption]. kept: 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. 11 x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). [assumption]. kept: 12 x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) = x ^ (y v (z ^ u)). [copy(11),flip(a)]. kept: 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # answer(distributivity). [deny(1)]. ============================== 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.01 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 (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 #13 (T,wt=5): 26 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #14 (T,wt=5): 27 x v x = x. [para(6(a,1),7(a,1,2))]. given #15 (T,wt=5): 30 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #16 (T,wt=5): 33 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #17 (A,wt=11): 17 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. given #18 (T,wt=5): 61 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. given #19 (T,wt=4): 68 1' = 0. [hyper(10,a,33,a,b,61,a)]. given #20 (T,wt=5): 62 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. given #21 (T,wt=4): 71 0' = 1. [hyper(10,a,62,a,b,30,a)]. given #22 (A,wt=7): 18 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #23 (T,wt=5): 69 1 v x = 1. [para(61(a,1),6(a,1))]. given #24 (T,wt=5): 72 0 ^ x = 0. [para(62(a,1),6(a,1,2))]. given #25 (T,wt=5): 79 x v 1 = 1. [para(18(a,1),61(a,1)),flip(a)]. given #26 (T,wt=5): 81 x ^ 0 = 0. [para(72(a,1),4(a,1)),flip(a)]. given #27 (A,wt=13): 19 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #28 (T,wt=7): 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #29 (T,wt=7): 83 1 != x | x' = 0. [back_rewrite(63),rewrite([81(4)]),xx(b)]. given #30 (T,wt=7): 84 0 != x | x' = 1. [para(79(a,1),10(a,1)),rewrite([30(5)]),flip(b),xx(a)]. given #31 (T,wt=8): 70 x v (x' v y) = 1. [back_rewrite(28),rewrite([69(5)])]. given #32 (A,wt=11): 20 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #33 (T,wt=8): 73 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite([72(5)])]. given #34 (T,wt=8): 80 x v (y v x') = 1. [back_rewrite(50),rewrite([79(5)])]. given #35 (T,wt=8): 82 x ^ (y ^ x') = 0. [back_rewrite(67),rewrite([81(5)])]. given #36 (T,wt=8): 103 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #37 (A,wt=13): 21 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #38 (T,wt=8): 116 x ^ (y v x)' = 0. [para(2(a,1),103(a,1,2,1))]. given #39 (T,wt=9): 48 x ^ (y v (x v z)) = x. [para(15(a,1),6(a,1,2))]. given #40 (T,wt=9): 52 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. given #41 (T,wt=9): 54 x ^ (y ^ x) = y ^ x. [para(26(a,1),5(a,2,2)),rewrite([4(2)])]. given #42 (A,wt=11): 22 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #43 (T,wt=8): 143 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #44 (T,wt=8): 152 x v (y ^ x)' = 1. [para(4(a,1),143(a,1,2,1))]. given #45 (T,wt=9): 57 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. given #46 (T,wt=9): 59 x v (y v x) = y v x. [para(27(a,1),3(a,2,2)),rewrite([2(2)])]. given #47 (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 #48 (T,wt=9): 66 x v (y ^ (x ^ z)) = x. [para(17(a,1),7(a,1,2))]. given #49 (T,wt=9): 74 x ^ (y v (z v x)) = x. [para(3(a,1),18(a,1,2))]. given #50 (T,wt=9): 94 x v (y ^ (z ^ x)) = x. [para(5(a,1),24(a,1,2))]. given #51 (T,wt=10): 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #52 (A,wt=13): 25 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #53 (T,wt=10): 32 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #54 (T,wt=10): 60 1 != x | 0 != x | x' = x. [para(27(a,1),10(a,1)),rewrite([26(3)]),flip(a),flip(b)]. given #55 (T,wt=10): 101 x v (y v (x' v z)) = 1. [para(70(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #56 (T,wt=10): 108 x ^ (y ^ (x' ^ z)) = 0. [para(73(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #57 (A,wt=14): 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #58 (T,wt=5): 228 x'' = x. [para(8(a,1),34(a,1)),rewrite([4(5),9(5)]),xx(a),xx(b)]. given #59 (T,wt=8): 244 x' v (y v x) = 1. [para(228(a,1),80(a,1,2,2))]. given #60 (T,wt=8): 245 x' ^ (y ^ x) = 0. [para(228(a,1),82(a,1,2,2))]. given #61 (T,wt=10): 109 x ^ ((x v y)' ^ z) = 0. [para(73(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #62 (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 #63 (T,wt=10): 111 x v (y v (z v x')) = 1. [para(3(a,1),80(a,1,2))]. given #64 (T,wt=10): 114 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),82(a,1,2))]. given #65 (T,wt=10): 115 x ^ (y ^ (x v z)') = 0. [para(82(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #66 (T,wt=10): 119 x ^ (y v (x v z))' = 0. [para(15(a,1),103(a,1,2,1))]. given #67 (A,wt=21): 37 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 #68 (T,wt=10): 127 x ^ (y v (z v x))' = 0. [para(3(a,1),116(a,1,2,1))]. given #69 (T,wt=10): 128 x ^ ((y v x)' ^ z) = 0. [para(116(a,1),5(a,1,1)),rewrite([72(2)]),flip(a)]. given #70 (T,wt=10): 131 x ^ (y ^ (z v x)') = 0. [para(116(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #71 (T,wt=10): 148 x v ((x ^ y)' v z) = 1. [para(70(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #72 (A,wt=27): 38 x ^ (y v (z v (x ^ ((x ^ (y v z)) v (u ^ w))))) = x ^ (y v (z v (u ^ w))). [para(3(a,1),12(a,1,2)),rewrite([3(11)])]. given #73 (T,wt=10): 149 x v (y v (x ^ z)') = 1. [para(80(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #74 (T,wt=10): 155 x v (y ^ (x ^ z))' = 1. [para(17(a,1),143(a,1,2,1))]. given #75 (T,wt=10): 156 x v ((y ^ x)' v z) = 1. [para(152(a,1),3(a,1,1)),rewrite([69(2)]),flip(a)]. given #76 (T,wt=10): 158 x v (y ^ (z ^ x))' = 1. [para(5(a,1),152(a,1,2,1))]. given #77 (A,wt=21): 39 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 #78 (T,wt=10): 160 x v (y v (z ^ x)') = 1. [para(152(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #79 (T,wt=10): 199 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. given #80 (T,wt=10): 214 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),32(a,1,2,2,1))]. given #81 (T,wt=10): 246 x' v (y v (x v z)) = 1. [para(228(a,1),101(a,1,2,2,1))]. given #82 (A,wt=25): 40 x ^ ((y v (x ^ ((x ^ y) v (z ^ u)))) ^ w) = x ^ ((y v (z ^ u)) ^ w). [para(12(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)]. given #83 (T,wt=10): 247 x' ^ (y ^ (x ^ z)) = 0. [para(228(a,1),108(a,1,2,2,1))]. given #84 (T,wt=10): 248 x' v (y v (z v x)) = 1. [para(3(a,1),244(a,1,2))]. given #85 (T,wt=10): 253 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),245(a,1,2))]. given #86 (T,wt=10): 531 (x ^ y)' v (z v x) = 1. [para(7(a,1),248(a,1,2,2))]. given #87 (A,wt=29): 41 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (y ^ z)) v (u ^ w)))))) = x ^ (y ^ (z v (u ^ w))). [para(12(a,1),5(a,1)),rewrite([5(4),5(7),5(10)]),flip(a)]. given #88 (T,wt=10): 534 (x ^ y)' v (z v y) = 1. [para(24(a,1),248(a,1,2,2))]. given #89 (T,wt=10): 544 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),253(a,1,2,2))]. given #90 (T,wt=10): 546 (x v y)' ^ (z ^ y) = 0. [para(18(a,1),253(a,1,2,2))]. given #91 (T,wt=11): 49 x v (y v (x ^ z)) = y v x. [para(7(a,1),15(a,1,2)),flip(a)]. given #92 (A,wt=17): 42 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 #93 (T,wt=11): 65 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. given #94 (T,wt=11): 75 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. given #95 (T,wt=11): 78 x ^ (y ^ (z v x)) = y ^ x. [para(18(a,1),17(a,1,2)),flip(a)]. given #96 (T,wt=11): 92 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. given #97 (A,wt=20): 51 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(15(a,1),10(a,1))]. given #98 (T,wt=11): 96 x v (y v (z ^ x)) = y v x. [para(24(a,1),15(a,1,2)),flip(a)]. given #99 (T,wt=11): 133 x ^ (y v (z v (x v u))) = x. [para(3(a,1),48(a,1,2))]. given #100 (T,wt=11): 140 (x v y) ^ (z ^ x) = z ^ x. [para(54(a,1),20(a,2)),rewrite([139(4)])]. given #101 (T,wt=11): 168 (x v y) ^ (y v x) = x v y. [para(59(a,1),19(a,1,2))]. given #102 (A,wt=14): 56 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(36),rewrite([52(4)])]. given #103 (T,wt=7): 885 x' != 1 | 0 = x. [para(245(a,1),56(b,1)),rewrite([228(8),245(9)]),flip(a),flip(c),xx(b)]. given #104 (T,wt=10): 874 (x v y) ^ (y v x)' = 0. [para(168(a,1),245(a,1,2)),rewrite([4(4)])]. given #105 (T,wt=11): 169 (x ^ y) v (z v x) = z v x. [para(59(a,1),22(a,2)),rewrite([166(4)])]. given #106 (T,wt=11): 180 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),66(a,1,2))]. given #107 (A,wt=13): 76 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(18(a,1),5(a,1)),flip(a)]. given #108 (T,wt=11): 183 x ^ (y v (z v (u v x))) = x. [para(3(a,1),74(a,1,2,2))]. given #109 (T,wt=11): 192 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),94(a,1,2,2))]. given #110 (T,wt=11): 212 (x ^ y) v (y ^ x) = x ^ y. [para(54(a,1),25(a,1,2))]. given #111 (T,wt=10): 992 (x ^ y) v (y ^ x)' = 1. [para(212(a,1),244(a,1,2)),rewrite([2(4)])]. given #112 (A,wt=13): 77 (x v y) ^ (x v (z v y)) = x v y. [para(15(a,1),18(a,1,2))]. given #113 (T,wt=11): 264 x v y != 1 | (x v y)' = 0. [para(33(a,1),35(a,1,2)),rewrite([4(6),72(6)]),xx(b)]. given #114 (T,wt=11): 265 x v y != 0 | (x v y)' = 1. [para(79(a,1),35(a,1,2)),rewrite([79(2),4(6),61(6)]),xx(a)]. given #115 (T,wt=11): 721 (x v y) ^ (z ^ y) = z ^ y. [para(54(a,1),75(a,2)),rewrite([139(4)])]. given #116 (T,wt=11): 768 (x ^ y) v (z v y) = z v y. [para(59(a,1),92(a,2)),rewrite([166(4)])]. given #117 (A,wt=13): 85 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),19(a,1,1))]. given #118 (T,wt=11): 886 (x v y)' != 1 | x v y = 0. [para(544(a,1),56(b,1)),rewrite([228(10),544(12)]),flip(a),xx(b)]. given #119 (T,wt=11): 1031 x v y != 1 | (y v x)' = 0. [para(2(a,1),264(a,1))]. given #120 (T,wt=11): 1033 x ^ y != 1 | (x ^ y)' = 0. [para(25(a,1),264(a,1)),rewrite([25(7)])]. given #121 (T,wt=11): 1034 x v y != 0 | (y v x)' = 1. [para(2(a,1),265(a,1))]. given #122 (A,wt=13): 86 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),19(a,1,2)),rewrite([3(3)])]. given #123 (T,wt=11): 1036 x ^ y != 0 | (x ^ y)' = 1. [para(25(a,1),265(a,1)),rewrite([25(7)])]. given #124 (T,wt=11): 1092 (x v y)' != 1 | y v x = 0. [para(2(a,1),886(a,1,1))]. given #125 (T,wt=11): 1094 (x ^ y)' != 1 | x ^ y = 0. [para(25(a,1),886(a,1,1)),rewrite([25(8)])]. given #126 (T,wt=11): 1097 x ^ y != 1 | (y ^ x)' = 0. [para(212(a,1),1031(a,1)),rewrite([212(6)])]. given #127 (A,wt=19): 87 (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 #128 (T,wt=11): 1101 x ^ y != 0 | (y ^ x)' = 1. [para(212(a,1),1034(a,1)),rewrite([212(6)])]. given #129 (T,wt=11): 1137 (x ^ y)' != 1 | y ^ x = 0. [para(212(a,1),1092(a,1,1)),rewrite([212(7)])]. given #130 (T,wt=12): 99 x v (y v ((x v y)' v z)) = 1. [para(70(a,1),3(a,1)),flip(a)]. given #131 (T,wt=12): 107 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(73(a,1),5(a,1)),flip(a)]. given #132 (A,wt=17): 88 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(19(a,1),5(a,1,1)),flip(a)]. given #133 (T,wt=12): 110 x v (y v (z v (x v y)')) = 1. [para(80(a,1),3(a,1)),flip(a)]. given #134 (T,wt=12): 113 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(82(a,1),5(a,1)),flip(a)]. given #135 (T,wt=12): 117 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),103(a,1,2,1))]. given #136 (T,wt=12): 118 x ^ (y ^ ((x ^ y) v z)') = 0. [para(103(a,1),5(a,1)),flip(a)]. given #137 (A,wt=19): 89 (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 #138 (T,wt=12): 129 x ^ (y ^ (z v (x ^ y))') = 0. [para(116(a,1),5(a,1)),flip(a)]. given #139 (T,wt=12): 130 (x v y) ^ (x v (z v y))' = 0. [para(15(a,1),116(a,1,2,1))]. given #140 (T,wt=12): 150 ((x ^ y) v z) ^ (x v z)' = 0. [para(22(a,1),116(a,1,2,1))]. given #141 (T,wt=12): 151 x v (y v ((x v y) ^ z)') = 1. [para(143(a,1),3(a,1)),flip(a)]. given #142 (A,wt=15): 90 (x v y) ^ (x v (z v (y v u))) = x v y. [para(15(a,1),19(a,1,2,2))]. given #143 (T,wt=12): 153 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),143(a,1,2,1))]. given #144 (T,wt=12): 157 x v (y v (z ^ (x v y))') = 1. [para(152(a,1),3(a,1)),flip(a)]. given #145 (T,wt=12): 161 (x ^ y) v (x ^ (z ^ y))' = 1. [para(17(a,1),152(a,1,2,1))]. given #146 (T,wt=12): 162 ((x v y) ^ z) v (x ^ z)' = 1. [para(20(a,1),152(a,1,2,1))]. given #147 (A,wt=17): 91 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(19(a,1),17(a,1,2)),flip(a)]. given #148 (T,wt=12): 202 x v (y v (z v (x v z)')) = 1. [para(29(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #149 (T,wt=12): 204 x v (y v ((x ^ z) v y)') = 1. [para(29(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #150 (T,wt=12): 216 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(32(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #151 (T,wt=12): 218 x ^ (y ^ ((x v z) ^ y)') = 0. [para(32(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #152 (A,wt=13): 93 x v (y v (z ^ (x v y))) = x v y. [para(24(a,1),3(a,1)),flip(a)]. given #153 (T,wt=12): 220 x v (y v (z v (x' v u))) = 1. [para(3(a,1),101(a,1,2))]. given #154 (T,wt=12): 222 x v (y v ((x ^ z)' v u)) = 1. [para(101(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #155 (T,wt=12): 224 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),108(a,1,2))]. given #156 (T,wt=12): 225 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(108(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #157 (A,wt=14): 95 1 != x | y ^ x != 0 | x' = y ^ x. [para(24(a,1),10(a,1)),rewrite([54(4)]),flip(a)]. given #158 (T,wt=12): 250 x v ((x v y)' v (z v y)) = 1. [para(15(a,1),244(a,1,2)),rewrite([15(5)])]. given #159 (T,wt=12): 254 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(17(a,1),245(a,1,2)),rewrite([17(5)])]. given #160 (T,wt=12): 258 x ^ ((y v (x v z))' ^ u) = 0. [para(15(a,1),109(a,1,2,1,1))]. given #161 (T,wt=12): 286 x v (y v (z v (u v x'))) = 1. [para(3(a,1),111(a,1,2,2))]. given #162 (A,wt=13): 97 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(17(a,1),24(a,1,2))]. given #163 (T,wt=12): 288 x v (y v (z v (x ^ u)')) = 1. [para(111(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #164 (T,wt=12): 293 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),114(a,1,2,2))]. given #165 (T,wt=12): 294 x ^ (y ^ (z ^ (x v u)')) = 0. [para(114(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #166 (T,wt=12): 297 x ^ (y ^ (z v (x v u))') = 0. [para(15(a,1),115(a,1,2,2,1))]. given #167 (A,wt=15): 100 x ^ (x' v y) != 0 | x' v y = x'. [para(70(a,1),10(a,1)),flip(c),xx(a)]. given #168 (T,wt=12): 299 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),119(a,1,2,1))]. given #169 (T,wt=12): 333 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),127(a,1,2,1,2))]. given #170 (T,wt=12): 334 x ^ ((y v (z v x))' ^ u) = 0. [para(127(a,1),5(a,1,1)),rewrite([72(2)]),flip(a)]. given #171 (T,wt=12): 337 x ^ (y ^ (z v (u v x))') = 0. [para(127(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #172 (A,wt=17): 102 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(20(a,1),5(a,1)),rewrite([5(2)]),flip(a)]. given #173 (T,wt=12): 343 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(128(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #174 (T,wt=12): 346 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),131(a,1,2))]. given #175 (T,wt=12): 353 x v ((y ^ (x ^ z))' v u) = 1. [para(17(a,1),148(a,1,2,1,1))]. given #176 (T,wt=12): 375 x v (y v (z ^ (x ^ u))') = 1. [para(17(a,1),149(a,1,2,2,1))]. given #177 (A,wt=13): 104 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(15(a,1),20(a,1,2,1))]. given #178 (T,wt=12): 381 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),155(a,1,2,1))]. given #179 (T,wt=12): 386 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),156(a,1,2,1,1))]. given #180 (T,wt=12): 388 x v (y v ((z ^ x)' v u)) = 1. [para(156(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #181 (T,wt=12): 395 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),158(a,1,2,1,2))]. given #182 (A,wt=15): 105 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(20(a,1),17(a,1,2)),flip(a)]. given #183 (T,wt=12): 397 x v (y v (z ^ (u ^ x))') = 1. [para(158(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #184 (T,wt=12): 440 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),160(a,1,2))]. given #185 (T,wt=12): 448 x v (y v ((y v x)' v z)) = 1. [para(199(a,1),3(a,1,1)),rewrite([69(2),3(5)]),flip(a)]. given #186 (T,wt=12): 452 x v (y v (z v (z v x)')) = 1. [para(199(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #187 (A,wt=15): 106 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(20(a,1),24(a,1,2)),rewrite([2(4)])]. given #188 (T,wt=12): 454 x v (y v (y v (x ^ z))') = 1. [para(199(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #189 (T,wt=12): 457 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(214(a,1),5(a,1,1)),rewrite([72(2),5(5)]),flip(a)]. given #190 (T,wt=12): 460 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(214(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #191 (T,wt=12): 462 x ^ (y ^ (y ^ (x v z))') = 0. [para(214(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #192 (A,wt=15): 112 x ^ (y v x') != 0 | y v x' = x'. [para(80(a,1),10(a,1)),flip(c),xx(a)]. given #193 (T,wt=12): 464 x' v (y v (z v (x v u))) = 1. [para(3(a,1),246(a,1,2))]. given #194 (T,wt=12): 529 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),247(a,1,2))]. given #195 (T,wt=12): 530 x' v (y v (z v (u v x))) = 1. [para(3(a,1),248(a,1,2,2))]. given #196 (T,wt=12): 537 (x ^ (y ^ z))' v (u v y) = 1. [para(66(a,1),248(a,1,2,2))]. given #197 (A,wt=13): 120 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. given #198 (T,wt=12): 538 (x ^ (y ^ z))' v (u v z) = 1. [para(94(a,1),248(a,1,2,2))]. given #199 (T,wt=12): 543 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),253(a,1,2,2))]. given #200 (T,wt=12): 550 (x v (y v z))' ^ (u ^ y) = 0. [para(48(a,1),253(a,1,2,2))]. given #201 (T,wt=12): 551 (x v (y v z))' ^ (u ^ z) = 0. [para(74(a,1),253(a,1,2,2))]. given #202 (A,wt=19): 121 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 #203 (T,wt=12): 552 (x ^ y)' v (z v (x v u)) = 1. [para(531(a,1),3(a,1,1)),rewrite([69(2),3(5)]),flip(a)]. given #204 (T,wt=12): 553 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),531(a,1,2))]. given #205 (T,wt=12): 617 (x ^ y)' v (z v (y v u)) = 1. [para(534(a,1),3(a,1,1)),rewrite([69(2),3(5)]),flip(a)]. given #206 (T,wt=12): 618 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),534(a,1,2))]. given #207 (A,wt=15): 122 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(15(a,1),21(a,1,2,2))]. given #208 (T,wt=12): 627 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(544(a,1),5(a,1,1)),rewrite([72(2),5(5)]),flip(a)]. given #209 (T,wt=12): 628 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),544(a,1,2))]. given #210 (T,wt=12): 632 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(546(a,1),5(a,1,1)),rewrite([72(2),5(5)]),flip(a)]. given #211 (T,wt=12): 633 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),546(a,1,2))]. given #212 (A,wt=17): 123 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(21(a,1),17(a,1,2)),flip(a)]. given #213 (T,wt=12): 644 (x v (y ^ z)) ^ (x v y)' = 0. [para(49(a,1),116(a,1,2,1))]. given #214 (T,wt=12): 647 x v (y v (x v (y ^ z))') = 1. [para(49(a,1),244(a,1,2)),rewrite([2(5),3(5)])]. given #215 (T,wt=12): 704 (x ^ (y v z)) v (x ^ y)' = 1. [para(65(a,1),152(a,1,2,1))]. given #216 (T,wt=12): 706 x ^ (y ^ (x ^ (y v z))') = 0. [para(65(a,1),245(a,1,2)),rewrite([4(5),5(5)])]. given #217 (A,wt=19): 124 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 #218 (T,wt=12): 723 ((x v y) ^ z) v (y ^ z)' = 1. [para(75(a,1),152(a,1,2,1))]. given #219 (T,wt=12): 727 x ^ (y ^ ((z v x) ^ y)') = 0. [para(32(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #220 (T,wt=12): 731 x ^ (y ^ (y ^ (z v x))') = 0. [para(214(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #221 (T,wt=12): 745 (x ^ (y v z)) v (x ^ z)' = 1. [para(78(a,1),152(a,1,2,1))]. given #222 (A,wt=19): 125 (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 #223 (T,wt=12): 749 x ^ (y ^ (x ^ (z v y))') = 0. [para(78(a,1),245(a,1,2)),rewrite([4(5),5(5)])]. given #224 (T,wt=12): 767 ((x ^ y) v z) ^ (y v z)' = 0. [para(92(a,1),116(a,1,2,1))]. given #225 (T,wt=12): 772 x v (y v ((z ^ x) v y)') = 1. [para(29(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #226 (T,wt=12): 778 x v (y v (y v (z ^ x))') = 1. [para(199(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #227 (A,wt=15): 126 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(21(a,1),20(a,1,2)),rewrite([20(3)]),flip(a)]. given #228 (T,wt=12): 828 (x v (y ^ z)) ^ (x v z)' = 0. [para(96(a,1),116(a,1,2,1))]. given #229 (T,wt=12): 831 x v (y v (x v (z ^ y))') = 1. [para(96(a,1),244(a,1,2)),rewrite([2(5),3(5)])]. given #230 (T,wt=12): 875 x v (y v (z ^ (y v x))') = 1. [para(168(a,1),158(a,1,2,1,2)),rewrite([3(5)])]. given #231 (T,wt=12): 876 x v (y v (z v (y v x)')) = 1. [para(168(a,1),160(a,1,2,2,1)),rewrite([3(5)])]. given #232 (A,wt=15): 132 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),48(a,1,2,2))]. given #233 (T,wt=12): 877 (x v y)' ^ (z ^ (y v x)) = 0. [para(168(a,1),253(a,1,2,2))]. given #234 (T,wt=12): 878 (x v y)' v (z v (y v x)) = 1. [para(168(a,1),534(a,1,1,1))]. given #235 (T,wt=12): 879 (x v y) ^ (y v (x v z))' = 0. [para(168(a,1),544(a,1,2)),rewrite([3(2),4(5)])]. given #236 (T,wt=12): 880 (x v y) ^ (z v (y v x))' = 0. [para(168(a,1),546(a,1,2)),rewrite([4(5)])]. given #237 (A,wt=13): 134 x ^ (y ^ (z v (x v u))) = y ^ x. [para(48(a,1),17(a,1,2)),flip(a)]. given #238 (T,wt=12): 890 (x v y) ^ ((y v x)' ^ z) = 0. [para(874(a,1),5(a,1,1)),rewrite([72(2)]),flip(a)]. given #239 (T,wt=12): 892 (x v y) ^ (z ^ (y v x)') = 0. [para(874(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #240 (T,wt=12): 994 x ^ (y ^ (z v (y ^ x))') = 0. [para(212(a,1),127(a,1,2,1,2)),rewrite([5(5)])]. given #241 (T,wt=12): 995 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(212(a,1),131(a,1,2,2,1)),rewrite([5(5)])]. given #242 (A,wt=13): 135 x v (y v (x v z)) = y v (x v z). [para(48(a,1),24(a,1,2)),rewrite([2(3)])]. given #243 (T,wt=12): 996 (x ^ y)' v (z v (y ^ x)) = 1. [para(212(a,1),248(a,1,2,2))]. given #244 (T,wt=12): 997 (x ^ y) v (y ^ (x ^ z))' = 1. [para(212(a,1),531(a,1,2)),rewrite([5(2),2(5)])]. given #245 (T,wt=12): 998 (x ^ y) v (z ^ (y ^ x))' = 1. [para(212(a,1),534(a,1,2)),rewrite([2(5)])]. given #246 (T,wt=12): 999 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(212(a,1),546(a,1,1,1))]. given #247 (A,wt=13): 137 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(52(a,1),5(a,2,2)),rewrite([17(3),5(2)])]. given #248 (T,wt=12): 1002 (x ^ y) v ((y ^ x)' v z) = 1. [para(992(a,1),3(a,1,1)),rewrite([69(2)]),flip(a)]. given #249 (T,wt=12): 1005 (x ^ y) v (z v (y ^ x)') = 1. [para(992(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #250 (T,wt=12): 1115 x v ((y v x)' v (z v y)) = 1. [para(29(a,1),86(a,1,1)),rewrite([3(6),61(7),29(9)])]. given #251 (T,wt=12): 1117 (x v y) ^ (y v (z v x))' = 0. [para(86(a,1),245(a,1,2)),rewrite([4(5)])]. given #252 (A,wt=13): 139 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),54(a,1,2)),rewrite([5(5)])]. given #253 (T,wt=12): 1242 ((x ^ y) v z) ^ (z v x)' = 0. [para(169(a,1),117(a,1,2,1))]. given #254 (T,wt=12): 1244 ((x ^ y) v z) ^ (z v y)' = 0. [para(768(a,1),117(a,1,2,1))]. given #255 (T,wt=12): 1245 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),118(a,1,2,2,1,1))]. given #256 (T,wt=12): 1304 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),150(a,1,1))]. given #257 (A,wt=17): 141 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 #258 (T,wt=12): 1306 (x v y)' ^ ((x ^ z) v y) = 0. [para(150(a,1),4(a,1)),flip(a)]. given #259 (T,wt=12): 1308 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),150(a,1,2,1))]. given #260 (T,wt=12): 1312 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(24(a,1),150(a,1,2,1))]. given #261 (T,wt=12): 1328 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),151(a,1,2,2,1,1))]. given #262 (A,wt=17): 142 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),22(a,1,2,1))]. given #263 (T,wt=12): 1359 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),153(a,1,2,1)),rewrite([5(3)])]. given #264 (T,wt=12): 1368 ((x v y) ^ z) v (z ^ x)' = 1. [para(140(a,1),153(a,1,2,1))]. given #265 (T,wt=12): 1370 ((x v y) ^ z) v (z ^ y)' = 1. [para(721(a,1),153(a,1,2,1))]. given #266 (T,wt=12): 1411 (x ^ y)' v ((x v z) ^ y) = 1. [para(162(a,1),2(a,1)),flip(a)]. given #267 (A,wt=22): 144 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(22(a,1),10(a,1))]. given #268 (T,wt=12): 1412 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),162(a,1,1))]. given #269 (T,wt=12): 1414 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),162(a,1,2,1))]. given #270 (T,wt=12): 1419 ((x v y) ^ (z v x)) v x' = 1. [para(18(a,1),162(a,1,2,1))]. given #271 (T,wt=12): 1490 x v (y v ((y ^ z) v x)') = 1. [para(204(a,1),15(a,1)),flip(a)]. given #272 (A,wt=15): 145 x v (y v ((x ^ z) v u)) = y v (x v u). [para(22(a,1),15(a,1,2)),flip(a)]. given #273 (T,wt=12): 1493 x v ((x ^ y) v (x ^ z))' = 1. [para(204(a,1),22(a,1)),flip(a)]. given #274 (T,wt=12): 1497 x v ((x ^ y) v (z ^ x))' = 1. [para(204(a,1),92(a,1)),flip(a)]. given #275 (T,wt=12): 1523 x ^ (y ^ ((y v z) ^ x)') = 0. [para(218(a,1),17(a,1)),flip(a)]. given #276 (T,wt=12): 1525 x ^ ((x v y) ^ (x v z))' = 0. [para(218(a,1),20(a,1)),flip(a)]. given #277 (A,wt=13): 146 x v ((y ^ (x ^ z)) v u) = x v u. [para(17(a,1),22(a,1,2,1))]. given #278 (T,wt=12): 1528 x ^ ((x v y) ^ (z v x))' = 0. [para(218(a,1),75(a,1)),flip(a)]. given #279 (T,wt=12): 1633 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),254(a,1,2,1,1))]. given #280 (T,wt=12): 2107 x v (y v ((z ^ y) v x)') = 1. [para(768(a,1),448(a,1,2)),rewrite([2(4)])]. given #281 (T,wt=12): 2181 x v ((y ^ x) v (x ^ z))' = 1. [para(454(a,1),92(a,1)),flip(a)]. given #282 (A,wt=15): 147 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite([4(4)])]. given #283 (T,wt=12): 2196 x ^ (y ^ ((z v y) ^ x)') = 0. [para(721(a,1),457(a,1,2)),rewrite([4(4)])]. given #284 (T,wt=12): 2228 x ^ ((y v x) ^ (x v z))' = 0. [para(462(a,1),75(a,1)),flip(a)]. given #285 (T,wt=12): 2769 (x v y)' ^ (x v (y ^ z)) = 0. [para(644(a,1),4(a,1)),flip(a)]. given #286 (T,wt=12): 2802 (x ^ y)' v (x ^ (y v z)) = 1. [para(704(a,1),2(a,1)),flip(a)]. given #287 (A,wt=15): 154 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(143(a,1),10(a,1)),flip(c),xx(a)]. given #288 (T,wt=7): 4930 x' != 0 | 1 = x. [para(245(a,1),154(a,1,2,1)),rewrite([71(3),4(3),61(3),245(6),71(5),228(6)])]. given #289 (T,wt=11): 4931 (x v y)' != 0 | x v y = 1. [para(544(a,1),154(a,1,2,1)),rewrite([71(4),4(4),61(4),544(8),71(6),228(8)]),flip(b)]. given #290 (T,wt=11): 4932 (x ^ y)' != 0 | x ^ y = 1. [para(999(a,1),154(a,1,2,1)),rewrite([71(4),4(4),61(4),999(9),71(6),228(8)]),flip(b)]. given #291 (T,wt=11): 4933 (x v y)' != 0 | y v x = 1. [para(2(a,1),4931(a,1,1))]. given #292 (A,wt=15): 159 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(152(a,1),10(a,1)),flip(c),xx(a)]. given #293 (T,wt=11): 4935 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),4932(a,1,1))]. given #294 (T,wt=12): 2929 (x ^ y)' v ((z v x) ^ y) = 1. [para(723(a,1),2(a,1)),flip(a)]. given #295 (T,wt=12): 2931 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),723(a,1,1))]. given #296 (T,wt=12): 2933 ((x v y) ^ (y v z)) v y' = 1. [para(6(a,1),723(a,1,2,1))]. given #297 (A,wt=14): 163 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(21(a,1),152(a,1,2,1))]. given #298 (T,wt=12): 2938 ((x v y) ^ (z v y)) v y' = 1. [para(18(a,1),723(a,1,2,1))]. given #299 (T,wt=12): 2988 x ^ ((y v x) ^ (z v x))' = 0. [para(727(a,1),75(a,1)),flip(a)]. given #300 (T,wt=12): 3029 (x ^ y)' v (x ^ (z v y)) = 1. [para(745(a,1),2(a,1)),flip(a)]. given #301 (T,wt=12): 3131 (x v (y ^ z)) ^ (z v x)' = 0. [para(2(a,1),767(a,1,1))]. given #302 (A,wt=14): 164 x v y != 1 | 0 != x | x' = x v y. [para(57(a,1),10(a,1)),rewrite([6(5)]),flip(b)]. given #303 (T,wt=12): 3132 (x v y)' ^ ((z ^ x) v y) = 0. [para(767(a,1),4(a,1)),flip(a)]. given #304 (T,wt=12): 3134 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(7(a,1),767(a,1,2,1))]. given #305 (T,wt=12): 3138 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(24(a,1),767(a,1,2,1))]. given #306 (T,wt=12): 3192 x v ((y ^ x) v (z ^ x))' = 1. [para(772(a,1),92(a,1)),flip(a)]. given #307 (A,wt=13): 166 x v (y v (z v x)) = y v (z v x). [para(3(a,1),59(a,1,2)),rewrite([3(5)])]. given #308 (T,wt=12): 3320 (x v y)' ^ (x v (z ^ y)) = 0. [para(828(a,1),4(a,1)),flip(a)]. given #309 (T,wt=12): 3706 (x v y)' ^ ((y ^ z) v x) = 0. [para(1242(a,1),4(a,1)),flip(a)]. given #310 (T,wt=12): 3722 (x v y)' ^ ((z ^ y) v x) = 0. [para(1244(a,1),4(a,1)),flip(a)]. given #311 (T,wt=12): 3773 (x v y)' ^ (y v (x ^ z)) = 0. [para(1304(a,1),4(a,1)),flip(a)]. given #312 (A,wt=14): 167 x v y != 1 | 0 != y | y' = x v y. [para(59(a,1),10(a,1)),rewrite([18(5)]),flip(b)]. given #313 (T,wt=12): 3922 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),1306(a,1,1,1))]. given #314 (T,wt=12): 3926 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(24(a,1),1306(a,1,1,1))]. given #315 (T,wt=12): 4161 (x ^ y)' v ((y v z) ^ x) = 1. [para(1368(a,1),2(a,1)),flip(a)]. given #316 (T,wt=12): 4183 (x ^ y)' v ((z v y) ^ x) = 1. [para(1370(a,1),2(a,1)),flip(a)]. given #317 (A,wt=13): 170 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),23(a,1,2,2,1))]. given #318 (T,wt=12): 4210 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),1411(a,1,2))]. given #319 (T,wt=12): 4212 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),1411(a,1,1,1))]. given #320 (T,wt=12): 4216 x' v ((x v y) ^ (z v x)) = 1. [para(18(a,1),1411(a,1,1,1))]. given #321 (T,wt=12): 4966 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),2929(a,1,2))]. given #322 (A,wt=19): 171 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 #323 (T,wt=12): 4968 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),2929(a,1,1,1))]. given #324 (T,wt=12): 4972 x' v ((y v x) ^ (z v x)) = 1. [para(18(a,1),2929(a,1,1,1))]. given #325 (T,wt=12): 5199 (x v y)' ^ (y v (z ^ x)) = 0. [para(3131(a,1),4(a,1)),flip(a)]. given #326 (T,wt=12): 5250 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(7(a,1),3132(a,1,1,1))]. given #327 (A,wt=26): 172 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))]. given #328 (T,wt=12): 5254 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(24(a,1),3132(a,1,1,1))]. given #329 (T,wt=13): 182 x v (y v (z ^ (x ^ u))) = y v x. [para(66(a,1),15(a,1,2)),flip(a)]. given #330 (T,wt=13): 184 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(74(a,1),5(a,1,1)),flip(a)]. given #331 (T,wt=13): 187 x ^ (y ^ (z v (u v x))) = y ^ x. [para(74(a,1),17(a,1,2)),flip(a)]. given #332 (A,wt=17): 173 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)]. given #333 (T,wt=13): 190 x v ((y ^ (z ^ x)) v u) = x v u. [para(94(a,1),3(a,1,1)),flip(a)]. given #334 (T,wt=13): 194 x v (y v (z ^ (u ^ x))) = y v x. [para(94(a,1),15(a,1,2)),flip(a)]. given #335 (T,wt=13): 205 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),25(a,1,1))]. given #336 (T,wt=13): 206 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),25(a,1,2)),rewrite([5(3)])]. given #337 (A,wt=19): 174 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 #338 (T,wt=13): 234 x ^ (x ^ y)' != 0 | x ^ y = x. [para(143(a,1),34(a,1)),rewrite([4(6),228(11)]),xx(a)]. given #339 (T,wt=13): 235 x ^ (y ^ x)' != 0 | y ^ x = x. [para(152(a,1),34(a,1)),rewrite([4(6),228(11)]),xx(a)]. given #340 (T,wt=13): 249 x' ^ (y v x) != 0 | y v x = x. [para(244(a,1),10(a,1)),rewrite([228(10)]),flip(c),xx(a)]. given #341 (T,wt=13): 793 x' ^ (x v y) != 0 | x v y = x. [para(70(a,1),51(a,1)),rewrite([228(10)]),flip(c),xx(a)]. given #342 (A,wt=15): 175 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(17(a,1),23(a,1,2,2))]. given #343 (T,wt=13): 849 x ^ (y v (z v (u v (x v w)))) = x. [para(3(a,1),133(a,1,2,2))]. given #344 (T,wt=13): 859 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(15(a,1),140(a,1,1))]. given #345 (T,wt=13): 873 x v (y v (z ^ (y v x))) = x v y. [para(168(a,1),94(a,1,2,2)),rewrite([3(4)])]. given #346 (T,wt=13): 881 (x v (y v z)) ^ (y v x) = y v x. [para(168(a,1),140(a,1,2)),rewrite([3(2),168(7)])]. given #347 (A,wt=19): 176 (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 #348 (T,wt=13): 899 (x ^ (y ^ z)) v (u v y) = u v y. [para(17(a,1),169(a,1,1))]. given #349 (T,wt=13): 916 x v (y ^ (z ^ (u ^ (x ^ w)))) = x. [para(5(a,1),180(a,1,2,2))]. given #350 (T,wt=13): 926 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(4(a,1),76(a,1,2,2,2))]. given #351 (T,wt=13): 946 x ^ (y v (z v (u v (w v x)))) = x. [para(3(a,1),183(a,1,2,2,2))]. given #352 (A,wt=14): 177 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(23(a,1),116(a,1,2,1))]. given #353 (T,wt=13): 963 x v (y ^ (z ^ (u ^ (w ^ x)))) = x. [para(5(a,1),192(a,1,2,2,2))]. given #354 (T,wt=13): 990 (x ^ (y ^ z)) v (y ^ x) = x ^ y. [para(212(a,1),22(a,2)),rewrite([5(3),985(6)])]. given #355 (T,wt=13): 1009 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),77(a,1,2)),rewrite([3(3)])]. given #356 (T,wt=13): 1037 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),721(a,1,1))]. given #357 (A,wt=15): 178 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 #358 (T,wt=13): 1052 (x v (y v z)) ^ (z v y) = z v y. [para(168(a,1),721(a,1,2)),rewrite([168(7)])]. given #359 (T,wt=13): 1057 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),768(a,1,1))]. given #360 (T,wt=13): 1081 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(212(a,1),768(a,1,2)),rewrite([212(7)])]. given #361 (T,wt=13): 1105 (x v (y v z)) ^ (z v x) = z v x. [para(86(a,1),4(a,1)),flip(a)]. given #362 (A,wt=15): 179 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),66(a,1,2,2))]. given #363 (T,wt=13): 1682 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),97(a,1,2)),rewrite([5(3)])]. given #364 (T,wt=13): 3248 x ^ (((x v y) ^ (x v z)) v u) = x. [para(126(a,1),20(a,1)),rewrite([6(2)]),flip(a)]. given #365 (T,wt=13): 3261 x ^ (((x v y) ^ (z v x)) v u) = x. [para(126(a,1),75(a,1)),rewrite([18(2)]),flip(a)]. given #366 (T,wt=13): 3949 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(228(a,1),1308(a,1,2)),rewrite([4(6)])]. given #367 (A,wt=18): 181 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(66(a,1),10(a,1)),rewrite([137(5)]),flip(a)]. given #368 (T,wt=13): 3962 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(228(a,1),1312(a,1,2)),rewrite([4(6)])]. given #369 (T,wt=13): 4327 x v ((x' v y) ^ (x' v z)) = 1. [para(228(a,1),1414(a,1,2)),rewrite([2(6)])]. given #370 (T,wt=13): 4350 x v ((x' v y) ^ (z v x')) = 1. [para(228(a,1),1419(a,1,2)),rewrite([2(6)])]. given #371 (T,wt=13): 5077 x v ((y v x') ^ (x' v z)) = 1. [para(228(a,1),2933(a,1,2)),rewrite([2(6)])]. given #372 (A,wt=15): 185 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(74(a,1),5(a,1)),flip(a)]. given #373 (T,wt=13): 5116 x v ((y v x') ^ (z v x')) = 1. [para(228(a,1),2938(a,1,2)),rewrite([2(6)])]. given #374 (T,wt=13): 5274 x v (y v x)' != 1 | y v x = x. [para(3132(a,1),144(b,1)),rewrite([2(3),228(11),4(12),103(12),62(11)]),xx(b)]. given #375 (T,wt=13): 5283 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(228(a,1),3134(a,1,2)),rewrite([4(6)])]. given #376 (T,wt=13): 5298 x ^ ((y ^ x') v (z ^ x')) = 0. [para(228(a,1),3138(a,1,2)),rewrite([4(6)])]. given #377 (A,wt=15): 186 (x v y) ^ (z v (x v (u v y))) = x v y. [para(15(a,1),74(a,1,2,2))]. given #378 (T,wt=13): 5449 x v (x v y)' != 1 | x v y = x. [para(3722(a,1),144(b,1)),rewrite([2(3),228(11),4(12),116(12),62(11)]),xx(b)]. given #379 (T,wt=13): 5894 x' v (x ^ y) != 1 | x ^ y = x. [para(5250(a,1),144(b,1)),rewrite([228(10),4(10),9(10),62(11)]),flip(c),xx(b)]. given #380 (T,wt=13): 6015 x' v (y ^ x) != 1 | y ^ x = x. [para(5254(a,1),144(b,1)),rewrite([228(10),4(10),9(10),62(11)]),flip(c),xx(b)]. given #381 (T,wt=13): 6678 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(206(a,1),2(a,1)),flip(a)]. given #382 (A,wt=17): 188 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(22(a,1),74(a,1,2,2))]. given #383 (T,wt=13): 6898 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),234(a,1,2,1))]. given #384 (T,wt=13): 6903 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),235(a,1,2,1))]. given #385 (T,wt=13): 6905 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),235(a,1,2,1)),rewrite([6(7)]),flip(b)]. given #386 (T,wt=13): 6907 (x v y) ^ y' != 0 | x v y = y. [para(18(a,1),235(a,1,2,1)),rewrite([18(7)]),flip(b)]. given #387 (A,wt=21): 189 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(23(a,1),74(a,1,2,2))]. given #388 (T,wt=13): 6939 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),249(a,1,2))]. given #389 (T,wt=13): 6957 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),793(a,1,2))]. given #390 (T,wt=13): 7941 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(178(a,1),22(a,1)),rewrite([7(2)]),flip(a)]. given #391 (T,wt=13): 7956 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(178(a,1),92(a,1)),rewrite([24(2)]),flip(a)]. given #392 (A,wt=15): 191 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(94(a,1),3(a,1)),flip(a)]. given #393 (T,wt=13): 8383 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),3248(a,1,2,1,1))]. given #394 (T,wt=13): 8384 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),3248(a,1,2))]. given #395 (T,wt=13): 8470 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),3261(a,1,2,1,1))]. given #396 (T,wt=13): 8471 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),3261(a,1,2))]. given #397 (A,wt=18): 193 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(94(a,1),10(a,1)),rewrite([139(5)]),flip(a)]. given #398 (T,wt=13): 8827 x v (x v y)' != 1 | y v x = x. [para(2(a,1),5274(a,1,2,1))]. given #399 (T,wt=13): 8830 (x ^ y) v x' != 1 | x ^ y = x. [para(7(a,1),5274(a,1,2,1)),rewrite([7(7)]),flip(b)]. given #400 (T,wt=13): 8832 (x ^ y) v y' != 1 | x ^ y = y. [para(24(a,1),5274(a,1,2,1)),rewrite([24(7)]),flip(b)]. given #401 (T,wt=13): 8980 x v (y v x)' != 1 | x v y = x. [para(2(a,1),5449(a,1,2,1))]. given #402 (A,wt=15): 195 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(17(a,1),94(a,1,2,2))]. given #403 (T,wt=13): 8990 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),5894(a,1,2))]. given #404 (T,wt=13): 9004 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),6015(a,1,2))]. given #405 (T,wt=13): 9213 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),6905(a,1,1))]. given #406 (T,wt=13): 9218 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),6907(a,1,1))]. given #407 (A,wt=17): 196 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(19(a,1),94(a,1,2,2)),rewrite([3(5),3(4)])]. given #408 (T,wt=13): 9342 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),7941(a,1,2,1,1))]. given #409 (T,wt=13): 9343 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),7941(a,1,2))]. given #410 (T,wt=13): 9442 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),7956(a,1,2,1,1))]. given #411 (T,wt=13): 9443 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),7956(a,1,2))]. given #412 (A,wt=17): 197 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(20(a,1),94(a,1,2,2))]. given #413 (T,wt=13): 9672 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),8383(a,1,2))]. given #414 (T,wt=13): 9847 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),8470(a,1,2))]. given #415 (T,wt=13): 10134 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),8830(a,1,1))]. given #416 (T,wt=13): 10139 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),8832(a,1,1))]. given #417 (A,wt=21): 198 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(21(a,1),94(a,1,2,2))]. given #418 (T,wt=13): 10425 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(4(a,1),9342(a,1,2))]. given #419 (T,wt=13): 10620 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),9442(a,1,2))]. given #420 (T,wt=14): 200 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 #421 (T,wt=14): 203 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 #422 (A,wt=19): 201 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(29(a,1),10(a,1)),flip(c),xx(a)]. Low Water (keep): wt=39.000, iters=6681 given #423 (T,wt=14): 215 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(32(a,1),5(a,1)),rewrite([5(3)]),flip(a)]. given #424 (T,wt=14): 217 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(17(a,1),32(a,1,2,2,1)),rewrite([5(5)])]. given #425 (T,wt=14): 219 x v (y v (z v ((x v y)' v u))) = 1. [para(101(a,1),3(a,1)),flip(a)]. given #426 (T,wt=14): 223 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0. [para(108(a,1),5(a,1)),flip(a)]. given #427 (A,wt=19): 207 (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 #428 (T,wt=14): 227 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),34(a,1)),rewrite([4(4),52(4)]),flip(a)]. given #429 (T,wt=14): 230 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.000, iters=6736 given #430 (T,wt=14): 236 x v y != 1 | 0 != x | (x v y)' = x. [para(57(a,1),34(a,1)),rewrite([4(5),6(5)]),flip(b)]. given #431 (T,wt=14): 237 x v y != 1 | 0 != y | (x v y)' = y. [para(59(a,1),34(a,1)),rewrite([4(5),18(5)]),flip(b)]. given #432 (A,wt=22): 208 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),137(6),52(6)])]. given #433 (T,wt=14): 251 x v (y v (y v ((x v y) ^ z))') = 1. [para(23(a,1),244(a,1,2)),rewrite([2(6),3(6)])]. given #434 (T,wt=14): 255 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(21(a,1),245(a,1,2)),rewrite([4(6),5(6)])]. given #435 (T,wt=14): 256 (x v y) ^ ((x v (y v z))' ^ u) = 0. [para(3(a,1),109(a,1,2,1,1))]. given #436 (T,wt=14): 257 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0. [para(109(a,1),5(a,1)),flip(a)]. given #437 (A,wt=17): 209 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(25(a,1),15(a,1,2)),flip(a)]. Low Water (keep): wt=37.000, iters=6828 Low Water (keep): wt=35.000, iters=6775 given #438 (T,wt=14): 275 x v y != 1 | 0 != y | (y v x)' = y. [para(59(a,1),35(a,1)),rewrite([4(5),6(5)]),flip(b)]. Low Water (keep): wt=34.000, iters=6738 given #439 (T,wt=14): 285 x v (y v (z v (u v (x v y)'))) = 1. [para(111(a,1),3(a,1)),flip(a)]. given #440 (T,wt=14): 292 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0. [para(114(a,1),5(a,1)),flip(a)]. given #441 (T,wt=14): 295 (x v y) ^ (z ^ (x v (y v u))') = 0. [para(3(a,1),115(a,1,2,2,1))]. Low Water (keep): wt=33.000, iters=6692 given #442 (A,wt=19): 210 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(17(a,1),25(a,1,1)),rewrite([5(4)])]. given #443 (T,wt=14): 296 x ^ (y ^ (z ^ ((x ^ y) v u)')) = 0. [para(115(a,1),5(a,1)),flip(a)]. given #444 (T,wt=14): 298 (x v y) ^ (z v (x v (y v u)))' = 0. [para(3(a,1),119(a,1,2,1,2))]. given #445 (T,wt=14): 300 x ^ (y ^ (z v ((x ^ y) v u))') = 0. [para(119(a,1),5(a,1)),flip(a)]. given #446 (T,wt=14): 335 x ^ (y ^ (z v (u v (x ^ y)))') = 0. [para(127(a,1),5(a,1)),flip(a)]. given #447 (A,wt=15): 211 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(17(a,1),25(a,1,2,2))]. given #448 (T,wt=14): 336 (x v y) ^ (z v (x v (u v y)))' = 0. [para(15(a,1),127(a,1,2,1,2))]. given #449 (T,wt=14): 338 ((x ^ y) v z) ^ (u v (x v z))' = 0. [para(22(a,1),127(a,1,2,1,2))]. given #450 (T,wt=14): 340 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0. [para(25(a,1),127(a,1,2,1,2)),rewrite([5(6),5(5)])]. Low Water (keep): wt=31.000, iters=6778 given #451 (T,wt=14): 341 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0. [para(128(a,1),5(a,1)),flip(a)]. given #452 (A,wt=17): 213 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(25(a,1),74(a,1,2,2)),rewrite([5(5),5(4)])]. given #453 (T,wt=14): 342 (x v y) ^ ((x v (z v y))' ^ u) = 0. [para(15(a,1),128(a,1,2,1,1))]. given #454 (T,wt=14): 344 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0. [para(22(a,1),128(a,1,2,1,1))]. given #455 (T,wt=14): 347 (x v y) ^ (z ^ (x v (u v y))') = 0. [para(15(a,1),131(a,1,2,2,1))]. given #456 (T,wt=14): 348 ((x ^ y) v z) ^ (u ^ (x v z)') = 0. [para(22(a,1),131(a,1,2,2,1))]. given #457 (A,wt=19): 221 x ^ (y v (x' v z)) != 0 | y v (x' v z) = x'. [para(101(a,1),10(a,1)),flip(c),xx(a)]. given #458 (T,wt=14): 350 x v (y v (((x v y) ^ z)' v u)) = 1. [para(148(a,1),3(a,1)),flip(a)]. given #459 (T,wt=14): 351 (x ^ y) v ((x ^ (y ^ z))' v u) = 1. [para(5(a,1),148(a,1,2,1,1))]. given #460 (T,wt=14): 372 x v (y v (z v ((x v y) ^ u)')) = 1. [para(149(a,1),3(a,1)),flip(a)]. given #461 (T,wt=14): 373 (x ^ y) v (z v (x ^ (y ^ u))') = 1. [para(5(a,1),149(a,1,2,2,1))]. given #462 (A,wt=20): 226 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),34(a,1))]. Low Water (keep): wt=30.000, iters=6854 Low Water (keep): wt=29.000, iters=6753 given #463 (T,wt=14): 379 x v (y v (z ^ ((x v y) ^ u))') = 1. [para(155(a,1),3(a,1)),flip(a)]. given #464 (T,wt=14): 380 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1. [para(5(a,1),155(a,1,2,1,2))]. given #465 (T,wt=14): 385 x v (y v ((z ^ (x v y))' v u)) = 1. [para(156(a,1),3(a,1)),flip(a)]. given #466 (T,wt=14): 389 (x ^ y) v ((x ^ (z ^ y))' v u) = 1. [para(17(a,1),156(a,1,2,1,1))]. given #467 (A,wt=20): 229 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(15(a,1),34(a,1))]. given #468 (T,wt=14): 390 ((x v y) ^ z) v ((x ^ z)' v u) = 1. [para(20(a,1),156(a,1,2,1,1))]. Low Water (keep): wt=28.000, iters=6694 given #469 (T,wt=14): 394 x v (y v (z ^ (u ^ (x v y)))') = 1. [para(158(a,1),3(a,1)),flip(a)]. Low Water (keep): wt=27.000, iters=6676 given #470 (T,wt=14): 398 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1. [para(17(a,1),158(a,1,2,1,2))]. given #471 (T,wt=14): 399 x v (y v (z v (u ^ (x v y))')) = 1. [para(19(a,1),158(a,1,2,1,2)),rewrite([3(6),3(5)])]. given #472 (A,wt=15): 231 x ^ (x' v y) != 0 | (x' v y)' = x. [para(70(a,1),34(a,1)),rewrite([4(6)]),xx(a)]. given #473 (T,wt=14): 400 ((x v y) ^ z) v (u ^ (x ^ z))' = 1. [para(20(a,1),158(a,1,2,1,2))]. given #474 (T,wt=14): 442 (x ^ y) v (z v (x ^ (u ^ y))') = 1. [para(17(a,1),160(a,1,2,2,1))]. given #475 (T,wt=14): 443 ((x v y) ^ z) v (u v (x ^ z)') = 1. [para(20(a,1),160(a,1,2,2,1))]. given #476 (T,wt=14): 449 x v (y v (z v (z v (x v y))')) = 1. [para(199(a,1),3(a,1)),flip(a)]. given #477 (A,wt=15): 232 x ^ (y v x') != 0 | (y v x')' = x. [para(80(a,1),34(a,1)),rewrite([4(6)]),xx(a)]. given #478 (T,wt=14): 450 x v (y v (z v (y v (z v x))')) = 1. [para(3(a,1),199(a,1,2,2,1)),rewrite([3(5)])]. given #479 (T,wt=14): 453 x v (y v (z v (x v (z v y))')) = 1. [para(15(a,1),199(a,1,2,2,1)),rewrite([3(6)])]. given #480 (T,wt=14): 458 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0. [para(214(a,1),5(a,1)),flip(a)]. given #481 (T,wt=14): 459 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0. [para(5(a,1),214(a,1,2,2,1)),rewrite([5(5)])]. given #482 (A,wt=22): 233 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 #483 (T,wt=14): 461 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0. [para(17(a,1),214(a,1,2,2,1)),rewrite([5(6)])]. given #484 (T,wt=14): 463 (x v y)' v (z v (x v (y v u))) = 1. [para(3(a,1),246(a,1,2,2))]. given #485 (T,wt=14): 528 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0. [para(5(a,1),247(a,1,2,2))]. given #486 (T,wt=14): 533 (x v y)' v (z v (x v (u v y))) = 1. [para(15(a,1),248(a,1,2,2))]. given #487 (A,wt=26): 238 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 #488 (T,wt=14): 535 ((x ^ y) v z)' v (u v (x v z)) = 1. [para(22(a,1),248(a,1,2,2))]. given #489 (T,wt=14): 539 (x ^ (y ^ z))' v (u v (x ^ y)) = 1. [para(25(a,1),248(a,1,2,2))]. given #490 (T,wt=14): 545 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0. [para(17(a,1),253(a,1,2,2))]. given #491 (T,wt=14): 547 (x v (y v z))' ^ (u ^ (x v y)) = 0. [para(19(a,1),253(a,1,2,2))]. given #492 (A,wt=18): 239 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(66(a,1),34(a,1)),rewrite([4(5),137(5)]),flip(a)]. given #493 (T,wt=14): 548 ((x v y) ^ z)' ^ (u ^ (x ^ z)) = 0. [para(20(a,1),253(a,1,2,2))]. given #494 (T,wt=14): 555 x v (((x v y) ^ z)' v (u v y)) = 1. [para(15(a,1),531(a,1,2)),rewrite([15(6)])]. given #495 (T,wt=14): 556 x v (y v (((x ^ z) v y) ^ u)') = 1. [para(22(a,1),531(a,1,2)),rewrite([2(6),3(6)])]. Low Water (keep): wt=26.000, iters=6740 given #496 (T,wt=14): 620 x v ((y ^ (x v z))' v (u v z)) = 1. [para(15(a,1),534(a,1,2)),rewrite([15(6)])]. given #497 (A,wt=18): 240 1 != x | y ^ (z ^ x) != 0 | (y ^ (z ^ x))' = x. [para(94(a,1),34(a,1)),rewrite([4(5),139(5)]),flip(a)]. given #498 (T,wt=14): 621 (x ^ (y ^ z))' v (u v (x ^ z)) = 1. [para(17(a,1),534(a,1,1,1))]. given #499 (T,wt=14): 622 (x ^ y)' v (z v ((x v u) ^ y)) = 1. [para(20(a,1),534(a,1,1,1))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 170 (0.00 of 8.52 sec). given #500 (T,wt=14): 624 x v (y v (z ^ ((x ^ u) v y))') = 1. [para(22(a,1),534(a,1,2)),rewrite([2(6),3(6)])]. given #501 (T,wt=14): 629 x ^ (((x ^ y) v z)' ^ (u ^ y)) = 0. [para(17(a,1),544(a,1,2)),rewrite([17(6)])]. given #502 (A,wt=19): 241 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 #503 (T,wt=14): 630 x ^ (y ^ (((x v z) ^ y) v u)') = 0. [para(20(a,1),544(a,1,2)),rewrite([4(6),5(6)])]. given #504 (T,wt=14): 634 (x v (y v z))' ^ (u ^ (x v z)) = 0. [para(15(a,1),546(a,1,1,1))]. given #505 (T,wt=14): 635 x ^ ((y v (x ^ z))' ^ (u ^ z)) = 0. [para(17(a,1),546(a,1,2)),rewrite([17(6)])]. Low Water (keep): wt=25.000, iters=6708 given #506 (T,wt=14): 636 x ^ (y ^ (z v ((x v u) ^ y))') = 0. [para(20(a,1),546(a,1,2)),rewrite([4(6),5(6)])]. given #507 (A,wt=22): 242 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),137(6),52(6)])]. given #508 (T,wt=14): 638 (x v y)' ^ (z ^ ((x ^ u) v y)) = 0. [para(22(a,1),546(a,1,1,1))]. given #509 (T,wt=14): 650 (x v (y ^ z)) ^ (u v (x v y))' = 0. [para(49(a,1),127(a,1,2,1,2))]. given #510 (T,wt=14): 651 (x v (y ^ z)) ^ ((x v y)' ^ u) = 0. [para(49(a,1),128(a,1,2,1,1))]. given #511 (T,wt=14): 652 (x v (y ^ z)) ^ (u ^ (x v y)') = 0. [para(49(a,1),131(a,1,2,2,1))]. given #512 (A,wt=19): 243 x ^ (y v (x' v z)) != 0 | (y v (x' v z))' = x. [para(101(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #513 (T,wt=14): 653 (x v (y ^ z))' v (u v (x v y)) = 1. [para(49(a,1),248(a,1,2,2))]. given #514 (T,wt=14): 654 x v (y v ((x v (y ^ z)) ^ u)') = 1. [para(49(a,1),531(a,1,2)),rewrite([2(6),3(6)])]. given #515 (T,wt=14): 655 x v (y v (z ^ (x v (y ^ u)))') = 1. [para(49(a,1),534(a,1,2)),rewrite([2(6),3(6)])]. given #516 (T,wt=14): 656 (x v y)' ^ (z ^ (x v (y ^ u))) = 0. [para(49(a,1),546(a,1,1,1))]. given #517 (A,wt=15): 252 (x v y) ^ y' != 0 | (x v y)' = y'. [para(244(a,1),34(a,1)),xx(a)]. given #518 (T,wt=14): 707 (x ^ (y v z)) v ((x ^ y)' v u) = 1. [para(65(a,1),156(a,1,2,1,1))]. given #519 (T,wt=14): 708 (x ^ (y v z)) v (u ^ (x ^ y))' = 1. [para(65(a,1),158(a,1,2,1,2))]. given #520 (T,wt=14): 709 (x ^ (y v z)) v (u v (x ^ y)') = 1. [para(65(a,1),160(a,1,2,2,1))]. given #521 (T,wt=14): 710 (x ^ (y v z))' ^ (u ^ (x ^ y)) = 0. [para(65(a,1),253(a,1,2,2))]. given #522 (A,wt=20): 259 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 #523 (T,wt=14): 711 (x ^ y)' v (z v (x ^ (y v u))) = 1. [para(65(a,1),534(a,1,1,1))]. given #524 (T,wt=14): 712 x ^ (y ^ ((x ^ (y v z)) v u)') = 0. [para(65(a,1),544(a,1,2)),rewrite([4(6),5(6)])]. given #525 (T,wt=14): 713 x ^ (y ^ (z v (x ^ (y v u)))') = 0. [para(65(a,1),546(a,1,2)),rewrite([4(6),5(6)])]. given #526 (T,wt=14): 728 ((x v y) ^ z) v ((y ^ z)' v u) = 1. [para(75(a,1),156(a,1,2,1,1))]. Low Water (keep): wt=24.000, iters=6667 given #527 (A,wt=26): 260 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 #528 (T,wt=14): 729 ((x v y) ^ z) v (u ^ (y ^ z))' = 1. [para(75(a,1),158(a,1,2,1,2))]. given #529 (T,wt=14): 730 ((x v y) ^ z) v (u v (y ^ z)') = 1. [para(75(a,1),160(a,1,2,2,1))]. given #530 (T,wt=14): 732 ((x v y) ^ z)' ^ (u ^ (y ^ z)) = 0. [para(75(a,1),253(a,1,2,2))]. given #531 (T,wt=14): 733 (x ^ y)' v (z v ((u v x) ^ y)) = 1. [para(75(a,1),534(a,1,1,1))]. given #532 (A,wt=18): 261 x v y != 1 | y ^ z != 0 | (x v y)' = y ^ z. [para(7(a,1),35(a,1,2)),rewrite([17(6),75(6)])]. given #533 (T,wt=14): 734 x ^ (y ^ (((z v x) ^ y) v u)') = 0. [para(75(a,1),544(a,1,2)),rewrite([4(6),5(6)])]. given #534 (T,wt=14): 735 x ^ (y ^ (z v ((u v x) ^ y))') = 0. [para(75(a,1),546(a,1,2)),rewrite([4(6),5(6)])]. given #535 (T,wt=14): 750 (x ^ (y v z)) v ((x ^ z)' v u) = 1. [para(78(a,1),156(a,1,2,1,1))]. given #536 (T,wt=14): 751 (x ^ (y v z)) v (u ^ (x ^ z))' = 1. [para(78(a,1),158(a,1,2,1,2))]. given #537 (A,wt=26): 262 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))]. Low Water (keep): wt=23.000, iters=6729 given #538 (T,wt=14): 752 (x ^ (y v z)) v (u v (x ^ z)') = 1. [para(78(a,1),160(a,1,2,2,1))]. given #539 (T,wt=14): 753 (x ^ (y v z))' ^ (u ^ (x ^ z)) = 0. [para(78(a,1),253(a,1,2,2))]. given #540 (T,wt=14): 754 (x ^ y)' v (z v (x ^ (u v y))) = 1. [para(78(a,1),534(a,1,1,1))]. given #541 (T,wt=14): 755 x ^ (y ^ ((x ^ (z v y)) v u)') = 0. [para(78(a,1),544(a,1,2)),rewrite([4(6),5(6)])]. given #542 (A,wt=20): 263 x v (y v z) != 1 | (y v x) ^ z != 0 | (y v x)' = z. [para(15(a,1),35(a,1))]. given #543 (T,wt=14): 756 x ^ (y ^ (z v (x ^ (u v y)))') = 0. [para(78(a,1),546(a,1,2)),rewrite([4(6),5(6)])]. given #544 (T,wt=14): 775 ((x ^ y) v z) ^ (u v (y v z))' = 0. [para(92(a,1),127(a,1,2,1,2))]. given #545 (T,wt=14): 776 ((x ^ y) v z) ^ ((y v z)' ^ u) = 0. [para(92(a,1),128(a,1,2,1,1))]. given #546 (T,wt=14): 777 ((x ^ y) v z) ^ (u ^ (y v z)') = 0. [para(92(a,1),131(a,1,2,2,1))]. given #547 (A,wt=19): 267 (x v y) ^ (y' v z) != 0 | (x v y)' = y' v z. [para(70(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #548 (T,wt=14): 779 ((x ^ y) v z)' v (u v (y v z)) = 1. [para(92(a,1),248(a,1,2,2))]. given #549 (T,wt=14): 780 x v (y v (((z ^ x) v y) ^ u)') = 1. [para(92(a,1),531(a,1,2)),rewrite([2(6),3(6)])]. Low Water (keep): wt=22.000, iters=6715 given #550 (T,wt=14): 781 x v (y v (z ^ ((u ^ x) v y))') = 1. [para(92(a,1),534(a,1,2)),rewrite([2(6),3(6)])]. given #551 (T,wt=14): 782 (x v y)' ^ (z ^ ((u ^ x) v y)) = 0. [para(92(a,1),546(a,1,1,1))]. given #552 (A,wt=19): 268 (x v y) ^ (z v y') != 0 | (x v y)' = z v y'. [para(80(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #553 (T,wt=14): 834 (x v (y ^ z)) ^ (u v (x v z))' = 0. [para(96(a,1),127(a,1,2,1,2))]. given #554 (T,wt=14): 835 (x v (y ^ z)) ^ ((x v z)' ^ u) = 0. [para(96(a,1),128(a,1,2,1,1))]. given #555 (T,wt=14): 836 (x v (y ^ z)) ^ (u ^ (x v z)') = 0. [para(96(a,1),131(a,1,2,2,1))]. given #556 (T,wt=14): 837 (x v (y ^ z))' v (u v (x v z)) = 1. [para(96(a,1),248(a,1,2,2))]. given #557 (A,wt=15): 269 (x v y) ^ x' != 0 | (x v y)' = x'. [para(80(a,1),35(a,1)),xx(a)]. given #558 (T,wt=14): 838 x v (y v ((x v (z ^ y)) ^ u)') = 1. [para(96(a,1),531(a,1,2)),rewrite([2(6),3(6)])]. given #559 (T,wt=14): 839 x v (y v (z ^ (x v (u ^ y)))') = 1. [para(96(a,1),534(a,1,2)),rewrite([2(6),3(6)])]. given #560 (T,wt=14): 840 (x v y)' ^ (z ^ (x v (u ^ y))) = 0. [para(96(a,1),546(a,1,1,1))]. given #561 (T,wt=14): 853 (x v (y v (z v u)))' ^ (w ^ z) = 0. [para(133(a,1),253(a,1,2,2))]. given #562 (A,wt=28): 270 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 #563 (T,wt=14): 854 x' v (y v (z v (u v (x v w)))) = 1. [para(133(a,1),534(a,1,1,1))]. given #564 (T,wt=14): 855 x ^ (y v (z v (u v (x v w))))' = 0. [para(133(a,1),546(a,1,2)),rewrite([4(6)])]. given #565 (T,wt=14): 882 1 != x | y ^ x != 0 | x' = x ^ y. [para(4(a,1),56(b,1))]. given #566 (T,wt=14): 888 (x v (y v z)) ^ (z v (x v y))' = 0. [para(3(a,1),874(a,1,1))]. given #567 (A,wt=19): 271 (x v y) ^ (y ^ z)' != 0 | (x v y)' = (y ^ z)'. [para(143(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #568 (T,wt=14): 889 (x v (y v z)) ^ (y v (z v x))' = 0. [para(3(a,1),874(a,1,2,1))]. given #569 (T,wt=14): 891 (x v (y v z)) ^ (x v (z v y))' = 0. [para(15(a,1),874(a,1,1)),rewrite([3(4)])]. given #570 (T,wt=14): 921 (x ^ (y ^ (z ^ u)))' v (w v z) = 1. [para(180(a,1),248(a,1,2,2))]. given #571 (T,wt=14): 922 x v (y ^ (z ^ (u ^ (x ^ w))))' = 1. [para(180(a,1),534(a,1,2)),rewrite([2(6)])]. given #572 (A,wt=19): 272 (x v y) ^ (z ^ y)' != 0 | (x v y)' = (z ^ y)'. [para(152(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #573 (T,wt=14): 923 x' ^ (y ^ (z ^ (u ^ (x ^ w)))) = 0. [para(180(a,1),546(a,1,1,1))]. given #574 (T,wt=14): 931 (x ^ (y v (z ^ x))) v (z ^ x)' = 1. [para(76(a,1),152(a,1,2,1))]. given #575 (T,wt=14): 933 x ^ (y ^ (y ^ (z v (x ^ y)))') = 0. [para(76(a,1),245(a,1,2)),rewrite([4(6),5(6)])]. given #576 (T,wt=14): 954 (x v (y v (z v u)))' ^ (w ^ u) = 0. [para(183(a,1),253(a,1,2,2))]. given #577 (A,wt=24): 273 x v (y v z) != 1 | (x v y) ^ (y v z) != 0 | (x v y)' = y v z. [para(57(a,1),35(a,1,2))]. given #578 (T,wt=14): 955 x' v (y v (z v (u v (w v x)))) = 1. [para(183(a,1),534(a,1,1,1))]. given #579 (T,wt=14): 956 x ^ (y v (z v (u v (w v x))))' = 0. [para(183(a,1),546(a,1,2)),rewrite([4(6)])]. given #580 (T,wt=14): 972 (x ^ (y ^ (z ^ u)))' v (w v u) = 1. [para(192(a,1),248(a,1,2,2))]. given #581 (T,wt=14): 973 x v (y ^ (z ^ (u ^ (w ^ x))))' = 1. [para(192(a,1),534(a,1,2)),rewrite([2(6)])]. given #582 (A,wt=24): 274 x v (y v z) != 1 | (x v z) ^ (y v z) != 0 | (x v z)' = y v z. [para(59(a,1),35(a,1,2))]. given #583 (T,wt=14): 974 x' ^ (y ^ (z ^ (u ^ (w ^ x)))) = 0. [para(192(a,1),546(a,1,1,1))]. given #584 (T,wt=14): 1003 (x ^ (y ^ z)) v (z ^ (x ^ y))' = 1. [para(5(a,1),992(a,1,1))]. given #585 (T,wt=14): 1004 (x ^ (y ^ z)) v (y ^ (z ^ x))' = 1. [para(5(a,1),992(a,1,2,1))]. given #586 (T,wt=14): 1006 (x ^ (y ^ z)) v (x ^ (z ^ y))' = 1. [para(17(a,1),992(a,1,1)),rewrite([5(4)])]. given #587 (A,wt=32): 276 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 #588 (T,wt=14): 1020 x v (y v (z v ((x v z)' v u))) = 1. [para(77(a,1),156(a,1,2,1,1)),rewrite([3(6),3(5)])]. given #589 (T,wt=14): 1021 x v (y v (z v (u ^ (x v z))')) = 1. [para(77(a,1),158(a,1,2,1,2)),rewrite([3(6),3(5)])]. given #590 (T,wt=14): 1022 x v (y v (z v (u v (x v z)'))) = 1. [para(77(a,1),160(a,1,2,2,1)),rewrite([3(6),3(5)])]. given #591 (T,wt=14): 1023 (x v y) ^ (x v (z v (y v u)))' = 0. [para(77(a,1),544(a,1,2)),rewrite([3(3),3(2),4(6)])]. given #592 (A,wt=22): 277 x v y != 1 | (x v y) ^ z != 0 | (x v y)' = (x v y) ^ z. [para(23(a,1),35(a,1)),rewrite([52(7)])]. given #593 (T,wt=14): 1118 x v (y v (z v ((z v x)' v u))) = 1. [para(86(a,1),156(a,1,2,1,1)),rewrite([3(6),3(5)])]. given #594 (T,wt=14): 1119 x v (y v (z v (u ^ (z v x))')) = 1. [para(86(a,1),158(a,1,2,1,2)),rewrite([3(6),3(5)])]. given #595 (T,wt=14): 1120 x v (y v (z v (u v (z v x)'))) = 1. [para(86(a,1),160(a,1,2,2,1)),rewrite([3(6),3(5)])]. given #596 (T,wt=14): 1121 (x v (y v z))' ^ (u ^ (z v x)) = 0. [para(86(a,1),253(a,1,2,2))]. given #597 (A,wt=23): 280 (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([79(2)]),xx(a)]. given #598 (T,wt=14): 1122 (x v y)' v (z v (y v (u v x))) = 1. [para(86(a,1),534(a,1,1,1))]. given #599 (T,wt=14): 1123 (x v y) ^ (y v (z v (x v u)))' = 0. [para(86(a,1),544(a,1,2)),rewrite([3(3),3(2),4(6)])]. given #600 (T,wt=14): 1124 (x v y) ^ (z v (y v (u v x)))' = 0. [para(86(a,1),546(a,1,2)),rewrite([4(6)])]. given #601 (T,wt=14): 1171 x v (y v (((x ^ z) v y)' v u)) = 1. [para(99(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #602 (A,wt=23): 282 (x v y) ^ (z v (y' v u)) != 0 | (x v y)' = z v (y' v u). [para(101(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #603 (T,wt=14): 1175 x v (y v (((z ^ x) v y)' v u)) = 1. [para(99(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #604 (T,wt=14): 1178 x v ((y v x)' v (z v (u v y))) = 1. [para(99(a,1),86(a,1,1)),rewrite([3(7),3(6),61(8),99(11)])]. given #605 (T,wt=14): 1180 x ^ (y ^ (z ^ ((x ^ z)' ^ u))) = 0. [para(107(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. Low Water (keep): wt=21.000, iters=6803 given #606 (T,wt=14): 1182 x ^ (y ^ (((x v z) ^ y)' ^ u)) = 0. [para(107(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #607 (A,wt=19): 283 (x v y) ^ (x' v z) != 0 | (x v y)' = x' v z. [para(101(a,1),35(a,1)),xx(a)]. given #608 (T,wt=14): 1184 x ^ (y ^ (((z v x) ^ y)' ^ u)) = 0. [para(107(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #609 (T,wt=14): 1224 x v (y v (z v ((x ^ u) v y)')) = 1. [para(110(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #610 (T,wt=14): 1228 x v (y v (z v ((u ^ x) v y)')) = 1. [para(110(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #611 (T,wt=14): 1231 x v (y v ((z v x)' v (u v z))) = 1. [para(110(a,1),86(a,1,1)),rewrite([3(7),3(6),61(8),110(11)])]. given #612 (A,wt=19): 284 (x v y') ^ (z v y) != 0 | (x v y')' = z v y. [para(244(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #613 (T,wt=14): 1233 x ^ (y ^ (z ^ (u ^ (x ^ z)'))) = 0. [para(113(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #614 (T,wt=14): 1235 x ^ (y ^ (z ^ ((x v u) ^ y)')) = 0. [para(113(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #615 (T,wt=14): 1237 x ^ (y ^ (z ^ ((u v x) ^ y)')) = 0. [para(113(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #616 (T,wt=14): 1241 (x v (y ^ z)) ^ (x v (u v y))' = 0. [para(169(a,1),117(a,1,2,1,2))]. given #617 (A,wt=19): 287 x ^ (y v (z v x')) != 0 | y v (z v x') = x'. [para(111(a,1),10(a,1)),flip(c),xx(a)]. given #618 (T,wt=14): 1243 (x v (y ^ z)) ^ (x v (u v z))' = 0. [para(768(a,1),117(a,1,2,1,2))]. given #619 (T,wt=14): 1247 x ^ (y ^ (z ^ ((x ^ z) v u)')) = 0. [para(118(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #620 (T,wt=14): 1260 x v (y v (z v (u v (x' v w)))) = 1. [para(111(a,1),89(a,1,1,2)),rewrite([79(2),3(5),3(4),61(8),286(11)])]. given #621 (T,wt=14): 1261 x v (y v (z v ((x ^ u)' v w))) = 1. [para(149(a,1),89(a,1,1,2)),rewrite([79(2),3(5),61(8),288(11)])]. given #622 (A,wt=19): 289 x ^ (y v (z v x')) != 0 | (y v (z v x'))' = x. [para(111(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #623 (T,wt=10): 18570 x v y != 0 | y v x = 0. [para(85(a,1),289(a,1)),rewrite([199(7),68(5)]),flip(b)]. given #624 (T,wt=10): 18573 x ^ y != 0 | y ^ x = 0. [para(212(a,1),18570(a,1)),rewrite([212(6)])]. given #625 (T,wt=14): 1263 x v (y v ((z ^ (x ^ u))' v w)) = 1. [para(155(a,1),89(a,1,1,2)),rewrite([79(2),61(8),375(11)])]. given #626 (T,wt=14): 1264 x v (y v ((z ^ (u ^ x))' v w)) = 1. [para(158(a,1),89(a,1,1,2)),rewrite([79(2),61(8),397(11)])]. given #627 (A,wt=23): 290 (x v y) ^ (z v (u v y')) != 0 | (x v y)' = z v (u v y'). [para(111(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #628 (T,wt=14): 1265 x v (y v (z v ((u ^ x)' v w))) = 1. [para(160(a,1),89(a,1,1,2)),rewrite([79(2),3(5),61(8),440(11)])]. given #629 (T,wt=14): 1269 (x ^ y)' v (z v (u v (x v w))) = 1. [para(531(a,1),89(a,1,1,2)),rewrite([79(2),3(5),61(8),553(11)])]. given #630 (T,wt=14): 1270 (x ^ y)' v (z v (u v (y v w))) = 1. [para(534(a,1),89(a,1,1,2)),rewrite([79(2),3(5),61(8),618(11)])]. given #631 (T,wt=14): 1277 (x ^ y) v (z v ((y ^ x)' v u)) = 1. [para(992(a,1),89(a,1,1,2)),rewrite([79(2),61(8),1005(11)])]. given #632 (A,wt=19): 291 (x v y) ^ (z v x') != 0 | (x v y)' = z v x'. [para(111(a,1),35(a,1)),xx(a)]. given #633 (T,wt=14): 1282 x v (y v (z v ((y v x)' v u))) = 1. [para(110(a,1),89(a,1,1)),rewrite([3(5),61(8),876(11)])]. given #634 (T,wt=14): 1284 x ^ (y ^ (z ^ (u v (x ^ z))')) = 0. [para(129(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #635 (T,wt=14): 1288 (x v y) ^ (x v (z v (u v y)))' = 0. [para(3(a,1),130(a,1,2,1,2))]. given #636 (T,wt=14): 1292 (x v ((x v y) ^ z)) ^ (x v y)' = 0. [para(23(a,1),130(a,1,2,1))]. given #637 (A,wt=27): 301 x ^ (y v (z v (x ^ ((u ^ w) v (x ^ (y v z)))))) = x ^ (y v (z v (u ^ w))). [para(3(a,1),37(a,1,2)),rewrite([3(11)])]. given #638 (T,wt=14): 1293 (x v (y ^ (z ^ u))) ^ (x v z)' = 0. [para(66(a,1),130(a,1,2,1,2))]. Low Water (keep): wt=20.000, iters=6696 given #639 (T,wt=14): 1294 (x v (y ^ (z ^ u))) ^ (x v u)' = 0. [para(94(a,1),130(a,1,2,1,2))]. given #640 (T,wt=14): 1302 (x v (y ^ z)) ^ (x v (z ^ y))' = 0. [para(212(a,1),130(a,1,2,1,2))]. given #641 (T,wt=14): 1311 ((x ^ (y ^ z)) v u) ^ (y v u)' = 0. [para(17(a,1),150(a,1,1,1))]. given #642 (A,wt=21): 302 x ^ (y v (x ^ ((z ^ u) v (y ^ x)))) = x ^ (y v (z ^ u)). [para(4(a,1),37(a,1,2,2,2,2))]. given #643 (T,wt=14): 1315 ((x ^ y) v (z ^ (x ^ u))) ^ x' = 0. [para(66(a,1),150(a,1,2,1))]. given #644 (T,wt=14): 1316 ((x ^ y) v (z ^ (u ^ x))) ^ x' = 0. [para(94(a,1),150(a,1,2,1))]. given #645 (T,wt=14): 1322 ((x ^ y) v z) ^ (y v (u v z))' = 0. [para(140(a,1),150(a,1,1,1)),rewrite([3(4)])]. given #646 (T,wt=14): 1325 (x v (y v z)) ^ (y v (x v z))' = 0. [para(85(a,1),150(a,1,1,1)),rewrite([3(2),3(4)])]. given #647 (A,wt=25): 303 x ^ ((y v (x ^ ((z ^ u) v (x ^ y)))) ^ w) = x ^ ((y v (z ^ u)) ^ w). [para(37(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)]. given #648 (T,wt=14): 1326 ((x ^ y) v z) ^ (x v (z v u))' = 0. [para(150(a,1),88(a,1,2)),rewrite([4(4),72(4)]),flip(a)]. given #649 (T,wt=14): 1331 x v (y v (z v ((x v z) ^ u)')) = 1. [para(151(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #650 (T,wt=14): 1337 x v (((y v x) ^ z)' v (u v y)) = 1. [para(151(a,1),86(a,1,1)),rewrite([3(7),61(8),151(11)])]. given #651 (T,wt=14): 1339 x v (y v (((y v x) ^ z)' v u)) = 1. [para(151(a,1),89(a,1,1)),rewrite([61(8),1328(11)])]. given #652 (A,wt=29): 304 x ^ (y ^ (z v (x ^ (y ^ ((u ^ w) v (x ^ (y ^ z))))))) = x ^ (y ^ (z v (u ^ w))). [para(37(a,1),5(a,1)),rewrite([5(4),5(8),5(10)]),flip(a)]. given #653 (T,wt=14): 1363 (x ^ y) v (x ^ (z ^ (y ^ u)))' = 1. [para(17(a,1),153(a,1,2,1,2))]. given #654 (T,wt=14): 1367 (x ^ (y v z)) v (x ^ (u ^ y))' = 1. [para(140(a,1),153(a,1,2,1,2))]. given #655 (T,wt=14): 1369 (x ^ (y v z)) v (x ^ (u ^ z))' = 1. [para(721(a,1),153(a,1,2,1,2))]. given #656 (T,wt=14): 1371 (x ^ (y v z)) v (x ^ (z v y))' = 1. [para(85(a,1),153(a,1,2,1,2))]. given #657 (A,wt=17): 305 x ^ (y v (x ^ (z v (x ^ y)))) = x ^ (y v z). [para(6(a,1),37(a,1,2,2,2,1)),rewrite([6(7)])]. given #658 (T,wt=13): 19074 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(66(a,1),305(a,1,2,2,2)),rewrite([2(6),7(6)])]. given #659 (T,wt=13): 19075 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(94(a,1),305(a,1,2,2,2)),rewrite([2(6),24(6)])]. given #660 (T,wt=13): 19085 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(205(a,1),305(a,1,2,2,2)),rewrite([52(3),19074(4)]),flip(a)]. given #661 (T,wt=13): 19101 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(2(a,1),19074(a,1,2))]. given #662 (A,wt=25): 306 x ^ (y ^ (z v (x ^ ((u ^ w) v (x ^ z))))) = y ^ (x ^ (z v (u ^ w))). [para(37(a,1),17(a,1,2)),flip(a)]. given #663 (T,wt=13): 19129 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(2(a,1),19075(a,1,2))]. given #664 (T,wt=13): 19130 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(4(a,1),19075(a,1,2,2))]. given #665 (T,wt=13): 19163 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(2(a,1),19085(a,1,2))]. given #666 (T,wt=13): 19235 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(4(a,1),19129(a,1,2,1))]. given #667 (A,wt=27): 307 x ^ ((y ^ z) v (x ^ ((u ^ w) v (y ^ (x ^ z))))) = x ^ ((y ^ z) v (u ^ w)). [para(17(a,1),37(a,1,2,2,2,2))]. given #668 (T,wt=14): 1380 x v ((y ^ (z v x))' v (u v z)) = 1. [para(157(a,1),86(a,1,1)),rewrite([3(7),61(8),157(11)])]. given #669 (T,wt=14): 1382 x v (y v ((z ^ (y v x))' v u)) = 1. [para(157(a,1),89(a,1,1)),rewrite([61(8),875(11)])]. given #670 (T,wt=14): 1384 (x ^ y) v (x ^ (z ^ (u ^ y)))' = 1. [para(5(a,1),161(a,1,2,1,2))]. given #671 (T,wt=14): 1390 (x ^ ((x ^ y) v z)) v (x ^ y)' = 1. [para(21(a,1),161(a,1,2,1))]. given #672 (A,wt=21): 308 x ^ (y v (x ^ (z v (u v (x ^ y))))) = x ^ (y v (z v u)). [para(19(a,1),37(a,1,2,2,2,1)),rewrite([3(3),19(10)])]. given #673 (T,wt=14): 1391 (x ^ (y v (z v u))) v (x ^ z)' = 1. [para(48(a,1),161(a,1,2,1,2))]. given #674 (T,wt=14): 1392 (x ^ (y v (z v u))) v (x ^ u)' = 1. [para(74(a,1),161(a,1,2,1,2))]. given #675 (T,wt=14): 1402 (x ^ (y v (x ^ z))) v (x ^ z)' = 1. [para(76(a,1),161(a,1,2,1))]. given #676 (T,wt=14): 1416 ((x v (y v z)) ^ u) v (y ^ u)' = 1. [para(15(a,1),162(a,1,1,1))]. given #677 (A,wt=31): 309 x v ((y ^ (x v (z ^ u))) v (y ^ ((z ^ u) v (y ^ x)))) = x v (y ^ ((z ^ u) v (y ^ x))). [para(37(a,1),24(a,1,2)),rewrite([2(9),15(9)])]. given #678 (T,wt=14): 1423 ((x v y) ^ (z v (x v u))) v x' = 1. [para(48(a,1),162(a,1,2,1))]. given #679 (T,wt=14): 1424 ((x v y) ^ (z v (u v x))) v x' = 1. [para(74(a,1),162(a,1,2,1))]. given #680 (T,wt=14): 1433 ((x v y) ^ z) v (y ^ (u ^ z))' = 1. [para(169(a,1),162(a,1,1,1)),rewrite([5(4)])]. given #681 (T,wt=14): 1437 (x ^ y)' v (((x v z) ^ y) v u) = 1. [para(162(a,1),85(a,1,1)),rewrite([61(8),1411(11)])]. given #682 (A,wt=25): 310 x ^ (y v ((x v z) ^ ((u ^ w) v ((x v z) ^ y)))) = x ^ (y v (u ^ w)). [para(37(a,1),20(a,1,2)),rewrite([20(5)]),flip(a)]. given #683 (T,wt=14): 1475 x v (y v (z v (u v (x v u)'))) = 1. [para(3(a,1),202(a,1,2))]. given #684 (T,wt=14): 1477 x v (y v (z v ((x ^ u) v z)')) = 1. [para(202(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #685 (T,wt=14): 1482 x v (y v (z v ((u ^ x) v z)')) = 1. [para(202(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #686 (T,wt=14): 1492 x v (y v ((z ^ (x ^ u)) v y)') = 1. [para(17(a,1),204(a,1,2,2,1,1))]. given #687 (A,wt=29): 311 x ^ (((x v y) ^ z) v (x ^ ((u ^ w) v (x ^ z)))) = x ^ (((x v y) ^ z) v (u ^ w)). [para(20(a,1),37(a,1,2,2,2,2))]. given #688 (T,wt=14): 1501 x v (((y ^ z) v x)' v (u v y)) = 1. [para(204(a,1),86(a,1,1)),rewrite([3(7),61(8),204(11)])]. given #689 (T,wt=14): 1504 x v (y v (((y ^ z) v x)' v u)) = 1. [para(204(a,1),89(a,1,1)),rewrite([61(8),1490(11)])]. given #690 (T,wt=14): 1508 x ^ (y ^ (z ^ (u ^ (x ^ u)'))) = 0. [para(5(a,1),216(a,1,2))]. given #691 (T,wt=14): 1510 x ^ (y ^ (z ^ ((x v u) ^ z)')) = 0. [para(216(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #692 (A,wt=33): 315 x ^ ((y ^ ((x ^ y) v z)) v (x ^ ((u ^ w) v (x ^ y)))) = x ^ ((y ^ ((x ^ y) v z)) v (u ^ w)). [para(21(a,1),37(a,1,2,2,2,2))]. given #693 (T,wt=14): 1514 x ^ (y ^ (z ^ ((u v x) ^ z)')) = 0. [para(216(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #694 (T,wt=14): 1522 x ^ (y ^ ((z v (x v u)) ^ y)') = 0. [para(15(a,1),218(a,1,2,2,1,1))]. given #695 (T,wt=14): 1534 (x v (y ^ (z v x))) ^ (z v x)' = 0. [para(93(a,1),116(a,1,2,1))]. given #696 (T,wt=14): 1537 x v (y v (y v (z ^ (x v y)))') = 1. [para(93(a,1),244(a,1,2)),rewrite([2(6),3(6)])]. given #697 (A,wt=19): 320 x ^ ((y ^ (z ^ u)) v (x ^ (y ^ z))) = x ^ (y ^ z). [para(66(a,1),37(a,1,2,2,2)),rewrite([5(2),5(8),2(10),25(10)])]. given #698 (T,wt=14): 1558 (x v (y ^ (x v z))) ^ (x v z)' = 0. [para(93(a,1),130(a,1,2,1))]. given #699 (T,wt=14): 1572 x ^ (y ^ (z ^ (u ^ (x' ^ w)))) = 0. [para(5(a,1),224(a,1,2,2))]. given #700 (T,wt=14): 1573 x ^ (y ^ (z ^ ((x v u)' ^ w))) = 0. [para(224(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #701 (T,wt=14): 1575 x ^ (y ^ (z ^ ((u v x)' ^ w))) = 0. [para(224(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #702 (A,wt=33): 321 x v ((y ^ ((z ^ u) v (y ^ x))) v (w ^ (y ^ (x v (z ^ u))))) = x v (y ^ ((z ^ u) v (y ^ x))). [para(37(a,1),94(a,1,2,2)),rewrite([3(10)])]. given #703 (T,wt=14): 1578 x ^ (y ^ ((z v (x v u))' ^ w)) = 0. [para(15(a,1),225(a,1,2,2,1,1))]. given #704 (T,wt=14): 1580 1 != x | x ^ y != 0 | x' = y ^ x. [para(4(a,1),95(b,1))]. given #705 (T,wt=14): 1604 x v ((x v y)' v (z v (y v u))) = 1. [para(250(a,1),3(a,1,1)),rewrite([69(2),3(6),3(5)]),flip(a)]. given #706 (T,wt=14): 1606 x v ((x v y)' v (z v (u v y))) = 1. [para(3(a,1),250(a,1,2,2))]. given #707 (A,wt=45): 331 x ^ (y v ((x ^ ((z ^ u) v (x ^ y))) v (x ^ ((w ^ v5) v (x ^ (y v (z ^ u))))))) = x ^ (y v ((x ^ ((z ^ u) v (x ^ y))) v (w ^ v5))). [para(37(a,1),37(a,1,2,2,2,2)),rewrite([3(12),3(20)])]. given #708 (T,wt=14): 1608 x v (y v ((x v z)' v (u v z))) = 1. [para(250(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #709 (T,wt=14): 1610 x v (((x ^ y) v z)' v (u v z)) = 1. [para(250(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #710 (T,wt=14): 1613 x v (y v (x v (z ^ (y ^ u)))') = 1. [para(66(a,1),250(a,1,2,2)),rewrite([2(5)])]. given #711 (T,wt=14): 1614 x v (y v (x v (z ^ (u ^ y)))') = 1. [para(94(a,1),250(a,1,2,2)),rewrite([2(5)])]. given #712 (A,wt=16): 339 (x v ((y v x) ^ z)) ^ (u v (y v x))' = 0. [para(23(a,1),127(a,1,2,1,2))]. given #713 (T,wt=14): 1622 x v (((y ^ x) v z)' v (u v z)) = 1. [para(250(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #714 (T,wt=14): 1630 x v ((y ^ z) v (x v (z ^ y))') = 1. [para(212(a,1),250(a,1,2,2)),rewrite([2(5)])]. given #715 (T,wt=14): 1634 x ^ ((x ^ y)' ^ (z ^ (y ^ u))) = 0. [para(254(a,1),5(a,1,1)),rewrite([72(2),5(6),5(5)]),flip(a)]. given #716 (T,wt=14): 1636 x ^ ((x ^ y)' ^ (z ^ (u ^ y))) = 0. [para(5(a,1),254(a,1,2,2))]. given #717 (A,wt=16): 345 (x v ((y v x) ^ z)) ^ ((y v x)' ^ u) = 0. [para(23(a,1),128(a,1,2,1,1))]. given #718 (T,wt=14): 1637 x ^ (y ^ ((x ^ z)' ^ (u ^ z))) = 0. [para(254(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #719 (T,wt=14): 1639 x ^ (((x v y) ^ z)' ^ (u ^ z)) = 0. [para(254(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #720 (T,wt=14): 1642 x ^ (y ^ (x ^ (z v (y v u)))') = 0. [para(48(a,1),254(a,1,2,2)),rewrite([4(5)])]. given #721 (T,wt=14): 1643 x ^ (y ^ (x ^ (z v (u v y)))') = 0. [para(74(a,1),254(a,1,2,2)),rewrite([4(5)])]. given #722 (A,wt=16): 349 (x v ((y v x) ^ z)) ^ (u ^ (y v x)') = 0. [para(23(a,1),131(a,1,2,2,1))]. given #723 (T,wt=14): 1649 x ^ (((y v x) ^ z)' ^ (u ^ z)) = 0. [para(254(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #724 (T,wt=14): 1654 x ^ ((y v z) ^ (x ^ (z v y))') = 0. [para(168(a,1),254(a,1,2,2)),rewrite([4(5)])]. given #725 (T,wt=14): 1666 x ^ ((y v (z v (x v u)))' ^ w) = 0. [para(3(a,1),258(a,1,2,1,1))]. given #726 (T,wt=14): 1669 x ^ (y ^ ((z v (u v x))' ^ w)) = 0. [para(169(a,1),258(a,1,2,1,1,2)),rewrite([5(6)])]. given #727 (A,wt=19): 352 x ^ ((x ^ y)' v z) != 0 | (x ^ y)' v z = x'. [para(148(a,1),10(a,1)),flip(c),xx(a)]. given #728 (T,wt=14): 1673 x v (y v (z v (u v (w v x')))) = 1. [para(3(a,1),286(a,1,2,2,2))]. given #729 (T,wt=14): 1674 x v (y v (z v (u v (x ^ w)'))) = 1. [para(286(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #730 (T,wt=14): 1679 x v (y v (z v (u v (w ^ x)'))) = 1. [para(286(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #731 (T,wt=14): 1718 x v (y v (z v (u ^ (x ^ w))')) = 1. [para(17(a,1),288(a,1,2,2,2,1))]. given #732 (A,wt=19): 354 x ^ ((x ^ y)' v z) != 0 | ((x ^ y)' v z)' = x. [para(148(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #733 (T,wt=14): 1723 x v (y v (z v (u v (y v x)'))) = 1. [para(85(a,1),288(a,1,2,2,2,1)),rewrite([3(6)])]. given #734 (T,wt=14): 1727 x ^ (y ^ (z ^ (u ^ (w ^ x')))) = 0. [para(5(a,1),293(a,1,2,2,2))]. given #735 (T,wt=14): 1728 x ^ (y ^ (z ^ (u ^ (x v w)'))) = 0. [para(293(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #736 (T,wt=14): 1730 x ^ (y ^ (z ^ (u ^ (w v x)'))) = 0. [para(293(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #737 (A,wt=23): 355 (x v y) ^ ((y ^ z)' v u) != 0 | (x v y)' = (y ^ z)' v u. [para(148(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #738 (T,wt=14): 1733 x ^ (y ^ (z ^ (u v (x v w))')) = 0. [para(15(a,1),294(a,1,2,2,2,1))]. given #739 (T,wt=14): 1735 x ^ (y ^ (z v (u v (x v w)))') = 0. [para(3(a,1),297(a,1,2,2,1))]. given #740 (T,wt=14): 1738 x ^ (y ^ (z ^ (u v (w v x))')) = 0. [para(169(a,1),297(a,1,2,2,1,2)),rewrite([5(6)])]. given #741 (T,wt=14): 1745 x ^ (y ^ (z v (u v (w v x)))') = 0. [para(169(a,1),299(a,1,2,1,2,2)),rewrite([5(6)])]. given #742 (A,wt=27): 356 x ^ (y v (z v (x ^ ((x ^ (z v y)) v (u ^ w))))) = x ^ (y v (z v (u ^ w))). [para(2(a,1),38(a,1,2,2,2,2,1,2))]. given #743 (T,wt=14): 1746 x ^ ((y v (z v (u v x)))' ^ w) = 0. [para(333(a,1),5(a,1,1)),rewrite([72(2)]),flip(a)]. given #744 (T,wt=14): 1756 x ^ (y ^ (z v (u v (y ^ x)))') = 0. [para(212(a,1),333(a,1,2,1,2,2)),rewrite([5(6)])]. given #745 (T,wt=14): 1769 x ^ (y ^ ((z v (y ^ x))' ^ u)) = 0. [para(212(a,1),334(a,1,2,1,1,2)),rewrite([5(6)])]. given #746 (T,wt=14): 1781 x ^ (y ^ (z ^ (u v (y ^ x))')) = 0. [para(212(a,1),337(a,1,2,2,1,2)),rewrite([5(6)])]. given #747 (A,wt=33): 357 x ^ (y v (z v (u v (x ^ ((x ^ (y v (z v u))) v (w ^ v5)))))) = x ^ (y v (z v (u v (w ^ v5)))). [para(3(a,1),38(a,1,2,2,2,2,1,2)),rewrite([3(9),3(14)])]. given #748 (T,wt=14): 1835 x ^ (y ^ (x ^ ((x ^ y) v z))') = 0. [para(102(a,1),216(a,1))]. given #749 (T,wt=14): 1858 x ^ (y ^ (z ^ ((y ^ x)' ^ u))) = 0. [para(212(a,1),343(a,1,2,2,1,1)),rewrite([5(6)])]. given #750 (T,wt=14): 1870 x ^ (y ^ (z ^ (u ^ (y ^ x)'))) = 0. [para(212(a,1),346(a,1,2,2,2,1)),rewrite([5(6)])]. given #751 (T,wt=14): 1878 x v ((y ^ (z ^ (x ^ u)))' v w) = 1. [para(5(a,1),353(a,1,2,1,1))]. given #752 (A,wt=27): 358 x ^ (y v (z v (x ^ (((y v z) ^ x) v (u ^ w))))) = x ^ (y v (z v (u ^ w))). [para(4(a,1),38(a,1,2,2,2,2,1))]. given #753 (T,wt=14): 1884 (x ^ (y ^ z))' v (u v (w v y)) = 1. [para(353(a,1),86(a,1,1)),rewrite([3(7),61(8),353(11)])]. given #754 (T,wt=14): 1889 x v (y v (z ^ (u ^ (x ^ w)))') = 1. [para(5(a,1),375(a,1,2,2,1))]. given #755 (T,wt=14): 1894 x v (y v (z v (u ^ (w ^ x))')) = 1. [para(140(a,1),375(a,1,2,2,1,2)),rewrite([3(6)])]. given #756 (T,wt=14): 1895 x v (y v (z v (u ^ (y v x))')) = 1. [para(85(a,1),375(a,1,2,2,1,2)),rewrite([3(6)])]. given #757 (A,wt=31): 359 x ^ ((y v (z v (x ^ ((x ^ (y v z)) v (u ^ w))))) ^ v5) = x ^ ((y v (z v (u ^ w))) ^ v5). [para(38(a,1),5(a,1,1)),rewrite([5(5)]),flip(a)]. given #758 (T,wt=14): 1905 x ^ (y ^ (y ^ (z v (x v u)))') = 0. [para(214(a,1),104(a,1,2)),rewrite([81(2)]),flip(a)]. given #759 (T,wt=14): 1928 x ^ ((x v y) ^ (z v (x v u)))' = 0. [para(104(a,1),218(a,1))]. given #760 (T,wt=14): 1948 x v (y v (z ^ (u ^ (w ^ x)))') = 1. [para(140(a,1),381(a,1,2,1,2,2)),rewrite([3(6)])]. given #761 (T,wt=14): 1949 x v (y v (z ^ (u ^ (y v x)))') = 1. [para(85(a,1),381(a,1,2,1,2,2)),rewrite([3(6)])]. given #762 (A,wt=35): 360 x ^ (y ^ (z v (u v (x ^ (y ^ ((x ^ (y ^ (z v u))) v (w ^ v5))))))) = x ^ (y ^ (z v (u v (w ^ v5)))). [para(38(a,1),5(a,1)),rewrite([5(5),5(9),5(12)]),flip(a)]. given #763 (T,wt=14): 1953 x v ((y ^ (z ^ (u ^ x)))' v w) = 1. [para(5(a,1),386(a,1,2,1,1,2))]. given #764 (T,wt=14): 1968 (x ^ (y ^ z))' v (u v (w v z)) = 1. [para(386(a,1),86(a,1,1)),rewrite([3(7),61(8),386(11)])]. given #765 (T,wt=14): 2036 x ^ (y ^ ((x ^ (y v z))' ^ u)) = 0. [para(107(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #766 (T,wt=14): 2037 x ^ (y ^ (z ^ (x ^ (y v u))')) = 0. [para(113(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #767 (A,wt=23): 361 x ^ (y v (z v (x ^ ((x ^ (y v z)) v u)))) = x ^ (y v (z v u)). [para(6(a,1),38(a,1,2,2,2,2,2)),rewrite([6(9)])]. given #768 (T,wt=14): 2041 x ^ (y ^ ((x v z) ^ (y v u))') = 0. [para(218(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #769 (T,wt=14): 2100 x v (y v ((y v (x ^ z))' v u)) = 1. [para(448(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #770 (T,wt=14): 2105 x v (y v ((y v (z ^ x))' v u)) = 1. [para(448(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #771 (T,wt=14): 2112 x v (y v (z v (u v (u v x)'))) = 1. [para(3(a,1),452(a,1,2))]. given #772 (A,wt=33): 362 x ^ (y v (z v (u v (x ^ ((x ^ (z v (y v u))) v (w ^ v5)))))) = x ^ (y v (z v (u v (w ^ v5)))). [para(15(a,1),38(a,1,2,2,2,2,1,2)),rewrite([3(8),3(13)])]. given #773 (T,wt=14): 2114 x v (y v (z v (z v (x ^ u))')) = 1. [para(452(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #774 (T,wt=14): 2119 x v (y v (z v (z v (u ^ x))')) = 1. [para(452(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #775 (T,wt=14): 2177 x v (y v (y v (z ^ (x ^ u)))') = 1. [para(17(a,1),454(a,1,2,2,1,2))]. given #776 (T,wt=14): 2184 x v (y v (z v (z v (y v x))')) = 1. [para(85(a,1),454(a,1,2,2,1,2)),rewrite([3(6)])]. given #777 (A,wt=31): 363 x ^ (y ^ (z v (u v (x ^ ((x ^ (z v u)) v (w ^ v5)))))) = y ^ (x ^ (z v (u v (w ^ v5)))). [para(38(a,1),17(a,1,2)),flip(a)]. given #778 (T,wt=14): 2185 x v ((x v (y ^ z))' v (u v y)) = 1. [para(454(a,1),86(a,1,1)),rewrite([3(7),61(8),454(11)])]. given #779 (T,wt=14): 2187 x v (y v ((x v (y ^ z))' v u)) = 1. [para(454(a,1),89(a,1,1)),rewrite([61(8),647(11)])]. given #780 (T,wt=14): 2191 x ^ (y ^ (z ^ ((z ^ x)' ^ u))) = 0. [para(457(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #781 (T,wt=14): 2193 x ^ (y ^ ((y ^ (x v z))' ^ u)) = 0. [para(457(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #782 (A,wt=41): 364 x v (y v ((z ^ (x v (y v (u ^ w)))) v (z ^ ((z ^ (x v y)) v (u ^ w))))) = x v (y v (z ^ ((z ^ (x v y)) v (u ^ w)))). [para(38(a,1),24(a,1,2)),rewrite([2(12),15(12),15(11)])]. given #783 (T,wt=14): 2195 x ^ (y ^ ((y ^ (z v x))' ^ u)) = 0. [para(457(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #784 (T,wt=14): 2199 (x v y)' ^ (((x ^ z) v y) ^ u) = 0. [para(150(a,1),457(a,1,2,2,1,1)),rewrite([71(6),61(6)])]. given #785 (T,wt=14): 2202 x ^ (y ^ (((y v z) ^ x)' ^ u)) = 0. [para(457(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #786 (T,wt=14): 2205 x ^ (y ^ (z ^ (u ^ (u ^ x)'))) = 0. [para(5(a,1),460(a,1,2))]. given #787 (A,wt=31): 365 x ^ (y v (z v ((x v u) ^ (((x v u) ^ (y v z)) v (w ^ v5))))) = x ^ (y v (z v (w ^ v5))). [para(38(a,1),20(a,1,2)),rewrite([20(6)]),flip(a)]. given #788 (T,wt=14): 2207 x ^ (y ^ (z ^ (z ^ (x v u))')) = 0. [para(460(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #789 (T,wt=14): 2210 x ^ (y ^ (z ^ (z ^ (u v x))')) = 0. [para(460(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #790 (T,wt=14): 2211 x ^ ((y ^ x)' ^ (z ^ (u ^ y))) = 0. [para(107(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6),5(5)])]. given #791 (T,wt=14): 2214 x ^ (y ^ ((z ^ x)' ^ (u ^ z))) = 0. [para(113(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6),5(5)])]. given #792 (A,wt=28): 366 x v (y v ((z ^ ((z ^ (x v y)) v (u ^ w))) v (z ^ (x v (y v (u ^ w))))')) = 1. [para(38(a,1),152(a,1,2,1)),rewrite([3(13),3(12)])]. given #793 (T,wt=14): 2215 x ^ (((y ^ x) v z)' ^ (u ^ y)) = 0. [para(118(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #794 (T,wt=14): 2216 x ^ ((y v (z ^ x))' ^ (u ^ z)) = 0. [para(129(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #795 (T,wt=14): 2217 x ^ (((y v z) ^ x)' ^ (u ^ y)) = 0. [para(218(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #796 (T,wt=14): 2218 (x ^ y)' ^ (z ^ (y ^ (u ^ x))) = 0. [para(254(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6),5(5)])]. given #797 (A,wt=43): 368 x v (y v ((z ^ ((z ^ (x v y)) v (u ^ w))) v (v5 ^ (z ^ (x v (y v (u ^ w))))))) = x v (y v (z ^ ((z ^ (x v y)) v (u ^ w)))). [para(38(a,1),94(a,1,2,2)),rewrite([3(13),3(12)])]. given #798 (T,wt=14): 2219 (x v (y v z))' ^ (u ^ (w ^ y)) = 0. [para(258(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #799 (T,wt=14): 2220 (x v (y v z))' ^ (u ^ (w ^ z)) = 0. [para(334(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #800 (T,wt=14): 2224 x ^ (y ^ ((z v (y v u)) ^ x)') = 0. [para(104(a,1),460(a,1,2))]. given #801 (T,wt=14): 2230 x ^ ((y v (x v z)) ^ (x v u))' = 0. [para(462(a,1),104(a,1)),flip(a)]. given #802 (A,wt=28): 370 x ^ ((y v (z v (u ^ w))) ^ (y v (z v (x ^ ((x ^ (y v z)) v (u ^ w)))))') = 0. [para(38(a,1),245(a,1,2)),rewrite([4(13),5(13)])]. given #803 (T,wt=14): 2231 x ^ (y ^ ((y v z) ^ (x v u))') = 0. [para(462(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #804 (T,wt=14): 2233 x ^ ((x ^ (y v z))' ^ (u ^ y)) = 0. [para(462(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #805 (T,wt=14): 2241 (x ^ y)' v (z v (u v (w v x))) = 1. [para(169(a,1),464(a,1,2,2,2))]. given #806 (T,wt=14): 2242 (x ^ y)' v (z v (u v (w v y))) = 1. [para(768(a,1),464(a,1,2,2,2))]. given #807 (A,wt=55): 371 x ^ (y v (z v ((x ^ ((x ^ (y v z)) v (u ^ w))) v (x ^ ((x ^ (y v (z v (u ^ w)))) v (v5 ^ v6)))))) = x ^ (y v (z v ((x ^ ((x ^ (y v z)) v (u ^ w))) v (v5 ^ v6)))). [para(38(a,1),38(a,1,2,2,2,2,1)),rewrite([3(14),3(24)])]. given #808 (T,wt=14): 2246 (x v y)' ^ (z ^ (u ^ (w ^ x))) = 0. [para(140(a,1),529(a,1,2,2,2))]. given #809 (T,wt=14): 2247 (x v y)' ^ (z ^ (u ^ (w ^ y))) = 0. [para(721(a,1),529(a,1,2,2,2))]. given #810 (T,wt=14): 2248 (x v y)' ^ (z ^ (u ^ (y v x))) = 0. [para(85(a,1),529(a,1,2,2,2))]. given #811 (T,wt=14): 2251 (x v (y v z))' ^ (u ^ (y ^ w)) = 0. [para(104(a,1),529(a,1,2,2))]. given #812 (A,wt=19): 374 x ^ (y v (x ^ z)') != 0 | y v (x ^ z)' = x'. [para(149(a,1),10(a,1)),flip(c),xx(a)]. given #813 (T,wt=14): 2265 (x ^ y)' v (z v (u v (y ^ x))) = 1. [para(212(a,1),530(a,1,2,2,2))]. given #814 (T,wt=14): 2270 (x ^ (y ^ z))' v (u v (y v w)) = 1. [para(537(a,1),3(a,1,1)),rewrite([69(2),3(6)]),flip(a)]. given #815 (T,wt=14): 2281 (x ^ (y ^ z))' v (u v (z v w)) = 1. [para(140(a,1),537(a,1,1,1,2))]. given #816 (T,wt=14): 2283 (x ^ y) v (z ^ (y ^ (x ^ u)))' = 1. [para(212(a,1),537(a,1,2)),rewrite([5(2),2(6)])]. given #817 (A,wt=19): 376 x ^ (y v (x ^ z)') != 0 | (y v (x ^ z)')' = x. [para(149(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #818 (T,wt=14): 2284 (x ^ (y v z))' v (u v (z v y)) = 1. [para(85(a,1),537(a,1,1,1,2))]. given #819 (T,wt=14): 2297 (x ^ ((x ^ y) v z)) v (y ^ x)' = 1. [para(120(a,1),152(a,1,2,1))]. given #820 (T,wt=14): 2299 x ^ (y ^ (y ^ ((y ^ x) v z))') = 0. [para(120(a,1),245(a,1,2)),rewrite([4(6),5(6)])]. given #821 (T,wt=14): 2318 (x ^ ((y ^ x) v z)) v (x ^ y)' = 1. [para(120(a,1),161(a,1,2,1))]. given #822 (A,wt=23): 377 (x v y) ^ (z v (y ^ u)') != 0 | (x v y)' = z v (y ^ u)'. [para(149(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #823 (T,wt=14): 2329 (x ^ y) v (z v (u ^ (y ^ x))') = 1. [para(120(a,1),395(a,1,2,1,2)),rewrite([3(6)])]. given #824 (T,wt=14): 2332 (x ^ y) v (z v (u v (y ^ x)')) = 1. [para(120(a,1),397(a,1,2,2,1)),rewrite([3(6)])]. given #825 (T,wt=14): 2356 (x ^ y) v (z ^ (u ^ (y ^ x)))' = 1. [para(212(a,1),538(a,1,2)),rewrite([2(6)])]. given #826 (T,wt=14): 2370 (x ^ y)' v (z v ((y ^ x) v u)) = 1. [para(120(a,1),538(a,1,1,1))]. given #827 (A,wt=19): 378 (x v y) ^ (x ^ z)' != 0 | (x v y)' = (x ^ z)'. [para(149(a,1),35(a,1)),xx(a)]. given #828 (T,wt=14): 2394 ((x ^ y) v z)' ^ (u ^ (y ^ x)) = 0. [para(120(a,1),543(a,1,2,2))]. given #829 (T,wt=14): 2404 (x v y) ^ (z v (y v (x v u)))' = 0. [para(168(a,1),550(a,1,2)),rewrite([3(2),4(6)])]. given #830 (T,wt=14): 2405 (x v (y v z))' ^ (u ^ (z ^ w)) = 0. [para(169(a,1),550(a,1,1,1,2))]. given #831 (T,wt=14): 2420 (x v y)' ^ (z ^ (u ^ (y ^ w))) = 0. [para(66(a,1),551(a,1,1,1,2))]. given #832 (A,wt=19): 382 x ^ (y ^ (x ^ z))' != 0 | (y ^ (x ^ z))' = x'. [para(155(a,1),10(a,1)),flip(c),xx(a)]. given #833 (T,wt=14): 2430 (x v y) ^ (z v (u v (y v x)))' = 0. [para(168(a,1),551(a,1,2)),rewrite([4(6)])]. given #834 (T,wt=14): 2435 (x v (y ^ z))' ^ (u ^ (z ^ y)) = 0. [para(212(a,1),551(a,1,1,1,2))]. given #835 (T,wt=14): 2510 (x v y)' v (z v (y v (x v u))) = 1. [para(85(a,1),552(a,1,1,1)),rewrite([3(4)])]. given #836 (T,wt=14): 2524 (x ^ (y ^ z))' v (u v (y ^ x)) = 1. [para(212(a,1),553(a,1,2,2)),rewrite([5(2)])]. given #837 (A,wt=17): 383 x ^ (y ^ (x ^ z))' != 0 | y ^ (x ^ z) = x. [para(155(a,1),34(a,1)),rewrite([4(7),228(13)]),xx(a)]. given #838 (T,wt=14): 2525 (x v y)' v (z v (u v (y v x))) = 1. [para(85(a,1),553(a,1,1,1))]. given #839 (T,wt=14): 2568 (x ^ (y ^ z))' v (u v (z ^ y)) = 1. [para(212(a,1),618(a,1,2,2))]. given #840 (T,wt=14): 2627 (x v y)' ^ (z ^ (u ^ (x ^ w))) = 0. [para(5(a,1),627(a,1,2))]. given #841 (T,wt=14): 2629 (x v (y v z))' ^ (u ^ (y v x)) = 0. [para(85(a,1),627(a,1,2,2)),rewrite([3(2)])]. given #842 (A,wt=23): 384 (x v y) ^ (z ^ (y ^ u))' != 0 | (x v y)' = (z ^ (y ^ u))'. [para(155(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #843 (T,wt=14): 2660 (x ^ y)' ^ (z ^ (y ^ (x ^ u))) = 0. [para(212(a,1),632(a,1,1,1)),rewrite([5(4)])]. given #844 (T,wt=14): 2661 (x v (y v z))' ^ (u ^ (z v y)) = 0. [para(85(a,1),632(a,1,2,2))]. given #845 (T,wt=14): 2679 (x ^ y)' ^ (z ^ (u ^ (y ^ x))) = 0. [para(212(a,1),633(a,1,1,1))]. given #846 (T,wt=14): 2690 x ^ (y ^ (z v ((y ^ x) v u))') = 0. [para(120(a,1),633(a,1,2)),rewrite([4(6),5(6)])]. given #847 (A,wt=19): 387 x ^ ((y ^ x)' v z) != 0 | (y ^ x)' v z = x'. [para(156(a,1),10(a,1)),flip(c),xx(a)]. given #848 (T,wt=14): 2713 (x v y) ^ (z ^ ((y v x)' ^ u)) = 0. [para(874(a,1),123(a,1,2,2,2,1)),rewrite([62(5),874(10),81(8)])]. given #849 (T,wt=14): 2777 (x v (y ^ z)) ^ (x v (z v u))' = 0. [para(140(a,1),644(a,1,1,2))]. given #850 (T,wt=14): 2783 (x v y)' ^ ((x v (y ^ z)) ^ u) = 0. [para(644(a,1),457(a,1,2,2,1,1)),rewrite([71(6),61(6)])]. given #851 (T,wt=14): 2787 x v (y v (z v (x v (z ^ u))')) = 1. [para(647(a,1),15(a,1,2)),rewrite([79(2)]),flip(a)]. given #852 (A,wt=16): 391 (x ^ ((y ^ x) v z)) v ((y ^ x)' v u) = 1. [para(21(a,1),156(a,1,2,1,1))]. given #853 (T,wt=14): 2788 x v (y v ((x ^ z) v (y ^ u))') = 1. [para(647(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #854 (T,wt=14): 2793 x v (y v ((z ^ x) v (y ^ u))') = 1. [para(647(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #855 (T,wt=14): 2795 x v (y v (z v (x v (u ^ y))')) = 1. [para(140(a,1),647(a,1,2,2,1,2)),rewrite([3(5)])]. given #856 (T,wt=14): 2796 x v (y v (z v (x v (u ^ z))')) = 1. [para(721(a,1),647(a,1,2,2,1,2)),rewrite([3(5)])]. given #857 (A,wt=19): 392 x ^ ((y ^ x)' v z) != 0 | ((y ^ x)' v z)' = x. [para(156(a,1),34(a,1)),rewrite([4(7)]),xx(a)]. given #858 (T,wt=14): 2797 x v ((y v (x ^ z))' v (u v y)) = 1. [para(647(a,1),86(a,1,1)),rewrite([3(7),61(8),647(11)])]. given #859 (T,wt=14): 2815 (x ^ (y v z)) v (x ^ (z ^ u))' = 1. [para(169(a,1),704(a,1,1,2))]. given #860 (T,wt=14): 2818 (x ^ y)' v ((x ^ (y v z)) v u) = 1. [para(704(a,1),85(a,1,1)),rewrite([61(8),2802(11)])]. given #861 (T,wt=14): 2829 x ^ (y ^ (z ^ (x ^ (z v u))')) = 0. [para(706(a,1),17(a,1,2)),rewrite([81(2)]),flip(a)]. given #862 (A,wt=23): 393 (x v y) ^ ((z ^ y)' v u) != 0 | (x v y)' = (z ^ y)' v u. [para(156(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #863 (T,wt=14): 2831 x ^ (y ^ ((z v x) ^ (y v u))') = 0. [para(706(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #864 (T,wt=14): 2832 x ^ (y ^ (z ^ (x ^ (u v y))')) = 0. [para(169(a,1),706(a,1,2,2,1,2)),rewrite([5(5)])]. given #865 (T,wt=14): 2833 x ^ (y ^ (z ^ (x ^ (u v z))')) = 0. [para(768(a,1),706(a,1,2,2,1,2)),rewrite([5(5)])]. given #866 (T,wt=14): 2837 x ^ ((y ^ (x v z))' ^ (u ^ y)) = 0. [para(706(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #867 (A,wt=19): 396 x ^ (y ^ (z ^ x))' != 0 | (y ^ (z ^ x))' = x'. [para(158(a,1),10(a,1)),flip(c),xx(a)]. given #868 (T,wt=14): 2880 x ^ (y ^ (((y ^ x) v z)' ^ u)) = 0. [para(118(a,1),124(a,1,2,2,2,1)),rewrite([62(5),1245(11)])]. given #869 (T,wt=14): 2930 ((x v (y v z)) ^ u) v (z ^ u)' = 1. [para(3(a,1),723(a,1,1,1))]. given #870 (T,wt=14): 2942 ((x v y) ^ (z v (y v u))) v y' = 1. [para(48(a,1),723(a,1,2,1))]. given #871 (T,wt=14): 2945 ((x v y) ^ (z v (u v y))) v y' = 1. [para(74(a,1),723(a,1,2,1))]. given #872 (A,wt=16): 401 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x))' = 1. [para(21(a,1),158(a,1,2,1,2))]. given #873 (T,wt=14): 2959 (x ^ (y ^ z)) v (y ^ (x ^ z))' = 1. [para(212(a,1),723(a,1,1,1)),rewrite([5(2),5(4)])]. given #874 (T,wt=14): 2961 (x ^ y)' v (((z v x) ^ y) v u) = 1. [para(723(a,1),85(a,1,1)),rewrite([61(8),2929(11)])]. given #875 (T,wt=14): 2978 x ^ (y ^ ((z v (u v x)) ^ y)') = 0. [para(3(a,1),727(a,1,2,2,1,1))]. given #876 (T,wt=14): 2997 x ^ ((y v x) ^ (z v (x v u)))' = 0. [para(727(a,1),104(a,1)),flip(a)]. given #877 (A,wt=17): 402 x ^ (y ^ (z ^ x))' != 0 | y ^ (z ^ x) = x. [para(158(a,1),34(a,1)),rewrite([4(7),228(13)]),xx(a)]. given #878 (T,wt=14): 2998 x ^ (((y v z) ^ x)' ^ (u ^ z)) = 0. [para(727(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #879 (T,wt=14): 3002 x ^ (y ^ (((z v y) ^ x)' ^ u)) = 0. [para(727(a,1),124(a,1,2,2,2,1)),rewrite([62(5),2196(11)])]. given #880 (T,wt=14): 3004 x ^ (y ^ (y ^ (z v (u v x)))') = 0. [para(3(a,1),731(a,1,2,2,1,2))]. given #881 (T,wt=14): 3015 x ^ (y ^ (z ^ (z ^ (y ^ x))')) = 0. [para(212(a,1),731(a,1,2,2,1,2)),rewrite([5(6)])]. given #882 (A,wt=23): 403 (x v y) ^ (z ^ (u ^ y))' != 0 | (x v y)' = (z ^ (u ^ y))'. [para(158(a,1),35(a,1,2)),rewrite([79(2)]),xx(a)]. given #883 (T,wt=14): 3023 x ^ ((y v (x v z)) ^ (u v x))' = 0. [para(731(a,1),104(a,1)),flip(a)]. given #884 (T,wt=14): 3024 x ^ (y ^ ((y v z) ^ (u v x))') = 0. [para(731(a,1),105(a,1,2)),rewrite([81(2)]),flip(a)]. given #885 (T,wt=14): 3025 x ^ ((x ^ (y v z))' ^ (u ^ z)) = 0. [para(731(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #886 (T,wt=14): 3027 x ^ (y ^ ((x ^ (z v y))' ^ u)) = 0. [para(731(a,1),124(a,1,2,2,2,1)),rewrite([62(5),749(11)])]. given #887 (A,wt=29): 405 x ^ (y ^ (z v (x ^ (y ^ ((z ^ (x ^ y)) v (u ^ w)))))) = x ^ (y ^ (z v (u ^ w))). [para(39(a,1),5(a,1)),rewrite([5(4),5(10)]),flip(a)]. given #888 (T,wt=14): 3052 (x ^ y)' v ((x ^ (z v y)) v u) = 1. [para(745(a,1),85(a,1,1)),rewrite([61(8),3029(11)])]. given #889 (T,wt=14): 3113 x ^ (y ^ ((x v z) ^ (u v y))') = 0. [para(749(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. given #890 (T,wt=14): 3118 x ^ (y ^ ((z v x) ^ (u v y))') = 0. [para(749(a,1),75(a,1,2)),rewrite([81(2)]),flip(a)]. given #891 (T,wt=14): 3128 x ^ ((y ^ (z v x))' ^ (u ^ y)) = 0. [para(749(a,1),460(a,1,2,2,2,1)),rewrite([71(6),30(6),5(6)])]. given #892 (A,wt=27): 406 x ^ ((y ^ z) v (x ^ ((y ^ (z ^ x)) v (u ^ w)))) = x ^ ((y ^ z) v (u ^ w)). [para(5(a,1),39(a,1,2,2,2,1))]. given #893 (T,wt=14): 3133 ((x ^ (y ^ z)) v u) ^ (z v u)' = 0. [para(5(a,1),767(a,1,1,1))]. given #894 (T,wt=14): 3143 ((x ^ y) v (z ^ (y ^ u))) ^ y' = 0. [para(66(a,1),767(a,1,2,1))]. given #895 (T,wt=14): 3144 ((x ^ y) v (z ^ (u ^ y))) ^ y' = 0. [para(94(a,1),767(a,1,2,1))]. given #896 (T,wt=14): 3158 ((x ^ y) v z) ^ (y v (z v u))' = 0. [para(767(a,1),88(a,1,2)),rewrite([4(4),72(4)]),flip(a)]. given #897 (A,wt=17): 408 x ^ (y v (x ^ ((y ^ x) v z))) = x ^ (y v z). [para(6(a,1),39(a,1,2,2,2,2)),rewrite([6(7)])]. given #898 (T,wt=14): 3168 (x v y)' ^ (((z ^ x) v y) ^ u) = 0. [para(767(a,1),457(a,1,2,2,1,1)),rewrite([71(6),61(6)])]. given #899 (T,wt=14): 3178 x v (y v ((z ^ (u ^ x)) v y)') = 1. [para(5(a,1),772(a,1,2,2,1,1))]. given #900 (T,wt=14): 3197 x v (((y ^ z) v x)' v (u v z)) = 1. [para(772(a,1),86(a,1,1)),rewrite([3(7),61(8),772(11)])]. Low Water (displace): id=22471, wt=19.000 Low Water (displace): id=22472, wt=18.000 Low Water (displace): id=22483, wt=16.000 given #901 (T,wt=14): 3201 x v (y v (((z ^ y) v x)' v u)) = 1. [para(772(a,1),89(a,1,1)),rewrite([61(8),2107(11)])]. given #902 (A,wt=29): 411 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (z ^ y)) v (u ^ w)))))) = x ^ (y ^ (z v (u ^ w))). [para(17(a,1),39(a,1,2,2,2,1)),rewrite([5(7),5(9),5(13)])]. given #903 (T,wt=14): 3215 x v (y v (y v (z ^ (u ^ x)))') = 1. [para(5(a,1),778(a,1,2,2,1,2))]. given #904 (T,wt=14): 3231 x v ((x v (y ^ z))' v (u v z)) = 1. [para(778(a,1),86(a,1,1)),rewrite([3(7),61(8),778(11)])]. given #905 (T,wt=14): 3236 x v (y v ((x v (z ^ y))' v u)) = 1. [para(778(a,1),89(a,1,1)),rewrite([61(8),831(11)])]. given #906 (T,wt=14): 3347 (x v y)' ^ ((x v (z ^ y)) ^ u) = 0. [para(828(a,1),457(a,1,2,2,1,1)),rewrite([71(6),61(6)])]. given #907 (A,wt=33): 416 (x v y) ^ (z ^ (x v ((x v y) ^ (z ^ ((x ^ z) v (u ^ w)))))) = (x v y) ^ (z ^ (x v (u ^ w))). [para(20(a,1),39(a,1,2,2,2,1)),rewrite([5(8),5(10),5(15)])]. given #908 (T,wt=14): 3359 x v (y v ((x ^ z) v (u ^ y))') = 1. [para(831(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #909 (T,wt=14): 3368 x v (y v ((z ^ x) v (u ^ y))') = 1. [para(831(a,1),92(a,1,2)),rewrite([79(2)]),flip(a)]. given #910 (T,wt=14): 3373 x v ((y v (z ^ x))' v (u v y)) = 1. [para(831(a,1),86(a,1,1)),rewrite([3(7),61(8),831(11)])]. given #911 (T,wt=14): 3393 x v (y v (z ^ (y v (x ^ u)))') = 1. [para(875(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. given #912 (A,wt=26): 417 x' ^ (y ^ (x v (x' ^ (y ^ (z ^ u))))) = x' ^ (y ^ (x v (z ^ u))). [para(73(a,1),39(a,1,2,2,2,1)),rewrite([62(7),5(6),5(8),5(13)])]. Low Water (displace): id=22736, wt=15.000 given #913 (T,wt=13): 22734 x' ^ (y ^ (x v (y' ^ z))) = 0. [para(73(a,1),417(a,1,2,2,2,2)),rewrite([4(4),72(4),33(3),245(3)]),flip(a)]. given #914 (T,wt=11): 23047 x' ^ (y ^ (x v y')) = 0. [para(6(a,1),22734(a,1,2,2,2))]. given #915 (T,wt=11): 23061 x ^ ((y v x') ^ y') = 0. [hyper(18573,a,23047,a),rewrite([5(5)])]. given #916 (T,wt=11): 23066 x ^ (y' ^ (y v x')) = 0. [hyper(236,a,2959,a,b,23047,a(flip)),rewrite([23047(5),62(8),228(7),23047(10)])]. given #917 (A,wt=26): 418 x ^ (y' ^ (y v (x ^ (y' ^ (z ^ u))))) = x ^ (y' ^ (y v (z ^ u))). [para(82(a,1),39(a,1,2,2,2,1)),rewrite([62(7),5(6),5(8),5(13)])]. given #918 (T,wt=11): 23071 (x v y') ^ (x' ^ y) = 0. [hyper(236,a,1003,a,b,23047,a(flip)),rewrite([23047(5),62(8),228(7),23047(10)])]. Low Water (displace): id=23294, wt=14.000 Low Water (displace): id=23320, wt=12.000 Low Water (displace): id=23336, wt=11.000 given #919 (T,wt=11): 23081 x' ^ (y ^ (y' v x)) = 0. [para(2(a,1),23047(a,1,2,2))]. given #920 (T,wt=10): 23642 x ^ (x' v y) = x ^ y. [hyper(34,a,1402,a,b,23081,a),rewrite([228(3),657(5)]),flip(a)]. given #921 (T,wt=9): 23672 x ^ (x' ^ y)' = x. [para(143(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #922 (A,wt=26): 419 (x v y)' ^ (x v ((x v y)' ^ (z ^ u))) = (x v y)' ^ (x v (z ^ u)). [para(103(a,1),39(a,1,2,2,2,1)),rewrite([62(7)])]. given #923 (T,wt=9): 23673 x ^ (y ^ x')' = x. [para(152(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #924 (T,wt=10): 23665 x ^ (y v x') = x ^ y. [para(2(a,1),23642(a,1,2))]. given #925 (T,wt=10): 23940 x' ^ (x ^ y)' = x'. [para(228(a,1),23672(a,1,2,1,1))]. Low Water (keep): wt=19.000, iters=6678 given #926 (T,wt=10): 24128 x' ^ (y ^ x)' = x'. [para(228(a,1),23673(a,1,2,1,2))]. given #927 (A,wt=26): 421 (x v y)' ^ (y v ((x v y)' ^ (z ^ u))) = (x v y)' ^ (y v (z ^ u)). [para(116(a,1),39(a,1,2,2,2,1)),rewrite([62(7)])]. given #928 (T,wt=11): 23097 x' ^ ((y v x) ^ y') = 0. [hyper(261,a,2945,a,b,23061,a),rewrite([2945(6),68(2),228(4)]),flip(a)]. given #929 (T,wt=11): 23643 (x' v y) ^ (y' ^ x) = 0. [hyper(236,a,1003,a,b,23081,a(flip)),rewrite([23642(4),245(3),62(8),228(7),23642(9),245(8)])]. given #930 (T,wt=11): 23675 x ^ (y v (x' v y)') = x. [para(29(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #931 (T,wt=11): 23676 x' ^ (x v y) = x' ^ y. [para(228(a,1),23642(a,1,2,1))]. given #932 (A,wt=32): 426 x ^ ((y ^ x)' ^ (y v (x ^ ((y ^ x)' ^ (z ^ u))))) = x ^ ((y ^ x)' ^ (y v (z ^ u))). [para(32(a,1),39(a,1,2,2,2,1)),rewrite([62(9),5(8),5(10),5(16)])]. given #933 (T,wt=11): 23677 x ^ ((x' ^ y)' v z) = x. [para(148(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #934 (T,wt=11): 23678 x ^ (y v (x' ^ z)') = x. [para(149(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #935 (T,wt=11): 23679 x ^ (y ^ (x' ^ z))' = x. [para(155(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #936 (T,wt=11): 23680 x ^ ((y ^ x')' v z) = x. [para(156(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #937 (A,wt=32): 427 x ^ (y' ^ (z ^ (y v (x ^ (y' ^ (z ^ (u ^ w))))))) = x ^ (y' ^ (z ^ (y v (u ^ w)))). [para(108(a,1),39(a,1,2,2,2,1)),rewrite([62(9),5(8),5(7),5(10),5(9),5(16),5(15)])]. given #938 (T,wt=11): 23681 x ^ (y ^ (z ^ x'))' = x. [para(158(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #939 (T,wt=11): 23682 x ^ (y v (z ^ x')') = x. [para(160(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #940 (T,wt=11): 23683 x ^ (y v (y v x')') = x. [para(199(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. given #941 (T,wt=11): 23944 x ^ ((y v x)' ^ z)' = x. [para(23672(a,1),75(a,1,2)),rewrite([18(2)]),flip(a)]. given #942 (A,wt=32): 430 (x v y)' ^ (z ^ (x v ((x v y)' ^ (z ^ (u ^ w))))) = (x v y)' ^ (z ^ (x v (u ^ w))). [para(109(a,1),39(a,1,2,2,2,1)),rewrite([62(9),5(8),5(10),5(16)])]. given #943 (T,wt=11): 24126 x ^ (y ^ (x v z)')' = x. [para(23673(a,1),20(a,1,2)),rewrite([6(2)]),flip(a)]. given #944 (T,wt=11): 24132 x ^ (y ^ (z v x)')' = x. [para(23673(a,1),75(a,1,2)),rewrite([18(2)]),flip(a)]. given #945 (T,wt=11): 24284 x' ^ (y v x) = x' ^ y. [para(228(a,1),23665(a,1,2,2))]. given #946 (T,wt=11): 24384 x' ^ y != 0 | x v y = x. [back_rewrite(6957),rewrite([24284(3)])]. given #947 (A,wt=24): 437 x v ((y ^ ((x ^ y) v (z ^ u))) v ((y ^ (x v (z ^ u)))' v w)) = 1. [para(39(a,1),156(a,1,2,1,1)),rewrite([3(11)])]. given #948 (T,wt=9): 27408 x v (y v x')' = x. [hyper(24384,a,116,a)]. given #949 (T,wt=9): 27413 x v (x' v y)' = x. [hyper(24384,a,103,a)]. given #950 (T,wt=10): 27453 x' v (y v x)' = x'. [para(228(a,1),27408(a,1,2,1,2))]. Low Water (keep): wt=18.000, iters=6697 given #951 (T,wt=10): 27607 x' v (x v y)' = x'. [para(228(a,1),27413(a,1,2,1,1))]. given #952 (A,wt=24): 438 x v ((y ^ ((x ^ y) v (z ^ u))) v (w ^ (y ^ (x v (z ^ u))))') = 1. [para(39(a,1),158(a,1,2,1,2)),rewrite([3(11)])]. given #953 (T,wt=11): 24385 x' ^ y != 0 | y v x = x. [back_rewrite(249),rewrite([24284(3)])]. given #954 (T,wt=11): 24740 (x v y) ^ (x' ^ y') = 0. [hyper(18573,a,23097,a),rewrite([5(5)])]. given #955 (T,wt=11): 25018 (x v y) ^ (y' ^ x') = 0. [hyper(236,a,2959,a,b,23097,a(flip)),rewrite([23097(5),62(8),228(7),23097(10)])]. given #956 (T,wt=11): 25048 x' ^ y = (y v x) ^ x'. [para(23097(a,1),205(a,1,2)),rewrite([2(5),62(5),24284(6)]),flip(a)]. given #957 (A,wt=19): 441 x ^ (y v (z ^ x)') != 0 | y v (z ^ x)' = x'. [para(160(a,1),10(a,1)),flip(c),xx(a)]. given #958 (T,wt=11): 25425 x' ^ y = (x v y) ^ x'. [para(23676(a,1),4(a,1))]. given #959 (T,wt=11): 26650 x ^ ((x v y)' ^ z)' = x. [para(2(a,1),23944(a,1,2,1,1,1))]. given #960 (T,wt=11): 27401 x v (y ^ (y ^ x')') = x. [hyper(24384,a,214,a)]. given #961 (T,wt=11): 27402 x v (y ^ (z v x')') = x. [hyper(24384,a,131,a)]. given #962 (A,wt=16): 444 (x ^ ((y ^ x) v z)) v (u v (y ^ x)') = 1. [para(21(a,1),160(a,1,2,2,1))]. given #963 (T,wt=11): 27414 x v (y ^ (x' ^ y)') = x. [hyper(24384,a,32,a)]. given #964 (T,wt=11): 27415 x ^ y' != 0 | y v x = y. [para(4(a,1),24384(a,1))]. given #965 (T,wt=11): 27444 x v (y' v x)' = x v y. [back_rewrite(25215),rewrite([27413(4)]),flip(a)]. given #966 (T,wt=10): 28917 (x' v y) ^ (y v x) = y. [para(27444(a,1),23665(a,1,2)),rewrite([4(7),18(7)])]. given #967 (A,wt=21): 471 x ^ ((y v (x ^ ((x ^ y) v z))) ^ u) = x ^ ((y v z) ^ u). [para(6(a,1),40(a,1,2,1,2,2,2)),rewrite([6(8)])]. given #968 (T,wt=10): 28923 (x ^ y) v (y' ^ x) = x. [para(27444(a,1),27444(a,1,2,1)),rewrite([28918(4),228(2),28918(4),28918(8),228(6),2(6),7(6)])]. given #969 (T,wt=10): 28924 x v (x' ^ y) = x v y. [para(27444(a,1),27444(a,2)),rewrite([28918(3),2(4),28877(4),228(4)])]. given #970 (T,wt=10): 29035 (x v y) ^ (x v y') = x. [para(2(a,1),28917(a,1,1)),rewrite([4(4)])]. given #971 (T,wt=10): 29036 (x v y) ^ (x' v y) = y. [para(2(a,1),28917(a,1,2)),rewrite([4(4)])]. given #972 (A,wt=29): 476 x ^ (y ^ ((z v (x ^ ((x ^ z) v (u ^ w)))) ^ v5)) = y ^ (x ^ ((z v (u ^ w)) ^ v5)). [para(40(a,1),17(a,1,2)),flip(a)]. given #973 (T,wt=10): 29038 (x v y) ^ (y' v x) = x. [para(28917(a,1),4(a,1)),flip(a)]. given #974 (T,wt=10): 29045 (x v y') ^ (y v x) = x. [para(59(a,1),28917(a,1,2)),rewrite([2(3),28879(3)])]. given #975 (T,wt=10): 29047 (x v y) ^ (y v x') = y. [para(228(a,1),28917(a,1,1,1))]. given #976 (T,wt=10): 29304 (x v y)' = y' ^ x'. [para(27408(a,1),28917(a,1,1)),rewrite([228(3),2(4),28879(4),23676(4),228(5)]),flip(a)]. given #977 (A,wt=29): 480 x ^ ((y v ((x v z) ^ (((x v z) ^ y) v (u ^ w)))) ^ v5) = x ^ ((y v (u ^ w)) ^ v5). [para(40(a,1),20(a,1,2)),rewrite([20(6)]),flip(a)]. given #978 (T,wt=10): 29363 x v (y ^ x') = x v y. [back_rewrite(28869),rewrite([29304(3),228(2)])]. given #979 (T,wt=10): 31189 (x ^ y) v (x ^ y') = x. [para(4(a,1),28923(a,1,2))]. given #980 (T,wt=10): 37086 (x ^ y)' = x' v y'. [back_rewrite(31418),rewrite([31901(6)])]. given #981 (T,wt=11): 28181 x ^ y' != 0 | x v y = y. [para(4(a,1),24385(a,1))]. given #982 (A,wt=28): 505 x' ^ (((y ^ x) v (x' ^ (z ^ u))) ^ w) = x' ^ (((y ^ x) v (z ^ u)) ^ w). [para(245(a,1),40(a,1,2,1,2,2,1)),rewrite([62(6)])]. given #983 (T,wt=11): 28506 (x v y) ^ y' = x ^ y'. [para(25048(a,1),4(a,1))]. given #984 (T,wt=11): 28569 (x v y) ^ x' = y ^ x'. [para(25425(a,1),4(a,1))]. given #985 (T,wt=11): 28878 x v y != 1 | y' v x = x. [para(27444(a,1),34(a,1)),rewrite([4(7),116(7),228(10)]),xx(b)]. given #986 (T,wt=10): 38964 x ^ y != 1 | y ^ x = 1. [para(205(a,1),28878(a,1)),rewrite([37086(6),37086(6),2(10),36835(10)]),flip(b)]. given #987 (A,wt=29): 559 x ^ (y ^ (z v (x ^ (y ^ ((y ^ (z ^ x)) v (u ^ w)))))) = x ^ (y ^ (z v (u ^ w))). [para(4(a,1),41(a,1,2,2,2,2,2,1)),rewrite([5(2)])]. given #988 (T,wt=10): 38977 x v y != 1 | y v x = 1. [para(168(a,1),38964(a,1)),rewrite([168(6)])]. given #989 (T,wt=11): 28910 x v y != 1 | x v y' = x. [para(27444(a,1),8980(a,1))]. given #990 (T,wt=11): 28955 x v y' != 1 | x v y = x. [back_rewrite(8980),rewrite([28879(3)])]. given #991 (T,wt=11): 28956 x v y' != 1 | y v x = x. [back_rewrite(5274),rewrite([28879(3)])]. given #992 (A,wt=25): 561 x ^ (y ^ (z v (x ^ (y ^ ((x ^ (y ^ z)) v u))))) = x ^ (y ^ (z v u)). [para(6(a,1),41(a,1,2,2,2,2,2,2)),rewrite([6(10)])]. given #993 (T,wt=11): 29017 x ^ y != 0 | y' ^ x = x. [back_rewrite(23773),rewrite([28918(6)])]. given #994 (T,wt=11): 29031 0 != x | x v y = x' ^ y. [back_rewrite(28865),rewrite([28924(5)])]. given #995 (T,wt=11): 29414 x ^ y != 0 | x ^ y' = x. [back_rewrite(24390),rewrite([29304(5),29363(7),29304(6),228(5)])]. given #996 (T,wt=11): 31196 (x ^ y) v x' = y v x'. [para(18(a,1),28923(a,1,2)),rewrite([4(3),23665(3)])]. ============================== PROOF ================================= % Proof 1 at 54.69 (+ 0.62) seconds: distributivity. % Length of proof is 123. % Level of proof is 26. % Maximum clause weight is 26.000. % Given clauses 996. 1 x ^ (y v z) = (x ^ y) v (x ^ z) # answer(distributivity) # label(non_clause) # label(goal). [goal]. 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]. 11 x ^ (y v (z ^ u)) = x ^ (y v (x ^ ((x ^ y) v (z ^ u)))) # label(H65). [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)]. 15 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])]. 17 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. 18 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. 20 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 21 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. 22 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. 23 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 25 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. 26 x ^ x = x. [para(7(a,1),6(a,1,2))]. 27 x v x = x. [para(6(a,1),7(a,1,2))]. 28 x v (x' v y) = 1 v y. [para(8(a,1),3(a,1,1)),flip(a)]. 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. 30 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. 31 x ^ (x' ^ y) = 0 ^ y. [para(9(a,1),5(a,1,1)),flip(a)]. 33 x v 0 = x. [para(9(a,1),7(a,1,2))]. 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. 39 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))]. 40 x ^ ((y v (x ^ ((x ^ y) v (z ^ u)))) ^ w) = x ^ ((y v (z ^ u)) ^ w). [para(12(a,1),5(a,1,1)),rewrite([5(4)]),flip(a)]. 42 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)])]. 51 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(15(a,1),10(a,1))]. 52 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. 57 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. 61 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. 62 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. 65 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. 67 x ^ (y ^ x') = y ^ 0. [para(9(a,1),17(a,1,2)),flip(a)]. 68 1' = 0. [hyper(10,a,33,a,b,61,a)]. 69 1 v x = 1. [para(61(a,1),6(a,1))]. 70 x v (x' v y) = 1. [back_rewrite(28),rewrite([69(5)])]. 72 0 ^ x = 0. [para(62(a,1),6(a,1,2))]. 73 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite([72(5)])]. 76 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(18(a,1),5(a,1)),flip(a)]. 79 x v 1 = 1. [para(18(a,1),61(a,1)),flip(a)]. 81 x ^ 0 = 0. [para(72(a,1),4(a,1)),flip(a)]. 82 x ^ (y ^ x') = 0. [back_rewrite(67),rewrite([81(5)])]. 92 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. 93 x v (y v (z ^ (x v y))) = x v y. [para(24(a,1),3(a,1)),flip(a)]. 94 x v (y ^ (z ^ x)) = x. [para(5(a,1),24(a,1,2))]. 97 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(17(a,1),24(a,1,2))]. 103 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite([81(2)]),flip(a)]. 120 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. 125 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(21(a,1),24(a,1,2)),rewrite([2(5)])]. 143 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite([79(2)]),flip(a)]. 147 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite([4(4)])]. 152 x v (y ^ x)' = 1. [para(4(a,1),143(a,1,2,1))]. 161 (x ^ y) v (x ^ (z ^ y))' = 1. [para(17(a,1),152(a,1,2,1))]. 176 (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)])]. 228 x'' = x. [para(8(a,1),34(a,1)),rewrite([4(5),9(5)]),xx(a),xx(b)]. 245 x' ^ (y ^ x) = 0. [para(228(a,1),82(a,1,2,2))]. 408 x ^ (y v (x ^ ((y ^ x) v z))) = x ^ (y v z). [para(6(a,1),39(a,1,2,2,2,2)),rewrite([6(7)])]. 417 x' ^ (y ^ (x v (x' ^ (y ^ (z ^ u))))) = x' ^ (y ^ (x v (z ^ u))). [para(73(a,1),39(a,1,2,2,2,1)),rewrite([62(7),5(6),5(8),5(13)])]. 471 x ^ ((y v (x ^ ((x ^ y) v z))) ^ u) = x ^ ((y v z) ^ u). [para(6(a,1),40(a,1,2,1,2,2,2)),rewrite([6(8)])]. 657 x ^ (x' v (x ^ y)) = x ^ (x' v y). [para(9(a,1),42(a,1,2,2,2,1)),rewrite([62(3)])]. 671 x ^ (y v (x ^ (y v z))) = x ^ (y v z). [para(57(a,1),42(a,2,2)),rewrite([15(3),92(3)])]. 762 x v (y v ((z ^ x) v u)) = y v (x v u). [para(92(a,1),15(a,1,2)),flip(a)]. 793 x' ^ (x v y) != 0 | x v y = x. [para(70(a,1),51(a,1)),rewrite([228(10)]),flip(c),xx(a)]. 1402 (x ^ (y v (x ^ z))) v (x ^ z)' = 1. [para(76(a,1),161(a,1,2,1))]. 2323 (x ^ y) v (x ^ ((y ^ x) v z)) = x ^ ((y ^ x) v z). [para(120(a,1),97(a,1,2)),rewrite([2(5)])]. 4772 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(7(a,1),147(a,1,1))]. 4781 (x ^ (y v z)) v (x ^ ((y ^ u) v z)) = x ^ (y v z). [para(147(a,1),25(a,1,2,2))]. 6957 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),793(a,1,2))]. 7297 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(24(a,1),176(a,1,1)),rewrite([24(3),24(7)])]. 22426 x v (y ^ ((x ^ y) v z)) = x v (y ^ (x v z)). [para(408(a,1),24(a,1,2)),rewrite([2(7),15(7),4781(6)]),flip(a)]. 22734 x' ^ (y ^ (x v (y' ^ z))) = 0. [para(73(a,1),417(a,1,2,2,2,2)),rewrite([4(4),72(4),33(3),245(3)]),flip(a)]. 23047 x' ^ (y ^ (x v y')) = 0. [para(6(a,1),22734(a,1,2,2,2))]. 23081 x' ^ (y ^ (y' v x)) = 0. [para(2(a,1),23047(a,1,2,2))]. 23642 x ^ (x' v y) = x ^ y. [hyper(34,a,1402,a,b,23081,a),rewrite([228(3),657(5)]),flip(a)]. 23665 x ^ (y v x') = x ^ y. [para(2(a,1),23642(a,1,2))]. 23672 x ^ (x' ^ y)' = x. [para(143(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. 23673 x ^ (y ^ x')' = x. [para(152(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. 23675 x ^ (y v (x' v y)') = x. [para(29(a,1),23642(a,1,2)),rewrite([30(2)]),flip(a)]. 23676 x' ^ (x v y) = x' ^ y. [para(228(a,1),23642(a,1,2,1))]. 24127 (x ^ y')' v (z ^ y) = (x ^ y')'. [para(23673(a,1),94(a,1,2,2))]. 24128 x' ^ (y ^ x)' = x'. [para(228(a,1),23673(a,1,2,1,2))]. 24133 x v ((y ^ x')' v z) = (y ^ x')' v z. [para(23673(a,1),92(a,1,2,1)),rewrite([15(5)])]. 24280 x ^ ((y v x') ^ z) = x ^ (y ^ z). [para(23665(a,1),5(a,1,1)),rewrite([5(2)]),flip(a)]. 24284 x' ^ (y v x) = x' ^ y. [para(228(a,1),23665(a,1,2,2))]. 24384 x' ^ y != 0 | x v y = x. [back_rewrite(6957),rewrite([24284(3)])]. 24564 x' ^ (y ^ (z ^ x)') = y ^ x'. [para(24128(a,1),17(a,1,2)),flip(a)]. 24566 x' ^ (y v x)' = (y v x)'. [para(18(a,1),24128(a,1,2,1)),rewrite([4(4)])]. 25215 x v (y v (y' v x)') = x v (y' v x)'. [para(23675(a,1),93(a,1,2,2)),rewrite([2(4)])]. 25429 x' ^ ((x ^ y) v z) = x' ^ z. [para(22(a,1),23676(a,1,2)),rewrite([23676(3)]),flip(a)]. 27413 x v (x' v y)' = x. [hyper(24384,a,103,a)]. 27444 x v (y' v x)' = x v y. [back_rewrite(25215),rewrite([27413(4)]),flip(a)]. 28877 x v (x' ^ y)' = (x' ^ y)'. [para(143(a,1),27444(a,1,2,1)),rewrite([68(5),2(5),62(5),2(7)]),flip(a)]. 28917 (x' v y) ^ (y v x) = y. [para(27444(a,1),23665(a,1,2)),rewrite([4(7),18(7)])]. 28918 (x' v y)' = y' ^ x. [para(27444(a,1),23676(a,1,2)),rewrite([23676(3),24566(7)]),flip(a)]. 28923 (x ^ y) v (y' ^ x) = x. [para(27444(a,1),27444(a,1,2,1)),rewrite([28918(4),228(2),28918(4),28918(8),228(6),2(6),7(6)])]. 28924 x v (x' ^ y) = x v y. [para(27444(a,1),27444(a,2)),rewrite([28918(3),2(4),28877(4),228(4)])]. 29047 (x v y) ^ (y v x') = y. [para(228(a,1),28917(a,1,1,1))]. 31196 (x ^ y) v x' = y v x'. [para(18(a,1),28923(a,1,2)),rewrite([4(3),23665(3)])]. 31396 x' v (x ^ (x ^ y)') = (x ^ y)'. [para(23672(a,1),28923(a,1,2)),rewrite([228(2),4(3),2(5),228(7)])]. 31399 x ^ (x ^ y)' = x ^ y'. [para(28923(a,1),23676(a,1,2)),rewrite([4(3),4(8),5(8),24564(8)])]. 31418 (x ^ y)' = x' v (x ^ y'). [back_rewrite(31396),rewrite([31399(4)]),flip(a)]. 31900 x' v ((x ^ y) v z) = x' v (y v z). [back_rewrite(24133),rewrite([31418(3),228(3),3(4),762(5),31418(6),228(6),3(7)]),flip(a)]. 31901 x' v (x ^ y) = x' v y. [back_rewrite(24127),rewrite([31418(3),228(3),3(5),31900(5),24(3),31418(5),228(5)]),flip(a)]. 37086 (x ^ y)' = x' v y'. [back_rewrite(31418),rewrite([31901(6)])]. 37146 x v (y ^ (x' ^ z)) = x v (y ^ z). [para(17(a,1),28924(a,1,2))]. 37166 (x ^ y) v (y ^ (x' ^ z)) = y ^ ((x ^ y) v z). [para(125(a,1),28924(a,2)),rewrite([37086(3),17(8),24280(8),25429(5)])]. 37831 x ^ ((y v z) ^ ((x ^ ((x ^ y) v z)) v y')) = x ^ ((x ^ y) v z). [para(29047(a,1),471(a,1,2)),rewrite([52(4)]),flip(a)]. 39476 (x ^ ((x ^ y) v z)) v y' = x v y'. [para(120(a,1),31196(a,1,1)),rewrite([31196(3)]),flip(a)]. 39588 x ^ ((x ^ y) v z) = (y v z) ^ x. [back_rewrite(37831),rewrite([39476(6),65(5)]),flip(a)]. 40124 (x ^ y) v (x ^ z) = x ^ (y v (x ^ z)). [back_rewrite(4772),rewrite([39588(4),4(3)]),flip(a)]. 40469 x ^ ((y ^ x) v z) = x ^ (y v z). [back_rewrite(2323),rewrite([40124(5),22426(4),671(4)]),flip(a)]. 40484 c1 ^ (c2 v (c1 ^ c3)) != c1 ^ (c2 v c3) # answer(distributivity). [back_rewrite(13),rewrite([40124(7)])]. 40615 (x ^ y) v (y ^ (x' ^ z)) = y ^ (x v z). [back_rewrite(37166),rewrite([40469(8)])]. 40706 (x ^ y) v (y ^ z) = y ^ (x v (y ^ z)). [back_rewrite(7297),rewrite([40469(4)]),flip(a)]. 40765 x ^ (y v (x ^ z)) = x ^ (y v z). [back_rewrite(40615),rewrite([40706(5),37146(4)])]. 40766 $F # answer(distributivity). [resolve(40765,a,40484,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=996. Generated=1756099. Kept=40763. proofs=1. Usable=206. Sos=9299. Demods=8428. Limbo=59, Disabled=31209. Hints=0. Kept_by_rule=0, Deleted_by_rule=326. Forward_subsumed=1629086. Back_subsumed=84. Sos_limit_deleted=85924. Sos_displaced=5761. Sos_removed=0. New_demodulators=37247 (6 lex), Back_demodulated=25351. Back_unit_deleted=0. Demod_attempts=38362804. Demod_rewrites=9766776. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=395456. Nonunit_bsub_feature_tests=88869. Megabytes=32.26. User_CPU=54.69, System_CPU=0.62, Wall_clock=56. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5147 exit (max_proofs) Tue Nov 3 09:47:33 2009