============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 3863 was started by mccune on cleo.thornwood,
Wed Nov 22 11:24:17 2006
The command was "/home/mccune/bin/prover9 -f cs.in DN.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).

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

% Reading from file DN.in


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

formulas(sos).
(A @ B) * C != C * (A @ B) # answer(N).
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 != x * z | y = z.  [assumption].
x * y != z * y | x = z.  [assumption].
(x * y) * z = x * y * z.  [assumption].
x * y * (y @ x) = y * x.  [assumption].
(x @ y) * (z @ y) = x * z @ y.  [assumption].
(A @ B) * C != C * (A @ B) # answer(N).  [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([ A, B, C, *, @ ]).
After inverse_order:  (no changes).
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:

formulas(usable).
end_of_list.

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

formulas(demodulators).
3 (x * y) * z = x * y * z.  [assumption].
4 x * y * (y @ x) = y * x.  [assumption].
6 x * y @ z = (x @ z) * (y @ z).  [copy(5),flip(a)].
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

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

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

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

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

given #7 (F,wt=15): 18 (A @ B) * C * x != C * (A @ B) * x # answer(N).  [ur(2,b,7,a),rewrite(3(6),3(12))].

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

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

given #10 (T,wt=10): 26 x * y != x | x @ x = y.  [para(10(a,1),1(a,1)),flip(a)].

given #11 (A,wt=14): 8 x * y * z != x * y * u | z = u.  [para(3(a,1),1(a,1)),rewrite(3(4))].

given #12 (F,wt=15): 32 C * (A @ B) * (C @ C) != (A @ B) * C # answer(N).  [para(10(a,1),18(a,1,2)),flip(a)].

given #13 (F,wt=17): 22 C * (A @ B) * (C @ (A @ B)) != C * (A @ B) # answer(N).  [para(4(a,1),18(a,1)),flip(a)].

given #14 (T,wt=10): 27 x * (y @ y) != y | y = x.  [para(10(a,1),2(a,1)),flip(a)].

given #15 (T,wt=10): 28 x * (y @ y) != y | x = y.  [para(10(a,1),2(a,2))].

given #16 (A,wt=14): 9 x * y * z != u * z | x * y = u.  [para(3(a,1),2(a,1))].

given #17 (F,wt=17): 24 (A @ B) * C * ((A @ B) @ C) != (A @ B) * C # answer(N).  [para(4(a,1),18(a,2))].

given #18 (F,wt=19): 20 x * (A @ B) * C * y != x * C * (A @ B) * y # answer(N).  [ur(1,b,18,a)].

given #19 (T,wt=11): 29 x * (x @ x) * y = x * y.  [para(10(a,1),3(a,1,1)),flip(a)].

given #20 (T,wt=7): 62 (x @ x) * y = y.  [hyper(8,a,29,a)].

given #21 (A,wt=14): 11 x * y != z * x | z * (z @ x) = y.  [para(4(a,1),1(a,1)),flip(a)].

given #22 (F,wt=19): 21 C * (A @ B) * x * (x @ C) != (A @ B) * x * C # answer(N).  [para(4(a,1),18(a,1,2)),flip(a)].

given #23 (F,wt=17): 84 C * (A @ B) * ((x @ x) @ C) != (A @ B) * C # answer(N).  [para(62(a,1),21(a,1,2,2)),rewrite(62(15))].

given #24 (T,wt=6): 81 x != y | y = x.  [para(10(a,1),11(a,2)),rewrite(62(2),70(4),10(3))].

given #25 (T,wt=9): 69 x * ((y @ y) @ x) = x.  [para(62(a,1),4(a,1,2)),rewrite(62(5))].

given #26 (A,wt=14): 12 x * y * (y @ z) != y * z | z = x.  [para(4(a,1),2(a,1)),flip(a)].

given #27 (F,wt=19): 25 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N).  [ur(1,b,19,a)].

given #28 (F,wt=19): 33 (A @ B) * C * ((A @ B) @ (A @ B)) != C * (A @ B) # answer(N).  [para(10(a,1),18(a,2,2))].

given #29 (T,wt=9): 76 x * (x @ x * x) = x.  [hyper(11,a,3,a)].

