============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5150 was started by mccune on cleo, Tue Nov 3 09:47:44 2009 The command was "/home/mccune/LADR/bin/prover9 -f lt.in uc.in H49.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 H49.in assign(max_seconds,30). assign(constant_weight,0). 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). (all x all y (x ^ y = x -> x' v y' = x')). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all x all y (x ^ y = x -> x' v y' = x')) # label(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 ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. c1 ^ c2 = c1. [deny(1)]. c1' != c1' v c2'. [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, 1, c1, c2, ^, v, ' ]). After inverse_order: Function symbol precedence: function_order([ 0, 1, c1, c2, ^, 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 ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ (y v u)))) # label(H49). [assumption]. kept: 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. kept: 13 c1 ^ c2 = c1. [deny(1)]. 14 c1' != c1' v c2'. [deny(1)]. kept: 15 c1' v c2' != c1'. [copy(14),flip(a)]. ============================== 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 = c1. [deny(1)]. 15 c1' v c2' != c1'. [copy(14),flip(a)]. end_of_list. formulas(demodulators). 2 x v y = y v x. [assumption]. % (lex-dep) 3 (x v y) v z = x v (y v z). [assumption]. 4 x ^ y = y ^ x. [assumption]. % (lex-dep) 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. 6 x ^ (x v y) = x. [assumption]. 7 x v (x ^ y) = x. [assumption]. 8 x v x' = 1. [assumption]. 9 x ^ x' = 0. [assumption]. 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. 13 c1 ^ c2 = c1. [deny(1)]. 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: 16 x v (y v z) = z v (x v y). [para(3(a,1),2(a,1))]. given #3 (I,wt=7): 4 x ^ y = y ^ x. [assumption]. given #4 (I,wt=11): 5 (x ^ y) ^ z = x ^ (y ^ z). [assumption]. % Operation ^ is associative-commutative; CAC redundancy checks enabled. % back CAC tautology: 18 x ^ (y ^ z) = z ^ (x ^ y). [para(5(a,1),4(a,1))]. given #5 (I,wt=7): 6 x ^ (x v y) = x. [assumption]. given #6 (I,wt=7): 7 x v (x ^ y) = x. [assumption]. given #7 (I,wt=5): 8 x v x' = 1. [assumption]. given #8 (I,wt=5): 9 x ^ x' = 0. [assumption]. given #9 (I,wt=12): 10 x v y != 1 | x ^ y != 0 | x' = y. [assumption]. given #10 (I,wt=23): 12 x ^ (y v ((x ^ z) v (z ^ (y v u)))) = x ^ (y v (z ^ (x v u))). [copy(11),flip(a)]. given #11 (I,wt=2): 13 c1 ^ c2 = c1. [deny(1)]. given #12 (I,wt=5): 15 c1' v c2' != c1'. [copy(14),flip(a)]. given #13 (A,wt=11): 17 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite([3(2)])]. given #14 (T,wt=4): 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. given #15 (T,wt=4): 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. given #16 (T,wt=4): 64 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. given #17 (T,wt=2): 70 1' = 0. [hyper(10,a,35,a,b,64,a)]. given #18 (A,wt=11): 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. given #19 (T,wt=3): 71 1 v x = 1. [para(64(a,1),6(a,1))]. given #20 (T,wt=3): 79 x v 1 = 1. [para(71(a,1),2(a,1)),flip(a)]. given #21 (T,wt=2): 81 0' = 1. [hyper(10,a,79,a,b,32,a)]. given #22 (T,wt=4): 65 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. given #23 (A,wt=7): 20 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #24 (T,wt=3): 83 0 ^ x = 0. [para(65(a,1),6(a,1,2))]. given #25 (T,wt=3): 94 x ^ 0 = 0. [para(83(a,1),4(a,1)),flip(a)]. given #26 (T,wt=5): 28 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #27 (T,wt=5): 29 x v x = x. [para(6(a,1),7(a,1,2))]. given #28 (A,wt=13): 21 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #29 (T,wt=5): 82 0 != x | x' = 1. [para(79(a,1),10(a,1)),rewrite([32(5)]),flip(b),xx(a)]. given #30 (T,wt=5): 96 1 != x | x' = 0. [back_rewrite(66),rewrite([94(4)]),xx(b)]. given #31 (T,wt=6): 53 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. given #32 (T,wt=3): 117 c1 ^ c2' = 0. [para(9(a,1),53(a,1,2)),rewrite([4(3),83(3)]),flip(a)]. given #33 (A,wt=11): 22 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #34 (T,wt=4): 116 c1 ^ (c2 v x) = c1. [para(6(a,1),53(a,1,2)),rewrite([13(3)]),flip(a)]. given #35 (T,wt=4): 121 c1 ^ (x v c2) = c1. [para(20(a,1),53(a,1,2)),rewrite([13(3)]),flip(a)]. given #36 (T,wt=5): 122 c1 ^ (c2' ^ x) = 0. [para(117(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #37 (T,wt=5): 124 c1 ^ (x ^ c2') = 0. [para(117(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #38 (A,wt=13): 23 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #39 (T,wt=6): 54 c2 ^ (x ^ c1) = x ^ c1. [para(13(a,1),5(a,2,2)),rewrite([4(4)])]. given #40 (T,wt=4): 153 c2 v (x ^ c1) = c2. [para(54(a,1),7(a,1,2))]. given #41 (T,wt=2): 160 c1 v c2 = c2. [para(64(a,1),153(a,1,2)),rewrite([2(3)])]. given #42 (T,wt=4): 155 c2 v (c1 ^ x) = c2. [para(4(a,1),153(a,1,2))]. given #43 (A,wt=11): 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #44 (T,wt=4): 163 c2 != 1 | c1 != 0 | c1' = c2. [para(160(a,1),10(a,1)),rewrite([13(6)])]. given #45 (T,wt=6): 78 c1 ^ (x ^ c2) = x ^ c1. [para(13(a,1),19(a,1,2)),flip(a)]. given #46 (T,wt=6): 134 c1 ^ (x v (c2 v y)) = c1. [para(17(a,1),116(a,1,2))]. given #47 (T,wt=6): 136 c1 ^ (x v (y v c2)) = c1. [para(3(a,1),121(a,1,2))]. given #48 (A,wt=13): 25 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #49 (T,wt=6): 156 c2 v (x ^ (y ^ c1)) = c2. [para(5(a,1),153(a,1,2))]. given #50 (T,wt=6): 161 c1 v (c2 v x) = c2 v x. [para(160(a,1),3(a,1,1)),flip(a)]. given #51 (T,wt=6): 162 c2 v (x v c1) = x v c2. [para(160(a,1),3(a,2,2)),rewrite([2(4)])]. given #52 (T,wt=6): 165 c1 v (x v c2) = x v c2. [para(160(a,1),17(a,1,2)),flip(a)]. given #53 (A,wt=7): 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #54 (T,wt=6): 171 c2 v (x ^ (c1 ^ y)) = c2. [para(19(a,1),155(a,1,2))]. given #55 (T,wt=6): 212 c2 v (x v c1) = c2 v x. [para(162(a,2),2(a,1))]. given #56 (T,wt=7): 62 c1 ^ (x v (c2 ^ (c1 v y))) = c1. [back_rewrite(55),rewrite([56(8)]),flip(a)]. given #57 (T,wt=7): 72 x v (x' v y) = 1. [back_rewrite(30),rewrite([71(5)])]. given #58 (A,wt=13): 27 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #59 (F,wt=5): 251 c1 ^ (c1' v c2') != 0. [ur(10,a,72,a,c,15,a(flip))]. given #60 (T,wt=3): 257 c2 v c1' = 1. [para(72(a,1),165(a,1)),rewrite([2(5)]),flip(a)]. given #61 (T,wt=5): 271 c2 v (c1' v x) = 1. [para(257(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #62 (T,wt=5): 274 c2 v (x v c1') = 1. [para(257(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #63 (T,wt=6): 272 c2 ^ c1' != 0 | c2' = c1'. [para(257(a,1),10(a,1)),xx(a)]. given #64 (A,wt=9): 31 x v (y v (x v y)') = 1. [para(8(a,1),3(a,1)),flip(a)]. given #65 (T,wt=7): 80 x v (y v x') = 1. [back_rewrite(58),rewrite([79(5)])]. given #66 (T,wt=7): 85 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite([83(5)])]. given #67 (T,wt=7): 95 x ^ (y ^ x') = 0. [back_rewrite(75),rewrite([94(5)])]. given #68 (T,wt=7): 126 x ^ (x v y)' = 0. [para(9(a,1),22(a,1,2)),rewrite([94(2)]),flip(a)]. given #69 (A,wt=9): 34 x ^ (y ^ (x ^ y)') = 0. [para(9(a,1),5(a,1)),flip(a)]. given #70 (T,wt=5): 306 c1 ^ (c2 v x)' = 0. [para(126(a,1),53(a,1,2)),rewrite([4(3),83(3)]),flip(a)]. given #71 (T,wt=5): 307 c1 ^ (x v c2)' = 0. [para(165(a,1),126(a,1,2,1))]. given #72 (T,wt=7): 141 c1 ^ (x ^ (c2' ^ y)) = 0. [para(122(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #73 (T,wt=7): 142 c1 ^ (x ^ (y ^ c2')) = 0. [para(5(a,1),124(a,1,2))]. given #74 (A,wt=12): 36 x v y != 1 | y ^ x != 0 | y' = x. [para(2(a,1),10(a,1))]. given #75 (T,wt=4): 332 c2 != 1 | c1 != 0 | c2' = c1. [para(160(a,1),36(a,1)),rewrite([4(6),13(6)])]. given #76 (T,wt=4): 344 c2 ^ c1' != 0 | c2 = c1. [para(257(a,1),36(a,1)),rewrite([4(7),329(12)]),flip(c),xx(a)]. given #77 (T,wt=5): 329 x'' = x. [para(8(a,1),36(a,1)),rewrite([4(5),9(5)]),xx(a),xx(b)]. given #78 (T,wt=7): 175 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite([79(2)]),flip(a)]. given #79 (A,wt=18): 37 x v (y v z) != 1 | (x v y) ^ z != 0 | (x v y)' = z. [para(3(a,1),10(a,1))]. given #80 (T,wt=5): 357 c2 v (x ^ c1)' = 1. [para(54(a,1),175(a,1,2,1))]. given #81 (T,wt=5): 392 c2 v (c1 ^ x)' = 1. [para(4(a,1),357(a,1,2,1))]. given #82 (T,wt=7): 243 c1 ^ (x v (c2 ^ (y v c1))) = c1. [para(2(a,1),62(a,1,2,2,2))]. given #83 (T,wt=7): 244 c1 ^ ((c2 ^ (c1 v x)) v y) = c1. [para(2(a,1),62(a,1,2))]. given #84 (A,wt=23): 39 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 #85 (T,wt=7): 277 c2 v (x v (c1' v y)) = 1. [para(271(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #86 (T,wt=7): 278 c2 v (x v (y v c1')) = 1. [para(3(a,1),274(a,1,2))]. given #87 (T,wt=7): 301 x ^ (y v x)' = 0. [para(2(a,1),126(a,1,2,1))]. given #88 (T,wt=7): 313 c1 ^ (x ^ (c2 ^ x)') = 0. [para(34(a,1),53(a,1,2)),rewrite([4(3),83(3)]),flip(a)]. given #89 (A,wt=23): 40 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 #90 (T,wt=6): 518 c1 ^ (c2 ^ (c1 v x))' = 0. [para(313(a,1),22(a,1)),flip(a)]. given #91 (T,wt=6): 564 c1 ^ (c2 ^ (x v c1))' = 0. [para(2(a,1),518(a,1,2,1,2))]. given #92 (T,wt=7): 315 c1 ^ ((c2 v x)' ^ y) = 0. [para(306(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #93 (T,wt=7): 317 c1 ^ (x v (c2 v y))' = 0. [para(17(a,1),306(a,1,2,1))]. given #94 (A,wt=29): 41 x ^ (y v (z v ((x ^ u) v (u ^ (y v (z v w)))))) = x ^ (y v (z v (u ^ (x v w)))). [para(3(a,1),12(a,1,2,2,2,2)),rewrite([3(7),3(12)])]. given #95 (T,wt=7): 318 c1 ^ (x ^ (c2 v y)') = 0. [para(306(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #96 (T,wt=7): 319 c1 ^ (x v (y v c2))' = 0. [para(3(a,1),307(a,1,2,1))]. given #97 (T,wt=7): 320 c1 ^ ((x v c2)' ^ y) = 0. [para(307(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #98 (T,wt=7): 322 c1 ^ (x ^ (y v c2)') = 0. [para(307(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #99 (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 #100 (T,wt=7): 349 x' v (y v x) = 1. [para(329(a,1),80(a,1,2,2))]. given #101 (T,wt=7): 350 x' ^ (y ^ x) = 0. [para(329(a,1),95(a,1,2,2))]. given #102 (T,wt=7): 352 x v (y ^ x)' = 1. [para(4(a,1),175(a,1,2,1))]. given #103 (T,wt=7): 391 c2 v ((x ^ c1)' v y) = 1. [para(357(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #104 (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 #105 (T,wt=7): 393 c2 v (x ^ (y ^ c1))' = 1. [para(5(a,1),357(a,1,2,1))]. given #106 (T,wt=7): 396 c2 v (x v (y ^ c1)') = 1. [para(357(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #107 (T,wt=7): 399 c2 v ((c1 ^ x)' v y) = 1. [para(392(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #108 (T,wt=7): 402 c2 v (x v (c1 ^ y)') = 1. [para(392(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #109 (A,wt=27): 44 x ^ ((y v ((x ^ z) v (z ^ (y v u)))) ^ w) = x ^ ((y v (z ^ (x v u))) ^ w). [para(12(a,1),5(a,1,1)),rewrite([5(5)]),flip(a)]. given #110 (T,wt=7): 403 c2 v (x ^ (c1 ^ y))' = 1. [para(19(a,1),392(a,1,2,1))]. given #111 (T,wt=7): 406 c1 ^ ((c2 ^ (x v c1)) v y) = c1. [para(2(a,1),243(a,1,2))]. given #112 (T,wt=7): 508 (x v c1) ^ (c2 v x)' = 0. [para(212(a,1),301(a,1,2,1))]. given #113 (T,wt=6): 1063 (c1 v (c2 ^ x)) ^ c2' = 0. [para(7(a,1),508(a,1,2,1)),rewrite([2(4)])]. given #114 (A,wt=31): 45 x ^ (y ^ (z v ((x ^ (y ^ u)) v (u ^ (z v w))))) = x ^ (y ^ (z v (u ^ ((x ^ y) v w)))). [para(12(a,1),5(a,1)),rewrite([5(6),5(8)]),flip(a)]. given #115 (T,wt=6): 1069 (c1 v (x ^ c2)) ^ c2' = 0. [para(26(a,1),508(a,1,2,1)),rewrite([2(4)])]. given #116 (T,wt=6): 1076 c2' ^ (c1 v (c2 ^ x)) = 0. [para(1063(a,1),4(a,1)),flip(a)]. given #117 (T,wt=6): 1213 c2' ^ (c1 v (x ^ c2)) = 0. [para(1069(a,1),4(a,1)),flip(a)]. given #118 (T,wt=7): 510 c1 ^ (x ^ (x ^ c2)') = 0. [para(4(a,1),313(a,1,2,2,1))]. given #119 (A,wt=29): 46 x ^ (y v ((x ^ (z ^ u)) v (z ^ (u ^ (y v w))))) = x ^ (y v (z ^ (u ^ (x v w)))). [para(5(a,1),12(a,1,2,2,2)),rewrite([5(11)])]. given #120 (T,wt=7): 516 x ^ (c1 ^ (c2 ^ x)') = 0. [para(313(a,1),19(a,1)),flip(a)]. given #121 (T,wt=7): 767 c2 v (x v (x v c1)') = 1. [para(212(a,1),349(a,1,2)),rewrite([2(6),3(6)])]. given #122 (T,wt=6): 1375 c2 v (c1 v (c2 ^ x))' = 1. [para(767(a,1),24(a,1)),rewrite([2(6)]),flip(a)]. given #123 (T,wt=6): 1386 c2 v (c1 v (x ^ c2))' = 1. [para(4(a,1),1375(a,1,2,1,2))]. given #124 (A,wt=16): 49 x ^ (y v (z ^ (x v y'))) = x ^ (y v z). [para(8(a,1),12(a,1,2,2,2,2)),rewrite([32(3),2(2),26(2)]),flip(a)]. given #125 (T,wt=7): 776 x ^ (c1 ^ (x ^ c2)') = 0. [para(78(a,1),350(a,1,2)),rewrite([4(6),5(6)])]. given #126 (T,wt=7): 794 (c2 ^ x) v (c1 ^ x)' = 1. [para(53(a,1),352(a,1,2,1))]. given #127 (T,wt=6): 1447 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),794(a,1,2,1))]. given #128 (T,wt=6): 1454 (c2 ^ (x v c1)) v c1' = 1. [para(20(a,1),794(a,1,2,1))]. given #129 (A,wt=49): 51 x ^ (y v ((x ^ (z v (u ^ (x v w)))) v ((z v ((x ^ u) v (u ^ (z v w)))) ^ (y v v5)))) = x ^ (y v ((z v ((x ^ u) v (u ^ (z v w)))) ^ (x v v5))). [para(12(a,1),12(a,1,2,2,1))]. given #130 (T,wt=6): 1476 c1' v (c2 ^ (c1 v x)) = 1. [para(1447(a,1),2(a,1)),flip(a)]. given #131 (T,wt=6): 1488 c1' v (c2 ^ (x v c1)) = 1. [para(1454(a,1),2(a,1)),flip(a)]. given #132 (T,wt=7): 797 (x ^ c2) v (x ^ c1)' = 1. [para(78(a,1),352(a,1,2,1))]. given #133 (T,wt=7): 1059 (c1 v x) ^ (c2 v x)' = 0. [para(2(a,1),508(a,1,1))]. given #134 (A,wt=31): 52 x ^ (y v (z ^ (x v ((z ^ u) v (u ^ (y v w)))))) = x ^ (y v (z ^ (x v (u ^ (z v w))))). [para(12(a,1),12(a,1,2,2,2)),rewrite([12(8)]),flip(a)]. given #135 (T,wt=7): 1060 (x v c1) ^ (x v c2)' = 0. [para(2(a,1),508(a,1,2,1))]. given #136 (T,wt=7): 1367 c2 v (x v (c1 v x)') = 1. [para(2(a,1),767(a,1,2,2,1))]. given #137 (T,wt=7): 1374 x v (c2 v (x v c1)') = 1. [para(767(a,1),17(a,1)),flip(a)]. given #138 (T,wt=7): 1445 (x ^ c2) v (c1 ^ x)' = 1. [para(4(a,1),794(a,1,1))]. given #139 (A,wt=9): 56 x ^ (y v (x v z)) = x. [para(17(a,1),6(a,1,2))]. given #140 (T,wt=7): 1446 (c2 ^ x) v (x ^ c1)' = 1. [para(4(a,1),794(a,1,2,1))]. given #141 (T,wt=7): 1686 (c1 v x) ^ (x v c2)' = 0. [para(2(a,1),1059(a,1,2,1))]. given #142 (T,wt=7): 1859 x v (c2 v (c1 v x)') = 1. [para(1367(a,1),17(a,1)),flip(a)]. given #143 (T,wt=8): 103 1 != x | 0 != x | x' = x. [para(29(a,1),10(a,1)),rewrite([28(3)]),flip(a),flip(b)]. given #144 (A,wt=11): 57 x v (y v (x ^ z)) = y v x. [para(7(a,1),17(a,1,2)),flip(a)]. given #145 (T,wt=8): 131 c1 ^ ((c2 v x) ^ y) = c1 ^ y. [para(22(a,1),53(a,1,2)),rewrite([53(4)]),flip(a)]. given #146 (T,wt=8): 135 c1 ^ (x ^ (c2 v y)) = x ^ c1. [para(116(a,1),19(a,1,2)),flip(a)]. given #147 (T,wt=8): 137 c1 ^ ((x v c2) ^ y) = c1 ^ y. [para(121(a,1),5(a,1,1)),flip(a)]. given #148 (T,wt=8): 139 c1 ^ (x ^ (y v c2)) = x ^ c1. [para(121(a,1),19(a,1,2)),flip(a)]. given #149 (A,wt=18): 59 x v (y v z) != 1 | y ^ (x v z) != 0 | y' = x v z. [para(17(a,1),10(a,1))]. given #150 (T,wt=8): 154 c2 v ((x ^ c1) v y) = c2 v y. [para(153(a,1),3(a,1,1)),flip(a)]. given #151 (T,wt=8): 157 c2 != 1 | x ^ c1 != 0 | c2' = x ^ c1. [para(153(a,1),10(a,1)),rewrite([54(7)])]. given #152 (T,wt=3): 2144 c2 != 1 | c2' = 0. [para(83(a,1),157(b,1)),rewrite([83(11)]),xx(b)]. given #153 (T,wt=8): 159 c2 v (x v (y ^ c1)) = x v c2. [para(153(a,1),17(a,1,2)),flip(a)]. given #154 (A,wt=27): 60 x ^ (y v ((x ^ z) v (z ^ (u v (y v w))))) = x ^ (y v (z ^ (x v (u v w)))). [para(17(a,1),12(a,1,2,2,2,2))]. given #155 (T,wt=8): 166 (x v c1) ^ (x v c2) = x v c1. [para(160(a,1),21(a,1,2,2))]. given #156 (T,wt=8): 167 c2 v ((c1 ^ x) v y) = c2 v y. [para(155(a,1),3(a,1,1)),flip(a)]. given #157 (T,wt=8): 168 c2 != 1 | c1 ^ x != 0 | c2' = c1 ^ x. [para(155(a,1),10(a,1)),rewrite([19(7),53(7)])]. given #158 (T,wt=8): 170 c2 v (x v (c1 ^ y)) = x v c2. [para(155(a,1),17(a,1,2)),flip(a)]. given #159 (A,wt=23): 61 x ^ ((x ^ y) v (z v (y ^ (z v u)))) = x ^ (z v (y ^ (x v u))). [para(17(a,1),12(a,1,2))]. given #160 (T,wt=8): 184 c1 ^ (x v (y v (c2 v z))) = c1. [para(3(a,1),134(a,1,2))]. given #161 (T,wt=8): 188 c1 ^ (x v (y v (z v c2))) = c1. [para(3(a,1),136(a,1,2,2))]. given #162 (T,wt=8): 203 c2 v (x ^ (y ^ (z ^ c1))) = c2. [para(5(a,1),156(a,1,2,2))]. given #163 (T,wt=8): 208 c2 v x != 1 | c1 != 0 | c1' = c2 v x. [para(161(a,1),10(a,1)),rewrite([116(8)])]. given #164 (A,wt=13): 63 x ^ (y v ((x v z) ^ (x v u))) = x. [back_rewrite(47),rewrite([56(6)]),flip(a)]. given #165 (T,wt=3): 2591 c1 != 0 | c1' = 1. [para(8(a,1),208(a,1)),rewrite([8(12)]),xx(a)]. given #166 (T,wt=8): 220 x v c2 != 1 | c1 != 0 | c1' = x v c2. [para(165(a,1),10(a,1)),rewrite([121(8)])]. given #167 (T,wt=8): 224 (c1 v x) ^ (x v c2) = c1 v x. [para(165(a,1),21(a,1,2))]. given #168 (T,wt=8): 231 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(53(a,1),26(a,1,2)),rewrite([2(5)])]. given #169 (A,wt=21): 68 x ^ (y v (x' ^ (y v z))) = x ^ (y v (x' ^ (x v z))). [back_rewrite(50),rewrite([65(5)])]. given #170 (T,wt=8): 234 (x ^ c1) v (x ^ c2) = x ^ c2. [para(78(a,1),26(a,1,2)),rewrite([2(5)])]. given #171 (T,wt=8): 236 c2 v (x ^ (y ^ (c1 ^ z))) = c2. [para(5(a,1),171(a,1,2))]. given #172 (T,wt=8): 242 (x v c1) ^ (c2 v x) = x v c1. [para(212(a,1),20(a,1,2))]. given #173 (T,wt=8): 268 (c2 ^ x) v (x ^ c1) = c2 ^ x. [para(54(a,1),27(a,1,2))]. given #174 (A,wt=19): 69 x ^ (y v (z ^ (x v (y ^ u)))) = x ^ (y v (z ^ x)). [back_rewrite(48),rewrite([67(5)]),flip(a)]. given #175 (T,wt=8): 269 (c1 ^ x) v (x ^ c1) = c1 ^ x. [para(78(a,1),27(a,1,2))]. given #176 (T,wt=7): 3048 (c1 ^ x) v (x ^ c1)' = 1. [para(269(a,1),349(a,1,2)),rewrite([2(6)])]. given #177 (T,wt=8): 331 c2 != 1 | x ^ c1 != 0 | (x ^ c1)' = c2. [para(153(a,1),36(a,1)),rewrite([4(7),54(7)])]. given #178 (T,wt=8): 333 c2 != 1 | c1 ^ x != 0 | (c1 ^ x)' = c2. [para(155(a,1),36(a,1)),rewrite([4(7),19(7),53(7)])]. given #179 (A,wt=11): 73 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),19(a,1,2)),flip(a)]. given #180 (T,wt=8): 337 c2 v x != 1 | c1 != 0 | (c2 v x)' = c1. [para(161(a,1),36(a,1)),rewrite([4(8),116(8)])]. given #181 (T,wt=8): 338 x v c2 != 1 | c1 != 0 | (x v c2)' = c1. [para(165(a,1),36(a,1)),rewrite([4(8),121(8)])]. given #182 (T,wt=8): 397 c2 ^ (x ^ c1)' != 0 | x ^ c1 = c2. [para(357(a,1),36(a,1)),rewrite([4(8),329(14)]),xx(a)]. given #183 (T,wt=8): 404 c2 ^ (c1 ^ x)' != 0 | c1 ^ x = c2. [para(392(a,1),36(a,1)),rewrite([4(8),329(14)]),xx(a)]. given #184 (A,wt=9): 74 x v (y ^ (x ^ z)) = x. [para(19(a,1),7(a,1,2))]. given #185 (T,wt=8): 565 c1 ^ ((c2 ^ (c1 v x))' ^ y) = 0. [para(518(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #186 (T,wt=8): 567 c1 ^ (c2 ^ (x v (c1 v y)))' = 0. [para(17(a,1),518(a,1,2,1,2))]. given #187 (T,wt=8): 568 c1 ^ (x ^ (c2 ^ (c1 v y))') = 0. [para(518(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #188 (T,wt=8): 570 c1 ^ (c2 ^ (x v (y v c1)))' = 0. [para(3(a,1),564(a,1,2,1,2))]. given #189 (A,wt=29): 76 x ^ (y v ((z ^ (x ^ u)) v (z ^ (u ^ (y v w))))) = x ^ (y v (z ^ (u ^ (x v w)))). [para(19(a,1),12(a,1,2,2,1)),rewrite([5(5),5(11)])]. given #190 (T,wt=8): 571 c1 ^ ((c2 ^ (x v c1))' ^ y) = 0. [para(564(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #191 (T,wt=8): 573 c1 ^ (x ^ (c2 ^ (y v c1))') = 0. [para(564(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #192 (T,wt=8): 777 c1 ^ (x v (c2 ^ (c1 v y)))' = 0. [para(62(a,1),350(a,1,2)),rewrite([4(8)])]. given #193 (T,wt=8): 778 c1 ^ (x v (c2 ^ (y v c1)))' = 0. [para(243(a,1),350(a,1,2)),rewrite([4(8)])]. given #194 (A,wt=27): 77 x ^ (y ^ (z v ((x ^ u) v (u ^ (z v w))))) = y ^ (x ^ (z v (u ^ (x v w)))). [para(12(a,1),19(a,1,2)),flip(a)]. given #195 (T,wt=8): 779 c1 ^ ((c2 ^ (c1 v x)) v y)' = 0. [para(244(a,1),350(a,1,2)),rewrite([4(8)])]. given #196 (T,wt=8): 802 (c2 ^ (c1 v x)) v (y v c1') = 1. [para(244(a,1),352(a,1,2,1)),rewrite([3(8)])]. given #197 (T,wt=8): 1055 c1 ^ ((c2 ^ (x v c1)) v y)' = 0. [para(406(a,1),350(a,1,2)),rewrite([4(8)])]. given #198 (T,wt=8): 1056 (c2 ^ (x v c1)) v (y v c1') = 1. [para(406(a,1),352(a,1,2,1)),rewrite([3(8)])]. given #199 (A,wt=13): 84 x ^ ((x ^ y) v (y ^ z)) = y ^ x. [para(65(a,1),12(a,1,2,2,2,2)),rewrite([65(5),65(8),73(7)])]. given #200 (T,wt=8): 1077 (c1 v (c2 ^ x)) ^ (c2' ^ y) = 0. [para(1063(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #201 (T,wt=8): 1079 (c1 v (c2 ^ x)) ^ (y ^ c2') = 0. [para(1063(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #202 (T,wt=8): 1080 (c1 v (x ^ (c2 ^ y))) ^ c2' = 0. [para(19(a,1),1063(a,1,1,2))]. given #203 (T,wt=8): 1214 (c1 v (x ^ c2)) ^ (c2' ^ y) = 0. [para(1069(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #204 (A,wt=9): 86 x ^ (y v (z v x)) = x. [para(3(a,1),20(a,1,2))]. given #205 (T,wt=8): 1215 (c1 v (x ^ (y ^ c2))) ^ c2' = 0. [para(5(a,1),1069(a,1,1,2))]. given #206 (T,wt=8): 1217 (c1 v (x ^ c2)) ^ (y ^ c2') = 0. [para(1069(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #207 (T,wt=8): 1225 c2' ^ ((c1 v (c2 ^ x)) ^ y) = 0. [para(1076(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #208 (T,wt=8): 1227 c2' ^ (x ^ (c1 v (c2 ^ y))) = 0. [para(1076(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #209 (A,wt=11): 87 x ^ ((y v x) ^ z) = x ^ z. [para(20(a,1),5(a,1,1)),flip(a)]. given #210 (T,wt=5): 3801 c2' ^ (x ^ c1) = 0. [para(9(a,1),1227(a,1,2,2,2)),rewrite([2(5),65(5)])]. given #211 (T,wt=7): 3872 c2' ^ (x ^ (c1 ^ y)) = 0. [para(3801(a,1),5(a,1,1)),rewrite([83(2),5(6)]),flip(a)]. given #212 (T,wt=7): 3873 c2' ^ (x ^ (y ^ c1)) = 0. [para(5(a,1),3801(a,1,2))]. given #213 (T,wt=8): 1228 c2' ^ (c1 v (x ^ (c2 ^ y))) = 0. [para(19(a,1),1076(a,1,2,2))]. given #214 (A,wt=13): 88 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(20(a,1),5(a,1)),flip(a)]. given #215 (T,wt=8): 1242 c2' ^ ((c1 v (x ^ c2)) ^ y) = 0. [para(1213(a,1),5(a,1,1)),rewrite([83(2)]),flip(a)]. given #216 (T,wt=8): 1243 c2' ^ (c1 v (x ^ (y ^ c2))) = 0. [para(5(a,1),1213(a,1,2,2))]. given #217 (T,wt=8): 1245 c2' ^ (x ^ (c1 v (y ^ c2))) = 0. [para(1213(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #218 (T,wt=8): 1385 c2 v ((c1 v (c2 ^ x))' v y) = 1. [para(1375(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #219 (A,wt=9): 89 x ^ (x ^ y) = x ^ y. [para(7(a,1),20(a,1,2)),rewrite([4(2)])]. given #220 (T,wt=8): 1389 c2 v (x v (c1 v (c2 ^ y))') = 1. [para(1375(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #221 (T,wt=8): 1390 c2 v (c1 v (x ^ (c2 ^ y)))' = 1. [para(19(a,1),1375(a,1,2,1,2))]. given #222 (T,wt=8): 1398 c2 v ((c1 v (x ^ c2))' v y) = 1. [para(1386(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #223 (T,wt=8): 1399 c2 v (c1 v (x ^ (y ^ c2)))' = 1. [para(5(a,1),1386(a,1,2,1,2))]. given #224 (A,wt=13): 90 x ^ (y v ((z v x) ^ (x v u))) = x. [para(20(a,1),12(a,1,2,2,1)),rewrite([56(6)]),flip(a)]. given #225 (T,wt=8): 1402 c2 v (x v (c1 v (y ^ c2))') = 1. [para(1386(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #226 (T,wt=8): 1477 (c2 ^ (c1 v x)) v (c1' v y) = 1. [para(1447(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #227 (T,wt=8): 1480 (c2 ^ (x v (c1 v y))) v c1' = 1. [para(17(a,1),1447(a,1,1,2))]. given #228 (T,wt=8): 1489 (c2 ^ (x v c1)) v (c1' v y) = 1. [para(1454(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #229 (A,wt=13): 91 (x v y) ^ (x v (z v y)) = x v y. [para(17(a,1),20(a,1,2))]. given #230 (T,wt=8): 1490 (c2 ^ (x v (y v c1))) v c1' = 1. [para(3(a,1),1454(a,1,1,2))]. given #231 (T,wt=8): 1652 c1' v ((c2 ^ (c1 v x)) v y) = 1. [para(1476(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #232 (T,wt=8): 1653 c1' v (x v (c2 ^ (c1 v y))) = 1. [para(1476(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #233 (T,wt=5): 4310 c1' v (x v c2) = 1. [para(8(a,1),1653(a,1,2,2,2)),rewrite([4(5),64(5)])]. given #234 (A,wt=11): 92 x ^ (y ^ (z v x)) = y ^ x. [para(20(a,1),19(a,1,2)),flip(a)]. given #235 (T,wt=7): 4323 c1' v (x v (c2 v y)) = 1. [para(4310(a,1),3(a,1,1)),rewrite([71(2),3(6)]),flip(a)]. given #236 (T,wt=7): 4324 c1' v (x v (y v c2)) = 1. [para(3(a,1),4310(a,1,2))]. given #237 (T,wt=8): 1654 c1' v (c2 ^ (x v (c1 v y))) = 1. [para(17(a,1),1476(a,1,2,2))]. given #238 (T,wt=8): 1662 c1' v ((c2 ^ (x v c1)) v y) = 1. [para(1488(a,1),3(a,1,1)),rewrite([71(2)]),flip(a)]. given #239 (A,wt=12): 93 1 != x | x ^ y != 0 | x' = x ^ y. [back_rewrite(38),rewrite([89(4)])]. given #240 (T,wt=3): 4444 c1 != 1 | c1' = 0. [para(117(a,1),93(b,1)),rewrite([117(12)]),flip(a),xx(b)]. given #241 (T,wt=3): 4447 c2' != 1 | c2 = 0. [para(1076(a,1),93(b,1)),rewrite([329(10),1076(15)]),flip(a),xx(b)]. given #242 (T,wt=4): 4440 c1 != 1 | c1 != 0 | c1' = c1. [para(13(a,1),93(b,1)),rewrite([13(11)]),flip(a)]. given #243 (T,wt=5): 4446 x' != 1 | 0 = x. [para(350(a,1),93(b,1)),rewrite([329(8),350(9)]),flip(a),flip(c),xx(b)]. given #244 (A,wt=9): 98 x ^ (y ^ x) = y ^ x. [para(28(a,1),5(a,2,2)),rewrite([4(2)])]. given #245 (F,wt=6): 4452 (c1 ^ (c1' v c2'))' != 1. [ur(4446,b,251,a(flip))]. given #246 (T,wt=8): 1663 c1' v (c2 ^ (x v (y v c1))) = 1. [para(3(a,1),1488(a,1,2,2))]. given #247 (T,wt=8): 1664 c1' v (x v (c2 ^ (y v c1))) = 1. [para(1488(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #248 (T,wt=8): 2091 c1' ^ (c2 v x) != 0 | c2 v x = c1. [para(271(a,1),59(a,1)),rewrite([329(13)]),flip(c),xx(a)]. given #249 (T,wt=3): 4486 c1' != 0 | c1 = 1. [para(8(a,1),2091(a,1,2)),rewrite([4(4),64(4),8(8)]),flip(b)]. given #250 (A,wt=9): 100 x v (x v y) = x v y. [para(29(a,1),3(a,1,1)),flip(a)]. given #251 (T,wt=8): 2139 (x ^ c1) v (y v c2) = y v c2. [para(57(a,1),154(a,2)),rewrite([1969(8)])]. given #252 (T,wt=8): 2142 c2 != 1 | c1 ^ x != 0 | c2' = x ^ c1. [para(4(a,1),157(b,1))]. given #253 (T,wt=8): 2346 (c1 ^ x) v (y v c2) = y v c2. [para(57(a,1),167(a,2)),rewrite([1969(8)])]. given #254 (T,wt=8): 2351 c2 != 1 | x ^ c1 != 0 | c2' = c1 ^ x. [para(4(a,1),168(b,1))]. given #255 (A,wt=9): 102 x v (y v x) = y v x. [para(29(a,1),3(a,2,2)),rewrite([2(2)])]. given #256 (T,wt=8): 2590 x v c2 != 1 | c1 != 0 | c1' = c2 v x. [para(2(a,1),208(a,1))]. given #257 (T,wt=8): 2614 c2 v x != 1 | c1 != 0 | c1' = x v c2. [para(2(a,1),220(a,1))]. given #258 (T,wt=8): 2616 (c1 v x) ^ (c2 v x) = c1 v x. [para(2(a,1),224(a,1,2))]. given #259 (T,wt=8): 2617 (x v c2) ^ (c1 v x) = c1 v x. [para(224(a,1),4(a,1)),flip(a)]. given #260 (A,wt=17): 104 x ^ (y v (z ^ (x v y))) = x ^ (y v (z ^ x)). [para(29(a,1),12(a,1,2,2,2,2)),rewrite([67(5)]),flip(a)]. given #261 (T,wt=8): 2643 (x ^ c1) v (c2 ^ x) = c2 ^ x. [para(4(a,1),231(a,1,1))]. given #262 (T,wt=8): 2644 (c1 ^ x) v (x ^ c2) = c2 ^ x. [para(4(a,1),231(a,1,2))]. given #263 (T,wt=7): 4816 (c2 ^ x) v (x ^ c2)' = 1. [para(2644(a,1),349(a,1,2)),rewrite([2(6)])]. given #264 (T,wt=8): 2645 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),231(a,1,1))]. given #265 (A,wt=17): 105 x ^ (y v ((y v z) ^ (x v z))) = x ^ (y v z). [back_rewrite(99),rewrite([100(7)])]. given #266 (T,wt=8): 2653 c1 v (c2 ^ (x v c1)) = c2 ^ (x v c1). [para(20(a,1),231(a,1,1))]. given #267 (T,wt=8): 2923 (c2 v x) ^ (x v c1) = x v c1. [para(242(a,1),4(a,1)),flip(a)]. given #268 (T,wt=8): 2925 c2 ^ (c1 v (c2 ^ x)) = c1 v (c2 ^ x). [para(7(a,1),242(a,1,2)),rewrite([2(4),4(6),2(10)])]. given #269 (T,wt=7): 5025 c2 v (x ^ (c1 v (c2 ^ y))) = c2. [para(2925(a,1),74(a,1,2,2))]. given #270 (A,wt=13): 106 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),21(a,1,1))]. given #271 (T,wt=7): 5034 c2 v (x ^ (c1 v (y ^ c2))) = c2. [para(4(a,1),5025(a,1,2,2,2))]. given #272 (T,wt=7): 5035 c2 v ((c1 v (c2 ^ x)) ^ y) = c2. [para(4(a,1),5025(a,1,2))]. given #273 (T,wt=7): 5115 c2 v ((c1 v (x ^ c2)) ^ y) = c2. [para(4(a,1),5034(a,1,2))]. given #274 (T,wt=8): 2931 c2 ^ (c1 v (x ^ c2)) = c1 v (x ^ c2). [para(26(a,1),242(a,1,2)),rewrite([2(4),4(6),2(10)])]. given #275 (A,wt=13): 107 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),21(a,1,2)),rewrite([3(3)])]. given #276 (T,wt=7): 5250 (x ^ c1)' v (y v c2) = 1. [para(357(a,1),107(a,1,1)),rewrite([64(8),357(11)])]. given #277 (T,wt=7): 5251 (c1 ^ x)' v (y v c2) = 1. [para(392(a,1),107(a,1,1)),rewrite([64(8),392(11)])]. given #278 (T,wt=8): 3086 c2 != 1 | c1 ^ x != 0 | (x ^ c1)' = c2. [para(4(a,1),331(b,1))]. given #279 (T,wt=8): 3088 c2 != 1 | x ^ c1 != 0 | (c1 ^ x)' = c2. [para(4(a,1),333(b,1))]. given #280 (A,wt=19): 108 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),21(a,1,1)),rewrite([3(5),3(8)])]. given #281 (T,wt=8): 3115 (c2 v x) ^ (y ^ c1) = y ^ c1. [para(73(a,1),131(a,2)),rewrite([3095(8)])]. given #282 (T,wt=8): 3116 (x v c2) ^ (y ^ c1) = y ^ c1. [para(73(a,1),137(a,2)),rewrite([3095(8)])]. given #283 (T,wt=8): 3127 x v c2 != 1 | c1 != 0 | (c2 v x)' = c1. [para(2(a,1),337(a,1))]. given #284 (T,wt=8): 3129 c2 v x != 1 | c1 != 0 | (x v c2)' = c1. [para(2(a,1),338(a,1))]. given #285 (A,wt=17): 109 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(21(a,1),5(a,1,1)),flip(a)]. given #286 (T,wt=8): 3131 c2 ^ (c1 ^ x)' != 0 | x ^ c1 = c2. [para(4(a,1),397(a,1,2,1))]. given #287 (T,wt=8): 3133 c2 ^ (x ^ c1)' != 0 | c1 ^ x = c2. [para(4(a,1),404(a,1,2,1))]. given #288 (T,wt=8): 4325 c1' ^ (x v c2) != 0 | x v c2 = c1. [para(4310(a,1),10(a,1)),rewrite([329(13)]),flip(c),xx(a)]. given #289 (T,wt=8): 4443 c1 != 1 | c1 ^ x != 0 | c1' = c1 ^ x. [para(53(a,1),93(b,1)),rewrite([53(13)]),flip(a)]. given #290 (A,wt=19): 111 x ^ (y v ((y v z) ^ (x v (z v u)))) = x ^ (y v z). [para(21(a,1),12(a,1,2,2,2)),rewrite([2(4),26(4),100(2)]),flip(a)]. given #291 (T,wt=8): 4445 c1 != 1 | x ^ c1 != 0 | c1' = x ^ c1. [para(78(a,1),93(b,1)),rewrite([78(13)]),flip(a)]. given #292 (T,wt=8): 4484 c1' ^ (x v c2) != 0 | c2 v x = c1. [para(2(a,1),2091(a,1,2))]. given #293 (T,wt=8): 4485 (c2 v x) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),2091(a,1))]. given #294 (T,wt=8): 4806 (x ^ c2) v (c1 ^ x) = c2 ^ x. [para(2644(a,1),2(a,1)),flip(a)]. given #295 (A,wt=19): 112 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(17(a,1),21(a,1,1)),rewrite([3(4)])]. given #296 (T,wt=8): 4947 x ^ (c1 v (x ^ c2)) = c2 ^ x. [para(2653(a,1),12(a,2,2)),rewrite([29(7),4(6),13(6),2(5),100(6),73(10)])]. given #297 (T,wt=8): 4954 x ^ (c1 v (c2 ^ x)) = c2 ^ x. [para(2653(a,1),42(a,2,2)),rewrite([29(7),4(6),13(6),2(5),100(6),73(10)])]. given #298 (T,wt=8): 5046 c2 v (x ^ (c1 v (c2 ^ y)))' = 1. [para(5025(a,1),349(a,1,2)),rewrite([2(8)])]. given #299 (T,wt=8): 5127 c2 v (x ^ (c1 v (y ^ c2)))' = 1. [para(5034(a,1),349(a,1,2)),rewrite([2(8)])]. given #300 (A,wt=15): 113 (x v y) ^ (x v (z v (y v u))) = x v y. [para(17(a,1),21(a,1,2,2))]. given #301 (T,wt=8): 5157 c2 v ((c1 v (c2 ^ x)) ^ y)' = 1. [para(5035(a,1),349(a,1,2)),rewrite([2(8)])]. given #302 (T,wt=8): 5187 c2 v ((c1 v (x ^ c2)) ^ y)' = 1. [para(5115(a,1),349(a,1,2)),rewrite([2(8)])]. given #303 (T,wt=8): 5269 (c1 v (c2 ^ x))' v (y v c2) = 1. [para(1375(a,1),107(a,1,1)),rewrite([64(10),1375(15)])]. given #304 (T,wt=8): 5270 (c1 v (x ^ c2))' v (y v c2) = 1. [para(1386(a,1),107(a,1,1)),rewrite([64(10),1386(15)])]. given #305 (A,wt=17): 114 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(21(a,1),19(a,1,2)),flip(a)]. given #306 (T,wt=8): 5483 c1' ^ (c2 v x) != 0 | x v c2 = c1. [para(2(a,1),4325(a,1,2))]. given #307 (T,wt=8): 5485 (x v c2) ^ c1' != 0 | x v c2 = c1. [para(4(a,1),4325(a,1))]. given #308 (T,wt=8): 5486 c1 != 1 | x ^ c1 != 0 | c1' = c1 ^ x. [para(4(a,1),4443(b,1))]. given #309 (T,wt=8): 5569 c1 != 1 | c1 ^ x != 0 | c1' = x ^ c1. [para(4(a,1),4445(b,1))]. given #310 (A,wt=10): 115 c2 ^ (x ^ (c1 ^ y)) = x ^ (c1 ^ y). [para(53(a,1),5(a,2,2)),rewrite([19(5),5(4)])]. given #311 (T,wt=8): 5571 (x v c2) ^ c1' != 0 | c2 v x = c1. [para(4(a,1),4484(a,1))]. given #312 (T,wt=8): 5729 c2 ^ (x ^ (c1 v (x ^ c2))') = 0. [para(4947(a,1),350(a,1,2)),rewrite([4(8),5(8)])]. given #313 (T,wt=8): 5730 c1 v ((x ^ c2) v (c2 ^ x)') = 1. [para(4947(a,1),352(a,1,2,1)),rewrite([3(8)])]. given #314 (T,wt=8): 5995 (c2 v x) ^ c1' != 0 | x v c2 = c1. [para(4(a,1),5483(a,1))]. given #315 (A,wt=21): 118 c1 ^ (x v ((c1 ^ y) v (c2 ^ (y ^ (x v z))))) = c1 ^ (x v (c2 ^ (y ^ (c1 v z)))). [para(53(a,1),12(a,1,2,2,1)),rewrite([5(7),5(16)])]. given #316 (T,wt=9): 132 c1 ^ (x v ((c2 v y) ^ (c1 v z))) = c1. [para(116(a,1),12(a,1,2,2,1)),rewrite([56(9)]),flip(a)]. given #317 (T,wt=9): 138 c1 ^ (x v ((y v c2) ^ (c1 v z))) = c1. [para(121(a,1),12(a,1,2,2,1)),rewrite([56(9)]),flip(a)]. given #318 (T,wt=9): 225 x v (y ^ (z ^ x)) = x. [para(5(a,1),26(a,1,2))]. given #319 (T,wt=9): 245 c1 ^ (x v (y v (c2 ^ (c1 v z)))) = c1. [para(3(a,1),62(a,1,2))]. given #320 (A,wt=19): 119 c1 ^ (x v ((c2 ^ y) v (y ^ (x v z)))) = c1 ^ (x v (y ^ (c2 v z))). [para(12(a,1),53(a,1,2)),rewrite([53(8)]),flip(a)]. given #321 (T,wt=9): 248 c1 ^ (x v (c2 ^ (y v (c1 v z)))) = c1. [para(17(a,1),62(a,1,2,2,2))]. given #322 (T,wt=9): 255 x v (y v (x' v z)) = 1. [para(72(a,1),17(a,1,2)),rewrite([79(2)]),flip(a)]. given #323 (T,wt=9): 256 x v ((x ^ y)' v z) = 1. [para(72(a,1),24(a,1,2)),rewrite([79(2)]),flip(a)]. given #324 (T,wt=9): 281 x v (y v (y v x)') = 1. [para(2(a,1),31(a,1,2,2,1))]. given #325 (A,wt=10): 120 c1 ^ (x ^ (c2 ^ y)) = x ^ (c1 ^ y). [para(53(a,1),19(a,1,2)),flip(a)]. given #326 (T,wt=9): 289 x v (y v (z v x')) = 1. [para(3(a,1),80(a,1,2))]. given #327 (T,wt=9): 292 x v (y v (x ^ z)') = 1. [para(80(a,1),24(a,1,2)),rewrite([79(2)]),flip(a)]. given #328 (T,wt=9): 295 x ^ (y ^ (x' ^ z)) = 0. [para(85(a,1),19(a,1,2)),rewrite([94(2)]),flip(a)]. given #329 (T,wt=9): 296 x ^ ((x v y)' ^ z) = 0. [para(85(a,1),22(a,1,2)),rewrite([94(2)]),flip(a)]. given #330 (A,wt=16): 123 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))). [para(117(a,1),12(a,1,2,2,1)),rewrite([65(7)]),flip(a)]. ============================== PROOF ================================= % Proof 1 at 1.90 (+ 0.02) seconds. % Length of proof is 42. % Level of proof is 11. % Maximum clause weight is 23.000. % Given clauses 330. 1 (all x all y (x ^ y = x -> x' v y' = x')) # 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 ^ (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 = c1. [deny(1)]. 14 c1' != c1' v c2'. [deny(1)]. 15 c1' v c2' != c1'. [copy(14),flip(a)]. 19 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite([5(2)])]. 24 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. 26 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 30 x v (x' v y) = 1 v y. [para(8(a,1),3(a,1,1)),flip(a)]. 32 x ^ 1 = x. [para(8(a,1),6(a,1,2))]. 33 x ^ (x' ^ y) = 0 ^ y. [para(9(a,1),5(a,1,1)),flip(a)]. 35 x v 0 = x. [para(9(a,1),7(a,1,2))]. 53 c1 ^ (c2 ^ x) = c1 ^ x. [para(13(a,1),5(a,1,1)),flip(a)]. 64 1 ^ x = x. [para(32(a,1),4(a,1)),flip(a)]. 65 0 v x = x. [para(35(a,1),2(a,1)),flip(a)]. 71 1 v x = 1. [para(64(a,1),6(a,1))]. 72 x v (x' v y) = 1. [back_rewrite(30),rewrite([71(5)])]. 79 x v 1 = 1. [para(71(a,1),2(a,1)),flip(a)]. 83 0 ^ x = 0. [para(65(a,1),6(a,1,2))]. 85 x ^ (x' ^ y) = 0. [back_rewrite(33),rewrite([83(5)])]. 117 c1 ^ c2' = 0. [para(9(a,1),53(a,1,2)),rewrite([4(3),83(3)]),flip(a)]. 123 c1 ^ (x v (c2' ^ (c1 v y))) = c1 ^ (x v (c2' ^ (x v y))). [para(117(a,1),12(a,1,2,2,1)),rewrite([65(7)]),flip(a)]. 175 x v (x ^ y)' = 1. [para(8(a,1),24(a,1,2)),rewrite([79(2)]),flip(a)]. 231 (c1 ^ x) v (c2 ^ x) = c2 ^ x. [para(53(a,1),26(a,1,2)),rewrite([2(5)])]. 251 c1 ^ (c1' v c2') != 0. [ur(10,a,72,a,c,15,a(flip))]. 352 x v (y ^ x)' = 1. [para(4(a,1),175(a,1,2,1))]. 794 (c2 ^ x) v (c1 ^ x)' = 1. [para(53(a,1),352(a,1,2,1))]. 1447 (c2 ^ (c1 v x)) v c1' = 1. [para(6(a,1),794(a,1,2,1))]. 1476 c1' v (c2 ^ (c1 v x)) = 1. [para(1447(a,1),2(a,1)),flip(a)]. 2645 c1 v (c2 ^ (c1 v x)) = c2 ^ (c1 v x). [para(6(a,1),231(a,1,1))]. 6686 c1 ^ (c1' v c2') = 0. [para(1476(a,1),123(a,2,2,2,2)),rewrite([2645(11),19(10),85(10),2(5),65(5),9(4),4(8),64(8)]),flip(a)]. 6687 $F. [resolve(6686,a,251,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=330. Generated=47926. Kept=6683. proofs=1. Usable=327. Sos=6001. Demods=4693. Limbo=78, Disabled=288. Hints=0. Kept_by_rule=0, Deleted_by_rule=31. Forward_subsumed=41212. Back_subsumed=49. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=4872 (6 lex), Back_demodulated=225. Back_unit_deleted=0. Demod_attempts=832339. Demod_rewrites=132739. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=23384. Nonunit_bsub_feature_tests=7976. Megabytes=11.00. User_CPU=1.90, System_CPU=0.02, Wall_clock=2. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5150 exit (max_proofs) Tue Nov 3 09:47:46 2009