============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 12983 was started by mccune on cleo.thornwood, Mon Jun 19 16:39:33 2006 The command was "/home/mccune/bin/prover9 -f na-ring-1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file na-ring-1.in clauses(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 INITIAL CLAUSES =============== % Clauses before input processing: clauses(usable). end_of_list. clauses(sos). 1 x + 0 = x. [input]. 2 x + - x = 0. [input]. 3 (x + y) + z = x + (y + z). [input]. 4 x + y = y + x. [input]. 5 x * (y + z) = (x * y) + (x * z). [input]. 6 (x + y) * z = (x * z) + (y * z). [input]. 7 (x * x) * y = x * (x * y). [input]. 8 (x * y) * x = x * (y * x). [input]. 9 (B * A) * A != B * (A * A). [input]. end_of_list. clauses(demodulators). end_of_list. Predicate elimination: (none). 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 associative-commutative; redundancy checks enabled. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. 14 x * (y + z) = (x * y) + (x * z). [input]. 15 (x + y) * z = (x * z) + (y * z). [input]. 16 (x * x) * y = x * (x * y). [input]. 17 (x * y) * x = x * (y * x). [input]. 18 (B * A) * A != B * (A * A). [input]. end_of_list. clauses(demodulators). 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. % (lex-dep) 14 x * (y + z) = (x * y) + (x * z). [input]. 15 (x + y) * z = (x * z) + (y * z). [input]. 16 (x * x) * y = x * (x * y). [input]. 17 (x * y) * x = x * (y * x). [input]. end_of_list. clauses(denials). end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=5): 10 x + 0 = x. [input]. given #2 (I,wt=6): 11 x + - x = 0. [input]. given #3 (I,wt=11): 12 (x + y) + z = x + (y + z). [input]. given #4 (I,wt=7): 13 x + y = y + x. [input]. given #5 (I,wt=13): 14 x * (y + z) = (x * y) + (x * z). [input]. given #6 (I,wt=13): 15 (x + y) * z = (x * z) + (y * z). [input]. given #7 (I,wt=11): 16 (x * x) * y = x * (x * y). [input]. given #8 (I,wt=11): 17 (x * y) * x = x * (y * x). [input]. given #9 (I,wt=11): 18 (B * A) * A != B * (A * A). [input]. given #10 (T,wt=5): 23 0 + x = x. [para(13(a,1),10(a,1))]. given #11 (A,wt=10): 21 x + (y + - (x + y)) = 0. [para(12(a,1),11(a,1))]. given #12 (F,wt=4): 36 - 0 = 0. [para(23(a,1),11(a,1))]. given #13 (F,wt=8): 25 x + (- x + y) = y. [back_demod(22),demod(23(5))]. given #14 (T,wt=5): 44 - - x = x. [para(11(a,1),25(a,1,2)),demod(10(2)),flip(a)]. given #15 (T,wt=8): 45 x + (y + - x) = y. [para(13(a,1),25(a,1,2))]. given #16 (A,wt=11): 24 x + (y + z) = y + (x + z). [para(13(a,1),12(a,1,1)),demod(12(2))]. given #17 (F,wt=8): 54 - x + (y + x) = y. [para(44(a,1),45(a,1,2,2))]. given #18 (F,wt=9): 48 x + - (- y + x) = y. [para(21(a,1),25(a,1,2)),demod(10(2)),flip(a)]. given #19 (T,wt=9): 64 x + - (x + y) = - y. [para(54(a,1),54(a,1,2)),demod(13(3))]. given #20 (T,wt=10): 81 - (x + y) = - y + - x. [para(54(a,1),64(a,1,2,1)),flip(a)]. given #21 (A,wt=11): 26 (x * y) + (x * 0) = x * y. [para(10(a,1),14(a,1,2)),flip(a)]. given #22 (F,wt=11): 28 (x * y) + (0 * y) = x * y. [para(10(a,1),15(a,1,1)),flip(a)]. given #23 (F,wt=11): 37 (x * 0) + (x * y) = x * y. [para(23(a,1),14(a,1,2)),flip(a)]. given #24 (T,wt=5): 105 x * 0 = 0. [para(37(a,1),54(a,1,2)),demod(13(4),11(4)),flip(a)]. given #25 (T,wt=9): 107 0 * (0 * x) = 0 * x. [para(105(a,1),16(a,1,1)),flip(a)]. given #26 (A,wt=12): 29 (x * y) + (- x * y) = 0 * y. [para(11(a,1),15(a,1,1)),flip(a)]. given #27 (F,wt=9): 108 x * (0 * x) = 0 * x. [para(105(a,1),17(a,1,1)),flip(a)]. given #28 (F,wt=10): 106 (x * y) + (x * - y) = 0. [back_demod(27),demod(105(6))]. given #29 (T,wt=9): 133 - (x * - y) = x * y. [para(106(a,1),54(a,1,2)),demod(13(5),23(5))]. given #30 (T,wt=9): 138 x * - y = - (x * y). [para(133(a,1),44(a,1,1)),flip(a)]. given #31 (A,wt=47): 30 (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(14(a,1),16(a,1,1)),demod(15(2),15(5),12(7),15(8),16(2),15(8),15(8),16(8),13(9),24(10),15(14),14(16),15(14),15(19),12(22))]. given #32 (F,wt=10): 124 - x * (0 * x) = 0 * x. [para(108(a,1),29(a,1,1)),demod(109(7),107(8))]. given #33 (F,wt=11): 38 (0 * x) + (y * x) = y * x. [para(23(a,1),15(a,1,1)),flip(a)]. given #34 (T,wt=5): 189 0 * x = 0. [para(38(a,1),54(a,1,2)),demod(13(4),11(4)),flip(a)]. given #35 (T,wt=9): 192 - (- x * y) = x * y. [back_demod(118),demod(189(2),23(5))]. given #36 (A,wt=47): 31 (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(15(a,1),16(a,1,1)),demod(14(2),14(5),12(7),15(8),16(2),15(8),15(8),16(8),13(9),24(10),15(14),14(16),15(14),15(19),12(22))]. given #37 (F,wt=9): 204 - x * y = - (x * y). [para(192(a,1),44(a,1,1)),flip(a)]. given #38 (F,wt=12): 49 x + (y + (- x + z)) = y + z. [para(45(a,1),12(a,1,1)),demod(12(4)),flip(a)]. given #39 (T,wt=12): 51 x + (y + (z + - x)) = y + z. [para(12(a,1),45(a,1,2))]. given #40 (T,wt=12): 57 - x + (y + (x + z)) = y + z. [para(54(a,1),12(a,1,1)),demod(12(4)),flip(a)]. given #41 (A,wt=19): 32 (x * (x * (x * x))) * y = x * (x * (x * (x * y))). [para(16(a,1),16(a,1,1)),demod(16(7),16(8))]. given #42 (F,wt=12): 58 - x + (y + (z + x)) = y + z. [para(12(a,1),54(a,1,2))]. given #43 (F,wt=16): 217 x + (y + (z + (- x + u))) = y + (z + u). [para(12(a,1),49(a,1,2)),demod(12(7))]. given #44 (T,wt=16): 218 x + (y + (z + (u + - x))) = y + (z + u). [para(12(a,1),51(a,1,2,2))]. given #45 (T,wt=16): 220 - x + (y + (z + (x + u))) = y + (z + u). [para(12(a,1),57(a,1,2)),demod(12(7))]. given #46 (A,wt=47): 33 (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(17(a,1),14(a,1)),demod(14(3),14(5),15(3),15(8),12(11),15(13),15(15),17(13),15(18),15(20),17(20),12(22)),flip(a)]. given #47 (F,wt=16): 228 - x + (y + (z + (u + x))) = y + (z + u). [para(12(a,1),58(a,1,2,2))]. given #48 (F,wt=19): 34 (x * (x * y)) * (x * x) = x * (x * (y * (x * x))). [para(16(a,1),17(a,1,1)),demod(16(8))]. given #49 (T,wt=19): 35 (x * (y * x)) * (x * y) = (x * y) * (x * (x * y)). [para(17(a,1),17(a,1,1))]. given #50 (T,wt=20): 231 x + (y + (z + (u + (- x + v)))) = y + (z + (u + v)). [para(12(a,1),217(a,1,2,2)),demod(12(8))]. given #51 (A,wt=51): 143 (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(30(a,1),12(a,1,1)),demod(12(12),12(11),12(10),12(23),12(22)),flip(a)]. given #52 (F,wt=20): 232 x + (y + (z + (u + (v + - x)))) = y + (z + (u + v)). [para(12(a,1),218(a,1,2,2,2))]. given #53 (F,wt=20): 233 - x + (y + (z + (u + (x + v)))) = y + (z + (u + v)). [para(12(a,1),220(a,1,2,2)),demod(12(8))]. given #54 (T,wt=20): 269 - x + (y + (z + (u + (v + x)))) = y + (z + (u + v)). [para(12(a,1),228(a,1,2,2,2))]. given #55 (T,wt=24): 285 x + (y + (z + (u + (v + (- x + w))))) = y + (z + (u + (v + w))). [para(12(a,1),231(a,1,2,2,2)),demod(12(9))]. given #56 (A,wt=63): 144 (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(30(a,1),14(a,1,2)),demod(14(12),14(12),14(12),14(27),14(27)),flip(a)]. given #57 (F,wt=24): 286 x + (y + (z + (u + (v + (w + - x))))) = y + (z + (u + (v + w))). [para(231(a,1),218(a,2,2)),demod(12(7),12(6),12(5),12(4),231(8))]. given #58 (F,wt=24): 287 - x + (y + (z + (u + (v + (w + x))))) = y + (z + (u + (v + w))). [para(231(a,1),228(a,2,2)),demod(12(7),12(6),12(5),12(4),231(8))]. given #59 (T,wt=24): 347 - x + (y + (z + (u + (v + (x + w))))) = y + (z + (u + (v + w))). [para(12(a,1),233(a,1,2,2,2)),demod(12(9))]. given #60 (T,wt=27): 275 (x * (y * (y * x))) * (x * (y * y)) = (x * (y * y)) * (x * (x * (y * y))). [para(16(a,1),35(a,1,1,2))]. given #61 (A,wt=95): 145 (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(14(a,1),30(a,1,1,2)),demod(14(4),14(7),14(9),14(13),14(18),12(21),12(22),12(23),14(25),14(27),14(30),14(32),14(35),14(37),14(40),14(42),12(44),12(45),12(46))]. given #62 (F,wt=27): 277 (x * (x * (y * x))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * y))). [para(17(a,1),35(a,1,1,2))]. given #63 (F,wt=27): 394 (x * (x * x)) * (x * (x * (x * x))) = x * (x * (x * (x * (x * (x * x))))). [para(275(a,1),32(a,1))]. Demod_limit: 0 ((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(14(a,1),394(a,1,1,2)),demod(15(3),15(6),12(8),14(9),15(3),14(12),15(8),14(15),15(13),15(18),12(21),12(22),12(23),14(28),15(27),15(30),12(32),14(33),15(27),14(36),15(32),14(39),15(37),15(42),12(45),12(46),12(47),14(48),15(27),14(52),15(34),14(56),15(41),14(60),15(48),14(64),15(55),14(68),15(62),14(72),15(69),15(76),12(80),12(81),12(82),12(83),12(84),12(85),12(86),14(87),15(27),394(6),15(30),15(33),15(36),15(39),15(42),15(45),14(138),15(82),15(85),15(88),15(91),15(94),15(97),15(100),14(189),15(137),15(140),15(143),15(146),15(149),15(152),15(155),14(240),15(192),15(195),15(198),15(201),15(204),15(207),15(210),14(291),15(247),15(250),15(253),15(256),15(259),15(262),15(265),14(342),15(302),15(305),15(308),15(311),15(314),15(317),15(320),14(393),15(357),15(360),15(363),15(366),15(369),15(372),15(375),14(444),15(412),15(415),15(418),15(421),15(424),15(427),15(430),14(495),15(467),15(470),15(473),15(476),15(479),15(482),15(485),14(546),15(522),15(525),15(528),15(531),15(534),15(537),15(540),14(597),15(577),15(580),15(583),15(586),15(589),15(592),15(595),14(648),15(632),15(635),15(638),15(641),15(644),15(647),15(650),14(699),15(687),15(690),15(693),15(696),15(699),15(702),15(705),14(750),15(742),15(745),15(748),15(751),15(754),15(757),15(760),14(801),15(797),15(800),15(803),15(806),15(809),15(812),15(815),15(852),15(855),15(858),15(861),15(864),15(867),15(870),394(873),13(874),24(875),24(876),24(877),24(878),24(879),12(881),12(880),12(879),12(878),12(877),12(876),12(875),12(882),12(881),12(880),12(879),12(878),12(877),12(876),12(883),12(882),12(881),12(880),12(879),12(878),12(877),12(884),12(883),12(882),12(881),12(880),12(879),12(878),12(885),12(884),12(883),12(882),12(881),12(880),12(879),12(886),12(885),12(884),12(883),12(882),12(881),12(880),12(887),12(886),12(885),12(884),12(883),12(882),12(881))]. Demod_limit (steps=-1, size=1819). The most recent kept clause is 453. From here on, a short message will be printed for each 100 times the limit is hit. given #64 (T,wt=28): 346 x + (y + (z + (u + (v + (w + (v6 + - x)))))) = y + (z + (u + (v + (w + v6)))). [para(231(a,1),232(a,2,2,2)),demod(12(7),12(6),12(5),12(4),231(8))]. given #65 (T,wt=28): 348 - x + (y + (z + (u + (v + (w + (v6 + x)))))) = y + (z + (u + (v + (w + v6)))). [para(231(a,1),269(a,2,2,2)),demod(12(7),12(6),12(5),12(4),231(8))]. given #66 (A,wt=63): 146 ((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(30(a,1),15(a,1,1)),demod(15(12),15(12),15(12),15(27),15(27)),flip(a)]. given #67 (F,wt=28): 350 x + (y + (z + (u + (v + (w + (- x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(12(a,1),285(a,1,2,2,2,2)),demod(12(10))]. given #68 (F,wt=28): 387 - x + (y + (z + (u + (v + (w + (x + v6)))))) = y + (z + (u + (v + (w + v6)))). [para(287(a,1),12(a,1,1)),demod(12(5),12(4),12(3),12(2),12(12),12(11),12(10),12(9),12(8)),flip(a)]. given #69 (T,wt=31): 270 (x * (x * (y * (x * x)))) * (x * (x * y)) = (x * (x * y)) * (x * (x * (x * (x * y)))). [para(34(a,1),17(a,1,1)),demod(16(13))]. given #70 (T,wt=31): 276 ((x * y) * (x * (x * y))) * (x * (y * x)) = (x * (y * x)) * ((x * y) * (x * (y * x))). [para(35(a,1),17(a,1,1))]. given #71 (A,wt=63): 147 (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(16(a,1),30(a,1,1,2)),demod(16(4),16(11),16(18),16(19),16(21),16(25))]. given #72 (F,wt=32): 351 x + (y + (z + (u + (v + (w + (v6 + (v7 + - x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(285(a,1),232(a,2,2,2)),demod(12(8),12(7),12(6),12(5),12(4),285(9))]. given #73 (F,wt=32): 352 - x + (y + (z + (u + (v + (w + (v6 + (v7 + x))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(285(a,1),269(a,2,2,2)),demod(12(8),12(7),12(6),12(5),12(4),285(9))]. given #74 (T,wt=32): 461 x + (y + (z + (u + (v + (w + (v6 + (- x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(346(a,1),12(a,1,1)),demod(12(6),12(5),12(4),12(3),12(2),12(14),12(13),12(12),12(11),12(10),12(9)),flip(a)]. given #75 (T,wt=32): 465 - x + (y + (z + (u + (v + (w + (v6 + (x + v7))))))) = y + (z + (u + (v + (w + (v6 + v7))))). [para(348(a,1),12(a,1,1)),demod(12(6),12(5),12(4),12(3),12(2),12(14),12(13),12(12),12(11),12(10),12(9)),flip(a)]. given #76 (A,wt=63): 148 (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(16(a,1),30(a,1,2,1,2)),demod(16(6),16(8),16(20),16(22),16(26),16(27))]. given #77 (F,wt=35): 225 (x * (x * (x * (x * (x * (x * (x * x))))))) * y = x * (x * (x * (x * (x * (x * (x * (x * y))))))). [para(32(a,1),16(a,1,1)),demod(32(15),32(16))]. given #78 (F,wt=35): 226 (x * (x * (x * (x * y)))) * (x * (x * (x * x))) = x * (x * (x * (x * (y * (x * (x * (x * x))))))). [para(32(a,1),17(a,1,1)),demod(32(16))]. given #79 (T,wt=35): 229 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_demod(224),demod(228(23))]. given #80 (T,wt=27): 630 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(229(a,1),57(a,1,2,2)),demod(57(13)),flip(a)]. given #81 (A,wt=67): 227 (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(32(a,1),32(a,1,1,2,2)),demod(32(14),32(15),32(29),32(30),32(31),32(32))]. Demod_limit hit 100 times. given #82 (F,wt=23): 707 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(630(a,1),23(a,1)),demod(23(7)),flip(a)]. given #83 (F,wt=23): 770 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(17(a,1),707(a,1,1))]. given #84 (T,wt=15): 821 x + ((y * z) * z) = x + (y * (z * z)). [para(770(a,1),57(a,1,2,2)),demod(58(10)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 3.32 (+ 0.01) seconds. % Length of proof is 28. % Level of proof is 13. % Maximum clause weight is 48. % Given clauses 84. 10 x + 0 = x. [input]. 11 x + - x = 0. [input]. 12 (x + y) + z = x + (y + z). [input]. 13 x + y = y + x. [input]. 14 x * (y + z) = (x * y) + (x * z). [input]. 15 (x + y) * z = (x * z) + (y * z). [input]. 16 (x * x) * y = x * (x * y). [input]. 17 (x * y) * x = x * (y * x). [input]. 18 (B * A) * A != B * (A * A). [input]. 22 x + (- x + y) = 0 + y. [para(11(a,1),12(a,1,1)),flip(a)]. 23 0 + x = x. [para(13(a,1),10(a,1))]. 24 x + (y + z) = y + (x + z). [para(13(a,1),12(a,1,1)),demod(12(2))]. 25 x + (- x + y) = y. [back_demod(22),demod(23(5))]. 31 (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(15(a,1),16(a,1,1)),demod(14(2),14(5),12(7),15(8),16(2),15(8),15(8),16(8),13(9),24(10),15(14),14(16),15(14),15(19),12(22))]. 44 - - x = x. [para(11(a,1),25(a,1,2)),demod(10(2)),flip(a)]. 45 x + (y + - x) = y. [para(13(a,1),25(a,1,2))]. 54 - x + (y + x) = y. [para(44(a,1),45(a,1,2,2))]. 57 - x + (y + (x + z)) = y + z. [para(54(a,1),12(a,1,1)),demod(12(4)),flip(a)]. 58 - x + (y + (z + x)) = y + z. [para(12(a,1),54(a,1,2))]. 224 (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(31(a,1),57(a,1,2)),flip(a)]. 228 - x + (y + (z + (u + x))) = y + (z + u). [para(12(a,1),58(a,1,2,2))]. 229 (x * (x * y)) + (((x * z) * y) + ((z * x) * y)) = (x * (x * y)) + ((z * (x * y)) + (x * (z * y))). [back_demod(224),demod(228(23))]. 630 x + (((y * z) * u) + ((z * y) * u)) = x + ((z * (y * u)) + (y * (z * u))). [para(229(a,1),57(a,1,2,2)),demod(57(13)),flip(a)]. 707 ((x * y) * z) + ((y * x) * z) = (y * (x * z)) + (x * (y * z)). [para(630(a,1),23(a,1)),demod(23(7)),flip(a)]. 770 (x * (y * x)) + ((y * x) * x) = (y * (x * x)) + (x * (y * x)). [para(17(a,1),707(a,1,1))]. 821 x + ((y * z) * z) = x + (y * (z * z)). [para(770(a,1),57(a,1,2,2)),demod(58(10)),flip(a)]. 851 (x * y) * y = x * (y * y). [para(821(a,1),23(a,1)),demod(23(4)),flip(a)]. 852 $F. [resolve(851,a,18,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=84. Generated=12100. Kept=842. proofs=1. Usable=58. Sos=359. Demods=342. Denials=0. 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=706287. 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.90. User_CPU=3.32, System_CPU=0.01, Wall_clock=4. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 12983 exit (max_proofs) Mon Jun 19 16:39:37 2006