============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3284 was started by mccune on cleo.thornwood, Wed Nov 22 11:21:31 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). associator(x,y,z) = ((x * y) * z) + -(x * (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]. associator(x,y,z) = ((x * y) * z) + -(x * (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, *, +, -, associator ]). After inverse_order: Function symbol precedence: lex([ 0, c1, c2, +, -, *, associator ]). Folding symbols: associator/3. After fold_eq: Function symbol precedence: lex([ 0, c1, c2, 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). 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]. 9 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(8),rewrite(5(7)),flip(a)]. 10 (x * x) * y = x * (x * y) # label(left). [assumption]. 11 (x * y) * x = x * (y * x) # label(flexible). [assumption]. 12 (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]. 9 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(8),rewrite(5(7)),flip(a)]. 10 (x * x) * y = x * (x * y) # label(left). [assumption]. 11 (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=17): 9 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(8),rewrite(5(7)),flip(a)]. given #8 (I,wt=11): 10 (x * x) * y = x * (x * y) # label(left). [assumption]. given #9 (I,wt=11): 11 (x * y) * x = x * (y * x) # label(flexible). [assumption]. given #10 (I,wt=11): 12 (c1 * c2) * c2 != c1 * (c2 * c2) # label(right) # answer(right). [deny(1)]. given #11 (A,wt=10): 15 x + (y + -(x + y)) = 0. [para(4(a,1),3(a,1))]. given #12 (F,wt=4): 43 -0 = 0. [para(3(a,1),15(a,1,2,2,1)),rewrite(19(5))]. given #13 (F,wt=5): 17 0 + x = x. [para(5(a,1),2(a,1))]. given #14 (T,wt=6): 34 associator(x,x,y) = 0. [para(10(a,1),9(a,1,2)),rewrite(5(6),3(6)),flip(a)]. given #15 (T,wt=6): 40 associator(x,y,x) = 0. [para(11(a,1),9(a,1,2)),rewrite(5(6),3(6)),flip(a)]. given #16 (A,wt=11): 18 x + (y + z) = y + (x + z). [para(5(a,1),4(a,1,1)),rewrite(4(2))]. given #17 (F,wt=8): 19 x + (-x + y) = y. [back_rewrite(16),rewrite(17(5))]. given #18 (F,wt=16): 75 associator(c1,c2,c2) + (c1 * (c2 * c2)) != c1 * (c2 * c2) # answer(right). [back_rewrite(12),rewrite(58(5))]. given #19 (T,wt=5): 55 --x = x. [para(3(a,1),19(a,1,2)),rewrite(2(2)),flip(a)]. given #20 (T,wt=8): 51 x + (y + -x) = y. [para(3(a,1),18(a,1,2)),rewrite(2(2)),flip(a)]. given #21 (A,wt=11): 20 (x * y) + (x * 0) = x * y. [para(2(a,1),6(a,1,2)),flip(a)]. given #22 (F,wt=5): 85 x * 0 = 0. [para(20(a,1),15(a,1,2,2,1)),rewrite(51(7))]. given #23 (F,wt=8): 80 -x + (y + x) = y. [para(55(a,1),51(a,1,2,2))]. given #24 (T,wt=9): 59 x + -(-y + x) = y. [para(15(a,1),19(a,1,2)),rewrite(2(2)),flip(a)]. given #25 (T,wt=9): 95 x + -(x + y) = -y. [para(80(a,1),80(a,1,2)),rewrite(5(3))]. given #26 (A,wt=11): 22 (x * y) + (0 * y) = x * y. [para(2(a,1),7(a,1,1)),flip(a)]. given #27 (F,wt=10): 87 (x * y) + (x * -y) = 0. [back_rewrite(21),rewrite(85(6))]. given #28 (F,wt=9): 127 -(x * -y) = x * y. [para(87(a,1),80(a,1,2)),rewrite(5(5),17(5))]. given #29 (T,wt=9): 128 x * -y = -(x * y). [para(127(a,1),55(a,1,1)),flip(a)]. given #30 (T,wt=10): 113 -(x + y) = -y + -x. [para(80(a,1),95(a,1,2,1)),flip(a)]. given #31 (A,wt=12): 23 (x * y) + (-x * y) = 0 * y. [para(3(a,1),7(a,1,1)),flip(a)]. given #32 (F,wt=11): 50 (0 * x) + (y * x) = y * x. [para(17(a,1),7(a,1,1)),flip(a)]. given #33 (F,wt=5): 144 0 * x = 0. [para(50(a,1),80(a,1,2)),rewrite(5(4),3(4)),flip(a)]. given #34 (T,wt=6): 145 associator(x,0,y) = 0. [back_rewrite(138),rewrite(144(5),85(5),5(5),17(5),73(4),3(2),144(4))]. given #35 (T,wt=9): 147 -(-x * y) = x * y. [back_rewrite(136),rewrite(144(2),17(5))]. given #36 (A,wt=16): 58 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(9(a,1),19(a,1,2)),rewrite(5(4)),flip(a)]. given #37 (F,wt=6): 156 associator(x,y,0) = 0. [para(58(a,1),85(a,1)),rewrite(85(4),85(4),5(4),17(4))]. given #38 (F,wt=6): 159 associator(0,x,y) = 0. [para(144(a,1),58(a,1,1)),rewrite(144(2),144(6),5(5),17(5)),flip(a)]. given #39 (T,wt=9): 152 -x * y = -(x * y). [para(147(a,1),55(a,1,1)),flip(a)]. given #40 (T,wt=12): 60 x + (y + (-x + z)) = y + z. [para(19(a,1),18(a,1,2)),flip(a)]. given #41 (A,wt=46): 62 associator(x,y * x,x * y) + ((x * associator(y,x,x * y)) + (x * (y * (x * (x * y))))) = associator(x,y,x * (x * y)) + (x * (y * (x * (x * y)))). [back_rewrite(42),rewrite(58(4),58(6),6(10),58(16))]. given #42 (F,wt=12): 77 x + (y + (z + -x)) = y + z. [para(4(a,1),51(a,1,2))]. given #43 (F,wt=12): 88 -x + (y + (x + z)) = y + z. [para(80(a,1),4(a,1,1)),rewrite(4(4)),flip(a)]. given #44 (T,wt=12): 89 -x + (y + (z + x)) = y + z. [para(4(a,1),80(a,1,2))]. given #45 (T,wt=16): 71 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_rewrite(29),rewrite(58(8),58(12),4(15),5(16),4(16),4(15),4(14),54(15))]. given #46 (A,wt=37): 63 associator(x,x * y,x * x) + ((x * associator(x,y,x * x)) + (x * (x * (y * (x * x))))) = x * (x * (y * (x * x))). [back_rewrite(41),rewrite(58(4),58(6),6(10))]. given #47 (F,wt=11): 183 associator(x + y,x,z) = associator(y,x,z). [para(34(a,1),71(a,1,1)),rewrite(17(3)),flip(a)]. given #48 (F,wt=7): 201 associator(-x,x,y) = 0. [para(3(a,1),183(a,1,1)),rewrite(159(2)),flip(a)]. given #49 (T,wt=7): 215 associator(x,-x,y) = 0. [para(55(a,1),201(a,1,1))]. given #50 (T,wt=8): 203 associator(x,y,y + x) = 0. [para(183(a,1),40(a,1))]. given #51 (A,wt=57): 66 (x * (y * x)) + (associator(x,y,z) + (associator(z,y,x) + ((z * (y * x)) + ((x * (y * z)) + (z * (y * z)))))) = (x * (y * x)) + ((z * (y * x)) + ((x * (y * z)) + (z * (y * z)))). [back_rewrite(36),rewrite(58(4),58(8),4(13),18(14),4(13))]. given #52 (F,wt=8): 224 associator(x,y,x + y) = 0. [para(5(a,1),203(a,1,3))]. given #53 (F,wt=9): 262 associator(x,-x + y,y) = 0. [para(19(a,1),224(a,1,3))]. given #54 (T,wt=9): 263 associator(x,y + -x,y) = 0. [para(51(a,1),224(a,1,3))]. given #55 (T,wt=9): 264 associator(-x,y + x,y) = 0. [para(80(a,1),224(a,1,3))]. given #56 (A,wt=37): 67 associator(x,x * (x * x),y) + ((x * associator(x,x * x,y)) + (x * (x * (x * (x * y))))) = x * (x * (x * (x * y))). [back_rewrite(35),rewrite(58(4),58(6),10(7),6(10))]. given #57 (F,wt=9): 275 associator(-x,x + y,y) = 0. [para(55(a,1),262(a,1,2,1))]. given #58 (F,wt=10): 231 associator(x,y,y + (y + x)) = 0. [para(203(a,1),183(a,1)),flip(a)]. given #59 (T,wt=10): 316 associator(x,y,y + (x + y)) = 0. [para(5(a,1),231(a,1,3,2))]. given #60 (T,wt=10): 329 associator(x,y,x + (y + y)) = 0. [para(18(a,1),316(a,1,3))]. given #61 (A,wt=20): 68 associator(x,x * y,z) + (x * associator(x,y,z)) = associator(x * x,y,z). [back_rewrite(33),rewrite(58(7),58(8),6(11),5(14),4(14),4(13),3(12),5(6),17(6))]. given #62 (F,wt=8): 358 associator(x * x,y,x) = 0. [para(40(a,1),68(a,1,1)),rewrite(40(2),85(3),2(3)),flip(a)]. given #63 (F,wt=9): 391 associator(x * x,y,-x) = 0. [para(128(a,1),358(a,1,1)),rewrite(152(2),55(3))]. given #64 (T,wt=11): 184 associator(x + y,y,z) = associator(x,y,z). [para(34(a,1),71(a,1,2)),rewrite(5(3),17(3)),flip(a)]. given #65 (T,wt=11): 185 associator(x + y,z,x) = associator(y,z,x). [para(40(a,1),71(a,1,1)),rewrite(17(3)),flip(a)]. given #66 (A,wt=57): 69 (x * (x * y)) + ((z * (z * y)) + (associator(z,x,y) + (associator(x,z,y) + ((x * (z * y)) + (z * (x * y)))))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y)))). [back_rewrite(31),rewrite(58(6),58(10),18(13),4(12))]. given #67 (F,wt=7): 416 associator(-x,y,x) = 0. [para(3(a,1),185(a,1,1)),rewrite(159(2)),flip(a)]. given #68 (F,wt=7): 489 associator(x,y,-x) = 0. [para(55(a,1),416(a,1,1))]. given #69 (T,wt=8): 418 associator(x,y + x,y) = 0. [para(185(a,1),34(a,1))]. given #70 (T,wt=8): 500 associator(x,x + y,y) = 0. [para(5(a,1),418(a,1,2))]. given #71 (A,wt=57): 70 (x * (x * y)) + ((z * (z * y)) + (associator(x,z,y) + (associator(z,x,y) + ((z * (x * y)) + (x * (z * y)))))) = (x * (x * y)) + ((z * (x * y)) + ((x * (z * y)) + (z * (z * y)))). [back_rewrite(30),rewrite(58(6),58(10),18(13),4(12))]. given #72 (F,wt=9): 512 associator(x,y,-x + y) = 0. [para(19(a,1),500(a,1,2))]. given #73 (F,wt=9): 513 associator(x,y,y + -x) = 0. [para(51(a,1),500(a,1,2))]. given #74 (T,wt=9): 514 associator(-x,y,y + x) = 0. [para(80(a,1),500(a,1,2))]. given #75 (T,wt=9): 612 associator(-x,y,x + y) = 0. [para(55(a,1),512(a,1,3,1))]. given #76 (A,wt=16): 73 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_rewrite(27),rewrite(58(8),58(12),4(15),5(16),4(16),4(15),4(14),54(15))]. ============================== PROOF ================================= % Proof 1 at 0.38 (+ 0.00) seconds: right. % Length of proof is 40. % Level of proof is 10. % Maximum clause weight is 31. % Given clauses 76. 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 associator(x,y,z) = ((x * y) * z) + -(x * (y * z)). [assumption]. 9 -(x * (y * z)) + ((x * y) * z) = associator(x,y,z). [copy(8),rewrite(5(7)),flip(a)]. 10 (x * x) * y = x * (x * y) # label(left). [assumption]. 11 (x * y) * x = x * (y * x) # label(flexible). [assumption]. 12 (c1 * c2) * c2 != c1 * (c2 * c2) # label(right) # answer(right). [deny(1)]. 15 x + (y + -(x + y)) = 0. [para(4(a,1),3(a,1))]. 16 x + (-x + y) = 0 + y. [para(3(a,1),4(a,1,1)),flip(a)]. 17 0 + x = x. [para(5(a,1),2(a,1))]. 18 x + (y + z) = y + (x + z). [para(5(a,1),4(a,1,1)),rewrite(4(2))]. 19 x + (-x + y) = y. [back_rewrite(16),rewrite(17(5))]. 27 -((x * (y * z)) + (x * (u * z))) + (((x * y) * z) + ((x * u) * z)) = associator(x,y + u,z). [para(6(a,1),9(a,1,2,1)),rewrite(7(2),6(4),7(10))]. 29 -((x * (y * z)) + (u * (y * z))) + (((x * y) * z) + ((u * y) * z)) = associator(x + u,y,z). [para(7(a,1),9(a,1,1,1)),rewrite(7(8),7(10))]. 34 associator(x,x,y) = 0. [para(10(a,1),9(a,1,2)),rewrite(5(6),3(6)),flip(a)]. 40 associator(x,y,x) = 0. [para(11(a,1),9(a,1,2)),rewrite(5(6),3(6)),flip(a)]. 50 (0 * x) + (y * x) = y * x. [para(17(a,1),7(a,1,1)),flip(a)]. 51 x + (y + -x) = y. [para(3(a,1),18(a,1,2)),rewrite(2(2)),flip(a)]. 54 x + (y + (z + -(x + z))) = y. [para(15(a,1),18(a,1,2)),rewrite(2(2)),flip(a)]. 55 --x = x. [para(3(a,1),19(a,1,2)),rewrite(2(2)),flip(a)]. 58 (x * y) * z = associator(x,y,z) + (x * (y * z)). [para(9(a,1),19(a,1,2)),rewrite(5(4)),flip(a)]. 71 associator(x,y,z) + associator(u,y,z) = associator(x + u,y,z). [back_rewrite(29),rewrite(58(8),58(12),4(15),5(16),4(16),4(15),4(14),54(15))]. 73 associator(x,y,z) + associator(x,u,z) = associator(x,y + u,z). [back_rewrite(27),rewrite(58(8),58(12),4(15),5(16),4(16),4(15),4(14),54(15))]. 75 associator(c1,c2,c2) + (c1 * (c2 * c2)) != c1 * (c2 * c2) # answer(right). [back_rewrite(12),rewrite(58(5))]. 80 -x + (y + x) = y. [para(55(a,1),51(a,1,2,2))]. 144 0 * x = 0. [para(50(a,1),80(a,1,2)),rewrite(5(4),3(4)),flip(a)]. 159 associator(0,x,y) = 0. [para(144(a,1),58(a,1,1)),rewrite(144(2),144(6),5(5),17(5)),flip(a)]. 183 associator(x + y,x,z) = associator(y,x,z). [para(34(a,1),71(a,1,1)),rewrite(17(3)),flip(a)]. 201 associator(-x,x,y) = 0. [para(3(a,1),183(a,1,1)),rewrite(159(2)),flip(a)]. 203 associator(x,y,y + x) = 0. [para(183(a,1),40(a,1))]. 215 associator(x,-x,y) = 0. [para(55(a,1),201(a,1,1))]. 224 associator(x,y,x + y) = 0. [para(5(a,1),203(a,1,3))]. 262 associator(x,-x + y,y) = 0. [para(19(a,1),224(a,1,3))]. 674 associator(x,y,y) = 0. [para(262(a,1),73(a,2)),rewrite(215(2),17(3))]. 742 $F # answer(right). [back_rewrite(75),rewrite(674(4),17(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=76. Generated=2997. Kept=739. proofs=1. Usable=51. Sos=378. Demods=394. Limbo=68, Disabled=252. Hints=0. Weight_deleted=249. Literals_deleted=0. Forward_subsumed=2008. Back_subsumed=5. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=602 (2 lex), Back_demodulated=237. Back_unit_deleted=0. Demod_attempts=98061. Demod_rewrites=24172. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.25. User_CPU=0.38, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 3284 exit (max_proofs) Wed Nov 22 11:21:31 2006