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

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

% Reading from file a2.in


clauses(sos).
(((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).
B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B | ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).
end_of_list.

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

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [input].
2 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B | ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).  [input].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:  no changes.

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ A, B, C, v, ^ ]).
After inverse_order: Function symbol precedence:  lex([ A, B, C, v, ^ ]).
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, 4).  % (nonunit Horn with equality)

Auto_process settings:
  % set(back_unit_deletion).  % (Horn set with negative nonunits)
    % set(back_unit_deletion) -> set(unit_deletion).

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

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

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
3 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [input].
4 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B | ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).  [input].
end_of_list.

clauses(demodulators).
3 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [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=29): 3 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [input].

given #2 (I,wt=40): 4 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B | ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).  [input].

given #3 (F,wt=21): 7 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v v) = y.  [para(3(a,1),3(a,1,1,2))].

given #4 (T,wt=25): 11 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y.  [para(7(a,1),7(a,1,2,1))].

given #5 (T,wt=27): 12 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((v v y) ^ (w v y)) v v6) = y.  [para(11(a,1),3(a,1,1,2,1,1))].

given #6 (A,wt=61): 5 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z).  [para(3(a,1),3(a,1,1,2,1,1))].

given #7 (F,wt=33): 18 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (y v v) = y v y.  [para(7(a,1),12(a,1,2,1))].

given #8 (F,wt=31): 30 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (y v u) = y v y.  [para(11(a,1),18(a,1,1,2,1,2))].

given #9 (T,wt=33): 26 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y.  [para(12(a,1),5(a,1,1,1,1,2)),demod(12(17),12(22),12(26),12(27),12(31))].

given #10 (T,wt=21): 38 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (v v y)) v w) = y.  [para(3(a,1),26(a,1,1,2))].

given #11 (A,wt=83): 6 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v (((w ^ ((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v))) v z) ^ v6)) ^ (((v7 v (((y v z) ^ (u v z)) v v)) ^ (v8 v (((y v z) ^ (u v z)) v v))) v v9) = ((y v z) ^ (u v z)) v v.  [para(3(a,1),3(a,1,1,2,1,2))].

given #12 (F,wt=23): 51 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y.  [para(7(a,1),38(a,1,2,1))].

given #13 (F,wt=21): 71 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y.  [para(11(a,1),51(a,1,1,2))].

given #14 (T,wt=15): 88 ((x v x) v (x v x)) ^ (x v y) = x v x.  [para(71(a,1),71(a,1,1,1))].

given #15 (T,wt=17): 87 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x.  [para(71(a,1),51(a,1,1,1))].

given #16 (A,wt=83): 8 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(3(a,1),3(a,1,2,1))].

given #17 (F,wt=19): 76 ((x v x) v ((x v x) v (x v x))) ^ (x v y) = x v x.  [para(71(a,1),11(a,1,1,1))].

given #18 (F,wt=23): 61 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v v) = y ^ z.  [para(38(a,1),38(a,1,2,1))].

given #19 (T,wt=15): 108 ((x v x) v (y ^ x)) ^ (x v z) = x v x.  [para(61(a,1),87(a,1,1,2))].

given #20 (T,wt=21): 107 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y.  [para(61(a,1),51(a,1,1,2))].

given #21 (A,wt=35): 9 (((x v (y v y)) ^ (y v y)) v (((z ^ ((y v y) v (y v y))) v (u ^ (y v y))) ^ v)) ^ (y v w) = y v y.  [para(7(a,1),3(a,1,2,1))].

given #22 (F,wt=23): 97 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(8(a,1),87(a,1,1,2))].

given #23 (F,wt=21): 138 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(11(a,1),97(a,1,1,2,1,1))].

given #24 (T,wt=21): 148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(61(a,1),97(a,1,1,2,1,1))].

given #25 (T,wt=13): 165 ((x v x) v x) ^ (x v y) = x v x.  [para(3(a,1),148(a,1,1,2))].

given #26 (A,wt=65): 10 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ (z v w) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(3(a,1),7(a,1,2,1))].

given #27 (F,wt=17): 180 (((x v y) ^ y) v (y v y)) ^ ((y v y) v z) = y.  [para(165(a,1),7(a,1,2,1))].

given #28 (F,wt=17): 185 (((x v y) ^ y) v (z ^ y)) ^ ((y v y) v u) = y.  [para(165(a,1),38(a,1,2,1))].

given #29 (T,wt=19): 202 (((x v y) ^ y) v (z ^ y)) ^ (((y v y) v u) v v) = y.  [para(180(a,1),61(a,1,1,1,1,2)),demod(180(8),180(9),180(15))].

given #30 (T,wt=21): 232 (((x v y) ^ y) v (z ^ y)) ^ ((((y v y) v u) v v) v w) = y.  [para(202(a,1),61(a,1,1,1,1,2)),demod(202(9),202(10),202(17))].

given #31 (A,wt=43): 13 (((x v (y v z)) ^ (y v z)) v (((u ^ ((y v z) v (y v z))) v (y v y)) ^ v)) ^ (((w v (y v z)) ^ (v6 v (y v z))) v v7) = y v z.  [para(11(a,1),3(a,1,1,2,1,2))].

given #32 (F,wt=23): 99 (((x v y) ^ y) v (z ^ y)) ^ ((((u v y) ^ (v v y)) v w) v v6) = y.  [para(3(a,1),61(a,1,1,1,1,2)),demod(3(14),3(15),3(23))].

given #33 (F,wt=23): 181 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(165(a,1),12(a,1,2,1))].

given #34 (T,wt=23): 200 (((x v x) v (x v x)) v x) ^ ((x v x) v y) = (x v x) v (x v x).  [para(180(a,1),87(a,1,1,2))].

given #35 (T,wt=21): 332 (((x v y) ^ y) v (y v y)) ^ (((y v y) v (y v y)) v z) = y.  [para(200(a,1),7(a,1,2,1))].

given #36 (A,wt=71): 14 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v (((v ^ ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) v (w ^ (((y v y) v (z ^ y)) ^ u))) ^ v6)) ^ (y v v7) = ((y v y) v (z ^ y)) ^ u.  [para(12(a,1),3(a,1,2,1))].

given #37 (F,wt=23): 216 ((x v x) v (y ^ (x v x))) ^ (((x v x) v (x v x)) v z) = x v x.  [para(71(a,1),185(a,1,1,1))].

given #38 (F,wt=21): 363 ((x v x) v (x v x)) ^ (((x v x) v (x v x)) v y) = x v x.  [para(11(a,1),216(a,1,1,2))].

given #39 (T,wt=21): 365 ((x v x) v (y ^ x)) ^ (((x v x) v (x v x)) v z) = x v x.  [para(61(a,1),216(a,1,1,2))].

given #40 (T,wt=23): 257 (((x v y) ^ y) v (z ^ y)) ^ (((((y v y) v u) v v) v w) v v6) = y.  [para(232(a,1),61(a,1,1,1,1,2)),demod(232(10),232(11),232(19))].

given #41 (A,wt=81): 15 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v z) ^ w)) ^ (((v6 v (((y v z) ^ (u v z)) v v)) ^ (v7 v (((y v z) ^ (u v z)) v v))) v v8) = ((y v z) ^ (u v z)) v v.  [para(3(a,1),12(a,1,1,2,1,2))].

given #42 (F,wt=25): 50 (((x v (y ^ z)) ^ (y ^ z)) v ((y ^ z) v (y ^ z))) ^ (z v u) = y ^ z.  [para(38(a,1),7(a,1,2,1))].

given #43 (F,wt=19): 422 (((x v y) ^ y) v (y v y)) ^ (((y v y) v z) v u) = y.  [para(180(a,1),50(a,1,1,1,1,2)),demod(180(8),180(9),180(9),180(15))].

given #44 (T,wt=21): 423 (((x v y) ^ y) v (y v y)) ^ ((((y v y) v z) v u) v v) = y.  [para(202(a,1),50(a,1,1,1,1,2)),demod(202(9),202(10),202(10),202(17))].

given #45 (T,wt=23): 418 (((x v y) ^ y) v (y v y)) ^ ((((z v y) ^ (u v y)) v v) v w) = y.  [para(3(a,1),50(a,1,1,1,1,2)),demod(3(14),3(15),3(15),3(23))].

given #46 (A,wt=81): 16 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(3(a,1),12(a,1,2,1))].

given #47 (F,wt=23): 424 (((x v y) ^ y) v (y v y)) ^ (((((y v y) v z) v u) v v) v w) = y.  [para(232(a,1),50(a,1,1,1,1,2)),demod(232(10),232(11),232(11),232(19))].

given #48 (F,wt=25): 81 ((x v x) v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (x v z) = x v x.  [para(71(a,1),30(a,1,1,1))].

given #49 (T,wt=25): 100 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ ((y v u) v v) = y v y.  [para(11(a,1),61(a,1,1,1,1,2)),demod(11(12),11(14),11(20))].

given #50 (T,wt=19): 455 ((x v x) v (y ^ (x v x))) ^ ((x v z) v u) = x v x.  [para(71(a,1),100(a,1,1,1))].

given #51 (A,wt=55): 17 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u))) ^ (y v v) = ((y v y) v (z ^ y)) ^ u.  [para(12(a,1),7(a,1,2,1))].

given #52 (F,wt=17): 487 ((x v x) v (x v x)) ^ ((x v y) v z) = x v x.  [para(11(a,1),455(a,1,1,2))].

given #53 (F,wt=17): 489 ((x v x) v (y ^ x)) ^ ((x v z) v u) = x v x.  [para(61(a,1),455(a,1,1,2))].

given #54 (T,wt=23): 448 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ ((y v z) v u) = y v y.  [para(11(a,1),100(a,1,1,2))].

given #55 (T,wt=23): 459 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ ((y v u) v v) = y v y.  [para(61(a,1),100(a,1,1,2))].

given #56 (A,wt=41): 19 (((x v (y v z)) ^ (y v z)) v ((((y v z) v (y v z)) v (y v y)) ^ u)) ^ (((v v (y v z)) ^ (w v (y v z))) v v6) = y v z.  [para(11(a,1),12(a,1,1,2,1,2))].

given #57 (F,wt=23): 494 ((x v x) v (((x v x) v (y ^ x)) ^ z)) ^ ((x v u) v v) = x v x.  [para(14(a,1),455(a,1,1,2))].

given #58 (F,wt=25): 112 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ ((z v v) v w) = y ^ z.  [para(61(a,1),61(a,1,1,1,1,2)),demod(61(11),61(13),61(19))].

