============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13018 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:19 2006
The command was "/home/mccune/bin/prover9 -t 10 -f qg2.in".
============================== end of head ===========================

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

% Reading from file qg2.in


formulas(sos).
(all x all y all z (x * y = x * z -> y = z)).
(all x all y all z (y * x = z * x -> y = z)).
end_of_list.

clauses(sos).
x * (y * (y * x)) = y * x.
end_of_list.

clauses(goals).
x * (x * y) = y * x.
end_of_list.

% From the command line: assign(max_seconds, 10).

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

============================== PROCESS GOALS =========================

% Each goal clause was negated; the result (to be placed in sos):

clauses(negated_goals).
c2 * c1 != c1 * (c1 * c2).
end_of_list.

============================== end of process goals ==================

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 x * (y * (y * x)) = y * x.  [input].
2 x * y != x * z | y = z.  [clausify].
3 x * y != z * y | x = z.  [clausify].
4 c2 * c1 != c1 * (c1 * c2).  [clausify].
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([ c1, c2, * ]).
After inverse_order: Function symbol precedence:  lex([ c1, c2, * ]).
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).
5 x * (y * (y * x)) = y * x.  [input].
6 x * y != x * z | y = z.  [clausify].
7 x * y != z * y | x = z.  [clausify].
8 c2 * c1 != c1 * (c1 * c2).  [clausify].
end_of_list.

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

given #2 (I,wt=10): 6 x * y != x * z | y = z.  [clausify].

given #3 (I,wt=10): 7 x * y != z * y | x = z.  [clausify].

given #4 (I,wt=9): 8 c2 * c1 != c1 * (c1 * c2).  [clausify].

given #5 (T,wt=7): 11 x * (x * x) = x.  [hyper(6,a,5,a)].

given #6 (A,wt=15): 9 (x * (x * y)) * (y * (x * y)) = x * y.  [para(5(a,1),5(a,1,2,2)),demod(5(8))].

given #7 (F,wt=13): 16 (c2 * c1) * x != (c1 * (c1 * c2)) * x.  [ur(7,b,8,a)].

given #8 (F,wt=13): 17 x * (c2 * c1) != x * (c1 * (c1 * c2)).  [ur(6,b,8,a)].

given #9 (T,wt=9): 13 (x * x) * (x * x) = x.  [back_demod(10),demod(11(5))].

given #10 (T,wt=9): 38 (x * x) * x = x * x.  [para(13(a,1),11(a,1,2))].

given #11 (A,wt=14): 12 x * y != z * x | z * (z * x) = y.  [para(5(a,1),6(a,1)),flip(a)].

given #12 (F,wt=9): 35 c2 * (c2 * c1) != c1 * c2.  [para(5(a,1),17(a,2))].

given #13 (F,wt=13): 32 (c2 * c1) * (c2 * (c1 * c2)) != c1 * c2.  [para(9(a,1),16(a,2))].

given #14 (T,wt=5): 39 x * x = x.  [hyper(7,a,38,a)].

given #15 (T,wt=8): 40 x * y != x | x = y.  [para(38(a,1),6(a,1)),demod(39(1),39(1)),flip(a)].

given #16 (A,wt=14): 14 x * (y * (y * z)) != y * z | z = x.  [para(5(a,1),7(a,1)),flip(a)].

given #17 (F,wt=13): 44 (c2 * c1) * (c1 * (c1 * c2)) != c2 * c1.  [para(38(a,1),17(a,1)),demod(39(7),39(10)),flip(a)].

given #18 (F,wt=13): 47 (c1 * (c1 * c2)) * (c2 * c1) != c2 * c1.  [back_demod(30),demod(39(12))].

given #19 (T,wt=8): 41 x * y != x | y = x.  [para(38(a,1),6(a,2)),demod(39(1),39(2))].

given #20 (T,wt=8): 42 x * y != y | y = x.  [para(38(a,1),7(a,1)),demod(39(1),39(3)),flip(a)].

given #21 (A,wt=14): 15 x * (y * (y * z)) != y * z | x = z.  [para(5(a,1),7(a,2))].

given #22 (F,wt=13): 54 (c2 * (c2 * c1)) * x != (c1 * c2) * x.  [ur(7,b,35,a)].

given #23 (F,wt=13): 55 x * (c2 * (c2 * c1)) != x * (c1 * c2).  [ur(6,b,35,a)].

given #24 (T,wt=8): 43 x * y != y | x = y.  [para(38(a,1),7(a,2)),demod(39(2),39(3))].

given #25 (T,wt=12): 58 x * y != y | x * (x * y) = y.  [para(39(a,1),12(a,1)),flip(a)].

given #26 (A,wt=19): 21 (x * (y * x)) * ((y * (y * x)) * (y * x)) = y * x.  [para(9(a,1),5(a,1,2,2)),demod(9(12))].

given #27 (F,wt=13): 63 (c1 * c2) * (c2 * (c2 * c1)) != c1 * c2.  [ur(40,b,35,a(flip))].

given #28 (F,wt=13): 98 (c2 * (c2 * c1)) * (c1 * c2) != c1 * c2.  [ur(42,b,35,a(flip))].

given #29 (T,wt=16): 77 x * (x * y) != x * y | x * (x * y) = y.  [para(39(a,1),14(a,1)),flip(b)].

given #30 (T,wt=18): 23 (x * (x * y)) * z != x * y | y * (x * y) = z.  [para(9(a,1),6(a,1)),flip(a)].

given #31 (A,wt=18): 24 x * (y * (z * y)) != z * y | z * (z * y) = x.  [para(9(a,1),7(a,1)),flip(a)].

given #32 (F,wt=13): 113 (c1 * c2) * (c1 * (c2 * c1)) != c2 * c1.  [para(9(a,1),54(a,1)),flip(a)].

given #33 (F,wt=15): 45 (c1 * (c1 * c2)) * (c2 * c1) != c1 * (c1 * c2).  [para(38(a,1),17(a,2)),demod(39(11),39(20))].

given #34 (T,wt=18): 51 x * y != z * y | z * (z * y) = x * (x * y).  [para(5(a,1),12(a,1))].

given #35 (T,wt=20): 67 x * (x * y) != x * y | y * (x * y) = x * (x * y).  [para(9(a,1),40(a,1)),flip(a),flip(b)].

given #36 (A,wt=23): 25 ((x * (x * y)) * (x * y)) * ((y * (x * y)) * (x * y)) = x * y.  [para(9(a,1),9(a,1,1,2)),demod(9(11),9(14))].

given #37 (F,wt=15): 46 (c2 * c1) * (c1 * (c1 * c2)) != c1 * (c1 * c2).  [back_demod(31),demod(39(14))].

given #38 (F,wt=15): 49 (c1 * c2) * (c1 * (c2 * c1)) != c1 * (c1 * c2).  [ur(12,b,17,a(flip))].

given #39 (T,wt=20): 102 x * (y * x) != y * x | x * (y * x) = y * (y * x).  [para(9(a,1),42(a,1)),flip(a)].

given #40 (T,wt=22): 53 (x * (y * x)) * z != y * x | (y * (y * x)) * (y * x) = z.  [para(9(a,1),12(a,2)),demod(9(12))].

given #41 (A,wt=17): 26 ((c2 * c1) * x) * y != ((c1 * (c1 * c2)) * x) * y.  [ur(7,b,16,a)].

given #42 (F,wt=15): 59 (c2 * (c2 * c1)) * (c1 * c2) != c2 * (c2 * c1).  [ur(40,b,35,a)].

given #43 (F,wt=15): 92 (c1 * c2) * (c2 * (c2 * c1)) != c2 * (c2 * c1).  [ur(42,b,35,a)].

given #44 (T,wt=22): 76 x * ((y * (y * z)) * (y * z)) != y * z | z * (y * z) = x.  [para(9(a,1),14(a,1,2,2)),demod(9(10))].

given #45 (T,wt=24): 123 x * (y * x) != y * x | (y * (y * x)) * (y * x) = x * (y * x).  [para(9(a,1),58(a,1)),demod(9(11)),flip(a)].

given #46 (A,wt=17): 27 x * ((c2 * c1) * y) != x * ((c1 * (c1 * c2)) * y).  [ur(6,b,16,a)].

given #47 (F,wt=15): 119 (c2 * c1) * (c2 * (c1 * c2)) != c2 * (c2 * c1).  [ur(12,b,55,a)].

given #48 (F,wt=15): 180 c2 * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * c2.  [ur(12,b,45,a(flip))].

given #49 (T,wt=26): 52 x * (y * (y * z)) != y * z | z * (y * z) = x * (x * (y * (y * z))).  [para(9(a,1),12(a,1)),flip(a),flip(b)].

given #50 (T,wt=26): 126 ((x * (x * y)) * (x * y)) * z != x * y | (y * (x * y)) * (x * y) = z.  [para(21(a,1),12(a,2)),demod(21(16))].

given #51 (A,wt=19): 28 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c2 * c1).  [para(5(a,1),16(a,1)),flip(a)].

given #52 (F,wt=15): 198 c2 * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,46,a(flip))].

given #53 (F,wt=15): 208 c2 * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * c2.  [ur(12,b,49,a(flip))].

given #54 (T,wt=26): 127 x * ((y * (z * y)) * (z * y)) != z * y | (z * (z * y)) * (z * y) = x.  [para(21(a,1),14(a,1,2,2)),demod(21(12))].

given #55 (T,wt=27): 124 ((x * (y * x)) * (y * x)) * (((y * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(21(a,1),9(a,1,1,2)),demod(21(15),21(18))].

given #56 (A,wt=21): 29 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [para(5(a,1),16(a,2))].

given #57 (F,wt=15): 251 c1 * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * c1.  [ur(12,b,59,a(flip))].

given #58 (F,wt=15): 259 c1 * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,92,a(flip))].

given #59 (T,wt=28): 128 (x * (x * y)) * (x * y) != x * y | (x * (x * y)) * (x * y) = y * (x * y).  [para(21(a,1),42(a,1)),flip(a)].

given #60 (T,wt=30): 125 x * (y * (z * y)) != z * y | (z * (z * y)) * (z * y) = x * (x * (y * (z * y))).  [para(21(a,1),12(a,1)),flip(a),flip(b)].

given #61 (A,wt=17): 33 (x * (c2 * c1)) * y != (x * (c1 * (c1 * c2))) * y.  [ur(7,b,17,a)].

given #62 (F,wt=15): 299 c1 * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * c1.  [ur(12,b,119,a(flip))].

given #63 (F,wt=17): 34 x * (y * (c2 * c1)) != x * (y * (c1 * (c1 * c2))).  [ur(6,b,17,a)].

given #64 (T,wt=30): 156 ((x * (y * x)) * (y * x)) * z != y * x | ((y * (y * x)) * (y * x)) * (y * x) = z.  [para(21(a,1),23(a,1,1,2)),demod(21(12),21(18))].

given #65 (T,wt=30): 163 x * (((y * (y * z)) * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x.  [para(21(a,1),24(a,1,2,2)),demod(21(14),21(18))].

given #66 (A,wt=19): 48 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(12,b,16,a)].

given #67 (F,wt=17): 56 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,32,a)].

given #68 (F,wt=17): 57 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,32,a)].

given #69 (T,wt=31): 130 (((x * (x * y)) * (x * y)) * (x * y)) * (((y * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(21(a,1),21(a,1,1,2)),demod(21(15),21(17),21(20))].

given #70 (T,wt=32): 129 (x * (x * y)) * (x * y) != x * y | (y * (x * y)) * (x * y) = (x * (x * y)) * (x * y).  [para(21(a,1),58(a,1)),demod(21(15)),flip(a)].

given #71 (A,wt=21): 50 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(12,b,16,a(flip))].

given #72 (F,wt=17): 64 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != c1 * c2.  [ur(40,b,32,a(flip))].

given #73 (F,wt=17): 80 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c2 * c1) * x.  [ur(7,b,44,a)].

given #74 (T,wt=32): 147 (x * (y * x)) * (y * x) != y * x | (x * (y * x)) * (y * x) = (y * (y * x)) * (y * x).  [para(21(a,1),77(a,1,2)),demod(21(11),21(15))].

given #75 (T,wt=34): 185 (((x * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((y * (x * y)) * (x * y)) * (x * y) = z.  [para(25(a,1),23(a,1,1,2)),demod(25(16),25(22))].

given #76 (A,wt=23): 60 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != (c2 * c1) * (c2 * (c1 * c2)).  [ur(40,b,32,a)].

given #77 (F,wt=17): 81 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c2 * c1).  [ur(6,b,44,a)].

given #78 (F,wt=17): 82 (c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2))) != c2 * c1.  [ur(40,b,44,a(flip))].

given #79 (T,wt=34): 186 x * (((y * (z * y)) * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x.  [para(25(a,1),24(a,1,2,2)),demod(25(16),25(22))].

given #80 (T,wt=35): 183 (((x * (y * x)) * (y * x)) * (y * x)) * ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(25(a,1),21(a,1,1,2)),demod(25(19),25(21),25(24))].

given #81 (A,wt=19): 61 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c2 * c1).  [ur(40,b,17,a)].

given #82 (F,wt=17): 86 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,47,a)].

given #83 (F,wt=17): 87 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,47,a)].

given #84 (T,wt=36): 182 (x * (y * x)) * (y * x) != y * x | ((y * (y * x)) * (y * x)) * (y * x) = (x * (y * x)) * (y * x).  [para(21(a,1),67(a,1,2)),demod(21(11),21(17),21(21))].

given #85 (T,wt=38): 181 x * ((y * (y * z)) * (y * z)) != y * z | (z * (y * z)) * (y * z) = x * (x * ((y * (y * z)) * (y * z))).  [para(21(a,1),51(a,1)),demod(21(22)),flip(a),flip(b)].

given #86 (A,wt=19): 62 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c2 * c1) * x.  [ur(40,b,16,a)].

given #87 (F,wt=17): 88 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != c2 * c1.  [ur(40,b,47,a(flip))].

given #88 (F,wt=17): 96 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(42,b,47,a(flip))].

given #89 (T,wt=38): 217 (((x * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((y * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(25(a,1),53(a,1,1,2)),demod(25(16),25(22),25(24))].

given #90 (T,wt=38): 268 x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((z * (y * z)) * (y * z)) * (y * z) = x.  [para(25(a,1),76(a,1,2,1,2)),demod(25(15),25(18),25(24))].

given #91 (A,wt=21): 65 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c1 * (c1 * c2)).  [ur(40,b,17,a(flip))].

given #92 (F,wt=17): 97 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != c2 * c1.  [ur(42,b,44,a(flip))].

given #93 (F,wt=17): 99 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(42,b,32,a(flip))].

given #94 (T,wt=39): 189 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(25(a,1),25(a,1,1,1,2)),demod(25(15),25(21),25(23),25(26))].

given #95 (T,wt=40): 184 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((x * (x * y)) * (x * y)) * (x * y) = (y * (x * y)) * (x * y).  [para(25(a,1),77(a,1,2)),demod(25(15),25(21))].

given #96 (A,wt=21): 66 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c1 * (c1 * c2)) * x.  [ur(40,b,16,a(flip))].

given #97 (F,wt=17): 109 ((c2 * (c2 * c1)) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,54,a)].

given #98 (F,wt=17): 110 x * ((c2 * (c2 * c1)) * y) != x * ((c1 * c2) * y).  [ur(6,b,54,a)].

given #99 (T,wt=42): 187 x * ((y * (z * y)) * (z * y)) != z * y | ((z * (z * y)) * (z * y)) * (z * y) = x * (x * ((y * (z * y)) * (z * y))).  [para(25(a,1),51(a,1)),demod(25(26)),flip(a),flip(b)].

given #100 (T,wt=42): 317 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((y * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(25(a,1),126(a,1,1,1,2)),demod(25(15),25(18),25(24),25(26))].

given #101 (A,wt=21): 68 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(14,b,35,a)].

given #102 (F,wt=17): 120 (x * (c2 * (c2 * c1))) * y != (x * (c1 * c2)) * y.  [ur(7,b,55,a)].

given #103 (F,wt=17): 121 x * (y * (c2 * (c2 * c1))) != x * (y * (c1 * c2)).  [ur(6,b,55,a)].

given #104 (T,wt=42): 358 x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((z * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(25(a,1),127(a,1,2,1,2)),demod(25(15),25(18),25(24),25(26))].

given #105 (T,wt=43): 359 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(124(a,1),25(a,1,1,1,2)),demod(124(17),124(25),124(27),124(30))].

given #106 (A,wt=29): 69 (c1 * c2) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * ((c2 * c1) * (c2 * (c1 * c2))).  [ur(14,b,32,a)].

given #107 (F,wt=17): 131 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != c1 * c2.  [ur(43,b,63,a)].

given #108 (F,wt=17): 133 (c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1))) != c1 * c2.  [ur(41,b,63,a)].

given #109 (T,wt=44): 188 ((x * (x * y)) * (x * y)) * (x * y) != x * y | ((y * (x * y)) * (x * y)) * (x * y) = ((x * (x * y)) * (x * y)) * (x * y).  [para(25(a,1),67(a,1,2)),demod(25(15),25(21),25(27))].

given #110 (T,wt=44): 210 ((x * (y * x)) * (y * x)) * (y * x) != y * x | ((x * (y * x)) * (y * x)) * (y * x) = ((y * (y * x)) * (y * x)) * (y * x).  [para(25(a,1),102(a,1,2)),demod(25(15),25(21),25(27))].

