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


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

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

formulas(demodulators).
3 (x * y) * z = x * y * z.  [assumption].
4 x * y * (y @ x) = y * x.  [assumption].
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=19): 5 x * y * z * y * x = y * x * z * x * y.  [assumption].

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

given #7 (F,wt=17): 24 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D).  [ur(2,b,7,a),rewrite(3(14))].

given #8 (F,wt=17): 25 x * (A * B @ C) != x * (A @ C) * (B @ C) # answer(D).  [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): 31 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=21): 26 x * (A * B @ C) * y != x * (A @ C) * (B @ C) * y # answer(D).  [ur(1,b,24,a)].

given #13 (F,wt=21): 29 (A * B @ C) * ((B @ C) @ (A @ C)) != (B @ C) * (A @ C) # answer(D).  [para(4(a,1),24(a,2))].

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

given #15 (T,wt=10): 33 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=21): 30 x * y * (A * B @ C) != x * y * (A @ C) * (B @ C) # answer(D).  [ur(1,b,25,a)].

given #18 (F,wt=19): 61 C * A * B * (A @ C) * (B @ C) != A * B * C # answer(D).  [para(4(a,1),30(a,1)),rewrite(3(5),3(17)),flip(a)].

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

given #20 (T,wt=7): 64 (x @ x) * y = y.  [hyper(8,a,34,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=21): 38 (A * B @ C) * ((B @ C) @ (B @ C)) != (A @ C) * (B @ C) # answer(D).  [para(10(a,1),24(a,2,2))].

given #23 (F,wt=23): 28 (A * B @ C) * x * (x @ (B @ C)) != (A @ C) * x * (B @ C) # answer(D).  [para(4(a,1),24(a,2,2))].

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

given #25 (T,wt=9): 73 x * ((y @ y) @ x) = x.  [para(64(a,1),4(a,1,2)),rewrite(64(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=21): 87 (A * B @ C) * ((x @ x) @ (B @ C)) != (A @ C) * (B @ C) # answer(D).  [para(64(a,1),28(a,1,2)),rewrite(64(19))].

given #28 (F,wt=23): 62 C * A * B * (A @ C) * (B @ C) * x != A * B * C * x # answer(D).  [ur(9,b,61,a),rewrite(3(13),3(12),3(11),3(20),3(19))].

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

given #30 (T,wt=9): 88 (x @ x) @ y = y @ y.  [hyper(31,a,73,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=23): 63 x * C * A * B * (A @ C) * (B @ C) != x * A * B * C # answer(D).  [ur(1,b,61,a)].

given #33 (F,wt=23): 94 (A @ C) * (B @ C) * ((x @ x) @ (A * B @ C)) != A * B @ C # answer(D).  [para(73(a,1),24(a,1)),flip(a)].

given #34 (T,wt=9): 112 x @ x * x = x @ x.  [hyper(31,a,79,a),flip(a)].

given #35 (T,wt=9): 114 ((x @ x) @ y) * z = z.  [para(88(a,2),64(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=17): 152 C * A * (A * B @ C) != A * C * (B @ C) # answer(D).  [para(14(a,1),30(a,2))].

given #38 (F,wt=21): 159 C * A * (A * B @ C) * x != A * C * (B @ C) * x # answer(D).  [ur(9,b,152,a),rewrite(3(9),3(18),3(17))].

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

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

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

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=21): 161 x * C * A * (A * B @ C) != x * A * C * (B @ C) # answer(D).  [ur(1,b,152,a)].

given #43 (F,wt=23): 108 C * A * B * (A @ C) * (B @ C) * (C @ B) != A * C * B # answer(D).  [para(4(a,1),62(a,2,2))].

given #44 (T,wt=5): 178 c_0 @ x = c_0.  [back_rewrite(169),rewrite(174(1),174(3))].

given #45 (T,wt=5): 184 c_0 * x = x.  [back_rewrite(134),rewrite(174(1),178(2),178(2))].

