============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13133 was started by mccune on cleo.thornwood,
Mon Jun 19 16:41:41 2006
The command was "/home/mccune/bin/prover9 -f cs.in ND.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 ND.in


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

clauses(sos).
(A @ C) * (B @ C) != A * B @ C # answer(D).
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 = z * (x @ y).  [input].
6 (A @ C) * (B @ C) != A * B @ C # answer(D).  [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 = z * (x @ y).  [input].
12 A * B @ C != (A @ C) * (B @ C) # answer(D).  [copy(6),flip(a)].
end_of_list.

clauses(demodulators).
9 (x * y) * z = x * y * z.  [input].
10 x * y * (y @ x) = y * x.  [input].
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=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 = z * (x @ y).  [input].

given #6 (I,wt=13): 12 A * B @ C != (A @ C) * (B @ C) # answer(D).  [copy(6),flip(a)].

given #7 (F,wt=17): 29 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D).  [ur(8,b,12,a),demod(9(14))].

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

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

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

given #11 (A,wt=14): 13 x * y * z != x * y * u | z = u.  [para(9(a,1),7(a,1)),demod(9(4))].

given #12 (F,wt=17): 35 (A @ C) * (B @ C) * x != x * (A * B @ C) # answer(D).  [para(11(a,1),29(a,1)),flip(a)].

given #13 (F,wt=17): 36 (A * B @ C) * x != (A @ C) * x * (B @ C) # answer(D).  [para(11(a,1),29(a,2,2))].

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

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

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

given #17 (F,wt=17): 39 (A * B @ C) * x != x * (A @ C) * (B @ C) # answer(D).  [para(11(a,2),30(a,1))].

given #18 (F,wt=17): 67 (A @ C) * x * (B @ C) != x * (A * B @ C) # answer(D).  [para(11(a,1),35(a,1,2))].

given #19 (T,wt=10): 74 (x @ x) * y != x | x = y.  [para(11(a,2),41(a,1))].

given #20 (T,wt=10): 75 (x @ x) * y != x | y = x.  [para(11(a,2),42(a,1))].

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

given #22 (F,wt=19): 103 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D).  [ur(16,b,30,a),demod(9(12),9(18))].

given #23 (F,wt=19): 104 C * (A @ C) * A * B * (B @ C) != A * B * C # answer(D).  [ur(16,b,67,a(flip)),demod(9(11),9(18))].

given #24 (T,wt=9): 98 x * (x @ (y @ z)) = x.  [hyper(16,a,11,a)].

given #25 (T,wt=9): 99 x * (x @ x * x) = x.  [hyper(16,a,9,a)].

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

given #27 (F,wt=21): 31 x * (A * B @ C) * y != x * (A @ C) * (B @ C) * y # answer(D).  [ur(7,b,29,a)].

given #28 (F,wt=21): 37 x * y * (A * B @ C) != x * y * (A @ C) * (B @ C) # answer(D).  [ur(7,b,30,a)].

given #29 (T,wt=9): 116 x @ (y @ z) = x @ x.  [hyper(40,a,98,a),flip(a)].

given #30 (T,wt=9): 130 x @ x * x = x @ x.  [hyper(40,a,99,a),flip(a)].

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

given #32 (F,wt=21): 63 (A @ C) * (B @ C) * x * y != x * (A * B @ C) * y # answer(D).  [ur(8,b,35,a),demod(9(9),9(8),9(16))].

given #33 (F,wt=21): 64 x * (A @ C) * (B @ C) * y != x * y * (A * B @ C) # answer(D).  [ur(7,b,35,a)].

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

given #35 (T,wt=10): 136 x * y != y | y @ y = x.  [para(15(a,1),17(a,2)),demod(98(3))].

given #36 (A,wt=15): 19 x * y * (y @ x) * z = y * x * z.  [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)].

given #37 (F,wt=17): 190 C * A * (A * B @ C) != A * C * (B @ C) # answer(D).  [para(19(a,1),37(a,2))].

given #38 (F,wt=21): 65 (A @ C) * (B @ C) * x * y != x * y * (A * B @ C) # answer(D).  [para(9(a,1),35(a,2))].

given #39 (T,wt=6): 196 x != y | y = x.  [back_demod(74),demod(168(2))].

given #40 (T,wt=7): 168 (x @ x) * y = y.  [hyper(13,a,19,a)].

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

given #41 (A,wt=17): 20 x * y * z * (z @ x * y) = z * x * y.  [para(10(a,1),9(a,1)),flip(a)].

given #42 (F,wt=17): 220 (B @ C) * (A @ C) * x != x * (A * B @ C) # answer(D).  [back_demod(203),demod(214(14)),flip(a)].

given #43 (F,wt=17): 221 (A * B @ C) * x != (B @ C) * (A @ C) * x # answer(D).  [back_demod(191),demod(214(14))].

given #44 (T,wt=5): 217 x @ x = c_0.  [new_symbol(204)].

given #45 (T,wt=5): 219 x * c_0 = x.  [back_demod(146),demod(214(3),217(1)),flip(a)].

given #46 (A,wt=17): 21 x * y * z * (y * z @ x) = y * z * x.  [para(9(a,1),10(a,1,2)),demod(9(7))].

