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


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

clauses(sos).
A * B * C * B * A != B * A * C * A * B # answer(E).
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 * B * A != B * A * C * A * B # answer(E).  [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 * B * A != B * A * C * A * B # answer(E).  [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=19): 12 A * B * C * B * A != B * A * C * A * B # answer(E).  [input].

given #7 (F,wt=23): 26 A * B * C * B * A * x != B * A * C * A * B * x # answer(E).  [ur(8,b,12,a),demod(9(10),9(9),9(8),9(7),9(20),9(19),9(18),9(17))].

given #8 (F,wt=23): 27 x * A * B * C * B * A != x * B * A * C * A * B # answer(E).  [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): 30 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=23): 28 B * A * C * A * B * (A @ B) != A * B * C * A * B # answer(E).  [para(10(a,1),26(a,1,2,2,2)),flip(a)].

given #13 (F,wt=23): 29 A * B * C * B * A * (B @ A) != B * A * C * B * A # answer(E).  [para(10(a,1),26(a,2,2,2,2))].

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

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

given #18 (F,wt=23): 38 A * B * C * B * A * (B @ B) != B * A * C * A * B # answer(E).  [para(15(a,1),26(a,2,2,2,2,2))].

given #19 (T,wt=11): 24 x @ (y @ z) = u @ (v @ w).  [para(11(a,1),11(a,1))].

given #20 (T,wt=11): 25 (x @ y) @ z = (u @ v) @ w.  [para(11(a,2),11(a,2))].

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=9): 56 x * (x @ x * x) = x.  [hyper(16,a,9,a)].

given #23 (F,wt=9): 63 x @ x * x = x @ x.  [hyper(30,a,56,a),flip(a)].

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

given #25 (T,wt=7): 66 (x @ x) * y = y.  [hyper(13,a,33,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=6): 83 x != y | y = x.  [back_demod(72),demod(74(4),15(3))].

given #28 (F,wt=9): 76 x * ((y @ y) @ x) = x.  [para(66(a,1),10(a,1,2)),demod(66(5))].

given #29 (T,wt=7): 108 x * (y @ y) = x.  [back_demod(74),demod(96(3)),flip(a)].

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

given #30 (T,wt=5): 113 x @ x = c_0.  [new_symbol(109)].

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=5): 117 x * c_0 = x.  [back_demod(108),demod(113(1))].

given #33 (F,wt=5): 121 c_0 @ x = c_0.  [back_demod(92),demod(113(1),113(3))].

given #34 (T,wt=5): 125 c_0 * x = x.  [back_demod(66),demod(113(1))].

given #35 (T,wt=5): 131 x @ c_0 = c_0.  [para(113(a,1),24(a,1,2)),demod(128(4))].

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=7): 127 x @ x * x = c_0.  [back_demod(63),demod(113(3))].

given #38 (F,wt=7): 128 x @ (y @ z) = c_0.  [para(113(a,1),11(a,1,1)),demod(121(2)),flip(a)].

given #39 (T,wt=7): 130 (x @ y) @ z = c_0.  [para(113(a,1),11(a,2))].

given #40 (T,wt=8): 116 x * y != x | c_0 = y.  [back_demod(110),demod(113(3))].

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=25): 157 B * A * C * A * B * (A @ C * B) != A * B * A * C * B # answer(E).  [para(20(a,1),26(a,1,2,2)),flip(a)].

given #43 (F,wt=25): 158 A * B * C * B * A * (B @ C * A) != B * A * B * C * A # answer(E).  [para(20(a,1),26(a,2,2,2))].

given #44 (T,wt=8): 124 x * y != y | c_0 = x.  [back_demod(75),demod(113(3))].

given #45 (T,wt=10): 88 x * y != y * y | y = x.  [para(15(a,1),17(a,1,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=25): 170 B * A * C * A * B * (B * A @ C) != A * B * B * A * C # answer(E).  [para(21(a,1),26(a,1,2,2)),flip(a)].

