============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 4151 was started by mccune on cleo.thornwood, Wed Nov 22 11:33:00 2006 The command was "/home/mccune/bin/prover9 -f lt.in H33-H34.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 H33-H34.in formulas(sos). x ^ (y v (x ^ (z v u))) = x ^ (y v ((x v y) ^ (z v u))) # label(H33). end_of_list. formulas(goals). x ^ (y v (z ^ u)) = x ^ (y v (z ^ (y v (u ^ (y v z))))) # answer(H34). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x ^ (y v (z ^ u)) = x ^ (y v (z ^ (y v (u ^ (y v z))))) # answer(H34) # 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 ^ (y v (x ^ (z v u))) = x ^ (y v ((x v y) ^ (z v u))) # label(H33). [assumption]. c1 ^ (c2 v (c3 ^ (c2 v (c4 ^ (c2 v c3))))) != c1 ^ (c2 v (c3 ^ c4)) # answer(H34). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, v, ^ ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). 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]. 9 x ^ (y v ((x v y) ^ (z v u))) = x ^ (y v (x ^ (z v u))). [copy(8),flip(a)]. 10 c1 ^ (c2 v (c3 ^ (c2 v (c4 ^ (c2 v c3))))) != c1 ^ (c2 v (c3 ^ c4)) # answer(H34). [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]. 9 x ^ (y v ((x v y) ^ (z v u))) = x ^ (y v (x ^ (z v u))). [copy(8),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: 11 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: 13 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=21): 9 x ^ (y v ((x v y) ^ (z v u))) = x ^ (y v (x ^ (z v u))). [copy(8),flip(a)]. given #8 (I,wt=21): 10 c1 ^ (c2 v (c3 ^ (c2 v (c4 ^ (c2 v c3))))) != c1 ^ (c2 v (c3 ^ c4)) # answer(H34). [deny(1)]. given #9 (T,wt=5): 23 x ^ x = x. [para(7(a,1),6(a,1,2))]. given #10 (T,wt=5): 24 x v x = x. [para(6(a,1),7(a,1,2))]. given #11 (A,wt=11): 12 x v (y v z) = y v (x v z). [para(2(a,1),3(a,1,1)),rewrite(3(2))]. given #12 (F,wt=7): 15 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. given #13 (F,wt=7): 21 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. given #14 (T,wt=9): 34 x ^ (x ^ y) = x ^ y. [para(23(a,1),5(a,1,1)),flip(a)]. given #15 (T,wt=9): 36 x ^ (y ^ x) = y ^ x. [para(23(a,1),5(a,2,2)),rewrite(4(2))]. given #16 (A,wt=11): 14 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. given #17 (F,wt=9): 37 x v (x v y) = x v y. [para(24(a,1),3(a,1,1)),flip(a)]. given #18 (F,wt=9): 39 x v (y v x) = y v x. [para(24(a,1),3(a,2,2)),rewrite(2(2))]. given #19 (T,wt=9): 40 x ^ (y v (x v z)) = x. [para(12(a,1),6(a,1,2))]. given #20 (T,wt=9): 42 x ^ (y v (z v x)) = x. [para(3(a,1),15(a,1,2))]. given #21 (A,wt=13): 16 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. given #22 (F,wt=9): 48 x v (y ^ (z ^ x)) = x. [para(5(a,1),21(a,1,2))]. given #23 (F,wt=9): 55 x v (y ^ (x ^ z)) = x. [para(14(a,1),7(a,1,2))]. given #24 (T,wt=11): 17 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. given #25 (T,wt=11): 19 x v ((x ^ y) v z) = x v z. [para(7(a,1),3(a,1,1)),flip(a)]. given #26 (A,wt=13): 18 x ^ (y ^ ((x ^ y) v z)) = x ^ y. [para(6(a,1),5(a,1)),flip(a)]. given #27 (F,wt=11): 41 x v (y v (x ^ z)) = y v x. [para(7(a,1),12(a,1,2)),flip(a)]. given #28 (F,wt=11): 43 x ^ ((y v x) ^ z) = x ^ z. [para(15(a,1),5(a,1,1)),flip(a)]. given #29 (T,wt=11): 46 x v ((y ^ x) v z) = x v z. [para(21(a,1),3(a,1,1)),flip(a)]. given #30 (T,wt=11): 49 x v (y v (z ^ x)) = y v x. [para(21(a,1),12(a,1,2)),flip(a)]. given #31 (A,wt=13): 20 x v (y v ((x v y) ^ z)) = x v y. [para(7(a,1),3(a,1)),flip(a)]. given #32 (F,wt=11): 54 x ^ (y ^ (x v z)) = y ^ x. [para(6(a,1),14(a,1,2)),flip(a)]. given #33 (F,wt=11): 56 x ^ (y ^ (z v x)) = y ^ x. [para(15(a,1),14(a,1,2)),flip(a)]. given #34 (T,wt=11): 63 x ^ (y v (z v (x v u))) = x. [para(3(a,1),40(a,1,2))]. given #35 (T,wt=11): 67 x ^ (y v (z v (u v x))) = x. [para(3(a,1),42(a,1,2,2))]. given #36 (A,wt=13): 22 (x ^ y) v (x ^ (y ^ z)) = x ^ y. [para(5(a,1),7(a,1,2))]. given #37 (F,wt=11): 79 (x v y) ^ (y v x) = x v y. [para(39(a,1),16(a,1,2))]. given #38 (F,wt=11): 82 x v (y ^ (z ^ (u ^ x))) = x. [para(5(a,1),48(a,1,2,2))]. given #39 (T,wt=11): 89 x v (y ^ (z ^ (x ^ u))) = x. [para(5(a,1),55(a,1,2))]. given #40 (T,wt=11): 93 (x v y) ^ (z ^ x) = z ^ x. [para(36(a,1),17(a,2)),rewrite(53(4))]. given #41 (A,wt=21): 25 x ^ (y v ((y v x) ^ (z v u))) = x ^ (y v (x ^ (z v u))). [para(2(a,1),9(a,1,2,2,1))]. given #42 (F,wt=11): 100 (x ^ y) v (z v x) = z v x. [para(39(a,1),19(a,2)),rewrite(61(4))]. given #43 (F,wt=11): 117 (x v y) ^ (z ^ y) = z ^ y. [para(36(a,1),43(a,2)),rewrite(53(4))]. given #44 (T,wt=11): 128 (x ^ y) v (z v y) = z v y. [para(39(a,1),46(a,2)),rewrite(61(4))]. given #45 (T,wt=11): 191 (x ^ y) v (y ^ x) = x ^ y. [para(36(a,1),22(a,1,2))]. given #46 (A,wt=29): 26 (x v y) ^ (z v ((x v (y v z)) ^ (u v v))) = (x v y) ^ (z v ((x v y) ^ (u v v))). [para(3(a,1),9(a,1,2,2,1))]. given #47 (F,wt=13): 44 x ^ (y ^ (z v (x ^ y))) = x ^ y. [para(15(a,1),5(a,1)),flip(a)]. given #48 (F,wt=13): 45 (x v y) ^ (x v (z v y)) = x v y. [para(12(a,1),15(a,1,2))]. given #49 (T,wt=13): 47 x v (y v (z ^ (x v y))) = x v y. [para(21(a,1),3(a,1)),flip(a)]. given #50 (T,wt=13): 51 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(34(a,1),5(a,2,2)),rewrite(14(3),5(2))]. given #51 (A,wt=27): 27 x ^ (y v (z v ((x v (y v z)) ^ (u v v)))) = x ^ (y v (z v (x ^ (u v v)))). [para(3(a,1),9(a,1,2)),rewrite(3(11))]. given #52 (F,wt=13): 53 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(5(a,1),36(a,1,2)),rewrite(5(5))]. given #53 (F,wt=13): 57 (x ^ y) v (x ^ (z ^ y)) = x ^ y. [para(14(a,1),21(a,1,2))]. given #54 (T,wt=13): 59 x v (y v (x v z)) = y v (x v z). [para(37(a,1),3(a,2,2)),rewrite(12(3),3(2))]. given #55 (T,wt=13): 61 x v (y v (z v x)) = y v (z v x). [para(3(a,1),39(a,1,2)),rewrite(3(5))]. given #56 (A,wt=21): 28 x ^ (y v ((z v u) ^ (x v y))) = x ^ (y v (x ^ (z v u))). [para(4(a,1),9(a,1,2,2))]. given #57 (F,wt=13): 64 x ^ ((y v (x v z)) ^ u) = x ^ u. [para(40(a,1),5(a,1,1)),flip(a)]. given #58 (F,wt=13): 66 x ^ (y ^ (z v (x v u))) = y ^ x. [para(40(a,1),14(a,1,2)),flip(a)]. given #59 (T,wt=13): 68 x ^ ((y v (z v x)) ^ u) = x ^ u. [para(42(a,1),5(a,1,1)),flip(a)]. given #60 (T,wt=13): 71 x ^ (y ^ (z v (u v x))) = y ^ x. [para(42(a,1),14(a,1,2)),flip(a)]. given #61 (A,wt=25): 29 x ^ ((y v ((x v y) ^ (z v u))) ^ v) = x ^ ((y v (x ^ (z v u))) ^ v). [para(9(a,1),5(a,1,1)),rewrite(5(5)),flip(a)]. given #62 (F,wt=13): 72 (x v y) ^ (y v (x v z)) = y v x. [para(2(a,1),16(a,1,1))]. given #63 (F,wt=13): 73 (x v y) ^ (y v (z v x)) = x v y. [para(2(a,1),16(a,1,2)),rewrite(3(3))]. given #64 (T,wt=13): 80 x v ((y ^ (z ^ x)) v u) = x v u. [para(48(a,1),3(a,1,1)),flip(a)]. given #65 (T,wt=13): 83 x v (y v (z ^ (u ^ x))) = y v x. [para(48(a,1),12(a,1,2)),flip(a)]. given #66 (A,wt=29): 30 x ^ (y ^ (z v (((x ^ y) v z) ^ (u v v)))) = x ^ (y ^ (z v (x ^ (y ^ (u v v))))). [para(9(a,1),5(a,1)),rewrite(5(4),5(6)),flip(a)]. given #67 (F,wt=13): 86 x v ((y ^ (x ^ z)) v u) = x v u. [para(55(a,1),3(a,1,1)),flip(a)]. given #68 (F,wt=13): 90 x v (y v (z ^ (x ^ u))) = y v x. [para(55(a,1),12(a,1,2)),flip(a)]. given #69 (T,wt=13): 102 x ^ (y ^ ((y ^ x) v z)) = x ^ y. [para(4(a,1),18(a,1,2,2,1))]. given #70 (T,wt=13): 144 x v (y v ((y v x) ^ z)) = x v y. [para(2(a,1),20(a,1,2,2,1))]. given #71 (A,wt=17): 32 x ^ (y v ((x v y) ^ z)) = x ^ (y v (x ^ z)). [para(7(a,1),9(a,1,2,2,2)),rewrite(7(6))]. given #72 (F,wt=13): 172 x ^ (y v (z v (u v (x v v)))) = x. [para(3(a,1),63(a,1,2,2))]. given #73 (F,wt=13): 176 x ^ (y v (z v (u v (v v x)))) = x. [para(3(a,1),67(a,1,2,2,2))]. given #74 (T,wt=13): 188 (x ^ y) v (y ^ (x ^ z)) = y ^ x. [para(4(a,1),22(a,1,1))]. given #75 (T,wt=13): 189 (x ^ y) v (y ^ (z ^ x)) = x ^ y. [para(4(a,1),22(a,1,2)),rewrite(5(3))]. given #76 (A,wt=15): 62 (x v y) ^ (z v (x v (y v u))) = x v y. [para(3(a,1),40(a,1,2,2))]. given #77 (F,wt=13): 201 x v (y v (z ^ (y v x))) = x v y. [para(79(a,1),48(a,1,2,2)),rewrite(3(4))]. given #78 (F,wt=13): 202 (x v (y v z)) ^ (y v x) = x v y. [para(79(a,1),17(a,2)),rewrite(3(3),199(6))]. given #79 (T,wt=13): 205 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(5(a,1),82(a,1,2,2,2))]. given #80 (T,wt=13): 211 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(82(a,1),19(a,1,2)),rewrite(7(2)),flip(a)]. given #81 (A,wt=15): 65 x ^ (y ^ (z v ((x ^ y) v u))) = x ^ y. [para(40(a,1),5(a,1)),flip(a)]. given #82 (F,wt=13): 225 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(12(a,1),93(a,1,1))]. given #83 (F,wt=13): 258 (x ^ (y ^ z)) v (u v y) = u v y. [para(14(a,1),100(a,1,1))]. given #84 (T,wt=13): 267 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(3(a,1),117(a,1,1))]. given #85 (T,wt=13): 283 (x v (y v z)) ^ (z v y) = z v y. [para(79(a,1),117(a,1,2)),rewrite(79(7))]. given #86 (A,wt=15): 69 x ^ (y ^ (z v (u v (x ^ y)))) = x ^ y. [para(42(a,1),5(a,1)),flip(a)]. given #87 (F,wt=13): 286 (x ^ (y ^ z)) v (u v z) = u v z. [para(5(a,1),128(a,1,1))]. given #88 (F,wt=13): 308 x ^ (y ^ (z v (y ^ x))) = x ^ y. [para(191(a,1),42(a,1,2,2)),rewrite(5(4))]. given #89 (T,wt=13): 310 (x ^ (y ^ z)) v (y ^ x) = y ^ x. [para(191(a,1),100(a,1,2)),rewrite(5(2),191(7))]. given #90 (T,wt=13): 311 (x ^ (y ^ z)) v (z ^ y) = z ^ y. [para(191(a,1),128(a,1,2)),rewrite(191(7))]. given #91 (A,wt=15): 70 (x v y) ^ (z v (x v (u v y))) = x v y. [para(12(a,1),42(a,1,2,2))]. given #92 (F,wt=13): 355 (x v y) ^ (z v (y v x)) = x v y. [para(2(a,1),45(a,1,2)),rewrite(3(3))]. given #93 (F,wt=13): 417 (x ^ y) v (z ^ (y ^ x)) = x ^ y. [para(4(a,1),57(a,1,2)),rewrite(5(3))]. given #94 (T,wt=13): 640 (x v (y v z)) ^ (z v x) = z v x. [para(73(a,1),4(a,1)),flip(a)]. given #95 (T,wt=13): 934 (x ^ (y ^ z)) v (z ^ x) = z ^ x. [para(189(a,1),2(a,1)),flip(a)]. given #96 (A,wt=19): 74 (x v (y v z)) ^ (x v (y v (z v u))) = x v (y v z). [para(3(a,1),16(a,1,1)),rewrite(3(5),3(8))]. given #97 (F,wt=15): 77 (x v y) ^ (x v (z v (y v u))) = x v y. [para(12(a,1),16(a,1,2,2))]. given #98 (F,wt=15): 81 x v (y v (z ^ (u ^ (x v y)))) = x v y. [para(48(a,1),3(a,1)),flip(a)]. given #99 (T,wt=15): 84 (x ^ y) v (z ^ (x ^ (u ^ y))) = x ^ y. [para(14(a,1),48(a,1,2,2))]. given #100 (T,wt=15): 87 x v (y v (z ^ ((x v y) ^ u))) = x v y. [para(55(a,1),3(a,1)),flip(a)]. given #101 (A,wt=17): 75 (x v y) ^ ((x v (y v z)) ^ u) = (x v y) ^ u. [para(16(a,1),5(a,1,1)),flip(a)]. given #102 (F,wt=15): 88 (x ^ y) v (z ^ (x ^ (y ^ u))) = x ^ y. [para(5(a,1),55(a,1,2,2))]. given #103 (F,wt=15): 92 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(17(a,1),21(a,1,2)),rewrite(2(4))]. given #104 (T,wt=15): 94 x ^ (y ^ ((x v z) ^ u)) = y ^ (x ^ u). [para(17(a,1),14(a,1,2)),flip(a)]. given #105 (T,wt=15): 98 x v (y v ((x ^ z) v u)) = y v (x v u). [para(19(a,1),12(a,1,2)),flip(a)]. given #106 (A,wt=19): 76 (x v (y v z)) ^ (y v (x v (z v u))) = y v (x v z). [para(12(a,1),16(a,1,1)),rewrite(3(4))]. given #107 (F,wt=15): 99 (x v y) ^ ((x ^ z) v y) = (x ^ z) v y. [para(19(a,1),15(a,1,2)),rewrite(4(4))]. given #108 (F,wt=15): 108 x ^ (y ^ (((x v z) ^ y) v u)) = x ^ y. [para(18(a,1),17(a,1,2)),rewrite(17(3)),flip(a)]. given #109 (T,wt=13): 1867 x ^ (((x v y) ^ (x v z)) v u) = x. [para(108(a,1),17(a,1)),rewrite(6(2)),flip(a)]. given #110 (T,wt=13): 1868 x ^ (((x v y) ^ (z v x)) v u) = x. [para(108(a,1),43(a,1)),rewrite(15(2)),flip(a)]. given #111 (A,wt=17): 78 (x v y) ^ (z ^ (x v (y v u))) = z ^ (x v y). [para(16(a,1),14(a,1,2)),flip(a)]. given #112 (F,wt=13): 1911 x ^ (((y v x) ^ (x v z)) v u) = x. [para(2(a,1),1867(a,1,2,1,1))]. given #113 (F,wt=13): 1912 x ^ (y v ((x v z) ^ (x v u))) = x. [para(2(a,1),1867(a,1,2))]. given #114 (T,wt=13): 1952 x ^ (((y v x) ^ (z v x)) v u) = x. [para(2(a,1),1868(a,1,2,1,1))]. given #115 (T,wt=13): 1953 x ^ (y v ((x v z) ^ (u v x))) = x. [para(2(a,1),1868(a,1,2))]. given #116 (A,wt=17): 85 x v (y v (z v (u ^ (x v y)))) = x v (y v z). [para(16(a,1),48(a,1,2,2)),rewrite(3(5),3(4))]. given #117 (F,wt=13): 2052 x ^ (y v ((z v x) ^ (x v u))) = x. [para(2(a,1),1911(a,1,2))]. given #118 (F,wt=13): 2130 x ^ (y v ((z v x) ^ (u v x))) = x. [para(2(a,1),1952(a,1,2))]. given #119 (T,wt=15): 110 x v (y v (z v (x ^ u))) = y v (z v x). [para(3(a,1),41(a,1,2)),rewrite(3(6))]. given #120 (T,wt=15): 112 (x v y) ^ (x v (y ^ z)) = x v (y ^ z). [para(41(a,1),15(a,1,2)),rewrite(4(4))]. given #121 (A,wt=17): 91 x ^ (y ^ (((x ^ y) v z) ^ u)) = x ^ (y ^ u). [para(17(a,1),5(a,1)),rewrite(5(2)),flip(a)]. given #122 (F,wt=15): 116 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(43(a,1),21(a,1,2)),rewrite(2(4))]. given #123 (F,wt=13): 2579 x v ((y v z) ^ (y v x)) = x v y. [para(202(a,1),116(a,1,2)),rewrite(2(5),3(5),1659(4),202(8))]. given #124 (T,wt=13): 2625 x v ((y v z) ^ (z v x)) = x v z. [para(2(a,1),2579(a,1,2,1))]. given #125 (T,wt=13): 2626 x v ((y v z) ^ (x v y)) = x v y. [para(2(a,1),2579(a,1,2,2))]. given #126 (A,wt=17): 95 ((x v y) ^ z) v (u ^ (x ^ z)) = (x v y) ^ z. [para(17(a,1),48(a,1,2,2))]. given #127 (F,wt=13): 2630 x v ((y v x) ^ (y v z)) = x v y. [para(4(a,1),2579(a,1,2))]. given #128 (F,wt=13): 2691 x v ((y v z) ^ (x v z)) = x v z. [para(2(a,1),2625(a,1,2,2))]. given #129 (T,wt=13): 2695 x v ((y v x) ^ (z v y)) = x v y. [para(4(a,1),2625(a,1,2))]. given #130 (T,wt=13): 2788 x v ((x v y) ^ (y v z)) = x v y. [para(4(a,1),2626(a,1,2))]. given #131 (A,wt=17): 96 x v (y v (((x v y) ^ z) v u)) = x v (y v u). [para(19(a,1),3(a,1)),rewrite(3(2)),flip(a)]. given #132 (F,wt=13): 2962 x v ((x v y) ^ (z v y)) = x v y. [para(4(a,1),2691(a,1,2))]. given #133 (F,wt=15): 118 x ^ (y ^ ((z v x) ^ u)) = y ^ (x ^ u). [para(43(a,1),14(a,1,2)),flip(a)]. given #134 (T,wt=15): 122 x ^ (y ^ (((z v x) ^ y) v u)) = x ^ y. [para(18(a,1),43(a,1,2)),rewrite(43(3)),flip(a)]. given #135 (T,wt=15): 125 x v (y v ((z ^ x) v u)) = y v (x v u). [para(46(a,1),12(a,1,2)),flip(a)]. given #136 (A,wt=17): 97 (x ^ y) v ((x ^ (y ^ z)) v u) = (x ^ y) v u. [para(5(a,1),19(a,1,2,1))]. given #137 (F,wt=15): 126 (x v y) ^ ((z ^ x) v y) = (z ^ x) v y. [para(46(a,1),15(a,1,2)),rewrite(4(4))]. given #138 (F,wt=15): 135 x v (y v (z v (u ^ x))) = y v (z v x). [para(3(a,1),49(a,1,2)),rewrite(3(6))]. given #139 (T,wt=15): 136 (x v y) ^ (x v (z ^ y)) = x v (z ^ y). [para(49(a,1),15(a,1,2)),rewrite(4(4))]. given #140 (T,wt=13): 3658 x ^ ((y ^ x) v (y ^ z)) = x ^ y. [para(188(a,1),136(a,1,2)),rewrite(14(5),4(4),1811(4),188(8))]. given #141 (A,wt=17): 101 ((x ^ y) v z) ^ (u v (x v z)) = (x ^ y) v z. [para(19(a,1),42(a,1,2,2))]. given #142 (F,wt=13): 3705 x ^ ((y ^ z) v (y ^ x)) = x ^ y. [para(2(a,1),3658(a,1,2))]. given #143 (F,wt=13): 3706 x ^ ((x ^ y) v (y ^ z)) = x ^ y. [para(4(a,1),3658(a,1,2,1))]. given #144 (T,wt=13): 3707 x ^ ((y ^ x) v (z ^ y)) = x ^ y. [para(4(a,1),3658(a,1,2,2))]. given #145 (T,wt=13): 3868 x ^ ((y ^ z) v (z ^ x)) = x ^ z. [para(4(a,1),3705(a,1,2,1))]. given #146 (A,wt=19): 103 x ^ (y ^ (z ^ ((x ^ (y ^ z)) v u))) = x ^ (y ^ z). [para(18(a,1),5(a,1)),rewrite(5(2),5(4)),flip(a)]. given #147 (F,wt=13): 3869 x ^ ((y ^ z) v (x ^ y)) = x ^ y. [para(4(a,1),3705(a,1,2,2))]. given #148 (F,wt=13): 3929 x ^ ((x ^ y) v (z ^ y)) = x ^ y. [para(4(a,1),3706(a,1,2,2))]. given #149 (T,wt=13): 4075 x ^ ((y ^ z) v (x ^ z)) = x ^ z. [para(4(a,1),3868(a,1,2,2))]. given #150 (T,wt=15): 150 x v (y v (((x ^ z) v y) ^ u)) = x v y. [para(20(a,1),19(a,1,2)),rewrite(19(3)),flip(a)]. given #151 (A,wt=19): 104 (x ^ y) v (y ^ ((x ^ y) v z)) = y ^ ((x ^ y) v z). [para(18(a,1),21(a,1,2)),rewrite(2(5))]. given #152 (F,wt=13): 4330 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(150(a,1),19(a,1)),rewrite(7(2)),flip(a)]. given #153 (F,wt=13): 4332 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(150(a,1),46(a,1)),rewrite(21(2)),flip(a)]. given #154 (T,wt=13): 4481 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(4(a,1),4330(a,1,2,1,1))]. given #155 (T,wt=13): 4482 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(4(a,1),4330(a,1,2))]. given #156 (A,wt=17): 105 x ^ (y ^ (z ^ ((x ^ z) v u))) = y ^ (x ^ z). [para(18(a,1),14(a,1,2)),flip(a)]. given #157 (F,wt=13): 4541 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(4(a,1),4332(a,1,2,1,1))]. given #158 (F,wt=13): 4542 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(4(a,1),4332(a,1,2))]. given #159 (T,wt=13): 4645 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(4(a,1),4481(a,1,2))]. given #160 (T,wt=13): 4818 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(4(a,1),4541(a,1,2))]. given #161 (A,wt=19): 106 x ^ (y ^ (z ^ ((y ^ (x ^ z)) v u))) = x ^ (y ^ z). [para(14(a,1),18(a,1,2,2,1)),rewrite(5(5))]. given #162 (F,wt=15): 152 x v (y v (((z ^ x) v y) ^ u)) = x v y. [para(20(a,1),46(a,1,2)),rewrite(46(3)),flip(a)]. given #163 (F,wt=15): 154 x ^ (y ^ (z ^ (x v u))) = y ^ (z ^ x). [para(5(a,1),54(a,1,2)),rewrite(5(6))]. given #164 (T,wt=15): 155 (x ^ y) v (x ^ (y v z)) = x ^ (y v z). [para(54(a,1),21(a,1,2)),rewrite(2(4))]. given #165 (T,wt=15): 160 x ^ (y ^ (z ^ (u v x))) = y ^ (z ^ x). [para(5(a,1),56(a,1,2)),rewrite(5(6))]. given #166 (A,wt=21): 107 (x ^ ((y ^ x) v z)) v (u ^ (y ^ x)) = x ^ ((y ^ x) v z). [para(18(a,1),48(a,1,2,2))]. given #167 (F,wt=15): 162 (x ^ y) v (x ^ (z v y)) = x ^ (z v y). [para(56(a,1),21(a,1,2)),rewrite(2(4))]. given #168 (F,wt=15): 173 x ^ ((y v (z v (x v u))) ^ v) = x ^ v. [para(63(a,1),5(a,1,1)),flip(a)]. given #169 (T,wt=15): 175 x ^ (y ^ (z v (u v (x v v)))) = y ^ x. [para(63(a,1),14(a,1,2)),flip(a)]. given #170 (T,wt=15): 177 x ^ ((y v (z v (u v x))) ^ v) = x ^ v. [para(67(a,1),5(a,1,1)),flip(a)]. given #171 (A,wt=17): 109 x v (y v (z v ((x v y) ^ u))) = z v (x v y). [para(41(a,1),3(a,1)),flip(a)]. given #172 (F,wt=15): 181 x ^ (y ^ (z v (u v (v v x)))) = y ^ x. [para(67(a,1),14(a,1,2)),flip(a)]. given #173 (F,wt=15): 193 (x ^ y) v (x ^ (z ^ (y ^ u))) = x ^ y. [para(14(a,1),22(a,1,2,2))]. given #174 (T,wt=15): 198 (x v y) ^ ((y v x) ^ z) = (x v y) ^ z. [para(79(a,1),5(a,1,1)),flip(a)]. given #175 (T,wt=15): 199 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(79(a,1),5(a,2,2)),rewrite(4(4))]. ============================== PROOF ================================= % Proof 1 at 1.54 (+ 0.02) seconds: H34. % Length of proof is 32. % Level of proof is 10. % Maximum clause weight is 21. % Given clauses 175. 1 x ^ (y v (z ^ u)) = x ^ (y v (z ^ (y v (u ^ (y v z))))) # answer(H34) # 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 ^ (y v (x ^ (z v u))) = x ^ (y v ((x v y) ^ (z v u))) # label(H33). [assumption]. 9 x ^ (y v ((x v y) ^ (z v u))) = x ^ (y v (x ^ (z v u))). [copy(8),flip(a)]. 10 c1 ^ (c2 v (c3 ^ (c2 v (c4 ^ (c2 v c3))))) != c1 ^ (c2 v (c3 ^ c4)) # answer(H34). [deny(1)]. 14 x ^ (y ^ z) = y ^ (x ^ z). [para(4(a,1),5(a,1,1)),rewrite(5(2))]. 15 x ^ (y v x) = x. [para(2(a,1),6(a,1,2))]. 16 (x v y) ^ (x v (y v z)) = x v y. [para(3(a,1),6(a,1,2))]. 17 x ^ ((x v y) ^ z) = x ^ z. [para(6(a,1),5(a,1,1)),flip(a)]. 21 x v (y ^ x) = x. [para(4(a,1),7(a,1,2))]. 24 x v x = x. [para(6(a,1),7(a,1,2))]. 32 x ^ (y v ((x v y) ^ z)) = x ^ (y v (x ^ z)). [para(7(a,1),9(a,1,2,2,2)),rewrite(7(6))]. 39 x v (y v x) = y v x. [para(24(a,1),3(a,2,2)),rewrite(2(2))]. 43 x ^ ((y v x) ^ z) = x ^ z. [para(15(a,1),5(a,1,1)),flip(a)]. 56 x ^ (y ^ (z v x)) = y ^ x. [para(15(a,1),14(a,1,2)),flip(a)]. 79 (x v y) ^ (y v x) = x v y. [para(39(a,1),16(a,1,2))]. 92 (x ^ y) v ((x v z) ^ y) = (x v z) ^ y. [para(17(a,1),21(a,1,2)),rewrite(2(4))]. 116 (x ^ y) v ((z v x) ^ y) = (z v x) ^ y. [para(43(a,1),21(a,1,2)),rewrite(2(4))]. 199 (x v y) ^ (z ^ (y v x)) = z ^ (y v x). [para(79(a,1),5(a,2,2)),rewrite(4(4))]. 202 (x v (y v z)) ^ (y v x) = x v y. [para(79(a,1),17(a,2)),rewrite(3(3),199(6))]. 1659 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(6(a,1),92(a,1,1))]. 2579 x v ((y v z) ^ (y v x)) = x v y. [para(202(a,1),116(a,1,2)),rewrite(2(5),3(5),1659(4),202(8))]. 2625 x v ((y v z) ^ (z v x)) = x v z. [para(2(a,1),2579(a,1,2,1))]. 2691 x v ((y v z) ^ (x v z)) = x v z. [para(2(a,1),2625(a,1,2,2))]. 2963 x v (y ^ (x v (y ^ z))) = x v (y ^ z). [para(7(a,1),2691(a,1,2,1))]. 6353 x ^ (y v (z ^ (y v x))) = x ^ (y v (z ^ x)). [para(199(a,1),32(a,1,2,2)),rewrite(56(7))]. 6385 $F # answer(H34). [back_rewrite(10),rewrite(6353(11),4(7),2963(10)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=175. Generated=48848. Kept=6382. proofs=1. Usable=167. Sos=5899. Demods=5716. Limbo=32, Disabled=292. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=42465. Back_subsumed=76. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=5933 (6 lex), Back_demodulated=206. Back_unit_deleted=0. Demod_attempts=666939. Demod_rewrites=124968. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=7.09. User_CPU=1.54, System_CPU=0.02, Wall_clock=1. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 4151 exit (max_proofs) Wed Nov 22 11:33:01 2006