============================== Prover9 ===============================
Prover9 (32) version August-2006A, August 2006.
Process 11561 was started by mccune on cleo.thornwood,
Sat Aug 12 21:08:38 2006
The command was "/home/mccune/bin/prover9 -f dn1.in".
============================== end of head ===========================

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

% Reading from file dn1.in

assign(new_constants,1).

formulas(sos).
(((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).
B v A != A v B | (A v B) v C != A v (B v C) | ((A v B)' v (A' v B)')' != B # answer(robbins_basis).
end_of_list.

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

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

% Formulas that are not ordinary clauses:

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

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

% Clauses before input processing:

formulas(usable).
end_of_list.

formulas(sos).
(((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).  [assumption].
B v A != A v B | (A v B) v C != A v (B v C) | ((A v B)' v (A' v B)')' != B # answer(robbins_basis).  [assumption].
end_of_list.

formulas(demodulators).
end_of_list.

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

No predicates eliminated.

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

Auto_denials:  (no changes).

Term ordering decisions:
Relation symbol precedence:  lex([ = ]).
Function symbol precedence:  lex([ A, B, C, v, ' ]).
After inverse_order:  (no changes).
Unfolding symbols: (none).

Auto_inference settings:
  % set(paramodulation).  % (positive equality literals)
    % set(paramodulation) -> set(back_demod).
  % set(hyper_resolution).  % (nonunit Horn with equality)
  % set(neg_ur_resolution).  % (nonunit Horn with equality)
  % assign(para_lit_limit, 3).  % (nonunit Horn with equality)

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

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

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

% Clauses after input processing:

formulas(usable).
end_of_list.

formulas(sos).
1 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).  [assumption].
2 B v A != A v B | (A v B) v C != A v (B v C) | ((A v B)' v (A' v B)')' != B # answer(robbins_basis).  [assumption].
end_of_list.

formulas(demodulators).
1 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).  [assumption].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=22): 1 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).  [assumption].

given #2 (I,wt=31): 2 B v A != A v B | (A v B) v C != A v (B v C) | ((A v B)' v (A' v B)')' != B # answer(robbins_basis).  [assumption].

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

given #4 (T,wt=11): 12 ((x v x')' v x)' = x'.  [para(1(a,1),7(a,1,1,1,1,1))].

given #5 (T,wt=17): 15 (x' v (x v (x' v (x v y)')')')' = x.  [para(12(a,1),1(a,1,1,1))].

given #6 (A,wt=25): 3 ((x v y)' v (((z v u)' v x)' v (y' v (y v v)')')')' = y.  [para(1(a,1),1(a,1,1,1,1,1))].

given #7 (F,wt=10): 39 (x' v (x v x)')' = x.  [para(15(a,1),15(a,1,1,2,1,2))].

given #8 (F,wt=15): 27 (((x v y)' v z)' v (x v z)')' = z.  [para(15(a,1),1(a,1,1,2,1,2))].

given #9 (T,wt=13): 87 ((x v y)' v (x' v y)')' = y.  [para(15(a,1),27(a,1,1,1,1,1))].

given #10 (T,wt=13): 109 (((x v x') v x)' v x')' = x.  [para(12(a,1),87(a,1,1,2))].

given #11 (A,wt=49): 4 (x v ((y v z)' v ((y v (x' v (x v u)')')'' v ((y v (x' v (x v u)')')' v v)')')')' = (y v (x' v (x v u)')')'.  [para(1(a,1),1(a,1,1,1))].

given #12 (F,wt=18): 95 B v A != A v B | (A v B) v C != A v (B v C) # answer(robbins_basis).  [back_rewrite(2),rewrite(87(29)),xx(c)].

given #13 (F,wt=14): 139 (x v ((x v x') v x')')' = x'.  [para(109(a,1),27(a,1,1,1))].

given #14 (T,wt=8): 196 (x' v x')' = x.  [para(139(a,1),15(a,1,1,2,1,2,1,2)),rewrite(119(9))].

given #15 (T,wt=9): 221 (x v x')' v x = x.  [para(12(a,1),196(a,1,1,1)),rewrite(12(6),196(4)),flip(a)].

given #16 (A,wt=28): 8 (x' v ((((x'' v y)' v x)' v z)' v (x' v (x v u)')')')' = x.  [para(7(a,1),1(a,1,1,1))].

given #17 (F,wt=9): 225 (x'' v x)' = x'.  [para(196(a,1),39(a,1,1,2))].

given #18 (F,wt=9): 245 x'' v x'' = x.  [back_rewrite(1),rewrite(216(12),240(2),240(4))].

given #19 (T,wt=7): 273 x'' v x = x.  [para(225(a,1),245(a,1,1,1)),rewrite(225(6),245(5)),flip(a)].

given #20 (T,wt=10): 240 (x v x)' = x' v x'.  [para(196(a,1),196(a,1,1,1)),rewrite(196(4))].

given #21 (A,wt=56): 10 ((((((((x' v (x v y)')''' v z)' v (x' v (x v y)')')' v u)' v (x' v (x v y)')'')' v v)' v x)' v (x' v (x v y)')'')' = x.  [para(7(a,1),1(a,1,1,2))].

given #22 (F,wt=9): 277 x v (x v x) = x v x.  [para(240(a,1),273(a,1,1,1)),rewrite(240(4),245(5))].

given #23 (F,wt=12): 239 x v ((x v x') v x')' = x.  [para(139(a,1),196(a,1,1,1)),rewrite(139(8),196(4)),flip(a)].

given #24 (T,wt=13): 200 ((x' v y)' v (x v y)')' = y.  [para(139(a,1),27(a,1,1,1,1,1))].

given #25 (T,wt=11): 292 (x' v (x' v x)')' = x.  [para(273(a,1),200(a,1,1,1,1))].

given #26 (A,wt=38): 18 (((((x' v (x v y)')' v (x' v (x v y)')'')' v z)' v x)' v (x' v (x v y)')'')' = x.  [para(12(a,1),1(a,1,1,2))].

given #27 (F,wt=11): 295 (x v (x v x')')' = x'.  [para(240(a,1),200(a,1,1,1)),rewrite(245(5))].

given #28 (F,wt=9): 315 x v (x v x')' = x.  [para(295(a,1),245(a,1,1,1)),rewrite(295(7),245(5)),flip(a)].

given #29 (T,wt=13): 230 (x v (x'' v x')')' = x'.  [para(196(a,1),87(a,1,1,1))].

given #30 (T,wt=11): 319 x v (x'' v x')' = x.  [para(230(a,1),245(a,1,1,1)),rewrite(230(9),245(5)),flip(a)].

given #31 (A,wt=20): 23 ((x v y)' v (x' v (y' v (y v z)')')')' = y.  [para(15(a,1),1(a,1,1,1,1,1))].

given #32 (F,wt=13): 287 (x' v ((x v x') v x)')' = x.  [para(221(a,1),200(a,1,1,1,1))].

given #33 (F,wt=13): 293 ((x''' v x)' v x')' = x.  [para(273(a,1),200(a,1,1,2,1))].

given #34 (T,wt=14): 296 ((x' v x)' v (x' v x'))' = x.  [para(240(a,1),200(a,1,1,2))].

given #35 (T,wt=13): 351 ((x'' v x')' v x)' = x'.  [para(245(a,1),296(a,1,1,2))].

given #36 (A,wt=66): 24 ((x v y) v (x v (((x v y) v ((x v y)' v ((x v y) v z)')')'' v (((x v y) v ((x v y)' v ((x v y) v z)')')' v u)')')')' = ((x v y) v ((x v y)' v ((x v y) v z)')')'.  [para(15(a,1),1(a,1,1,1))].

given #37 (F,wt=11): 355 (x'' v x')' v x = x.  [para(351(a,1),245(a,1,1,1)),rewrite(351(9),245(5)),flip(a)].

given #38 (F,wt=14): 306 x' v (x' v x)' = x' v x'.  [para(292(a,1),245(a,1,1,1)),rewrite(292(7)),flip(a)].

given #39 (T,wt=14): 341 (((x' v x) v x')' v x)' = x'.  [para(23(a,1),23(a,1,1,2))].

given #40 (T,wt=12): 363 ((x' v x) v x')' v x = x.  [para(341(a,1),245(a,1,1,1)),rewrite(341(9),245(5)),flip(a)].

given #41 (A,wt=18): 31 ((((x' v x)' v y)' v x')' v x)' = x'.  [para(15(a,1),7(a,1,1,1,1,1,1,1,1,1))].

given #42 (F,wt=15): 107 (x' v ((x v x')'' v x)')' = x.  [para(12(a,1),87(a,1,1,1))].

given #43 (F,wt=14): 373 x v (x v (x' v x'))' = x v x.  [para(107(a,1),306(a,1,1)),rewrite(371(8),240(4),245(5),371(8),371(14),240(10),245(11),371(14),240(10),245(11))].

given #44 (T,wt=15): 118 ((x v y)' v ((z v x)' v y)')' = y.  [para(87(a,1),27(a,1,1,1,1,1))].

given #45 (T,wt=11): 379 ((x' v x)' v x')' = x.  [para(221(a,1),118(a,1,1,2,1))].

given #46 (A,wt=18): 32 ((((x'' v y)' v x) v x')' v x)' = x'.  [para(15(a,1),7(a,1,1,1,1,1))].

given #47 (F,wt=14): 408 (x' v x)' v x' = x' v x'.  [para(379(a,1),245(a,1,1,1)),rewrite(379(7)),flip(a)].

given #48 (F,wt=15): 228 (((x' v y)' v x')' v x)' = x'.  [para(196(a,1),27(a,1,1,2))].

given #49 (T,wt=5): 429 x v x = x.  [back_rewrite(373),rewrite(418(3),315(4)),flip(a)].

given #50 (T,wt=5): 430 x'' = x.  [back_rewrite(372),rewrite(429(3),429(2),429(4),429(6),371(8),429(3),429(3))].

given #51 (A,wt=22): 40 ((x v y)' v ((z v x)' v (y' v (y v u)')')')' = y.  [para(3(a,1),1(a,1,1,1,1,1))].

given #52 (F,wt=11): 422 (x' v x)' v x' = x'.  [back_rewrite(408),rewrite(418(8))].

given #53 (F,wt=11): 440 x' v (x' v x)' = x'.  [back_rewrite(306),rewrite(429(8))].

given #54 (T,wt=13): 416 ((x' v y)' v x')' v x = x.  [para(228(a,1),245(a,1,1,1)),rewrite(228(10),245(5)),flip(a)].

given #55 (T,wt=13): 425 (x' v ((y v x)' v x)')' = x.  [back_rewrite(383),rewrite(418(3))].

given #56 (A,wt=29): 45 (((x v (y' v (y v z)')')' v u)' v (y v (u' v (u v v)')')')' = u.  [para(1(a,1),3(a,1,1,2,1,1))].

given #57 (F,wt=13): 433 x' v ((x v x') v x)' = x'.  [back_rewrite(343),rewrite(429(9))].

given #58 (F,wt=12): 585 x v ((x' v x) v x')' = x.  [para(430(a,1),433(a,1,1)),rewrite(430(3),430(8))].

given #59 (T,wt=13): 441 x' v ((x' v x) v x)' = x'.  [back_rewrite(299),rewrite(429(3),429(4),429(9))].

given #60 (T,wt=13): 442 (x' v y)' v (x v y)' = y'.  [back_rewrite(289),rewrite(429(9))].

given #61 (A,wt=25): 77 (((((x' v y)' v (x v z)')' v u)' v x)' v (x v z)')' = x.  [para(27(a,1),1(a,1,1,2))].

given #62 (F,wt=13): 452 (x v y)' v (x' v y)' = y'.  [back_rewrite(254),rewrite(429(9))].

given #63 (F,wt=13): 453 ((x v x') v x)' v x' = x'.  [back_rewrite(253),rewrite(429(9))].

given #64 (T,wt=13): 542 ((x v y)' v x)' v x' = x'.  [para(430(a,1),416(a,1,1,1,1,1,1)),rewrite(430(4))].

given #65 (T,wt=13): 551 x' v ((y v x)' v x)' = x'.  [para(425(a,1),430(a,1,1)),flip(a)].

given #66 (A,wt=32): 78 (x v ((y v z)' v (y v (x' v (x v u)')')')')' = (y v (x' v (x v u)')')'.  [para(1(a,1),27(a,1,1,1))].

given #67 (F,wt=13): 634 x v ((y v x')' v x')' = x.  [para(430(a,1),551(a,1,1)),rewrite(430(9))].

given #68 (F,wt=14): 460 (((x v y)' v x) v x')' v x = x.  [back_rewrite(411),rewrite(430(2))].

given #69 (T,wt=14): 629 x v (((x v x') v x) v x')' = x.  [para(453(a,1),442(a,1,1,1)),rewrite(430(2),430(9))].

given #70 (T,wt=14): 630 (((x v x') v x) v x')' v x = x.  [para(453(a,1),442(a,1,2,1)),rewrite(430(5),430(8),430(9))].

given #71 (A,wt=38): 79 (((((x v y)' v z)' v u)' v (x v (z' v (z v v)')')')' v z)' = (x v (z' v (z v v)')')'.  [para(1(a,1),27(a,1,1,2))].

given #72 (F,wt=14): 631 x v (((x v y)' v x) v x')' = x.  [para(542(a,1),442(a,1,1,1)),rewrite(430(2),430(9))].

given #73 (F,wt=15): 426 (x v y)' v ((z v x)' v y)' = y'.  [back_rewrite(380),rewrite(418(10))].

given #74 (T,wt=13): 771 (x v (y v x)')' v x = y v x.  [para(442(a,1),426(a,1,2,1)),rewrite(430(6),430(8))].

given #75 (T,wt=9): 785 (x v y')' v y = y.  [para(771(a,1),416(a,1,1,1))].

given #76 (A,wt=33): 89 (((x' v y)' v (x v (x' v (x v z)')')')' v x)' = (x v (x' v (x v z)')')'.  [para(15(a,1),27(a,1,1,2))].

given #77 (F,wt=9): 797 x v (y v x) = y v x.  [para(442(a,1),785(a,1,1,1)),rewrite(430(2))].

given #78 (F,wt=10): 788 (x v y)' v y' = y'.  [para(771(a,1),542(a,1,1,1))].

given #79 (T,wt=11): 789 x v ((y v x) v x')' = x.  [para(771(a,1),631(a,1,2,1,1))].

given #80 (T,wt=13): 796 x' v ((y v x') v x)' = x'.  [para(785(a,1),442(a,1,1,1))].

given #81 (A,wt=18): 93 (x v ((y v z)' v (y v x)')')' = (y v x)'.  [para(27(a,1),27(a,1,1,1))].

given #82 (F,wt=14): 826 (x v ((x v y)' v x')')' = x'.  [para(429(a,1),93(a,1,1,2,1,2,1)),rewrite(429(8))].

given #83 (F,wt=12): 854 x v ((x v y)' v x')' = x.  [para(826(a,1),430(a,1,1)),rewrite(430(2)),flip(a)].

given #84 (T,wt=14): 860 x' v ((x' v y)' v x)' = x'.  [para(430(a,1),854(a,1,2,1,2))].

given #85 (T,wt=15): 451 ((x v y)' v z)' v (x v z)' = z'.  [back_rewrite(255),rewrite(429(10))].

given #86 (A,wt=21): 98 ((((x v (x v y)')' v z)' v x)' v (x v y)')' = x.  [para(87(a,1),1(a,1,1,2))].

% Operation v is commutative; C redundancy checks enabled.

given #87 (F,wt=11): 1007 C v (A v B) != A v (B v C) # answer(robbins_basis).  [back_rewrite(95),rewrite(904(3),904(12)),xx(a)].

given #88 (F,wt=7): 904 x v y = y v x.  [back_rewrite(871),rewrite(899(5))].

given #89 (T,wt=9): 883 x v (y v x')' = x.  [para(788(a,1),451(a,1,1,1)),rewrite(430(2),430(6))].

given #90 (T,wt=9): 898 x v (x v y) = x v y.  [para(98(a,1),785(a,1,1))].

given #91 (A,wt=16): 600 x v ((y' v x) v (y v x)')' = y v x.  [para(442(a,1),442(a,1,1,1)),rewrite(430(2),430(10))].

given #92 (F,wt=9): 962 x v (x' v y)' = x.  [back_rewrite(889),rewrite(904(7),901(8),904(5),904(7),907(7),904(4)),flip(a)].

given #93 (F,wt=10): 882 x' v (y v x)' = x'.  [para(785(a,1),451(a,1,1,1))].

given #94 (T,wt=10): 1027 x' v (x v y)' = x'.  [para(430(a,1),962(a,1,2,1,1))].

given #95 (T,wt=13): 958 x v (x v (x v y)')' = x v y.  [back_rewrite(896),rewrite(904(5))].

given #96 (A,wt=15): 621 (((x v y)' v z)' v (z v x)')' = z.  [para(442(a,1),77(a,1,1,1,1,1,1,1,1)),rewrite(430(2))].

given #97 (F,wt=13): 992 x v (x v (y v x)')' = y v x.  [back_rewrite(771),rewrite(904(5))].

given #98 (F,wt=13): 1009 (x v y)' v (y' v x)' = x'.  [para(904(a,1),452(a,1,1,1))].

given #99 (T,wt=13): 1010 (x v y)' v (y v x')' = y'.  [para(904(a,1),452(a,1,2,1))].

given #100 (T,wt=13): 1051 (x v y')' v (y v x)' = x'.  [para(430(a,1),1009(a,1,2,1,1))].

given #101 (A,wt=17): 627 x v ((y v x) v (y' v x)')' = y' v x.  [para(452(a,1),442(a,1,1,1)),rewrite(430(2),430(11))].

given #102 (F,wt=13): 1055 (x' v y)' v (y v x)' = y'.  [para(1009(a,1),904(a,1)),flip(a)].

given #103 (F,wt=13): 1056 (x v y)' v (x v y')' = x'.  [para(904(a,1),1009(a,1,2,1))].

given #104 (T,wt=15): 938 (x v y)' v ((x v z)' v y)' = y'.  [back_rewrite(449),rewrite(899(9),904(7))].

given #105 (T,wt=15): 957 (x v y)' v (x v (x v y)')' = x'.  [back_rewrite(897),rewrite(904(3),904(7))].

given #106 (A,wt=21): 767 x v ((y v x) v ((z v y)' v x)')' = (z v y)' v x.  [para(426(a,1),442(a,1,1,1)),rewrite(430(2),430(13))].

given #107 (F,wt=15): 1011 (x v y)' v ((z v y)' v x)' = x'.  [para(904(a,1),426(a,1,1,1))].

given #108 (F,wt=15): 1012 (x v y)' v (y v (z v x)')' = y'.  [para(904(a,1),426(a,1,2,1))].

given #109 (T,wt=15): 1034 ((x v y)' v z)' v (z v x)' = z'.  [para(621(a,1),430(a,1,1)),flip(a)].

given #110 (T,wt=15): 1087 (x v y)' v ((y v z)' v x)' = x'.  [para(904(a,1),938(a,1,1,1))].

given #111 (A,wt=25): 784 x v ((y v (z v x)')' v ((u v z)' v x)')' = (u v z)' v x.  [para(426(a,1),426(a,1,1,1)),rewrite(430(2),430(16))].

given #112 (F,wt=11): 1264 x v (y v (y v x)')' = x.  [para(1087(a,1),784(a,1,2,1)),rewrite(430(2),429(1),904(3),904(5)),flip(a)].

given #113 (F,wt=11): 1274 x v (y v (x v y)')' = x.  [para(904(a,1),1264(a,1,2,1,2,1))].

given #114 (T,wt=13): 1315 x v ((y v x) v (y v x)')' = x.  [para(797(a,1),1274(a,1,2,1,2,1))].

given #115 (T,wt=13): 1317 x v ((x v y) v (x v y)')' = x.  [para(898(a,1),1274(a,1,2,1,2,1))].

given #116 (A,wt=16): 827 x v ((y v z)' v (y v x)')' = y v x.  [para(93(a,1),430(a,1,1)),rewrite(430(3)),flip(a)].

given #117 (F,wt=13): 1346 x v ((x v y) v (y v x)')' = x.  [para(904(a,1),1315(a,1,2,1,1))].

given #118 (F,wt=13): 1347 x v ((y v x) v (x v y)')' = x.  [para(904(a,1),1315(a,1,2,1,2,1))].

given #119 (T,wt=15): 1088 (x v y)' v (y v (x v z)')' = y'.  [para(904(a,1),938(a,1,2,1))].

given #120 (T,wt=15): 1152 ((x v y)' v z)' v (z v y)' = z'.  [para(1011(a,1),904(a,1)),flip(a)].

given #121 (A,wt=31): 830 (x v y')' v (y v ((x v z)' v (x v y')')')' = (x v z)' v (x v y')'.  [para(93(a,1),442(a,1,1)),rewrite(430(21))].

given #122 (F,wt=15): 1153 (x v y)' v (x v (z v y)')' = x'.  [para(904(a,1),1011(a,1,2,1))].

given #123 (F,wt=15): 1160 (x v (y v z)')' v (z v x)' = x'.  [para(882(a,1),1011(a,1,2,1,1,1)),rewrite(430(6))].

given #124 (T,wt=15): 1161 (x v (y v z)')' v (y v x)' = x'.  [para(1027(a,1),1011(a,1,2,1,1,1)),rewrite(430(6))].

given #125 (T,wt=15): 1198 (x v y)' v (x v (y v z)')' = x'.  [para(904(a,1),1034(a,1,1,1)),rewrite(904(7))].

given #126 (A,wt=29): 834 (x v y)' v (y' v ((x v z)' v (x v y)')')' = (x v z)' v (x v y)'.  [para(93(a,1),452(a,1,1)),rewrite(430(19))].

given #127 (F,wt=15): 1280 (x v y)' v (y v y')' = (x v y)'.  [para(882(a,1),1264(a,1,2,1,2,1)),rewrite(430(5),904(4))].

NOTE: New constant: (x v x')' = c_0.  [new_symbol(1664)].
NOTE: New Function symbol precedence:  lex([ A, B, C, c_0, v, ' ]).

given #128 (F,wt=5): 1713 c_0 v x = x.  [back_rewrite(1675),rewrite(1683(3))].

given #129 (T,wt=5): 1714 x v c_0 = x.  [back_rewrite(1656),rewrite(1683(3))].

given #130 (T,wt=7): 1683 (x v x')' = c_0.  [new_symbol(1664)].

given #131 (A,wt=31): 840 (x v y)' v ((z v y)' v ((x v u)' v (x v y)')')' = (x v u)' v (x v y)'.  [para(93(a,1),426(a,1,1)),rewrite(430(20))].

given #132 (F,wt=7): 1716 (x v c_0')' = c_0.  [para(1713(a,1),883(a,1))].

given #133 (F,wt=7): 1719 c_0' = x v x'.  [para(1713(a,1),1009(a,1,1,1)),rewrite(904(4),1713(4),430(3),904(2)),flip(a)].

given #134 (T,wt=7): 1791 x v c_0' = c_0'.  [para(1716(a,1),430(a,1,1)),flip(a)].

given #135 (T,wt=7): 1792 c_0' v x = c_0'.  [para(1716(a,1),784(a,1,2,1,1,1,2)),rewrite(1714(4),904(8),1718(8),430(6),904(5),1713(5),430(4),904(8),1718(8))].

given #136 (A,wt=18): 869 x v (((y v z)' v x) v (y v x)')' = y v x.  [para(451(a,1),442(a,1,1,1)),rewrite(430(2),430(11))].

given #137 (F,wt=9): 1679 x v x' = y v y'.  [back_rewrite(1357),rewrite(1676(5),1675(7),430(4),1638(3),1676(6))].

given #138 (F,wt=9): 1689 (x' v (x v y))' = c_0.  [back_rewrite(1003),rewrite(1683(4),1682(8),430(4),1685(5),430(4),1683(7))].

given #139 (T,wt=9): 1721 c_0' = (x v y) v x'.  [para(1713(a,1),1034(a,1,2,1)),rewrite(904(4),1713(4),430(3)),flip(a)].

given #140 (T,wt=9): 1722 c_0' = x' v (x v y).  [para(1713(a,1),1087(a,1,1,1)),rewrite(904(5),1713(5),430(4)),flip(a)].

given #141 (A,wt=19): 879 x v (y v ((z v y)' v x)')' = (z v y)' v x.  [para(426(a,1),451(a,1,1,1)),rewrite(430(2),430(12))].

given #142 (F,wt=9): 1724 (x v (y v y'))' = c_0.  [para(1683(a,1),452(a,2)),rewrite(1701(8),1683(7),904(6),1713(6))].

given #143 (F,wt=9): 1867 (x v (x' v y))' = c_0.  [para(430(a,1),1689(a,1,1,1))].

given #144 (T,wt=9): 1869 ((x v y) v x')' = c_0.  [para(904(a,1),1689(a,1,1))].

given #145 (T,wt=9): 2016 (x v (y v x'))' = c_0.  [para(797(a,1),1867(a,1,1,2))].

given #146 (A,wt=39): 910 (x v (((y v x)' v z)' v (x v (((y v u)' v x)' v v)')')')' = (x v (((y v u)' v x)' v v)')'.  [back_rewrite(735),rewrite(899(5),899(15),904(11),904(15),899(27),904(23))].

given #147 (F,wt=11): 1638 x' v (y v x) = x v x'.  [para(1280(a,1),426(a,1,2,1)),rewrite(883(4),430(4),430(7))].

given #148 (F,wt=11): 1657 (x v y) v y' = y v y'.  [para(1280(a,1),1152(a,1,1,1)),rewrite(430(3),904(5),883(5),430(7))].

given #149 (T,wt=11): 1680 (x v y) v x' = z v z'.  [back_rewrite(1353),rewrite(1676(9),1656(5),1676(11))].

given #150 (T,wt=11): 1681 x' v (x v y) = z v z'.  [back_rewrite(1352),rewrite(1676(7),1656(7),430(4),1676(7))].

given #151 (A,wt=26): 917 (x v y)' v (y v ((x v y)' v (((x v z)' v y)' v u)'))' = y'.  [back_rewrite(717),rewrite(899(11),904(9),904(10),899(16),904(14))].

given #152 (F,wt=11): 1794 (x v y) v (x v y)' = c_0'.  [para(1719(a,2),767(a,2)),rewrite(430(3),430(4),797(3),430(7),904(6),1683(7),904(4),1713(4))].

given #153 (F,wt=11): 1872 ((x' v (x v y)) v z)' = c_0.  [para(1689(a,1),1027(a,1,1)),rewrite(1713(7),1689(9))].

given #154 (T,wt=11): 1907 x v (y v x)' = y' v x.  [back_rewrite(1071),rewrite(1880(6),1880(12),882(9),904(7),882(7),430(4),904(3))].

given #155 (T,wt=11): 1968 (((x v y) v x') v z)' = c_0.  [para(1721(a,1),962(a,1,2,1,1)),rewrite(1713(7))].

given #156 (A,wt=22): 919 x v ((y v x)' v (((y v z)' v x)' v u)')' = y v x.  [back_rewrite(704),rewrite(899(11),904(9),904(11),899(16))].

given #157 (F,wt=11): 1974 c_0' = x' v ((x v y) v z).  [para(1721(a,2),827(a,2)),rewrite(1869(8),904(6),1713(6),430(5)),flip(a)].

given #158 (F,wt=11): 1978 c_0' = ((x v y) v x') v z.  [para(1721(a,1),1792(a,1,1)),flip(a)].

given #159 (T,wt=11): 1979 c_0' = (x' v (x v y)) v z.  [para(1689(a,1),1721(a,2,2)),rewrite(904(8),1713(8))].

given #160 (T,wt=11): 1981 c_0' = (x v y) v (x' v z).  [para(1722(a,2),827(a,2)),rewrite(1689(8),904(6),1713(6),430(5)),flip(a)].

given #161 (A,wt=28): 948 (x v ((x v y)' v (((x' v z)' v (x v y)')' v u)')')' = (x v y)'.  [back_rewrite(493),rewrite(901(16),904(12))].

given #162 (F,wt=11): 2007 c_0' = ((x v y) v z) v y'.  [para(1689(a,1),879(a,1,2,1,2)),rewrite(1714(4),1875(9)),flip(a)].

given #163 (F,wt=11): 2013 (x v x') v y = x v x'.  [para(1724(a,1),784(a,1,2,1,1,1,2)),rewrite(1714(4),1701(8),1683(6),904(5),1713(5),430(4),1701(8))].

given #164 (T,wt=11): 2014 x v (y v y') = y v y'.  [para(1724(a,1),827(a,1,2,1,2)),rewrite(904(6),1713(6),430(5),2013(4)),flip(a)].

given #165 (T,wt=11): 2020 x v (x' v y) = x v x'.  [para(1867(a,1),958(a,1,2,1,2)),rewrite(1714(2)),flip(a)].

given #166 (A,wt=25): 968 x v (((y v x)' v z)' v ((u v y)' v x)')' = (u v y)' v x.  [back_rewrite(880),rewrite(904(11))].

given #167 (F,wt=11): 2036 x v (y v x') = x v x'.  [para(2016(a,1),958(a,1,2,1,2)),rewrite(1714(2)),flip(a)].

given #168 (F,wt=11): 2047 c_0' = (x v (y v z)) v z'.  [para(2016(a,1),879(a,1,2,1,2)),rewrite(430(3),1714(4),430(9),1638(9),1794(8)),flip(a)].

given #169 (T,wt=11): 2247 x v (x v y)' = y' v x.  [para(904(a,1),1907(a,1,2,1))].

given #170 (T,wt=11): 2333 (x' v ((x v y) v z))' = c_0.  [para(1974(a,1),430(a,1,1))].

given #171 (A,wt=22): 969 x v ((y v x)' v (z v ((y v u)' v x)')')' = y v x.  [back_rewrite(878),rewrite(904(9))].

given #172 (F,wt=11): 2334 c_0' = x v ((x' v y) v z).  [para(430(a,1),1974(a,2,1))].

given #173 (F,wt=11): 2336 c_0' = x' v (y v (x v z)).  [para(797(a,1),1974(a,2,2))].

given #174 (T,wt=11): 2337 c_0' = ((x v y) v z) v x'.  [para(1974(a,2),904(a,1))].

given #175 (T,wt=11): 2374 ((x v y) v (x' v z))' = c_0.  [para(1981(a,1),430(a,1,1))].

given #176 (A,wt=21): 973 x v ((y' v x)' v ((y v x)' v z)')' = y' v x.  [back_rewrite(874),rewrite(904(8),904(10))].

given #177 (F,wt=11): 2375 c_0' = (x v y) v (z v x').  [para(797(a,1),1981(a,2,2))].

given #178 (F,wt=11): 2426 (x v ((x' v y) v z))' = c_0.  [para(883(a,1),948(a,1,1,2,1,2,1,1,1)),rewrite(430(4),2020(3),1683(3),430(5),1713(6),430(5),430(9),2020(8),1683(8))].

given #179 (T,wt=11): 2447 (((x v y) v z) v y')' = c_0.  [para(2007(a,1),430(a,1,1))].

given #180 (T,wt=11): 2448 c_0' = x v ((y v x') v z).  [para(430(a,1),2007(a,2,2)),rewrite(904(6))].

given #181 (A,wt=20): 974 x v ((y v x)' v ((y' v x)' v z)')' = y v x.  [back_rewrite(872),rewrite(904(8),904(10))].

given #182 (F,wt=11): 2455 c_0' = (x' v y) v (z v x).  [para(882(a,1),2007(a,2,1,1)),rewrite(430(7))].

given #183 (F,wt=11): 2546 ((x v (y v z)) v z')' = c_0.  [para(2047(a,1),430(a,1,1))].

given #184 (T,wt=11): 2547 c_0' = x v (y v (z v x')).  [para(430(a,1),2047(a,2,2)),rewrite(904(6))].

given #185 (T,wt=11): 2552 c_0' = x' v (y v (z v x)).  [para(2047(a,2),904(a,1))].

given #186 (A,wt=37): 981 (x v (y v z)')' v (z v ((x v u)' v (x v (y v z)')')')' = (x v u)' v (x v (y v z)')'.  [back_rewrite(841),rewrite(904(15))].

given #187 (F,wt=11): 2553 c_0' = (x v (y v z)) v y'.  [para(904(a,1),2047(a,2,1,2))].

given #188 (F,wt=11): 2555 c_0' = (x v y) v (z v y').  [para(883(a,1),2047(a,2,1,2)),rewrite(430(7))].

given #189 (T,wt=11): 2558 c_0' = (x v y') v (z v y).  [para(882(a,1),2047(a,2,1,2)),rewrite(430(7))].

given #190 (T,wt=11): 2629 (x' v (y v (x v z)))' = c_0.  [para(797(a,1),2333(a,1,1,2))].

given #191 (A,wt=21): 991 x v ((y' v x)' v (z v (y v x)')')' = y' v x.  [back_rewrite(772),rewrite(904(8))].

given #192 (F,wt=11): 2630 (((x v y) v z) v x')' = c_0.  [para(904(a,1),2333(a,1,1))].

given #193 (F,wt=11): 2706 c_0' = x v (y v (x' v z)).  [para(797(a,1),2334(a,2,2))].

given #194 (T,wt=11): 2735 x v ((x' v y) v z)' = x.  [para(2334(a,2),2247(a,1,2,1)),rewrite(430(3),1714(2),904(5)),flip(a)].

given #195 (T,wt=11): 2805 ((x v y) v (z v x'))' = c_0.  [para(797(a,1),2374(a,1,1,2))].

given #196 (A,wt=20): 993 x v ((y v x)' v (z v (y' v x)')')' = y v x.  [back_rewrite(769),rewrite(904(8))].

given #197 (F,wt=11): 2893 (x v ((y v x') v z))' = c_0.  [para(797(a,1),2426(a,1,1,2,1))].

given #198 (F,wt=11): 2894 (x v (y v (x' v z)))' = c_0.  [para(797(a,1),2426(a,1,1,2))].

given #199 (T,wt=11): 2905 ((x' v y) v (z v x))' = c_0.  [para(882(a,1),2447(a,1,1,1,1)),rewrite(430(5))].

given #200 (T,wt=11): 2940 x v ((y v x') v z)' = x.  [para(2448(a,2),2247(a,1,2,1)),rewrite(430(3),1714(2),904(5)),flip(a)].

given #201 (A,wt=29): 998 (x v ((y' v x)' v ((x v ((y' v x) v z)')' v u)')')' = (y' v x)'.  [back_rewrite(620),rewrite(904(5),904(12),904(14))].

given #202 (F,wt=11): 3022 (x v (y v (z v x')))' = c_0.  [para(430(a,1),2546(a,1,1,2)),rewrite(904(4))].

given #203 (F,wt=11): 3024 ((x v (y v z)) v y')' = c_0.  [para(904(a,1),2546(a,1,1,1,2))].

given #204 (T,wt=11): 3025 (x' v (y v (z v x)))' = c_0.  [para(904(a,1),2546(a,1,1))].

given #205 (T,wt=11): 3027 ((x v y) v (z v y'))' = c_0.  [para(883(a,1),2546(a,1,1,1,2)),rewrite(430(5))].

given #206 (A,wt=28): 1000 x v ((x v y)' v (x v (((x' v z)' v (x v y)')' v u)'))' = x v y.  [back_rewrite(618),rewrite(904(10),904(13),904(15))].

given #207 (F,wt=11): 3028 ((x v y') v (z v y))' = c_0.  [para(882(a,1),2546(a,1,1,1,2)),rewrite(430(5))].

given #208 (F,wt=11): 3065 x v (y v (z v x'))' = x.  [para(2547(a,2),2247(a,1,2,1)),rewrite(430(3),1714(2),904(5)),flip(a)].

given #209 (T,wt=11): 3364 x v (y v (x' v z))' = x.  [para(2706(a,2),2247(a,1,2,1)),rewrite(430(3),1714(2),904(5)),flip(a)].

given #210 (T,wt=12): 1682 x' v ((x v y) v z)' = x'.  [back_rewrite(1340),rewrite(1676(4),1675(10),430(7))].

given #211 (A,wt=25): 1002 (x v y)' v (x v (((x' v z)' v (x v y)')' v u)')' = x'.  [back_rewrite(611),rewrite(904(10),904(14))].

given #212 (F,wt=12): 1971 x' v (y v (x v z))' = x'.  [para(1721(a,2),767(a,1,2,1,1)),rewrite(904(8),1876(9),1792(4),430(4),904(3),1713(3),904(6)),flip(a)].

given #213 (F,wt=12): 1975 x' v (x v (y v z)') = c_0'.  [para(1160(a,1),1721(a,2,1)),rewrite(430(8)),flip(a)].

given #214 (T,wt=12): 1982 (x v (y v z)') v x' = c_0'.  [para(1160(a,1),1722(a,2,2)),rewrite(430(7)),flip(a)].

given #215 (T,wt=12): 2176 x' v (y v (z v x))' = x'.  [para(1657(a,1),784(a,1,2,1,1,1,2,1)),rewrite(1683(4),1714(3),904(7),2154(8),882(5),904(6)),flip(a)].

given #216 (A,wt=19): 1013 x' v ((y v x)' v (z v x')')' = z v x'.  [para(883(a,1),426(a,1,1,1)),rewrite(430(13))].

given #217 (F,wt=12): 2475 x' v ((y v x) v z)' = x'.  [para(2007(a,2),1907(a,1,2,1)),rewrite(430(4),904(3),1713(3),904(6)),flip(a)].

given #218 (F,wt=13): 1707 (x v y) v (y v x)' = x v x'.  [back_rewrite(1417),rewrite(1682(8),430(3),904(2)),flip(a)].

given #219 (T,wt=11): 3948 (x v y) v (y v x) = y v x.  [para(1707(a,1),2247(a,1,2,1)),rewrite(1683(4),904(3),1713(3),430(4)),flip(a)].

given #220 (T,wt=13): 1875 (x v y)' v ((x v y) v z) = c_0'.  [para(1689(a,1),767(a,1,2,1,2)),rewrite(904(7),1713(7),1868(6),1794(6)),flip(a)].

given #221 (A,wt=19): 1014 (x v y) v (y v (z v (x v y))')' = z v (x v y).  [para(883(a,1),426(a,1,2,1)),rewrite(430(3),430(8),904(7),430(10),430(11))].

given #222 (F,wt=13): 1878 (x v y')' v (y v z) = y v z.  [para(1689(a,1),784(a,1,2,1,1,1,2)),rewrite(1714(3),1781(8),883(7)),flip(a)].

given #223 (F,wt=13): 1916 x v ((y v z) v (y v x)')' = x.  [back_rewrite(1414),rewrite(1907(9),430(3))].

given #224 (T,wt=13): 1970 x' v (x v y) = (z v u) v z'.  [para(1721(a,1),938(a,2)),rewrite(1714(2),904(5),1713(5),430(4))].

given #225 (T,wt=13): 1972 (x v y) v x' = (z v u) v z'.  [para(1721(a,1),1034(a,2)),rewrite(904(4),1713(4),430(3),1713(3))].

given #226 (A,wt=19): 1028 x' v ((y v x)' v (x' v z)')' = x' v z.  [para(962(a,1),426(a,1,1,1)),rewrite(430(13))].

given #227 (F,wt=13): 1980 x' v (x v y) = z' v (z v u).  [para(1722(a,1),938(a,2)),rewrite(1714(2),904(5),1713(5),430(4))].

given #228 (F,wt=13): 1984 x v ((x v y) v z) = (x v y) v z.  [para(1722(a,2),869(a,1,2,1,1)),rewrite(1874(8),1792(8),430(5),904(4),1713(4)),flip(a)].

given #229 (T,wt=13): 2025 (x' v y) v (x v z) = x v x'.  [para(1867(a,1),827(a,1,2,1,2)),rewrite(904(6),1713(6),430(5),2020(7))].

given #230 (T,wt=13): 2044 (x v y') v (y v z) = y v y'.  [para(2016(a,1),827(a,1,2,1,2)),rewrite(904(6),1713(6),430(5),2036(7))].

given #231 (A,wt=19): 1029 (x v y) v (y v ((x v y) v z)')' = (x v y) v z.  [para(962(a,1),426(a,1,2,1)),rewrite(430(3),430(8),904(7),430(10),430(11))].

given #232 (F,wt=13): 2153 (x v y')' v (z v y) = z v y.  [para(1638(a,1),767(a,1,2,1,1)),rewrite(1678(9),2013(6),1683(4),904(3),1713(3)),flip(a)].

given #233 (F,wt=13): 2157 (x v y) v (y' v z) = y v y'.  [para(1638(a,1),827(a,1,2,1,2,1)),rewrite(1683(7),904(6),1713(6),430(5),1638(7))].

given #234 (T,wt=13): 2160 x v (y v (x v z)) = y v (x v z).  [para(1638(a,1),869(a,1,2,1,1)),rewrite(1794(6),2038(8),1792(8),430(5),904(4),1713(4)),flip(a)].

given #235 (T,wt=13): 2177 x' v ((y v x) v z) = x v x'.  [para(1657(a,1),827(a,1,2,1,2,1)),rewrite(1683(7),904(6),1713(6),430(5),1657(7))].

given #236 (A,wt=17): 1030 x v ((y v x')' v (z v x)')' = z v x.  [para(882(a,1),426(a,1,1,1)),rewrite(430(2),430(11))].

given #237 (F,wt=13): 2179 x' v ((x v y) v z) = u v u'.  [para(1680(a,1),827(a,2)),rewrite(1869(8),904(6),1713(6),430(5))].

given #238 (F,wt=13): 2181 ((x v y) v x') v z = u v u'.  [para(1869(a,1),1680(a,1,2)),rewrite(904(6),1713(6))].

given #239 (T,wt=13): 2182 (x v y) v (x' v z) = u v u'.  [para(1681(a,1),827(a,2)),rewrite(1689(8),904(6),1713(6),430(5))].

given #240 (T,wt=13): 2183 ((x v y) v z) v y' = u v u'.  [para(1681(a,1),879(a,2)),rewrite(1875(7),430(5),1714(4))].

given #241 (A,wt=17): 1031 x v ((y v x')' v (x v z)')' = x v z.  [para(1027(a,1),426(a,1,1,1)),rewrite(430(2),430(11))].

given #242 (F,wt=13): 2351 c_0' = ((x v y) v z) v (x' v u).  [para(1974(a,2),827(a,2)),rewrite(2333(10),904(7),1713(7),430(6)),flip(a)].

given #243 (F,wt=13): 2358 c_0' = (((x v y) v z) v u) v y'.  [para(1974(a,2),879(a,1,2,1,2,1)),rewrite(430(6),1714(5),2348(11)),flip(a)].

given #244 (T,wt=13): 2440 ((x v y) v z) v (x v y)' = c_0'.  [para(948(a,1),1721(a,2,2)),rewrite(2412(16)),flip(a)].

given #245 (T,wt=13): 2548 (x v (y v z)) v z' = u v u'.  [para(2047(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #246 (A,wt=22): 1036 x v ((x v y)' v (z v ((y v u)' v x)')')' = x v y.  [para(621(a,1),426(a,1,1)),rewrite(904(9),430(14))].

given #247 (F,wt=13): 2568 c_0' = x' v ((y v (z v x)) v u).  [para(2047(a,2),827(a,2)),rewrite(2546(10),904(7),1713(7),430(6)),flip(a)].

given #248 (F,wt=13): 2620 (x' v y)' v (x v z) = x v z.  [para(1981(a,2),2247(a,1,2,1)),rewrite(430(4),904(3),1713(3)),flip(a)].

given #249 (T,wt=13): 2622 x v ((y v x) v z) = (y v x) v z.  [para(2007(a,2),2247(a,1,2,1)),rewrite(430(5),904(4),1713(4),430(4)),flip(a)].

given #250 (T,wt=13): 2628 x v (y v (z v x)) = y v (z v x).  [para(2047(a,2),2247(a,1,2,1)),rewrite(430(5),904(4),1713(4),430(4)),flip(a)].

given #251 (A,wt=21): 1053 x v ((y' v x)' v (z v (x v y)')')' = y' v x.  [para(1009(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(14))].

given #252 (F,wt=13): 2738 x' v (y v (x v z)) = u v u'.  [para(2336(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #253 (F,wt=13): 2756 c_0' = (x v (y v z)) v (y' v u).  [para(2336(a,2),827(a,2)),rewrite(2629(10),904(7),1713(7),430(6)),flip(a)].

given #254 (T,wt=13): 2763 c_0' = (x v ((y v z) v u)) v z'.  [para(2336(a,2),879(a,1,2,1,2,1)),rewrite(430(6),1714(5),2753(11)),flip(a)].

given #255 (T,wt=13): 2778 ((x v y) v z) v x' = u v u'.  [para(2337(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #256 (A,wt=21): 1061 x v ((x v y')' v (z v (y v x)')')' = x v y'.  [para(1010(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(14))].

given #257 (F,wt=13): 2787 c_0' = x' v (((x v y) v z) v u).  [para(2337(a,2),827(a,2)),rewrite(2630(10),904(7),1713(7),430(6)),flip(a)].

given #258 (F,wt=13): 2844 (x v y) v (z v x') = u v u'.  [para(2375(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #259 (T,wt=13): 2928 c_0' = ((x v (y v z)) v u) v z'.  [para(2448(a,2),879(a,1,2,1,2,1)),rewrite(430(3),430(6),1714(5),430(10),2177(11),1794(9)),flip(a)].

given #260 (T,wt=13): 2981 (x' v y) v (z v x) = u v u'.  [para(2455(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #261 (A,wt=20): 1064 x v ((y v x)' v (z v (x v y')')')' = y v x.  [para(1051(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(13))].

given #262 (F,wt=13): 3003 (x' v y)' v (z v x) = z v x.  [para(2455(a,2),1907(a,1,2,1)),rewrite(430(4),904(3),1713(3)),flip(a)].

given #263 (F,wt=13): 3051 c_0' = (x v (y v (z v u))) v u'.  [para(2547(a,2),879(a,1,2,1,2,1)),rewrite(430(3),430(6),1714(5),430(10),3045(11)),flip(a)].

given #264 (T,wt=13): 3081 x' v (y v (z v x)) = u v u'.  [para(2552(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #265 (T,wt=13): 3089 c_0' = (x v (y v z)) v (z' v u).  [para(2552(a,2),827(a,2)),rewrite(3025(10),904(7),1713(7),430(6)),flip(a)].

given #266 (A,wt=20): 1076 x v ((x v y)' v (z v (y' v x)')')' = x v y.  [para(1055(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(13))].

given #267 (F,wt=13): 3163 (x v (y v z)) v y' = u v u'.  [para(2553(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #268 (F,wt=13): 3172 c_0' = x' v ((y v (x v z)) v u).  [para(2553(a,2),827(a,2)),rewrite(3024(10),904(7),1713(7),430(6)),flip(a)].

given #269 (T,wt=13): 3200 (x v y) v (z v y') = u v u'.  [para(2555(a,1),452(a,2)),rewrite(1714(2),904(4),1713(4),430(3),904(2)),flip(a)].

given #270 (T,wt=13): 3215 c_0' = (x v y') v ((z v y) v u).  [para(2555(a,2),827(a,2)),rewrite(3027(10),904(7),1713(7),430(6)),flip(a)].

given #271 (A,wt=21): 1080 x v ((x v y')' v (z v (x v y)')')' = x v y'.  [para(1056(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(14))].

given #272 (F,wt=11): 5503 (x v y) v z = (x v z) v y.  [back_rewrite(4696),rewrite(5500(3))].

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

% Proof 1 at 2.36 (+ 0.03) seconds: robbins_basis.
% Length of proof is 136.
% Level of proof is 41.
% Maximum clause weight is 90.
% Given clauses 272.

1 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1).  [assumption].
2 B v A != A v B | (A v B) v C != A v (B v C) | ((A v B)' v (A' v B)')' != B # answer(robbins_basis).  [assumption].
7 (((((x'' v y)' v x)' v z)' v x')' v x)' = x'.  [para(1(a,1),1(a,1,1,2))].
12 ((x v x')' v x)' = x'.  [para(1(a,1),7(a,1,1,1,1,1))].
15 (x' v (x v (x' v (x v y)')')')' = x.  [para(12(a,1),1(a,1,1,1))].
23 ((x v y)' v (x' v (y' v (y v z)')')')' = y.  [para(15(a,1),1(a,1,1,1,1,1))].
27 (((x v y)' v z)' v (x v z)')' = z.  [para(15(a,1),1(a,1,1,2,1,2))].
39 (x' v (x v x)')' = x.  [para(15(a,1),15(a,1,1,2,1,2))].
77 (((((x' v y)' v (x v z)')' v u)' v x)' v (x v z)')' = x.  [para(27(a,1),1(a,1,1,2))].
79 (((((x v y)' v z)' v u)' v (x v (z' v (z v v)')')')' v z)' = (x v (z' v (z v v)')')'.  [para(1(a,1),27(a,1,1,2))].
87 ((x v y)' v (x' v y)')' = y.  [para(15(a,1),27(a,1,1,1,1,1))].
93 (x v ((y v z)' v (y v x)')')' = (y v x)'.  [para(27(a,1),27(a,1,1,1))].
95 B v A != A v B | (A v B) v C != A v (B v C) # answer(robbins_basis).  [back_rewrite(2),rewrite(87(29)),xx(c)].
98 ((((x v (x v y)')' v z)' v x)' v (x v y)')' = x.  [para(87(a,1),1(a,1,1,2))].
107 (x' v ((x v x')'' v x)')' = x.  [para(12(a,1),87(a,1,1,1))].
109 (((x v x') v x)' v x')' = x.  [para(12(a,1),87(a,1,1,2))].
118 ((x v y)' v ((z v x)' v y)')' = y.  [para(87(a,1),27(a,1,1,1,1,1))].
119 (x v (y v (y' v x)')')' = (y' v x)'.  [para(87(a,1),27(a,1,1,1))].
139 (x v ((x v x') v x')')' = x'.  [para(109(a,1),27(a,1,1,1))].
196 (x' v x')' = x.  [para(139(a,1),15(a,1,1,2,1,2,1,2)),rewrite(119(9))].
200 ((x' v y)' v (x v y)')' = y.  [para(139(a,1),27(a,1,1,1,1,1))].
216 ((x v y)' v z)' v (x v (z' v (z v u)')')' = (z v z)'.  [para(1(a,1),196(a,1,1,1)),rewrite(1(13)),flip(a)].
221 (x v x')' v x = x.  [para(12(a,1),196(a,1,1,1)),rewrite(12(6),196(4)),flip(a)].
225 (x'' v x)' = x'.  [para(196(a,1),39(a,1,1,2))].
228 (((x' v y)' v x')' v x)' = x'.  [para(196(a,1),27(a,1,1,2))].
229 (x v x)' = ((y v z)' v x)' v (y v x)'.  [para(27(a,1),196(a,1,1,1)),rewrite(27(8))].
232 (x v x)' = (y v x)' v (y' v x)'.  [para(87(a,1),196(a,1,1,1)),rewrite(87(7))].
240 (x v x)' = x' v x'.  [para(196(a,1),196(a,1,1,1)),rewrite(196(4))].
245 x'' v x'' = x.  [back_rewrite(1),rewrite(216(12),240(2),240(4))].
254 (x v y)' v (x' v y)' = y' v y'.  [back_rewrite(232),rewrite(240(2)),flip(a)].
255 ((x v y)' v z)' v (x v z)' = z' v z'.  [back_rewrite(229),rewrite(240(2)),flip(a)].
257 ((x v y)' v z)' v (x v (z' v (z v u)')')' = z' v z'.  [back_rewrite(216),rewrite(240(14))].
273 x'' v x = x.  [para(225(a,1),245(a,1,1,1)),rewrite(225(6),245(5)),flip(a)].
287 (x' v ((x v x') v x)')' = x.  [para(221(a,1),200(a,1,1,1,1))].
289 (x' v y)' v (x v y)' = y' v y'.  [para(200(a,1),245(a,1,1,1)),rewrite(200(8)),flip(a)].
292 (x' v (x' v x)')' = x.  [para(273(a,1),200(a,1,1,1,1))].
295 (x v (x v x')')' = x'.  [para(240(a,1),200(a,1,1,1)),rewrite(245(5))].
306 x' v (x' v x)' = x' v x'.  [para(292(a,1),245(a,1,1,1)),rewrite(292(7)),flip(a)].
315 x v (x v x')' = x.  [para(295(a,1),245(a,1,1,1)),rewrite(295(7),245(5)),flip(a)].
341 (((x' v x) v x')' v x)' = x'.  [para(23(a,1),23(a,1,1,2))].
343 x' v ((x v x') v x)' = x' v x'.  [para(287(a,1),245(a,1,1,1)),rewrite(287(8)),flip(a)].
363 ((x' v x) v x')' v x = x.  [para(341(a,1),245(a,1,1,1)),rewrite(341(9),245(5)),flip(a)].
371 x' v ((x v x')'' v x)' = x' v x'.  [para(107(a,1),245(a,1,1,1)),rewrite(107(10)),flip(a)].
372 ((x' v x') v (((x v x) v (x' v x'))'' v (x v x))')' = x v x.  [para(240(a,1),107(a,1,1,1)),rewrite(240(6))].
373 x v (x v (x' v x'))' = x v x.  [para(107(a,1),306(a,1,1)),rewrite(371(8),240(4),245(5),371(8),371(14),240(10),245(11),371(14),240(10),245(11))].
379 ((x' v x)' v x')' = x.  [para(221(a,1),118(a,1,1,2,1))].
380 (x v y)' v ((z v x)' v y)' = y' v y'.  [para(118(a,1),245(a,1,1,1)),rewrite(118(9)),flip(a)].
408 (x' v x)' v x' = x' v x'.  [para(379(a,1),245(a,1,1,1)),rewrite(379(7)),flip(a)].
416 ((x' v y)' v x')' v x = x.  [para(228(a,1),245(a,1,1,1)),rewrite(228(10),245(5)),flip(a)].
418 x' v x' = x'.  [para(408(a,1),228(a,1,1,1,1)),rewrite(240(4),245(5),240(2))].
426 (x v y)' v ((z v x)' v y)' = y'.  [back_rewrite(380),rewrite(418(10))].
429 x v x = x.  [back_rewrite(373),rewrite(418(3),315(4)),flip(a)].
430 x'' = x.  [back_rewrite(372),rewrite(429(3),429(2),429(4),429(6),371(8),429(3),429(3))].
433 x' v ((x v x') v x)' = x'.  [back_rewrite(343),rewrite(429(9))].
442 (x' v y)' v (x v y)' = y'.  [back_rewrite(289),rewrite(429(9))].
449 ((x v y)' v z)' v (x v (z' v (z v u)')')' = z'.  [back_rewrite(257),rewrite(429(15))].
451 ((x v y)' v z)' v (x v z)' = z'.  [back_rewrite(255),rewrite(429(10))].
452 (x v y)' v (x' v y)' = y'.  [back_rewrite(254),rewrite(429(9))].
542 ((x v y)' v x)' v x' = x'.  [para(430(a,1),416(a,1,1,1,1,1,1)),rewrite(430(4))].
600 x v ((y' v x) v (y v x)')' = y v x.  [para(442(a,1),442(a,1,1,1)),rewrite(430(2),430(10))].
610 (((((((x' v x) v x') v y)' v x')' v z)' v ((x' v x) v x')')' v x')' = ((x' v x) v x')'.  [para(363(a,1),77(a,1,1,1,1,1,1,1,1,2,1)),rewrite(430(6),363(24))].
627 x v ((y v x) v (y' v x)')' = y' v x.  [para(452(a,1),442(a,1,1,1)),rewrite(430(2),430(11))].
715 ((((x v y) v z)' v (x v ((((x v y) v (x v y)') v (x v y)) v ((((x v y) v (x v y)') v (x v y))' v u)')')')' v (((x v y) v (x v y)') v (x v y))')' = (x v ((((x v y) v (x v y)') v (x v y)) v ((((x v y) v (x v y)') v (x v y))' v u)')')'.  [para(433(a,1),79(a,1,1,1,1,1,1,1,1)),rewrite(430(3),430(11),430(41))].
767 x v ((y v x) v ((z v y)' v x)')' = (z v y)' v x.  [para(426(a,1),442(a,1,1,1)),rewrite(430(2),430(13))].
771 (x v (y v x)')' v x = y v x.  [para(442(a,1),426(a,1,2,1)),rewrite(430(6),430(8))].
784 x v ((y v (z v x)')' v ((u v z)' v x)')' = (u v z)' v x.  [para(426(a,1),426(a,1,1,1)),rewrite(430(2),430(16))].
785 (x v y')' v y = y.  [para(771(a,1),416(a,1,1,1))].
788 (x v y)' v y' = y'.  [para(771(a,1),542(a,1,1,1))].
797 x v (y v x) = y v x.  [para(442(a,1),785(a,1,1,1)),rewrite(430(2))].
827 x v ((y v z)' v (y v x)')' = y v x.  [para(93(a,1),430(a,1,1)),rewrite(430(3)),flip(a)].
871 x v (y' v (y v x)')' = y v x.  [para(442(a,1),451(a,1,1,1)),rewrite(430(2),430(9))].
879 x v (y v ((z v y)' v x)')' = (z v y)' v x.  [para(426(a,1),451(a,1,1,1)),rewrite(430(2),430(12))].
882 x' v (y v x)' = x'.  [para(785(a,1),451(a,1,1,1))].
883 x v (y v x')' = x.  [para(788(a,1),451(a,1,1,1)),rewrite(430(2),430(6))].
898 x v (x v y) = x v y.  [para(98(a,1),785(a,1,1))].
899 (x' v (x v y)')' = x.  [para(785(a,1),98(a,1,1,1,1))].
901 (x v (x' v y)')' = x'.  [para(788(a,1),98(a,1,1,1,1)),rewrite(430(2))].
904 x v y = y v x.  [back_rewrite(871),rewrite(899(5))].
938 (x v y)' v ((x v z)' v y)' = y'.  [back_rewrite(449),rewrite(899(9),904(7))].
945 (((x v y) v (x v y)')' v (((x v y) v z)' v (x v ((x v y) v (x v y)')')')')' = (x v ((x v y) v (x v y)')')'.  [back_rewrite(715),rewrite(904(9),898(9),904(13),898(13),901(16),904(18),898(18),904(18),904(25),898(25),904(29),898(29),901(32))].
1003 (x' v ((x v x')' v ((x' v ((x v x') v y)')' v z)')')' = (x v x')'.  [back_rewrite(610),rewrite(904(2),904(4),797(4),904(6),904(11),904(13),797(13),904(13),904(16),904(19),904(21),797(21))].
1007 C v (A v B) != A v (B v C) # answer(robbins_basis).  [back_rewrite(95),rewrite(904(3),904(12)),xx(a)].
1009 (x v y)' v (y' v x)' = x'.  [para(904(a,1),452(a,1,1,1))].
1011 (x v y)' v ((z v y)' v x)' = x'.  [para(904(a,1),426(a,1,1,1))].
1053 x v ((y' v x)' v (z v (x v y)')')' = y' v x.  [para(1009(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(14))].
1056 (x v y)' v (x v y')' = x'.  [para(904(a,1),1009(a,1,2,1))].
1071 ((x v y) v (x' v y)')' v ((x' v y)' v (y' v ((x v y) v (x' v y)')'))' = x' v y.  [para(627(a,1),600(a,1,2,1,2,1)),rewrite(904(18),627(27))].
1080 x v ((x v y')' v (z v (x v y)')')' = x v y'.  [para(1056(a,1),426(a,1,1,1)),rewrite(430(2),904(8),430(14))].
1087 (x v y)' v ((y v z)' v x)' = x'.  [para(904(a,1),938(a,1,1,1))].
1088 (x v y)' v (y v (x v z)')' = y'.  [para(904(a,1),938(a,1,2,1))].
1152 ((x v y)' v z)' v (z v y)' = z'.  [para(1011(a,1),904(a,1)),flip(a)].
1264 x v (y v (y v x)')' = x.  [para(1087(a,1),784(a,1,2,1)),rewrite(430(2),429(1),904(3),904(5)),flip(a)].
1274 x v (y v (x v y)')' = x.  [para(904(a,1),1264(a,1,2,1,2,1))].
1280 (x v y)' v (y v y')' = (x v y)'.  [para(882(a,1),1264(a,1,2,1,2,1)),rewrite(430(5),904(4))].
1315 x v ((y v x) v (y v x)')' = x.  [para(797(a,1),1274(a,1,2,1,2,1))].
1317 x v ((x v y) v (x v y)')' = x.  [para(898(a,1),1274(a,1,2,1,2,1))].
1340 (((x v y) v (x v y)')' v (x' v ((x v y) v z)')')' = x'.  [back_rewrite(945),rewrite(1317(14),904(10),1317(19))].
1359 ((x v y) v (x v y)')' v ((z v y')' v ((u v y)' v ((x v y) v (x v y)')')')' = (u v y)' v ((x v y) v (x v y)')'.  [para(1315(a,1),784(a,1,2,1,1,1,2,1))].
1362 (x v x')' v ((y v x) v (y v x)')' = ((y v x) v (y v x)')'.  [para(1315(a,1),1264(a,1,2,1,2,1)),rewrite(904(9))].
1365 x' v ((y v x)' v ((x v z) v (x v z)')')' = (x v z) v (x v z)'.  [para(1317(a,1),426(a,1,1,1)),rewrite(430(17))].
1369 ((x v y) v (x v y)')' v (x' v ((x v y) v (x v y)')')' = x.  [para(1317(a,1),600(a,1,2,1,2,1)),rewrite(904(14),898(14),1317(20))].
1378 ((x v y) v (x v y)')' v ((z v x')' v ((u v x)' v ((x v y) v (x v y)')')')' = (u v x)' v ((x v y) v (x v y)')'.  [para(1317(a,1),784(a,1,2,1,1,1,2,1))].
1381 (x v x')' v ((x v y) v (x v y)')' = ((x v y) v (x v y)')'.  [para(1317(a,1),1264(a,1,2,1,2,1)),rewrite(904(9))].
1414 x v ((y v x)' v ((y v z)' v (y v x)')')' = x.  [para(827(a,1),1274(a,1,2,1,2,1)),rewrite(904(9))].
1638 x' v (y v x) = x v x'.  [para(1280(a,1),426(a,1,2,1)),rewrite(883(4),430(4),430(7))].
1653 ((x v y) v (x v y)')' = (y v y')'.  [para(1280(a,1),1264(a,1,2,1,2,1)),rewrite(430(8),904(7),1362(9))].
1656 x v (y v y')' = x.  [para(1088(a,1),1280(a,1,1,1)),rewrite(430(2),430(9),904(8),1653(9),430(5),904(4),1653(5),1088(11),430(6))].
1657 (x v y) v y' = y v y'.  [para(1280(a,1),1152(a,1,1,1)),rewrite(430(3),904(5),883(5),430(7))].
1664 (x v x')' = (y v y')'.  [back_rewrite(1381),rewrite(1653(8),1656(7),1653(8))].
1667 (x v x')' v ((y v z')' v (u v z))' = (u v z)'.  [back_rewrite(1378),rewrite(1653(5),1653(13),1656(12),430(9),1653(17),1656(16))].
1675 (x v x')' v y = y.  [back_rewrite(1369),rewrite(1653(5),1653(9),1656(8),430(5))].
1676 (x v y) v (x v y)' = x v x'.  [back_rewrite(1365),rewrite(1653(8),1656(7),430(4),1638(3)),flip(a)].
1678 ((x v y')' v (z v y))' = (z v y)'.  [back_rewrite(1359),rewrite(1676(4),1676(12),1656(12),430(9),1675(10),1676(12),1656(12))].
1682 x' v ((x v y) v z)' = x'.  [back_rewrite(1340),rewrite(1676(4),1675(10),430(7))].
1683 (x v x')' = c_0.  [new_symbol(1664)].
1685 c_0 v (x v y)' = (x v y)'.  [back_rewrite(1667),rewrite(1683(3),1678(7))].
1689 (x' v (x v y))' = c_0.  [back_rewrite(1003),rewrite(1683(4),1682(8),430(4),1685(5),430(4),1683(7))].
1713 c_0 v x = x.  [back_rewrite(1675),rewrite(1683(3))].
1714 x v c_0 = x.  [back_rewrite(1656),rewrite(1683(3))].
1719 c_0' = x v x'.  [para(1713(a,1),1009(a,1,1,1)),rewrite(904(4),1713(4),430(3),904(2)),flip(a)].
1794 (x v y) v (x v y)' = c_0'.  [para(1719(a,2),767(a,2)),rewrite(430(3),430(4),797(3),430(7),904(6),1683(7),904(4),1713(4))].
1868 (x v ((y v x) v z))' = ((y v x) v z)'.  [para(1689(a,1),426(a,1,2)),rewrite(904(6),1713(6))].
1875 (x v y)' v ((x v y) v z) = c_0'.  [para(1689(a,1),767(a,1,2,1,2)),rewrite(904(7),1713(7),1868(6),1794(6)),flip(a)].
1880 ((x v y) v (x' v z)')' = (x v y)'.  [para(1689(a,1),1088(a,1,1)),rewrite(1713(8))].
1907 x v (y v x)' = y' v x.  [back_rewrite(1071),rewrite(1880(6),1880(12),882(9),904(7),882(7),430(4),904(3))].
1916 x v ((y v z) v (y v x)')' = x.  [back_rewrite(1414),rewrite(1907(9),430(3))].
2007 c_0' = ((x v y) v z) v y'.  [para(1689(a,1),879(a,1,2,1,2)),rewrite(1714(4),1875(9)),flip(a)].
2154 (x' v (y v (z v x))')' = x.  [para(1638(a,1),1011(a,1,1,1)),rewrite(1683(3),904(6),1713(8),430(8))].
2176 x' v (y v (z v x))' = x'.  [para(1657(a,1),784(a,1,2,1,1,1,2,1)),rewrite(1683(4),1714(3),904(7),2154(8),882(5),904(6)),flip(a)].
2475 x' v ((y v x) v z)' = x'.  [para(2007(a,2),1907(a,1,2,1)),rewrite(430(4),904(3),1713(3),904(6)),flip(a)].
4696 (x v y) v (x v z) = (x v z) v y.  [para(1916(a,1),1053(a,1,2,1,2,1)),rewrite(430(4),904(7),2475(7),430(3),430(5)),flip(a)].
5500 (x v y) v (x v z) = (x v y) v z.  [para(1916(a,1),1080(a,1,2,1,2,1)),rewrite(430(5),904(7),2176(7),430(3),430(6)),flip(a)].
5503 (x v y) v z = (x v z) v y.  [back_rewrite(4696),rewrite(5500(3))].
5509 (x v y) v z = y v (x v z).  [para(5503(a,1),904(a,1))].
5510 x v (y v z) = z v (x v y).  [para(904(a,1),5503(a,1,1)),rewrite(5509(2),5509(4))].
5511 $F # answer(robbins_basis).  [resolve(5510,a,1007,a(flip))].

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

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

Given=272. Generated=75992. Kept=5510. proofs=1.
Usable=155. Sos=2893. Demods=2331. Limbo=6, Disabled=2457. Hints=0.
Weight_deleted=71. Literals_deleted=0.
Forward_subsumed=70411. Back_subsumed=518.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=4458 (3 lex), Back_demodulated=1937. Back_unit_deleted=0.
Demod_attempts=1430111. Demod_rewrites=238108.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=2.
Megabytes=5.09.
User_CPU=2.36, System_CPU=0.04, Wall_clock=2.

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

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

THEOREM PROVED

Exiting with 1 proof.

Process 11561 exit (max_proofs) Sat Aug 12 21:08:40 2006