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

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

% Reading from file cs.in

op(450,infix,@).
op(400,infix_right,*).
assign(new_constants,1).
assign(max_weight,25).

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

% Reading from file AN.in


clauses(sos).
(x @ y) @ z = u @ (v @ w).
end_of_list.

clauses(sos).
(A @ B) * C != C * (A @ B) # answer(N).
end_of_list.

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

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 x * y != x * z | y = z.  [input].
2 x * y != z * y | x = z.  [input].
3 (x * y) * z = x * y * z.  [input].
4 x * y * (y @ x) = y * x.  [input].
5 (x @ y) @ z = u @ (v @ w).  [input].
6 (A @ B) * C != C * (A @ B) # answer(N).  [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([ A, B, C, *, @ ]).
After inverse_order: Function symbol precedence:  lex([ A, B, C, *, @ ]).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 2).  % (nonunit Horn with equality)

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 != x * z | y = z.  [input].
8 x * y != z * y | x = z.  [input].
9 (x * y) * z = x * y * z.  [input].
10 x * y * (y @ x) = y * x.  [input].
11 (x @ y) @ z = u @ (v @ w).  [input].
12 (A @ B) * C != C * (A @ B) # answer(N).  [input].
end_of_list.

clauses(demodulators).
9 (x * y) * z = x * y * z.  [input].
10 x * y * (y @ x) = y * x.  [input].
end_of_list.

clauses(denials).
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

given #2 (I,wt=10): 8 x * y != z * y | x = z.  [input].

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

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

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

given #6 (I,wt=11): 12 (A @ B) * C != C * (A @ B) # answer(N).  [input].

given #7 (F,wt=15): 26 (A @ B) * C * x != C * (A @ B) * x # answer(N).  [ur(8,b,12,a),demod(9(6),9(12))].

given #8 (F,wt=15): 27 x * (A @ B) * C != x * C * (A @ B) # answer(N).  [ur(7,b,12,a)].

given #9 (T,wt=7): 15 x * (x @ x) = x.  [hyper(7,a,10,a)].

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

% Proof 1 at 0.00 (+ 0.00) seconds: N.
% Length of proof is 11.
% Level of proof is 3.
% Maximum clause weight is 19.
% Given clauses 9.

7 x * y != x * z | y = z.  [input].
8 x * y != z * y | x = z.  [input].
9 (x * y) * z = x * y * z.  [input].
10 x * y * (y @ x) = y * x.  [input].
11 (x @ y) @ z = u @ (v @ w).  [input].
12 (A @ B) * C != C * (A @ B) # answer(N).  [input].
15 x * (x @ x) = x.  [hyper(7,a,10,a)].
23 (x @ y) * z * ((u @ v) @ w) = z * (x @ y).  [para(11(a,2),10(a,1,2,2))].
26 (A @ B) * C * x != C * (A @ B) * x # answer(N).  [ur(8,b,12,a),demod(9(6),9(12))].
42 (A @ B) * C * ((A @ B) @ (A @ B)) != C * (A @ B) # answer(N).  [para(15(a,1),26(a,2,2))].
43 $F # answer(N).  [resolve(42,a,23,a)].

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

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

Given=9. Generated=83. Kept=36. proofs=1.
Usable=9. Sos=18. Demods=10. Denials=0. Limbo=8, Disabled=6. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=47. Back_subsumed=0.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=10 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
Demod_attempts=753. Demod_rewrites=58.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=23. Nonunit_bsub_feature_tests=12.
Megabytes=0.06.
User_CPU=0.00, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13116 exit (max_proofs) Mon Jun 19 16:41:29 2006