============================== Prover9 ===============================
Prover9 (32) version November-2006, November 2006.
Process 3285 was started by mccune on cleo.thornwood,
Wed Nov 22 11:21:31 2006
The command was "/home/mccune/bin/prover9 -f x3-ring.in".
============================== end of head ===========================

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

% Reading from file x3-ring.in

assign(order,kbo).

formulas(sos).
x + 0 = x.
x + -x = 0.
(x + y) + z = x + (y + z).
x + y = y + x.
x * (y + z) = (x * y) + (x * z).
(x + z) * y = (x * y) + (z * y).
(x * y) * z = x * (y * z).
x * (x * x) = x # label("hypothesis x^3=x").
end_of_list.

formulas(goals).
x * y = y * x # label(commutativity).
end_of_list.

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 x * y = y * x # label(commutativity) # label(goal).  [goal].

============================== end of process non-clausal formulas ===

============================== PROCESS INITIAL CLAUSES ===============

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
x + 0 = x.  [assumption].
x + -x = 0.  [assumption].
(x + y) + z = x + (y + z).  [assumption].
x + y = y + x.  [assumption].
x * (y + z) = (x * y) + (x * z).  [assumption].
(x + y) * z = (x * z) + (y * z).  [assumption].
(x * y) * z = x * (y * z).  [assumption].
x * (x * x) = x # label("hypothesis x^3=x").  [assumption].
c2 * c1 != c1 * c2 # label(commutativity).  [deny(1)].
end_of_list.

formulas(demodulators).
end_of_list.

============================== PREDICATE ELIMINATION =================

No predicates eliminated.

============================== end predicate elimination =============

Auto_denials:
  % copying label commutativity to answer in negative clause

Term ordering decisions:

% Assigning unary symbol - kb_weight 0 and highest precedence (7).
Function symbol KB weights:  0=1. c1=1. c2=1. *=1. +=1. -=0.
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ 0, c1, c2, *, +, - ]).
Skipping inverse_order, because term ordering is KBO.
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).

Auto_process settings:  (no changes).

% Operation + is commutative; C redundancy checks enabled.

============================== end of process initial clauses ========

============================== CLAUSES FOR SEARCH ====================

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
2 x + 0 = x.  [assumption].
3 x + -x = 0.  [assumption].
4 (x + y) + z = x + (y + z).  [assumption].
5 x + y = y + x.  [assumption].
7 (x * y) + (x * z) = x * (y + z).  [copy(6),flip(a)].
9 (x * y) + (z * y) = (x + z) * y.  [copy(8),flip(a)].
10 (x * y) * z = x * (y * z).  [assumption].
11 x * (x * x) = x # label("hypothesis x^3=x").  [assumption].
12 c2 * c1 != c1 * c2 # label(commutativity) # answer(commutativity).  [deny(1)].
end_of_list.

formulas(demodulators).
2 x + 0 = x.  [assumption].
3 x + -x = 0.  [assumption].
4 (x + y) + z = x + (y + z).  [assumption].
5 x + y = y + x.  [assumption].
        % (lex-dep)
7 (x * y) + (x * z) = x * (y + z).  [copy(6),flip(a)].
9 (x * y) + (z * y) = (x + z) * y.  [copy(8),flip(a)].
10 (x * y) * z = x * (y * z).  [assumption].
11 x * (x * x) = x # label("hypothesis x^3=x").  [assumption].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=5): 2 x + 0 = x.  [assumption].

given #2 (I,wt=6): 3 x + -x = 0.  [assumption].

given #3 (I,wt=11): 4 (x + y) + z = x + (y + z).  [assumption].

given #4 (I,wt=7): 5 x + y = y + x.  [assumption].

% Operation + is associative-commutative; CAC redundancy checks enabled.

given #5 (I,wt=13): 7 (x * y) + (x * z) = x * (y + z).  [copy(6),flip(a)].

given #6 (I,wt=13): 9 (x * y) + (z * y) = (x + z) * y.  [copy(8),flip(a)].

given #7 (I,wt=11): 10 (x * y) * z = x * (y * z).  [assumption].

given #8 (I,wt=7): 11 x * (x * x) = x # label("hypothesis x^3=x").  [assumption].

given #9 (I,wt=7): 12 c2 * c1 != c1 * c2 # label(commutativity) # answer(commutativity).  [deny(1)].

given #10 (T,wt=5): 18 0 + x = x.  [para(5(a,1),2(a,1))].

given #11 (A,wt=10): 15 x + (y + -(x + y)) = 0.  [para(4(a,1),3(a,1))].

given #12 (F,wt=4): 31 -0 = 0.  [para(18(a,1),3(a,1))].

given #13 (F,wt=8): 17 -x + (y + x) = y.  [para(3(a,1),4(a,2,2)),rewrite(5(3),2(5))].

given #14 (T,wt=5): 35 --x = x.  [para(3(a,1),17(a,1,2)),rewrite(2(4))].

given #15 (T,wt=8): 20 x + (-x + y) = y.  [back_rewrite(16),rewrite(18(5))].

given #16 (A,wt=11): 19 x + (y + z) = y + (x + z).  [para(5(a,1),4(a,1,1)),rewrite(4(2))].

given #17 (F,wt=8): 42 x + (y + -x) = y.  [para(35(a,1),17(a,1,1))].

given #18 (F,wt=9): 40 -(x + -(y + x)) = y.  [para(15(a,1),17(a,1,2)),rewrite(5(6),18(6))].

given #19 (T,wt=9): 41 x + -(x + y) = -y.  [para(17(a,1),17(a,1,2)),rewrite(5(3))].

given #20 (T,wt=10): 62 -(x + y) = -y + -x.  [para(17(a,1),41(a,1,2,1)),flip(a)].

given #21 (A,wt=17): 21 (x * y) + ((x * z) + u) = (x * (y + z)) + u.  [para(7(a,1),4(a,1,1)),flip(a)].

given #22 (F,wt=11): 23 (x + x) * y = x * (y + y).  [para(9(a,1),7(a,1))].

