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

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

% Reading from file gt.in

op(450,infix,@).
op(400,infix_right,*).
assign(eq_defs,fold).
assign(max_weight,25).

clauses(sos).
(x * y) * z = x * y * z.
e * x = x.
x ' * x = e.
x @ y = x ' * y ' * x * y.
end_of_list.

% Reading from file NA.in


clauses(sos).
(x @ y) * z = z * (x @ y).
end_of_list.

clauses(sos).
(A @ B) @ C != D @ (F @ G) # answer(A).
end_of_list.

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

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 (x * y) * z = x * y * z.  [input].
2 e * x = x.  [input].
3 x ' * x = e.  [input].
4 x @ y = x ' * y ' * x * y.  [input].
5 (x @ y) * z = z * (x @ y).  [input].
6 (A @ B) @ C != D @ (F @ G) # answer(A).  [input].
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, A, B, C, D, F, G, *, @, ' ]).
After inverse_order: Function symbol precedence:  lex([ e, A, B, C, D, F, G, *, ', @ ]).
Folding symbols: @/2.
After fold_eq: Function symbol precedence:  lex([ e, A, B, C, D, F, G, @, *, ' ]).

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 * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * z = z * (x @ y).  [input].
12 (A @ B) @ C != D @ (F @ G) # answer(A).  [input].
end_of_list.

clauses(demodulators).
7 (x * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * z = z * (x @ y).  [input].
        % (lex-dep)
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

given #3 (I,wt=6): 9 x ' * x = e.  [input].

given #4 (I,wt=13): 10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].

given #5 (I,wt=11): 11 (x @ y) * z = z * (x @ y).  [input].

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

% Proof 1 at 0.00 (+ 0.00) seconds: A.
% Length of proof is 12.
% Level of proof is 3.
% Maximum clause weight is 13.
% Given clauses 5.

4 x @ y = x ' * y ' * x * y.  [input].
7 (x * y) * z = x * y * z.  [input].
8 e * x = x.  [input].
9 x ' * x = e.  [input].
10 x ' * y ' * x * y = x @ y.  [copy(4),flip(a)].
11 (x @ y) * z = z * (x @ y).  [input].
12 (A @ B) @ C != D @ (F @ G) # answer(A).  [input].
13 x ' * x * y = y.  [para(9(a,1),7(a,1,1)),demod(8(2)),flip(a)].
22 (x @ y) * (x @ y) ' = e.  [para(11(a,2),9(a,1))].
23 (x @ y) @ z = e.  [para(11(a,1),10(a,1,2,2)),demod(13(6),11(4,R),22(4)),flip(a)].
24 x @ (y @ z) = e.  [para(11(a,2),10(a,1,2,2)),demod(13(6),9(2)),flip(a)].
25 $F # answer(A).  [back_demod(12),demod(23(5),24(6)),xx(a)].

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

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

Given=5. Generated=52. Kept=18. proofs=1.
Usable=5. Sos=10. Demods=13. Denials=0. Limbo=2, Disabled=7. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=33. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=13 (1 lex), Back_demodulated=1. Back_unit_deleted=0.
Demod_attempts=433. Demod_rewrites=55.
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 13130 exit (max_proofs) Mon Jun 19 16:41:41 2006