============================== Prover9 =============================== Prover9 (32) version 2009-11A, November 2009. Process 5156 was started by mccune on cleo, Tue Nov 3 09:48:29 2009 The command was "/home/mccune/LADR/bin/prover9 -f dn1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file dn1.in assign(max_seconds,30). assign(new_constants,1). formulas(sos). (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1). end_of_list. formulas(goals). y v x = x v y & (x v y) v z = x v (y v z) & ((x v y)' v (x' v y)')' = y # answer(robbins_basis). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 y v x = x v y & (x v y) v z = x v (y v z) & ((x v y)' v (x' v y)')' = y # answer(robbins_basis) # label(non_clause) # label(goal). [goal]. ============================== 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]. c1 v c2 != c2 v c1 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [deny(1)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: (no changes). Term ordering decisions: Predicate symbol precedence: predicate_order([ = ]). Function symbol precedence: function_order([ c1, c2, c3, v, ' ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(hyper_resolution). % (nonunit Horn with equality) % set(hyper_resolution) -> set(pos_hyper_resolution). % set(neg_ur_resolution). % (nonunit Horn with equality) % assign(para_lit_limit, 3). % (nonunit Horn with equality) Auto_process settings: % set(unit_deletion). % (Horn set with negative nonunits) kept: 2 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1). [assumption]. 3 c1 v c2 != c2 v c1 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [deny(1)]. kept: 4 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [copy(3),flip(a)]. ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 2 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1). [assumption]. 4 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [copy(3),flip(a)]. end_of_list. formulas(demodulators). 2 (((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.01 seconds. given #1 (I,wt=22): 2 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1). [assumption]. given #2 (I,wt=31): 4 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [copy(3),flip(a)]. given #3 (A,wt=25): 5 ((x v y)' v (((z v u)' v x)' v (y' v (y v w)')')')' = y. [para(2(a,1),2(a,1,1,1,1,1))]. given #4 (T,wt=11): 18 ((x v x')' v x)' = x'. [para(2(a,1),5(a,1,1,2))]. given #5 (T,wt=17): 22 (x' v (x v (x' v (x v y)')')')' = x. [para(18(a,1),2(a,1,1,1))]. given #6 (T,wt=10): 39 (x' v (x v x)')' = x. [para(22(a,1),22(a,1,1,2,1,2))]. given #7 (T,wt=15): 31 (((x v y)' v z)' v (x v z)')' = z. [para(22(a,1),2(a,1,1,2,1,2))]. given #8 (A,wt=49): 6 (x v ((y v z)' v ((y v (x' v (x v u)')')'' v ((y v (x' v (x v u)')')' v w)')')')' = (y v (x' v (x v u)')')'. [para(2(a,1),2(a,1,1,1))]. given #9 (F,wt=18): 66 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) # answer(robbins_basis). [back_rewrite(4),rewrite([58(29)]),xx(c)]. given #10 (T,wt=13): 58 ((x v y)' v (x' v y)')' = y. [para(22(a,1),31(a,1,1,1,1,1))]. given #11 (T,wt=13): 101 (((x v x') v x)' v x')' = x. [para(18(a,1),58(a,1,1,2))]. given #12 (T,wt=14): 138 (x v ((x v x') v x')')' = x'. [para(101(a,1),31(a,1,1,1))]. given #13 (T,wt=8): 156 (x' v x')' = x. [para(138(a,1),22(a,1,1,2,1,2,1,2)),rewrite([112(9)])]. given #14 (A,wt=22): 9 (((((x'' v y)' v x)' v z)' v x')' v x)' = x'. [para(2(a,1),2(a,1,1,2))]. given #15 (T,wt=9): 179 (x v x')' v x = x. [para(18(a,1),156(a,1,1,1)),rewrite([18(6),156(4)]),flip(a)]. given #16 (T,wt=9): 183 (x'' v x)' = x'. [para(156(a,1),39(a,1,1,2))]. given #17 (T,wt=9): 203 x'' v x'' = x. [back_rewrite(2),rewrite([176(12),198(2),198(4)])]. given #18 (T,wt=7): 229 x'' v x = x. [para(183(a,1),203(a,1,1,1)),rewrite([183(6),203(5)]),flip(a)]. given #19 (A,wt=22): 10 ((x v y)' v ((z v x)' v (y' v (y v u)')')')' = y. [para(5(a,1),2(a,1,1,1,1,1))]. given #20 (T,wt=10): 198 (x v x)' = x' v x'. [para(156(a,1),156(a,1,1,1)),rewrite([156(4)])]. given #21 (T,wt=9): 242 x v (x v x) = x v x. [para(198(a,1),229(a,1,1,1)),rewrite([198(4),203(5)])]. given #22 (T,wt=12): 197 x v ((x v x') v x')' = x. [para(138(a,1),156(a,1,1,1)),rewrite([138(8),156(4)]),flip(a)]. given #23 (T,wt=13): 160 ((x' v y)' v (x v y)')' = y. [para(138(a,1),31(a,1,1,1,1,1))]. given #24 (A,wt=28): 13 (((x v y)' v (z v u)')' v (x v ((z v u)'' v u)')')' = (z v u)'. [para(5(a,1),2(a,1,1,2,1,2,1,2))]. given #25 (T,wt=11): 250 (x' v (x' v x)')' = x. [para(229(a,1),160(a,1,1,1,1))]. given #26 (T,wt=11): 253 (x v (x v x')')' = x'. [para(198(a,1),160(a,1,1,1)),rewrite([203(5)])]. given #27 (T,wt=9): 281 x v (x v x')' = x. [para(253(a,1),203(a,1,1,1)),rewrite([253(7),203(5)]),flip(a)]. given #28 (T,wt=13): 191 (x v (x'' v x')')' = x'. [para(156(a,1),58(a,1,1,1))]. given #29 (A,wt=58): 14 (x v (((y v z)' v ((u v w)' v x)')' v ((u v (x' v (x v v5)')')'' v ((u v (x' v (x v v5)')')' v v6)')')')' = (u v (x' v (x v v5)')')'. [para(2(a,1),5(a,1,1,1))]. given #30 (T,wt=11): 285 x v (x'' v x')' = x. [para(191(a,1),203(a,1,1,1)),rewrite([191(9),203(5)]),flip(a)]. given #31 (T,wt=13): 245 (x' v ((x v x') v x)')' = x. [para(179(a,1),160(a,1,1,1,1))]. given #32 (T,wt=13): 251 ((x''' v x)' v x')' = x. [para(229(a,1),160(a,1,1,2,1))]. given #33 (T,wt=14): 254 ((x' v x)' v (x' v x'))' = x. [para(198(a,1),160(a,1,1,2))]. given #34 (A,wt=29): 15 (((x v (y' v (y v z)')')' v u)' v (y v (u' v (u v w)')')')' = u. [para(2(a,1),5(a,1,1,2,1,1))]. given #35 (T,wt=13): 323 ((x'' v x')' v x)' = x'. [para(203(a,1),254(a,1,1,2))]. given #36 (T,wt=11): 350 (x'' v x')' v x = x. [para(323(a,1),203(a,1,1,1)),rewrite([323(9),203(5)]),flip(a)]. given #37 (T,wt=14): 278 x' v (x' v x)' = x' v x'. [para(250(a,1),203(a,1,1,1)),rewrite([250(7)]),flip(a)]. given #38 (T,wt=15): 99 (x' v ((x v x')'' v x)')' = x. [para(18(a,1),58(a,1,1,1))]. given #39 (A,wt=38): 24 (((((x' v (x v y)')' v (x' v (x v y)')'')' v z)' v x)' v (x' v (x v y)')'')' = x. [para(18(a,1),2(a,1,1,2))]. given #40 (T,wt=14): 356 x v (x v (x' v x'))' = x v x. [para(99(a,1),278(a,1,1)),rewrite([354(8),198(4),203(5),354(8),354(14),198(10),203(11),354(14),198(10),203(11)])]. given #41 (T,wt=15): 111 ((x v y)' v ((z v x)' v y)')' = y. [para(58(a,1),31(a,1,1,1,1,1))]. given #42 (T,wt=11): 366 ((x' v x)' v x')' = x. [para(179(a,1),111(a,1,1,2,1))]. given #43 (T,wt=14): 394 (x' v x)' v x' = x' v x'. [para(366(a,1),203(a,1,1,1)),rewrite([366(7)]),flip(a)]. given #44 (A,wt=20): 27 ((x v y)' v (x' v (y' v (y v z)')')')' = y. [para(22(a,1),2(a,1,1,1,1,1))]. given #45 (T,wt=14): 415 (x v (x' v x'))' v x = x v x. [para(27(a,1),394(a,1,1,1,1)),rewrite([400(11),400(16),198(9),203(10),400(17),198(10),203(11),400(17),198(10),203(11)])]. given #46 (T,wt=14): 423 (((x' v x) v x')' v x)' = x'. [para(27(a,1),27(a,1,1,2))]. given #47 (T,wt=12): 426 ((x' v x) v x')' v x = x. [para(423(a,1),203(a,1,1,1)),rewrite([423(9),203(5)]),flip(a)]. given #48 (T,wt=15): 186 (((x' v y)' v x')' v x)' = x'. [para(156(a,1),31(a,1,1,2))]. given #49 (A,wt=25): 50 (((((x' v y)' v (x v z)')' v u)' v x)' v (x v z)')' = x. [para(31(a,1),2(a,1,1,2))]. given #50 (T,wt=5): 433 x v x = x. [para(186(a,1),415(a,1,1,1,2,1)),rewrite([430(7),430(8),432(3),430(10),179(4),430(7),430(7)]),flip(a)]. given #51 (T,wt=5): 436 x'' = x. [back_rewrite(405),rewrite([433(1),433(6),433(5),400(11),433(3),433(3)])]. given #52 (T,wt=11): 438 (x' v x)' v x' = x'. [back_rewrite(394),rewrite([433(8)])]. given #53 (T,wt=11): 454 x' v (x' v x)' = x'. [back_rewrite(278),rewrite([433(8)])]. given #54 (A,wt=32): 52 (x v ((y v z)' v (y v (x' v (x v u)')')')')' = (y v (x' v (x v u)')')'. [para(2(a,1),31(a,1,1,1))]. given #55 (T,wt=13): 430 ((x' v y)' v x')' v x = x. [para(186(a,1),203(a,1,1,1)),rewrite([186(10),203(5)]),flip(a)]. given #56 (T,wt=13): 439 (x' v ((y v x)' v x)')' = x. [back_rewrite(372),rewrite([433(3),433(4),433(8)])]. given #57 (T,wt=13): 449 x' v ((x v x') v x)' = x'. [back_rewrite(313),rewrite([433(9)])]. given #58 (T,wt=12): 591 x v ((x' v x) v x')' = x. [para(436(a,1),449(a,1,1)),rewrite([436(3),436(8)])]. given #59 (A,wt=38): 53 (((((x v y)' v z)' v u)' v (x v (z' v (z v w)')')')' v z)' = (x v (z' v (z v w)')')'. [para(2(a,1),31(a,1,1,2))]. given #60 (T,wt=13): 456 x' v ((x' v x) v x)' = x'. [back_rewrite(257),rewrite([433(3),433(4),433(9)])]. given #61 (T,wt=13): 457 (x' v y)' v (x v y)' = y'. [back_rewrite(247),rewrite([433(9)])]. given #62 (T,wt=13): 464 (x v y)' v (x' v y)' = y'. [back_rewrite(212),rewrite([433(9)])]. given #63 (T,wt=13): 465 ((x v x') v x)' v x' = x'. [back_rewrite(211),rewrite([433(9)])]. given #64 (A,wt=17): 56 ((((x v x')' v y)' v x)' v x')' = x. [para(18(a,1),31(a,1,1,2))]. given #65 (T,wt=13): 578 ((x v y)' v x)' v x' = x'. [para(436(a,1),430(a,1,1,1,1,1,1)),rewrite([436(4)])]. given #66 (T,wt=13): 587 x' v ((y v x)' v x)' = x'. [para(439(a,1),436(a,1,1)),flip(a)]. given #67 (T,wt=13): 658 x v ((y v x')' v x')' = x. [para(436(a,1),587(a,1,1)),rewrite([436(9)])]. given #68 (T,wt=14): 645 x v (((x v x') v x) v x')' = x. [para(465(a,1),457(a,1,1,1)),rewrite([436(2),436(9)])]. given #69 (A,wt=33): 60 (((x' v y)' v (x v (x' v (x v z)')')')' v x)' = (x v (x' v (x v z)')')'. [para(22(a,1),31(a,1,1,2))]. given #70 (T,wt=14): 646 (((x v x') v x) v x')' v x = x. [para(465(a,1),457(a,1,2,1)),rewrite([436(5),436(8),436(9)])]. given #71 (T,wt=14): 654 x v (((x v y)' v x) v x')' = x. [para(578(a,1),457(a,1,1,1)),rewrite([436(2),436(9)])]. given #72 (T,wt=14): 655 (((x v y)' v x) v x')' v x = x. [para(578(a,1),457(a,1,2,1)),rewrite([436(5),436(8),436(9)])]. given #73 (T,wt=15): 440 (x v y)' v ((z v x)' v y)' = y'. [back_rewrite(367),rewrite([433(10)])]. given #74 (A,wt=18): 64 (x v ((y v z)' v (y v x)')')' = (y v x)'. [para(31(a,1),31(a,1,1,1))]. given #75 (T,wt=11): 755 (x v (y v x))' = (y v x)'. [para(433(a,1),64(a,1,1,2,1)),rewrite([436(3)])]. given #76 (T,wt=9): 796 x v (y v x) = y v x. [para(755(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. given #77 (T,wt=10): 807 (x v y)' v y' = y'. [para(457(a,1),796(a,1,2)),rewrite([457(10)])]. given #78 (T,wt=9): 808 (x v y')' v y = y. [para(436(a,1),807(a,1,2)),rewrite([436(6)])]. given #79 (A,wt=24): 65 (((((x v y)' v z)' v u)' v (x v z)')' v z)' = (x v z)'. [para(31(a,1),31(a,1,1,2))]. given #80 (T,wt=11): 809 x v ((y v x) v x')' = x. [para(807(a,1),457(a,1,1,1)),rewrite([436(2),436(7)])]. given #81 (T,wt=11): 842 ((x v y) v y)' = (x v y)'. [para(807(a,1),65(a,1,1,1,1)),rewrite([436(3)])]. given #82 (T,wt=9): 860 (x v y) v y = x v y. [para(842(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. given #83 (T,wt=10): 864 x' v (y v x)' = x'. [para(457(a,1),860(a,1,1)),rewrite([457(10)])]. given #84 (A,wt=29): 67 (((x v y)' v z)' v (x v (z' v (u v (z' v (z v w)')')')')')' = z. [para(6(a,1),2(a,1,1,2,1,2,1,2))]. given #85 (T,wt=9): 865 x v (y v x')' = x. [para(436(a,1),864(a,1,1)),rewrite([436(6)])]. given #86 (T,wt=13): 729 (x v (y v x)')' v x = y v x. [para(457(a,1),440(a,1,2,1)),rewrite([436(6),436(8)])]. given #87 (T,wt=13): 866 x v (x v (y v x)')' = y v x. [para(864(a,1),457(a,1,1,1)),rewrite([436(2),436(8)])]. given #88 (T,wt=15): 463 ((x v y)' v z)' v (x v z)' = z'. [back_rewrite(213),rewrite([433(10)])]. given #89 (A,wt=22): 85 (((x v (y' v (y v z)')')' v u)' v (y v u)')' = u. [para(6(a,1),31(a,1,1,1,1,1))]. given #90 (T,wt=14): 911 x v (y' v (y v x)')' = y v x. [para(457(a,1),463(a,1,1,1)),rewrite([436(2),436(9)])]. given #91 (T,wt=14): 955 (x' v (x v y)')' v y = x v y. [para(911(a,1),911(a,1,2,1,2,1)),rewrite([864(9),436(7),911(12)])]. given #92 (T,wt=15): 728 ((x v y)' v z)' v (y v z)' = z'. [para(457(a,1),440(a,1,2,1,1,1)),rewrite([436(6)])]. given #93 (T,wt=15): 913 x v (y v (y' v x)')' = y' v x. [para(464(a,1),463(a,1,1,1)),rewrite([436(2),436(10)])]. given #94 (A,wt=21): 94 ((((x v (x v y)')' v z)' v x)' v (x v y)')' = x. [para(58(a,1),2(a,1,1,2))]. % Operation v is commutative; C redundancy checks enabled. % back CAC tautology: 1038 (x v y)' = (y v x)'. [back_rewrite(878),rewrite([1000(9),865(7),1001(5)])]. given #95 (F,wt=11): 1138 c3 v (c1 v c2) != c2 v (c1 v c3) # answer(robbins_basis). [back_rewrite(66),rewrite([1069(3),1069(10),1069(12)]),xx(a)]. given #96 (T,wt=7): 1069 x v y = y v x. [back_rewrite(911),rewrite([1001(5)])]. given #97 (T,wt=9): 999 x v (x v y) = x v y. [para(94(a,1),807(a,1,1)),rewrite([436(3),436(5)])]. given #98 (T,wt=9): 1140 x v (x' v y)' = x. [para(1069(a,1),865(a,1,2,1))]. given #99 (T,wt=10): 1139 x' v (x v y)' = x'. [para(1069(a,1),464(a,1,1,1)),rewrite([1063(6)])]. given #100 (A,wt=16): 637 x v ((y' v x) v (y v x)')' = y v x. [para(457(a,1),457(a,1,1,1)),rewrite([436(2),436(10)])]. given #101 (T,wt=13): 1017 x v (x v (x v y)')' = x v y. [para(94(a,1),728(a,1,1)),rewrite([436(8)])]. given #102 (T,wt=13): 1141 (x v y')' v (y v x)' = x'. [back_rewrite(1065),rewrite([1139(11)])]. given #103 (T,wt=13): 1142 (x' v y)' v (y v x)' = y'. [back_rewrite(1064),rewrite([1139(10)])]. given #104 (T,wt=13): 1143 (x v y)' v (y' v x)' = x'. [back_rewrite(1063),rewrite([1139(10)])]. given #105 (A,wt=17): 643 x v ((y v x) v (y' v x)')' = y' v x. [para(464(a,1),457(a,1,1,1)),rewrite([436(2),436(11)])]. given #106 (T,wt=13): 1144 (x v y)' v (y v x')' = y'. [back_rewrite(1062),rewrite([1139(11)])]. given #107 (T,wt=13): 1167 (x v y)' v (x v y')' = x'. [para(1069(a,1),1141(a,1,2,1)),rewrite([1069(6)])]. given #108 (T,wt=15): 954 (x v y)' v ((x v z)' v y)' = y'. [para(463(a,1),911(a,1,2,1,2,1)),rewrite([436(7),436(7),860(6),463(14)])]. given #109 (T,wt=15): 1101 (x v y)' v (x v (x v y)')' = x'. [back_rewrite(1006),rewrite([1069(5)])]. given #110 (A,wt=21): 725 x v ((y v x) v ((z v y)' v x)')' = (z v y)' v x. [para(440(a,1),457(a,1,1,1)),rewrite([436(2),436(13)])]. given #111 (T,wt=15): 1145 (x v y)' v ((z v y)' v x)' = x'. [back_rewrite(1061),rewrite([1139(11)])]. given #112 (T,wt=15): 1146 (x v y)' v (y v (z v x)')' = y'. [back_rewrite(1060),rewrite([1139(13)])]. given #113 (T,wt=15): 1147 (x v (y v z)')' v (y v x)' = x'. [back_rewrite(1059),rewrite([1139(13)])]. given #114 (T,wt=15): 1148 ((x v y)' v z)' v (z v x)' = z'. [back_rewrite(1058),rewrite([1139(11)])]. given #115 (A,wt=25): 742 x v ((y v (z v x)')' v ((u v z)' v x)')' = (u v z)' v x. [para(440(a,1),440(a,1,1,1)),rewrite([436(2),436(16)])]. given #116 (T,wt=15): 1149 (x v (y v z)')' v (z v x)' = x'. [back_rewrite(1057),rewrite([1139(13)])]. given #117 (T,wt=15): 1150 ((x v y)' v z)' v (z v y)' = z'. [back_rewrite(1056),rewrite([1139(11)])]. given #118 (T,wt=15): 1199 (x v y)' v ((y v z)' v x)' = x'. [para(1069(a,1),954(a,1,1,1))]. given #119 (T,wt=11): 1410 x v (y v (y v x)')' = x. [para(1199(a,1),742(a,1,2,1)),rewrite([436(2),433(1),1069(3),1069(5)]),flip(a)]. given #120 (A,wt=16): 756 x v ((y v z)' v (y v x)')' = y v x. [para(64(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. given #121 (T,wt=11): 1422 x v (y v (x v y)')' = x. [para(1069(a,1),1410(a,1,2,1,2,1))]. given #122 (T,wt=12): 1458 x' v ((x v y) v z)' = x'. [back_rewrite(1128),rewrite([1424(10),436(7),1423(10),436(7)])]. given #123 (T,wt=11): 1538 x v ((x' v y) v z)' = x. [para(436(a,1),1458(a,1,1)),rewrite([436(7)])]. given #124 (T,wt=11): 1548 (x v y) v x' = x v x'. [para(1458(a,1),866(a,1,2,1)),rewrite([436(3),1069(2)]),flip(a)]. given #125 (A,wt=31): 766 (x v y')' v (y v ((x v z)' v (x v y')')')' = (x v z)' v (x v y')'. [para(64(a,1),457(a,1,1)),rewrite([436(21)])]. given #126 (T,wt=11): 1576 x v (y v x)' = y' v x. [back_rewrite(1183),rewrite([1550(5),1550(11),864(9),1069(7),864(7),436(4),1069(3)])]. given #127 (T,wt=11): 1626 x v ((y v x') v z)' = x. [para(796(a,1),1538(a,1,2,1,1))]. given #128 (T,wt=9): 1741 x v (y v y')' = x. [para(1548(a,1),1626(a,1,2,1))]. NOTE: New constant: x v x' = c_0. [new_symbol(1746)]. NOTE: New Function symbol precedence: function_order([ c1, c2, c3, c_0, v, ' ]). given #129 (T,wt=5): 1763 c_0 v x = c_0. [back_rewrite(1753),rewrite([1754(2),1754(4)])]. given #130 (A,wt=31): 785 (x v y)' v ((z v y)' v ((x v u)' v (x v y)')')' = (x v u)' v (x v y)'. [para(64(a,1),440(a,1,1)),rewrite([436(20)])]. given #131 (T,wt=5): 1775 x v c_0 = c_0. [para(1763(a,1),796(a,1,2)),rewrite([1763(4)])]. given #132 (T,wt=6): 1754 x v x' = c_0. [new_symbol(1746)]. given #133 (T,wt=6): 1764 c_0' v x = x. [back_rewrite(1749),rewrite([1754(2)])]. given #134 (T,wt=6): 1765 x v c_0' = x. [back_rewrite(1741),rewrite([1754(2)])]. given #135 (A,wt=17): 867 x v ((y v x')' v (z v x)')' = z v x. [para(864(a,1),440(a,1,1,1)),rewrite([436(2),436(11)])]. given #136 (T,wt=8): 1761 x' v (y v x) = c_0. [back_rewrite(1647),rewrite([1752(5),1754(5)])]. given #137 (T,wt=8): 1767 x v (y v x') = c_0. [back_rewrite(1640),rewrite([1754(2)]),flip(a)]. given #138 (T,wt=8): 1768 x' v (x v y) = c_0. [back_rewrite(1636),rewrite([1754(5)])]. given #139 (T,wt=8): 1769 (x v y) v y' = c_0. [back_rewrite(1635),rewrite([1754(5)])]. given #140 (A,wt=19): 899 x' v ((y v x)' v (z v x')')' = z v x'. [para(865(a,1),440(a,1,1,1)),rewrite([436(13)])]. given #141 (T,wt=8): 1770 x v (x' v y) = c_0. [back_rewrite(1633),rewrite([1754(5)])]. given #142 (T,wt=8): 1771 (x v y) v x' = c_0. [back_rewrite(1548),rewrite([1754(5)])]. given #143 (T,wt=10): 1766 x' v ((x v y) v z) = c_0. [back_rewrite(1653),rewrite([1754(6)])]. given #144 (T,wt=10): 1832 x v ((y v x') v z) = c_0. [para(1458(a,1),867(a,1,2,1)),rewrite([436(4),1767(3),1069(5)]),flip(a)]. given #145 (A,wt=18): 909 x v (((y v z)' v x) v (y v x)')' = y v x. [para(463(a,1),457(a,1,1,1)),rewrite([436(2),436(11)])]. given #146 (T,wt=10): 1838 x v (y v (z v x')) = c_0. [para(1626(a,1),867(a,1,2,1)),rewrite([436(4),1767(3),436(5),1069(5)]),flip(a)]. given #147 (T,wt=10): 1846 (x v y) v (y' v z) = c_0. [para(1761(a,1),756(a,1,2,1,2,1)),rewrite([1069(7),1764(7),436(5),1761(7)])]. given #148 (T,wt=10): 1847 ((x v y) v z) v x' = c_0. [para(1458(a,1),1761(a,1,2)),rewrite([436(4)])]. given #149 (T,wt=10): 1848 x v ((x' v y) v z) = c_0. [para(1538(a,1),1761(a,1,2)),rewrite([436(5),1069(4)])]. given #150 (A,wt=19): 916 x v (y v ((z v y)' v x)')' = (z v y)' v x. [para(440(a,1),463(a,1,1,1)),rewrite([436(2),436(12)])]. given #151 (T,wt=10): 1854 (x v y') v (y v z) = c_0. [para(1767(a,1),756(a,1,2,1,2,1)),rewrite([1069(7),1764(7),436(5),1767(7)])]. given #152 (T,wt=10): 1858 (x v y) v (x' v z) = c_0. [para(1768(a,1),756(a,1,2,1,2,1)),rewrite([1069(7),1764(7),436(5),1768(7)])]. given #153 (T,wt=10): 1861 x' v ((y v x) v z) = c_0. [para(1769(a,1),756(a,1,2,1,2,1)),rewrite([1069(7),1764(7),436(5),1769(7)])]. given #154 (T,wt=10): 1871 ((x v y) v z) v y' = c_0. [para(1458(a,1),899(a,1,2,1)),rewrite([436(4),1761(3)]),flip(a)]. given #155 (A,wt=19): 919 (x v y) v (x v (z v (x v y))')' = z v (x v y). [para(864(a,1),463(a,1,1,1)),rewrite([436(3),436(11)])]. given #156 (T,wt=10): 1873 (x v (y v z)) v z' = c_0. [para(1626(a,1),899(a,1,2,1)),rewrite([436(4),1761(3),436(4)]),flip(a)]. given #157 (T,wt=10): 1879 (x' v y) v (x v z) = c_0. [para(1770(a,1),756(a,1,2,1,2,1)),rewrite([1069(7),1764(7),436(5),1770(7)])]. given #158 (T,wt=10): 1883 x' v (y v (x v z)) = c_0. [para(796(a,1),1766(a,1,2))]. given #159 (T,wt=10): 1954 x' v (y v (z v x)) = c_0. [para(436(a,1),1838(a,1,2,2,2))]. given #160 (A,wt=18): 961 x v (((y v z)' v x) v (z v x)')' = z v x. [para(728(a,1),457(a,1,1,1)),rewrite([436(2),436(11)])]. given #161 (T,wt=10): 1958 (x v y) v (z v y') = c_0. [para(864(a,1),1838(a,1,2,2))]. given #162 (T,wt=10): 1959 (x v y') v (z v y) = c_0. [para(865(a,1),1838(a,1,2,2))]. given #163 (T,wt=10): 1960 x v (y v (x' v z)) = c_0. [para(1069(a,1),1838(a,1,2,2))]. given #164 (T,wt=10): 1961 (x' v y) v (z v x) = c_0. [para(1140(a,1),1838(a,1,2,2))]. given #165 (A,wt=19): 968 (x v y) v (y v (z v (x v y))')' = z v (x v y). [para(864(a,1),728(a,1,1,1)),rewrite([436(3),436(11)])]. given #166 (T,wt=10): 1962 (x v y) v (z v x') = c_0. [para(1139(a,1),1838(a,1,2,2))]. given #167 (T,wt=10): 1978 (x v (y v z)) v y' = c_0. [para(1143(a,1),1846(a,1,2))]. given #168 (T,wt=11): 1627 x v (y v (x' v z))' = x. [para(796(a,1),1538(a,1,2,1))]. given #169 (T,wt=11): 1696 x v (x v y)' = y' v x. [para(1069(a,1),1576(a,1,2,1))]. given #170 (A,wt=16): 973 x v ((y v z)' v (z v x)')' = z v x. [para(728(a,1),463(a,1,1,1)),rewrite([436(2),436(10)])]. given #171 (T,wt=11): 1724 x v (y v (z v x'))' = x. [para(796(a,1),1626(a,1,2,1))]. given #172 (T,wt=12): 1544 x' v ((y v x) v z)' = x'. [para(796(a,1),1458(a,1,2,1,1))]. given #173 (T,wt=12): 1545 x' v (y v (x v z))' = x'. [para(796(a,1),1458(a,1,2,1))]. given #174 (T,wt=12): 1860 x' v (y v (z v x))' = x'. [para(1769(a,1),742(a,1,2,1,1,1,2,1)),rewrite([1765(4),1069(7),1843(8),864(5),1069(6)]),flip(a)]. given #175 (A,wt=28): 1048 (x v ((x v y)' v (((x' v z)' v (x v y)')' v u)')')' = (x v y)'. [back_rewrite(532),rewrite([1000(16),1010(12,R)])]. given #176 (T,wt=12): 1890 ((x v y) v z) v (x' v u) = c_0. [para(1766(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1766(9)])]. given #177 (T,wt=12): 1900 ((x v y') v z) v (y v u) = c_0. [para(1832(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1832(9)])]. given #178 (T,wt=12): 1901 ((x' v y) v z) v (x v u) = c_0. [para(1538(a,1),1832(a,1,2,1))]. given #179 (T,wt=12): 1970 (x v (y v z')) v (z v u) = c_0. [para(1838(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1838(9)])]. given #180 (A,wt=22): 1066 x v ((y v x)' v (((z v y)' v x)' v u)')' = y v x. [back_rewrite(943),rewrite([1001(5),1010(9,R),1010(11)])]. given #181 (T,wt=12): 1971 ((x v y) v z) v (u v x') = c_0. [para(1458(a,1),1838(a,1,2,2))]. given #182 (T,wt=12): 1972 ((x' v y) v z) v (u v x) = c_0. [para(1538(a,1),1838(a,1,2,2))]. given #183 (T,wt=12): 1975 ((x v y') v z) v (u v y) = c_0. [para(1626(a,1),1838(a,1,2,2))]. given #184 (T,wt=12): 1985 (x' v y) v ((z v x) v u) = c_0. [para(1846(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1846(9)])]. given #185 (A,wt=22): 1068 x v ((y v x)' v (z v ((u v y)' v x)')')' = y v x. [back_rewrite(933),rewrite([1001(5),1010(9,R)])]. given #186 (T,wt=12): 1986 x' v (((x v y) v z) v u) = c_0. [para(1458(a,1),1846(a,1,1)),rewrite([436(5)])]. given #187 (T,wt=12): 1987 x v (((x' v y) v z) v u) = c_0. [para(1538(a,1),1846(a,1,1)),rewrite([436(5)])]. given #188 (T,wt=12): 1988 x v (((y v x') v z) v u) = c_0. [para(1626(a,1),1846(a,1,1)),rewrite([436(5)])]. given #189 (T,wt=12): 2017 (((x v y) v z) v u) v y' = c_0. [para(1766(a,1),916(a,1,2,1,2,1)),rewrite([1765(6),1766(11)])]. given #190 (A,wt=22): 1072 x v ((y v x)' v (z v ((y v u)' v x)')')' = y v x. [back_rewrite(882),rewrite([1001(12),864(10),436(8),1069(9),1001(17),864(15),436(13)])]. given #191 (T,wt=12): 2018 ((x v (y v z)) v u) v z' = c_0. [para(1832(a,1),916(a,1,2,1,2,1)),rewrite([436(3),1765(6),436(10),1861(11)])]. given #192 (T,wt=12): 2019 (x v (y v (z v u))) v u' = c_0. [para(1838(a,1),916(a,1,2,1,2,1)),rewrite([436(3),1765(6),436(10),1954(11)])]. given #193 (T,wt=12): 2028 (x v y) v ((z v x') v u) = c_0. [para(1854(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1854(9)])]. given #194 (T,wt=12): 2035 (x' v y) v ((x v z) v u) = c_0. [para(1858(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1858(9)])]. given #195 (A,wt=39): 1074 (x v (((y v x)' v z)' v (x v (((y v u)' v x)' v w)')')')' = (x v (((y v u)' v x)' v w)')'. [back_rewrite(620),rewrite([1001(5),1001(15),1069(11),1069(15),1001(27),1069(23)])]. given #196 (T,wt=12): 2044 ((x v y) v z) v (y' v u) = c_0. [para(1861(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1861(9)])]. given #197 (T,wt=12): 2047 x' v (((y v x) v z) v u) = c_0. [para(1871(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1871(9)])]. given #198 (T,wt=12): 2048 (x v y) v ((x' v z) v u) = c_0. [para(1538(a,1),1871(a,1,1,1)),rewrite([436(6)])]. given #199 (T,wt=12): 2065 x' v ((y v (z v x)) v u) = c_0. [para(1873(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1873(9)])]. given #200 (A,wt=22): 1079 x v ((y v x)' v (((y v z)' v x)' v u)')' = y v x. [back_rewrite(606),rewrite([1001(11),1069(9),1069(11),1001(16)])]. given #201 (T,wt=12): 2066 (x v y') v ((y v z) v u) = c_0. [para(1458(a,1),1873(a,1,1,2)),rewrite([436(6)])]. given #202 (T,wt=12): 2067 (x v y) v ((y' v z) v u) = c_0. [para(1538(a,1),1873(a,1,1,2)),rewrite([436(6)])]. given #203 (T,wt=12): 2068 (x v y) v ((z v y') v u) = c_0. [para(1626(a,1),1873(a,1,1,2)),rewrite([436(6)])]. given #204 (T,wt=12): 2084 (x v (y v z)) v (y' v u) = c_0. [para(1883(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1883(9)])]. given #205 (A,wt=21): 1106 x v ((y' v x)' v (z v (y v x)')')' = y' v x. [back_rewrite(964),rewrite([1069(8),1069(10)])]. given #206 (T,wt=12): 2086 (x v ((y v z) v u)) v z' = c_0. [para(1883(a,1),916(a,1,2,1,2,1)),rewrite([1765(6),1883(11)])]. given #207 (T,wt=12): 2090 (x v (y v z)) v (z' v u) = c_0. [para(1954(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1954(9)])]. given #208 (T,wt=12): 2144 (x v y') v ((z v y) v u) = c_0. [para(1958(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1958(9)])]. given #209 (T,wt=12): 2145 x' v (y v ((x v z) v u)) = c_0. [para(1458(a,1),1958(a,1,1)),rewrite([436(5)])]. given #210 (A,wt=20): 1107 x v ((y v x)' v (z v (y' v x)')')' = y v x. [back_rewrite(963),rewrite([1069(8),1069(10)])]. given #211 (T,wt=12): 2146 (x v ((y v z) v u)) v y' = c_0. [para(1458(a,1),1958(a,1,2))]. given #212 (T,wt=12): 2147 x v (y v ((x' v z) v u)) = c_0. [para(1538(a,1),1958(a,1,1)),rewrite([436(5)])]. given #213 (T,wt=12): 2148 x v (y v ((z v x') v u)) = c_0. [para(1626(a,1),1958(a,1,1)),rewrite([436(5)])]. given #214 (T,wt=12): 2161 (x v (y' v z)) v (y v u) = c_0. [para(1960(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1960(9)])]. given #215 (A,wt=19): 1110 x' v ((x v y)' v (z v x')')' = z v x'. [back_rewrite(921),rewrite([1069(9)])]. given #216 (T,wt=12): 2166 (((x v y) v z) v u) v x' = c_0. [para(1458(a,1),1961(a,1,2)),rewrite([436(4)])]. given #217 (T,wt=12): 2186 x' v ((y v (x v z)) v u) = c_0. [para(1978(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1978(9)])]. given #218 (T,wt=12): 2208 (x v (y' v z)) v (u v y) = c_0. [para(1627(a,1),1838(a,1,2,2))]. given #219 (T,wt=12): 2209 x v ((y v (x' v z)) v u) = c_0. [para(1627(a,1),1846(a,1,1)),rewrite([436(5)])]. given #220 (A,wt=17): 1111 x v ((x' v y)' v (z v x)')' = z v x. [back_rewrite(920),rewrite([1069(8)])]. given #221 (T,wt=12): 2211 (x v y) v (z v (x' v u)) = c_0. [para(1627(a,1),1871(a,1,1,1)),rewrite([436(6)])]. given #222 (T,wt=12): 2212 (x v y) v (z v (y' v u)) = c_0. [para(1627(a,1),1873(a,1,1,2)),rewrite([436(6)])]. given #223 (T,wt=12): 2213 x v (y v (z v (x' v u))) = c_0. [para(1627(a,1),1958(a,1,1)),rewrite([436(5)])]. given #224 (T,wt=12): 2276 (x v (y v z')) v (u v z) = c_0. [para(1838(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1838(9)])]. given #225 (A,wt=25): 1113 x v (((y v x)' v z)' v ((u v y)' v x)')' = (u v y)' v x. [back_rewrite(917),rewrite([1069(11)])]. given #226 (T,wt=12): 2277 (x' v y) v (z v (u v x)) = c_0. [para(1846(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1846(9)])]. given #227 (T,wt=12): 2281 (x v y) v (z v (u v x')) = c_0. [para(1854(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1854(9)])]. given #228 (T,wt=12): 2282 (x' v y) v (z v (x v u)) = c_0. [para(1858(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1858(9)])]. given #229 (T,wt=12): 2283 ((x v y) v z) v (u v y') = c_0. [para(1861(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1861(9)])]. given #230 (A,wt=21): 1114 x v ((y' v x)' v ((y v x)' v z)')' = y' v x. [back_rewrite(914),rewrite([1069(8),1069(10)])]. given #231 (T,wt=12): 2284 x' v (y v ((z v x) v u)) = c_0. [para(1871(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1871(9)])]. given #232 (T,wt=12): 2286 x' v (y v (z v (u v x))) = c_0. [para(1873(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1873(9)])]. given #233 (T,wt=12): 2287 (x v (y v z)) v (u v y') = c_0. [para(1883(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1883(9)])]. given #234 (T,wt=12): 2288 (x v (y v z)) v (u v z') = c_0. [para(1954(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1954(9)])]. given #235 (A,wt=20): 1115 x v ((y v x)' v ((y' v x)' v z)')' = y v x. [back_rewrite(912),rewrite([1069(8),1069(10)])]. given #236 (T,wt=12): 2289 (x v y') v (z v (u v y)) = c_0. [para(1958(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1958(9)])]. given #237 (T,wt=12): 2290 (x v y) v (z v (u v y')) = c_0. [para(1959(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1959(9)])]. given #238 (T,wt=12): 2292 (x v y') v (z v (y v u)) = c_0. [para(1962(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1962(9)])]. given #239 (T,wt=12): 2293 x' v (y v (z v (x v u))) = c_0. [para(1978(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),1978(9)])]. given #240 (A,wt=41): 1116 ((x v y)' v ((z v (x v y)')' v (((x v y)' v ((z v (x v y)') v u)')' v w)')')' = (z v (x v y)')'. [back_rewrite(854),rewrite([1069(8),1069(16),1069(20)])]. given #241 (T,wt=12): 2321 x v ((y v (z v x')) v u) = c_0. [para(1724(a,1),1846(a,1,1)),rewrite([436(5)])]. given #242 (T,wt=12): 2323 x v (y v (z v (u v x'))) = c_0. [para(1724(a,1),1958(a,1,1)),rewrite([436(5)])]. given #243 (T,wt=12): 2364 (x v (y v (z v u))) v z' = c_0. [para(1545(a,1),1958(a,1,2))]. given #244 (T,wt=12): 2365 ((x v (y v z)) v u) v y' = c_0. [para(1545(a,1),1961(a,1,2)),rewrite([436(4)])]. given #245 (A,wt=39): 1117 (x v ((y v x)' v ((x v (((y v x)' v (((y v z)' v x)' v u)')' v w)')' v v5)')')' = (y v x)'. [back_rewrite(845),rewrite([1069(9),1069(13),1069(19),1069(21)])]. given #246 (T,wt=13): 1540 (x v y) v (y' v z)' = x v y. [para(464(a,1),1458(a,1,2,1,1)),rewrite([436(3),436(8)])]. given #247 (T,wt=13): 1546 x v ((x v y) v z) = (x v y) v z. [para(1458(a,1),864(a,1,2,1)),rewrite([436(4),436(4),1069(3),436(7)])]. given #248 (T,wt=13): 1550 (x v y) v (x' v z)' = x v y. [para(1143(a,1),1458(a,1,2,1,1)),rewrite([436(3),436(8)])]. given #249 (T,wt=13): 1592 x v ((y v z) v (y v x)')' = x. [back_rewrite(1537),rewrite([1576(9),436(3)])]. given #250 (A,wt=30): 1120 (x v y)' v (y v (z v ((x v y)' v (((x v u)' v y)' v w)')')')' = y'. [back_rewrite(835),rewrite([1069(11),1069(15)])]. given #251 (T,wt=12): 3977 x v ((y v z) v (y v x)') = c_0. [para(1592(a,1),1761(a,1,2)),rewrite([436(6),1069(5)])]. given #252 (T,wt=12): 4222 x v ((y v z) v (z v x)') = c_0. [para(796(a,1),3977(a,1,2,1))]. given #253 (T,wt=10): 4343 (x v y) v (y v x)' = c_0. [para(4222(a,1),1546(a,1)),flip(a)]. given #254 (T,wt=11): 4357 (x v y) v (y v x) = y v x. [para(4343(a,1),1696(a,1,2,1)),rewrite([1765(4),436(4)]),flip(a)]. given #255 (A,wt=37): 1130 (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(786),rewrite([1069(15)])]. given #256 (T,wt=12): 4223 x v ((y v z) v (x v y)') = c_0. [para(1069(a,1),3977(a,1,2,2,1))]. given #257 (T,wt=12): 4224 x v ((y v x)' v (y v z)) = c_0. [para(1069(a,1),3977(a,1,2))]. given #258 (T,wt=12): 4279 x v ((y v z) v (x v z)') = c_0. [para(1069(a,1),4222(a,1,2,2,1))]. given #259 (T,wt=12): 4280 x v ((y v x)' v (z v y)) = c_0. [para(1069(a,1),4222(a,1,2))]. given #260 (A,wt=25): 1133 (x v y)' v (x v (((x' v z)' v (x v y)')' v u)')' = x'. [back_rewrite(555),rewrite([1069(10),1069(14)])]. given #261 (T,wt=12): 4355 (x v y)' v ((y v x) v z) = c_0. [para(4343(a,1),756(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),4343(9)])]. given #262 (T,wt=12): 4358 (x v y)' v (z v (y v x)) = c_0. [para(4343(a,1),973(a,1,2,1,2,1)),rewrite([1069(8),1764(8),436(6),4343(9)])]. given #263 (T,wt=12): 4366 ((x v y) v z) v (y v x)' = c_0. [para(4357(a,1),1847(a,1,1,1))]. given #264 (T,wt=12): 4367 (x v y) v (z v (y v x)') = c_0. [para(4357(a,1),1854(a,1,2)),rewrite([1069(5)])]. given #265 (A,wt=19): 1151 x' v ((y v x)' v (x' v z)')' = x' v z. [para(1140(a,1),440(a,1,1,1)),rewrite([436(13)])]. given #266 (T,wt=12): 4368 (x v y) v ((y v x)' v z) = c_0. [para(4357(a,1),1858(a,1,1))]. given #267 (T,wt=12): 4370 (x v (y v z)) v (z v y)' = c_0. [para(4357(a,1),1978(a,1,1,2))]. given #268 (T,wt=12): 4473 x v ((x v y)' v (y v z)) = c_0. [para(1069(a,1),4223(a,1,2))]. given #269 (T,wt=12): 4575 x v ((x v y)' v (z v y)) = c_0. [para(1069(a,1),4279(a,1,2))]. given #270 (A,wt=19): 1152 (x v y) v (y v ((x v y) v z)')' = (x v y) v z. [para(1140(a,1),440(a,1,2,1)),rewrite([436(3),436(8),1069(7),436(10),436(11)])]. given #271 (T,wt=12): 4684 x v (y v ((y v x)' v z)) = c_0. [para(1546(a,1),4280(a,1,2)),rewrite([1069(4)])]. given #272 (T,wt=12): 4874 x v (y v ((x v y)' v z)) = c_0. [para(1546(a,1),4575(a,1,2)),rewrite([1069(4)])]. given #273 (T,wt=12): 4914 x v (y v (z v (y v x)')) = c_0. [para(796(a,1),4684(a,1,2,2))]. given #274 (T,wt=12): 4978 x v (y v (z v (x v y)')) = c_0. [para(796(a,1),4874(a,1,2,2))]. given #275 (A,wt=17): 1153 x v ((y v x')' v (x v z)')' = x v z. [para(1139(a,1),440(a,1,1,1)),rewrite([436(2),436(11)])]. given #276 (T,wt=12): 5084 (x v y)' v ((x v z) v y) = c_0. [para(1592(a,1),4914(a,1,2,2))]. given #277 (T,wt=12): 5174 (x v y)' v ((z v x) v y) = c_0. [para(796(a,1),5084(a,1,2,1))]. given #278 (T,wt=12): 5175 ((x v y) v z) v (x v z)' = c_0. [para(5084(a,1),1069(a,1)),flip(a)]. given #279 (T,wt=12): 5176 (x v y)' v ((y v z) v x) = c_0. [para(1069(a,1),5084(a,1,1,1))]. given #280 (A,wt=20): 1166 x v ((y v x)' v (z v (x v y')')')' = y v x. [para(1141(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(13)])]. given #281 (T,wt=12): 5177 (x v y)' v (y v (x v z)) = c_0. [para(1069(a,1),5084(a,1,2))]. given #282 (T,wt=12): 5277 ((x v y) v z) v (y v z)' = c_0. [para(5174(a,1),1069(a,1)),flip(a)]. given #283 (T,wt=12): 5278 (x v y)' v ((z v y) v x) = c_0. [para(1069(a,1),5174(a,1,1,1))]. given #284 (T,wt=12): 5279 (x v y)' v (y v (z v x)) = c_0. [para(1069(a,1),5174(a,1,2))]. given #285 (A,wt=20): 1172 x v ((x v y)' v (z v (y' v x)')')' = x v y. [para(1142(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(13)])]. given #286 (T,wt=12): 5386 (x v (y v z)) v (y v x)' = c_0. [para(1069(a,1),5175(a,1,1))]. given #287 (T,wt=12): 5387 ((x v y) v z) v (z v x)' = c_0. [para(1069(a,1),5175(a,1,2,1))]. given #288 (T,wt=12): 5400 (x v y)' v (x v (y v z)) = c_0. [para(1069(a,1),5176(a,1,2))]. given #289 (T,wt=12): 5572 (x v (y v z)) v (z v x)' = c_0. [para(1069(a,1),5277(a,1,1))]. given #290 (A,wt=21): 1176 x v ((y' v x)' v (z v (x v y)')')' = y' v x. [para(1143(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(14)])]. given #291 (T,wt=12): 5573 ((x v y) v z) v (z v y)' = c_0. [para(1069(a,1),5277(a,1,2,1))]. given #292 (T,wt=12): 5586 (x v y)' v (x v (z v y)) = c_0. [para(1069(a,1),5278(a,1,2))]. given #293 (T,wt=12): 5786 (x v (y v z)) v (x v y)' = c_0. [para(1069(a,1),5386(a,1,2,1))]. given #294 (T,wt=12): 5828 (x v (y v z)) v (x v z)' = c_0. [para(1069(a,1),5572(a,1,2,1))]. given #295 (A,wt=21): 1188 x v ((x v y')' v (z v (y v x)')')' = x v y'. [para(1144(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(14)])]. given #296 (T,wt=13): 1720 x v ((y v x) v z) = (y v x) v z. [para(1626(a,1),464(a,1,2,1)),rewrite([436(2),436(7),1069(6),1696(6),436(4),1069(3),436(5),436(7)])]. given #297 (T,wt=13): 1845 (x v y')' v (z v y) = z v y. [para(1761(a,1),742(a,1,2,1,1,1,2,1)),rewrite([1765(4),1751(8),865(7)]),flip(a)]. given #298 (T,wt=13): 1857 (x v y')' v (y v z) = y v z. [para(1768(a,1),742(a,1,2,1,1,1,2,1)),rewrite([1765(4),1772(8),865(7)]),flip(a)]. given #299 (T,wt=13): 1872 (x v y) v (z v y')' = x v y. [para(899(a,1),1576(a,1,2,1)),rewrite([1069(11),1576(11),436(3),436(7),1275(13)])]. given #300 (A,wt=21): 1192 x v ((x v y')' v (z v (x v y)')')' = x v y'. [para(1167(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(14)])]. given #301 (T,wt=11): 6167 (x v y) v z = (x v z) v y. [back_rewrite(5490),rewrite([6140(3)])]. ============================== PROOF ================================= % Proof 1 at 3.01 (+ 0.05) seconds: robbins_basis. % Length of proof is 120. % Level of proof is 37. % Maximum clause weight is 36.000. % Given clauses 301. 1 y v x = x v y & (x v y) v z = x v (y v z) & ((x v y)' v (x' v y)')' = y # answer(robbins_basis) # label(non_clause) # label(goal). [goal]. 2 (((x v y)' v z)' v (x v (z' v (z v u)')')')' = z # label(DN1). [assumption]. 3 c1 v c2 != c2 v c1 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [deny(1)]. 4 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) | ((c2 v c1)' v (c2' v c1)')' != c1 # answer(robbins_basis). [copy(3),flip(a)]. 5 ((x v y)' v (((z v u)' v x)' v (y' v (y v w)')')')' = y. [para(2(a,1),2(a,1,1,1,1,1))]. 18 ((x v x')' v x)' = x'. [para(2(a,1),5(a,1,1,2))]. 22 (x' v (x v (x' v (x v y)')')')' = x. [para(18(a,1),2(a,1,1,1))]. 27 ((x v y)' v (x' v (y' v (y v z)')')')' = y. [para(22(a,1),2(a,1,1,1,1,1))]. 31 (((x v y)' v z)' v (x v z)')' = z. [para(22(a,1),2(a,1,1,2,1,2))]. 58 ((x v y)' v (x' v y)')' = y. [para(22(a,1),31(a,1,1,1,1,1))]. 64 (x v ((y v z)' v (y v x)')')' = (y v x)'. [para(31(a,1),31(a,1,1,1))]. 65 (((((x v y)' v z)' v u)' v (x v z)')' v z)' = (x v z)'. [para(31(a,1),31(a,1,1,2))]. 66 c2 v c1 != c1 v c2 | (c2 v c1) v c3 != c2 v (c1 v c3) # answer(robbins_basis). [back_rewrite(4),rewrite([58(29)]),xx(c)]. 94 ((((x v (x v y)')' v z)' v x)' v (x v y)')' = x. [para(58(a,1),2(a,1,1,2))]. 101 (((x v x') v x)' v x')' = x. [para(18(a,1),58(a,1,1,2))]. 111 ((x v y)' v ((z v x)' v y)')' = y. [para(58(a,1),31(a,1,1,1,1,1))]. 112 (x v (y v (y' v x)')')' = (y' v x)'. [para(58(a,1),31(a,1,1,1))]. 138 (x v ((x v x') v x')')' = x'. [para(101(a,1),31(a,1,1,1))]. 156 (x' v x')' = x. [para(138(a,1),22(a,1,1,2,1,2,1,2)),rewrite([112(9)])]. 160 ((x' v y)' v (x v y)')' = y. [para(138(a,1),31(a,1,1,1,1,1))]. 176 ((x v y)' v z)' v (x v (z' v (z v u)')')' = (z v z)'. [para(2(a,1),156(a,1,1,1)),rewrite([2(13)]),flip(a)]. 179 (x v x')' v x = x. [para(18(a,1),156(a,1,1,1)),rewrite([18(6),156(4)]),flip(a)]. 186 (((x' v y)' v x')' v x)' = x'. [para(156(a,1),31(a,1,1,2))]. 187 (x v x)' = ((y v z)' v x)' v (y v x)'. [para(31(a,1),156(a,1,1,1)),rewrite([31(8)])]. 193 (x v x)' = (y v x)' v (y' v x)'. [para(58(a,1),156(a,1,1,1)),rewrite([58(7)])]. 198 (x v x)' = x' v x'. [para(156(a,1),156(a,1,1,1)),rewrite([156(4)])]. 203 x'' v x'' = x. [back_rewrite(2),rewrite([176(12),198(2),198(4)])]. 212 (x v y)' v (x' v y)' = y' v y'. [back_rewrite(193),rewrite([198(2)]),flip(a)]. 213 ((x v y)' v z)' v (x v z)' = z' v z'. [back_rewrite(187),rewrite([198(2)]),flip(a)]. 247 (x' v y)' v (x v y)' = y' v y'. [para(160(a,1),203(a,1,1,1)),rewrite([160(8)]),flip(a)]. 253 (x v (x v x')')' = x'. [para(198(a,1),160(a,1,1,1)),rewrite([203(5)])]. 281 x v (x v x')' = x. [para(253(a,1),203(a,1,1,1)),rewrite([253(7),203(5)]),flip(a)]. 366 ((x' v x)' v x')' = x. [para(179(a,1),111(a,1,1,2,1))]. 367 (x v y)' v ((z v x)' v y)' = y' v y'. [para(111(a,1),203(a,1,1,1)),rewrite([111(9)]),flip(a)]. 394 (x' v x)' v x' = x' v x'. [para(366(a,1),203(a,1,1,1)),rewrite([366(7)]),flip(a)]. 400 (x v y)' v (x' v (y' v (y v z)')')' = y' v y'. [para(27(a,1),203(a,1,1,1)),rewrite([27(13)]),flip(a)]. 405 ((x v (y v y))' v (x' v ((y' v y') v ((y v y) v z)')')')' = y v y. [para(198(a,1),27(a,1,1,2,1,2,1,1))]. 415 (x v (x' v x'))' v x = x v x. [para(27(a,1),394(a,1,1,1,1)),rewrite([400(11),400(16),198(9),203(10),400(17),198(10),203(11),400(17),198(10),203(11)])]. 430 ((x' v y)' v x')' v x = x. [para(186(a,1),203(a,1,1,1)),rewrite([186(10),203(5)]),flip(a)]. 432 x' v x' = x'. [para(394(a,1),186(a,1,1,1,1)),rewrite([198(4),203(5),198(2)])]. 433 x v x = x. [para(186(a,1),415(a,1,1,1,2,1)),rewrite([430(7),430(8),432(3),430(10),179(4),430(7),430(7)]),flip(a)]. 436 x'' = x. [back_rewrite(405),rewrite([433(1),433(6),433(5),400(11),433(3),433(3)])]. 440 (x v y)' v ((z v x)' v y)' = y'. [back_rewrite(367),rewrite([433(10)])]. 457 (x' v y)' v (x v y)' = y'. [back_rewrite(247),rewrite([433(9)])]. 463 ((x v y)' v z)' v (x v z)' = z'. [back_rewrite(213),rewrite([433(10)])]. 464 (x v y)' v (x' v y)' = y'. [back_rewrite(212),rewrite([433(9)])]. 637 x v ((y' v x) v (y v x)')' = y v x. [para(457(a,1),457(a,1,1,1)),rewrite([436(2),436(10)])]. 643 x v ((y v x) v (y' v x)')' = y' v x. [para(464(a,1),457(a,1,1,1)),rewrite([436(2),436(11)])]. 742 x v ((y v (z v x)')' v ((u v z)' v x)')' = (u v z)' v x. [para(440(a,1),440(a,1,1,1)),rewrite([436(2),436(16)])]. 755 (x v (y v x))' = (y v x)'. [para(433(a,1),64(a,1,1,2,1)),rewrite([436(3)])]. 756 x v ((y v z)' v (y v x)')' = y v x. [para(64(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. 796 x v (y v x) = y v x. [para(755(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. 807 (x v y)' v y' = y'. [para(457(a,1),796(a,1,2)),rewrite([457(10)])]. 808 (x v y')' v y = y. [para(436(a,1),807(a,1,2)),rewrite([436(6)])]. 819 (((((x v y)' v (x v x')')' v z)' v x')' v (x v x')')' = x'. [para(281(a,1),65(a,1,1,1,1,2,1)),rewrite([281(21)])]. 842 ((x v y) v y)' = (x v y)'. [para(807(a,1),65(a,1,1,1,1)),rewrite([436(3)])]. 860 (x v y) v y = x v y. [para(842(a,1),436(a,1,1)),rewrite([436(3)]),flip(a)]. 864 x' v (y v x)' = x'. [para(457(a,1),860(a,1,1)),rewrite([457(10)])]. 865 x v (y v x')' = x. [para(436(a,1),864(a,1,1)),rewrite([436(6)])]. 866 x v (x v (y v x)')' = y v x. [para(864(a,1),457(a,1,1,1)),rewrite([436(2),436(8)])]. 911 x v (y' v (y v x)')' = y v x. [para(457(a,1),463(a,1,1,1)),rewrite([436(2),436(9)])]. 946 (x v y')' v (y v (x' v (x v y')')')' = x' v (x v y')'. [para(911(a,1),457(a,1,1,1)),rewrite([436(19)])]. 948 (x v y)' v (y' v (x' v (x v y)')')' = x' v (x v y)'. [para(911(a,1),464(a,1,1,1)),rewrite([436(17)])]. 950 (x v y)' v ((z v y)' v (x' v (x v y)')')' = x' v (x v y)'. [para(911(a,1),440(a,1,1,1)),rewrite([436(18)])]. 952 (x v (y v z)')' v (y v (x' v (x v (y v z)')')')' = x' v (x v (y v z)')'. [para(911(a,1),463(a,1,1,1)),rewrite([436(22)])]. 954 (x v y)' v ((x v z)' v y)' = y'. [para(463(a,1),911(a,1,2,1,2,1)),rewrite([436(7),436(7),860(6),463(14)])]. 999 x v (x v y) = x v y. [para(94(a,1),807(a,1,1)),rewrite([436(3),436(5)])]. 1001 (x' v (x v y)')' = x. [para(808(a,1),94(a,1,1,1,1))]. 1059 (x v (y v z)')' v (y v x)' = x' v (x v (y v z)')'. [back_rewrite(952),rewrite([1001(11)])]. 1061 (x v y)' v ((z v y)' v x)' = x' v (x v y)'. [back_rewrite(950),rewrite([1001(9)])]. 1063 (x v y)' v (y' v x)' = x' v (x v y)'. [back_rewrite(948),rewrite([1001(8)])]. 1065 (x v y')' v (y v x)' = x' v (x v y')'. [back_rewrite(946),rewrite([1001(9)])]. 1069 x v y = y v x. [back_rewrite(911),rewrite([1001(5)])]. 1128 ((x v x')' v (x' v (((x v y)' v (x v x')')' v z)')')' = x'. [back_rewrite(819),rewrite([1069(11),1069(16)])]. 1138 c3 v (c1 v c2) != c2 v (c1 v c3) # answer(robbins_basis). [back_rewrite(66),rewrite([1069(3),1069(10),1069(12)]),xx(a)]. 1139 x' v (x v y)' = x'. [para(1069(a,1),464(a,1,1,1)),rewrite([1063(6)])]. 1140 x v (x' v y)' = x. [para(1069(a,1),865(a,1,2,1))]. 1141 (x v y')' v (y v x)' = x'. [back_rewrite(1065),rewrite([1139(11)])]. 1143 (x v y)' v (y' v x)' = x'. [back_rewrite(1063),rewrite([1139(10)])]. 1145 (x v y)' v ((z v y)' v x)' = x'. [back_rewrite(1061),rewrite([1139(11)])]. 1147 (x v (y v z)')' v (y v x)' = x'. [back_rewrite(1059),rewrite([1139(13)])]. 1166 x v ((y v x)' v (z v (x v y')')')' = y v x. [para(1141(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(13)])]. 1167 (x v y)' v (x v y')' = x'. [para(1069(a,1),1141(a,1,2,1)),rewrite([1069(6)])]. 1183 ((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(643(a,1),637(a,1,2,1,2,1)),rewrite([1069(18),643(27)])]. 1192 x v ((x v y')' v (z v (x v y)')')' = x v y'. [para(1167(a,1),440(a,1,1,1)),rewrite([436(2),1069(8),436(14)])]. 1199 (x v y)' v ((y v z)' v x)' = x'. [para(1069(a,1),954(a,1,1,1))]. 1410 x v (y v (y v x)')' = x. [para(1199(a,1),742(a,1,2,1)),rewrite([436(2),433(1),1069(3),1069(5)]),flip(a)]. 1422 x v (y v (x v y)')' = x. [para(1069(a,1),1410(a,1,2,1,2,1))]. 1423 (x v x')' v (x' v y)' = (x' v y)'. [para(1140(a,1),1410(a,1,2,1,2,1)),rewrite([1069(7)])]. 1424 (x v y)' v (x v x')' = (x v y)'. [para(1139(a,1),1410(a,1,2,1,2,1)),rewrite([436(5),1069(4)])]. 1458 x' v ((x v y) v z)' = x'. [back_rewrite(1128),rewrite([1424(10),436(7),1423(10),436(7)])]. 1537 x v ((y v x)' v ((y v z)' v (y v x)')')' = x. [para(756(a,1),1422(a,1,2,1,2,1)),rewrite([1069(9)])]. 1538 x v ((x' v y) v z)' = x. [para(436(a,1),1458(a,1,1)),rewrite([436(7)])]. 1544 x' v ((y v x) v z)' = x'. [para(796(a,1),1458(a,1,2,1,1))]. 1548 (x v y) v x' = x v x'. [para(1458(a,1),866(a,1,2,1)),rewrite([436(3),1069(2)]),flip(a)]. 1550 (x v y) v (x' v z)' = x v y. [para(1143(a,1),1458(a,1,2,1,1)),rewrite([436(3),436(8)])]. 1576 x v (y v x)' = y' v x. [back_rewrite(1183),rewrite([1550(5),1550(11),864(9),1069(7),864(7),436(4),1069(3)])]. 1592 x v ((y v z) v (y v x)')' = x. [back_rewrite(1537),rewrite([1576(9),436(3)])]. 1626 x v ((y v x') v z)' = x. [para(796(a,1),1538(a,1,2,1,1))]. 1634 (x v y) v (x v y)' = y' v (x v y). [para(464(a,1),1548(a,1,1)),rewrite([436(4),436(8),1069(7)]),flip(a)]. 1635 (x v y) v y' = y v y'. [para(796(a,1),1548(a,1,1))]. 1636 x' v (x v y) = x v x'. [para(1548(a,1),1069(a,1)),flip(a)]. 1647 (x v y) v (z v (x v y)') = z v z'. [para(1147(a,1),1548(a,1,1)),rewrite([436(6),1636(5),436(11),1069(10),1634(10),436(5)]),flip(a)]. 1741 x v (y v y')' = x. [para(1548(a,1),1626(a,1,2,1))]. 1746 x v x' = y v y'. [para(1741(a,1),464(a,1,1,1)),rewrite([1741(6),436(3),1069(2),436(6)])]. 1749 (x v x')' v y = y. [para(1741(a,1),796(a,1,2)),rewrite([1741(8)])]. 1752 (x v y) v (z v (x v y)') = y' v (x v y). [para(1741(a,1),742(a,1,2,1)),rewrite([436(3),436(4),796(3),436(6),436(10),1069(9),1634(9)])]. 1754 x v x' = c_0. [new_symbol(1746)]. 1761 x' v (y v x) = c_0. [back_rewrite(1647),rewrite([1752(5),1754(5)])]. 1764 c_0' v x = x. [back_rewrite(1749),rewrite([1754(2)])]. 1765 x v c_0' = x. [back_rewrite(1741),rewrite([1754(2)])]. 1769 (x v y) v y' = c_0. [back_rewrite(1635),rewrite([1754(5)])]. 1843 (x' v (y v (z v x))')' = x. [para(1761(a,1),1145(a,1,1,1)),rewrite([1069(7),1764(9),436(8)])]. 1860 x' v (y v (z v x))' = x'. [para(1769(a,1),742(a,1,2,1,1,1,2,1)),rewrite([1765(4),1069(7),1843(8),864(5),1069(6)]),flip(a)]. 5490 (x v y) v (x v z) = (x v z) v y. [para(1592(a,1),1166(a,1,2,1,2,1)),rewrite([1069(7),1544(7),436(3)]),flip(a)]. 6140 (x v y) v (x v z) = (x v y) v z. [para(1592(a,1),1192(a,1,2,1,2,1)),rewrite([436(5),1069(7),1860(7),436(3),436(6)]),flip(a)]. 6167 (x v y) v z = (x v z) v y. [back_rewrite(5490),rewrite([6140(3)])]. 6179 (x v y) v z = y v (x v z). [para(6167(a,1),1069(a,1))]. 6181 x v (y v z) = z v (y v x). [para(6167(a,1),999(a,1,2)),rewrite([6179(3),796(4),6179(4)])]. 6182 $F # answer(robbins_basis). [resolve(6181,a,1138,a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=301. Generated=97344. Kept=6179. proofs=1. Usable=197. Sos=3839. Demods=4043. Limbo=8, Disabled=2136. Hints=0. Kept_by_rule=0, Deleted_by_rule=126. Forward_subsumed=91039. Back_subsumed=477. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=6167 (8 lex), Back_demodulated=1656. Back_unit_deleted=0. Demod_attempts=1643085. Demod_rewrites=268729. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=2. Megabytes=7.92. User_CPU=3.01, System_CPU=0.05, Wall_clock=3. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 1 proof. Process 5156 exit (max_proofs) Tue Nov 3 09:48:32 2009