given #59 (T,wt=25): 116 (((x v y) v (x v y)) v (x v x)) ^ ((x v y) v z) = (x v y) v (x v y).  [para(11(a,1),108(a,1,1,2))].

given #60 (T,wt=25): 123 (((x v y) v (x v y)) v (z ^ x)) ^ ((x v y) v u) = (x v y) v (x v y).  [para(61(a,1),108(a,1,1,2))].

given #61 (A,wt=69): 20 (((x v (((y v y) v (z ^ y)) ^ u)) ^ (((y v y) v (z ^ y)) ^ u)) v ((((((y v y) v (z ^ y)) ^ u) v (((y v y) v (z ^ y)) ^ u)) v (v ^ (((y v y) v (z ^ y)) ^ u))) ^ w)) ^ (y v v6) = ((y v y) v (z ^ y)) ^ u.  [para(12(a,1),12(a,1,2,1))].

given #62 (F,wt=25): 179 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(165(a,1),3(a,1,2,1))].

given #63 (F,wt=23): 600 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(61(a,1),179(a,1,1,2,1,1))].

given #64 (T,wt=15): 618 (((x v y) ^ y) v y) ^ ((y v y) v z) = y.  [para(3(a,1),600(a,1,1,2))].

given #65 (T,wt=15): 646 (((x v y) ^ y) v (y v y)) ^ (y v z) = y.  [para(618(a,1),7(a,1,2,1))].

given #66 (A,wt=35): 21 (((x v y) ^ y) v (((((z ^ (y v y)) v (u ^ y)) ^ v) v (w ^ y)) ^ v6)) ^ (((v7 v y) ^ (v8 v y)) v v9) = y.  [para(3(a,1),5(a,1,1,1,1,2)),demod(3(19),3(25),3(29),3(30),3(34))].

given #67 (F,wt=11): 677 (x v x) v (x v x) = x v x.  [para(71(a,1),646(a,1,1,1)),demod(676(8))].

given #68 (F,wt=11): 786 (x v x) ^ (x v y) = x v x.  [back_demod(88),demod(677(3))].

given #69 (T,wt=13): 676 (x v (x v x)) ^ (x v y) = x v x.  [para(646(a,1),71(a,1,1,1))].

given #70 (T,wt=13): 683 (x v (y ^ x)) ^ (x v z) = x v x.  [para(646(a,1),107(a,1,1,1))].

given #71 (A,wt=89): 22 (((x v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)).  [para(3(a,1),5(a,1,1,2))].

given #72 (F,wt=13): 758 (x v x) ^ ((x v y) v z) = x v x.  [back_demod(487),demod(677(3))].

given #73 (F,wt=13): 879 (((x v y) ^ y) v y) ^ (y v y) = y.  [para(677(a,1),618(a,1,2))].

given #74 (T,wt=15): 651 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y.  [para(618(a,1),38(a,1,2,1))].

given #75 (T,wt=15): 674 (x v (y ^ (x v x))) ^ (x v z) = x v x.  [para(646(a,1),51(a,1,1,1))].

given #76 (A,wt=77): 23 (((x v (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)))) ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)))) v (((u ^ z) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z))))) ^ v6)) ^ (z v v7) = ((y ^ (z v z)) v (u ^ z)) ^ (v v (u ^ z)).  [para(3(a,1),5(a,1,2,1))].

given #77 (F,wt=15): 721 ((x v x) v x) ^ ((x v y) v z) = x v x.  [para(646(a,1),455(a,1,1,2))].

given #78 (F,wt=15): 724 (x v (x v x)) ^ ((x v y) v z) = x v x.  [para(646(a,1),448(a,1,1,1))].

given #79 (T,wt=15): 725 (x v (y ^ x)) ^ ((x v z) v u) = x v x.  [para(646(a,1),459(a,1,1,1))].

given #80 (T,wt=15): 740 (x v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_demod(666),demod(677(3),677(3))].

given #81 (A,wt=81): 24 (((x v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ (((u v y) ^ (v v y)) v v6) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w.  [para(5(a,1),7(a,1,2,1))].

given #82 (F,wt=15): 767 (x v x) ^ (((x v x) v y) v z) = x v x.  [back_demod(428),demod(677(4),677(3),677(4))].

given #83 (F,wt=17): 655 (((x v y) ^ y) v (z ^ y)) ^ ((y v u) v v) = y.  [para(618(a,1),99(a,1,2,1,1))].

given #84 (T,wt=17): 658 (((x v y) ^ y) v (y v y)) ^ ((y v z) v u) = y.  [para(618(a,1),418(a,1,2,1,1))].

given #85 (T,wt=17): 713 (x v (x v x)) ^ (((x v x) v y) v z) = x v x.  [para(646(a,1),422(a,1,1,1)),demod(677(3),677(5))].

given #86 (A,wt=99): 25 (((x v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (((((y v (z ^ ((u v y) ^ (v v y)))) ^ w) v ((y v (z ^ ((u v y) ^ (v v y)))) ^ w)) v (v6 ^ ((y v (z ^ ((u v y) ^ (v v y)))) ^ w))) ^ v7)) ^ (((u v y) ^ (v v y)) v v8) = (y v (z ^ ((u v y) ^ (v v y)))) ^ w.  [para(5(a,1),12(a,1,2,1))].

given #87 (F,wt=17): 719 (x v (y ^ (x v x))) ^ ((x v z) v u) = x v x.  [para(646(a,1),100(a,1,1,1))].

given #88 (F,wt=17): 766 (x v x) ^ ((((x v x) v y) v z) v u) = x v x.  [back_demod(429),demod(677(4),677(3),677(4))].

given #89 (T,wt=17): 788 ((x v x) v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_demod(81),demod(677(4),677(4))].

given #90 (T,wt=19): 675 (((x v (y v y)) ^ (y v y)) v y) ^ (y v z) = y v y.  [para(646(a,1),51(a,1,1,2))].

given #91 (A,wt=69): 27 (((x v (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y)))) v (((z ^ y) v (v ^ (((y v y) v (z ^ y)) ^ (u v (z ^ y))))) ^ w)) ^ (y v v6) = ((y v y) v (z ^ y)) ^ (u v (z ^ y)).  [para(12(a,1),5(a,1,2,1))].

given #92 (F,wt=19): 687 ((x v x) v ((x v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(646(a,1),97(a,1,1,2,1,1))].

given #93 (F,wt=19): 694 (x v (y ^ (x v x))) ^ (((x v x) v z) v u) = x v x.  [para(646(a,1),202(a,1,1,1)),demod(677(6))].

given #94 (T,wt=17): 1218 (x v (y ^ x)) ^ (((x v x) v z) v u) = x v x.  [para(61(a,1),694(a,1,1,2))].

given #95 (T,wt=19): 714 (x v (x v x)) ^ ((((x v x) v y) v z) v u) = x v x.  [para(646(a,1),423(a,1,1,1)),demod(677(3),677(5))].

given #96 (A,wt=73): 28 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((((z v (v ^ ((y v z) ^ (u v z)))) ^ w) v (v6 ^ ((y v z) ^ (u v z)))) ^ v7)) ^ (((v8 v ((y v z) ^ (u v z))) ^ (v9 v ((y v z) ^ (u v z)))) v v10) = (y v z) ^ (u v z).  [para(5(a,1),5(a,1,1,1,1,2)),demod(5(36),5(46),5(53),5(57),5(64))].

given #97 (F,wt=19): 730 (((x v y) ^ y) v (z ^ y)) ^ (((y v u) v v) v w) = y.  [para(646(a,1),112(a,1,1,1,1,2)),demod(646(7),646(8),646(14))].

given #98 (F,wt=19): 764 (x v x) ^ (((((x v x) v y) v z) v u) v v) = x v x.  [back_demod(444),demod(677(4),677(3),677(4))].

given #99 (T,wt=19): 883 ((x v x) v ((y ^ x) v (y ^ x))) ^ (x v z) = x v x.  [para(786(a,1),148(a,1,1,2))].

given #100 (T,wt=19): 903 ((x v y) v x) ^ ((x v y) v z) = (x v y) v (x v y).  [para(646(a,1),683(a,1,1,2))].

given #101 (A,wt=95): 36 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v z) ^ w) v (v6 ^ (((y v z) ^ (u v z)) v v))) ^ v7)) ^ (((v8 v (((y v z) ^ (u v z)) v v)) ^ (v9 v (((y v z) ^ (u v z)) v v))) v v10) = ((y v z) ^ (u v z)) v v.  [para(3(a,1),26(a,1,1,2,1,1,1,2))].

given #102 (F,wt=19): 913 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v v) = y.  [para(38(a,1),22(a,1,1,1,1,2)),demod(38(13),38(15),38(16),38(20))].

given #103 (F,wt=13): 1423 (((x v y) ^ y) v y) ^ (y v z) = y.  [para(618(a,1),913(a,1,2,1))].

given #104 (T,wt=19): 965 (x v (((x v x) v (y ^ x)) ^ z)) ^ (x v u) = x v x.  [para(14(a,1),674(a,1,1,2))].

given #105 (T,wt=19): 1012 ((x v x) v ((x v x) ^ y)) ^ ((x v x) v z) = x v x.  [para(677(a,1),740(a,1,1,2,1)),demod(677(10))].

given #106 (A,wt=95): 37 (((x v (((y v z) ^ (u v z)) v v)) ^ (((y v z) ^ (u v z)) v v)) v ((((((((y v z) ^ (u v z)) v v) v (((y v z) ^ (u v z)) v v)) v (w ^ (((y v z) ^ (u v z)) v v))) ^ v6) v z) ^ v7)) ^ (((v8 v (((y v z) ^ (u v z)) v v)) ^ (v9 v (((y v z) ^ (u v z)) v v))) v v10) = ((y v z) ^ (u v z)) v v.  [para(3(a,1),26(a,1,1,2,1,2))].

given #107 (F,wt=19): 1115 (((x v y) ^ y) v (y v y)) ^ (((y v z) v u) v v) = y.  [para(655(a,1),50(a,1,1,1,1,2)),demod(655(8),655(9),655(9),655(15))].

given #108 (F,wt=19): 1428 (((x v y) ^ y) v y) ^ (((y v z) v (y v z)) v u) = y.  [para(903(a,1),913(a,1,2,1))].

given #109 (T,wt=17): 1473 (((x v y) ^ y) v y) ^ ((y v z) v (y v z)) = y.  [para(677(a,1),1428(a,1,2))].

