----- Prover9 July-2005E-work, 18 July 2005 -----
Process 28709 was started by mccune on theorem.mcs.anl.gov,
Tue Aug  9 11:36:27 2005
The command was "prover9 -f winker1.in".

% Reading from file winker1.in

set(auto).
    % set(auto) -> set(auto1).
    % set(auto1) -> set(auto_inference).
    % set(auto1) -> set(fof_reduction).
    % set(auto1) -> set(predicate_elimination).
    % set(auto1) -> set(unfold_eq).
    % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647).
    % set(unfold_eq) -> clear(fold_eq).
    % set(auto1) -> set(inverse_order).
    % set(auto1) -> assign(new_constants, 1).
    % assign(new_constants, 1) -> clear(x_proofs).
    % assign(new_constants, 1) -> clear(rx_proofs).
    % set(auto1) -> assign(lex_dep_demod_lim, 11).
    % set(auto1) -> set(lex_dep_demod_sane).
    % set(auto1) -> assign(max_weight, 100).
    % set(auto1) -> assign(age_part, 1).
    % set(auto1) -> assign(weight_part, 2).
    % set(auto1) -> assign(weight_neg_part, 2).
    % set(auto1) -> assign(sos_limit, 10000).
    % set(auto1) -> clear(x_proofs).
    % set(auto1) -> assign(stats, lots).
    % set(auto1) -> assign(max_megs, 200).
    % set(auto1) -> clear(clocks).