given #48 (F,wt=25): 171 A * B * C * B * A * (A * B @ C) != B * A * A * B * C # answer(E).  [para(21(a,1),26(a,2,2,2))].

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

given #50 (T,wt=7): 183 x * x @ x = c_0.  [hyper(116,a,168,a),flip(a)].

given #51 (A,wt=11): 39 (x @ y) * z = z * (x @ y).  [back_demod(22),demod(35(6))].

given #52 (F,wt=12): 114 x * y != y | x * (x @ y) = c_0.  [back_demod(112),demod(113(3)),flip(b)].

given #53 (F,wt=12): 115 x * y * z != x * y | c_0 = z.  [back_demod(111),demod(113(5))].

given #54 (T,wt=12): 122 x * (x @ y) != x * y | c_0 = y.  [back_demod(91),demod(113(5))].

given #55 (T,wt=12): 123 x * y * z != z | x * y = c_0.  [back_demod(81),demod(113(4)),flip(b)].

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

given #57 (F,wt=12): 204 (x @ y) * z != z | x @ y = c_0.  [para(39(a,2),116(a,1)),flip(b)].

given #58 (F,wt=12): 207 x * (y @ z) != x | y @ z = c_0.  [para(39(a,1),124(a,1)),flip(b)].

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

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

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

given #62 (F,wt=10): 268 x * y != x * z | z = y.  [para(117(a,1),43(a,2,2)),demod(125(2),131(5),117(5))].

given #63 (F,wt=13): 126 x * y @ x * y * x * y = c_0.  [back_demod(65),demod(113(8))].

given #64 (T,wt=13): 185 x * y * x * y @ x * y = c_0.  [para(9(a,1),183(a,1,1))].

given #65 (T,wt=13): 263 x * (y * x @ y) = x * (x @ y).  [hyper(43,a,21,a),flip(a)].

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

given #67 (F,wt=9): 295 x * y @ x = y @ x.  [hyper(268,a,263,a),flip(a)].

given #68 (F,wt=9): 318 (x @ y) * z @ z = c_0.  [para(39(a,2),295(a,1,1)),demod(130(5))].

given #69 (T,wt=12): 304 x * y != y * x | y @ x = c_0.  [para(117(a,1),44(a,1,2))].

given #70 (T,wt=13): 264 x * (x @ x * y) = x * (x @ y).  [hyper(43,a,20,a),flip(a)].

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

given #72 (F,wt=9): 332 x @ x * y = x @ y.  [hyper(268,a,264,a),flip(a)].

given #73 (F,wt=9): 363 x @ (y @ z) * x = c_0.  [para(39(a,2),332(a,1,2)),demod(128(5))].

given #74 (T,wt=13): 313 x * (x @ y) @ y = x * y @ y.  [para(10(a,1),295(a,1,1)),flip(a)].

given #75 (T,wt=11): 379 (x @ y) * z * z @ z = c_0.  [para(318(a,1),313(a,1,1,2)),demod(117(4),318(3),9(4)),flip(a)].

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

given #77 (F,wt=13): 321 (x @ y) * z @ z * (x @ y) = c_0.  [back_demod(293),demod(312(8))].

given #78 (F,wt=13): 322 x * (y @ z) @ (y @ z) * x = c_0.  [back_demod(291),demod(312(8))].

given #79 (T,wt=13): 327 x * (y @ z) * u @ x * u = c_0.  [para(19(a,1),318(a,1,1)),demod(128(5),125(5))].

given #80 (T,wt=13): 359 x @ y * (y @ x) = x @ y * x.  [para(10(a,1),332(a,1,2)),flip(a)].

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

given #82 (F,wt=10): 442 x * y != z * y | z = x.  [para(117(a,1),51(a,2,2)),demod(131(2),117(2),117(5))].

given #83 (F,wt=11): 431 x @ (y @ z) * x * x = c_0.  [para(318(a,1),359(a,1,2,2)),demod(117(4),363(3),9(4)),flip(a)].

given #84 (T,wt=13): 369 x * y @ x * (z @ u) * y = c_0.  [para(19(a,1),363(a,1,2)),demod(128(2),125(2))].