given #23 (F,wt=9): 70 0 * (x + x) = 0 * x.  [para(2(a,1),23(a,1,1)),flip(a)].

given #24 (T,wt=9): 71 (x + x) * 0 = x * 0.  [para(2(a,1),23(a,2,2))].

given #25 (T,wt=11): 29 x * (x * (x * y)) = x * y.  [para(11(a,1),10(a,1,1)),rewrite(10(3)),flip(a)].

given #26 (A,wt=17): 22 (x * y) + ((z * y) + u) = ((x + z) * y) + u.  [para(9(a,1),4(a,1,1)),flip(a)].

given #27 (F,wt=12): 36 -x + (y + (x + z)) = y + z.  [para(17(a,1),4(a,1,1)),rewrite(4(4)),flip(a)].

given #28 (F,wt=12): 37 -x + (y + (z + x)) = y + z.  [para(4(a,1),17(a,1,2))].

given #29 (T,wt=12): 49 x + (y + (-x + z)) = y + z.  [para(19(a,1),20(a,1,2))].

given #30 (T,wt=12): 51 x + (y + (z + -x)) = y + z.  [para(4(a,1),42(a,1,2))].

given #31 (A,wt=17): 24 (x * (y * z)) + (u * z) = ((x * y) + u) * z.  [para(10(a,1),9(a,1,1))].

given #32 (F,wt=13): 26 x * ((x * x) + y) = x + (x * y).  [para(11(a,1),7(a,1,1)),flip(a)].

given #33 (F,wt=7): 176 x + (x * 0) = x.  [para(2(a,1),26(a,1,2)),rewrite(11(2)),flip(a)].

given #34 (T,wt=5): 208 0 * 0 = 0.  [para(176(a,1),18(a,1)),flip(a)].

given #35 (T,wt=5): 216 x * 0 = 0.  [para(208(a,1),9(a,1,1)),rewrite(214(4),18(3)),flip(a)].

given #36 (A,wt=17): 25 (x * y) + (z * (u * y)) = (x + (z * u)) * y.  [para(10(a,1),9(a,1,2))].

given #37 (F,wt=9): 220 x * (0 * y) = 0 * y.  [para(216(a,1),10(a,1,1)),flip(a)].

given #38 (F,wt=10): 218 x + (x * -(x * x)) = 0.  [back_rewrite(177),rewrite(216(6))].

given #39 (T,wt=9): 253 -(x * -(x * x)) = x.  [para(218(a,1),17(a,1,2)),rewrite(5(6),18(6))].

given #40 (T,wt=9): 266 x * -(x * x) = -x.  [para(253(a,1),35(a,1,1)),flip(a)].

given #41 (A,wt=13): 27 x * (y + (x * x)) = x + (x * y).  [para(11(a,1),7(a,1,2)),rewrite(5(2)),flip(a)].

given #42 (F,wt=9): 279 x * (x * -x) = -x.  [para(266(a,1),29(a,1,2,2)),rewrite(266(6))].

given #43 (F,wt=9): 307 -x * (-x * x) = x.  [para(35(a,1),279(a,1,2,2)),rewrite(35(6))].

given #44 (T,wt=11): 185 x * (x * (x + x)) = x + x.  [para(11(a,1),26(a,2,2)),rewrite(7(3))].

given #45 (T,wt=11): 190 (x + x) * (x * x) = x + x.  [para(26(a,1),23(a,2)),rewrite(11(5))].

given #46 (A,wt=15): 28 x + (y * (x * x)) = (x + y) * (x * x).  [para(11(a,1),9(a,1,1))].

given #47 (F,wt=11): 207 x * (y + (0 * y)) = x * y.  [para(176(a,1),9(a,2,1)),rewrite(10(4),7(5))].

given #48 (F,wt=7): 391 x + (0 * x) = x.  [para(207(a,1),11(a,1,2)),rewrite(390(8),222(5),5(3),18(3),10(2),11(2)),flip(a)].

given #49 (T,wt=6): 395 0 * -x = 0.  [para(391(a,1),20(a,1,2)),rewrite(3(2)),flip(a)].

given #50 (T,wt=5): 410 0 * x = 0.  [para(35(a,1),395(a,1,2))].

given #51 (A,wt=15): 30 x * (y * (x * (y * (x * y)))) = x * y.  [para(11(a,1),10(a,1)),rewrite(10(4)),flip(a)].

given #52 (F,wt=12): 412 x * (y + (-(x * x) * y)) = 0.  [back_rewrite(251),rewrite(410(7))].

given #53 (F,wt=13): 157 ((x * x) + y) * x = x + (y * x).  [para(11(a,1),24(a,1,1)),flip(a)].

given #54 (T,wt=10): 442 x + (-(x * x) * x) = 0.  [para(3(a,1),157(a,1,1)),rewrite(410(2)),flip(a)].

given #55 (T,wt=9): 472 -(-(x * x) * x) = x.  [para(442(a,1),17(a,1,2)),rewrite(5(6),18(6))].

given #56 (A,wt=14): 38 -(x * y) + (x * (z + y)) = x * z.  [para(7(a,1),17(a,1,2))].

given #57 (F,wt=9): 492 -(x * y) = x * -y.  [para(17(a,1),38(a,1,2,2)),rewrite(5(5),60(5))].

given #58 (F,wt=9): 501 -x * -y = x * y.  [para(412(a,1),38(a,1,2)),rewrite(492(2),10(3),305(4),492(3),5(5),18(5))].

given #59 (T,wt=9): 572 -x * y = x * -y.  [para(35(a,1),501(a,1,1)),flip(a)].

given #60 (T,wt=13): 223 (x + (y * y)) * y = y + (x * y).  [para(11(a,1),25(a,1,2)),rewrite(5(2)),flip(a)].

given #61 (A,wt=17): 44 (x * y) + (z + (x * u)) = z + (x * (y + u)).  [para(7(a,1),19(a,1,2)),flip(a)].

given #62 (F,wt=14): 565 (x + x) * (x * -x) = -x + -x.  [para(190(a,1),492(a,1,1)),rewrite(62(2),492(6)),flip(a)].