given #46 (A,wt=17): 16 x * y * z * (y * z @ x) = y * z * x.  [para(3(a,1),4(a,1,2)),rewrite(3(7))].

given #47 (F,wt=23): 109 A * B * C * (A @ C) * B != A * B * C * B * (A @ C) # answer(D).  [para(5(a,1),62(a,1,2,2)),rewrite(14(19),14(14)),flip(a)].

given #48 (F,wt=23): 164 C * A * (A * B @ C) * ((B @ C) @ C) != A * (B @ C) * C # answer(D).  [para(4(a,1),159(a,2,2))].

given #49 (T,wt=5): 194 x * c_0 = x.  [back_rewrite(115),rewrite(174(1),178(2),178(2))].

given #50 (T,wt=7): 195 x @ x * x = c_0.  [back_rewrite(112),rewrite(174(3))].

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

given #52 (F,wt=25): 27 (A @ C) * (B @ C) * x * (x @ (A * B @ C)) != x * (A * B @ C) # answer(D).  [para(4(a,1),24(a,1)),flip(a)].

given #53 (F,wt=25): 42 x * y * z * (A * B @ C) != x * y * z * (A @ C) * (B @ C) # answer(D).  [ur(8,b,25,a)].

given #54 (T,wt=7): 199 x * (x @ c_0) = x.  [back_rewrite(191),rewrite(194(5))].

given #55 (T,wt=8): 187 x * y != x | c_0 = y.  [back_rewrite(130),rewrite(174(3),178(4),178(4))].

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

given #57 (F,wt=25): 43 x * y * (A * B @ C) * z != x * y * (A @ C) * (B @ C) * z # answer(D).  [ur(8,b,24,a)].

given #58 (F,wt=25): 49 x * (A @ C) * (B @ C) * ((A * B @ C) @ x) != (A * B @ C) * x # answer(D).  [para(4(a,1),26(a,1)),flip(a)].

given #59 (T,wt=5): 252 x @ c_0 = c_0.  [hyper(187,a,199,a),flip(a)].

given #60 (T,wt=8): 190 x * y != y | c_0 = x.  [back_rewrite(125),rewrite(174(3),178(4))].

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

given #62 (F,wt=25): 50 x * (A * B @ C) * ((B @ C) @ (A @ C)) != x * (B @ C) * (A @ C) # answer(D).  [para(4(a,1),26(a,2,2))].

given #63 (F,wt=25): 52 (A * B @ C) * ((B @ C) @ (A @ C)) * x != (B @ C) * (A @ C) * x # answer(D).  [ur(2,b,29,a),rewrite(3(14),3(22))].

given #64 (T,wt=9): 214 x * (x * x @ x) = x.  [hyper(8,a,16,a)].

given #65 (T,wt=7): 264 x * x @ x = c_0.  [hyper(187,a,214,a),flip(a)].

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

given #67 (F,wt=25): 160 x * y * C * A * (A * B @ C) != x * y * A * C * (B @ C) # answer(D).  [ur(8,b,152,a)].

given #68 (F,wt=25): 162 x * C * A * (A * B @ C) * y != x * A * C * (B @ C) * y # answer(D).  [ur(1,b,159,a)].

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

given #70 (T,wt=12): 185 x * (x @ y) != x * y | c_0 = y.  [back_rewrite(133),rewrite(174(5),178(6))].

given #71 (A,wt=23): 21 x * y * z * u * z * y = x * z * y * u * y * z.  [para(5(a,1),3(a,2,2)),rewrite(3(5))].

given #72 (F,wt=25): 163 A * C * (B @ C) * ((A * B @ C) @ A) != C * (A * B @ C) * A # answer(D).  [para(4(a,1),159(a,1,2)),flip(a)].

