============================== Prover9 =============================== Prover9 (32) version Aug-2007, Aug 2007. Process 15965 was started by mccune on cleo, Tue Aug 7 09:30:26 2007 The command was "/home/mccune/LADR/bin/prover9 -f na-ring-3.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file na-ring-3.in assign(max_seconds,30). 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(non_clause) # 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: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ 0, c1, c2, *, +, -, associator ]). After inverse_order: Function symbol precedence: function_order([ 0, c1, c2, +, -, *, associator ]). Folding symbols: associator/3. After fold_eq: Function symbol precedence: function_order([ 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 (T,wt=4): 43 -0 = 0. [para(3(a,1),15(a,1,2,2,1)),rewrite([19(5)])]. given #13 (T,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 (T,wt=8): 19 x + (-x + y) = y. [back_rewrite(16),rewrite([17(5)])]. given #18 (T,wt=5): 55 --x = x. [para(3(a,1),19(a,1,2)),rewrite([2(2)]),flip(a)]. given #19 (T,wt=8): 51 x + (y + -x) = y. [para(3(a,1),18(a,1,2)),rewrite([2(2)]),flip(a)]. given #20 (T,wt=8): 80 -x + (y + x) = y. [para(55(a,1),51(a,1,2,2))]. 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=16): 75 associator(c1,c2,c2) + (c1 * (c2 * c2)) != c1 * (c2 * c2) # answer(right). [back_rewrite(12),rewrite([58(5)])]. given #23 (T,wt=5): 93 x * 0 = 0. [para(20(a,1),15(a,1,2,2,1)),rewrite([51(7)])]. 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): 88 x + -(x + y) = -y. [para(80(a,1),80(a,1,2)),rewrite([5(3)])]. given #26 (T,wt=10): 95 (x * y) + (x * -y) = 0. [back_rewrite(21),rewrite([93(6)])]. given #27 (A,wt=11): 22 (x * y) + (0 * y) = x * y. [para(2(a,1),7(a,1,1)),flip(a)]. given #28 (T,wt=9): 120 -(x * -y) = x * y. [para(95(a,1),80(a,1,2)),rewrite([5(5),17(5)])]. given #29 (T,wt=9): 128 x * -y = -(x * y). [para(120(a,1),55(a,1,1)),flip(a)]. given #30 (T,wt=10): 113 -(x + y) = -y + -x. [para(80(a,1),88(a,1,2,1)),flip(a)]. given #31 (T,wt=11): 50 (0 * x) + (y * x) = y * x. [para(17(a,1),7(a,1,1)),flip(a)]. given #32 (A,wt=16): 57 (x * y) + ((-x * y) + (z * y)) = z * y. [para(19(a,1),7(a,1,1)),rewrite([7(5)]),flip(a)]. given #33 (T,wt=5): 136 0 * x = 0. [para(50(a,1),80(a,1,2)),rewrite([5(4),3(4)]),flip(a)]. given #34 (T,wt=9): 144 -(-x * y) = x * y. [para(57(a,1),80(a,1,2)),rewrite([113(5),5(8),19(8)])]. given #35 (T,wt=6): 148 associator(x,0,y) = 0. [back_rewrite(137),rewrite([146(7),128(8),3(9),5(5),17(5),73(4),3(2)])]. given #36 (T,wt=9): 146 -x * y = -(x * y). [para(144(a,1),55(a,1,1)),flip(a)]. given #37 (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 #38 (T,wt=6): 152 associator(x,y,0) = 0. [para(58(a,1),93(a,1)),rewrite([93(4),93(4),5(4),17(4)])]. given #39 (T,wt=6): 155 associator(0,x,y) = 0. [para(136(a,1),58(a,1,1)),rewrite([136(2),136(6),5(5),17(5)]),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 (T,wt=12): 77 x + (y + (z + -x)) = y + z. [para(4(a,1),51(a,1,2))]. given #42 (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 #43 (T,wt=12): 81 -x + (y + (x + z)) = y + z. [para(80(a,1),4(a,1,1)),rewrite([4(4)]),flip(a)]. given #44 (T,wt=12): 82 -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 (T,wt=11): 179 associator(x + y,x,z) = associator(y,x,z). [para(34(a,1),71(a,1,1)),rewrite([17(3)]),flip(a)]. given #47 (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 #48 (T,wt=7): 188 associator(-x,x,y) = 0. [para(3(a,1),179(a,1,1)),rewrite([155(2)]),flip(a)]. given #49 (T,wt=7): 211 associator(x,-x,y) = 0. [para(55(a,1),188(a,1,1))]. given #50 (T,wt=8): 190 associator(x,y,y + x) = 0. [para(179(a,1),40(a,1))]. given #51 (T,wt=8): 220 associator(x,y,x + y) = 0. [para(5(a,1),190(a,1,3))]. given #52 (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 #53 (T,wt=9): 230 associator(x,-x + y,y) = 0. [para(19(a,1),220(a,1,3))]. given #54 (T,wt=9): 231 associator(x,y + -x,y) = 0. [para(51(a,1),220(a,1,3))]. given #55 (T,wt=9): 232 associator(-x,y + x,y) = 0. [para(80(a,1),220(a,1,3))]. given #56 (T,wt=9): 272 associator(-x,x + y,y) = 0. [para(55(a,1),230(a,1,2,1))]. given #57 (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 #58 (T,wt=10): 226 associator(x,y,y + (y + x)) = 0. [para(190(a,1),179(a,1)),flip(a)]. given #59 (T,wt=10): 313 associator(x,y,y + (x + y)) = 0. [para(5(a,1),226(a,1,3,2))]. given #60 (T,wt=10): 326 associator(x,y,x + (y + y)) = 0. [para(18(a,1),313(a,1,3))]. given #61 (T,wt=11): 180 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 #62 (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 #63 (T,wt=8): 369 associator(x * x,y,x) = 0. [para(40(a,1),68(a,1,1)),rewrite([40(2),93(3),2(3)]),flip(a)]. given #64 (T,wt=9): 404 associator(x * x,y,-x) = 0. [para(128(a,1),369(a,1,1)),rewrite([146(2),55(3)])]. given #65 (T,wt=11): 181 associator(x + y,z,x) = associator(y,z,x). [para(40(a,1),71(a,1,1)),rewrite([17(3)]),flip(a)]. given #66 (T,wt=7): 415 associator(-x,y,x) = 0. [para(3(a,1),181(a,1,1)),rewrite([155(2)]),flip(a)]. given #67 (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 #68 (T,wt=7): 431 associator(x,y,-x) = 0. [para(55(a,1),415(a,1,1))]. given #69 (T,wt=8): 417 associator(x,y + x,y) = 0. [para(181(a,1),34(a,1))]. given #70 (T,wt=8): 499 associator(x,x + y,y) = 0. [para(5(a,1),417(a,1,2))]. given #71 (T,wt=9): 511 associator(x,y,-x + y) = 0. [para(19(a,1),499(a,1,2))]. given #72 (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 #73 (T,wt=9): 512 associator(x,y,y + -x) = 0. [para(51(a,1),499(a,1,2))]. given #74 (T,wt=9): 513 associator(-x,y,y + x) = 0. [para(80(a,1),499(a,1,2))]. given #75 (T,wt=9): 527 associator(-x,y,x + y) = 0. [para(55(a,1),511(a,1,3,1))]. given #76 (T,wt=10): 428 associator(x,-x + -y,y) = 0. [para(181(a,1),211(a,1)),rewrite([113(2)])]. given #77 (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.37 (+ 0.00) seconds: right. % Length of proof is 40. % Level of proof is 10. % Maximum clause weight is 31. % Given clauses 77. 1 (y * x) * x = y * (x * x) # label(right) # label(non_clause) # 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))]. 136 0 * x = 0. [para(50(a,1),80(a,1,2)),rewrite([5(4),3(4)]),flip(a)]. 155 associator(0,x,y) = 0. [para(136(a,1),58(a,1,1)),rewrite([136(2),136(6),5(5),17(5)]),flip(a)]. 179 associator(x + y,x,z) = associator(y,x,z). [para(34(a,1),71(a,1,1)),rewrite([17(3)]),flip(a)]. 188 associator(-x,x,y) = 0. [para(3(a,1),179(a,1,1)),rewrite([155(2)]),flip(a)]. 190 associator(x,y,y + x) = 0. [para(179(a,1),40(a,1))]. 211 associator(x,-x,y) = 0. [para(55(a,1),188(a,1,1))]. 220 associator(x,y,x + y) = 0. [para(5(a,1),190(a,1,3))]. 230 associator(x,-x + y,y) = 0. [para(19(a,1),220(a,1,3))]. 683 associator(x,y,y) = 0. [para(230(a,1),73(a,2)),rewrite([211(2),17(3)])]. 758 $F # answer(right). [back_rewrite(75),rewrite([683(4),17(7)]),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=77. Generated=2990. Kept=755. proofs=1. Usable=51. Sos=385. Demods=406. Limbo=75, Disabled=254. Hints=0. Weight_deleted=252. Literals_deleted=0. Forward_subsumed=1982. Back_subsumed=7. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=616 (2 lex), Back_demodulated=237. Back_unit_deleted=0. Demod_attempts=99072. Demod_rewrites=24625. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=1.27. User_CPU=0.37, System_CPU=0.00, Wall_clock=0. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 15965 exit (max_proofs) Tue Aug 7 09:30:26 2007