given #85 (T,wt=13): 388 (x @ y) * z * z * z @ z = c_0.  [para(379(a,1),313(a,1,1,2)),demod(117(5),379(4),9(5),9(4)),flip(a)].

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

given #87 (F,wt=13): 434 x @ (y @ z) * x * x * x = c_0.  [para(379(a,1),359(a,1,2,2)),demod(117(5),431(4),9(5),9(4)),flip(a)].

given #88 (F,wt=14): 86 (x @ y) * z != u * (x @ y) | z = u.  [para(11(a,1),17(a,1,2,2)),demod(35(4)),flip(a)].

given #89 (T,wt=14): 107 x * (y @ z) != u * x | y @ z = u.  [back_demod(89),demod(96(5))].

given #90 (T,wt=14): 149 (x @ y) * z != u * (x @ y) | u = z.  [para(130(a,1),18(a,1,2,2)),demod(117(3)),flip(a)].

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

given #92 (F,wt=14): 187 (x @ y) * z != z * u | x @ y = u.  [para(39(a,2),7(a,1))].

given #93 (F,wt=14): 267 x * (y @ x) * z != y * x | y = z.  [para(10(a,1),43(a,2)),demod(128(7),117(7))].

given #94 (T,wt=12): 508 x * (y @ x) != y * x | c_0 = y.  [para(10(a,1),267(a,1)),demod(39(2),130(6)),flip(b)].

given #95 (T,wt=14): 277 x * y * z != x * y * u | u = z.  [para(9(a,1),268(a,1)),demod(9(4))].

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

given #97 (F,wt=13): 532 x * (x @ y * x) = x * (x @ y).  [hyper(58,a,19,a),demod(39(5))].

given #98 (F,wt=9): 544 x @ y * x = x @ y.  [hyper(268,a,532,a),flip(a)].

given #99 (T,wt=9): 572 x * y @ y = x @ y.  [para(10(a,1),544(a,1,2)),demod(570(4),313(4)),flip(a)].

given #100 (T,wt=11): 569 x @ y * (y @ x) = x @ y.  [back_demod(359),demod(544(5))].

given #101 (A,wt=20): 59 x * y * z != z * u | x * y * (x * y @ z) = u.  [para(9(a,1),16(a,2)),demod(9(8)),flip(a)].

given #102 (F,wt=11): 586 x * (x @ y) @ y = x @ y.  [back_demod(313),demod(572(5))].

given #103 (F,wt=13): 563 x * y @ x * (x @ y) = y @ x.  [back_demod(432),demod(544(8),295(6))].

given #104 (T,wt=13): 570 x * (x @ y) @ x * y = x @ y.  [back_demod(381),demod(558(8))].

given #105 (T,wt=13): 571 x @ y * z * x = x @ y * z.  [para(9(a,1),544(a,1,2))].

given #106 (A,wt=18): 60 x * y != z * y | z * (z @ y) = x * (x @ y).  [para(10(a,1),16(a,1))].

given #107 (F,wt=13): 580 x * y @ y * (y @ x) = x @ y.  [back_demod(552),demod(572(6))].

given #108 (F,wt=13): 581 x * (x @ y) @ y * x = x @ y.  [back_demod(550),demod(572(8),544(6))].

given #109 (T,wt=13): 590 x * y * z @ z = x * y @ z.  [para(9(a,1),572(a,1,1))].

given #110 (T,wt=13): 632 x * x * y @ y * x = x @ y.  [para(563(a,1),563(a,1,2,2)),demod(9(4),10(3),9(5),10(5),570(8))].

given #111 (A,wt=20): 84 x * y * z * (y * z @ u) != y * z * u | u = x.  [para(9(a,1),17(a,1,2)),demod(9(7))].

given #112 (F,wt=13): 646 x * y @ y * y * x = x @ y.  [para(563(a,1),570(a,1,1,2)),demod(9(3),10(3),9(5),10(4),563(8))].