given #73 (F,wt=25): 165 A * C * (A * B @ C) * C * A != A * C * (B @ C) * A * C # answer(D).  [para(5(a,1),159(a,1))].

given #74 (T,wt=12): 188 x * y * z != z | x * y = c_0.  [back_rewrite(129),rewrite(174(4),178(5)),flip(b)].

given #75 (T,wt=12): 196 x * y != y | x * (x @ y) = c_0.  [back_rewrite(100),rewrite(174(3),178(4)),flip(b)].

given #76 (A,wt=23): 22 x * y * z * u * y * x = y * x * z * u * x * y.  [para(3(a,1),5(a,1,2,2)),rewrite(3(8))].

given #77 (F,wt=25): 166 C * A * (A * B @ C) * C * A != C * A * (B @ C) * A * C # answer(D).  [para(5(a,1),159(a,2))].

given #78 (F,wt=25): 210 C * A * B * (A @ C) * (B @ C) * (C @ A * B) != C * A * B # answer(D).  [para(15(a,1),62(a,2))].

given #79 (T,wt=12): 197 x * y * z != x * y | c_0 = z.  [back_rewrite(95),rewrite(174(5),178(6))].

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

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

given #82 (F,wt=25): 213 C * A * (A * B @ C) * ((B @ C) @ A * C) != (B @ C) * A * C # answer(D).  [para(15(a,1),159(a,2))].

given #83 (F,wt=25): 222 A * B * C * ((A @ C) * (B @ C) @ B) != A * C * (B @ C) * B # answer(D).  [para(16(a,1),62(a,1,2,2)),rewrite(14(13)),flip(a)].

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

given #85 (T,wt=13): 80 x * y * (x * y @ x) = y * x.  [hyper(11,a,3,a(flip)),rewrite(3(4))].

given #86 (A,wt=18): 44 x * y * z * u != x * y * z * v | u = v.  [para(3(a,1),8(a,1,2)),rewrite(3(5))].

given #87 (F,wt=25): 223 C * A * B * (A @ C) * (B @ C) * (B * C @ A) != B * C * A # answer(D).  [para(16(a,1),62(a,2))].

given #88 (F,wt=25): 226 C * A * (A * B @ C) * (C * (B @ C) @ A) != C * (B @ C) * A # answer(D).  [para(16(a,1),159(a,2))].

given #89 (T,wt=13): 192 x * y @ x * y * x * y = c_0.  [back_rewrite(122),rewrite(174(8))].

given #90 (T,wt=13): 200 x * y * (y @ y * x) = y * x.  [hyper(1,a,15,a)].

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

given #92 (F,wt=25): 325 (A * B @ C) * ((A @ C) * (B @ C) @ (A @ C)) != (B @ C) * (A @ C) # answer(D).  [para(80(a,1),24(a,2))].

given #93 (F,wt=25): 328 C * A * B * (A @ C) * (B @ C) * (B * C @ B) != A * C * B # answer(D).  [para(80(a,1),62(a,2,2))].

given #94 (T,wt=10): 371 x * y != x * z | z = y.  [para(184(a,1),45(a,1,2)),rewrite(194(3),252(5),194(5))].

given #95 (T,wt=13): 266 x * y * x * y @ x * y = c_0.  [para(3(a,1),264(a,1,1))].

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

given #97 (F,wt=25): 331 C * A * (A * B @ C) * (C * (B @ C) @ C) != A * (B @ C) * C # answer(D).  [para(80(a,1),159(a,2,2))].

given #98 (F,wt=25): 353 (A * B @ C) * ((B @ C) @ (B @ C) * (A @ C)) != (B @ C) * (A @ C) # answer(D).  [para(200(a,1),24(a,2))].

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

given #100 (T,wt=13): 321 x * (y * x @ y) = x * (x @ y).  [hyper(11,a,80,a),flip(a)].

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

given #102 (F,wt=25): 356 C * A * B * (A @ C) * (B @ C) * (C @ C * B) != A * C * B # answer(D).  [para(200(a,1),62(a,2,2))].

