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


clauses(sos).
x * y * z * y * x = y * x * z * x * y.
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 * y * x = y * x * z * x * y.  [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 * y * x = y * x * z * x * y.  [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=19): 11 x * y * z * y * x = y * x * z * x * y.  [input].

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

given #7 (F,wt=15): 29 (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): 30 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)].

given #10 (T,wt=10): 37 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=15): 43 C * (A @ B) * (C @ C) != (A @ B) * C # answer(N).  [para(15(a,1),29(a,1,2)),flip(a)].

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

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

given #15 (T,wt=10): 39 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): 35 (A @ B) * C * ((A @ B) @ C) != (A @ B) * C # answer(N).  [para(10(a,1),29(a,2))].

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

given #19 (T,wt=11): 40 x * (x @ x) * y = x * y.  [para(15(a,1),9(a,1,1)),flip(a)].

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

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): 32 C * (A @ B) * x * (x @ C) != (A @ B) * x * C # answer(N).  [para(10(a,1),29(a,1,2)),flip(a)].

given #23 (F,wt=17): 103 C * (A @ B) * ((x @ x) @ C) != (A @ B) * C # answer(N).  [para(78(a,1),32(a,1,2,2)),demod(78(15))].

given #24 (T,wt=6): 99 x != y | y = x.  [para(15(a,1),16(a,2)),demod(78(2),88(4),15(3))].

given #25 (T,wt=9): 87 x * ((y @ y) @ x) = x.  [para(78(a,1),10(a,1,2)),demod(78(5))].

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=19): 36 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N).  [ur(7,b,30,a)].

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

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

given #30 (T,wt=9): 107 (x @ x) @ y = y @ y.  [hyper(37,a,87,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=19): 57 x * C * (A @ B) * (C @ C) != x * (A @ B) * C # answer(N).  [ur(7,b,43,a)].

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

given #34 (T,wt=9): 128 x @ x * x = x @ x.  [hyper(37,a,93,a),flip(a)].

given #35 (T,wt=9): 130 ((x @ x) @ y) * z = z.  [para(107(a,2),78(a,1,1))].

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=15): 175 B * A * C * (A @ B) != A * B * C # answer(N).  [para(19(a,1),36(a,1)),flip(a)].

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

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

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

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

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=19): 179 B * A * C * (A @ B) * x != A * B * C * x # answer(N).  [ur(14,b,175,a),demod(9(9),9(8),9(16),9(15))].

given #43 (F,wt=17): 232 A * B * C * ((A @ B) @ C) != A * B * C # answer(N).  [para(10(a,1),179(a,1,2,2)),demod(19(9)),flip(a)].

given #44 (T,wt=5): 193 c_0 @ x = c_0.  [back_demod(184),demod(189(1),189(3))].

given #45 (T,wt=5): 200 c_0 * x = x.  [back_demod(150),demod(189(1),193(2),193(2))].

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=19): 181 x * B * A * C * (A @ B) != x * A * B * C # answer(N).  [ur(7,b,175,a)].

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

given #49 (T,wt=5): 209 x * c_0 = x.  [back_demod(132),demod(189(1),193(2),193(2))].

given #50 (T,wt=7): 210 x @ x * x = c_0.  [back_demod(128),demod(189(3))].

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

given #52 (F,wt=21): 34 (A @ B) * C * x * (x @ (A @ B)) != C * x * (A @ B) # answer(N).  [para(10(a,1),29(a,2,2))].

given #53 (F,wt=21): 59 C * (A @ B) * (C @ (A @ B)) * x != C * (A @ B) * x # answer(N).  [ur(8,b,33,a),demod(9(12),9(11),9(18))].

given #54 (T,wt=7): 214 x * (x @ c_0) = x.  [back_demod(207),demod(209(5))].

given #55 (T,wt=8): 203 x * y != x | c_0 = y.  [back_demod(146),demod(189(3),193(4),193(4))].

given #56 (A,wt=22): 23 x * y * z * y * u != y * u * z * u * y | u = x.  [para(11(a,1),8(a,1)),flip(a)].

given #57 (F,wt=21): 60 x * C * (A @ B) * (C @ (A @ B)) != x * C * (A @ B) # answer(N).  [ur(7,b,33,a)].

