----- Prover9 July-2005E-work, 18 July 2005 ----- Process 28946 was started by mccune on theorem.mcs.anl.gov, Tue Aug 9 11:56:54 2005 The command was "prover9 -f winker2.in". % Reading from file winker2.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). assign(max_weight,50). assign(constant_weight,0). terms(weights). x ' ' = 1000. end_of_list. 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 # label(Robbins). (C v D) ' = C '. end_of_list. assign(max_proofs,- 1). clauses(goals). A v A != A # answer(Idempotence). x v y != x # answer(Winker1a). x v y != y # answer(Winker1b). (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 9 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). 10 (x v y) v z = x v (y v z). [input] 11 x v y = y v x. [input] 12 ((x v y) ' v (x v y ') ') ' = x # label(Robbins). [copy 3 demod (11)] 13 (C v D) ' = C '. [input] end_of_list. clauses(demodulators). 10 (x v y) v z = x v (y v z). [input] 11 x v y = y v x. [input] % (lex-dep) 12 ((x v y) ' v (x v y ') ') ' = x # label(Robbins). [copy 3 demod (11)] 13 (C v D) ' = C '. [input] end_of_list. clauses(goals). 14 A v A != A # answer(Idempotence). [input] 15 x v y != x # answer(Winker1a). [input] 16 x v y != y # answer(Winker1b). [input] 17 (B v A ') ' v (A ' v B ') ' != A # answer(Huntington_a) # action(in_proof -> exit). [input] 18 (A v B ') ' v (A ' v B ') ' != B # answer(Huntington_b) # action(in_proof -> exit). [input] end_of_list. % Starting search at 0.00 seconds. given #1 (wt=11): 10 (x v y) v z = x v (y v z). [input] given #2 (wt=7): 11 x v y = y v x. [input] given #3 (wt=13): 12 ((x v y) ' v (x v y ') ') ' = x # label(Robbins). [copy 3 demod (11)] given #4 (wt=4): 13 (C v D) ' = C '. [input] given #5 (wt=7): 27 (C ' v (C v D ') ') ' = C. [para (13 (a 1) 12 (a 1 1 1))] given #6 (wt=11): 19 x v (y v z) = y v (x v z). [para (11 (a 1) 10 (a 1 1)) demod (10)] given #7 (wt=9): 30 (C v (C v (C ' v D ')) ') ' = C '. [para (27 (a 1) 12 (a 1 1 2)) demod (19 11)] given #8 (wt=10): 33 (C ' v (C v (C v (C ' v D '))) ') ' = C. [para (30 (a 1) 12 (a 1 1 2)) demod (11)] given #9 (wt=11): 20 x v (y v z) = z v (x v y). [para (11 (a 1) 10 (a 1)) flip a] given #10 (wt=11): 21 x v (y v z) = x v (z v y). [para (11 (a 1) 10 (a 2 2)) demod (10)] given #11 (wt=19): 22 ((x v (y v z)) ' v (x v (y v z ')) ') ' = x v y. [para (10 (a 1) 12 (a 1 1 1 1)) demod (10)] given #12 (wt=11): 36 x v (y v z) = z v (y v x). [para (11 (a 1) 20 (a 2 2))] given #13 (wt=12): 28 ((x v (C v D)) ' v (x v C ') ') ' = x. [para (13 (a 1) 12 (a 1 1 2 1 2))] given #14 (wt=12): 35 (C v (C v (C v (C ' v (C ' v D ')))) ') ' = C '. [para (33 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #15 (wt=12): 65 ((C v (D v x)) ' v (x v C ') ') ' = x. [para (11 (a 1) 28 (a 1 1 1 1)) demod (10)] given #16 (wt=13): 23 ((x v y) ' v (y v x ') ') ' = y. [para (11 (a 1) 12 (a 1 1 1 1))] given #17 (wt=7): 89 (C ' v (D v C ') ') ' = D. [para (13 (a 1) 23 (a 1 1 1))] given #18 (wt=9): 102 (D v (D v (C ' v C ')) ') ' = C '. [para (89 (a 1) 12 (a 1 1 2)) demod (19 11)] given #19 (wt=10): 106 (C ' v (D v (D v (C ' v C '))) ') ' = D. [para (102 (a 1) 12 (a 1 1 2)) demod (11)] given #20 (wt=12): 66 ((x v (C v D)) ' v (C ' v x) ') ' = x. [para (11 (a 1) 28 (a 1 1 2 1))] given #21 (wt=13): 24 ((x v y) ' v (y ' v x) ') ' = x. [para (11 (a 1) 12 (a 1 1 2 1))] given #22 (wt=11): 134 (C v (C v (C v D ') ') ') ' = (C v D ') '. [para (27 (a 1) 24 (a 1 1 2)) demod (11 11)] given #23 (wt=11): 155 (D v (C v (D v C ') ') ') ' = (D v C ') '. [para (89 (a 1) 24 (a 1 1 2)) demod (11 11)] given #24 (wt=12): 69 ((C v (x v D)) ' v (x v C ') ') ' = x. [para (19 (a 1) 28 (a 1 1 1 1))] given #25 (wt=12): 74 ((C v (D v x)) ' v (C ' v x) ') ' = x. [para (11 (a 1) 65 (a 1 1 2 1))] given #26 (wt=21): 25 ((x v y) ' v (x v ((y v z) ' v (y v z ') ')) ') ' = x. [para (12 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #27 (wt=12): 75 ((x v C ') ' v (C v (D v x)) ') ' = x. [para (11 (a 1) 65 (a 1 1))] given #28 (wt=12): 111 (D v (D v (D v (C ' v (C ' v C ')))) ') ' = C '. [para (106 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #29 (wt=12): 115 ((C ' v x) ' v (x v (C v D)) ') ' = x. [para (11 (a 1) 66 (a 1 1))] given #30 (wt=12): 119 ((C v (x v D)) ' v (C ' v x) ') ' = x. [para (19 (a 1) 66 (a 1 1 1 1))] given #31 (wt=18): 26 (x v (x v (y ' v (x v y) ')) ') ' = (x v y) '. [para (12 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #32 (wt=9): 306 (x v y) ' = (y v x) '. [para (11 (a 1) 26 (a 1 1 2 1 2 2 1)) demod (87)] given #33 (wt=12): 164 ((C v D ') ' v (C v (C v (C v D ') ')) ') ' = C. [para (134 (a 1) 12 (a 1 1 2)) demod (11)] given #34 (wt=12): 170 ((D v C ') ' v (C v (D v (D v C ') ')) ') ' = D. [para (155 (a 1) 12 (a 1 1 2)) demod (19 11)] given #35 (wt=12): 175 ((x v C ') ' v (C v (x v D)) ') ' = x. [para (11 (a 1) 69 (a 1 1))] given #36 (wt=15): 29 ((x v C) ' v (x v (C ' v (C v D ') ')) ') ' = x. [para (27 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #37 (wt=12): 288 ((C ' v x) ' v (C v (x v D)) ') ' = x. [para (19 (a 1) 115 (a 1 1 2 1))] given #38 (wt=13): 72 (C ' v (C v (C v (C v (C ' v (C ' v D '))))) ') ' = C. [para (35 (a 1) 12 (a 1 1 2)) demod (11)] given #39 (wt=13): 84 ((x v y) ' v (x ' v y) ') ' = y. [para (11 (a 1) 23 (a 1 1 2 1))] given #40 (wt=13): 85 ((x v y ') ' v (y v x) ') ' = x. [para (11 (a 1) 23 (a 1 1))] given #41 (wt=17): 31 ((x v (y v z)) ' v (y v (x v z) ') ') ' = y. [para (19 (a 1) 12 (a 1 1 1 1))] given #42 (wt=13): 128 ((x ' v y) ' v (y v x) ') ' = y. [para (11 (a 1) 24 (a 1 1))] given #43 (wt=13): 277 (C ' v (D v (D v (D v (C ' v (C ' v C '))))) ') ' = D. [para (111 (a 1) 12 (a 1 1 2)) demod (11)] given #44 (wt=14): 198 (C ' v (C v ((D v x) ' v (D v x ') ')) ') ' = C. [para (13 (a 1) 25 (a 1 1 1))] given #45 (wt=13): 613 (C ' v (C v ((C v (D v D)) ' v (D v C ') ')) ') ' = C. [para (13 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (19)] given #46 (wt=17): 32 ((x v C ') ' v (x v (C v (C v (C ' v D ')) ')) ') ' = x. [para (30 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #47 (wt=14): 609 (C ' v (C v ((x v D) ' v (D v x ') ')) ') ' = C. [para (11 (a 1) 198 (a 1 1 2 1 2 1 1))] given #48 (wt=11): 702 (C ' v (C v (C ' v (D v C ') ')) ') ' = C. [para (13 (a 1) 609 (a 1 1 2 1 2 1))] given #49 (wt=13): 717 (C v (C v (C ' v (C ' v (D v C ') '))) ') ' = C '. [para (702 (a 1) 12 (a 1 1 2)) demod (19 11)] given #50 (wt=14): 631 (C ' v (C v (C ' v (D v (D v (C ' v C '))) ')) ') ' = C. [para (102 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #51 (wt=18): 34 ((x v C) ' v (x v (C ' v (C v (C v (C ' v D '))) ')) ') ' = x. [para (33 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #52 (wt=14): 731 (C ' v (C v (C v (C ' v (C ' v (D v C ') ')))) ') ' = C. [para (717 (a 1) 12 (a 1 1 2)) demod (11)] given #53 (wt=15): 90 ((C ' v ((C v D ') ' v x)) ' v (x v C) ') ' = x. [para (27 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #54 (wt=15): 101 ((x v D) ' v (x v (C ' v (D v C ') ')) ') ' = x. [para (89 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #55 (wt=15): 104 ((C ' v ((D v C ') ' v x)) ' v (x v D) ') ' = x. [para (89 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #56 (wt=17): 37 ((x v (y v z)) ' v (y v (z v x) ') ') ' = y. [para (20 (a 1) 12 (a 1 1 1 1))] given #57 (wt=15): 133 ((x v (C ' v (C v D ') ')) ' v (C v x) ') ' = x. [para (27 (a 1) 24 (a 1 1 2 1 1))] given #58 (wt=11): 886 (C ' v (D v (C ' v (C v D ') ')) ') ' = D. [para (13 (a 1) 133 (a 1 1 2)) demod (11)] given #59 (wt=13): 911 (D v (D v (C ' v (C ' v (C v D ') '))) ') ' = C '. [para (886 (a 1) 12 (a 1 1 2)) demod (19 11)] given #60 (wt=14): 925 (C ' v (D v (D v (C ' v (C ' v (C v D ') ')))) ') ' = D. [para (911 (a 1) 12 (a 1 1 2)) demod (11)] given #61 (wt=17): 38 ((x v (y v z)) ' v (z v (x v y) ') ') ' = z. [para (20 (a 2) 12 (a 1 1 1 1))] given #62 (wt=15): 154 ((x v (C ' v (D v C ') ')) ' v (D v x) ') ' = x. [para (89 (a 1) 24 (a 1 1 2 1 1))] given #63 (wt=15): 371 ((C v x) ' v (x v (C ' v (C v D ') ')) ') ' = x. [para (11 (a 1) 29 (a 1 1 1 1))] given #64 (wt=15): 372 ((x v C) ' v (C ' v ((C v D ') ' v x)) ') ' = x. [para (11 (a 1) 29 (a 1 1 2 1)) demod (10)] given #65 (wt=15): 374 ((x v C) ' v (C ' v (x v (C v D ') ')) ') ' = x. [para (19 (a 1) 29 (a 1 1 2 1))] given #66 (wt=17): 39 ((x v (y v z)) ' v (x v (z v y) ') ') ' = x. [para (21 (a 1) 12 (a 1 1 1 1))] given #67 (wt=15): 392 (C v (C v (C v (C v (C ' v (C ' v (C ' v D ')))))) ') ' = C '. [para (72 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #68 (wt=15): 405 ((C v x) ' v (C ' v ((C v D ') ' v x)) ') ' = x. [para (27 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #69 (wt=15): 420 ((D v x) ' v (C ' v ((D v C ') ' v x)) ') ' = x. [para (89 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #70 (wt=15): 464 ((x v D) ' v (C ' v ((D v C ') ' v x)) ') ' = x. [para (89 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #71 (wt=25): 40 ((x v (y v (z v u))) ' v (x v (y v (z v u '))) ') ' = x v (y v z). [para (10 (a 1) 22 (a 1 1 1 1 2)) demod (10)] given #72 (wt=15): 514 ((x v D) ' v (C ' v (x v (D v C ') ')) ') ' = x. [para (89 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #73 (wt=15): 562 ((D v x) ' v (x v (C ' v (D v C ') ')) ') ' = x. [para (89 (a 1) 128 (a 1 1 1 1 1))] given #74 (wt=15): 595 (D v (D v (D v (D v (C ' v (C ' v (C ' v C ')))))) ') ' = C '. [para (277 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #75 (wt=15): 614 (C ' v (C v (C ' v (D v (C ' v (C v D ') ')) ')) ') ' = C. [para (27 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11 13 11)] given #76 (wt=19): 41 ((x v (y v z)) ' v (x v (z v y ')) ') ' = x v z. [para (11 (a 1) 22 (a 1 1 1 1 2))] given #77 (wt=15): 671 (C v (C v (C ' v ((C v (D v D)) ' v (D v C ') '))) ') ' = C '. [para (613 (a 1) 12 (a 1 1 2)) demod (19 11)] given #78 (wt=15): 887 ((C v x) ' v (C ' v (x v (C v D ') ')) ') ' = x. [para (19 (a 1) 133 (a 1 1 1 1)) demod (11)] given #79 (wt=15): 980 ((D v x) ' v (C ' v (x v (D v C ') ')) ') ' = x. [para (19 (a 1) 154 (a 1 1 1 1)) demod (11)] given #80 (wt=16): 344 (C v (C v (C v ((C v D ') ' v (C v D ') '))) ') ' = (C v D ') '. [para (164 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #81 (wt=19): 42 ((x v (y v z)) ' v (z v (x v y ')) ') ' = z v x. [para (11 (a 1) 22 (a 1 1 1 1)) demod (10)] given #82 (wt=16): 353 (D v (C v (D v ((D v C ') ' v (D v C ') '))) ') ' = (D v C ') '. [para (170 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #83 (wt=16): 611 (C v (C v (C ' v ((D v x) ' v (D v x ') '))) ') ' = C '. [para (198 (a 1) 12 (a 1 1 2)) demod (19 11)] given #84 (wt=16): 629 (C ' v (C v ((D v D) ' v (D v (C ' v (D v C ') ')) ')) ') ' = C. [para (89 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11)] given #85 (wt=16): 639 (C ' v (C v ((D v C ') ' v (C v (D v (D v C ') ')) ')) ') ' = C. [para (155 (a 1) 198 (a 1 1 2 1 2 2)) demod (19 11)] given #86 (wt=19): 43 ((x v (y v z)) ' v (x v (z ' v y)) ') ' = x v y. [para (11 (a 1) 22 (a 1 1 2 1 2))] given #87 (wt=16): 701 (C v (C v (C ' v ((x v D) ' v (D v x ') '))) ') ' = C '. [para (609 (a 1) 12 (a 1 1 2)) demod (19 11)] given #88 (wt=16): 746 (C v (C v (C ' v (C ' v (D v (D v (C ' v C '))) '))) ') ' = C '. [para (631 (a 1) 12 (a 1 1 2)) demod (19 11)] given #89 (wt=16): 775 (C v (C v (C v (C ' v (C ' v (C ' v (D v C ') '))))) ') ' = C '. [para (731 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #90 (wt=16): 940 (D v (D v (D v (C ' v (C ' v (C ' v (C v D ') '))))) ') ' = C '. [para (925 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #91 (wt=19): 44 ((x v (y v z)) ' v (y v (z ' v x)) ') ' = x v y. [para (11 (a 1) 22 (a 1 1 2 1)) demod (10)] given #92 (wt=16): 1080 (C ' v (C v (C v (C v (C v (C ' v (C ' v (C ' v D '))))))) ') ' = C. [para (392 (a 1) 12 (a 1 1 2)) demod (11)] given #93 (wt=16): 1276 (C ' v (D v (D v (D v (D v (C ' v (C ' v (C ' v C '))))))) ') ' = D. [para (595 (a 1) 12 (a 1 1 2)) demod (11)] given #94 (wt=16): 1399 (C ' v (C v (C v (C ' v ((C v (D v D)) ' v (D v C ') ')))) ') ' = C. [para (671 (a 1) 12 (a 1 1 2)) demod (11)] given #95 (wt=17): 60 ((x v (y v z)) ' v (z v (y v x) ') ') ' = z. [para (36 (a 1) 12 (a 1 1 1 1))] given #96 (wt=27): 45 ((x v (y v z)) ' v (x v ((y v (z v u)) ' v (y v (z v u ')) ')) ') ' = x. [para (22 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #97 (wt=17): 68 (x v (x v (C ' v (x v (C v D)) ')) ') ' = (x v (C v D)) '. [para (28 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #98 (wt=17): 77 (x v (x v (C ' v (C v (D v x)) ')) ') ' = (C v (D v x)) '. [para (65 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #99 (wt=17): 91 (C ' v (C ' v (C v (C ' v D ')) ') ') ' = (C v (C ' v D ')) '. [para (30 (a 1) 23 (a 1 1 1)) demod (11)] given #100 (wt=17): 92 ((C v ((C v (C ' v D ')) ' v x)) ' v (x v C ') ') ' = x. [para (30 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #101 (wt=26): 46 (x v (y v (x v (y v (z ' v (x v (y v z)) '))) ')) ' = (x v (y v z)) '. [para (22 (a 1) 12 (a 1 1 2)) demod (11 10 10 11 10)] given #102 (wt=17): 105 ((x v C ') ' v (x v (D v (D v (C ' v C ')) ')) ') ' = x. [para (102 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #103 (wt=17): 108 (C ' v (D ' v (D v (C ' v C ')) ') ') ' = (D v (C ' v C ')) '. [para (102 (a 1) 23 (a 1 1 1)) demod (11)] given #104 (wt=17): 109 ((D v ((D v (C ' v C ')) ' v x)) ' v (x v C ') ') ' = x. [para (102 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #105 (wt=17): 117 (x v (C ' v (x v (x v (C v D)) ')) ') ' = (x v (C v D)) '. [para (66 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #106 (wt=27): 47 ((x v (y v z)) ' v (x v (y v ((z v u) ' v (z v u ') '))) ') ' = x v y. [para (12 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #107 (wt=17): 135 ((x v (y v z)) ' v ((x v z) ' v y) ') ' = y. [para (19 (a 1) 24 (a 1 1 1 1))] given #108 (wt=17): 136 ((x v (C v (C v (C ' v D ')) ')) ' v (C ' v x) ') ' = x. [para (30 (a 1) 24 (a 1 1 2 1 1))] given #109 (wt=17): 138 (C v (C v (C v (C v (C ' v D '))) ') ') ' = (C v (C v (C ' v D '))) '. [para (33 (a 1) 24 (a 1 1 2)) demod (11 11)] given #110 (wt=17): 139 ((x v (y v z)) ' v ((z v x) ' v y) ') ' = y. [para (20 (a 1) 24 (a 1 1 1 1))] given #111 (wt=18): 48 ((x v (y v (C v D))) ' v (x v (y v C ')) ') ' = x v y. [para (13 (a 1) 22 (a 1 1 2 1 2 2))] given #112 (wt=17): 140 ((x v (y v z)) ' v ((x v y) ' v z) ') ' = z. [para (20 (a 2) 24 (a 1 1 1 1))] given #113 (wt=17): 141 ((x v (y v z)) ' v ((z v y) ' v x) ') ' = x. [para (21 (a 1) 24 (a 1 1 1 1))] given #114 (wt=17): 145 ((x v (y v z)) ' v ((y v x) ' v z) ') ' = z. [para (36 (a 1) 24 (a 1 1 1 1))] given #115 (wt=17): 147 (x v (x v (C v (D v (x v C ') '))) ') ' = (x v C ') '. [para (28 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #116 (wt=21): 49 ((x v (y v C)) ' v (x v (y v (C ' v (C v D ') '))) ') ' = x v y. [para (27 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #117 (wt=17): 150 (x v (C v (D v (x v (x v C ') '))) ') ' = (x v C ') '. [para (65 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #118 (wt=17): 156 ((x v (D v (D v (C ' v C ')) ')) ' v (C ' v x) ') ' = x. [para (102 (a 1) 24 (a 1 1 2 1 1))] given #119 (wt=17): 158 (D v (C v (D v (D v (C ' v C '))) ') ') ' = (D v (D v (C ' v C '))) '. [para (106 (a 1) 24 (a 1 1 2)) demod (11 11)] given #120 (wt=17): 160 (x v (x v (C v (D v (C ' v x) '))) ') ' = (C ' v x) '. [para (66 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #121 (wt=23): 50 ((x v (y v (z v u))) ' v (x v (z v (y v u) ')) ') ' = x v z. [para (19 (a 1) 22 (a 1 1 1 1 2))] given #122 (wt=13): 3400 ((C v D ') ' v (C v (C v (D v (C v D ') '))) ') ' = C. [para (27 (a 1) 160 (a 1 1 2 1 2 2 2)) demod (11 11 10 10 27)] given #123 (wt=13): 3409 ((D v C ') ' v (C v (D v (D v (D v C ') '))) ') ' = D. [para (89 (a 1) 160 (a 1 1 2 1 2 2 2)) demod (11 10 10 89)] given #124 (wt=9): 3666 (C v (D v (D v (D v C ') '))) ' = C '. [back_demod 3232 demod (3652) flip a] given #125 (wt=12): 3669 (C ' v (C v (D v (D v (D v C ') ')) ') ') ' = C. [para (3666 (a 1) 12 (a 1 1 1))] given #126 (wt=19): 51 ((x v (y v z)) ' v (y v (x v z ')) ') ' = y v x. [para (19 (a 1) 22 (a 1 1 1 1))] given #127 (wt=12): 3688 (C ' v (C v (D v (D v (D v C ')))) ') ' = C v (D v D). [para (3666 (a 1) 40 (a 1 1 2)) demod (11)] given #128 (wt=13): 3671 (C ' v (C v (D v (D v (D v C ') ') ')) ') ' = C v D. [para (3666 (a 1) 22 (a 1 1 1))] given #129 (wt=14): 3681 (C v (C v (C ' v (D v (D v (D v C ') ')) ')) ') ' = C '. [para (3666 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 3666)] given #130 (wt=14): 3879 (C v (D v (D v (C v (D v (D v (D v (C ' v C '))))) '))) ' = C '. [para (3688 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 11 10 10)] given #131 (wt=23): 52 ((x v (y v C ')) ' v (x v (y v (C v (C v (C ' v D ')) '))) ') ' = x v y. [para (30 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #132 (wt=15): 3673 (C ' v (D v (C ' v (D v C ') ')) ') ' = D v (D v C ') '. [para (3666 (a 1) 65 (a 1 1 1)) demod (11 19)] given #133 (wt=15): 3698 (C v (D v (C v (D v (C ' v (D v (D v C ') ') '))) ')) ' = C '. [para (3666 (a 1) 46 (a 1 1 2 2 1 2 2 2)) demod (11 3666)] given #134 (wt=15): 3940 (C ' v (C v (C v (C ' v (D v (D v (D v C ') ')) '))) ') ' = C. [para (3681 (a 1) 12 (a 1 1 2)) demod (11)] given #135 (wt=17): 177 (x v (x v (C ' v (C v (x v D)) ')) ') ' = (C v (x v D)) '. [para (69 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #136 (wt=24): 53 ((x v (y v C)) ' v (x v (y v (C ' v (C v (C v (C ' v D '))) '))) ') ' = x v y. [para (33 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #137 (wt=17): 181 (x v (C v (x v (D v (x v C ') '))) ') ' = (x v C ') '. [para (69 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #138 (wt=17): 183 (x v (C ' v (x v (C v (D v x)) ')) ') ' = (C v (D v x)) '. [para (74 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #139 (wt=17): 191 (x v (C v (D v (x v (C ' v x) '))) ') ' = (C ' v x) '. [para (74 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #140 (wt=17): 298 (x v (C ' v (x v (C v (x v D)) ')) ') ' = (C v (x v D)) '. [para (119 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #141 (wt=23): 54 ((x v (y v (z v u))) ' v (x v (z v (u v y) ')) ') ' = x v z. [para (20 (a 1) 22 (a 1 1 1 1 2))] given #142 (wt=17): 302 (x v (C v (x v (D v (C ' v x) '))) ') ' = (C ' v x) '. [para (119 (a 1) 24 (a 1 1 2)) demod (11 10 10 11)] given #143 (wt=17): 408 ((C ' v x) ' v (C v ((C v (C ' v D ')) ' v x)) ') ' = x. [para (30 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #144 (wt=17): 421 ((C ' v x) ' v (D v ((D v (C ' v C ')) ' v x)) ') ' = x. [para (102 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #145 (wt=17): 449 ((x v (y v z) ') ' v (y v (z v x)) ') ' = x. [para (10 (a 1) 85 (a 1 1 2 1))] given #146 (wt=19): 55 ((x v (y v z)) ' v (y v (z v x ')) ') ' = y v z. [para (20 (a 1) 22 (a 1 1 1 1))] given #147 (wt=17): 452 ((x v C ') ' v (C v ((C v (C ' v D ')) ' v x)) ') ' = x. [para (30 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #148 (wt=17): 465 ((x v C ') ' v (D v ((D v (C ' v C ')) ' v x)) ') ' = x. [para (102 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #149 (wt=17): 484 ((x v (y v z) ') ' v (z v (y v x)) ') ' = x. [para (306 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #150 (wt=17): 496 ((x v (y v z) ') ' v (y v (x v z)) ') ' = x. [para (11 (a 1) 31 (a 1 1))] given #151 (wt=19): 56 ((x v (y v z)) ' v (z ' v (x v y)) ') ' = x v y. [para (20 (a 1) 22 (a 1 1 2 1))] given #152 (wt=17): 498 ((x v C ') ' v (C v (x v (C v (C ' v D ')) ')) ') ' = x. [para (30 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #153 (wt=17): 515 ((x v C ') ' v (D v (x v (D v (C ' v C ')) ')) ') ' = x. [para (102 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #154 (wt=17): 549 (((x v y) ' v z) ' v (x v (z v y)) ') ' = z. [para (19 (a 1) 128 (a 1 1 2 1))] given #155 (wt=17): 550 ((C ' v x) ' v (x v (C v (C v (C ' v D ')) ')) ') ' = x. [para (30 (a 1) 128 (a 1 1 1 1 1))] given #156 (wt=23): 57 ((x v (y v (z v u))) ' v (x v (u v (y v z) ')) ') ' = x v u. [para (20 (a 2) 22 (a 1 1 1 1 2))] given #157 (wt=16): 5159 (C ' v (C v ((D v D) ' v (D v C ') ')) ') ' = C v (D v C ') '. [para (3666 (a 1) 57 (a 1 1 1)) demod (11)] given #158 (wt=17): 553 (((x v y) ' v z) ' v (y v (z v x)) ') ' = z. [para (20 (a 1) 128 (a 1 1 2 1))] given #159 (wt=17): 555 (((x v y) ' v z) ' v (z v (y v x)) ') ' = z. [para (21 (a 1) 128 (a 1 1 2 1))] given #160 (wt=17): 563 ((C ' v x) ' v (x v (D v (D v (C ' v C ')) ')) ') ' = x. [para (102 (a 1) 128 (a 1 1 1 1 1))] given #161 (wt=23): 58 ((x v (y v (z v u))) ' v (x v (y v (u v z) ')) ') ' = x v y. [para (21 (a 1) 22 (a 1 1 1 1 2))] given #162 (wt=17): 648 (C ' v (C v (C ' v (D v (D v (D v (C ' v (C ' v C '))))) ')) ') ' = C. [para (111 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #163 (wt=17): 851 ((x v (y v z) ') ' v (z v (x v y)) ') ' = x. [para (11 (a 1) 37 (a 1 1))] given #164 (wt=17): 1294 (C v (C v (C ' v (C ' v (D v (C ' v (C v D ') ')) '))) ') ' = C '. [para (614 (a 1) 12 (a 1 1 2)) demod (19 11)] given #165 (wt=17): 1454 ((C v D ') ' v (C v (C v (C v ((C v D ') ' v (C v D ') ')))) ') ' = C. [para (344 (a 1) 12 (a 1 1 2)) demod (11)] given #166 (wt=33): 59 ((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 (22 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #167 (wt=17): 1571 ((D v C ') ' v (C v (D v (D v ((D v C ') ' v (D v C ') ')))) ') ' = D. [para (353 (a 1) 12 (a 1 1 2)) demod (19 11)] given #168 (wt=17): 1590 (C ' v (C v (C v (C ' v ((D v x) ' v (D v x ') ')))) ') ' = C. [para (611 (a 1) 12 (a 1 1 2)) demod (11)] given #169 (wt=17): 1833 (C ' v (C v (C v (C ' v ((x v D) ' v (D v x ') ')))) ') ' = C. [para (701 (a 1) 12 (a 1 1 2)) demod (11)] given #170 (wt=17): 1853 (C ' v (C v (C v (C ' v (C ' v (D v (D v (C ' v C '))) ')))) ') ' = C. [para (746 (a 1) 12 (a 1 1 2)) demod (11)] given #171 (wt=23): 61 ((x v (y v (z v u))) ' v (x v (u v (z v y) ')) ') ' = x v u. [para (36 (a 1) 22 (a 1 1 1 1 2))] given #172 (wt=17): 1873 (C ' v (C v (C v (C v (C ' v (C ' v (C ' v (D v C ') ')))))) ') ' = C. [para (775 (a 1) 12 (a 1 1 2)) demod (11)] given #173 (wt=17): 1893 (C ' v (D v (D v (D v (C ' v (C ' v (C ' v (C v D ') ')))))) ') ' = D. [para (940 (a 1) 12 (a 1 1 2)) demod (11)] given #174 (wt=17): 2782 ((C v (x v (C v (C ' v D ')) ')) ' v (C ' v x) ') ' = x. [para (30 (a 1) 135 (a 1 1 2 1 1))] given #175 (wt=17): 2800 ((D v (x v (D v (C ' v C ')) ')) ' v (C ' v x) ') ' = x. [para (102 (a 1) 135 (a 1 1 2 1 1))] given #176 (wt=19): 62 ((x v (y v z)) ' v (z v (y v x ')) ') ' = z v y. [para (36 (a 1) 22 (a 1 1 1 1))] given #177 (wt=17): 2917 (C v (C v ((C v D ') ' v (C v (C ' v D ')) ')) ') ' = (C v D ') '. [para (27 (a 1) 136 (a 1 1 2)) demod (19 11)] given #178 (wt=17): 2923 (D v (C v ((D v C ') ' v (C v (C ' v D ')) ')) ') ' = (D v C ') '. [para (89 (a 1) 136 (a 1 1 2)) demod (19 11)] given #179 (wt=17): 3213 (x v (D v (x v (C v (x v C ') '))) ') ' = (x v C ') '. [para (20 (a 1) 147 (a 1 1 2 1)) demod (11 19 10)] given #180 (wt=17): 3309 (C v (D v ((D v (C ' v C ')) ' v (C v D ') ')) ') ' = (C v D ') '. [para (27 (a 1) 156 (a 1 1 2)) demod (11 10 11)] given #181 (wt=19): 63 ((x v (y v z)) ' v (z ' v (y v x)) ') ' = x v y. [para (36 (a 1) 22 (a 1 1 2 1))] given #182 (wt=17): 3316 (D v (D v ((D v C ') ' v (D v (C ' v C ')) ')) ') ' = (D v C ') '. [para (89 (a 1) 156 (a 1 1 2)) demod (19 11)] given #183 (wt=17): 3404 (x v (D v (x v (C v (C ' v x) '))) ') ' = (C ' v x) '. [para (20 (a 1) 160 (a 1 1 2 1)) demod (11 19 10)] given #184 (wt=17): 3613 (C v (C v (C v (D v ((C v D ') ' v (C v D ') ')))) ') ' = (C v D ') '. [para (3400 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #185 (wt=17): 3640 (D v (C v (D v (D v ((D v C ') ' v (D v C ') ')))) ') ' = (D v C ') '. [para (3409 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #186 (wt=18): 64 ((C v (D v (x v y))) ' v (x v (y v C ')) ') ' = x v y. [para (10 (a 1) 28 (a 1 1 2 1)) demod (19 11)] given #187 (wt=13): 6619 (C v (D v (D v ((D v C ') ' v (D v C ') ')))) ' = C '. [para (3640 (a 1) 154 (a 1 1 2)) demod (11 10 11 5550) flip a] given #188 (wt=16): 6665 (C ' v (C v (D v (D v ((D v C ') ' v (D v C ') '))) ') ') ' = C. [para (6619 (a 1) 12 (a 1 1 1))] given #189 (wt=17): 3670 ((x v C ') ' v (x v (C v (D v (D v (D v C ') ')))) ') ' = x. [para (3666 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #190 (wt=17): 3674 (C ' v (D v (D v (C ' v (D v C ') '))) ') ' = D v (D v (D v C ') '). [para (3666 (a 1) 23 (a 1 1 1)) demod (11 19 19)] given #191 (wt=20): 67 ((x v y) ' v (x v ((y v (C v D)) ' v (y v C ') ')) ') ' = x. [para (28 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #192 (wt=8): 6810 (C v (D v (D v C ') ')) ' = C '. [para (89 (a 1) 67 (a 1 1 1)) demod (11 10 11 89 11 19 357)] given #193 (wt=10): 6899 (C ' v (C v (D v (D v C '))) ') ' = C v D. [para (6810 (a 1) 22 (a 1 1 2)) demod (11)] given #194 (wt=11): 6896 (C ' v (C v (D v (D v C ') ') ') ') ' = C. [para (6810 (a 1) 12 (a 1 1 1))] given #195 (wt=12): 6934 (C v (D v (C v (D v (D v (C ' v C ')))) ')) ' = C '. [para (6899 (a 1) 12 (a 1 1 2)) demod (19 19 19 11 10)] given #196 (wt=26): 70 ((x v (y v z)) ' v (x v (y v ((z v (C v D)) ' v (z v C ') '))) ') ' = x v y. [para (28 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #197 (wt=13): 6906 (C v (C v (C ' v (D v (D v C ') ') ')) ') ' = C '. [para (6810 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 6810)] given #198 (wt=14): 6797 (C v (C v (C ' v (C v (D v (C v D ') ')) ')) ') ' = C '. [para (27 (a 1) 67 (a 1 1 1)) demod (11 10 11 27 11 19)] given #199 (wt=14): 7004 (C ' v (C v (C v (D v (D v (D v (C ' v C ')))))) ') ' = C v D. [para (6934 (a 1) 22 (a 1 1 2)) demod (19 11)] given #200 (wt=14): 7068 (C ' v (C v (C v (C ' v (D v (D v C ') ') '))) ') ' = C. [para (6906 (a 1) 12 (a 1 1 2)) demod (11)] given #201 (wt=20): 71 ((x v C ') ' v (x v (C v (C v (C v (C ' v (C ' v D ')))) ')) ') ' = x. [para (35 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #202 (wt=15): 6913 (C ' v (C v (D ' v (D v C ') ')) ') ' = C v (D v C ') '. [para (6810 (a 1) 41 (a 1 1 1)) demod (11)] given #203 (wt=15): 6933 (C ' v (C v (C ' v (D v (C ' v (D v C ') ')) ')) ') ' = C. [para (6810 (a 1) 67 (a 1 1 1)) demod (11 19 10 19 3666 11 19)] given #204 (wt=15): 7003 (C ' v (C v (D v (C v (D v (D v (C ' v C ')))) ') ') ') ' = C. [para (6934 (a 1) 12 (a 1 1 1))] given #205 (wt=15): 7016 (C ' v (D v (C v (C v (D v (D v (C ' v C ')))) ') ') ') ' = D. [para (6934 (a 1) 31 (a 1 1 1))] given #206 (wt=26): 73 ((x v (y v C ')) ' v (x v (y v (C v (C v (C v (C ' v (C ' v D ')))) '))) ') ' = x v y. [para (35 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #207 (wt=15): 7099 (C ' v (C v (C v (C ' v (C v (D v (C v D ') ')) '))) ') ' = C. [para (6797 (a 1) 12 (a 1 1 2)) demod (11)] given #208 (wt=16): 6897 ((x v C ') ' v (x v (C v (D v (D v C ') '))) ') ' = x. [para (6810 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #209 (wt=16): 6900 ((C v (D v ((D v C ') ' v x))) ' v (x v C ') ') ' = x. [para (6810 (a 1) 23 (a 1 1 2 1 2)) demod (10 10)] given #210 (wt=16): 6901 ((x v (C v (D v (D v C ') '))) ' v (C ' v x) ') ' = x. [para (6810 (a 1) 24 (a 1 1 2 1 1))] given #211 (wt=20): 76 ((x v y) ' v (x v ((C v (D v y)) ' v (y v C ') ')) ') ' = x. [para (65 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #212 (wt=16): 6907 ((C ' v x) ' v (C v (D v ((D v C ') ' v x))) ') ' = x. [para (6810 (a 1) 84 (a 1 1 2 1 1)) demod (10 10 11)] given #213 (wt=16): 6908 ((x v C ') ' v (C v (D v ((D v C ') ' v x))) ') ' = x. [para (6810 (a 1) 85 (a 1 1 1 1 2)) demod (10 10)] given #214 (wt=16): 6909 ((x v C ') ' v (C v (x v (D v (D v C ') '))) ') ' = x. [para (6810 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #215 (wt=16): 6910 ((C ' v x) ' v (x v (C v (D v (D v C ') '))) ') ' = x. [para (6810 (a 1) 128 (a 1 1 1 1 1))] given #216 (wt=18): 78 ((C v (x v (D v y))) ' v (x v (y v C ')) ') ' = x v y. [para (19 (a 1) 65 (a 1 1 1 1 2)) demod (10)] given #217 (wt=16): 6924 ((C v (x v (D v (D v C ') '))) ' v (C ' v x) ') ' = x. [para (6810 (a 1) 135 (a 1 1 2 1 1))] given #218 (wt=16): 6929 ((C ' v x) ' v (C v (x v (D v (D v C ') '))) ') ' = x. [para (6810 (a 1) 549 (a 1 1 1 1 1))] given #219 (wt=16): 6938 (C v (D v (C v (C v (D v (D v C '))) ') ')) ' = (C v (D v (D v C '))) '. [para (6899 (a 1) 24 (a 1 1 2)) demod (11 11 10)] given #220 (wt=16): 7128 (C v (D v (C v (C v (D v (D v (D v (C ' v (C ' v C '))))))) ')) ' = C '. [para (7004 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 19 11 10)] given #221 (wt=18): 79 ((C v (x v (D v y))) ' v (y v (x v C ')) ') ' = y v x. [para (20 (a 1) 65 (a 1 1 1 1 2)) demod (10)] given #222 (wt=16): 7158 (C v (C v (C v (C ' v (C ' v (D v (D v C ') ') ')))) ') ' = C '. [para (7068 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #223 (wt=16): 7389 ((x v C ') ' v (C v (D v (x v (D v C ') '))) ') ' = x. [para (11 (a 1) 6900 (a 1 1 1 1 2 2)) demod (11)] given #224 (wt=16): 7430 (C v (C v (D v ((D v C ') ' v (C v D ') '))) ') ' = (C v D ') '. [para (27 (a 1) 6901 (a 1 1 2)) demod (11 10 10 11)] given #225 (wt=16): 7520 ((C ' v x) ' v (C v (D v (x v (D v C ') '))) ') ' = x. [para (11 (a 1) 6907 (a 1 1 2 1 2 2))] given #226 (wt=18): 80 ((C v (x v (y v D))) ' v (x v (y v C ')) ') ' = x v y. [para (20 (a 2) 65 (a 1 1 1 1 2)) demod (10)] given #227 (wt=16): 7644 ((C v (D v (x v (D v C ') '))) ' v (C ' v x) ') ' = x. [para (19 (a 1) 6924 (a 1 1 1 1 2))] given #228 (wt=17): 3675 ((C v (D v (D v ((D v C ') ' v x)))) ' v (x v C ') ') ' = x. [para (3666 (a 1) 23 (a 1 1 2 1 2)) demod (10 10 10)] given #229 (wt=17): 3676 ((x v (C v (D v (D v (D v C ') ')))) ' v (C ' v x) ') ' = x. [para (3666 (a 1) 24 (a 1 1 2 1 1))] given #230 (wt=17): 3682 ((C ' v x) ' v (C v (D v (D v ((D v C ') ' v x)))) ') ' = x. [para (3666 (a 1) 84 (a 1 1 2 1 1)) demod (10 10 10 11)] given #231 (wt=18): 81 ((C v (D v (x v y))) ' v (y v (x v C ')) ') ' = y v x. [para (21 (a 1) 65 (a 1 1 1 1 2)) demod (10)] given #232 (wt=17): 3683 ((x v C ') ' v (C v (D v (D v ((D v C ') ' v x)))) ') ' = x. [para (3666 (a 1) 85 (a 1 1 1 1 2)) demod (10 10 10)] given #233 (wt=17): 3684 ((x v C ') ' v (C v (x v (D v (D v (D v C ') ')))) ') ' = x. [para (3666 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #234 (wt=17): 3685 ((C ' v x) ' v (x v (C v (D v (D v (D v C ') ')))) ') ' = x. [para (3666 (a 1) 128 (a 1 1 1 1 1))] given #235 (wt=17): 3689 (C ' v (C v (D v (D ' v (D v C ') '))) ') ' = C v (D v (D v C ') '). [para (3666 (a 1) 41 (a 1 1 1)) demod (11 19)] given #236 (wt=26): 82 ((x v (y v z)) ' v (x v (y v ((C v (D v z)) ' v (z v C ') '))) ') ' = x v y. [para (65 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #237 (wt=17): 3696 (D v ((D v C ') ' v (D v (C ' v (C ' v (D v C ') '))) ')) ' = C '. [para (3666 (a 1) 77 (a 1 1 2 1 2 2)) demod (11 19 10 10 3666)] given #238 (wt=17): 3702 ((C v (x v (D v (D v (D v C ') ')))) ' v (C ' v x) ') ' = x. [para (3666 (a 1) 135 (a 1 1 2 1 1))] given #239 (wt=17): 3967 (C ' v (C v (D v (D v (C v (D v (D v (D v (C ' v C '))))) ')) ') ') ' = C. [para (3879 (a 1) 12 (a 1 1 1))] given #240 (wt=17): 3980 (C ' v (D v (C v (D v (C v (D v (D v (D v (C ' v C '))))) ')) ') ') ' = D. [para (3879 (a 1) 31 (a 1 1 1))] given #241 (wt=18): 83 ((C v (x v (y v D))) ' v (y v (x v C ')) ') ' = y v x. [para (36 (a 1) 65 (a 1 1 1 1 2)) demod (10)] given #242 (wt=17): 3986 (C ' v (C v (C v (D v (D v (D v (D v (D v (C ' v C ')))))))) ') ' = C v (D v D). [para (3879 (a 1) 40 (a 1 1 2)) demod (19 19 11)] given #243 (wt=17): 4074 (C ' v (C v (C v (D v (D v (C ' v (D v (D v C ') ') '))))) ') ' = C v D. [para (3698 (a 1) 22 (a 1 1 2)) demod (19 11)] given #244 (wt=17): 4108 (C v (C v (C v (C ' v (C ' v (D v (D v (D v C ') ')) ')))) ') ' = C '. [para (3940 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #245 (wt=17): 4412 ((C ' v x) ' v (C v (x v (C v (C ' v D ')) ')) ') ' = x. [para (11 (a 1) 408 (a 1 1 2 1 2))] given #246 (wt=21): 86 ((x v y) ' v (x v ((z v y) ' v (y v z ') ')) ') ' = x. [para (23 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #247 (wt=17): 4445 ((C ' v x) ' v (D v (x v (D v (C ' v C ')) ')) ') ' = x. [para (11 (a 1) 421 (a 1 1 2 1 2))] given #248 (wt=17): 5084 ((C ' v x) ' v (C v (x v (D v (D v (D v C ') ')))) ') ' = x. [para (3666 (a 1) 549 (a 1 1 1 1 1))] given #249 (wt=17): 6667 (C ' v (C v (D v (D v ((D v C ') ' v (D v C ') ')) ')) ') ' = C v D. [para (6619 (a 1) 22 (a 1 1 1))] given #250 (wt=17): 6800 (C v (C v (C ' v (C v (D v (C v (C v (C ' v D '))) ')) ')) ') ' = C '. [para (33 (a 1) 67 (a 1 1 1)) demod (11 10 11 33 11 19)] given #251 (wt=18): 87 (x v (x v (y ' v (y v x) ')) ') ' = (y v x) '. [para (23 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #252 (wt=17): 6812 (D v (D v (C ' v (C v (D v (D v (D v (C ' v C '))) ')) ')) ') ' = C '. [para (106 (a 1) 67 (a 1 1 1)) demod (11 10 11 106 11 19)] given #253 (wt=17): 6936 (C v (D v (C v (D v (C v (D v (D v C '))) ')) ')) ' = (C v (D v (D v C '))) '. [para (6899 (a 1) 66 (a 1 1 2)) demod (11 10 11 10)] given #254 (wt=17): 7013 (C v (C v (C ' v (D v (C v (D v (D v (C ' v C ')))) ') ')) ') ' = C '. [para (6934 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 6934)] given #255 (wt=17): 7063 (C ' v (C v (D v (C ' v (D v (C ' v (D v C ') ')) '))) ') ' = C v D. [para (3666 (a 1) 70 (a 1 1 1)) demod (11 19 10 19 3666 11 19)] given #256 (wt=21): 88 (((x v y) ' v ((x v y ') ' v z)) ' v (z v x) ') ' = z. [para (12 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #257 (wt=17): 7204 (C v ((D v C ') ' v (C v (C ' v (D ' v (D v C ') '))) ')) ' = C '. [para (6913 (a 1) 12 (a 1 1 2)) demod (19 11 10)] given #258 (wt=17): 7237 (C v (C v (C ' v (C ' v (D v (C ' v (D v C ') ')) '))) ') ' = C '. [para (6933 (a 1) 12 (a 1 1 2)) demod (19 11)] given #259 (wt=17): 7294 (D v (D v (C ' v (C v (C v (D v (D v (C ' v C ')))) ') ')) ') ' = C '. [para (7016 (a 1) 12 (a 1 1 2)) demod (19 11)] given #260 (wt=17): 7333 (C v (C v (C v (C ' v (C ' v (C v (D v (C v D ') ')) ')))) ') ' = C '. [para (7099 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #261 (wt=18): 93 ((C ' v ((C v (C v (C ' v D '))) ' v x)) ' v (x v C) ') ' = x. [para (33 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #262 (wt=17): 7785 (C ' v (C v (C v (C v (C ' v (C ' v (D v (D v C ') ') '))))) ') ' = C. [para (7158 (a 1) 12 (a 1 1 2)) demod (11)] given #263 (wt=17): 7836 ((C v D ') ' v (C v (C v (D v ((D v C ') ' v (C v D ') ')))) ') ' = C. [para (7430 (a 1) 12 (a 1 1 2)) demod (11)] given #264 (wt=17): 7929 ((x v C ') ' v (C v (D v (D v (x v (D v C ') ')))) ') ' = x. [para (11 (a 1) 3675 (a 1 1 1 1 2 2 2)) demod (11)] given #265 (wt=17): 7934 ((x v C ') ' v (C v (D v (x v (D v (D v C ') ')))) ') ' = x. [para (20 (a 1) 3675 (a 1 1 1 1 2 2)) demod (11)] given #266 (wt=27): 94 ((x v (y v z)) ' v (x v (y v ((u v z) ' v (z v u ') '))) ') ' = x v y. [para (23 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #267 (wt=17): 7956 (C v (C v (D v (D v ((D v C ') ' v (C v D ') ')))) ') ' = (C v D ') '. [para (27 (a 1) 3676 (a 1 1 2)) demod (11 10 10 10 11)] given #268 (wt=17): 7992 ((C ' v x) ' v (C v (D v (D v (x v (D v C ') ')))) ') ' = x. [para (11 (a 1) 3682 (a 1 1 2 1 2 2 2))] given #269 (wt=17): 7998 ((C ' v x) ' v (C v (D v (x v (D v (D v C ') ')))) ') ' = x. [para (20 (a 1) 3682 (a 1 1 2 1 2 2))] given #270 (wt=17): 8117 ((C v (D v (x v (D v (D v C ') ')))) ' v (C ' v x) ') ' = x. [para (19 (a 1) 3702 (a 1 1 1 1 2))] given #271 (wt=27): 95 (((x v (y v z)) ' v ((x v (y v z ')) ' v u)) ' v (u v (x v y)) ') ' = u. [para (22 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #272 (wt=17): 8825 ((C v (D v (D v (x v (D v C ') ')))) ' v (C ' v x) ') ' = x. [para (11 (a 1) 7992 (a 1 1))] given #273 (wt=18): 110 ((x v D) ' v (x v (C ' v (D v (D v (C ' v C '))) ')) ') ' = x. [para (106 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #274 (wt=18): 113 ((C ' v ((D v (D v (C ' v C '))) ' v x)) ' v (x v D) ') ' = x. [para (106 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #275 (wt=18): 114 ((x v (y v (C v D))) ' v (C ' v (x v y)) ') ' = x v y. [para (10 (a 1) 66 (a 1 1 1 1))] given #276 (wt=20): 96 (((x v (C v D)) ' v ((x v C ') ' v y)) ' v (y v x) ') ' = y. [para (28 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #277 (wt=18): 120 ((C v (D v (x v y))) ' v (x v (C ' v y)) ') ' = x v y. [para (19 (a 1) 66 (a 1 1 2 1)) demod (19 11)] given #278 (wt=18): 121 (C v (C v (D v (C v (C v (C ' v D '))) ')) ') ' = (C v (C v (C ' v D '))) '. [para (33 (a 1) 66 (a 1 1 2)) demod (11 10 11)] given #279 (wt=18): 122 ((C v (D v (x v y))) ' v (y v (C ' v x)) ') ' = x v y. [para (20 (a 1) 66 (a 1 1 2 1)) demod (19 11)] given #280 (wt=18): 123 ((C v (D v (x v y))) ' v (C ' v (y v x)) ') ' = x v y. [para (21 (a 1) 66 (a 1 1 2 1)) demod (19 11)] given #281 (wt=23): 97 (C ' v (C ' v (C v (C v (C ' v (C ' v D ')))) ') ') ' = (C v (C v (C ' v (C ' v D ')))) '. [para (35 (a 1) 23 (a 1 1 1)) demod (11)] given #282 (wt=18): 127 (D v (C v (D v (D v (D v (C ' v C '))) ')) ') ' = (D v (D v (C ' v C '))) '. [para (106 (a 1) 66 (a 1 1 2)) demod (11 10 11)] given #283 (wt=18): 130 (x v (y ' v (x v (x v y) ')) ') ' = (x v y) '. [para (24 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #284 (wt=18): 137 ((x v (C ' v (C v (C v (C ' v D '))) ')) ' v (C v x) ') ' = x. [para (33 (a 1) 24 (a 1 1 2 1 1))] given #285 (wt=14): 9088 (C ' v (D v (C ' v (C v (C v (C ' v D '))) ')) ') ' = D. [para (13 (a 1) 137 (a 1 1 2)) demod (11)] given #286 (wt=20): 98 ((C v ((C v (C v (C ' v (C ' v D ')))) ' v x)) ' v (x v C ') ') ' = x. [para (35 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #287 (wt=16): 9115 (D v (D v (C ' v (C ' v (C v (C v (C ' v D '))) '))) ') ' = C '. [para (9088 (a 1) 12 (a 1 1 2)) demod (19 11)] given #288 (wt=17): 9161 (C ' v (D v (D v (C ' v (C ' v (C v (C v (C ' v D '))) ')))) ') ' = D. [para (9115 (a 1) 12 (a 1 1 2)) demod (11)] given #289 (wt=18): 157 ((x v (C ' v (D v (D v (C ' v C '))) ')) ' v (D v x) ') ' = x. [para (106 (a 1) 24 (a 1 1 2 1 1))] given #290 (wt=18): 184 ((C v (x v (D v y))) ' v (C ' v (x v y)) ') ' = x v y. [para (19 (a 1) 74 (a 1 1 1 1 2))] given #291 (wt=20): 99 (((C v (D v x)) ' v ((x v C ') ' v y)) ' v (y v x) ') ' = y. [para (65 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #292 (wt=18): 185 ((C v (x v (D v y))) ' v (C ' v (y v x)) ') ' = y v x. [para (20 (a 1) 74 (a 1 1 1 1 2))] given #293 (wt=18): 186 ((C v (x v (y v D))) ' v (C ' v (x v y)) ') ' = x v y. [para (20 (a 2) 74 (a 1 1 1 1 2))] given #294 (wt=18): 188 ((C v (x v (y v D))) ' v (C ' v (y v x)) ') ' = y v x. [para (36 (a 1) 74 (a 1 1 1 1 2))] given #295 (wt=18): 264 ((x v (y v C ')) ' v (C v (D v (x v y))) ') ' = x v y. [para (10 (a 1) 75 (a 1 1 1 1))] given #296 (wt=21): 100 (((x v y) ' v ((y v x ') ' v z)) ' v (z v y) ') ' = z. [para (23 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #297 (wt=18): 266 ((x v (y v C ')) ' v (C v (x v (D v y))) ') ' = x v y. [para (19 (a 1) 75 (a 1 1 2 1 2)) demod (10)] given #298 (wt=18): 267 ((x v (y v C ')) ' v (C v (y v (D v x))) ') ' = x v y. [para (20 (a 1) 75 (a 1 1 2 1 2)) demod (10)] given #299 (wt=18): 268 ((x v (y v C ')) ' v (C v (x v (y v D))) ') ' = x v y. [para (20 (a 2) 75 (a 1 1 2 1 2)) demod (10)] given #300 (wt=18): 269 ((x v (y v C ')) ' v (C v (D v (y v x))) ') ' = x v y. [para (21 (a 1) 75 (a 1 1 2 1 2)) demod (10)] given #301 (wt=21): 103 ((x v (y v D)) ' v (x v (y v (C ' v (D v C ') '))) ') ' = x v y. [para (89 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #302 (wt=18): 271 ((x v (y v C ')) ' v (C v (y v (x v D))) ') ' = x v y. [para (36 (a 1) 75 (a 1 1 2 1 2)) demod (10)] given #303 (wt=18): 285 ((C ' v (x v y)) ' v (x v (y v (C v D))) ') ' = x v y. [para (10 (a 1) 115 (a 1 1 2 1))] given #304 (wt=18): 287 ((x v (C ' v y)) ' v (C v (D v (x v y))) ') ' = x v y. [para (19 (a 1) 115 (a 1 1 1 1)) demod (19 11)] given #305 (wt=18): 289 ((x v (C ' v y)) ' v (C v (D v (y v x))) ') ' = y v x. [para (20 (a 1) 115 (a 1 1 1 1)) demod (19 11)] given #306 (wt=23): 107 ((x v (y v C ')) ' v (x v (y v (D v (D v (C ' v C ')) '))) ') ' = x v y. [para (102 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #307 (wt=18): 290 ((C ' v (x v y)) ' v (C v (D v (y v x))) ') ' = y v x. [para (21 (a 1) 115 (a 1 1 1 1)) demod (19 11)] given #308 (wt=18): 383 ((C ' v (x v y)) ' v (C v (x v (y v D))) ') ' = x v y. [para (10 (a 1) 288 (a 1 1 2 1 2))] given #309 (wt=18): 403 (x v (y ' v (x v (y v x) ')) ') ' = (y v x) '. [para (84 (a 1) 12 (a 1 1 2)) demod (11 10 11)] given #310 (wt=18): 409 ((C v x) ' v (C ' v ((C v (C v (C ' v D '))) ' v x)) ') ' = x. [para (33 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #311 (wt=24): 112 ((x v (y v D)) ' v (x v (y v (C ' v (D v (D v (C ' v C '))) '))) ') ' = x v y. [para (106 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #312 (wt=18): 422 ((D v x) ' v (C ' v ((D v (D v (C ' v C '))) ' v x)) ') ' = x. [para (106 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #313 (wt=18): 453 ((x v C) ' v (C ' v ((C v (C v (C ' v D '))) ' v x)) ') ' = x. [para (33 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #314 (wt=18): 466 ((x v D) ' v (C ' v ((D v (D v (C ' v C '))) ' v x)) ') ' = x. [para (106 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #315 (wt=18): 499 ((x v C) ' v (C ' v (x v (C v (C v (C ' v D '))) ')) ') ' = x. [para (33 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #316 (wt=20): 116 ((x v y) ' v (x v ((y v (C v D)) ' v (C ' v y) ')) ') ' = x. [para (66 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #317 (wt=18): 516 ((x v D) ' v (C ' v (x v (D v (D v (C ' v C '))) ')) ') ' = x. [para (106 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #318 (wt=18): 551 ((C v x) ' v (x v (C ' v (C v (C v (C ' v D '))) ')) ') ' = x. [para (33 (a 1) 128 (a 1 1 1 1 1))] given #319 (wt=18): 564 ((D v x) ' v (x v (C ' v (D v (D v (C ' v C '))) ')) ') ' = x. [para (106 (a 1) 128 (a 1 1 1 1 1))] given #320 (wt=18): 615 (C ' v (C v ((x v (D v y)) ' v (D v (x v y) ') ')) ') ' = C. [para (19 (a 1) 198 (a 1 1 2 1 2 1 1))] given #321 (wt=26): 124 ((x v (y v z)) ' v (x v (y v ((z v (C v D)) ' v (C ' v z) '))) ') ' = x v y. [para (66 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #322 (wt=18): 616 (C ' v (C v ((D v C ') ' v (C v (D v (C v (C ' v D ')) ')) ')) ') ' = C. [para (30 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (19 11)] given #323 (wt=18): 617 (C ' v (C v (C ' v (D v (C ' v (C v (C v (C ' v D '))) ')) ')) ') ' = C. [para (33 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11 13 11)] given #324 (wt=18): 618 (C ' v (C v ((x v (D v y)) ' v (D v (y v x) ') ')) ') ' = C. [para (20 (a 1) 198 (a 1 1 2 1 2 1 1))] given #325 (wt=18): 619 (C ' v (C v ((x v (y v D)) ' v (D v (x v y) ') ')) ') ' = C. [para (20 (a 2) 198 (a 1 1 2 1 2 1 1))] given #326 (wt=20): 125 (((x v (C v D)) ' v ((C ' v x) ' v y)) ' v (y v x) ') ' = y. [para (66 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #327 (wt=18): 620 (C ' v (C v ((D v (x v y)) ' v (D v (y v x) ') ')) ') ' = C. [para (21 (a 1) 198 (a 1 1 2 1 2 1 1))] given #328 (wt=18): 623 (C ' v (C v ((x v (y v D)) ' v (D v (y v x) ') ')) ') ' = C. [para (36 (a 1) 198 (a 1 1 2 1 2 1 1))] given #329 (wt=18): 630 (C ' v (C v ((D v C ') ' v (D v (D v (D v (C ' v C ')) ')) ')) ') ' = C. [para (102 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11)] given #330 (wt=18): 939 (C ' v (C v (C ' v (D v (D v (C ' v (C ' v (C v D ') ')))) ')) ') ' = C. [para (911 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #331 (wt=21): 129 ((x v y) ' v (x v ((y v z) ' v (z ' v y) ')) ') ' = x. [para (24 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #332 (wt=18): 1314 ((x v (C v (D v y))) ' v (x v (y v C ')) ') ' = x v y. [para (13 (a 1) 41 (a 1 1 2 1 2 2)) demod (10)] given #333 (wt=18): 1475 ((x v (C v (D v y))) ' v (y v (x v C ')) ') ' = y v x. [para (13 (a 1) 42 (a 1 1 2 1 2 2)) demod (10)] given #334 (wt=18): 1607 (C v (C v (C ' v ((D v D) ' v (D v (C ' v (D v C ') ')) '))) ') ' = C '. [para (89 (a 1) 611 (a 1 1 2 1 2 2 2 1 2)) demod (11)] given #335 (wt=18): 1732 ((x v (y v (C v D))) ' v (x v (C ' v y)) ') ' = x v y. [para (13 (a 1) 43 (a 1 1 2 1 2 1))] given #336 (wt=21): 131 ((x v ((y v z) ' v (y v z ') ')) ' v (y v x) ') ' = x. [para (12 (a 1) 24 (a 1 1 2 1 1))] given #337 (wt=14): 9887 (C ' v (D v ((C v x) ' v (C v x ') ')) ') ' = D. [para (13 (a 1) 131 (a 1 1 2)) demod (11)] given #338 (wt=13): 9981 (C ' v (D v ((C v (C v D)) ' v (C v C ') ')) ') ' = D. [para (13 (a 1) 9887 (a 1 1 2 1 2 2 1 2))] given #339 (wt=14): 9977 (C ' v (D v ((x v C) ' v (C v x ') ')) ') ' = D. [para (11 (a 1) 9887 (a 1 1 2 1 2 1 1))] given #340 (wt=15): 9996 (C ' v (D v (C ' v (C v (C ' v (D v C ') ')) ')) ') ' = D. [para (89 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (13 11)] given #341 (wt=19): 132 (x v (x v (y v (x v y ') ')) ') ' = (x v y ') '. [para (12 (a 1) 24 (a 1 1 2)) demod (11 10 11)] low water: id=5423, wt=44 low water: id=5539, wt=43 low water: id=5535, wt=42 low water: id=5594, wt=41 given #342 (wt=15): 10176 (C ' v (D v (C ' v (C v (D v (D v C ') ') ') ')) ') ' = D. [para (6810 (a 1) 9887 (a 1 1 2 1 2 1))] given #343 (wt=15): 10323 (D v (D v (C ' v ((C v (C v D)) ' v (C v C ') '))) ') ' = C '. [para (9981 (a 1) 12 (a 1 1 2)) demod (19 11)] low water: id=5531, wt=40 given #344 (wt=16): 9979 (D v (D v (C ' v ((C v x) ' v (C v x ') '))) ') ' = C '. [para (9887 (a 1) 12 (a 1 1 2)) demod (19 11)] low water: id=5963, wt=39 low water: id=6212, wt=38 low water: id=6509, wt=37 low water: id=5734, wt=36 low water: id=6726, wt=35 low water: id=7033, wt=34 low water: id=7127, wt=33 given #345 (wt=16): 9982 (C ' v (D v ((C v C) ' v (C v (C ' v (C v D ') ')) ')) ') ' = D. [para (27 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #346 (wt=27): 142 ((x v (y v z)) ' v (x v (y v ((z v u) ' v (u ' v z) '))) ') ' = x v y. [para (24 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #347 (wt=16): 10004 (C ' v (D v ((C v D ') ' v (C v (C v (C v D ') ')) ')) ') ' = D. [para (134 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #348 (wt=16): 10112 (C ' v (D v (C ' v (C v (D v (D v (D v C ') ')) ') ')) ') ' = D. [para (3666 (a 1) 9887 (a 1 1 2 1 2 1))] given #349 (wt=16): 10342 (D v (D v (C ' v ((x v C) ' v (C v x ') '))) ') ' = C '. [para (9977 (a 1) 12 (a 1 1 2)) demod (19 11)] given #350 (wt=16): 10535 (C ' v (D v (D v (C ' v ((C v (C v D)) ' v (C v C ') ')))) ') ' = D. [para (9981 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 9981)] given #351 (wt=27): 143 ((x v ((y v (z v u)) ' v (y v (z v u ')) ')) ' v (y v (z v x)) ') ' = x. [para (22 (a 1) 24 (a 1 1 2 1 1)) demod (10)] given #352 (wt=17): 9992 (C ' v (D v (C ' v (C v (C v (C v (C ' v (C ' v D '))))) ')) ') ' = D. [para (35 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #353 (wt=17): 10177 (C ' v (D v ((C v C ') ' v (C v (C v (D v (D v C ') '))) ')) ') ' = D. [para (6810 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #354 (wt=17): 10361 (D v (D v (C ' v (C ' v (C v (C ' v (D v C ') ')) '))) ') ' = C '. [para (9996 (a 1) 12 (a 1 1 2)) demod (19 11)] given #355 (wt=17): 10533 (C ' v (D v (D v (C ' v ((C v x) ' v (C v x ') ')))) ') ' = D. [para (9887 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 9887)] low water: id=7578, wt=32 low water: id=7800, wt=31 given #356 (wt=27): 144 (x v (y v (x v (y v (z v (x v (y v z ')) '))) ')) ' = (x v (y v z ')) '. [para (22 (a 1) 24 (a 1 1 2)) demod (11 10 10 11 10)] given #357 (wt=17): 10537 (C ' v (D v (D v (C ' v ((x v C) ' v (C v x ') ')))) ') ' = D. [para (9977 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 9977)] given #358 (wt=17): 10540 (D v (D v (C ' v (C ' v (C v (D v (D v C ') ') ') '))) ') ' = C '. [para (10176 (a 1) 12 (a 1 1 2)) demod (19 11)] given #359 (wt=18): 1917 ((x v (y v (C v D))) ' v (y v (C ' v x)) ') ' = x v y. [para (13 (a 1) 44 (a 1 1 2 1 2 1))] given #360 (wt=18): 2027 (C v (C v (C v (C v (C v (C ' v (C ' v (C ' v (C ' v D ')))))))) ') ' = C '. [para (1080 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 11)] given #361 (wt=20): 146 ((x v ((y v (C v D)) ' v (y v C ') ')) ' v (y v x) ') ' = x. [para (28 (a 1) 24 (a 1 1 2 1 1))] given #362 (wt=18): 2048 (D v (D v (D v (D v (D v (C ' v (C ' v (C ' v (C ' v C ')))))))) ') ' = C '. [para (1276 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 11)] given #363 (wt=18): 2069 (C v (C v (C v (C ' v (C ' v ((C v (D v D)) ' v (D v C ') '))))) ') ' = C '. [para (1399 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #364 (wt=18): 2269 (C ' v (C v ((C v (D v D)) ' v (D v (D v (C ' v (C v (D v D)) '))) ')) ') ' = C. [para (68 (a 1) 198 (a 1 1 2 1 2 2)) demod (19 19 11)] given #365 (wt=18): 2783 ((C v x) ' v (C ' v (x v (C v (C v (C ' v D '))) ')) ') ' = x. [para (33 (a 1) 135 (a 1 1 2 1 1)) demod (11)] given #366 (wt=20): 148 ((x v (C v (C v (C v (C ' v (C ' v D ')))) ')) ' v (C ' v x) ') ' = x. [para (35 (a 1) 24 (a 1 1 2 1 1))] given #367 (wt=18): 2801 ((D v x) ' v (C ' v (x v (D v (D v (C ' v C '))) ')) ') ' = x. [para (106 (a 1) 135 (a 1 1 2 1 1)) demod (11)] given #368 (wt=18): 2971 ((C v (C v (C ' v D '))) ' v (C v (C v (C v (C v (C ' v D '))) ')) ') ' = C. [para (138 (a 1) 12 (a 1 1 2)) demod (11)] given #369 (wt=18): 3062 ((x v (C v (y v D))) ' v (x v (y v C ')) ') ' = x v y. [para (19 (a 1) 48 (a 1 1 1 1 2))] given #370 (wt=18): 3063 ((x v (y v (C v D))) ' v (y v (x v C ')) ') ' = y v x. [para (19 (a 1) 48 (a 1 1 1 1))] given #371 (wt=20): 149 ((x v ((C v (D v y)) ' v (y v C ') ')) ' v (y v x) ') ' = x. [para (65 (a 1) 24 (a 1 1 2 1 1))] given #372 (wt=18): 3065 ((x v (y v (C v D))) ' v (C ' v (y v x)) ') ' = x v y. [para (36 (a 1) 48 (a 1 1 2 1))] given #373 (wt=18): 3229 (C ' v (C v ((D v C ') ' v (C v (D v (D v (D v (D v C ') ')))) ')) ') ' = C. [para (147 (a 1) 198 (a 1 1 2 1 2 2)) demod (19 19 11)] given #374 (wt=18): 3369 ((D v (D v (C ' v C '))) ' v (C v (D v (D v (D v (C ' v C '))) ')) ') ' = D. [para (158 (a 1) 12 (a 1 1 2)) demod (19 11)] given #375 (wt=10): 11023 (D v (D v (C ' v C '))) ' = (D v C ') '. [back_demod 127 demod (11010) flip a] given #376 (wt=21): 151 (((x v y) ' v ((y ' v x) ' v z)) ' v (z v x) ') ' = z. [para (24 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #377 (wt=14): 11025 ((D v C ') ' v (D v (D v (C ' v C ') ')) ') ' = D v D. [para (11023 (a 1) 22 (a 1 1 1))] given #378 (wt=14): 11039 ((D v C ') ' v (C v (D v (D v C '))) ') ' = D v (D v C '). [para (11023 (a 1) 40 (a 1 1 2)) demod (11 19 19 11)] given #379 (wt=15): 11049 ((D v C ') ' v (D v (C ' v (D v C ') ')) ') ' = D v C '. [para (11023 (a 1) 50 (a 1 1 1))] given #380 (wt=16): 11037 ((D v C ') ' v (C ' v (C ' v (D v D) ')) ') ' = C ' v C '. [para (11023 (a 1) 38 (a 1 1 1)) demod (10)] given #381 (wt=21): 152 ((x v ((y v z) ' v (z v y ') ')) ' v (z v x) ') ' = x. [para (23 (a 1) 24 (a 1 1 2 1 1))] given #382 (wt=17): 11027 ((D v C ') ' v (D v (C ' v (C ' v D '))) ') ' = D v (C ' v C '). [para (11023 (a 1) 23 (a 1 1 1)) demod (10 10)] given #383 (wt=18): 3968 (C ' v (C v (D v (D v (C v (D v (D v (D v (C ' v C '))))) ') ')) ') ' = C v D. [para (3879 (a 1) 22 (a 1 1 1))] given #384 (wt=18): 4073 (C ' v (C v (D v (C v (D v (C ' v (D v (D v C ') ') '))) ') ') ') ' = C. [para (3698 (a 1) 12 (a 1 1 1))] given #385 (wt=18): 4086 (C ' v (D v (C v (C v (D v (C ' v (D v (D v C ') ') '))) ') ') ') ' = D. [para (3698 (a 1) 31 (a 1 1 1))] given #386 (wt=19): 153 (x v (y v (x v (x v y ') ')) ') ' = (x v y ') '. [para (23 (a 1) 24 (a 1 1 2)) demod (11 10 11)] given #387 (wt=18): 5167 (C v ((D v C ') ' v (C v (C ' v ((D v D) ' v (D v C ') '))) ')) ' = C '. [para (5159 (a 1) 12 (a 1 1 2)) demod (19 11 10)] given #388 (wt=18): 5387 (C ' v (C v (C v (C ' v (C ' v (D v (C ' v (C v D ') ')) ')))) ') ' = C. [para (1294 (a 1) 12 (a 1 1 2)) demod (11)] given #389 (wt=18): 6207 ((C v D ') ' v (C v (C v ((C v D ') ' v (C v (C ' v D ')) '))) ') ' = C. [para (2917 (a 1) 12 (a 1 1 2)) demod (11)] given #390 (wt=18): 6236 ((D v C ') ' v (C v (D v ((D v C ') ' v (C v (C ' v D ')) '))) ') ' = D. [para (2923 (a 1) 12 (a 1 1 2)) demod (19 11)] given #391 (wt=20): 159 ((x v ((y v (C v D)) ' v (C ' v y) ')) ' v (y v x) ') ' = x. [para (66 (a 1) 24 (a 1 1 2 1 1))] given #392 (wt=18): 6296 ((C v D ') ' v (C v (D v ((D v (C ' v C ')) ' v (C v D ') '))) ') ' = C. [para (3309 (a 1) 12 (a 1 1 2)) demod (11)] given #393 (wt=18): 6522 ((D v C ') ' v (D v (D v ((D v C ') ' v (D v (C ' v C ')) '))) ') ' = D. [para (3316 (a 1) 12 (a 1 1 2)) demod (11)] given #394 (wt=18): 6580 ((C v D ') ' v (C v (C v (C v (D v ((C v D ') ' v (C v D ') '))))) ') ' = C. [para (3613 (a 1) 12 (a 1 1 2)) demod (11)] given #395 (wt=18): 6677 (C v (C v (C ' v (D v (D v ((D v C ') ' v (D v C ') '))) ')) ') ' = C '. [para (6619 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 6619)] given #396 (wt=21): 161 ((x v ((y v z) ' v (z ' v y) ')) ' v (y v x) ') ' = x. [para (24 (a 1) 24 (a 1 1 2 1 1))] given #397 (wt=18): 6683 (C ' v (C v (D v (D v ((D v C ') ' v (D v C ') ') '))) ') ' = C v (D v D). [para (6619 (a 1) 40 (a 1 1 1))] given #398 (wt=18): 6842 (C v (C v (C ' v (C v (D v (C v (C ' v (D v C ') ')) ')) ')) ') ' = C '. [para (702 (a 1) 67 (a 1 1 1)) demod (11 10 11 702 11 19)] given #399 (wt=18): 6847 (D v (D v (C ' v (C v (D v (D v (C ' v (C v D ') ')) ')) ')) ') ' = C '. [para (886 (a 1) 67 (a 1 1 1)) demod (11 10 11 886 11 19)] given #400 (wt=18): 6919 ((x v (C v D)) ' v (x v (C ' v (C v (D v (D v C '))) ')) ') ' = x. [para (6810 (a 1) 45 (a 1 1 2 1 2 2)) demod (11)] given #401 (wt=19): 162 (x v (x v (y v (y ' v x) ')) ') ' = (y ' v x) '. [para (24 (a 1) 24 (a 1 1 2)) demod (11 10 11)] given #402 (wt=18): 6935 ((C ' v ((C v (D v (D v C '))) ' v x)) ' v (x v (C v D)) ') ' = x. [para (6899 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #403 (wt=18): 6937 ((x v (C ' v (C v (D v (D v C '))) ')) ' v (C v (D v x)) ') ' = x. [para (6899 (a 1) 24 (a 1 1 2 1 1)) demod (10)] given #404 (wt=18): 6943 ((C v (D v x)) ' v (C ' v ((C v (D v (D v C '))) ' v x)) ') ' = x. [para (6899 (a 1) 84 (a 1 1 2 1 1)) demod (10 10 11)] given #405 (wt=18): 6944 ((x v (C v D)) ' v (C ' v ((C v (D v (D v C '))) ' v x)) ') ' = x. [para (6899 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #406 (wt=19): 163 ((x v (C v D ') ') ' v (x v (C v (C v (C v D ') ') ')) ') ' = x. [para (134 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #407 (wt=13): 11349 (C v (C v (C ' v (C v (C v D ') ') ')) ') ' = C '. [para (12 (a 1) 163 (a 1 1 1)) demod (13 19 13)] given #408 (wt=14): 11352 (C ' v (C v (C v (C ' v (C v (C v D ') ') '))) ') ' = C. [para (11349 (a 1) 12 (a 1 1 2)) demod (11)] given #409 (wt=16): 11370 (C v (C v (C v (C ' v (C ' v (C v (C v D ') ') ')))) ') ' = C '. [para (11349 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 11349)] given #410 (wt=17): 11389 (C ' v (C v (C v (C v (C ' v (C ' v (C v (C v D ') ') '))))) ') ' = C. [para (11352 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 11352)] given #411 (wt=25): 165 ((x v (y v (C v D ') ')) ' v (x v (y v (C v (C v (C v D ') ') '))) ') ' = x v y. [para (134 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #412 (wt=18): 6945 ((x v (C v D)) ' v (C ' v (x v (C v (D v (D v C '))) ')) ') ' = x. [para (6899 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #413 (wt=18): 6946 ((C v (D v x)) ' v (x v (C ' v (C v (D v (D v C '))) ')) ') ' = x. [para (6899 (a 1) 128 (a 1 1 1 1 1)) demod (10)] given #414 (wt=18): 6957 ((C v (D v x)) ' v (C ' v (x v (C v (D v (D v C '))) ')) ') ' = x. [para (6899 (a 1) 135 (a 1 1 2 1 1)) demod (10 11)] given #415 (wt=18): 6968 (C v (D v (C v (D v (C ' v (C v (D v (C v (D v (D v C '))) ')) '))) ')) ' = C '. [para (6899 (a 1) 67 (a 1 1 1)) demod (11 10 11 6899 11 10 19 19 10)] given #416 (wt=19): 166 ((C v D ') ' v (C ' v (C v (C v D ') ') ') ') ' = (C v (C v D ') ') '. [para (134 (a 1) 23 (a 1 1 1)) demod (11)] given #417 (wt=18): 7002 (C v (C v (C ' v (C v (D v (C v (D v (D v C ') ') ') ')) ')) ') ' = C '. [para (6896 (a 1) 67 (a 1 1 1)) demod (11 10 11 6896 11 19)] given #418 (wt=18): 7616 ((C v (x v (D v y))) ' v (x v (C ' v y)) ') ' = x v y. [para (11 (a 1) 78 (a 1 1 2 1 2))] given #419 (wt=18): 7617 ((C v (x v (D v y))) ' v (y v (C ' v x)) ') ' = x v y. [para (11 (a 1) 78 (a 1 1 2 1)) demod (10)] given #420 (wt=18): 7694 ((C v (D v (D v C '))) ' v (C v (C v (D v (C v (D v (D v C '))) '))) ') ' = C v D. [para (6938 (a 1) 22 (a 1 1 2)) demod (19 11)] given #421 (wt=19): 167 ((C v ((C v (C v D ') ') ' v x)) ' v (x v (C v D ') ') ') ' = x. [para (134 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #422 (wt=18): 7727 (C ' v (C v (C v (C v (D v (D v (D v (D v (C ' v (C ' v C '))))))))) ') ' = C v D. [para (7128 (a 1) 22 (a 1 1 2)) demod (19 19 11)] given #423 (wt=18): 7896 ((C v (x v (y v D))) ' v (x v (C ' v y)) ') ' = x v y. [para (11 (a 1) 80 (a 1 1 2 1 2))] given #424 (wt=18): 7897 ((C v (x v (y v D))) ' v (y v (C ' v x)) ') ' = x v y. [para (11 (a 1) 80 (a 1 1 2 1)) demod (10)] given #425 (wt=18): 8164 ((x v (C v (y v D))) ' v (y v (x v C ')) ') ' = y v x. [para (19 (a 1) 83 (a 1 1 1 1))] given #426 (wt=19): 168 ((x v (C v (C v (C v D ') ') ')) ' v ((C v D ') ' v x) ') ' = x. [para (134 (a 1) 24 (a 1 1 2 1 1))] given #427 (wt=18): 8215 (C ' v (C v (C v (C v (C ' v (C ' v (D v (D v (D v C ') ')) '))))) ') ' = C. [para (4108 (a 1) 12 (a 1 1 2)) demod (11)] given #428 (wt=18): 8380 (C ' v (C v (C v (C ' v (C v (D v (C v (C v (C ' v D '))) ')) '))) ') ' = C. [para (6800 (a 1) 12 (a 1 1 2)) demod (11)] given #429 (wt=18): 8467 (C ' v (C v (C v (C ' v (D v (C v (D v (D v (C ' v C ')))) ') '))) ') ' = C. [para (7013 (a 1) 12 (a 1 1 2)) demod (11)] given #430 (wt=18): 8678 (C ' v (C v (C v (C ' v (C ' v (D v (C ' v (D v C ') ')) ')))) ') ' = C. [para (7237 (a 1) 12 (a 1 1 2)) demod (11)] given #431 (wt=19): 169 ((x v (D v C ') ') ' v (x v (D v (C v (D v C ') ') ')) ') ' = x. [para (155 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #432 (wt=13): 11497 (D v (D v (C ' v (C v (D v C ') ') ')) ') ' = C '. [para (12 (a 1) 169 (a 1 1 1)) demod (11 13 19 11 13)] given #433 (wt=14): 11501 (C ' v (D v (D v (C ' v (C v (D v C ') ') '))) ') ' = D. [para (11497 (a 1) 12 (a 1 1 2)) demod (11)] given #434 (wt=16): 11521 (D v (D v (D v (C ' v (C ' v (C v (D v C ') ') ')))) ') ' = C '. [para (11497 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 11497)] given #435 (wt=17): 11498 (D v (D v ((C v (D v D)) ' v (C v (D v C ') ') ')) ') ' = (C v (D v D)) '. [para (28 (a 1) 169 (a 1 1 1)) demod (19 19 19)] given #436 (wt=25): 171 ((x v (y v (D v C ') ')) ' v (x v (y v (D v (C v (D v C ') ') '))) ') ' = x v y. [para (155 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #437 (wt=14): 11578 (C ' v (C v (D v (D v (C v (D v C ') ') '))) ') ' = C v D. [para (6810 (a 1) 171 (a 1 1 1))] given #438 (wt=16): 11580 (C v (D v (C v (D v (D v (C ' v (C v (D v C ') ') ')))) ')) ' = C '. [para (11578 (a 1) 12 (a 1 1 2)) demod (19 19 19 11 10)] given #439 (wt=17): 11537 (C ' v (D v (D v (D v (C ' v (C ' v (C v (D v C ') ') '))))) ') ' = D. [para (11501 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 11501)] given #440 (wt=18): 8691 (C ' v (D v (D v (C ' v (C v (C v (D v (D v (C ' v C ')))) ') '))) ') ' = D. [para (7294 (a 1) 12 (a 1 1 2)) demod (11)] given #441 (wt=19): 172 ((D v C ') ' v (D ' v (C v (D v C ') ') ') ') ' = (C v (D v C ') ') '. [para (155 (a 1) 23 (a 1 1 1)) demod (11)] given #442 (wt=18): 8707 (C ' v (C v (C v (C v (C ' v (C ' v (C v (D v (C v D ') ')) '))))) ') ' = C. [para (7333 (a 1) 12 (a 1 1 2)) demod (11)] given #443 (wt=18): 8811 ((C v D ') ' v (C v (C v (D v (D v ((D v C ') ' v (C v D ') '))))) ') ' = C. [para (7956 (a 1) 12 (a 1 1 2)) demod (11)] given #444 (wt=18): 8917 ((x v (C v (D v y))) ' v (C ' v (x v y)) ') ' = x v y. [para (11 (a 1) 114 (a 1 1 1 1 2)) demod (10)] given #445 (wt=18): 8918 ((x v (C v (D v y))) ' v (C ' v (y v x)) ') ' = y v x. [para (11 (a 1) 114 (a 1 1 1 1)) demod (10 10)] given #446 (wt=19): 173 ((D v ((C v (D v C ') ') ' v x)) ' v (x v (D v C ') ') ') ' = x. [para (155 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #447 (wt=18): 8920 ((x v (C v (y v D))) ' v (C ' v (x v y)) ') ' = x v y. [para (19 (a 1) 114 (a 1 1 1 1 2))] given #448 (wt=18): 9213 ((C ' v (x v y)) ' v (C v (x v (D v y))) ') ' = x v y. [para (11 (a 1) 184 (a 1 1))] given #449 (wt=18): 9264 ((C ' v (x v y)) ' v (C v (y v (D v x))) ') ' = x v y. [para (11 (a 1) 185 (a 1 1))] given #450 (wt=18): 9305 ((C ' v (x v y)) ' v (C v (y v (x v D))) ') ' = x v y. [para (11 (a 1) 188 (a 1 1))] given #451 (wt=19): 174 ((x v (D v (C v (D v C ') ') ')) ' v ((D v C ') ' v x) ') ' = x. [para (155 (a 1) 24 (a 1 1 2 1 1))] low water: id=8673, wt=30 given #452 (wt=18): 9307 ((x v (C v (y v D))) ' v (C ' v (y v x)) ') ' = y v x. [para (19 (a 1) 188 (a 1 1 1 1))] given #453 (wt=18): 9379 ((x v (C ' v y)) ' v (C v (x v (D v y))) ') ' = x v y. [para (11 (a 1) 266 (a 1 1 1 1 2))] given #454 (wt=18): 9380 ((x v (C ' v y)) ' v (C v (y v (D v x))) ') ' = y v x. [para (11 (a 1) 266 (a 1 1 1 1)) demod (10)] given #455 (wt=18): 9381 ((x v (y v C ')) ' v (x v (C v (D v y))) ') ' = x v y. [para (19 (a 1) 266 (a 1 1 2 1))] given #456 (wt=20): 176 ((x v y) ' v (x v ((C v (y v D)) ' v (y v C ') ')) ') ' = x. [para (69 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #457 (wt=18): 9390 ((x v (y v C ')) ' v (y v (C v (D v x))) ') ' = x v y. [para (19 (a 1) 267 (a 1 1 2 1))] given #458 (wt=18): 9396 ((x v (C ' v y)) ' v (C v (x v (y v D))) ') ' = x v y. [para (11 (a 1) 268 (a 1 1 1 1 2))] given #459 (wt=18): 9397 ((x v (C ' v y)) ' v (C v (y v (x v D))) ') ' = y v x. [para (11 (a 1) 268 (a 1 1 1 1)) demod (10)] given #460 (wt=18): 9398 ((x v (y v C ')) ' v (x v (C v (y v D))) ') ' = x v y. [para (19 (a 1) 268 (a 1 1 2 1))] given #461 (wt=26): 178 ((x v (y v z)) ' v (x v (y v ((C v (z v D)) ' v (z v C ') '))) ') ' = x v y. [para (69 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #462 (wt=18): 9409 ((x v (y v C ')) ' v (y v (C v (x v D))) ') ' = x v y. [para (19 (a 1) 271 (a 1 1 2 1))] given #463 (wt=18): 9412 ((C ' v (x v y)) ' v (y v (x v (C v D))) ') ' = y v x. [para (11 (a 1) 285 (a 1 1 1 1 2))] given #464 (wt=18): 9413 ((C ' v (x v y)) ' v (x v (C v (D v y))) ') ' = x v y. [para (11 (a 1) 285 (a 1 1 2 1 2)) demod (10)] given #465 (wt=18): 9414 ((C ' v (x v y)) ' v (y v (C v (D v x))) ') ' = x v y. [para (11 (a 1) 285 (a 1 1 2 1)) demod (10 10)] given #466 (wt=20): 179 (((C v (x v D)) ' v ((x v C ') ' v y)) ' v (y v x) ') ' = y. [para (69 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #467 (wt=18): 9416 ((x v (C ' v y)) ' v (x v (y v (C v D))) ') ' = x v y. [para (19 (a 1) 285 (a 1 1 1 1))] given #468 (wt=18): 9417 ((C ' v (x v y)) ' v (x v (C v (y v D))) ') ' = x v y. [para (19 (a 1) 285 (a 1 1 2 1 2))] given #469 (wt=18): 9419 ((x v (C ' v y)) ' v (y v (x v (C v D))) ') ' = y v x. [para (20 (a 1) 285 (a 1 1 1 1))] given #470 (wt=18): 9423 ((x v (y v C ')) ' v (y v (x v (C v D))) ') ' = y v x. [para (36 (a 1) 285 (a 1 1 1 1))] given #471 (wt=20): 180 ((x v ((C v (y v D)) ' v (y v C ') ')) ' v (y v x) ') ' = x. [para (69 (a 1) 24 (a 1 1 2 1 1))] given #472 (wt=18): 9794 ((x v (C v (D v y))) ' v (x v (C ' v y)) ') ' = x v y. [para (11 (a 1) 1314 (a 1 1 2 1 2))] given #473 (wt=18): 9795 ((x v (C v (D v y))) ' v (y v (C ' v x)) ') ' = x v y. [para (11 (a 1) 1314 (a 1 1 2 1)) demod (10)] given #474 (wt=18): 9863 ((x v (C v (y v D))) ' v (x v (C ' v y)) ') ' = x v y. [para (19 (a 1) 1732 (a 1 1 1 1 2))] given #475 (wt=18): 9983 (C ' v (D v ((x v (C v y)) ' v (C v (x v y) ') ')) ') ' = D. [para (19 (a 1) 9887 (a 1 1 2 1 2 1 1))] given #476 (wt=20): 182 ((x v y) ' v (x v ((C v (D v y)) ' v (C ' v y) ')) ') ' = x. [para (74 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #477 (wt=18): 9984 (C ' v (D v ((C v C ') ' v (C v (C v (C v (C ' v D ')) ')) ')) ') ' = D. [para (30 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #478 (wt=18): 9986 (C ' v (D v ((x v (C v y)) ' v (C v (y v x) ') ')) ') ' = D. [para (20 (a 1) 9887 (a 1 1 2 1 2 1 1))] given #479 (wt=18): 9987 (C ' v (D v ((x v (y v C)) ' v (C v (x v y) ') ')) ') ' = D. [para (20 (a 2) 9887 (a 1 1 2 1 2 1 1))] given #480 (wt=18): 9988 (C ' v (D v ((C v (x v y)) ' v (C v (y v x) ') ')) ') ' = D. [para (21 (a 1) 9887 (a 1 1 2 1 2 1 1))] given #481 (wt=26): 187 ((x v (y v z)) ' v (x v (y v ((C v (D v z)) ' v (C ' v z) '))) ') ' = x v y. [para (74 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #482 (wt=18): 9989 (C ' v (D v ((x v (y v C)) ' v (C v (y v x) ') ')) ') ' = D. [para (36 (a 1) 9887 (a 1 1 2 1 2 1 1))] given #483 (wt=18): 9997 (C ' v (D v ((C v C ') ' v (C v (D v (D v (C ' v C ')) ')) ')) ') ' = D. [para (102 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #484 (wt=18): 10036 (C ' v (D v (C ' v (C v (C v (C ' v (C ' v (D v C ') ')))) ')) ') ' = D. [para (717 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #485 (wt=18): 10086 (C ' v (D v ((C v (C v D)) ' v (C v (C v (C ' v (C v (C v D)) '))) ')) ') ' = D. [para (68 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #486 (wt=20): 189 (((C v (D v x)) ' v ((C ' v x) ' v y)) ' v (y v x) ') ' = y. [para (74 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #487 (wt=18): 10105 (C ' v (D v ((C v C ') ' v (C v (C v (C v (D v (C v C ') ')))) ')) ') ' = D. [para (147 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #488 (wt=18): 10113 (C ' v (D v ((C v C ') ' v (C v (C v (D v (D v (D v C ') ')))) ')) ') ' = D. [para (3666 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #489 (wt=18): 10183 (C ' v (D v (C ' v (C v (C v (C ' v (D v (D v C ') ') '))) ')) ') ' = D. [para (6906 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #490 (wt=18): 10538 (C ' v (D v (D v (C ' v (C ' v (C v (C ' v (D v C ') ')) ')))) ') ' = D. [para (9996 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 9996)] given #491 (wt=20): 190 ((x v ((C v (D v y)) ' v (C ' v y) ')) ' v (y v x) ') ' = x. [para (74 (a 1) 24 (a 1 1 2 1 1))] given #492 (wt=18): 10555 (C ' v (D v (D v (C ' v (C ' v (C v (D v (D v C ') ') ') ')))) ') ' = D. [para (10176 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 10176)] given #493 (wt=18): 10571 (D v (D v (D v (C ' v (C ' v ((C v (C v D)) ' v (C v C ') '))))) ') ' = C '. [para (10323 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 10323)] given #494 (wt=18): 10573 (D v (D v (C ' v ((C v C) ' v (C v (C ' v (C v D ') ')) '))) ') ' = C '. [para (27 (a 1) 9979 (a 1 1 2 1 2 2 2 1 2)) demod (11)] given #495 (wt=18): 10591 (D v (D v (C ' v ((C v D ') ' v (C v (C v (C v D ') ')) '))) ') ' = C '. [para (134 (a 1) 9979 (a 1 1 2 1 2 2 2)) demod (11)] given #496 (wt=21): 192 ((x v y) ' v (y v ((x v z) ' v (x v z ') ')) ') ' = y. [para (11 (a 1) 25 (a 1 1 1 1))] given #497 (wt=18): 10660 (D v (D v (C ' v (C ' v (C v (D v (D v (D v C ') ')) ') '))) ') ' = C '. [para (3666 (a 1) 9979 (a 1 1 2 1 2 2 1))] given #498 (wt=18): 10943 ((x v (C v (y v D))) ' v (y v (C ' v x)) ') ' = x v y. [para (19 (a 1) 1917 (a 1 1 1 1 2))] given #499 (wt=18): 11024 ((x v (D v (D v (C ' v C ')))) ' v (x v (D v C ') ') ') ' = x. [para (11023 (a 1) 12 (a 1 1 2 1 2))] % Back_subsumption disabled, ratio of kept to back_subsumed is 1969 (0.00 of 18.90 sec). given #500 (wt=16): 11824 (D v (D v (D v (C ' v (C ' v (C v (D v D)) ')))) ') ' = (C v (D v D)) '. [para (28 (a 1) 11024 (a 1 1 2)) demod (19 11 10 10 10 11 19)] given #501 (wt=21): 193 ((x v y) ' v ((y v z) ' v ((y v z ') ' v x)) ') ' = x. [para (11 (a 1) 25 (a 1 1 2 1)) demod (10)] given #502 (wt=17): 11827 ((C v (D v D)) ' v (D v (D v (D v (C ' v (C ' v (C v (D v D)) '))))) ') ' = D. [para (11824 (a 1) 12 (a 1 1 2)) demod (11)] given #503 (wt=18): 11028 ((D v (D v (C ' v (C ' v x)))) ' v (x v (D v C ') ') ') ' = x. [para (11023 (a 1) 23 (a 1 1 2 1 2)) demod (10 10 10)] given #504 (wt=18): 11029 ((x v (D v (D v (C ' v C ')))) ' v ((D v C ') ' v x) ') ' = x. [para (11023 (a 1) 24 (a 1 1 2 1 1))] given #505 (wt=18): 11032 ((D v (D v (C ' v (C ' v x)))) ' v ((D v C ') ' v x) ') ' = x. [para (11023 (a 1) 84 (a 1 1 2 1 1)) demod (10 10 10)] given #506 (wt=29): 194 ((x v y) ' v (x v ((y v z) ' v (y v ((z v u) ' v (z v u ') ')) ')) ') ' = x. [para (25 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #507 (wt=18): 11033 ((x v (D v C ') ') ' v (D v (D v (C ' v (C ' v x)))) ') ' = x. [para (11023 (a 1) 85 (a 1 1 1 1 2)) demod (10 10 10)] given #508 (wt=18): 11034 ((D v (x v (D v (C ' v C ')))) ' v (x v (D v C ') ') ') ' = x. [para (11023 (a 1) 31 (a 1 1 2 1 2))] given #509 (wt=18): 11035 (((D v C ') ' v x) ' v (x v (D v (D v (C ' v C ')))) ') ' = x. [para (11023 (a 1) 128 (a 1 1 1 1 1))] given #510 (wt=18): 11046 (D v (D v (D v (D v ((D v C ') ' v (C ' v C ') '))) ')) ' = (D v C ') '. [para (11023 (a 1) 46 (a 1 1 2 2 1 2 2 2)) demod (11 11023)] given #511 (wt=26): 195 (x v (x v ((x v y) ' v ((y v z) ' v (y v z ') '))) ') ' = (x v y) '. [para (25 (a 1) 12 (a 1 1 2)) demod (19 11)] given #512 (wt=18): 11048 ((D v (x v (D v (C ' v C ')))) ' v ((D v C ') ' v x) ') ' = x. [para (11023 (a 1) 135 (a 1 1 2 1 1))] given #513 (wt=18): 11053 ((x v (D v C ') ') ' v (D v (x v (D v (C ' v C ')))) ') ' = x. [para (11023 (a 1) 496 (a 1 1 1 1 2))] given #514 (wt=18): 11055 (((D v C ') ' v x) ' v (D v (x v (D v (C ' v C ')))) ') ' = x. [para (11023 (a 1) 549 (a 1 1 1 1 1))] given #515 (wt=18): 11105 (D v (D v (C ' v (C v (D v (D v (C ' v (D v C ') ')))) '))) ' = (D v C ') '. [para (11039 (a 1) 12 (a 1 1 2)) demod (11 10 10 10 11 10 10)] given #516 (wt=32): 196 (x v ((x v y) ' v (((x v y ') ' v z) ' v ((x v y ') ' v z ') ')) ') ' = (x v y) '. [para (12 (a 1) 25 (a 1 1 1))] given #517 (wt=18): 11280 ((C v (x v D)) ' v (x v (C ' v (C v (D v (D v C '))) ')) ') ' = x. [para (19 (a 1) 6919 (a 1 1 1 1))] given #518 (wt=18): 11319 ((C ' v ((C v (D v (D v C '))) ' v x)) ' v (C v (x v D)) ') ' = x. [para (19 (a 1) 6935 (a 1 1 2 1))] given #519 (wt=18): 11325 ((x v (C ' v (C v (D v (D v C '))) ')) ' v (C v (x v D)) ') ' = x. [para (11 (a 1) 6937 (a 1 1 2 1 2))] given #520 (wt=18): 11336 ((C v (x v D)) ' v (C ' v ((C v (D v (D v C '))) ' v x)) ') ' = x. [para (11 (a 1) 6943 (a 1 1 1 1 2))] given #521 (wt=26): 197 ((x v (y v z) ') ' v (x v (y v (y v (z ' v (y v z) ')) ')) ') ' = x. [para (12 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #522 (wt=18): 11369 (C ' v (D v (C ' v (C v (C v (C ' v (C v (C v D ') ') '))) ')) ') ' = D. [para (11349 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #523 (wt=18): 11424 ((C v (x v D)) ' v (C ' v (x v (C v (D v (D v C '))) ')) ') ' = x. [para (19 (a 1) 6945 (a 1 1 1 1))] given #524 (wt=18): 11511 (C ' v (C v (C ' v (D v (D v (C ' v (C v (D v C ') ') '))) ')) ') ' = C. [para (11497 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #525 (wt=18): 11556 ((C v (D v D)) ' v (D v (D v ((C v (D v D)) ' v (C v (D v C ') ') '))) ') ' = D. [para (11498 (a 1) 12 (a 1 1 2)) demod (11)] given #526 (wt=21): 199 (C v (C ' v (((C v D ') ' v x) ' v ((C v D ') ' v x ') ')) ') ' = C '. [para (27 (a 1) 25 (a 1 1 1))] given #527 (wt=17): 11965 (C v (C ' v (D ' v (C ' v (D ' v (C v D ') ')) ')) ') ' = C '. [para (23 (a 1) 199 (a 1 1 2 1 2 2)) demod (11 11 10 11)] given #528 (wt=18): 11597 (C ' v (C v (C v (D v (D v (D v (C ' v (C v (D v C ') ') ')))))) ') ' = C v D. [para (11578 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 10 19 19 19 19 19 19 19 11578)] given #529 (wt=18): 11658 ((C ' v (x v y)) ' v (y v (C v (x v D))) ') ' = x v y. [para (19 (a 1) 9305 (a 1 1 2 1))] given #530 (wt=18): 11677 ((x v (C ' v y)) ' v (y v (C v (D v x))) ') ' = y v x. [para (19 (a 1) 9380 (a 1 1 2 1))] given #531 (wt=23): 200 ((x v y) ' v (x v ((y v C) ' v (y v (C ' v (C v D ') ')) ')) ') ' = x. [para (27 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #532 (wt=18): 11699 ((x v (C ' v y)) ' v (x v (C v (y v D))) ') ' = x v y. [para (19 (a 1) 9396 (a 1 1 2 1))] given #533 (wt=18): 11701 ((x v (C ' v y)) ' v (y v (C v (x v D))) ') ' = y v x. [para (19 (a 1) 9397 (a 1 1 2 1))] given #534 (wt=18): 11852 ((D v (D v (C ' v (x v C ')))) ' v (x v (D v C ') ') ') ' = x. [para (11 (a 1) 11028 (a 1 1 1 1 2 2 2))] given #535 (wt=18): 11855 ((D v (D v (x v (C ' v C ')))) ' v (x v (D v C ') ') ') ' = x. [para (20 (a 1) 11028 (a 1 1 1 1 2 2))] given #536 (wt=27): 201 ((x v (y v z)) ' v (y v ((x v (z v u)) ' v (x v (z v u ')) ')) ') ' = y. [para (19 (a 1) 25 (a 1 1 1 1)) demod (10 10)] given #537 (wt=18): 11864 ((D v (D v (C ' v (x v C ')))) ' v ((D v C ') ' v x) ') ' = x. [para (11 (a 1) 11032 (a 1 1 1 1 2 2 2))] given #538 (wt=18): 11868 ((D v (D v (x v (C ' v C ')))) ' v ((D v C ') ' v x) ') ' = x. [para (20 (a 1) 11032 (a 1 1 1 1 2 2))] given #539 (wt=18): 11874 ((x v (D v C ') ') ' v (D v (D v (C ' v (x v C ')))) ') ' = x. [para (11 (a 1) 11033 (a 1 1 2 1 2 2 2))] given #540 (wt=18): 11877 ((x v (D v C ') ') ' v (D v (D v (x v (C ' v C ')))) ') ' = x. [para (20 (a 1) 11033 (a 1 1 2 1 2 2))] given #541 (wt=25): 202 ((x v y) ' v (x v ((z v (y v u)) ' v (y v (z v u) ') ')) ') ' = x. [para (19 (a 1) 25 (a 1 1 2 1 2 1 1))] given #542 (wt=18): 11906 (((D v C ') ' v x) ' v (D v (D v (x v (C ' v C ')))) ') ' = x. [para (19 (a 1) 11055 (a 1 1 2 1 2))] given #543 (wt=18): 11913 (C v (C v (C ' v (C v (C v ((C v D ') ' v (C v D ') '))) ')) ') ' = C '. [para (164 (a 1) 196 (a 1 1 2 1 2 2)) demod (13 19 19 11 19 13)] given #544 (wt=18): 11983 (C v (C v (C ' v (C v (D v ((D v C ') ' v (C v D ') '))) ')) ') ' = C '. [para (6810 (a 1) 199 (a 1 1 2 1 2 2 1 2)) demod (11 10 10 11 27 11 19)] given #545 (wt=18): 11996 (C ' v (C v (C ' v (D ' v (C ' v (D ' v (C v D ') ')) '))) ') ' = C. [para (11965 (a 1) 12 (a 1 1 2)) demod (11)] given #546 (wt=21): 203 ((x v y) ' v ((y v z) ' v (x v (y v z ') ')) ') ' = x. [para (19 (a 1) 25 (a 1 1 2 1))] given #547 (wt=18): 12043 (((D v C ') ' v x) ' v (D v (D v (C ' v (x v C ')))) ') ' = x. [para (11 (a 1) 11864 (a 1 1))] given #548 (wt=19): 348 (C v (C v (D ' v (C v (C v (C v D ') ')) ')) ') ' = (C v (C v (C v D ') ')) '. [para (164 (a 1) 24 (a 1 1 2)) demod (11 10 11)] given #549 (wt=19): 373 (x v (x v (C ' v ((x v C) ' v (C v D ') '))) ') ' = (x v C) '. [para (29 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #550 (wt=19): 377 (x v (x v (C ' v ((C v D ') ' v (x v C) '))) ') ' = (x v C) '. [para (29 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #551 (wt=24): 204 (C ' v (C v (((C v (C ' v D ')) ' v x) ' v ((C v (C ' v D ')) ' v x ') ')) ') ' = C. [para (30 (a 1) 25 (a 1 1 1))] low water: id=9151, wt=29 given #552 (wt=16): 12076 (C ' v (C v (C ' v (C ' v (C v (C ' v D ')) ') ')) ') ' = C. [para (31 (a 1) 204 (a 1 1 2 1 2 1)) demod (27 11)] given #553 (wt=18): 12083 (C v (C v (C ' v (C ' v (C ' v (C v (C ' v D ')) ') '))) ') ' = C '. [para (12076 (a 1) 12 (a 1 1 2)) demod (19 11)] given #554 (wt=19): 406 ((x v (y v z)) ' v (y ' v (x v z)) ') ' = x v z. [para (19 (a 1) 84 (a 1 1 1 1))] given #555 (wt=19): 407 ((x v (y v z)) ' v (y v (x ' v z)) ') ' = y v z. [para (19 (a 1) 84 (a 1 1 2 1))] given #556 (wt=25): 205 ((x v y) ' v (x v ((y v C ') ' v (y v (C v (C v (C ' v D ')) ')) ')) ') ' = x. [para (30 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #557 (wt=19): 410 ((x v (y v z)) ' v (y ' v (z v x)) ') ' = z v x. [para (20 (a 1) 84 (a 1 1 1 1))] given #558 (wt=19): 411 ((x v (y v z)) ' v (z v (x ' v y)) ') ' = y v z. [para (20 (a 1) 84 (a 1 1 2 1))] given #559 (wt=19): 412 ((x v (y v z)) ' v (x ' v (z v y)) ') ' = z v y. [para (21 (a 1) 84 (a 1 1 1 1))] given #560 (wt=19): 425 (x v (y v (x v (y ' v x) ')) ') ' = (y ' v x) '. [para (84 (a 1) 24 (a 1 1 2)) demod (11 10 11)] given #561 (wt=27): 206 (C v (C ' v (((C v (C v (C ' v D '))) ' v x) ' v ((C v (C v (C ' v D '))) ' v x ') ')) ') ' = C '. [para (33 (a 1) 25 (a 1 1 1))] given #562 (wt=19): 427 (((C v D ') ' v x) ' v (C v ((C v (C v D ') ') ' v x)) ') ' = x. [para (134 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #563 (wt=19): 428 (((D v C ') ' v x) ' v (D v ((C v (D v C ') ') ' v x)) ') ' = x. [para (155 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #564 (wt=19): 448 ((x v (y v z ')) ' v (z v (x v y)) ') ' = x v y. [para (10 (a 1) 85 (a 1 1 1 1))] given #565 (wt=19): 451 ((x v (y v z ')) ' v (x v (z v y)) ') ' = x v y. [para (19 (a 1) 85 (a 1 1 2 1)) demod (10)] given #566 (wt=26): 207 ((x v y) ' v (x v ((y v C) ' v (y v (C ' v (C v (C v (C ' v D '))) ')) ')) ') ' = x. [para (33 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #567 (wt=19): 454 ((x v (y v z ')) ' v (y v (z v x)) ') ' = x v y. [para (20 (a 1) 85 (a 1 1 2 1)) demod (10)] given #568 (wt=19): 455 ((x v (y v z ')) ' v (z v (y v x)) ') ' = x v y. [para (21 (a 1) 85 (a 1 1 2 1)) demod (10)] given #569 (wt=19): 458 ((x v (y v z ')) ' v (y v (x v z)) ') ' = x v y. [para (36 (a 1) 85 (a 1 1 2 1)) demod (10)] given #570 (wt=19): 470 ((x v (C v D ') ') ' v (C v ((C v (C v D ') ') ' v x)) ') ' = x. [para (134 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #571 (wt=27): 208 ((x v (y v z)) ' v (y v ((z v (x v u)) ' v (z v (x v u ')) ')) ') ' = y. [para (20 (a 1) 25 (a 1 1 1 1)) demod (10 10)] given #572 (wt=19): 471 ((x v (D v C ') ') ' v (D v ((C v (D v C ') ') ' v x)) ') ' = x. [para (155 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #573 (wt=19): 521 ((x v (C v D ') ') ' v (C v (x v (C v (C v D ') ') ')) ') ' = x. [para (134 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #574 (wt=19): 522 ((x v (D v C ') ') ' v (D v (x v (C v (D v C ') ') ')) ') ' = x. [para (155 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #575 (wt=19): 546 ((x ' v (y v z)) ' v (y v (z v x)) ') ' = y v z. [para (10 (a 1) 128 (a 1 1 2 1))] given #576 (wt=25): 209 ((x v y) ' v (x v ((z v (y v u)) ' v (y v (u v z) ') ')) ') ' = x. [para (20 (a 1) 25 (a 1 1 2 1 2 1 1))] given #577 (wt=19): 548 ((x v (y ' v z)) ' v (x v (z v y)) ') ' = x v z. [para (19 (a 1) 128 (a 1 1 1 1)) demod (10)] given #578 (wt=19): 552 ((x v (y ' v z)) ' v (z v (x v y)) ') ' = z v x. [para (20 (a 1) 128 (a 1 1 1 1)) demod (10)] given #579 (wt=19): 554 ((x ' v (y v z)) ' v (z v (y v x)) ') ' = z v y. [para (21 (a 1) 128 (a 1 1 1 1)) demod (10)] given #580 (wt=19): 568 (((C v D ') ' v x) ' v (x v (C v (C v (C v D ') ') ')) ') ' = x. [para (134 (a 1) 128 (a 1 1 1 1 1))] given #581 (wt=27): 210 ((x v (y v z)) ' v (z v ((x v (y v u)) ' v (x v (y v u ')) ')) ') ' = z. [para (20 (a 2) 25 (a 1 1 1 1)) demod (10 10)] given #582 (wt=19): 569 (((D v C ') ' v x) ' v (x v (D v (C v (D v C ') ') ')) ') ' = x. [para (155 (a 1) 128 (a 1 1 1 1 1))] given #583 (wt=19): 653 (C ' v (C v ((D v x) ' v (D v (D v (x ' v (D v x) '))) ')) ') ' = C. [para (26 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #584 (wt=19): 716 ((x v C) ' v (x v (C ' v (C v (C ' v (D v C ') ')) ')) ') ' = x. [para (702 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #585 (wt=19): 719 ((C ' v ((C v (C ' v (D v C ') ')) ' v x)) ' v (x v C) ') ' = x. [para (702 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #586 (wt=25): 211 ((x v y) ' v (x v ((z v (u v y)) ' v (y v (z v u) ') ')) ') ' = x. [para (20 (a 2) 25 (a 1 1 2 1 2 1 1))] given #587 (wt=19): 720 ((x v (C ' v (C v (C ' v (D v C ') ')) ')) ' v (C v x) ') ' = x. [para (702 (a 1) 24 (a 1 1 2 1 1))] given #588 (wt=19): 721 (C v (C v (C v (C ' v (D v C ') ')) ') ') ' = (C v (C ' v (D v C ') ')) '. [para (702 (a 1) 24 (a 1 1 2)) demod (11 11)] given #589 (wt=19): 726 ((C v x) ' v (C ' v ((C v (C ' v (D v C ') ')) ' v x)) ') ' = x. [para (702 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #590 (wt=19): 727 ((x v C) ' v (C ' v ((C v (C ' v (D v C ') ')) ' v x)) ') ' = x. [para (702 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #591 (wt=27): 212 ((x v (y v z)) ' v (x v ((z v (y v u)) ' v (z v (y v u ')) ')) ') ' = x. [para (21 (a 1) 25 (a 1 1 1 1)) demod (10 10)] given #592 (wt=19): 728 ((x v C) ' v (C ' v (x v (C v (C ' v (D v C ') ')) ')) ') ' = x. [para (702 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #593 (wt=19): 729 ((C v x) ' v (x v (C ' v (C v (C ' v (D v C ') ')) ')) ') ' = x. [para (702 (a 1) 128 (a 1 1 1 1 1))] given #594 (wt=19): 730 (C ' v (C v (C ' v (D v (C ' v (C v (C ' v (D v C ') ')) ')) ')) ') ' = C. [para (702 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11 13 11)] given #595 (wt=19): 801 (x v (C ' v (x v ((x v C) ' v (C v D ') '))) ') ' = (x v C) '. [para (90 (a 1) 24 (a 1 1 2)) demod (19 20 11)] given #596 (wt=25): 213 ((x v y) ' v (x v ((y v (z v u)) ' v (y v (u v z) ') ')) ') ' = x. [para (21 (a 1) 25 (a 1 1 2 1 2 1 1))] given #597 (wt=19): 807 (x v (C ' v ((C v D ') ' v (x v (x v C) '))) ') ' = (x v C) '. [para (90 (a 1) 84 (a 1 1 2)) demod (10 10 11)] given #598 (wt=19): 813 (x v (x v (C ' v ((x v D) ' v (D v C ') '))) ') ' = (x v D) '. [para (101 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #599 (wt=19): 816 (x v (x v (C ' v ((D v C ') ' v (x v D) '))) ') ' = (x v D) '. [para (101 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #600 (wt=19): 838 (x v (C ' v (x v ((x v D) ' v (D v C ') '))) ') ' = (x v D) '. [para (104 (a 1) 24 (a 1 1 2)) demod (19 20 11)] given #601 (wt=35): 214 ((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 (25 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #602 (wt=19): 844 (x v (C ' v ((D v C ') ' v (x v (x v D) '))) ') ' = (x v D) '. [para (104 (a 1) 84 (a 1 1 2)) demod (10 10 11)] given #603 (wt=19): 896 (x v (x v (C ' v ((C v x) ' v (C v D ') '))) ') ' = (C v x) '. [para (133 (a 1) 24 (a 1 1 2)) demod (19 19 11)] given #604 (wt=19): 903 (x v (x v (C ' v ((C v D ') ' v (C v x) '))) ') ' = (C v x) '. [para (133 (a 1) 84 (a 1 1 2)) demod (10 10 11)] given #605 (wt=19): 910 ((x v D) ' v (x v (C ' v (D v (C ' v (C v D ') ')) ')) ') ' = x. [para (886 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #606 (wt=42): 215 (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 (22 (a 1) 25 (a 1 1 1)) demod (10)] given #607 (wt=19): 913 ((C ' v ((D v (C ' v (C v D ') ')) ' v x)) ' v (x v D) ') ' = x. [para (886 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #608 (wt=19): 914 ((x v (C ' v (D v (C ' v (C v D ') ')) ')) ' v (D v x) ') ' = x. [para (886 (a 1) 24 (a 1 1 2 1 1))] given #609 (wt=19): 915 (D v (C v (D v (C ' v (C v D ') ')) ') ') ' = (D v (C ' v (C v D ') ')) '. [para (886 (a 1) 24 (a 1 1 2)) demod (11 11)] given #610 (wt=19): 920 ((D v x) ' v (C ' v ((D v (C ' v (C v D ') ')) ' v x)) ') ' = x. [para (886 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #611 (wt=35): 216 ((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 (22 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #612 (wt=19): 921 ((x v D) ' v (C ' v ((D v (C ' v (C v D ') ')) ' v x)) ') ' = x. [para (886 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #613 (wt=19): 922 ((x v D) ' v (C ' v (x v (D v (C ' v (C v D ') ')) ')) ') ' = x. [para (886 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #614 (wt=19): 923 ((D v x) ' v (x v (C ' v (D v (C ' v (C v D ') ')) ')) ') ' = x. [para (886 (a 1) 128 (a 1 1 1 1 1))] given #615 (wt=19): 988 (x v (x v (C ' v ((D v x) ' v (D v C ') '))) ') ' = (D v x) '. [para (154 (a 1) 24 (a 1 1 2)) demod (19 19 11)] given #616 (wt=34): 217 ((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 (22 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 10 11 10)] given #617 (wt=19): 996 (x v (x v (C ' v ((D v C ') ' v (D v x) '))) ') ' = (D v x) '. [para (154 (a 1) 84 (a 1 1 2)) demod (10 10 11)] given #618 (wt=19): 1019 (x v (C ' v ((C v D ') ' v (x v (C v x) '))) ') ' = (C v x) '. [para (371 (a 1) 37 (a 1 1 2)) demod (11 10 11)] given #619 (wt=19): 1040 (x v (C ' v (x v ((C v D ') ' v (x v C) '))) ') ' = (x v C) '. [para (374 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #620 (wt=19): 1079 (x v (C ' v (x v ((C v x) ' v (C v D ') '))) ') ' = (C v x) '. [para (371 (a 1) 39 (a 1 1 2)) demod (10 19 20 11)] given #621 (wt=27): 218 ((x v (y v z)) ' v (z v ((y v (x v u)) ' v (y v (x v u ')) ')) ') ' = z. [para (36 (a 1) 25 (a 1 1 1 1)) demod (10 10)] given #622 (wt=19): 1112 (x v (C ' v (x v ((D v x) ' v (D v C ') '))) ') ' = (D v x) '. [para (420 (a 1) 12 (a 1 1 2)) demod (19 20 11)] given #623 (wt=19): 1122 (x v (C ' v ((D v C ') ' v (x v (D v x) '))) ') ' = (D v x) '. [para (420 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #624 (wt=19): 1248 (x v (C ' v (x v ((D v C ') ' v (x v D) '))) ') ' = (x v D) '. [para (514 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #625 (wt=19): 1309 ((x v (y v z)) ' v (x v (y ' v z)) ') ' = x v z. [para (11 (a 1) 41 (a 1 1 2 1 2))] given #626 (wt=25): 219 ((x v y) ' v (x v ((z v (u v y)) ' v (y v (u v z) ') ')) ') ' = x. [para (36 (a 1) 25 (a 1 1 2 1 2 1 1))] given #627 (wt=19): 1310 ((x v (y v z)) ' v (z v (y ' v x)) ') ' = x v z. [para (11 (a 1) 41 (a 1 1 2 1)) demod (10)] given #628 (wt=19): 1422 (x v (C ' v (x v ((C v D ') ' v (C v x) '))) ') ' = (C v x) '. [para (887 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #629 (wt=19): 1441 (x v (C ' v (x v ((D v C ') ' v (D v x) '))) ') ' = (D v x) '. [para (980 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #630 (wt=19): 1624 (C v (C v (C ' v (C ' v (D v (D v (D v (C ' v (C ' v C '))))) '))) ') ' = C '. [para (111 (a 1) 611 (a 1 1 2 1 2 2 2)) demod (11)] given #631 (wt=30): 220 (x v ((x v (C v D)) ' v (((x v C ') ' v y) ' v ((x v C ') ' v y ') ')) ') ' = (x v (C v D)) '. [para (28 (a 1) 25 (a 1 1 1))] given #632 (wt=19): 2253 ((x v (C v D)) ' v (x v (x v (C ' v (x v (C v D)) '))) ') ' = x. [para (68 (a 1) 12 (a 1 1 2)) demod (11)] given #633 (wt=19): 2280 ((C v (D v x)) ' v (x v (x v (C ' v (C v (D v x)) '))) ') ' = x. [para (77 (a 1) 12 (a 1 1 2)) demod (11)] given #634 (wt=19): 2307 ((C v (C ' v D ')) ' v (C ' v (C ' v (C v (C ' v D ')) ')) ') ' = C '. [para (91 (a 1) 12 (a 1 1 2)) demod (11)] given #635 (wt=19): 2508 ((D v (C ' v C ')) ' v (C ' v (D ' v (D v (C ' v C ')) ')) ') ' = C '. [para (108 (a 1) 12 (a 1 1 2)) demod (11)] given #636 (wt=28): 221 ((x v y) ' v (x v ((y v z) ' v (y v ((z v (C v D)) ' v (z v C ') ')) ')) ') ' = x. [para (28 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #637 (wt=19): 2563 ((x v (C v D)) ' v (x v (C ' v (x v (x v (C v D)) '))) ') ' = x. [para (117 (a 1) 12 (a 1 1 2)) demod (11)] given #638 (wt=19): 2576 ((x v (C v D)) ' v (C ' v (x v (x v (x v (C v D)) '))) ') ' = x. [para (117 (a 1) 31 (a 1 1 2)) demod (11)] given #639 (wt=19): 2806 ((C v (x v (C v (C v D ') ') ')) ' v ((C v D ') ' v x) ') ' = x. [para (134 (a 1) 135 (a 1 1 2 1 1))] given #640 (wt=19): 2807 ((D v (x v (C v (D v C ') ') ')) ' v ((D v C ') ' v x) ') ' = x. [para (155 (a 1) 135 (a 1 1 2 1 1))] given #641 (wt=25): 222 ((x v (y v (C v D)) ') ' v (x v (y v (y v (C ' v (y v (C v D)) ')) ')) ') ' = x. [para (28 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #642 (wt=19): 2841 ((C v x) ' v (C ' v (x v (C v (C ' v (D v C ') ')) ')) ') ' = x. [para (702 (a 1) 135 (a 1 1 2 1 1)) demod (11)] given #643 (wt=19): 2852 ((D v x) ' v (C ' v (x v (D v (C ' v (C v D ') ')) ')) ') ' = x. [para (886 (a 1) 135 (a 1 1 2 1 1)) demod (11)] given #644 (wt=19): 3212 ((x v C ') ' v (x v (x v (C v (D v (x v C ') ')))) ') ' = x. [para (147 (a 1) 12 (a 1 1 2)) demod (11)] given #645 (wt=19): 3230 ((x v C ') ' v (C v (D v (x v (x v (x v C ') ')))) ') ' = x. [para (147 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #646 (wt=30): 223 (C ' v (C v (((C v (C v (C ' v (C ' v D ')))) ' v x) ' v ((C v (C v (C ' v (C ' v D ')))) ' v x ') ')) ') ' = C. [para (35 (a 1) 25 (a 1 1 1))] given #647 (wt=19): 3280 ((x v C ') ' v (x v (C v (D v (x v (x v C ') ')))) ') ' = x. [para (150 (a 1) 12 (a 1 1 2)) demod (11)] given #648 (wt=19): 3291 ((x v C ') ' v (C v (x v (D v (x v (x v C ') ')))) ') ' = x. [para (150 (a 1) 31 (a 1 1 2)) demod (11)] given #649 (wt=19): 3294 ((x v C ') ' v (D v (x v (x v (C v (x v C ') ')))) ') ' = x. [para (150 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #650 (wt=19): 3301 ((x v C ') ' v (D v (x v (C v (x v (x v C ') ')))) ') ' = x. [para (150 (a 1) 60 (a 1 1 2)) demod (11 19 19 10 11)] given #651 (wt=28): 224 ((x v y) ' v (x v ((y v C ') ' v (y v (C v (C v (C v (C ' v (C ' v D ')))) ')) ')) ') ' = x. [para (35 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #652 (wt=19): 3399 ((C ' v x) ' v (x v (x v (C v (D v (C ' v x) ')))) ') ' = x. [para (160 (a 1) 12 (a 1 1 2)) demod (11)] given #653 (wt=19): 3402 ((C v (C v (C ' v D '))) ' v (C v (C v (D v (C v (C v (C ' v D '))) '))) ') ' = C. [para (33 (a 1) 160 (a 1 1 2 1 2 2 2)) demod (11 11 10 10 33)] given #654 (wt=19): 3431 ((C ' v x) ' v (C v (D v (x v (x v (C ' v x) ')))) ') ' = x. [para (160 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #655 (wt=19): 3884 (C v (D v (D v (C v (C v (D v (D v (D v C ')))) ') '))) ' = (C v (D v (D v (D v C ')))) '. [para (3688 (a 1) 24 (a 1 1 2)) demod (11 11 10 10)] given #656 (wt=21): 225 ((x v C) ' v (x v (C ' v (C v (C v (C v (C ' v (C ' v D '))))) ')) ') ' = x. [para (35 (a 1) 25 (a 1 1 2 1 2 2)) demod (11)] given #657 (wt=19): 3977 (C v (C v (C ' v (D v (D v (C v (D v (D v (D v (C ' v C '))))) ')) ')) ') ' = C '. [para (3879 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 3879)] given #658 (wt=19): 4138 ((C v (x v D)) ' v (x v (x v (C ' v (C v (x v D)) '))) ') ' = x. [para (177 (a 1) 12 (a 1 1 2)) demod (11)] given #659 (wt=19): 4202 ((x v C ') ' v (x v (C v (x v (D v (x v C ') ')))) ') ' = x. [para (181 (a 1) 12 (a 1 1 2)) demod (11)] given #660 (wt=19): 4213 ((x v C ') ' v (C v (x v (x v (D v (x v C ') ')))) ') ' = x. [para (181 (a 1) 31 (a 1 1 2)) demod (11)] given #661 (wt=30): 226 (x v ((C v (D v x)) ' v (((x v C ') ' v y) ' v ((x v C ') ' v y ') ')) ') ' = (C v (D v x)) '. [para (65 (a 1) 25 (a 1 1 1))] given #662 (wt=19): 4216 ((x v C ') ' v (x v (D v (x v (C v (x v C ') ')))) ') ' = x. [para (181 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #663 (wt=19): 4230 ((C v (D v x)) ' v (x v (C ' v (x v (C v (D v x)) '))) ') ' = x. [para (183 (a 1) 12 (a 1 1 2)) demod (11)] given #664 (wt=19): 4246 ((C v (D v x)) ' v (C ' v (x v (x v (C v (D v x)) '))) ') ' = x. [para (183 (a 1) 31 (a 1 1 2)) demod (11)] given #665 (wt=19): 4263 ((C ' v x) ' v (x v (C v (D v (x v (C ' v x) ')))) ') ' = x. [para (191 (a 1) 12 (a 1 1 2)) demod (11)] given #666 (wt=28): 227 ((x v y) ' v (x v ((y v z) ' v (y v ((C v (D v z)) ' v (z v C ') ')) ')) ') ' = x. [para (65 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #667 (wt=19): 4275 ((C ' v x) ' v (C v (x v (D v (x v (C ' v x) ')))) ') ' = x. [para (191 (a 1) 31 (a 1 1 2)) demod (11)] given #668 (wt=19): 4278 ((C ' v x) ' v (D v (x v (x v (C v (C ' v x) ')))) ') ' = x. [para (191 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #669 (wt=19): 4285 ((C ' v x) ' v (D v (x v (C v (x v (C ' v x) ')))) ') ' = x. [para (191 (a 1) 60 (a 1 1 2)) demod (11 19 19 10 11)] given #670 (wt=19): 4293 ((C v (x v D)) ' v (x v (C ' v (x v (C v (x v D)) '))) ') ' = x. [para (298 (a 1) 12 (a 1 1 2)) demod (11)] given #671 (wt=25): 228 ((x v (C v (D v y)) ') ' v (x v (y v (y v (C ' v (C v (D v y)) ')) ')) ') ' = x. [para (65 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #672 (wt=19): 4304 ((C v (x v D)) ' v (C ' v (x v (x v (C v (x v D)) '))) ') ' = x. [para (298 (a 1) 31 (a 1 1 2)) demod (11)] given #673 (wt=19): 4384 ((C ' v x) ' v (x v (C v (x v (D v (C ' v x) ')))) ') ' = x. [para (302 (a 1) 12 (a 1 1 2)) demod (11)] given #674 (wt=19): 4395 ((C ' v x) ' v (C v (x v (x v (D v (C ' v x) ')))) ') ' = x. [para (302 (a 1) 31 (a 1 1 2)) demod (11)] given #675 (wt=19): 4398 ((C ' v x) ' v (x v (D v (x v (C v (C ' v x) ')))) ') ' = x. [para (302 (a 1) 37 (a 1 1 2)) demod (11 19 19 10 11)] given #676 (wt=29): 229 (((x v y) ' v ((x v ((y v z) ' v (y v z ') ')) ' v u)) ' v (u v x) ') ' = u. [para (25 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #677 (wt=19): 5042 (((C v D ') ' v x) ' v (C v (x v (C v (C v D ') ') ')) ') ' = x. [para (134 (a 1) 549 (a 1 1 1 1 1))] given #678 (wt=19): 5043 (((D v C ') ' v x) ' v (D v (x v (C v (D v C ') ') ')) ') ' = x. [para (155 (a 1) 549 (a 1 1 1 1 1))] given #679 (wt=19): 5566 (C v (C v (C v (C ' v (C ' v ((D v x) ' v (D v x ') '))))) ') ' = C '. [para (1590 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #680 (wt=19): 5581 (C ' v (C v (C v (C ' v ((D v D) ' v (D v (C ' v (D v C ') ')) ')))) ') ' = C. [para (89 (a 1) 1590 (a 1 1 2 1 2 2 2 2 1 2)) demod (11)] given #681 (wt=26): 230 (x v (x v ((y v z) ' v ((y v z ') ' v (x v y) '))) ') ' = (x v y) '. [para (25 (a 1) 23 (a 1 1 2)) demod (10 10 11)] given #682 (wt=19): 5768 (C v (C v (C v (C ' v (C ' v ((x v D) ' v (D v x ') '))))) ') ' = C '. [para (1833 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #683 (wt=19): 5880 (C v (C v (C v (C v (C ' v (C ' v (C ' v (C ' v (D v C ') '))))))) ') ' = C '. [para (1873 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #684 (wt=19): 5910 (D v (D v (D v (D v (C ' v (C ' v (C ' v (C ' v (C v D ') '))))))) ') ' = C '. [para (1893 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #685 (wt=19): 6693 (C v (D v (C v (D v (C ' v (D v ((D v C ') ' v (D v C ') ')) '))) ')) ' = C '. [para (6619 (a 1) 46 (a 1 1 2 2 1 2 2 2)) demod (11 6619)] given #686 (wt=32): 231 (x v ((y v x) ' v (((x v y ') ' v z) ' v ((x v y ') ' v z ') ')) ') ' = (y v x) '. [para (23 (a 1) 25 (a 1 1 1))] given #687 (wt=19): 6764 (D v (D v ((D v C ') ' v (D v (D v (C ' v (C ' v (D v C ') ')))) '))) ' = C '. [para (3674 (a 1) 12 (a 1 1 2)) demod (19 19 11 10 10)] given #688 (wt=19): 6870 (C v (C v (C ' v (C v (D v (C v (D v (D v (D v C ') ')) ') ')) ')) ') ' = C '. [para (3669 (a 1) 67 (a 1 1 1)) demod (11 10 11 3669 11 19)] low water: id=9718, wt=28 given #689 (wt=19): 6903 ((x v C) ' v (x v (C ' v (C v (D v (D v C ') ') ') ')) ') ' = x. [para (6810 (a 1) 25 (a 1 1 2 1 2 1))] given #690 (wt=19): 6911 (C ' v (D v (C ' v ((D v C ') ' v (C v D ') '))) ') ' = D v (D v C ') '. [para (6810 (a 1) 133 (a 1 1 2)) demod (19 10 19 11)] given #691 (wt=29): 232 ((x v y) ' v (x v ((y v z) ' v (y v ((u v z) ' v (z v u ') ')) ')) ') ' = x. [para (23 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #692 (wt=19): 6947 (C ' v (C v ((C v (D v D)) ' v (D v (C ' v (C v (D v (D v C '))) ')) ')) ') ' = C. [para (6899 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (19 11)] given #693 (wt=19): 6960 ((C v (D v (D v C '))) ' v (C v (C v (D v (D v (C v (D v (D v C '))) ')))) ') ' = C v D. [para (6899 (a 1) 160 (a 1 1 2 1 2 2 2)) demod (19 11 10 10 10 6899)] given #694 (wt=19): 6969 ((C ' v ((C v (D v (D v C ') ') ') ' v x)) ' v (x v C) ') ' = x. [para (6896 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #695 (wt=19): 6971 ((x v (C ' v (C v (D v (D v C ') ') ') ')) ' v (C v x) ') ' = x. [para (6896 (a 1) 24 (a 1 1 2 1 1))] given #696 (wt=26): 233 ((x v (y v z) ') ' v (x v (z v (z v (y ' v (y v z) ')) ')) ') ' = x. [para (23 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #697 (wt=17): 12514 (D v (C ' v (C ' v (C ' v (D ' v (D v C ') ')) ')) ') ' = C '. [para (89 (a 1) 233 (a 1 1 1))] given #698 (wt=18): 12518 (C ' v (D v (C ' v (C ' v (C ' v (D ' v (D v C ') ')) '))) ') ' = D. [para (12514 (a 1) 12 (a 1 1 2)) demod (11)] given #699 (wt=19): 6972 (C v (C v (C v (D v (D v C ') ') ') ') ') ' = (C v (D v (D v C ') ') ') '. [para (6896 (a 1) 24 (a 1 1 2)) demod (11 11)] given #700 (wt=19): 6977 ((C v x) ' v (C ' v ((C v (D v (D v C ') ') ') ' v x)) ') ' = x. [para (6896 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #701 (wt=21): 234 (D v (C ' v (((D v C ') ' v x) ' v ((D v C ') ' v x ') ')) ') ' = C '. [para (89 (a 1) 25 (a 1 1 1))] given #702 (wt=18): 12540 (D v (D v (C ' v (C v (D v ((D v C ') ' v (D v C ') '))) ')) ') ' = C '. [para (6810 (a 1) 234 (a 1 1 2 1 2 2 1 2)) demod (19 19 11 89 11 19)] given #703 (wt=19): 6978 ((x v C) ' v (C ' v ((C v (D v (D v C ') ') ') ' v x)) ') ' = x. [para (6896 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #704 (wt=19): 6979 ((x v C) ' v (C ' v (x v (C v (D v (D v C ') ') ') ')) ') ' = x. [para (6896 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #705 (wt=19): 6980 ((C v x) ' v (x v (C ' v (C v (D v (D v C ') ') ') ')) ') ' = x. [para (6896 (a 1) 128 (a 1 1 1 1 1))] given #706 (wt=23): 235 ((x v y) ' v (x v ((y v D) ' v (y v (C ' v (D v C ') ')) ')) ') ' = x. [para (89 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #707 (wt=19): 6981 (C ' v (C v (C ' v (D v (C ' v (C v (D v (D v C ') ') ') ')) ')) ') ' = C. [para (6896 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (11 13 11)] given #708 (wt=19): 6991 ((C v x) ' v (C ' v (x v (C v (D v (D v C ') ') ') ')) ') ' = x. [para (6896 (a 1) 135 (a 1 1 2 1 1)) demod (11)] given #709 (wt=19): 7216 (C ' v (C v (C ' v (D v (C ' v (C v (D ' v (D v C ') ')) ')) ')) ') ' = C. [para (6913 (a 1) 198 (a 1 1 2 1 2 2 1 2)) demod (19 6810 11)] given #710 (wt=19): 7691 ((C v (D v (D v C '))) ' v (C v (D v (C v (C v (D v (D v C '))) ') ') ') ') ' = C. [para (6938 (a 1) 12 (a 1 1 1))] given #711 (wt=24): 236 (C ' v (D v (((D v (C ' v C ')) ' v x) ' v ((D v (C ' v C ')) ' v x ') ')) ') ' = D. [para (102 (a 1) 25 (a 1 1 1))] given #712 (wt=16): 12564 (C ' v (D v (C ' v (D ' v (D v (C ' v C ')) ') ')) ') ' = D. [para (31 (a 1) 236 (a 1 1 2 1 2 1)) demod (89 11)] given #713 (wt=18): 12570 (D v (D v (C ' v (C ' v (D ' v (D v (C ' v C ')) ') '))) ') ' = C '. [para (12564 (a 1) 12 (a 1 1 2)) demod (19 11)] given #714 (wt=19): 7703 ((C v (D v (D v C '))) ' v (D v (C v (C v (C v (D v (D v C '))) ') ') ') ') ' = D. [para (6938 (a 1) 31 (a 1 1 1))] given #715 (wt=19): 7726 (C ' v (C v (D v (C v (C v (D v (D v (D v (C ' v (C ' v C '))))))) ') ') ') ' = C. [para (7128 (a 1) 12 (a 1 1 1))] given #716 (wt=25): 237 ((x v y) ' v (x v ((y v C ') ' v (y v (D v (D v (C ' v C ')) ')) ')) ') ' = x. [para (102 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #717 (wt=19): 7736 (C ' v (D v (C v (C v (C v (D v (D v (D v (C ' v (C ' v C '))))))) ') ') ') ' = D. [para (7128 (a 1) 31 (a 1 1 1))] given #718 (wt=19): 8067 (C v (D v ((D v C ') ' v (C v (D v (C ' v (D ' v (D v C ') ')))) '))) ' = C '. [para (3689 (a 1) 12 (a 1 1 2)) demod (19 19 11 10 10)] given #719 (wt=19): 8150 (D v (D v (C ' v (C v (D v (C v (D v (D v (D v (C ' v C '))))) ')) ')) ') ' = C '. [para (3980 (a 1) 12 (a 1 1 2)) demod (19 11)] given #720 (wt=19): 8186 (C v (D v (D v (C v (C v (D v (D v (D v (D v (D v (C ' v (C ' v C '))))))))) '))) ' = C '. [para (3986 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 19 19 19 11 10 10)] given #721 (wt=20): 240 ((x v C ') ' v (x v (D v (D v (D v (C ' v (C ' v C ')))) ')) ') ' = x. [para (106 (a 1) 25 (a 1 1 2 1 2 2)) demod (19 19 11)] given #722 (wt=19): 8201 (C v (D v (C v (C v (D v (D v (C ' v (C ' v (D v (D v C ') ') ')))))) ')) ' = C '. [para (4074 (a 1) 12 (a 1 1 2)) demod (19 19 19 19 11 10)] given #723 (wt=19): 8411 (C ' v (C v ((x v D) ' v (D v (D v (x ' v (x v D) '))) ')) ') ' = C. [para (87 (a 1) 198 (a 1 1 2 1 2 2)) demod (11)] given #724 (wt=19): 8481 (C v (D v (C v (D v (C ' v (C ' v (D v (C ' v (D v C ') ')) ')))) ')) ' = C '. [para (7063 (a 1) 12 (a 1 1 2)) demod (19 19 11 10)] given #725 (wt=19): 8742 (C v (C v (C v (C v (C ' v (C ' v (C ' v (D v (D v C ') ') ')))))) ') ' = C '. [para (7785 (a 1) 12 (a 1 1 2)) demod (19 19 19 11)] given #726 (wt=30): 241 (x v ((x v (C v D)) ' v (((C ' v x) ' v y) ' v ((C ' v x) ' v y ') ')) ') ' = (x v (C v D)) '. [para (66 (a 1) 25 (a 1 1 1))] given #727 (wt=19): 9177 (D v (D v (D v (C ' v (C ' v (C ' v (C v (C v (C ' v D '))) '))))) ') ' = C '. [para (9161 (a 1) 12 (a 1 1 2)) demod (19 19 11)] given #728 (wt=19): 9594 (C ' v (C v (C ' v (D v (C v (C v (D v (D v (C ' v C ')))) ') ') ')) ') ' = C. [para (6934 (a 1) 615 (a 1 1 2 1 2 1))] given #729 (wt=19): 9985 (C ' v (D v ((C v C) ' v (C v (C ' v (C v (C v (C ' v D '))) ')) ')) ') ' = D. [para (33 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #730 (wt=19): 10014 (C ' v (D v ((C v x) ' v (C v (C v (x ' v (C v x) '))) ')) ') ' = D. [para (26 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #731 (wt=28): 242 ((x v y) ' v (x v ((y v z) ' v (y v ((z v (C v D)) ' v (C ' v z) ')) ')) ') ' = x. [para (66 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #732 (wt=19): 10045 (C ' v (D v (C ' v (C v (C ' v (D v (C ' v (C v D ') ')) ')) ')) ') ' = D. [para (886 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (13 11)] given #733 (wt=19): 10118 (C ' v (D v (C ' v (C v (C v (C ' v (D v (D v (D v C ') ')) '))) ')) ') ' = D. [para (3681 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #734 (wt=19): 10121 (C ' v (D v (C ' v (C v (C ' v (D v (C ' v (D v C ') ')) ')) ')) ') ' = D. [para (3673 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (6810 11)] given #735 (wt=19): 10178 (C ' v (D v ((C v (C v D)) ' v (C v (C ' v (C v (D v (D v C '))) ')) ')) ') ' = D. [para (6899 (a 1) 9887 (a 1 1 2 1 2 2 1 2)) demod (11)] given #736 (wt=25): 243 ((x v (y v (C v D)) ') ' v (x v (y v (C ' v (y v (y v (C v D)) ')) ')) ') ' = x. [para (66 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #737 (wt=19): 10180 (C ' v (D v (C ' v (C v (D v (C v (D v (D v (C ' v C ')))) ') ') ')) ') ' = D. [para (6934 (a 1) 9887 (a 1 1 2 1 2 1))] given #738 (wt=19): 10185 (C ' v (D v (C ' v (C v (C v (C ' v (C v (D v (C v D ') ')) '))) ')) ') ' = D. [para (6797 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #739 (wt=19): 10240 (C ' v (D v ((x v C) ' v (C v (C v (x ' v (x v C) '))) ')) ') ' = D. [para (87 (a 1) 9887 (a 1 1 2 1 2 2)) demod (11)] given #740 (wt=19): 10426 (C ' v (C v (C v (C v (C v (C v (C ' v (C ' v (C ' v (C ' v D '))))))))) ') ' = C. [para (1080 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 19 19 1080)] given #741 (wt=29): 244 ((x v ((y v z) ' v (y v ((z v u) ' v (z v u ') ')) ')) ' v (y v x) ') ' = x. [para (25 (a 1) 24 (a 1 1 2 1 1))] given #742 (wt=19): 10427 (C ' v (D v (D v (D v (D v (D v (C ' v (C ' v (C ' v (C ' v C '))))))))) ') ' = D. [para (1276 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 19 19 1276)] given #743 (wt=19): 10428 (C ' v (C v (C v (C v (C ' v (C ' v ((C v (D v D)) ' v (D v C ') ')))))) ') ' = C. [para (1399 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 1399)] given #744 (wt=19): 10476 (C ' v (C v (C v (C ' v (D v (D v ((D v C ') ' v (D v C ') '))) '))) ') ' = C. [para (6665 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 6665)] given #745 (wt=19): 10583 (D v (D v (C ' v (C ' v (C v (C v (C v (C ' v (C ' v D '))))) '))) ') ' = C '. [para (35 (a 1) 9979 (a 1 1 2 1 2 2 2)) demod (11)] given #746 (wt=35): 245 (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 (25 (a 1) 24 (a 1 1 2)) demod (11 10 11)] given #747 (wt=19): 10682 (D v (D v (C ' v ((C v C ') ' v (C v (C v (D v (D v C ') '))) '))) ') ' = C '. [para (6810 (a 1) 9979 (a 1 1 2 1 2 2 2 1 2)) demod (11)] given #748 (wt=19): 10722 (D v (D v (D v (C ' v (C ' v ((C v x) ' v (C v x ') '))))) ') ' = C '. [para (9979 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 9979)] given #749 (wt=19): 10737 (C ' v (D v (D v (C ' v ((C v C) ' v (C v (C ' v (C v D ') ')) ')))) ') ' = D. [para (9982 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 9982)] given #750 (wt=19): 10751 (C ' v (D v (D v (C ' v ((C v D ') ' v (C v (C v (C v D ') ')) ')))) ') ' = D. [para (10004 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 10004)] given #751 (wt=32): 246 (x v ((x v y) ' v (((y ' v x) ' v z) ' v ((y ' v x) ' v z ') ')) ') ' = (x v y) '. [para (24 (a 1) 25 (a 1 1 1))] given #752 (wt=19): 10763 (C ' v (D v (D v (C ' v (C ' v (C v (D v (D v (D v C ') ')) ') ')))) ') ' = D. [para (10112 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 10112)] given #753 (wt=19): 10778 (D v (D v (D v (C ' v (C ' v ((x v C) ' v (C v x ') '))))) ') ' = C '. [para (10342 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 10342)] given #754 (wt=19): 10787 (C ' v (D v (D v (D v (C ' v (C ' v ((C v (C v D)) ' v (C v C ') ')))))) ') ' = D. [para (10535 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 19 10535)] given #755 (wt=19): 11036 (C ' v (C v ((D v (D v (D v (C ' v C ')))) ' v (D v (D v C ') ') ')) ') ' = C. [para (11023 (a 1) 198 (a 1 1 2 1 2 2 1 2))] given #756 (wt=29): 247 ((x v y) ' v (x v ((y v z) ' v (y v ((z v u) ' v (u ' v z) ')) ')) ') ' = x. [para (24 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #757 (wt=19): 11074 (C ' v (D v ((C v (D v (D v (C ' v C ')))) ' v (C v (D v C ') ') ')) ') ' = D. [para (11023 (a 1) 9887 (a 1 1 2 1 2 2 1 2))] given #758 (wt=19): 11121 (D v (C ' v (D v (C ' v ((D v C ') ' v (D v C ') '))) ')) ' = (D v C ') '. [para (11049 (a 1) 12 (a 1 1 2)) demod (19 19 11 10)] given #759 (wt=16): 12660 ((D v C ') ' v (D v (D v ((D v C ') ' v (D v C ') '))) ') ' = D. [para (11121 (a 1) 12 (a 1 1 1)) demod (6669)] given #760 (wt=19): 11270 (C ' v (C v (C v (C ' v (C v (D v (C v (C ' v (D v C ') ')) ')) '))) ') ' = C. [para (6842 (a 1) 12 (a 1 1 2)) demod (11)] given #761 (wt=26): 248 ((x v (y v z) ') ' v (x v (y v (z ' v (y v (y v z) ')) ')) ') ' = x. [para (24 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #762 (wt=19): 11274 (C ' v (D v (D v (C ' v (C v (D v (D v (C ' v (C v D ') ')) ')) '))) ') ' = D. [para (6847 (a 1) 12 (a 1 1 2)) demod (11)] given #763 (wt=19): 11334 (C ' v (C ' v ((D v C ') ' v (C v (D v (D v C '))) ')) ') ' = (D v C ') '. [para (6810 (a 1) 6937 (a 1 1 2)) demod (19 11)] given #764 (wt=19): 11403 (C v (C v (C v (C v (C ' v (C ' v (C ' v (C v (C v D ') ') ')))))) ') ' = C '. [para (11370 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 11370)] given #765 (wt=19): 11447 (C ' v (C v (C v (C ' v (C v (D v (C v (D v (D v C ') ') ') ')) '))) ') ' = C. [para (7002 (a 1) 12 (a 1 1 2)) demod (11)] given #766 (wt=26): 249 ((C v D ') ' v (C v (((C v (C v D ') ') ' v x) ' v ((C v (C v D ') ') ' v x ') ')) ') ' = C. [para (134 (a 1) 25 (a 1 1 1))] given #767 (wt=19): 11554 (D v (D v (D v (D v (C ' v (C ' v (C ' v (C v (D v C ') ') ')))))) ') ' = C '. [para (11521 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 11521)] given #768 (wt=19): 11599 (C ' v (C v (D v (C v (D v (D v (C ' v (C v (D v C ') ') ')))) ') ') ') ' = C. [para (11580 (a 1) 12 (a 1 1 1))] given #769 (wt=19): 11603 (C ' v (D v (C v (C v (D v (D v (C ' v (C v (D v C ') ') ')))) ') ') ') ' = D. [para (11580 (a 1) 31 (a 1 1 1))] given #770 (wt=19): 11825 (C ' v (D v (D v (C ' v (C ' v (C ' v D ') ')))) ') ' = (C ' v D ') '. [para (85 (a 1) 11024 (a 1 1 2)) demod (11 10 10 10 11)] given #771 (wt=27): 250 ((x v y) ' v (x v ((y v (C v D ') ') ' v (y v (C v (C v (C v D ') ') ')) ')) ') ' = x. [para (134 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #772 (wt=19): 11939 (C ' v (C v (C v (C v ((C ' v D ') ' v (C v (C ' v D ')) ')) ')) ') ' = C. [para (30 (a 1) 197 (a 1 1 1))] given #773 (wt=19): 11942 (C ' v (D v (D v (D v ((C ' v C ') ' v (D v (C ' v C ')) ')) ')) ') ' = D. [para (102 (a 1) 197 (a 1 1 1))] given #774 (wt=19): 11959 (C v (C v (C ' v (C v ((C v D ') ' v (C v (C ' v D ')) ')) ')) ') ' = C '. [para (30 (a 1) 199 (a 1 1 2 1 2 2 1 2)) demod (19 11 27 11 19)] given #775 (wt=19): 11967 (C v (C v (C ' v (D v ((D v (C ' v C ')) ' v (C v D ') ')) ')) ') ' = C '. [para (102 (a 1) 199 (a 1 1 2 1 2 2 1 2)) demod (11 10 11 27 11 19)] given #776 (wt=20): 251 ((x v C) ' v (x v ((C v D ') ' v (C v (C v (C v D ') ')) ')) ') ' = x. [para (134 (a 1) 25 (a 1 1 2 1 2 2)) demod (11)] given #777 (wt=19): 11976 (C v (C v (C ' v (C v (C v (D v ((C v D ') ' v (C v D ') ')))) ')) ') ' = C '. [para (147 (a 1) 199 (a 1 1 2 1 2 2)) demod (11 27 11 11 10 10 19 19 19 11 27 11 19)] given #778 (wt=19): 11977 (C v (C v (C ' v (C v (D v (D v ((D v C ') ' v (C v D ') ')))) ')) ') ' = C '. [para (3666 (a 1) 199 (a 1 1 2 1 2 2 1 2)) demod (11 10 10 10 11 27 11 19)] given #779 (wt=19): 12026 (C ' v (C v (C ' v (D v (C ' v ((D v C ') ' v (C v D ') '))) ')) ') ' = C. [para (6810 (a 1) 200 (a 1 1 1)) demod (11 6810 19 10 19)] given #780 (wt=19): 12051 (C ' v (C v (C v (C ' v (C v (C v ((C v D ') ' v (C v D ') '))) '))) ') ' = C. [para (11913 (a 1) 12 (a 1 1 2)) demod (11)] given #781 (wt=26): 252 ((D v C ') ' v (D v (((C v (D v C ') ') ' v x) ' v ((C v (D v C ') ') ' v x ') ')) ') ' = D. [para (155 (a 1) 25 (a 1 1 1))] given #782 (wt=19): 12055 (C ' v (C v (C v (C ' v (C v (D v ((D v C ') ' v (C v D ') '))) '))) ') ' = C. [para (11983 (a 1) 12 (a 1 1 2)) demod (11)] given #783 (wt=19): 12094 (C ' v (C v (C v (C ' v (C ' v (C ' v (C v (C ' v D ')) ') ')))) ') ' = C. [para (12076 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 12076)] given #784 (wt=19): 12099 ((x ' v (y v z)) ' v (y v (x v z)) ') ' = y v z. [para (11 (a 1) 406 (a 1 1))] given #785 (wt=19): 12121 ((x v (y ' v z)) ' v (y v (x v z)) ') ' = x v z. [para (11 (a 1) 407 (a 1 1))] given #786 (wt=27): 253 ((x v y) ' v (x v ((y v (D v C ') ') ' v (y v (D v (C v (D v C ') ') ')) ')) ') ' = x. [para (155 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #787 (wt=19): 12141 (D v (D v (C ' v (C v ((D v C ') ' v (C v (C ' v D ')) ')) ')) ') ' = C '. [para (89 (a 1) 205 (a 1 1 1)) demod (11 89 19 19)] given #788 (wt=19): 12152 ((x ' v (y v z)) ' v (z v (x v y)) ') ' = y v z. [para (11 (a 1) 410 (a 1 1))] given #789 (wt=19): 12171 ((x v (y ' v z)) ' v (y v (z v x)) ') ' = z v x. [para (11 (a 1) 411 (a 1 1))] given #790 (wt=19): 12190 ((x ' v (y v z)) ' v (x v (z v y)) ') ' = y v z. [para (11 (a 1) 412 (a 1 1))] given #791 (wt=30): 255 (x v ((C v (x v D)) ' v (((x v C ') ' v y) ' v ((x v C ') ' v y ') ')) ') ' = (C v (x v D)) '. [para (69 (a 1) 25 (a 1 1 1))] given #792 (wt=19): 12255 (C ' v (C v (C v (C ' v (C v (D v (C ' v (C v (C ' v D ')) '))) '))) ') ' = C. [para (448 (a 1) 204 (a 1 1 2 1 2 2)) demod (19 11 10 10 11 10)] given #793 (wt=19): 12258 ((x v (y ' v z)) ' v (z v (y v x)) ') ' = z v x. [para (11 (a 1) 451 (a 1 1 1 1)) demod (10)] given #794 (wt=19): 12334 (C ' v (C v (C v (D ' v (C v (C v (D ' v (C v (C ' v D ')) '))) '))) ') ' = C. [para (548 (a 1) 204 (a 1 1 2 1 2 2)) demod (11 11 10 10 11 10)] given #795 (wt=19): 12358 (C ' v (C v ((x v D) ' v (D v (D v (x ' v (D v x) '))) ')) ') ' = C. [para (11 (a 1) 653 (a 1 1 2 1 2 1 1))] given #796 (wt=28): 256 ((x v y) ' v (x v ((y v z) ' v (y v ((C v (z v D)) ' v (z v C ') ')) ')) ') ' = x. [para (69 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #797 (wt=19): 12359 (C ' v (C v ((D v x) ' v (D v (D v (x ' v (x v D) '))) ')) ') ' = C. [para (11 (a 1) 653 (a 1 1 2 1 2 2 1 2 2 2 1))] given #798 (wt=19): 12416 ((C v (D v x)) ' v (x v (x v (C ' v (x v (C v D)) '))) ') ' = x. [para (11 (a 1) 2253 (a 1 1 1 1)) demod (10)] given #799 (wt=19): 12417 ((x v (C v D)) ' v (x v (x v (C ' v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 2253 (a 1 1 2 1 2 2 2 1)) demod (10)] given #800 (wt=19): 12418 ((C v (x v D)) ' v (x v (x v (C ' v (x v (C v D)) '))) ') ' = x. [para (19 (a 1) 2253 (a 1 1 1 1))] given #801 (wt=25): 257 ((x v (C v (y v D)) ') ' v (x v (y v (y v (C ' v (C v (y v D)) ')) ')) ') ' = x. [para (69 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #802 (wt=19): 12419 ((x v (C v D)) ' v (x v (x v (C ' v (C v (x v D)) '))) ') ' = x. [para (19 (a 1) 2253 (a 1 1 2 1 2 2 2 1))] given #803 (wt=19): 12420 ((C v (x v D)) ' v (x v (x v (C ' v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 2280 (a 1 1 1 1 2))] given #804 (wt=19): 12421 ((C v (D v x)) ' v (x v (x v (C ' v (C v (x v D)) '))) ') ' = x. [para (11 (a 1) 2280 (a 1 1 2 1 2 2 2 1 2))] given #805 (wt=19): 12423 ((C v (D v x)) ' v (x v (C ' v (x v (x v (C v D)) '))) ') ' = x. [para (11 (a 1) 2563 (a 1 1 1 1)) demod (10)] given #806 (wt=30): 258 (x v ((C v (D v x)) ' v (((C ' v x) ' v y) ' v ((C ' v x) ' v y ') ')) ') ' = (C v (D v x)) '. [para (74 (a 1) 25 (a 1 1 1))] given #807 (wt=19): 12424 ((x v (C v D)) ' v (x v (C ' v (x v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 2563 (a 1 1 2 1 2 2 2 1)) demod (10)] given #808 (wt=19): 12425 ((C v (x v D)) ' v (x v (C ' v (x v (x v (C v D)) '))) ') ' = x. [para (19 (a 1) 2563 (a 1 1 1 1))] given #809 (wt=19): 12426 ((x v (C v D)) ' v (x v (C ' v (x v (C v (x v D)) '))) ') ' = x. [para (19 (a 1) 2563 (a 1 1 2 1 2 2 2 1))] given #810 (wt=19): 12427 ((C v (D v x)) ' v (C ' v (x v (x v (x v (C v D)) '))) ') ' = x. [para (11 (a 1) 2576 (a 1 1 1 1)) demod (10)] given #811 (wt=28): 259 ((x v y) ' v (x v ((y v z) ' v (y v ((C v (D v z)) ' v (C ' v z) ')) ')) ') ' = x. [para (74 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #812 (wt=19): 12428 ((x v (C v D)) ' v (C ' v (x v (x v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 2576 (a 1 1 2 1 2 2 2 1)) demod (10)] given #813 (wt=19): 12429 ((C v (x v D)) ' v (C ' v (x v (x v (x v (C v D)) '))) ') ' = x. [para (19 (a 1) 2576 (a 1 1 1 1))] given #814 (wt=19): 12430 ((x v (C v D)) ' v (C ' v (x v (x v (C v (x v D)) '))) ') ' = x. [para (19 (a 1) 2576 (a 1 1 2 1 2 2 2 1))] given #815 (wt=19): 12431 (C v (C v ((C v C ') ' v (C v (C ' v (C v (C v D)) ')) ')) ') ' = (C v C ') '. [para (175 (a 1) 222 (a 1 1 1)) demod (19)] given #816 (wt=25): 260 ((x v (C v (D v y)) ') ' v (x v (y v (C ' v (y v (C v (D v y)) ')) ')) ') ' = x. [para (74 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #817 (wt=19): 12434 ((C ' v x) ' v (x v (x v (C v (D v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3212 (a 1 1 1 1))] given #818 (wt=19): 12435 ((x v C ') ' v (x v (x v (C v (D v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3212 (a 1 1 2 1 2 2 2 2 1))] given #819 (wt=19): 12436 ((C ' v x) ' v (C v (D v (x v (x v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3230 (a 1 1 1 1))] given #820 (wt=19): 12437 ((x v C ') ' v (C v (D v (x v (x v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3230 (a 1 1 2 1 2 2 2 2 1))] given #821 (wt=48): 261 (x v ((x v y) ' v (((x v ((y v z) ' v (y v z ') ')) ' v u) ' v ((x v ((y v z) ' v (y v z ') ')) ' v u ') ')) ') ' = (x v y) '. [para (25 (a 1) 25 (a 1 1 1))] given #822 (wt=19): 12439 ((C ' v x) ' v (x v (C v (D v (x v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3280 (a 1 1 1 1))] given #823 (wt=19): 12440 ((x v C ') ' v (x v (C v (D v (x v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3280 (a 1 1 2 1 2 2 2 2 1))] given #824 (wt=19): 12441 ((C ' v x) ' v (C v (x v (D v (x v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3291 (a 1 1 1 1))] given #825 (wt=19): 12442 ((x v C ') ' v (C v (x v (D v (x v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3291 (a 1 1 2 1 2 2 2 2 1))] given #826 (wt=37): 262 ((x v y) ' v (x v ((y v z) ' v (y v ((z v u) ' v (z v ((u v v) ' v (u v v ') ')) ')) ')) ') ' = x. [para (25 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #827 (wt=19): 12443 ((C ' v x) ' v (D v (x v (x v (C v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3294 (a 1 1 1 1))] given #828 (wt=19): 12444 ((x v C ') ' v (D v (x v (x v (C v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3294 (a 1 1 2 1 2 2 2 2 1))] given #829 (wt=19): 12445 ((C ' v x) ' v (D v (x v (C v (x v (x v C ') ')))) ') ' = x. [para (11 (a 1) 3301 (a 1 1 1 1))] given #830 (wt=19): 12446 ((x v C ') ' v (D v (x v (C v (x v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 3301 (a 1 1 2 1 2 2 2 2 1))] given #831 (wt=34): 263 ((x v (y v z) ') ' v (x v (y v (y v ((y v z) ' v ((z v u) ' v (z v u ') '))) ')) ') ' = x. [para (25 (a 1) 25 (a 1 1 2 1 2 2)) demod (19 11)] given #832 (wt=19): 12454 ((C ' v x) ' v (x v (C v (x v (D v (x v C ') ')))) ') ' = x. [para (11 (a 1) 4202 (a 1 1 1 1))] given #833 (wt=19): 12455 ((x v C ') ' v (x v (C v (x v (D v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 4202 (a 1 1 2 1 2 2 2 2 1))] given #834 (wt=19): 12456 ((C ' v x) ' v (C v (x v (x v (D v (x v C ') ')))) ') ' = x. [para (11 (a 1) 4213 (a 1 1 1 1))] given #835 (wt=19): 12457 ((x v C ') ' v (C v (x v (x v (D v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 4213 (a 1 1 2 1 2 2 2 2 1))] given #836 (wt=20): 265 ((x v y) ' v (x v ((y v C ') ' v (C v (D v y)) ')) ') ' = x. [para (75 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #837 (wt=19): 12460 ((C ' v x) ' v (x v (D v (x v (C v (x v C ') ')))) ') ' = x. [para (11 (a 1) 4216 (a 1 1 1 1))] given #838 (wt=19): 12461 ((x v C ') ' v (x v (D v (x v (C v (C ' v x) ')))) ') ' = x. [para (11 (a 1) 4216 (a 1 1 2 1 2 2 2 2 1))] given #839 (wt=19): 12462 ((C v (x v D)) ' v (x v (C ' v (x v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 4230 (a 1 1 1 1 2))] given #840 (wt=19): 12463 ((C v (D v x)) ' v (x v (C ' v (x v (C v (x v D)) '))) ') ' = x. [para (11 (a 1) 4230 (a 1 1 2 1 2 2 2 1 2))] given #841 (wt=26): 270 ((x v (y v z)) ' v (x v (y v ((z v C ') ' v (C v (D v z)) '))) ') ' = x v y. [para (75 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #842 (wt=19): 12464 ((C v (x v D)) ' v (C ' v (x v (x v (C v (D v x)) '))) ') ' = x. [para (11 (a 1) 4246 (a 1 1 1 1 2))] given #843 (wt=19): 12465 ((C v (D v x)) ' v (C ' v (x v (x v (C v (x v D)) '))) ') ' = x. [para (11 (a 1) 4246 (a 1 1 2 1 2 2 2 1 2))] given #844 (wt=19): 12466 (D v (D v ((D v C ') ' v (D v (C ' v (C v (D v D)) ')) ')) ') ' = (D v C ') '. [para (175 (a 1) 228 (a 1 1 1)) demod (19)] given #845 (wt=19): 12525 (D v (D v (C ' v (D v ((D v C ') ' v (D v (C ' v C ')) ')) ')) ') ' = C '. [para (102 (a 1) 234 (a 1 1 2 1 2 2 1 2)) demod (19 11 89 11 19)] given #846 (wt=20): 272 (((x v C ') ' v ((C v (D v x)) ' v y)) ' v (y v x) ') ' = y. [para (75 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #847 (wt=19): 12553 (C ' v (D v (D v (C ' v (C v (D v ((D v C ') ' v (D v C ') '))) '))) ') ' = D. [para (12540 (a 1) 12 (a 1 1 2)) demod (11)] given #848 (wt=19): 12567 (C ' v (D v (D v (C ' v (C v (D v (C ' v (D v (C ' v C ')) '))) '))) ') ' = D. [para (448 (a 1) 236 (a 1 1 2 1 2 2)) demod (11 10 10 11 10)] given #849 (wt=19): 12580 (C ' v (D v (D v (C ' v (C ' v (D ' v (D v (C ' v C ')) ') ')))) ') ' = D. [para (12564 (a 1) 132 (a 1 1 2 1 2 2)) demod (11 19 19 12564)] given #850 (wt=19): 12617 (C ' v (D v ((x v C) ' v (C v (C v (x ' v (C v x) '))) ')) ') ' = D. [para (11 (a 1) 10014 (a 1 1 2 1 2 1 1))] given #851 (wt=20): 273 ((x v ((y v C ') ' v (C v (D v y)) ')) ' v (y v x) ') ' = x. [para (75 (a 1) 24 (a 1 1 2 1 1))] given #852 (wt=14): 12823 (C v (D v ((D v C ') ' v (C v (C ' v D ')) '))) ' = C '. [para (6236 (a 1) 273 (a 1 1 2)) demod (11 89 6810 11 10 11 12528) flip a] given #853 (wt=14): 12824 (D v (D v ((D v C ') ' v (D v (C ' v C ')) '))) ' = C '. [para (6522 (a 1) 273 (a 1 1 2)) demod (11 89 6810 11 10 11 12532) flip a] given #854 (wt=17): 12825 (C ' v (C v (D v ((D v C ') ' v (C v (C ' v D ')) ')) ') ') ' = C. [para (12823 (a 1) 12 (a 1 1 1))] given #855 (wt=18): 12827 (C ' v (C v (D v ((D v C ') ' v (C v (C ' v D ')) ') ')) ') ' = C v D. [para (12823 (a 1) 22 (a 1 1 1))] given #856 (wt=30): 274 (x v ((x v C ') ' v (((C v (D v x)) ' v y) ' v ((C v (D v x)) ' v y ') ')) ') ' = (x v C ') '. [para (75 (a 1) 25 (a 1 1 1))] given #857 (wt=18): 12850 (C ' v (D v (D v ((D v C ') ' v (D v (C ' v C ')) ') ')) ') ' = D v D. [para (12824 (a 1) 22 (a 1 1 1))] given #858 (wt=19): 12618 (C ' v (D v ((C v x) ' v (C v (C v (x ' v (x v C) '))) ')) ') ' = D. [para (11 (a 1) 10014 (a 1 1 2 1 2 2 1 2 2 2 1))] given #859 (wt=19): 12684 ((C v D ') ' v (C v (C v (C v (C v (D ' v (C v (C v D ') ') '))) ')) ') ' = C. [para (85 (a 1) 249 (a 1 1 2 1 2 2)) demod (11 11 10 10 11)] given #860 (wt=19): 12715 ((D v C ') ' v (C v (D v (C v (D v (C ' v (C v (D v C ') ') '))) ')) ') ' = D. [para (85 (a 1) 252 (a 1 1 2 1 2 2)) demod (11 11 10 10 11 19)] given #861 (wt=28): 275 ((x v y) ' v (x v ((y v z) ' v (y v ((z v C ') ' v (C v (D v z)) ')) ')) ') ' = x. [para (75 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #862 (wt=19): 12830 (C v (C v (C ' v (D v ((D v C ') ' v (C v (C ' v D ')) ')) ')) ') ' = C '. [para (12823 (a 1) 26 (a 1 1 2 1 2 2)) demod (11 12823)] given #863 (wt=20): 280 ((D v ((D v (D v (C ' v (C ' v C ')))) ' v x)) ' v (x v C ') ') ' = x. [para (111 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #864 (wt=20): 281 ((x v (D v (D v (D v (C ' v (C ' v C ')))) ')) ' v (C ' v x) ') ' = x. [para (111 (a 1) 24 (a 1 1 2 1 1))] given #865 (wt=20): 286 ((x v y) ' v (x v ((C ' v y) ' v (y v (C v D)) ')) ') ' = x. [para (115 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #866 (wt=25): 276 ((x v (y v C ') ') ' v (x v (y v (C v (D v (y v (y v C ') '))) ')) ') ' = x. [para (75 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 10 11)] given #867 (wt=20): 292 (((C ' v x) ' v ((x v (C v D)) ' v y)) ' v (y v x) ') ' = y. [para (115 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #868 (wt=20): 293 ((x v ((C ' v y) ' v (y v (C v D)) ')) ' v (y v x) ') ' = x. [para (115 (a 1) 24 (a 1 1 2 1 1))] given #869 (wt=20): 297 ((x v y) ' v (x v ((C v (y v D)) ' v (C ' v y) ')) ') ' = x. [para (119 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #870 (wt=20): 300 (((C v (x v D)) ' v ((C ' v x) ' v y)) ' v (y v x) ') ' = y. [para (119 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #871 (wt=26): 278 ((x v (y v C ')) ' v (x v (y v (D v (D v (D v (C ' v (C ' v C ')))) '))) ') ' = x v y. [para (111 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #872 (wt=20): 301 ((x v ((C v (y v D)) ' v (C ' v y) ')) ' v (y v x) ') ' = x. [para (119 (a 1) 24 (a 1 1 2 1 1))] given #873 (wt=20): 307 ((x v y) ' v (x v (x v (y ' v (x v y) '))) ') ' = x. [para (26 (a 1) 12 (a 1 1 2)) demod (11)] given #874 (wt=20): 346 (((C v D ') ' v ((C v (C v (C v D ') ')) ' v x)) ' v (x v C) ') ' = x. [para (164 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #875 (wt=20): 347 ((x v ((C v D ') ' v (C v (C v (C v D ') ')) ')) ' v (C v x) ') ' = x. [para (164 (a 1) 24 (a 1 1 2 1 1))] given #876 (wt=23): 279 (C ' v (D ' v (D v (D v (C ' v (C ' v C ')))) ') ') ' = (D v (D v (C ' v (C ' v C ')))) '. [para (111 (a 1) 23 (a 1 1 1)) demod (11)] given #877 (wt=20): 362 ((x v y) ' v (x v ((y v C ') ' v (C v (y v D)) ')) ') ' = x. [para (175 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #878 (wt=20): 364 (((x v C ') ' v ((C v (x v D)) ' v y)) ' v (y v x) ') ' = y. [para (175 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #879 (wt=20): 365 ((x v ((y v C ') ' v (C v (y v D)) ')) ' v (y v x) ') ' = x. [para (175 (a 1) 24 (a 1 1 2 1 1))] given #880 (wt=20): 384 ((x v y) ' v (x v ((C ' v y) ' v (C v (y v D)) ')) ') ' = x. [para (288 (a 1) 12 (a 1 1 2 1 2)) demod (11)] given #881 (wt=30): 282 (C ' v (D v (((D v (D v (C ' v (C ' v C ')))) ' v x) ' v ((D v (D v (C ' v (C ' v C ')))) ' v x ') ')) ') ' = D. [para (111 (a 1) 25 (a 1 1 1))] given #882 (wt=19): 12890 (C ' v (D v (C ' v (D ' v (D v (D v (C ' v (C ' v C ')))) ') ')) ') ' = D. [para (11028 (a 1) 282 (a 1 1 2 1 2 1)) demod (89 11)] given #883 (wt=20): 386 (((C ' v x) ' v ((C v (x v D)) ' v y)) ' v (y v x) ') ' = y. [para (288 (a 1) 23 (a 1 1 2 1 2)) demod (10)] given #884 (wt=20): 387 ((x v ((C ' v y) ' v (C v (y v D)) ')) ' v (y v x) ') ' = x. [para (288 (a 1) 24 (a 1 1 2 1 1))] given #885 (wt=20): 415 ((x v y) ' v ((x v (C v D)) ' v ((x v C ') ' v y)) ') ' = y. [para (28 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #886 (wt=28): 283 ((x v y) ' v (x v ((y v C ') ' v (y v (D v (D v (D v (C ' v (C ' v C ')))) ')) ')) ') ' = x. [para (111 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #887 (wt=20): 416 ((C ' v x) ' v (C v ((C v (C v (C ' v (C ' v D ')))) ' v x)) ') ' = x. [para (35 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #888 (wt=20): 417 ((x v y) ' v ((C v (D v x)) ' v ((x v C ') ' v y)) ') ' = y. [para (65 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #889 (wt=20): 423 ((x v y) ' v ((x v (C v D)) ' v ((C ' v x) ' v y)) ') ' = y. [para (66 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #890 (wt=20): 429 ((x v y) ' v ((C v (x v D)) ' v ((x v C ') ' v y)) ') ' = y. [para (69 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #891 (wt=21): 284 ((x v D) ' v (x v (C ' v (D v (D v (D v (C ' v (C ' v C '))))) ')) ') ' = x. [para (111 (a 1) 25 (a 1 1 2 1 2 2)) demod (11)] given #892 (wt=20): 430 ((x v y) ' v ((C v (D v x)) ' v ((C ' v x) ' v y)) ') ' = y. [para (74 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #893 (wt=20): 435 ((x v y) ' v ((x v C ') ' v ((C v (D v x)) ' v y)) ') ' = y. [para (75 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #894 (wt=20): 436 ((C ' v x) ' v (D v ((D v (D v (C ' v (C ' v C ')))) ' v x)) ') ' = x. [para (111 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #895 (wt=20): 437 ((x v y) ' v ((C ' v x) ' v ((x v (C v D)) ' v y)) ') ' = y. [para (115 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #896 (wt=26): 291 ((x v (y v z)) ' v (x v (y v ((C ' v z) ' v (z v (C v D)) '))) ') ' = x v y. [para (115 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #897 (wt=20): 438 ((x v y) ' v ((C v (x v D)) ' v ((C ' v x) ' v y)) ') ' = y. [para (119 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #898 (wt=20): 441 ((C v x) ' v ((C v D ') ' v ((C v (C v (C v D ') ')) ' v x)) ') ' = x. [para (164 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #899 (wt=20): 443 ((x v y) ' v ((x v C ') ' v ((C v (x v D)) ' v y)) ') ' = y. [para (175 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #900 (wt=20): 445 ((x v y) ' v ((C ' v x) ' v ((C v (x v D)) ' v y)) ') ' = y. [para (288 (a 1) 84 (a 1 1 2 1 1)) demod (10 11)] given #901 (wt=30): 294 (x v ((C ' v x) ' v (((x v (C v D)) ' v y) ' v ((x v (C v D)) ' v y ') ')) ') ' = (C ' v x) '. [para (115 (a 1) 25 (a 1 1 1))] given #902 (wt=20): 459 ((x v y) ' v ((y v (C v D)) ' v ((y v C ') ' v x)) ') ' = x. [para (28 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #903 (wt=20): 460 ((x v C ') ' v (C v ((C v (C v (C ' v (C ' v D ')))) ' v x)) ') ' = x. [para (35 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #904 (wt=20): 461 ((x v y) ' v ((C v (D v y)) ' v ((y v C ') ' v x)) ') ' = x. [para (65 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #905 (wt=20): 467 ((x v y) ' v ((y v (C v D)) ' v ((C ' v y) ' v x)) ') ' = x. [para (66 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #906 (wt=28): 295 ((x v y) ' v (x v ((y v z) ' v (y v ((C ' v z) ' v (z v (C v D)) ')) ')) ') ' = x. [para (115 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #907 (wt=20): 472 ((x v y) ' v ((C v (y v D)) ' v ((y v C ') ' v x)) ') ' = x. [para (69 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #908 (wt=20): 473 ((x v y) ' v ((C v (D v y)) ' v ((C ' v y) ' v x)) ') ' = x. [para (74 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #909 (wt=20): 478 ((x v y) ' v ((y v C ') ' v ((C v (D v y)) ' v x)) ') ' = x. [para (75 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #910 (wt=20): 479 ((x v C ') ' v (D v ((D v (D v (C ' v (C ' v C ')))) ' v x)) ') ' = x. [para (111 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #911 (wt=25): 296 ((x v (C ' v y) ') ' v (x v (y v (y v (C v (D v (C ' v y) '))) ')) ') ' = x. [para (115 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 10 11)] given #912 (wt=20): 480 ((x v y) ' v ((C ' v y) ' v ((y v (C v D)) ' v x)) ') ' = x. [para (115 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #913 (wt=20): 481 ((x v y) ' v ((C v (y v D)) ' v ((C ' v y) ' v x)) ') ' = x. [para (119 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #914 (wt=20): 485 ((x v C) ' v ((C v D ') ' v ((C v (C v (C v D ') ')) ' v x)) ') ' = x. [para (164 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #915 (wt=20): 487 ((x v y) ' v ((y v C ') ' v ((C v (y v D)) ' v x)) ') ' = x. [para (175 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #916 (wt=26): 299 ((x v (y v z)) ' v (x v (y v ((C v (z v D)) ' v (C ' v z) '))) ') ' = x v y. [para (119 (a 1) 22 (a 1 1 2 1 2 2)) demod (11)] given #917 (wt=20): 489 ((x v y) ' v ((C ' v y) ' v ((C v (y v D)) ' v x)) ') ' = x. [para (288 (a 1) 85 (a 1 1 1 1 2)) demod (10)] given #918 (wt=20): 509 ((x v y) ' v ((y v (C v D)) ' v (x v (y v C ') ')) ') ' = x. [para (28 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #919 (wt=20): 510 ((x v C ') ' v (C v (x v (C v (C v (C ' v (C ' v D ')))) ')) ') ' = x. [para (35 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #920 (wt=20): 511 ((x v y) ' v ((C v (D v y)) ' v (x v (y v C ') ')) ') ' = x. [para (65 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #921 (wt=30): 303 (x v ((C v (x v D)) ' v (((C ' v x) ' v y) ' v ((C ' v x) ' v y ') ')) ') ' = (C v (x v D)) '. [para (119 (a 1) 25 (a 1 1 1))] given #922 (wt=20): 517 ((x v y) ' v ((y v (C v D)) ' v (x v (C ' v y) ')) ') ' = x. [para (66 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #923 (wt=20): 523 ((x v y) ' v ((C v (y v D)) ' v (x v (y v C ') ')) ') ' = x. [para (69 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #924 (wt=20): 524 ((x v y) ' v ((C v (D v y)) ' v (x v (C ' v y) ')) ') ' = x. [para (74 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #925 (wt=20): 529 ((x v y) ' v ((y v C ') ' v (x v (C v (D v y)) ')) ') ' = x. [para (75 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #926 (wt=28): 304 ((x v y) ' v (x v ((y v z) ' v (y v ((C v (z v D)) ' v (C ' v z) ')) ')) ') ' = x. [para (119 (a 1) 25 (a 1 1 2 1 2 2 1 2)) demod (11)] given #927 (wt=20): 530 ((x v C ') ' v (D v (x v (D v (D v (C ' v (C ' v C ')))) ')) ') ' = x. [para (111 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #928 (wt=20): 531 ((x v y) ' v ((C ' v y) ' v (x v (y v (C v D)) ')) ') ' = x. [para (115 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #929 (wt=20): 532 ((x v y) ' v ((C v (y v D)) ' v (x v (C ' v y) ')) ') ' = x. [para (119 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #930 (wt=20): 535 ((x v C) ' v ((C v D ') ' v (x v (C v (C v (C v D ') ')) ')) ') ' = x. [para (164 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #931 (wt=25): 305 ((x v (C v (y v D)) ') ' v (x v (y v (C ' v (y v (C v (y v D)) ')) ')) ') ' = x. [para (119 (a 1) 25 (a 1 1 2 1 2 2)) demod (11 10 11)] given #932 (wt=20): 537 ((x v y) ' v ((y v C ') ' v (x v (C v (y v D)) ')) ') ' = x. [para (175 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #933 (wt=20): 539 ((x v y) ' v ((C ' v y) ' v (x v (C v (y v D)) ')) ') ' = x. [para (288 (a 1) 31 (a 1 1 2 1 2)) demod (11)] given #934 (wt=20): 557 ((x v y) ' v (y v ((x v (C v