given #103 (F,wt=9): 384 x * y @ x = y @ x.  [hyper(371,a,321,a),flip(a)].

given #104 (T,wt=11): 395 (x @ y) * y * x = x * y.  [hyper(47,a,14,a)].

given #105 (T,wt=9): 457 (x @ y) @ y * x = c_0.  [para(395(a,1),299(a,1)),rewrite(3(4),4(4)),xx(a)].

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

given #107 (F,wt=17): 419 (A * B @ C) * C * B != (A @ C) * B * C # answer(D).  [para(395(a,1),24(a,2,2))].

given #108 (F,wt=19): 418 (A @ C) * (B @ C) * C * A * B != A * B * C # answer(D).  [para(395(a,1),24(a,1)),rewrite(3(5)),flip(a)].

given #109 (T,wt=9): 458 y * x @ (x @ y) = c_0.  [para(395(a,1),299(a,2)),rewrite(3(3),4(3)),xx(a)].

given #110 (T,wt=9): 469 x * y @ (x @ y) = c_0.  [para(395(a,1),384(a,1,1)),rewrite(458(6))].

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

given #112 (F,wt=21): 420 ((B @ C) @ (A @ C)) * (A * B @ C) != (B @ C) * (A @ C) # answer(D).  [para(395(a,1),25(a,2))].

given #113 (F,wt=21): 426 x * (A * B @ C) * C * B != x * (A @ C) * B * C # answer(D).  [para(395(a,1),26(a,2,2,2))].

given #114 (T,wt=9): 478 x * y @ y * x = c_0.  [para(457(a,1),384(a,2)),rewrite(3(3),4(3))].

given #115 (T,wt=11): 471 (x * y @ y) @ x * y = c_0.  [para(4(a,1),457(a,1,2)),rewrite(400(3))].

given #116 (A,wt=18): 56 x * y * (y @ z) != u * y * z | u * z = x.  [para(4(a,1),9(a,1,2)),flip(a)].

given #117 (F,wt=21): 441 C * A * (A * B @ C) * C * B != A * C * B * C # answer(D).  [para(395(a,1),159(a,2,2,2))].

given #118 (F,wt=21): 495 (A * B @ C) * C * B * x != (A @ C) * B * C * x # answer(D).  [ur(54,b,419,a),rewrite(3(18),3(17))].

given #119 (T,wt=10): 572 x * y != z * y | z = x.  [para(194(a,1),56(a,2,2)),rewrite(252(2),194(2),194(5))].

given #120 (T,wt=11): 479 (x @ y) @ y * y * x = c_0.  [para(384(a,1),457(a,1,1))].

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

given #122 (F,wt=21): 512 (A * B @ C) * B * C != (A @ C) * B * C * (B @ C) # answer(D).  [para(469(a,1),28(a,1,2,2)),rewrite(194(10),3(19))].

given #123 (F,wt=21): 582 (A * B @ C) * C * B * (C @ B) != (A @ C) * C * B # answer(D).  [para(4(a,1),495(a,2,2))].

given #124 (T,wt=11): 500 x * y @ (x * y @ y) = c_0.  [para(4(a,1),458(a,1,1)),rewrite(400(4))].

given #125 (T,wt=11): 507 x * x * y @ (y @ x) = c_0.  [para(384(a,1),458(a,1,2))].

given #126 (A,wt=18): 58 x * y * z * (z @ u) != z * u | x * y = u.  [para(4(a,1),9(a,2))].

given #127 (F,wt=21): 611 (A * B @ C) * C * C * B != (A @ C) * C * B * C # answer(D).  [para(507(a,1),28(a,1,2,2)),rewrite(194(12),3(23),3(22),4(22))].

given #128 (F,wt=23): 424 x * (A @ C) * (B @ C) * C * A * B != x * A * B * C # answer(D).  [para(395(a,1),26(a,1,2)),rewrite(3(5)),flip(a)].