given #58 (F,wt=21): 71 (A @ B) * C * ((A @ B) @ C) * x != (A @ B) * C * x # answer(N).  [ur(14,b,35,a),demod(9(11),9(18))].

given #59 (T,wt=5): 290 x @ c_0 = c_0.  [hyper(203,a,214,a),flip(a)].

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

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

given #62 (F,wt=21): 73 x * (A @ B) * C * ((A @ B) @ C) != x * (A @ B) * C # answer(N).  [ur(7,b,35,a)].

given #63 (F,wt=21): 237 A * B * C * ((A @ B) @ C) * x != A * B * C * x # answer(N).  [para(19(a,1),179(a,1,2,2)),demod(19(10)),flip(a)].

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

given #65 (T,wt=7): 313 x * x @ x = c_0.  [hyper(203,a,244,a),flip(a)].

given #66 (A,wt=23): 25 x * y * z * y * x * u = y * x * z * x * y * u.  [para(11(a,1),9(a,1,1)),demod(9(5),9(4),9(3),9(2),9(9),9(8),9(7))].

given #67 (F,wt=21): 241 B * A * C * (A @ B) * (C @ A * B) != C * A * B # answer(N).  [para(20(a,1),179(a,2))].

given #68 (F,wt=21): 243 x * A * B * C * ((A @ B) @ C) != x * A * B * C # answer(N).  [ur(7,b,232,a)].

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

given #70 (T,wt=12): 201 x * (x @ y) != x * y | c_0 = y.  [back_demod(149),demod(189(5),193(6))].

given #71 (A,wt=23): 26 x * y * z * u * z * y = x * z * y * u * y * z.  [para(11(a,1),9(a,2,2)),demod(9(5))].

given #72 (F,wt=21): 261 B * A * C * (A @ B) * (B * C @ A) != B * C * A # answer(N).  [para(21(a,1),179(a,2))].

given #73 (F,wt=21): 307 A * B * C * ((A @ B) @ C) * (C @ B) != A * C * B # answer(N).  [para(10(a,1),237(a,2,2))].

given #74 (T,wt=12): 204 x * y * z != z | x * y = c_0.  [back_demod(145),demod(189(4),193(5)),flip(b)].

given #75 (T,wt=12): 211 x * y != y | x * (x @ y) = c_0.  [back_demod(119),demod(189(3),193(4)),flip(b)].

given #76 (A,wt=23): 27 x * y * z * u * y * x = y * x * z * u * x * y.  [para(9(a,1),11(a,1,2,2)),demod(9(8))].

given #77 (F,wt=23): 48 x * y * z * (A @ B) * C != x * y * z * C * (A @ B) # answer(N).  [ur(13,b,30,a)].

given #78 (F,wt=23): 49 x * y * (A @ B) * C * z != x * y * C * (A @ B) * z # answer(N).  [ur(13,b,29,a)].

given #79 (T,wt=12): 212 x * y * z != x * y | c_0 = z.  [back_demod(114),demod(189(5),193(6))].

given #80 (T,wt=12): 336 x @ y != x * y | y * x = c_0.  [para(10(a,1),204(a,1)),flip(a)].

given #81 (A,wt=23): 28 x * (x @ y) * y * (x @ y) * x = (x @ y) * x * x * y.  [para(10(a,1),11(a,1,2,2)),flip(a)].

given #82 (F,wt=23): 74 x * C * (A @ B) * y * (y @ C) != x * (A @ B) * y * C # answer(N).  [para(10(a,1),31(a,1,2,2)),flip(a)].

given #83 (F,wt=23): 76 C * x * (A @ B) * x * C != x * (A @ B) * C * C * x # answer(N).  [para(11(a,1),31(a,2)),flip(a)].

given #84 (T,wt=12): 356 x * y != y * x | x @ y = c_0.  [para(10(a,1),212(a,1)),flip(b)].

given #85 (T,wt=13): 94 x * y * (x * y @ x) = y * x.  [hyper(16,a,9,a(flip)),demod(9(4))].

given #86 (A,wt=18): 50 x * y * z * u != x * y * z * v | u = v.  [para(9(a,1),13(a,1,2)),demod(9(5))].

given #87 (F,wt=19): 383 (A @ B) * C * (C * (A @ B) @ C) != (A @ B) * C # answer(N).  [para(94(a,1),29(a,2))].