given #63 (F,wt=14): 590 x * ((y + (x * (x * -y))) * z) = 0.  [back_rewrite(529),rewrite(572(2))].

given #64 (T,wt=12): 683 (x + (y * (y * -x))) * y = 0.  [para(590(a,1),30(a,1,2,2,2)),rewrite(216(10),216(6),216(6)),flip(a)].

given #65 (T,wt=13): 695 (x + (y * (y * -x))) * -y = 0.  [para(35(a,1),683(a,1,1,2,2,2)),rewrite(608(5),492(3),492(2))].

given #66 (A,wt=17): 45 (x * y) + (z + (u * y)) = z + ((x + u) * y).  [para(9(a,1),19(a,1,2)),flip(a)].

given #67 (F,wt=14): 608 (-x + y) * z = (x + -y) * -z.  [para(572(a,1),9(a,1,1)),rewrite(569(4)),flip(a)].

given #68 (F,wt=14): 619 (x + x) * ((x + (x + x)) * -x) = 0.  [back_rewrite(514),rewrite(608(7),62(5),35(3),35(3))].

given #69 (T,wt=13): 791 (x + x) * ((x + (x + x)) * x) = 0.  [para(35(a,1),619(a,1,2,2)),rewrite(608(9),62(7),35(5),35(5),608(8),35(2),492(6),35(5))].

given #70 (T,wt=13): 803 x * ((x + (x + x)) * (x + x)) = 0.  [para(791(a,1),9(a,2)),rewrite(7(9),7(7))].

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

given #72 (F,wt=11): 829 (x + (x + x)) * (x + x) = 0.  [para(803(a,1),157(a,2,2)),rewrite(10(9),816(8),803(7),216(4),18(2),803(5),5(7),18(7)),flip(a)].

given #73 (F,wt=13): 954 (x + (x + x)) * ((x + x) * y) = 0.  [para(829(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].

given #74 (T,wt=11): 975 (x + x) * (x + (x + x)) = 0.  [para(954(a,1),30(a,1,2,2,2)),rewrite(216(6),216(5),216(3)),flip(a)].

given #75 (T,wt=13): 960 (x + (x + x)) * (-x + -x) = 0.  [para(829(a,1),492(a,1,1)),rewrite(31(2),62(5)),flip(a)].

given #76 (A,wt=21): 67 (x * y) + (z + ((x * u) + v)) = z + ((x * (y + u)) + v).  [para(21(a,1),19(a,1,2)),flip(a)].

given #77 (F,wt=13): 971 (x + (x + x)) * (x * (y + y)) = 0.  [para(23(a,1),954(a,1,2))].

given #78 (F,wt=13): 987 (x + x) * ((x + (x + x)) * y) = 0.  [para(975(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].

given #79 (T,wt=13): 1054 x + (x + (x + (x + (x + x)))) = 0.  [para(971(a,1),28(a,2)),rewrite(19(4),5(3),967(8),999(5),19(5),19(4),19(3),5(2))].

given #80 (T,wt=11): 1079 (x + (x + x)) * (y + y) = 0.  [para(22(a,1),1054(a,1,2,2)),rewrite(7(7),75(7),21(7),9(6))].

given #81 (A,wt=17): 72 (x + (y + (x + y))) * z = (x + y) * (z + z).  [para(4(a,1),23(a,1,1))].

given #82 (F,wt=13): 1083 x + (x + (x + x)) = -x + -x.  [back_rewrite(309),rewrite(1082(8),1058(4))].

given #83 (F,wt=13): 1101 (x + (x + x)) * (y * (z + z)) = 0.  [para(7(a,1),1079(a,1,2))].

given #84 (T,wt=13): 1104 (x + (x + x)) * ((y + y) * z) = 0.  [para(9(a,1),1079(a,1,2))].

given #85 (T,wt=11): 1270 (x + x) * (y + (y + y)) = 0.  [para(1104(a,1),30(a,1,2,2,2)),rewrite(216(6),216(5),216(3)),flip(a)].

given #86 (A,wt=17): 73 (x + x) * (y + z) = x * (y + (z + (y + z))).  [para(4(a,1),23(a,2,2))].

given #87 (F,wt=13): 1277 (x + x) * (y * (z + (z + z))) = 0.  [para(7(a,1),1270(a,1,2,2)),rewrite(7(5))].

given #88 (F,wt=13): 1280 (x + x) * ((y + (y + y)) * z) = 0.  [para(9(a,1),1270(a,1,2,2)),rewrite(9(5))].

given #89 (T,wt=14): 692 (x * y) + (y * (y * (x * -y))) = 0.  [para(683(a,1),9(a,2)),rewrite(10(5),10(4),572(3))].

given #90 (T,wt=11): 1405 x * (x * (y * x)) = y * x.  [para(692(a,1),17(a,1,2)),rewrite(492(5),492(4),492(3),35(2),5(5),18(5))].

given #91 (A,wt=19): 74 (x * (y + y)) + ((x + x) * z) = (x + x) * (y + z).  [para(23(a,1),7(a,1,1))].

given #92 (F,wt=13): 1455 x * (x * (y * -x)) = y * -x.  [para(1405(a,1),492(a,1,1)),rewrite(492(2),492(5),492(4)),flip(a)].

given #93 (F,wt=14): 693 (x + (y * (y * -x))) * (y * z) = 0.  [para(683(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].

given #94 (T,wt=14): 706 (x + (y * (y + (y * -x)))) * y = y.  [para(683(a,1),157(a,2,2)),rewrite(44(6),2(8))].

given #95 (T,wt=14): 765 (x + -y) * -z = (y + -x) * z.  [para(5(a,1),608(a,1,1)),flip(a)].

given #96 (A,wt=19): 75 ((x + x) * y) + (x * (z + z)) = (x + x) * (y + z).  [para(23(a,1),7(a,1,2))].

given #97 (F,wt=14): 1231 -x + (-x + -x) = x + (x + x).  [para(1083(a,1),20(a,1,2)),rewrite(35(2),35(2)),flip(a)].