given #129 (T,wt=11): 525 x * y * x @ (y @ x) = c_0.  [para(384(a,1),469(a,1,2)),rewrite(3(2))].

given #130 (T,wt=11): 639 x * y * y @ (x @ y) = c_0.  [para(525(a,1),384(a,2)),rewrite(415(4))].

given #131 (A,wt=22): 59 x * y * z * y * x != u * z * x * y | y * x = u.  [para(5(a,1),9(a,1))].

given #132 (F,wt=23): 436 C * A * B * (A @ C) * B * C != A * B * C * C * B # answer(D).  [para(395(a,1),62(a,1,2,2,2,2))].

given #133 (F,wt=23): 440 A * C * (B @ C) * C * A * B != C * A * A * B * C # answer(D).  [para(395(a,1),159(a,1,2,2)),rewrite(3(7)),flip(a)].

given #134 (T,wt=12): 391 x * (x @ y) != x | x @ y = c_0.  [para(321(a,1),187(a,1)),rewrite(384(6)),flip(b)].

given #135 (T,wt=12): 450 x * y != x | (x @ y) * y = c_0.  [para(395(a,1),188(a,1))].

given #136 (A,wt=15): 68 x * y * y * x = y * x * x * y.  [para(34(a,1),5(a,1,2)),rewrite(64(6))].

given #137 (F,wt=23): 498 (A @ C) * (B @ C) * C * A * B * x != A * B * C * x # answer(D).  [ur(54,b,418,a),rewrite(3(12),3(11),3(20),3(19))].

given #138 (F,wt=19): 711 A * B * C * (B @ A) != (A @ C) * B * C * A # answer(D).  [para(4(a,1),498(a,1,2,2,2)),rewrite(415(12)),flip(a)].

given #139 (T,wt=12): 455 (x @ y) * y != x * y | c_0 = x.  [para(395(a,1),197(a,1)),flip(a)].

given #140 (T,wt=13): 350 x * (x @ x * y) = x * (x @ y).  [hyper(11,a,200,a),flip(a)].

given #141 (A,wt=20): 81 x * y * z != u * x * y | u * (u @ x * y) = z.  [para(3(a,1),11(a,1))].

given #142 (F,wt=23): 614 (A @ C) * (B @ C) * C * C * A * B != C * A * B * C # answer(D).  [para(507(a,1),27(a,1,2,2,2)),rewrite(194(15),3(28),3(27),3(26),16(27))].

given #143 (F,wt=23): 656 C * A * (B @ C) * A * C * B != C * A * A * B * C # answer(D).  [para(20(a,1),440(a,1))].

given #144 (T,wt=9): 726 x @ x * y = x @ y.  [hyper(371,a,350,a),flip(a)].

given #145 (T,wt=9): 766 (x @ y) @ x * y = c_0.  [para(395(a,1),726(a,1,2)),rewrite(457(6))].

given #146 (A,wt=20): 82 x * y * z != z * u | x * y * (x * y @ z) = u.  [para(3(a,1),11(a,2)),rewrite(3(8)),flip(a)].

given #147 (F,wt=23): 665 C * A * B * (A @ C) * B * C != A * C * B * B * C # answer(D).  [para(68(a,1),62(a,2,2)),rewrite(395(13))].

given #148 (F,wt=23): 712 (A @ C) * (B @ C) * C * A * B * (C @ B) != A * C * B # answer(D).  [para(4(a,1),498(a,2,2))].

given #149 (T,wt=11): 767 (x @ y) @ x * y * x = c_0.  [para(726(a,1),457(a,1,1)),rewrite(3(3))].

given #150 (T,wt=11): 768 x * y * x @ (x @ y) = c_0.  [para(726(a,1),458(a,1,2)),rewrite(3(2))].

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