given #88 (F,wt=19): 392 A * B * C * (C * (A @ B) @ C) != A * B * C # answer(N).  [para(94(a,1),179(a,1,2,2)),demod(19(9)),flip(a)].

given #89 (T,wt=13): 208 x * y @ x * y * x * y = c_0.  [back_demod(138),demod(189(8))].

given #90 (T,wt=13): 215 x * y * (y @ y * x) = y * x.  [hyper(7,a,20,a)].

given #91 (A,wt=18): 51 x * y * z != x * u * y | u * (u @ y) = z.  [para(10(a,1),13(a,1,2)),flip(a)].

given #92 (F,wt=19): 418 C * (A @ B) * (C @ C * (A @ B)) != C * (A @ B) # answer(N).  [para(215(a,1),29(a,1)),flip(a)].

given #93 (F,wt=21): 382 C * (A @ B) * ((A @ B) * C @ (A @ B)) != C * (A @ B) # answer(N).  [para(94(a,1),29(a,1)),flip(a)].

given #94 (T,wt=10): 442 x * y != x * z | z = y.  [para(200(a,1),51(a,1,2)),demod(209(3),290(5),209(5))].

given #95 (T,wt=13): 315 x * y * x * y @ x * y = c_0.  [para(9(a,1),313(a,1,1))].

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

given #97 (F,wt=21): 393 B * A * C * (A @ B) * (B * C @ B) != A * C * B # answer(N).  [para(94(a,1),179(a,2,2))].

given #98 (F,wt=21): 419 (A @ B) * C * ((A @ B) @ (A @ B) * C) != (A @ B) * C # answer(N).  [para(215(a,1),29(a,2))].

given #99 (T,wt=12): 456 x * y != y * x | y @ x = c_0.  [para(209(a,1),52(a,1,2))].

given #100 (T,wt=13): 378 x * (y * x @ y) = x * (x @ y).  [hyper(16,a,94,a),flip(a)].

given #101 (A,wt=22): 53 x * y * z * y * x != y * x * u | z * x * y = u.  [para(11(a,1),13(a,1))].

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

% Proof 1 at 0.11 (+ 0.00) seconds: N.
% Length of proof is 18.
% Level of proof is 6.
% Maximum clause weight is 23.
% Given clauses 101.

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 * y * x = y * x * z * x * y.  [input].
12 (A @ B) * C != C * (A @ B) # answer(N).  [input].
13 x * y * z != x * y * u | z = u.  [para(9(a,1),7(a,1)),demod(9(4))].
14 x * y * z != u * z | x * y = u.  [para(9(a,1),8(a,1))].
19 x * y * (y @ x) * z = y * x * z.  [para(10(a,1),9(a,1,1)),demod(9(2),9(5)),flip(a)].
27 x * y * z * u * y * x = y * x * z * u * x * y.  [para(9(a,1),11(a,1,2,2)),demod(9(8))].
30 x * (A @ B) * C != x * C * (A @ B) # answer(N).  [ur(7,b,12,a)].
36 x * y * (A @ B) * C != x * y * C * (A @ B) # answer(N).  [ur(7,b,30,a)].
53 x * y * z * y * x != y * x * u | z * x * y = u.  [para(11(a,1),13(a,1))].
175 B * A * C * (A @ B) != A * B * C # answer(N).  [para(19(a,1),36(a,1)),flip(a)].
179 B * A * C * (A @ B) * x != A * B * C * x # answer(N).  [ur(14,b,175,a),demod(9(9),9(8),9(16),9(15))].
349 A * B * C * (A @ B) * B * A != A * B * C * A * B # answer(N).  [para(27(a,1),179(a,1))].
471 (x @ y) * y * x = x * y.  [hyper(53,a,19,a)].
474 $F # answer(N).  [back_demod(349),demod(471(10)),xx(a)].

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

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

Given=101. Generated=4273. Kept=467. proofs=1.
Usable=73. Sos=238. Demods=52. Denials=0. Limbo=3, Disabled=159. Hints=0.
Weight_deleted=1855. Literals_deleted=0.
Forward_subsumed=1950. Back_subsumed=5.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=100 (0 lex), Back_demodulated=148. Back_unit_deleted=0.
Demod_attempts=88170. Demod_rewrites=9044.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=7061. Nonunit_bsub_feature_tests=2362.
Megabytes=0.46.
User_CPU=0.11, System_CPU=0.00, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

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