============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13011 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:06 2006
The command was "/home/mccune/bin/prover9 -f cancel1.in".
============================== end of head ===========================

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

% Reading from file cancel1.in


clauses(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).
(all x all y all z (x * y = x * z -> y = z)).
end_of_list.

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

============================== PROCESS GOALS =========================

% Each goal formula was negated; the result (to be placed in sos):

clauses(negated_goals).
c1 * c3 = c1 * c2.
c3 != c2.
end_of_list.

============================== end of process goals ==================

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 (x * e) * x = x.  [input].
2 x * (x * y) = y.  [input].
3 (x * y) * (z * u) = (x * z) * (y * u).  [input].
4 ((x * x) * x) * x = e.  [input].
5 c1 * c3 = c1 * c2.  [clausify].
6 c3 != c2.  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:  no changes.

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ e, c1, c2, c3, * ]).
After inverse_order: Function symbol precedence:  lex([ e, c1, c2, c3, * ]).
Unfolding symbols: (none).

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

Auto_process settings:  no changes.

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
7 (x * e) * x = x.  [input].
8 x * (x * y) = y.  [input].
9 (x * y) * (z * u) = (x * z) * (y * u).  [input].
10 ((x * x) * x) * x = e.  [input].
11 c1 * c3 = c1 * c2.  [clausify].
12 c3 != c2.  [clausify].
end_of_list.

clauses(demodulators).
7 (x * e) * x = x.  [input].
8 x * (x * y) = y.  [input].
10 ((x * x) * x) * x = e.  [input].
11 c1 * c3 = c1 * c2.  [clausify].
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

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

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

given #5 (I,wt=7): 11 c1 * c3 = c1 * c2.  [clausify].

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

% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 5.
% Level of proof is 2.
% Maximum clause weight is 7.
% Given clauses 5.

8 x * (x * y) = y.  [input].
11 c1 * c3 = c1 * c2.  [clausify].
12 c3 != c2.  [clausify].
28 c3 = c2.  [para(11(a,1),8(a,1,2)),demod(8(5)),flip(a)].
29 $F.  [resolve(28,a,12,a)].

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

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

Given=5. Generated=54. Kept=22. proofs=1.
Usable=5. Sos=16. Demods=13. Denials=0. Limbo=0, Disabled=6. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=32. 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=406. Demod_rewrites=24.
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.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13011 exit (max_proofs) Mon Jun 19 16:40:06 2006