given #152 (F,wt=21): 824 (A * B @ C) * B * C * B != (A @ C) * B * B * C # answer(D).  [para(768(a,1),28(a,1,2,2)),rewrite(194(12),3(23),3(22),4(22))].

given #153 (F,wt=23): 713 A * B * C * (B @ A) * x != (A @ C) * B * C * A * x # answer(D).  [para(14(a,1),498(a,1,2,2,2)),rewrite(415(13)),flip(a)].

given #154 (T,wt=11): 769 x * x * y @ (x @ y) = c_0.  [para(726(a,1),469(a,1,2))].

given #155 (T,wt=11): 782 x * y @ (y @ x * y) = c_0.  [back_rewrite(510),rewrite(755(4))].

given #156 (A,wt=20): 102 x * y * z * (y * z @ u) != y * z * u | u = x.  [para(3(a,1),12(a,1,2)),rewrite(3(7))].

given #157 (F,wt=21): 836 (A @ C) * B * C * A * ((B @ A) @ C) != B * A * C # answer(D).  [para(4(a,1),713(a,1,2,2)),rewrite(14(9)),flip(a)].

given #158 (F,wt=21): 840 A * B * C * (B @ A) * (C * A @ B) != A * C * B # answer(D).  [para(16(a,1),713(a,2,2)),rewrite(415(24))].

given #159 (T,wt=11): 792 (x @ y * x) @ y * x = c_0.  [para(4(a,1),766(a,1,2)),rewrite(755(3))].

given #160 (T,wt=11): 801 (x @ y) @ y * x * y = c_0.  [para(384(a,1),766(a,1,1)),rewrite(3(3))].

given #161 (A,wt=20): 120 x * y * z * (y * z @ u) != y * z * u | x = u.  [para(3(a,1),13(a,1,2)),rewrite(3(7))].

given #162 (F,wt=21): 883 A * B * C * ((A @ C) * (B @ C) @ B) != A * B * C # answer(D).  [back_rewrite(222),rewrite(866(23))].

given #163 (F,wt=23): 717 (A @ C) * B * C * A * A * B != A * B * C * B * A # answer(D).  [para(68(a,1),498(a,1,2,2,2)),rewrite(415(16))].

given #164 (T,wt=11): 805 (x @ y) @ x * x * y = c_0.  [para(726(a,1),766(a,1,1))].

given #165 (T,wt=11): 866 x * (y @ x) * y = y * x.  [para(782(a,1),4(a,1,2,2)),rewrite(194(5),526(4),3(5),744(4)),flip(a)].

given #166 (A,wt=18): 136 x * y * z != y * u | x * (x @ y) * z = u.  [para(14(a,1),1(a,1))].

given #167 (F,wt=17): 936 C * A * (A * B @ C) * B != A * B * C # answer(D).  [para(866(a,1),159(a,2,2))].

given #168 (F,wt=19): 931 C * (A @ C) * (B @ C) * A * B != A * B * C # answer(D).  [para(866(a,1),26(a,1)),rewrite(3(5)),flip(a)].

given #169 (T,wt=11): 874 x * y @ (x @ y * x) = c_0.  [para(782(a,1),384(a,2)),rewrite(526(4))].

given #170 (T,wt=11): 899 (x @ y * x) @ x * y = c_0.  [para(792(a,1),726(a,2)),rewrite(526(6))].

given #171 (A,wt=18): 137 x * y * (y @ z) * u != y * z * u | z = x.  [para(14(a,1),2(a,1)),flip(a)].

given #172 (F,wt=21): 943 x * C * A * (A * B @ C) * B != x * A * B * C # answer(D).  [para(866(a,1),162(a,2,2,2))].

given #173 (F,wt=21): 989 C * A * (A * B @ C) * B * x != A * B * C * x # answer(D).  [ur(572,b,936,a),rewrite(3(6),3(5),3(18),3(17),3(16)),flip(a)].