given #111 (A,wt=25): 70 (x * (c1 * (c1 * c2))) * (y * (y * (x * (c2 * c1)))) != y * (x * (c2 * c1)).  [ur(14,b,17,a)].

given #112 (F,wt=17): 137 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c1 * c2) * x.  [ur(7,b,63,a)].

given #113 (F,wt=17): 138 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c1 * c2).  [ur(6,b,63,a)].

given #114 (T,wt=46): 363 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(124(a,1),126(a,1,1,1,2)),demod(124(17),124(20),124(28),124(30))].

given #115 (T,wt=46): 364 x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((z * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(124(a,1),127(a,1,2,1,2)),demod(124(19),124(22),124(28),124(30))].

given #116 (A,wt=25): 71 ((c1 * (c1 * c2)) * x) * (y * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x).  [ur(14,b,16,a)].

given #117 (F,wt=17): 139 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,98,a)].

given #118 (F,wt=17): 141 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != c1 * c2.  [ur(41,b,98,a)].

given #119 (T,wt=47): 365 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(124(a,1),124(a,1,1,1,2)),demod(124(19),124(25),124(27),124(29),124(32))].

given #120 (T,wt=48): 269 ((x * (y * x)) * (y * x)) * (y * x) != y * x | (((y * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((x * (y * x)) * (y * x)) * (y * x).  [para(25(a,1),123(a,1,2)),demod(25(15),25(21),25(23),25(29))].

given #121 (A,wt=19): 72 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(14,b,35,a(flip))].

given #122 (F,wt=17): 145 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,98,a)].

given #123 (F,wt=17): 146 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,98,a)].

given #124 (T,wt=50): 308 x * (((y * (y * z)) * (y * z)) * (y * z)) != y * z | ((z * (y * z)) * (y * z)) * (y * z) = x * (x * (((y * (y * z)) * (y * z)) * (y * z))).  [para(25(a,1),52(a,1,2,2)),demod(25(16),25(22),25(28))].

given #125 (T,wt=50): 468 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(124(a,1),156(a,1,1,1,2)),demod(124(19),124(22),124(28),124(30),124(32))].

given #126 (A,wt=23): 73 ((c2 * c1) * (c2 * (c1 * c2))) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(14,b,32,a(flip))].

given #127 (F,wt=17): 150 (c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))) != c2 * c1.  [ur(23,b,17,a)].

given #128 (F,wt=17): 152 (c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))) != c1 * c2.  [ur(23,b,55,a(flip))].

given #129 (T,wt=50): 481 x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(124(a,1),163(a,1,2,1,1,2)),demod(124(17),124(19),124(22),124(30),124(32))].

given #130 (T,wt=51): 543 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(130(a,1),124(a,1,1,1,2)),demod(130(21),130(29),130(31),130(33),130(36))].

given #131 (A,wt=27): 74 (x * (c2 * c1)) * (y * (y * (x * (c1 * (c1 * c2))))) != y * (x * (c1 * (c1 * c2))).  [ur(14,b,17,a(flip))].

given #132 (F,wt=17): 164 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,113,a)].

given #133 (F,wt=17): 166 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != c2 * c1.  [ur(41,b,113,a)].

given #134 (T,wt=52): 360 (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((y * (x * y)) * (x * y)) * (x * y).  [para(124(a,1),102(a,1,2)),demod(124(19),124(27),124(33))].

given #135 (T,wt=54): 362 x * (((y * (z * y)) * (z * y)) * (z * y)) != z * y | (((z * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * (((y * (z * y)) * (z * y)) * (z * y))).  [para(124(a,1),52(a,1,2,2)),demod(124(18),124(26),124(32))].

given #136 (A,wt=27): 75 ((c2 * c1) * x) * (y * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x).  [ur(14,b,16,a(flip))].

given #137 (F,wt=17): 170 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,113,a)].

given #138 (F,wt=17): 171 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,113,a)].

given #139 (T,wt=54): 550 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(130(a,1),156(a,1,1,1,2)),demod(130(21),130(24),130(32),130(34),130(36))].

given #140 (T,wt=54): 551 x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(130(a,1),163(a,1,2,1,1,2)),demod(130(21),130(23),130(26),130(34),130(36))].

given #141 (A,wt=23): 78 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1) != (c2 * c1) * (c1 * (c1 * c2)).  [ur(40,b,44,a)].

given #142 (F,wt=17): 212 (c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)) != c2 * c1.  [ur(53,b,54,a)].

given #143 (F,wt=17): 216 (c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)) != c1 * c2.  [ur(53,b,16,a(flip))].

given #144 (T,wt=55): 552 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(130(a,1),130(a,1,1,1,1,2)),demod(130(21),130(23),130(31),130(33),130(35),130(38))].

given #145 (T,wt=56): 361 (((x * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((y * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((x * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(124(a,1),123(a,1,2)),demod(124(19),124(25),124(27),124(35))].

given #146 (A,wt=29): 79 (c2 * c1) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))).  [ur(14,b,44,a)].

given #147 (F,wt=17): 541 c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2.  [ur(12,b,57,a(flip))].

given #148 (F,wt=17): 648 c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1.  [ur(12,b,81,a(flip))].

given #149 (T,wt=56): 397 (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((y * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(124(a,1),128(a,1,1,2)),demod(124(17),124(19),124(25),124(27),124(35))].

given #150 (T,wt=58): 613 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(130(a,1),185(a,1,1,1,1,2)),demod(130(21),130(23),130(26),130(34),130(36),130(38))].

given #151 (A,wt=23): 83 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c2 * c1))) != x * (c2 * c1).  [ur(14,b,44,a(flip))].

given #152 (F,wt=17): 746 c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1.  [ur(12,b,87,a(flip))].

given #153 (F,wt=17): 1215 c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2.  [ur(12,b,138,a(flip))].

given #154 (T,wt=58): 671 x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(130(a,1),186(a,1,2,1,1,2)),demod(130(21),130(23),130(26),130(34),130(36),130(38))].

given #155 (T,wt=59): 677 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(183(a,1),130(a,1,1,1,1,2)),demod(183(23),183(25),183(35),183(37),183(39),183(42))].

given #156 (A,wt=29): 85 (c2 * c1) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)).  [ur(14,b,47,a)].

given #157 (F,wt=17): 1396 c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2.  [ur(12,b,146,a(flip))].

given #158 (F,wt=17): 1615 c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1.  [ur(12,b,171,a(flip))].

given #159 (T,wt=60): 542 (((x * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((x * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(130(a,1),123(a,1,2)),demod(130(21),130(29),130(31),130(39))].

given #160 (T,wt=62): 398 x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((z * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * ((((y * (y * z)) * (y * z)) * (y * z)) * (y * z))).  [para(124(a,1),125(a,1,2,2)),demod(124(20),124(26),124(28),124(36))].

given #161 (A,wt=23): 89 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c2 * c1))) != x * (c2 * c1).  [ur(14,b,47,a(flip))].

given #162 (F,wt=19): 94 (x * (c1 * (c1 * c2))) * (x * (c2 * c1)) != x * (c2 * c1).  [ur(42,b,17,a)].

given #163 (F,wt=19): 95 ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x) != (c2 * c1) * x.  [ur(42,b,16,a)].

given #164 (T,wt=62): 680 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(183(a,1),185(a,1,1,1,1,2)),demod(183(23),183(25),183(28),183(38),183(40),183(42))].

given #165 (T,wt=62): 681 x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(183(a,1),186(a,1,2,1,1,2)),demod(183(25),183(27),183(30),183(38),183(40),183(42))].

given #166 (A,wt=23): 90 (c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)) != (c1 * (c1 * c2)) * (c2 * c1).  [ur(42,b,47,a)].

given #167 (F,wt=19): 104 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c1 * c2) * x.  [ur(41,b,54,a)].

given #168 (F,wt=19): 111 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c1 * c2) * x.  [ur(42,b,54,a(flip))].

given #169 (T,wt=63): 682 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(183(a,1),183(a,1,1,1,1,2)),demod(183(25),183(27),183(35),183(37),183(39),183(41),183(44))].

given #170 (T,wt=64): 544 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((y * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(130(a,1),128(a,1,1,2)),demod(130(21),130(23),130(31),130(33),130(41))].

given #171 (A,wt=23): 93 (c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))) != (c2 * c1) * (c2 * (c1 * c2)).  [ur(42,b,32,a)].

given #172 (F,wt=19): 112 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c1 * c2) * x.  [ur(12,b,54,a(flip))].

given #173 (F,wt=19): 115 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c1 * c2).  [ur(41,b,55,a)].

given #174 (T,wt=66): 545 x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * ((((y * (z * y)) * (z * y)) * (z * y)) * (z * y))).  [para(130(a,1),125(a,1,2,2)),demod(130(22),130(30),130(32),130(40))].

given #175 (T,wt=66): 791 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(183(a,1),217(a,1,1,1,1,2)),demod(183(25),183(27),183(30),183(38),183(40),183(42),183(44))].

given #176 (A,wt=21): 100 (x * (c2 * c1)) * (x * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)).  [ur(42,b,17,a(flip))].

given #177 (F,wt=19): 122 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c1 * c2).  [ur(42,b,55,a(flip))].

given #178 (F,wt=19): 177 ((c1 * (c1 * c2)) * (c2 * c1)) * x != (c1 * (c1 * c2)) * x.  [ur(7,b,45,a)].

given #179 (T,wt=66): 809 x * (((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(183(a,1),268(a,1,2,1,1,1,2)),demod(183(23),183(25),183(27),183(30),183(40),183(42),183(44))].

given #180 (T,wt=67): 848 (((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(189(a,1),183(a,1,1,1,1,2)),demod(189(27),189(29),189(39),189(41),189(43),189(45),189(48))].

given #181 (A,wt=21): 101 ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x) != (c1 * (c1 * c2)) * x.  [ur(42,b,16,a(flip))].

given #182 (F,wt=19): 178 x * ((c1 * (c1 * c2)) * (c2 * c1)) != x * (c1 * (c1 * c2)).  [ur(6,b,45,a)].

given #183 (F,wt=19): 179 ((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,45,a(flip))].

given #184 (T,wt=68): 555 ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(130(a,1),129(a,1,1,2)),demod(130(21),130(23),130(31),130(33),130(41),130(43))].

given #185 (T,wt=68): 600 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(130(a,1),147(a,1,1,2)),demod(130(21),130(23),130(31),130(33),130(41),130(43))].

given #186 (A,wt=21): 103 ((c1 * c2) * x) * ((c2 * (c2 * c1)) * x) != (c2 * (c2 * c1)) * x.  [ur(42,b,54,a)].

given #187 (F,wt=19): 195 ((c2 * c1) * (c1 * (c1 * c2))) * x != (c1 * (c1 * c2)) * x.  [ur(7,b,46,a)].

given #188 (F,wt=19): 196 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)).  [ur(6,b,46,a)].

given #189 (T,wt=70): 851 (((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(189(a,1),217(a,1,1,1,1,2)),demod(189(27),189(29),189(32),189(42),189(44),189(46),189(48))].

given #190 (T,wt=70): 852 x * ((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(189(a,1),268(a,1,2,1,1,1,2)),demod(189(27),189(29),189(31),189(34),189(44),189(46),189(48))].

given #191 (A,wt=21): 105 ((c2 * (c2 * c1)) * x) * ((c1 * c2) * x) != (c2 * (c2 * c1)) * x.  [ur(40,b,54,a)].

given #192 (F,wt=19): 197 ((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,46,a(flip))].

given #193 (F,wt=19): 205 ((c1 * c2) * (c1 * (c2 * c1))) * x != (c1 * (c1 * c2)) * x.  [ur(7,b,49,a)].

given #194 (T,wt=71): 853 ((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(189(a,1),189(a,1,1,1,1,1,2)),demod(189(27),189(29),189(31),189(41),189(43),189(45),189(47),189(50))].

given #195 (T,wt=72): 678 ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(183(a,1),129(a,1,1,2)),demod(183(23),183(25),183(35),183(37),183(45),183(47))].

given #196 (A,wt=25): 106 ((c2 * (c2 * c1)) * x) * (y * (y * ((c1 * c2) * x))) != y * ((c1 * c2) * x).  [ur(15,b,54,a)].

given #197 (F,wt=19): 206 x * ((c1 * c2) * (c1 * (c2 * c1))) != x * (c1 * (c1 * c2)).  [ur(6,b,49,a)].

given #198 (F,wt=19): 207 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,49,a(flip))].

given #199 (T,wt=74): 672 x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * (((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))).  [para(183(a,1),125(a,1,2,2)),demod(183(26),183(34),183(36),183(46))].

given #200 (T,wt=74): 961 ((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(189(a,1),317(a,1,1,1,1,1,2)),demod(189(27),189(29),189(31),189(34),189(44),189(46),189(48),189(50))].

given #201 (A,wt=27): 107 ((c1 * c2) * x) * (y * (y * ((c2 * (c2 * c1)) * x))) != y * ((c2 * (c2 * c1)) * x).  [ur(14,b,54,a)].

given #202 (F,wt=19): 248 ((c2 * (c2 * c1)) * (c1 * c2)) * x != (c2 * (c2 * c1)) * x.  [ur(7,b,59,a)].

given #203 (F,wt=19): 249 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * (c2 * (c2 * c1)).  [ur(6,b,59,a)].

given #204 (T,wt=74): 1083 x * ((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(189(a,1),358(a,1,2,1,1,1,2)),demod(189(27),189(29),189(31),189(34),189(44),189(46),189(48),189(50))].

given #205 (T,wt=75): 1089 ((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(359(a,1),189(a,1,1,1,1,1,2)),demod(359(29),359(31),359(33),359(45),359(47),359(49),359(51),359(54))].

given #206 (A,wt=21): 108 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c2 * (c2 * c1)) * x.  [ur(12,b,54,a)].

given #207 (F,wt=19): 250 ((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,59,a(flip))].

given #208 (F,wt=19): 256 ((c1 * c2) * (c2 * (c2 * c1))) * x != (c2 * (c2 * c1)) * x.  [ur(7,b,92,a)].

given #209 (T,wt=76): 679 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(183(a,1),147(a,1,1,2)),demod(183(25),183(27),183(37),183(39),183(47),183(49))].

given #210 (T,wt=78): 748 x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * (((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y))).  [para(183(a,1),181(a,1,2,1,2)),demod(183(23),183(26),183(36),183(38),183(46),183(48))].

given #211 (A,wt=21): 114 (x * (c1 * c2)) * (x * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)).  [ur(42,b,55,a)].

given #212 (F,wt=19): 257 x * ((c1 * c2) * (c2 * (c2 * c1))) != x * (c2 * (c2 * c1)).  [ur(6,b,92,a)].

given #213 (F,wt=19): 258 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,92,a(flip))].

given #214 (T,wt=78): 1092 ((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(359(a,1),317(a,1,1,1,1,1,2)),demod(359(29),359(31),359(33),359(36),359(48),359(50),359(52),359(54))].

given #215 (T,wt=78): 1097 x * (((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(359(a,1),358(a,1,2,1,1,1,2)),demod(359(31),359(33),359(35),359(38),359(48),359(50),359(52),359(54))].

given #216 (A,wt=21): 116 (x * (c2 * (c2 * c1))) * (x * (c1 * c2)) != x * (c2 * (c2 * c1)).  [ur(40,b,55,a)].

given #217 (F,wt=19): 280 x * ((c2 * c1) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x.  [ur(12,b,27,a)].

given #218 (F,wt=19): 296 ((c2 * c1) * (c2 * (c1 * c2))) * x != (c2 * (c2 * c1)) * x.  [ur(7,b,119,a)].

given #219 (T,wt=79): 1098 (((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(359(a,1),359(a,1,1,1,1,1,2)),demod(359(31),359(33),359(35),359(45),359(47),359(49),359(51),359(53),359(56))].

given #220 (T,wt=80): 747 (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(183(a,1),182(a,1,1,2)),demod(183(25),183(27),183(35),183(37),183(39),183(49),183(51))].

given #221 (A,wt=25): 117 (x * (c2 * (c2 * c1))) * (y * (y * (x * (c1 * c2)))) != y * (x * (c1 * c2)).  [ur(15,b,55,a)].

given #222 (F,wt=19): 297 x * ((c2 * c1) * (c2 * (c1 * c2))) != x * (c2 * (c2 * c1)).  [ur(6,b,119,a)].

given #223 (F,wt=19): 298 ((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,119,a(flip))].

given #224 (T,wt=80): 847 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(189(a,1),147(a,1,1,2)),demod(189(27),189(29),189(39),189(41),189(51),189(53))].

given #225 (T,wt=82): 1238 (((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(359(a,1),363(a,1,1,1,1,1,2)),demod(359(31),359(33),359(35),359(38),359(48),359(50),359(52),359(54),359(56))].

given #226 (A,wt=27): 118 (x * (c1 * c2)) * (y * (y * (x * (c2 * (c2 * c1))))) != y * (x * (c2 * (c2 * c1))).  [ur(14,b,55,a)].

given #227 (F,wt=19): 300 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2) != c1 * c2.  [ur(43,b,180,a)].

given #228 (F,wt=19): 302 (c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2.  [ur(41,b,180,a)].

given #229 (T,wt=82): 1261 x * (((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(359(a,1),364(a,1,2,1,1,1,1,2)),demod(359(29),359(31),359(33),359(35),359(38),359(50),359(52),359(54),359(56))].