given #30 (T,wt=9): 88 (x @ x) @ y = y @ y.  [hyper(26,a,69,a),flip(a)].

given #31 (A,wt=14): 13 x * y * (y @ z) != y * z | x = z.  [para(4(a,1),2(a,2))].

given #32 (F,wt=19): 44 x * C * (A @ B) * (C @ C) != x * (A @ B) * C # answer(N).  [ur(1,b,32,a)].

given #33 (F,wt=19): 95 (A @ B) * C * ((x @ x) @ (A @ B)) != C * (A @ B) # answer(N).  [para(69(a,1),18(a,2,2))].

given #34 (T,wt=9): 110 x @ x * x = x @ x.  [hyper(26,a,76,a),flip(a)].

given #35 (T,wt=9): 114 ((x @ x) @ y) * z = z.  [para(88(a,2),62(a,1,1))].

given #36 (A,wt=15): 14 x * y * (y @ x) * z = y * x * z.  [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)].

given #37 (F,wt=15): 158 B * A * C * (A @ B) != A * B * C # answer(N).  [para(14(a,1),25(a,1)),flip(a)].

given #38 (F,wt=19): 115 C * (A @ B) * (((x @ x) @ y) @ C) != (A @ B) * C # answer(N).  [para(88(a,2),84(a,1,2,2,1))].

given #39 (T,wt=10): 68 x * y != y | z @ z = x.  [para(62(a,1),2(a,1)),flip(a)].

NOTE: New constant: x @ x = c_0.  [new_symbol(168)].
NOTE: New Function symbol precedence:  lex([ A, B, C, c_0, *, @ ]).

given #40 (T,wt=5): 171 x @ x = c_0.  [new_symbol(168)].

given #41 (A,wt=17): 15 x * y * z * (z @ x * y) = z * x * y.  [para(4(a,1),3(a,1)),flip(a)].

given #42 (F,wt=19): 162 B * A * C * (A @ B) * x != A * B * C * x # answer(N).  [ur(9,b,158,a),rewrite(3(9),3(8),3(16),3(15))].

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

% Proof 1 at 0.02 (+ 0.00) seconds: N.
% Length of proof is 15.
% Level of proof is 5.
% Maximum clause weight is 19.
% Given clauses 42.

1 x * y != x * z | y = z.  [assumption].
2 x * y != z * y | x = z.  [assumption].
3 (x * y) * z = x * y * z.  [assumption].
4 x * y * (y @ x) = y * x.  [assumption].
5 (x @ y) * (z @ y) = x * z @ y.  [assumption].
6 x * y @ z = (x @ z) * (y @ z).  [copy(5),flip(a)].
7 (A @ B) * C != C * (A @ B) # answer(N).  [assumption].
9 x * y * z != u * z | x * y = u.  [para(3(a,1),2(a,1))].
14 x * y * (y @ x) * z = y * x * z.  [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)].
16 x * y * z * (y @ x) * (z @ x) = y * z * x.  [para(3(a,1),4(a,1,2)),rewrite(6(2),3(8))].
19 x * (A @ B) * C != x * C * (A @ B) # answer(N).  [ur(1,b,7,a)].
25 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N).  [ur(1,b,19,a)].
158 B * A * C * (A @ B) != A * B * C # answer(N).  [para(14(a,1),25(a,1)),flip(a)].
162 B * A * C * (A @ B) * x != A * B * C * x # answer(N).  [ur(9,b,158,a),rewrite(3(9),3(8),3(16),3(15))].
214 $F # answer(N).  [para(4(a,1),162(a,2,2)),rewrite(16(13)),xx(a)].

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

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

Given=42. Generated=982. Kept=212. proofs=1.
Usable=24. Sos=86. Demods=28. Limbo=4, Disabled=104. Hints=0.
Weight_deleted=158. Literals_deleted=0.
Forward_subsumed=611. Back_subsumed=6.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=61 (0 lex), Back_demodulated=92. Back_unit_deleted=0.
Demod_attempts=14818. Demod_rewrites=1447.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=1372. Nonunit_bsub_feature_tests=792.
Megabytes=0.22.
User_CPU=0.02, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3863 exit (max_proofs) Wed Nov 22 11:24:17 2006