given #98 (F,wt=14): 1456 x * (y * (z + (x * (x * -z)))) = 0.  [para(1405(a,1),590(a,1,2))].

given #99 (T,wt=14): 1532 x * (y * (-z + (x * (x * z)))) = 0.  [para(1455(a,1),590(a,1,2)),rewrite(62(5),492(4),492(3),35(2),5(4))].

given #100 (T,wt=14): 1569 (x + (y * (y * -x))) * (z * y) = 0.  [para(1405(a,1),693(a,1,2))].

given #101 (A,wt=17): 76 x * (y + (y + z)) = ((x + x) * y) + (x * z).  [para(23(a,2),7(a,1,1)),rewrite(4(6)),flip(a)].

given #102 (F,wt=15): 78 x * ((y + y) * z) = x * (y * (z + z)).  [para(7(a,1),23(a,1,1)),rewrite(10(3),10(6))].

given #103 (F,wt=15): 79 (x + x) * (y * z) = x * (y * (z + z)).  [para(7(a,1),23(a,2,2))].

given #104 (T,wt=15): 84 (x + x) * (y * z) = x * ((y + y) * z).  [para(9(a,1),23(a,2,2))].

given #105 (T,wt=15): 93 ((x + x) * y) + z = (x * (y + y)) + z.  [para(23(a,2),21(a,2,1)),rewrite(21(4)),flip(a)].

given #106 (A,wt=17): 77 x * (y + (z + z)) = (x * y) + ((x + x) * z).  [para(23(a,2),7(a,1,2)),flip(a)].

given #107 (F,wt=15): 108 x * ((x * (x * y)) + z) = x * (y + z).  [para(29(a,1),7(a,1,1)),rewrite(7(3)),flip(a)].

given #108 (F,wt=15): 109 x * (y + (x * (x * z))) = x * (y + z).  [para(29(a,1),7(a,1,2)),rewrite(7(3)),flip(a)].

given #109 (T,wt=15): 153 (x + (x * y)) * z = x * (z + (y * z)).  [para(24(a,1),7(a,1)),rewrite(5(2),5(5))].

given #110 (T,wt=15): 179 x + (x * (x * y)) = x * (x * (x + y)).  [para(7(a,1),26(a,1,2)),flip(a)].

given #111 (A,wt=17): 80 (x + (x + y)) * z = (x * (z + z)) + (y * z).  [para(23(a,1),9(a,1,1)),rewrite(4(6)),flip(a)].

given #112 (F,wt=15): 181 x + (x * (y * x)) = x * ((x + y) * x).  [para(9(a,1),26(a,1,2)),flip(a)].

given #113 (F,wt=15): 301 x * ((x * -x) + y) = -x + (x * y).  [para(279(a,1),7(a,1,1)),flip(a)].

given #114 (T,wt=15): 302 x * (y + (x * -x)) = -x + (x * y).  [para(279(a,1),7(a,1,2)),rewrite(5(3)),flip(a)].

given #115 (T,wt=15): 334 x * (x * ((x + x) * y)) = (x + x) * y.  [para(185(a,1),10(a,1,1)),rewrite(10(5)),flip(a)].

given #116 (A,wt=17): 81 (x + (y + y)) * z = (x * z) + (y * (z + z)).  [para(23(a,1),9(a,1,2)),flip(a)].

given #117 (F,wt=15): 342 x * (x * (x + (x + x))) = x + (x + x).  [para(185(a,1),26(a,2,2)),rewrite(7(4))].

given #118 (F,wt=15): 349 (x + x) * (x * (x * y)) = (x + x) * y.  [para(190(a,1),10(a,1,1)),rewrite(10(5)),flip(a)].

given #119 (T,wt=15): 386 (x + (x + x)) * (x * x) = x + (x + x).  [para(190(a,1),28(a,1,2)),flip(a)].

given #120 (T,wt=15): 564 x * (x * (-x + -x)) = -x + -x.  [para(185(a,1),492(a,1,1)),rewrite(62(2),492(6),62(5)),flip(a)].

given #121 (A,wt=19): 82 ((x + x) * y) + (z * (y + y)) = (x + z) * (y + y).  [para(23(a,2),9(a,1,1))].

given #122 (F,wt=15): 614 (x * y) + (z * -y) = (x + -z) * y.  [back_rewrite(568),rewrite(608(8),35(8))].

given #123 (F,wt=15): 621 (x + y) * ((x + y) * (y + x)) = y + x.  [back_rewrite(321),rewrite(608(8),35(5),62(6),608(9),35(2),492(7),62(6),35(4),35(4))].

given #124 (T,wt=15): 643 x + ((y + y) * z) = x + (y * (z + z)).  [para(23(a,2),44(a,2,2)),rewrite(44(4)),flip(a)].

given #125 (T,wt=15): 957 x * ((x + (x + x)) * x) = x + (x + x).  [para(829(a,1),26(a,2,2)),rewrite(947(7),5(7),4(7),947(8),801(6),5(8),18(8))].

given #126 (A,wt=19): 83 (x * (y + y)) + ((z + z) * y) = (x + z) * (y + y).  [para(23(a,2),9(a,1,2))].

given #127 (F,wt=15): 1087 (x + x) * (y + (x * ((x + x) * y))) = 0.  [back_rewrite(616),rewrite(1083(4),608(6),35(3),35(4))].

given #128 (F,wt=15): 1098 (x + (x + x)) * (y + (z + (y + z))) = 0.  [para(4(a,1),1079(a,1,2))].

given #129 (T,wt=15): 1234 (x + x) * (y + y) = x * (-y + -y).  [para(1083(a,1),22(a,1)),rewrite(492(2),492(4),7(5),7(9),75(9)),flip(a)].

given #130 (T,wt=15): 1240 (x + (y * (y * (x + x)))) * (y + y) = 0.  [back_rewrite(698),rewrite(1234(5),35(2),35(2))].

given #131 (A,wt=23): 88 (x * (y + y)) + (((x + x) * z) + u) = ((x + x) * (y + z)) + u.  [para(23(a,1),21(a,1,1))].