given #230 (T,wt=83): 1313 (((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(365(a,1),359(a,1,1,1,1,1,2)),demod(365(33),365(35),365(37),365(49),365(51),365(53),365(55),365(57),365(60))].

given #231 (A,wt=23): 134 ((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)).  [ur(40,b,63,a)].

given #232 (F,wt=19): 306 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c1 * c2) * x.  [ur(7,b,180,a)].

given #233 (F,wt=19): 307 x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c1 * c2).  [ur(6,b,180,a)].

given #234 (T,wt=84): 849 (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = (((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(189(a,1),182(a,1,1,2)),demod(189(27),189(29),189(39),189(41),189(43),189(53),189(55))].

given #235 (T,wt=86): 850 x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * ((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))).  [para(189(a,1),181(a,1,2,1,2)),demod(189(27),189(30),189(40),189(42),189(52),189(54))].

given #236 (A,wt=23): 135 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(15,b,63,a)].

given #237 (F,wt=19): 331 c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,28,a(flip))].

given #238 (F,wt=19): 332 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2) != c1 * c2.  [ur(43,b,198,a)].

given #239 (T,wt=86): 1315 (((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | (((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(365(a,1),363(a,1,1,1,1,1,2)),demod(365(33),365(35),365(37),365(40),365(52),365(54),365(56),365(58),365(60))].

given #240 (T,wt=86): 1316 x * ((((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(365(a,1),364(a,1,2,1,1,1,1,2)),demod(365(33),365(35),365(37),365(39),365(42),365(54),365(56),365(58),365(60))].

given #241 (A,wt=29): 136 (c1 * c2) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))).  [ur(14,b,63,a)].

given #242 (F,wt=19): 334 (c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2.  [ur(41,b,198,a)].

given #243 (F,wt=19): 338 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c1 * c2) * x.  [ur(7,b,198,a)].

given #244 (T,wt=87): 1317 ((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * ((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(365(a,1),365(a,1,1,1,1,1,1,2)),demod(365(33),365(35),365(37),365(39),365(51),365(53),365(55),365(57),365(59),365(62))].

given #245 (T,wt=88): 854 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = (((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(189(a,1),184(a,1,1,1,2)),demod(189(27),189(29),189(31),189(41),189(43),189(45),189(55),189(57))].

given #246 (A,wt=23): 140 (c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)) != (c2 * (c2 * c1)) * (c1 * c2).  [ur(42,b,98,a)].

given #247 (F,wt=19): 339 x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c1 * c2).  [ur(6,b,198,a)].

given #248 (F,wt=19): 340 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2) != c1 * c2.  [ur(43,b,208,a)].

given #249 (T,wt=90): 940 x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x * (x * ((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y))).  [para(189(a,1),187(a,1,2,1,2)),demod(189(27),189(30),189(40),189(42),189(44),189(54),189(56))].

given #250 (T,wt=90): 1417 ((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | (((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(365(a,1),468(a,1,1,1,1,1,1,2)),demod(365(33),365(35),365(37),365(39),365(42),365(54),365(56),365(58),365(60),365(62))].

given #251 (A,wt=23): 143 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(15,b,98,a)].

given #252 (F,wt=19): 342 (c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2.  [ur(41,b,208,a)].

given #253 (F,wt=19): 346 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c1 * c2) * x.  [ur(7,b,208,a)].

given #254 (T,wt=90): 1483 x * ((((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | (((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(365(a,1),481(a,1,2,1,1,1,1,2)),demod(365(33),365(35),365(37),365(39),365(42),365(54),365(56),365(58),365(60),365(62))].

given #255 (T,wt=91): 1492 ((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(543(a,1),365(a,1,1,1,1,1,1,2)),demod(543(35),543(37),543(39),543(41),543(55),543(57),543(59),543(61),543(63),543(66))].

given #256 (A,wt=29): 144 (c1 * c2) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)).  [ur(14,b,98,a)].

given #257 (F,wt=19): 347 x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c1 * c2).  [ur(6,b,208,a)].

given #258 (F,wt=19): 381 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1) != c2 * c1.  [ur(43,b,251,a)].

given #259 (T,wt=92): 1088 ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(359(a,1),182(a,1,1,2)),demod(359(31),359(33),359(43),359(45),359(47),359(59),359(61))].

given #260 (T,wt=92): 1090 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(359(a,1),184(a,1,1,1,2)),demod(359(29),359(31),359(33),359(43),359(45),359(47),359(59),359(61))].

given #261 (A,wt=21): 148 (c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2)) != c2 * (c2 * c1).  [ur(23,b,55,a)].

given #262 (F,wt=19): 383 (c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1.  [ur(41,b,251,a)].

given #263 (F,wt=19): 387 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c2 * c1) * x.  [ur(7,b,251,a)].

given #264 (T,wt=94): 1493 ((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * z != y * x | ((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = z.  [para(543(a,1),468(a,1,1,1,1,1,1,2)),demod(543(35),543(37),543(39),543(41),543(44),543(58),543(60),543(62),543(64),543(66))].

given #265 (T,wt=94): 1494 x * (((((((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | (((((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x.  [para(543(a,1),481(a,1,2,1,1,1,1,2)),demod(543(37),543(39),543(41),543(43),543(46),543(58),543(60),543(62),543(64),543(66))].

given #266 (A,wt=29): 149 (x * (x * (c2 * (c2 * c1)))) * ((c1 * c2) * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(23,b,54,a)].

given #267 (F,wt=19): 388 x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c2 * c1).  [ur(6,b,251,a)].

given #268 (F,wt=19): 389 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1) != c2 * c1.  [ur(43,b,259,a)].

given #269 (T,wt=95): 1495 (((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) = x * y.  [para(543(a,1),543(a,1,1,1,1,1,1,2)),demod(543(37),543(39),543(41),543(43),543(55),543(57),543(59),543(61),543(63),543(65),543(68))].

given #270 (T,wt=96): 1135 ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) != y * x | (((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x) = ((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x).  [para(359(a,1),188(a,1,1,1,2)),demod(359(29),359(31),359(33),359(45),359(47),359(49),359(59),359(61),359(63))].

given #271 (A,wt=25): 151 (x * (x * (c2 * c1))) * ((c1 * (c1 * c2)) * (x * (c2 * c1))) != x * (c2 * c1).  [ur(23,b,16,a)].

given #272 (F,wt=19): 391 (c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1.  [ur(41,b,259,a)].

given #273 (F,wt=19): 395 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c2 * c1) * x.  [ur(7,b,259,a)].

given #274 (T,wt=98): 1091 x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) != y * z | ((((((z * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z) = x * (x * (((((((y * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z)) * (y * z))).  [para(359(a,1),187(a,1,2,1,2)),demod(359(31),359(34),359(44),359(46),359(48),359(60),359(62))].

given #275 (T,wt=98): 1634 (((((((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * z != x * y | ((((((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = z.  [para(543(a,1),550(a,1,1,1,1,1,1,2)),demod(543(37),543(39),543(41),543(43),543(46),543(58),543(60),543(62),543(64),543(66),543(68))].

given #276 (A,wt=25): 153 (x * (x * (c1 * c2))) * ((c2 * (c2 * c1)) * (x * (c1 * c2))) != x * (c1 * c2).  [ur(23,b,54,a(flip))].

given #277 (F,wt=19): 396 x * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c2 * c1).  [ur(6,b,259,a)].

given #278 (F,wt=19): 425 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1) != c2 * c1.  [ur(43,b,299,a)].

given #279 (T,wt=98): 1653 x * (((((((((((y * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) != z * y | ((((((((((z * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y)) * (z * y) = x.  [para(543(a,1),551(a,1,2,1,1,1,1,1,2)),demod(543(35),543(37),543(39),543(41),543(43),543(46),543(60),543(62),543(64),543(66),543(68))].

given #280 (T,wt=99): 1684 (((((((((((x * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * ((((((((((((y * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) * (y * x)) = y * x.  [para(552(a,1),543(a,1,1,1,1,1,1,2)),demod(552(39),552(41),552(43),552(45),552(59),552(61),552(63),552(65),552(67),552(69),552(72))].

given #281 (A,wt=21): 154 (c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1)) != c1 * (c1 * c2).  [ur(23,b,17,a(flip))].

given #282 (F,wt=19): 427 (c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * c1.  [ur(41,b,299,a)].

given #283 (F,wt=19): 431 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c2 * c1) * x.  [ur(7,b,299,a)].

given #284 (T,wt=100): 1136 (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) != x * y | (((((((x * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y) = ((((((y * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y)) * (x * y).  [para(359(a,1),210(a,1,1,1,2)),demod(359(31),359(33),359(35),359(47),359(49),359(51),359(61),359(63),359(65))].

given #285 (T,wt=19): 432 x * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c2 * c1).  [ur(6,b,299,a)].

given #286 (A,wt=29): 155 (x * (x * (c1 * (c1 * c2)))) * ((c2 * c1) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [ur(23,b,16,a(flip))].

given #287 (F,wt=19): 445 (c2 * c1) * (x * (x * (c1 * (c1 * c2)))) != x * (c2 * c1).  [ur(12,b,34,a)].

given #288 (F,wt=19): 636 (c2 * c1) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1).  [ur(12,b,81,a),demod(39(12)),flip(a)].

given #289 (T,wt=19): 937 x * ((c1 * c2) * ((c2 * (c2 * c1)) * x)) != (c1 * c2) * x.  [ur(12,b,110,a(flip))].

given #290 (T,wt=19): 1059 (c1 * c2) * (x * (x * (c2 * (c2 * c1)))) != x * (c1 * c2).  [ur(12,b,121,a(flip))].

given #291 (A,wt=21): 157 (c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1))) != c2 * (c2 * c1).  [ur(24,b,55,a)].

given #292 (F,wt=19): 1132 (c2 * (c2 * c1)) * (c1 * c2) != (c1 * c2) * (c2 * (c2 * c1)).  [ur(12,b,133,a)].

given #293 (F,wt=19): 1342 c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,72,a(flip))].

given #294 (T,wt=19): 3015 c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2.  [ur(12,b,307,a(flip))].

given #295 (T,wt=19): 3197 c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2.  [ur(12,b,339,a(flip))].

given #296 (A,wt=29): 158 ((c1 * c2) * ((c2 * (c2 * c1)) * x)) * (x * ((c2 * (c2 * c1)) * x)) != (c2 * (c2 * c1)) * x.  [ur(24,b,54,a)].

given #297 (F,wt=19): 3372 c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2.  [ur(12,b,347,a(flip))].

given #298 (F,wt=19): 3519 c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1.  [ur(12,b,388,a(flip))].

given #299 (T,wt=19): 3674 c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1.  [ur(12,b,396,a(flip))].

given #300 (T,wt=19): 3781 c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1.  [ur(12,b,432,a(flip))].

given #301 (A,wt=25): 159 ((c1 * (c1 * c2)) * ((c2 * c1) * x)) * (x * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(24,b,16,a)].

given #302 (F,wt=21): 161 (c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(24,b,17,a(flip))].

given #303 (F,wt=21): 172 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != c1 * (c1 * c2).  [ur(43,b,45,a)].

given #304 (T,wt=21): 173 (c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1)) != c1 * (c1 * c2).  [ur(41,b,45,a)].

given #305 (T,wt=21): 190 ((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2)) != c1 * (c1 * c2).  [ur(43,b,46,a)].

given #306 (A,wt=25): 160 ((c2 * (c2 * c1)) * ((c1 * c2) * x)) * (x * ((c1 * c2) * x)) != (c1 * c2) * x.  [ur(24,b,54,a(flip))].

given #307 (F,wt=21): 192 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(41,b,46,a)].

given #308 (F,wt=21): 199 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != c1 * (c1 * c2).  [ur(43,b,49,a)].

given #309 (T,wt=21): 201 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != c1 * (c1 * c2).  [ur(41,b,49,a)].

given #310 (T,wt=21): 213 (c1 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * (c1 * c2))) != c2 * c1.  [ur(53,b,17,a)].

given #311 (A,wt=29): 162 ((c2 * c1) * ((c1 * (c1 * c2)) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(24,b,16,a(flip))].

given #312 (F,wt=21): 214 (c2 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * (c2 * c1))) != c1 * c2.  [ur(53,b,55,a(flip))].

given #313 (F,wt=21): 230 (((c2 * c1) * x) * y) * z != (((c1 * (c1 * c2)) * x) * y) * z.  [ur(7,b,26,a)].

given #314 (T,wt=21): 231 x * (((c2 * c1) * y) * z) != x * (((c1 * (c1 * c2)) * y) * z).  [ur(6,b,26,a)].

given #315 (T,wt=21): 242 ((c2 * c1) * (c1 * c2)) * ((c2 * (c1 * c2)) * (c1 * c2)) != c1 * c2.  [para(25(a,1),26(a,2))].

given #316 (A,wt=23): 165 (c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)).  [ur(42,b,113,a)].

given #317 (F,wt=21): 243 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != c2 * (c2 * c1).  [ur(43,b,59,a)].

given #318 (F,wt=21): 244 (c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2)) != c2 * (c2 * c1).  [ur(41,b,59,a)].

given #319 (T,wt=21): 252 ((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1)) != c2 * (c2 * c1).  [ur(43,b,92,a)].

given #320 (T,wt=21): 253 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != c2 * (c2 * c1).  [ur(41,b,92,a)].

given #321 (A,wt=23): 167 ((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1) != (c1 * c2) * (c1 * (c2 * c1)).  [ur(40,b,113,a)].

given #322 (F,wt=21): 263 (c1 * (c1 * (c1 * c2))) * ((c2 * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(76,b,17,a)].

given #323 (F,wt=21): 264 (c2 * (c2 * (c2 * c1))) * ((c1 * (c1 * c2)) * (c1 * c2)) != c1 * c2.  [ur(76,b,55,a(flip))].

given #324 (T,wt=21): 281 (x * ((c2 * c1) * y)) * z != (x * ((c1 * (c1 * c2)) * y)) * z.  [ur(7,b,27,a)].

given #325 (T,wt=21): 282 x * (y * ((c2 * c1) * z)) != x * (y * ((c1 * (c1 * c2)) * z)).  [ur(6,b,27,a)].

given #326 (A,wt=23): 168 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c2 * c1))) != x * (c2 * c1).  [ur(15,b,113,a)].

given #327 (F,wt=21): 287 x * ((c1 * (c1 * c2)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x.  [ur(12,b,27,a(flip))].

given #328 (F,wt=21): 290 ((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1)) != c2 * (c2 * c1).  [ur(43,b,119,a)].

given #329 (T,wt=21): 292 (c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2))) != c2 * (c2 * c1).  [ur(41,b,119,a)].

given #330 (T,wt=21): 349 ((c1 * c2) * (c2 * c1)) * ((c1 * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(127,b,54,a)].

given #331 (A,wt=29): 169 (c2 * c1) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))).  [ur(14,b,113,a)].

given #332 (F,wt=21): 412 ((x * (c2 * c1)) * y) * z != ((x * (c1 * (c1 * c2))) * y) * z.  [ur(7,b,33,a)].

given #333 (F,wt=21): 413 x * ((y * (c2 * c1)) * z) != x * ((y * (c1 * (c1 * c2))) * z).  [ur(6,b,33,a)].

given #334 (T,wt=21): 446 (x * (y * (c2 * c1))) * z != (x * (y * (c1 * (c1 * c2)))) * z.  [ur(7,b,34,a)].

given #335 (T,wt=21): 447 x * (y * (z * (c2 * c1))) != x * (y * (z * (c1 * (c1 * c2)))).  [ur(6,b,34,a)].

given #336 (A,wt=25): 174 ((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2)) != (c1 * (c1 * c2)) * (c2 * c1).  [ur(40,b,45,a)].

given #337 (F,wt=21): 454 (c1 * (c1 * c2)) * (x * (x * (c2 * c1))) != x * (c1 * (c1 * c2)).  [ur(12,b,34,a(flip))].

given #338 (F,wt=21): 508 (((c2 * c1) * (c2 * (c1 * c2))) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,56,a)].

given #339 (T,wt=21): 509 x * (((c2 * c1) * (c2 * (c1 * c2))) * y) != x * ((c1 * c2) * y).  [ur(6,b,56,a)].

given #340 (T,wt=21): 531 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * y != (x * (c1 * c2)) * y.  [ur(7,b,57,a)].

given #341 (A,wt=27): 175 ((c1 * (c1 * c2)) * (c2 * c1)) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [ur(15,b,45,a)].

given #342 (F,wt=21): 532 x * (y * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (y * (c1 * c2)).  [ur(6,b,57,a)].

given #343 (F,wt=21): 539 (c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,57,a(flip))].

given #344 (T,wt=21): 540 (c1 * (c1 * c2)) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2.  [ur(23,b,57,a(flip))].

given #345 (T,wt=21): 572 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * (c1 * c2) != c1 * c2.  [ur(43,b,64,a)].

given #346 (A,wt=31): 176 (c1 * (c1 * c2)) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * ((c1 * (c1 * c2)) * (c2 * c1)).  [ur(14,b,45,a)].

given #347 (F,wt=21): 573 (c1 * c2) * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != c1 * c2.  [ur(41,b,64,a)].

given #348 (F,wt=21): 577 ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) * x != (c1 * c2) * x.  [ur(7,b,64,a)].

