============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10607 was started by mccune on cleo.thornwood, Sat Aug 12 20:57:15 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). 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). associator(x,y,z) = ((x * y) * z) + -(x * (y * z)). 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]. associator(x,y,z) = ((x * y) * z) + -(x * (y * z)). [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, *, +, -, 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 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]. 11 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),rewrite(4(7)),flip(a)]. 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]. 11 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),rewrite(4(7)),flip(a)]. 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 (I,wt=17): 11 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),rewrite(4(7)),flip(a)]. given #11 (A,wt=10): 14 x + (y + -(x + y)) = 0. [para(3(a,1),2(a,1))]. given #12 (F,wt=4): 42 -0 = 0. [para(2(a,1),14(a,1,2,2,1)),rewrite(18(5))]. given #13 (F,wt=5): 16 0 + x = x. [para(4(a,1),1(a,1))]. given #14 (T,wt=6): 37 associator(x,x,y) = 0. [para(7(a,1),11(a,1,2)),rewrite(4(6),2(6)),flip(a)]. given #15 (T,wt=6): 41 associator(x,y,x) = 0. [para(8(a,1),11(a,1,2)),rewrite(4(6),2(6)),flip(a)]. given #16 (A,wt=11): 17 x + (y + z) = y + (x + z). [para(4(a,1),3(a,1,1)),rewrite(3(2))]. given #17 (F,wt=8): 18 x + (-x + y) = y. [back_rewrite(15),rewrite(16(5))]. given #18 (F,wt=16): 74 associator(B,A,A) + (B * (A * A)) != B * (A * A). [back_rewrite(9),rewrite(57(5))]. given #19 (T,wt=5): 54 --x = x. [para(2(a,1),18(a,1,2)),rewrite(1(2)),flip(a)]. given #20 (T,wt=8): 50 x + (y + -x) = y. [para(2(a,1),17(a,1,2)),rewrite(1(2)),flip(a)]. given #21 (A,wt=11): 19 (x * y) + (x * 0) = x * y. [para(1(a,1),5(a,1,2)),flip(a)]. given #22 (F,wt=5): 84 x * 0 = 0. [para(19(a,1),14(a,1,2,2,1)),rewrite(50(7))]. given #23 (F,wt=8): 79 -x + (y + x) = y. [para(54(a,1),50(a,1,2,2))]. given #24 (T,wt=9): 58 x + -(-y + x) = y. [para(14(a,1),18(a,1,2)),rewrite(1(2)),flip(a)]. given #25 (T,wt=9): 94 x + -(x + y) = -y. [para(79(a,1),79(a,1,2)),rewrite(4(3))]. given #26 (A,wt=11): 21 (x * y) + (0 * y) = x * y. [para(1(a,1),6(a,1,1)),flip(a)]. given #27 (F,wt=10): 86 (x * y) + (x * -y) = 0. [back_rewrite(20),rewrite(84(6))]. given #28 (F,wt=9): 126 -(x * -y) = x * y. [para(86(a,1),79(a,1,2)),rewrite(4(5),16(5))]. given #29 (T,wt=9): 127 x * -y = -(x * y). [para(126(a,1),54(a,1,1)),flip(a)]. given #30 (T,wt=10): 112 -(x + y) = -y + -x. [para(79(a,1),94(a,1,2,1)),flip(a)]. given #31 (A,wt=12): 22 (x * y) + (-x * y) = 0 * y. [para(2(a,1),6(a,1,1)),flip(a)]. given #32 (F,wt=11): 49 (0 * x) + (y * x) = y * x. [para(16(a,1),6(a,1,1)),flip(a)]. given #33 (F,wt=5): 143 0 * x = 0. [para(49(a,1),79(a,1,2)),rewrite(4(4),2(4)),flip(a)]. given #34 (T,wt=6): 144 associator(x,0,y) = 0. [back_rewrite(137),rewrite(143(5),84(5),4(5),16(5),66(4),2(2),143(4))]. given #35 (T,wt=9): 146 -(-x * y) = x * y. [back_rewrite(135),rewrite(143(2),16(5))]. given #36 (A,wt=16): 57 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(11(a,1),18(a,1,2)),rewrite(4(4)),flip(a)]. given #37 (F,wt=6): 155 associator(x,y,0) = 0. [para(57(a,1),84(a,1)),rewrite(84(4),84(4),4(4),16(4))]. given #38 (F,wt=6): 158 associator(0,x,y) = 0. [para(143(a,1),57(a,1,1)),rewrite(143(2),143(6),4(5),16(5)),flip(a)]. given #39 (T,wt=9): 151 -x * y = -(x * y). [para(146(a,1),54(a,1,1)),flip(a)]. given #40 (T,wt=12): 59 x + (y + (-x + z)) = y + z. [para(18(a,1),17(a,1,2)),flip(a)]. given #41 (A,wt=20): 63 associator(x,x * y,z) + (x * associator(x,y,z)) = associator(x * x,y,z). [back_rewrite(36),rewrite(57(7),57(8),5(11),4(14),3(14),3(13),2(12),4(6),16(6))]. given #42 (F,wt=8): 169 associator(x * x,y,x) = 0. [para(41(a,1),63(a,1,1)),rewrite(41(2),84(3),1(3)),flip(a)]. given #43 (F,wt=9): 178 associator(x * x,y,-x) = 0. [para(127(a,1),169(a,1,1)),rewrite(151(2),54(3))]. given #44 (T,wt=12): 76 x + (y + (z + -x)) = y + z. [para(3(a,1),50(a,1,2))]. given #45 (T,wt=12): 87 -x + (y + (x + z)) = y + z. [para(79(a,1),3(a,1,1)),rewrite(3(4)),flip(a)]. given #46 (A,wt=16): 64 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_rewrite(34),rewrite(57(8),57(12),3(15),4(16),3(16),3(15),3(14),53(15))]. given #47 (F,wt=11): 191 associator(x + y,x,z) = associator(y,x,z). [para(37(a,1),64(a,1,1)),rewrite(16(3)),flip(a)]. given #48 (F,wt=7): 204 associator(-x,x,y) = 0. [para(2(a,1),191(a,1,1)),rewrite(158(2)),flip(a)]. given #49 (T,wt=7): 217 associator(x,-x,y) = 0. [para(54(a,1),204(a,1,1))]. given #50 (T,wt=8): 206 associator(x,y,y + x) = 0. [para(191(a,1),41(a,1))]. given #51 (A,wt=16): 66 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_rewrite(32),rewrite(57(8),57(12),3(15),4(16),3(16),3(15),3(14),53(15))]. given #52 (F,wt=8): 224 associator(x,y,x + y) = 0. [para(4(a,1),206(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. 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]. 10 associator(x,y,z) = ((x * y) * z) + -(x * (y * z)). [assumption]. 11 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(10),rewrite(4(7)),flip(a)]. 14 x + (y + -(x + y)) = 0. [para(3(a,1),2(a,1))]. 15 x + (-x + y) = 0 + y. [para(2(a,1),3(a,1,1)),flip(a)]. 16 0 + x = x. [para(4(a,1),1(a,1))]. 17 x + (y + z) = y + (x + z). [para(4(a,1),3(a,1,1)),rewrite(3(2))]. 18 x + (-x + y) = y. [back_rewrite(15),rewrite(16(5))]. 32 -((x * (y * z)) + (x * (u * z))) + (((x * y) * z) + ((x * u) * z)) = associator(x,y + u,z). [para(5(a,1),11(a,1,2,1)),rewrite(6(2),5(4),6(10))]. 34 -((x * (y * z)) + (u * (y * z))) + (((x * y) * z) + ((u * y) * z)) = associator(x + u,y,z). [para(6(a,1),11(a,1,1,1)),rewrite(6(8),6(10))]. 37 associator(x,x,y) = 0. [para(7(a,1),11(a,1,2)),rewrite(4(6),2(6)),flip(a)]. 41 associator(x,y,x) = 0. [para(8(a,1),11(a,1,2)),rewrite(4(6),2(6)),flip(a)]. 49 (0 * x) + (y * x) = y * x. [para(16(a,1),6(a,1,1)),flip(a)]. 50 x + (y + -x) = y. [para(2(a,1),17(a,1,2)),rewrite(1(2)),flip(a)]. 53 x + (y + (z + -(x + z))) = y. [para(14(a,1),17(a,1,2)),rewrite(1(2)),flip(a)]. 54 --x = x. [para(2(a,1),18(a,1,2)),rewrite(1(2)),flip(a)]. 57 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(11(a,1),18(a,1,2)),rewrite(4(4)),flip(a)]. 64 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_rewrite(34),rewrite(57(8),57(12),3(15),4(16),3(16),3(15),3(14),53(15))]. 66 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_rewrite(32),rewrite(57(8),57(12),3(15),4(16),3(16),3(15),3(14),53(15))]. 74 associator(B,A,A) + (B * (A * A)) != B * (A * A). [back_rewrite(9),rewrite(57(5))]. 79 -x + (y + x) = y. [para(54(a,1),50(a,1,2,2))]. 143 0 * x = 0. [para(49(a,1),79(a,1,2)),rewrite(4(4),2(4)),flip(a)]. 158 associator(0,x,y) = 0. [para(143(a,1),57(a,1,1)),rewrite(143(2),143(6),4(5),16(5)),flip(a)]. 191 associator(x + y,x,z) = associator(y,x,z). [para(37(a,1),64(a,1,1)),rewrite(16(3)),flip(a)]. 204 associator(-x,x,y) = 0. [para(2(a,1),191(a,1,1)),rewrite(158(2)),flip(a)]. 206 associator(x,y,y + x) = 0. [para(191(a,1),41(a,1))]. 217 associator(x,-x,y) = 0. [para(54(a,1),204(a,1,1))]. 224 associator(x,y,x + y) = 0. [para(4(a,1),206(a,1,3))]. 250 associator(x,-x + y,z) = associator(x,y,z). [para(217(a,1),66(a,1,1)),rewrite(16(3)),flip(a)]. 260 associator(x,y,y) = 0. [para(18(a,1),224(a,1,3)),rewrite(250(3))]. 272 $F. [back_rewrite(74),rewrite(260(4),16(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=52. Generated=1227. Kept=270. proofs=1. Usable=37. Sos=98. Demods=134. 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=13733. 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.30. User_CPU=0.03, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 10607 exit (max_proofs) Sat Aug 12 20:57:15 2006