============================== Prover9 ===============================
Prover9 (32) version 2009-11A, November 2009.
Process 4306 was started by mccune on cleo,
Tue Nov  3 09:37:44 2009
The command was "/home/mccune/LADR/bin/prover9 -f cancel1.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file cancel1.in

assign(max_seconds,30).

formulas(sos).
(x * e) * x = x.
x * (x * y) = y.
(x * y) * (z * u) = (x * z) * (y * u).
((x * x) * x) * x = e.
end_of_list.

formulas(goals).
x * y = x * z -> y = z.
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 x * y = x * z -> y = z # 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 * e) * x = x.  [assumption].
x * (x * y) = y.  [assumption].
(x * y) * (z * u) = (x * z) * (y * u).  [assumption].
((x * x) * x) * x = e.  [assumption].
c1 * c3 = c1 * c2.  [deny(1)].
c3 != 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([ e, c1, c2, c3, * ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)

Auto_process settings:  (no changes).

kept:      2 (x * e) * x = x.  [assumption].
kept:      3 x * (x * y) = y.  [assumption].
kept:      4 (x * y) * (z * u) = (x * z) * (y * u).  [assumption].
kept:      5 ((x * x) * x) * x = e.  [assumption].
kept:      6 c1 * c3 = c1 * c2.  [deny(1)].
kept:      7 c3 != c2.  [deny(1)].

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 (x * e) * x = x.  [assumption].
3 x * (x * y) = y.  [assumption].
4 (x * y) * (z * u) = (x * z) * (y * u).  [assumption].
5 ((x * x) * x) * x = e.  [assumption].
6 c1 * c3 = c1 * c2.  [deny(1)].
7 c3 != c2.  [deny(1)].
end_of_list.

formulas(demodulators).
2 (x * e) * x = x.  [assumption].
3 x * (x * y) = y.  [assumption].
5 ((x * x) * x) * x = e.  [assumption].
6 c1 * c3 = c1 * c2.  [deny(1)].
end_of_list.

============================== end of clauses for search =============

============================== SEARCH ================================

% Starting search at 0.01 seconds.

given #1 (I,wt=7): 2 (x * e) * x = x.  [assumption].

given #2 (I,wt=7): 3 x * (x * y) = y.  [assumption].

given #3 (I,wt=15): 4 (x * y) * (z * u) = (x * z) * (y * u).  [assumption].

given #4 (I,wt=9): 5 ((x * x) * x) * x = e.  [assumption].

given #5 (I,wt=7): 6 c1 * c3 = c1 * c2.  [deny(1)].

============================== PROOF =================================

% Proof 1 at 0.01 (+ 0.00) seconds.
% Length of proof is 6.
% Level of proof is 3.
% Maximum clause weight is 7.000.
% Given clauses 5.

1 x * y = x * z -> y = z # label(non_clause) # label(goal).  [goal].
3 x * (x * y) = y.  [assumption].
6 c1 * c3 = c1 * c2.  [deny(1)].
7 c3 != c2.  [deny(1)].
23 c3 = c2.  [para(6(a,1),3(a,1,2)),rewrite([3(5)]),flip(a)].
24 $F.  [resolve(23,a,7,a)].

============================== end of proof ==========================

============================== STATISTICS ============================

Given=5. Generated=50. Kept=22. proofs=1.
Usable=5. Sos=16. Demods=13. Limbo=0, Disabled=6. Hints=0.
Kept_by_rule=0, Deleted_by_rule=0.
Forward_subsumed=28. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=13 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=401. Demod_rewrites=20.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=0.04.
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.

============================== end of statistics =====================

============================== end of search =========================

THEOREM PROVED

Exiting with 1 proof.

Process 4306 exit (max_proofs) Tue Nov  3 09:37:44 2009