given #349 (T,wt=21): 578 x * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c1 * c2).  [ur(6,b,64,a)].

given #350 (T,wt=21): 590 (((c2 * c1) * (c1 * (c1 * c2))) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,80,a)].

given #351 (A,wt=25): 191 (c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2))) != (c2 * c1) * (c1 * (c1 * c2)).  [ur(42,b,46,a)].

given #352 (F,wt=21): 591 x * (((c2 * c1) * (c1 * (c1 * c2))) * y) != x * ((c2 * c1) * y).  [ur(6,b,80,a)].

given #353 (F,wt=21): 637 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * y != (x * (c2 * c1)) * y.  [ur(7,b,81,a)].

given #354 (T,wt=21): 638 x * (y * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (y * (c2 * c1)).  [ur(6,b,81,a)].

given #355 (T,wt=21): 646 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,81,a(flip))].

given #356 (A,wt=27): 193 ((c2 * c1) * (c1 * (c1 * c2))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [ur(15,b,46,a)].

given #357 (F,wt=21): 647 (c2 * (c2 * c1)) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1.  [ur(23,b,81,a(flip))].

given #358 (F,wt=21): 649 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1.  [ur(43,b,82,a)].

given #359 (T,wt=21): 650 (c2 * c1) * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * c1.  [ur(41,b,82,a)].

given #360 (T,wt=21): 654 ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) * x != (c2 * c1) * x.  [ur(7,b,82,a)].

given #361 (A,wt=31): 194 (c1 * (c1 * c2)) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * ((c2 * c1) * (c1 * (c1 * c2))).  [ur(14,b,46,a)].

given #362 (F,wt=21): 655 x * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c2 * c1).  [ur(6,b,82,a)].

given #363 (F,wt=21): 710 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,86,a)].

given #364 (T,wt=21): 711 x * (((c1 * (c1 * c2)) * (c2 * c1)) * y) != x * ((c2 * c1) * y).  [ur(6,b,86,a)].

given #365 (T,wt=21): 734 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * y != (x * (c2 * c1)) * y.  [ur(7,b,87,a)].

given #366 (A,wt=25): 200 (c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1))) != (c1 * c2) * (c1 * (c2 * c1)).  [ur(42,b,49,a)].

given #367 (F,wt=21): 735 x * (y * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (y * (c2 * c1)).  [ur(6,b,87,a)].

given #368 (F,wt=21): 744 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,87,a(flip))].

given #369 (T,wt=21): 745 (c2 * (c2 * c1)) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1.  [ur(23,b,87,a(flip))].

given #370 (T,wt=21): 760 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,88,a)].

given #371 (A,wt=25): 202 ((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2)) != (c1 * c2) * (c1 * (c2 * c1)).  [ur(40,b,49,a)].

given #372 (F,wt=21): 761 (c2 * c1) * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * c1.  [ur(41,b,88,a)].

given #373 (F,wt=21): 765 ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,88,a)].

given #374 (T,wt=21): 766 x * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,88,a)].

given #375 (T,wt=21): 767 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,96,a)].

given #376 (A,wt=27): 203 ((c1 * c2) * (c1 * (c2 * c1))) * (x * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [ur(15,b,49,a)].

given #377 (F,wt=21): 768 (c2 * c1) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(41,b,96,a)].

given #378 (F,wt=21): 772 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,96,a)].

given #379 (T,wt=21): 773 x * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,96,a)].

given #380 (T,wt=21): 830 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,97,a)].

given #381 (A,wt=31): 204 (c1 * (c1 * c2)) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * ((c1 * c2) * (c1 * (c2 * c1))).  [ur(14,b,49,a)].

given #382 (F,wt=21): 831 (c2 * c1) * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != c2 * c1.  [ur(41,b,97,a)].

given #383 (F,wt=21): 835 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,97,a)].

given #384 (T,wt=21): 836 x * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,97,a)].

given #385 (T,wt=21): 837 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,99,a)].

given #386 (A,wt=25): 209 (c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1))) != (c1 * c2) * (c2 * (c2 * c1)).  [ur(102,b,54,a)].

given #387 (F,wt=21): 838 (c1 * c2) * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != c1 * c2.  [ur(41,b,99,a)].

given #388 (F,wt=21): 841 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,99,a)].

given #389 (T,wt=21): 842 x * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,99,a)].

given #390 (T,wt=21): 888 (((c2 * (c2 * c1)) * x) * y) * z != (((c1 * c2) * x) * y) * z.  [ur(7,b,109,a)].

given #391 (A,wt=27): 211 ((c2 * c1) * (c2 * (c2 * c1))) * ((c2 * (c2 * (c2 * c1))) * (c1 * c2)) != c2 * (c2 * c1).  [ur(53,b,55,a)].

given #392 (F,wt=21): 889 x * (((c2 * (c2 * c1)) * y) * z) != x * (((c1 * c2) * y) * z).  [ur(6,b,109,a)].

given #393 (F,wt=21): 922 x * ((c2 * (c2 * c1)) * ((c1 * c2) * x)) != (c2 * (c2 * c1)) * x.  [ur(12,b,110,a)].

given #394 (T,wt=21): 923 (x * ((c2 * (c2 * c1)) * y)) * z != (x * ((c1 * c2) * y)) * z.  [ur(7,b,110,a)].

given #395 (T,wt=21): 924 x * (y * ((c2 * (c2 * c1)) * z)) != x * (y * ((c1 * c2) * z)).  [ur(6,b,110,a)].

given #396 (A,wt=27): 215 ((c1 * c2) * (c1 * (c1 * c2))) * ((c1 * (c1 * (c1 * c2))) * (c2 * c1)) != c1 * (c1 * c2).  [ur(53,b,17,a(flip))].

given #397 (F,wt=21): 1006 ((x * (c2 * (c2 * c1))) * y) * z != ((x * (c1 * c2)) * y) * z.  [ur(7,b,120,a)].

given #398 (F,wt=21): 1007 x * ((y * (c2 * (c2 * c1))) * z) != x * ((y * (c1 * c2)) * z).  [ur(6,b,120,a)].

given #399 (T,wt=21): 1043 (c2 * (c2 * c1)) * (x * (x * (c1 * c2))) != x * (c2 * (c2 * c1)).  [ur(12,b,121,a)].

given #400 (T,wt=21): 1044 (x * (y * (c2 * (c2 * c1)))) * z != (x * (y * (c1 * c2))) * z.  [ur(7,b,121,a)].

given #401 (A,wt=33): 218 ((c2 * c1) * x) * (((c1 * (c1 * c2)) * x) * ((c2 * c1) * x)) != ((c1 * (c1 * c2)) * x) * ((c2 * c1) * x).  [ur(102,b,26,a)].

given #402 (F,wt=21): 1045 x * (y * (z * (c2 * (c2 * c1)))) != x * (y * (z * (c1 * c2))).  [ur(6,b,121,a)].

given #403 (F,wt=21): 1118 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,131,a)].

given #404 (T,wt=21): 1120 (c1 * c2) * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != c1 * c2.  [ur(41,b,131,a)].

given #405 (T,wt=21): 1124 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,131,a)].

given #406 (A,wt=31): 220 (x * ((c2 * c1) * x)) * (((c1 * (c1 * c2)) * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(53,b,26,a)].

given #407 (F,wt=21): 1125 x * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,131,a)].

given #408 (F,wt=21): 1126 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2.  [ur(43,b,133,a)].

given #409 (T,wt=21): 1127 (c1 * c2) * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2.  [ur(41,b,133,a)].

given #410 (T,wt=21): 1133 ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) * x != (c1 * c2) * x.  [ur(7,b,133,a)].

given #411 (A,wt=27): 221 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c1 * (c1 * c2)) * x) * y.  [ur(43,b,26,a)].

given #412 (F,wt=21): 1134 x * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c1 * c2).  [ur(6,b,133,a)].

given #413 (F,wt=21): 1174 (((c1 * c2) * (c2 * (c2 * c1))) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,137,a)].

given #414 (T,wt=21): 1175 x * (((c1 * c2) * (c2 * (c2 * c1))) * y) != x * ((c1 * c2) * y).  [ur(6,b,137,a)].

given #415 (T,wt=21): 1199 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * y != (x * (c1 * c2)) * y.  [ur(7,b,138,a)].

given #416 (A,wt=25): 222 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c2 * c1) * x) * y.  [ur(42,b,26,a)].

given #417 (F,wt=21): 1200 x * (y * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (y * (c1 * c2)).  [ur(6,b,138,a)].

given #418 (F,wt=21): 1213 (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,138,a(flip))].

given #419 (T,wt=21): 1214 (c1 * (c1 * c2)) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * c2.  [ur(23,b,138,a(flip))].

given #420 (T,wt=21): 1288 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,139,a)].

given #421 (A,wt=27): 223 (((c1 * (c1 * c2)) * x) * y) * (((c2 * c1) * x) * y) != ((c1 * (c1 * c2)) * x) * y.  [ur(41,b,26,a)].

given #422 (F,wt=21): 1290 (c1 * c2) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != c1 * c2.  [ur(41,b,139,a)].

given #423 (F,wt=21): 1294 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,139,a)].

given #424 (T,wt=21): 1295 x * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,139,a)].

given #425 (T,wt=21): 1297 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(43,b,141,a)].

given #426 (A,wt=25): 224 (((c2 * c1) * x) * y) * (((c1 * (c1 * c2)) * x) * y) != ((c2 * c1) * x) * y.  [ur(40,b,26,a)].

given #427 (F,wt=21): 1299 (c1 * c2) * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2.  [ur(41,b,141,a)].

given #428 (F,wt=21): 1304 ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,141,a)].

given #429 (T,wt=21): 1305 x * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,141,a)].

given #430 (T,wt=21): 1354 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,145,a)].

given #431 (A,wt=33): 225 (((c1 * (c1 * c2)) * x) * (((c2 * c1) * x) * y)) * (y * (((c2 * c1) * x) * y)) != ((c2 * c1) * x) * y.  [ur(24,b,26,a)].

given #432 (F,wt=21): 1355 x * (((c2 * (c2 * c1)) * (c1 * c2)) * y) != x * ((c1 * c2) * y).  [ur(6,b,145,a)].

given #433 (F,wt=21): 1378 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * y != (x * (c1 * c2)) * y.  [ur(7,b,146,a)].

given #434 (T,wt=21): 1379 x * (y * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (y * (c1 * c2)).  [ur(6,b,146,a)].

given #435 (T,wt=21): 1394 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,146,a(flip))].

given #436 (A,wt=33): 226 (x * (x * ((c2 * c1) * y))) * (((c1 * (c1 * c2)) * y) * (x * ((c2 * c1) * y))) != x * ((c2 * c1) * y).  [ur(23,b,26,a)].

given #437 (F,wt=21): 1395 (c1 * (c1 * c2)) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * c2.  [ur(23,b,146,a(flip))].

given #438 (F,wt=21): 1446 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * (c2 * c1) != c2 * c1.  [ur(43,b,150,a)].

given #439 (T,wt=21): 1448 (c2 * c1) * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c2 * c1.  [ur(41,b,150,a)].

given #440 (T,wt=21): 1452 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * x != (c2 * c1) * x.  [ur(7,b,150,a)].

given #441 (A,wt=33): 227 (((c2 * c1) * x) * y) * (z * (z * (((c1 * (c1 * c2)) * x) * y))) != z * (((c1 * (c1 * c2)) * x) * y).  [ur(15,b,26,a)].

given #442 (F,wt=21): 1453 x * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != x * (c2 * c1).  [ur(6,b,150,a)].

given #443 (F,wt=21): 1454 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * (c1 * c2) != c1 * c2.  [ur(43,b,152,a)].

given #444 (T,wt=21): 1456 (c1 * c2) * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c1 * c2.  [ur(41,b,152,a)].

given #445 (T,wt=21): 1460 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * x != (c1 * c2) * x.  [ur(7,b,152,a)].

given #446 (A,wt=31): 228 (((c1 * (c1 * c2)) * x) * y) * (z * (z * (((c2 * c1) * x) * y))) != z * (((c2 * c1) * x) * y).  [ur(14,b,26,a)].

given #447 (F,wt=21): 1461 x * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != x * (c1 * c2).  [ur(6,b,152,a)].

given #448 (F,wt=21): 1519 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,164,a)].

given #449 (T,wt=21): 1521 (c2 * c1) * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != c2 * c1.  [ur(41,b,164,a)].

given #450 (T,wt=21): 1525 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,164,a)].

given #451 (A,wt=25): 229 x * (((c1 * (c1 * c2)) * y) * (((c2 * c1) * y) * x)) != ((c2 * c1) * y) * x.  [ur(12,b,26,a)].

given #452 (F,wt=21): 1526 x * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,164,a)].

given #453 (F,wt=21): 1527 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * (c2 * c1) != c2 * c1.  [ur(43,b,166,a)].

given #454 (T,wt=21): 1529 (c2 * c1) * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1.  [ur(41,b,166,a)].

given #455 (T,wt=21): 1533 ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) * x != (c2 * c1) * x.  [ur(7,b,166,a)].

given #456 (A,wt=35): 232 ((c1 * (c1 * c2)) * x) * (((c2 * c1) * x) * ((c1 * (c1 * c2)) * x)) != ((c2 * c1) * x) * ((c1 * (c1 * c2)) * x).  [ur(102,b,26,a(flip))].

given #457 (F,wt=21): 1534 x * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c2 * c1).  [ur(6,b,166,a)].

given #458 (F,wt=21): 1568 (((c1 * c2) * (c1 * (c2 * c1))) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,170,a)].

given #459 (T,wt=21): 1569 x * (((c1 * c2) * (c1 * (c2 * c1))) * y) != x * ((c2 * c1) * y).  [ur(6,b,170,a)].

given #460 (T,wt=21): 1595 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * y != (x * (c2 * c1)) * y.  [ur(7,b,171,a)].

given #461 (A,wt=37): 234 (x * ((c1 * (c1 * c2)) * x)) * (((c2 * c1) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(53,b,26,a(flip))].

given #462 (F,wt=21): 1596 x * (y * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (y * (c2 * c1)).  [ur(6,b,171,a)].

given #463 (F,wt=21): 1613 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,171,a(flip))].

given #464 (T,wt=21): 1614 (c2 * (c2 * c1)) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * c1.  [ur(23,b,171,a(flip))].

given #465 (T,wt=21): 1661 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,212,a)].

given #466 (A,wt=37): 235 (((c2 * c1) * x) * (((c1 * (c1 * c2)) * x) * y)) * (y * (((c1 * (c1 * c2)) * x) * y)) != ((c1 * (c1 * c2)) * x) * y.  [ur(24,b,26,a(flip))].

given #467 (F,wt=21): 1663 (c2 * c1) * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != c2 * c1.  [ur(41,b,212,a)].

given #468 (F,wt=21): 1667 ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,212,a)].

given #469 (T,wt=21): 1668 x * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,212,a)].

given #470 (T,wt=21): 1669 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(43,b,216,a)].

given #471 (A,wt=37): 236 (x * (x * ((c1 * (c1 * c2)) * y))) * (((c2 * c1) * y) * (x * ((c1 * (c1 * c2)) * y))) != x * ((c1 * (c1 * c2)) * y).  [ur(23,b,26,a(flip))].

given #472 (F,wt=21): 1671 (c1 * c2) * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != c1 * c2.  [ur(41,b,216,a)].

given #473 (F,wt=21): 1675 ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,216,a)].

given #474 (T,wt=21): 1676 x * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,216,a)].

given #475 (T,wt=21): 1705 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c1 * c2) != c1 * c2.  [ur(43,b,541,a)].

given #476 (A,wt=27): 237 x * (((c2 * c1) * y) * (((c1 * (c1 * c2)) * y) * x)) != ((c1 * (c1 * c2)) * y) * x.  [ur(12,b,26,a(flip))].

given #477 (F,wt=21): 1707 (c1 * c2) * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2.  [ur(41,b,541,a)].

given #478 (F,wt=21): 1711 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * x != (c1 * c2) * x.  [ur(7,b,541,a)].

given #479 (T,wt=21): 1712 x * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c1 * c2).  [ur(6,b,541,a)].

given #480 (T,wt=21): 1713 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c2 * c1) != c2 * c1.  [ur(43,b,648,a)].

given #481 (A,wt=23): 238 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * y != (x * (c2 * c1)) * y.  [para(5(a,1),26(a,1,1)),flip(a)].

given #482 (F,wt=21): 1715 (c2 * c1) * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1.  [ur(41,b,648,a)].

given #483 (F,wt=21): 1719 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * x != (c2 * c1) * x.  [ur(7,b,648,a)].

given #484 (T,wt=21): 1720 x * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c2 * c1).  [ur(6,b,648,a)].

given #485 (T,wt=21): 1771 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c2 * c1) != c2 * c1.  [ur(43,b,746,a)].

given #486 (A,wt=25): 239 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * y != (x * (c1 * (c1 * c2))) * y.  [para(5(a,1),26(a,2,1))].

given #487 (F,wt=21): 1773 (c2 * c1) * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1.  [ur(41,b,746,a)].

given #488 (F,wt=21): 1777 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * x != (c2 * c1) * x.  [ur(7,b,746,a)].

given #489 (T,wt=21): 1778 x * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c2 * c1).  [ur(6,b,746,a)].

given #490 (T,wt=21): 1779 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c1 * c2) != c1 * c2.  [ur(43,b,1215,a)].