given #113 (F,wt=14): 439 x * y * z != y * z | x * z = z.  [para(10(a,1),51(a,1)),flip(a)].

given #114 (T,wt=14): 441 x * y != z * x | y * (x @ y) = z.  [para(10(a,1),51(a,2)),demod(128(2),117(2)),flip(a)].

given #115 (T,wt=11): 769 x * (x @ y) * (y @ x) = x.  [hyper(441,a,10,a),demod(569(5),9(4))].

given #116 (A,wt=20): 132 x * y * z * (y * z @ u) != y * z * u | x = u.  [para(9(a,1),18(a,1,2)),demod(9(7))].

given #117 (F,wt=9): 777 (x @ y) * (y @ x) = c_0.  [hyper(116,a,769,a),flip(a)].

given #118 (F,wt=10): 803 x @ y != c_0 | y @ x = c_0.  [para(777(a,1),116(a,1)),flip(a),flip(b)].

given #119 (T,wt=10): 815 x * y != y | y @ x = x.  [para(777(a,1),267(a,1,2)),demod(117(2)),flip(a),flip(b)].

given #120 (T,wt=11): 798 (x @ y) * (y @ x) * z = z.  [para(777(a,1),9(a,1,1)),demod(125(2)),flip(a)].

given #121 (A,wt=18): 133 x * y * z != y * u | x * (x @ y) * z = u.  [para(19(a,1),7(a,1))].

given #122 (F,wt=11): 802 (x @ y) * z * (y @ x) = z.  [para(777(a,1),19(a,2,2)),demod(128(3),125(4),117(6))].

given #123 (F,wt=10): 868 x * y != x | y @ x = y.  [para(802(a,1),17(a,1)),flip(a),flip(b)].

given #124 (T,wt=12): 773 x * y != x | y * (x @ y) = c_0.  [para(125(a,1),441(a,2))].

given #125 (T,wt=12): 776 x * x * y != x | x * y = c_0.  [back_demod(626),demod(769(4)),flip(a)].

given #126 (A,wt=18): 134 x * y * (y @ z) * u != y * z * u | z = x.  [para(19(a,1),8(a,1)),flip(a)].

given #127 (F,wt=12): 796 (x @ y) * z != c_0 | y @ x = z.  [para(777(a,1),7(a,1)),flip(a)].

given #128 (F,wt=12): 797 x * (y @ z) != c_0 | z @ y = x.  [para(777(a,1),8(a,1)),flip(a)].

given #129 (T,wt=12): 804 x * (y @ z) != x | z @ y = c_0.  [para(777(a,1),115(a,1,2)),demod(117(2)),flip(a),flip(b)].

given #130 (T,wt=12): 805 x @ y != z | z * (y @ x) = c_0.  [para(777(a,1),123(a,1,2)),demod(117(2)),flip(a)].

given #131 (A,wt=18): 135 x * y * (y @ z) * u != y * z * u | x = z.  [para(19(a,1),8(a,2))].

given #132 (F,wt=12): 808 (x @ y) * z != z | y @ x = c_0.  [para(777(a,1),44(a,1,2)),demod(117(2),130(5)),flip(a),flip(b)].

given #133 (F,wt=12): 812 x * y != c_0 | y @ x = y * x.  [para(777(a,1),52(a,1)),flip(a),flip(b)].

given #134 (T,wt=12): 819 c_0 != x | x * (y @ z) = y @ z.  [para(777(a,1),439(a,1,2)),demod(117(2),777(3)),flip(a)].

given #135 (T,wt=12): 832 x @ y != z | (y @ x) * z = c_0.  [para(798(a,1),116(a,1)),flip(a),flip(b)].

given #136 (A,wt=21): 136 x * y * z * (z @ x * y) * u = z * x * y * u.  [para(19(a,1),9(a,1)),demod(9(2)),flip(a)].

given #137 (F,wt=12): 896 x * y * x != x | y * x = c_0.  [para(10(a,1),776(a,1,2)),demod(10(6))].

given #138 (F,wt=12): 918 c_0 != x | (y @ z) * x = y @ z.  [para(798(a,1),796(a,1)),flip(a),flip(b)].

