3a done. 3b partially

1 files changed, 273 insertions, 0 deletions

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