given #47 (F,wt=17): 260 (B @ C) * x * (A @ C) != x * (A * B @ C) # answer(D).  [para(10(a,1),220(a,1,2)),demod(237(12),219(10))].

given #48 (F,wt=17): 265 (A * B @ C) * x != (B @ C) * x * (A @ C) # answer(D).  [para(10(a,1),221(a,2,2)),demod(237(9),219(7))].

given #49 (T,wt=5): 231 c_0 * x = x.  [back_demod(168),demod(217(1))].

given #50 (T,wt=7): 228 x * (c_0 @ x) = x.  [back_demod(207),demod(217(1))].

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

given #52 (F,wt=19): 201 (A @ C) * C * A * B * (B @ C) != A * B * C # answer(D).  [para(10(a,1),65(a,2)),demod(11(12),9(12),9(11),9(18))].

given #53 (F,wt=21): 69 (A * B @ C) * x * y != (A @ C) * x * (B @ C) * y # answer(D).  [ur(8,b,36,a),demod(9(7),9(16),9(15))].

given #54 (T,wt=7): 235 x @ x * x = c_0.  [back_demod(130),demod(217(3))].

given #55 (T,wt=7): 237 x @ (y @ z) = c_0.  [back_demod(116),demod(217(3))].

given #56 (A,wt=14): 23 (x @ y) * z != z * u | x @ y = u.  [para(11(a,2),7(a,1))].

given #57 (F,wt=21): 70 x * (A * B @ C) * y != x * (A @ C) * y * (B @ C) # answer(D).  [ur(7,b,36,a)].

given #58 (F,wt=21): 71 (A * B @ C) * x * y != (A @ C) * x * y * (B @ C) # answer(D).  [para(9(a,1),36(a,2,2))].

given #59 (T,wt=5): 329 x @ c_0 = c_0.  [para(217(a,1),237(a,1,2))].

given #60 (T,wt=8): 229 x * y != y | c_0 = x.  [back_demod(206),demod(217(3))].

given #61 (A,wt=14): 24 (x @ y) * z != u * (x @ y) | z = u.  [para(11(a,1),7(a,2))].

given #62 (F,wt=17): 336 C * B * (A * B @ C) != B * C * (A @ C) # answer(D).  [para(10(a,1),71(a,2,2)),demod(11(9),9(9),11(16),9(16))].

given #63 (F,wt=21): 87 (A * B @ C) * x * y != x * (A @ C) * (B @ C) * y # answer(D).  [ur(14,b,39,a),demod(9(16),9(15))].

given #64 (T,wt=8): 241 x * y != x | c_0 = y.  [back_demod(40),demod(217(3))].

given #65 (T,wt=5): 359 c_0 @ x = c_0.  [hyper(241,a,228,a),flip(a)].

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

given #67 (F,wt=21): 89 x * (A * B @ C) * y != x * y * (A @ C) * (B @ C) # answer(D).  [ur(7,b,39,a)].

given #68 (F,wt=21): 90 (A * B @ C) * x * y != x * y * (A @ C) * (B @ C) # answer(D).  [para(9(a,1),39(a,2))].

given #69 (T,wt=9): 268 x * (x * x @ x) = x.  [hyper(13,a,21,a)].

given #70 (T,wt=7): 369 x * x @ x = c_0.  [hyper(241,a,268,a),flip(a)].

given #71 (A,wt=15): 26 (x @ y) * z * u = z * (x @ y) * u.  [para(11(a,1),9(a,1,1)),demod(9(3)),flip(a)].

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

% Proof 1 at 0.07 (+ 0.00) seconds: D.
% Length of proof is 12.
% Level of proof is 4.
% Maximum clause weight is 19.
% Given clauses 71.

6 (A @ C) * (B @ C) != A * B @ C # answer(D).  [input].
7 x * y != x * z | y = z.  [input].
9 (x * y) * z = x * y * z.  [input].
10 x * y * (y @ x) = y * x.  [input].
11 (x @ y) * z = z * (x @ y).  [input].
12 A * B @ C != (A @ C) * (B @ C) # answer(D).  [copy(6),flip(a)].
16 x * y != z * x | z * (z @ x) = y.  [para(10(a,1),7(a,1)),flip(a)].
19 x * y * (y @ x) * z = y * x * z.  [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)].
26 (x @ y) * z * u = z * (x @ y) * u.  [para(11(a,1),9(a,1,1)),demod(9(3)),flip(a)].
30 x * (A * B @ C) != x * (A @ C) * (B @ C) # answer(D).  [ur(7,b,12,a)].
103 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D).  [ur(16,b,30,a),demod(9(12),9(18))].
394 $F # answer(D).  [para(26(a,2),103(a,1,2,2)),demod(19(13),10(8)),xx(a)].

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

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

Given=71. Generated=2327. Kept=387. proofs=1.
Usable=57. Sos=201. Demods=36. Denials=0. Limbo=21, Disabled=114. Hints=0.
Weight_deleted=441. Literals_deleted=0.
Forward_subsumed=1498. Back_subsumed=15.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=63 (1 lex), Back_demodulated=93. Back_unit_deleted=0.
Demod_attempts=39506. Demod_rewrites=3217.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=3848. Nonunit_bsub_feature_tests=1794.
Megabytes=0.36.
User_CPU=0.07, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

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