given #132 (F,wt=15): 1251 (x + (x + x)) * (y * (z * (u + u))) = 0.  [para(7(a,1),1101(a,1,2,2))].

given #133 (F,wt=15): 1254 (x + (x + x)) * (y * ((z + z) * u)) = 0.  [para(9(a,1),1101(a,1,2,2))].

given #134 (T,wt=15): 1273 (x + (y + (x + y))) * (z + (z + z)) = 0.  [para(4(a,1),1270(a,1,1))].

given #135 (T,wt=15): 1384 (x + x) * (y * (z * (u + (u + u)))) = 0.  [para(7(a,1),1277(a,1,2,2,2)),rewrite(7(5))].

given #136 (A,wt=23): 89 ((x + x) * y) + ((x * (z + z)) + u) = ((x + x) * (y + z)) + u.  [para(23(a,1),21(a,1,2,1))].

given #137 (F,wt=15): 1387 (x + x) * (y * ((z + (z + z)) * u)) = 0.  [para(9(a,1),1277(a,1,2,2,2)),rewrite(9(5))].

given #138 (F,wt=15): 1409 (x + ((y + y) * (y * x))) * (y + y) = 0.  [para(23(a,1),692(a,1,2,2)),rewrite(62(5),62(9),7(12),19(10),5(9),1231(9),19(7),19(6),5(5),3(5),2(5),221(8))].

given #139 (T,wt=15): 1410 (x + (y * ((y + y) * x))) * (y + y) = 0.  [para(23(a,1),692(a,1,2)),rewrite(62(5),62(11),7(15),7(12),19(10),5(9),1231(9),19(7),19(6),5(5),3(5),2(5),221(8))].

given #140 (T,wt=15): 1437 x * (x * (y * (x * z))) = y * (x * z).  [para(1405(a,1),10(a,1,1)),rewrite(10(2),10(5),10(4)),flip(a)].

given #141 (A,wt=21): 90 ((x + x) * y) + ((x * z) + u) = (x * (y + (y + z))) + u.  [para(23(a,2),21(a,1,1)),rewrite(4(7))].

given #142 (F,wt=15): 1439 x * (x * (y * (z * x))) = y * (z * x).  [para(10(a,1),1405(a,1,2,2)),rewrite(10(6))].

given #143 (F,wt=15): 1448 x * (x * (x + (y * x))) = x + (y * x).  [para(1405(a,1),26(a,2,2)),rewrite(7(4))].

given #144 (T,wt=15): 1453 x * (y * (x * (y * (y * x)))) = y * x.  [para(30(a,1),1405(a,1,2,2)),rewrite(10(10),10(9),10(8),10(7),30(9),10(7),10(6),10(5),10(4),1405(3),30(10))].

given #145 (T,wt=15): 1570 (x + (y * (y * -x))) * (z * -y) = 0.  [para(1455(a,1),693(a,1,2))].

given #146 (A,wt=21): 91 (x * (y + (z + z))) + u = (x * y) + (((x + x) * z) + u).  [para(23(a,2),21(a,1,2,1)),flip(a)].

given #147 (F,wt=15): 1658 (x + (y * -y)) * y = -y + (x * y).  [para(765(a,1),157(a,1)),rewrite(572(3),35(2),492(2),572(8),35(7))].

given #148 (F,wt=15): 1750 (x + (x + x)) * y = x * (y + (y + y)).  [para(9(a,1),1231(a,2,2)),rewrite(492(2),492(4),492(6),7(7),7(7),1231(5),9(7)),flip(a)].

given #149 (T,wt=15): 2086 x * (x * (y * (x + x))) = y * (x + x).  [back_rewrite(1440),rewrite(2001(6),35(2),35(2))].

given #150 (T,wt=15): 2317 (x * (y + y)) + z = z + ((x + x) * y).  [para(93(a,1),5(a,1))].

given #151 (A,wt=21): 92 ((x + x) * (y + z)) + u = (x * (y + (z + (y + z)))) + u.  [para(23(a,1),21(a,2,1)),rewrite(21(6),19(7),5(6))].

given #152 (F,wt=15): 2318 ((x + x) * y) + z = z + (x * (y + y)).  [para(93(a,2),5(a,1))].

given #153 (F,wt=15): 2375 x * ((x + x) * (x * y)) = (x + x) * y.  [back_rewrite(2222),rewrite(2368(6),35(3))].

given #154 (T,wt=15): 2908 x * ((x + (x * y)) * x) = x + (y * x).  [para(179(a,1),157(a,1,1)),rewrite(10(5),26(4),10(5),2602(4),26(3),10(4),10(7),10(8),29(7),10(7),10(6),1405(7))].

given #155 (T,wt=15): 3407 x * ((x + x) * (y * x)) = y * (x + x).  [back_rewrite(2177),rewrite(3395(6),492(4),35(3))].

given #156 (A,wt=19): 111 x * (y * (x * (y * (x * (y * z))))) = x * (y * z).  [para(29(a,1),10(a,1)),rewrite(10(2),10(5),10(6)),flip(a)].

given #157 (F,wt=15): 3714 (x + (x + x)) * (y + (x * (x * y))) = 0.  [para(386(a,1),153(a,1,1,2)),rewrite(19(5),5(4),19(4),19(3),5(2),1083(3),42(4),3(2),410(2),10(5)),flip(a)].

given #158 (F,wt=15): 3968 (x + y) * ((y + x) * (x + y)) = x + y.  [para(5(a,1),621(a,1,1))].

given #159 (T,wt=15): 3969 (x + y) * ((y + x) * (y + x)) = y + x.  [para(5(a,1),621(a,1,2,1))].

given #160 (T,wt=15): 4226 (x + (x + x)) * (y + (z + (z + y))) = 0.  [para(5(a,1),1098(a,1,2,2,2))].

given #161 (A,wt=19): 117 ((x + y) * z) + (y * u) = (x * z) + (y * (z + u)).  [para(7(a,1),22(a,1,2)),flip(a)].