given #110 (T,wt=21): 647 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (y v v) = y.  [para(618(a,1),12(a,1,2,1))].

given #111 (A,wt=97): 39 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v ((((((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v)) v (w ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v6) v (v7 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v8)) ^ (z v v9) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(3(a,1),26(a,1,2,1))].

given #112 (F,wt=21): 696 (x v (y ^ (x v x))) ^ ((((x v x) v z) v u) v v) = x v x.  [para(646(a,1),232(a,1,1,1)),demod(677(6))].

given #113 (F,wt=19): 1514 (x v (y ^ x)) ^ ((((x v x) v z) v u) v v) = x v x.  [para(61(a,1),696(a,1,1,2))].

given #114 (T,wt=19): 1516 ((x v x) v x) ^ ((((x v x) v y) v z) v u) = x v x.  [para(181(a,1),696(a,1,1,2)),demod(677(5),677(10))].

given #115 (T,wt=21): 718 (x v (x v x)) ^ (((((x v x) v y) v z) v u) v v) = x v x.  [para(646(a,1),424(a,1,1,1)),demod(677(3),677(5))].

given #116 (A,wt=85): 40 (((x v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) v ((((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w))) ^ (y v v6) = ((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w.  [para(26(a,1),7(a,1,2,1))].

given #117 (F,wt=21): 720 (((x v (y v y)) ^ (y v y)) v y) ^ ((y v z) v u) = y v y.  [para(646(a,1),100(a,1,1,2))].

given #118 (F,wt=21): 734 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(646(a,1),179(a,1,1,2,1,1))].

given #119 (T,wt=19): 1599 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y.  [para(677(a,1),734(a,1,2))].

given #120 (T,wt=21): 742 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [back_demod(664),demod(677(3))].

given #121 (A,wt=49): 42 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (y v y)) ^ u) v (v ^ (y v z))) ^ w)) ^ (((v6 v (y v z)) ^ (v7 v (y v z))) v v8) = y v z.  [para(11(a,1),26(a,1,1,2,1,1,1,2))].

given #122 (F,wt=17): 1642 (x v (((x v x) v x) ^ y)) ^ (x v z) = x v x.  [para(646(a,1),742(a,1,1,2,1,2))].

given #123 (F,wt=21): 791 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [back_demod(74),demod(677(4),677(3))].

given #124 (T,wt=17): 1697 (x v x) ^ (((x v y) v (x v y)) v z) = x v x.  [para(116(a,1),791(a,1,2,1))].

given #125 (T,wt=19): 1698 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x.  [para(677(a,1),791(a,1,2,1,1))].

given #126 (A,wt=7): 1750 x ^ (x v y) = x.  [para(99(a,1),1698(a,1,2,1)),demod(1738(5),1738(7))].

given #127 (F,wt=5): 1787 x v x = x.  [back_demod(1447),demod(1738(5),1738(6),786(3),1738(6))].

given #128 (F,wt=5): 2300 x ^ x = x.  [back_demod(1785),demod(1815(2),1815(3),1815(2),1787(1),1815(3))].

given #129 (T,wt=7): 1815 (x v y) ^ y = y.  [back_demod(1738),demod(1787(5))].

given #130 (T,wt=9): 1835 x ^ ((x v y) v z) = x.  [back_demod(1697),demod(1787(1),1787(3),1787(4))].

given #131 (A,wt=29): 1790 ((x ^ (y v x)) v (((x ^ (y v x)) v x) ^ z)) ^ ((x ^ (y v x)) v u) = x ^ (y v x).  [back_demod(1784),demod(1787(1),1787(1),1787(3),1787(3),1787(5),1787(5),1787(7),1787(5),1787(8),1787(8),1787(12),1787(12),1787(14),1787(14),1787(16))].

given #132 (F,wt=9): 2157 (x ^ y) ^ y = x ^ y.  [back_demod(866),demod(1787(1),1787(3),1815(4),1787(2),1787(3),1787(4),1787(3),1787(2),1787(3))].

given #133 (F,wt=11): 1832 (x ^ y) ^ (y v z) = x ^ y.  [back_demod(1701),demod(1787(3),1787(2),1787(6))].

given #134 (T,wt=11): 1834 x ^ ((x ^ (y v x)) v z) = x.  [back_demod(1698),demod(1787(1),1787(1),1787(1),1787(5))].

given #135 (T,wt=9): 2328 x ^ (x ^ (y v x)) = x.  [para(1787(a,1),1834(a,1,2))].

given #136 (A,wt=31): 1793 (((x ^ (y v x)) v z) v x) ^ (((((x ^ (y v x)) v z) v u) v v) v w) = (x ^ (y v x)) v z.  [back_demod(1781),demod(1787(1),1787(1),1787(4),1787(5),1787(5),1787(8),1787(8),1787(11),1787(12),1787(12),1787(15),1787(15),1787(18))].

given #137 (F,wt=11): 1837 (x ^ y) ^ (x v z) = x ^ y.  [back_demod(1695),demod(1787(1),1787(1),1787(3),1787(3),1815(4),1787(2),1787(2),1787(3),1787(2),1787(4),1787(4))].

given #138 (F,wt=9): 2331 (x ^ y) ^ x = x ^ y.  [para(1787(a,1),1837(a,1,2))].

given #139 (T,wt=7): 2333 x ^ (y v x) = x.  [para(1815(a,1),2331(a,1,1)),demod(1815(4))].

given #140 (T,wt=7): 2336 x v (x ^ y) = x.  [back_demod(2327),demod(2333(2),2333(2),1787(1),2333(4))].

given #141 (A,wt=27): 1818 (((x v y) v z) v ((((x v y) v z) v x) ^ u)) ^ ((x v y) v z) = (x v y) v z.  [back_demod(1735),demod(1787(3),1787(6),1815(6),1787(5),1787(5),1787(10),1787(12),1787(12),1787(13))].

given #142 (F,wt=9): 2332 x ^ ((y v x) v z) = x.  [para(1815(a,1),1837(a,1,1)),demod(1815(5))].

given #143 (F,wt=9): 2335 (x v y) v x = x v y.  [back_demod(2329),demod(2333(2),2333(4))].

given #144 (T,wt=7): 2358 (x v y) ^ x = x.  [para(2335(a,1),1815(a,1,1))].

given #145 (T,wt=9): 2353 x ^ (x ^ y) = x ^ y.  [para(2336(a,1),1815(a,1,1))].

given #146 (A,wt=29): 1819 (((x v y) v z) v ((((x v y) v z) v x) ^ u)) ^ (((x v y) v z) v v) = (x v y) v z.  [back_demod(1734),demod(1787(3),1787(6),1815(6),1787(5),1787(5),1787(10),1787(12),1787(12),1787(14))].

given #147 (F,wt=9): 2354 (x v y) v y = x v y.  [para(1815(a,1),2336(a,1,2))].

given #148 (F,wt=11): 1944 x ^ (((x v y) v z) v u) = x.  [back_demod(1516),demod(1787(1),1787(1),1787(1),1787(5))].

given #149 (T,wt=11): 2196 (x v (y ^ x)) ^ (x v z) = x.  [back_demod(683),demod(1787(5))].

given #150 (T,wt=7): 2361 x v (y ^ x) = x.  [para(2196(a,1),2300(a,1)),flip(a)].

given #151 (A,wt=51): 1822 (((x v y) v z) v (((((u ^ ((x v y) v z)) v (v ^ ((x v y) v z))) ^ w) v x) ^ v6)) ^ (((v7 v ((x v y) v z)) ^ (v8 v ((x v y) v z))) v v9) = (x v y) v z.  [back_demod(1722),demod(1787(3),1787(6),1815(6),1787(5),1787(7),1787(7),1787(8),1787(11),1787(16),1787(19),1787(25))].

given #152 (F,wt=9): 2428 x ^ (y ^ x) = y ^ x.  [para(2361(a,1),1815(a,1,1))].

given #153 (F,wt=9): 2464 ((x v y) v z) ^ x = x.  [para(1835(a,1),2428(a,1,2)),demod(1835(6))].

given #154 (T,wt=9): 2467 ((x v y) v z) ^ y = y.  [para(2332(a,1),2428(a,1,2)),demod(2332(6))].

given #155 (T,wt=11): 2357 x ^ (((y v x) v z) v u) = x.  [para(2332(a,1),1832(a,1,1)),demod(2332(7))].

given #156 (A,wt=51): 1823 (((x v y) v z) v (((((u ^ ((x v y) v z)) v x) ^ v) v (w ^ ((x v y) v z))) ^ v6)) ^ (((v7 v ((x v y) v z)) ^ (v8 v ((x v y) v z))) v v9) = (x v y) v z.  [back_demod(1721),demod(1787(3),1787(6),1815(6),1787(5),1787(7),1787(7),1787(6),1787(10),1787(16),1787(19),1787(25))].

given #157 (F,wt=11): 2430 (x v y) v (z ^ x) = x v y.  [para(1832(a,1),2361(a,1,2))].

given #158 (F,wt=11): 2431 (x v y) v (x ^ z) = x v y.  [para(1837(a,1),2361(a,1,2))].

given #159 (T,wt=11): 2465 (x v y) ^ (z ^ x) = z ^ x.  [para(1832(a,1),2428(a,1,2)),demod(1832(6))].

given #160 (T,wt=11): 2466 (x v y) ^ (x ^ z) = x ^ z.  [para(1837(a,1),2428(a,1,2)),demod(1837(6))].

given #161 (A,wt=31): 1824 (((x v y) v z) v (((u ^ ((x v y) v z)) v x) ^ v)) ^ (((x v y) v z) v w) = (x v y) v z.  [back_demod(1720),demod(1787(3),1787(6),1815(6),1787(5),1787(6),1787(11),1787(13),1787(13),1787(15))].

given #162 (F,wt=11): 2468 (((x v y) v z) v u) ^ x = x.  [para(1944(a,1),2428(a,1,2)),demod(1944(8))].

given #163 (F,wt=11): 2471 (((x v y) v z) v u) ^ y = y.  [para(2357(a,1),2428(a,1,2)),demod(2357(8))].

given #164 (T,wt=13): 1833 x ^ (((y v x) ^ (z v x)) v u) = x.  [back_demod(1700),demod(1787(1),1787(1),1787(2),1815(2),1787(2),1787(3),1815(3),1787(6))].

given #165 (T,wt=11): 2523 x ^ ((y v x) ^ (z v x)) = x.  [para(1787(a,1),1833(a,1,2))].