given #174 (T,wt=11): 911 (x @ y) @ x * y * y = c_0.  [para(801(a,1),726(a,2)),rewrite(415(5))].

given #175 (T,wt=11): 927 (x @ y) * x = x * (x @ y).  [hyper(11,a,866,a),flip(a)].

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

given #177 (F,wt=17): 1061 (A * B @ C) * B != (A @ C) * B * (B @ C) # answer(D).  [para(927(a,1),24(a,2,2))].

given #178 (F,wt=19): 1039 A * B * C * (B @ (A * B @ C)) != A * B * C # answer(D).  [para(4(a,1),989(a,1,2,2)),rewrite(16(11)),flip(a)].

given #179 (T,wt=7): 1054 x @ (x @ y) = c_0.  [hyper(383,a,927,a)].

given #180 (T,wt=7): 1055 (x @ y) @ x = c_0.  [hyper(299,a,927,a)].

given #181 (A,wt=21): 139 x * y * z * (z @ x * y) * u = z * x * y * u.  [para(14(a,1),3(a,1)),rewrite(3(2)),flip(a)].

given #182 (F,wt=21): 1041 C * A * (A * B @ C) * B * (C @ B) != A * C * B # answer(D).  [para(4(a,1),989(a,2,2))].

given #183 (F,wt=21): 1060 A * B * (A * B @ C) != (A @ C) * (B @ C) * A * B # answer(D).  [para(927(a,1),24(a,1)),rewrite(3(9))].

given #184 (T,wt=11): 979 x * (x @ y) * (y @ x) = x.  [hyper(136,a,4,a)].

given #185 (T,wt=9): 1165 (x @ y) * (y @ x) = c_0.  [hyper(187,a,979,a),flip(a)].

given #186 (A,wt=21): 140 x * y * z * (y * z @ x) * u = y * z * x * u.  [para(3(a,1),14(a,1,2)),rewrite(3(9))].

given #187 (F,wt=13): 1200 (A * B @ C) * (C @ B) != A @ C # answer(D).  [para(1165(a,1),24(a,2,2)),rewrite(194(14))].

given #188 (F,wt=15): 1195 C * A * B * (A @ C) != A * C * B # answer(D).  [back_rewrite(108),rewrite(1165(13),194(8))].

given #189 (T,wt=9): 1227 (x @ y) @ (y @ x) = c_0.  [para(1165(a,1),299(a,1)),rewrite(1165(4)),xx(a)].

given #190 (T,wt=10): 1216 x @ y != c_0 | y @ x = c_0.  [para(1165(a,1),187(a,1)),flip(a),flip(b)].

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

given #192 (F,wt=15): 1199 (A @ C) * (B @ C) * (C @ A * B) != c_0 # answer(D).  [para(1165(a,1),24(a,1)),flip(a)].

given #193 (F,wt=15): 1201 (C @ A * B) * (A @ C) * (B @ C) != c_0 # answer(D).  [para(1165(a,1),25(a,1)),flip(a)].

given #194 (T,wt=11): 1085 x * (x @ y) @ (x @ y) = c_0.  [para(927(a,1),384(a,1,1)),rewrite(1054(6))].

given #195 (T,wt=11): 1090 (x @ y) @ x * (x @ y) = c_0.  [para(927(a,1),726(a,1,2)),rewrite(1055(6))].

given #196 (A,wt=22): 146 x * y * z * u != x * z * v | y * (y @ z) * u = v.  [para(14(a,1),8(a,1,2))].

given #197 (F,wt=17): 1203 x * (A @ C) * (B @ C) * (C @ A * B) != x # answer(D).  [para(1165(a,1),26(a,1,2)),rewrite(194(2)),flip(a)].

given #198 (F,wt=17): 1204 x * (A * B @ C) * (C @ B) != x * (A @ C) # answer(D).  [para(1165(a,1),26(a,2,2,2)),rewrite(194(15))].

