From 0db54aa974ded619a1644d8cd8daf9f9aa157898 Mon Sep 17 00:00:00 2001 From: Koen van der Heijden Date: Sat, 14 Jan 2017 20:06:41 +0100 Subject: 3a done. 3b partially --- logic/logic_a.in | 9 ++ logic/logic_a.out | 157 +++++++++++++++++++++++++++++++ logic/logic_b.in | 12 +++ logic/logic_b.out | 273 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 451 insertions(+) create mode 100644 logic/logic_a.in create mode 100644 logic/logic_a.out create mode 100644 logic/logic_b.in create mode 100644 logic/logic_b.out (limited to 'logic') diff --git a/logic/logic_a.in b/logic/logic_a.in new file mode 100644 index 0000000..625351d --- /dev/null +++ b/logic/logic_a.in @@ -0,0 +1,9 @@ +formulas(sos). + a(x,x)=x. + a(x,y)=a(y,x). + a(x,a(y,z))=a(a(x,y),z). +end_of_list. + +formulas(goals). + all p all q (a(p,a(q,a(p,a(q,a(p,a(q,p))))))=a(p,q)). +end_of_list. diff --git a/logic/logic_a.out b/logic/logic_a.out new file mode 100644 index 0000000..828d77f --- /dev/null +++ b/logic/logic_a.out @@ -0,0 +1,157 @@ +============================== Prover9 =============================== +Prover9 (64) version 2009-11A, November 2009. +Process 7784 was started by koen on vdheijden-arch, +Sat Jan 14 16:51:59 2017 +The command was "prover9 -f logic_a.in". +============================== end of head =========================== + +============================== INPUT ================================= + +% Reading from file logic_a.in + + +formulas(sos). +a(x,x) = x. +a(x,y) = a(y,x). +a(x,a(y,z)) = a(a(x,y),z). +end_of_list. + +formulas(goals). +(all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)). +end_of_list. + +============================== end of input ========================== + +============================== PROCESS NON-CLAUSAL FORMULAS ========== + +% Formulas that are not ordinary clauses: +1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # 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). +a(x,x) = x. [assumption]. +a(x,y) = a(y,x). [assumption]. +a(x,a(y,z)) = a(a(x,y),z). [assumption]. +a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2). [deny(1)]. +end_of_list. + +formulas(demodulators). +end_of_list. + +============================== PREDICATE ELIMINATION ================= + +No predicates eliminated. + +============================== end predicate elimination ============= + +Auto_denials: (no changes). + +Term ordering decisions: +Predicate symbol precedence: predicate_order([ = ]). +Function symbol precedence: function_order([ c1, c2, a ]). +After inverse_order: (no changes). +Unfolding symbols: (none). + +Auto_inference settings: + % set(paramodulation). % (positive equality literals) + +Auto_process settings: (no changes). + +kept: 2 a(x,x) = x. [assumption]. + +% Operation a is commutative; C redundancy checks enabled. +kept: 3 a(x,y) = a(y,x). [assumption]. + 4 a(x,a(y,z)) = a(a(x,y),z). [assumption]. +kept: 5 a(a(x,y),z) = a(x,a(y,z)). [copy(4),flip(a)]. + 6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2). [deny(1)]. +kept: 7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2). [copy(6),rewrite([3(8)])]. + +============================== end of process initial clauses ======== + +============================== CLAUSES FOR SEARCH ==================== + +% Clauses after input processing: + +formulas(usable). +end_of_list. + +formulas(sos). +2 a(x,x) = x. [assumption]. +3 a(x,y) = a(y,x). [assumption]. +5 a(a(x,y),z) = a(x,a(y,z)). [copy(4),flip(a)]. +7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2). [copy(6),rewrite([3(8)])]. +end_of_list. + +formulas(demodulators). +2 a(x,x) = x. [assumption]. +3 a(x,y) = a(y,x). [assumption]. + % (lex-dep) +5 a(a(x,y),z) = a(x,a(y,z)). [copy(4),flip(a)]. +end_of_list. + +============================== end of clauses for search ============= + +============================== SEARCH ================================ + +% Starting search at 0.02 seconds. + +given #1 (I,wt=5): 2 a(x,x) = x. [assumption]. + +given #2 (I,wt=7): 3 a(x,y) = a(y,x). [assumption]. + +given #3 (I,wt=11): 5 a(a(x,y),z) = a(x,a(y,z)). [copy(4),flip(a)]. + +% Operation a is associative-commutative; CAC redundancy checks enabled. + +============================== PROOF ================================= + +% Proof 1 at 0.02 (+ 0.00) seconds. +% Length of proof is 10. +% Level of proof is 3. +% Maximum clause weight is 17.000. +% Given clauses 3. + +1 (all p all q a(p,a(q,a(p,a(q,a(p,a(q,p)))))) = a(p,q)) # label(non_clause) # label(goal). [goal]. +2 a(x,x) = x. [assumption]. +3 a(x,y) = a(y,x). [assumption]. +4 a(x,a(y,z)) = a(a(x,y),z). [assumption]. +5 a(a(x,y),z) = a(x,a(y,z)). [copy(4),flip(a)]. +6 a(c1,a(c2,a(c1,a(c2,a(c1,a(c2,c1)))))) != a(c1,c2). [deny(1)]. +7 a(c1,a(c2,a(c1,a(c2,a(c1,a(c1,c2)))))) != a(c1,c2). [copy(6),rewrite([3(8)])]. +9 a(x,a(x,y)) = a(x,y). [para(2(a,1),5(a,1,1)),flip(a)]. +10 a(x,a(y,x)) = a(y,x). [para(2(a,1),5(a,2,2)),rewrite([3(2)])]. +13 $F. [back_rewrite(7),rewrite([9(9),10(8),9(7),10(6),9(5)]),xx(a)]. + +============================== end of proof ========================== + +============================== STATISTICS ============================ + +Given=3. Generated=27. Kept=9. proofs=1. +Usable=3. Sos=1. Demods=8. Limbo=4, Disabled=5. Hints=0. +Kept_by_rule=0, Deleted_by_rule=0. +Forward_subsumed=17. Back_subsumed=0. +Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. +New_demodulators=8 (3 lex), Back_demodulated=1. Back_unit_deleted=0. +Demod_attempts=222. Demod_rewrites=33. +Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. +Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. +Megabytes=0.05. +User_CPU=0.02, System_CPU=0.00, Wall_clock=0. + +============================== end of statistics ===================== + +============================== end of search ========================= + +THEOREM PROVED + +Exiting with 1 proof. + +Process 7784 exit (max_proofs) Sat Jan 14 16:51:59 2017 diff --git a/logic/logic_b.in b/logic/logic_b.in new file mode 100644 index 0000000..6e087e7 --- /dev/null +++ b/logic/logic_b.in @@ -0,0 +1,12 @@ +formulas(sos). + (x*(y*z)=(x*y)*z). + (x*I=x). + (x*inv(x)=I). +end_of_list. + +formulas(goals). + all x (I*x=x). + all x (inv(inv(x))=x). + all x (inv(x)*x=I). + all x all y (x*y=y*x). +end_of_list. diff --git a/logic/logic_b.out b/logic/logic_b.out new file mode 100644 index 0000000..da9e9b0 --- /dev/null +++ b/logic/logic_b.out @@ -0,0 +1,273 @@ +============================== Prover9 =============================== +Prover9 (64) version 2009-11A, November 2009. +Process 13543 was started by koen on vdheijden-arch, +Sat Jan 14 20:02:31 2017 +The command was "prover9 -f logic_b.in". +============================== end of head =========================== + +============================== INPUT ================================= + +% Reading from file logic_b.in + + +formulas(sos). +x * (y * z) = (x * y) * z. +x * I = x. +x * inv(x) = I. +end_of_list. + +formulas(goals). +(all x I * x = x). +(all x inv(inv(x)) = x). +(all x inv(x) * x = I). +(all x all y x * y = y * x). +end_of_list. + +============================== end of input ========================== + +============================== PROCESS NON-CLAUSAL FORMULAS ========== + +% Formulas that are not ordinary clauses: +1 (all x I * x = x) # label(non_clause) # label(goal). [goal]. +2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal). [goal]. +3 (all x inv(x) * x = I) # label(non_clause) # label(goal). [goal]. +4 (all x all y x * y = y * x) # 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 * (y * z) = (x * y) * z. [assumption]. +x * I = x. [assumption]. +x * inv(x) = I. [assumption]. +I * c1 != c1. [deny(1)]. +inv(inv(c2)) != c2. [deny(2)]. +inv(c3) * c3 != I. [deny(3)]. +c5 * c4 != c4 * c5. [deny(4)]. +end_of_list. + +formulas(demodulators). +end_of_list. + +============================== PREDICATE ELIMINATION ================= + +No predicates eliminated. + +============================== end predicate elimination ============= + +Auto_denials: + % assign(max_proofs, 4). % (Horn set with more than one neg. clause) + +WARNING, because some of the denials share constants, +some of the denials or their descendents may be subsumed, +preventing the target number of proofs from being found. +The shared constants are: I. + +Term ordering decisions: +Predicate symbol precedence: predicate_order([ = ]). +Function symbol precedence: function_order([ I, c1, c2, c3, c4, c5, *, inv ]). +After inverse_order: Function symbol precedence: function_order([ I, c1, c2, c3, c4, c5, *, inv ]). +Unfolding symbols: (none). + +Auto_inference settings: + % set(paramodulation). % (positive equality literals) + +Auto_process settings: (no changes). + + 5 x * (y * z) = (x * y) * z. [assumption]. +kept: 6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +kept: 7 x * I = x. [assumption]. +kept: 8 x * inv(x) = I. [assumption]. +kept: 9 I * c1 != c1. [deny(1)]. +kept: 10 inv(inv(c2)) != c2. [deny(2)]. +kept: 11 inv(c3) * c3 != I. [deny(3)]. +kept: 12 c5 * c4 != c4 * c5. [deny(4)]. + +============================== end of process initial clauses ======== + +============================== CLAUSES FOR SEARCH ==================== + +% Clauses after input processing: + +formulas(usable). +end_of_list. + +formulas(sos). +6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +7 x * I = x. [assumption]. +8 x * inv(x) = I. [assumption]. +9 I * c1 != c1. [deny(1)]. +10 inv(inv(c2)) != c2. [deny(2)]. +11 inv(c3) * c3 != I. [deny(3)]. +12 c5 * c4 != c4 * c5. [deny(4)]. +end_of_list. + +formulas(demodulators). +6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +7 x * I = x. [assumption]. +8 x * inv(x) = I. [assumption]. +end_of_list. + +============================== end of clauses for search ============= + +============================== SEARCH ================================ + +% Starting search at 0.02 seconds. + +given #1 (I,wt=11): 6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. + +given #2 (I,wt=5): 7 x * I = x. [assumption]. + +given #3 (I,wt=6): 8 x * inv(x) = I. [assumption]. + +given #4 (I,wt=5): 9 I * c1 != c1. [deny(1)]. + +given #5 (I,wt=5): 10 inv(inv(c2)) != c2. [deny(2)]. + +given #6 (I,wt=6): 11 inv(c3) * c3 != I. [deny(3)]. + +given #7 (I,wt=7): 12 c5 * c4 != c4 * c5. [deny(4)]. + +given #8 (A,wt=9): 13 x * (I * y) = x * y. [para(7(a,1),6(a,1,1)),flip(a)]. + +given #9 (T,wt=6): 16 x * inv(I) = x. [para(8(a,1),13(a,1,2)),rewrite([7(2)]),flip(a)]. + +given #10 (T,wt=10): 14 x * (inv(x) * y) = I * y. [para(8(a,1),6(a,1,1)),flip(a)]. + +given #11 (T,wt=7): 19 I * inv(inv(x)) = x. [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)]. + +============================== PROOF ================================= + +% Proof 1 at 0.02 (+ 0.00) seconds. +% Length of proof is 12. +% Level of proof is 6. +% Maximum clause weight is 11.000. +% Given clauses 11. + +1 (all x I * x = x) # label(non_clause) # label(goal). [goal]. +5 x * (y * z) = (x * y) * z. [assumption]. +6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +7 x * I = x. [assumption]. +8 x * inv(x) = I. [assumption]. +9 I * c1 != c1. [deny(1)]. +13 x * (I * y) = x * y. [para(7(a,1),6(a,1,1)),flip(a)]. +14 x * (inv(x) * y) = I * y. [para(8(a,1),6(a,1,1)),flip(a)]. +19 I * inv(inv(x)) = x. [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)]. +21 x * inv(inv(y)) = x * y. [para(19(a,1),6(a,2,2)),rewrite([7(2)])]. +22 I * x = x. [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])]. +23 $F. [resolve(22,a,9,a)]. + +============================== end of proof ========================== +% Redundant proof: 27 $F. [back_rewrite(9),rewrite([22(3)]),xx(a)]. + +% Disable descendants (x means already disabled): + 9x + +given #12 (T,wt=5): 22 I * x = x. [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])]. + +given #13 (A,wt=10): 15 x * (y * inv(x * y)) = I. [para(8(a,1),6(a,1)),flip(a)]. + +given #14 (T,wt=4): 28 inv(I) = I. [para(22(a,1),8(a,1))]. + +given #15 (T,wt=8): 26 x * (inv(x) * y) = y. [back_rewrite(14),rewrite([22(5)])]. + +============================== PROOF ================================= + +% Proof 2 at 0.02 (+ 0.00) seconds. +% Length of proof is 14. +% Level of proof is 8. +% Maximum clause weight is 11.000. +% Given clauses 15. + +2 (all x inv(inv(x)) = x) # label(non_clause) # label(goal). [goal]. +5 x * (y * z) = (x * y) * z. [assumption]. +6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +7 x * I = x. [assumption]. +8 x * inv(x) = I. [assumption]. +10 inv(inv(c2)) != c2. [deny(2)]. +13 x * (I * y) = x * y. [para(7(a,1),6(a,1,1)),flip(a)]. +14 x * (inv(x) * y) = I * y. [para(8(a,1),6(a,1,1)),flip(a)]. +19 I * inv(inv(x)) = x. [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)]. +21 x * inv(inv(y)) = x * y. [para(19(a,1),6(a,2,2)),rewrite([7(2)])]. +22 I * x = x. [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])]. +26 x * (inv(x) * y) = y. [back_rewrite(14),rewrite([22(5)])]. +30 inv(inv(x)) = x. [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)]. +31 $F. [resolve(30,a,10,a)]. + +============================== end of proof ========================== +% Redundant proof: 33 $F. [back_rewrite(10),rewrite([30(3)]),xx(a)]. + +% Disable descendants (x means already disabled): + 10x + +given #16 (T,wt=5): 30 inv(inv(x)) = x. [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)]. + +============================== PROOF ================================= + +% Proof 3 at 0.02 (+ 0.00) seconds. +% Length of proof is 15. +% Level of proof is 9. +% Maximum clause weight is 11.000. +% Given clauses 16. + +3 (all x inv(x) * x = I) # label(non_clause) # label(goal). [goal]. +5 x * (y * z) = (x * y) * z. [assumption]. +6 (x * y) * z = x * (y * z). [copy(5),flip(a)]. +7 x * I = x. [assumption]. +8 x * inv(x) = I. [assumption]. +11 inv(c3) * c3 != I. [deny(3)]. +13 x * (I * y) = x * y. [para(7(a,1),6(a,1,1)),flip(a)]. +14 x * (inv(x) * y) = I * y. [para(8(a,1),6(a,1,1)),flip(a)]. +19 I * inv(inv(x)) = x. [para(8(a,1),14(a,1,2)),rewrite([7(2)]),flip(a)]. +21 x * inv(inv(y)) = x * y. [para(19(a,1),6(a,2,2)),rewrite([7(2)])]. +22 I * x = x. [para(19(a,1),13(a,2)),rewrite([21(5),13(4)])]. +26 x * (inv(x) * y) = y. [back_rewrite(14),rewrite([22(5)])]. +30 inv(inv(x)) = x. [para(8(a,1),26(a,1,2)),rewrite([7(2)]),flip(a)]. +34 inv(x) * x = I. [para(30(a,1),8(a,1,2))]. +35 $F. [resolve(34,a,11,a)]. + +============================== end of proof ========================== +% Redundant proof: 37 $F. [back_rewrite(11),rewrite([34(4)]),xx(a)]. + +% Disable descendants (x means already disabled): + 11x + +given #17 (T,wt=6): 34 inv(x) * x = I. [para(30(a,1),8(a,1,2))]. + +given #18 (A,wt=12): 25 x * (y * (inv(x * y) * z)) = z. [back_rewrite(18),rewrite([22(7)])]. + +given #19 (T,wt=8): 36 inv(x) * (x * y) = y. [para(30(a,1),26(a,1,2,1))]. + +given #20 (T,wt=9): 42 x * inv(y * x) = inv(y). [para(15(a,1),36(a,1,2)),rewrite([7(3)]),flip(a)]. + +given #21 (T,wt=10): 47 inv(x * y) = inv(y) * inv(x). [para(42(a,1),36(a,1,2)),flip(a)]. + +============================== STATISTICS ============================ + +Given=21. Generated=238. Kept=36. proofs=3. +Usable=11. Sos=0. Demods=10. Limbo=0, Disabled=32. Hints=0. +Kept_by_rule=0, Deleted_by_rule=0. +Forward_subsumed=199. Back_subsumed=0. +Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. +New_demodulators=32 (0 lex), Back_demodulated=25. Back_unit_deleted=0. +Demod_attempts=1855. Demod_rewrites=422. +Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. +Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. +Megabytes=0.09. +User_CPU=0.02, System_CPU=0.00, Wall_clock=0. + +============================== end of statistics ===================== + +============================== end of search ========================= + +SEARCH FAILED + +Exiting with 3 proofs. + +Process 13543 exit (sos_empty) Sat Jan 14 20:02:31 2017 -- cgit v1.2.1