============================== Prover9 =============================== Prover9 (32) version June-2006C, June 2006. Process 12985 was started by mccune on cleo.thornwood, Mon Jun 19 16:39:37 2006 The command was "/home/mccune/bin/prover9 -f na-ring-3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file na-ring-3.in assign(eq_defs,fold). 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). associator(x,y,z) = ((x * y) * z) + - (x * (y * z)). 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]. 10 associator(x,y,z) = ((x * y) * z) + - (x * (y * z)). [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, *, +, -, associator ]). After inverse_order: Function symbol precedence: lex([ 0, A, B, +, -, *, associator ]). Folding symbols: associator/3. After fold_eq: Function symbol precedence: lex([ 0, A, B, associator, +, -, * ]). 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). 11 x + 0 = x. [input]. 12 x + - x = 0. [input]. 13 (x + y) + z = x + (y + z). [input]. 14 x + y = y + x. [input]. 15 x * (y + z) = (x * y) + (x * z). [input]. 16 (x + y) * z = (x * z) + (y * z). [input]. 17 (x * x) * y = x * (x * y). [input]. 18 (x * y) * x = x * (y * x). [input]. 19 (B * A) * A != B * (A * A). [input]. 20 - (x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),demod(14(7)),flip(a)]. end_of_list. clauses(demodulators). 11 x + 0 = x. [input]. 12 x + - x = 0. [input]. 13 (x + y) + z = x + (y + z). [input]. 14 x + y = y + x. [input]. % (lex-dep) 15 x * (y + z) = (x * y) + (x * z). [input]. 16 (x + y) * z = (x * z) + (y * z). [input]. 17 (x * x) * y = x * (x * y). [input]. 18 (x * y) * x = x * (y * x). [input]. 20 - (x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),demod(14(7)),flip(a)]. 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): 11 x + 0 = x. [input]. given #2 (I,wt=6): 12 x + - x = 0. [input]. given #3 (I,wt=11): 13 (x + y) + z = x + (y + z). [input]. given #4 (I,wt=7): 14 x + y = y + x. [input]. given #5 (I,wt=13): 15 x * (y + z) = (x * y) + (x * z). [input]. given #6 (I,wt=13): 16 (x + y) * z = (x * z) + (y * z). [input]. given #7 (I,wt=11): 17 (x * x) * y = x * (x * y). [input]. given #8 (I,wt=11): 18 (x * y) * x = x * (y * x). [input]. given #9 (I,wt=11): 19 (B * A) * A != B * (A * A). [input]. given #10 (I,wt=17): 20 - (x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),demod(14(7)),flip(a)]. given #11 (A,wt=10): 23 x + (y + - (x + y)) = 0. [para(13(a,1),12(a,1))]. given #12 (F,wt=4): 51 - 0 = 0. [para(12(a,1),23(a,1,2,2,1)),demod(27(5))]. given #13 (F,wt=5): 25 0 + x = x. [para(14(a,1),11(a,1))]. given #14 (T,wt=6): 46 associator(x,x,y) = 0. [para(17(a,1),20(a,1,2)),demod(14(6),12(6)),flip(a)]. given #15 (T,wt=6): 50 associator(x,y,x) = 0. [para(18(a,1),20(a,1,2)),demod(14(6),12(6)),flip(a)]. given #16 (A,wt=11): 26 x + (y + z) = y + (x + z). [para(14(a,1),13(a,1,1)),demod(13(2))]. given #17 (F,wt=8): 27 x + (- x + y) = y. [back_demod(24),demod(25(5))]. given #18 (F,wt=16): 83 associator(B,A,A) + (B * (A * A)) != B * (A * A). [back_demod(19),demod(66(5))]. given #19 (T,wt=5): 63 - - x = x. [para(12(a,1),27(a,1,2)),demod(11(2)),flip(a)]. given #20 (T,wt=8): 59 x + (y + - x) = y. [para(12(a,1),26(a,1,2)),demod(11(2)),flip(a)]. given #21 (A,wt=11): 28 (x * y) + (x * 0) = x * y. [para(11(a,1),15(a,1,2)),flip(a)]. given #22 (F,wt=5): 93 x * 0 = 0. [para(28(a,1),23(a,1,2,2,1)),demod(59(7))]. given #23 (F,wt=8): 88 - x + (y + x) = y. [para(63(a,1),59(a,1,2,2))]. given #24 (T,wt=9): 67 x + - (- y + x) = y. [para(23(a,1),27(a,1,2)),demod(11(2)),flip(a)]. given #25 (T,wt=9): 103 x + - (x + y) = - y. [para(88(a,1),88(a,1,2)),demod(14(3))]. given #26 (A,wt=11): 30 (x * y) + (0 * y) = x * y. [para(11(a,1),16(a,1,1)),flip(a)]. given #27 (F,wt=10): 95 (x * y) + (x * - y) = 0. [back_demod(29),demod(93(6))]. given #28 (F,wt=9): 135 - (x * - y) = x * y. [para(95(a,1),88(a,1,2)),demod(14(5),25(5))]. given #29 (T,wt=9): 136 x * - y = - (x * y). [para(135(a,1),63(a,1,1)),flip(a)]. given #30 (T,wt=10): 121 - (x + y) = - y + - x. [para(88(a,1),103(a,1,2,1)),flip(a)]. given #31 (A,wt=12): 31 (x * y) + (- x * y) = 0 * y. [para(12(a,1),16(a,1,1)),flip(a)]. given #32 (F,wt=11): 58 (0 * x) + (y * x) = y * x. [para(25(a,1),16(a,1,1)),flip(a)]. given #33 (F,wt=5): 152 0 * x = 0. [para(58(a,1),88(a,1,2)),demod(14(4),12(4)),flip(a)]. given #34 (T,wt=6): 153 associator(x,0,y) = 0. [back_demod(146),demod(152(5),93(5),14(5),25(5),75(4),12(2),152(4))]. given #35 (T,wt=9): 155 - (- x * y) = x * y. [back_demod(144),demod(152(2),25(5))]. given #36 (A,wt=16): 66 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(20(a,1),27(a,1,2)),demod(14(4)),flip(a)]. given #37 (F,wt=6): 164 associator(x,y,0) = 0. [para(66(a,1),93(a,1)),demod(93(4),93(4),14(4),25(4))]. given #38 (F,wt=6): 167 associator(0,x,y) = 0. [para(152(a,1),66(a,1,1)),demod(152(2),152(6),14(5),25(5)),flip(a)]. given #39 (T,wt=9): 160 - x * y = - (x * y). [para(155(a,1),63(a,1,1)),flip(a)]. given #40 (T,wt=12): 68 x + (y + (- x + z)) = y + z. [para(27(a,1),26(a,1,2)),flip(a)]. given #41 (A,wt=20): 72 associator(x,x * y,z) + (x * associator(x,y,z)) = associator(x * x,y,z). [back_demod(45),demod(66(7),66(8),15(11),14(14),13(14),13(13),12(12),14(6),25(6))]. given #42 (F,wt=8): 178 associator(x * x,y,x) = 0. [para(50(a,1),72(a,1,1)),demod(50(2),93(3),11(3)),flip(a)]. given #43 (F,wt=9): 187 associator(x * x,y,- x) = 0. [para(136(a,1),178(a,1,1)),demod(160(2),63(3))]. given #44 (T,wt=12): 85 x + (y + (z + - x)) = y + z. [para(13(a,1),59(a,1,2))]. given #45 (T,wt=12): 96 - x + (y + (x + z)) = y + z. [para(88(a,1),13(a,1,1)),demod(13(4)),flip(a)]. given #46 (A,wt=16): 73 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_demod(43),demod(66(8),66(12),13(15),14(16),13(16),13(15),13(14),62(15))]. given #47 (F,wt=11): 200 associator(x + y,x,z) = associator(y,x,z). [para(46(a,1),73(a,1,1)),demod(25(3)),flip(a)]. given #48 (F,wt=7): 213 associator(- x,x,y) = 0. [para(12(a,1),200(a,1,1)),demod(167(2)),flip(a)]. given #49 (T,wt=7): 226 associator(x,- x,y) = 0. [para(63(a,1),213(a,1,1))]. given #50 (T,wt=8): 215 associator(x,y,y + x) = 0. [para(200(a,1),50(a,1))]. given #51 (A,wt=16): 75 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_demod(41),demod(66(8),66(12),13(15),14(16),13(16),13(15),13(14),62(15))]. given #52 (F,wt=8): 233 associator(x,y,x + y) = 0. [para(14(a,1),215(a,1,3))]. ============================== PROOF ================================= % Proof 1 at 0.03 (+ 0.00) seconds. % Length of proof is 39. % Level of proof is 11. % Maximum clause weight is 31. % Given clauses 52. 10 associator(x,y,z) = ((x * y) * z) + - (x * (y * z)). [input]. 11 x + 0 = x. [input]. 12 x + - x = 0. [input]. 13 (x + y) + z = x + (y + z). [input]. 14 x + y = y + x. [input]. 15 x * (y + z) = (x * y) + (x * z). [input]. 16 (x + y) * z = (x * z) + (y * z). [input]. 17 (x * x) * y = x * (x * y). [input]. 18 (x * y) * x = x * (y * x). [input]. 19 (B * A) * A != B * (A * A). [input]. 20 - (x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),demod(14(7)),flip(a)]. 23 x + (y + - (x + y)) = 0. [para(13(a,1),12(a,1))]. 24 x + (- x + y) = 0 + y. [para(12(a,1),13(a,1,1)),flip(a)]. 25 0 + x = x. [para(14(a,1),11(a,1))]. 26 x + (y + z) = y + (x + z). [para(14(a,1),13(a,1,1)),demod(13(2))]. 27 x + (- x + y) = y. [back_demod(24),demod(25(5))]. 41 - ((x * (y * z)) + (x * (u * z))) + (((x * y) * z) + ((x * u) * z)) = associator(x,y + u,z). [para(15(a,1),20(a,1,2,1)),demod(16(2),15(4),16(10))]. 43 - ((x * (y * z)) + (u * (y * z))) + (((x * y) * z) + ((u * y) * z)) = associator(x + u,y,z). [para(16(a,1),20(a,1,1,1)),demod(16(8),16(10))]. 46 associator(x,x,y) = 0. [para(17(a,1),20(a,1,2)),demod(14(6),12(6)),flip(a)]. 50 associator(x,y,x) = 0. [para(18(a,1),20(a,1,2)),demod(14(6),12(6)),flip(a)]. 58 (0 * x) + (y * x) = y * x. [para(25(a,1),16(a,1,1)),flip(a)]. 59 x + (y + - x) = y. [para(12(a,1),26(a,1,2)),demod(11(2)),flip(a)]. 62 x + (y + (z + - (x + z))) = y. [para(23(a,1),26(a,1,2)),demod(11(2)),flip(a)]. 63 - - x = x. [para(12(a,1),27(a,1,2)),demod(11(2)),flip(a)]. 66 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(20(a,1),27(a,1,2)),demod(14(4)),flip(a)]. 73 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_demod(43),demod(66(8),66(12),13(15),14(16),13(16),13(15),13(14),62(15))]. 75 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_demod(41),demod(66(8),66(12),13(15),14(16),13(16),13(15),13(14),62(15))]. 83 associator(B,A,A) + (B * (A * A)) != B * (A * A). [back_demod(19),demod(66(5))]. 88 - x + (y + x) = y. [para(63(a,1),59(a,1,2,2))]. 152 0 * x = 0. [para(58(a,1),88(a,1,2)),demod(14(4),12(4)),flip(a)]. 167 associator(0,x,y) = 0. [para(152(a,1),66(a,1,1)),demod(152(2),152(6),14(5),25(5)),flip(a)]. 200 associator(x + y,x,z) = associator(y,x,z). [para(46(a,1),73(a,1,1)),demod(25(3)),flip(a)]. 213 associator(- x,x,y) = 0. [para(12(a,1),200(a,1,1)),demod(167(2)),flip(a)]. 215 associator(x,y,y + x) = 0. [para(200(a,1),50(a,1))]. 226 associator(x,- x,y) = 0. [para(63(a,1),213(a,1,1))]. 233 associator(x,y,x + y) = 0. [para(14(a,1),215(a,1,3))]. 259 associator(x,- x + y,z) = associator(x,y,z). [para(226(a,1),75(a,1,1)),demod(25(3)),flip(a)]. 269 associator(x,y,y) = 0. [para(27(a,1),233(a,1,3)),demod(259(3))]. 281 $F. [back_demod(83),demod(269(4),25(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=1227. Kept=270. proofs=1. Usable=37. Sos=98. Demods=134. Denials=0. Limbo=12, Disabled=133. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=956. Back_subsumed=4. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=251 (2 lex), Back_demodulated=119. Back_unit_deleted=0. Demod_attempts=13680. Demod_rewrites=2844. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=0.31. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 12985 exit (max_proofs) Mon Jun 19 16:39:37 2006