============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11396 was started by mccune on cleo.thornwood,
Sat Aug 12 21:00:58 2006
The command was "/home/mccune/bin/prover9 -f quot-xy3b.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file quot-xy3b.in

op(400,infix_right,*).
set(restrict_denials).
assign(max_weight,35).

formulas(sos).
(x * y) * z = x * y * z # label(associativity).
x * y != u | x * z != u | y = z # label(left_cancellation_extended).
y * x != u | z * x != u | y = z # label(right_cancellation_extended).
x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").
b * b0 = a * a0.
d * b0 = c * a0.
b * d0 = a * c0.
d * d0 != c * c0.
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) * z = x * y * z # label(associativity).  [assumption].
x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
b * b0 = a * a0.  [assumption].
d * b0 = c * a0.  [assumption].
b * d0 = a * c0.  [assumption].
d * d0 != c * c0.  [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, a0, b, b0, c, c0, d, d0, * ]).
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, 3).  % (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) * z = x * y * z # label(associativity).  [assumption].
2 x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
8 d * d0 != c * c0.  [assumption].
end_of_list.

formulas(demodulators).
1 (x * y) * z = x * y * z # label(associativity).  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
end_of_list.

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

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

% Starting search at 0.00 seconds.

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

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

given #3 (I,wt=13): 3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].

given #4 (I,wt=23): 4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].

given #5 (I,wt=7): 5 b * b0 = a * a0.  [assumption].

given #6 (I,wt=7): 6 d * b0 = c * a0.  [assumption].

given #7 (I,wt=7): 7 b * d0 = a * c0.  [assumption].

given #8 (I,wt=0): 8 d * d0 != c * c0.  [assumption].

given #9 (T,wt=11): 18 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #10 (T,wt=11): 22 d * b0 * x = c * a0 * x.  [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #11 (A,wt=17): 9 x * y * z != u | x * y * v != u | z = v.  [para(1(a,1),2(a,1)),rewrite(1(5))].

given #12 (F,wt=0): 30 d * d0 * x * c * c0 * x * c * c0 * x != x * c * c0 * x * c * c0 * x * c * c0.  [ur(3,b,4,a,c,8,a),rewrite(1(10),1(12),1(14),1(25),1(27))].

given #13 (F,wt=0): 31 d * d0 * x != c * c0 * x.  [ur(3,b,1,a,c,8,a),rewrite(1(4))].

given #14 (T,wt=11): 26 b * d0 * x = a * c0 * x.  [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].

given #15 (T,wt=13): 19 a * a0 != x | b * y != x | b0 = y.  [para(5(a,1),2(a,1))].

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

given #17 (F,wt=0): 32 c * c0 * x * d * d0 * x * d * d0 * x != x * d * d0 * x * d * d0 * x * d * d0.  [ur(3,a,4,a,c,8,a),rewrite(1(10),1(12),1(14),1(25),1(27))].

given #18 (F,wt=0): 33 x * y * d * d0 != x * y * c * c0.  [ur(2,b,1,a,c,8,a),rewrite(1(5))].

given #19 (T,wt=13): 20 a * a0 != x | y * b0 != x | b = y.  [para(5(a,1),3(a,1))].

given #20 (T,wt=13): 23 c * a0 != x | d * y != x | b0 = y.  [para(6(a,1),2(a,1))].

given #21 (A,wt=31): 11 x * y * y * x * y * y * x * y = y * x * y * y * x * y * y * x.  [hyper(2,a,1,a(flip),b,4,a),rewrite(1(3),1(5),1(12),1(14))].

given #22 (F,wt=0): 34 x * d * d0 != x * c * c0.  [ur(2,b,1,a(flip),c,8,a),rewrite(1(8))].

given #23 (F,wt=0): 44 x * y * z * d * d0 != x * y * z * c * c0.  [ur(9,b,1,a,c,8,a),rewrite(1(6))].

given #24 (T,wt=13): 24 c * a0 != x | y * b0 != x | d = y.  [para(6(a,1),3(a,1))].

given #25 (T,wt=13): 27 a * c0 != x | b * y != x | d0 = y.  [para(7(a,1),2(a,1))].

given #26 (A,wt=27): 12 x * y * x * y * x * y * z = y * x * y * x * y * x * z.  [para(4(a,1),1(a,1,1)),rewrite(1(6),1(5),1(4),1(3),1(2),1(11),1(10),1(9),1(8))].

given #27 (F,wt=0): 55 x * y * z * d * d0 * u * c * c0 * u * c * c0 * u != x * y * z * u * c * c0 * u * c * c0 * u * c * c0.  [ur(9,b,1,a,c,30,a),rewrite(1(17))].

