============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11365 was started by mccune on cleo.thornwood,
Sat Aug 12 21:00:03 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).

formulas(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


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

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

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

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

% Formulas that are not ordinary clauses:

============================== 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].
e * x = x.  [assumption].
x' * x = e.  [assumption].
x @ y = x' * y' * x * y.  [assumption].
(x @ y) * z = z * (x @ y).  [assumption].
(A @ B) @ C != D @ (F @ G) # answer(A).  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

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:

formulas(usable).
end_of_list.

formulas(sos).
1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
6 (x @ y) * z = z * (x @ y).  [assumption].
7 (A @ B) @ C != D @ (F @ G) # answer(A).  [assumption].
end_of_list.

formulas(demodulators).
1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
6 (x @ y) * z = z * (x @ y).  [assumption].
        % (lex-dep)
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

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

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

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

============================== 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.

1 (x * y) * z = x * y * z.  [assumption].
2 e * x = x.  [assumption].
3 x' * x = e.  [assumption].
4 x @ y = x' * y' * x * y.  [assumption].
5 x' * y' * x * y = x @ y.  [copy(4),flip(a)].
6 (x @ y) * z = z * (x @ y).  [assumption].
7 (A @ B) @ C != D @ (F @ G) # answer(A).  [assumption].
8 x' * x * y = y.  [para(3(a,1),1(a,1,1)),rewrite(2(2)),flip(a)].
17 (x @ y) * (x @ y)' = e.  [para(6(a,2),3(a,1))].
18 (x @ y) @ z = e.  [para(6(a,1),5(a,1,2,2)),rewrite(8(6),6(4,R),17(4)),flip(a)].
19 x @ (y @ z) = e.  [para(6(a,2),5(a,1,2,2)),rewrite(8(6),3(2)),flip(a)].
20 $F # answer(A).  [back_rewrite(7),rewrite(18(5),19(6)),xx(a)].

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

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

Given=5. Generated=52. Kept=18. proofs=1.
Usable=5. Sos=10. Demods=13. 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=463. 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 11365 exit (max_proofs) Sat Aug 12 21:00:03 2006