given #199 (T,wt=11): 1198 (x @ y) * (y @ x) * z = z.  [para(1165(a,1),3(a,1,1)),rewrite(184(2)),flip(a)].

given #200 (T,wt=9): 1398 ((x @ y) @ z) @ z = c_0.  [para(1198(a,1),766(a,1,2)),rewrite(1397(4))].

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

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

% Proof 1 at 0.35 (+ 0.01) seconds: D.
% Length of proof is 27.
% Level of proof is 8.
% Maximum clause weight is 23.
% Given clauses 201.

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 = y * x * z * x * y.  [assumption].
6 (A @ C) * (B @ C) != A * B @ C # answer(D).  [assumption].
7 A * B @ C != (A @ C) * (B @ C) # answer(D).  [copy(6),flip(a)].
8 x * y * z != x * y * u | z = u.  [para(3(a,1),1(a,1)),rewrite(3(4))].
9 x * y * z != u * z | x * y = u.  [para(3(a,1),2(a,1))].
10 x * (x @ x) = x.  [hyper(1,a,4,a)].
14 x * y * (y @ x) * z = y * x * z.  [para(4(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)].
20 x * y * z * y * x * u = y * x * z * x * y * u.  [para(5(a,1),3(a,1,1)),rewrite(3(5),3(4),3(3),3(2),3(9),3(8),3(7))].
24 (A * B @ C) * x != (A @ C) * (B @ C) * x # answer(D).  [ur(2,b,7,a),rewrite(3(14))].
34 x * (x @ x) * y = x * y.  [para(10(a,1),3(a,1,1)),flip(a)].
47 x * y * z * y * x != y * x * u | z * x * y = u.  [para(5(a,1),8(a,1))].
54 x * y * z * u != v * u | x * y * z = v.  [para(3(a,1),9(a,1,2))].
64 (x @ x) * y = y.  [hyper(8,a,34,a)].
68 x * y * y * x = y * x * x * y.  [para(34(a,1),5(a,1,2)),rewrite(64(6))].
147 x * y * z != y * x * u | (x @ y) * z = u.  [para(14(a,1),8(a,1))].
395 (x @ y) * y * x = x * y.  [hyper(47,a,14,a)].
415 (x @ y) * y * x * z = x * y * z.  [para(395(a,1),3(a,1,1)),rewrite(3(2),3(5)),flip(a)].
418 (A @ C) * (B @ C) * C * A * B != A * B * C # answer(D).  [para(395(a,1),24(a,1)),rewrite(3(5)),flip(a)].
498 (A @ C) * (B @ C) * C * A * B * x != A * B * C * x # answer(D).  [ur(54,b,418,a),rewrite(3(12),3(11),3(20),3(19))].
717 (A @ C) * B * C * A * A * B != A * B * C * B * A # answer(D).  [para(68(a,1),498(a,1,2,2,2)),rewrite(415(16))].
916 (A @ C) * B * C * A * A * B != B * A * C * A * B # answer(D).  [para(5(a,1),717(a,2))].
1437 (x @ y) * z * y * x * u = z * x * y * u.  [hyper(147,a,20,a)].
1438 $F # answer(D).  [resolve(1437,a,916,a)].

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

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

Given=201. Generated=13334. Kept=1436. proofs=1.
Usable=159. Sos=876. Demods=321. Limbo=2, Disabled=404. Hints=0.
Weight_deleted=5987. Literals_deleted=0.
Forward_subsumed=5911. Back_subsumed=52.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=484 (0 lex), Back_demodulated=346. Back_unit_deleted=0.
Demod_attempts=301608. Demod_rewrites=32663.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=44723. Nonunit_bsub_feature_tests=11381.
Megabytes=1.32.
User_CPU=0.35, System_CPU=0.01, Wall_clock=0.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3868 exit (max_proofs) Wed Nov 22 11:24:23 2006