given #491 (A,wt=31): 240 ((c1 * (c1 * c2)) * (x * (c2 * c1))) * ((x * (x * (c2 * c1))) * (x * (c2 * c1))) != x * (c2 * c1).  [para(21(a,1),26(a,1)),flip(a)].

given #492 (F,wt=21): 1781 (c1 * c2) * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2.  [ur(41,b,1215,a)].

given #493 (F,wt=21): 1785 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * x != (c1 * c2) * x.  [ur(7,b,1215,a)].

given #494 (T,wt=21): 1786 x * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c1 * c2).  [ur(6,b,1215,a)].

given #495 (T,wt=21): 1833 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c1 * c2) != c1 * c2.  [ur(43,b,1396,a)].

given #496 (A,wt=37): 241 ((c2 * c1) * (x * (c1 * (c1 * c2)))) * ((x * (x * (c1 * (c1 * c2)))) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [para(21(a,1),26(a,2))].

given #497 (F,wt=21): 1835 (c1 * c2) * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2.  [ur(41,b,1396,a)].

given #498 (F,wt=21): 1839 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * x != (c1 * c2) * x.  [ur(7,b,1396,a)].

given #499 (T,wt=21): 1840 x * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c1 * c2).  [ur(6,b,1396,a)].

NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 103 (0.00 of 9.04 sec).

given #500 (T,wt=21): 1841 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c2 * c1) != c2 * c1.  [ur(43,b,1615,a)].

given #501 (A,wt=25): 245 ((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1)) != (c2 * (c2 * c1)) * (c1 * c2).  [ur(40,b,59,a)].

given #502 (F,wt=21): 1843 (c2 * c1) * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c2 * c1.  [ur(41,b,1615,a)].

given #503 (F,wt=21): 1847 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * x != (c2 * c1) * x.  [ur(7,b,1615,a)].

given #504 (T,wt=21): 1848 x * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c2 * c1).  [ur(6,b,1615,a)].

given #505 (T,wt=21): 2233 (c1 * c2) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * (c1 * c2).  [ur(12,b,178,a(flip))].

given #506 (A,wt=27): 246 ((c2 * (c2 * c1)) * (c1 * c2)) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(15,b,59,a)].

given #507 (F,wt=21): 2321 (c1 * c2) * (c1 * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * (c1 * c2).  [ur(12,b,196,a(flip))].

given #508 (F,wt=21): 2470 (c1 * c2) * (c1 * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * (c1 * c2).  [ur(12,b,206,a(flip))].

given #509 (T,wt=21): 2576 (c2 * c1) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * (c2 * c1).  [ur(12,b,249,a(flip))].

given #510 (T,wt=21): 2701 (c2 * c1) * (c2 * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * (c2 * c1).  [ur(12,b,257,a(flip))].

given #511 (A,wt=31): 247 (c2 * (c2 * c1)) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * ((c2 * (c2 * c1)) * (c1 * c2)).  [ur(14,b,59,a)].

given #512 (F,wt=21): 2869 (c2 * c1) * (c2 * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * (c2 * c1).  [ur(12,b,297,a(flip))].

given #513 (F,wt=21): 3390 c1 * ((c2 * (c2 * (c2 * c1))) * ((c2 * c1) * (c1 * c2))) != c2 * c1.  [ur(12,b,148,a(flip))].

given #514 (T,wt=21): 3694 c2 * ((c1 * (c1 * (c1 * c2))) * ((c1 * c2) * (c2 * c1))) != c1 * c2.  [ur(12,b,154,a(flip))].

given #515 (T,wt=21): 3907 c1 * ((c2 * (c1 * c2)) * ((c2 * c1) * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,157,a(flip))].

given #516 (A,wt=27): 254 ((c1 * c2) * (c2 * (c2 * c1))) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(15,b,92,a)].

given #517 (F,wt=21): 4007 c2 * ((c1 * (c2 * c1)) * ((c1 * c2) * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,161,a(flip))].

given #518 (F,wt=21): 4016 c2 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,172,a(flip))].

given #519 (T,wt=21): 4025 c2 * ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * (c2 * c1))) != c1 * c2.  [ur(12,b,173,a(flip))].

given #520 (T,wt=21): 4033 c2 * (((c2 * c1) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,190,a(flip))].

given #521 (A,wt=31): 255 (c2 * (c2 * c1)) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * ((c1 * c2) * (c2 * (c2 * c1))).  [ur(14,b,92,a)].

given #522 (F,wt=21): 4054 c2 * ((c1 * (c1 * c2)) * ((c2 * c1) * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,192,a(flip))].

given #523 (F,wt=21): 4063 c2 * (((c1 * c2) * (c1 * (c2 * c1))) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,199,a(flip))].

given #524 (T,wt=21): 4072 c2 * ((c1 * (c1 * c2)) * ((c1 * c2) * (c1 * (c2 * c1)))) != c1 * c2.  [ur(12,b,201,a(flip))].

given #525 (T,wt=21): 4221 c1 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,243,a(flip))].

given #526 (A,wt=27): 260 ((c2 * c1) * (c1 * c2)) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * (c2 * c1).  [ur(76,b,55,a)].

given #527 (F,wt=21): 4230 c1 * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c1 * c2))) != c2 * c1.  [ur(12,b,244,a(flip))].

given #528 (F,wt=21): 4238 c1 * (((c1 * c2) * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,252,a(flip))].

given #529 (T,wt=21): 4247 c1 * ((c2 * (c2 * c1)) * ((c1 * c2) * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,253,a(flip))].

given #530 (T,wt=21): 4438 c1 * (((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,290,a(flip))].

given #531 (A,wt=37): 261 ((c1 * c2) * (x * (c2 * (c2 * c1)))) * ((x * (x * (c2 * (c2 * c1)))) * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(76,b,54,a)].

given #532 (F,wt=21): 4447 c1 * ((c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2)))) != c2 * c1.  [ur(12,b,292,a(flip))].

given #533 (F,wt=21): 5191 c2 * (c1 * ((c1 * c2) * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2.  [ur(12,b,578,a(flip))].

given #534 (T,wt=21): 5529 c1 * (c2 * ((c2 * c1) * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1.  [ur(12,b,655,a(flip))].

given #535 (T,wt=21): 5827 c1 * (c2 * ((c2 * c1) * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1.  [ur(12,b,766,a(flip))].

given #536 (A,wt=41): 262 (((c1 * (c1 * c2)) * x) * (y * ((c2 * c1) * x))) * ((y * (y * ((c2 * c1) * x))) * (y * ((c2 * c1) * x))) != y * ((c2 * c1) * x).  [ur(76,b,26,a)].

given #537 (F,wt=21): 5936 c1 * (c2 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * c1))) != c2 * c1.  [ur(12,b,773,a(flip))].

given #538 (F,wt=21): 6038 c1 * (c2 * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * c1))) != c2 * c1.  [ur(12,b,836,a(flip))].

given #539 (T,wt=21): 6127 c2 * (c1 * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * c2))) != c1 * c2.  [ur(12,b,842,a(flip))].

given #540 (T,wt=21): 6748 c2 * (c1 * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * c2))) != c1 * c2.  [ur(12,b,1125,a(flip))].

given #541 (A,wt=31): 265 ((c2 * (c2 * c1)) * (x * (c1 * c2))) * ((x * (x * (c1 * c2))) * (x * (c1 * c2))) != x * (c1 * c2).  [ur(76,b,54,a(flip))].

given #542 (F,wt=21): 6844 c2 * (c1 * ((c1 * c2) * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2.  [ur(12,b,1134,a(flip))].

given #543 (F,wt=21): 7125 c2 * (c1 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * c2))) != c1 * c2.  [ur(12,b,1295,a(flip))].

given #544 (T,wt=21): 7218 c2 * (c1 * ((c1 * c2) * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2.  [ur(12,b,1305,a(flip))].

given #545 (T,wt=21): 7497 c1 * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != c2 * c1.  [ur(12,b,1453,a(flip))].

given #546 (A,wt=47): 266 (((c2 * c1) * x) * (y * ((c1 * (c1 * c2)) * x))) * ((y * (y * ((c1 * (c1 * c2)) * x))) * (y * ((c1 * (c1 * c2)) * x))) != y * ((c1 * (c1 * c2)) * x).  [ur(76,b,26,a(flip))].

given #547 (F,wt=21): 7583 c2 * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != c1 * c2.  [ur(12,b,1461,a(flip))].

given #548 (F,wt=21): 7669 c1 * (c2 * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * c1))) != c2 * c1.  [ur(12,b,1526,a(flip))].

given #549 (T,wt=21): 7746 c1 * (c2 * ((c2 * c1) * ((c1 * c2) * (c1 * (c2 * c1))))) != c2 * c1.  [ur(12,b,1534,a(flip))].

given #550 (T,wt=21): 7972 c1 * (c2 * ((c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)))) != c2 * c1.  [ur(12,b,1668,a(flip))].

given #551 (A,wt=27): 267 ((c1 * c2) * (c2 * c1)) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(76,b,17,a(flip))].

given #552 (F,wt=21): 8049 c2 * (c1 * ((c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)))) != c1 * c2.  [ur(12,b,1676,a(flip))].

given #553 (F,wt=21): 8129 c2 * (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) != c1 * c2.  [ur(12,b,1712,a(flip))].

given #554 (T,wt=21): 8208 c1 * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != c2 * c1.  [ur(12,b,1720,a(flip))].

given #555 (T,wt=21): 8279 c1 * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != c2 * c1.  [ur(12,b,1778,a(flip))].

given #556 (A,wt=31): 270 (x * ((c1 * (c1 * c2)) * x)) * (((c2 * c1) * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(76,b,27,a)].

given #557 (F,wt=21): 8348 c2 * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != c1 * c2.  [ur(12,b,1786,a(flip))].

given #558 (F,wt=21): 8412 c2 * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != c1 * c2.  [ur(12,b,1840,a(flip))].

given #559 (T,wt=21): 8479 c1 * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != c2 * c1.  [ur(12,b,1848,a(flip))].

given #560 (T,wt=21): 8489 c2 * ((c1 * c2) * (c1 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2.  [ur(12,b,2233,a(flip))].

given #561 (A,wt=31): 271 (x * ((c2 * c1) * x)) * (((c2 * c1) * ((c2 * c1) * x)) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x.  [ur(53,b,27,a)].

given #562 (F,wt=21): 8514 c2 * ((c1 * c2) * (c1 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2.  [ur(12,b,2321,a(flip))].

given #563 (F,wt=21): 8524 c2 * ((c1 * c2) * (c1 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2.  [ur(12,b,2470,a(flip))].

given #564 (T,wt=21): 8534 c1 * ((c2 * c1) * (c2 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1.  [ur(12,b,2576,a(flip))].

given #565 (T,wt=21): 8544 c1 * ((c2 * c1) * (c2 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1.  [ur(12,b,2701,a(flip))].

given #566 (A,wt=27): 272 (x * ((c2 * c1) * y)) * (x * ((c1 * (c1 * c2)) * y)) != x * ((c1 * (c1 * c2)) * y).  [ur(43,b,27,a)].

given #567 (F,wt=21): 8564 c1 * ((c2 * c1) * (c2 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1.  [ur(12,b,2869,a(flip))].

given #568 (F,wt=23): 288 x * ((c1 * (c1 * c2)) * (y * (y * (c2 * c1)))) != x * (y * (c2 * c1)).  [para(5(a,1),27(a,1,2)),flip(a)].

given #569 (T,wt=23): 329 ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,28,a(flip))].

given #570 (T,wt=23): 330 (c2 * (c2 * c1)) * ((c1 * (c1 * c2)) * (c1 * (c1 * (c2 * c1)))) != c2 * c1.  [ur(23,b,28,a(flip))].

given #571 (A,wt=25): 273 (x * ((c1 * (c1 * c2)) * y)) * (x * ((c2 * c1) * y)) != x * ((c2 * c1) * y).  [ur(42,b,27,a)].

given #572 (F,wt=23): 380 (c1 * c2) * ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2))))) != c1 * (c1 * c2).  [ur(12,b,29,a(flip))].

given #573 (F,wt=23): 490 (x * ((c1 * (c1 * c2)) * ((c2 * c1) * x))) * y != ((c2 * c1) * x) * y.  [ur(7,b,48,a)].

given #574 (T,wt=23): 491 x * (y * ((c1 * (c1 * c2)) * ((c2 * c1) * y))) != x * ((c2 * c1) * y).  [ur(6,b,48,a)].

given #575 (T,wt=23): 499 (((c2 * c1) * (c2 * (c1 * c2))) * x) * ((c1 * c2) * x) != (c1 * c2) * x.  [ur(43,b,56,a)].

given #576 (A,wt=27): 274 (x * ((c1 * (c1 * c2)) * y)) * (x * ((c2 * c1) * y)) != x * ((c1 * (c1 * c2)) * y).  [ur(41,b,27,a)].

given #577 (F,wt=23): 501 ((c1 * c2) * x) * (((c2 * c1) * (c2 * (c1 * c2))) * x) != (c1 * c2) * x.  [ur(41,b,56,a)].

given #578 (F,wt=23): 515 x * (((c2 * c1) * (c2 * (c1 * c2))) * ((c1 * c2) * x)) != (c1 * c2) * x.  [ur(12,b,56,a(flip))].

given #579 (T,wt=23): 522 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * (x * (c1 * c2)) != x * (c1 * c2).  [ur(43,b,57,a)].

given #580 (T,wt=23): 524 (x * (c1 * c2)) * (x * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (c1 * c2).  [ur(41,b,57,a)].

given #581 (A,wt=25): 275 (x * ((c2 * c1) * y)) * (x * ((c1 * (c1 * c2)) * y)) != x * ((c2 * c1) * y).  [ur(40,b,27,a)].

given #582 (F,wt=23): 530 (c2 * (c1 * c2)) * ((c2 * c1) * (c1 * c2)) != (c2 * c1) * (c2 * (c1 * c2)).  [ur(12,b,57,a)].

given #583 (F,wt=23): 581 (((c2 * c1) * (c1 * (c1 * c2))) * x) * ((c2 * c1) * x) != (c2 * c1) * x.  [ur(43,b,80,a)].

given #584 (T,wt=23): 583 ((c2 * c1) * x) * (((c2 * c1) * (c1 * (c1 * c2))) * x) != (c2 * c1) * x.  [ur(41,b,80,a)].

given #585 (T,wt=23): 597 x * (((c2 * c1) * (c1 * (c1 * c2))) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(12,b,80,a(flip))].

given #586 (A,wt=25): 276 ((c2 * c1) * ((c1 * (c1 * c2)) * x)) * (x * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(24,b,27,a)].

given #587 (F,wt=23): 628 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * (x * (c2 * c1)) != x * (c2 * c1).  [ur(43,b,81,a)].

given #588 (F,wt=23): 630 (x * (c2 * c1)) * (x * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (c2 * c1).  [ur(41,b,81,a)].

given #589 (T,wt=23): 688 ((x * (c2 * c1)) * (x * (c1 * (c1 * c2)))) * y != (x * (c2 * c1)) * y.  [ur(7,b,61,a)].

given #590 (T,wt=23): 689 x * ((y * (c2 * c1)) * (y * (c1 * (c1 * c2)))) != x * (y * (c2 * c1)).  [ur(6,b,61,a)].

given #591 (A,wt=25): 277 ((c2 * c1) * ((c2 * c1) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x.  [ur(23,b,27,a)].

given #592 (F,wt=23): 698 (c2 * (c2 * c1)) * ((c1 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c2 * c1.  [ur(23,b,61,a(flip))].

given #593 (F,wt=23): 701 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * ((c2 * c1) * x) != (c2 * c1) * x.  [ur(43,b,86,a)].

given #594 (T,wt=23): 703 ((c2 * c1) * x) * (((c1 * (c1 * c2)) * (c2 * c1)) * x) != (c2 * c1) * x.  [ur(41,b,86,a)].

given #595 (T,wt=23): 717 x * (((c1 * (c1 * c2)) * (c2 * c1)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(12,b,86,a(flip))].

given #596 (A,wt=33): 278 (x * ((c2 * c1) * y)) * (z * (z * (x * ((c1 * (c1 * c2)) * y)))) != z * (x * ((c1 * (c1 * c2)) * y)).  [ur(15,b,27,a)].

given #597 (F,wt=23): 726 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * (x * (c2 * c1)) != x * (c2 * c1).  [ur(43,b,87,a)].

given #598 (F,wt=23): 728 (x * (c2 * c1)) * (x * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (c2 * c1).  [ur(41,b,87,a)].

given #599 (T,wt=23): 754 (((c2 * c1) * x) * ((c1 * (c1 * c2)) * x)) * y != ((c2 * c1) * x) * y.  [ur(7,b,62,a)].

given #600 (T,wt=23): 755 x * (((c2 * c1) * y) * ((c1 * (c1 * c2)) * y)) != x * ((c2 * c1) * y).  [ur(6,b,62,a)].

given #601 (A,wt=31): 279 (x * ((c1 * (c1 * c2)) * y)) * (z * (z * (x * ((c2 * c1) * y)))) != z * (x * ((c2 * c1) * y)).  [ur(14,b,27,a)].

given #602 (F,wt=23): 829 (c1 * c2) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c2 * c1))) != c1 * (c1 * c2).  [ur(12,b,65,a(flip))].