given #166 (A,wt=31): 1825 (((x v y) v z) v ((x v (u ^ ((x v y) v z))) ^ v)) ^ (((x v y) v z) v w) = (x v y) v z.  [back_demod(1719),demod(1787(3),1787(6),1815(6),1787(3),1787(5),1787(11),1787(13),1787(13),1787(15))].

given #167 (F,wt=11): 2541 x ^ ((x v y) ^ (z v x)) = x.  [para(2335(a,1),2523(a,1,2,1))].

given #168 (F,wt=11): 2542 x ^ ((y v x) ^ (x v z)) = x.  [para(2335(a,1),2523(a,1,2,2))].

given #169 (T,wt=11): 2546 ((x v y) ^ (z v y)) ^ y = y.  [para(2523(a,1),2428(a,1,2)),demod(2523(8))].

given #170 (T,wt=11): 2563 x ^ ((x v y) ^ (x v z)) = x.  [para(2335(a,1),2541(a,1,2,2))].

given #171 (A,wt=23): 1826 ((x v y) v ((x v (z ^ (x v y))) ^ u)) ^ ((x v y) v v) = x v y.  [back_demod(1717),demod(1787(3),1787(5),1815(4),1787(2),1787(4),1787(9),1787(12))].

given #172 (F,wt=29): 2579 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(4),demod(2574(38)),xx(d)].

given #173 (F,wt=11): 2566 ((x v y) ^ (z v x)) ^ x = x.  [para(2541(a,1),2428(a,1,2)),demod(2541(8))].

given #174 (T,wt=11): 2574 ((x v y) ^ (y v z)) ^ y = y.  [para(2542(a,1),2428(a,1,2)),demod(2542(8))].

given #175 (T,wt=11): 2590 ((x v y) ^ (x v z)) ^ x = x.  [para(2563(a,1),2428(a,1,2)),demod(2563(8))].

given #176 (A,wt=29): 1830 ((x v y) v ((x v (x v y)) ^ z)) ^ (((u v (x v y)) ^ (v v (x v y))) v w) = x v y.  [back_demod(1709),demod(1787(3),1787(5),1815(4),1787(2),1787(4),1787(8),1787(10),1787(15))].

given #177 (F,wt=13): 1843 (x ^ y) ^ ((x v z) v u) = x ^ y.  [back_demod(1688),demod(1787(1),1787(1),1787(3),1787(3),1815(4),1787(2),1787(2),1787(3),1787(3),1787(4),1787(3),1787(2),1787(5),1787(5))].

given #178 (F,wt=13): 1982 (x ^ y) ^ ((y v z) v u) = x ^ y.  [back_demod(1421),demod(1815(4),1787(3),1787(4))].

given #179 (T,wt=13): 2046 x ^ ((((x v y) v z) v u) v v) = x.  [back_demod(1293),demod(1815(2),1787(1),1787(1))].

given #180 (T,wt=13): 2429 ((x v y) v z) v x = (x v y) v z.  [para(1835(a,1),2361(a,1,2))].

given #181 (A,wt=29): 1840 (x v (((((x ^ y) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ (((v6 v x) ^ (v7 v x)) v v8) = x.  [back_demod(1692),demod(1787(1),1787(2),1815(2),1787(1),1787(1),1787(2),1787(5),1787(9),1787(10),1787(14))].

given #182 (F,wt=13): 2432 ((x v y) v z) v y = (x v y) v z.  [para(2332(a,1),2361(a,1,2))].

given #183 (F,wt=13): 2469 x ^ ((((y v x) v z) v u) v v) = x.  [para(2357(a,1),1832(a,1,1)),demod(2357(9))].

given #184 (T,wt=13): 2504 ((x v y) v z) ^ (u ^ x) = u ^ x.  [para(2430(a,1),2467(a,1,1,1))].

given #185 (T,wt=13): 2506 ((x v y) v z) ^ (x ^ u) = x ^ u.  [para(2431(a,1),2467(a,1,1,1))].

given #186 (A,wt=33): 1842 ((x ^ y) v (((((z ^ (x ^ y)) v (u ^ (x ^ y))) ^ v) v (w ^ (x ^ y))) ^ v6)) ^ (x v v7) = x ^ y.  [back_demod(1689),demod(1787(1),1787(1),1787(3),1787(3),1815(4),1787(2),1787(2),1787(3),1787(3),1787(4),1787(4),1787(4),1787(8),1787(8),1787(13),1787(15),1787(15))].

given #187 (F,wt=13): 2507 ((((x v y) v z) v u) v v) ^ x = x.  [para(1944(a,1),2465(a,1,2)),demod(1944(9))].

given #188 (F,wt=13): 2508 ((((x v y) v z) v u) v v) ^ y = y.  [para(2357(a,1),2465(a,1,2)),demod(2357(9))].

given #189 (T,wt=13): 2526 x ^ (((x v y) ^ (z v x)) v u) = x.  [para(2335(a,1),1833(a,1,2,1,1))].

given #190 (T,wt=13): 2527 x ^ (((y v x) ^ (x v z)) v u) = x.  [para(2335(a,1),1833(a,1,2,1,2))].

given #191 (A,wt=33): 1846 ((x v y) v (((z ^ (x v y)) v (x ^ u)) ^ v)) ^ (((w v (x v y)) ^ (v6 v (x v y))) v v7) = x v y.  [back_demod(1685),demod(1787(1),1787(3),1815(4),1787(2),1787(3),1787(4),1787(4),1787(4),1787(8),1787(10),1787(15))].

given #192 (F,wt=13): 2531 (((x v y) ^ (z v y)) v u) ^ y = y.  [para(1833(a,1),2428(a,1,2)),demod(1833(10))].

given #193 (F,wt=13): 2570 (((x v y) ^ (z v x)) v u) ^ x = x.  [para(2541(a,1),2465(a,1,2)),demod(2541(9))].

given #194 (T,wt=13): 2578 (((x v y) ^ (y v z)) v u) ^ y = y.  [para(2542(a,1),2465(a,1,2)),demod(2542(9))].

given #195 (T,wt=13): 2588 x ^ (((x v y) ^ (x v z)) v u) = x.  [para(2563(a,1),1832(a,1,1)),demod(2563(9))].

given #196 (A,wt=21): 1849 (x v (((x ^ y) v x) ^ z)) ^ (((u v x) ^ (v v x)) v w) = x.  [back_demod(1682),demod(1787(1),1787(2),1815(2),1787(1),1787(5),1787(6),1787(10))].

given #197 (F,wt=11): 2835 x v (((x ^ y) v x) ^ z) = x.  [para(1849(a,1),2333(a,1)),flip(a)].

given #198 (F,wt=20): 2904 B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(2579),demod(2868(7)),xx(a)].

given #199 (T,wt=9): 2860 x v ((x ^ y) v x) = x.  [para(1750(a,1),2835(a,1,2))].

given #200 (T,wt=7): 2905 (x ^ y) v x = x.  [para(2860(a,1),1815(a,1,1)),demod(2333(3)),flip(a)].

given #201 (A,wt=31): 1851 ((x v y) v ((((x v y) ^ z) v x) ^ u)) ^ (((v v (x v y)) ^ (w v (x v y))) v v6) = x v y.  [back_demod(1680),demod(1787(3),1787(5),1815(4),1787(4),1787(9),1787(11),1787(16))].

given #202 (F,wt=7): 2930 (x ^ y) v y = y.  [para(2428(a,1),2905(a,1,1))].

given #203 (F,wt=9): 2868 x v (y ^ (x ^ z)) = x.  [para(2465(a,1),2835(a,1,2))].

given #204 (T,wt=9): 2870 x v ((x ^ y) ^ z) = x.  [para(2466(a,1),2835(a,1,2))].

given #205 (T,wt=9): 2926 x v (y v x) = y v x.  [para(1815(a,1),2905(a,1,1))].

given #206 (A,wt=25): 1857 ((x ^ y) v ((((x ^ y) ^ z) v (u ^ (x ^ y))) ^ v)) ^ (y v w) = x ^ y.  [back_demod(1673),demod(1787(3),1787(5),1815(4),1787(4),1787(6),1787(9),1787(13))].

given #207 (F,wt=11): 3096 ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(2904),demod(3049(7)),xx(a)].

given #208 (F,wt=9): 2929 x v (x v y) = x v y.  [para(2358(a,1),2905(a,1,1))].

given #209 (T,wt=9): 2968 x v (y ^ (z ^ x)) = x.  [para(2930(a,1),2430(a,1,1)),demod(2930(5))].

given #210 (T,wt=9): 2969 x v ((y ^ x) ^ z) = x.  [para(2930(a,1),2431(a,1,1)),demod(2930(5))].

given #211 (A,wt=17): 1862 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (x v v) = x.  [back_demod(1665),demod(1787(1),1787(2),1815(2),1787(1),1787(2),1787(6),1787(7),1815(7),1787(8))].

given #212 (F,wt=9): 3049 x ^ (y v (x v z)) = x.  [para(2926(a,1),1835(a,1,2))].

given #213 (F,wt=9): 3052 x ^ (y v (z v x)) = x.  [para(2926(a,1),2332(a,1,2))].

given #214 (T,wt=9): 3055 (x v (y v z)) ^ y = y.  [para(2926(a,1),2464(a,1,1))].

given #215 (T,wt=9): 3056 (x v (y v z)) ^ z = z.  [para(2926(a,1),2467(a,1,1))].

given #216 (A,wt=49): 1876 (((x v y) ^ (z v y)) v ((((x v y) ^ (z v y)) v ((y v (u ^ ((x v y) ^ (z v y)))) ^ v)) ^ w)) ^ (((x v y) ^ (z v y)) v v6) = (x v y) ^ (z v y).  [back_demod(1643),demod(1787(10),1787(27))].

given #217 (F,wt=9): 3094 (x ^ (y ^ z)) v y = y.  [para(2868(a,1),2926(a,1,2)),demod(2868(6))].

given #218 (F,wt=9): 3095 ((x ^ y) ^ z) v x = x.  [para(2870(a,1),2926(a,1,2)),demod(2870(6))].

given #219 (T,wt=9): 3146 (x ^ (y ^ z)) v z = z.  [para(2968(a,1),2926(a,1,2)),demod(2968(6))].

given #220 (T,wt=9): 3168 ((x ^ y) ^ z) v y = y.  [para(2969(a,1),2926(a,1,2)),demod(2969(6))].

given #221 (A,wt=21): 1880 (x v ((x v (((y ^ x) v (z ^ x)) ^ u)) ^ v)) ^ (x v w) = x.  [back_demod(1639),demod(1787(1),1787(1),1787(10))].

