============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3281 was started by mccune on cleo.thornwood, Wed Nov 22 11:21:28 2006 The command was "/home/mccune/bin/prover9 -f na-ring-1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file na-ring-1.in formulas(sos). x + 0 = x. x + -x = 0. (x + y) + z = x + (y + z). x + y = y + x. x * (y + z) = (x * y) + (x * z). (x + y) * z = (x * z) + (y * z). (x * x) * y = x * (x * y) # label(left). (x * y) * x = x * (y * x) # label(flexible). end_of_list. formulas(goals). (y * x) * x = y * (x * x) # label(right). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (y * x) * x = y * (x * x) # label(right) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). x + 0 = x. [assumption]. x + -x = 0. [assumption]. (x + y) + z = x + (y + z). [assumption]. x + y = y + x. [assumption]. x * (y + z) = (x * y) + (x * z). [assumption]. (x + y) * z = (x * z) + (y * z). [assumption]. (x * x) * y = x * (x * y) # label(left). [assumption]. (x * y) * x = x * (y * x) # label(flexible). [assumption]. (c1 * c2) * c2 != c1 * (c2 * c2) # label(right). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % copying label right to answer in negative clause Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ 0, c1, c2, *, +, - ]). After inverse_order: Function symbol precedence: lex([ 0, c1, c2, +, -, * ]). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). % 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 + 0 = x. [assumption]. 3 x + -x = 0. [assumption]. 4 (x + y) + z = x + (y + z). [assumption]. 5 x + y = y + x. [assumption]. 6 x * (y + z) = (x * y) + (x * z). [assumption]. 7 (x + y) * z = (x * z) + (y * z). [assumption]. 8 (x * x) * y = x * (x * y) # label(left). [assumption]. 9 (x * y) * x = x * (y * x) # label(flexible). [assumption]. 10 (c1 * c2) * c2 != c1 * (c2 * c2) # label(right) # answer(right). [deny(1)]. end_of_list. formulas(demodulators). 2 x + 0 = x. [assumption]. 3 x + -x = 0. [assumption]. 4 (x + y) + z = x + (y + z). [assumption]. 5 x + y = y + x. [assumption]. % (lex-dep) 6 x * (y + z) = (x * y) + (x * z). [assumption]. 7 (x + y) * z = (x * z) + (y * z). [assumption]. 8 (x * x) * y = x * (x * y) # label(left). [assumption]. 9 (x * y) * x = x * (y * x) # label(flexible). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 2 x + 0 = x. [assumption]. given #2 (I,wt=6): 3 x + -x = 0. [assumption]. given #3 (I,wt=11): 4 (x + y) + z = x + (y + z). [assumption]. given #4 (I,wt=7): 5 x + y = y + x. [assumption]. % Operation + is associative-commutative; CAC redundancy checks enabled. given #5 (I,wt=13): 6 x * (y + z) = (x * y) + (x * z). [assumption]. given #6 (I,wt=13): 7 (x + y) * z = (x * z) + (y * z). [assumption]. given #7 (I,wt=11): 8 (x * x) * y = x * (x * y) # label(left). [assumption]. given #8 (I,wt=11): 9 (x * y) * x = x * (y * x) # label(flexible). [assumption]. given #9 (I,wt=11): 10 (c1 * c2) * c2 != c1 * (c2 * c2) # label(right) # answer(right). [deny(1)]. given #10 (T,wt=5): 15 0 + x = x. [para(5(a,1),2(a,1))]. given #11 (A,wt=10): 13 x + (y + -(x + y)) = 0. [para(4(a,1),3(a,1))]. given #12 (F,wt=4): 28 -0 = 0. [para(15(a,1),3(a,1))]. given #13 (F,wt=8): 17 x + (-x + y) = y. [back_rewrite(14),rewrite(15(5))]. given #14 (T,wt=5): 36 --x = x. [para(3(a,1),17(a,1,2)),rewrite(2(2)),flip(a)]. given #15 (T,wt=8): 37 x + (y + -x) = y. [para(5(a,1),17(a,1,2))]. given #16 (A,wt=11): 16 x + (y + z) = y + (x + z). [para(5(a,1),4(a,1,1)),rewrite(4(2))]. given #17 (F,wt=8): 46 -x + (y + x) = y. [para(36(a,1),37(a,1,2,2))]. given #18 (F,wt=9): 40 x + -(-y + x) = y. [para(13(a,1),17(a,1,2)),rewrite(2(2)),flip(a)]. given #19 (T,wt=9): 56 x + -(x + y) = -y. [para(46(a,1),46(a,1,2)),rewrite(5(3))]. given #20 (T,wt=10): 73 -(x + y) = -y + -x. [para(46(a,1),56(a,1,2,1)),flip(a)]. given #21 (A,wt=11): 18 (x * y) + (x * 0) = x * y. [para(2(a,1),6(a,1,2)),flip(a)]. given #22 (F,wt=11): 20 (x * y) + (0 * y) = x * y. [para(2(a,1),7(a,1,1)),flip(a)]. given #23 (F,wt=11): 29 (x * 0) + (x * y) = x * y. [para(15(a,1),6(a,1,2)),flip(a)]. given #24 (T,wt=5): 97 x * 0 = 0. [para(29(a,1),46(a,1,2)),rewrite(5(4),3(4)),flip(a)]. given #25 (T,wt=9): 99 0 * (0 * x) = 0 * x. [para(97(a,1),8(a,1,1)),flip(a)]. given #26 (A,wt=12): 21 (x * y) + (-x * y) = 0 * y. [para(3(a,1),7(a,1,1)),flip(a)]. given #27 (F,wt=9): 100 x * (0 * x) = 0 * x. [para(97(a,1),9(a,1,1)),flip(a)]. given #28 (F,wt=10): 98 (x * y) + (x * -y) = 0. [back_rewrite(19),rewrite(97(6))]. given #29 (T,wt=9): 125 -(x * -y) = x * y. [para(98(a,1),46(a,1,2)),rewrite(5(5),15(5))]. given #30 (T,wt=9): 130 x * -y = -(x * y). [para(125(a,1),36(a,1,1)),flip(a)]. given #31 (A,wt=47): 22 (x * (x * y)) + ((z * (z * y)) + (((z * x) * y) + ((x * z) * y))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y)))). [para(6(a,1),8(a,1,1)),rewrite(7(2),7(5),4(7),7(8),8(2),7(8),7(8),8(8),5(9),16(10),7(14),6(16),7(14),7(19),4(22))]. given #32 (F,wt=10): 116 -x * (0 * x) = 0 * x. [para(100(a,1),21(a,1,1)),rewrite(101(7),99(8))]. given #33 (F,wt=11): 30 (0 * x) + (y * x) = y * x. [para(15(a,1),7(a,1,1)),flip(a)]. given #34 (T,wt=5): 181 0 * x = 0. [para(30(a,1),46(a,1,2)),rewrite(5(4),3(4)),flip(a)]. given #35 (T,wt=9): 184 -(-x * y) = x * y. [back_rewrite(110),rewrite(181(2),15(5))]. given #36 (A,wt=47): 23 (x * (x * y)) + ((z * (z * y)) + (((x * z) * y) + ((z * x) * y))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y)))). [para(7(a,1),8(a,1,1)),rewrite(6(2),6(5),4(7),7(8),8(2),7(8),7(8),8(8),5(9),16(10),7(14),6(16),7(14),7(19),4(22))]. given #37 (F,wt=9): 196 -x * y = -(x * y). [para(184(a,1),36(a,1,1)),flip(a)]. given #38 (F,wt=12): 41 x + (y + (-x + z)) = y + z. [para(37(a,1),4(a,1,1)),rewrite(4(4)),flip(a)]. given #39 (T,wt=12): 43 x + (y + (z + -x)) = y + z. [para(4(a,1),37(a,1,2))]. given #40 (T,wt=12): 49 -x + (y + (x + z)) = y + z. [para(46(a,1),4(a,1,1)),rewrite(4(4)),flip(a)]. given #41 (A,wt=19): 24 (x * (x * (x * x))) * y = x * (x * (x * (x * y))). [para(8(a,1),8(a,1,1)),rewrite(8(7),8(8))]. given #42 (F,wt=12): 50 -x + (y + (z + x)) = y + z. [para(4(a,1),46(a,1,2))]. given #43 (F,wt=16): 209 x + (y + (z + (-x + u))) = y + (z + u). [para(4(a,1),41(a,1,2)),rewrite(4(7))]. given #44 (T,wt=16): 210 x + (y + (z + (u + -x))) = y + (z + u). [para(4(a,1),43(a,1,2,2))]. given #45 (T,wt=16): 212 -x + (y + (z + (x + u))) = y + (z + u). [para(4(a,1),49(a,1,2)),rewrite(4(7))]. given #46 (A,wt=47): 25 (x * (y * x)) + (((z * y) * x) + (((x * y) * z) + (z * (y * z)))) = (x * (y * x)) + ((z * (y * x)) + ((x * (y * z)) + (z * (y * z)))). [para(9(a,1),6(a,1)),rewrite(6(3),6(5),7(3),7(8),4(11),7(13),7(15),9(13),7(18),7(20),9(20),4(22)),flip(a)]. given #47 (F,wt=16): 220 -x + (y + (z + (u + x))) = y + (z + u). [para(4(a,1),50(a,1,2,2))]. given #48 (F,wt=19): 26 (x * (x * y)) * (x * x) = x * (x * (y * (x * x))). [para(8(a,1),9(a,1,1)),rewrite(8(8))]. given #49 (T,wt=19): 27 (x * (y * x)) * (x * y) = (x * y) * (x * (x * y)). [para(9(a,1),9(a,1,1))]. given #50 (T,wt=20): 223 x + (y + (z + (u + (-x + v)))) = y + (z + (u + v)). [para(4(a,1),209(a,1,2,2)),rewrite(4(8))]. given #51 (A,wt=51): 135 (x * (x * y)) + ((z * (z * y)) + (((z * x) * y) + (((x * z) * y) + u))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + ((z * (z * y)) + u))). [para(22(a,1),4(a,1,1)),rewrite(4(12),4(11),4(10),4(23),4(22)),flip(a)]. given #52 (F,wt=20): 224 x + (y + (z + (u + (v + -x)))) = y + (z + (u + v)). [para(4(a,1),210(a,1,2,2,2))]. given #53 (F,wt=20): 225 -x + (y + (z + (u + (x + v)))) = y + (z + (u + v)). [para(4(a,1),212(a,1,2,2)),rewrite(4(8))]. given #54 (T,wt=20): 261 -x + (y + (z + (u + (v + x)))) = y + (z + (u + v)). [para(4(a,1),220(a,1,2,2,2))]. given #55 (T,wt=24): 277 x + (y + (z + (u + (v + (-x + w))))) = y + (z + (u + (v + w))). [para(4(a,1),223(a,1,2,2,2)),rewrite(4(9))]. given #56 (A,wt=63): 136 (x * (y * (y * z))) + ((x * (u * (u * z))) + ((x * ((u * y) * z)) + (x * ((y * u) * z)))) = (x * (y * (y * z))) + ((x * (u * (y * z))) + ((x * (y * (u * z))) + (x * (u * (u * z))))). [para(22(a,1),6(a,1,2)),rewrite(6(12),6(12),6(12),6(27),6(27)),flip(a)]. given #57 (F,wt=24): 278 x + (y + (z + (u + (v + (w + -x))))) = y + (z + (u + (v + w))). [para(223(a,1),210(a,2,2)),rewrite(4(7),4(6),4(5),4(4),223(8))]. given #58 (F,wt=24): 279 -x + (y + (z + (u + (v + (w + x))))) = y + (z + (u + (v + w))). [para(223(a,1),220(a,2,2)),rewrite(4(7),4(6),4(5),4(4),223(8))]. given #59 (T,wt=24): 339 -x + (y + (z + (u + (v + (x + w))))) = y + (z + (u + (v + w))). [para(4(a,1),225(a,1,2,2,2)),rewrite(4(9))]. given #60 (T,wt=27): 267 (x * (y * (y * x))) * (x * (y * y)) = (x * (y * y)) * (x * (x * (y * y))). [para(8(a,1),27(a,1,1,2))]. given #61 (A,wt=95): 137 (x * (x * y)) + ((x * (x * z)) + ((u * (u * y)) + ((u * (u * z)) + (((u * x) * y) + (((u * x) * z) + (((x * u) * y) + ((x * u) * z))))))) = (x * (x * y)) + ((x * (x * z)) + ((u * (x * y)) + ((u * (x * z)) + ((x * (u * y)) + ((x * (u * z)) + ((u * (u * y)) + (u * (u * z)))))))). [para(6(a,1),22(a,1,1,2)),rewrite(6(4),6(7),6(9),6(13),6(18),4(21),4(22),4(23),6(25),6(27),6(30),6(32),6(35),6(37),6(40),6(42),4(44),4(45),4(46))]. given #62 (F,wt=27): 269 (x * (x * (y * x))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * y))). [para(9(a,1),27(a,1,1,2))]. given #63 (F,wt=27): 386 (x * (x * x)) * (x * (x * (x * x))) = x * (x * (x * (x * (x * (x * x))))). [para(267(a,1),24(a,1))]. Demod_limit: ((y * (y * (y * (y * (y * (y * y)))))) + (((z * (y * y)) * (y * (y * (y * y)))) + (((y * (z * y)) * (y * (y * (y * y)))) + (((z * (z * y)) * (y * (y * (y * y)))) + (((y * (y * z)) * (y * (y * (y * y)))) + (((z * (y * z)) * (y * (y * (y * y)))) + (((y * (z * z)) * (y * (y * (y * y)))) + ((z * (z * z)) * (y * (y * (y * y))))))))))) + ((((y * (y * y)) * (z * (y * (y * y)))) + (((z * (y * y)) * (z * (y * (y * y)))) + (((y * (z * y)) * (z * (y * (y * y)))) + (((z * (z * y)) * (z * (y * (y * y)))) + (((y * (y * z)) * (z * (y * (y * y)))) + (((z * (y * z)) * (z * (y * (y * y)))) + (((y * (z * z)) * (z * (y * (y * y)))) + ((z * (z * z)) * (z * (y * (y * y))))))))))) + ((((y * (y * y)) * (y * (z * (y * y)))) + (((z * (y * y)) * (y * (z * (y * y)))) + (((y * (z * y)) * (y * (z * (y * y)))) + (((z * (z * y)) * (y * (z * (y * y)))) + (((y * (y * z)) * (y * (z * (y * y)))) + (((z * (y * z)) * (y * (z * (y * y)))) + (((y * (z * z)) * (y * (z * (y * y)))) + ((z * (z * z)) * (y * (z * (y * y))))))))))) + ((((y * (y * y)) * (z * (z * (y * y)))) + (((z * (y * y)) * (z * (z * (y * y)))) + (((y * (z * y)) * (z * (z * (y * y)))) + (((z * (z * y)) * (z * (z * (y * y)))) + (((y * (y * z)) * (z * (z * (y * y)))) + (((z * (y * z)) * (z * (z * (y * y)))) + (((y * (z * z)) * (z * (z * (y * y)))) + ((z * (z * z)) * (z * (z * (y * y))))))))))) + ((((y * (y * y)) * (y * (y * (z * y)))) + (((z * (y * y)) * (y * (y * (z * y)))) + (((y * (z * y)) * (y * (y * (z * y)))) + (((z * (z * y)) * (y * (y * (z * y)))) + (((y * (y * z)) * (y * (y * (z * y)))) + (((z * (y * z)) * (y * (y * (z * y)))) + (((y * (z * z)) * (y * (y * (z * y)))) + ((z * (z * z)) * (y * (y * (z * y))))))))))) + ((((y * (y * y)) * (z * (y * (z * y)))) + (((z * (y * y)) * (z * (y * (z * y)))) + (((y * (z * y)) * (z * (y * (z * y)))) + (((z * (z * y)) * (z * (y * (z * y)))) + (((y * (y * z)) * (z * (y * (z * y)))) + (((z * (y * z)) * (z * (y * (z * y)))) + (((y * (z * z)) * (z * (y * (z * y)))) + ((z * (z * z)) * (z * (y * (z * y))))))))))) + ((((y * (y * y)) * (y * (z * (z * y)))) + (((z * (y * y)) * (y * (z * (z * y)))) + (((y * (z * y)) * (y * (z * (z * y)))) + (((z * (z * y)) * (y * (z * (z * y)))) + (((y * (y * z)) * (y * (z * (z * y)))) + (((z * (y * z)) * (y * (z * (z * y)))) + (((y * (z * z)) * (y * (z * (z * y)))) + ((z * (z * z)) * (y * (z * (z * y))))))))))) + ((((y * (y * y)) * (z * (z * (z * y)))) + (((z * (y * y)) * (z * (z * (z * y)))) + (((y * (z * y)) * (z * (z * (z * y)))) + (((z * (z * y)) * (z * (z * (z * y)))) + (((y * (y * z)) * (z * (z * (z * y)))) + (((z * (y * z)) * (z * (z * (z * y)))) + (((y * (z * z)) * (z * (z * (z * y)))) + ((z * (z * z)) * (z * (z * (z * y))))))))))) + (((y * (y * y)) * (y * (y * (y * z)))) + (((z * (y * y)) * (y * (y * (y * z)))) + (((y * (z * y)) * (y * (y * (y * z)))) + (((z * (z * y)) * (y * (y * (y * z)))) + (((y * (y * z)) * (y * (y * (y * z)))) + (((z * (y * z)) * (y * (y * (y * z)))) + (((y * (z * z)) * (y * (y * (y * z)))) + (((z * (z * z)) * (y * (y * (y * z)))) + (((y * (y * y)) * (z * (y * (y * z)))) + (((z * (y * y)) * (z * (y * (y * z)))) + (((y * (z * y)) * (z * (y * (y * z)))) + (((z * (z * y)) * (z * (y * (y * z)))) + (((y * (y * z)) * (z * (y * (y * z)))) + (((z * (y * z)) * (z * (y * (y * z)))) + (((y * (z * z)) * (z * (y * (y * z)))) + (((z * (z * z)) * (z * (y * (y * z)))) + (((y * (y * y)) * (y * (z * (y * z)))) + (((z * (y * y)) * (y * (z * (y * z)))) + (((y * (z * y)) * (y * (z * (y * z)))) + (((z * (z * y)) * (y * (z * (y * z)))) + (((y * (y * z)) * (y * (z * (y * z)))) + (((z * (y * z)) * (y * (z * (y * z)))) + (((y * (z * z)) * (y * (z * (y * z)))) + (((z * (z * z)) * (y * (z * (y * z)))) + (((y * (y * y)) * (z * (z * (y * z)))) + (((z * (y * y)) * (z * (z * (y * z)))) + (((y * (z * y)) * (z * (z * (y * z)))) + (((z * (z * y)) * (z * (z * (y * z)))) + (((y * (y * z)) * (z * (z * (y * z)))) + (((z * (y * z)) * (z * (z * (y * z)))) + (((y * (z * z)) * (z * (z * (y * z)))) + (((z * (z * z)) * (z * (z * (y * z)))) + (((y * (y * y)) * (y * (y * (z * z)))) + (((z * (y * y)) * (y * (y * (z * z)))) + (((y * (z * y)) * (y * (y * (z * z)))) + (((z * (z * y)) * (y * (y * (z * z)))) + (((y * (y * z)) * (y * (y * (z * z)))) + (((z * (y * z)) * (y * (y * (z * z)))) + (((y * (z * z)) * (y * (y * (z * z)))) + (((z * (z * z)) * (y * (y * (z * z)))) + (((y * (y * y)) * (z * (y * (z * z)))) + (((z * (y * y)) * (z * (y * (z * z)))) + (((y * (z * y)) * (z * (y * (z * z)))) + (((z * (z * y)) * (z * (y * (z * z)))) + (((y * (y * z)) * (z * (y * (z * z)))) + (((z * (y * z)) * (z * (y * (z * z)))) + (((y * (z * z)) * (z * (y * (z * z)))) + (((z * (z * z)) * (z * (y * (z * z)))) + (((y * (y * y)) * (y * (z * (z * z)))) + (((z * (y * y)) * (y * (z * (z * z)))) + (((y * (z * y)) * (y * (z * (z * z)))) + (((z * (z * y)) * (y * (z * (z * z)))) + (((y * (y * z)) * (y * (z * (z * z)))) + (((z * (y * z)) * (y * (z * (z * z)))) + (((y * (z * z)) * (y * (z * (z * z)))) + (((z * (z * z)) * (y * (z * (z * z)))) + (((y * (y * y)) * (z * (z * (z * z)))) + ((z * (z * (z * (z * (z * (z * z)))))) + (((z * (y * y)) * (z * (z * (z * z)))) + (((y * (z * y)) * (z * (z * (z * z)))) + (((z * (z * y)) * (z * (z * (z * z)))) + (((y * (y * z)) * (z * (z * (z * z)))) + (((z * (y * z)) * (z * (z * (z * z)))) + ((y * (z * z)) * (z * (z * (z * z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = (y + z) * ((y + z) * ((y + z) * ((y + z) * ((y + z) * ((y + z) * (y + z)))))). [para(6(a,1),386(a,1,1,2)),rewrite(7(3),7(6),4(8),6(9),7(3),6(12),7(8),6(15),7(13),7(18),4(21),4(22),4(23),6(28),7(27),7(30),4(32),6(33),7(27),6(36),7(32),6(39),7(37),7(42),4(45),4(46),4(47),6(48),7(27),6(52),7(34),6(56),7(41),6(60),7(48),6(64),7(55),6(68),7(62),6(72),7(69),7(76),4(80),4(81),4(82),4(83),4(84),4(85),4(86),6(87),7(27),386(6),7(30),7(33),7(36),7(39),7(42),7(45),6(138),7(82),7(85),7(88),7(91),7(94),7(97),7(100),6(189),7(137),7(140),7(143),7(146),7(149),7(152),7(155),6(240),7(192),7(195),7(198),7(201),7(204),7(207),7(210),6(291),7(247),7(250),7(253),7(256),7(259),7(262),7(265),6(342),7(302),7(305),7(308),7(311),7(314),7(317),7(320),6(393),7(357),7(360),7(363),7(366),7(369),7(372),7(375),6(444),7(412),7(415),7(418),7(421),7(424),7(427),7(430),6(495),7(467),7(470),7(473),7(476),7(479),7(482),7(485),6(546),7(522),7(525),7(528),7(531),7(534),7(537),7(540),6(597),7(577),7(580),7(583),7(586),7(589),7(592),7(595),6(648),7(632),7(635),7(638),7(641),7(644),7(647),7(650),6(699),7(687),7(690),7(693),7(696),7(699),7(702),7(705),6(750),7(742),7(745),7(748),7(751),7(754),7(757),7(760),6(801),7(797),7(800),7(803),7(806),7(809),7(812),7(815),7(852),7(855),7(858),7(861),7(864),7(867),7(870),386(873),5(874),16(875),16(876),16(877),16(878),16(879),4(881),4(880),4(879),4(878),4(877),4(876),4(875),4(882),4(881),4(880),4(879),4(878),4(877),4(876),4(883),4(882),4(881),4(880),4(879),4(878),4(877),4(884),4(883),4(882),4(881),4(880),4(879),4(878),4(885),4(884),4(883),4(882),4(881),4(880),4(879),4(886),4(885),4(884),4(883),4(882),4(881),4(880),4(887),4(886),4(885),4(884),4(883),4(882),4(881))]. Demod_limit (steps=-1, size=1819). The most recent kept clause is 445. From here on, a short message will be printed for each 100 times the limit is hit. given #64 (T,wt=28): 338 x + (y + (z + (u + (v + (w + (v6 + -x)))))) = y + (z + (u + (v + (w + v6)))). [para(223(a,1),224(a,2,2,2)),rewrite(4(7),4(6),4(5),4(4),223(8))]. given #65 (T,wt=28): 340 -x + (y + (z + (u + (v + (w + (v6 + x)))))) = y + (z + (u + (v + (w + v6)))). [para(223(a,1),261(a,2,2,2)),rewrite(4(7),4(6),4(5),4(4),223(8))]. given #66 (A,wt=63): 138 ((x * (x * y)) * z) + (((u * (u * y)) * z) + ((((u * x) * y) * z) + (((x * u) * y) * z))) = ((x * (x * y)) * z) + (((u * (x * y)) * z) + (((x * (u * y)) * z) + ((u * (u * y)) * z))). [para(22(a,1),7(a,1,1)),rewrite(7(12),7(12),7(12),7(27),7(27)),flip(a)]. given #67 (F,wt=28): 342 x + (y + (z + (u + (v + (w + (-x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(4(a,1),277(a,1,2,2,2,2)),rewrite(4(10))]. given #68 (F,wt=28): 379 -x + (y + (z + (u + (v + (w + (x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(279(a,1),4(a,1,1)),rewrite(4(5),4(4),4(3),4(2),4(12),4(11),4(10),4(9),4(8)),flip(a)]. given #69 (T,wt=31): 262 (x * (x * (y * (x * x)))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * (x * y)))). [para(26(a,1),9(a,1,1)),rewrite(8(13))]. given #70 (T,wt=31): 268 ((x * y) * (x * (x * y))) * (x * (y * x)) = (x * (y * x)) * ((x * y) * (x * (y * x))). [para(27(a,1),9(a,1,1))]. given #71 (A,wt=63): 139 (x * (x * (x * (x * y)))) + ((z * (z * y)) + (((z * (x * x)) * y) + ((x * (x * z)) * y))) = (x * (x * (x * (x * y)))) + ((z * (x * (x * y))) + ((x * (x * (z * y))) + (z * (z * y)))). [para(8(a,1),22(a,1,1,2)),rewrite(8(4),8(11),8(18),8(19),8(21),8(25))]. given #72 (F,wt=32): 343 x + (y + (z + (u + (v + (w + (v6 + (v7 + -x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(277(a,1),224(a,2,2,2)),rewrite(4(8),4(7),4(6),4(5),4(4),277(9))]. given #73 (F,wt=32): 344 -x + (y + (z + (u + (v + (w + (v6 + (v7 + x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(277(a,1),261(a,2,2,2)),rewrite(4(8),4(7),4(6),4(5),4(4),277(9))]. given #74 (T,wt=32): 453 x + (y + (z + (u + (v + (w + (v6 + (-x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(338(a,1),4(a,1,1)),rewrite(4(6),4(5),4(4),4(3),4(2),4(14),4(13),4(12),4(11),4(10),4(9)),flip(a)]. given #75 (T,wt=32): 457 -x + (y + (z + (u + (v + (w + (v6 + (x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(340(a,1),4(a,1,1)),rewrite(4(6),4(5),4(4),4(3),4(2),4(14),4(13),4(12),4(11),4(10),4(9)),flip(a)]. given #76 (A,wt=63): 140 (x * (x * y)) + ((z * (z * (z * (z * y)))) + (((z * (z * x)) * y) + ((x * (z * z)) * y))) = (x * (x * y)) + ((z * (z * (x * y))) + ((x * (z * (z * y))) + (z * (z * (z * (z * y)))))). [para(8(a,1),22(a,1,2,1,2)),rewrite(8(6),8(8),8(20),8(22),8(26),8(27))]. given #77 (F,wt=35): 217 (x * (x * (x * (x * (x * (x * (x * x))))))) * y = x * (x * (x * (x * (x * (x * (x * (x * y))))))). [para(24(a,1),8(a,1,1)),rewrite(24(15),24(16))]. given #78 (F,wt=35): 218 (x * (x * (x * (x * y)))) * (x * (x * (x * x))) = x * (x * (x * (x * (y * (x * (x * (x * x))))))). [para(24(a,1),9(a,1,1)),rewrite(24(16))]. given #79 (T,wt=35): 221 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_rewrite(216),rewrite(220(23))]. given #80 (T,wt=27): 622 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(221(a,1),49(a,1,2,2)),rewrite(49(13)),flip(a)]. given #81 (A,wt=67): 219 (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * x))))))))))))))) * y = x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * (x * y))))))))))))))). [para(24(a,1),24(a,1,1,2,2)),rewrite(24(14),24(15),24(29),24(30),24(31),24(32))]. Demod_limit hit 100 times. given #82 (F,wt=23): 699 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(622(a,1),15(a,1)),rewrite(15(7)),flip(a)]. given #83 (F,wt=23): 762 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(9(a,1),699(a,1,1))]. given #84 (T,wt=15): 813 x + ((y * z) * z) = x + (y * (z * z)). [para(762(a,1),49(a,1,2,2)),rewrite(50(10)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 3.17 (+ 0.01) seconds: right. % Length of proof is 29. % Level of proof is 13. % Maximum clause weight is 48. % Given clauses 84. 1 (y * x) * x = y * (x * x) # label(right) # label(goal). [goal]. 2 x + 0 = x. [assumption]. 3 x + -x = 0. [assumption]. 4 (x + y) + z = x + (y + z). [assumption]. 5 x + y = y + x. [assumption]. 6 x * (y + z) = (x * y) + (x * z). [assumption]. 7 (x + y) * z = (x * z) + (y * z). [assumption]. 8 (x * x) * y = x * (x * y) # label(left). [assumption]. 9 (x * y) * x = x * (y * x) # label(flexible). [assumption]. 10 (c1 * c2) * c2 != c1 * (c2 * c2) # label(right) # answer(right). [deny(1)]. 14 x + (-x + y) = 0 + y. [para(3(a,1),4(a,1,1)),flip(a)]. 15 0 + x = x. [para(5(a,1),2(a,1))]. 16 x + (y + z) = y + (x + z). [para(5(a,1),4(a,1,1)),rewrite(4(2))]. 17 x + (-x + y) = y. [back_rewrite(14),rewrite(15(5))]. 23 (x * (x * y)) + ((z * (z * y)) + (((x * z) * y) + ((z * x) * y))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y)))). [para(7(a,1),8(a,1,1)),rewrite(6(2),6(5),4(7),7(8),8(2),7(8),7(8),8(8),5(9),16(10),7(14),6(16),7(14),7(19),4(22))]. 36 --x = x. [para(3(a,1),17(a,1,2)),rewrite(2(2)),flip(a)]. 37 x + (y + -x) = y. [para(5(a,1),17(a,1,2))]. 46 -x + (y + x) = y. [para(36(a,1),37(a,1,2,2))]. 49 -x + (y + (x + z)) = y + z. [para(46(a,1),4(a,1,1)),rewrite(4(4)),flip(a)]. 50 -x + (y + (z + x)) = y + z. [para(4(a,1),46(a,1,2))]. 216 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = -(z * (z * y)) + ((x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y))))). [para(23(a,1),49(a,1,2)),flip(a)]. 220 -x + (y + (z + (u + x))) = y + (z + u). [para(4(a,1),50(a,1,2,2))]. 221 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_rewrite(216),rewrite(220(23))]. 622 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(221(a,1),49(a,1,2,2)),rewrite(49(13)),flip(a)]. 699 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(622(a,1),15(a,1)),rewrite(15(7)),flip(a)]. 762 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(9(a,1),699(a,1,1))]. 813 x + ((y * z) * z) = x + (y * (z * z)). [para(762(a,1),49(a,1,2,2)),rewrite(50(10)),flip(a)]. 843 (x * y) * y = x * (y * y). [para(813(a,1),15(a,1)),rewrite(15(4)),flip(a)]. 844 $F # answer(right). [resolve(843,a,10,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=84. Generated=12100. Kept=842. proofs=1. Usable=58. Sos=359. Demods=342. Limbo=8, Disabled=425. Hints=0. Weight_deleted=1428. Literals_deleted=0. Forward_subsumed=9830. Back_subsumed=63. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=703 (2 lex), Back_demodulated=353. Back_unit_deleted=0. Demod_attempts=706332. Demod_rewrites=113505. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=2.09. User_CPU=3.17, System_CPU=0.01, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3281 exit (max_proofs) Wed Nov 22 11:21:31 2006