given #603 (F,wt=23): 903 ((c2 * (c2 * c1)) * (x * (x * (c1 * c2)))) * y != (x * (c1 * c2)) * y.  [para(5(a,1),109(a,2,1))].

given #604 (T,wt=23): 939 x * ((c2 * (c2 * c1)) * (y * (y * (c1 * c2)))) != x * (y * (c1 * c2)).  [para(5(a,1),110(a,2,2))].

given #605 (T,wt=23): 983 (c2 * c1) * ((c1 * c2) * (c2 * (c2 * (c2 * (c2 * c1))))) != c2 * (c2 * c1).  [ur(12,b,68,a(flip))].

given #606 (A,wt=37): 283 (x * ((c2 * c1) * x)) * (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(76,b,27,a(flip))].

given #607 (F,wt=23): 1165 (((c1 * c2) * (c2 * (c2 * c1))) * x) * ((c1 * c2) * x) != (c1 * c2) * x.  [ur(43,b,137,a)].

given #608 (F,wt=23): 1167 ((c1 * c2) * x) * (((c1 * c2) * (c2 * (c2 * c1))) * x) != (c1 * c2) * x.  [ur(41,b,137,a)].

given #609 (T,wt=23): 1179 x * (((c1 * c2) * (c2 * (c2 * c1))) * ((c1 * c2) * x)) != (c1 * c2) * x.  [ur(12,b,137,a(flip))].

given #610 (T,wt=23): 1192 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * (x * (c1 * c2)) != x * (c1 * c2).  [ur(43,b,138,a)].

given #611 (A,wt=37): 284 (x * ((c1 * (c1 * c2)) * x)) * (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x.  [ur(53,b,27,a(flip))].

given #612 (F,wt=23): 1194 (x * (c1 * c2)) * (x * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (c1 * c2).  [ur(41,b,138,a)].

given #613 (F,wt=23): 1340 ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,72,a(flip))].

given #614 (T,wt=23): 1341 (c1 * (c1 * c2)) * ((c2 * (c2 * c1)) * (c2 * (c2 * (c1 * c2)))) != c1 * c2.  [ur(23,b,72,a(flip))].

given #615 (T,wt=23): 1345 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * ((c1 * c2) * x) != (c1 * c2) * x.  [ur(43,b,145,a)].

given #616 (A,wt=29): 285 ((c1 * (c1 * c2)) * ((c2 * c1) * x)) * (x * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(24,b,27,a(flip))].

given #617 (F,wt=23): 1347 ((c1 * c2) * x) * (((c2 * (c2 * c1)) * (c1 * c2)) * x) != (c1 * c2) * x.  [ur(41,b,145,a)].

given #618 (F,wt=23): 1359 x * (((c2 * (c2 * c1)) * (c1 * c2)) * ((c1 * c2) * x)) != (c1 * c2) * x.  [ur(12,b,145,a(flip))].

given #619 (T,wt=23): 1371 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * (x * (c1 * c2)) != x * (c1 * c2).  [ur(43,b,146,a)].

given #620 (T,wt=23): 1373 (x * (c1 * c2)) * (x * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (c1 * c2).  [ur(41,b,146,a)].

given #621 (A,wt=29): 286 ((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * (x * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x.  [ur(23,b,27,a(flip))].

given #622 (F,wt=23): 1445 c2 * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,73,a(flip))].

given #623 (F,wt=23): 1559 (((c1 * c2) * (c1 * (c2 * c1))) * x) * ((c2 * c1) * x) != (c2 * c1) * x.  [ur(43,b,170,a)].

given #624 (T,wt=23): 1561 ((c2 * c1) * x) * (((c1 * c2) * (c1 * (c2 * c1))) * x) != (c2 * c1) * x.  [ur(41,b,170,a)].

given #625 (T,wt=23): 1573 x * (((c1 * c2) * (c1 * (c2 * c1))) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(12,b,170,a(flip))].

given #626 (A,wt=25): 289 x * ((c2 * c1) * (y * (y * (c1 * (c1 * c2))))) != x * (y * (c1 * (c1 * c2))).  [para(5(a,1),27(a,2,2))].

given #627 (F,wt=23): 1586 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * (x * (c2 * c1)) != x * (c2 * c1).  [ur(43,b,171,a)].

given #628 (F,wt=23): 1588 (x * (c2 * c1)) * (x * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (c2 * c1).  [ur(41,b,171,a)].

given #629 (T,wt=23): 1594 (c1 * (c2 * c1)) * ((c1 * c2) * (c2 * c1)) != (c1 * c2) * (c1 * (c2 * c1)).  [ur(12,b,171,a)].

given #630 (T,wt=23): 1770 c1 * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,83,a(flip))].

given #631 (A,wt=25): 291 (c2 * (c2 * c1)) * ((c2 * c1) * (c2 * (c1 * c2))) != (c2 * c1) * (c2 * (c1 * c2)).  [ur(42,b,119,a)].

given #632 (F,wt=23): 1883 c1 * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,89,a(flip))].

given #633 (F,wt=23): 1888 ((x * (c1 * (c1 * c2))) * (x * (c2 * c1))) * y != (x * (c2 * c1)) * y.  [ur(7,b,94,a)].

given #634 (T,wt=23): 1889 x * ((y * (c1 * (c1 * c2))) * (y * (c2 * c1))) != x * (y * (c2 * c1)).  [ur(6,b,94,a)].

given #635 (T,wt=23): 1910 (c2 * (c2 * c1)) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c2 * c1))) != c2 * c1.  [ur(23,b,94,a(flip))].

given #636 (A,wt=25): 293 ((c2 * c1) * (c2 * (c1 * c2))) * (c2 * (c2 * c1)) != (c2 * c1) * (c2 * (c1 * c2)).  [ur(40,b,119,a)].

given #637 (F,wt=23): 1915 (((c1 * (c1 * c2)) * x) * ((c2 * c1) * x)) * y != ((c2 * c1) * x) * y.  [ur(7,b,95,a)].

given #638 (F,wt=23): 1916 x * (((c1 * (c1 * c2)) * y) * ((c2 * c1) * y)) != x * ((c2 * c1) * y).  [ur(6,b,95,a)].

given #639 (T,wt=23): 1973 (((c1 * c2) * x) * ((c2 * (c2 * c1)) * x)) * y != ((c1 * c2) * x) * y.  [ur(7,b,104,a)].

given #640 (T,wt=23): 1974 x * (((c1 * c2) * y) * ((c2 * (c2 * c1)) * y)) != x * ((c1 * c2) * y).  [ur(6,b,104,a)].

given #641 (A,wt=27): 294 ((c2 * c1) * (c2 * (c1 * c2))) * (x * (x * (c2 * (c2 * c1)))) != x * (c2 * (c2 * c1)).  [ur(15,b,119,a)].

given #642 (F,wt=23): 1984 (((c2 * (c2 * c1)) * x) * ((c1 * c2) * x)) * y != ((c1 * c2) * x) * y.  [ur(7,b,111,a)].

given #643 (F,wt=23): 1985 x * (((c2 * (c2 * c1)) * y) * ((c1 * c2) * y)) != x * ((c1 * c2) * y).  [ur(6,b,111,a)].

given #644 (T,wt=23): 2012 (x * ((c2 * (c2 * c1)) * ((c1 * c2) * x))) * y != ((c1 * c2) * x) * y.  [ur(7,b,112,a)].

given #645 (T,wt=23): 2013 x * (y * ((c2 * (c2 * c1)) * ((c1 * c2) * y))) != x * ((c1 * c2) * y).  [ur(6,b,112,a)].

given #646 (A,wt=31): 295 (c2 * (c2 * c1)) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * ((c2 * c1) * (c2 * (c1 * c2))).  [ur(14,b,119,a)].

given #647 (F,wt=23): 2023 ((x * (c1 * c2)) * (x * (c2 * (c2 * c1)))) * y != (x * (c1 * c2)) * y.  [ur(7,b,115,a)].

given #648 (F,wt=23): 2024 x * ((y * (c1 * c2)) * (y * (c2 * (c2 * c1)))) != x * (y * (c1 * c2)).  [ur(6,b,115,a)].

given #649 (T,wt=23): 2047 (c1 * (c1 * c2)) * ((c2 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c1 * c2.  [ur(23,b,115,a(flip))].

given #650 (T,wt=23): 2092 (c1 * c2) * ((c1 * (c2 * c1)) * (c1 * (c1 * (c1 * c2)))) != c1 * (c1 * c2).  [ur(12,b,100,a(flip))].

given #651 (A,wt=27): 301 (c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) != c2 * ((c1 * (c1 * c2)) * (c2 * c1)).  [ur(42,b,180,a)].

given #652 (F,wt=23): 2098 ((x * (c2 * (c2 * c1))) * (x * (c1 * c2))) * y != (x * (c1 * c2)) * y.  [ur(7,b,122,a)].

given #653 (F,wt=23): 2099 x * ((y * (c2 * (c2 * c1))) * (y * (c1 * c2))) != x * (y * (c1 * c2)).  [ur(6,b,122,a)].

given #654 (T,wt=23): 2123 (c1 * (c1 * c2)) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c1 * c2))) != c1 * c2.  [ur(23,b,122,a(flip))].

given #655 (T,wt=23): 2134 (((c1 * (c1 * c2)) * (c2 * c1)) * x) * y != ((c1 * (c1 * c2)) * x) * y.  [ur(7,b,177,a)].

given #656 (A,wt=27): 303 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2) != c2 * ((c1 * (c1 * c2)) * (c2 * c1)).  [ur(40,b,180,a)].

given #657 (F,wt=23): 2135 x * (((c1 * (c1 * c2)) * (c2 * c1)) * y) != x * ((c1 * (c1 * c2)) * y).  [ur(6,b,177,a)].

given #658 (F,wt=23): 2140 (c2 * (c1 * c2)) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c1 * c2)) != c1 * c2.  [ur(53,b,177,a(flip))].

given #659 (T,wt=23): 2205 (x * ((c1 * (c1 * c2)) * (c2 * c1))) * y != (x * (c1 * (c1 * c2))) * y.  [ur(7,b,178,a)].

given #660 (T,wt=23): 2206 x * (y * ((c1 * (c1 * c2)) * (c2 * c1))) != x * (y * (c1 * (c1 * c2))).  [ur(6,b,178,a)].

given #661 (A,wt=25): 304 (c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(15,b,180,a)].

given #662 (F,wt=23): 2234 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(43,b,179,a)].

given #663 (F,wt=23): 2236 (c1 * c2) * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) != c1 * c2.  [ur(41,b,179,a)].

given #664 (T,wt=23): 2240 (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,179,a)].

given #665 (T,wt=23): 2241 x * (((c1 * (c1 * c2)) * (c2 * c1)) * (c2 * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,179,a)].

given #666 (A,wt=33): 305 (c1 * c2) * (x * (x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))).  [ur(14,b,180,a)].

given #667 (F,wt=23): 2265 (((c2 * c1) * (c1 * (c1 * c2))) * x) * y != ((c1 * (c1 * c2)) * x) * y.  [ur(7,b,195,a)].

given #668 (F,wt=23): 2266 x * (((c2 * c1) * (c1 * (c1 * c2))) * y) != x * ((c1 * (c1 * c2)) * y).  [ur(6,b,195,a)].

given #669 (T,wt=23): 2270 (c2 * (c1 * c2)) * (((c2 * c1) * (c1 * (c1 * c2))) * (c1 * c2)) != c1 * c2.  [ur(53,b,195,a(flip))].

given #670 (T,wt=23): 2293 (x * ((c2 * c1) * (c1 * (c1 * c2)))) * y != (x * (c1 * (c1 * c2))) * y.  [ur(7,b,196,a)].

given #671 (A,wt=33): 309 ((c2 * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) * (((c2 * c1) * (c2 * (c2 * c1))) * (c1 * c2)) != c2 * (c2 * c1).  [ur(126,b,55,a)].

given #672 (F,wt=23): 2294 x * (y * ((c2 * c1) * (c1 * (c1 * c2)))) != x * (y * (c1 * (c1 * c2))).  [ur(6,b,196,a)].

given #673 (F,wt=23): 2361 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(43,b,197,a)].

given #674 (T,wt=23): 2363 (c1 * c2) * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) != c1 * c2.  [ur(41,b,197,a)].

given #675 (T,wt=23): 2367 (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,197,a)].

given #676 (A,wt=37): 310 (((c2 * c1) * ((c2 * c1) * x)) * ((c2 * c1) * x)) * ((x * ((c2 * c1) * x)) * ((c1 * (c1 * c2)) * x)) != (c2 * c1) * x.  [ur(126,b,27,a)].

given #677 (F,wt=23): 2368 x * (((c2 * c1) * (c1 * (c1 * c2))) * (c2 * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,197,a)].

given #678 (F,wt=23): 2381 (((c1 * c2) * (c1 * (c2 * c1))) * x) * y != ((c1 * (c1 * c2)) * x) * y.  [ur(7,b,205,a)].

given #679 (T,wt=23): 2382 x * (((c1 * c2) * (c1 * (c2 * c1))) * y) != x * ((c1 * (c1 * c2)) * y).  [ur(6,b,205,a)].

given #680 (T,wt=23): 2387 (c2 * (c1 * c2)) * (((c1 * c2) * (c1 * (c2 * c1))) * (c1 * c2)) != c1 * c2.  [ur(53,b,205,a(flip))].

given #681 (A,wt=37): 311 ((x * (x * (c2 * c1))) * (x * (c2 * c1))) * (((c1 * (c1 * c2)) * (x * (c2 * c1))) * (x * (c2 * c1))) != x * (c2 * c1).  [ur(126,b,26,a)].

given #682 (F,wt=23): 2442 (x * ((c1 * c2) * (c1 * (c2 * c1)))) * y != (x * (c1 * (c1 * c2))) * y.  [ur(7,b,206,a)].

given #683 (F,wt=23): 2443 x * (y * ((c1 * c2) * (c1 * (c2 * c1)))) != x * (y * (c1 * (c1 * c2))).  [ur(6,b,206,a)].

given #684 (T,wt=23): 2471 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) * (c1 * c2) != c1 * c2.  [ur(43,b,207,a)].

given #685 (T,wt=23): 2473 (c1 * c2) * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) != c1 * c2.  [ur(41,b,207,a)].

given #686 (A,wt=25): 312 ((c2 * (c2 * c1)) * (c2 * c1)) * ((c1 * (c2 * c1)) * (c1 * (c1 * c2))) != c2 * c1.  [ur(126,b,17,a)].

given #687 (F,wt=23): 2477 (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) * x != (c1 * c2) * x.  [ur(7,b,207,a)].

given #688 (F,wt=23): 2478 x * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c1 * c2))) != x * (c1 * c2).  [ur(6,b,207,a)].

given #689 (T,wt=23): 2519 (((c2 * (c2 * c1)) * (c1 * c2)) * x) * y != ((c2 * (c2 * c1)) * x) * y.  [ur(7,b,248,a)].

given #690 (T,wt=23): 2520 x * (((c2 * (c2 * c1)) * (c1 * c2)) * y) != x * ((c2 * (c2 * c1)) * y).  [ur(6,b,248,a)].

given #691 (A,wt=25): 313 ((c1 * (c1 * c2)) * (c1 * c2)) * ((c2 * (c1 * c2)) * (c2 * (c2 * c1))) != c1 * c2.  [ur(126,b,55,a(flip))].

given #692 (F,wt=23): 2525 (c1 * (c2 * c1)) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c2 * c1)) != c2 * c1.  [ur(53,b,248,a(flip))].

given #693 (F,wt=23): 2548 (x * ((c2 * (c2 * c1)) * (c1 * c2))) * y != (x * (c2 * (c2 * c1))) * y.  [ur(7,b,249,a)].

given #694 (T,wt=23): 2549 x * (y * ((c2 * (c2 * c1)) * (c1 * c2))) != x * (y * (c2 * (c2 * c1))).  [ur(6,b,249,a)].

given #695 (T,wt=23): 2603 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,250,a)].

given #696 (A,wt=45): 314 (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) * ((x * ((c1 * (c1 * c2)) * x)) * ((c2 * c1) * x)) != (c1 * (c1 * c2)) * x.  [ur(126,b,27,a(flip))].

given #697 (F,wt=23): 2605 (c2 * c1) * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) != c2 * c1.  [ur(41,b,250,a)].

given #698 (F,wt=23): 2609 (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,250,a)].

given #699 (T,wt=23): 2610 x * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,250,a)].

given #700 (T,wt=23): 2622 (((c1 * c2) * (c2 * (c2 * c1))) * x) * y != ((c2 * (c2 * c1)) * x) * y.  [ur(7,b,256,a)].

given #701 (A,wt=45): 315 ((x * (x * (c1 * (c1 * c2)))) * (x * (c1 * (c1 * c2)))) * (((c2 * c1) * (x * (c1 * (c1 * c2)))) * (x * (c1 * (c1 * c2)))) != x * (c1 * (c1 * c2)).  [ur(126,b,26,a(flip))].

given #702 (F,wt=23): 2623 x * (((c1 * c2) * (c2 * (c2 * c1))) * y) != x * ((c2 * (c2 * c1)) * y).  [ur(6,b,256,a)].

given #703 (F,wt=23): 2627 (c1 * (c2 * c1)) * (((c1 * c2) * (c2 * (c2 * c1))) * (c2 * c1)) != c2 * c1.  [ur(53,b,256,a(flip))].

