============================== Prover9 ===============================
Prover9 (32) version 22-May-2007, May 2007.
Process 27456 was started by mccune on cleo,
Tue May 22 14:46:01 2007
The command was "/home/mccune/bin/prover9 -f gt.in NA.in".
============================== end of head ===========================

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

% Reading from file gt.in

assign(max_seconds,30).
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:
Predicate symbol precedence:  predicate_order([ = ]).
Function symbol precedence:  function_order([ e, A, B, C, D, F, G, *, @, ' ]).
After inverse_order: Function symbol precedence:  function_order([ e, A, B, C, D, F, G, *, ', @ ]).
Folding symbols: @/2.
After fold_eq: Function symbol precedence:  function_order([ 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=45. Kept=18. proofs=1.
Usable=5. Sos=10. Demods=13. Limbo=2, Disabled=7. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=26. 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=418. Demod_rewrites=52.
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 27456 exit (max_proofs) Tue May 22 14:46:01 2007