given #139 (T,wt=14): 477 x * (y @ z) != u | (y @ z) * x = u.  [para(128(a,1),52(a,1,2)),demod(117(2)),flip(a)].

given #140 (T,wt=14): 478 (x @ y) * z != u | z * (x @ y) = u.  [para(130(a,1),52(a,1,2)),demod(117(2)),flip(a)].

given #141 (A,wt=21): 137 x * y * z * (y * z @ x) * u = y * z * x * u.  [para(9(a,1),19(a,1,2)),demod(9(9))].

given #142 (F,wt=14): 480 (x @ y) * z != x * y | y * x = z.  [para(39(a,2),52(a,1))].

given #143 (F,wt=14): 507 x * y * (z @ x) != z * x | z = y.  [para(10(a,1),267(a,1,2)),demod(128(7),117(7))].

given #144 (T,wt=14): 511 (x @ y) * y * z != x * y | x = z.  [para(19(a,1),267(a,1)),demod(130(7),125(7))].

given #145 (T,wt=14): 740 x * y * z != z * y | z @ y = x.  [para(10(a,1),84(a,2)),demod(128(3),117(2))].

given #146 (A,wt=15): 138 x * y * z * (y @ x) = y * x * z.  [para(10(a,1),19(a,1,2,2)),demod(128(6),117(6))].

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

% Proof 1 at 0.16 (+ 0.00) seconds: E.
% Length of proof is 24.
% Level of proof is 12.
% Maximum clause weight is 19.
% Given clauses 146.

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 = u @ (v @ w).  [input].
12 A * B * C * B * A != B * A * C * A * B # answer(E).  [input].
13 x * y * z != x * y * u | z = u.  [para(9(a,1),7(a,1)),demod(9(4))].
15 x * (x @ x) = x.  [hyper(7,a,10,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)].
30 x * y != x | x @ x = y.  [para(15(a,1),7(a,1)),flip(a)].
33 x * (x @ x) * y = x * y.  [para(15(a,1),9(a,1,1)),flip(a)].
66 (x @ x) * y = y.  [hyper(13,a,33,a)].
74 x * (x @ (y @ y)) = x * (y @ y).  [hyper(16,a,66,a)].
76 x * ((y @ y) @ x) = x.  [para(66(a,1),10(a,1,2)),demod(66(5))].
92 (x @ x) @ y = y @ y.  [hyper(30,a,76,a),flip(a)].
96 x * (y @ (z @ u)) = x.  [para(11(a,1),76(a,1,2))].
108 x * (y @ y) = x.  [back_demod(74),demod(96(3)),flip(a)].
109 x @ x = y @ y.  [hyper(30,a,108,a)].
113 x @ x = c_0.  [new_symbol(109)].
117 x * c_0 = x.  [back_demod(108),demod(113(1))].
121 c_0 @ x = c_0.  [back_demod(92),demod(113(1),113(3))].
128 x @ (y @ z) = c_0.  [para(113(a,1),11(a,1,1)),demod(121(2)),flip(a)].
138 x * y * z * (y @ x) = y * x * z.  [para(10(a,1),19(a,1,2,2)),demod(128(6),117(6))].
1052 $F # answer(E).  [para(138(a,2),12(a,1)),demod(9(11),9(10),10(10)),xx(a)].

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

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

Given=146. Generated=7324. Kept=1045. proofs=1.
Usable=111. Sos=641. Demods=218. Denials=0. Limbo=6, Disabled=293. Hints=0.
Weight_deleted=1224. Literals_deleted=0.
Forward_subsumed=5054. Back_subsumed=74.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=353 (1 lex), Back_demodulated=213. Back_unit_deleted=0.
Demod_attempts=102955. Demod_rewrites=16390.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=47724. Nonunit_bsub_feature_tests=15680.
Megabytes=0.78.
User_CPU=0.16, System_CPU=0.00, Wall_clock=1.

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

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

THEOREM PROVED

Exiting with 1 proof.

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