given #704 (T,wt=23): 2653 (c2 * c1) * ((c2 * (c1 * c2)) * (c2 * (c2 * (c2 * c1)))) != c2 * (c2 * c1).  [ur(12,b,114,a(flip))].

given #705 (T,wt=23): 2673 (x * ((c1 * c2) * (c2 * (c2 * c1)))) * y != (x * (c2 * (c2 * c1))) * y.  [ur(7,b,257,a)].

given #706 (A,wt=33): 316 ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) * (((c1 * c2) * (c1 * (c1 * c2))) * (c2 * c1)) != c1 * (c1 * c2).  [ur(126,b,17,a(flip))].

given #707 (F,wt=23): 2674 x * (y * ((c1 * c2) * (c2 * (c2 * c1)))) != x * (y * (c2 * (c2 * c1))).  [ur(6,b,257,a)].

given #708 (F,wt=23): 2702 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,258,a)].

given #709 (T,wt=23): 2704 (c2 * c1) * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) != c2 * c1.  [ur(41,b,258,a)].

given #710 (T,wt=23): 2708 (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,258,a)].

given #711 (A,wt=25): 319 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (x * (c2 * c1)) != x * (c2 * c1).  [ur(43,b,28,a)].

given #712 (F,wt=23): 2709 x * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,258,a)].

given #713 (F,wt=23): 2749 (c2 * c1) * ((c2 * (c2 * (c2 * c1))) * (c2 * (c1 * c2))) != c2 * (c2 * c1).  [ur(12,b,116,a(flip))].

given #714 (T,wt=23): 2758 (x * ((c2 * c1) * ((c1 * (c1 * c2)) * x))) * y != ((c2 * c1) * x) * y.  [ur(7,b,280,a)].

given #715 (T,wt=23): 2759 x * (y * ((c2 * c1) * ((c1 * (c1 * c2)) * y))) != x * ((c2 * c1) * y).  [ur(6,b,280,a)].

given #716 (A,wt=33): 320 (x * (c2 * c1)) * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) != (c1 * (c1 * c2)) * (x * (x * (c2 * c1))).  [ur(42,b,28,a)].

given #717 (F,wt=23): 2778 (((c2 * c1) * (c2 * (c1 * c2))) * x) * y != ((c2 * (c2 * c1)) * x) * y.  [ur(7,b,296,a)].

given #718 (F,wt=23): 2779 x * (((c2 * c1) * (c2 * (c1 * c2))) * y) != x * ((c2 * (c2 * c1)) * y).  [ur(6,b,296,a)].

given #719 (T,wt=23): 2784 (c1 * (c2 * c1)) * (((c2 * c1) * (c2 * (c1 * c2))) * (c2 * c1)) != c2 * c1.  [ur(53,b,296,a(flip))].

given #720 (T,wt=23): 2841 (x * ((c2 * c1) * (c2 * (c1 * c2)))) * y != (x * (c2 * (c2 * c1))) * y.  [ur(7,b,297,a)].

given #721 (A,wt=25): 321 (x * (c2 * c1)) * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) != x * (c2 * c1).  [ur(41,b,28,a)].

given #722 (F,wt=23): 2842 x * (y * ((c2 * c1) * (c2 * (c1 * c2)))) != x * (y * (c2 * (c2 * c1))).  [ur(6,b,297,a)].

given #723 (F,wt=23): 2870 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) * (c2 * c1) != c2 * c1.  [ur(43,b,298,a)].

given #724 (T,wt=23): 2872 (c2 * c1) * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) != c2 * c1.  [ur(41,b,298,a)].

given #725 (T,wt=23): 2876 (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) * x != (c2 * c1) * x.  [ur(7,b,298,a)].

given #726 (A,wt=33): 322 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (x * (c2 * c1)) != (c1 * (c1 * c2)) * (x * (x * (c2 * c1))).  [ur(40,b,28,a)].

given #727 (F,wt=23): 2877 x * (((c2 * c1) * (c2 * (c1 * c2))) * (c1 * (c2 * c1))) != x * (c2 * c1).  [ur(6,b,298,a)].

given #728 (F,wt=23): 2908 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,300,a)].

given #729 (T,wt=23): 2910 (c1 * c2) * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) != c1 * c2.  [ur(41,b,300,a)].

given #730 (T,wt=23): 2914 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,300,a)].

given #731 (A,wt=31): 324 ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))) * (y * (y * (x * (c2 * c1)))) != y * (x * (c2 * c1)).  [ur(15,b,28,a)].

given #732 (F,wt=23): 2915 x * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,300,a)].

given #733 (F,wt=23): 2916 ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c1 * c2) != c1 * c2.  [ur(43,b,302,a)].

given #734 (T,wt=23): 2918 (c1 * c2) * ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2.  [ur(41,b,302,a)].

given #735 (T,wt=23): 2922 ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * x != (c1 * c2) * x.  [ur(7,b,302,a)].

given #736 (A,wt=39): 325 (x * (c2 * c1)) * (y * (y * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))))) != y * ((c1 * (c1 * c2)) * (x * (x * (c2 * c1)))).  [ur(14,b,28,a)].

given #737 (F,wt=23): 2923 x * ((c1 * c2) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c1 * c2).  [ur(6,b,302,a)].

given #738 (F,wt=23): 2954 ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,306,a)].

given #739 (T,wt=23): 2955 x * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * y) != x * ((c1 * c2) * y).  [ur(6,b,306,a)].

given #740 (T,wt=23): 2979 (x * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * y != (x * (c1 * c2)) * y.  [ur(7,b,307,a)].

given #741 (A,wt=35): 326 ((c2 * (c2 * c1)) * (c2 * c1)) * ((c1 * (c1 * c2)) * ((c1 * (c2 * c1)) * ((c1 * (c2 * c1)) * (c2 * c1)))) != c2 * c1.  [ur(126,b,28,a(flip))].

given #742 (F,wt=23): 2980 x * (y * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (y * (c1 * c2)).  [ur(6,b,307,a)].

given #743 (F,wt=23): 3013 (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,307,a(flip))].

given #744 (T,wt=23): 3014 (c1 * (c1 * c2)) * (c2 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c1 * c2.  [ur(23,b,307,a(flip))].

given #745 (T,wt=23): 3052 c2 * (((c1 * c2) * (c2 * (c2 * c1))) * (c1 * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,135,a(flip))].

given #746 (A,wt=27): 327 ((c1 * (c1 * c2)) * (c1 * (c1 * (c2 * c1)))) * ((c2 * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(76,b,28,a(flip))].

given #747 (F,wt=23): 3053 (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) * (c2 * c1) != c2 * c1.  [ur(43,b,331,a)].

given #748 (F,wt=23): 3055 (c2 * c1) * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != c2 * c1.  [ur(41,b,331,a)].

given #749 (T,wt=23): 3059 (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) * x != (c2 * c1) * x.  [ur(7,b,331,a)].

given #750 (T,wt=23): 3060 x * (c1 * ((c1 * (c1 * c2)) * (c2 * (c2 * (c2 * c1))))) != x * (c2 * c1).  [ur(6,b,331,a)].

given #751 (A,wt=31): 328 (c1 * (c2 * c1)) * ((c1 * (c1 * c2)) * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c2 * c1)))) != c2 * c1.  [ur(53,b,28,a(flip))].

given #752 (F,wt=23): 3061 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,332,a)].

given #753 (F,wt=23): 3063 (c1 * c2) * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) != c1 * c2.  [ur(41,b,332,a)].

given #754 (T,wt=23): 3067 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,332,a)].

given #755 (T,wt=23): 3068 x * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,332,a)].

given #756 (A,wt=27): 333 (c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) != c2 * ((c2 * c1) * (c1 * (c1 * c2))).  [ur(42,b,198,a)].

given #757 (F,wt=23): 3106 ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c1 * c2) != c1 * c2.  [ur(43,b,334,a)].

given #758 (F,wt=23): 3108 (c1 * c2) * ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2.  [ur(41,b,334,a)].

given #759 (T,wt=23): 3112 ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * x != (c1 * c2) * x.  [ur(7,b,334,a)].

given #760 (T,wt=23): 3113 x * ((c1 * c2) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c1 * c2).  [ur(6,b,334,a)].

given #761 (A,wt=27): 335 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c1 * c2) != c2 * ((c2 * c1) * (c1 * (c1 * c2))).  [ur(40,b,198,a)].

given #762 (F,wt=23): 3125 ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,338,a)].

given #763 (F,wt=23): 3126 x * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * y) != x * ((c1 * c2) * y).  [ur(6,b,338,a)].

given #764 (T,wt=23): 3159 (x * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * y != (x * (c1 * c2)) * y.  [ur(7,b,339,a)].

given #765 (T,wt=23): 3160 x * (y * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (y * (c1 * c2)).  [ur(6,b,339,a)].

given #766 (A,wt=25): 336 (c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(15,b,198,a)].

low water: id=5955, wt=91

low water: id=6094, wt=89

given #767 (F,wt=23): 3195 (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,339,a(flip))].

given #768 (F,wt=23): 3196 (c1 * (c1 * c2)) * (c2 * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c1 * c2.  [ur(23,b,339,a(flip))].

low water: id=6189, wt=87

given #769 (T,wt=23): 3198 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) * (c1 * c2) != c1 * c2.  [ur(43,b,340,a)].

given #770 (T,wt=23): 3200 (c1 * c2) * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) != c1 * c2.  [ur(41,b,340,a)].

low water: id=6442, wt=85

given #771 (A,wt=33): 337 (c1 * c2) * (x * (x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != x * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))).  [ur(14,b,198,a)].

given #772 (F,wt=23): 3204 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) * x != (c1 * c2) * x.  [ur(7,b,340,a)].

given #773 (F,wt=23): 3205 x * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2)) != x * (c1 * c2).  [ur(6,b,340,a)].

low water: id=6509, wt=83

low water: id=6658, wt=81

given #774 (T,wt=23): 3254 c2 * (((c2 * (c2 * c1)) * (c1 * c2)) * (c1 * (c1 * (c1 * c2)))) != c1 * c2.  [ur(12,b,143,a(flip))].

given #775 (T,wt=23): 3255 ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c1 * c2) != c1 * c2.  [ur(43,b,342,a)].

given #776 (A,wt=27): 341 (c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) != c2 * ((c1 * c2) * (c1 * (c2 * c1))).  [ur(42,b,208,a)].

given #777 (F,wt=23): 3257 (c1 * c2) * ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2.  [ur(41,b,342,a)].

given #778 (F,wt=23): 3261 ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * x != (c1 * c2) * x.  [ur(7,b,342,a)].

low water: id=6651, wt=79

given #779 (T,wt=23): 3262 x * ((c1 * c2) * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c1 * c2).  [ur(6,b,342,a)].

low water: id=6932, wt=77

given #780 (T,wt=23): 3274 ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * x) * y != ((c1 * c2) * x) * y.  [ur(7,b,346,a)].

given #781 (A,wt=27): 343 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c1 * c2) != c2 * ((c1 * c2) * (c1 * (c2 * c1))).  [ur(40,b,208,a)].

given #782 (F,wt=23): 3275 x * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * y) != x * ((c1 * c2) * y).  [ur(6,b,346,a)].

given #783 (F,wt=23): 3332 (x * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * y != (x * (c1 * c2)) * y.  [ur(7,b,347,a)].

given #784 (T,wt=23): 3333 x * (y * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (y * (c1 * c2)).  [ur(6,b,347,a)].

low water: id=7047, wt=75

low water: id=7193, wt=73

given #785 (T,wt=23): 3370 (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) * (c2 * (c1 * c2)) != c1 * c2.  [ur(24,b,347,a(flip))].

given #786 (A,wt=25): 344 (c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (x * (x * (c1 * c2))) != x * (c1 * c2).  [ur(15,b,208,a)].

given #787 (F,wt=23): 3371 (c1 * (c1 * c2)) * (c2 * (c2 * ((c1 * c2) * (c1 * (c2 * c1))))) != c1 * c2.  [ur(23,b,347,a(flip))].

given #788 (F,wt=23): 3373 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,381,a)].

given #789 (T,wt=23): 3375 (c2 * c1) * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) != c2 * c1.  [ur(41,b,381,a)].

given #790 (T,wt=23): 3379 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,381,a)].

given #791 (A,wt=33): 345 (c1 * c2) * (x * (x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != x * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))).  [ur(14,b,208,a)].

given #792 (F,wt=23): 3380 x * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,381,a)].

given #793 (F,wt=23): 3391 ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c2 * c1) != c2 * c1.  [ur(43,b,383,a)].

given #794 (T,wt=23): 3393 (c2 * c1) * ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1.  [ur(41,b,383,a)].

given #795 (T,wt=23): 3397 ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * x != (c2 * c1) * x.  [ur(7,b,383,a)].

low water: id=7392, wt=71

given #796 (A,wt=33): 348 ((c2 * (c2 * (c2 * c1))) * (c1 * c2)) * (((c2 * c1) * (c2 * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * (c2 * c1).  [ur(127,b,55,a)].

given #797 (F,wt=23): 3398 x * ((c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c2 * c1).  [ur(6,b,383,a)].

low water: id=7474, wt=69

given #798 (F,wt=23): 3410 ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,387,a)].

given #799 (T,wt=23): 3411 x * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * y) != x * ((c2 * c1) * y).  [ur(6,b,387,a)].

given #800 (T,wt=23): 3477 (x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * y != (x * (c2 * c1)) * y.  [ur(7,b,388,a)].

given #801 (A,wt=37): 350 (((c2 * c1) * ((c2 * c1) * x)) * ((c1 * (c1 * c2)) * x)) * ((x * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(127,b,27,a)].

given #802 (F,wt=23): 3478 x * (y * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (y * (c2 * c1)).  [ur(6,b,388,a)].

low water: id=7539, wt=67

given #803 (F,wt=23): 3517 (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,388,a(flip))].

given #804 (T,wt=23): 3518 (c2 * (c2 * c1)) * (c1 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c2 * c1.  [ur(23,b,388,a(flip))].

given #805 (T,wt=23): 3520 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,389,a)].

given #806 (A,wt=37): 351 (((c1 * (c1 * c2)) * ((c2 * c1) * x)) * ((c2 * c1) * x)) * ((x * ((c2 * c1) * x)) * ((c2 * c1) * x)) != (c2 * c1) * x.  [ur(127,b,26,a)].

given #807 (F,wt=23): 3522 (c2 * c1) * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) != c2 * c1.  [ur(41,b,389,a)].

given #808 (F,wt=23): 3526 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,389,a)].

given #809 (T,wt=23): 3527 x * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,389,a)].

low water: id=7750, wt=65

given #810 (T,wt=23): 3558 ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c2 * c1) != c2 * c1.  [ur(43,b,391,a)].

given #811 (A,wt=25): 352 ((c2 * (c2 * c1)) * (c1 * (c1 * c2))) * ((c1 * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(127,b,17,a)].

given #812 (F,wt=23): 3560 (c2 * c1) * ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1.  [ur(41,b,391,a)].

given #813 (F,wt=23): 3564 ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * x != (c2 * c1) * x.  [ur(7,b,391,a)].

given #814 (T,wt=23): 3565 x * ((c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c2 * c1).  [ur(6,b,391,a)].

given #815 (T,wt=23): 3577 ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,395,a)].

given #816 (A,wt=25): 353 ((c1 * (c1 * c2)) * (c2 * (c2 * c1))) * ((c2 * (c1 * c2)) * (c1 * c2)) != c1 * c2.  [ur(127,b,55,a(flip))].

given #817 (F,wt=23): 3578 x * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * y) != x * ((c2 * c1) * y).  [ur(6,b,395,a)].

given #818 (F,wt=23): 3632 (x * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * y != (x * (c2 * c1)) * y.  [ur(7,b,396,a)].

given #819 (T,wt=23): 3633 x * (y * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (y * (c2 * c1)).  [ur(6,b,396,a)].

low water: id=7912, wt=63

given #820 (T,wt=23): 3672 (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,396,a(flip))].

given #821 (A,wt=35): 354 ((c1 * (c1 * c2)) * ((c2 * (c2 * c1)) * ((c2 * (c2 * c1)) * (c2 * c1)))) * ((c1 * (c2 * c1)) * (c2 * c1)) != c2 * c1.  [ur(127,b,28,a(flip))].

given #822 (F,wt=23): 3673 (c2 * (c2 * c1)) * (c1 * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c2 * c1.  [ur(23,b,396,a(flip))].

given #823 (F,wt=23): 3675 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) * (c2 * c1) != c2 * c1.  [ur(43,b,425,a)].

given #824 (T,wt=23): 3677 (c2 * c1) * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) != c2 * c1.  [ur(41,b,425,a)].

given #825 (T,wt=23): 3681 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) * x != (c2 * c1) * x.  [ur(7,b,425,a)].

low water: id=8030, wt=61

given #826 (A,wt=45): 355 (((c1 * (c1 * c2)) * ((c1 * (c1 * c2)) * x)) * ((c2 * c1) * x)) * ((x * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(127,b,27,a(flip))].

given #827 (F,wt=23): 3682 x * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c2 * c1)) != x * (c2 * c1).  [ur(6,b,425,a)].

given #828 (F,wt=23): 3695 ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c2 * c1) != c2 * c1.  [ur(43,b,427,a)].

given #829 (T,wt=23): 3697 (c2 * c1) * ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1.  [ur(41,b,427,a)].

given #830 (T,wt=23): 3701 ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * x != (c2 * c1) * x.  [ur(7,b,427,a)].