given #28 (F,wt=0): 56 x * y * d * d0 * z * c * c0 * z * c * c0 * z != x * y * z * c * c0 * z * c * c0 * z * c * c0.  [ur(9,b,1,a(flip),c,30,a),rewrite(1(32))].

given #29 (T,wt=13): 28 a * c0 != x | y * d0 != x | b = y.  [para(7(a,1),3(a,1))].

given #30 (T,wt=13): 83 a * a0 != x | a * c0 != x | d0 = b0.  [para(7(a,1),19(b,1)),flip(c)].

given #31 (A,wt=35): 13 x * y * z * x * y * z * x * y * z = z * x * y * z * x * y * z * x * y.  [para(4(a,1),1(a,1)),rewrite(1(5),1(7),1(11),1(13)),flip(a)].

given #32 (F,wt=0): 57 d * d0 * x * c * c0 * x * c * c0 * x * y * x * c * c0 * x * c * c0 * x * c * c0 * y * x * c * c0 * x * c * c0 * x * c * c0 * y != y * x * c * c0 * x * c * c0 * x * c * c0 * y * x * c * c0 * x * c * c0 * x * c * c0 * y * x * c * c0 * x * c * c0 * x * c * c0.  [ur(3,b,4,a,c,30,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86))].

given #33 (F,wt=0): 58 d * d0 * x * c * c0 * x * c * c0 * x * y != x * c * c0 * x * c * c0 * x * c * c0 * y.  [ur(3,b,1,a,c,30,a),rewrite(1(15),1(14),1(13),1(12),1(11),1(10),1(9),1(8),1(29),1(28),1(27),1(26),1(25),1(24),1(23))].

given #34 (T,wt=13): 139 a * a0 != x | c * a0 != x | d = b.  [para(6(a,1),20(b,1)),flip(c)].

given #35 (T,wt=17): 35 a * a0 * x != y | b * z != y | b0 * x = z.  [para(18(a,1),2(a,1))].

given #36 (A,wt=27): 14 x * y * z * y * z * y * z = x * z * y * z * y * z * y.  [para(4(a,1),1(a,2,2)),rewrite(1(6))].

given #37 (F,wt=0): 59 x * c * c0 * x * c * c0 * x * c * c0 * y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y != y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x * y * d * d0 * x * c * c0 * x * c * c0 * x.  [ur(3,a,4,a,c,30,a),rewrite(1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(45),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(47),1(46),1(45),1(44),1(43),1(42),1(41),1(40),1(91),1(90),1(89),1(88),1(87),1(86),1(85),1(84),1(93),1(92),1(91),1(90),1(89),1(88),1(87),1(86))].

given #38 (F,wt=0): 60 d * d * d0 * b0 * c * c0 * b0 * c * c0 * b0 != c * a0 * c * c0 * b0 * c * c0 * b0 * c * c0.  [ur(2,b,22,a,c,30,a)].

given #39 (T,wt=17): 36 a * a0 * x != y | z * b0 * x != y | b = z.  [para(18(a,1),3(a,1))].

given #40 (T,wt=17): 39 c * a0 * x != y | d * z != y | b0 * x = z.  [para(22(a,1),2(a,1))].

given #41 (A,wt=29): 15 x * y * x * y * x * y != z | y * u != z | x * y * x * y * x = u.  [para(4(a,1),2(a,1))].

given #42 (F,wt=0): 61 b * d * d0 * b0 * c * c0 * b0 * c * c0 * b0 != a * a0 * c * c0 * b0 * c * c0 * b0 * c * c0.  [ur(2,b,18,a,c,30,a)].

given #43 (F,wt=0): 64 x * d * d0 * y * c * c0 * y * c * c0 * y != x * y * c * c0 * y * c * c0 * y * c * c0.  [ur(2,b,1,a(flip),c,30,a),rewrite(1(30))].

given #44 (T,wt=17): 40 c * a0 * x != y | z * b0 * x != y | d = z.  [para(22(a,1),3(a,1))].

given #45 (T,wt=17): 48 x * a * a0 != y | x * b * z != y | b0 = z.  [para(5(a,1),9(a,1,2))].

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

given #47 (F,wt=0): 67 c * c0 * d * d0 * c * c0 != c0 * c * c0 * c * c0 * c.  [ur(9,b,4,a,c,31,a)].

given #48 (F,wt=0): 68 x * y * z * d * d0 * u != x * y * z * c * c0 * u.  [ur(9,b,1,a,c,31,a),rewrite(1(7))].

given #49 (T,wt=17): 49 x * c * a0 != y | x * d * z != y | b0 = z.  [para(6(a,1),9(a,1,2))].