given #162 (F,wt=15): 4423 (x + (y + (y + x))) * (z + (z + z)) = 0.  [para(5(a,1),1273(a,1,1,2,2))].

given #163 (F,wt=15): 4628 x * (y * (x * (y * x))) = y * (y * x).  [para(30(a,1),1437(a,1,2)),flip(a)].

given #164 (T,wt=15): 5170 x * (y * (x * (x * y))) = y * (x * y).  [para(1405(a,1),1453(a,1,2,2,2)),rewrite(10(4),4628(5),10(4))].

given #165 (T,wt=15): 6321 (x + x) * (x * (y * x)) = y * (x + x).  [para(1405(a,1),2375(a,1,2,2)),rewrite(3407(4)),flip(a)].

given #166 (A,wt=21): 118 (x * (y * z)) + ((u * z) + v) = (((x * y) + u) * z) + v.  [para(10(a,1),22(a,1,1))].

given #167 (F,wt=15): 7467 x * (y * (y * x)) = y * (x * (y * x)).  [para(4628(a,1),1437(a,1,2))].

given #168 (F,wt=16): 135 -x + (y + (z + (x + u))) = y + (z + u).  [para(4(a,1),36(a,1,2)),rewrite(4(7))].

given #169 (T,wt=16): 140 -x + (y + (z + (u + x))) = y + (z + u).  [para(4(a,1),37(a,1,2,2))].

given #170 (T,wt=16): 143 x + (y + (z + (-x + u))) = y + (z + u).  [para(4(a,1),49(a,1,2)),rewrite(4(7))].

given #171 (A,wt=21): 119 (x * y) + ((z * (u * y)) + v) = ((x + (z * u)) * y) + v.  [para(10(a,1),22(a,1,2,1))].

given #172 (F,wt=16): 148 x + (y + (z + (u + -x))) = y + (z + u).  [para(4(a,1),51(a,1,2,2))].

given #173 (F,wt=16): 313 ((x * x) + y) * -x = -x + (y * -x).  [para(279(a,1),24(a,1,1)),flip(a)].

given #174 (T,wt=16): 316 (x + (y * y)) * -y = -y + (x * -y).  [para(279(a,1),25(a,1,2)),rewrite(5(4)),flip(a)].

given #175 (T,wt=16): 569 (x * -y) + (z * y) = (x + -z) * -y.  [para(501(a,1),9(a,1,2))].

given #176 (A,wt=19): 120 ((x + y) * (x * x)) + z = x + ((y * (x * x)) + z).  [para(11(a,1),22(a,1,1)),flip(a)].

given #177 (F,wt=16): 690 (x + ((y * (y * -x)) + z)) * y = z * y.  [para(683(a,1),9(a,1,1)),rewrite(18(3),4(6)),flip(a)].

given #178 (F,wt=15): 9008 ((x * (x * y)) + z) * x = (y + z) * x.  [para(20(a,1),690(a,1,1,2)),rewrite(492(6),492(5),35(4)),flip(a)].

given #179 (T,wt=15): 9010 (x + (y * (y * z))) * y = (z + x) * y.  [para(42(a,1),690(a,1,1,2)),rewrite(492(6),492(5),35(4)),flip(a)].

given #180 (T,wt=16): 778 (x + (y * -y)) * -y = y + (x * -y).  [para(608(a,1),223(a,1)),rewrite(492(2),572(7))].

given #181 (A,wt=19): 121 ((x + y) * (y * y)) + z = y + ((x * (y * y)) + z).  [para(11(a,1),22(a,1,2,1)),rewrite(19(4)),flip(a)].

given #182 (F,wt=16): 1551 (x + (y * (y * -x))) * ((y + y) * z) = 0.  [para(23(a,2),693(a,1,2))].

given #183 (F,wt=16): 1749 (x + (x + x)) * -y = (x + (x + x)) * y.  [para(1231(a,1),9(a,2,1)),rewrite(572(2),608(6),35(4),9(6))].

given #184 (T,wt=16): 1763 x * (y * ((z + (x * (x * -z))) * u)) = 0.  [para(1456(a,1),10(a,1,1)),rewrite(410(2),10(7)),flip(a)].

given #185 (T,wt=16): 1765 x * (y * (z * (u + (x * (x * -u))))) = 0.  [para(10(a,1),1456(a,1,2))].

given #186 (A,wt=21): 123 (x * y) + (z + ((u * y) + v)) = z + (((x + u) * y) + v).  [para(22(a,1),19(a,1,2)),flip(a)].

given #187 (F,wt=16): 1771 x * (y + (y * (x * (x * (y * -y))))) = 0.  [para(26(a,1),1456(a,1,2)),rewrite(492(2))].

given #188 (F,wt=14): 10288 (x * y) + (y * (x * (y * -y))) = 0.  [para(1771(a,1),7(a,2)),rewrite(7509(7))].

given #189 (T,wt=11): 10363 x * (y * (x * x)) = y * x.  [para(10288(a,1),17(a,1,2)),rewrite(492(5),492(4),492(3),35(2),5(5),18(5))].

given #190 (T,wt=11): 10506 x * (y * y) = y * (x * y).  [para(10363(a,1),1437(a,1,2)),flip(a)].

given #191 (A,wt=23): 126 (x * (y + z)) + ((u * z) + v) = (x * y) + (((x + u) * z) + v).  [para(22(a,1),21(a,1,2)),flip(a)].

given #192 (F,wt=12): 10372 (x + (y * (x * -y))) * y = 0.  [para(157(a,1),10288(a,1,1)),rewrite(173(7),4(8),612(7),62(3),492(2),5(4),652(8),20(5))].

given #193 (F,wt=12): 11565 ((x * y) + (y * -x)) * x = 0.  [para(7(a,1),10372(a,1,1)),rewrite(10(3),1512(5))].

given #194 (T,wt=12): 11736 ((x * y) + (y * -x)) * y = 0.  [para(117(a,1),11565(a,1,1)),rewrite(62(3),20(5),11650(6))].