clauses(sos).
(x v y) v z = x v (y v z).
x v y = y v x.
((x v y ') ' v (x v y) ') ' = x.
C v D = C.
end_of_list.
assign(max_proofs,- 1).

clauses(goals).
A v A != A # answer(Idempotence).
(B v A ') ' v (A ' v B ') ' != A # answer(Huntington_a) # action(in_proof -> exit).
(A v B ') ' v (A ' v B ') ' != B # answer(Huntington_b) # action(in_proof -> exit).
end_of_list.

% Finished reading the input.

% Entering prover search function.
% Assigned IDs to 7 clauses.
% Relation symbol precedence:  lex([ = ]).
% Function symbol precedence:  lex([ C, D, A, B, v, ' ]).
% After inverse_order: % Function symbol precedence:  lex([ C, D, A, B, v, ' ]).
% Unfolding symbols: (none).

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

% Reasonable options, based on the structure of the clauses:
  % (nothing changed)

% Operation v is associative-commutative; redundancy checks enabled.

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
8 (x v y) v z = x v (y v z).  [input]
9 x v y = y v x.  [input]
10 ((x v y) ' v (x v y ') ') ' = x.  [copy 3 demod (9)]
11 C v D = C.  [input]
end_of_list.

clauses(demodulators).
8 (x v y) v z = x v (y v z).  [input]
9 x v y = y v x.  [input]
        % (lex-dep)
10 ((x v y) ' v (x v y ') ') ' = x.  [copy 3 demod (9)]
11 C v D = C.  [input]
end_of_list.

clauses(goals).
12 A v A != A # answer(Idempotence).  [input]
13 (B v A ') ' v (A ' v B ') ' != A # answer(Huntington_a) # action(in_proof -> exit).  [input]
14 (A v B ') ' v (A ' v B ') ' != B # answer(Huntington_b) # action(in_proof -> exit).  [input]
end_of_list.

% Starting search at 0.02 seconds.

given #1 (wt=11): 8 (x v y) v z = x v (y v z).  [input]

given #2 (wt=7): 9 x v y = y v x.  [input]

given #3 (wt=13): 10 ((x v y) ' v (x v y ') ') ' = x.  [copy 3 demod (9)]

given #4 (wt=5): 11 C v D = C.  [input]

given #5 (wt=9): 24 C v (D v x) = C v x.  [para (11 (a 1) 8 (a 1 1)) flip a]

given #6 (wt=11): 15 x v (y v z) = y v (x v z).  [para (9 (a 1) 8 (a 1 1)) demod (8)]

given #7 (wt=9): 27 C v (x v D) = C v x.  [para (9 (a 1) 24 (a 1 2))]

given #8 (wt=11): 16 x v (y v z) = z v (x v y).  [para (9 (a 1) 8 (a 1)) flip a]

given #9 (wt=11): 17 x v (y v z) = x v (z v y).  [para (9 (a 1) 8 (a 2 2)) demod (8)]

given #10 (wt=11): 25 (C ' v (C v D ') ') ' = C.  [para (11 (a 1) 10 (a 1 1 1 1))]

given #11 (wt=19): 18 ((x v (y v z)) ' v (x v (y v z ')) ') ' = x v y.  [para (8 (a 1) 10 (a 1 1 1 1)) demod (8)]

given #12 (wt=11): 33 x v (y v z) = z v (y v x).  [para (9 (a 1) 16 (a 2 2))]

given #13 (wt=11): 36 C v (x v y) = x v (y v C).  [para (16 (a 2) 24 (a 2)) demod (24)]

given #14 (wt=13): 19 ((x v y) ' v (y v x ') ') ' = y.  [para (9 (a 1) 10 (a 1 1 1 1))]

given #15 (wt=11): 74 (C ' v (D v C ') ') ' = D.  [para (11 (a 1) 19 (a 1 1 1 1))]

given #16 (wt=13): 20 ((x v y) ' v (y ' v x) ') ' = x.  [para (9 (a 1) 10 (a 1 1 2 1))]

given #17 (wt=13): 26 D v (x v (C v y)) = x v (C v y).  [para (24 (a 1) 8 (a 2 2)) demod (15 8)]

given #18 (wt=13): 30 C v (x v (D v y)) = C v (x v y).  [para (15 (a 1) 24 (a 1 2))]

given #19 (wt=13): 31 C v (x v (y v D)) = C v (x v y).  [para (8 (a 1) 27 (a 1 2))]

given #20 (wt=13): 67 ((x v y) ' v (x ' v y) ') ' = y.  [para (9 (a 1) 19 (a 1 1 2 1))]

given #21 (wt=20): 21 (x v ((x v y) ' v (x v y ') ' ') ') ' = (x v y) '.  [para (10 (a 1) 10 (a 1 1 1))]

given #22 (wt=9): 158 (x v y) ' = (y v x) '.  [para (9 (a 1) 21 (a 1 1 2 1 1 1)) demod (69)]

given #23 (wt=13): 68 ((x v y ') ' v (y v x) ') ' = x.  [para (9 (a 1) 19 (a 1 1))]

given #24 (wt=13): 90 ((x ' v y) ' v (y v x) ') ' = y.  [para (9 (a 1) 20 (a 1 1))]

given #25 (wt=13): 115 D v (x v (y v C)) = x v (C v y).  [para (9 (a 1) 26 (a 1 2 2))]

given #26 (wt=21): 22 ((x v y) ' v (x v ((y v z) ' v (y v z ') ')) ') ' = x.  [para (10 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #27 (wt=13): 258 D v (x v (y v C)) = x v (y v C).  [para (9 (a 1) 115 (a 2 2))]

given #28 (wt=14): 40 (C v (C v (C ' v D ')) ') ' = C '.  [para (25 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #29 (wt=14): 86 (D v (D v (C ' v C ')) ') ' = C '.  [para (74 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #30 (wt=15): 28 ((C v x) ' v (C v (D v x) ') ') ' = C.  [para (24 (a 1) 10 (a 1 1 1 1))]

given #31 (wt=18): 23 (x v (x v (y ' v (x v y) ')) ') ' = (x v y) '.  [para (10 (a 1) 10 (a 1 1 2)) demod (9 8 9)]

given #32 (wt=13): 384 (C ' v (C v (D v D) ') ') ' = C.  [para (11 (a 1) 28 (a 1 1 1 1))]

given #33 (wt=15): 32 ((C v x) ' v (C v (x v D) ') ') ' = C.  [para (27 (a 1) 10 (a 1 1 1 1))]

given #34 (wt=15): 382 ((x v C) ' v (C v (D v x) ') ') ' = C.  [para (9 (a 1) 28 (a 1 1 1 1))]

given #35 (wt=15): 491 ((x v C) ' v (C v (x v D) ') ') ' = C.  [para (9 (a 1) 32 (a 1 1 1 1))]

given #36 (wt=17): 29 ((x v (y v z)) ' v (y v (x v z) ') ') ' = y.  [para (15 (a 1) 10 (a 1 1 1 1))]

given #37 (wt=15): 557 ((C v x) ' v (D v (C v x) ') ') ' = D.  [para (24 (a 1) 29 (a 1 1 1 1))]

given #38 (wt=15): 607 ((x v C) ' v (D v (C v x) ') ') ' = D.  [para (9 (a 1) 557 (a 1 1 1 1))]

given #39 (wt=15): 608 ((C v x) ' v (D v (x v C) ') ') ' = D.  [para (9 (a 1) 557 (a 1 1 2 1 2 1))]

given #40 (wt=15): 639 ((x v C) ' v (D v (x v C) ') ') ' = D.  [para (9 (a 1) 607 (a 1 1 2 1 2 1))]

given #41 (wt=17): 34 ((x v (y v z)) ' v (y v (z v x) ') ') ' = y.  [para (16 (a 1) 10 (a 1 1 1 1))]

given #42 (wt=16): 38 (C v (C ' v (C v D ') ' ') ') ' = C '.  [para (25 (a 1) 10 (a 1 1 1))]

given #43 (wt=16): 84 (D v (C ' v (D v C ') ' ') ') ' = C '.  [para (74 (a 1) 10 (a 1 1 1))]

given #44 (wt=16): 353 (C ' v (C v (C v (C ' v D '))) ') ' = C.  [para (40 (a 1) 10 (a 1 1 2)) demod (9)]

given #45 (wt=16): 368 (C ' v (D v (D v (C ' v C '))) ') ' = D.  [para (86 (a 1) 10 (a 1 1 2)) demod (9)]

given #46 (wt=17): 35 ((x v (y v z)) ' v (z v (x v y) ') ') ' = z.  [para (16 (a 2) 10 (a 1 1 1 1))]

given #47 (wt=16): 473 (C v (C v (C ' v (D v D) ')) ') ' = C '.  [para (384 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #48 (wt=17): 37 ((x v (y v z)) ' v (x v (z v y) ') ') ' = x.  [para (17 (a 1) 10 (a 1 1 1 1))]

given #49 (wt=17): 50 ((x v C) ' v (x v (C v D ')) ') ' = x v C.  [para (11 (a 1) 18 (a 1 1 1 1 2))]

given #50 (wt=17): 55 ((C v x) ' v (C v (x v D ')) ') ' = C v x.  [para (27 (a 1) 18 (a 1 1 1 1))]

given #51 (wt=19): 39 ((x v C) ' v (x v (C ' v (C v D ') ')) ') ' = x.  [para (25 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #52 (wt=17): 63 ((x v (y v z)) ' v (z v (y v x) ') ') ' = z.  [para (33 (a 1) 10 (a 1 1 1 1))]

given #53 (wt=17): 75 ((C v x) ' v (D v (x v C ')) ') ' = D v x.  [para (24 (a 1) 19 (a 1 1 1 1)) demod (8)]

given #54 (wt=11): 1040 D v (x v y) = x v (y v D).  [para (16 (a 2) 75 (a 2)) demod (8 1029)]

given #55 (wt=15): 1034 (C ' v (D v (D v C ')) ') ' = D v D.  [para (11 (a 1) 75 (a 1 1 1 1))]

given #56 (wt=25): 41 ((x v (y v (z v u))) ' v (x v (y v (z v u '))) ') ' = x v (y v z).  [para (8 (a 1) 18 (a 1 1 1 1 2)) demod (8)]

given #57 (wt=17): 76 ((C v x) ' v (x v (D v C ')) ') ' = x v D.  [para (27 (a 1) 19 (a 1 1 1 1)) demod (8)]

given #58 (wt=17): 96 ((x v (y v z)) ' v ((x v z) ' v y) ') ' = y.  [para (15 (a 1) 20 (a 1 1 1 1))]

given #59 (wt=17): 97 ((x v (y v z)) ' v ((z v x) ' v y) ') ' = y.  [para (16 (a 1) 20 (a 1 1 1 1))]

given #60 (wt=17): 98 ((x v (y v z)) ' v ((x v y) ' v z) ') ' = z.  [para (16 (a 2) 20 (a 1 1 1 1))]

given #61 (wt=19): 42 ((x v (y v z)) ' v (x v (z v y ')) ') ' = x v z.  [para (9 (a 1) 18 (a 1 1 1 1 2))]

given #62 (wt=17): 99 ((x v (y v z)) ' v ((z v y) ' v x) ') ' = x.  [para (17 (a 1) 20 (a 1 1 1 1))]

given #63 (wt=17): 101 (C v (C v (C v D ') ') ') ' = (C v D ') '.  [para (25 (a 1) 20 (a 1 1 2)) demod (9 9)]

given #64 (wt=17): 105 ((x v (y v z)) ' v ((y v x) ' v z) ') ' = z.  [para (33 (a 1) 20 (a 1 1 1 1))]

given #65 (wt=17): 111 (D v (C v (D v C ') ') ') ' = (D v C ') '.  [para (74 (a 1) 20 (a 1 1 2)) demod (9 9)]

given #66 (wt=19): 43 ((x v (y v z)) ' v (z v (x v y ')) ') ' = z v x.  [para (9 (a 1) 18 (a 1 1 1 1)) demod (8)]

given #67 (wt=17): 114 D v (x v (y v (C v z))) = C v (x v (y v z)).  [para (8 (a 1) 26 (a 1 2)) demod (15 8)]

given #68 (wt=17): 123 C v (x v (y v (D v z))) = C v (x v (y v z)).  [para (8 (a 1) 30 (a 1 2)) demod (8)]

given #69 (wt=17): 125 C v (x v (y v (z v D))) = C v (x v (y v z)).  [para (16 (a 2) 30 (a 1 2 2))]

given #70 (wt=17): 137 ((C v x) ' v (D v (C ' v x)) ') ' = D v x.  [para (24 (a 1) 67 (a 1 1 1 1)) demod (15)]

given #71 (wt=19): 44 ((x v (y v z)) ' v (x v (z ' v y)) ') ' = x v y.  [para (9 (a 1) 18 (a 1 1 2 1 2))]

given #72 (wt=17): 202 ((x v (y v z) ') ' v (y v (z v x)) ') ' = x.  [para (8 (a 1) 68 (a 1 1 2 1))]

given #73 (wt=17): 206 ((x v (D v C ')) ' v (C v x) ') ' = x v D.  [para (27 (a 1) 68 (a 1 1 2 1)) demod (8)]

given #74 (wt=17): 226 ((x v (y v z) ') ' v (z v (y v x)) ') ' = x.  [para (158 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #75 (wt=17): 232 (((x v y) ' v z) ' v (x v (z v y)) ') ' = z.  [para (15 (a 1) 90 (a 1 1 2 1))]

given #76 (wt=19): 45 ((x v (y v z)) ' v (y v (z ' v x)) ') ' = x v y.  [para (9 (a 1) 18 (a 1 1 2 1)) demod (8)]

given #77 (wt=17): 234 (((x v y) ' v z) ' v (y v (z v x)) ') ' = z.  [para (16 (a 1) 90 (a 1 1 2 1))]

given #78 (wt=17): 236 (((x v y) ' v z) ' v (z v (y v x)) ') ' = z.  [para (17 (a 1) 90 (a 1 1 2 1))]

given #79 (wt=17): 256 D v (x v (y v (z v C))) = C v (x v (y v z)).  [para (8 (a 1) 115 (a 1 2)) demod (15 8)]

given #80 (wt=17): 385 ((C v x) ' v (C v (D v (D v x)) ') ') ' = C.  [para (24 (a 1) 28 (a 1 1 1 1))]

given #81 (wt=28): 46 (x v (y v ((x v (y v z)) ' v (x v (y v z ')) ' ') ')) ' = (x v (y v z)) '.  [para (18 (a 1) 10 (a 1 1 1)) demod (8)]

given #82 (wt=15): 2283 (C ' v (C v (D v (D v D)) ') ') ' = C.  [para (11 (a 1) 385 (a 1 1 1 1))]

given #83 (wt=17): 387 ((C v x) ' v (C v (D v (x v D)) ') ') ' = C.  [para (27 (a 1) 28 (a 1 1 1 1))]

given #84 (wt=17): 555 ((x v (y v z) ') ' v (y v (x v z)) ') ' = x.  [para (9 (a 1) 29 (a 1 1))]

given #85 (wt=17): 707 ((x v (y v z) ') ' v (z v (x v y)) ') ' = x.  [para (9 (a 1) 34 (a 1 1))]

given #86 (wt=27): 47 ((x v (y v z)) ' v (x v ((y v (z v u)) ' v (y v (z v u ')) ')) ') ' = x.  [para (18 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #87 (wt=17): 908 ((C v x) ' v (x v (C v D ')) ') ' = x v C.  [para (9 (a 1) 50 (a 1 1 1 1))]

given #88 (wt=17): 909 ((x v C) ' v (C v (D ' v x)) ') ' = x v C.  [para (9 (a 1) 50 (a 1 1 2 1)) demod (8)]

given #89 (wt=17): 913 ((x v C) ' v (C v (x v D ')) ') ' = x v C.  [para (15 (a 1) 50 (a 1 1 2 1))]

given #90 (wt=17): 933 ((C v x) ' v (C v (D ' v x)) ') ' = C v x.  [para (9 (a 1) 55 (a 1 1 2 1 2))]

given #91 (wt=26): 48 (x v (y v (x v (y v (z ' v (x v (y v z)) '))) ')) ' = (x v (y v z)) '.  [para (18 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #92 (wt=17): 1030 ((x v C) ' v (D v (x v C ')) ') ' = D v x.  [para (9 (a 1) 75 (a 1 1 1 1))]

given #93 (wt=17): 1070 (C ' v (D v (C ' v (C v D ') ')) ') ' = D.  [para (1040 (a 1) 39 (a 1 1 2 1)) demod (9 11 9 15)]

given #94 (wt=17): 1185 ((x v C) ' v (x v (D v C ')) ') ' = x v D.  [para (9 (a 1) 76 (a 1 1 1 1))]

given #95 (wt=17): 1585 ((D v C ') ' v (C v (D v C ') ') ') ' = D.  [para (111 (a 1) 10 (a 1 1 2)) demod (15 24 9)]

given #96 (wt=27): 49 ((x v (y v z)) ' v (x v (y v ((z v u) ' v (z v u ') '))) ') ' = x v y.  [para (10 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #97 (wt=17): 1793 ((x v C) ' v (D v (C ' v x)) ') ' = D v x.  [para (9 (a 1) 137 (a 1 1 1 1))]

given #98 (wt=17): 2279 ((x v C) ' v (C v (D v (D v x)) ') ') ' = C.  [para (9 (a 1) 385 (a 1 1 1 1))]

given #99 (wt=17): 2289 ((C v x) ' v (C v (x v (D v D)) ') ') ' = C.  [para (16 (a 1) 385 (a 1 1 2 1 2 1))]

given #100 (wt=17): 2463 ((x v C) ' v (C v (D v (x v D)) ') ') ' = C.  [para (9 (a 1) 387 (a 1 1 1 1))]

given #101 (wt=21): 51 ((x v (C v y)) ' v (x v (C v (D v y) ')) ') ' = x v C.  [para (24 (a 1) 18 (a 1 1 1 1 2))]

given #102 (wt=17): 2668 ((x v (C v D ')) ' v (C v x) ') ' = x v C.  [para (9 (a 1) 908 (a 1 1))]

given #103 (wt=17): 2708 ((C v (D ' v x)) ' v (x v C) ') ' = x v C.  [para (9 (a 1) 909 (a 1 1))]

given #104 (wt=17): 3341 ((D v (C ' v x)) ' v (x v C) ') ' = D v x.  [para (9 (a 1) 1793 (a 1 1))]

given #105 (wt=17): 3386 ((x v C) ' v (C v (x v (D v D)) ') ') ' = C.  [para (16 (a 1) 2279 (a 1 1 2 1 2 1))]

given #106 (wt=23): 52 ((x v (y v (z v u))) ' v (x v (z v (y v u) ')) ') ' = x v z.  [para (15 (a 1) 18 (a 1 1 1 1 2))]

given #107 (wt=18): 71 (x v (x v (y ' v (y v x) ')) ') ' = (y v x) '.  [para (19 (a 1) 10 (a 1 1 2)) demod (9 8 9)]

given #108 (wt=18): 93 (x v (y ' v (x v (x v y) ')) ') ' = (x v y) '.  [para (20 (a 1) 10 (a 1 1 2)) demod (9 8 9)]

given #109 (wt=18): 135 (x v (y ' v (x v (y v x) ')) ') ' = (y v x) '.  [para (67 (a 1) 10 (a 1 1 2)) demod (9 8 9)]

given #110 (wt=18): 352 (C ' v (C v (C v (C ' v D ')) ' ') ') ' = C.  [para (40 (a 1) 10 (a 1 1 1))]

given #111 (wt=19): 53 ((x v (y v z)) ' v (y v (x v z ')) ') ' = y v x.  [para (15 (a 1) 18 (a 1 1 1 1))]

given #112 (wt=18): 367 (C ' v (D v (D v (C ' v C ')) ' ') ') ' = D.  [para (86 (a 1) 10 (a 1 1 1))]

given #113 (wt=18): 423 (C ' v (C v (C ' v (C v D ') ' ')) ') ' = C.  [para (25 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 25)]

given #114 (wt=18): 432 (C ' v (D v (C ' v (D v C ') ' ')) ') ' = D.  [para (74 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 74)]

given #115 (wt=18): 471 (C v (C ' v (C v (D v D) ') ' ') ') ' = C '.  [para (384 (a 1) 10 (a 1 1 1))]

given #116 (wt=21): 54 ((x v (C v y)) ' v (x v (C v (y v D) ')) ') ' = x v C.  [para (27 (a 1) 18 (a 1 1 1 1 2))]

given #117 (wt=18): 856 (C ' v (C v (C v (C ' v (D v D) '))) ') ' = C.  [para (473 (a 1) 10 (a 1 1 2)) demod (9)]

given #118 (wt=18): 1073 (D v (D v (D v (D v (C ' v C '))) ')) ' = C '.  [para (1034 (a 1) 10 (a 1 1 2)) demod (15 15 9 8)]

given #119 (wt=18): 2437 (C v (C v (C ' v (D v (D v D)) ')) ') ' = C '.  [para (2283 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #120 (wt=19): 57 ((x v (y v z)) ' v (y v (z v x ')) ') ' = y v z.  [para (16 (a 1) 18 (a 1 1 1 1))]

given #121 (wt=23): 56 ((x v (y v (z v u))) ' v (x v (z v (u v y) ')) ') ' = x v z.  [para (16 (a 1) 18 (a 1 1 1 1 2))]

given #122 (wt=19): 58 ((x v (y v z)) ' v (z ' v (x v y)) ') ' = x v y.  [para (16 (a 1) 18 (a 1 1 2 1))]

given #123 (wt=19): 65 ((x v (y v z)) ' v (z v (y v x ')) ') ' = z v y.  [para (33 (a 1) 18 (a 1 1 1 1))]

given #124 (wt=19): 66 ((x v (y v z)) ' v (z ' v (y v x)) ') ' = x v y.  [para (33 (a 1) 18 (a 1 1 2 1))]

given #125 (wt=19): 77 (C v (C ' ' v (C v D ') ') ') ' = (C v D ') '.  [para (25 (a 1) 19 (a 1 1 1)) demod (9)]

given #126 (wt=23): 59 ((x v (y v (z v u))) ' v (x v (u v (y v z) ')) ') ' = x v u.  [para (16 (a 2) 18 (a 1 1 1 1 2))]

given #127 (wt=19): 78 ((C ' v ((C v D ') ' v x)) ' v (x v C) ') ' = x.  [para (25 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #128 (wt=19): 85 ((x v D) ' v (x v (C ' v (D v C ') ')) ') ' = x.  [para (74 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #129 (wt=17): 5661 (C ' v (C v (C ' v (D v C ') ')) ') ' = C.  [para (11 (a 1) 85 (a 1 1 1 1))]

given #130 (wt=19): 88 (D v (C ' ' v (D v C ') ') ') ' = (D v C ') '.  [para (74 (a 1) 19 (a 1 1 1)) demod (9)]

given #131 (wt=23): 60 ((x v (y v (z v u))) ' v (x v (y v (u v z) ')) ') ' = x v y.  [para (17 (a 1) 18 (a 1 1 1 1 2))]

given #132 (wt=19): 89 ((C ' v ((D v C ') ' v x)) ' v (x v D) ') ' = x.  [para (74 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #133 (wt=19): 95 (x v (x v (y v (x v y ') ')) ') ' = (x v y ') '.  [para (10 (a 1) 20 (a 1 1 2)) demod (9 8 9)]

given #134 (wt=19): 100 ((x v (C ' v (C v D ') ')) ' v (C v x) ') ' = x.  [para (25 (a 1) 20 (a 1 1 2 1 1))]

given #135 (wt=19): 109 (x v (y v (x v (x v y ') ')) ') ' = (x v y ') '.  [para (19 (a 1) 20 (a 1 1 2)) demod (9 8 9)]

given #136 (wt=25): 61 ((x v (y v C)) ' v (x v (y v (C ' v (C v D ') '))) ') ' = x v y.  [para (25 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #137 (wt=19): 110 ((x v (C ' v (D v C ') ')) ' v (D v x) ') ' = x.  [para (74 (a 1) 20 (a 1 1 2 1 1))]

given #138 (wt=19): 113 (x v (x v (y v (y ' v x) ')) ') ' = (y ' v x) '.  [para (20 (a 1) 20 (a 1 1 2)) demod (9 8 9)]

given #139 (wt=19): 116 ((x v (C v y)) ' v (D v (x v (C v y)) ') ') ' = D.  [para (26 (a 1) 10 (a 1 1 1 1))]

given #140 (wt=19): 124 ((C v (x v y)) ' v (C v (x v (D v y)) ') ') ' = C.  [para (30 (a 1) 10 (a 1 1 1 1))]

given #141 (wt=33): 62 ((x v (y v (z v u))) ' v (x v (y v ((z v (u v v)) ' v (z v (u v v ')) '))) ') ' = x v y.  [para (18 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #142 (wt=19): 129 ((C v (x v y)) ' v (C v (x v (y v D)) ') ') ' = C.  [para (31 (a 1) 10 (a 1 1 1 1))]

given #143 (wt=19): 138 ((x v (y v z)) ' v (y ' v (x v z)) ') ' = x v z.  [para (15 (a 1) 67 (a 1 1 1 1))]

given #144 (wt=19): 139 ((x v (y v z)) ' v (y v (x ' v z)) ') ' = y v z.  [para (15 (a 1) 67 (a 1 1 2 1))]

given #145 (wt=19): 140 ((x v (y v z)) ' v (y ' v (z v x)) ') ' = z v x.  [para (16 (a 1) 67 (a 1 1 1 1))]

given #146 (wt=23): 64 ((x v (y v (z v u))) ' v (x v (u v (z v y) ')) ') ' = x v u.  [para (33 (a 1) 18 (a 1 1 1 1 2))]

given #147 (wt=19): 141 ((x v (y v z)) ' v (z v (x ' v y)) ') ' = y v z.  [para (16 (a 1) 67 (a 1 1 2 1))]

given #148 (wt=19): 142 ((x v (y v z)) ' v (x ' v (z v y)) ') ' = z v y.  [para (17 (a 1) 67 (a 1 1 1 1))]

given #149 (wt=19): 143 ((C v x) ' v (C ' v ((C v D ') ' v x)) ') ' = x.  [para (25 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #150 (wt=19): 150 ((D v x) ' v (C ' v ((D v C ') ' v x)) ') ' = x.  [para (74 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #151 (wt=20): 69 (x v ((y v x) ' v (x v y ') ' ') ') ' = (y v x) '.  [para (19 (a 1) 10 (a 1 1 1))]

given #152 (wt=19): 152 (x v (y v (x v (y ' v x) ')) ') ' = (y ' v x) '.  [para (67 (a 1) 20 (a 1 1 2)) demod (9 8 9)]

given #153 (wt=19): 201 ((x v (y v z ')) ' v (z v (x v y)) ') ' = x v y.  [para (8 (a 1) 68 (a 1 1 1 1))]

given #154 (wt=19): 205 ((x v (y v z ')) ' v (x v (z v y)) ') ' = x v y.  [para (15 (a 1) 68 (a 1 1 2 1)) demod (8)]

given #155 (wt=19): 207 ((x v (y v z ')) ' v (y v (z v x)) ') ' = x v y.  [para (16 (a 1) 68 (a 1 1 2 1)) demod (8)]

given #156 (wt=21): 70 ((x v y) ' v (x v ((z v y) ' v (y v z ') ')) ') ' = x.  [para (19 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #157 (wt=19): 208 ((x v (y v z ')) ' v (z v (y v x)) ') ' = x v y.  [para (17 (a 1) 68 (a 1 1 2 1)) demod (8)]

given #158 (wt=19): 209 ((x v C) ' v (C ' v ((C v D ') ' v x)) ') ' = x.  [para (25 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #159 (wt=19): 212 ((x v (y v z ')) ' v (y v (x v z)) ') ' = x v y.  [para (33 (a 1) 68 (a 1 1 2 1)) demod (8)]

given #160 (wt=19): 215 ((x v D) ' v (C ' v ((D v C ') ' v x)) ') ' = x.  [para (74 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #161 (wt=21): 72 (x v ((x v y ') ' v (x v y) ' ') ') ' = (x v y ') '.  [para (10 (a 1) 19 (a 1 1 1))]

given #162 (wt=19): 228 ((x ' v (y v z)) ' v (y v (z v x)) ') ' = y v z.  [para (8 (a 1) 90 (a 1 1 2 1))]

given #163 (wt=19): 231 ((x v (y ' v z)) ' v (x v (z v y)) ') ' = x v z.  [para (15 (a 1) 90 (a 1 1 1 1)) demod (8)]

given #164 (wt=19): 233 ((x v (y ' v z)) ' v (z v (x v y)) ') ' = z v x.  [para (16 (a 1) 90 (a 1 1 1 1)) demod (8)]

given #165 (wt=19): 235 ((x ' v (y v z)) ' v (z v (y v x)) ') ' = z v y.  [para (17 (a 1) 90 (a 1 1 1 1)) demod (8)]

given #166 (wt=21): 73 (((x v y) ' v ((x v y ') ' v z)) ' v (z v x) ') ' = z.  [para (10 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #167 (wt=19): 237 ((C v x) ' v (x v (C ' v (C v D ') ')) ') ' = x.  [para (25 (a 1) 90 (a 1 1 1 1 1))]

given #168 (wt=19): 242 ((D v x) ' v (x v (C ' v (D v C ') ')) ') ' = x.  [para (74 (a 1) 90 (a 1 1 1 1 1))]

given #169 (wt=19): 259 ((x v (C v y)) ' v (D v (x v (y v C)) ') ') ' = D.  [para (115 (a 1) 10 (a 1 1 1 1))]

given #170 (wt=19): 272 (C ' v (C v ((D v x) ' v (D v x ') ')) ') ' = C.  [para (11 (a 1) 22 (a 1 1 1 1))]

given #171 (wt=27): 79 ((x v (y v z)) ' v (x v (y v ((u v z) ' v (z v u ') '))) ') ' = x v y.  [para (19 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #172 (wt=19): 345 ((x v (y v C)) ' v (D v (x v (y v C)) ') ') ' = D.  [para (258 (a 1) 10 (a 1 1 1 1))]

given #173 (wt=19): 386 ((x v (C v y)) ' v (C v (D v (x v y)) ') ') ' = C.  [para (15 (a 1) 28 (a 1 1 1 1))]

given #174 (wt=19): 388 ((x v (C v y)) ' v (C v (D v (y v x)) ') ') ' = C.  [para (16 (a 1) 28 (a 1 1 1 1))]

given #175 (wt=19): 389 ((C v (x v y)) ' v (C v (y v (D v x)) ') ') ' = C.  [para (16 (a 1) 28 (a 1 1 2 1 2 1))]

given #176 (wt=29): 80 (x v (y v ((x v (y v z ')) ' v (x v (y v z)) ' ') ')) ' = (x v (y v z ')) '.  [para (18 (a 1) 19 (a 1 1 1)) demod (8)]

given #177 (wt=19): 390 ((x v (y v C)) ' v (C v (D v (x v y)) ') ') ' = C.  [para (16 (a 2) 28 (a 1 1 1 1))]

given #178 (wt=19): 391 ((C v (x v y)) ' v (C v (D v (y v x)) ') ') ' = C.  [para (17 (a 1) 28 (a 1 1 1 1))]

given #179 (wt=19): 393 ((x v (y v C)) ' v (C v (D v (y v x)) ') ') ' = C.  [para (33 (a 1) 28 (a 1 1 1 1))]

given #180 (wt=19): 394 ((C v (x v y)) ' v (C v (y v (x v D)) ') ') ' = C.  [para (33 (a 1) 28 (a 1 1 2 1 2 1))]

given #181 (wt=27): 81 (((x v (y v z)) ' v ((x v (y v z ')) ' v u)) ' v (u v (x v y)) ') ' = u.  [para (18 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #182 (wt=19): 556 ((x v (C v y)) ' v (C v (x v (D v y)) ') ') ' = C.  [para (24 (a 1) 29 (a 1 1 1 1 2))]

given #183 (wt=19): 559 ((x v (C v y)) ' v (C v (x v (y v D)) ') ') ' = C.  [para (27 (a 1) 29 (a 1 1 1 1 2))]

given #184 (wt=19): 565 ((x v C) ' v (C ' v (x v (C v D ') ')) ') ' = x.  [para (25 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #185 (wt=19): 573 ((x v D) ' v (C ' v (x v (D v C ') ')) ') ' = x.  [para (74 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #186 (wt=21): 82 (x v ((x v y ') ' v (y v x) ' ') ') ' = (x v y ') '.  [para (19 (a 1) 19 (a 1 1 1))]

given #187 (wt=19): 612 ((x v (C v y)) ' v (D v (C v (x v y)) ') ') ' = D.  [para (15 (a 1) 557 (a 1 1 1 1))]

given #188 (wt=19): 613 ((C v (x v y)) ' v (D v (x v (C v y)) ') ') ' = D.  [para (15 (a 1) 557 (a 1 1 2 1 2 1))]

given #189 (wt=19): 614 ((x v (C v y)) ' v (D v (C v (y v x)) ') ') ' = D.  [para (16 (a 1) 557 (a 1 1 1 1))]

given #190 (wt=19): 615 ((C v (x v y)) ' v (D v (y v (C v x)) ') ') ' = D.  [para (16 (a 1) 557 (a 1 1 2 1 2 1))]

given #191 (wt=21): 83 (((x v y) ' v ((y v x ') ' v z)) ' v (z v y) ') ' = z.  [para (19 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #192 (wt=19): 616 ((x v (y v C)) ' v (D v (C v (x v y)) ') ') ' = D.  [para (16 (a 2) 557 (a 1 1 1 1))]

given #193 (wt=19): 617 ((C v (x v y)) ' v (D v (x v (y v C)) ') ') ' = D.  [para (16 (a 2) 557 (a 1 1 2 1 2 1))]

given #194 (wt=19): 618 ((C v (x v y)) ' v (D v (C v (y v x)) ') ') ' = D.  [para (17 (a 1) 557 (a 1 1 1 1))]

given #195 (wt=19): 620 ((x v (y v C)) ' v (D v (C v (y v x)) ') ') ' = D.  [para (33 (a 1) 557 (a 1 1 1 1))]

given #196 (wt=25): 87 ((x v (y v D)) ' v (x v (y v (C ' v (D v C ') '))) ') ' = x v y.  [para (74 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #197 (wt=19): 621 ((C v (x v y)) ' v (D v (y v (x v C)) ') ') ' = D.  [para (33 (a 1) 557 (a 1 1 2 1 2 1))]

given #198 (wt=19): 710 ((x v (C v y)) ' v (C v (y v (D v x)) ') ') ' = C.  [para (27 (a 1) 34 (a 1 1 1 1 2)) demod (8)]

given #199 (wt=19): 781 (C v (C v (C v (C ' v (C ' v D ')))) ') ' = C '.  [para (353 (a 1) 10 (a 1 1 2)) demod (15 15 9)]

given #200 (wt=19): 800 (D v (D v (D v (C ' v (C ' v C ')))) ') ' = C '.  [para (368 (a 1) 10 (a 1 1 2)) demod (15 15 9)]

given #201 (wt=20): 91 (x v ((x v y) ' v (y ' v x) ' ') ') ' = (x v y) '.  [para (20 (a 1) 10 (a 1 1 1))]

given #202 (wt=19): 897 ((x v (y v C)) ' v (D v (y v (C v x)) ') ') ' = D.  [para (258 (a 1) 37 (a 1 1 1 1)) demod (8)]

given #203 (wt=19): 1226 ((C v x) ' v (C ' v (x v (C v D ') ')) ') ' = x.  [para (25 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #204 (wt=19): 1234 ((D v x) ' v (C ' v (x v (D v C ') ')) ') ' = x.  [para (74 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #205 (wt=19): 1385 ((x v (y v z)) ' v (x v (y ' v z)) ') ' = x v z.  [para (9 (a 1) 42 (a 1 1 2 1 2))]

given #206 (wt=21): 92 ((x v y) ' v (x v ((y v z) ' v (z ' v y) ')) ') ' = x.  [para (20 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #207 (wt=19): 1386 ((x v (y v z)) ' v (z v (y ' v x)) ') ' = x v z.  [para (9 (a 1) 42 (a 1 1 2 1)) demod (8)]

given #208 (wt=19): 1514 ((C v D ') ' v (C v (C v (C v D ') ')) ') ' = C.  [para (101 (a 1) 10 (a 1 1 2)) demod (9)]

given #209 (wt=19): 2284 ((C v x) ' v (C v (D v (D v (D v x))) ') ') ' = C.  [para (24 (a 1) 385 (a 1 1 1 1))]

given #210 (wt=17): 10162 (C ' v (C v (D v (D v (D v D))) ') ') ' = C.  [para (11 (a 1) 2284 (a 1 1 1 1))]

given #211 (wt=21): 94 ((x v ((y v z) ' v (y v z ') ')) ' v (y v x) ') ' = x.  [para (10 (a 1) 20 (a 1 1 2 1 1))]

low water: id=5281, wt=55

low water: id=5293, wt=53

low water: id=5598, wt=48

low water: id=5356, wt=47

low water: id=5600, wt=46

low water: id=5707, wt=45

low water: id=5859, wt=44

low water: id=6075, wt=43

low water: id=6045, wt=42

low water: id=6305, wt=41

low water: id=6674, wt=40

given #212 (wt=19): 2286 ((C v x) ' v (C v (D v (D v (x v D))) ') ') ' = C.  [para (27 (a 1) 385 (a 1 1 1 1))]

low water: id=6704, wt=39

given #213 (wt=19): 3492 ((x v C) ' v (x v (C v (D v D) ')) ') ' = x v C.  [para (11 (a 1) 51 (a 1 1 1 1 2))]

given #214 (wt=19): 3531 ((C v x) ' v (x v (C v (D v D) ')) ') ' = x v C.  [para (1040 (a 2) 51 (a 1 1 1 1)) demod (16 24)]

low water: id=6789, wt=38

given #215 (wt=19): 6679 ((x v (y v C)) ' v (D v (x v (C v y)) ') ') ' = D.  [para (9 (a 1) 116 (a 1 1 1 1 2))]

given #216 (wt=27): 102 ((x v (y v z)) ' v (x v (y v ((z v u) ' v (u ' v z) '))) ') ' = x v y.  [para (20 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #217 (wt=19): 6684 ((x v (C v y)) ' v (D v (y v (x v C)) ') ') ' = D.  [para (16 (a 1) 116 (a 1 1 2 1 2 1))]

low water: id=7167, wt=37

given #218 (wt=19): 6689 ((x v (C v y)) ' v (D v (y v (C v x)) ') ') ' = D.  [para (33 (a 1) 116 (a 1 1 1 1))]

given #219 (wt=19): 6727 ((x v (y v C)) ' v (C v (x v (D v y)) ') ') ' = C.  [para (16 (a 2) 124 (a 1 1 1 1))]

given #220 (wt=19): 6730 ((x v (y v C)) ' v (C v (y v (D v x)) ') ') ' = C.  [para (33 (a 1) 124 (a 1 1 1 1))]

given #221 (wt=27): 103 ((x v ((y v (z v u)) ' v (y v (z v u ')) ')) ' v (y v (z v x)) ') ' = x.  [para (18 (a 1) 20 (a 1 1 2 1 1)) demod (8)]

given #222 (wt=19): 6792 ((x v (C v y)) ' v (C v (y v (x v D)) ') ') ' = C.  [para (16 (a 1) 129 (a 1 1 1 1))]

low water: id=7417, wt=36

given #223 (wt=19): 6793 ((x v (y v C)) ' v (C v (x v (y v D)) ') ') ' = C.  [para (16 (a 2) 129 (a 1 1 1 1))]

given #224 (wt=19): 6794 ((x v (y v C)) ' v (C v (y v (x v D)) ') ') ' = C.  [para (33 (a 1) 129 (a 1 1 1 1))]

given #225 (wt=19): 6829 ((x ' v (y v z)) ' v (y v (x v z)) ') ' = y v z.  [para (9 (a 1) 138 (a 1 1))]

low water: id=7553, wt=35

given #226 (wt=27): 104 (x v (y v (x v (y v (z v (x v (y v z ')) '))) ')) ' = (x v (y v z ')) '.  [para (18 (a 1) 20 (a 1 1 2)) demod (9 8 8 9 8)]

given #227 (wt=19): 7007 ((x v (y ' v z)) ' v (y v (x v z)) ') ' = x v z.  [para (9 (a 1) 139 (a 1 1))]

given #228 (wt=19): 7186 ((x ' v (y v z)) ' v (z v (x v y)) ') ' = y v z.  [para (9 (a 1) 140 (a 1 1))]

given #229 (wt=19): 7423 ((x v (y ' v z)) ' v (y v (z v x)) ') ' = z v x.  [para (9 (a 1) 141 (a 1 1))]

low water: id=7781, wt=34

given #230 (wt=19): 7596 ((x ' v (y v z)) ' v (x v (z v y)) ') ' = y v z.  [para (9 (a 1) 142 (a 1 1))]

given #231 (wt=21): 106 (x v ((y ' v x) ' v (x v y) ' ') ') ' = (y ' v x) '.  [para (20 (a 1) 19 (a 1 1 1))]

given #232 (wt=19): 8132 ((x v (y ' v z)) ' v (z v (y v x)) ') ' = z v x.  [para (9 (a 1) 205 (a 1 1 1 1)) demod (8)]

low water: id=8041, wt=33

given #233 (wt=19): 8320 (C ' v (C v ((x v D) ' v (D v x ') ')) ') ' = C.  [para (11 (a 1) 70 (a 1 1 1 1))]

given #234 (wt=19): 9218 ((x v (y v C)) ' v (D v (y v (x v C)) ') ') ' = D.  [para (16 (a 1) 259 (a 1 1 1 1))]

given #235 (wt=19): 10158 ((x v C) ' v (C v (D v (D v (D v x))) ') ') ' = C.  [para (9 (a 1) 2284 (a 1 1 1 1))]

given #236 (wt=21): 107 (((x v y) ' v ((y ' v x) ' v z)) ' v (z v x) ') ' = z.  [para (20 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #237 (wt=19): 10168 ((C v x) ' v (C v (D v (x v (D v D))) ') ') ' = C.  [para (16 (a 1) 2284 (a 1 1 2 1 2 1 2))]

given #238 (wt=19): 10226 (C ' v (D v ((C v x) ' v (C v x ') ')) ') ' = D.  [para (11 (a 1) 94 (a 1 1 2 1)) demod (9)]

given #239 (wt=19): 10339 ((x v C) ' v (C v (D v (D v (x v D))) ') ') ' = C.  [para (9 (a 1) 2286 (a 1 1 1 1))]

given #240 (wt=19): 10356 ((x v C) ' v (C v ((D v D) ' v x)) ') ' = x v C.  [para (9 (a 1) 3492 (a 1 1 2 1)) demod (8)]

given #241 (wt=21): 108 ((x v ((y v z) ' v (z v y ') ')) ' v (z v x) ') ' = x.  [para (19 (a 1) 20 (a 1 1 2 1 1))]

given #242 (wt=19): 10360 ((x v C) ' v (C v (x v (D v D) ')) ') ' = x v C.  [para (15 (a 1) 3492 (a 1 1 2 1))]

given #243 (wt=19): 10375 ((C v x) ' v (C v ((D v D) ' v x)) ') ' = x v C.  [para (9 (a 1) 3531 (a 1 1 2 1)) demod (8)]

given #244 (wt=19): 10376 ((x v (C v (D v D) ')) ' v (C v x) ') ' = x v C.  [para (9 (a 1) 3531 (a 1 1))]

given #245 (wt=19): 10380 ((C v x) ' v (C v (x v (D v D) ')) ') ' = C v x.  [para (24 (a 1) 3531 (a 1 1 1 1)) demod (15 8 24 9 24)]

given #246 (wt=21): 112 ((x v ((y v z) ' v (z ' v y) ')) ' v (y v x) ') ' = x.  [para (20 (a 1) 20 (a 1 1 2 1 1))]

given #247 (wt=19): 10787 ((x v C) ' v (C v (D v (x v (D v D))) ') ') ' = C.  [para (16 (a 1) 10158 (a 1 1 2 1 2 1 2))]

given #248 (wt=19): 10842 ((C v x) ' v (C v (x v (D v (D v D))) ') ') ' = C.  [para (15 (a 1) 10168 (a 1 1 2 1 2 1))]

given #249 (wt=19): 10853 (C ' v (D v ((x v C) ' v (C v x ') ')) ') ' = D.  [para (9 (a 1) 10226 (a 1 1 2 1 2 1 1))]

given #250 (wt=19): 10956 ((C v ((D v D) ' v x)) ' v (x v C) ') ' = x v C.  [para (9 (a 1) 10356 (a 1 1))]

given #251 (wt=25): 119 ((x v (y v (C v z))) ' v (x v (D v (y v (C v z)) ')) ') ' = x v D.  [para (26 (a 1) 18 (a 1 1 1 1 2))]

given #252 (wt=19): 11044 ((x v C) ' v (C v (x v (D v (D v D))) ') ') ' = C.  [para (15 (a 1) 10787 (a 1 1 2 1 2 1))]

given #253 (wt=20): 133 (x v ((y v x) ' v (y ' v x) ' ') ') ' = (y v x) '.  [para (67 (a 1) 10 (a 1 1 1))]

given #254 (wt=20): 170 (C ' v (C v (C ' v (C v D ') ' ') ' ') ') ' = C.  [para (25 (a 1) 21 (a 1 1 2 1 1)) demod (25)]

given #255 (wt=20): 183 (C ' v (D v (C ' v (D v C ') ' ') ' ') ') ' = D.  [para (74 (a 1) 21 (a 1 1 2 1 1)) demod (74)]

given #256 (wt=21): 120 ((x v (C v y)) ' v (D v (x v (C v y) ')) ') ' = D v x.  [para (26 (a 1) 18 (a 1 1 1 1))]

given #257 (wt=19): 11160 ((C v x) ' v (D v (D v (C v x) ')) ') ' = D v D.  [para (1040 (a 1) 120 (a 1 1 1 1)) demod (27)]

given #258 (wt=19): 11164 ((x v C) ' v (D v (D v (C v x) ')) ') ' = D v D.  [para (9 (a 1) 11160 (a 1 1 1 1))]

given #259 (wt=19): 11165 ((C v x) ' v (D v (D v (x v C) ')) ') ' = D v D.  [para (9 (a 1) 11160 (a 1 1 2 1 2 2 1))]

given #260 (wt=19): 11185 ((x v C) ' v (D v (D v (x v C) ')) ') ' = D v D.  [para (71 (a 1) 11160 (a 1 1 1)) demod (71)]

given #261 (wt=23): 122 ((x v (C v y)) ' v (x v (C v (y v D '))) ') ' = x v (C v y).  [para (26 (a 1) 19 (a 1 1 1 1)) demod (8 8)]

given #262 (wt=20): 383 (C v (C v ((C v x) ' v (D v x) ')) ') ' = (C v x) '.  [para (28 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #263 (wt=20): 413 (C ' v (C v (D v (C v (C ' v D ')) ') ') ') ' = C.  [para (40 (a 1) 28 (a 1 1 1))]

given #264 (wt=20): 414 ((C v C ') ' v (C v (D v (C ' v C ')) ') ') ' = C.  [para (86 (a 1) 28 (a 1 1 2 1 2)) demod (9)]

given #265 (wt=20): 416 ((x v y) ' v (x v (x v (y ' v (x v y) '))) ') ' = x.  [para (23 (a 1) 10 (a 1 1 2)) demod (9)]

given #266 (wt=25): 126 ((x v (C v (y v z))) ' v (x v (C v (y v (D v z)) ')) ') ' = x v C.  [para (30 (a 1) 18 (a 1 1 1 1 2))]

given #267 (wt=20): 418 (C v (C v ((x v D) ' v (C v x) ')) ') ' = (C v x) '.  [para (27 (a 1) 23 (a 1 1 2 1 2 2 1)) demod (27)]

given #268 (wt=20): 490 (C ' v (C v (C ' v (C v (D v D) ') ' ')) ') ' = C.  [para (384 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 384)]

given #269 (wt=20): 492 (C v (C v ((C v x) ' v (x v D) ')) ') ' = (C v x) '.  [para (32 (a 1) 10 (a 1 1 2)) demod (15 9)]

low water: id=8731, wt=32

given #270 (wt=20): 513 (C v (C v ((x v C) ' v (D v x) ')) ') ' = (x v C) '.  [para (382 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #271 (wt=21): 127 ((C v (x v y)) ' v (C v (x v (D v y) ')) ') ' = C v x.  [para (30 (a 1) 18 (a 1 1 1 1))]

given #272 (wt=20): 517 (C v (C v ((D v x) ' v (x v C) ')) ') ' = (x v C) '.  [para (382 (a 1) 19 (a 1 1 2)) demod (8 9)]

given #273 (wt=20): 535 (C v (C v ((x v C) ' v (x v D) ')) ') ' = (x v C) '.  [para (491 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #274 (wt=20): 611 (D v (D v ((C v x) ' v (C v x) ')) ') ' = (C v x) '.  [para (557 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #275 (wt=20): 642 (D v (D v ((x v C) ' v (C v x) ')) ') ' = (x v C) '.  [para (607 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #276 (wt=23): 128 ((C v (x v y)) ' v (x v (D v (y v C '))) ') ' = x v (D v y).  [para (30 (a 1) 19 (a 1 1 1 1)) demod (8 8)]

given #277 (wt=20): 646 (D v (D v ((C v x) ' v (x v C) ')) ') ' = (x v C) '.  [para (607 (a 1) 19 (a 1 1 2)) demod (8 9)]

given #278 (wt=20): 686 (D v (D v ((x v C) ' v (x v C) ')) ') ' = (x v C) '.  [para (639 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #279 (wt=20): 855 (C ' v (C v (C v (C ' v (D v D) ')) ' ') ') ' = C.  [para (473 (a 1) 10 (a 1 1 1))]

given #280 (wt=20): 1071 (D v (D v (C ' v (D v (D v C ')) ' ') ')) ' = C '.  [para (1034 (a 1) 10 (a 1 1 1)) demod (8)]

given #281 (wt=25): 130 ((x v (C v (y v z))) ' v (x v (C v (y v (z v D)) ')) ') ' = x v C.  [para (31 (a 1) 18 (a 1 1 1 1 2))]

given #282 (wt=20): 2435 (C v (C ' v (C v (D v (D v D)) ') ' ') ') ' = C '.  [para (2283 (a 1) 10 (a 1 1 1))]

given #283 (wt=20): 2972 (D v (D v (C ' v (C ' v (C v D ') '))) ') ' = C '.  [para (1070 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #284 (wt=20): 3825 ((x v y) ' v (y v (y v (x ' v (x v y) '))) ') ' = y.  [para (71 (a 1) 10 (a 1 1 2)) demod (9)]

given #285 (wt=20): 4019 ((x v y) ' v (x v (y ' v (x v (x v y) '))) ') ' = x.  [para (93 (a 1) 10 (a 1 1 2)) demod (9)]

given #286 (wt=21): 131 ((C v (x v y)) ' v (C v (x v (y v D) ')) ') ' = C v x.  [para (31 (a 1) 18 (a 1 1 1 1))]

given #287 (wt=20): 4052 ((x v y) ' v (y ' v (x v (x v (x v y) '))) ') ' = x.  [para (93 (a 1) 29 (a 1 1 2)) demod (9)]

given #288 (wt=20): 4145 ((x v y) ' v (y v (x ' v (y v (x v y) '))) ') ' = y.  [para (135 (a 1) 10 (a 1 1 2)) demod (9)]

given #289 (wt=20): 4193 ((x v y) ' v (x ' v (y v (y v (x v y) '))) ') ' = y.  [para (135 (a 1) 29 (a 1 1 2)) demod (9)]

given #290 (wt=20): 4747 (C ' v (C v (C v (C ' v (D v (D v D)) '))) ') ' = C.  [para (2437 (a 1) 10 (a 1 1 2)) demod (9)]

given #291 (wt=23): 132 ((C v (x v y)) ' v (x v (y v (D v C '))) ') ' = x v (y v D).  [para (31 (a 1) 19 (a 1 1 1 1)) demod (8 8)]

given #292 (wt=20): 5699 (C v (C v (C ' v (C ' v (D v C ') '))) ') ' = C '.  [para (5661 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #293 (wt=20): 10204 (C v (C v (C ' v (D v (D v (D v D))) ')) ') ' = C '.  [para (10162 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #294 (wt=20): 11268 ((x v y) ' v (y v (y v (x ' v (y v x) '))) ') ' = y.  [para (9 (a 1) 416 (a 1 1 1 1))]

given #295 (wt=20): 11269 ((x v y) ' v (x v (x v (y ' v (y v x) '))) ') ' = x.  [para (9 (a 1) 416 (a 1 1 2 1 2 2 2 1))]

given #296 (wt=21): 134 ((x v y) ' v (x v ((z v y) ' v (z ' v y) ')) ') ' = x.  [para (67 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #297 (wt=20): 11475 ((x v y) ' v (y v (x ' v (y v (y v x) '))) ') ' = y.  [para (9 (a 1) 4019 (a 1 1 1 1))]

given #298 (wt=20): 11476 ((x v y) ' v (x v (y ' v (x v (y v x) '))) ') ' = x.  [para (9 (a 1) 4019 (a 1 1 2 1 2 2 2 1))]

given #299 (wt=20): 11496 ((x v y) ' v (x ' v (y v (y v (y v x) '))) ') ' = y.  [para (9 (a 1) 4052 (a 1 1 1 1))]

given #300 (wt=20): 11497 ((x v y) ' v (y ' v (x v (x v (y v x) '))) ') ' = x.  [para (9 (a 1) 4052 (a 1 1 2 1 2 2 2 1))]

given #301 (wt=21): 136 ((x v y) ' v ((x v z) ' v ((x v z ') ' v y)) ') ' = y.  [para (10 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #302 (wt=21): 147 (x v ((y ' v x) ' v (y v x) ' ') ') ' = (y ' v x) '.  [para (67 (a 1) 19 (a 1 1 1))]

given #303 (wt=21): 148 (((x v y) ' v ((x ' v y) ' v z)) ' v (z v y) ') ' = z.  [para (67 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #304 (wt=21): 149 ((x v y) ' v ((z v x) ' v ((x v z ') ' v y)) ') ' = y.  [para (19 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

low water: id=9210, wt=31

given #305 (wt=21): 151 ((x v ((y v z) ' v (y ' v z) ')) ' v (z v x) ') ' = x.  [para (67 (a 1) 20 (a 1 1 2 1 1))]

given #306 (wt=27): 144 ((x v (y v z)) ' v (x v (y v ((u v z) ' v (u ' v z) '))) ') ' = x v y.  [para (67 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #307 (wt=21): 153 ((x v y) ' v ((x v z) ' v ((z ' v x) ' v y)) ') ' = y.  [para (20 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #308 (wt=21): 157 ((x v y) ' v ((z v x) ' v ((z ' v x) ' v y)) ') ' = y.  [para (67 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #309 (wt=21): 203 ((x v y) ' v (x v ((y v z ') ' v (z v y) ')) ') ' = x.  [para (68 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #310 (wt=21): 204 ((x v y) ' v ((y v z) ' v ((y v z ') ' v x)) ') ' = x.  [para (10 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #311 (wt=27): 145 ((x v (y v z)) ' v ((x v (y v u)) ' v ((x v (y v u ')) ' v z)) ') ' = z.  [para (18 (a 1) 67 (a 1 1 2 1 1)) demod (8 8 9)]

given #312 (wt=21): 213 (((x v y ') ' v ((y v x) ' v z)) ' v (z v x) ') ' = z.  [para (68 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #313 (wt=21): 214 ((x v y) ' v ((z v y) ' v ((y v z ') ' v x)) ') ' = x.  [para (19 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #314 (wt=21): 216 ((x v ((y v z ') ' v (z v y) ')) ' v (y v x) ') ' = x.  [para (68 (a 1) 20 (a 1 1 2 1 1))]

given #315 (wt=21): 217 ((x v y) ' v ((y v z) ' v ((z ' v y) ' v x)) ') ' = x.  [para (20 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #316 (wt=23): 154 ((x v (C v y)) ' v (D ' v (x v (C v y))) ') ' = x v (C v y).  [para (26 (a 1) 67 (a 1 1 1 1))]

given #317 (wt=21): 220 ((x v y) ' v ((x v z ') ' v ((z v x) ' v y)) ') ' = y.  [para (68 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #318 (wt=21): 221 ((x v y) ' v ((z v y) ' v ((z ' v y) ' v x)) ') ' = x.  [para (67 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #319 (wt=21): 227 ((x v y) ' v ((y v z ') ' v ((z v y) ' v x)) ') ' = x.  [para (68 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #320 (wt=21): 229 ((x v y) ' v (x v ((z ' v y) ' v (y v z) ')) ') ' = x.  [para (90 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #321 (wt=23): 155 ((C v (x v y)) ' v (C ' v (x v (D v y))) ') ' = x v (D v y).  [para (30 (a 1) 67 (a 1 1 1 1))]

given #322 (wt=21): 230 ((x v y) ' v (y v ((x v z) ' v (x v z ') ')) ') ' = y.  [para (10 (a 1) 90 (a 1 1 1 1 1))]

given #323 (wt=21): 240 (((x ' v y) ' v ((y v x) ' v z)) ' v (z v y) ') ' = z.  [para (90 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #324 (wt=21): 241 ((x v y) ' v (y v ((z v x) ' v (x v z ') ')) ') ' = y.  [para (19 (a 1) 90 (a 1 1 1 1 1))]

given #325 (wt=21): 243 ((x v ((y ' v z) ' v (z v y) ')) ' v (z v x) ') ' = x.  [para (90 (a 1) 20 (a 1 1 2 1 1))]

given #326 (wt=23): 156 ((C v (x v y)) ' v (C ' v (x v (y v D))) ') ' = x v (y v D).  [para (31 (a 1) 67 (a 1 1 1 1))]

given #327 (wt=21): 244 ((x v y) ' v (y v ((x v z) ' v (z ' v x) ')) ') ' = y.  [para (20 (a 1) 90 (a 1 1 1 1 1))]

given #328 (wt=21): 245 ((x v y) ' v ((z ' v x) ' v ((x v z) ' v y)) ') ' = y.  [para (90 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #329 (wt=21): 246 ((x v y) ' v (y v ((z v x) ' v (z ' v x) ')) ') ' = y.  [para (67 (a 1) 90 (a 1 1 1 1 1))]

given #330 (wt=21): 251 ((x v y) ' v ((z ' v y) ' v ((y v z) ' v x)) ') ' = x.  [para (90 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #331 (wt=24): 159 ((x v y) ' v (x v ((x v y) ' v (x v y ') ' ') ' ') ') ' = x.  [para (21 (a 1) 10 (a 1 1 1))]

given #332 (wt=21): 252 ((x v y) ' v (y v ((x v z ') ' v (z v x) ')) ') ' = y.  [para (68 (a 1) 90 (a 1 1 1 1 1))]

given #333 (wt=21): 253 ((x v y) ' v (y v ((z ' v x) ' v (x v z) ')) ') ' = y.  [para (90 (a 1) 90 (a 1 1 1 1 1))]

given #334 (wt=21): 261 ((x v (C v y)) ' v (D v (x v (y v C) ')) ') ' = D v x.  [para (115 (a 1) 18 (a 1 1 1 1))]

given #335 (wt=21): 277 ((x v y) ' v ((y v z) ' v (x v (y v z ') ')) ') ' = x.  [para (15 (a 1) 22 (a 1 1 2 1))]

given #336 (wt=28): 160 ((x v (y v z) ') ' v (x v (y v ((y v z) ' v (y v z ') ' ') ')) ') ' = x.  [para (21 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #337 (wt=21): 347 ((x v (y v C)) ' v (D v (x v (y v C) ')) ') ' = D v x.  [para (258 (a 1) 18 (a 1 1 1 1))]

given #338 (wt=21): 399 ((C v (x v y)) ' v (C v (D v (x v (D v y))) ') ') ' = C.  [para (30 (a 1) 28 (a 1 1 1 1))]

given #339 (wt=21): 400 ((C v (x v y)) ' v (C v (D v (x v (y v D))) ') ') ' = C.  [para (31 (a 1) 28 (a 1 1 1 1))]

given #340 (wt=21): 462 (C v (C v (C ' v (C v (C ' v D ')) ' ')) ') ' = C '.  [para (40 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 40)]

given #341 (wt=22): 161 ((x v y) ' v (x v ((x v y) ' v (x v y ') ' ')) ') ' = x.  [para (21 (a 1) 10 (a 1 1 2)) demod (9)]

given #342 (wt=21): 464 (D v (D v (C ' v (D v (C ' v C ')) ' ')) ') ' = C '.  [para (86 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 86)]

given #343 (wt=21): 472 ((x v C) ' v (x v (C ' v (C v (D v D) ') ')) ') ' = x.  [para (384 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #344 (wt=19): 11995 (C ' v (D v (C ' v (C v (D v D) ') ')) ') ' = D.  [para (1040 (a 1) 472 (a 1 1 2 1)) demod (9 11 9 15)]

given #345 (wt=21): 476 ((C ' v ((C v (D v D) ') ' v x)) ' v (x v C) ') ' = x.  [para (384 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #346 (wt=37): 162 (x v ((x v ((y v z) ' v (y v z ') ')) ' v (x v y) ' ') ') ' = (x v ((y v z) ' v (y v z ') ')) '.  [para (10 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #347 (wt=21): 477 ((x v (C ' v (C v (D v D) ') ')) ' v (C v x) ') ' = x.  [para (384 (a 1) 20 (a 1 1 2 1 1))]

given #348 (wt=21): 478 (C v (C v (C v (D v D) ') ') ') ' = (C v (D v D) ') '.  [para (384 (a 1) 20 (a 1 1 2)) demod (9 9)]

given #349 (wt=21): 479 ((C v x) ' v (C ' v ((C v (D v D) ') ' v x)) ') ' = x.  [para (384 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #350 (wt=21): 483 ((x v C) ' v (C ' v ((C v (D v D) ') ' v x)) ') ' = x.  [para (384 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #351 (wt=31): 163 ((x v y) ' v (x ' v (x v (y ' v (x v y) ')) ') ') ' = (x v (y ' v (x v y) ')) '.  [para (10 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #352 (wt=21): 484 ((C v x) ' v (x v (C ' v (C v (D v D) ') ')) ') ' = x.  [para (384 (a 1) 90 (a 1 1 1 1 1))]

given #353 (wt=21): 554 ((x v (y v (z v u))) ' v (z v (x v (y v u)) ') ') ' = z.  [para (8 (a 1) 29 (a 1 1 1 1)) demod (8)]

given #354 (wt=21): 558 ((x v (y v (z v u))) ' v (y v (z v (x v u)) ') ') ' = y.  [para (15 (a 1) 29 (a 1 1 2 1 2 1))]

given #355 (wt=21): 560 ((x v (y v (z v u))) ' v (z v (x v (u v y)) ') ') ' = z.  [para (16 (a 1) 29 (a 1 1 1 1 2))]

given #356 (wt=22): 164 (C v ((C v x) ' v (C v (D v x) ') ' ') ') ' = (C v x) '.  [para (24 (a 1) 21 (a 1 1 2 1 1 1)) demod (24)]

given #357 (wt=21): 561 ((x v (y v (z v u))) ' v (y v (u v (x v z)) ') ') ' = y.  [para (16 (a 1) 29 (a 1 1 2 1 2 1))]

given #358 (wt=21): 562 ((x v (y v (z v u))) ' v (u v (x v (y v z)) ') ') ' = u.  [para (16 (a 2) 29 (a 1 1 1 1 2))]

given #359 (wt=21): 563 ((x v (y v (z v u))) ' v (y v (z v (u v x)) ') ') ' = y.  [para (16 (a 2) 29 (a 1 1 2 1 2 1))]

given #360 (wt=21): 564 ((x v (y v (z v u))) ' v (y v (x v (u v z)) ') ') ' = y.  [para (17 (a 1) 29 (a 1 1 1 1 2))]

given #361 (wt=26): 165 (x v ((y v (x v z)) ' v (x v (y v z) ') ' ') ') ' = (x v (y v z)) '.  [para (15 (a 1) 21 (a 1 1 2 1 1 1))]

given #362 (wt=21): 568 ((x v (y v (z v u))) ' v (u v (x v (z v y)) ') ') ' = u.  [para (33 (a 1) 29 (a 1 1 1 1 2))]

given #363 (wt=21): 569 ((x v (y v (z v u))) ' v (y v (u v (z v x)) ') ') ' = y.  [para (33 (a 1) 29 (a 1 1 2 1 2 1))]

given #364 (wt=21): 572 ((x v y) ' v ((z v y) ' v (x v (y v z ') ')) ') ' = x.  [para (19 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #365 (wt=21): 576 ((x v y) ' v ((y v z) ' v (x v (z ' v y) ')) ') ' = x.  [para (20 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #366 (wt=22): 166 (C v ((C v x) ' v (C v (x v D) ') ' ') ') ' = (C v x) '.  [para (27 (a 1) 21 (a 1 1 2 1 1 1)) demod (27)]

given #367 (wt=21): 581 ((x v y) ' v ((z v y) ' v (x v (z ' v y) ')) ') ' = x.  [para (67 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #368 (wt=21): 587 ((x v y) ' v ((y v z ') ' v (x v (z v y) ')) ') ' = x.  [para (68 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #369 (wt=21): 589 ((x v y) ' v ((z ' v y) ' v (x v (y v z) ')) ') ' = x.  [para (90 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #370 (wt=21): 602 ((x v C) ' v (C ' v (x v (C v (D v D) ') ')) ') ' = x.  [para (384 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #371 (wt=26): 167 (x v ((y v (x v z)) ' v (x v (z v y) ') ' ') ') ' = (x v (z v y)) '.  [para (16 (a 1) 21 (a 1 1 2 1 1 1))]

given #372 (wt=21): 706 ((x v (y v (z v u))) ' v (z v (u v (x v y)) ') ') ' = z.  [para (8 (a 1) 34 (a 1 1 1 1))]

given #373 (wt=21): 709 ((x v (y v (z v u))) ' v (z v (y v (u v x)) ') ') ' = z.  [para (15 (a 1) 34 (a 1 1 1 1 2)) demod (8)]

given #374 (wt=21): 711 ((x v (y v (z v u))) ' v (z v (u v (y v x)) ') ') ' = z.  [para (16 (a 1) 34 (a 1 1 1 1 2)) demod (8)]

given #375 (wt=21): 712 ((x v (y v (z v u))) ' v (u v (y v (z v x)) ') ') ' = u.  [para (16 (a 2) 34 (a 1 1 1 1 2)) demod (8)]

given #376 (wt=26): 168 (x v ((y v (z v x)) ' v (x v (y v z) ') ' ') ') ' = (x v (y v z)) '.  [para (16 (a 2) 21 (a 1 1 2 1 1 1))]

given #377 (wt=21): 715 ((x v (y v (z v u))) ' v (u v (z v (y v x)) ') ') ' = u.  [para (33 (a 1) 34 (a 1 1 1 1 2)) demod (8)]

given #378 (wt=21): 716 ((x v (y v (z v u))) ' v (z v (y v (x v u)) ') ') ' = z.  [para (33 (a 1) 34 (a 1 1 2 1 2 1)) demod (8)]

given #379 (wt=21): 780 (C v (C ' v (C v (C v (C ' v D '))) ' ') ') ' = C '.  [para (353 (a 1) 10 (a 1 1 1))]

given #380 (wt=21): 799 (D v (C ' v (D v (D v (C ' v C '))) ' ') ') ' = C '.  [para (368 (a 1) 10 (a 1 1 1))]

given #381 (wt=26): 169 (x v ((x v (y v z)) ' v (x v (z v y) ') ' ') ') ' = (x v (z v y)) '.  [para (17 (a 1) 21 (a 1 1 2 1 1 1))]

given #382 (wt=21): 819 ((x v (C v y)) ' v (D v (y v (x v C) ')) ') ' = D v y.  [para (24 (a 1) 35 (a 1 1 1 1 2)) demod (8)]

given #383 (wt=21): 821 ((x v (y v (z v u))) ' v (u v (y v (x v z)) ') ') ' = u.  [para (15 (a 1) 35 (a 1 1 2 1 2 1)) demod (8)]

given #384 (wt=21): 822 ((x v (C v y)) ' v (y v (D v (x v C) ')) ') ' = y v D.  [para (27 (a 1) 35 (a 1 1 1 1 2)) demod (8)]

given #385 (wt=21): 824 ((x v (y v (z v u))) ' v (u v (z v (x v y)) ') ') ' = u.  [para (16 (a 1) 35 (a 1 1 2 1 2 1)) demod (8)]

given #386 (wt=33): 171 (x v ((x v (C ' v (C v D ') ')) ' v (x v C) ' ') ') ' = (x v (C ' v (C v D ') ')) '.  [para (25 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #387 (wt=21): 833 ((x v (C v y)) ' v (C v (y v (D v x) ')) ') ' = C v y.  [para (26 (a 1) 35 (a 1 1 1 1)) demod (8)]

given #388 (wt=21): 835 ((C v (x v y)) ' v (D v (y v (C v x) ')) ') ' = D v y.  [para (30 (a 1) 35 (a 1 1 1 1)) demod (8)]

given #389 (wt=21): 837 ((C v (x v y)) ' v (y v (D v (C v x) ')) ') ' = y v D.  [para (31 (a 1) 35 (a 1 1 1 1)) demod (8)]

given #390 (wt=21): 849 ((x v (y v C)) ' v (y v (C v (D v x) ')) ') ' = y v C.  [para (258 (a 1) 35 (a 1 1 1 1)) demod (8)]

given #391 (wt=25): 172 (C ' v (C ' v (C v (C ' v D ')) ') ') ' = (C v (C ' v D ')) '.  [para (25 (a 1) 21 (a 1 1 2 1 2 1)) demod (15 9 15)]

given #392 (wt=21): 874 ((x v (y v (z v u))) ' v (x v (u v (y v z)) ') ') ' = x.  [para (8 (a 1) 37 (a 1 1 1 1 2))]

given #393 (wt=21): 875 ((x v (y v (z v u))) ' v (x v (z v (u v y)) ') ') ' = x.  [para (8 (a 1) 37 (a 1 1 2 1 2 1))]

given #394 (wt=21): 877 ((x v (y v (z v u))) ' v (x v (y v (u v z)) ') ') ' = x.  [para (15 (a 1) 37 (a 1 1 1 1 2)) demod (8)]

given #395 (wt=21): 878 ((x v (y v (z v u))) ' v (x v (u v (z v y)) ') ') ' = x.  [para (17 (a 1) 37 (a 1 1 1 1 2)) demod (8)]

given #396 (wt=34): 173 ((x v (y v (z v u) ')) ' v (x v (y v (z v ((z v u) ' v (z v u ') ' ') '))) ') ' = x v y.  [para (21 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #397 (wt=21): 880 ((x v (y v (z v u))) ' v (x v (z v (y v u)) ') ') ' = x.  [para (33 (a 1) 37 (a 1 1 1 1 2)) demod (8)]

given #398 (wt=21): 989 ((x v (C v y)) ' v (D v (y v (C v x) ')) ') ' = D v y.  [para (24 (a 1) 63 (a 1 1 1 1 2)) demod (8)]

given #399 (wt=21): 991 ((x v (C v y)) ' v (y v (D v (C v x) ')) ') ' = y v D.  [para (27 (a 1) 63 (a 1 1 1 1 2)) demod (8)]

given #400 (wt=21): 1001 ((x v (C v y)) ' v (C v (y v (x v D) ')) ') ' = C v y.  [para (26 (a 1) 63 (a 1 1 1 1)) demod (8)]

given #401 (wt=34): 174 ((x v (y v z)) ' v (x v (y v ((x v (y v z)) ' v (x v (y v z ')) ' ') ' ')) ') ' = x v y.  [para (18 (a 1) 21 (a 1 1 2 1 1)) demod (8 18)]

given #402 (wt=21): 1003 ((C v (x v y)) ' v (D v (y v (x v C) ')) ') ' = D v y.  [para (30 (a 1) 63 (a 1 1 1 1)) demod (8)]

given #403 (wt=21): 1005 ((C v (x v y)) ' v (y v (D v (x v C) ')) ') ' = y v D.  [para (31 (a 1) 63 (a 1 1 1 1)) demod (8)]

given #404 (wt=21): 1018 ((x v (y v C)) ' v (y v (C v (x v D) ')) ') ' = y v C.  [para (258 (a 1) 63 (a 1 1 1 1)) demod (8)]

given #405 (wt=21): 1035 ((C v x) ' v (D v (D v (x v C '))) ') ' = D v (D v x).  [para (24 (a 1) 75 (a 1 1 1 1)) demod (8)]

given #406 (wt=47): 175 (x v ((x v ((y v (z v u)) ' v (y v (z v u ')) ')) ' v (x v (y v z)) ' ') ') ' = (x v ((y v (z v u)) ' v (y v (z v u ')) ')) '.  [para (18 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #407 (wt=19): 12473 (C ' v (D v (D v (D v C '))) ') ' = D v (D v D).  [para (11 (a 1) 1035 (a 1 1 1 1))]

given #408 (wt=21): 1037 ((C v x) ' v (D v (x v (D v C '))) ') ' = D v (x v D).  [para (27 (a 1) 75 (a 1 1 1 1)) demod (8)]

given #409 (wt=21): 1213 ((x v (y v (z v u))) ' v ((x v (y v u)) ' v z) ') ' = z.  [para (8 (a 1) 96 (a 1 1 1 1)) demod (8)]

given #410 (wt=21): 1216 ((x v y) ' v ((x v z) ' v (y v (x v z ') ')) ') ' = y.  [para (10 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #411 (wt=43): 176 ((x v (y v z)) ' v ((x v y) ' v (x v (y v (z ' v (x v (y v z)) '))) ') ') ' = (x v (y v (z ' v (x v (y v z)) '))) '.  [para (18 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 8 9 9 8 8)]

given #412 (wt=21): 1217 ((x v (y v (z v u))) ' v ((z v (x v u)) ' v y) ') ' = y.  [para (15 (a 1) 96 (a 1 1 2 1 1 1))]

given #413 (wt=21): 1219 ((x v (y v (z v u))) ' v ((x v (u v y)) ' v z) ') ' = z.  [para (16 (a 1) 96 (a 1 1 1 1 2))]

given #414 (wt=21): 1220 ((x v (y v (z v u))) ' v ((u v (x v z)) ' v y) ') ' = y.  [para (16 (a 1) 96 (a 1 1 2 1 1 1))]

given #415 (wt=21): 1222 ((x v (y v (z v u))) ' v ((x v (y v z)) ' v u) ') ' = u.  [para (16 (a 2) 96 (a 1 1 1 1 2))]

given #416 (wt=26): 177 (x v ((y v (z v x)) ' v (x v (z v y) ') ' ') ') ' = (x v (z v y)) '.  [para (33 (a 1) 21 (a 1 1 2 1 1 1))]

given #417 (wt=21): 1223 ((x v (y v (z v u))) ' v ((z v (u v x)) ' v y) ') ' = y.  [para (16 (a 2) 96 (a 1 1 2 1 1 1))]

given #418 (wt=21): 1224 ((x v (y v (z v u))) ' v ((x v (u v z)) ' v y) ') ' = y.  [para (17 (a 1) 96 (a 1 1 1 1 2))]

given #419 (wt=21): 1229 ((x v (y v (z v u))) ' v ((x v (z v y)) ' v u) ') ' = u.  [para (33 (a 1) 96 (a 1 1 1 1 2))]

given #420 (wt=21): 1230 ((x v (y v (z v u))) ' v ((u v (z v x)) ' v y) ') ' = y.  [para (33 (a 1) 96 (a 1 1 2 1 1 1))]

given #421 (wt=35): 178 ((x v y) ' v (x ' v ((x v y) ' v (x v y ') ' ') ') ') ' = ((x v y) ' v (x v y ') ' ') '.  [para (21 (a 1) 19 (a 1 1 1)) demod (9)]

given #422 (wt=21): 1233 ((x v y) ' v ((z v x) ' v (y v (x v z ') ')) ') ' = y.  [para (19 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #423 (wt=21): 1237 ((x v y) ' v ((x v z) ' v (y v (z ' v x) ')) ') ' = y.  [para (20 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #424 (wt=21): 1239 ((x v y) ' v ((z v x) ' v (y v (z ' v x) ')) ') ' = y.  [para (67 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #425 (wt=21): 1246 ((x v y) ' v ((x v z ') ' v (y v (z v x) ')) ') ' = y.  [para (68 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #426 (wt=28): 179 ((x v (((x v y) ' v (x v y ') ' ') ' v z)) ' v (z v (x v y) ') ') ' = z.  [para (21 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #427 (wt=21): 1248 ((x v y) ' v ((z ' v x) ' v (y v (x v z) ')) ') ' = y.  [para (90 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #428 (wt=21): 1261 ((C v x) ' v (C ' v (x v (C v (D v D) ') ')) ') ' = x.  [para (384 (a 1) 96 (a 1 1 2 1 1)) demod (9)]

given #429 (wt=21): 1293 ((x v (y v (z v u))) ' v ((u v (x v y)) ' v z) ') ' = z.  [para (8 (a 1) 97 (a 1 1 1 1))]

given #430 (wt=21): 1296 ((x v (y v (z v u))) ' v ((y v (u v x)) ' v z) ') ' = z.  [para (15 (a 1) 97 (a 1 1 1 1 2)) demod (8)]

given #431 (wt=24): 180 ((x v y) ' v (y v ((x v y) ' v (y v x ') ' ') ' ') ') ' = y.  [para (19 (a 1) 21 (a 1 1 2 1 1)) demod (19)]

given #432 (wt=21): 1298 ((x v (y v (z v u))) ' v ((u v (y v x)) ' v z) ') ' = z.  [para (16 (a 1) 97 (a 1 1 1 1 2)) demod (8)]

given #433 (wt=21): 1300 ((x v (y v (z v u))) ' v ((y v (z v x)) ' v u) ') ' = u.  [para (16 (a 2) 97 (a 1 1 1 1 2)) demod (8)]

low water: id=10337, wt=30

given #434 (wt=21): 1304 ((x v (y v (z v u))) ' v ((z v (y v x)) ' v u) ') ' = u.  [para (33 (a 1) 97 (a 1 1 1 1 2)) demod (8)]

given #435 (wt=21): 1305 ((x v (y v (z v u))) ' v ((y v (x v u)) ' v z) ') ' = z.  [para (33 (a 1) 97 (a 1 1 2 1 1 1)) demod (8)]

given #436 (wt=37): 181 (x v ((x v ((y v z) ' v (z v y ') ')) ' v (x v z) ' ') ') ' = (x v ((y v z) ' v (z v y ') ')) '.  [para (19 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #437 (wt=21): 1348 ((x v (C v y)) ' v (D v ((x v C) ' v y)) ') ' = D v y.  [para (24 (a 1) 98 (a 1 1 1 1 2)) demod (15)]

given #438 (wt=21): 1350 ((x v (y v (z v u))) ' v ((y v (x v z)) ' v u) ') ' = u.  [para (15 (a 1) 98 (a 1 1 2 1 1 1)) demod (8)]

given #439 (wt=21): 1353 ((x v (y v (z v u))) ' v ((z v (x v y)) ' v u) ') ' = u.  [para (16 (a 1) 98 (a 1 1 2 1 1 1)) demod (8)]

given #440 (wt=21): 1363 ((x v (C v y)) ' v (C v ((D v x) ' v y)) ') ' = C v y.  [para (26 (a 1) 98 (a 1 1 1 1)) demod (15)]

given #441 (wt=31): 182 ((x v y) ' v (y ' v (y v (x ' v (x v y) ')) ') ') ' = (y v (x ' v (x v y) ')) '.  [para (19 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #442 (wt=21): 1365 ((C v (x v y)) ' v (D v ((C v x) ' v y)) ') ' = D v y.  [para (30 (a 1) 98 (a 1 1 1 1)) demod (15)]

given #443 (wt=21): 1378 ((x v (y v C)) ' v (C v ((D v x) ' v y)) ') ' = y v C.  [para (258 (a 1) 98 (a 1 1 1 1)) demod (16)]

given #444 (wt=21): 1467 ((x v (y v (z v u))) ' v ((u v (y v z)) ' v x) ') ' = x.  [para (8 (a 1) 99 (a 1 1 1 1 2))]

given #445 (wt=21): 1469 ((x v (y v (z v u))) ' v ((z v (u v y)) ' v x) ') ' = x.  [para (8 (a 1) 99 (a 1 1 2 1 1 1))]

given #446 (wt=33): 184 (x v ((x v (C ' v (D v C ') ')) ' v (x v D) ' ') ') ' = (x v (C ' v (D v C ') ')) '.  [para (74 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #447 (wt=21): 1472 ((x v (y v (z v u))) ' v ((y v (u v z)) ' v x) ') ' = x.  [para (15 (a 1) 99 (a 1 1 1 1 2)) demod (8)]

given #448 (wt=21): 1475 ((x v (y v (z v u))) ' v ((u v (z v y)) ' v x) ') ' = x.  [para (17 (a 1) 99 (a 1 1 1 1 2)) demod (8)]

given #449 (wt=21): 1478 ((x v (y v (z v u))) ' v ((z v (y v u)) ' v x) ') ' = x.  [para (33 (a 1) 99 (a 1 1 1 1 2)) demod (8)]

given #450 (wt=21): 1512 ((C v D ') ' v (C v (C v (C v D ') ') ' ') ') ' = C.  [para (101 (a 1) 10 (a 1 1 1))]

given #451 (wt=25): 185 (C ' v (D ' v (D v (C ' v C ')) ') ') ' = (D v (C ' v C ')) '.  [para (74 (a 1) 21 (a 1 1 2 1 2 1)) demod (15 9 15)]

given #452 (wt=21): 1540 ((x v (C v y)) ' v (D v ((C v x) ' v y)) ') ' = D v y.  [para (24 (a 1) 105 (a 1 1 1 1 2)) demod (15)]

given #453 (wt=21): 1552 ((x v (C v y)) ' v (C v ((x v D) ' v y)) ') ' = C v y.  [para (26 (a 1) 105 (a 1 1 1 1)) demod (15)]

given #454 (wt=21): 1554 ((C v (x v y)) ' v (D v ((x v C) ' v y)) ') ' = D v y.  [para (30 (a 1) 105 (a 1 1 1 1)) demod (15)]

given #455 (wt=21): 1566 ((x v (y v C)) ' v (C v ((x v D) ' v y)) ') ' = y v C.  [para (258 (a 1) 105 (a 1 1 1 1)) demod (16)]

given #456 (wt=28): 186 ((x v (y v ((y v z) ' v (y v z ') ' ') ')) ' v ((y v z) ' v x) ') ' = x.  [para (21 (a 1) 20 (a 1 1 2 1 1))]

given #457 (wt=21): 1583 ((D v C ') ' v (D v (C v (D v C ') ') ' ') ') ' = D.  [para (111 (a 1) 10 (a 1 1 1))]

given #458 (wt=21): 1698 D v (x v (y v (z v (C v u)))) = C v (x v (y v (z v u))).  [para (8 (a 1) 114 (a 1 2 2)) demod (8)]

given #459 (wt=21): 1700 D v (x v (y v (z v (u v C)))) = C v (x v (y v (z v u))).  [para (16 (a 2) 114 (a 1 2 2 2))]

given #460 (wt=21): 1704 C v (x v (y v (z v (D v u)))) = C v (x v (y v (z v u))).  [para (30 (a 1) 114 (a 1 2 2 2)) demod (114) flip a]

given #461 (wt=39): 187 ((x ' v y) ' v (x v ((x ' v y) ' v (x ' v y ') ' ') ') ') ' = ((x ' v y) ' v (x ' v y ') ' ') '.  [para (21 (a 1) 20 (a 1 1 2)) demod (9 9)]

given #462 (wt=21): 1705 C v (x v (y v (z v (u v D)))) = C v (x v (y v (z v u))).  [para (31 (a 1) 114 (a 1 2 2 2)) demod (114) flip a]

given #463 (wt=21): 1797 ((C v x) ' v (D v (D v (C ' v x))) ') ' = D v (D v x).  [para (24 (a 1) 137 (a 1 1 1 1)) demod (15)]

given #464 (wt=21): 1852 ((x v (C v y)) ' v (D v ((C v y) ' v x)) ') ' = D v x.  [para (26 (a 1) 44 (a 1 1 1 1))]

given #465 (wt=21): 1854 ((C v (x v y)) ' v (C v ((D v y) ' v x)) ') ' = C v x.  [para (30 (a 1) 44 (a 1 1 1 1))]

given #466 (wt=24): 188 ((x v y) ' v (x v ((x v y) ' v (y ' v x) ' ') ' ') ') ' = x.  [para (20 (a 1) 21 (a 1 1 2 1 1)) demod (20)]

given #467 (wt=21): 1855 ((C v (x v y)) ' v (C v ((y v D) ' v x)) ') ' = C v x.  [para (31 (a 1) 44 (a 1 1 1 1))]

given #468 (wt=21): 1871 ((x v (y v C)) ' v (D v ((y v C) ' v x)) ') ' = D v x.  [para (258 (a 1) 44 (a 1 1 1 1))]

given #469 (wt=21): 1931 ((x v (y v (z v u)) ') ' v (y v (z v (u v x))) ') ' = x.  [para (8 (a 1) 202 (a 1 1 1 1 2 1)) demod (8)]

given #470 (wt=21): 1933 ((D v (x v (y v C) ')) ' v (y v (C v x)) ') ' = D v x.  [para (24 (a 1) 202 (a 1 1 2 1 2)) demod (8)]

given #471 (wt=37): 189 (x v ((x v ((y v z) ' v (z ' v y) ')) ' v (x v y) ' ') ') ' = (x v ((y v z) ' v (z ' v y) ')) '.  [para (20 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #472 (wt=21): 1934 ((x v (y v (z v u)) ') ' v (z v (y v (u v x))) ') ' = x.  [para (15 (a 1) 202 (a 1 1 1 1 2 1)) demod (8)]

given #473 (wt=21): 1936 ((x v (D v (y v C) ')) ' v (y v (C v x)) ') ' = x v D.  [para (27 (a 1) 202 (a 1 1 2 1 2)) demod (8)]

given #474 (wt=21): 1937 ((x v (y v (z v u)) ') ' v (z v (u v (y v x))) ') ' = x.  [para (16 (a 1) 202 (a 1 1 1 1 2 1)) demod (8)]

given #475 (wt=21): 1939 ((x v (y v (z v u)) ') ' v (u v (y v (z v x))) ') ' = x.  [para (16 (a 2) 202 (a 1 1 1 1 2 1)) demod (8)]

given #476 (wt=31): 190 ((x v y) ' v (x ' v (y ' v (x v (x v y) ')) ') ') ' = (y ' v (x v (x v y) ')) '.  [para (20 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #477 (wt=21): 1941 ((x v (y v (z v u)) ') ' v (y v (u v (z v x))) ') ' = x.  [para (17 (a 1) 202 (a 1 1 1 1 2 1)) demod (8)]

given #478 (wt=21): 1944 ((x v (y v (z v u)) ') ' v (u v (z v (y v x))) ') ' = x.  [para (33 (a 1) 202 (a 1 1 1 1 2 1)) demod (8)]

given #479 (wt=21): 1947 ((C v (x v (D v y) ')) ' v (y v (C v x)) ') ' = C v x.  [para (26 (a 1) 202 (a 1 1 2 1)) demod (8)]

given #480 (wt=21): 1949 ((D v (x v (C v y) ')) ' v (C v (y v x)) ') ' = D v x.  [para (30 (a 1) 202 (a 1 1 2 1)) demod (8)]

given #481 (wt=28): 191 (D v ((x v (C v y)) ' v (D v (x v (C v y)) ') ' ') ') ' = (x v (C v y)) '.  [para (26 (a 1) 21 (a 1 1 2 1 1 1)) demod (26)]

given #482 (wt=21): 1951 ((x v (D v (C v y) ')) ' v (C v (y v x)) ') ' = x v D.  [para (31 (a 1) 202 (a 1 1 2 1)) demod (8)]

given #483 (wt=21): 1962 ((x v (C v (D v y) ')) ' v (y v (x v C)) ') ' = x v C.  [para (258 (a 1) 202 (a 1 1 2 1)) demod (8)]

given #484 (wt=21): 1997 ((D v (x v (C v y) ')) ' v (y v (C v x)) ') ' = D v x.  [para (24 (a 1) 226 (a 1 1 2 1 2)) demod (8)]

given #485 (wt=21): 1999 ((x v (D v (C v y) ')) ' v (y v (C v x)) ') ' = x v D.  [para (27 (a 1) 226 (a 1 1 2 1 2)) demod (8)]

given #486 (wt=28): 192 (C v ((C v (x v y)) ' v (C v (x v (D v y)) ') ' ') ') ' = (C v (x v y)) '.  [para (30 (a 1) 21 (a 1 1 2 1 1 1)) demod (30)]

given #487 (wt=21): 2006 ((C v (x v (y v D) ')) ' v (y v (C v x)) ') ' = C v x.  [para (26 (a 1) 226 (a 1 1 2 1)) demod (8)]

given #488 (wt=21): 2008 ((D v (x v (y v C) ')) ' v (C v (y v x)) ') ' = D v x.  [para (30 (a 1) 226 (a 1 1 2 1)) demod (8)]

given #489 (wt=21): 2010 ((x v (D v (y v C) ')) ' v (C v (y v x)) ') ' = x v D.  [para (31 (a 1) 226 (a 1 1 2 1)) demod (8)]

given #490 (wt=21): 2021 ((x v (C v (y v D) ')) ' v (y v (x v C)) ') ' = x v C.  [para (258 (a 1) 226 (a 1 1 2 1)) demod (8)]

given #491 (wt=28): 193 (C v ((C v (x v y)) ' v (C v (x v (y v D)) ') ' ') ') ' = (C v (x v y)) '.  [para (31 (a 1) 21 (a 1 1 2 1 1 1)) demod (31)]

given #492 (wt=21): 2042 (((x v (y v z)) ' v u) ' v (x v (y v (u v z))) ') ' = u.  [para (8 (a 1) 232 (a 1 1 1 1 1 1)) demod (8)]

given #493 (wt=21): 2044 (((x v (y v z)) ' v u) ' v (y v (u v (x v z))) ') ' = u.  [para (15 (a 1) 232 (a 1 1 1 1 1 1))]

given #494 (wt=21): 2046 (((x v (y v z)) ' v u) ' v (y v (u v (z v x))) ') ' = u.  [para (16 (a 1) 232 (a 1 1 1 1 1 1))]

given #495 (wt=21): 2048 (((x v (y v z)) ' v u) ' v (x v (z v (u v y))) ') ' = u.  [para (16 (a 1) 232 (a 1 1 2 1 2))]

given #496 (wt=28): 194 (((x v y) ' v z) ' v (x v (((x v y) ' v (x v y ') ' ') ' v z)) ') ' = z.  [para (21 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #497 (wt=21): 2049 (((x v (y v z)) ' v u) ' v (z v (u v (x v y))) ') ' = u.  [para (16 (a 2) 232 (a 1 1 1 1 1 1))]

given #498 (wt=21): 2050 (((x v (y v z)) ' v u) ' v (x v (u v (z v y))) ') ' = u.  [para (17 (a 1) 232 (a 1 1 1 1 1 1))]

given #499 (wt=21): 2053 (((x v (y v z)) ' v u) ' v (z v (u v (y v x))) ') ' = u.  [para (33 (a 1) 232 (a 1 1 1 1 1 1))]

% Back_subsumption disabled, ratio of kept to back_subsumed is 226 (0.00 of 40.94 sec).

given #500 (wt=21): 2080 ((x v (C v y)) ' v (C v ((D v y) ' v x)) ') ' = x v C.  [para (24 (a 1) 45 (a 1 1 1 1 2))]

given #501 (wt=24): 195 ((x v y) ' v (y v ((x v y) ' v (x ' v y) ' ') ' ') ') ' = y.  [para (67 (a 1) 21 (a 1 1 2 1 1)) demod (67)]

given #502 (wt=21): 2083 ((x v (C v y)) ' v (C v ((y v D) ' v x)) ') ' = x v C.  [para (27 (a 1) 45 (a 1 1 1 1 2))]

given #503 (wt=21): 2100 ((x v (C v y)) ' v (x v (D v (C v y) ')) ') ' = D v x.  [para (26 (a 1) 45 (a 1 1 1 1)) demod (9)]

given #504 (wt=21): 2102 ((C v (x v y)) ' v (x v (C v (D v y) ')) ') ' = C v x.  [para (30 (a 1) 45 (a 1 1 1 1)) demod (9)]

given #505 (wt=21): 2104 ((C v (x v y)) ' v (x v (C v (y v D) ')) ') ' = C v x.  [para (31 (a 1) 45 (a 1 1 1 1)) demod (9)]

given #506 (wt=37): 196 (x v ((x v ((y v z) ' v (y ' v z) ')) ' v (x v z) ' ') ') ' = (x v ((y v z) ' v (y ' v z) ')) '.  [para (67 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #507 (wt=21): 2121 ((x v (y v C)) ' v (x v (D v (y v C) ')) ') ' = D v x.  [para (258 (a 1) 45 (a 1 1 1 1)) demod (9)]

given #508 (wt=21): 2191 (((x v (y v z)) ' v u) ' v (y v (z v (u v x))) ') ' = u.  [para (8 (a 1) 234 (a 1 1 2 1))]

given #509 (wt=21): 2193 (((x v (y v z)) ' v u) ' v (z v (x v (u v y))) ') ' = u.  [para (15 (a 1) 234 (a 1 1 2 1 2)) demod (8)]

given #510 (wt=21): 2195 (((x v (y v z)) ' v u) ' v (z v (y v (u v x))) ') ' = u.  [para (16 (a 1) 234 (a 1 1 2 1 2)) demod (8)]

given #511 (wt=31): 197 ((x v y) ' v (y ' v (x ' v (y v (x v y) ')) ') ') ' = (x ' v (y v (x v y) ')) '.  [para (67 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #512 (wt=21): 2198 (((x v (y v z)) ' v u) ' v (y v (x v (u v z))) ') ' = u.  [para (33 (a 1) 234 (a 1 1 1 1 1 1)) demod (8)]

given #513 (wt=21): 2214 (((x v (y v z)) ' v u) ' v (u v (z v (x v y))) ') ' = u.  [para (8 (a 1) 236 (a 1 1 1 1 1 1))]

given #514 (wt=21): 2215 (((x v (y v z)) ' v u) ' v (u v (y v (z v x))) ') ' = u.  [para (8 (a 1) 236 (a 1 1 2 1 2))]

given #515 (wt=21): 2217 (((x v (y v z)) ' v u) ' v (u v (x v (z v y))) ') ' = u.  [para (15 (a 1) 236 (a 1 1 1 1 1 1)) demod (8)]

given #516 (wt=31): 198 (x v ((x v y) ' v (x v ((x v y) ' v (x v y ') ' ') ' ') ' ') ') ' = (x v y) '.  [para (21 (a 1) 21 (a 1 1 2 1 1)) demod (21)]

given #517 (wt=21): 2220 (((x v (y v z)) ' v u) ' v (u v (z v (y v x))) ') ' = u.  [para (17 (a 1) 236 (a 1 1 1 1 1 1)) demod (8)]

given #518 (wt=21): 2223 (((x v (y v z)) ' v u) ' v (u v (y v (x v z))) ') ' = u.  [para (33 (a 1) 236 (a 1 1 1 1 1 1)) demod (8)]

given #519 (wt=21): 2285 ((x v (C v y)) ' v (C v (D v (D v (x v y))) ') ') ' = C.  [para (15 (a 1) 385 (a 1 1 1 1))]

given #520 (wt=21): 2287 ((x v (C v y)) ' v (C v (D v (D v (y v x))) ') ') ' = C.  [para (16 (a 1) 385 (a 1 1 1 1))]

given #521 (wt=48): 199 (x v ((x v (y v ((y v z) ' v (y v z ') ' ') ')) ' v (x v (y v z) ') ' ') ') ' = (x v (y v ((y v z) ' v (y v z ') ' ') ')) '.  [para (21 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #522 (wt=21): 2288 ((C v (x v y)) ' v (C v (D v (y v (D v x))) ') ') ' = C.  [para (16 (a 1) 385 (a 1 1 2 1 2 1 2))]

given #523 (wt=21): 2290 ((x v (y v C)) ' v (C v (D v (D v (x v y))) ') ') ' = C.  [para (16 (a 2) 385 (a 1 1 1 1))]

given #524 (wt=21): 2291 ((C v (x v y)) ' v (C v (D v (D v (y v x))) ') ') ' = C.  [para (17 (a 1) 385 (a 1 1 1 1))]

given #525 (wt=21): 2293 ((x v (y v C)) ' v (C v (D v (D v (y v x))) ') ') ' = C.  [para (33 (a 1) 385 (a 1 1 1 1))]

given #526 (wt=39): 200 (x v ((x v y) ' ' v (x v ((x v y) ' v (x v y ') ' ')) ') ') ' = (x v ((x v y) ' v (x v y ') ' ')) '.  [para (21 (a 1) 21 (a 1 1 2 1 2 1)) demod (9)]

given #527 (wt=21): 2294 ((C v (x v y)) ' v (C v (D v (y v (x v D))) ') ') ' = C.  [para (33 (a 1) 385 (a 1 1 2 1 2 1 2))]

given #528 (wt=21): 2493 ((x v (y v (z v u)) ') ' v (y v (z v (x v u))) ') ' = x.  [para (8 (a 1) 555 (a 1 1 1 1 2 1)) demod (8)]

given #529 (wt=21): 2494 ((x v (y v (z v u)) ') ' v (z v (x v (y v u))) ') ' = x.  [para (15 (a 1) 555 (a 1 1 1 1 2 1))]

given #530 (wt=21): 2495 ((x v (y v (z v u)) ') ' v (z v (x v (u v y))) ') ' = x.  [para (16 (a 1) 555 (a 1 1 1 1 2 1))]

given #531 (wt=27): 210 ((x v (y v z)) ' v (x v (y v ((z v u ') ' v (u v z) '))) ') ' = x v y.  [para (68 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #532 (wt=21): 2496 ((x v (y v (z v u)) ') ' v (y v (u v (x v z))) ') ' = x.  [para (16 (a 1) 555 (a 1 1 2 1 2))]

given #533 (wt=21): 2497 ((x v (y v (z v u)) ') ' v (u v (x v (y v z))) ') ' = x.  [para (16 (a 2) 555 (a 1 1 1 1 2 1))]

low water: id=10940, wt=29

given #534 (wt=21): 2498 ((x v (y v (z v u)) ') ' v (y v (x v (u v z))) ') ' = x.  [para (17 (a 1) 555 (a 1 1 1 1 2 1))]

given #535 (wt=21): 2500 ((x v (y v (z v u)) ') ' v (u v (x v (z v y))) ') ' = x.  [para (33 (a 1) 555 (a 1 1 1 1 2 1))]

given #536 (wt=27): 211 ((x v (y v z)) ' v ((y v (z v u)) ' v ((y v (z v u ')) ' v x)) ') ' = x.  [para (18 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #537 (wt=21): 2516 ((x v (y v (z v u)) ') ' v (z v (u v (x v y))) ') ' = x.  [para (8 (a 1) 707 (a 1 1 2 1))]

given #538 (wt=21): 2517 ((x v (y v (z v u)) ') ' v (u v (y v (x v z))) ') ' = x.  [para (15 (a 1) 707 (a 1 1 2 1 2)) demod (8)]

given #539 (wt=21): 2518 ((x v (y v (z v u)) ') ' v (u v (z v (x v y))) ') ' = x.  [para (16 (a 1) 707 (a 1 1 2 1 2)) demod (8)]

given #540 (wt=21): 2520 ((x v (y v (z v u)) ') ' v (z v (y v (x v u))) ') ' = x.  [para (33 (a 1) 707 (a 1 1 1 1 2 1)) demod (8)]

given #541 (wt=23): 218 ((x v (D v (y v C '))) ' v (C v (x v y)) ') ' = x v (D v y).  [para (30 (a 1) 68 (a 1 1 2 1)) demod (8 8)]

given #542 (wt=21): 3418 ((C v (x v y)) ' v (C v (x v (y v (D v D))) ') ') ' = C.  [para (8 (a 1) 2289 (a 1 1 2 1 2 1))]

given #543 (wt=21): 3489 ((x v (y v C)) ' v (x v (C v (D v y) ')) ') ' = x v C.  [para (9 (a 1) 51 (a 1 1 1 1 2))]

given #544 (wt=21): 3490 ((C v (x v y)) ' v (y v (C v (D v x) ')) ') ' = y v C.  [para (9 (a 1) 51 (a 1 1 1 1)) demod (8)]

given #545 (wt=21): 3495 ((x v (C v y)) ' v (C v (x v (D v y) ')) ') ' = x v C.  [para (15 (a 1) 51 (a 1 1 2 1))]

given #546 (wt=23): 219 ((x v (y v (D v C '))) ' v (C v (x v y)) ') ' = x v (y v D).  [para (31 (a 1) 68 (a 1 1 2 1)) demod (8 8)]

given #547 (wt=21): 3503 ((x v (C v y)) ' v (y v (C v (D v x) ')) ') ' = y v C.  [para (33 (a 1) 51 (a 1 1 1 1))]

given #548 (wt=21): 3667 ((x v (y v C)) ' v (x v (C v (y v D) ')) ') ' = x v C.  [para (11 (a 1) 52 (a 1 1 1 1 2 2))]

given #549 (wt=21): 3696 ((C v (x v y)) ' v (C v (y v (x v D) ')) ') ' = C v y.  [para (31 (a 1) 52 (a 1 1 1 1))]

given #550 (wt=21): 3713 ((x v (y v C)) ' v (D v (y v (x v C) ')) ') ' = D v y.  [para (258 (a 1) 52 (a 1 1 1 1))]

given #551 (wt=25): 222 ((x v y ') ' v (x v ((x v y ') ' v (y v x) ' ') ' ') ') ' = x.  [para (68 (a 1) 21 (a 1 1 2 1 1)) demod (68)]

given #552 (wt=21): 3829 ((C v D ') ' v (C v (C ' ' v (C v D ') ')) ') ' = C.  [para (25 (a 1) 71 (a 1 1 2 1 2 2)) demod (9 9 8 25)]

given #553 (wt=21): 3835 ((D v C ') ' v (D v (C ' ' v (D v C ') ')) ') ' = D.  [para (74 (a 1) 71 (a 1 1 2 1 2 2)) demod (9 9 8 74)]

given #554 (wt=21): 4333 ((x v (C v y)) ' v (C v (x v (y v D) ')) ') ' = C v x.  [para (27 (a 1) 53 (a 1 1 1 1 2))]

given #555 (wt=21): 4511 (C v (C v (C ' v (C ' v (C v D ') ' '))) ') ' = C '.  [para (423 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #556 (wt=37): 223 (x v ((x v ((y v z ') ' v (z v y) ')) ' v (x v y) ' ') ') ' = (x v ((y v z ') ' v (z v y) ')) '.  [para (68 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #557 (wt=21): 4547 (D v (D v (C ' v (C ' v (D v C ') ' '))) ') ' = C '.  [para (432 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #558 (wt=21): 4623 ((C v (x v y)) ' v (y v (C v (x v D) ')) ') ' = y v C.  [para (9 (a 1) 54 (a 1 1 1 1)) demod (8)]

given #559 (wt=21): 4626 ((x v (C v y)) ' v (y v (C v (x v D) ')) ') ' = y v C.  [para (33 (a 1) 54 (a 1 1 1 1))]

given #560 (wt=21): 4668 (C v (C v (C v (C ' v (C ' v (D v D) ')))) ') ' = C '.  [para (856 (a 1) 10 (a 1 1 2)) demod (15 15 9)]

given #561 (wt=32): 224 ((x v y ') ' v (x ' v (y v (x v (x v y ') ')) ') ') ' = (y v (x v (x v y ') ')) '.  [para (68 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #562 (wt=21): 4942 ((x v (C v y)) ' v (x v (D v (y v C) ')) ') ' = x v D.  [para (24 (a 1) 56 (a 1 1 1 1 2))]

given #563 (wt=21): 4960 ((C v (x v y)) ' v (C v (y v (D v x) ')) ') ' = C v y.  [para (31 (a 1) 56 (a 1 1 1 1))]

given #564 (wt=21): 4973 ((x v (y v C)) ' v (D v (y v (C v x) ')) ') ' = D v y.  [para (258 (a 1) 56 (a 1 1 1 1))]

given #565 (wt=21): 5800 ((x v (y v C)) ' v (D v (x v (C v y) ')) ') ' = D v x.  [para (258 (a 1) 60 (a 1 1 1 1))]

given #566 (wt=28): 225 ((x v (y v z) ') ' v (y v (((y v z) ' v (y v z ') ' ') ' v x)) ') ' = x.  [para (21 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #567 (wt=21): 5893 ((x v y ') ' v (x v (x v (y v (x v y ') '))) ') ' = x.  [para (95 (a 1) 10 (a 1 1 2)) demod (9)]

given #568 (wt=21): 5909 ((x v y ') ' v (x v (y v (x v (x v y ') '))) ') ' = x.  [para (68 (a 1) 95 (a 1 1 2 1 2 2)) demod (9 9 8 8 68)]

given #569 (wt=21): 5912 ((x ' v y) ' v (y v (y v (x v (x ' v y) '))) ') ' = y.  [para (90 (a 1) 95 (a 1 1 2 1 2 2)) demod (9 9 8 8 90)]

given #570 (wt=21): 5952 (C ' v (C v (C v (C v (C ' v (C ' v D '))))) ') ' = C.  [para (353 (a 1) 95 (a 1 1 2 1 2 2)) demod (9 15 15 15 353)]

given #571 (wt=27): 238 ((x v (y v z)) ' v (x v (y v ((u ' v z) ' v (z v u) '))) ') ' = x v y.  [para (90 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #572 (wt=21): 5954 (C ' v (D v (D v (D v (C ' v (C ' v C '))))) ') ' = D.  [para (368 (a 1) 95 (a 1 1 2 1 2 2)) demod (9 15 15 15 368)]

given #573 (wt=21): 6226 ((x v y ') ' v (y v (x v (x v (x v y ') '))) ') ' = x.  [para (109 (a 1) 29 (a 1 1 2)) demod (9)]

given #574 (wt=21): 6485 ((x ' v y) ' v (y v (x v (y v (x ' v y) '))) ') ' = y.  [para (67 (a 1) 113 (a 1 1 2 1 2 2)) demod (9 9 8 8 67)]

given #575 (wt=21): 6736 ((C v (x v y)) ' v (C v (x v (D v (D v y))) ') ') ' = C.  [para (30 (a 1) 124 (a 1 1 1 1))]

given #576 (wt=27): 239 ((x v (y v z)) ' v (z v ((x v (y v u)) ' v (x v (y v u ')) ')) ') ' = z.  [para (18 (a 1) 90 (a 1 1 1 1 1)) demod (8)]

given #577 (wt=21): 6737 ((C v (x v y)) ' v (C v (x v (D v (y v D))) ') ') ' = C.  [para (31 (a 1) 124 (a 1 1 1 1))]

given #578 (wt=21): 7362 ((x v (y v C)) ' v (x v (D v (C v y) ')) ') ' = x v D.  [para (11 (a 1) 64 (a 1 1 1 1 2 2))]

given #579 (wt=21): 7943 ((x ' v y) ' v (x v (y v (y v (x ' v y) '))) ') ' = y.  [para (152 (a 1) 29 (a 1 1 2)) demod (9)]

given #580 (wt=21): 8493 ((x v (C v (D v y) ')) ' v (C v (x v y)) ') ' = x v C.  [para (30 (a 1) 212 (a 1 1 2 1))]

given #581 (wt=25): 247 ((x ' v y) ' v (y v ((x ' v y) ' v (y v x) ' ') ' ') ') ' = y.  [para (90 (a 1) 21 (a 1 1 2 1 1)) demod (90)]

given #582 (wt=21): 8494 ((x v (C v (y v D) ')) ' v (C v (x v y)) ') ' = x v C.  [para (31 (a 1) 212 (a 1 1 2 1))]

given #583 (wt=21): 8741 ((C v ((D v x) ' v y)) ' v (y v (C v x)) ') ' = y v C.  [para (24 (a 1) 228 (a 1 1 2 1 2)) demod (16)]

given #584 (wt=21): 8744 ((C v ((x v D) ' v y)) ' v (y v (C v x)) ') ' = y v C.  [para (27 (a 1) 228 (a 1 1 2 1 2)) demod (16)]

given #585 (wt=21): 8758 ((D v ((C v x) ' v y)) ' v (y v (C v x)) ') ' = D v y.  [para (26 (a 1) 228 (a 1 1 2 1)) demod (15)]

given #586 (wt=37): 248 (x v ((x v ((y ' v z) ' v (z v y) ')) ' v (x v z) ' ') ') ' = (x v ((y ' v z) ' v (z v y) ')) '.  [para (90 (a 1) 21 (a 1 1 2 1 2 1 1 2))]

given #587 (wt=21): 8760 ((C v ((D v x) ' v y)) ' v (C v (y v x)) ') ' = C v y.  [para (30 (a 1) 228 (a 1 1 2 1)) demod (15)]

given #588 (wt=21): 8762 ((C v ((x v D) ' v y)) ' v (C v (y v x)) ') ' = C v y.  [para (31 (a 1) 228 (a 1 1 2 1)) demod (15)]

given #589 (wt=21): 8767 ((D v ((x v C) ' v y)) ' v (y v (x v C)) ') ' = D v y.  [para (258 (a 1) 228 (a 1 1 2 1)) demod (15)]

given #590 (wt=21): 9244 (C ' v (C v ((C v x) ' v (D v (x v C) ') ')) ') ' = C.  [para (36 (a 2) 272 (a 1 1 2 1 2 1 1)) demod (24)]

given #591 (wt=32): 249 ((x ' v y) ' v (y ' v (y v (x v (x ' v y) ')) ') ') ' = (y v (x v (x ' v y) ')) '.  [para (90 (a 1) 21 (a 1 1 2 1 2 1)) demod (9 8 9 9 8)]

given #592 (wt=21): 9344 ((x v (C v y)) ' v (C v (D v (x v (D v y))) ') ') ' = C.  [para (24 (a 1) 386 (a 1 1 1 1 2))]

given #593 (wt=21): 9346 ((x v (C v y)) ' v (C v (D v (x v (y v D))) ') ') ' = C.  [para (27 (a 1) 386 (a 1 1 1 1 2))]

given #594 (wt=21): 9380 ((x v (C v y)) ' v (C v (D v (y v (D v x))) ') ') ' = C.  [para (27 (a 1) 388 (a 1 1 1 1 2)) demod (8)]

given #595 (wt=21): 9426 ((C v (x v y)) ' v (C v (y v (D v (D v x))) ') ') ' = C.  [para (1040 (a 2) 389 (a 1 1 2 1 2 1 2)) demod (8 30)]

given #596 (wt=28): 250 (((x v y) ' v z) ' v (z v (x v ((x v y) ' v (x v y ') ' ') ')) ') ' = z.  [para (21 (a 1) 90 (a 1 1 1 1 1))]

given #597 (wt=21): 9512 ((x v (C v y)) ' v (C v (x v (D v (D v y))) ') ') ' = C.  [para (24 (a 1) 556 (a 1 1 1 1 2))]

given #598 (wt=21): 9514 ((x v (C v y)) ' v (C v (x v (D v (y v D))) ') ') ' = C.  [para (27 (a 1) 556 (a 1 1 1 1 2))]

given #599 (wt=21): 10163 ((C v x) ' v (C v (D v (D v (D v (D v x)))) ') ') ' = C.  [para (24 (a 1) 2284 (a 1 1 1 1))]

given #600 (wt=19): 13455 (C ' v (C v (D v (D v (D v (D v D)))) ') ') ' = C.  [para (11 (a 1) 10163 (a 1 1 1 1))]

given #601 (wt=25): 260 ((x v (y v (C v z))) ' v (x v (D v (y v (z v C)) ')) ') ' = x v D.  [para (115 (a 1) 18 (a 1 1 1 1 2))]

given #602 (wt=21): 10165 ((C v x) ' v (C v (D v (D v (D v (x v D)))) ') ') ' = C.  [para (27 (a 1) 2284 (a 1 1 1 1))]

given #603 (wt=21): 10858 (C ' v (D v ((C v x) ' v (C v (D v x) ') ')) ') ' = D.  [para (24 (a 1) 10226 (a 1 1 2 1 2 1 1))]

given #604 (wt=21): 10860 (C ' v (D v ((C v x) ' v (C v (x v D) ') ')) ') ' = D.  [para (27 (a 1) 10226 (a 1 1 2 1 2 1 1))]

given #605 (wt=21): 11147 ((C v (x v y)) ' v (D v (x v (C v y) ')) ') ' = D v x.  [para (15 (a 1) 120 (a 1 1 1 1))]

given #606 (wt=23): 262 ((x v (C v y)) ' v (x v (y v (C v D '))) ') ' = x v (y v C).  [para (115 (a 1) 19 (a 1 1 1 1)) demod (8 8)]

given #607 (wt=21): 11242 (C ' v (C v ((C v x) ' v (D v (C v x) ') ')) ') ' = C.  [para (383 (a 1) 272 (a 1 1 2 1 2 2 1 2)) demod (15 24 383)]

given #608 (wt=21): 11348 (C ' v (C v ((x v C) ' v (D v (x v C) ') ')) ') ' = C.  [para (513 (a 1) 272 (a 1 1 2 1 2 2 1 2)) demod (15 24 513)]

given #609 (wt=21): 11353 ((x v (y v C)) ' v (C v (x v (D v y) ')) ') ' = C v x.  [para (16 (a 2) 127 (a 1 1 1 1))]

given #610 (wt=21): 11355 ((x v (y v C)) ' v (C v (y v (D v x) ')) ') ' = C v y.  [para (33 (a 1) 127 (a 1 1 1 1))]

given #611 (wt=23): 263 ((x v (C v y)) ' v (D ' v (x v (y v C))) ') ' = x v (y v C).  [para (115 (a 1) 67 (a 1 1 1 1))]

given #612 (wt=21): 11402 ((C v x) ' v (x v (D v (D v C '))) ') ' = x v (D v D).  [para (27 (a 1) 128 (a 1 1 1 1))]

given #613 (wt=21): 11494 ((x v (y v C)) ' v (C v (x v (y v D) ')) ') ' = C v x.  [para (16 (a 2) 131 (a 1 1 1 1))]

given #614 (wt=21): 11495 ((x v (y v C)) ' v (C v (y v (x v D) ')) ') ' = C v y.  [para (33 (a 1) 131 (a 1 1 1 1))]

given #615 (wt=21): 11958 ((x v (C v y)) ' v (D v ((y v C) ' v x)) ') ' = D v x.  [para (9 (a 1) 261 (a 1 1 2 1 2))]

given #616 (wt=28): 264 (D v ((x v (C v y)) ' v (D v (x v (y v C)) ') ' ') ') ' = (x v (y v C)) '.  [para (115 (a 1) 21 (a 1 1 2 1 1 1)) demod (258)]

given #617 (wt=21): 11959 ((C v (x v y)) ' v (D v (x v (y v C) ')) ') ' = D v x.  [para (15 (a 1) 261 (a 1 1 1 1))]

given #618 (wt=21): 11975 ((x v (y v C)) ' v (C v (D v (x v (D v y))) ') ') ' = C.  [para (16 (a 2) 399 (a 1 1 1 1))]

given #619 (wt=21): 11978 ((x v (y v C)) ' v (C v (D v (y v (D v x))) ') ') ' = C.  [para (33 (a 1) 399 (a 1 1 1 1))]

given #620 (wt=21): 11984 ((x v (C v y)) ' v (C v (D v (y v (x v D))) ') ') ' = C.  [para (16 (a 1) 400 (a 1 1 1 1))]

given #621 (wt=28): 265 (D v ((x v (y v C)) ' v (D v (x v (y v C)) ') ' ') ') ' = (x v (C v y)) '.  [para (115 (a 1) 21 (a 2 1)) demod (258)]

given #622 (wt=21): 11985 ((x v (y v C)) ' v (C v (D v (x v (y v D))) ') ') ' = C.  [para (16 (a 2) 400 (a 1 1 1 1))]

given #623 (wt=21): 11986 ((x v (y v C)) ' v (C v (D v (y v (x v D))) ') ') ' = C.  [para (33 (a 1) 400 (a 1 1 1 1))]

given #624 (wt=21): 12379 ((x v (y v C)) ' v (y v (D v (x v C) ')) ') ' = y v D.  [para (9 (a 1) 822 (a 1 1 1 1 2))]

given #625 (wt=21): 12380 ((C v (x v y)) ' v (x v (D v (y v C) ')) ') ' = x v D.  [para (9 (a 1) 822 (a 1 1 1 1)) demod (8)]

given #626 (wt=23): 266 ((x v (y v (C v D '))) ' v (x v (C v y)) ') ' = x v (y v C).  [para (115 (a 1) 68 (a 1 1 2 1)) demod (8 8)]

given #627 (wt=21): 12409 ((C v (x v y)) ' v (x v (D v (C v y) ')) ') ' = x v D.  [para (9 (a 1) 837 (a 1 1 1 1 2))]

given #628 (wt=21): 12410 ((x v (y v C)) ' v (y v (D v (C v x) ')) ') ' = y v D.  [para (16 (a 2) 837 (a 1 1 1 1))]

given #629 (wt=21): 12471 ((x v C) ' v (D v (D v (x v C '))) ') ' = D v (D v x).  [para (9 (a 1) 1035 (a 1 1 1 1))]

given #630 (wt=21): 12492 ((x v C) ' v (D v (x v (D v C '))) ') ' = D v (x v D).  [para (9 (a 1) 1037 (a 1 1 1 1))]

given #631 (wt=28): 267 (x v ((x v y) ' v (x v ((y v z) ' v (y v z ') ')) ' ') ') ' = (x v y) '.  [para (22 (a 1) 10 (a 1 1 1))]

given #632 (wt=21): 12733 ((x v (y v C)) ' v (D v ((x v C) ' v y)) ') ' = D v y.  [para (9 (a 1) 1348 (a 1 1 1 1 2))]

given #633 (wt=21): 12734 ((C v (x v y)) ' v (D v ((y v C) ' v x)) ') ' = D v x.  [para (9 (a 1) 1348 (a 1 1 1 1)) demod (8)]

given #634 (wt=21): 12771 ((C v (x v y)) ' v (C v ((D v x) ' v y)) ') ' = C v y.  [para (15 (a 1) 1363 (a 1 1 1 1))]

given #635 (wt=21): 12774 ((x v (y v C)) ' v (C v ((D v y) ' v x)) ') ' = C v x.  [para (16 (a 1) 1363 (a 1 1 1 1))]

given #636 (wt=29): 268 ((x v y) ' v (x v ((y v z) ' v (y v ((z v u) ' v (z v u ') ')) ')) ') ' = x.  [para (22 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #637 (wt=21): 12781 ((C v (x v y)) ' v (D v ((C v y) ' v x)) ') ' = D v x.  [para (9 (a 1) 1365 (a 1 1 1 1 2))]

given #638 (wt=21): 12787 ((x v (y v C)) ' v (D v ((C v x) ' v y)) ') ' = D v y.  [para (16 (a 2) 1365 (a 1 1 1 1))]

given #639 (wt=21): 12790 ((x v (y v C)) ' v (D v ((C v y) ' v x)) ') ' = D v x.  [para (33 (a 1) 1365 (a 1 1 1 1))]

given #640 (wt=21): 12793 ((C v ((D v x) ' v y)) ' v (x v (y v C)) ') ' = y v C.  [para (9 (a 1) 1378 (a 1 1))]

given #641 (wt=26): 269 (x v (x v ((x v y) ' v ((y v z) ' v (y v z ') '))) ') ' = (x v y) '.  [para (22 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #642 (wt=21): 12856 ((C v (x v y)) ' v (C v ((x v D) ' v y)) ') ' = C v y.  [para (15 (a 1) 1552 (a 1 1 1 1))]

given #643 (wt=21): 12859 ((x v (y v C)) ' v (C v ((y v D) ' v x)) ') ' = C v x.  [para (16 (a 1) 1552 (a 1 1 1 1))]

given #644 (wt=21): 12872 ((C v ((x v D) ' v y)) ' v (x v (y v C)) ') ' = y v C.  [para (9 (a 1) 1566 (a 1 1))]

given #645 (wt=21): 12901 ((x v C) ' v (D v (D v (C ' v x))) ') ' = D v (D v x).  [para (9 (a 1) 1797 (a 1 1 1 1))]

given #646 (wt=32): 270 (x v ((x v y) ' v (((x v y ') ' v z) ' v ((x v y ') ' v z ') ')) ') ' = (x v y) '.  [para (10 (a 1) 22 (a 1 1 1))]

given #647 (wt=21): 12976 ((D v (x v (y v C) ')) ' v (y v (x v C)) ') ' = D v x.  [para (9 (a 1) 1933 (a 1 1 2 1 2))]

given #648 (wt=21): 13009 ((x v (D v (y v C) ')) ' v (y v (x v C)) ') ' = x v D.  [para (9 (a 1) 1936 (a 1 1 2 1 2))]

given #649 (wt=21): 13010 ((x v (D v (y v C) ')) ' v (C v (x v y)) ') ' = x v D.  [para (9 (a 1) 1936 (a 1 1 2 1)) demod (8)]

given #650 (wt=21): 13058 ((C v (x v (D v y) ')) ' v (y v (x v C)) ') ' = C v x.  [para (9 (a 1) 1947 (a 1 1 2 1 2))]

given #651 (wt=26): 271 ((x v (y v z) ') ' v (x v (y v (y v (z ' v (y v z) ')) ')) ') ' = x.  [para (10 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 9)]

given #652 (wt=21): 13059 ((x v (C v (D v y) ')) ' v (y v (C v x)) ') ' = C v x.  [para (15 (a 1) 1947 (a 1 1 1 1))]

given #653 (wt=21): 13060 ((C v (x v (D v y) ')) ' v (C v (y v x)) ') ' = C v x.  [para (15 (a 1) 1947 (a 1 1 2 1))]

given #654 (wt=21): 13063 ((D v (x v (C v y) ')) ' v (y v (x v C)) ') ' = D v x.  [para (16 (a 2) 1949 (a 1 1 2 1))]

given #655 (wt=21): 13067 ((x v (D v (C v y) ')) ' v (C v (x v y)) ') ' = x v D.  [para (9 (a 1) 1951 (a 1 1 2 1 2))]

given #656 (wt=25): 273 ((C v x) ' v (C v ((D v (x v y)) ' v (D v (x v y ')) ')) ') ' = C.  [para (24 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #657 (wt=21): 13068 ((x v (D v (C v y) ')) ' v (y v (x v C)) ') ' = x v D.  [para (16 (a 2) 1951 (a 1 1 2 1))]

given #658 (wt=21): 13070 ((x v (C v (D v y) ')) ' v (C v (y v x)) ') ' = x v C.  [para (16 (a 1) 1962 (a 1 1 2 1))]

given #659 (wt=21): 13075 ((C v (x v (y v D) ')) ' v (y v (x v C)) ') ' = C v x.  [para (9 (a 1) 2006 (a 1 1 2 1 2))]

given #660 (wt=21): 13076 ((x v (C v (y v D) ')) ' v (y v (C v x)) ') ' = C v x.  [para (15 (a 1) 2006 (a 1 1 1 1))]

given #661 (wt=23): 274 ((x v C) ' v (x v ((C v y) ' v (C v (D v y) ') ')) ') ' = x.  [para (24 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #662 (wt=21): 13077 ((C v (x v (y v D) ')) ' v (C v (y v x)) ') ' = C v x.  [para (15 (a 1) 2006 (a 1 1 2 1))]

given #663 (wt=21): 13080 ((x v (C v (y v D) ')) ' v (C v (y v x)) ') ' = x v C.  [para (16 (a 1) 2021 (a 1 1 2 1))]

given #664 (wt=21): 13238 ((C v (x v y)) ' v (C v (y v (D v (x v D))) ') ') ' = C.  [para (15 (a 1) 2294 (a 1 1 2 1 2 1))]

given #665 (wt=21): 13315 ((x v (D v (D v C '))) ' v (C v x) ') ' = x v (D v D).  [para (27 (a 1) 218 (a 1 1 2 1))]

given #666 (wt=27): 275 ((x v (y v z)) ' v (y v ((x v (z v u)) ' v (x v (z v u ')) ')) ') ' = y.  [para (15 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #667 (wt=21): 13318 ((C v (x v y)) ' v (C v (y v (x v (D v D))) ') ') ' = C.  [para (9 (a 1) 3418 (a 1 1 1 1 2))]

given #668 (wt=21): 13320 ((x v (C v y)) ' v (C v (x v (y v (D v D))) ') ') ' = C.  [para (15 (a 1) 3418 (a 1 1 1 1))]

given #669 (wt=21): 13322 ((x v (C v y)) ' v (C v (y v (x v (D v D))) ') ') ' = C.  [para (16 (a 1) 3418 (a 1 1 1 1))]

given #670 (wt=21): 13324 ((x v (y v C)) ' v (C v (x v (y v (D v D))) ') ') ' = C.  [para (16 (a 2) 3418 (a 1 1 1 1))]

given #671 (wt=25): 276 ((x v y) ' v (x v ((z v (y v u)) ' v (y v (z v u) ') ')) ') ' = x.  [para (15 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #672 (wt=21): 13327 ((x v (y v C)) ' v (C v (y v (x v (D v D))) ') ') ' = C.  [para (33 (a 1) 3418 (a 1 1 1 1))]

given #673 (wt=21): 13350 ((x ' v y) ' v (y v (y v (x v (y v x ') '))) ') ' = y.  [para (9 (a 1) 5893 (a 1 1 1 1))]

given #674 (wt=21): 13351 ((x v y ') ' v (x v (x v (y v (y ' v x) '))) ') ' = x.  [para (9 (a 1) 5893 (a 1 1 2 1 2 2 2 1))]

given #675 (wt=21): 13354 ((x ' v y) ' v (y v (x v (y v (y v x ') '))) ') ' = y.  [para (9 (a 1) 5909 (a 1 1 1 1))]

given #676 (wt=25): 278 ((C v x) ' v (C v ((x v (D v y)) ' v (x v (D v y ')) ')) ') ' = C.  [para (27 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #677 (wt=21): 13355 ((x v y ') ' v (x v (y v (x v (y ' v x) '))) ') ' = x.  [para (9 (a 1) 5909 (a 1 1 2 1 2 2 2 1))]

given #678 (wt=21): 13356 ((x ' v y) ' v (x v (y v (y v (y v x ') '))) ') ' = y.  [para (9 (a 1) 6226 (a 1 1 1 1))]

given #679 (wt=21): 13357 ((x v y ') ' v (y v (x v (x v (y ' v x) '))) ') ' = x.  [para (9 (a 1) 6226 (a 1 1 2 1 2 2 2 1))]

given #680 (wt=21): 13361 ((x v (C v y)) ' v (C v (y v (D v (D v x))) ') ') ' = C.  [para (16 (a 1) 6736 (a 1 1 1 1))]

given #681 (wt=23): 279 ((x v C) ' v (x v ((C v y) ' v (C v (y v D) ') ')) ') ' = x.  [para (27 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #682 (wt=21): 13363 ((x v (y v C)) ' v (C v (x v (D v (D v y))) ') ') ' = C.  [para (16 (a 2) 6736 (a 1 1 1 1))]

given #683 (wt=21): 13364 ((x v (y v C)) ' v (C v (y v (D v (D v x))) ') ') ' = C.  [para (33 (a 1) 6736 (a 1 1 1 1))]

given #684 (wt=21): 13367 ((x v (C v y)) ' v (C v (y v (D v (x v D))) ') ') ' = C.  [para (16 (a 1) 6737 (a 1 1 1 1))]

given #685 (wt=21): 13368 ((x v (y v C)) ' v (C v (x v (D v (y v D))) ') ') ' = C.  [para (16 (a 2) 6737 (a 1 1 1 1))]

given #686 (wt=27): 280 ((x v (y v z)) ' v (y v ((z v (x v u)) ' v (z v (x v u ')) ')) ') ' = y.  [para (16 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #687 (wt=21): 13369 ((x v (y v C)) ' v (C v (y v (D v (x v D))) ') ') ' = C.  [para (33 (a 1) 6737 (a 1 1 1 1))]

given #688 (wt=21): 13381 ((C v ((D v x) ' v y)) ' v (y v (x v C)) ') ' = y v C.  [para (9 (a 1) 8741 (a 1 1 2 1 2))]

given #689 (wt=21): 13392 ((C v ((x v D) ' v y)) ' v (y v (x v C)) ') ' = y v C.  [para (9 (a 1) 8744 (a 1 1 2 1 2))]

given #690 (wt=21): 13393 ((D v ((x v C) ' v y)) ' v (y v (C v x)) ') ' = D v y.  [para (9 (a 1) 8758 (a 1 1 1 1 2 1 1))]

given #691 (wt=25): 281 ((x v y) ' v (x v ((z v (y v u)) ' v (y v (u v z) ') ')) ') ' = x.  [para (16 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #692 (wt=21): 13394 ((D v ((C v x) ' v y)) ' v (y v (x v C)) ') ' = D v y.  [para (9 (a 1) 8758 (a 1 1 2 1 2))]

given #693 (wt=21): 13397 ((D v ((C v x) ' v y)) ' v (C v (y v x)) ') ' = D v y.  [para (15 (a 1) 8758 (a 1 1 2 1))]

given #694 (wt=21): 13400 ((D v ((C v x) ' v y)) ' v (x v (y v C)) ') ' = D v y.  [para (16 (a 1) 8758 (a 1 1 2 1))]

given #695 (wt=21): 13416 ((D v ((x v C) ' v y)) ' v (x v (y v C)) ') ' = D v y.  [para (15 (a 1) 8767 (a 1 1 2 1))]

given #696 (wt=25): 282 ((x v y) ' v (x v ((z v (u v y)) ' v (y v (z v u) ') ')) ') ' = x.  [para (16 (a 2) 22 (a 1 1 2 1 2 1 1))]

given #697 (wt=21): 13417 ((D v ((x v C) ' v y)) ' v (C v (y v x)) ') ' = D v y.  [para (16 (a 1) 8767 (a 1 1 2 1))]

given #698 (wt=21): 13453 ((x v C) ' v (C v (D v (D v (D v (D v x)))) ') ') ' = C.  [para (9 (a 1) 10163 (a 1 1 1 1))]

given #699 (wt=21): 13461 ((C v x) ' v (C v (D v (D v (x v (D v D)))) ') ') ' = C.  [para (16 (a 1) 10163 (a 1 1 2 1 2 1 2 2))]

given #700 (wt=21): 13478 ((x v C) ' v (C v (D v (D v (D v (x v D)))) ') ') ' = C.  [para (9 (a 1) 10165 (a 1 1 1 1))]

given #701 (wt=27): 283 ((x v (y v z)) ' v (x v ((z v (y v u)) ' v (z v (y v u ')) ')) ') ' = x.  [para (17 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #702 (wt=21): 13480 (C ' v (D v ((x v C) ' v (C v (D v x) ') ')) ') ' = D.  [para (9 (a 1) 10858 (a 1 1 2 1 2 1 1))]

given #703 (wt=21): 13494 (C ' v (D v ((x v C) ' v (C v (x v D) ') ')) ') ' = D.  [para (9 (a 1) 10860 (a 1 1 2 1 2 1 1))]

given #704 (wt=21): 13505 (C ' v (C v ((x v C) ' v (D v (C v x) ') ')) ') ' = C.  [para (9 (a 1) 11242 (a 1 1 2 1 2 1 1))]

given #705 (wt=21): 13520 ((x v C) ' v (x v (D v (D v C '))) ') ' = x v (D v D).  [para (9 (a 1) 11402 (a 1 1 1 1))]

given #706 (wt=25): 284 ((x v y) ' v (x v ((y v (z v u)) ' v (y v (u v z) ') ')) ') ' = x.  [para (17 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #707 (wt=21): 13552 ((D v (D v (C ' v x))) ' v (x v C) ') ' = D v (D v x).  [para (9 (a 1) 12901 (a 1 1))]

given #708 (wt=21): 13636 ((x v C) ' v (C v (D v (D v (x v (D v D)))) ') ') ' = C.  [para (16 (a 1) 13453 (a 1 1 2 1 2 1 2 2))]

given #709 (wt=21): 13640 ((C v x) ' v (C v (D v (x v (D v (D v D)))) ') ') ' = C.  [para (15 (a 1) 13461 (a 1 1 2 1 2 1 2))]

given #710 (wt=21): 13658 ((x v C) ' v (C v (D v (x v (D v (D v D)))) ') ') ' = C.  [para (15 (a 1) 13636 (a 1 1 2 1 2 1 2))]

given #711 (wt=28): 285 (C v (C ' v (((C v D ') ' v x) ' v ((C v D ') ' v x ') ')) ') ' = C '.  [para (25 (a 1) 22 (a 1 1 1))]

given #712 (wt=20): 13666 (C v (C v (C ' v (C v (C v D ') ') ')) ') ' = C '.  [para (68 (a 1) 285 (a 1 1 2 1 2 2)) demod (9 11 9 9 15)]

given #713 (wt=21): 13661 ((C v x) ' v (C v (x v (D v (D v (D v D)))) ') ') ' = C.  [para (15 (a 1) 13640 (a 1 1 2 1 2 1))]

given #714 (wt=21): 13663 ((x v C) ' v (C v (x v (D v (D v (D v D)))) ') ') ' = C.  [para (15 (a 1) 13658 (a 1 1 2 1 2 1))]

given #715 (wt=22): 288 ((x v C ') ' v (x v (C v (C v (C ' v D ')) ')) ') ' = x.  [para (25 (a 1) 22 (a 1 1 2 1 2 2)) demod (15 9)]

given #716 (wt=24): 286 ((x v C ') ' v (x v (C v (C ' v (C v D ') ' ') ')) ') ' = x.  [para (25 (a 1) 22 (a 1 1 2 1 2 1))]

given #717 (wt=22): 305 ((x v C ') ' v (x v (D v (D v (C ' v C ')) ')) ') ' = x.  [para (74 (a 1) 22 (a 1 1 2 1 2 2)) demod (15 9)]

given #718 (wt=22): 355 ((C v ((C v (C ' v D ')) ' v x)) ' v (x v C ') ') ' = x.  [para (40 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #719 (wt=22): 356 ((x v (C v (C v (C ' v D ')) ')) ' v (C ' v x) ') ' = x.  [para (40 (a 1) 20 (a 1 1 2 1 1))]

given #720 (wt=22): 357 ((C ' v x) ' v (C v ((C v (C ' v D ')) ' v x)) ') ' = x.  [para (40 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #721 (wt=27): 287 ((x v y) ' v (x v ((y v C) ' v (y v (C ' v (C v D ') ')) ')) ') ' = x.  [para (25 (a 1) 22 (a 1 1 2 1 2 2 1 2)) demod (9)]

given #722 (wt=22): 361 ((x v C ') ' v (C v ((C v (C ' v D ')) ' v x)) ') ' = x.  [para (40 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #723 (wt=22): 362 ((C ' v x) ' v (x v (C v (C v (C ' v D ')) ')) ') ' = x.  [para (40 (a 1) 90 (a 1 1 1 1 1))]

given #724 (wt=22): 370 ((D v ((D v (C ' v C ')) ' v x)) ' v (x v C ') ') ' = x.  [para (86 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #725 (wt=22): 371 ((x v (D v (D v (C ' v C ')) ')) ' v (C ' v x) ') ' = x.  [para (86 (a 1) 20 (a 1 1 2 1 1))]

given #726 (wt=35): 289 ((x v (y v z)) ' v (x v (y v ((z v u) ' v (z v ((u v v) ' v (u v v ') ')) '))) ') ' = x v y.  [para (22 (a 1) 18 (a 1 1 2 1 2 2)) demod (9)]

given #727 (wt=22): 372 ((C ' v x) ' v (D v ((D v (C ' v C ')) ' v x)) ') ' = x.  [para (86 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #728 (wt=22): 376 ((x v C ') ' v (D v ((D v (C ' v C ')) ' v x)) ') ' = x.  [para (86 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #729 (wt=22): 377 ((C ' v x) ' v (x v (D v (D v (C ' v C ')) ')) ') ' = x.  [para (86 (a 1) 90 (a 1 1 1 1 1))]

given #730 (wt=22): 415 ((x v y) ' v (x v (x v (y ' v (x v y) ')) ' ') ') ' = x.  [para (23 (a 1) 10 (a 1 1 1))]

given #731 (wt=42): 290 (x v (y v ((x v (y v z)) ' v (((x v (y v z ')) ' v u) ' v ((x v (y v z ')) ' v u ') ')) ')) ' = (x v (y v z)) '.  [para (18 (a 1) 22 (a 1 1 1)) demod (8)]

given #732 (wt=22): 430 ((x v y) ' v (y v ((x v y) ' v (y v x ') ' ')) ') ' = y.  [para (19 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 19)]

given #733 (wt=22): 436 ((x v y) ' v (x v ((x v y) ' v (y ' v x) ' ')) ') ' = x.  [para (20 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 20)]

given #734 (wt=22): 442 ((x v y) ' v (y v ((x v y) ' v (x ' v y) ' ')) ') ' = y.  [para (67 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 67)]

given #735 (wt=22): 480 (C ' v (C v (C ' v (C v (D v D) ') ' ') ' ') ') ' = C.  [para (384 (a 1) 21 (a 1 1 2 1 1)) demod (384)]

given #736 (wt=36): 291 ((x v (y v (z v u)) ') ' v (x v (y v (z v ((y v (z v u)) ' v (y v (z v u ')) ' ') '))) ') ' = x.  [para (18 (a 1) 22 (a 1 1 2 1 2 1)) demod (8)]

given #737 (wt=22): 511 (C v ((x v C) ' v (C v (D v x) ') ' ') ') ' = (x v C) '.  [para (382 (a 1) 10 (a 1 1 1))]

given #738 (wt=22): 533 (C v ((x v C) ' v (C v (x v D) ') ' ') ') ' = (x v C) '.  [para (491 (a 1) 10 (a 1 1 1))]

given #739 (wt=22): 596 ((x v C ') ' v (C v (x v (C v (C ' v D ')) ')) ') ' = x.  [para (40 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #740 (wt=22): 597 ((x v C ') ' v (D v (x v (D v (C ' v C ')) ')) ') ' = x.  [para (86 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #741 (wt=35): 292 ((x v y) ' v (x v ((y v (z v u)) ' v (y v ((z v (u v v)) ' v (z v (u v v ')) ')) ')) ') ' = x.  [para (18 (a 1) 22 (a 1 1 2 1 2 2 1 2)) demod (9)]

given #742 (wt=22): 609 (D v ((C v x) ' v (D v (C v x) ') ' ') ') ' = (C v x) '.  [para (557 (a 1) 10 (a 1 1 1))]

given #743 (wt=22): 640 (D v ((x v C) ' v (D v (C v x) ') ' ') ') ' = (x v C) '.  [para (607 (a 1) 10 (a 1 1 1))]

given #744 (wt=22): 663 (D v ((C v x) ' v (D v (x v C) ') ' ') ') ' = (C v x) '.  [para (608 (a 1) 10 (a 1 1 1))]

given #745 (wt=22): 684 (D v ((x v C) ' v (D v (x v C) ') ' ') ') ' = (x v C) '.  [para (639 (a 1) 10 (a 1 1 1))]

given #746 (wt=34): 293 ((x v (y v (z v u)) ') ' v (x v (y v (z v (y v (z v (u ' v (y v (z v u)) '))) '))) ') ' = x.  [para (18 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 8 9 8)]

given #747 (wt=22): 758 (C ' v (C v (D v (C ' v (C v D ') ' ') ') ') ') ' = C.  [para (38 (a 1) 28 (a 1 1 1))]

given #748 (wt=22): 776 ((C v C ') ' v (C v (C ' v (D v C ') ' ') ') ') ' = C.  [para (84 (a 1) 28 (a 1 1 2 1 2)) demod (9)]

given #749 (wt=22): 870 (C ' v (C v (D v (C v (C ' v (D v D) ')) ') ') ') ' = C.  [para (473 (a 1) 28 (a 1 1 1))]

given #750 (wt=22): 912 (x v (C v (x v (C v (D ' v (x v C) '))) ')) ' = (x v C) '.  [para (50 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #751 (wt=27): 294 ((x v (y v z)) ' v (z v ((y v (x v u)) ' v (y v (x v u ')) ')) ') ' = z.  [para (33 (a 1) 22 (a 1 1 1 1)) demod (8 8)]

given #752 (wt=22): 932 (x v (C v (C v (D ' v (x v (x v C) '))) ')) ' = (x v C) '.  [para (50 (a 1) 34 (a 1 1 2)) demod (9 8 9 8)]

given #753 (wt=22): 936 (C v (x v (C v (x v (D ' v (C v x) '))) ')) ' = (C v x) '.  [para (55 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #754 (wt=22): 1033 (D v (x v (D v (x v (C ' v (C v x) '))) ')) ' = (C v x) '.  [para (75 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #755 (wt=22): 1188 (x v (D v (x v (D v (C ' v (C v x) '))) ')) ' = (C v x) '.  [para (76 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #756 (wt=25): 295 ((x v y) ' v (x v ((z v (u v y)) ' v (y v (u v z) ') ')) ') ' = x.  [para (33 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #757 (wt=22): 1208 (x v (D v (D v (C ' v (x v (C v x) '))) ')) ' = (C v x) '.  [para (76 (a 1) 34 (a 1 1 2)) demod (9 8 9 8)]

given #758 (wt=22): 1254 ((C v (x v (C v (C ' v D ')) ')) ' v (C ' v x) ') ' = x.  [para (40 (a 1) 96 (a 1 1 2 1 1))]

given #759 (wt=22): 1255 ((D v (x v (D v (C ' v C ')) ')) ' v (C ' v x) ') ' = x.  [para (86 (a 1) 96 (a 1 1 2 1 1))]

given #760 (wt=22): 1796 (D v (x v (D v (C ' v (x v (C v x) '))) ')) ' = (C v x) '.  [para (137 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #761 (wt=29): 296 (((x v y) ' v ((x v ((y v z) ' v (y v z ') ')) ' v u)) ' v (u v x) ') ' = u.  [para (22 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #762 (wt=22): 2063 ((C ' v x) ' v (C v (x v (C v (C ' v D ')) ')) ') ' = x.  [para (40 (a 1) 232 (a 1 1 1 1 1))]

given #763 (wt=22): 2064 ((C ' v x) ' v (D v (x v (D v (C ' v C ')) ')) ') ' = x.  [para (86 (a 1) 232 (a 1 1 1 1 1))]

given #764 (wt=22): 2282 (C v (C v ((C v x) ' v (D v (D v x)) ')) ') ' = (C v x) '.  [para (385 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #765 (wt=22): 2312 (C ' v (C v (D v (D v (C v (C ' v D ')) ')) ') ') ' = C.  [para (40 (a 1) 385 (a 1 1 1))]

given #766 (wt=26): 297 (x v (x v ((y v z) ' v ((y v z ') ' v (x v y) '))) ') ' = (x v y) '.  [para (22 (a 1) 19 (a 1 1 2)) demod (8 8 9)]

given #767 (wt=22): 2454 (C ' v (C v (C ' v (C v (D v (D v D)) ') ' ')) ') ' = C.  [para (2283 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 2283)]

given #768 (wt=22): 2466 (C v (C v ((C v x) ' v (D v (x v D)) ')) ') ' = (C v x) '.  [para (387 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #769 (wt=22): 2671 (x v (C v (x v (C v (D ' v (C v x) '))) ')) ' = (C v x) '.  [para (908 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #770 (wt=22): 2690 (x v (C v (C v (D ' v (x v (C v x) '))) ')) ' = (C v x) '.  [para (908 (a 1) 34 (a 1 1 2)) demod (9 8 9 8)]

given #771 (wt=32): 298 (x v ((y v x) ' v (((x v y ') ' v z) ' v ((x v y ') ' v z ') ')) ') ' = (y v x) '.  [para (19 (a 1) 22 (a 1 1 1))]

given #772 (wt=22): 2752 (x v (C v (C v (x v (D ' v (x v C) '))) ')) ' = (x v C) '.  [para (913 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #773 (wt=22): 2782 (C v (x v (C v (D ' v (x v (C v x) '))) ')) ' = (C v x) '.  [para (933 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #774 (wt=22): 2943 (D v (x v (D v (x v (C ' v (x v C) '))) ')) ' = (x v C) '.  [para (1030 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #775 (wt=22): 2970 (D v (C ' v (D v (C ' v (C v D ') ')) ' ') ') ' = C '.  [para (1070 (a 1) 10 (a 1 1 1))]

given #776 (wt=28): 299 ((x v (y v z) ') ' v (x v (z v ((y v z) ' v (z v y ') ' ') ')) ') ' = x.  [para (19 (a 1) 22 (a 1 1 2 1 2 1))]

given #777 (wt=22): 3002 (x v (D v (x v (D v (C ' v (x v C) '))) ')) ' = (x v C) '.  [para (1185 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #778 (wt=22): 3020 (x v (D v (D v (C ' v (x v (x v C) '))) ')) ' = (x v C) '.  [para (1185 (a 1) 34 (a 1 1 2)) demod (9 8 9 8)]

given #779 (wt=22): 3344 (D v (x v (D v (C ' v (x v (x v C) '))) ')) ' = (x v C) '.  [para (1793 (a 1) 10 (a 1 1 2)) demod (9 8 8 9 8)]

given #780 (wt=22): 3385 (C v (C v ((x v C) ' v (D v (D v x)) ')) ') ' = (x v C) '.  [para (2279 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #781 (wt=29): 300 ((x v y) ' v (x v ((y v z) ' v (y v ((u v z) ' v (z v u ') ')) ')) ') ' = x.  [para (19 (a 1) 22 (a 1 1 2 1 2 2 1 2)) demod (9)]

given #782 (wt=22): 3390 (C v (C v ((D v (D v x)) ' v (x v C) ')) ') ' = (x v C) '.  [para (2279 (a 1) 19 (a 1 1 2)) demod (8 9)]

given #783 (wt=22): 3421 (C v (C v ((C v x) ' v (x v (D v D)) ')) ') ' = (C v x) '.  [para (2289 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #784 (wt=22): 3425 (C v (C v ((x v (D v D)) ' v (C v x) ')) ') ' = (C v x) '.  [para (2289 (a 1) 19 (a 1 1 2)) demod (8 9)]

given #785 (wt=22): 3457 (C v (C v ((x v C) ' v (D v (x v D)) ')) ') ' = (x v C) '.  [para (2463 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #786 (wt=26): 301 ((x v (y v z) ') ' v (x v (z v (z v (y ' v (y v z) ')) ')) ') ' = x.  [para (19 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 9)]

given #787 (wt=22): 3634 (C v (C v ((x v C) ' v (x v (D v D)) ')) ') ' = (x v C) '.  [para (3386 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #788 (wt=22): 3824 ((x v y) ' v (y v (y v (x ' v (x v y) ')) ' ') ') ' = y.  [para (71 (a 1) 10 (a 1 1 1))]

given #789 (wt=22): 4018 ((x v y) ' v (x v (y ' v (x v (x v y) ')) ' ') ') ' = x.  [para (93 (a 1) 10 (a 1 1 1))]

given #790 (wt=22): 4144 ((x v y) ' v (y v (x ' v (y v (x v y) ')) ' ') ') ' = y.  [para (135 (a 1) 10 (a 1 1 1))]

given #791 (wt=28): 302 (D v (C ' v (((D v C ') ' v x) ' v ((D v C ') ' v x ') ')) ') ' = C '.  [para (74 (a 1) 22 (a 1 1 1))]

given #792 (wt=11): 13742 (C v (D v C ') ') ' = C '.  [para (68 (a 1) 302 (a 1 1 2 1 2 2)) demod (11 9 9 15 3035)]

given #793 (wt=11): 13744 (C ' v (C v C ') ') ' = C.  [back_demod 1600 demod (13742 13742)]

given #794 (wt=14): 13777 (C v (C v (C ' v C ')) ') ' = C '.  [para (13742 (a 1) 95 (a 1 1 2 1 2 2)) demod (9 15 24 13742)]

given #795 (wt=15): 13745 (C ' v (C v (D v C ') ' ') ') ' = C.  [para (13742 (a 1) 10 (a 1 1 1))]

given #796 (wt=24): 303 ((x v C ') ' v (x v (D v (C ' v (D v C ') ' ') ')) ') ' = x.  [para (74 (a 1) 22 (a 1 1 2 1 2 1))]

given #797 (wt=16): 13792 (C v (C ' v (C v C ') ' ') ') ' = C '.  [para (13742 (a 1) 72 (a 1 1 2 1 1)) demod (24 13742)]

given #798 (wt=16): 13842 (C ' v (C v (C v (C ' v C '))) ') ' = C.  [para (13742 (a 1) 5893 (a 1 1 1)) demod (13742 9 15 24)]

given #799 (wt=17): 13757 (C ' v (C v (D v (D v C ') ') ') ') ' = C.  [para (13742 (a 1) 28 (a 1 1 1))]

given #800 (wt=17): 13813 (C ' v (D v (C ' v (C v C ') ')) ') ' = D.  [para (13742 (a 1) 10226 (a 1 1 2 1 2 2)) demod (24 9)]

given #801 (wt=27): 304 ((x v y) ' v (x v ((y v D) ' v (y v (C ' v (D v C ') ')) ')) ') ' = x.  [para (74 (a 1) 22 (a 1 1 2 1 2 2 1 2)) demod (9)]

given #802 (wt=17): 13863 (C v (C v (C v C ') ') ') ' = (C v C ') '.  [para (13744 (a 1) 20 (a 1 1 2)) demod (9 9)]

given #803 (wt=18): 13758 (C v (C v (C ' v (D v C ') ' ')) ') ' = C '.  [para (13742 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 13742)]

given #804 (wt=18): 13866 (C ' v (C v (C ' v (C v C ') ' ')) ') ' = C.  [para (13744 (a 1) 23 (a 1 1 2 1 2 2)) demod (9 15 13744)]

given #805 (wt=18): 13891 (C ' v (C v (C v (C ' v C ')) ' ') ') ' = C.  [para (13744 (a 1) 72 (a 1 1 2 1 1)) demod (15 13744)]

given #806 (wt=29): 306 ((x v ((y v z) ' v (y v ((z v u) ' v (z v u ') ')) ')) ' v (y v x) ') ' = x.  [para (22 (a 1) 20 (a 1 1 2 1 1))]

given #807 (wt=19): 13743 (C ' v (C v (C ' ' v (D v C ') ') ') ') ' = C.  [back_demod 5753 demod (13742)]

given #808 (wt=19): 13746 ((x v C ') ' v (x v (C v (D v C ') ')) ') ' = x.  [para (13742 (a 1) 10 (a 1 1 2 1 2)) demod (9)]

given #809 (wt=19): 13748 ((C v ((D v C ') ' v x)) ' v (x v C ') ') ' = x.  [para (13742 (a 1) 19 (a 1 1 2 1 2)) demod (8)]

given #810 (wt=19): 13749 ((x v (C v (D v C ') ')) ' v (C ' v x) ') ' = x.  [para (13742 (a 1) 20 (a 1 1 2 1 1))]

given #811 (wt=35): 307 (x v (x v (y v (x v ((y v z) ' v (y v z ') ')) ')) ') ' = (x v ((y v z) ' v (y v z ') ')) '.  [para (22 (a 1) 20 (a 1 1 2)) demod (9 8 9)]

given #812 (wt=19): 13750 ((C ' v x) ' v (C v ((D v C ') ' v x)) ') ' = x.  [para (13742 (a 1) 67 (a 1 1 2 1 1)) demod (8 9)]

given #813 (wt=19): 13752 (C v (C ' ' v (C v C ') ') ') ' = (C v C ') '.  [para (13742 (a 1) 21 (a 1 1 2 1 2 1)) demod (24 9 24)]

given #814 (wt=19): 13753 ((x v C ') ' v (C v ((D v C ') ' v x)) ') ' = x.  [para (13742 (a 1) 68 (a 1 1 1 1 2)) demod (8)]

given #815 (wt=19): 13754 ((C ' v x) ' v (x v (C v (D v C ') ')) ') ' = x.  [para (13742 (a 1) 90 (a 1 1 1 1 1))]

given #816 (wt=32): 308 (x v ((x v y) ' v (((y ' v x) ' v z) ' v ((y ' v x) ' v z ') ')) ') ' = (x v y) '.  [para (20 (a 1) 22 (a 1 1 1))]

given #817 (wt=19): 13756 ((x v C) ' v (x v (C ' v (C v C ') ')) ') ' = x.  [para (13742 (a 1) 22 (a 1 1 2 1 2 2)) demod (24 9)]

given #818 (wt=19): 13759 ((x v C ') ' v (C v (x v (D v C ') ')) ') ' = x.  [para (13742 (a 1) 29 (a 1 1 2 1 2)) demod (9)]

given #819 (wt=19): 13762 ((C v (x v (D v C ') ')) ' v (C ' v x) ') ' = x.  [para (13742 (a 1) 96 (a 1 1 2 1 1))]

given #820 (wt=19): 13766 ((C ' v x) ' v (C v (x v (D v C ') ')) ') ' = x.  [para (13742 (a 1) 232 (a 1 1 1 1 1))]

given #821 (wt=28): 309 ((x v (y v z) ') ' v (x v (y v ((y v z) ' v (z ' v y) ' ') ')) ') ' = x.  [para (20 (a 1) 22 (a 1 1 2 1 2 1))]

given #822 (wt=19): 13768 (C ' v (C v (D v (D v (D v C ') ')) ') ') ' = C.  [para (13742 (a 1) 385 (a 1 1 1))]

given #823 (wt=19): 13798 ((C ' v ((C v C ') ' v x)) ' v (x v C) ') ' = x.  [para (13742 (a 1) 73 (a 1 1 1 1 2 1)) demod (24 15)]

given #824 (wt=19): 13803 ((x v (C ' v (C v C ') ')) ' v (C v x) ') ' = x.  [para (13742 (a 1) 94 (a 1 1 1 1 2 2)) demod (24 9)]

given #825 (wt=19): 13818 ((C v x) ' v (C ' v ((C v C ') ' v x)) ') ' = x.  [para (13742 (a 1) 136 (a 1 1 2 1 2 1)) demod (24 15)]

given #826 (wt=29): 310 ((x v y) ' v (x v ((y v z) ' v (y v ((z v u) ' v (u ' v z) ')) ')) ') ' = x.  [para (20 (a 1) 22 (a 1 1 2 1 2 2 1 2)) demod (9)]

given #827 (wt=19): 13820 ((x v C) ' v (C ' v ((C v C ') ' v x)) ') ' = x.  [para (13742 (a 1) 204 (a 1 1 2 1 2 1)) demod (24 15)]

given #828 (wt=19): 13822 ((C v x) ' v (x v (C ' v (C v C ') ')) ') ' = x.  [para (13742 (a 1) 230 (a 1 1 2 1 2 2)) demod (24 9)]

given #829 (wt=19): 13830 ((x v C) ' v (C ' v (x v (C v C ') ')) ') ' = x.  [para (13742 (a 1) 587 (a 1 1 2 1 1)) demod (9 24)]

given #830 (wt=19): 13834 ((C v x) ' v (C ' v (x v (C v C ') ')) ') ' = x.  [para (13742 (a 1) 1246 (a 1 1 2 1 1)) demod (9 24)]

given #831 (wt=26): 311 ((x v (y v z) ') ' v (x v (y v (z ' v (y v (y v z) ')) ')) ') ' = x.  [para (20 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 9)]

given #832 (wt=19): 13879 ((C v C ') ' v (C v (C v (C v C ') ')) ') ' = C.  [para (13744 (a 1) 113 (a 1 1 2 1 2 2)) demod (9 8 13744)]

given #833 (wt=19): 13938 (C v (C v (C v (C ' v (C ' v C ')))) ') ' = C '.  [para (13744 (a 1) 5893 (a 1 1 1)) demod (13744 9 15 15 15 15)]

given #834 (wt=20): 13751 (C v (C ' v (C v (D v C ') ' ') ' ') ') ' = C '.  [para (13742 (a 1) 21 (a 1 1 2 1 1)) demod (13742)]

given #835 (wt=20): 13815 (C v (C v (C ' v (D v (D v C ') ') ')) ') ' = C '.  [para (13742 (a 1) 383 (a 1 1 2 1 2 1)) demod (13742)]

given #836 (wt=31): 312 ((x v (C v y)) ' v (D v ((x v (C v (y v z))) ' v (x v (C v (y v z '))) ')) ') ' = D.  [para (26 (a 1) 22 (a 1 1 1 1)) demod (8 8 8 8)]

given #837 (wt=20): 13816 (C ' v (C v (C v (C ' v (D v C ') ' '))) ') ' = C.  [para (13742 (a 1) 416 (a 1 1 1)) demod (13742 9)]

given #838 (wt=20): 13840 (C ' v (C v (C ' v (C v C ') ' ') ' ') ') ' = C.  [para (13742 (a 1) 222 (a 1 1 1)) demod (13742 9 24)]

given #839 (wt=20): 13959 (C ' v (C v (D v (C v (C ' v C ')) ') ') ') ' = C.  [para (13777 (a 1) 28 (a 1 1 1))]

given #840 (wt=20): 14048 (D v (D v (C ' v (C ' v (C v C ') '))) ') ' = C '.  [para (13813 (a 1) 10 (a 1 1 2)) demod (15 9)]

given #841 (wt=27): 313 ((x v D) ' v (x v ((y v (C v z)) ' v (D v (y v (C v z)) ') ')) ') ' = x.  [para (26 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #842 (wt=21): 13801 (C ' v (C v (D v (D v (D v (D v C ') '))) ') ') ' = C.  [para (13742 (a 1) 2284 (a 1 1 1))]

given #843 (wt=21): 13811 (C ' v (D v (C ' v (C v (D v C ') ' ') ')) ') ' = D.  [para (13742 (a 1) 10226 (a 1 1 2 1 2 1))]

given #844 (wt=21): 13828 ((C v C ') ' v (C v (C ' ' v (C v C ') ')) ') ' = C.  [para (13742 (a 1) 161 (a 1 1 2 1 2 2 1)) demod (24 24 9)]

given #845 (wt=15): 14160 (C v (C ' ' v (C v C ') ')) ' = C '.  [para (13828 (a 1) 20 (a 1 1 2)) demod (9 8 9 13946) flip a]

given #846 (wt=31): 314 ((C v (x v y)) ' v (C v ((x v (D v (y v z))) ' v (x v (D v (y v z '))) ')) ') ' = C.  [para (30 (a 1) 22 (a 1 1 1 1)) demod (8 8 8 8)]

given #847 (wt=9): 14190 D v (C v C ') ' = D.  [para (14160 (a 1) 835 (a 1 1 1)) demod (10226) flip a]

given #848 (wt=5): 14225 D ' ' = D.  [para (14190 (a 1) 202 (a 1 1 1 1)) demod (9 24 14221)]

given #849 (wt=5): 14261 D v D = D.  [para (14190 (a 1) 120 (a 1 1 2 1 2)) demod (15 24 9 14221 14254) flip a]

given #850 (wt=5): 14332 C ' ' = C.  [back_demod 14176 demod (14221 14221 14221)]

given #851 (wt=27): 315 ((x v C) ' v (x v ((C v (y v z)) ' v (C v (y v (D v z)) ') ')) ') ' = x.  [para (30 (a 1) 22 (a 1 1 2 1 2 1 1))]

given #852 (wt=7): 14341 (C v C) ' = C '.  [back_demod 14160 demod (14332 14221)]

given #853 (wt=9): 14221 x v (C v C ') ' = x.  [para (14190 (a 1) 42 (a 1 1 1 1 2)) demod (9 14213) flip a]

given #854 (wt=7): 14931 x ' ' ' = x '.  [para (14221 (a 1) 69 (a 1 1 2 1 1 1)) demod (14247 14247 14930 14221)]

-------- Proof 1 -------- (116.48 + 0.23 seconds) Idempotence.

-------- PROOF --------
Length of proof is 49.
Maximum clause weight is 28.
3 ((x v y ') ' v (x v y) ') ' = x.  [input]
8 (x v y) v z = x v (y v z).  [input]
9 x v y = y v x.  [input]
10 ((x v y) ' v (x v y ') ') ' = x.  [copy 3 demod (9)]
11 C v D = C.  [input]
12 A v A != A # answer(Idempotence).  [input]
15 x v (y v z) = y v (x v z).  [para (9 (a 1) 8 (a 1 1)) demod (8)]
16 x v (y v z) = z v (x v y).  [para (9 (a 1) 8 (a 1)) flip a]
18 ((x v (y v z)) ' v (x v (y v z ')) ') ' = x v y.  [para (8 (a 1) 10 (a 1 1 1 1)) demod (8)]
19 ((x v y) ' v (y v x ') ') ' = y.  [para (9 (a 1) 10 (a 1 1 1 1))]
20 ((x v y) ' v (y ' v x) ') ' = x.  [para (9 (a 1) 10 (a 1 1 2 1))]
21 (x v ((x v y) ' v (x v y ') ' ') ') ' = (x v y) '.  [para (10 (a 1) 10 (a 1 1 1))]
22 ((x v y) ' v (x v ((y v z) ' v (y v z ') ')) ') ' = x.  [para (10 (a 1) 10 (a 1 1 2 1 2)) demod (9)]
24 C v (D v x) = C v x.  [para (11 (a 1) 8 (a 1 1)) flip a]
28 ((C v x) ' v (C v (D v x) ') ') ' = C.  [para (24 (a 1) 10 (a 1 1 1 1))]
30 C v (x v (D v y)) = C v (x v y).  [para (15 (a 1) 24 (a 1 2))]
35 ((x v (y v z)) ' v (z v (x v y) ') ') ' = z.  [para (16 (a 2) 10 (a 1 1 1 1))]
42 ((x v (y v z)) ' v (x v (z v y ')) ') ' = x v z.  [para (9 (a 1) 18 (a 1 1 1 1 2))]
68 ((x v y ') ' v (y v x) ') ' = x.  [para (9 (a 1) 19 (a 1 1))]
69 (x v ((y v x) ' v (x v y ') ' ') ') ' = (y v x) '.  [para (19 (a 1) 10 (a 1 1 1))]
73 (((x v y) ' v ((x v y ') ' v z)) ' v (z v x) ') ' = z.  [para (10 (a 1) 19 (a 1 1 2 1 2)) demod (8)]
74 (C ' v (D v C ') ') ' = D.  [para (11 (a 1) 19 (a 1 1 1 1))]
94 ((x v ((y v z) ' v (y v z ') ')) ' v (y v x) ') ' = x.  [para (10 (a 1) 20 (a 1 1 2 1 1))]
111 (D v (C v (D v C ') ') ') ' = (D v C ') '.  [para (74 (a 1) 20 (a 1 1 2)) demod (9 9)]
113 (x v (x v (y v (y ' v x) ')) ') ' = (y ' v x) '.  [para (20 (a 1) 20 (a 1 1 2)) demod (9 8 9)]
161 ((x v y) ' v (x v ((x v y) ' v (x v y ') ' ')) ') ' = x.  [para (21 (a 1) 10 (a 1 1 2)) demod (9)]
207 ((x v (y v z ')) ' v (y v (z v x)) ') ' = x v y.  [para (16 (a 1) 68 (a 1 1 2 1)) demod (8)]
271 ((x v (y v z) ') ' v (x v (y v (y v (z ' v (y v z) ')) ')) ') ' = x.  [para (10 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 9)]
302 (D v (C ' v (((D v C ') ' v x) ' v ((D v C ') ' v x ') ')) ') ' = C '.  [para (74 (a 1) 22 (a 1 1 1))]
835 ((C v (x v y)) ' v (D v (y v (C v x) ')) ') ' = D v y.  [para (30 (a 1) 35 (a 1 1 1 1)) demod (8)]
1585 ((D v C ') ' v (C v (D v C ') ') ') ' = D.  [para (111 (a 1) 10 (a 1 1 2)) demod (15 24 9)]
1600 ((C v (D v C ') ') ' v (C v (C v (D v C ') ') ') ') ' = C.  [para (111 (a 1) 28 (a 1 1 2 1 2)) demod (9)]
3035 (D v (D v (C ' v (C v (D v C ') ') ')) ') ' = (C v (D v C ') ') '.  [para (1585 (a 1) 20 (a 1 1 2)) demod (9 8 9)]
10226 (C ' v (D v ((C v x) ' v (C v x ') ')) ') ' = D.  [para (11 (a 1) 94 (a 1 1 2 1)) demod (9)]
13742 (C v (D v C ') ') ' = C '.  [para (68 (a 1) 302 (a 1 1 2 1 2 2)) demod (11 9 9 15 3035)]
13744 (C ' v (C v C ') ') ' = C.  [back_demod 1600 demod (13742 13742)]
13828 ((C v C ') ' v (C v (C ' ' v (C v C ') ')) ') ' = C.  [para (13742 (a 1) 161 (a 1 1 2 1 2 2 1)) demod (24 24 9)]
13946 (C v (C v (C ' v (C v (C ' ' v (C v C ') ')) ')) ') ' = C '.  [para (13744 (a 1) 271 (a 1 1 1)) demod (15)]
14160 (C v (C ' ' v (C v C ') ')) ' = C '.  [para (13828 (a 1) 20 (a 1 1 2)) demod (9 8 9 13946) flip a]
14190 D v (C v C ') ' = D.  [para (14160 (a 1) 835 (a 1 1 1)) demod (10226) flip a]
14213 ((x v D) ' v (x v (D ' v (C v C ') ')) ') ' = x.  [para (14190 (a 1) 22 (a 1 1 2 1 2 2 1)) demod (15 24 9)]
14221 x v (C v C ') ' = x.  [para (14190 (a 1) 42 (a 1 1 1 1 2)) demod (9 14213) flip a]
14240 ((D ' v ((C v C ') ' v x)) ' v (x v D) ') ' = (C v C ') ' v x.  [para (14190 (a 1) 207 (a 1 1 2 1 2)) demod (16)]
14247 (C v C ') ' v x = x.  [para (14190 (a 1) 73 (a 1 1 1 1 2 1 1)) demod (15 24 15 14240)]
14930 (x v x ' ') ' ' = x ' '.  [para (14221 (a 1) 113 (a 1 1 2 1 2 2 1)) demod (14247 14247 14221)]
14931 x ' ' ' = x '.  [para (14221 (a 1) 69 (a 1 1 2 1 1 1)) demod (14247 14247 14930 14221)]
15054 x ' ' = x.  [para (10 (a 1) 14931 (a 1 1 1)) demod (10)]
15100 x v x = x.  [back_demod 14930 demod (15054 15054 15054)]
15101 $F # answer(Idempotence).  [resolve (15100 a 12 a)]

-------- end of proof  -------

% Disabling goal clause 12.

given #855 (wt=5): 15054 x ' ' = x.  [para (10 (a 1) 14931 (a 1 1 1)) demod (10)]

-------- Proof 2 -------- (117.57 + 0.23 seconds) Huntington_a.

-------- PROOF --------
Length of proof is 49.
Maximum clause weight is 28.
3 ((x v y ') ' v (x v y) ') ' = x.  [input]
8 (x v y) v z = x v (y v z).  [input]
9 x v y = y v x.  [input]
10 ((x v y) ' v (x v y ') ') ' = x.  [copy 3 demod (9)]
11 C v D = C.  [input]
13 (B v A ') ' v (A ' v B ') ' != A # answer(Huntington_a) # action(in_proof -> exit).  [input]
15 x v (y v z) = y v (x v z).  [para (9 (a 1) 8 (a 1 1)) demod (8)]
16 x v (y v z) = z v (x v y).  [para (9 (a 1) 8 (a 1)) flip a]
18 ((x v (y v z)) ' v (x v (y v z ')) ') ' = x v y.  [para (8 (a 1) 10 (a 1 1 1 1)) demod (8)]
19 ((x v y) ' v (y v x ') ') ' = y.  [para (9 (a 1) 10 (a 1 1 1 1))]
20 ((x v y) ' v (y ' v x) ') ' = x.  [para (9 (a 1) 10 (a 1 1 2 1))]
21 (x v ((x v y) ' v (x v y ') ' ') ') ' = (x v y) '.  [para (10 (a 1) 10 (a 1 1 1))]
22 ((x v y) ' v (x v ((y v z) ' v (y v z ') ')) ') ' = x.  [para (10 (a 1) 10 (a 1 1 2 1 2)) demod (9)]
24 C v (D v x) = C v x.  [para (11 (a 1) 8 (a 1 1)) flip a]
28 ((C v x) ' v (C v (D v x) ') ') ' = C.  [para (24 (a 1) 10 (a 1 1 1 1))]
30 C v (x v (D v y)) = C v (x v y).  [para (15 (a 1) 24 (a 1 2))]
35 ((x v (y v z)) ' v (z v (x v y) ') ') ' = z.  [para (16 (a 2) 10 (a 1 1 1 1))]
42 ((x v (y v z)) ' v (x v (z v y ')) ') ' = x v z.  [para (9 (a 1) 18 (a 1 1 1 1 2))]
68 ((x v y ') ' v (y v x) ') ' = x.  [para (9 (a 1) 19 (a 1 1))]
69 (x v ((y v x) ' v (x v y ') ' ') ') ' = (y v x) '.  [para (19 (a 1) 10 (a 1 1 1))]
73 (((x v y) ' v ((x v y ') ' v z)) ' v (z v x) ') ' = z.  [para (10 (a 1) 19 (a 1 1 2 1 2)) demod (8)]
74 (C ' v (D v C ') ') ' = D.  [para (11 (a 1) 19 (a 1 1 1 1))]
94 ((x v ((y v z) ' v (y v z ') ')) ' v (y v x) ') ' = x.  [para (10 (a 1) 20 (a 1 1 2 1 1))]
111 (D v (C v (D v C ') ') ') ' = (D v C ') '.  [para (74 (a 1) 20 (a 1 1 2)) demod (9 9)]
113 (x v (x v (y v (y ' v x) ')) ') ' = (y ' v x) '.  [para (20 (a 1) 20 (a 1 1 2)) demod (9 8 9)]
161 ((x v y) ' v (x v ((x v y) ' v (x v y ') ' ')) ') ' = x.  [para (21 (a 1) 10 (a 1 1 2)) demod (9)]
207 ((x v (y v z ')) ' v (y v (z v x)) ') ' = x v y.  [para (16 (a 1) 68 (a 1 1 2 1)) demod (8)]
271 ((x v (y v z) ') ' v (x v (y v (y v (z ' v (y v z) ')) ')) ') ' = x.  [para (10 (a 1) 22 (a 1 1 2 1 2 2)) demod (9 8 9)]
302 (D v (C ' v (((D v C ') ' v x) ' v ((D v C ') ' v x ') ')) ') ' = C '.  [para (74 (a 1) 22 (a 1 1 1))]
835 ((C v (x v y)) ' v (D v (y v (C v x) ')) ') ' = D v y.  [para (30 (a 1) 35 (a 1 1 1 1)) demod (8)]
1585 ((D v C ') ' v (C v (D v C ') ') ') ' = D.  [para (111 (a 1) 10 (a 1 1 2)) demod (15 24 9)]
1600 ((C v (D v C ') ') ' v (C v (C v (D v C ') ') ') ') ' = C.  [para (111 (a 1) 28 (a 1 1 2 1 2)) demod (9)]
3035 (D v (D v (C ' v (C v (D v C ') ') ')) ') ' = (C v (D v C ') ') '.  [para (1585 (a 1) 20 (a 1 1 2)) demod (9 8 9)]
10226 (C ' v (D v ((C v x) ' v (C v x ') ')) ') ' = D.  [para (11 (a 1) 94 (a 1 1 2 1)) demod (9)]
13742 (C v (D v C ') ') ' = C '.  [para (68 (a 1) 302 (a 1 1 2 1 2 2)) demod (11 9 9 15 3035)]
13744 (C ' v (C v C ') ') ' = C.  [back_demod 1600 demod (13742 13742)]
13828 ((C v C ') ' v (C v (C ' ' v (C v C ') ')) ') ' = C.  [para (13742 (a 1) 161 (a 1 1 2 1 2 2 1)) demod (24 24 9)]
13946 (C v (C v (C ' v (C v (C ' ' v (C v C ') ')) ')) ') ' = C '.  [para (13744 (a 1) 271 (a 1 1 1)) demod (15)]
14160 (C v (C ' ' v (C v C ') ')) ' = C '.  [para (13828 (a 1) 20 (a 1 1 2)) demod (9 8 9 13946) flip a]
14190 D v (C v C ') ' = D.  [para (14160 (a 1) 835 (a 1 1 1)) demod (10226) flip a]
14213 ((x v D) ' v (x v (D ' v (C v C ') ')) ') ' = x.  [para (14190 (a 1) 22 (a 1 1 2 1 2 2 1)) demod (15 24 9)]
14221 x v (C v C ') ' = x.  [para (14190 (a 1) 42 (a 1 1 1 1 2)) demod (9 14213) flip a]
14240 ((D ' v ((C v C ') ' v x)) ' v (x v D) ') ' = (C v C ') ' v x.  [para (14190 (a 1) 207 (a 1 1 2 1 2)) demod (16)]
14247 (C v C ') ' v x = x.  [para (14190 (a 1) 73 (a 1 1 1 1 2 1 1)) demod (15 24 15 14240)]
14930 (x v x ' ') ' ' = x ' '.  [para (14221 (a 1) 113 (a 1 1 2 1 2 2 1)) demod (14247 14247 14221)]
14931 x ' ' ' = x '.  [para (14221 (a 1) 69 (a 1 1 2 1 1 1)) demod (14247 14247 14930 14221)]
15054 x ' ' = x.  [para (10 (a 1) 14931 (a 1 1 1)) demod (10)]
15241 (x v y) ' v (y v x ') ' = y '.  [para (19 (a 1) 15054 (a 1 1)) flip a]
15697 $F # answer(Huntington_a).  [back_demod 13 demod (15241 15054) xx a]

-------- end of proof  -------

Given=855. Generated=817021. Kept=15688. Proofs=2.
Usable=532. Sos=6718. Demods=7704. Goals=1. Limbo=456, Disabled=7988. Hints=0.
Weight_deleted=10053. Literals_deleted=0.
Forward_subsumed=108802. Back_subsumed=58.
Sos_limit_deleted=682477. Sos_displaced=3158. Sos_removed=0.
New_demodulators=15676 (9 lex), Back_demodulated=4764. Back_unit_deleted=0.
Demod_attempts=34338575. Demod_rewrites=2221609.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
Megabytes=16.73.
User_CPU=117.57, System_CPU=0.23, Wall_clock=120.

SEARCH FAILED

Exiting with 2 proofs.

Process 28709 exit (action) Tue Aug  9 11:38:27 2005