given #50 (T,wt=17): 50 x * a * c0 != y | x * b * z != y | d0 = z.  [para(7(a,1),9(a,1,2))].

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

given #52 (F,wt=0): 69 x * y * d * d0 * z != x * y * c * c0 * z.  [ur(9,b,1,a(flip),c,31,a),rewrite(1(12))].

given #53 (F,wt=0): 70 d0 * d * d0 * d * d0 * d != d * d0 * c * c0 * d * d0.  [ur(9,a,4,a,c,31,a),flip(a)].

given #54 (T,wt=17): 77 a * c0 * x != y | b * z != y | d0 * x = z.  [para(26(a,1),2(a,1))].

given #55 (T,wt=17): 78 a * c0 * x != y | z * d0 * x != y | b = z.  [para(26(a,1),3(a,1))].

given #56 (A,wt=23): 21 b0 * a * a0 * a * a0 * b = a * a0 * a * a0 * a * a0.  [para(5(a,1),4(a,1,2,2,2,2)),rewrite(18(9),18(11),18(19),18(21)),flip(a)].

given #57 (F,wt=0): 71 d * d0 * x * y * c * c0 * x * y * c * c0 * x * y != y * c * c0 * x * y * c * c0 * x * y * c * c0 * x.  [ur(3,b,4,a,c,31,a),rewrite(1(13),1(12),1(15),1(14),1(17),1(16),1(31),1(30),1(33),1(32))].

given #58 (F,wt=0): 72 c * c0 * x * y * d * d0 * x * y * d * d0 * x * y != y * d * d0 * x * y * d * d0 * x * y * d * d0 * x.  [ur(3,a,4,a,c,31,a),rewrite(1(13),1(12),1(15),1(14),1(17),1(16),1(31),1(30),1(33),1(32))].

given #59 (T,wt=17): 84 a * a0 != x | a * a0 * y != x | b0 * y = b0.  [para(18(a,1),19(b,1)),flip(c)].

given #60 (T,wt=17): 85 a * a0 != x | a * c0 * y != x | d0 * y = b0.  [para(26(a,1),19(b,1)),flip(c)].

given #61 (A,wt=23): 29 d0 * a * c0 * a * c0 * b = a * c0 * a * c0 * a * c0.  [para(7(a,1),4(a,1,2,2,2,2)),rewrite(26(9),26(11),26(19),26(21)),flip(a)].

given #62 (F,wt=0): 73 c0 * d * d0 * c * c0 * c != c * c0 * c * c0 * c * c0.  [ur(2,b,4,a,c,31,a)].

given #63 (F,wt=0): 74 x * d * d0 * y != x * c * c0 * y.  [ur(2,b,1,a(flip),c,31,a),rewrite(1(10))].

given #64 (T,wt=17): 98 x * a * a0 != y | z * b0 != y | x * b = z.  [para(5(a,1),10(a,1,2))].

given #65 (T,wt=17): 99 x * y * b0 != z | a * a0 != z | x * y = b.  [para(5(a,1),10(b,1))].

given #66 (A,wt=35): 37 b0 * x * a * a0 * x * a * a0 * x * b = a * a0 * x * a * a0 * x * a * a0 * x.  [para(18(a,1),4(a,1,2,2,2,2)),rewrite(1(11),18(12),1(13),18(14),1(24),18(25),1(26),18(27),1(28)),flip(a)].

given #67 (F,wt=0): 75 d * d0 * d * d0 * d * d0 != d0 * c * c0 * d * d0 * d.  [ur(2,a,4,a,c,31,a),flip(a)].

given #68 (F,wt=0): 76 b * d * d0 * d0 * c * c0 * d0 * c * c0 * d0 != a * c0 * c * c0 * d0 * c * c0 * d0 * c * c0.  [ur(2,b,26,a,c,30,a)].

given #69 (T,wt=17): 100 x * c * a0 != y | z * b0 != y | x * d = z.  [para(6(a,1),10(a,1,2))].

given #70 (T,wt=17): 101 x * y * b0 != z | c * a0 != z | x * y = d.  [para(6(a,1),10(b,1))].

given #71 (A,wt=27): 38 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x.  [para(4(a,1),18(a,1,2))].

given #72 (F,wt=0): 86 d0 * x * d * d0 * x * d * d0 * x * d != c * c0 * x * d * d0 * x * d * d0 * x.  [ur(10,a,4,a,c,31,a),rewrite(1(12),1(14),1(13),1(24),1(26),1(28)),flip(a)].