given #222 (F,wt=11): 2934 (x ^ y) v (y v z) = y v z.  [para(2465(a,1),2905(a,1,1))].

given #223 (F,wt=11): 2936 (x ^ y) v (x v z) = x v z.  [para(2466(a,1),2905(a,1,1))].

given #224 (T,wt=11): 2977 (x v y) v (z ^ y) = x v y.  [para(1815(a,1),2868(a,1,2,2))].

given #225 (T,wt=11): 3013 (x v y) v (y ^ z) = x v y.  [para(1815(a,1),2870(a,1,2,1))].

given #226 (A,wt=23): 1884 (((x ^ y) v (z ^ x)) ^ u) ^ (x v v) = ((x ^ y) v (z ^ x)) ^ u.  [back_demod(1635),demod(1787(1),1787(1),1787(2),1787(6),1787(6),1787(7),1815(10),1787(5),1787(5),1787(6),1787(9),1787(9),1787(10),1787(13),1787(9),1787(5),1787(7),1787(7),1787(8))].

given #227 (F,wt=11): 3050 (x ^ y) ^ (z v y) = x ^ y.  [para(2926(a,1),1832(a,1,2))].

given #228 (F,wt=11): 3051 (x ^ y) ^ (z v x) = x ^ y.  [para(2926(a,1),1837(a,1,2))].

given #229 (T,wt=11): 3053 x ^ ((y v (x v z)) v u) = x.  [para(2926(a,1),1944(a,1,2,1))].

given #230 (T,wt=11): 3054 x ^ (y v ((x v z) v u)) = x.  [para(2926(a,1),1944(a,1,2))].

given #231 (A,wt=57): 1901 ((((x v y) ^ (z v y)) v u) v (((((x v y) ^ (z v y)) v u) v ((y v (v ^ ((x v y) ^ (z v y)))) ^ w)) ^ v6)) ^ ((((x v y) ^ (z v y)) v u) v v7) = ((x v y) ^ (z v y)) v u.  [back_demod(1602),demod(1815(10),1787(26))].

given #232 (F,wt=11): 3057 x ^ ((y v (z v x)) v u) = x.  [para(2926(a,1),2357(a,1,2,1))].

given #233 (F,wt=11): 3058 x ^ (y v ((z v x) v u)) = x.  [para(2926(a,1),2357(a,1,2))].

given #234 (T,wt=11): 3059 (x v y) ^ (z ^ y) = z ^ y.  [para(2926(a,1),2465(a,1,1))].

given #235 (T,wt=11): 3060 (x v y) ^ (y ^ z) = y ^ z.  [para(2926(a,1),2466(a,1,1))].

given #236 (A,wt=29): 1912 ((x v y) v (((x v y) v (((z ^ x) v (u ^ x)) ^ v)) ^ w)) ^ ((x v y) v v6) = x v y.  [back_demod(1586),demod(1815(4),1787(3),1787(12))].

given #237 (F,wt=11): 3061 ((x v (y v z)) v u) ^ y = y.  [para(2926(a,1),2468(a,1,1,1))].

given #238 (F,wt=11): 3062 (x v ((y v z) v u)) ^ y = y.  [para(2926(a,1),2468(a,1,1))].

given #239 (T,wt=11): 3063 ((x v (y v z)) v u) ^ z = z.  [para(2926(a,1),2471(a,1,1,1))].

given #240 (T,wt=11): 3064 (x v ((y v z) v u)) ^ z = z.  [para(2926(a,1),2471(a,1,1))].

given #241 (A,wt=49): 1936 ((((x v y) ^ (z v y)) v u) v ((y v (v ^ ((x v y) ^ (z v y)))) ^ w)) ^ ((((((x v y) ^ (z v y)) v u) v v6) v v7) v v8) = ((x v y) ^ (z v y)) v u.  [back_demod(1534),demod(1787(20),1787(28))].

given #242 (F,wt=11): 3263 (x ^ y) v (z v y) = z v y.  [para(1815(a,1),3094(a,1,1,2))].

given #243 (F,wt=11): 3267 x v (y ^ (z ^ (x ^ u))) = x.  [para(3094(a,1),2430(a,1,1)),demod(3094(7))].

given #244 (T,wt=11): 3268 x v ((y ^ (x ^ z)) ^ u) = x.  [para(3094(a,1),2431(a,1,1)),demod(3094(7))].

given #245 (T,wt=11): 3292 (x ^ y) v (z v x) = z v x.  [para(1815(a,1),3095(a,1,1,1))].

given #246 (A,wt=27): 1940 ((x v y) v (((z ^ x) v (u ^ x)) ^ v)) ^ ((((x v y) v w) v v6) v v7) = x v y.  [back_demod(1528),demod(1787(2),1787(9),1787(14))].

given #247 (F,wt=11): 3296 x v (y ^ ((x ^ z) ^ u)) = x.  [para(3095(a,1),2430(a,1,1)),demod(3095(7))].

given #248 (F,wt=11): 3297 x v (((x ^ y) ^ z) ^ u) = x.  [para(3095(a,1),2431(a,1,1)),demod(3095(7))].

given #249 (T,wt=11): 3323 x v (y ^ (z ^ (u ^ x))) = x.  [para(3146(a,1),2430(a,1,1)),demod(3146(7))].

given #250 (T,wt=11): 3324 x v ((y ^ (z ^ x)) ^ u) = x.  [para(3146(a,1),2431(a,1,1)),demod(3146(7))].

given #251 (A,wt=43): 1941 (((x v y) ^ (z v y)) v ((y v (u ^ ((x v y) ^ (z v y)))) ^ v)) ^ (((((x v y) ^ (z v y)) v w) v v6) v v7) = (x v y) ^ (z v y).  [back_demod(1521),demod(1787(17),1787(24))].

given #252 (F,wt=11): 3334 x v (y ^ ((z ^ x) ^ u)) = x.  [para(3168(a,1),2430(a,1,1)),demod(3168(7))].

given #253 (F,wt=11): 3335 x v (((y ^ x) ^ z) ^ u) = x.  [para(3168(a,1),2431(a,1,1)),demod(3168(7))].

given #254 (T,wt=11): 3396 (x ^ (y ^ (z ^ u))) v z = z.  [para(3094(a,1),2934(a,1,2)),demod(3094(7))].

given #255 (T,wt=11): 3397 (x ^ ((y ^ z) ^ u)) v y = y.  [para(3095(a,1),2934(a,1,2)),demod(3095(7))].

given #256 (A,wt=21): 1947 (x v (((y ^ x) v (z ^ x)) ^ u)) ^ (((x v v) v w) v v6) = x.  [back_demod(1513),demod(1787(1),1787(6),1787(10))].

given #257 (F,wt=11): 3398 (x ^ (y ^ (z ^ u))) v u = u.  [para(3146(a,1),2934(a,1,2)),demod(3146(7))].

given #258 (F,wt=11): 3399 (x ^ ((y ^ z) ^ u)) v z = z.  [para(3168(a,1),2934(a,1,2)),demod(3168(7))].

given #259 (T,wt=11): 3400 ((x ^ (y ^ z)) ^ u) v y = y.  [para(3094(a,1),2936(a,1,2)),demod(3094(7))].

given #260 (T,wt=11): 3401 (((x ^ y) ^ z) ^ u) v x = x.  [para(3095(a,1),2936(a,1,2)),demod(3095(7))].

given #261 (A,wt=39): 1955 ((x v y) v (((((z ^ (x v y)) v (u ^ (x v y))) ^ v) v x) ^ w)) ^ (((v6 v (x v y)) ^ (v7 v (x v y))) v v8) = x v y.  [back_demod(1488),demod(1787(3),1787(5),1815(4),1787(4),1787(6),1787(13),1787(15),1787(20))].

given #262 (F,wt=11): 3402 ((x ^ (y ^ z)) ^ u) v z = z.  [para(3146(a,1),2936(a,1,2)),demod(3146(7))].

given #263 (F,wt=11): 3403 (((x ^ y) ^ z) ^ u) v y = y.  [para(3168(a,1),2936(a,1,2)),demod(3168(7))].

given #264 (T,wt=11): 3539 x ^ (y v (z v (x v u))) = x.  [para(3049(a,1),3050(a,1,1)),demod(3049(7))].

given #265 (T,wt=11): 3540 x ^ (y v (z v (u v x))) = x.  [para(3052(a,1),3050(a,1,1)),demod(3052(7))].

given #266 (A,wt=39): 1956 ((x v y) v (((((z ^ (x v y)) v x) ^ u) v (v ^ (x v y))) ^ w)) ^ (((v6 v (x v y)) ^ (v7 v (x v y))) v v8) = x v y.  [back_demod(1487),demod(1787(3),1787(5),1815(4),1787(4),1787(8),1787(13),1787(15),1787(20))].

given #267 (F,wt=11): 3669 (x v (y v (z v u))) ^ z = z.  [para(3049(a,1),3059(a,1,2)),demod(3049(7))].

given #268 (F,wt=11): 3670 (x v (y v (z v u))) ^ u = u.  [para(3052(a,1),3059(a,1,2)),demod(3052(7))].

given #269 (T,wt=13): 2592 (((x v y) ^ (x v z)) v u) ^ x = x.  [para(2563(a,1),2465(a,1,2)),demod(2563(9))].

given #270 (T,wt=13): 2628 x ^ (((x v y) v z) ^ (u v x)) = x.  [para(2429(a,1),2523(a,1,2,1))].

given #271 (A,wt=23): 1957 ((x v y) v (((z ^ (x v y)) v x) ^ u)) ^ ((x v y) v v) = x v y.  [back_demod(1486),demod(1787(3),1787(5),1815(4),1787(4),1787(9),1787(12))].

given #272 (F,wt=13): 2629 x ^ ((y v x) ^ ((x v z) v u)) = x.  [para(2429(a,1),2523(a,1,2,2))].

given #273 (F,wt=13): 2630 x ^ ((x v y) ^ ((x v z) v u)) = x.  [para(2429(a,1),2541(a,1,2,2))].

given #274 (T,wt=13): 2631 x ^ (((x v y) v z) ^ (x v u)) = x.  [para(2429(a,1),2542(a,1,2,1))].

given #275 (T,wt=13): 2632 (((x v y) v z) ^ (u v x)) ^ x = x.  [para(2429(a,1),2546(a,1,1,1))].

given #276 (A,wt=25): 1963 (((x ^ (y v z)) v y) ^ u) ^ ((y v z) v v) = ((x ^ (y v z)) v y) ^ u.  [back_demod(1479),demod(1787(3),1787(8),1815(10),1787(7),1787(11),1787(13),1787(9),1787(7),1787(10))].

