============================== Prover9 =============================== Prover9 (32) version April-2007, April 2007. Process 27120 was started by mccune on cleo, Fri Apr 13 09:21:27 2007 The command was "/home/mccune/bin/prover9 -f lt.in uc.in H27d.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 H27d.in assign(max_seconds,60). assign(max_weight,25). list(weights). weight(x') = weight(x). end_of_list. formulas(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). end_of_list. formulas(goals). x ^ (y v z) = (x ^ y) v (x ^ z) # label(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) # label(distributivity) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x v y = y v x. [assumption]. (x v y) v z = x v (y v z). [assumption]. x ^ y = y ^ x. [assumption]. (x ^ y) ^ z = x ^ (y ^ z). [assumption]. x ^ (x v y) = x. [assumption]. x v (x ^ y) = x. [assumption]. x v x' = 1. [assumption]. x ^ x' = 0. [assumption]. x v y != 1 | x ^ y != 0 | x' = y. [assumption]. x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label distributivity to answer in negative clause Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 0, 1, c1, c2, c3, ^, v, ' ]). After inverse_order: Function symbol precedence: lex([ 0, 1, c1, c2, c3, ^, v, ' ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(hyper_resolution). % (nonunit Horn with equality) % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: (no changes). % Operation v is commutative; C redundancy checks enabled. % Operation ^ is commutative; C redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 x v y = y v x. [assumption]. 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # 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 ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=7): 2 x v y = y v x. [assumption]. given #2 (I,wt=11): 3 (x v y) v z = x v (y v z). [assumption]. % Operation v is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 14 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 16 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=5): 8 x v x' = 1. [assumption]. given #8 (I,wt=5): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=13): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=23): 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. given #11 (I,wt=13): 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # 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): 67 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. given #19 (T,wt=3): 79 1' = 0. [hyper(10,a,33,a,b,67,a)]. given #20 (T,wt=5): 69 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. given #21 (T,wt=3): 82 0' = 1. [hyper(10,a,69,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): 80 1 v x = 1. [para(67(a,1),6(a,1))]. given #24 (T,wt=5): 83 0 ^ x = 0. [para(69(a,1),6(a,1,2))]. given #25 (T,wt=5): 93 x v 1 = 1. [para(18(a,1),67(a,1)),flip(a)]. given #26 (T,wt=5): 96 x ^ 0 = 0. [para(83(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=6): 94 0 != x | x' = 1. [back_rewrite(68),rewrite(93(2)),xx(a)]. given #29 (T,wt=6): 98 1 != x | x' = 0. [back_rewrite(70),rewrite(96(4)),xx(b)]. given #30 (T,wt=7): 24 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #31 (T,wt=7): 81 x v (x' v y) = 1. [back_rewrite(28),rewrite(80(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=7): 85 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite(83(5))]. given #34 (T,wt=7): 95 x v (y v x') = 1. [back_rewrite(50),rewrite(93(5))]. given #35 (T,wt=7): 97 x ^ (y ^ x') = 0. [back_rewrite(77),rewrite(96(5))]. given #36 (T,wt=7): 122 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite(96(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=7): 141 x ^ (y v x)' = 0. [para(2(a,1),122(a,1,2,1))]. given #39 (T,wt=9): 29 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #40 (T,wt=9): 32 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #41 (T,wt=9): 48 x ^ (y v (x v z)) = x. [para(15(a,1),6(a,1,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=7): 184 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #44 (T,wt=7): 195 x v (y ^ x)' = 1. [para(4(a,1),184(a,1,2,1))]. given #45 (T,wt=9): 54 x ^ (x ^ y) = x ^ y. [para(26(a,1),5(a,1,1)),flip(a)]. given #46 (T,wt=9): 56 x ^ (y ^ x) = y ^ x. [para(26(a,1),5(a,2,2)),rewrite(4(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): 57 1 != x | 0 != x | x' = x. [para(26(a,1),10(b,1)),rewrite(27(1)),flip(a),flip(b)]. given #49 (T,wt=9): 60 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. given #50 (T,wt=9): 62 x v (y v x) = y v x. [para(27(a,1),3(a,2,2)),rewrite(2(2))]. given #51 (T,wt=9): 76 x v (y ^ (x ^ z)) = x. [para(17(a,1),7(a,1,2))]. 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=9): 86 x ^ (y v (z v x)) = x. [para(3(a,1),18(a,1,2))]. given #54 (T,wt=9): 110 x v (y ^ (z ^ x)) = x. [para(5(a,1),24(a,1,2))]. given #55 (T,wt=9): 120 x v (y v (x' v z)) = 1. [para(81(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #56 (T,wt=9): 130 x ^ (y ^ (x' ^ z)) = 0. [para(85(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #57 (A,wt=13): 34 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #58 (T,wt=3): 279 x'' = x. [para(8(a,1),34(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. given #59 (T,wt=7): 296 x' v (y v x) = 1. [para(279(a,1),95(a,1,2,2))]. given #60 (T,wt=7): 297 x' ^ (y ^ x) = 0. [para(279(a,1),97(a,1,2,2))]. given #61 (T,wt=9): 131 x ^ ((x v y)' ^ z) = 0. [para(85(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #62 (A,wt=19): 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=9): 133 x v (y v (z v x')) = 1. [para(3(a,1),95(a,1,2))]. given #64 (T,wt=9): 137 x ^ (y ^ (z ^ x')) = 0. [para(5(a,1),97(a,1,2))]. given #65 (T,wt=9): 140 x ^ (y ^ (x v z)') = 0. [para(97(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #66 (T,wt=9): 146 x ^ (y v (x v z))' = 0. [para(15(a,1),122(a,1,2,1))]. given #67 (A,wt=13): 36 x v y != 1 | y ^ x != 0 | x' = y. [para(4(a,1),10(b,1))]. given #68 (T,wt=9): 155 x ^ (y v (z v x))' = 0. [para(3(a,1),141(a,1,2,1))]. given #69 (T,wt=9): 156 x ^ ((y v x)' ^ z) = 0. [para(141(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #70 (T,wt=9): 161 x ^ (y ^ (z v x)') = 0. [para(141(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #71 (T,wt=9): 162 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. given #72 (A,wt=19): 37 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. given #73 (T,wt=9): 168 x ^ (y ^ (y ^ x)') = 0. [para(4(a,1),32(a,1,2,2,1))]. given #74 (T,wt=9): 190 x v ((x ^ y)' v z) = 1. [para(81(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #75 (T,wt=9): 191 x v (y v (x ^ z)') = 1. [para(95(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #76 (T,wt=9): 199 x v (y ^ (x ^ z))' = 1. [para(17(a,1),184(a,1,2,1))]. given #77 (A,wt=23): 40 x ^ (y v ((x ^ z) v (z ^ (u v y)))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2,2,2))]. given #78 (T,wt=9): 200 x v ((y ^ x)' v z) = 1. [para(195(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #79 (T,wt=9): 202 x v (y ^ (z ^ x))' = 1. [para(5(a,1),195(a,1,2,1))]. given #80 (T,wt=9): 206 x v (y v (z ^ x)') = 1. [para(195(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #81 (T,wt=9): 298 x' v (y v (x v z)) = 1. [para(279(a,1),120(a,1,2,2,1))]. given #82 (A,wt=23): 41 x ^ (y v ((z ^ (y v u)) v (x ^ z))) = x ^ (y v (z ^ (x v u))). [para(2(a,1),12(a,1,2,2))]. given #83 (T,wt=9): 299 x' ^ (y ^ (x ^ z)) = 0. [para(279(a,1),130(a,1,2,2,1))]. given #84 (T,wt=9): 300 x' v (y v (z v x)) = 1. [para(3(a,1),296(a,1,2))]. given #85 (T,wt=9): 306 x' ^ (y ^ (z ^ x)) = 0. [para(5(a,1),297(a,1,2))]. given #86 (T,wt=9): 643 (x ^ y)' v (z v x) = 1. [para(7(a,1),300(a,1,2,2))]. given #87 (A,wt=23): 42 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,1))]. given #88 (T,wt=9): 647 (x ^ y)' v (z v y) = 1. [para(24(a,1),300(a,1,2,2))]. given #89 (T,wt=9): 660 (x v y)' ^ (z ^ x) = 0. [para(6(a,1),306(a,1,2,2))]. given #90 (T,wt=9): 664 (x v y)' ^ (z ^ y) = 0. [para(18(a,1),306(a,1,2,2))]. given #91 (T,wt=10): 326 x v y != 0 | (x v y)' = 1. [para(30(a,1),35(b,1)),rewrite(93(2),93(2)),xx(a)]. given #92 (A,wt=23): 43 x ^ (y v ((x ^ z) v ((y v u) ^ z))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,2))]. given #93 (T,wt=10): 327 x v y != 1 | (x v y)' = 0. [para(33(a,1),35(a,1,2)),rewrite(4(6),83(6)),xx(b)]. given #94 (T,wt=10): 439 x ^ y != 0 | (x ^ y)' = 1. [para(30(a,1),37(b,1,2)),rewrite(2(3),80(3)),xx(a)]. given #95 (T,wt=10): 440 x ^ y != 1 | (x ^ y)' = 0. [para(33(a,1),37(a,1)),rewrite(96(5),96(5)),xx(b)]. given #96 (T,wt=10): 748 x v y != 0 | (y v x)' = 1. [para(2(a,1),326(a,1))]. given #97 (A,wt=15): 46 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #98 (T,wt=10): 776 x v y != 1 | (y v x)' = 0. [para(2(a,1),327(a,1))]. given #99 (T,wt=10): 778 x ^ y != 0 | (y ^ x)' = 1. [para(4(a,1),439(a,1))]. given #100 (T,wt=10): 780 x ^ y != 1 | (y ^ x)' = 0. [para(4(a,1),440(a,1))]. given #101 (T,wt=11): 49 x v (y v (x ^ z)) = y v x. [para(7(a,1),15(a,1,2)),flip(a)]. given #102 (A,wt=19): 51 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(15(a,1),10(a,1))]. given #103 (T,wt=11): 75 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. given #104 (T,wt=11): 87 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. given #105 (T,wt=11): 92 x ^ (y ^ (z v x)) = y ^ x. [para(18(a,1),17(a,1,2)),flip(a)]. given #106 (T,wt=11): 108 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. given #107 (A,wt=23): 52 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(15(a,1),12(a,1,2))]. given #108 (T,wt=11): 113 x v (y v (z ^ x)) = y v x. [para(24(a,1),15(a,1,2)),flip(a)]. given #109 (T,wt=11): 117 x v (y v ((x v y)' v z)) = 1. [para(81(a,1),3(a,1)),flip(a)]. given #110 (T,wt=11): 127 x ^ (y ^ ((x ^ y)' ^ z)) = 0. [para(85(a,1),5(a,1)),flip(a)]. given #111 (T,wt=11): 132 x v (y v (z v (x v y)')) = 1. [para(95(a,1),3(a,1)),flip(a)]. given #112 (A,wt=13): 53 x ^ (y v ((x v z) ^ (x v u))) = x. [back_rewrite(44),rewrite(48(6)),flip(a)]. given #113 (T,wt=11): 136 x ^ (y ^ (z ^ (x ^ y)')) = 0. [para(97(a,1),5(a,1)),flip(a)]. given #114 (T,wt=11): 142 (x v y) ^ (x v (y v z))' = 0. [para(3(a,1),122(a,1,2,1))]. given #115 (T,wt=9): 1103 (x v y) ^ (y v x)' = 0. [para(62(a,1),142(a,1,2,1))]. given #116 (T,wt=11): 143 x ^ (y ^ ((x ^ y) v z)') = 0. [para(122(a,1),5(a,1)),flip(a)]. given #117 (A,wt=13): 59 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(39),rewrite(54(4))]. given #118 (T,wt=6): 1122 x' != 1 | 0 = x. [para(297(a,1),59(b,1)),rewrite(279(8),297(9)),flip(a),flip(c),xx(b)]. given #119 (T,wt=10): 1123 (x v y)' != 1 | x v y = 0. [para(660(a,1),59(b,1)),rewrite(279(10),660(12)),flip(a),xx(b)]. given #120 (T,wt=10): 1124 (x v y)' != 1 | y v x = 0. [para(2(a,1),1123(a,1,1))]. given #121 (T,wt=10): 1126 (x ^ y)' != 1 | x ^ y = 0. [para(25(a,1),1123(a,1,1)),rewrite(25(8))]. given #122 (A,wt=17): 64 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_rewrite(58),rewrite(60(7))]. given #123 (T,wt=10): 1129 (x ^ y)' != 1 | y ^ x = 0. [para(4(a,1),1126(a,1,1))]. given #124 (T,wt=11): 157 x ^ (y ^ (z v (x ^ y))') = 0. [para(141(a,1),5(a,1)),flip(a)]. given #125 (T,wt=11): 160 (x v y) ^ (x v (z v y))' = 0. [para(15(a,1),141(a,1,2,1))]. given #126 (T,wt=11): 166 x v (y v (z v (x v z)')) = 1. [para(29(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #127 (A,wt=13): 65 x v y != 1 | 0 != x | x' = x v y. [back_rewrite(38),rewrite(60(2))]. given #128 (T,wt=6): 1205 x' != 0 | 1 = x. [para(296(a,1),65(a,1)),rewrite(279(8),296(9)),flip(b),flip(c),xx(a)]. given #129 (T,wt=10): 1206 (x ^ y)' != 0 | x ^ y = 1. [para(643(a,1),65(a,1)),rewrite(279(10),643(12)),flip(b),xx(a)]. given #130 (T,wt=10): 1207 (x ^ y)' != 0 | y ^ x = 1. [para(4(a,1),1206(a,1,1))]. given #131 (T,wt=10): 1209 (x v y)' != 0 | x v y = 1. [para(19(a,1),1206(a,1,1)),rewrite(19(8))]. given #132 (A,wt=17): 71 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(33(a,1),12(a,1,2,2,2,2)),rewrite(63(5),33(6))]. given #133 (T,wt=10): 1212 (x v y)' != 0 | y v x = 1. [para(2(a,1),1209(a,1,1))]. given #134 (T,wt=11): 172 x ^ (y ^ (z ^ (x ^ z)')) = 0. [para(32(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #135 (T,wt=11): 174 x ^ (y ^ ((x v z) ^ y)') = 0. [para(32(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #136 (T,wt=11): 176 x ^ (y v (z v (x v u))) = x. [para(3(a,1),48(a,1,2))]. given #137 (A,wt=19): 72 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))). [back_rewrite(47),rewrite(69(5))]. given #138 (T,wt=11): 192 ((x ^ y) v z) ^ (x v z)' = 0. [para(22(a,1),141(a,1,2,1))]. given #139 (T,wt=11): 193 x v (y v ((x ^ z) v y)') = 1. [para(29(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #140 (T,wt=11): 194 x v (y v ((x v y) ^ z)') = 1. [para(184(a,1),3(a,1)),flip(a)]. given #141 (T,wt=11): 196 (x ^ y) v (x ^ (y ^ z))' = 1. [para(5(a,1),184(a,1,2,1))]. given #142 (A,wt=19): 73 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_rewrite(66),rewrite(71(9))]. given #143 (T,wt=9): 1462 (x ^ y) v (y ^ x)' = 1. [para(56(a,1),196(a,1,2,1))]. given #144 (T,wt=11): 201 x v (y v (z ^ (x v y))') = 1. [para(195(a,1),3(a,1)),flip(a)]. given #145 (T,wt=11): 207 (x ^ y) v (x ^ (z ^ y))' = 1. [para(17(a,1),195(a,1,2,1))]. given #146 (T,wt=11): 208 ((x v y) ^ z) v (x ^ z)' = 1. [para(20(a,1),195(a,1,2,1))]. given #147 (A,wt=19): 78 x v (y ^ z) != 1 | y ^ (x ^ z) != 0 | x' = y ^ z. [para(17(a,1),10(b,1))]. given #148 (T,wt=11): 214 (x v y) ^ (z ^ x) = z ^ x. [para(56(a,1),20(a,2)),rewrite(213(4))]. given #149 (T,wt=11): 229 (x v y) ^ (y v x) = x v y. [para(62(a,1),19(a,1,2))]. given #150 (T,wt=11): 230 (x ^ y) v (z v x) = z v x. [para(62(a,1),22(a,2)),rewrite(227(4))]. given #151 (T,wt=11): 232 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),76(a,1,2))]. given #152 (A,wt=13): 84 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [para(69(a,1),12(a,1,2,2,2,2)),rewrite(69(5),69(8),75(7))]. given #153 (T,wt=11): 244 (x ^ y) v (y ^ x) = x ^ y. [para(56(a,1),25(a,1,2))]. given #154 (T,wt=11): 245 x ^ (y v (z v (u v x))) = x. [para(3(a,1),86(a,1,2,2))]. given #155 (T,wt=11): 258 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),110(a,1,2,2))]. given #156 (T,wt=11): 267 x v (y v (z v (x' v u))) = 1. [para(3(a,1),120(a,1,2))]. given #157 (A,wt=13): 88 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(18(a,1),5(a,1)),flip(a)]. given #158 (T,wt=11): 270 x v (y v ((x ^ z)' v u)) = 1. [para(120(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #159 (T,wt=11): 272 x ^ (y ^ (z ^ (x' ^ u))) = 0. [para(5(a,1),130(a,1,2))]. given #160 (T,wt=11): 274 x ^ (y ^ ((x v z)' ^ u)) = 0. [para(130(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #161 (T,wt=11): 303 x v ((x v y)' v (z v y)) = 1. [para(15(a,1),296(a,1,2)),rewrite(15(5))]. given #162 (A,wt=13): 89 x v y != 1 | 0 != y | y' = x v y. [para(18(a,1),10(b,1)),rewrite(62(2)),flip(b)]. given #163 (T,wt=11): 310 x ^ ((x ^ y)' ^ (z ^ y)) = 0. [para(17(a,1),297(a,1,2)),rewrite(17(5))]. given #164 (T,wt=11): 316 x ^ ((y v (x v z))' ^ u) = 0. [para(15(a,1),131(a,1,2,1,1))]. given #165 (T,wt=11): 355 x v (y v (z v (u v x'))) = 1. [para(3(a,1),133(a,1,2,2))]. given #166 (T,wt=11): 358 x v (y v (z v (x ^ u)')) = 1. [para(133(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #167 (A,wt=13): 90 x ^ (y v ((z v x) ^ (x v u))) = x. [para(18(a,1),12(a,1,2,2,1)),rewrite(48(6)),flip(a)]. given #168 (T,wt=11): 363 x ^ (y ^ (z ^ (u ^ x'))) = 0. [para(5(a,1),137(a,1,2,2))]. given #169 (T,wt=11): 365 x ^ (y ^ (z ^ (x v u)')) = 0. [para(137(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #170 (T,wt=11): 370 x ^ (y ^ (z v (x v u))') = 0. [para(15(a,1),140(a,1,2,2,1))]. given #171 (T,wt=11): 373 x ^ (y v (z v (x v u)))' = 0. [para(3(a,1),146(a,1,2,1))]. given #172 (A,wt=13): 91 (x v y) ^ (x v (z v y)) = x v y. [para(15(a,1),18(a,1,2))]. given #173 (T,wt=11): 397 x ^ (y v (z v (u v x)))' = 0. [para(3(a,1),155(a,1,2,1,2))]. given #174 (T,wt=11): 398 x ^ ((y v (z v x))' ^ u) = 0. [para(155(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #175 (T,wt=11): 402 x ^ (y ^ (z v (u v x))') = 0. [para(155(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #176 (T,wt=11): 411 x ^ (y ^ ((z v x)' ^ u)) = 0. [para(156(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #177 (A,wt=13): 99 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),19(a,1,1))]. given #178 (T,wt=11): 416 x ^ (y ^ (z ^ (u v x)')) = 0. [para(5(a,1),161(a,1,2))]. given #179 (T,wt=11): 423 x v (y v ((y v x)' v z)) = 1. [para(162(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #180 (T,wt=11): 428 x v (y v (z v (z v x)')) = 1. [para(162(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #181 (T,wt=11): 430 x v (y v (y v (x ^ z))') = 1. [para(162(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. given #182 (A,wt=13): 100 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),19(a,1,2)),rewrite(3(3))]. given #183 (T,wt=11): 480 x ^ (y ^ ((y ^ x)' ^ z)) = 0. [para(168(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #184 (T,wt=11): 484 x ^ (y ^ (z ^ (z ^ x)')) = 0. [para(168(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #185 (T,wt=11): 486 x ^ (y ^ (y ^ (x v z))') = 0. [para(168(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. given #186 (T,wt=11): 494 x v ((y ^ (x ^ z))' v u) = 1. [para(17(a,1),190(a,1,2,1,1))]. given #187 (A,wt=19): 101 (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 #188 (T,wt=11): 502 x v (y v (z ^ (x ^ u))') = 1. [para(17(a,1),191(a,1,2,2,1))]. given #189 (T,wt=11): 509 x v (y ^ (z ^ (x ^ u)))' = 1. [para(5(a,1),199(a,1,2,1))]. given #190 (T,wt=11): 561 x v ((y ^ (z ^ x))' v u) = 1. [para(5(a,1),200(a,1,2,1,1))]. given #191 (T,wt=11): 565 x v (y v ((z ^ x)' v u)) = 1. [para(200(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #192 (A,wt=17): 102 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(19(a,1),5(a,1,1)),flip(a)]. given #193 (T,wt=11): 576 x v (y ^ (z ^ (u ^ x)))' = 1. [para(5(a,1),202(a,1,2,1,2))]. given #194 (T,wt=11): 580 x v (y v (z ^ (u ^ x))') = 1. [para(202(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #195 (T,wt=11): 590 x v (y v (z v (u ^ x)')) = 1. [para(3(a,1),206(a,1,2))]. given #196 (T,wt=11): 605 x' v (y v (z v (x v u))) = 1. [para(3(a,1),298(a,1,2))]. given #197 (A,wt=19): 104 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(19(a,1),12(a,1,2,2,2)),rewrite(2(4),24(4),60(2)),flip(a)]. given #198 (T,wt=11): 636 x' ^ (y ^ (z ^ (x ^ u))) = 0. [para(5(a,1),299(a,1,2))]. given #199 (T,wt=11): 642 x' v (y v (z v (u v x))) = 1. [para(3(a,1),300(a,1,2,2))]. given #200 (T,wt=11): 650 (x ^ (y ^ z))' v (u v y) = 1. [para(76(a,1),300(a,1,2,2))]. given #201 (T,wt=11): 652 (x ^ (y ^ z))' v (u v z) = 1. [para(110(a,1),300(a,1,2,2))]. given #202 (A,wt=19): 105 (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 #203 (T,wt=11): 659 x' ^ (y ^ (z ^ (u ^ x))) = 0. [para(5(a,1),306(a,1,2,2))]. given #204 (T,wt=11): 668 (x v (y v z))' ^ (u ^ y) = 0. [para(48(a,1),306(a,1,2,2))]. given #205 (T,wt=11): 669 (x v (y v z))' ^ (u ^ z) = 0. [para(86(a,1),306(a,1,2,2))]. given #206 (T,wt=11): 675 (x ^ y)' v (z v (x v u)) = 1. [para(643(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #207 (A,wt=15): 106 (x v y) ^ (x v (z v (y v u))) = x v y. [para(15(a,1),19(a,1,2,2))]. given #208 (T,wt=11): 676 (x ^ y)' v (z v (u v x)) = 1. [para(3(a,1),643(a,1,2))]. given #209 (T,wt=11): 707 (x ^ y)' v (z v (y v u)) = 1. [para(647(a,1),3(a,1,1)),rewrite(80(2),3(5)),flip(a)]. given #210 (T,wt=11): 708 (x ^ y)' v (z v (u v y)) = 1. [para(3(a,1),647(a,1,2))]. given #211 (T,wt=11): 723 (x v y)' ^ (z ^ (x ^ u)) = 0. [para(660(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #212 (A,wt=17): 107 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(19(a,1),17(a,1,2)),flip(a)]. given #213 (T,wt=11): 724 (x v y)' ^ (z ^ (u ^ x)) = 0. [para(5(a,1),660(a,1,2))]. given #214 (T,wt=11): 734 (x v y)' ^ (z ^ (y ^ u)) = 0. [para(664(a,1),5(a,1,1)),rewrite(83(2),5(5)),flip(a)]. given #215 (T,wt=11): 735 (x v y)' ^ (z ^ (u ^ y)) = 0. [para(5(a,1),664(a,1,2))]. given #216 (T,wt=11): 816 (x v (y ^ z)) ^ (x v y)' = 0. [para(49(a,1),141(a,1,2,1))]. given #217 (A,wt=13): 109 x v (y v (z ^ (x v y))) = x v y. [para(24(a,1),3(a,1)),flip(a)]. given #218 (T,wt=11): 819 x v (y v (x v (y ^ z))') = 1. [para(49(a,1),296(a,1,2)),rewrite(2(5),3(5))]. given #219 (T,wt=11): 859 (x ^ (y v z)) v (x ^ y)' = 1. [para(75(a,1),195(a,1,2,1))]. given #220 (T,wt=11): 861 x ^ (y ^ (x ^ (y v z))') = 0. [para(75(a,1),297(a,1,2)),rewrite(4(5),5(5))]. given #221 (T,wt=11): 876 x ^ (y ^ ((z v x) ^ y)') = 0. [para(32(a,1),87(a,1,2)),rewrite(96(2)),flip(a)]. given #222 (A,wt=13): 111 1 != x | y ^ x != 0 | x' = y ^ x. [para(24(a,1),10(a,1)),rewrite(56(4)),flip(a)]. given #223 (T,wt=11): 878 ((x v y) ^ z) v (y ^ z)' = 1. [para(87(a,1),195(a,1,2,1))]. given #224 (T,wt=11): 879 (x v y) ^ (z ^ y) = z ^ y. [para(56(a,1),87(a,2)),rewrite(213(4))]. given #225 (T,wt=11): 884 x ^ (y ^ (y ^ (z v x))') = 0. [para(168(a,1),87(a,1,2)),rewrite(96(2)),flip(a)]. given #226 (T,wt=11): 901 (x ^ (y v z)) v (x ^ z)' = 1. [para(92(a,1),195(a,1,2,1))]. given #227 (A,wt=19): 112 x ^ (y v (z ^ (x v (u ^ y)))) = x ^ (y v (z ^ x)). [para(24(a,1),12(a,1,2,2,2,2)),rewrite(74(5)),flip(a)]. given #228 (T,wt=11): 905 x ^ (y ^ (x ^ (z v y))') = 0. [para(92(a,1),297(a,1,2)),rewrite(4(5),5(5))]. given #229 (T,wt=11): 927 ((x ^ y) v z) ^ (y v z)' = 0. [para(108(a,1),141(a,1,2,1))]. given #230 (T,wt=11): 928 x v (y v ((z ^ x) v y)') = 1. [para(29(a,1),108(a,1,2)),rewrite(93(2)),flip(a)]. given #231 (T,wt=11): 930 (x ^ y) v (z v y) = z v y. [para(62(a,1),108(a,2)),rewrite(227(4))]. given #232 (A,wt=13): 114 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(17(a,1),24(a,1,2))]. given #233 (T,wt=11): 937 x v (y v (y v (z ^ x))') = 1. [para(162(a,1),108(a,1,2)),rewrite(93(2)),flip(a)]. given #234 (T,wt=11): 1012 (x v (y ^ z)) ^ (x v z)' = 0. [para(113(a,1),141(a,1,2,1))]. given #235 (T,wt=11): 1015 x v (y v (x v (z ^ y))') = 1. [para(113(a,1),296(a,1,2)),rewrite(2(5),3(5))]. given #236 (T,wt=11): 1051 x v (y v (z v (y v x)')) = 1. [para(2(a,1),132(a,1,2,2,2,1))]. given #237 (A,wt=21): 116 x v (y v z) != 1 | x v y != 0 | (x v y)' = x v (y v z). [back_rewrite(103),rewrite(115(4))]. given #238 (T,wt=11): 1089 x ^ (y ^ (z ^ (y ^ x)')) = 0. [para(4(a,1),136(a,1,2,2,2,1))]. given #239 (T,wt=11): 1098 (x v y) ^ (y v (x v z))' = 0. [para(2(a,1),142(a,1,1))]. given #240 (T,wt=11): 1099 (x v y) ^ (y v (z v x))' = 0. [para(2(a,1),142(a,1,2,1)),rewrite(3(3))]. given #241 (T,wt=11): 1108 (x v y) ^ ((y v x)' ^ z) = 0. [para(1103(a,1),5(a,1,1)),rewrite(83(2)),flip(a)]. given #242 (A,wt=12): 118 x ^ (x' v y) != 0 | x' v y = x'. [para(81(a,1),10(a,1)),flip(c),xx(a)]. given #243 (T,wt=11): 1110 (x v y) ^ (z ^ (y v x)') = 0. [para(1103(a,1),17(a,1,2)),rewrite(96(2)),flip(a)]. given #244 (T,wt=11): 1113 x ^ (y ^ ((y ^ x) v z)') = 0. [para(4(a,1),143(a,1,2,2,1,1))]. given #245 (T,wt=11): 1163 x ^ (y ^ (z v (y ^ x))') = 0. [para(4(a,1),157(a,1,2,2,1,2))]. given #246 (T,wt=11): 1170 (x v y) ^ (z v (y v x))' = 0. [para(2(a,1),160(a,1,2,1)),rewrite(3(3))]. given #247 (A,wt=17): 119 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z). [para(81(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #248 (T,wt=11): 1290 x ^ (y ^ ((y v z) ^ x)') = 0. [para(174(a,1),17(a,1)),flip(a)]. given #249 (T,wt=11): 1292 x ^ ((x v y) ^ (x v z))' = 0. [para(174(a,1),20(a,1)),flip(a)]. given #250 (T,wt=11): 1297 x ^ ((x v y) ^ (z v x))' = 0. [para(174(a,1),87(a,1)),flip(a)]. given #251 (T,wt=11): 1397 (x v (y ^ z)) ^ (y v x)' = 0. [para(2(a,1),192(a,1,1))]. given #252 (A,wt=17): 121 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(20(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #253 (T,wt=11): 1398 ((x ^ y) v z) ^ (z v x)' = 0. [para(2(a,1),192(a,1,2,1))]. given #254 (T,wt=11): 1400 (x v y)' ^ ((x ^ z) v y) = 0. [para(192(a,1),4(a,1)),flip(a)]. given #255 (T,wt=11): 1402 ((x ^ y) v (x ^ z)) ^ x' = 0. [para(7(a,1),192(a,1,2,1))]. given #256 (T,wt=11): 1407 ((x ^ y) v (z ^ x)) ^ x' = 0. [para(24(a,1),192(a,1,2,1))]. given #257 (A,wt=21): 123 x v ((x v y) ^ z) != 1 | x ^ z != 0 | x' = (x v y) ^ z. [para(20(a,1),10(b,1))]. given #258 (T,wt=11): 1426 x v (y v ((y ^ z) v x)') = 1. [para(193(a,1),15(a,1)),flip(a)]. given #259 (T,wt=11): 1429 x v ((x ^ y) v (x ^ z))' = 1. [para(193(a,1),22(a,1)),flip(a)]. given #260 (T,wt=11): 1436 x v ((x ^ y) v (z ^ x))' = 1. [para(193(a,1),108(a,1)),flip(a)]. given #261 (T,wt=11): 1442 x v (y v ((y v x) ^ z)') = 1. [para(2(a,1),194(a,1,2,2,1,1))]. given #262 (A,wt=13): 124 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(15(a,1),20(a,1,2,1))]. given #263 (T,wt=11): 1456 (x ^ y) v (y ^ (x ^ z))' = 1. [para(4(a,1),196(a,1,1))]. given #264 (T,wt=11): 1457 (x ^ y) v (y ^ (z ^ x))' = 1. [para(4(a,1),196(a,1,2,1)),rewrite(5(3))]. given #265 (T,wt=11): 1491 (x ^ y) v ((y ^ x)' v z) = 1. [para(1462(a,1),3(a,1,1)),rewrite(80(2)),flip(a)]. given #266 (T,wt=11): 1495 (x ^ y) v (z v (y ^ x)') = 1. [para(1462(a,1),15(a,1,2)),rewrite(93(2)),flip(a)]. given #267 (A,wt=15): 125 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(20(a,1),17(a,1,2)),flip(a)]. given #268 (T,wt=11): 1507 x v (y v (z ^ (y v x))') = 1. [para(2(a,1),201(a,1,2,2,1,2))]. given #269 (T,wt=11): 1521 (x ^ y) v (z ^ (y ^ x))' = 1. [para(4(a,1),207(a,1,2,1)),rewrite(5(3))]. given #270 (T,wt=11): 1551 (x ^ y)' v ((x v z) ^ y) = 1. [para(208(a,1),2(a,1)),flip(a)]. given #271 (T,wt=11): 1553 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),208(a,1,1))]. given #272 (A,wt=15): 126 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(20(a,1),24(a,1,2)),rewrite(2(4))]. given #273 (T,wt=11): 1554 ((x v y) ^ z) v (z ^ x)' = 1. [para(4(a,1),208(a,1,2,1))]. given #274 (T,wt=11): 1556 ((x v y) ^ (x v z)) v x' = 1. [para(6(a,1),208(a,1,2,1))]. given #275 (T,wt=11): 1562 ((x v y) ^ (z v x)) v x' = 1. [para(18(a,1),208(a,1,2,1))]. given #276 (T,wt=11): 1654 (x v y)' ^ (z ^ (y v x)) = 0. [para(229(a,1),306(a,1,2,2))]. given #277 (A,wt=12): 128 x v (x' ^ y) != 1 | x' ^ y = x'. [para(85(a,1),10(b,1)),flip(c),xx(b)]. given #278 (T,wt=11): 1656 (x v y)' v (z v (y v x)) = 1. [para(229(a,1),647(a,1,1,1))]. given #279 (T,wt=11): 1751 (x ^ y)' v (z v (y ^ x)) = 1. [para(244(a,1),300(a,1,2,2))]. given #280 (T,wt=11): 1753 (x ^ y)' ^ (z ^ (y ^ x)) = 0. [para(244(a,1),664(a,1,1,1))]. given #281 (T,wt=11): 1884 x v ((y v x)' v (z v y)) = 1. [para(2(a,1),303(a,1,2,1,1))]. given #282 (A,wt=23): 129 x ^ (y v (x' ^ (z ^ (y v u)))) = x ^ (y v (x' ^ (z ^ (x v u)))). [para(85(a,1),12(a,1,2,2,1)),rewrite(5(5),69(6),5(10))]. given #283 (T,wt=11): 1926 x ^ ((y ^ x)' ^ (z ^ y)) = 0. [para(4(a,1),310(a,1,2,1,1))]. given #284 (T,wt=11): 2224 x v (y v ((z ^ y) v x)') = 1. [para(108(a,1),428(a,1,2))]. given #285 (T,wt=11): 2247 x v ((y ^ x) v (x ^ z))' = 1. [para(430(a,1),108(a,1)),flip(a)]. given #286 (T,wt=11): 2315 x ^ (y ^ ((z v y) ^ x)') = 0. [para(87(a,1),484(a,1,2))]. given #287 (A,wt=12): 134 x ^ (y v x') != 0 | y v x' = x'. [para(95(a,1),10(a,1)),flip(c),xx(a)]. given #288 (T,wt=11): 2340 x ^ ((y v x) ^ (x v z))' = 0. [para(486(a,1),87(a,1)),flip(a)]. given #289 (T,wt=11): 3150 (x v y)' ^ (x v (y ^ z)) = 0. [para(816(a,1),4(a,1)),flip(a)]. given #290 (T,wt=11): 3236 (x ^ y)' v (x ^ (y v z)) = 1. [para(859(a,1),2(a,1)),flip(a)]. given #291 (T,wt=11): 3294 x ^ ((y v x) ^ (z v x))' = 0. [para(876(a,1),87(a,1)),flip(a)]. given #292 (A,wt=17): 135 x ^ (y v (z ^ (x v (u v y')))) = x ^ (y v z). [para(95(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #293 (T,wt=11): 3318 (x ^ y)' v ((z v x) ^ y) = 1. [para(878(a,1),2(a,1)),flip(a)]. given #294 (T,wt=11): 3320 (x ^ (y v z)) v (z ^ x)' = 1. [para(4(a,1),878(a,1,1))]. given #295 (T,wt=11): 3321 ((x v y) ^ z) v (z ^ y)' = 1. [para(4(a,1),878(a,1,2,1))]. given #296 (T,wt=11): 3323 ((x v y) ^ (y v z)) v y' = 1. [para(6(a,1),878(a,1,2,1))]. given #297 (A,wt=12): 138 x v (y ^ x') != 1 | y ^ x' = x'. [para(97(a,1),10(b,1)),flip(c),xx(b)]. given #298 (T,wt=11): 3329 ((x v y) ^ (z v y)) v y' = 1. [para(18(a,1),878(a,1,2,1))]. given #299 (T,wt=11): 3435 (x ^ y)' v (x ^ (z v y)) = 1. [para(901(a,1),2(a,1)),flip(a)]. given #300 (T,wt=11): 3542 (x v (y ^ z)) ^ (z v x)' = 0. [para(2(a,1),927(a,1,1))]. given #301 (T,wt=11): 3543 ((x ^ y) v z) ^ (z v y)' = 0. [para(2(a,1),927(a,1,2,1))]. given #302 (A,wt=23): 139 x ^ (y v (z ^ (x' ^ (y v u)))) = x ^ (y v (z ^ (x' ^ (x v u)))). [para(97(a,1),12(a,1,2,2,1)),rewrite(5(5),69(6),5(10))]. given #303 (T,wt=11): 3544 (x v y)' ^ ((z ^ x) v y) = 0. [para(927(a,1),4(a,1)),flip(a)]. given #304 (T,wt=11): 3546 ((x ^ y) v (y ^ z)) ^ y' = 0. [para(7(a,1),927(a,1,2,1))]. given #305 (T,wt=11): 3551 ((x ^ y) v (z ^ y)) ^ y' = 0. [para(24(a,1),927(a,1,2,1))]. given #306 (T,wt=11): 3613 x v ((y ^ x) v (z ^ x))' = 1. [para(928(a,1),108(a,1)),flip(a)]. given #307 (A,wt=12): 144 x v (x v y)' != 1 | (x v y)' = x'. [para(122(a,1),10(b,1)),flip(c),xx(b)]. given #308 (T,wt=11): 3760 (x v y)' ^ (x v (z ^ y)) = 0. [para(1012(a,1),4(a,1)),flip(a)]. given #309 (T,wt=11): 4133 (x v y)' ^ (y v (x ^ z)) = 0. [para(1397(a,1),4(a,1)),flip(a)]. given #310 (T,wt=11): 4272 (x v y)' ^ ((y ^ z) v x) = 0. [para(1398(a,1),4(a,1)),flip(a)]. given #311 (T,wt=11): 4292 x' ^ ((x ^ y) v (x ^ z)) = 0. [para(7(a,1),1400(a,1,1,1))]. given #312 (A,wt=23): 145 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))). [para(122(a,1),12(a,1,2,2,1)),rewrite(69(6))]. given #313 (T,wt=11): 4297 x' ^ ((x ^ y) v (z ^ x)) = 0. [para(24(a,1),1400(a,1,1,1))]. given #314 (T,wt=11): 4328 x ^ ((x' ^ y) v (x' ^ z)) = 0. [para(279(a,1),1402(a,1,2)),rewrite(4(6))]. given #315 (T,wt=11): 4350 x ^ ((x' ^ y) v (z ^ x')) = 0. [para(279(a,1),1407(a,1,2)),rewrite(4(6))]. given #316 (T,wt=11): 4788 (x ^ y)' v ((y v z) ^ x) = 1. [para(4(a,1),1551(a,1,1,1))]. given #317 (A,wt=13): 147 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),21(a,1,2,2,1))]. given #318 (T,wt=11): 4789 (x ^ y)' v (y ^ (x v z)) = 1. [para(4(a,1),1551(a,1,2))]. given #319 (T,wt=11): 4791 x' v ((x v y) ^ (x v z)) = 1. [para(6(a,1),1551(a,1,1,1))]. given #320 (T,wt=11): 4795 x' v ((x v y) ^ (z v x)) = 1. [para(18(a,1),1551(a,1,1,1))]. given #321 (T,wt=11): 4976 x v ((x' v y) ^ (x' v z)) = 1. [para(279(a,1),1556(a,1,2)),rewrite(2(6))]. given #322 (A,wt=19): 148 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(21(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #323 (T,wt=11): 5002 x v ((x' v y) ^ (z v x')) = 1. [para(279(a,1),1562(a,1,2)),rewrite(2(6))]. given #324 (T,wt=11): 5621 (x ^ y)' v ((z v y) ^ x) = 1. [para(4(a,1),3318(a,1,1,1))]. given #325 (T,wt=11): 5622 (x ^ y)' v (y ^ (z v x)) = 1. [para(4(a,1),3318(a,1,2))]. given #326 (T,wt=11): 5624 x' v ((y v x) ^ (x v z)) = 1. [para(6(a,1),3318(a,1,1,1))]. given #327 (A,wt=25): 149 x v (y ^ ((x ^ y) v z)) != 1 | x ^ y != 0 | x' = y ^ ((x ^ y) v z). [para(21(a,1),10(b,1))]. given #328 (T,wt=11): 5628 x' v ((y v x) ^ (z v x)) = 1. [para(18(a,1),3318(a,1,1,1))]. given #329 (T,wt=11): 5772 x v ((y v x') ^ (x' v z)) = 1. [para(279(a,1),3323(a,1,2)),rewrite(2(6))]. given #330 (T,wt=11): 5796 x v ((y v x') ^ (z v x')) = 1. [para(279(a,1),3329(a,1,2)),rewrite(2(6))]. given #331 (T,wt=11): 5853 (x v y)' ^ (y v (z ^ x)) = 0. [para(3542(a,1),4(a,1)),flip(a)]. given #332 (A,wt=15): 150 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(15(a,1),21(a,1,2,2))]. given #333 (T,wt=11): 5913 (x v y)' ^ ((z ^ y) v x) = 0. [para(3543(a,1),4(a,1)),flip(a)]. given #334 (T,wt=11): 6131 x' ^ ((y ^ x) v (x ^ z)) = 0. [para(7(a,1),3544(a,1,1,1))]. given #335 (T,wt=11): 6136 x' ^ ((y ^ x) v (z ^ x)) = 0. [para(24(a,1),3544(a,1,1,1))]. given #336 (T,wt=11): 6170 x ^ ((y ^ x') v (x' ^ z)) = 0. [para(279(a,1),3546(a,1,2)),rewrite(4(6))]. given #337 (A,wt=17): 151 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(21(a,1),17(a,1,2)),flip(a)]. given #338 (T,wt=11): 6190 x ^ ((y ^ x') v (z ^ x')) = 0. [para(279(a,1),3551(a,1,2)),rewrite(4(6))]. given #339 (T,wt=12): 158 x v (y v x)' != 1 | (y v x)' = x'. [para(141(a,1),10(b,1)),flip(c),xx(b)]. given #340 (T,wt=12): 197 x ^ (x ^ y)' != 0 | (x ^ y)' = x'. [para(184(a,1),10(a,1)),flip(c),xx(a)]. given #341 (T,wt=12): 203 x ^ (y ^ x)' != 0 | (y ^ x)' = x'. [para(195(a,1),10(a,1)),flip(c),xx(a)]. given #342 (A,wt=19): 152 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(17(a,1),21(a,1,2,2,1)),rewrite(5(5))]. given #343 (T,wt=12): 283 x ^ (x' v y) != 0 | (x' v y)' = x. [para(81(a,1),34(a,1)),rewrite(4(6)),xx(a)]. given #344 (T,wt=12): 284 x ^ (y v x') != 0 | (y v x')' = x. [para(95(a,1),34(a,1)),rewrite(4(6)),xx(a)]. given #345 (T,wt=12): 287 x ^ (x ^ y)' != 0 | x ^ y = x. [para(184(a,1),34(a,1)),rewrite(4(6),279(11)),xx(a)]. given #346 (T,wt=12): 288 x ^ (y ^ x)' != 0 | y ^ x = x. [para(195(a,1),34(a,1)),rewrite(4(6),279(11)),xx(a)]. given #347 (A,wt=19): 153 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(21(a,1),24(a,1,2)),rewrite(2(5))]. given #348 (T,wt=12): 301 x' ^ (y v x) != 0 | y v x = x. [para(296(a,1),10(a,1)),rewrite(279(10)),flip(c),xx(a)]. given #349 (T,wt=12): 305 (x v y) ^ y' != 0 | (x v y)' = y'. [para(296(a,1),34(a,1)),xx(a)]. given #350 (T,wt=12): 307 x' v (y ^ x) != 1 | y ^ x = x. [para(297(a,1),10(b,1)),rewrite(279(10)),flip(c),xx(b)]. given #351 (T,wt=12): 312 (x ^ y) v y' != 1 | x ^ y = y. [para(297(a,1),34(b,1)),rewrite(279(10)),flip(c),xx(b)]. given #352 (A,wt=15): 154 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(21(a,1),20(a,1,2)),rewrite(20(3)),flip(a)]. given #353 (T,wt=12): 334 (x v y) ^ x' != 0 | (x v y)' = x'. [para(95(a,1),35(a,1)),xx(a)]. given #354 (T,wt=12): 382 x v (x' ^ y) != 1 | (x' ^ y)' = x. [para(85(a,1),36(b,1)),rewrite(2(3)),xx(b)]. given #355 (T,wt=12): 383 x v (y ^ x') != 1 | (y ^ x')' = x. [para(97(a,1),36(b,1)),rewrite(2(3)),xx(b)]. given #356 (T,wt=12): 384 x v (x v y)' != 1 | x v y = x. [para(122(a,1),36(b,1)),rewrite(2(3),279(11)),xx(b)]. given #357 (A,wt=23): 159 x ^ (y v ((z v x)' ^ (y v u))) = x ^ (y v ((z v x)' ^ (x v u))). [para(141(a,1),12(a,1,2,2,1)),rewrite(69(6))]. given #358 (T,wt=12): 386 x v (y v x)' != 1 | y v x = x. [para(141(a,1),36(b,1)),rewrite(2(3),279(11)),xx(b)]. given #359 (T,wt=12): 391 (x v y) ^ y' != 0 | x v y = y. [para(296(a,1),36(a,1)),rewrite(279(10)),flip(c),xx(a)]. given #360 (T,wt=12): 392 (x ^ y) v y' != 1 | (x ^ y)' = y'. [para(297(a,1),36(b,1)),xx(b)]. given #361 (T,wt=12): 450 (x ^ y) v x' != 1 | (x ^ y)' = x'. [para(97(a,1),37(b,1)),xx(b)]. given #362 (A,wt=13): 163 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 #363 (T,wt=12): 834 x' ^ (x v y) != 0 | x v y = x. [para(81(a,1),51(a,1)),rewrite(279(10)),flip(c),xx(a)]. given #364 (T,wt=12): 1589 x' v (x ^ y) != 1 | x ^ y = x. [para(85(a,1),78(b,1)),rewrite(279(10)),flip(c),xx(b)]. given #365 (T,wt=12): 3930 x ^ (y v x') != 0 | x' v y = x'. [para(2(a,1),118(a,1,2))]. given #366 (T,wt=12): 5031 x v (y ^ x') != 1 | x' ^ y = x'. [para(4(a,1),128(a,1,2))]. given #367 (A,wt=16): 164 x ^ (y v (x v y)') != 0 | y v (x v y)' = x'. [para(29(a,1),10(a,1)),flip(c),xx(a)]. given #368 (T,wt=12): 5428 x ^ (x' v y) != 0 | y v x' = x'. [para(2(a,1),134(a,1,2))]. given #369 (T,wt=12): 5782 x v (x' ^ y) != 1 | y ^ x' = x'. [para(4(a,1),138(a,1,2))]. given #370 (T,wt=12): 6267 x v (y v x)' != 1 | (x v y)' = x'. [para(2(a,1),144(a,1,2,1))]. given #371 (T,wt=12): 7402 x v (x v y)' != 1 | (y v x)' = x'. [para(2(a,1),158(a,1,2,1))]. given #372 (A,wt=19): 165 x ^ (y v (z ^ (x v (u v (y v u)')))) = x ^ (y v z). [para(29(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #373 (T,wt=12): 7408 x ^ (y ^ x)' != 0 | (x ^ y)' = x'. [para(4(a,1),197(a,1,2,1))]. given #374 (T,wt=12): 7412 x ^ (x ^ y)' != 0 | (y ^ x)' = x'. [para(4(a,1),203(a,1,2,1))]. given #375 (T,wt=12): 7511 x ^ (y v x') != 0 | (x' v y)' = x. [para(2(a,1),283(a,1,2))]. given #376 (T,wt=12): 7515 x' ^ (x v y) != 0 | (x v y)' = x'. [para(279(a,1),283(a,1,2,1)),rewrite(279(7))]. given #377 (A,wt=13): 167 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 #378 (T,wt=12): 7529 x ^ (x' v y) != 0 | (y v x')' = x. [para(2(a,1),284(a,1,2))]. given #379 (T,wt=12): 7531 x' ^ (y v x) != 0 | (y v x)' = x'. [para(279(a,1),284(a,1,2,2)),rewrite(279(7))]. given #380 (T,wt=12): 7532 x ^ (y ^ x)' != 0 | x ^ y = x. [para(4(a,1),287(a,1,2,1))]. given #381 (T,wt=12): 7537 x ^ (x ^ y)' != 0 | y ^ x = x. [para(4(a,1),288(a,1,2,1))]. given #382 (A,wt=13): 169 x ^ (y ^ (z ^ (x ^ (y ^ z))')) = 0. [para(32(a,1),5(a,1)),rewrite(5(3)),flip(a)]. given #383 (T,wt=12): 7539 (x v y) ^ x' != 0 | x v y = x. [para(6(a,1),288(a,1,2,1)),rewrite(6(7)),flip(b)]. given #384 (T,wt=12): 7601 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),301(a,1,2))]. given #385 (T,wt=12): 7610 (x v y) ^ x' != 0 | (y v x)' = x'. [para(2(a,1),305(a,1,1))]. given #386 (T,wt=12): 7614 x' v (x ^ y) != 1 | y ^ x = x. [para(4(a,1),307(a,1,2))]. given #387 (A,wt=16): 170 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(32(a,1),10(b,1)),flip(c),xx(b)]. given #388 (T,wt=12): 7628 (x ^ y) v x' != 1 | y ^ x = x. [para(4(a,1),312(a,1,1))]. given #389 (T,wt=12): 7713 (x v y) ^ y' != 0 | (y v x)' = y'. [para(2(a,1),334(a,1,1))]. given #390 (T,wt=12): 7716 x v (y ^ x') != 1 | (x' ^ y)' = x. [para(4(a,1),382(a,1,2))]. given #391 (T,wt=12): 7718 x' v (x ^ y) != 1 | (x ^ y)' = x'. [para(279(a,1),382(a,1,2,1)),rewrite(279(7))]. given #392 (A,wt=25): 171 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ (x ^ (y v (z ^ (x v u))))') = 0. [para(12(a,1),32(a,1,2,2,1))]. given #393 (T,wt=12): 7722 x v (x' ^ y) != 1 | (y ^ x')' = x. [para(4(a,1),383(a,1,2))]. given #394 (T,wt=12): 7723 x' v (y ^ x) != 1 | (y ^ x)' = x'. [para(279(a,1),383(a,1,2,2)),rewrite(279(7))]. given #395 (T,wt=12): 7724 x v (y v x)' != 1 | x v y = x. [para(2(a,1),384(a,1,2,1))]. given #396 (T,wt=12): 7842 x v (x v y)' != 1 | y v x = x. [para(2(a,1),386(a,1,2,1))]. given #397 (A,wt=13): 173 x ^ (y ^ (z ^ (y ^ (x ^ z))')) = 0. [para(17(a,1),32(a,1,2,2,1)),rewrite(5(5))]. given #398 (T,wt=12): 7844 (x ^ y) v x' != 1 | x ^ y = x. [para(7(a,1),386(a,1,2,1)),rewrite(7(7)),flip(b)]. given #399 (T,wt=12): 7850 (x v y) ^ x' != 0 | y v x = x. [para(2(a,1),391(a,1,1))]. given #400 (T,wt=12): 7852 (x ^ y) v x' != 1 | (y ^ x)' = x'. [para(4(a,1),392(a,1,1))]. given #401 (T,wt=12): 7860 (x ^ y) v y' != 1 | (y ^ x)' = y'. [para(4(a,1),450(a,1,1))]. given #402 (A,wt=15): 175 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),48(a,1,2,2))]. given #403 (T,wt=12): 7871 x' ^ (y v x) != 0 | x v y = x. [para(2(a,1),834(a,1,2))]. given #404 (T,wt=12): 7888 x' v (y ^ x) != 1 | x ^ y = x. [para(4(a,1),1589(a,1,2))]. given #405 (T,wt=12): 7998 x' ^ (y v x) != 0 | (x v y)' = x'. [para(279(a,1),7511(a,1,2,2)),rewrite(279(7))]. given #406 (T,wt=12): 8025 x' ^ (x v y) != 0 | (y v x)' = x'. [para(279(a,1),7529(a,1,2,1)),rewrite(279(7))]. given #407 (A,wt=15): 178 x ^ (y v ((z v (x v u)) ^ (x v v))) = x. [para(48(a,1),12(a,1,2,2,1)),rewrite(48(7)),flip(a)]. given #408 (T,wt=12): 8052 (x v y) ^ y' != 0 | y v x = y. [para(2(a,1),7539(a,1,1))]. given #409 (T,wt=12): 8068 x' v (y ^ x) != 1 | (x ^ y)' = x'. [para(279(a,1),7716(a,1,2,2)),rewrite(279(7))]. given #410 (T,wt=12): 8123 x' v (x ^ y) != 1 | (y ^ x)' = x'. [para(279(a,1),7722(a,1,2,1)),rewrite(279(7))]. given #411 (T,wt=12): 8160 (x ^ y) v y' != 1 | y ^ x = y. [para(4(a,1),7844(a,1,1))]. given #412 (A,wt=13): 179 x ^ (y ^ (z v (x v u))) = y ^ x. [para(48(a,1),17(a,1,2)),flip(a)]. given #413 (T,wt=13): 180 x v (y v (x v z)) = y v (x v z). [para(48(a,1),24(a,1,2)),rewrite(2(3))]. given #414 (T,wt=13): 188 x v ((y ^ (x ^ z)) v u) = x v u. [para(17(a,1),22(a,1,2,1))]. given #415 (T,wt=13): 209 (x ^ ((y ^ x) v z)) v (y ^ x)' = 1. [para(21(a,1),195(a,1,2,1))]. given #416 (T,wt=13): 211 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(54(a,1),5(a,2,2)),rewrite(17(3),5(2))]. given #417 (A,wt=17): 181 x v (y v z) != 1 | 0 != y | y' = x v (y v z). [back_rewrite(177),rewrite(180(3))]. given #418 (T,wt=13): 213 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),56(a,1,2)),rewrite(5(5))]. given #419 (T,wt=13): 215 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),23(a,1,2,2,1))]. given #420 (T,wt=13): 223 (x v ((y v x) ^ z)) ^ (y v x)' = 0. [para(23(a,1),141(a,1,2,1))]. given #421 (T,wt=13): 227 x v (y v (z v x)) = y v (z v x). [para(3(a,1),62(a,1,2)),rewrite(3(5))]. given #422 (A,wt=17): 182 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 #423 (T,wt=13): 235 x v (y v (z ^ (x ^ u))) = y v x. [para(76(a,1),15(a,1,2)),flip(a)]. given #424 (T,wt=13): 236 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),25(a,1,1))]. given #425 (T,wt=13): 237 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),25(a,1,2)),rewrite(5(3))]. given #426 (T,wt=13): 246 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(86(a,1),5(a,1,1)),flip(a)]. given #427 (A,wt=17): 183 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),22(a,1,2,1))]. given #428 (T,wt=13): 252 x ^ (y ^ (z v (u v x))) = y ^ x. [para(86(a,1),17(a,1,2)),flip(a)]. given #429 (T,wt=13): 256 x v ((y ^ (z ^ x)) v u) = x v u. [para(110(a,1),3(a,1,1)),flip(a)]. given #430 (T,wt=13): 261 x v (y v (z ^ (u ^ x))) = y v x. [para(110(a,1),15(a,1,2)),flip(a)]. given #431 (T,wt=13): 266 x v (y v (z v ((x v y)' v u))) = 1. [para(120(a,1),3(a,1)),flip(a)]. given #432 (A,wt=21): 185 x v y != 1 | x ^ ((x ^ z) v y) != 0 | x' = (x ^ z) v y. [para(22(a,1),10(a,1))]. given #433 (T,wt=13): 271 x ^ (y ^ (z ^ ((x ^ y)' ^ u))) = 0. [para(130(a,1),5(a,1)),flip(a)]. given #434 (T,wt=13): 276 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),34(b,1))]. given #435 (T,wt=13): 278 1 != x | x ^ y != 0 | (x ^ y)' = x. [para(7(a,1),34(a,1)),rewrite(4(4),54(4)),flip(a)]. given #436 (T,wt=13): 282 1 != x | y ^ x != 0 | (y ^ x)' = x. [para(24(a,1),34(a,1)),rewrite(4(4),56(4)),flip(a)]. given #437 (A,wt=23): 186 x ^ (y v (z ^ (x v ((y ^ u) v v)))) = x ^ (y v (z ^ (x v v))). [para(22(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)]. given #438 (T,wt=13): 290 x v y != 1 | 0 != x | (x v y)' = x. [para(60(a,1),34(a,1)),rewrite(4(5),6(5)),flip(b)]. given #439 (T,wt=13): 291 x v y != 1 | 0 != y | (x v y)' = y. [para(62(a,1),34(a,1)),rewrite(4(5),18(5)),flip(b)]. given #440 (T,wt=13): 304 x v (y v (y v ((x v y) ^ z))') = 1. [para(23(a,1),296(a,1,2)),rewrite(2(6),3(6))]. given #441 (T,wt=13): 311 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(21(a,1),297(a,1,2)),rewrite(4(6),5(6))]. given #442 (A,wt=15): 187 x v (y v ((x ^ z) v u)) = y v (x v u). [para(22(a,1),15(a,1,2)),flip(a)]. given #443 (T,wt=13): 313 (x v y) ^ ((x v (y v z))' ^ u) = 0. [para(3(a,1),131(a,1,2,1,1))]. given #444 (T,wt=13): 314 x ^ (y ^ (((x ^ y) v z)' ^ u)) = 0. [para(131(a,1),5(a,1)),flip(a)]. given #445 (T,wt=13): 346 x v y != 1 | 0 != y | (y v x)' = y. [para(62(a,1),35(a,1)),rewrite(4(5),6(5)),flip(b)]. given #446 (T,wt=13): 354 x v (y v (z v (u v (x v y)'))) = 1. [para(133(a,1),3(a,1)),flip(a)]. given #447 (A,wt=15): 189 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(22(a,1),18(a,1,2)),rewrite(4(4))]. given #448 (T,wt=13): 362 x ^ (y ^ (z ^ (u ^ (x ^ y)'))) = 0. [para(137(a,1),5(a,1)),flip(a)]. given #449 (T,wt=13): 367 (x v y) ^ (z ^ (x v (y v u))') = 0. [para(3(a,1),140(a,1,2,2,1))]. given #450 (T,wt=13): 368 x ^ (y ^ (z ^ ((x ^ y) v u)')) = 0. [para(140(a,1),5(a,1)),flip(a)]. given #451 (T,wt=13): 372 (x v y) ^ (z v (x v (y v u)))' = 0. [para(3(a,1),146(a,1,2,1,2))]. given #452 (A,wt=17): 198 x ^ (y v (z ^ (x v (y ^ u)'))) = x ^ (y v z). [para(184(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #453 (T,wt=13): 374 x ^ (y ^ (z v ((x ^ y) v u))') = 0. [para(146(a,1),5(a,1)),flip(a)]. given #454 (T,wt=13): 399 x ^ (y ^ (z v (u v (x ^ y)))') = 0. [para(155(a,1),5(a,1)),flip(a)]. given #455 (T,wt=13): 401 (x v y) ^ (z v (x v (u v y)))' = 0. [para(15(a,1),155(a,1,2,1,2))]. given #456 (T,wt=13): 403 ((x ^ y) v z) ^ (u v (x v z))' = 0. [para(22(a,1),155(a,1,2,1,2))]. given #457 (A,wt=17): 204 x ^ (y v (z ^ (x v (u ^ y)'))) = x ^ (y v z). [para(195(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #458 (T,wt=13): 405 x ^ (y ^ (z ^ (u v (x ^ y))')) = 0. [para(25(a,1),155(a,1,2,1,2)),rewrite(5(6),5(5))]. given #459 (T,wt=13): 408 x ^ (y ^ ((z v (x ^ y))' ^ u)) = 0. [para(156(a,1),5(a,1)),flip(a)]. given #460 (T,wt=13): 410 (x v y) ^ ((x v (z v y))' ^ u) = 0. [para(15(a,1),156(a,1,2,1,1))]. given #461 (T,wt=13): 412 ((x ^ y) v z) ^ ((x v z)' ^ u) = 0. [para(22(a,1),156(a,1,2,1,1))]. given #462 (A,wt=23): 205 x v ((y ^ z) v ((z ^ (x v u)) v (y ^ (x v (z ^ (y v u))))')) = 1. [para(12(a,1),195(a,1,2,1)),rewrite(3(11),3(10))]. given #463 (T,wt=13): 418 (x v y) ^ (z ^ (x v (u v y))') = 0. [para(15(a,1),161(a,1,2,2,1))]. given #464 (T,wt=13): 419 ((x ^ y) v z) ^ (u ^ (x v z)') = 0. [para(22(a,1),161(a,1,2,2,1))]. given #465 (T,wt=13): 424 x v (y v (z v (z v (x v y))')) = 1. [para(162(a,1),3(a,1)),flip(a)]. given #466 (T,wt=13): 425 x v (y v (z v (y v (z v x))')) = 1. [para(3(a,1),162(a,1,2,2,1)),rewrite(3(5))]. given #467 (A,wt=19): 216 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 #468 (T,wt=13): 429 x v (y v (z v (x v (z v y))')) = 1. [para(15(a,1),162(a,1,2,2,1)),rewrite(3(6))]. given #469 (T,wt=13): 461 1 != x | y ^ x != 0 | (x ^ y)' = x. [para(56(a,1),37(b,1)),rewrite(2(2),7(2)),flip(a)]. given #470 (T,wt=13): 481 x ^ (y ^ (z ^ (z ^ (x ^ y))')) = 0. [para(168(a,1),5(a,1)),flip(a)]. given #471 (T,wt=13): 482 x ^ (y ^ (z ^ (y ^ (z ^ x))')) = 0. [para(5(a,1),168(a,1,2,2,1)),rewrite(5(5))]. given #472 (A,wt=25): 217 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 #473 (T,wt=13): 485 x ^ (y ^ (z ^ (x ^ (z ^ y))')) = 0. [para(17(a,1),168(a,1,2,2,1)),rewrite(5(6))]. given #474 (T,wt=13): 490 x v (y v (((x v y) ^ z)' v u)) = 1. [para(190(a,1),3(a,1)),flip(a)]. given #475 (T,wt=13): 491 (x ^ y) v ((x ^ (y ^ z))' v u) = 1. [para(5(a,1),190(a,1,2,1,1))]. given #476 (T,wt=13): 498 x v (y v (z v ((x v y) ^ u)')) = 1. [para(191(a,1),3(a,1)),flip(a)]. given #477 (A,wt=25): 218 x ^ (y v (z ^ (x v (u v ((y v u) ^ v))))) = x ^ (y v (z ^ (x v u))). [para(23(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)]. given #478 (T,wt=13): 499 (x ^ y) v (z v (x ^ (y ^ u))') = 1. [para(5(a,1),191(a,1,2,2,1))]. Low Water (keep, True_semantics): wt=25 given #479 (T,wt=13): 507 x v (y v (z ^ ((x v y) ^ u))') = 1. [para(199(a,1),3(a,1)),flip(a)]. given #480 (T,wt=13): 508 (x ^ y) v (z ^ (x ^ (y ^ u)))' = 1. [para(5(a,1),199(a,1,2,1,2))]. given #481 (T,wt=13): 560 x v (y v ((z ^ (x v y))' v u)) = 1. [para(200(a,1),3(a,1)),flip(a)]. given #482 (A,wt=17): 219 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 #483 (T,wt=13): 566 (x ^ y) v ((x ^ (z ^ y))' v u) = 1. [para(17(a,1),200(a,1,2,1,1))]. given #484 (T,wt=13): 567 ((x v y) ^ z) v ((x ^ z)' v u) = 1. [para(20(a,1),200(a,1,2,1,1))]. given #485 (T,wt=13): 575 x v (y v (z ^ (u ^ (x v y)))') = 1. [para(202(a,1),3(a,1)),flip(a)]. given #486 (T,wt=13): 581 (x ^ y) v (z ^ (x ^ (u ^ y)))' = 1. [para(17(a,1),202(a,1,2,1,2))]. given #487 (A,wt=19): 220 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 #488 (T,wt=13): 582 x v (y v (z v (u ^ (x v y))')) = 1. [para(19(a,1),202(a,1,2,1,2)),rewrite(3(6),3(5))]. given #489 (T,wt=13): 583 ((x v y) ^ z) v (u ^ (x ^ z))' = 1. [para(20(a,1),202(a,1,2,1,2))]. given #490 (T,wt=13): 594 (x ^ y) v (z v (x ^ (u ^ y))') = 1. [para(17(a,1),206(a,1,2,2,1))]. given #491 (T,wt=13): 595 ((x v y) ^ z) v (u v (x ^ z)') = 1. [para(20(a,1),206(a,1,2,2,1))]. given #492 (A,wt=15): 221 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(17(a,1),23(a,1,2,2))]. given #493 (T,wt=13): 604 (x v y)' v (z v (x v (y v u))) = 1. [para(3(a,1),298(a,1,2,2))]. given #494 (T,wt=13): 617 x ^ ((y ^ z) v (x ^ y)) = y ^ x. [para(69(a,1),41(a,1,2,2,1,2)),rewrite(69(5),69(8),75(7))]. given #495 (T,wt=13): 635 (x ^ y)' ^ (z ^ (x ^ (y ^ u))) = 0. [para(5(a,1),299(a,1,2,2))]. given #496 (T,wt=13): 646 (x v y)' v (z v (x v (u v y))) = 1. [para(15(a,1),300(a,1,2,2))]. given #497 (A,wt=19): 222 (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 #498 (T,wt=13): 648 ((x ^ y) v z)' v (u v (x v z)) = 1. [para(22(a,1),300(a,1,2,2))]. given #499 (T,wt=13): 651 (x ^ (y ^ z))' v (u v (x ^ y)) = 1. [para(25(a,1),300(a,1,2,2))]. NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 130 (0.00 of 5.98 sec). given #500 (T,wt=13): 663 (x ^ y)' ^ (z ^ (x ^ (u ^ y))) = 0. [para(17(a,1),306(a,1,2,2))]. given #501 (T,wt=13): 665 (x v (y v z))' ^ (u ^ (x v y)) = 0. [para(19(a,1),306(a,1,2,2))]. given #502 (A,wt=15): 224 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 #503 (T,wt=13): 666 ((x v y) ^ z)' ^ (u ^ (x ^ z)) = 0. [para(20(a,1),306(a,1,2,2))]. given #504 (T,wt=13): 679 x v (((x v y) ^ z)' v (u v y)) = 1. [para(15(a,1),643(a,1,2)),rewrite(15(6))]. given #505 (T,wt=13): 680 x v (y v (((x ^ z) v y) ^ u)') = 1. [para(22(a,1),643(a,1,2)),rewrite(2(6),3(6))]. given #506 (T,wt=13): 689 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(69(a,1),42(a,1,2,2,2,2)),rewrite(69(5),69(8),75(7))]. given #507 (A,wt=21): 225 x ^ (y v (z ^ (x v (y v u)))) = x ^ (y v (z ^ (x v u))). [para(60(a,1),12(a,1,2,2,2,2)),rewrite(12(6)),flip(a)]. given #508 (T,wt=13): 712 x v ((y ^ (x v z))' v (u v z)) = 1. [para(15(a,1),647(a,1,2)),rewrite(15(6))]. given #509 (T,wt=13): 713 (x ^ (y ^ z))' v (u v (x ^ z)) = 1. [para(17(a,1),647(a,1,1,1))]. given #510 (T,wt=13): 714 (x ^ y)' v (z v ((x v u) ^ y)) = 1. [para(20(a,1),647(a,1,1,1))]. given #511 (T,wt=13): 716 x v (y v (z ^ ((x ^ u) v y))') = 1. [para(22(a,1),647(a,1,2)),rewrite(2(6),3(6))]. given #512 (A,wt=21): 228 x ^ (y v (z ^ (x v (u v y)))) = x ^ (y v (z ^ (x v u))). [para(62(a,1),12(a,1,2,2,2,2)),rewrite(40(6)),flip(a)]. given #513 (T,wt=13): 727 x ^ (((x ^ y) v z)' ^ (u ^ y)) = 0. [para(17(a,1),660(a,1,2)),rewrite(17(6))]. given #514 (T,wt=13): 728 x ^ (y ^ (((x v z) ^ y) v u)') = 0. [para(20(a,1),660(a,1,2)),rewrite(4(6),5(6))]. given #515 (T,wt=13): 738 (x v (y v z))' ^ (u ^ (x v z)) = 0. [para(15(a,1),664(a,1,1,1))]. given #516 (T,wt=13): 739 x ^ ((y v (x ^ z))' ^ (u ^ z)) = 0. [para(17(a,1),664(a,1,2)),rewrite(17(6))]. given #517 (A,wt=15): 231 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),76(a,1,2,2))]. given #518 (T,wt=13): 740 x ^ (y ^ (z v ((x v u) ^ y))') = 0. [para(20(a,1),664(a,1,2)),rewrite(4(6),5(6))]. given #519 (T,wt=13): 742 (x v y)' ^ (z ^ ((x ^ u) v y)) = 0. [para(22(a,1),664(a,1,1,1))]. given #520 (T,wt=13): 753 x ^ ((x ^ y) v (z ^ y)) = y ^ x. [para(69(a,1),43(a,1,2,2,2,1)),rewrite(69(5),69(8),75(7))]. given #521 (T,wt=13): 792 x' ^ (x v (y ^ x')) = x' ^ (x v y). [para(27(a,1),46(a,1,2,2,2))]. given #522 (A,wt=17): 233 1 != x | y ^ (x ^ z) != 0 | x' = y ^ (x ^ z). [para(76(a,1),10(a,1)),rewrite(211(5)),flip(a)]. given #523 (T,wt=9): 13234 x' ^ (x v (x' v y)') = 0. [para(145(a,1),792(a,2)),rewrite(4(8),131(8),33(3),4(2),9(2),4011(10)),flip(a)]. given #524 (T,wt=7): 13301 x v (x' v y)' = x. [hyper(7601,a,13234,a),rewrite(2(4))]. given #525 (T,wt=7): 13319 x v (y v x')' = x. [para(2(a,1),13301(a,1,2,1))]. given #526 (T,wt=7): 13330 x' v (x v y)' = x'. [para(279(a,1),13301(a,1,2,1,1))]. given #527 (A,wt=19): 238 (x ^ (y ^ z)) v (x ^ (y ^ (z ^ u))) = x ^ (y ^ z). [para(5(a,1),25(a,1,1)),rewrite(5(5),5(8))]. given #528 (T,wt=7): 13428 x' v (y v x)' = x'. [para(279(a,1),13319(a,1,2,1,2))]. given #529 (T,wt=9): 13325 x v (y v (x' v z))' = x. [para(15(a,1),13301(a,1,2,1))]. given #530 (T,wt=9): 13326 x ^ (x' v y)' = (x' v y)'. [para(13301(a,1),18(a,1,2)),rewrite(4(4))]. given #531 (T,wt=9): 13327 x v ((x ^ y)' v z)' = x. [para(13301(a,1),22(a,1,2)),rewrite(7(2)),flip(a)]. given #532 (A,wt=21): 239 x ^ y != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = x ^ (y ^ z). [para(25(a,1),10(a,1)),rewrite(17(7),17(6),5(5),211(6),54(6))]. given #533 (T,wt=9): 13333 (x' v y)' ^ (z v x)' = 0. [para(13301(a,1),155(a,1,2,1,2))]. given #534 (T,wt=9): 13334 x v ((x' v y)' ^ z)' = 1. [para(13301(a,1),643(a,1,2)),rewrite(2(6))]. Low Water (keep, True_semantics): wt=24 given #535 (T,wt=9): 13336 x v (y ^ (x' v z)')' = 1. [para(13301(a,1),647(a,1,2)),rewrite(2(6))]. given #536 (T,wt=9): 13340 x v ((y ^ x)' v z)' = x. [para(13301(a,1),108(a,1,2)),rewrite(24(2)),flip(a)]. given #537 (A,wt=17): 241 (x ^ y) v (z v (x ^ (y ^ u))) = z v (x ^ y). [para(25(a,1),15(a,1,2)),flip(a)]. given #538 (T,wt=9): 13345 x v ((x' v y)' ^ z) = x. [para(13301(a,1),230(a,1,2)),rewrite(2(5),13301(9))]. given #539 (T,wt=9): 13366 x v (y ^ (x' v z)') = x. [para(13301(a,1),930(a,1,2)),rewrite(2(5),13301(9))]. Low Water (keep, True_semantics): wt=23 given #540 (T,wt=9): 13389 x v (y v (z v x'))' = x. [para(227(a,1),13301(a,1,2,1))]. given #541 (T,wt=9): 13424 x ^ (y v x')' = (y v x')'. [para(13319(a,1),18(a,1,2)),rewrite(4(4))]. given #542 (A,wt=19): 242 (x ^ (y ^ z)) v (y ^ (x ^ (z ^ u))) = y ^ (x ^ z). [para(17(a,1),25(a,1,1)),rewrite(5(4))]. given #543 (T,wt=9): 13425 x v (y v (x ^ z)')' = x. [para(13319(a,1),22(a,1,2)),rewrite(7(2)),flip(a)]. given #544 (T,wt=9): 13431 (x v y')' ^ (z v y)' = 0. [para(13319(a,1),155(a,1,2,1,2))]. given #545 (T,wt=9): 13432 x v ((y v x')' ^ z)' = 1. [para(13319(a,1),643(a,1,2)),rewrite(2(6))]. given #546 (T,wt=9): 13434 x v (y ^ (z v x')')' = 1. [para(13319(a,1),647(a,1,2)),rewrite(2(6))]. given #547 (A,wt=15): 243 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(17(a,1),25(a,1,2,2))]. given #548 (T,wt=9): 13438 x v (y v (z ^ x)')' = x. [para(13319(a,1),108(a,1,2)),rewrite(24(2)),flip(a)]. given #549 (T,wt=9): 13444 x v ((y v x')' ^ z) = x. [para(13319(a,1),230(a,1,2)),rewrite(2(5),13319(9))]. given #550 (T,wt=9): 13465 x v (y ^ (z v x')') = x. [para(13319(a,1),930(a,1,2)),rewrite(2(5),13319(9))]. given #551 (T,wt=9): 13526 x' v (y v (x v z))' = x'. [para(15(a,1),13330(a,1,2,1))]. given #552 (A,wt=15): 247 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(86(a,1),5(a,1)),flip(a)]. given #553 (T,wt=9): 13527 x' ^ (x v y)' = (x v y)'. [para(13330(a,1),18(a,1,2)),rewrite(4(4))]. given #554 (T,wt=9): 13532 (x v y)' ^ (z v x')' = 0. [para(13330(a,1),155(a,1,2,1,2))]. given #555 (T,wt=9): 13533 x' v ((x v y)' ^ z)' = 1. [para(13330(a,1),643(a,1,2)),rewrite(2(6))]. given #556 (T,wt=9): 13535 x' v (y ^ (x v z)')' = 1. [para(13330(a,1),647(a,1,2)),rewrite(2(6))]. given #557 (A,wt=17): 248 x v (y v z) != 1 | 0 != z | z' = x v (y v z). [para(86(a,1),10(b,1)),rewrite(227(3)),flip(b)]. given #558 (T,wt=9): 13541 x' != 1 | x' != 0 | x' = x. [para(13330(a,1),65(a,1)),rewrite(279(8),13330(10)),flip(b),flip(c)]. given #559 (T,wt=9): 13545 x' v ((x v y)' ^ z) = x'. [para(13330(a,1),230(a,1,2)),rewrite(2(5),13330(9))]. given #560 (T,wt=9): 13567 x' v (y ^ (x v z)') = x'. [para(13330(a,1),930(a,1,2)),rewrite(2(5),13330(9))]. given #561 (T,wt=9): 13595 x' v (y v (z v x))' = x'. [para(227(a,1),13330(a,1,2,1))]. given #562 (A,wt=15): 249 x ^ (y v ((z v (u v x)) ^ (x v v))) = x. [para(86(a,1),12(a,1,2,2,1)),rewrite(48(7)),flip(a)]. given #563 (T,wt=9): 13677 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),13428(a,1,2,1)),rewrite(2(4))]. given #564 (T,wt=7): 15857 x' ^ (x ^ y)' = x'. [para(13677(a,1),6(a,1,2))]. given #565 (T,wt=7): 15960 x' ^ (y ^ x)' = x'. [para(4(a,1),15857(a,1,2,1))]. given #566 (T,wt=7): 15964 x ^ (x' ^ y)' = x. [para(279(a,1),15857(a,1,1)),rewrite(279(6))]. given #567 (A,wt=15): 251 (x v y) ^ (z v (x v (u v y))) = x v y. [para(15(a,1),86(a,1,2,2))]. given #568 (T,wt=7): 16012 x ^ (y ^ x')' = x. [para(279(a,1),15960(a,1,1)),rewrite(279(6))]. given #569 (T,wt=9): 13682 x' ^ (y v x)' = (y v x)'. [para(13428(a,1),18(a,1,2)),rewrite(4(4))]. given #570 (T,wt=9): 13683 x' v (y ^ x)' = (y ^ x)'. [para(24(a,1),13428(a,1,2,1)),rewrite(2(4))]. given #571 (T,wt=9): 13693 (x v y)' ^ (z v y')' = 0. [para(13428(a,1),155(a,1,2,1,2))]. given #572 (A,wt=17): 253 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(22(a,1),86(a,1,2,2))]. Low Water (keep, True_semantics): wt=21 given #573 (T,wt=9): 13694 x' v ((y v x)' ^ z)' = 1. [para(13428(a,1),643(a,1,2)),rewrite(2(6))]. given #574 (T,wt=9): 13696 x' v (y ^ (z v x)')' = 1. [para(13428(a,1),647(a,1,2)),rewrite(2(6))]. given #575 (T,wt=9): 13708 x' v ((y v x)' ^ z) = x'. [para(13428(a,1),230(a,1,2)),rewrite(2(5),13428(9))]. given #576 (T,wt=9): 13730 x' v (y ^ (z v x)') = x'. [para(13428(a,1),930(a,1,2)),rewrite(2(5),13428(9))]. given #577 (A,wt=21): 254 (x v ((y v x) ^ z)) ^ (u v (y v x)) = x v ((y v x) ^ z). [para(23(a,1),86(a,1,2,2))]. given #578 (T,wt=9): 13890 x ^ (y' v (x ^ y))' = 0. [para(13326(a,1),157(a,1,2))]. given #579 (T,wt=9): 13902 x ^ (y' v (y ^ x))' = 0. [para(13326(a,1),1163(a,1,2))]. given #580 (T,wt=9): 13961 x' ^ ((x ^ y)' v z)' = 0. [para(13327(a,1),141(a,1,2,1)),rewrite(4(6))]. given #581 (T,wt=9): 14056 (x' v y)' ^ (x v z)' = 0. [para(2(a,1),13333(a,1,2,1))]. given #582 (A,wt=17): 255 x ^ (y ^ (z ^ (u v (x ^ y)))) = x ^ (y ^ z). [para(25(a,1),86(a,1,2,2)),rewrite(5(5),5(4))]. given #583 (T,wt=9): 14057 (x v y)' ^ (y' v z)' = 0. [para(13333(a,1),4(a,1)),flip(a)]. given #584 (T,wt=9): 14060 x' ^ ((y ^ x)' v z)' = 0. [para(24(a,1),13333(a,1,2,1)),rewrite(4(6))]. given #585 (T,wt=9): 14593 x ^ ((x ^ y) v y')' = 0. [para(13424(a,1),143(a,1,2))]. given #586 (T,wt=9): 14604 x ^ ((y ^ x) v y')' = 0. [para(13424(a,1),1113(a,1,2))]. given #587 (A,wt=15): 257 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(110(a,1),3(a,1)),flip(a)]. given #588 (T,wt=9): 14654 x' ^ ((x ^ y)' v z) = x'. [para(13327(a,1),13424(a,1,2,1)),rewrite(4(5),13327(10))]. given #589 (T,wt=9): 14656 x' ^ ((y ^ x)' v z) = x'. [para(13340(a,1),13424(a,1,2,1)),rewrite(4(5),13340(10))]. given #590 (T,wt=9): 14693 x' ^ (y v (x ^ z)')' = 0. [para(13425(a,1),141(a,1,2,1)),rewrite(4(6))]. given #591 (T,wt=9): 14775 x' ^ (y v (x ^ z)') = x'. [para(13425(a,1),13424(a,1,2,1)),rewrite(4(5),13425(10))]. given #592 (A,wt=17): 259 1 != x | y ^ (z ^ x) != 0 | x' = y ^ (z ^ x). [para(110(a,1),10(a,1)),rewrite(213(5)),flip(a)]. given #593 (T,wt=9): 14777 (x v y')' ^ (y v z)' = 0. [para(2(a,1),13431(a,1,2,1))]. given #594 (T,wt=9): 14780 x' ^ (y v (z ^ x)')' = 0. [para(24(a,1),13431(a,1,2,1)),rewrite(4(6))]. given #595 (T,wt=9): 15044 x' ^ (y v (z ^ x)') = x'. [para(13438(a,1),13424(a,1,2,1)),rewrite(4(5),13438(10))]. given #596 (T,wt=9): 15379 x ^ (y v (x ^ y'))' = 0. [para(13527(a,1),157(a,1,2))]. given #597 (A,wt=15): 262 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(17(a,1),110(a,1,2,2))]. given #598 (T,wt=9): 15394 x ^ (y v (y' ^ x))' = 0. [para(13527(a,1),1163(a,1,2))]. given #599 (T,wt=9): 15445 (x v y)' ^ (x' v z)' = 0. [para(2(a,1),13532(a,1,2,1))]. given #600 (T,wt=9): 15862 x v (x' ^ y)' = (x' ^ y)'. [para(279(a,1),13677(a,1,1))]. given #601 (T,wt=9): 15877 x v (y ^ (x v y'))' = 1. [para(13677(a,1),201(a,1,2))]. given #602 (A,wt=17): 263 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(19(a,1),110(a,1,2,2)),rewrite(3(5),3(4))]. given #603 (T,wt=9): 15910 x v (y ^ (y' v x))' = 1. [para(13677(a,1),1507(a,1,2))]. given #604 (T,wt=9): 15962 x' ^ (y ^ (x ^ z))' = x'. [para(17(a,1),15857(a,1,2,1))]. given #605 (T,wt=9): 15966 (x ^ y)' v (z ^ x')' = 1. [para(15857(a,1),202(a,1,2,1,2))]. given #606 (T,wt=9): 15987 x' ^ (y ^ (z ^ x))' = x'. [para(213(a,1),15857(a,1,2,1))]. given #607 (A,wt=17): 264 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(20(a,1),110(a,1,2,2))]. given #608 (T,wt=9): 16015 (x ^ y)' v (z ^ y')' = 1. [para(15960(a,1),202(a,1,2,1,2))]. given #609 (T,wt=9): 16094 x ^ (y ^ (x' ^ z))' = x. [para(17(a,1),15964(a,1,2,1))]. given #610 (T,wt=9): 16095 x ^ ((x v y)' ^ z)' = x. [para(15964(a,1),20(a,1,2)),rewrite(6(2)),flip(a)]. given #611 (T,wt=9): 16099 (x' ^ y)' v (z ^ x)' = 1. [para(15964(a,1),202(a,1,2,1,2))]. given #612 (A,wt=21): 265 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(21(a,1),110(a,1,2,2))]. given #613 (T,wt=9): 16101 x ^ ((x' ^ y)' v z)' = 0. [para(15964(a,1),660(a,1,2)),rewrite(4(6))]. Low Water (keep, True_semantics): wt=20 given #614 (T,wt=9): 16102 x ^ (y v (x' ^ z)')' = 0. [para(15964(a,1),664(a,1,2)),rewrite(4(6))]. given #615 (T,wt=9): 16103 x ^ ((y v x)' ^ z)' = x. [para(15964(a,1),87(a,1,2)),rewrite(18(2)),flip(a)]. given #616 (T,wt=9): 16109 x ^ ((x' ^ y)' v z) = x. [para(15964(a,1),214(a,1,2)),rewrite(4(5),15964(9))]. given #617 (A,wt=16): 268 x ^ (y v (x' v z)) != 0 | y v (x' v z) = x'. [para(120(a,1),10(a,1)),flip(c),xx(a)]. given #618 (T,wt=9): 16121 x ^ (y v (x' ^ z)') = x. [para(15964(a,1),879(a,1,2)),rewrite(4(5),15964(9))]. given #619 (T,wt=9): 16148 x ^ (y ^ (z ^ x'))' = x. [para(213(a,1),15964(a,1,2,1))]. given #620 (T,wt=9): 16235 x v (y ^ x')' = (y ^ x')'. [para(16012(a,1),24(a,1,2)),rewrite(2(4))]. given #621 (T,wt=9): 16236 x ^ (y ^ (x v z)')' = x. [para(16012(a,1),20(a,1,2)),rewrite(6(2)),flip(a)]. given #622 (A,wt=19): 269 x ^ (y v (z ^ (x v (u v (y' v v))))) = x ^ (y v z). [para(120(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. given #623 (T,wt=9): 16241 (x ^ y')' v (z ^ y)' = 1. [para(16012(a,1),202(a,1,2,1,2))]. given #624 (T,wt=9): 16243 x ^ ((y ^ x')' v z)' = 0. [para(16012(a,1),660(a,1,2)),rewrite(4(6))]. given #625 (T,wt=9): 16244 x ^ (y v (z ^ x')')' = 0. [para(16012(a,1),664(a,1,2)),rewrite(4(6))]. given #626 (T,wt=9): 16245 x ^ (y ^ (z v x)')' = x. [para(16012(a,1),87(a,1,2)),rewrite(18(2)),flip(a)]. given #627 (A,wt=16): 273 x v (y ^ (x' ^ z)) != 1 | y ^ (x' ^ z) = x'. [para(130(a,1),10(b,1)),flip(c),xx(b)]. given #628 (T,wt=9): 16251 x ^ ((y ^ x')' v z) = x. [para(16012(a,1),214(a,1,2)),rewrite(4(5),16012(9))]. given #629 (T,wt=9): 16262 x ^ (y v (z ^ x')') = x. [para(16012(a,1),879(a,1,2)),rewrite(4(5),16012(9))]. Low Water (keep, True_semantics): wt=19 given #630 (T,wt=9): 16531 (x ^ y)' v (x' ^ z)' = 1. [para(7(a,1),13694(a,1,2,1,1,1))]. given #631 (T,wt=9): 16535 (x ^ y)' v (y' ^ z)' = 1. [para(24(a,1),13694(a,1,2,1,1,1))]. given #632 (A,wt=19): 275 x v (y v z) != 1 | z ^ (x v y) != 0 | z' = x v y. [para(3(a,1),34(a,1))]. given #633 (T,wt=9): 17619 x v (y' ^ (x v y))' = 1. [para(15862(a,1),201(a,1,2))]. given #634 (T,wt=9): 17640 x v (y' ^ (y v x))' = 1. [para(15862(a,1),1507(a,1,2))]. given #635 (T,wt=9): 17871 (x ^ y')' v (y ^ z)' = 1. [para(15966(a,1),2(a,1)),flip(a)]. given #636 (T,wt=9): 18203 (x' ^ y)' v (x ^ z)' = 1. [para(4(a,1),16099(a,1,2,1))]. given #637 (A,wt=19): 277 x v (y ^ z) != 1 | y ^ (z ^ x) != 0 | (y ^ z)' = x. [para(5(a,1),34(b,1))]. given #638 (T,wt=9): 18600 x v ((x v y) ^ y')' = 1. [para(16235(a,1),194(a,1,2))]. given #639 (T,wt=9): 18618 x v ((y v x) ^ y')' = 1. [para(16235(a,1),1442(a,1,2))]. given #640 (T,wt=9): 18973 (x' ^ (x v y))' = (y ^ x')'. [hyper(37,a,17619,a,b,311,a),rewrite(2(7),792(8)),flip(a)]. given #641 (T,wt=9): 19099 (x' ^ (y v x))' = (y ^ x')'. [para(2(a,1),18973(a,1,1,2))]. given #642 (A,wt=19): 280 x v (y v z) != 1 | (x v z) ^ y != 0 | (x v z)' = y. [para(15(a,1),34(a,1))]. given #643 (T,wt=9): 19101 ((x v y) ^ x')' = (y ^ x')'. [para(4(a,1),18973(a,1,1))]. given #644 (T,wt=9): 19102 (x' ^ (x v y))' = (x' ^ y)'. [para(4(a,1),18973(a,2,1))]. given #645 (T,wt=9): 19107 (x' ^ (y v (x v y)'))' = x. [para(29(a,1),18973(a,1,1,2)),rewrite(4(3),67(3),279(2),4(5)),flip(a)]. given #646 (T,wt=9): 19112 (x ^ (x' v y))' = (y ^ x)'. [para(279(a,1),18973(a,1,1,1)),rewrite(279(6))]. given #647 (A,wt=19): 281 (x ^ y) v z != 1 | x ^ (z ^ y) != 0 | z' = x ^ y. [para(17(a,1),34(b,1))]. given #648 (T,wt=9): 19116 (x' ^ (y v (y v x)'))' = x. [para(162(a,1),18973(a,1,1,2)),rewrite(4(3),67(3),279(2),4(5)),flip(a)]. given #649 (T,wt=9): 19233 (x v y) ^ (x' ^ y)' = x. [para(18973(a,1),170(a,1,2,2)),rewrite(16249(7),19102(8),279(10)),xx(a)]. given #650 (T,wt=9): 19479 ((x v y) ^ y')' = (x ^ y')'. [para(4(a,1),19099(a,1,1))]. given #651 (T,wt=9): 19489 (x ^ (y v x'))' = (y ^ x)'. [para(279(a,1),19099(a,1,1,1)),rewrite(279(6))]. given #652 (A,wt=21): 286 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 #653 (T,wt=9): 19575 (x v y) ^ (y' ^ x)' = y. [para(19099(a,1),170(a,1,2,2)),rewrite(16261(7),19480(8),279(10)),xx(a)]. given #654 (T,wt=9): 19697 (x v y) ^ x' = y ^ x'. [para(19101(a,1),279(a,1,1)),rewrite(279(4)),flip(a)]. given #655 (T,wt=9): 19742 x' ^ (x v y) = x' ^ y. [para(19102(a,1),279(a,1,1)),rewrite(279(4)),flip(a)]. given #656 (T,wt=9): 19967 x' ^ (y v x) = x' ^ y. [back_rewrite(16722),rewrite(19961(8))]. given #657 (A,wt=17): 292 1 != x | y ^ (x ^ z) != 0 | (y ^ (x ^ z))' = x. [para(76(a,1),34(a,1)),rewrite(4(5),211(5)),flip(a)]. given #658 (T,wt=9): 19983 x' ^ (y v (x v y)') = x'. [para(19107(a,1),279(a,1,1)),flip(a)]. given #659 (T,wt=9): 20014 x ^ (x' v y) = y ^ x. [para(19112(a,1),279(a,1,1)),rewrite(279(3)),flip(a)]. given #660 (T,wt=9): 20068 (x' v y) ^ (y ^ x)' = x'. [para(19112(a,1),170(a,1,2,2)),rewrite(16024(6),20014(8)),xx(a)]. given #661 (T,wt=7): 21486 (x v y)' = x' ^ y'. [para(18(a,1),20068(a,1,2,1)),rewrite(2(3),21224(3),19697(4)),flip(a)]. given #662 (A,wt=21): 293 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),211(6),54(6))]. given #663 (T,wt=7): 21868 (x' ^ y')' = x v y. [back_rewrite(19538),rewrite(21486(5),17934(7))]. given #664 (T,wt=7): 25856 (x ^ y')' = x' v y. [para(279(a,1),21868(a,1,1,1))]. given #665 (T,wt=7): 26646 (x ^ y)' = x' v y'. [para(279(a,1),25856(a,1,1,2))]. given #666 (T,wt=9): 20494 (x v y) ^ y' = x ^ y'. [para(19479(a,1),279(a,1,1)),rewrite(279(4)),flip(a)]. given #667 (A,wt=16): 356 x ^ (y v (z v x')) != 0 | y v (z v x') = x'. [para(133(a,1),10(a,1)),flip(c),xx(a)]. given #668 (T,wt=9): 20510 x ^ (y v x') = y ^ x. [para(19489(a,1),279(a,1,1)),rewrite(279(3)),flip(a)]. given #669 (T,wt=9): 21350 (x v y) ^ (y v x') = y. [para(18(a,1),20014(a,2)),rewrite(2(4),21224(4))]. given #670 (T,wt=9): 25650 (x ^ y) v (x ^ y') = x. [back_rewrite(17498),rewrite(21494(4))]. given #671 (T,wt=9): 25719 x v (y' v (y ^ x')) = 1. [back_rewrite(20821),rewrite(21550(4))]. given #672 (A,wt=16): 364 x v (y ^ (z ^ x')) != 1 | y ^ (z ^ x') = x'. [para(137(a,1),10(b,1)),flip(c),xx(b)]. given #673 (T,wt=9): 25747 (x ^ y) v (y ^ x') = y. [back_rewrite(17497),rewrite(21550(4))]. ============================== PROOF ================================= % Proof 1 at 14.84 (+ 0.14) seconds: distributivity. % Length of proof is 113. % Level of proof is 24. % Maximum clause weight is 23. % Given clauses 673. 1 x ^ (y v z) = (x ^ y) v (x ^ z) # label(distributivity) # 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 ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 (c1 ^ c2) v (c1 ^ c3) != c1 ^ (c2 v c3) # label(distributivity) # 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)]. 24 x v (y ^ x) = x. [para(4(a,1),7(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)]. 32 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,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))]. 37 (x ^ y) v z != 1 | x ^ (y ^ z) != 0 | (x ^ y)' = z. [para(5(a,1),10(b,1))]. 42 x ^ (y v ((z ^ x) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [para(4(a,1),12(a,1,2,2,1))]. 46 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. 50 x v (y v x') = y v 1. [para(8(a,1),15(a,1,2)),flip(a)]. 60 x v (x v y) = x v y. [para(27(a,1),3(a,1,1)),flip(a)]. 67 1 ^ x = x. [para(30(a,1),4(a,1)),flip(a)]. 69 0 v x = x. [para(33(a,1),2(a,1)),flip(a)]. 75 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),17(a,1,2)),flip(a)]. 77 x ^ (y ^ x') = y ^ 0. [para(9(a,1),17(a,1,2)),flip(a)]. 80 1 v x = 1. [para(67(a,1),6(a,1))]. 81 x v (x' v y) = 1. [back_rewrite(28),rewrite(80(5))]. 83 0 ^ x = 0. [para(69(a,1),6(a,1,2))]. 85 x ^ (x' ^ y) = 0. [back_rewrite(31),rewrite(83(5))]. 87 x ^ ((y v x) ^ z) = x ^ z. [para(18(a,1),5(a,1,1)),flip(a)]. 93 x v 1 = 1. [para(18(a,1),67(a,1)),flip(a)]. 95 x v (y v x') = 1. [back_rewrite(50),rewrite(93(5))]. 96 x ^ 0 = 0. [para(83(a,1),4(a,1)),flip(a)]. 97 x ^ (y ^ x') = 0. [back_rewrite(77),rewrite(96(5))]. 108 x v ((y ^ x) v z) = x v z. [para(24(a,1),3(a,1,1)),flip(a)]. 119 x ^ (y v (z ^ (x v (y' v u)))) = x ^ (y v z). [para(81(a,1),12(a,1,2,2,2,2)),rewrite(30(3),2(2),24(2)),flip(a)]. 122 x ^ (x v y)' = 0. [para(9(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. 131 x ^ ((x v y)' ^ z) = 0. [para(85(a,1),20(a,1,2)),rewrite(96(2)),flip(a)]. 141 x ^ (y v x)' = 0. [para(2(a,1),122(a,1,2,1))]. 145 x ^ (y v ((x v z)' ^ (y v u))) = x ^ (y v ((x v z)' ^ (x v u))). [para(122(a,1),12(a,1,2,2,1)),rewrite(69(6))]. 157 x ^ (y ^ (z v (x ^ y))') = 0. [para(141(a,1),5(a,1)),flip(a)]. 162 x v (y v (y v x)') = 1. [para(2(a,1),29(a,1,2,2,1))]. 170 x v (y ^ (x ^ y)') != 1 | y ^ (x ^ y)' = x'. [para(32(a,1),10(b,1)),flip(c),xx(b)]. 184 x v (x ^ y)' = 1. [para(8(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. 195 x v (y ^ x)' = 1. [para(4(a,1),184(a,1,2,1))]. 201 x v (y v (z ^ (x v y))') = 1. [para(195(a,1),3(a,1)),flip(a)]. 208 ((x v y) ^ z) v (x ^ z)' = 1. [para(20(a,1),195(a,1,2,1))]. 276 x v y != 1 | x ^ y != 0 | y' = x. [para(4(a,1),34(b,1))]. 279 x'' = x. [para(8(a,1),34(a,1)),rewrite(4(5),9(5)),xx(a),xx(b)]. 296 x' v (y v x) = 1. [para(279(a,1),95(a,1,2,2))]. 297 x' ^ (y ^ x) = 0. [para(279(a,1),97(a,1,2,2))]. 301 x' ^ (y v x) != 0 | y v x = x. [para(296(a,1),10(a,1)),rewrite(279(10)),flip(c),xx(a)]. 311 x ^ (y ^ (y ^ ((x ^ y) v z))') = 0. [para(21(a,1),297(a,1,2)),rewrite(4(6),5(6))]. 430 x v (y v (y v (x ^ z))') = 1. [para(162(a,1),22(a,1,2)),rewrite(93(2)),flip(a)]. 689 x ^ ((y ^ x) v (y ^ z)) = y ^ x. [para(69(a,1),42(a,1,2,2,2,2)),rewrite(69(5),69(8),75(7))]. 792 x' ^ (x v (y ^ x')) = x' ^ (x v y). [para(27(a,1),46(a,1,2,2,2))]. 878 ((x v y) ^ z) v (y ^ z)' = 1. [para(87(a,1),195(a,1,2,1))]. 1553 (x ^ (y v z)) v (y ^ x)' = 1. [para(4(a,1),208(a,1,1))]. 2247 x v ((y ^ x) v (x ^ z))' = 1. [para(430(a,1),108(a,1)),flip(a)]. 4011 x' ^ (x v (y ^ (x' v z))) = x' ^ (x v y). [para(60(a,1),119(a,1,2,2,2))]. 7601 x' ^ (x v y) != 0 | y v x = x. [para(2(a,1),301(a,1,2))]. 13234 x' ^ (x v (x' v y)') = 0. [para(145(a,1),792(a,2)),rewrite(4(8),131(8),33(3),4(2),9(2),4011(10)),flip(a)]. 13301 x v (x' v y)' = x. [hyper(7601,a,13234,a),rewrite(2(4))]. 13319 x v (y v x')' = x. [para(2(a,1),13301(a,1,2,1))]. 13326 x ^ (x' v y)' = (x' v y)'. [para(13301(a,1),18(a,1,2)),rewrite(4(4))]. 13330 x' v (x v y)' = x'. [para(279(a,1),13301(a,1,2,1,1))]. 13428 x' v (y v x)' = x'. [para(279(a,1),13319(a,1,2,1,2))]. 13525 x' v (y v (x v z)') = y v x'. [para(13330(a,1),15(a,1,2)),flip(a)]. 13527 x' ^ (x v y)' = (x v y)'. [para(13330(a,1),18(a,1,2)),rewrite(4(4))]. 13677 x' v (x ^ y)' = (x ^ y)'. [para(7(a,1),13428(a,1,2,1)),rewrite(2(4))]. 13910 x' v (y v ((x' v y)' ^ (x v z))) = 1. [para(13326(a,1),1553(a,1,2,1)),rewrite(279(9),2(8),3(8))]. 15379 x ^ (y v (x ^ y'))' = 0. [para(13527(a,1),157(a,1,2))]. 15857 x' ^ (x ^ y)' = x'. [para(13677(a,1),6(a,1,2))]. 15862 x v (x' ^ y)' = (x' ^ y)'. [para(279(a,1),13677(a,1,1))]. 15960 x' ^ (y ^ x)' = x'. [para(4(a,1),15857(a,1,2,1))]. 16012 x ^ (y ^ x')' = x. [para(279(a,1),15960(a,1,1)),rewrite(279(6))]. 16024 x v ((x' v y) ^ (z ^ x)') = 1. [para(15960(a,1),208(a,1,2,1)),rewrite(279(7),2(6))]. 16261 x' v ((y v x) ^ (z ^ x')') = 1. [para(16012(a,1),878(a,1,2,1)),rewrite(2(7))]. 17497 (x ^ y) v (y ^ (x ^ y)') = y. [hyper(276,a,2247,a,b,15379,a),rewrite(279(7))]. 17619 x v (y' ^ (x v y))' = 1. [para(15862(a,1),201(a,1,2))]. 18973 (x' ^ (x v y))' = (y ^ x')'. [hyper(37,a,17619,a,b,311,a),rewrite(2(7),792(8)),flip(a)]. 19099 (x' ^ (y v x))' = (y ^ x')'. [para(2(a,1),18973(a,1,1,2))]. 19101 ((x v y) ^ x')' = (y ^ x')'. [para(4(a,1),18973(a,1,1))]. 19107 (x' ^ (y v (x v y)'))' = x. [para(29(a,1),18973(a,1,1,2)),rewrite(4(3),67(3),279(2),4(5)),flip(a)]. 19112 (x ^ (x' v y))' = (y ^ x)'. [para(279(a,1),18973(a,1,1,1)),rewrite(279(6))]. 19480 (x' ^ (y v x))' = (x' ^ y)'. [para(4(a,1),19099(a,2,1))]. 19575 (x v y) ^ (y' ^ x)' = y. [para(19099(a,1),170(a,1,2,2)),rewrite(16261(7),19480(8),279(10)),xx(a)]. 19697 (x v y) ^ x' = y ^ x'. [para(19101(a,1),279(a,1,1)),rewrite(279(4)),flip(a)]. 19983 x' ^ (y v (x v y)') = x'. [para(19107(a,1),279(a,1,1)),flip(a)]. 20014 x ^ (x' v y) = y ^ x. [para(19112(a,1),279(a,1,1)),rewrite(279(3)),flip(a)]. 20068 (x' v y) ^ (y ^ x)' = x'. [para(19112(a,1),170(a,1,2,2)),rewrite(16024(6),20014(8)),xx(a)]. 20601 (x' v y)' = x ^ (y ^ x)'. [para(13301(a,1),19575(a,1,1)),rewrite(279(4),4(3),20014(3)),flip(a)]. 20733 x' v (y v (x ^ (y ^ x)')) = 1. [back_rewrite(13910),rewrite(20601(4),5(6),75(6),4(4))]. 20881 ((x ^ y) v z) ^ y' = z ^ y'. [para(108(a,1),19697(a,1,1)),rewrite(19697(3)),flip(a)]. 21224 x v (y v x)' = x v y'. [para(19983(a,1),24(a,1,2)),rewrite(2(5),13525(5)),flip(a)]. 21486 (x v y)' = x' ^ y'. [para(18(a,1),20068(a,1,2,1)),rewrite(2(3),21224(3),19697(4)),flip(a)]. 21550 x ^ (y ^ x)' = x ^ y'. [para(20068(a,1),170(a,1,2,2,1)),rewrite(279(6),4(5),3(6),20733(6),20068(10),279(7),4(6),21486(9),279(8)),xx(a)]. 25747 (x ^ y) v (y ^ x') = y. [back_rewrite(17497),rewrite(21550(4))]. 30738 (x ^ y) v (x ^ (z ^ y')) = x ^ (y v z). [para(75(a,1),25747(a,1,1)),rewrite(5(5),19697(4))]. 30759 (x ^ y) v (x ^ z) = x ^ (y v z). [para(689(a,1),25747(a,1,1)),rewrite(20881(6),5(4),30738(5)),flip(a)]. 30760 $F # answer(distributivity). [resolve(30759,a,13,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=673. Generated=545357. Kept=30757. proofs=1. Usable=192. Sos=7043. Demods=5725. Limbo=31, Disabled=23501. Hints=0. Weight_deleted=17826. Literals_deleted=0. Forward_subsumed=489496. Back_subsumed=91. Sos_limit_deleted=7278. Sos_displaced=0. Sos_removed=0. New_demodulators=25629 (6 lex), Back_demodulated=23397. Back_unit_deleted=0. Demod_attempts=10269157. Demod_rewrites=2598710. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=594085. Nonunit_bsub_feature_tests=76237. Megabytes=23.47. User_CPU=14.84, System_CPU=0.14, Wall_clock=16. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 27120 exit (max_proofs) Fri Apr 13 09:21:43 2007