============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10604 was started by mccune on cleo.thornwood, Sat Aug 12 20:57:11 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). (x * y) * x = x * (y * x). (B * A) * A != B * (A * A). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: ============================== 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). [assumption]. (x * y) * x = x * (y * x). [assumption]. (B * A) * A != B * (A * A). [assumption]. 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([ 0, A, B, *, +, - ]). After inverse_order: Function symbol precedence: lex([ 0, A, B, +, -, * ]). 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). 1 x + 0 = x. [assumption]. 2 x + -x = 0. [assumption]. 3 (x + y) + z = x + (y + z). [assumption]. 4 x + y = y + x. [assumption]. 5 x * (y + z) = (x * y) + (x * z). [assumption]. 6 (x + y) * z = (x * z) + (y * z). [assumption]. 7 (x * x) * y = x * (x * y). [assumption]. 8 (x * y) * x = x * (y * x). [assumption]. 9 (B * A) * A != B * (A * A). [assumption]. end_of_list. formulas(demodulators). 1 x + 0 = x. [assumption]. 2 x + -x = 0. [assumption]. 3 (x + y) + z = x + (y + z). [assumption]. 4 x + y = y + x. [assumption]. % (lex-dep) 5 x * (y + z) = (x * y) + (x * z). [assumption]. 6 (x + y) * z = (x * z) + (y * z). [assumption]. 7 (x * x) * y = x * (x * y). [assumption]. 8 (x * y) * x = x * (y * x). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 1 x + 0 = x. [assumption]. given #2 (I,wt=6): 2 x + -x = 0. [assumption]. given #3 (I,wt=11): 3 (x + y) + z = x + (y + z). [assumption]. given #4 (I,wt=7): 4 x + y = y + x. [assumption]. % Operation + is associative-commutative; CAC redundancy checks enabled. given #5 (I,wt=13): 5 x * (y + z) = (x * y) + (x * z). [assumption]. given #6 (I,wt=13): 6 (x + y) * z = (x * z) + (y * z). [assumption]. given #7 (I,wt=11): 7 (x * x) * y = x * (x * y). [assumption]. given #8 (I,wt=11): 8 (x * y) * x = x * (y * x). [assumption]. given #9 (I,wt=11): 9 (B * A) * A != B * (A * A). [assumption]. given #10 (T,wt=5): 14 0 + x = x. [para(4(a,1),1(a,1))]. given #11 (A,wt=10): 12 x + (y + -(x + y)) = 0. [para(3(a,1),2(a,1))]. given #12 (F,wt=4): 27 -0 = 0. [para(14(a,1),2(a,1))]. given #13 (F,wt=8): 16 x + (-x + y) = y. [back_rewrite(13),rewrite(14(5))]. given #14 (T,wt=5): 35 --x = x. [para(2(a,1),16(a,1,2)),rewrite(1(2)),flip(a)]. given #15 (T,wt=8): 36 x + (y + -x) = y. [para(4(a,1),16(a,1,2))]. given #16 (A,wt=11): 15 x + (y + z) = y + (x + z). [para(4(a,1),3(a,1,1)),rewrite(3(2))]. given #17 (F,wt=8): 45 -x + (y + x) = y. [para(35(a,1),36(a,1,2,2))]. given #18 (F,wt=9): 39 x + -(-y + x) = y. [para(12(a,1),16(a,1,2)),rewrite(1(2)),flip(a)]. given #19 (T,wt=9): 55 x + -(x + y) = -y. [para(45(a,1),45(a,1,2)),rewrite(4(3))]. given #20 (T,wt=10): 72 -(x + y) = -y + -x. [para(45(a,1),55(a,1,2,1)),flip(a)]. given #21 (A,wt=11): 17 (x * y) + (x * 0) = x * y. [para(1(a,1),5(a,1,2)),flip(a)]. given #22 (F,wt=11): 19 (x * y) + (0 * y) = x * y. [para(1(a,1),6(a,1,1)),flip(a)]. given #23 (F,wt=11): 28 (x * 0) + (x * y) = x * y. [para(14(a,1),5(a,1,2)),flip(a)]. given #24 (T,wt=5): 96 x * 0 = 0. [para(28(a,1),45(a,1,2)),rewrite(4(4),2(4)),flip(a)]. given #25 (T,wt=9): 98 0 * (0 * x) = 0 * x. [para(96(a,1),7(a,1,1)),flip(a)]. given #26 (A,wt=12): 20 (x * y) + (-x * y) = 0 * y. [para(2(a,1),6(a,1,1)),flip(a)]. given #27 (F,wt=9): 99 x * (0 * x) = 0 * x. [para(96(a,1),8(a,1,1)),flip(a)]. given #28 (F,wt=10): 97 (x * y) + (x * -y) = 0. [back_rewrite(18),rewrite(96(6))]. given #29 (T,wt=9): 124 -(x * -y) = x * y. [para(97(a,1),45(a,1,2)),rewrite(4(5),14(5))]. given #30 (T,wt=9): 129 x * -y = -(x * y). [para(124(a,1),35(a,1,1)),flip(a)]. given #31 (A,wt=47): 21 (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(5(a,1),7(a,1,1)),rewrite(6(2),6(5),3(7),6(8),7(2),6(8),6(8),7(8),4(9),15(10),6(14),5(16),6(14),6(19),3(22))]. given #32 (F,wt=10): 115 -x * (0 * x) = 0 * x. [para(99(a,1),20(a,1,1)),rewrite(100(7),98(8))]. given #33 (F,wt=11): 29 (0 * x) + (y * x) = y * x. [para(14(a,1),6(a,1,1)),flip(a)]. given #34 (T,wt=5): 180 0 * x = 0. [para(29(a,1),45(a,1,2)),rewrite(4(4),2(4)),flip(a)]. given #35 (T,wt=9): 183 -(-x * y) = x * y. [back_rewrite(109),rewrite(180(2),14(5))]. given #36 (A,wt=47): 22 (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(6(a,1),7(a,1,1)),rewrite(5(2),5(5),3(7),6(8),7(2),6(8),6(8),7(8),4(9),15(10),6(14),5(16),6(14),6(19),3(22))]. given #37 (F,wt=9): 195 -x * y = -(x * y). [para(183(a,1),35(a,1,1)),flip(a)]. given #38 (F,wt=12): 40 x + (y + (-x + z)) = y + z. [para(36(a,1),3(a,1,1)),rewrite(3(4)),flip(a)]. given #39 (T,wt=12): 42 x + (y + (z + -x)) = y + z. [para(3(a,1),36(a,1,2))]. given #40 (T,wt=12): 48 -x + (y + (x + z)) = y + z. [para(45(a,1),3(a,1,1)),rewrite(3(4)),flip(a)]. given #41 (A,wt=19): 23 (x * (x * (x * x))) * y = x * (x * (x * (x * y))). [para(7(a,1),7(a,1,1)),rewrite(7(7),7(8))]. given #42 (F,wt=12): 49 -x + (y + (z + x)) = y + z. [para(3(a,1),45(a,1,2))]. given #43 (F,wt=16): 208 x + (y + (z + (-x + u))) = y + (z + u). [para(3(a,1),40(a,1,2)),rewrite(3(7))]. given #44 (T,wt=16): 209 x + (y + (z + (u + -x))) = y + (z + u). [para(3(a,1),42(a,1,2,2))]. given #45 (T,wt=16): 211 -x + (y + (z + (x + u))) = y + (z + u). [para(3(a,1),48(a,1,2)),rewrite(3(7))]. given #46 (A,wt=47): 24 (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(8(a,1),5(a,1)),rewrite(5(3),5(5),6(3),6(8),3(11),6(13),6(15),8(13),6(18),6(20),8(20),3(22)),flip(a)]. given #47 (F,wt=16): 219 -x + (y + (z + (u + x))) = y + (z + u). [para(3(a,1),49(a,1,2,2))]. given #48 (F,wt=19): 25 (x * (x * y)) * (x * x) = x * (x * (y * (x * x))). [para(7(a,1),8(a,1,1)),rewrite(7(8))]. given #49 (T,wt=19): 26 (x * (y * x)) * (x * y) = (x * y) * (x * (x * y)). [para(8(a,1),8(a,1,1))]. given #50 (T,wt=20): 222 x + (y + (z + (u + (-x + v)))) = y + (z + (u + v)). [para(3(a,1),208(a,1,2,2)),rewrite(3(8))]. given #51 (A,wt=51): 134 (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(21(a,1),3(a,1,1)),rewrite(3(12),3(11),3(10),3(23),3(22)),flip(a)]. given #52 (F,wt=20): 223 x + (y + (z + (u + (v + -x)))) = y + (z + (u + v)). [para(3(a,1),209(a,1,2,2,2))]. given #53 (F,wt=20): 224 -x + (y + (z + (u + (x + v)))) = y + (z + (u + v)). [para(3(a,1),211(a,1,2,2)),rewrite(3(8))]. given #54 (T,wt=20): 260 -x + (y + (z + (u + (v + x)))) = y + (z + (u + v)). [para(3(a,1),219(a,1,2,2,2))]. given #55 (T,wt=24): 276 x + (y + (z + (u + (v + (-x + w))))) = y + (z + (u + (v + w))). [para(3(a,1),222(a,1,2,2,2)),rewrite(3(9))]. given #56 (A,wt=63): 135 (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(21(a,1),5(a,1,2)),rewrite(5(12),5(12),5(12),5(27),5(27)),flip(a)]. given #57 (F,wt=24): 277 x + (y + (z + (u + (v + (w + -x))))) = y + (z + (u + (v + w))). [para(222(a,1),209(a,2,2)),rewrite(3(7),3(6),3(5),3(4),222(8))]. given #58 (F,wt=24): 278 -x + (y + (z + (u + (v + (w + x))))) = y + (z + (u + (v + w))). [para(222(a,1),219(a,2,2)),rewrite(3(7),3(6),3(5),3(4),222(8))]. given #59 (T,wt=24): 338 -x + (y + (z + (u + (v + (x + w))))) = y + (z + (u + (v + w))). [para(3(a,1),224(a,1,2,2,2)),rewrite(3(9))]. given #60 (T,wt=27): 266 (x * (y * (y * x))) * (x * (y * y)) = (x * (y * y)) * (x * (x * (y * y))). [para(7(a,1),26(a,1,1,2))]. given #61 (A,wt=95): 136 (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(5(a,1),21(a,1,1,2)),rewrite(5(4),5(7),5(9),5(13),5(18),3(21),3(22),3(23),5(25),5(27),5(30),5(32),5(35),5(37),5(40),5(42),3(44),3(45),3(46))]. given #62 (F,wt=27): 268 (x * (x * (y * x))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * y))). [para(8(a,1),26(a,1,1,2))]. given #63 (F,wt=27): 385 (x * (x * x)) * (x * (x * (x * x))) = x * (x * (x * (x * (x * (x * x))))). [para(266(a,1),23(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(5(a,1),385(a,1,1,2)),rewrite(6(3),6(6),3(8),5(9),6(3),5(12),6(8),5(15),6(13),6(18),3(21),3(22),3(23),5(28),6(27),6(30),3(32),5(33),6(27),5(36),6(32),5(39),6(37),6(42),3(45),3(46),3(47),5(48),6(27),5(52),6(34),5(56),6(41),5(60),6(48),5(64),6(55),5(68),6(62),5(72),6(69),6(76),3(80),3(81),3(82),3(83),3(84),3(85),3(86),5(87),6(27),385(6),6(30),6(33),6(36),6(39),6(42),6(45),5(138),6(82),6(85),6(88),6(91),6(94),6(97),6(100),5(189),6(137),6(140),6(143),6(146),6(149),6(152),6(155),5(240),6(192),6(195),6(198),6(201),6(204),6(207),6(210),5(291),6(247),6(250),6(253),6(256),6(259),6(262),6(265),5(342),6(302),6(305),6(308),6(311),6(314),6(317),6(320),5(393),6(357),6(360),6(363),6(366),6(369),6(372),6(375),5(444),6(412),6(415),6(418),6(421),6(424),6(427),6(430),5(495),6(467),6(470),6(473),6(476),6(479),6(482),6(485),5(546),6(522),6(525),6(528),6(531),6(534),6(537),6(540),5(597),6(577),6(580),6(583),6(586),6(589),6(592),6(595),5(648),6(632),6(635),6(638),6(641),6(644),6(647),6(650),5(699),6(687),6(690),6(693),6(696),6(699),6(702),6(705),5(750),6(742),6(745),6(748),6(751),6(754),6(757),6(760),5(801),6(797),6(800),6(803),6(806),6(809),6(812),6(815),6(852),6(855),6(858),6(861),6(864),6(867),6(870),385(873),4(874),15(875),15(876),15(877),15(878),15(879),3(881),3(880),3(879),3(878),3(877),3(876),3(875),3(882),3(881),3(880),3(879),3(878),3(877),3(876),3(883),3(882),3(881),3(880),3(879),3(878),3(877),3(884),3(883),3(882),3(881),3(880),3(879),3(878),3(885),3(884),3(883),3(882),3(881),3(880),3(879),3(886),3(885),3(884),3(883),3(882),3(881),3(880),3(887),3(886),3(885),3(884),3(883),3(882),3(881))]. Demod_limit (steps=-1, size=1819). The most recent kept clause is 444. From here on, a short message will be printed for each 100 times the limit is hit. given #64 (T,wt=28): 337 x + (y + (z + (u + (v + (w + (v6 + -x)))))) = y + (z + (u + (v + (w + v6)))). [para(222(a,1),223(a,2,2,2)),rewrite(3(7),3(6),3(5),3(4),222(8))]. given #65 (T,wt=28): 339 -x + (y + (z + (u + (v + (w + (v6 + x)))))) = y + (z + (u + (v + (w + v6)))). [para(222(a,1),260(a,2,2,2)),rewrite(3(7),3(6),3(5),3(4),222(8))]. given #66 (A,wt=63): 137 ((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(21(a,1),6(a,1,1)),rewrite(6(12),6(12),6(12),6(27),6(27)),flip(a)]. given #67 (F,wt=28): 341 x + (y + (z + (u + (v + (w + (-x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(3(a,1),276(a,1,2,2,2,2)),rewrite(3(10))]. given #68 (F,wt=28): 378 -x + (y + (z + (u + (v + (w + (x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(278(a,1),3(a,1,1)),rewrite(3(5),3(4),3(3),3(2),3(12),3(11),3(10),3(9),3(8)),flip(a)]. given #69 (T,wt=31): 261 (x * (x * (y * (x * x)))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * (x * y)))). [para(25(a,1),8(a,1,1)),rewrite(7(13))]. given #70 (T,wt=31): 267 ((x * y) * (x * (x * y))) * (x * (y * x)) = (x * (y * x)) * ((x * y) * (x * (y * x))). [para(26(a,1),8(a,1,1))]. given #71 (A,wt=63): 138 (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(7(a,1),21(a,1,1,2)),rewrite(7(4),7(11),7(18),7(19),7(21),7(25))]. given #72 (F,wt=32): 342 x + (y + (z + (u + (v + (w + (v6 + (v7 + -x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(276(a,1),223(a,2,2,2)),rewrite(3(8),3(7),3(6),3(5),3(4),276(9))]. given #73 (F,wt=32): 343 -x + (y + (z + (u + (v + (w + (v6 + (v7 + x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(276(a,1),260(a,2,2,2)),rewrite(3(8),3(7),3(6),3(5),3(4),276(9))]. given #74 (T,wt=32): 452 x + (y + (z + (u + (v + (w + (v6 + (-x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(337(a,1),3(a,1,1)),rewrite(3(6),3(5),3(4),3(3),3(2),3(14),3(13),3(12),3(11),3(10),3(9)),flip(a)]. given #75 (T,wt=32): 456 -x + (y + (z + (u + (v + (w + (v6 + (x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(339(a,1),3(a,1,1)),rewrite(3(6),3(5),3(4),3(3),3(2),3(14),3(13),3(12),3(11),3(10),3(9)),flip(a)]. given #76 (A,wt=63): 139 (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(7(a,1),21(a,1,2,1,2)),rewrite(7(6),7(8),7(20),7(22),7(26),7(27))]. given #77 (F,wt=35): 216 (x * (x * (x * (x * (x * (x * (x * x))))))) * y = x * (x * (x * (x * (x * (x * (x * (x * y))))))). [para(23(a,1),7(a,1,1)),rewrite(23(15),23(16))]. given #78 (F,wt=35): 217 (x * (x * (x * (x * y)))) * (x * (x * (x * x))) = x * (x * (x * (x * (y * (x * (x * (x * x))))))). [para(23(a,1),8(a,1,1)),rewrite(23(16))]. given #79 (T,wt=35): 220 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_rewrite(215),rewrite(219(23))]. given #80 (T,wt=27): 621 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(220(a,1),48(a,1,2,2)),rewrite(48(13)),flip(a)]. given #81 (A,wt=67): 218 (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(23(a,1),23(a,1,1,2,2)),rewrite(23(14),23(15),23(29),23(30),23(31),23(32))]. Demod_limit hit 100 times. given #82 (F,wt=23): 698 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(621(a,1),14(a,1)),rewrite(14(7)),flip(a)]. given #83 (F,wt=23): 761 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(8(a,1),698(a,1,1))]. given #84 (T,wt=15): 812 x + ((y * z) * z) = x + (y * (z * z)). [para(761(a,1),48(a,1,2,2)),rewrite(49(10)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 3.06 (+ 0.00) seconds. % Length of proof is 28. % Level of proof is 13. % Maximum clause weight is 48. % Given clauses 84. 1 x + 0 = x. [assumption]. 2 x + -x = 0. [assumption]. 3 (x + y) + z = x + (y + z). [assumption]. 4 x + y = y + x. [assumption]. 5 x * (y + z) = (x * y) + (x * z). [assumption]. 6 (x + y) * z = (x * z) + (y * z). [assumption]. 7 (x * x) * y = x * (x * y). [assumption]. 8 (x * y) * x = x * (y * x). [assumption]. 9 (B * A) * A != B * (A * A). [assumption]. 13 x + (-x + y) = 0 + y. [para(2(a,1),3(a,1,1)),flip(a)]. 14 0 + x = x. [para(4(a,1),1(a,1))]. 15 x + (y + z) = y + (x + z). [para(4(a,1),3(a,1,1)),rewrite(3(2))]. 16 x + (-x + y) = y. [back_rewrite(13),rewrite(14(5))]. 22 (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(6(a,1),7(a,1,1)),rewrite(5(2),5(5),3(7),6(8),7(2),6(8),6(8),7(8),4(9),15(10),6(14),5(16),6(14),6(19),3(22))]. 35 --x = x. [para(2(a,1),16(a,1,2)),rewrite(1(2)),flip(a)]. 36 x + (y + -x) = y. [para(4(a,1),16(a,1,2))]. 45 -x + (y + x) = y. [para(35(a,1),36(a,1,2,2))]. 48 -x + (y + (x + z)) = y + z. [para(45(a,1),3(a,1,1)),rewrite(3(4)),flip(a)]. 49 -x + (y + (z + x)) = y + z. [para(3(a,1),45(a,1,2))]. 215 (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(22(a,1),48(a,1,2)),flip(a)]. 219 -x + (y + (z + (u + x))) = y + (z + u). [para(3(a,1),49(a,1,2,2))]. 220 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_rewrite(215),rewrite(219(23))]. 621 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(220(a,1),48(a,1,2,2)),rewrite(48(13)),flip(a)]. 698 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(621(a,1),14(a,1)),rewrite(14(7)),flip(a)]. 761 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(8(a,1),698(a,1,1))]. 812 x + ((y * z) * z) = x + (y * (z * z)). [para(761(a,1),48(a,1,2,2)),rewrite(49(10)),flip(a)]. 842 (x * y) * y = x * (y * y). [para(812(a,1),14(a,1)),rewrite(14(4)),flip(a)]. 843 $F. [resolve(842,a,9,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=1.88. User_CPU=3.06, System_CPU=0.00, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10604 exit (max_proofs) Sat Aug 12 20:57:15 2006