given #277 (F,wt=13): 2633 ((x v y) ^ ((y v z) v u)) ^ y = y.  [para(2429(a,1),2546(a,1,1,2))].

given #278 (F,wt=13): 2634 ((x v y) ^ ((x v z) v u)) ^ x = x.  [para(2429(a,1),2566(a,1,1,2))].

given #279 (T,wt=13): 2635 (((x v y) v z) ^ (x v u)) ^ x = x.  [para(2429(a,1),2574(a,1,1,1))].

given #280 (T,wt=13): 2693 x ^ (((y v x) v z) ^ (u v x)) = x.  [para(2432(a,1),2523(a,1,2,1))].

given #281 (A,wt=35): 1981 (((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w) ^ (y v v6) = ((((x ^ y) v (z ^ y)) ^ u) v (v ^ y)) ^ w.  [back_demod(1424),demod(1787(1),1787(9),1815(16),1787(8),1787(15),1787(10))].

given #282 (F,wt=13): 2694 x ^ ((y v x) ^ ((z v x) v u)) = x.  [para(2432(a,1),2523(a,1,2,2))].

given #283 (F,wt=13): 2695 x ^ ((x v y) ^ ((z v x) v u)) = x.  [para(2432(a,1),2541(a,1,2,2))].

given #284 (T,wt=13): 2696 x ^ (((y v x) v z) ^ (x v u)) = x.  [para(2432(a,1),2542(a,1,2,1))].

given #285 (T,wt=13): 2697 (((x v y) v z) ^ (u v y)) ^ y = y.  [para(2432(a,1),2546(a,1,1,1))].

given #286 (A,wt=23): 1983 (((x ^ y) v (z ^ y)) ^ u) ^ (y v v) = ((x ^ y) v (z ^ y)) ^ u.  [back_demod(1418),demod(1815(10),1787(9),1787(5))].

given #287 (F,wt=13): 2698 ((x v y) ^ ((z v y) v u)) ^ y = y.  [para(2432(a,1),2546(a,1,1,2))].

given #288 (F,wt=13): 2699 ((x v y) ^ ((z v x) v u)) ^ x = x.  [para(2432(a,1),2566(a,1,1,2))].

given #289 (T,wt=13): 2700 (((x v y) v z) ^ (y v u)) ^ y = y.  [para(2432(a,1),2574(a,1,1,1))].

given #290 (T,wt=13): 2927 (x ^ (y ^ z)) ^ y = x ^ (y ^ z).  [para(2905(a,1),1832(a,1,2))].

given #291 (A,wt=53): 2000 (((x v y) ^ (z v y)) v ((((y v (u ^ ((x v y) ^ (z v y)))) ^ v) v (w ^ ((x v y) ^ (z v y)))) ^ v6)) ^ ((((x v y) ^ (z v y)) v v7) v v8) = (x v y) ^ (z v y).  [back_demod(1386),demod(1815(8),1787(25))].

given #292 (F,wt=13): 2928 ((x ^ y) ^ z) ^ x = (x ^ y) ^ z.  [para(2905(a,1),1837(a,1,2))].

given #293 (F,wt=13): 2931 x v ((x v y) v z) = (x v y) v z.  [para(2464(a,1),2905(a,1,1))].

given #294 (T,wt=13): 2932 x v ((y v x) v z) = (y v x) v z.  [para(2467(a,1),2905(a,1,1))].

given #295 (T,wt=13): 2933 x ^ (y ^ (x ^ z)) = y ^ (x ^ z).  [para(2905(a,1),2465(a,1,1))].

given #296 (A,wt=25): 2002 (x v (((((y ^ x) v (z ^ x)) ^ u) v (v ^ x)) ^ w)) ^ ((x v v6) v v7) = x.  [back_demod(1383),demod(1815(2),1787(1),1787(11))].

given #297 (F,wt=13): 2935 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z.  [para(2905(a,1),2466(a,1,1))].

given #298 (F,wt=13): 2966 (x ^ (y ^ z)) ^ z = x ^ (y ^ z).  [para(2930(a,1),1832(a,1,2))].

given #299 (T,wt=13): 2967 ((x ^ y) ^ z) ^ y = (x ^ y) ^ z.  [para(2930(a,1),1837(a,1,2))].

given #300 (T,wt=13): 2970 x ^ (y ^ (z ^ x)) = y ^ (z ^ x).  [para(2930(a,1),2465(a,1,1))].

given #301 (A,wt=49): 2005 ((((x v y) ^ (z v y)) v u) v (((v ^ (((x v y) ^ (z v y)) v u)) v y) ^ w)) ^ (((((x v y) ^ (z v y)) v u) v v6) v v7) = ((x v y) ^ (z v y)) v u.  [back_demod(1379),demod(1815(10),1787(13),1787(23))].

given #302 (F,wt=13): 2971 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z.  [para(2930(a,1),2466(a,1,1))].

given #303 (F,wt=13): 2980 (x v y) v (z ^ (u ^ x)) = x v y.  [para(2465(a,1),2868(a,1,2,2))].

given #304 (T,wt=13): 2981 (x v y) v (z ^ (x ^ u)) = x v y.  [para(2466(a,1),2868(a,1,2,2))].

given #305 (T,wt=13): 3016 (x v y) v ((z ^ x) ^ u) = x v y.  [para(2465(a,1),2870(a,1,2,1))].

given #306 (A,wt=35): 2017 (((x v y) ^ (z v y)) v (((u ^ ((x v y) ^ (z v y))) v y) ^ v)) ^ ((z v y) v w) = (x v y) ^ (z v y).  [back_demod(1358),demod(1787(7),1787(11),1815(8),1787(10),1787(13),1787(20))].

given #307 (F,wt=13): 3017 (x v y) v ((x ^ z) ^ u) = x v y.  [para(2466(a,1),2870(a,1,2,1))].

given #308 (F,wt=13): 3065 x ^ (y v ((z v x) ^ (u v x))) = x.  [para(2926(a,1),1833(a,1,2))].

given #309 (T,wt=13): 3066 (x ^ y) ^ ((z v x) v u) = x ^ y.  [para(2926(a,1),1843(a,1,2,1))].

given #310 (T,wt=13): 3067 (x ^ y) ^ (z v (x v u)) = x ^ y.  [para(2926(a,1),1843(a,1,2))].

given #311 (A,wt=33): 2018 ((x v y) v (((z ^ (x v y)) v (u ^ x)) ^ v)) ^ (((w v (x v y)) ^ (v6 v (x v y))) v v7) = x v y.  [back_demod(1357),demod(1787(1),1787(3),1815(4),1787(2),1787(3),1787(4),1787(6),1787(8),1787(10),1787(15))].

given #312 (F,wt=13): 3068 (x ^ y) ^ ((z v y) v u) = x ^ y.  [para(2926(a,1),1982(a,1,2,1))].

given #313 (F,wt=13): 3069 (x ^ y) ^ (z v (y v u)) = x ^ y.  [para(2926(a,1),1982(a,1,2))].

given #314 (T,wt=13): 3070 x ^ (((y v (x v z)) v u) v v) = x.  [para(2926(a,1),2046(a,1,2,1,1))].

given #315 (T,wt=13): 3071 x ^ ((y v ((x v z) v u)) v v) = x.  [para(2926(a,1),2046(a,1,2,1))].

given #316 (A,wt=63): 2025 ((((x v y) v z) v u) v ((((x v (v ^ (((x v y) v z) v u))) ^ w) v (v6 ^ (((x v y) v z) v u))) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_demod(1342),demod(1787(1),1787(5),1815(8),1787(4),1787(4),1787(10),1787(17),1787(21),1787(28))].

given #317 (F,wt=13): 3072 x ^ (y v (((x v z) v u) v v)) = x.  [para(2926(a,1),2046(a,1,2))].

given #318 (F,wt=13): 3073 (x v (y v z)) v y = x v (y v z).  [para(2926(a,1),2429(a,1,1)),demod(2926(7))].

given #319 (T,wt=13): 3074 (x v (y v z)) v z = x v (y v z).  [para(2926(a,1),2432(a,1,1)),demod(2926(7))].

given #320 (T,wt=13): 3075 x ^ (((y v (z v x)) v u) v v) = x.  [para(2926(a,1),2469(a,1,2,1,1))].

given #321 (A,wt=47): 2026 (((((x v y) v z) v u) v v) v (((w ^ ((((x v y) v z) v u) v v)) v x) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v.  [back_demod(1341),demod(1787(1),1787(6),1815(10),1787(5),1787(10),1787(13),1787(17),1787(21),1787(19))].

given #322 (F,wt=13): 3076 x ^ ((y v ((z v x) v u)) v v) = x.  [para(2926(a,1),2469(a,1,2,1))].

given #323 (F,wt=13): 3077 x ^ (y v (((z v x) v u) v v)) = x.  [para(2926(a,1),2469(a,1,2))].

given #324 (T,wt=13): 3078 ((x v y) v z) ^ (u ^ y) = u ^ y.  [para(2926(a,1),2504(a,1,1,1))].

given #325 (T,wt=13): 3079 (x v (y v z)) ^ (u ^ y) = u ^ y.  [para(2926(a,1),2504(a,1,1))].

given #326 (A,wt=47): 2027 (((((x v y) v z) v u) v v) v ((x v (w ^ ((((x v y) v z) v u) v v))) ^ v6)) ^ (((((x v y) v z) v u) v v) v v7) = (((x v y) v z) v u) v v.  [back_demod(1340),demod(1787(1),1787(6),1815(10),1787(5),1787(5),1787(13),1787(17),1787(21),1787(19))].

given #327 (F,wt=13): 3080 ((x v y) v z) ^ (y ^ u) = y ^ u.  [para(2926(a,1),2506(a,1,1,1))].

given #328 (F,wt=13): 3081 (x v (y v z)) ^ (y ^ u) = y ^ u.  [para(2926(a,1),2506(a,1,1))].

given #329 (T,wt=13): 3082 (((x v (y v z)) v u) v v) ^ y = y.  [para(2926(a,1),2507(a,1,1,1,1))].

given #330 (T,wt=13): 3083 ((x v ((y v z) v u)) v v) ^ y = y.  [para(2926(a,1),2507(a,1,1,1))].

given #331 (A,wt=15): 2031 x ^ (((((x v y) v z) v u) v v) v w) = x.  [back_demod(1333),demod(1787(1),1787(2),1815(2),1787(1),1787(1),1787(1),1787(7))].