given #831 (A,wt=45): 356 (((c2 * c1) * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) * ((x * ((c1 * (c1 * c2)) * x)) * ((c1 * (c1 * c2)) * x)) != (c1 * (c1 * c2)) * x.  [ur(127,b,26,a(flip))].

given #832 (F,wt=23): 3702 x * ((c2 * c1) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c2 * c1).  [ur(6,b,427,a)].

given #833 (F,wt=23): 3714 ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * x) * y != ((c2 * c1) * x) * y.  [ur(7,b,431,a)].

given #834 (T,wt=23): 3715 x * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * y) != x * ((c2 * c1) * y).  [ur(6,b,431,a)].

given #835 (T,wt=23): 3739 (x * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * y != (x * (c2 * c1)) * y.  [ur(7,b,432,a)].

low water: id=8218, wt=59

given #836 (A,wt=33): 357 ((c1 * (c1 * (c1 * c2))) * (c2 * c1)) * (((c1 * c2) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(127,b,17,a(flip))].

given #837 (F,wt=23): 3740 x * (y * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (y * (c2 * c1)).  [ur(6,b,432,a)].

given #838 (F,wt=23): 3779 (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) * (c1 * (c2 * c1)) != c2 * c1.  [ur(24,b,432,a(flip))].

given #839 (T,wt=23): 3780 (c2 * (c2 * c1)) * (c1 * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c2 * c1.  [ur(23,b,432,a(flip))].

given #840 (T,wt=23): 3810 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * y != (x * (c2 * c1)) * y.  [ur(7,b,445,a)].

given #841 (A,wt=29): 367 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * (x * (c1 * (c1 * c2))) != x * (c1 * (c1 * c2)).  [ur(43,b,29,a)].

given #842 (F,wt=23): 3811 x * ((c2 * c1) * (y * (y * (c1 * (c1 * c2))))) != x * (y * (c2 * c1)).  [ur(6,b,445,a)].

given #843 (F,wt=23): 3837 (c2 * (c2 * c1)) * ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2))))) != c2 * c1.  [ur(23,b,445,a(flip))].

given #844 (T,wt=23): 3844 ((c2 * c1) * (c1 * (c1 * c2))) * x != ((c1 * (c1 * c2)) * (c2 * c1)) * x.  [ur(7,b,636,a)].

given #845 (T,wt=23): 3845 x * ((c2 * c1) * (c1 * (c1 * c2))) != x * ((c1 * (c1 * c2)) * (c2 * c1)).  [ur(6,b,636,a)].

low water: id=8357, wt=57

given #846 (A,wt=35): 368 (x * (c1 * (c1 * c2))) * ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) != (c2 * c1) * (x * (x * (c1 * (c1 * c2)))).  [ur(42,b,29,a)].

given #847 (F,wt=23): 3854 (x * ((c1 * c2) * ((c2 * (c2 * c1)) * x))) * y != ((c1 * c2) * x) * y.  [ur(7,b,937,a)].

given #848 (F,wt=23): 3855 x * (y * ((c1 * c2) * ((c2 * (c2 * c1)) * y))) != x * ((c1 * c2) * y).  [ur(6,b,937,a)].

given #849 (T,wt=23): 3870 ((c1 * c2) * (x * (x * (c2 * (c2 * c1))))) * y != (x * (c1 * c2)) * y.  [ur(7,b,1059,a)].

given #850 (T,wt=23): 3871 x * ((c1 * c2) * (y * (y * (c2 * (c2 * c1))))) != x * (y * (c1 * c2)).  [ur(6,b,1059,a)].

given #851 (A,wt=29): 369 (x * (c1 * (c1 * c2))) * ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) != x * (c1 * (c1 * c2)).  [ur(41,b,29,a)].

given #852 (F,wt=23): 3897 (c1 * (c1 * c2)) * ((c1 * c2) * (c2 * (c2 * (c2 * (c2 * c1))))) != c1 * c2.  [ur(23,b,1059,a(flip))].

given #853 (F,wt=23): 3914 ((c2 * (c2 * c1)) * (c1 * c2)) * x != ((c1 * c2) * (c2 * (c2 * c1))) * x.  [ur(7,b,1132,a)].

given #854 (T,wt=23): 3915 x * ((c2 * (c2 * c1)) * (c1 * c2)) != x * ((c1 * c2) * (c2 * (c2 * c1))).  [ur(6,b,1132,a)].

given #855 (T,wt=23): 3916 (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) * (c1 * c2) != c1 * c2.  [ur(43,b,1342,a)].

given #856 (A,wt=35): 370 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * (x * (c1 * (c1 * c2))) != (c2 * c1) * (x * (x * (c1 * (c1 * c2)))).  [ur(40,b,29,a)].

given #857 (F,wt=23): 3918 (c1 * c2) * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != c1 * c2.  [ur(41,b,1342,a)].

given #858 (F,wt=23): 3922 (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) * x != (c1 * c2) * x.  [ur(7,b,1342,a)].

given #859 (T,wt=23): 3923 x * (c2 * ((c2 * (c2 * c1)) * (c1 * (c1 * (c1 * c2))))) != x * (c1 * c2).  [ur(6,b,1342,a)].

given #860 (T,wt=23): 3924 (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) * (c1 * c2) != c1 * c2.  [ur(43,b,3015,a)].

given #861 (A,wt=35): 372 ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))) * (y * (y * (x * (c1 * (c1 * c2))))) != y * (x * (c1 * (c1 * c2))).  [ur(15,b,29,a)].

given #862 (F,wt=23): 3926 (c1 * c2) * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != c1 * c2.  [ur(41,b,3015,a)].

given #863 (F,wt=23): 3930 (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) * x != (c1 * c2) * x.  [ur(7,b,3015,a)].

low water: id=8499, wt=55

given #864 (T,wt=23): 3931 x * (c2 * (c1 * (c2 * ((c1 * (c1 * c2)) * (c2 * c1))))) != x * (c1 * c2).  [ur(6,b,3015,a)].

given #865 (T,wt=23): 3932 (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) * (c1 * c2) != c1 * c2.  [ur(43,b,3197,a)].

given #866 (A,wt=41): 373 (x * (c1 * (c1 * c2))) * (y * (y * ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))))) != y * ((c2 * c1) * (x * (x * (c1 * (c1 * c2))))).  [ur(14,b,29,a)].

given #867 (F,wt=23): 3934 (c1 * c2) * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != c1 * c2.  [ur(41,b,3197,a)].

given #868 (F,wt=23): 3938 (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) * x != (c1 * c2) * x.  [ur(7,b,3197,a)].

given #869 (T,wt=23): 3939 x * (c2 * (c1 * (c2 * ((c2 * c1) * (c1 * (c1 * c2)))))) != x * (c1 * c2).  [ur(6,b,3197,a)].

low water: id=8597, wt=53

given #870 (T,wt=23): 3954 (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) * (c1 * c2) != c1 * c2.  [ur(43,b,3372,a)].

given #871 (A,wt=47): 374 ((c2 * c1) * ((c1 * (c1 * (c1 * c2))) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))))) * (((c1 * c2) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(127,b,29,a(flip))].

given #872 (F,wt=23): 3956 (c1 * c2) * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != c1 * c2.  [ur(41,b,3372,a)].

given #873 (F,wt=23): 3960 (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) * x != (c1 * c2) * x.  [ur(7,b,3372,a)].

given #874 (T,wt=23): 3961 x * (c2 * (c1 * (c2 * ((c1 * c2) * (c1 * (c2 * c1)))))) != x * (c1 * c2).  [ur(6,b,3372,a)].

given #875 (T,wt=23): 3962 (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) * (c2 * c1) != c2 * c1.  [ur(43,b,3519,a)].

given #876 (A,wt=49): 375 ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) * ((c2 * c1) * (((c1 * c2) * (c1 * (c1 * c2))) * (((c1 * c2) * (c1 * (c1 * c2))) * (c1 * (c1 * c2))))) != c1 * (c1 * c2).  [ur(126,b,29,a(flip))].

given #877 (F,wt=23): 3964 (c2 * c1) * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != c2 * c1.  [ur(41,b,3519,a)].

given #878 (F,wt=23): 3968 (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) * x != (c2 * c1) * x.  [ur(7,b,3519,a)].

given #879 (T,wt=23): 3969 x * (c1 * (c2 * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != x * (c2 * c1).  [ur(6,b,3519,a)].

given #880 (T,wt=23): 3970 (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) * (c2 * c1) != c2 * c1.  [ur(43,b,3674,a)].

given #881 (A,wt=37): 376 ((c2 * c1) * ((c1 * c2) * ((c1 * c2) * (c1 * (c1 * c2))))) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(76,b,29,a(flip))].

given #882 (F,wt=23): 3972 (c2 * c1) * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != c2 * c1.  [ur(41,b,3674,a)].

given #883 (F,wt=23): 3976 (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) * x != (c2 * c1) * x.  [ur(7,b,3674,a)].

given #884 (T,wt=23): 3977 x * (c1 * (c2 * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))))) != x * (c2 * c1).  [ur(6,b,3674,a)].

given #885 (T,wt=23): 3978 (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) * (c2 * c1) != c2 * c1.  [ur(43,b,3781,a)].

given #886 (A,wt=41): 377 ((c1 * c2) * (c1 * (c1 * c2))) * ((c2 * c1) * ((c1 * (c1 * (c1 * c2))) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c1 * c2))))) != c1 * (c1 * c2).  [ur(53,b,29,a(flip))].

given #887 (F,wt=23): 3980 (c2 * c1) * (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) != c2 * c1.  [ur(41,b,3781,a)].

given #888 (F,wt=23): 3984 (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) * x != (c2 * c1) * x.  [ur(7,b,3781,a)].

given #889 (T,wt=23): 3985 x * (c1 * (c2 * (c1 * ((c2 * c1) * (c2 * (c1 * c2)))))) != x * (c2 * c1).  [ur(6,b,3781,a)].

given #890 (T,wt=23): 4411 c1 * (((c1 * c2) * (c1 * (c2 * c1))) * (c2 * (c2 * (c2 * c1)))) != c2 * c1.  [ur(12,b,168,a(flip))].

given #891 (A,wt=29): 378 ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2))))) * ((c1 * c2) * (c1 * (c1 * c2))) != c1 * (c1 * c2).  [ur(24,b,29,a(flip))].

given #892 (F,wt=23): 4855 (c1 * c2) * ((c1 * (c1 * c2)) * (c1 * (c1 * (c2 * c1)))) != c1 * (c1 * c2).  [ur(12,b,454,a(flip))].

given #893 (F,wt=23): 4931 x * ((c1 * c2) * (((c2 * c1) * (c2 * (c1 * c2))) * x)) != (c1 * c2) * x.  [ur(12,b,509,a(flip))].

given #894 (T,wt=23): 5069 (c1 * c2) * (x * (x * ((c2 * c1) * (c2 * (c1 * c2))))) != x * (c1 * c2).  [ur(12,b,532,a(flip))].

given #895 (T,wt=23): 5272 x * ((c2 * c1) * (((c2 * c1) * (c1 * (c1 * c2))) * x)) != (c2 * c1) * x.  [ur(12,b,591,a(flip))].

low water: id=8834, wt=51

given #896 (A,wt=31): 379 (c1 * (c1 * (c1 * c2))) * ((c2 * c1) * ((c1 * c2) * ((c1 * c2) * (c1 * (c1 * c2))))) != c1 * (c1 * c2).  [ur(23,b,29,a(flip))].

given #897 (F,wt=23): 5383 (c2 * c1) * (x * (x * ((c2 * c1) * (c1 * (c1 * c2))))) != x * (c2 * c1).  [ur(12,b,638,a(flip))].

given #898 (F,wt=23): 5605 x * ((c2 * c1) * (((c1 * (c1 * c2)) * (c2 * c1)) * x)) != (c2 * c1) * x.  [ur(12,b,711,a(flip))].

given #899 (T,wt=23): 5720 (c2 * c1) * (x * (x * ((c1 * (c1 * c2)) * (c2 * c1)))) != x * (c2 * c1).  [ur(12,b,735,a(flip))].

low water: id=9086, wt=49

given #900 (T,wt=23): 6522 (c2 * c1) * ((c2 * (c2 * c1)) * (c2 * (c2 * (c1 * c2)))) != c2 * (c2 * c1).  [ur(12,b,1043,a(flip))].

given #901 (A,wt=27): 382 (c2 * c1) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) != c1 * ((c2 * (c2 * c1)) * (c1 * c2)).  [ur(42,b,251,a)].

given #902 (F,wt=23): 6911 x * ((c1 * c2) * (((c1 * c2) * (c2 * (c2 * c1))) * x)) != (c1 * c2) * x.  [ur(12,b,1175,a(flip))].

given #903 (F,wt=23): 7014 (c1 * c2) * (x * (x * ((c1 * c2) * (c2 * (c2 * c1))))) != x * (c1 * c2).  [ur(12,b,1200,a(flip))].

given #904 (T,wt=23): 7298 x * ((c1 * c2) * (((c2 * (c2 * c1)) * (c1 * c2)) * x)) != (c1 * c2) * x.  [ur(12,b,1355,a(flip))].

given #905 (T,wt=23): 7375 (c1 * c2) * (x * (x * ((c2 * (c2 * c1)) * (c1 * c2)))) != x * (c1 * c2).  [ur(12,b,1379,a(flip))].

given #906 (A,wt=27): 384 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c2 * c1) != c1 * ((c2 * (c2 * c1)) * (c1 * c2)).  [ur(40,b,251,a)].

given #907 (F,wt=23): 7802 x * ((c2 * c1) * (((c1 * c2) * (c1 * (c2 * c1))) * x)) != (c2 * c1) * x.  [ur(12,b,1569,a(flip))].

given #908 (F,wt=23): 7880 (c2 * c1) * (x * (x * ((c1 * c2) * (c1 * (c2 * c1))))) != x * (c2 * c1).  [ur(12,b,1596,a(flip))].

given #909 (T,wt=23): 9055 c2 * ((c1 * c2) * ((c2 * c1) * (c1 * (c1 * (c1 * (c1 * c2)))))) != c1 * c2.  [ur(12,b,380,a(flip))].

given #910 (T,wt=23): 9154 c2 * ((c1 * ((c2 * c1) * (c2 * (c1 * c2)))) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,522,a(flip))].

given #911 (A,wt=25): 385 (c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (x * (x * (c2 * c1))) != x * (c2 * c1).  [ur(15,b,251,a)].

given #912 (F,wt=23): 9170 c2 * ((c1 * (c1 * c2)) * (c1 * ((c2 * c1) * (c2 * (c1 * c2))))) != c1 * c2.  [ur(12,b,524,a(flip))].

given #913 (F,wt=23): 9251 c1 * ((c2 * ((c2 * c1) * (c1 * (c1 * c2)))) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,628,a(flip))].

given #914 (T,wt=23): 9267 c1 * ((c2 * (c2 * c1)) * (c2 * ((c2 * c1) * (c1 * (c1 * c2))))) != c2 * c1.  [ur(12,b,630,a(flip))].

given #915 (T,wt=23): 9374 c1 * ((c2 * ((c1 * (c1 * c2)) * (c2 * c1))) * (c2 * (c2 * c1))) != c2 * c1.  [ur(12,b,726,a(flip))].

given #916 (A,wt=33): 386 (c2 * c1) * (x * (x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))))) != x * (c1 * ((c2 * (c2 * c1)) * (c1 * c2))).  [ur(14,b,251,a)].

given #917 (F,wt=23): 9388 c1 * ((c2 * (c2 * c1)) * (c2 * ((c1 * (c1 * c2)) * (c2 * c1)))) != c2 * c1.  [ur(12,b,728,a(flip))].

given #918 (F,wt=23): 9438 c2 * ((c1 * c2) * ((c1 * (c1 * (c1 * c2))) * (c1 * (c2 * c1)))) != c1 * c2.  [ur(12,b,829,a(flip))].

given #919 (T,wt=23): 9478 c1 * ((c2 * c1) * ((c1 * c2) * (c2 * (c2 * (c2 * (c2 * c1)))))) != c2 * c1.  [ur(12,b,983,a(flip))].

given #920 (T,wt=23): 9527 c2 * ((c1 * ((c1 * c2) * (c2 * (c2 * c1)))) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,1192,a(flip))].

given #921 (A,wt=27): 390 (c2 * c1) * (c1 * ((c1 * c2) * (c2 * (c2 * c1)))) != c1 * ((c1 * c2) * (c2 * (c2 * c1))).  [ur(42,b,259,a)].

given #922 (F,wt=23): 9545 c2 * ((c1 * (c1 * c2)) * (c1 * ((c1 * c2) * (c2 * (c2 * c1))))) != c1 * c2.  [ur(12,b,1194,a(flip))].

given #923 (F,wt=23): 9608 c2 * ((c1 * ((c2 * (c2 * c1)) * (c1 * c2))) * (c1 * (c1 * c2))) != c1 * c2.  [ur(12,b,1371,a(flip))].

given #924 (T,wt=23): 9622 c2 * ((c1 * (c1 * c2)) * (c1 * ((c2 * (c2 * c1)) * (c1 * c2)))) != c1 * c2.  [ur(12,b,1373,a(flip))].

given #925 (T,wt=23): 9680 c1 * ((c2 * ((c1 * c2) * (c1 * (c2 * c1)))) * (c2