given #195 (T,wt=12): 11750 (x + (x * (y * -y))) * y = 0.  [para(11565(a,1),10363(a,1,2)),rewrite(216(2),10(3),492(5),9008(8)),flip(a)].

given #196 (A,wt=23): 127 ((x + y) * z) + ((y * u) + v) = (x * z) + ((y * (z + u)) + v).  [para(21(a,1),22(a,1,2)),flip(a)].

given #197 (F,wt=13): 10427 (x + (y * (x * -y))) * -y = 0.  [para(313(a,1),10288(a,1,1)),rewrite(35(10),572(9),173(10),572(10),492(9),35(8),4(9),580(8),62(4),492(3),5(5),8538(10),20(5))].

given #198 (F,wt=13): 10451 x * (y * (x * -x)) = y * -x.  [para(10363(a,1),492(a,1,1)),rewrite(492(2),492(5),492(4)),flip(a)].

given #199 (T,wt=13): 10851 x * (y * -y) = y * (x * -y).  [para(10506(a,1),492(a,1,1)),rewrite(492(3),492(2),492(5)),flip(a)].

given #200 (T,wt=13): 11851 (x + (x * (y * -y))) * -y = 0.  [para(9(a,1),11750(a,1,1)),rewrite(10(8),10(7),572(6),279(7))].

given #201 (A,wt=21): 128 ((x + (x + y)) * z) + u = (x * (z + z)) + ((y * z) + u).  [para(23(a,1),22(a,1,1)),rewrite(4(7)),flip(a)].

given #202 (F,wt=14): 11568 (x + (y * (x * -y))) * (y * z) = 0.  [para(10372(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].

given #203 (F,wt=10): 13251 (x * y) + (y * -x) = 0.  [para(11568(a,1),1405(a,1,2)),rewrite(216(6),1512(6)),flip(a)].

% Operation * is commutative; C redundancy checks enabled.

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

% Proof 1 at 4.33 (+ 0.04) seconds: commutativity.
% Length of proof is 78.
% Level of proof is 26.
% Maximum clause weight is 20.
% Given clauses 203.