given #332 (F,wt=13): 3084 (x v (((y v z) v u) v v)) ^ y = y.  [para(2926(a,1),2507(a,1,1))].

given #333 (F,wt=13): 3085 (((x v (y v z)) v u) v v) ^ z = z.  [para(2926(a,1),2508(a,1,1,1,1))].

given #334 (T,wt=13): 3086 ((x v ((y v z) v u)) v v) ^ z = z.  [para(2926(a,1),2508(a,1,1,1))].

given #335 (T,wt=13): 3087 (x v (((y v z) v u) v v)) ^ z = z.  [para(2926(a,1),2508(a,1,1))].

given #336 (A,wt=51): 2037 ((((x v y) v z) v u) v ((x v (v ^ (((x v y) v z) v u))) ^ w)) ^ (((v6 v (((x v y) v z) v u)) ^ (v7 v (((x v y) v z) v u))) v v8) = ((x v y) v z) v u.  [back_demod(1321),demod(1787(1),1787(5),1815(8),1787(4),1787(4),1787(11),1787(15),1787(22))].

given #337 (F,wt=13): 3088 x ^ (y v ((x v z) ^ (u v x))) = x.  [para(2926(a,1),2526(a,1,2))].

given #338 (F,wt=13): 3089 x ^ (y v ((z v x) ^ (x v u))) = x.  [para(2926(a,1),2527(a,1,2))].

given #339 (T,wt=13): 3090 (x v ((y v z) ^ (u v z))) ^ z = z.  [para(2926(a,1),2531(a,1,1))].

given #340 (T,wt=13): 3091 (x v ((y v z) ^ (u v y))) ^ y = y.  [para(2926(a,1),2570(a,1,1))].

given #341 (A,wt=63): 2040 ((((x v y) v z) v u) v (((((v ^ (((x v y) v z) v u)) v (w ^ (((x v y) v z) v u))) ^ v6) v x) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_demod(1309),demod(1815(8),1787(10))].

given #342 (F,wt=13): 3092 (x v ((y v z) ^ (z v u))) ^ z = z.  [para(2926(a,1),2578(a,1,1))].

given #343 (F,wt=13): 3093 x ^ (y v ((x v z) ^ (x v u))) = x.  [para(2926(a,1),2588(a,1,2))].

given #344 (T,wt=13): 3170 x v (((x ^ y) v (z ^ x)) ^ u) = x.  [para(1862(a,1),2300(a,1)),flip(a)].

given #345 (T,wt=11): 7862 x v ((x ^ y) v (z ^ x)) = x.  [para(1750(a,1),3170(a,1,2))].

given #346 (A,wt=63): 2041 ((((x v y) v z) v u) v (((((v ^ (((x v y) v z) v u)) v x) ^ w) v (v6 ^ (((x v y) v z) v u))) ^ v7)) ^ (((v8 v (((x v y) v z) v u)) ^ (v9 v (((x v y) v z) v u))) v v10) = ((x v y) v z) v u.  [back_demod(1308),demod(1815(8),1787(10))].

given #347 (F,wt=11): 8039 x v ((x ^ y) v (x ^ z)) = x.  [para(2331(a,1),7862(a,1,2,2))].

given #348 (F,wt=11): 8045 x v ((y ^ x) v (z ^ x)) = x.  [para(2428(a,1),7862(a,1,2,1))].

given #349 (T,wt=11): 8098 ((x ^ y) v (z ^ x)) v x = x.  [para(7862(a,1),2926(a,1,2)),demod(7862(8))].

given #350 (T,wt=11): 8320 x v ((y ^ x) v (x ^ z)) = x.  [para(2428(a,1),8039(a,1,2,1))].

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

% Proof 1 at 4.31 (+ 0.02) seconds: McKenzie.
% Length of proof is 100.
% Level of proof is 32.
% Maximum clause weight is 89.
% Given clauses 350.