given #73 (F,wt=0): 87 d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x * d != x * c * c0 * x * c * c0 * x * c * c0 * d * d0 * x * c * c0 * x * c * c0 * x * d * d0 * x * c * c0 * x * c * c0 * x.  [ur(10,a,4,a,c,30,a),rewrite(1(42),1(41),1(40),1(39),1(38),1(37),1(36),1(44),1(43),1(42),1(41),1(40),1(39),1(38),1(37),1(84),1(83),1(82),1(81),1(80),1(79),1(78),1(86),1(85),1(84),1(83),1(82),1(81),1(80),1(88),1(87),1(86),1(85),1(84),1(83),1(82)),flip(a)].

given #74 (T,wt=17): 102 x * a * c0 != y | z * d0 != y | x * b = z.  [para(7(a,1),10(a,1,2))].

given #75 (T,wt=17): 103 x * y * d0 != z | a * c0 != z | x * y = b.  [para(7(a,1),10(b,1))].

given #76 (A,wt=35): 41 c * a0 * x * c * a0 * x * c * a0 * x = b0 * x * c * a0 * x * c * a0 * x * d.  [para(22(a,1),4(a,1,2,2,2,2)),rewrite(1(11),22(12),1(13),22(14),1(24),22(25),1(26),22(27),1(28))].

given #77 (F,wt=0): 88 d0 * d * d0 * d * d0 * d != c * c0 * d * d0 * d * d0.  [ur(10,a,4,a,c,8,a),rewrite(1(11)),flip(a)].

given #78 (F,wt=0): 89 c0 * x * c * c0 * x * c * c0 * x * c != d * d0 * x * c * c0 * x * c * c0 * x.  [ur(10,a,4,a,c,31,a(flip)),rewrite(1(12),1(14),1(13),1(24),1(26),1(28)),flip(a)].

given #79 (T,wt=17): 141 c * a0 != x | c * a0 * y != x | b0 * y = b0.  [para(22(a,1),23(b,1)),flip(c)].

given #80 (T,wt=17): 235 a * c0 != x | a * a0 * y != x | b0 * y = d0.  [para(18(a,1),27(b,1)),flip(c)].

given #81 (A,wt=27): 42 d * x * b0 * x * b0 * x * b0 = c * a0 * x * b0 * x * b0 * x.  [para(4(a,1),22(a,1,2))].

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

% Proof 1 at 1.40 (+ 0.01) seconds.
% Length of proof is 16.
% Level of proof is 4.
% Maximum clause weight is 27.
% Given clauses 81.

1 (x * y) * z = x * y * z # label(associativity).  [assumption].
2 x * y != z | x * u != z | y = u # label(left_cancellation_extended).  [assumption].
3 x * y != z | u * y != z | x = u # label(right_cancellation_extended).  [assumption].
4 x * y * x * y * x * y = y * x * y * x * y * x # label("(xy)^3 = (yx)^3").  [assumption].
5 b * b0 = a * a0.  [assumption].
6 d * b0 = c * a0.  [assumption].
7 b * d0 = a * c0.  [assumption].
8 d * d0 != c * c0.  [assumption].
10 x * y * z != u | v * z != u | x * y = v.  [para(1(a,1),3(a,1))].
18 b * b0 * x = a * a0 * x.  [para(5(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
22 d * b0 * x = c * a0 * x.  [para(6(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
26 b * d0 * x = a * c0 * x.  [para(7(a,1),1(a,1,1)),rewrite(1(4)),flip(a)].
38 b * x * b0 * x * b0 * x * b0 = a * a0 * x * b0 * x * b0 * x.  [para(4(a,1),18(a,1,2))].
42 d * x * b0 * x * b0 * x * b0 = c * a0 * x * b0 * x * b0 * x.  [para(4(a,1),22(a,1,2))].
1118 a0 * d0 * b0 * d0 * b0 * d0 = c0 * b0 * d0 * b0 * d0 * b0.  [hyper(2,a,26,a(flip),b,38,a(flip)),flip(a)].
1338 $F.  [ur(10,a,42,a,c,8,a),rewrite(1(13),1118(25)),xx(a)].

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

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

Given=81. Generated=9147. Kept=1337. proofs=1.
Usable=80. Sos=1160. Demods=42. Limbo=13, Disabled=92. Hints=0.
Weight_deleted=826. Literals_deleted=0.
Forward_subsumed=6983. Back_subsumed=81.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=43 (0 lex), Back_demodulated=3. Back_unit_deleted=0.
Demod_attempts=898525. Demod_rewrites=179678.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=3049. Nonunit_bsub_feature_tests=278.
Megabytes=7.75.
User_CPU=1.40, System_CPU=0.01, Wall_clock=2.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 11396 exit (max_proofs) Sat Aug 12 21:01:00 2006