1 x * y = y * x # label(commutativity) # label(goal).  [goal].
2 x + 0 = x.  [assumption].
3 x + -x = 0.  [assumption].
4 (x + y) + z = x + (y + z).  [assumption].
5 x + y = y + x.  [assumption].
6 x * (y + z) = (x * y) + (x * z).  [assumption].
7 (x * y) + (x * z) = x * (y + z).  [copy(6),flip(a)].
8 (x + y) * z = (x * z) + (y * z).  [assumption].
9 (x * y) + (z * y) = (x + z) * y.  [copy(8),flip(a)].
10 (x * y) * z = x * (y * z).  [assumption].
11 x * (x * x) = x # label("hypothesis x^3=x").  [assumption].
12 c2 * c1 != c1 * c2 # label(commutativity) # answer(commutativity).  [deny(1)].
16 x + (-x + y) = 0 + y.  [para(3(a,1),4(a,1,1)),flip(a)].
17 -x + (y + x) = y.  [para(3(a,1),4(a,2,2)),rewrite(5(3),2(5))].
18 0 + x = x.  [para(5(a,1),2(a,1))].
19 x + (y + z) = y + (x + z).  [para(5(a,1),4(a,1,1)),rewrite(4(2))].
20 x + (-x + y) = y.  [back_rewrite(16),rewrite(18(5))].
24 (x * (y * z)) + (u * z) = ((x * y) + u) * z.  [para(10(a,1),9(a,1,1))].
25 (x * y) + (z * (u * y)) = (x + (z * u)) * y.  [para(10(a,1),9(a,1,2))].
26 x * ((x * x) + y) = x + (x * y).  [para(11(a,1),7(a,1,1)),flip(a)].
29 x * (x * (x * y)) = x * y.  [para(11(a,1),10(a,1,1)),rewrite(10(3)),flip(a)].
30 x * (y * (x * (y * (x * y)))) = x * y.  [para(11(a,1),10(a,1)),rewrite(10(4)),flip(a)].
35 --x = x.  [para(3(a,1),17(a,1,2)),rewrite(2(4))].
36 -x + (y + (x + z)) = y + z.  [para(17(a,1),4(a,1,1)),rewrite(4(4)),flip(a)].
38 -(x * y) + (x * (z + y)) = x * z.  [para(7(a,1),17(a,1,2))].
41 x + -(x + y) = -y.  [para(17(a,1),17(a,1,2)),rewrite(5(3))].
44 (x * y) + (z + (x * u)) = z + (x * (y + u)).  [para(7(a,1),19(a,1,2)),flip(a)].
60 (x * y) + -(x * (y + z)) = -(x * z).  [para(7(a,1),41(a,1,2,1))].
62 -(x + y) = -y + -x.  [para(17(a,1),41(a,1,2,1)),flip(a)].
157 ((x * x) + y) * x = x + (y * x).  [para(11(a,1),24(a,1,1)),flip(a)].
173 ((x * x) + y) * (x * z) = (x + (y * x)) * z.  [para(29(a,1),24(a,1,1)),rewrite(25(4)),flip(a)].
176 x + (x * 0) = x.  [para(2(a,1),26(a,1,2)),rewrite(11(2)),flip(a)].
177 x + (x * -(x * x)) = x * 0.  [para(3(a,1),26(a,1,2)),flip(a)].
207 x * (y + (0 * y)) = x * y.  [para(176(a,1),9(a,2,1)),rewrite(10(4),7(5))].
208 0 * 0 = 0.  [para(176(a,1),18(a,1)),flip(a)].
214 x + (y * 0) = x.  [para(176(a,1),36(a,1,2,2)),rewrite(17(3)),flip(a)].
216 x * 0 = 0.  [para(208(a,1),9(a,1,1)),rewrite(214(4),18(3)),flip(a)].
218 x + (x * -(x * x)) = 0.  [back_rewrite(177),rewrite(216(6))].
222 (x + (y * z)) * (z * z) = ((x * z) + y) * z.  [para(11(a,1),25(a,1,2,2)),rewrite(24(4)),flip(a)].
251 x * (y + (-(x * x) * y)) = 0 * y.  [para(218(a,1),9(a,2,1)),rewrite(10(5),7(6))].
253 -(x * -(x * x)) = x.  [para(218(a,1),17(a,1,2)),rewrite(5(6),18(6))].
266 x * -(x * x) = -x.  [para(253(a,1),35(a,1,1)),flip(a)].
279 x * (x * -x) = -x.  [para(266(a,1),29(a,1,2,2)),rewrite(266(6))].
305 x * (x * (-x * y)) = -x * y.  [para(279(a,1),10(a,1,1)),rewrite(10(5)),flip(a)].
390 x * ((y + (0 * y)) * z) = x * (y * z).  [para(207(a,1),10(a,1,1)),rewrite(10(2)),flip(a)].
391 x + (0 * x) = x.  [para(207(a,1),11(a,1,2)),rewrite(390(8),222(5),5(3),18(3),10(2),11(2)),flip(a)].
395 0 * -x = 0.  [para(391(a,1),20(a,1,2)),rewrite(3(2)),flip(a)].
410 0 * x = 0.  [para(35(a,1),395(a,1,2))].
412 x * (y + (-(x * x) * y)) = 0.  [back_rewrite(251),rewrite(410(7))].
431 x * ((y + (-(x * x) * y)) * z) = 0.  [para(412(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].
492 -(x * y) = x * -y.  [para(17(a,1),38(a,1,2,2)),rewrite(5(5),60(5))].
501 -x * -y = x * y.  [para(412(a,1),38(a,1,2)),rewrite(492(2),10(3),305(4),492(3),5(5),18(5))].
529 x * ((y + (x * (-x * y))) * z) = 0.  [back_rewrite(431),rewrite(492(2),10(3))].
569 (x * -y) + (z * y) = (x + -z) * -y.  [para(501(a,1),9(a,1,2))].
572 -x * y = x * -y.  [para(35(a,1),501(a,1,1)),flip(a)].
579 (x * y) + (z * (u * -y)) = (-x + (z * u)) * -y.  [para(501(a,1),25(a,1,1))].
590 x * ((y + (x * (x * -y))) * z) = 0.  [back_rewrite(529),rewrite(572(2))].
608 (-x + y) * z = (x + -y) * -z.  [para(572(a,1),9(a,1,1)),rewrite(569(4)),flip(a)].
612 (x * y) + (z * (u * -y)) = (x + (z * -u)) * y.  [back_rewrite(579),rewrite(608(10),492(7),35(10))].
652 x + ((y + (x * z)) * x) = (y + (x * (x + z))) * x.  [para(44(a,1),157(a,1,1)),flip(a)].
683 (x + (y * (y * -x))) * y = 0.  [para(590(a,1),30(a,1,2,2,2)),rewrite(216(10),216(6),216(6)),flip(a)].
692 (x * y) + (y * (y * (x * -y))) = 0.  [para(683(a,1),9(a,2)),rewrite(10(5),10(4),572(3))].
1405 x * (x * (y * x)) = y * x.  [para(692(a,1),17(a,1,2)),rewrite(492(5),492(4),492(3),35(2),5(5),18(5))].
1437 x * (x * (y * (x * z))) = y * (x * z).  [para(1405(a,1),10(a,1,1)),rewrite(10(2),10(5),10(4)),flip(a)].
1453 x * (y * (x * (y * (y * x)))) = y * x.  [para(30(a,1),1405(a,1,2,2)),rewrite(10(10),10(9),10(8),10(7),30(9),10(7),10(6),10(5),10(4),1405(3),30(10))].
1455 x * (x * (y * -x)) = y * -x.  [para(1405(a,1),492(a,1,1)),rewrite(492(2),492(5),492(4)),flip(a)].
1456 x * (y * (z + (x * (x * -z)))) = 0.  [para(1405(a,1),590(a,1,2))].
1512 x * (y + (x * (z * -x))) = (x * y) + (z * -x).  [para(1455(a,1),7(a,1,2)),flip(a)].
1771 x * (y + (y * (x * (x * (y * -y))))) = 0.  [para(26(a,1),1456(a,1,2)),rewrite(492(2))].
4628 x * (y * (x * (y * x))) = y * (y * x).  [para(30(a,1),1437(a,1,2)),flip(a)].
5170 x * (y * (x * (x * y))) = y * (x * y).  [para(1405(a,1),1453(a,1,2,2,2)),rewrite(10(4),4628(5),10(4))].
7509 x * (y * (x * (x * (y * z)))) = y * (x * (y * z)).  [para(5170(a,1),10(a,1,1)),rewrite(10(3),10(2),10(7),10(6),10(5)),flip(a)].
10288 (x * y) + (y * (x * (y * -y))) = 0.  [para(1771(a,1),7(a,2)),rewrite(7509(7))].
10372 (x + (y * (x * -y))) * y = 0.  [para(157(a,1),10288(a,1,1)),rewrite(173(7),4(8),612(7),62(3),492(2),5(4),652(8),20(5))].
11568 (x + (y * (x * -y))) * (y * z) = 0.  [para(10372(a,1),10(a,1,1)),rewrite(410(2)),flip(a)].
13251 (x * y) + (y * -x) = 0.  [para(11568(a,1),1405(a,1,2)),rewrite(216(6),1512(6)),flip(a)].
13324 x * y = y * x.  [para(13251(a,1),17(a,1,2)),rewrite(492(3),35(2),5(3),18(3))].
13325 $F # answer(commutativity).  [resolve(13324,a,12,a)].

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

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

Given=203. Generated=46019. Kept=13321. proofs=1.
Usable=141. Sos=10171. Demods=5945. Limbo=5, Disabled=3012. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=32698. Back_subsumed=243.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=8351 (4 lex), Back_demodulated=2760. Back_unit_deleted=0.
Demod_attempts=1138001. Demod_rewrites=238935.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=17.09.
User_CPU=4.33, System_CPU=0.04, Wall_clock=5.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 3285 exit (max_proofs) Wed Nov 22 11:21:36 2006