3 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ (((w v y) ^ (v6 v y)) v v7) = y # label(A2).  [input].
4 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B | ((A v B) ^ (B v C)) ^ B != B # answer(McKenzie).  [input].
5 (((x v ((y v z) ^ (u v z))) ^ ((y v z) ^ (u v z))) v ((z v (v ^ ((y v z) ^ (u v z)))) ^ w)) ^ (((v6 v ((y v z) ^ (u v z))) ^ (v7 v ((y v z) ^ (u v z)))) v v8) = (y v z) ^ (u v z).  [para(3(a,1),3(a,1,1,2,1,1))].
7 (((x v y) ^ y) v (y v y)) ^ (((z v y) ^ (u v y)) v v) = y.  [para(3(a,1),3(a,1,1,2))].
8 (((x v (((y ^ (z v z)) v (u ^ z)) ^ v)) ^ (((y ^ (z v z)) v (u ^ z)) ^ v)) v (((w ^ ((((y ^ (z v z)) v (u ^ z)) ^ v) v (((y ^ (z v z)) v (u ^ z)) ^ v))) v (v6 ^ (((y ^ (z v z)) v (u ^ z)) ^ v))) ^ v7)) ^ (z v v8) = ((y ^ (z v z)) v (u ^ z)) ^ v.  [para(3(a,1),3(a,1,2,1))].
11 (((x v (y v y)) ^ (y v y)) v ((y v y) v (y v y))) ^ (y v z) = y v y.  [para(7(a,1),7(a,1,2,1))].
12 (((x v y) ^ y) v (((y v y) v (z ^ y)) ^ u)) ^ (((v v y) ^ (w v y)) v v6) = y.  [para(11(a,1),3(a,1,1,2,1,1))].
18 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (z ^ (y v y))) ^ u)) ^ (y v v) = y v y.  [para(7(a,1),12(a,1,2,1))].
22 (((x v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) v u) ^ (((w v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)))) ^ (v6 v ((y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u))))) v v7) = (y v ((z v u) ^ u)) ^ (v v ((z v u) ^ u)).  [para(3(a,1),5(a,1,1,2))].
26 (((x v y) ^ y) v (((((y v y) v (z ^ y)) ^ u) v (v ^ y)) ^ w)) ^ (((v6 v y) ^ (v7 v y)) v v8) = y.  [para(12(a,1),5(a,1,1,1,1,2)),demod(12(17),12(22),12(26),12(27),12(31))].
30 (((x v (y v y)) ^ (y v y)) v ((((y v y) v (y v y)) v (y v y)) ^ z)) ^ (y v u) = y v y.  [para(11(a,1),18(a,1,1,2,1,2))].
38 (((x v y) ^ y) v (z ^ y)) ^ (((u v y) ^ (v v y)) v w) = y.  [para(3(a,1),26(a,1,1,2))].
42 (((x v (y v z)) ^ (y v z)) v ((((((y v z) v (y v z)) v (y v y)) ^ u) v (v ^ (y v z))) ^ w)) ^ (((v6 v (y v z)) ^ (v7 v (y v z))) v v8) = y v z.  [para(11(a,1),26(a,1,1,2,1,1,1,2))].
51 (((x v (y v y)) ^ (y v y)) v (z ^ (y v y))) ^ (y v u) = y v y.  [para(7(a,1),38(a,1,2,1))].
61 (((x v (y ^ z)) ^ (y ^ z)) v (u ^ (y ^ z))) ^ (z v v) = y ^ z.  [para(38(a,1),38(a,1,2,1))].
71 (((x v (y v y)) ^ (y v y)) v (y v y)) ^ (y v z) = y v y.  [para(11(a,1),51(a,1,1,2))].
74 ((x v x) v ((x v x) v (x v x))) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [para(71(a,1),7(a,1,1,1))].
87 ((x v x) v (y ^ (x v x))) ^ (x v z) = x v x.  [para(71(a,1),51(a,1,1,1))].
88 ((x v x) v (x v x)) ^ (x v y) = x v x.  [para(71(a,1),71(a,1,1,1))].
97 ((x v x) v (((y ^ (x v x)) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(8(a,1),87(a,1,1,2))].
99 (((x v y) ^ y) v (z ^ y)) ^ ((((u v y) ^ (v v y)) v w) v v6) = y.  [para(3(a,1),61(a,1,1,1,1,2)),demod(3(14),3(15),3(23))].
107 (((x v (y v y)) ^ (y v y)) v (z ^ y)) ^ (y v u) = y v y.  [para(61(a,1),51(a,1,1,2))].
108 ((x v x) v (y ^ x)) ^ (x v z) = x v x.  [para(61(a,1),87(a,1,1,2))].
116 (((x v y) v (x v y)) v (x v x)) ^ ((x v y) v z) = (x v y) v (x v y).  [para(11(a,1),108(a,1,1,2))].
148 ((x v x) v (((y ^ x) v (z ^ x)) ^ u)) ^ (x v v) = x v x.  [para(61(a,1),97(a,1,1,2,1,1))].
165 ((x v x) v x) ^ (x v y) = x v x.  [para(3(a,1),148(a,1,1,2))].
179 (((x v y) ^ y) v (((z ^ (y v y)) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(165(a,1),3(a,1,2,1))].
180 (((x v y) ^ y) v (y v y)) ^ ((y v y) v z) = y.  [para(165(a,1),7(a,1,2,1))].
202 (((x v y) ^ y) v (z ^ y)) ^ (((y v y) v u) v v) = y.  [para(180(a,1),61(a,1,1,1,1,2)),demod(180(8),180(9),180(15))].
232 (((x v y) ^ y) v (z ^ y)) ^ ((((y v y) v u) v v) v w) = y.  [para(202(a,1),61(a,1,1,1,1,2)),demod(202(9),202(10),202(17))].
600 (((x v y) ^ y) v (((z ^ y) v (u ^ y)) ^ v)) ^ ((y v y) v w) = y.  [para(61(a,1),179(a,1,1,2,1,1))].
618 (((x v y) ^ y) v y) ^ ((y v y) v z) = y.  [para(3(a,1),600(a,1,1,2))].
646 (((x v y) ^ y) v (y v y)) ^ (y v z) = y.  [para(618(a,1),7(a,1,2,1))].
651 (((x v y) ^ y) v (z ^ y)) ^ (y v u) = y.  [para(618(a,1),38(a,1,2,1))].
664 (x v ((((x v x) v (x v x)) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [para(646(a,1),18(a,1,1,1))].
666 (x v ((((x v x) v (x v x)) v (x v x)) ^ y)) ^ (x v z) = x v x.  [para(646(a,1),30(a,1,1,1))].
676 (x v (x v x)) ^ (x v y) = x v x.  [para(646(a,1),71(a,1,1,1))].
677 (x v x) v (x v x) = x v x.  [para(71(a,1),646(a,1,1,1)),demod(676(8))].
683 (x v (y ^ x)) ^ (x v z) = x v x.  [para(646(a,1),107(a,1,1,1))].
696 (x v (y ^ (x v x))) ^ ((((x v x) v z) v u) v v) = x v x.  [para(646(a,1),232(a,1,1,1)),demod(677(6))].
734 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ ((y v y) v v) = y.  [para(646(a,1),179(a,1,1,2,1,1))].
740 (x v ((x v x) ^ y)) ^ (x v z) = x v x.  [back_demod(666),demod(677(3),677(3))].
742 (x v (((x v x) v (y ^ (x v x))) ^ z)) ^ (x v u) = x v x.  [back_demod(664),demod(677(3))].
786 (x v x) ^ (x v y) = x v x.  [back_demod(88),demod(677(3))].
791 (x v x) ^ (((y v (x v x)) ^ (z v (x v x))) v u) = x v x.  [back_demod(74),demod(677(4),677(3))].
883 ((x v x) v ((y ^ x) v (y ^ x))) ^ (x v z) = x v x.  [para(786(a,1),148(a,1,1,2))].
913 (((x v y) ^ y) v y) ^ (((z v y) ^ (u v y)) v v) = y.  [para(38(a,1),22(a,1,1,1,1,2)),demod(38(13),38(15),38(16),38(20))].
1012 ((x v x) v ((x v x) ^ y)) ^ ((x v x) v z) = x v x.  [para(677(a,1),740(a,1,1,2,1)),demod(677(10))].
1447 ((((x v y) ^ y) v ((x v y) ^ y)) v y) ^ ((((x v y) ^ y) v ((x v y) ^ y)) v z) = ((x v y) ^ y) v ((x v y) ^ y).  [para(38(a,1),1012(a,1,1,2))].
1514 (x v (y ^ x)) ^ ((((x v x) v z) v u) v v) = x v x.  [para(61(a,1),696(a,1,1,2))].
1599 (((x v y) ^ y) v ((y v (z ^ y)) ^ u)) ^ (y v y) = y.  [para(677(a,1),734(a,1,2))].
1616 (((x v ((y v z) ^ z)) ^ ((y v z) ^ z)) v z) ^ (((y v z) ^ z) v ((y v z) ^ z)) = (y v z) ^ z.  [para(3(a,1),1599(a,1,1,2))].
1642 (x v (((x v x) v x) ^ y)) ^ (x v z) = x v x.  [para(646(a,1),742(a,1,1,2,1,2))].
1665 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v (u ^ (y v y))) ^ v)) ^ (((w v (y v y)) ^ (y v y)) v v6) = y v y.  [para(677(a,1),42(a,1,2,1,2)),demod(677(7),677(7))].
1682 (((x v (y v y)) ^ (y v y)) v ((((y v y) ^ z) v y) ^ u)) ^ (((v v (y v y)) ^ (w v (y v y))) v v6) = y v y.  [para(1599(a,1),42(a,1,1,2,1,2)),demod(677(7),677(7))].
1695 (((x v (((y v y) v y) ^ z)) ^ (((y v y) v y) ^ z)) v (((y v y) v y) ^ z)) ^ ((y v y) v u) = ((y v y) v y) ^ z.  [para(1642(a,1),913(a,1,2,1))].
1697 (x v x) ^ (((x v y) v (x v y)) v z) = x v x.  [para(116(a,1),791(a,1,2,1))].
1698 (x v x) ^ (((x v x) ^ (y v (x v x))) v z) = x v x.  [para(677(a,1),791(a,1,2,1,1))].
1700 (x v x) ^ (((y v ((z v (x v x)) ^ (x v x))) ^ (u v ((z v (x v x)) ^ (x v x)))) v v) = x v x.  [para(22(a,1),791(a,1,2,1))].
1701 ((x ^ y) v (x ^ y)) ^ ((y v y) v z) = (x ^ y) v (x ^ y).  [para(883(a,1),791(a,1,2,1))].
1738 ((x v y) ^ y) v ((x v y) ^ y) = y.  [para(38(a,1),1698(a,1,2,1)),demod(651(7)),flip(a)].
1750 x ^ (x v y) = x.  [para(99(a,1),1698(a,1,2,1)),demod(1738(5),1738(7))].
1781 ((((x v x) ^ (y v (x v x))) v z) v (x v x)) ^ (((((((x v x) ^ (y v (x v x))) v z) v (((x v x) ^ (y v (x v x))) v z)) v u) v v) v w) = (((x v x) ^ (y v (x v x))) v z) v (((x v x) ^ (y v (x v x))) v z).  [para(1698(a,1),1514(a,1,1,2))].
1785 (((x v ((y v z) ^ z)) ^ ((y v z) ^ z)) v z) ^ z = (y v z) ^ z.  [back_demod(1616),demod(1738(12))].
1787 x v x = x.  [back_demod(1447),demod(1738(5),1738(6),786(3),1738(6))].
1793 (((x ^ (y v x)) v z) v x) ^ (((((x ^ (y v x)) v z) v u) v v) v w) = (x ^ (y v x)) v z.  [back_demod(1781),demod(1787(1),1787(1),1787(4),1787(5),1787(5),1787(8),1787(8),1787(11),1787(12),1787(12),1787(15),1787(15),1787(18))].
1815 (x v y) ^ y = y.  [back_demod(1738),demod(1787(5))].
1832 (x ^ y) ^ (y v z) = x ^ y.  [back_demod(1701),demod(1787(3),1787(2),1787(6))].
1833 x ^ (((y v x) ^ (z v x)) v u) = x.  [back_demod(1700),demod(1787(1),1787(1),1787(2),1815(2),1787(2),1787(3),1815(3),1787(6))].
1835 x ^ ((x v y) v z) = x.  [back_demod(1697),demod(1787(1),1787(3),1787(4))].
1837 (x ^ y) ^ (x v z) = x ^ y.  [back_demod(1695),demod(1787(1),1787(1),1787(3),1787(3),1815(4),1787(2),1787(2),1787(3),1787(2),1787(4),1787(4))].
1849 (x v (((x ^ y) v x) ^ z)) ^ (((u v x) ^ (v v x)) v w) = x.  [back_demod(1682),demod(1787(1),1787(2),1815(2),1787(1),1787(5),1787(6),1787(10))].
1862 (x v (((x ^ y) v (z ^ x)) ^ u)) ^ (x v v) = x.  [back_demod(1665),demod(1787(1),1787(2),1815(2),1787(1),1787(2),1787(6),1787(7),1815(7),1787(8))].
2196 (x v (y ^ x)) ^ (x v z) = x.  [back_demod(683),demod(1787(5))].
2300 x ^ x = x.  [back_demod(1785),demod(1815(2),1815(3),1815(2),1787(1),1815(3))].
2329 ((x ^ (y v x)) v z) v x = (x ^ (y v x)) v z.  [para(1793(a,1),1835(a,1)),flip(a)].
2331 (x ^ y) ^ x = x ^ y.  [para(1787(a,1),1837(a,1,2))].
2333 x ^ (y v x) = x.  [para(1815(a,1),2331(a,1,1)),demod(1815(4))].
2335 (x v y) v x = x v y.  [back_demod(2329),demod(2333(2),2333(4))].
2361 x v (y ^ x) = x.  [para(2196(a,1),2300(a,1)),flip(a)].
2428 x ^ (y ^ x) = y ^ x.  [para(2361(a,1),1815(a,1,1))].
2465 (x v y) ^ (z ^ x) = z ^ x.  [para(1832(a,1),2428(a,1,2)),demod(1832(6))].
2523 x ^ ((y v x) ^ (z v x)) = x.  [para(1787(a,1),1833(a,1,2))].
2542 x ^ ((y v x) ^ (x v z)) = x.  [para(2335(a,1),2523(a,1,2,2))].
2574 ((x v y) ^ (y v z)) ^ y = y.  [para(2542(a,1),2428(a,1,2)),demod(2542(8))].
2579 B v (A ^ (B ^ C)) != B | B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(4),demod(2574(38)),xx(d)].
2835 x v (((x ^ y) v x) ^ z) = x.  [para(1849(a,1),2333(a,1)),flip(a)].
2860 x v ((x ^ y) v x) = x.  [para(1750(a,1),2835(a,1,2))].
2868 x v (y ^ (x ^ z)) = x.  [para(2465(a,1),2835(a,1,2))].
2904 B ^ (A v (B v C)) != B | ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(2579),demod(2868(7)),xx(a)].
2905 (x ^ y) v x = x.  [para(2860(a,1),1815(a,1,1)),demod(2333(3)),flip(a)].
2926 x v (y v x) = y v x.  [para(1815(a,1),2905(a,1,1))].
3049 x ^ (y v (x v z)) = x.  [para(2926(a,1),1835(a,1,2))].
3096 ((A ^ B) v (B ^ C)) v B != B # answer(McKenzie).  [back_demod(2904),demod(3049(7)),xx(a)].
3170 x v (((x ^ y) v (z ^ x)) ^ u) = x.  [para(1862(a,1),2300(a,1)),flip(a)].
7862 x v ((x ^ y) v (z ^ x)) = x.  [para(1750(a,1),3170(a,1,2))].
8039 x v ((x ^ y) v (x ^ z)) = x.  [para(2331(a,1),7862(a,1,2,2))].
8320 x v ((y ^ x) v (x ^ z)) = x.  [para(2428(a,1),8039(a,1,2,1))].
8733 ((x ^ y) v (y ^ z)) v y = y.  [para(8320(a,1),2926(a,1,2)),demod(8320(8))].
8734 $F # answer(McKenzie).  [resolve(8733,a,3096,a)].

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

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

Given=350. Generated=93657. Kept=8731. proofs=1.
Usable=179. Sos=5814. Demods=6017. Denials=0. Limbo=25, Disabled=2714. Hints=0.
Weight_deleted=7832. Literals_deleted=0.
Forward_subsumed=77026. Back_subsumed=289.
Sos_limit_deleted=68. Sos_displaced=0. Sos_removed=0.
New_demodulators=8726 (0 lex), Back_demodulated=2423. Back_unit_deleted=0.
Demod_attempts=4166047. Demod_rewrites=278355.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=3.
Megabytes=10.99.
User_CPU=4.31, System_CPU=0.02, Wall_clock=4.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 13093 exit (max_proofs) Mon Jun 19 16:41:20 2006