diff options
Diffstat (limited to 'logic/logic_a.out')
| -rw-r--r-- | logic/logic_a.out | 157 |
1 files changed, 157 insertions, 0 deletions
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 |