============================== Prover9 =============================== Prover9 (32) version November-2006, November 2006. Process 3926 was started by mccune on cleo.thornwood, Wed Nov 22 11:25:09 2006 The command was "/home/mccune/bin/prover9 -f omlsax2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file omlsax2.in assign(new_constants,1). assign(order,kbo). assign(eq_defs,fold). assign(max_weight,40). formulas(sos). f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x # label(OML_Sh). x v y = f(f(x,x),f(y,y)) # label(definition_join). x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). x' = f(x,x) # label(definition_complementation). end_of_list. formulas(goals). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS). f(f(x,x),f(x,y)) = x # answer(B_SS). f(x,f(x,f(x,y))) = f(x,y) # answer(OM_SS). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(goal). [goal]. 2 f(f(x,x),f(x,y)) = x # answer(B_SS) # label(goal). [goal]. 3 f(x,f(x,f(x,y))) = f(x,y) # answer(OM_SS) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [assumption]. x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. x' = f(x,x) # label(definition_complementation). [assumption]. f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [deny(2)]. f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [deny(3)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 3). % (Horn set with more than one neg. clause) Term ordering decisions: % Assigning unary symbol ' kb_weight 0 and highest precedence (12). Function symbol KB weights: c1=1. c2=1. c3=1. c4=1. c5=1. c6=1. c7=1. f=1. ^=1. v=1. '=0. Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, f, ^, v, ' ]). Skipping inverse_order, because term ordering is KBO. Folding symbols: '/1 ^/2 v/2. After fold_eq: Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, ^, v, ', f ]). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). Auto_process settings: (no changes). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 10 f(x,x) = x'. [copy(9),flip(a)]. 14 f(c4',f(c4,c5)) != c4 # answer(B_SS). [copy(13),rewrite(10(3))]. 15 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [deny(3)]. 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. 19 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(A_SS). [back_rewrite(12),rewrite(16(5),16(10))]. end_of_list. formulas(demodulators). 10 f(x,x) = x'. [copy(9),flip(a)]. 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 10 f(x,x) = x'. [copy(9),flip(a)]. given #2 (I,wt=8): 14 f(c4',f(c4,c5)) != c4 # answer(B_SS). [copy(13),rewrite(10(3))]. given #3 (I,wt=11): 15 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [deny(3)]. given #4 (I,wt=8): 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. given #5 (I,wt=9): 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. given #6 (I,wt=22): 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. given #7 (I,wt=11): 19 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(A_SS). [back_rewrite(12),rewrite(16(5),16(10))]. given #8 (F,wt=7): 20 x ^ x = x''. [para(10(a,1),16(a,1,1)),flip(a)]. given #9 (T,wt=7): 21 x v x = x''. [para(17(a,1),10(a,1))]. given #10 (T,wt=10): 22 (x v y)' = x' ^ y'. [para(17(a,1),16(a,1,1))]. given #11 (A,wt=12): 23 f(x ^ y,z') = f(x,y) v z. [para(16(a,1),17(a,1,1))]. given #12 (F,wt=12): 24 f(x',y ^ z) = x v f(y,z). [para(16(a,1),17(a,1,2))]. given #13 (F,wt=15): 38 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(16(a,1),23(a,1,2))]. given #14 (T,wt=18): 27 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),18(a,1,1,1)),rewrite(10(1))]. given #15 (T,wt=17): 44 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),27(a,1,1))]. given #16 (A,wt=21): 25 f(f(f(x',f(x,y)),z),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),18(a,1,1,1,1))]. given #17 (F,wt=17): 47 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(17(a,1),27(a,1,1))]. given #18 (F,wt=17): 68 f(x,f(x',f(f(y,f(x'',y)),y))) = x'. [para(27(a,1),25(a,1,1))]. given #19 (T,wt=18): 51 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(44(a,1),16(a,1,1)),flip(a)]. given #20 (T,wt=18): 69 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(47(a,1),16(a,1,1)),flip(a)]. given #21 (A,wt=21): 26 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),18(a,1,1,1,2))]. given #22 (F,wt=18): 74 f(x,f(x',f(x' v x'',x''))) = x'. [para(10(a,1),68(a,1,2,2,1,2)),rewrite(17(7))]. given #23 (F,wt=18): 75 x ^ f(x',f(f(y,f(x'',y)),y)) = x''. [para(68(a,1),16(a,1,1)),flip(a)]. given #24 (T,wt=18): 77 f(x,f(x',f(f(y',x' v y),y'))) = x'. [para(17(a,1),68(a,1,2,2,1,2))]. given #25 (T,wt=19): 36 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(18(a,1),18(a,1,1)),rewrite(16(3))]. given #26 (A,wt=20): 28 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y',z)),z))) = y. [para(10(a,1),18(a,1,1)),rewrite(16(4))]. given #27 (F,wt=17): 118 f(x''',f(x,f(f(y,f(x',y)),y))) = x. [para(44(a,1),36(a,1,2,1)),rewrite(51(12),44(18))]. given #28 (F,wt=16): 135 f(x''',f(x,f(x v x',x'))) = x. [para(10(a,1),118(a,1,2,2,1,2)),rewrite(17(7))]. given #29 (T,wt=17): 120 f(x' v y,f(x,f(f(z,f(x',z)),z))) = x. [para(47(a,1),36(a,1,2,1)),rewrite(69(10),47(16))]. given #30 (T,wt=16): 150 f(x' v y,f(x,f(x v x',x'))) = x. [para(10(a,1),120(a,1,2,2,1,2)),rewrite(17(6))]. given #31 (A,wt=22): 29 f(f(f(f(x,y),f(y,y')),z),f(y,f(y v y',y'))) = y. [para(10(a,1),18(a,1,2,2,1,2)),rewrite(17(9))]. given #32 (F,wt=17): 144 x''' ^ f(x,f(x v x',x')) = x'. [para(135(a,1),16(a,1,1)),flip(a)]. given #33 (F,wt=17): 158 (x' v y) ^ f(x,f(x v x',x')) = x'. [para(150(a,1),16(a,1,1)),flip(a)]. given #34 (T,wt=18): 117 f(f(x'',y),f(x,f(f(z,f(x',z)),z))) = x. [para(27(a,1),36(a,1,2,1)),rewrite(45(12),27(18))]. given #35 (T,wt=17): 171 f(f(x'',y),f(x,f(x v x',x'))) = x. [para(10(a,1),117(a,1,2,2,1,2)),rewrite(17(7))]. given #36 (A,wt=23): 30 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(z,f(y',z)),z)) = y'. [para(18(a,1),16(a,1,1)),flip(a)]. given #37 (F,wt=18): 136 x''' ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(118(a,1),16(a,1,1)),flip(a)]. given #38 (F,wt=18): 138 f(x''',f(x,f(f(y',x v y),y'))) = x. [para(17(a,1),118(a,1,2,2,1,2))]. given #39 (T,wt=18): 151 (x' v y) ^ f(x,f(f(z,f(x',z)),z)) = x'. [para(120(a,1),16(a,1,1)),flip(a)]. given #40 (T,wt=18): 153 f(x' v y,f(x,f(f(z',x v z),z'))) = x. [para(17(a,1),120(a,1,2,2,1,2))]. given #41 (A,wt=31): 31 f(f(f(f(x,f(y,z)),f(f(y,z),u)),v),f(f(y,z),f(f(u,f(y ^ z,u)),u))) = f(y,z). [para(16(a,1),18(a,1,2,2,1,2,1))]. given #42 (F,wt=18): 179 f(x'',y) ^ f(x,f(x v x',x')) = x'. [para(171(a,1),16(a,1,1)),flip(a)]. given #43 (F,wt=19): 57 f(x' ^ f(x,y),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),25(a,1,1)),rewrite(16(4))]. given #44 (T,wt=19): 89 f(f(x,y) ^ y',f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),26(a,1,1)),rewrite(16(4))]. given #45 (T,wt=19): 97 x ^ f(x',f(x' v x'',x'')) = x''. [para(74(a,1),16(a,1,1)),flip(a)]. given #46 (A,wt=26): 32 f(f(f(x v y,f(y',z)),u),f(y',f(f(z,f(y'',z)),z))) = y'. [para(17(a,1),18(a,1,1,1,1))]. given #47 (F,wt=19): 101 x ^ f(x',f(f(y',x' v y),y')) = x''. [para(17(a,1),75(a,1,2,2,1,2))]. given #48 (F,wt=19): 109 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(36(a,1),16(a,1,1)),rewrite(16(2)),flip(a)]. given #49 (T,wt=19): 172 f(x'',y) ^ f(x,f(f(z,f(x',z)),z)) = x'. [para(117(a,1),16(a,1,1)),flip(a)]. given #50 (T,wt=19): 174 f(f(x'',y),f(x,f(f(z',x v z),z'))) = x. [para(17(a,1),117(a,1,2,2,1,2))]. given #51 (A,wt=27): 33 f(f(f(f(x,y'),y v z),u),f(y',f(f(z',y' v z),z'))) = y'. [para(17(a,1),18(a,1,1,1,2)),rewrite(17(11))]. given #52 (F,wt=19): 195 x''' ^ f(x,f(f(y',x v y),y')) = x'. [para(17(a,1),136(a,1,2,2,1,2))]. given #53 (F,wt=19): 208 (x' v y) ^ f(x,f(f(z',x v z),z')) = x'. [para(17(a,1),151(a,1,2,2,1,2))]. given #54 (T,wt=19): 219 f(x' ^ f(x,x'),f(x,f(x v x',x'))) = x. [para(10(a,1),57(a,1,2,2,1,2)),rewrite(17(8))]. given #55 (T,wt=19): 229 f(x' ^ f(x,y),f(x,f(f(z,f(x',z)),z))) = x. [para(57(a,1),36(a,1,2,1)),rewrite(220(12),57(18))]. given #56 (A,wt=24): 34 f(f(f(f(x,y),f(y,z')),u),f(y,f(f(z',y v z),z'))) = y. [para(17(a,1),18(a,1,2,2,1,2))]. given #57 (F,wt=18): 284 f(x' ^ f(x,y),f(x,f(x v x',x'))) = x. [para(10(a,1),229(a,1,2,2,1,2)),rewrite(17(7))]. given #58 (F,wt=19): 238 f(f(x,y) ^ y',f(y,f(f(z,f(y',z)),z))) = y. [para(89(a,1),36(a,1,2,1)),rewrite(231(12),89(18))]. given #59 (T,wt=18): 312 f(f(x,y) ^ y',f(y,f(y v y',y'))) = y. [para(10(a,1),238(a,1,2,2,1,2)),rewrite(17(7))]. given #60 (T,wt=19): 302 (x' ^ f(x,y)) ^ f(x,f(x v x',x')) = x'. [para(284(a,1),16(a,1,1)),flip(a)]. given #61 (A,wt=37): 35 f(f(x,y),f(x,f(f(f(f(z,f(x',z)),z),f(x',f(f(z,f(x',z)),z))),f(f(z,f(x',z)),z)))) = x. [para(18(a,1),18(a,1,1,1))]. given #62 (F,wt=12): 361 f(x',f(x'',x)) = x''. [back_rewrite(147),rewrite(341(15))]. given #63 (F,wt=13): 360 x' ^ f(x'',x) = x'''. [back_rewrite(148),rewrite(341(15))]. given #64 (T,wt=14): 363 f(x'',x'' v x) = x'''. [para(17(a,1),361(a,1,2))]. given #65 (T,wt=15): 341 f(f(x,y),f(y,f(y v y',y'))) = y. [para(35(a,1),29(a,1,1))]. given #66 (A,wt=33): 37 f(f(f(f(x,y v z),f(y v z,u)),v),f(y v z,f(f(u,f(y' ^ z',u)),u))) = y v z. [para(22(a,1),18(a,1,2,2,1,2,1))]. given #67 (F,wt=14): 393 f(x',f(x,f(x v x',x'))) = x. [para(10(a,1),341(a,1,1))]. given #68 (F,wt=7): 417 x'' v x = x. [para(393(a,1),118(a,1,2,2,1,2)),rewrite(341(15),10(4),17(5))]. given #69 (T,wt=8): 414 f(x,x'') = x'. [para(393(a,1),68(a,1,2,2,1,2)),rewrite(341(22),10(3))]. given #70 (T,wt=9): 415 x ^ x'' = x''. [para(393(a,1),75(a,1,2,2,1,2)),rewrite(341(22),10(3))]. given #71 (A,wt=33): 39 f(f(f(f(x,y ^ z),f(y,z) v u),v),f(y ^ z,f(f(u',(y ^ z) v u),u'))) = y ^ z. [para(23(a,1),18(a,1,1,1,2)),rewrite(17(12))]. given #72 (F,wt=9): 418 f(x' v y,x') = x. [para(393(a,1),120(a,1,2,2,1,2)),rewrite(341(14),10(3))]. given #73 (F,wt=9): 443 x''''' = x'. [back_rewrite(420),rewrite(439(5))]. given #74 (T,wt=7): 522 x'''' = x. [para(443(a,1),414(a,1,2)),rewrite(17(5),417(3)),flip(a)]. ============================== PROOF ================================= % Proof 1 at 0.06 (+ 0.00) seconds: B_SS. % Length of proof is 66. % Level of proof is 19. % Maximum clause weight is 38. % Given clauses 74. 2 f(f(x,x),f(x,y)) = x # answer(B_SS) # label(goal). [goal]. 4 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [assumption]. 5 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 6 f(f(x,x),f(y,y)) = x v y. [copy(5),flip(a)]. 7 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 8 f(f(x,y),f(x,y)) = x ^ y. [copy(7),flip(a)]. 9 x' = f(x,x) # label(definition_complementation). [assumption]. 10 f(x,x) = x'. [copy(9),flip(a)]. 13 f(f(c4,c4),f(c4,c5)) != c4 # answer(B_SS). [deny(2)]. 14 f(c4',f(c4,c5)) != c4 # answer(B_SS). [copy(13),rewrite(10(3))]. 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. 22 (x v y)' = x' ^ y'. [para(17(a,1),16(a,1,1))]. 25 f(f(f(x',f(x,y)),z),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),18(a,1,1,1,1))]. 27 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),18(a,1,1,1)),rewrite(10(1))]. 29 f(f(f(f(x,y),f(y,y')),z),f(y,f(y v y',y'))) = y. [para(10(a,1),18(a,1,2,2,1,2)),rewrite(17(9))]. 35 f(f(x,y),f(x,f(f(f(f(z,f(x',z)),z),f(x',f(f(z,f(x',z)),z))),f(f(z,f(x',z)),z)))) = x. [para(18(a,1),18(a,1,1,1))]. 36 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(18(a,1),18(a,1,1)),rewrite(16(3))]. 44 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),27(a,1,1))]. 45 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(27(a,1),16(a,1,1)),flip(a)]. 47 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(17(a,1),27(a,1,1))]. 51 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(44(a,1),16(a,1,1)),flip(a)]. 57 f(x' ^ f(x,y),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),25(a,1,1)),rewrite(16(4))]. 68 f(x,f(x',f(f(y,f(x'',y)),y))) = x'. [para(27(a,1),25(a,1,1))]. 69 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(47(a,1),16(a,1,1)),flip(a)]. 75 x ^ f(x',f(f(y,f(x'',y)),y)) = x''. [para(68(a,1),16(a,1,1)),flip(a)]. 109 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(36(a,1),16(a,1,1)),rewrite(16(2)),flip(a)]. 117 f(f(x'',y),f(x,f(f(z,f(x',z)),z))) = x. [para(27(a,1),36(a,1,2,1)),rewrite(45(12),27(18))]. 118 f(x''',f(x,f(f(y,f(x',y)),y))) = x. [para(44(a,1),36(a,1,2,1)),rewrite(51(12),44(18))]. 120 f(x' v y,f(x,f(f(z,f(x',z)),z))) = x. [para(47(a,1),36(a,1,2,1)),rewrite(69(10),47(16))]. 135 f(x''',f(x,f(x v x',x'))) = x. [para(10(a,1),118(a,1,2,2,1,2)),rewrite(17(7))]. 136 x''' ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(118(a,1),16(a,1,1)),flip(a)]. 148 x' ^ f(x'',f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x'''. [para(135(a,1),75(a,1,2,2,1,2))]. 174 f(f(x'',y),f(x,f(f(z',x v z),z'))) = x. [para(17(a,1),117(a,1,2,2,1,2))]. 220 (x' ^ f(x,y)) ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(57(a,1),16(a,1,1)),flip(a)]. 229 f(x' ^ f(x,y),f(x,f(f(z,f(x',z)),z))) = x. [para(57(a,1),36(a,1,2,1)),rewrite(220(12),57(18))]. 284 f(x' ^ f(x,y),f(x,f(x v x',x'))) = x. [para(10(a,1),229(a,1,2,2,1,2)),rewrite(17(7))]. 307 f(x',f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x'))))) = f(x',f(x,y)). [para(284(a,1),36(a,1,2,2,1,2))]. 311 x' ^ f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x' ^ f(x,y). [para(284(a,1),109(a,1,2,2,1,2))]. 341 f(f(x,y),f(y,f(y v y',y'))) = y. [para(35(a,1),29(a,1,1))]. 351 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [back_rewrite(311),rewrite(341(16))]. 352 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [back_rewrite(307),rewrite(341(16))]. 360 x' ^ f(x'',x) = x'''. [back_rewrite(148),rewrite(341(15))]. 380 x'' ^ (x'' v x) = x''''. [para(17(a,1),360(a,1,2))]. 393 f(x',f(x,f(x v x',x'))) = x. [para(10(a,1),341(a,1,1))]. 414 f(x,x'') = x'. [para(393(a,1),68(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 415 x ^ x'' = x''. [para(393(a,1),75(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 417 x'' v x = x. [para(393(a,1),118(a,1,2,2,1,2)),rewrite(341(15),10(4),17(5))]. 418 f(x' v y,x') = x. [para(393(a,1),120(a,1,2,2,1,2)),rewrite(341(14),10(3))]. 420 x''' ^ x' = x'. [para(393(a,1),136(a,1,2,2,1,2)),rewrite(341(15),10(4))]. 424 f(x',f(x,f(f(y',x v y),y'))) = x. [para(393(a,1),174(a,1,1))]. 439 x'' ^ x = x''''. [back_rewrite(380),rewrite(417(5))]. 443 x''''' = x'. [back_rewrite(420),rewrite(439(5))]. 522 x'''' = x. [para(443(a,1),414(a,1,2)),rewrite(17(5),417(3)),flip(a)]. 533 x'' ^ x = x. [back_rewrite(439),rewrite(522(7))]. 535 f(x,y) = (x ^ y)'''. [para(16(a,1),522(a,1,1,1,1)),flip(a)]. 536 (x ^ y')''' = x''' v y. [para(522(a,1),17(a,1,1)),rewrite(535(2))]. 537 (x' ^ y)''' = x v y'''. [para(522(a,1),17(a,1,2)),rewrite(535(2))]. 584 ((x v y) ^ x)''' = x'''. [para(522(a,1),418(a,1,1,1)),rewrite(522(5),535(2))]. 611 x v (x ^ ((y' ^ (x v y))'' v y))'' = x. [back_rewrite(424),rewrite(535(4),537(7),22(3),535(9),536(12),22(8),536(8),522(6),535(8),535(12),536(15),522(4))]. 625 x v (x ^ y)'' = x''. [back_rewrite(352),rewrite(535(3),535(7),536(10),522(5),535(6),584(9),535(5),415(5),522(4),535(4),535(8),536(11),522(6)),flip(a)]. 626 x' ^ (x ^ y)''' = x'''. [back_rewrite(351),rewrite(535(3),535(7),536(10),522(5),625(5),535(4),533(4),415(5),535(5)),flip(a)]. 697 c4'' != c4 # answer(B_SS). [back_rewrite(14),rewrite(535(5),535(9),626(9),522(5))]. 699 x'' = x. [back_rewrite(611),rewrite(625(10))]. 700 $F # answer(B_SS). [resolve(699,a,697,a)]. ============================== end of proof ========================== % Redundant proof: 744 $F # answer(B_SS). [back_rewrite(697),rewrite(699(3)),xx(a)]. % Disable descendants (x means already disabled): 13x 14x 697x given #75 (T,wt=5): 699 x'' = x. [back_rewrite(611),rewrite(625(10))]. given #76 (A,wt=10): 421 (x' v y) ^ x' = x'. [para(393(a,1),151(a,1,2,2,1,2)),rewrite(341(14),10(3))]. given #77 (F,wt=14): 745 (c6 ^ (c6' v (c6 ^ c7)))' != (c6 ^ c7)' # answer(OM_SS). [back_rewrite(696),rewrite(699(4),699(8),699(10),699(14))]. given #78 (F,wt=15): 746 c2' v (c1 ^ c3)' != c1' v (c2 ^ c3)' # answer(A_SS). [back_rewrite(695),rewrite(699(3),699(7),699(10),699(14))]. given #79 (T,wt=5): 820 x v x = x. [back_rewrite(21),rewrite(699(3))]. given #80 (T,wt=5): 821 x ^ x = x. [back_rewrite(20),rewrite(699(3))]. given #81 (A,wt=25): 707 (x v y) ^ ((x v y) v ((z ^ ((x' ^ y') v z'))' ^ z)) = x v y. [back_rewrite(689),rewrite(699(7),699(10),699(12),698(16))]. given #82 (F,wt=7): 790 x v (x ^ y) = x. [back_rewrite(625),rewrite(699(3),699(4))]. given #83 (F,wt=7): 823 (x v y) ^ x = x. [para(699(a,1),421(a,1,1,1)),rewrite(699(3),699(4))]. given #84 (T,wt=8): 819 f(x,y) = (x ^ y)'. [back_rewrite(535),rewrite(699(4))]. given #85 (T,wt=9): 797 ((x ^ y) v y) v y = y. [back_rewrite(609),rewrite(699(3))]. given #86 (A,wt=25): 714 (((x' v y) ^ (y v z)) v u') ^ (y v ((z v (y ^ z')) ^ z')) = y. [back_rewrite(670),rewrite(699(2),699(6),699(6),699(8),699(10),699(13),699(15))]. given #87 (F,wt=9): 829 (x v y) v x = x v y. [para(823(a,1),790(a,1,2))]. given #88 (F,wt=9): 863 x v ((y ^ x) v x) = x. [para(797(a,1),829(a,1,1)),rewrite(797(6))]. given #89 (T,wt=10): 789 x' ^ (x ^ y)' = x'. [back_rewrite(626),rewrite(699(4),699(6))]. given #90 (T,wt=8): 866 x ^ (x v y') = x. [para(699(a,1),789(a,1,1)),rewrite(817(3),699(5))]. given #91 (A,wt=25): 723 ((x' ^ y') v y') v (y' ^ ((z ^ (y' v z')) v z')) = y'. [back_rewrite(641),rewrite(698(4),22(2),699(9),699(12),699(12),699(15))]. given #92 (F,wt=7): 871 x ^ (x v y) = x. [para(699(a,1),866(a,1,2,2))]. given #93 (F,wt=10): 817 (x' ^ y)' = x v y'. [back_rewrite(537),rewrite(699(4),699(5))]. given #94 (T,wt=9): 897 f(x,y) = x' v y'. [back_rewrite(819),rewrite(887(3))]. given #95 (T,wt=10): 887 (x ^ y)' = x' v y'. [para(699(a,1),817(a,1,1,1))]. given #96 (A,wt=21): 753 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u')) v u')) = y. [back_rewrite(686),rewrite(699(3),699(5),699(5),699(8),699(8),699(11))]. given #97 (F,wt=16): 914 c6' v (c6 ^ (c6' v c7')) != c6' v c7' # answer(OM_SS). [back_rewrite(745),rewrite(887(9),22(9),699(5),887(7),887(14))]. given #98 (F,wt=17): 913 c2' v (c1' v c3') != c1' v (c2' v c3') # answer(A_SS). [back_rewrite(746),rewrite(887(6),887(14))]. given #99 (T,wt=7): 933 (x ^ y) v x = x. [para(753(a,1),753(a,1,1,1)),rewrite(925(7),925(7),925(7),925(8))]. given #100 (T,wt=7): 934 (x ^ y) v y = y. [back_rewrite(924),rewrite(925(7))]. given #101 (A,wt=21): 757 ((x ^ y) v (y ^ z')) v (y ^ ((z' ^ (y v z)) v z)) = y. [back_rewrite(681),rewrite(699(3),699(5),699(9),699(11))]. given #102 (F,wt=7): 945 x v (y ^ x) = x. [para(934(a,1),829(a,1,1)),rewrite(934(4))]. given #103 (F,wt=9): 938 (x ^ y) ^ x = x ^ y. [back_rewrite(929),rewrite(934(2),934(4))]. given #104 (T,wt=9): 940 x ^ (x ^ y) = x ^ y. [back_rewrite(923),rewrite(934(2),934(4))]. given #105 (T,wt=9): 942 x v (x v y) = x v y. [back_rewrite(840),rewrite(934(7))]. given #106 (A,wt=21): 769 x ^ ((x ^ y) v ((z v ((x ^ y) ^ z')) ^ z')) = x ^ y. [back_rewrite(657),rewrite(699(3),699(6),699(9))]. given #107 (F,wt=9): 944 x ^ (y ^ x) = y ^ x. [para(934(a,1),823(a,1,1))]. given #108 (F,wt=9): 946 (x ^ y) ^ y = x ^ y. [para(934(a,1),871(a,1,2))]. given #109 (T,wt=10): 947 (x v x') ^ x' = x'. [back_rewrite(894),rewrite(943(5),944(6))]. given #110 (T,wt=8): 971 (x' v x) ^ x = x. [para(699(a,1),947(a,1,1,2)),rewrite(699(4),699(5))]. given #111 (A,wt=20): 777 x v ((x v y) ^ ((z' ^ ((x v y) v z)) v z)) = x v y. [back_rewrite(644),rewrite(699(7),699(9))]. given #112 (F,wt=8): 983 x ^ (x' v x) = x. [para(971(a,1),938(a,1,1)),rewrite(971(6))]. given #113 (F,wt=10): 976 x' ^ (x v x') = x'. [para(947(a,1),938(a,1,1)),rewrite(947(8))]. given #114 (T,wt=11): 936 ((x ^ y) v (y ^ z)) v y = y. [back_rewrite(758),rewrite(925(9))]. given #115 (T,wt=11): 943 (x' v y') ^ y' = y'. [para(934(a,1),22(a,1,1)),rewrite(887(3)),flip(a)]. given #116 (A,wt=16): 785 (x ^ y) v (y ^ ((z' ^ (y v z)) v z)) = y. [back_rewrite(630),rewrite(699(3),699(6),699(8))]. given #117 (F,wt=8): 1013 (x' v y) ^ y = y. [para(699(a,1),943(a,1,1,2)),rewrite(699(4),699(5))]. given #118 (F,wt=7): 1024 (x v y) ^ y = y. [para(699(a,1),1013(a,1,1,1))]. given #119 (T,wt=7): 1032 x ^ (y v x) = x. [para(1024(a,1),938(a,1,1)),rewrite(1024(4))]. given #120 (T,wt=9): 1030 (x v y) v y = x v y. [para(1024(a,1),790(a,1,2))]. given #121 (A,wt=17): 807 (x v y) ^ (x v ((z v (x ^ z')) ^ z')) = x. [back_rewrite(576),rewrite(699(3),699(5),699(8))]. given #122 (F,wt=9): 1031 x v (y v x) = y v x. [para(1024(a,1),933(a,1,1))]. given #123 (F,wt=11): 998 x v ((y ^ x) v (x ^ z)) = x. [para(936(a,1),829(a,1,1)),rewrite(936(8))]. given #124 (T,wt=11): 1001 ((x ^ y) v (x ^ z)) v x = x. [para(938(a,1),936(a,1,1,1))]. given #125 (T,wt=11): 1002 ((x ^ y) v (z ^ y)) v y = y. [para(944(a,1),936(a,1,1,2))]. given #126 (A,wt=16): 812 (x v y) ^ (x v ((z' v (x ^ z)) ^ z)) = x. [back_rewrite(563),rewrite(699(3),699(3),699(5),699(7))]. given #127 (F,wt=11): 1048 x v ((x ^ y) v (x ^ z)) = x. [para(938(a,1),998(a,1,2,1))]. given #128 (F,wt=11): 1049 x v ((y ^ x) v (z ^ x)) = x. [para(944(a,1),998(a,1,2,2))]. given #129 (T,wt=11): 1056 ((x ^ y) v (z ^ x)) v x = x. [para(944(a,1),1001(a,1,1,2))]. given #130 (T,wt=11): 1075 x v ((x ^ y) v (z ^ x)) = x. [para(944(a,1),1048(a,1,2,2))]. given #131 (A,wt=35): 849 (((x' v y) ^ (y v (z v u))) v v') ^ (y v (((z v u) v (y ^ (z' ^ u'))) ^ (z' ^ u'))) = y. [para(22(a,1),714(a,1,2,2,1,2,2)),rewrite(22(15))]. given #132 (F,wt=12): 1021 x ^ ((y' ^ (x v y)) v y) = x. [para(785(a,1),933(a,1)),flip(a)]. given #133 (F,wt=12): 1067 x v ((y' v (x ^ y)) ^ y) = x. [para(812(a,1),821(a,1)),flip(a)]. given #134 (T,wt=12): 1104 ((x' ^ (y v x)) v x) ^ y = y. [para(1021(a,1),944(a,1,2)),rewrite(1021(10))]. given #135 (T,wt=12): 1126 ((x' v (y ^ x)) ^ x) v y = y. [para(1067(a,1),1031(a,1,2)),rewrite(1067(10))]. given #136 (A,wt=25): 856 (((x' v y) ^ (y v z)) v u') v y = ((x' v y) ^ (y v z)) v u'. [para(714(a,1),790(a,1,2))]. given #137 (F,wt=13): 925 x ^ ((y ^ (x v y')) v y') = x. [para(753(a,1),797(a,1,1)),rewrite(790(7)),flip(a)]. given #138 (F,wt=13): 935 (((x ^ y) v (y ^ z)) ^ u) v y = y. [back_rewrite(805),rewrite(925(10))]. given #139 (T,wt=9): 1188 ((x ^ y) ^ z) v x = x. [para(933(a,1),935(a,1,1,1))]. given #140 (T,wt=9): 1189 ((x ^ y) ^ z) v y = y. [para(945(a,1),935(a,1,1,1))]. given #141 (A,wt=29): 964 x ^ ((x ^ y) v (((z v u) v ((x ^ y) ^ (z' ^ u'))) ^ (z' ^ u'))) = x ^ y. [para(22(a,1),769(a,1,2,2,1,2,2)),rewrite(22(10))]. given #142 (F,wt=9): 1201 x v ((x ^ y) ^ z) = x. [para(1188(a,1),829(a,1,1)),rewrite(1188(6))]. given #143 (F,wt=9): 1203 (x ^ (y ^ z)) v y = y. [para(944(a,1),1188(a,1,1))]. given #144 (T,wt=9): 1208 x v ((y ^ x) ^ z) = x. [para(1189(a,1),829(a,1,1)),rewrite(1189(6))]. given #145 (T,wt=9): 1210 (x ^ (y ^ z)) v z = z. [para(944(a,1),1189(a,1,1))]. given #146 (A,wt=29): 965 x ^ ((x ^ y) v (((z ^ u) v ((x ^ y) ^ (z' v u'))) ^ (z' v u'))) = x ^ y. [para(887(a,1),769(a,1,2,2,1,2,2)),rewrite(887(10))]. given #147 (F,wt=9): 1225 x v (y ^ (x ^ z)) = x. [para(944(a,1),1201(a,1,2))]. given #148 (F,wt=9): 1243 x v (y ^ (z ^ x)) = x. [para(944(a,1),1208(a,1,2))]. given #149 (T,wt=11): 1200 (x ^ y) v (x v z) = x v z. [para(823(a,1),1188(a,1,1,1))]. given #150 (T,wt=11): 1204 (x ^ y) v (z v x) = z v x. [para(1024(a,1),1188(a,1,1,1))]. given #151 (A,wt=21): 970 x ^ ((x ^ y') v ((y v (x ^ y')) ^ y')) = x ^ y'. [para(946(a,1),769(a,1,2,2,1,2))]. given #152 (F,wt=11): 1224 (x v y) v (x ^ z) = x v y. [para(823(a,1),1201(a,1,2,1))]. given #153 (F,wt=11): 1226 (x v y) v (y ^ z) = x v y. [para(1024(a,1),1201(a,1,2,1))]. given #154 (T,wt=11): 1238 (x ^ y) v (y v z) = y v z. [para(823(a,1),1203(a,1,1,2))]. given #155 (T,wt=11): 1240 (x ^ y) v (z v y) = z v y. [para(1024(a,1),1203(a,1,1,2))]. given #156 (A,wt=24): 978 ((x ^ (y v y')) v y') v ((y v y') ^ (y' v y)) = y v y'. [back_rewrite(975),rewrite(976(11))]. given #157 (F,wt=11): 1268 (x v y) v (z ^ x) = x v y. [para(823(a,1),1225(a,1,2,2))]. given #158 (F,wt=11): 1269 (x v y) v (z ^ y) = x v y. [para(1024(a,1),1225(a,1,2,2))]. given #159 (T,wt=11): 1278 (x v y) ^ (x ^ z) = x ^ z. [para(1200(a,1),823(a,1,1))]. given #160 (T,wt=9): 1383 ((x v y) v z) ^ x = x. [para(823(a,1),1278(a,1,2)),rewrite(823(5))]. given #161 (A,wt=17): 996 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(936(a,1),823(a,1,1))]. given #162 (F,wt=9): 1385 ((x v y) v z) ^ y = y. [para(1024(a,1),1278(a,1,2)),rewrite(1024(5))]. given #163 (F,wt=9): 1416 x ^ ((x v y) v z) = x. [para(1383(a,1),938(a,1,1)),rewrite(1383(6))]. given #164 (T,wt=9): 1419 (x v (y v z)) ^ y = y. [para(1031(a,1),1383(a,1,1))]. given #165 (T,wt=9): 1489 x ^ ((y v x) v z) = x. [para(1385(a,1),938(a,1,1)),rewrite(1385(6))]. given #166 (A,wt=15): 997 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(823(a,1),936(a,1,1,2))]. given #167 (F,wt=9): 1491 (x v (y v z)) ^ z = z. [para(1031(a,1),1385(a,1,1))]. given #168 (F,wt=9): 1513 x ^ (y v (x v z)) = x. [para(1031(a,1),1416(a,1,2))]. given #169 (T,wt=9): 1565 x ^ (y v (z v x)) = x. [para(1031(a,1),1489(a,1,2))]. given #170 (T,wt=11): 1280 (x ^ y) ^ (x v z) = x ^ y. [para(1200(a,1),871(a,1,2))]. given #171 (A,wt=17): 999 ((x ^ y) v (y ^ z)) ^ y = (x ^ y) v (y ^ z). [para(936(a,1),871(a,1,2))]. given #172 (F,wt=11): 1286 (((x ^ y) ^ z) ^ u) v x = x. [para(1188(a,1),1200(a,1,2)),rewrite(1188(7))]. given #173 (F,wt=11): 1287 (((x ^ y) ^ z) ^ u) v y = y. [para(1189(a,1),1200(a,1,2)),rewrite(1189(7))]. given #174 (T,wt=11): 1288 ((x ^ (y ^ z)) ^ u) v y = y. [para(1203(a,1),1200(a,1,2)),rewrite(1203(7))]. given #175 (T,wt=11): 1289 ((x ^ (y ^ z)) ^ u) v z = z. [para(1210(a,1),1200(a,1,2)),rewrite(1210(7))]. given #176 (A,wt=15): 1000 (x v ((x v y) ^ z)) v (x v y) = x v y. [para(871(a,1),936(a,1,1,1))]. given #177 (F,wt=11): 1292 (x v y) ^ (y ^ z) = y ^ z. [para(1204(a,1),823(a,1,1))]. given #178 (F,wt=11): 1294 (x ^ y) ^ (z v x) = x ^ y. [para(1204(a,1),871(a,1,2))]. given #179 (T,wt=11): 1312 x v (((x ^ y) ^ z) ^ u) = x. [para(1188(a,1),1224(a,1,1)),rewrite(1188(7))]. given #180 (T,wt=11): 1313 x v (((y ^ x) ^ z) ^ u) = x. [para(1189(a,1),1224(a,1,1)),rewrite(1189(7))]. given #181 (A,wt=24): 1008 x v ((((x' ^ y') v z') ^ (x v y)) v ((x v y) ^ z)) = x v y. [back_rewrite(986),rewrite(996(12))]. given #182 (F,wt=11): 1315 x v ((y ^ (x ^ z)) ^ u) = x. [para(1203(a,1),1224(a,1,1)),rewrite(1203(7))]. given #183 (F,wt=11): 1316 x v ((y ^ (z ^ x)) ^ u) = x. [para(1210(a,1),1224(a,1,1)),rewrite(1210(7))]. given #184 (T,wt=11): 1328 (x v y) ^ (z ^ x) = z ^ x. [para(1238(a,1),823(a,1,1))]. given #185 (T,wt=11): 1329 (x ^ y) ^ (y v z) = x ^ y. [para(1238(a,1),871(a,1,2))]. given #186 (A,wt=15): 1034 ((x ^ (y v z)) v z) v (y v z) = y v z. [para(1024(a,1),936(a,1,1,2))]. given #187 (F,wt=11): 1336 (x ^ ((y ^ z) ^ u)) v y = y. [para(1188(a,1),1238(a,1,2)),rewrite(1188(7))]. given #188 (F,wt=11): 1337 (x ^ ((y ^ z) ^ u)) v z = z. [para(1189(a,1),1238(a,1,2)),rewrite(1189(7))]. given #189 (T,wt=11): 1338 (x ^ (y ^ (z ^ u))) v z = z. [para(1203(a,1),1238(a,1,2)),rewrite(1203(7))]. given #190 (T,wt=11): 1339 (x ^ (y ^ (z ^ u))) v u = u. [para(1210(a,1),1238(a,1,2)),rewrite(1210(7))]. given #191 (A,wt=15): 1035 (x v ((y v x) ^ z)) v (y v x) = y v x. [para(1032(a,1),936(a,1,1,1))]. given #192 (F,wt=11): 1346 (x v y) ^ (z ^ y) = z ^ y. [para(1240(a,1),823(a,1,1))]. given #193 (F,wt=11): 1347 (x ^ y) ^ (z v y) = x ^ y. [para(1240(a,1),871(a,1,2))]. given #194 (T,wt=11): 1371 x v (y ^ ((x ^ z) ^ u)) = x. [para(1188(a,1),1268(a,1,1)),rewrite(1188(7))]. given #195 (T,wt=11): 1372 x v (y ^ ((z ^ x) ^ u)) = x. [para(1189(a,1),1268(a,1,1)),rewrite(1189(7))]. given #196 (A,wt=25): 1036 (x v y) ^ (x v (((z v u) v (x ^ (z' ^ u'))) ^ (z' ^ u'))) = x. [para(22(a,1),807(a,1,2,2,1,2,2)),rewrite(22(9))]. given #197 (F,wt=11): 1373 x v (y ^ (z ^ (x ^ u))) = x. [para(1203(a,1),1268(a,1,1)),rewrite(1203(7))]. given #198 (F,wt=11): 1374 x v (y ^ (z ^ (u ^ x))) = x. [para(1210(a,1),1268(a,1,1)),rewrite(1210(7))]. given #199 (T,wt=11): 1447 (((x v y) v z) v u) ^ x = x. [para(1383(a,1),1278(a,1,2)),rewrite(1383(7))]. given #200 (T,wt=11): 1510 (((x v y) v z) v u) ^ y = y. [para(1385(a,1),1278(a,1,2)),rewrite(1385(7))]. given #201 (A,wt=13): 1037 x v ((y v (x ^ y')) ^ y') = x. [para(807(a,1),821(a,1)),flip(a)]. given #202 (F,wt=11): 1563 ((x v (y v z)) v u) ^ y = y. [para(1419(a,1),1278(a,1,2)),rewrite(1419(7))]. given #203 (F,wt=11): 1573 (x v y) v (y v x) = y v x. [para(1032(a,1),997(a,1,1,1))]. % Operation v is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 2 at 0.20 (+ 0.00) seconds: OM_SS. % Length of proof is 112. % Level of proof is 28. % Maximum clause weight is 38. % Given clauses 203. 3 f(x,f(x,f(x,y))) = f(x,y) # answer(OM_SS) # label(goal). [goal]. 4 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [assumption]. 5 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 6 f(f(x,x),f(y,y)) = x v y. [copy(5),flip(a)]. 7 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 8 f(f(x,y),f(x,y)) = x ^ y. [copy(7),flip(a)]. 9 x' = f(x,x) # label(definition_complementation). [assumption]. 10 f(x,x) = x'. [copy(9),flip(a)]. 15 f(c6,f(c6,f(c6,c7))) != f(c6,c7) # answer(OM_SS). [deny(3)]. 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. 22 (x v y)' = x' ^ y'. [para(17(a,1),16(a,1,1))]. 23 f(x ^ y,z') = f(x,y) v z. [para(16(a,1),17(a,1,1))]. 25 f(f(f(x',f(x,y)),z),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),18(a,1,1,1,1))]. 26 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),18(a,1,1,1,2))]. 27 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),18(a,1,1,1)),rewrite(10(1))]. 28 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y',z)),z))) = y. [para(10(a,1),18(a,1,1)),rewrite(16(4))]. 29 f(f(f(f(x,y),f(y,y')),z),f(y,f(y v y',y'))) = y. [para(10(a,1),18(a,1,2,2,1,2)),rewrite(17(9))]. 35 f(f(x,y),f(x,f(f(f(f(z,f(x',z)),z),f(x',f(f(z,f(x',z)),z))),f(f(z,f(x',z)),z)))) = x. [para(18(a,1),18(a,1,1,1))]. 36 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(18(a,1),18(a,1,1)),rewrite(16(3))]. 44 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),27(a,1,1))]. 45 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(27(a,1),16(a,1,1)),flip(a)]. 47 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(17(a,1),27(a,1,1))]. 51 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(44(a,1),16(a,1,1)),flip(a)]. 57 f(x' ^ f(x,y),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),25(a,1,1)),rewrite(16(4))]. 68 f(x,f(x',f(f(y,f(x'',y)),y))) = x'. [para(27(a,1),25(a,1,1))]. 69 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(47(a,1),16(a,1,1)),flip(a)]. 75 x ^ f(x',f(f(y,f(x'',y)),y)) = x''. [para(68(a,1),16(a,1,1)),flip(a)]. 89 f(f(x,y) ^ y',f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),26(a,1,1)),rewrite(16(4))]. 90 f(f(f(x,y),y'),z) ^ f(y,f(f(y,f(y',y)),y)) = y'. [para(26(a,1),16(a,1,1)),flip(a)]. 109 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(36(a,1),16(a,1,1)),rewrite(16(2)),flip(a)]. 117 f(f(x'',y),f(x,f(f(z,f(x',z)),z))) = x. [para(27(a,1),36(a,1,2,1)),rewrite(45(12),27(18))]. 118 f(x''',f(x,f(f(y,f(x',y)),y))) = x. [para(44(a,1),36(a,1,2,1)),rewrite(51(12),44(18))]. 120 f(x' v y,f(x,f(f(z,f(x',z)),z))) = x. [para(47(a,1),36(a,1,2,1)),rewrite(69(10),47(16))]. 121 f(f(f(f(x,y),y'),z),f(y,f(f(u,f(y',u)),u))) = y. [para(26(a,1),36(a,1,2,1)),rewrite(90(14),26(20))]. 123 (f(x,y) ^ f(y,z)) ^ f(y,f(f(z,f(y',z)),z)) = y'. [para(28(a,1),16(a,1,1)),flip(a)]. 134 f(f(x,y) ^ f(y,z),f(y,f(f(u,f(y',u)),u))) = y. [para(28(a,1),36(a,1,2,1)),rewrite(123(12),28(18))]. 135 f(x''',f(x,f(x v x',x'))) = x. [para(10(a,1),118(a,1,2,2,1,2)),rewrite(17(7))]. 136 x''' ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(118(a,1),16(a,1,1)),flip(a)]. 148 x' ^ f(x'',f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x'''. [para(135(a,1),75(a,1,2,2,1,2))]. 151 (x' v y) ^ f(x,f(f(z,f(x',z)),z)) = x'. [para(120(a,1),16(a,1,1)),flip(a)]. 174 f(f(x'',y),f(x,f(f(z',x v z),z'))) = x. [para(17(a,1),117(a,1,2,2,1,2))]. 220 (x' ^ f(x,y)) ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(57(a,1),16(a,1,1)),flip(a)]. 229 f(x' ^ f(x,y),f(x,f(f(z,f(x',z)),z))) = x. [para(57(a,1),36(a,1,2,1)),rewrite(220(12),57(18))]. 231 (f(x,y) ^ y') ^ f(y,f(f(y,f(y',y)),y)) = y'. [para(89(a,1),16(a,1,1)),flip(a)]. 238 f(f(x,y) ^ y',f(y,f(f(z,f(y',z)),z))) = y. [para(89(a,1),36(a,1,2,1)),rewrite(231(12),89(18))]. 284 f(x' ^ f(x,y),f(x,f(x v x',x'))) = x. [para(10(a,1),229(a,1,2,2,1,2)),rewrite(17(7))]. 307 f(x',f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x'))))) = f(x',f(x,y)). [para(284(a,1),36(a,1,2,2,1,2))]. 311 x' ^ f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x' ^ f(x,y). [para(284(a,1),109(a,1,2,2,1,2))]. 341 f(f(x,y),f(y,f(y v y',y'))) = y. [para(35(a,1),29(a,1,1))]. 351 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [back_rewrite(311),rewrite(341(16))]. 352 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [back_rewrite(307),rewrite(341(16))]. 360 x' ^ f(x'',x) = x'''. [back_rewrite(148),rewrite(341(15))]. 380 x'' ^ (x'' v x) = x''''. [para(17(a,1),360(a,1,2))]. 393 f(x',f(x,f(x v x',x'))) = x. [para(10(a,1),341(a,1,1))]. 414 f(x,x'') = x'. [para(393(a,1),68(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 415 x ^ x'' = x''. [para(393(a,1),75(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 417 x'' v x = x. [para(393(a,1),118(a,1,2,2,1,2)),rewrite(341(15),10(4),17(5))]. 418 f(x' v y,x') = x. [para(393(a,1),120(a,1,2,2,1,2)),rewrite(341(14),10(3))]. 420 x''' ^ x' = x'. [para(393(a,1),136(a,1,2,2,1,2)),rewrite(341(15),10(4))]. 421 (x' v y) ^ x' = x'. [para(393(a,1),151(a,1,2,2,1,2)),rewrite(341(14),10(3))]. 424 f(x',f(x,f(f(y',x v y),y'))) = x. [para(393(a,1),174(a,1,1))]. 428 f(f(x,y),y') v y = y. [para(393(a,1),238(a,1,2,2,1,2)),rewrite(341(15),10(4),23(5))]. 439 x'' ^ x = x''''. [back_rewrite(380),rewrite(417(5))]. 443 x''''' = x'. [back_rewrite(420),rewrite(439(5))]. 522 x'''' = x. [para(443(a,1),414(a,1,2)),rewrite(17(5),417(3)),flip(a)]. 533 x'' ^ x = x. [back_rewrite(439),rewrite(522(7))]. 535 f(x,y) = (x ^ y)'''. [para(16(a,1),522(a,1,1,1,1)),flip(a)]. 536 (x ^ y')''' = x''' v y. [para(522(a,1),17(a,1,1)),rewrite(535(2))]. 537 (x' ^ y)''' = x v y'''. [para(522(a,1),17(a,1,2)),rewrite(535(2))]. 584 ((x v y) ^ x)''' = x'''. [para(522(a,1),418(a,1,1,1)),rewrite(522(5),535(2))]. 609 ((x ^ y)'' v y) v y = y. [back_rewrite(428),rewrite(535(1),535(6),536(9),522(5))]. 611 x v (x ^ ((y' ^ (x v y))'' v y))'' = x. [back_rewrite(424),rewrite(535(4),537(7),22(3),535(9),536(12),22(8),536(8),522(6),535(8),535(12),536(15),522(4))]. 625 x v (x ^ y)'' = x''. [back_rewrite(352),rewrite(535(3),535(7),536(10),522(5),535(6),584(9),535(5),415(5),522(4),535(4),535(8),536(11),522(6)),flip(a)]. 626 x' ^ (x ^ y)''' = x'''. [back_rewrite(351),rewrite(535(3),535(7),536(10),522(5),625(5),535(4),533(4),415(5),535(5)),flip(a)]. 680 ((x ^ y)'' v (y ^ z)'') v (y ^ ((u ^ (y v u'''))'' v u'''))'' = y. [back_rewrite(134),rewrite(535(1),535(5),535(11),537(14),535(14),535(18),537(21),535(21),535(25),536(28),536(12),522(5))]. 686 (((x ^ y)'' v y) ^ z)'' v (y ^ ((u ^ (y v u'''))'' v u'''))'' = y. [back_rewrite(121),rewrite(535(1),535(6),536(9),522(5),535(5),535(10),537(13),535(13),535(17),537(20),535(20),535(24),536(27),522(9))]. 696 (c6 ^ (c6''' v (c6 ^ c7)''))''' != (c6 ^ c7)''' # answer(OM_SS). [back_rewrite(15),rewrite(535(5),535(9),536(12),535(12),535(18))]. 699 x'' = x. [back_rewrite(611),rewrite(625(10))]. 745 (c6 ^ (c6' v (c6 ^ c7)))' != (c6 ^ c7)' # answer(OM_SS). [back_rewrite(696),rewrite(699(4),699(8),699(10),699(14))]. 753 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u')) v u')) = y. [back_rewrite(686),rewrite(699(3),699(5),699(5),699(8),699(8),699(11))]. 758 ((x ^ y) v (y ^ z)) v (y ^ ((u ^ (y v u')) v u')) = y. [back_rewrite(680),rewrite(699(3),699(4),699(5),699(8),699(8),699(11))]. 789 x' ^ (x ^ y)' = x'. [back_rewrite(626),rewrite(699(4),699(6))]. 790 x v (x ^ y) = x. [back_rewrite(625),rewrite(699(3),699(4))]. 797 ((x ^ y) v y) v y = y. [back_rewrite(609),rewrite(699(3))]. 817 (x' ^ y)' = x v y'. [back_rewrite(537),rewrite(699(4),699(5))]. 823 (x v y) ^ x = x. [para(699(a,1),421(a,1,1,1)),rewrite(699(3),699(4))]. 829 (x v y) v x = x v y. [para(823(a,1),790(a,1,2))]. 866 x ^ (x v y') = x. [para(699(a,1),789(a,1,1)),rewrite(817(3),699(5))]. 871 x ^ (x v y) = x. [para(699(a,1),866(a,1,2,2))]. 887 (x ^ y)' = x' v y'. [para(699(a,1),817(a,1,1,1))]. 914 c6' v (c6 ^ (c6' v c7')) != c6' v c7' # answer(OM_SS). [back_rewrite(745),rewrite(887(9),22(9),699(5),887(7),887(14))]. 924 (x ^ y) v (y ^ ((z ^ (y v z')) v z')) = y. [para(823(a,1),753(a,1,1))]. 925 x ^ ((y ^ (x v y')) v y') = x. [para(753(a,1),797(a,1,1)),rewrite(790(7)),flip(a)]. 929 (((x ^ y) v y) ^ z) ^ y = ((x ^ y) v y) ^ z. [para(753(a,1),871(a,1,2))]. 934 (x ^ y) v y = y. [back_rewrite(924),rewrite(925(7))]. 936 ((x ^ y) v (y ^ z)) v y = y. [back_rewrite(758),rewrite(925(9))]. 938 (x ^ y) ^ x = x ^ y. [back_rewrite(929),rewrite(934(2),934(4))]. 943 (x' v y') ^ y' = y'. [para(934(a,1),22(a,1,1)),rewrite(887(3)),flip(a)]. 996 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(936(a,1),823(a,1,1))]. 997 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(823(a,1),936(a,1,1,2))]. 1013 (x' v y) ^ y = y. [para(699(a,1),943(a,1,1,2)),rewrite(699(4),699(5))]. 1024 (x v y) ^ y = y. [para(699(a,1),1013(a,1,1,1))]. 1032 x ^ (y v x) = x. [para(1024(a,1),938(a,1,1)),rewrite(1024(4))]. 1168 (x' v y) ^ ((x ^ (x' v y)) v x') = x' v y. [para(829(a,1),925(a,1,2,1,2))]. 1448 (x v y) ^ ((z ^ (x v y)) v x) = (z ^ (x v y)) v x. [para(823(a,1),996(a,1,2,2)),rewrite(823(9))]. 1477 (x ^ (x' v y)) v x' = x' v y. [back_rewrite(1168),rewrite(1448(8))]. 1573 (x v y) v (y v x) = y v x. [para(1032(a,1),997(a,1,1,1))]. 2291 x v y = y v x. [para(1573(a,1),829(a,1,1)),rewrite(1573(3),1573(4))]. 2467 x' v (x ^ (x' v y)) = x' v y. [back_rewrite(1477),rewrite(2291(5))]. 2468 $F # answer(OM_SS). [resolve(2467,a,914,a)]. ============================== end of proof ========================== % Redundant proof: 2514 $F # answer(OM_SS). [back_rewrite(914),rewrite(2467(10)),xx(a)]. % Disable descendants (x means already disabled): 15x 696x 745x 914x given #204 (T,wt=7): 2291 x v y = y v x. [para(1573(a,1),829(a,1,1)),rewrite(1573(3),1573(4))]. given #205 (T,wt=11): 1614 ((x v (y v z)) v u) ^ z = z. [para(1491(a,1),1278(a,1,2)),rewrite(1491(7))]. given #206 (A,wt=16): 1041 ((x' v y') ^ (y' v z)) ^ y' = y'. [back_rewrite(951),rewrite(1037(14))]. given #207 (F,wt=11): 1657 x ^ (((x v y) v z) v u) = x. [para(1383(a,1),1280(a,1,1)),rewrite(1383(7))]. given #208 (F,wt=11): 1659 x ^ (((y v x) v z) v u) = x. [para(1385(a,1),1280(a,1,1)),rewrite(1385(7))]. given #209 (T,wt=11): 1660 x ^ ((y v (x v z)) v u) = x. [para(1419(a,1),1280(a,1,1)),rewrite(1419(7))]. given #210 (T,wt=11): 1662 x ^ ((y v (z v x)) v u) = x. [para(1491(a,1),1280(a,1,1)),rewrite(1491(7))]. given #211 (A,wt=22): 1042 ((x' ^ ((x' ^ y) v z)) v u') ^ (x' ^ y) = x' ^ y. [back_rewrite(857),rewrite(1037(17))]. given #212 (F,wt=11): 1790 (x v ((y v z) v u)) ^ y = y. [para(1383(a,1),1292(a,1,2)),rewrite(1383(7))]. given #213 (F,wt=11): 1792 (x v ((y v z) v u)) ^ z = z. [para(1385(a,1),1292(a,1,2)),rewrite(1385(7))]. given #214 (T,wt=11): 1793 (x v (y v (z v u))) ^ z = z. [para(1419(a,1),1292(a,1,2)),rewrite(1419(7))]. given #215 (T,wt=11): 1794 (x v (y v (z v u))) ^ u = u. [para(1491(a,1),1292(a,1,2)),rewrite(1491(7))]. given #216 (A,wt=14): 1043 (((x' v y) ^ (y v z)) v u) ^ y = y. [back_rewrite(851),rewrite(1037(11))]. given #217 (F,wt=11): 1804 x ^ (y v ((x v z) v u)) = x. [para(1383(a,1),1294(a,1,1)),rewrite(1383(7))]. given #218 (F,wt=11): 1806 x ^ (y v ((z v x) v u)) = x. [para(1385(a,1),1294(a,1,1)),rewrite(1385(7))]. given #219 (T,wt=11): 1807 x ^ (y v (z v (x v u))) = x. [para(1419(a,1),1294(a,1,1)),rewrite(1419(7))]. given #220 (T,wt=11): 1809 x ^ (y v (z v (u v x))) = x. [para(1491(a,1),1294(a,1,1)),rewrite(1491(7))]. given #221 (A,wt=15): 1047 (x v y) v (x v ((x v y) ^ z)) = x v y. [para(871(a,1),998(a,1,2,1))]. given #222 (F,wt=11): 2290 (x v y) ^ (y v x) = y v x. [para(1573(a,1),823(a,1,1))]. given #223 (F,wt=11): 2515 x' ^ y' = y' ^ x'. [para(2291(a,1),22(a,1,1)),rewrite(22(2))]. given #224 (T,wt=9): 2869 x' ^ y = y ^ x'. [para(699(a,1),2515(a,1,1)),rewrite(699(5)),flip(a)]. % Operation ^ is commutative; C redundancy checks enabled. % back CAC tautology: 2872 (x ^ y') v (z' ^ y') = (x ^ y') v (y' ^ z'). [para(2515(a,1),996(a,1,2,2)),rewrite(1059(8))]. % back CAC tautology: 2871 (x' ^ y') v (y' ^ z) = (y' ^ x') v (y' ^ z). [para(2515(a,1),996(a,1,2,1)),rewrite(1053(8)),flip(a)]. given #225 (T,wt=7): 2926 x ^ y = y ^ x. [para(699(a,1),2869(a,1,1)),rewrite(699(3))]. given #226 (A,wt=15): 1051 (x v y) v (y v ((x v y) ^ z)) = x v y. [para(1032(a,1),998(a,1,2,1))]. given #227 (F,wt=12): 2204 (x ^ y) v (x ^ x') = x ^ y. [para(1201(a,1),1037(a,1,2,1))]. given #228 (F,wt=12): 2205 (x ^ y) v (y ^ y') = x ^ y. [para(1208(a,1),1037(a,1,2,1))]. given #229 (T,wt=12): 2464 x v (x' ^ (y v x)) = y v x. [back_rewrite(1480),rewrite(2291(4))]. given #230 (T,wt=11): 3169 x v (x' v y) = x v x'. [para(1416(a,1),2464(a,1,2)),rewrite(2291(5)),flip(a)]. NOTE: New constant: x v x' = c_0. [new_symbol(3196)]. NOTE: New Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c_0, ^, v, ', f ]). given #231 (A,wt=17): 1053 x ^ ((x ^ y) v (x ^ z)) = (x ^ y) v (x ^ z). [para(1001(a,1),823(a,1,1))]. given #232 (F,wt=5): 3225 x ^ c_0 = x. [back_rewrite(3200),rewrite(3212(2))]. given #233 (F,wt=5): 3271 c_0 v x = c_0. [para(3225(a,1),945(a,1,2))]. given #234 (T,wt=5): 3272 c_0 ^ x = x. [para(3225(a,1),944(a,1,2)),rewrite(3225(4))]. given #235 (T,wt=5): 3273 x v c_0 = c_0. [para(3225(a,1),1238(a,1,1)),rewrite(3271(2),3271(4))]. given #236 (A,wt=17): 1059 x ^ ((y ^ x) v (z ^ x)) = (y ^ x) v (z ^ x). [para(1002(a,1),823(a,1,1))]. given #237 (F,wt=6): 3212 x v x' = c_0. [new_symbol(3196)]. given #238 (F,wt=6): 3274 x v c_0' = x. [para(3225(a,1),2205(a,1,1)),rewrite(3272(4),3225(5))]. given #239 (T,wt=6): 3334 c_0' v x = x. [para(3274(a,1),1031(a,1,2)),rewrite(3274(6))]. given #240 (T,wt=7): 3309 x ^ x' = c_0'. [para(3212(a,1),22(a,1,1)),rewrite(699(5),2926(4)),flip(a)]. given #241 (A,wt=15): 1078 (x v y) v (x v (z ^ (x v y))) = x v y. [para(871(a,1),1049(a,1,2,1))]. given #242 (F,wt=7): 3333 c_0' ^ x = c_0'. [para(3274(a,1),1032(a,1,2))]. given #243 (F,wt=7): 3337 x ^ c_0' = c_0'. [para(3274(a,1),1292(a,1,1)),rewrite(3333(3),3333(6))]. given #244 (T,wt=8): 3230 x' v (x v y) = c_0. [back_rewrite(3188),rewrite(3212(5))]. given #245 (T,wt=8): 3235 x v (y v x') = c_0. [back_rewrite(3170),rewrite(3212(5))]. given #246 (A,wt=15): 1079 (x v y) v (y v (z ^ (x v y))) = x v y. [para(1032(a,1),1049(a,1,2,1))]. given #247 (F,wt=8): 3236 x v (x' v y) = c_0. [back_rewrite(3169),rewrite(3212(5))]. given #248 (F,wt=8): 3350 x' v (y v x) = c_0. [para(1031(a,1),3230(a,1,2))]. given #249 (T,wt=10): 3231 x v (y v (z v x')) = c_0. [back_rewrite(3182),rewrite(3212(6))]. given #250 (T,wt=10): 3232 x v (y v (x' v z)) = c_0. [back_rewrite(3181),rewrite(3212(6))]. given #251 (A,wt=17): 1081 x ^ ((x ^ y) v (z ^ x)) = (x ^ y) v (z ^ x). [para(1056(a,1),823(a,1,1))]. given #252 (F,wt=10): 3233 x v ((y v x') v z) = c_0. [back_rewrite(3180),rewrite(3212(6))]. given #253 (F,wt=10): 3234 x v ((x' v y) v z) = c_0. [back_rewrite(3179),rewrite(3212(6))]. given #254 (T,wt=10): 3313 x' ^ (x ^ y') = c_0'. [back_rewrite(3186),rewrite(3309(6))]. given #255 (T,wt=9): 3453 x' ^ (x ^ y) = c_0'. [para(699(a,1),3313(a,1,2,2))]. given #256 (A,wt=17): 1084 x' ^ ((x' v y') ^ (z' v x')) = x'. [para(1075(a,1),22(a,1,1)),rewrite(22(6),887(4),887(7)),flip(a)]. given #257 (F,wt=9): 3456 x ^ (x' ^ y) = c_0'. [para(699(a,1),3453(a,1,1))]. given #258 (F,wt=9): 3458 x' ^ (y ^ x) = c_0'. [para(944(a,1),3453(a,1,2))]. given #259 (T,wt=9): 3488 x ^ (y ^ x') = c_0'. [para(944(a,1),3456(a,1,2))]. given #260 (T,wt=10): 3404 x' v (y v (z v x)) = c_0. [para(699(a,1),3231(a,1,2,2,2))]. given #261 (A,wt=21): 1183 x ^ (((y ^ x) v (x ^ z)) ^ u) = ((y ^ x) v (x ^ z)) ^ u. [para(935(a,1),823(a,1,1))]. given #262 (F,wt=10): 3409 x' v (y v (x v z)) = c_0. [para(699(a,1),3232(a,1,2,2,1))]. given #263 (F,wt=10): 3443 x' v ((y v x) v z) = c_0. [para(699(a,1),3233(a,1,2,1,2))]. given #264 (T,wt=10): 3448 x' v ((x v y) v z) = c_0. [para(699(a,1),3234(a,1,2,1,1))]. given #265 (T,wt=11): 3215 (x ^ y') v (x' v y) = c_0. [back_rewrite(3210),rewrite(3212(7))]. given #266 (A,wt=13): 1185 x v (((y ^ x) v (x ^ z)) ^ u) = x. [para(935(a,1),829(a,1,1)),rewrite(935(10))]. given #267 (F,wt=11): 3228 (x ^ y) v (x' v y') = c_0. [back_rewrite(3193),rewrite(3212(7))]. given #268 (F,wt=11): 3310 (x' ^ y') v (x v y) = c_0. [para(22(a,1),3212(a,1,2)),rewrite(2291(5))]. given #269 (T,wt=11): 3351 (x' v y') v (x v z) = c_0. [para(1200(a,1),3230(a,1,2)),rewrite(887(2))]. given #270 (T,wt=10): 3679 (x' v y) v (x v z) = c_0. [para(699(a,1),3351(a,1,1,2))]. given #271 (A,wt=13): 1199 x ^ ((x ^ y) ^ z) = (x ^ y) ^ z. [para(1188(a,1),823(a,1,1))]. given #272 (F,wt=10): 3684 (x v y) v (x' v z) = c_0. [para(699(a,1),3679(a,1,1,1))]. given #273 (F,wt=10): 3686 (x v y') v (y v z) = c_0. [para(1031(a,1),3679(a,1,1))]. given #274 (T,wt=10): 3687 (x' v y) v (z v x) = c_0. [para(1031(a,1),3679(a,1,2))]. given #275 (T,wt=10): 3712 (x v y) v (y' v z) = c_0. [para(1031(a,1),3684(a,1,1))]. given #276 (A,wt=13): 1207 x ^ ((y ^ x) ^ z) = (y ^ x) ^ z. [para(1189(a,1),823(a,1,1))]. given #277 (F,wt=10): 3713 (x v y) v (z v x') = c_0. [para(1031(a,1),3684(a,1,2))]. given #278 (F,wt=10): 3721 (x v y') v (z v y) = c_0. [para(1031(a,1),3686(a,1,2))]. given #279 (T,wt=10): 3753 (x v y) v (z v y') = c_0. [para(1031(a,1),3712(a,1,2))]. given #280 (T,wt=11): 3355 (x' ^ y') v (y v x) = c_0. [para(1573(a,1),3230(a,1,2)),rewrite(22(2))]. given #281 (A,wt=13): 1237 x ^ (y ^ (x ^ z)) = y ^ (x ^ z). [para(1203(a,1),823(a,1,1))]. given #282 (F,wt=11): 3359 (x' ^ y) v (x v y') = c_0. [para(3235(a,1),2464(a,1,2,2)),rewrite(22(5),699(5),2926(6),3272(6),2291(5),3235(8))]. given #283 (F,wt=11): 3636 (x ^ y') v (y v x') = c_0. [para(2291(a,1),3215(a,1,2))]. given #284 (T,wt=11): 3637 (x' ^ y) v (y' v x) = c_0. [para(2926(a,1),3215(a,1,1))]. given #285 (T,wt=11): 3668 (x ^ y) v (y' v x') = c_0. [para(2291(a,1),3228(a,1,2))]. given #286 (A,wt=13): 1251 x ^ (y ^ (z ^ x)) = y ^ (z ^ x). [para(1210(a,1),823(a,1,1))]. given #287 (F,wt=11): 3704 x' ^ ((x ^ y) ^ z) = c_0'. [para(1199(a,1),3453(a,1,2))]. given #288 (F,wt=11): 3705 x ^ ((x' ^ y) ^ z) = c_0'. [para(1199(a,1),3456(a,1,2))]. given #289 (T,wt=11): 3765 x' ^ ((y ^ x) ^ z) = c_0'. [para(1207(a,1),3453(a,1,2))]. given #290 (T,wt=11): 3766 x ^ ((y ^ x') ^ z) = c_0'. [para(1207(a,1),3456(a,1,2))]. given #291 (A,wt=13): 1279 x v ((x v y) v z) = (x v y) v z. [para(823(a,1),1200(a,1,1))]. given #292 (F,wt=11): 3814 x' ^ (y ^ (x ^ z)) = c_0'. [para(1237(a,1),3453(a,1,2))]. given #293 (F,wt=11): 3815 x ^ (y ^ (x' ^ z)) = c_0'. [para(1237(a,1),3456(a,1,2))]. given #294 (T,wt=11): 3854 x' ^ (y ^ (z ^ x)) = c_0'. [para(1251(a,1),3453(a,1,2))]. given #295 (T,wt=11): 3855 x ^ (y ^ (z ^ x')) = c_0'. [para(1251(a,1),3456(a,1,2))]. given #296 (A,wt=13): 1281 x v ((y v x) v z) = (y v x) v z. [para(1024(a,1),1200(a,1,1))]. given #297 (F,wt=11): 3879 (x ^ y) ^ (x' ^ z) = c_0'. [para(3704(a,1),1237(a,1)),flip(a)]. given #298 (F,wt=11): 3881 (x ^ y) ^ (z ^ x') = c_0'. [para(3704(a,1),1251(a,1)),flip(a)]. given #299 (T,wt=11): 3899 (x' ^ y) ^ (x ^ z) = c_0'. [para(3705(a,1),1237(a,1)),flip(a)]. given #300 (T,wt=11): 3901 (x' ^ y) ^ (z ^ x) = c_0'. [para(3705(a,1),1251(a,1)),flip(a)]. given #301 (A,wt=13): 1290 ((x ^ y) ^ z) v (x v u) = x v u. [para(1200(a,1),1200(a,1,2)),rewrite(1200(7))]. given #302 (F,wt=11): 3929 (x ^ y) ^ (y' ^ z) = c_0'. [para(3765(a,1),1237(a,1)),flip(a)]. given #303 (F,wt=11): 3932 (x ^ y) ^ (z ^ y') = c_0'. [para(3765(a,1),1251(a,1)),flip(a)]. given #304 (T,wt=11): 3942 (x ^ y') ^ (y ^ z) = c_0'. [para(3766(a,1),1237(a,1)),flip(a)]. given #305 (T,wt=11): 3944 (x ^ y') ^ (z ^ y) = c_0'. [para(3766(a,1),1251(a,1)),flip(a)]. given #306 (A,wt=13): 1293 x v (y v (x v z)) = y v (x v z). [para(823(a,1),1204(a,1,1))]. given #307 (F,wt=12): 2466 x v (x' ^ (x v y)) = x v y. [back_rewrite(1478),rewrite(2291(4))]. given #308 (F,wt=12): 2981 x ^ ((y' v x) ^ (x v z)) = x. [back_rewrite(2536),rewrite(2926(5))]. given #309 (T,wt=11): 4201 x ^ ((y v x) ^ (x v z)) = x. [para(699(a,1),2981(a,1,2,1,1))]. given #310 (T,wt=11): 4254 x ^ ((y v x) ^ (z v x)) = x. [para(1031(a,1),4201(a,1,2,2))]. given #311 (A,wt=13): 1295 x v (y v (z v x)) = y v (z v x). [para(1024(a,1),1204(a,1,1))]. given #312 (F,wt=11): 4291 x ^ ((x v y) ^ (x v z)) = x. [para(2291(a,1),4201(a,1,2,1))]. given #313 (F,wt=11): 4293 x ^ ((x v y) ^ (z v x)) = x. [para(2926(a,1),4201(a,1,2))]. given #314 (T,wt=12): 3099 x v (y ^ (y' v (x ^ y))) = x. [back_rewrite(1067),rewrite(2926(4))]. given #315 (T,wt=12): 3338 (x' ^ y') ^ (x v y) = c_0'. [para(22(a,1),3309(a,1,2)),rewrite(2926(5))]. given #316 (A,wt=13): 1297 ((x ^ y) ^ z) v (u v x) = u v x. [para(1204(a,1),1200(a,1,2)),rewrite(1204(7))]. given #317 (F,wt=12): 3339 (x ^ y) ^ (x' v y') = c_0'. [para(887(a,1),3309(a,1,2))]. given #318 (F,wt=12): 3464 (x' ^ y') ^ (y v x) = c_0'. [para(2290(a,1),3453(a,1,2)),rewrite(22(2))]. given #319 (T,wt=12): 3629 (x ^ y') ^ (x' v y) = c_0'. [para(3215(a,1),22(a,1,1)),rewrite(887(5),699(5),22(7),699(6),2926(7)),flip(a)]. given #320 (T,wt=12): 3819 (x' ^ y) ^ (x v y') = c_0'. [para(3359(a,1),22(a,1,1)),rewrite(887(5),699(4),22(7),699(7),2926(7)),flip(a)]. given #321 (A,wt=13): 1304 x v (((x ^ y) v (x ^ z)) ^ u) = x. [para(1001(a,1),1224(a,1,1)),rewrite(1001(9))]. given #322 (F,wt=12): 3832 (x' ^ y) ^ (y' v x) = c_0'. [para(3636(a,1),22(a,1,1)),rewrite(887(5),699(5),22(7),699(7),2926(7)),flip(a)]. given #323 (F,wt=12): 3837 (x ^ y') ^ (y v x') = c_0'. [para(3637(a,1),22(a,1,1)),rewrite(887(5),699(4),22(7),699(6),2926(7)),flip(a)]. given #324 (T,wt=12): 3842 (x ^ y) ^ (y' v x') = c_0'. [para(3668(a,1),22(a,1,1)),rewrite(887(4),22(9),699(7),699(7),2926(7)),flip(a)]. given #325 (T,wt=12): 3946 x v (y v ((x' v z) v u)) = c_0. [para(1279(a,1),3232(a,1,2,2))]. given #326 (A,wt=13): 1305 x v (((y ^ x) v (z ^ x)) ^ u) = x. [para(1002(a,1),1224(a,1,1)),rewrite(1002(9))]. given #327 (F,wt=12): 3947 x v (((y v x') v z) v u) = c_0. [para(1279(a,1),3233(a,1,2))]. given #328 (F,wt=12): 3948 x v (((x' v y) v z) v u) = c_0. [para(1279(a,1),3234(a,1,2,1))]. given #329 (T,wt=12): 3950 x' v (y v ((x v z) v u)) = c_0. [para(1279(a,1),3409(a,1,2,2))]. given #330 (T,wt=12): 3952 x' v (((y v x) v z) v u) = c_0. [para(1279(a,1),3443(a,1,2))]. given #331 (A,wt=13): 1306 x v (((x ^ y) v (z ^ x)) ^ u) = x. [para(1056(a,1),1224(a,1,1)),rewrite(1056(9))]. given #332 (F,wt=12): 3953 x' v (((x v y) v z) v u) = c_0. [para(1279(a,1),3448(a,1,2,1))]. given #333 (F,wt=12): 3954 ((x' v y) v z) v (x v u) = c_0. [para(1279(a,1),3679(a,1,1))]. given #334 (T,wt=12): 3955 (x' v y) v ((x v z) v u) = c_0. [para(1279(a,1),3679(a,1,2))]. given #335 (T,wt=12): 3956 ((x v y) v z) v (x' v u) = c_0. [para(1279(a,1),3684(a,1,1))]. given #336 (A,wt=15): 1311 x v ((((y ^ x) v (x ^ z)) ^ u) ^ v) = x. [para(935(a,1),1224(a,1,1)),rewrite(935(11))]. given #337 (F,wt=12): 3957 (x v y) v ((x' v z) v u) = c_0. [para(1279(a,1),3684(a,1,2))]. given #338 (F,wt=12): 3958 (x v y') v ((y v z) v u) = c_0. [para(1279(a,1),3686(a,1,2))]. given #339 (T,wt=12): 3959 ((x' v y) v z) v (u v x) = c_0. [para(1279(a,1),3687(a,1,1))]. given #340 (T,wt=12): 3961 (x v y) v ((y' v z) v u) = c_0. [para(1279(a,1),3712(a,1,2))]. given #341 (A,wt=13): 1317 (x v y) v ((x ^ z) ^ u) = x v y. [para(1200(a,1),1224(a,1,1)),rewrite(1200(7))]. given #342 (F,wt=12): 3962 ((x v y) v z) v (u v x') = c_0. [para(1279(a,1),3713(a,1,1))]. given #343 (F,wt=12): 4016 x v (y v ((z v x') v u)) = c_0. [para(1281(a,1),3232(a,1,2,2))]. given #344 (T,wt=12): 4017 x v ((y v (z v x')) v u) = c_0. [para(1281(a,1),3233(a,1,2))]. given #345 (T,wt=12): 4018 x v ((y v (x' v z)) v u) = c_0. [para(1281(a,1),3234(a,1,2))]. given #346 (A,wt=13): 1318 (x v y) v ((y ^ z) ^ u) = x v y. [para(1204(a,1),1224(a,1,1)),rewrite(1204(7))]. given #347 (F,wt=12): 4019 x' v (y v ((z v x) v u)) = c_0. [para(1281(a,1),3409(a,1,2,2))]. given #348 (F,wt=12): 4020 x' v ((y v (z v x)) v u) = c_0. [para(1281(a,1),3443(a,1,2))]. given #349 (T,wt=12): 4021 x' v ((y v (x v z)) v u) = c_0. [para(1281(a,1),3448(a,1,2))]. given #350 (T,wt=12): 4022 ((x v y') v z) v (y v u) = c_0. [para(1281(a,1),3679(a,1,1))]. given #351 (A,wt=13): 1340 ((x ^ y) ^ z) v (y v u) = y v u. [para(1238(a,1),1200(a,1,2)),rewrite(1238(7))]. given #352 (F,wt=12): 4023 (x' v y) v ((z v x) v u) = c_0. [para(1281(a,1),3679(a,1,2))]. given #353 (F,wt=12): 4024 ((x v y) v z) v (y' v u) = c_0. [para(1281(a,1),3684(a,1,1))]. given #354 (T,wt=12): 4025 (x v y) v ((z v x') v u) = c_0. [para(1281(a,1),3684(a,1,2))]. given #355 (T,wt=12): 4026 (x v y') v ((z v y) v u) = c_0. [para(1281(a,1),3686(a,1,2))]. given #356 (A,wt=13): 1341 (x ^ (y ^ z)) v (y v u) = y v u. [para(1200(a,1),1238(a,1,2)),rewrite(1200(7))]. given #357 (F,wt=12): 4027 ((x v y') v z) v (u v y) = c_0. [para(1281(a,1),3687(a,1,1))]. given #358 (F,wt=12): 4028 (x v y) v ((z v y') v u) = c_0. [para(1281(a,1),3712(a,1,2))]. given #359 (T,wt=12): 4029 ((x v y) v z) v (u v y') = c_0. [para(1281(a,1),3713(a,1,1))]. given #360 (T,wt=12): 4177 x v (y v (z v (x' v u))) = c_0. [para(1293(a,1),3232(a,1,2,2))]. given #361 (A,wt=13): 1342 (x ^ (y ^ z)) v (u v y) = u v y. [para(1204(a,1),1238(a,1,2)),rewrite(1204(7))]. given #362 (F,wt=12): 4179 x' v (y v (z v (x v u))) = c_0. [para(1293(a,1),3409(a,1,2,2))]. given #363 (F,wt=12): 4181 (x v (y' v z)) v (y v u) = c_0. [para(1293(a,1),3679(a,1,1))]. given #364 (T,wt=12): 4182 (x' v y) v (z v (x v u)) = c_0. [para(1293(a,1),3679(a,1,2))]. given #365 (T,wt=12): 4183 (x v (y v z)) v (y' v u) = c_0. [para(1293(a,1),3684(a,1,1))]. given #366 (A,wt=13): 1343 (x v y) v ((z ^ x) ^ u) = x v y. [para(1238(a,1),1224(a,1,1)),rewrite(1238(7))]. given #367 (F,wt=12): 4184 (x v y) v (z v (x' v u)) = c_0. [para(1293(a,1),3684(a,1,2))]. given #368 (F,wt=12): 4185 (x v y') v (z v (y v u)) = c_0. [para(1293(a,1),3686(a,1,2))]. given #369 (T,wt=12): 4186 (x v (y' v z)) v (u v y) = c_0. [para(1293(a,1),3687(a,1,1))]. given #370 (T,wt=12): 4188 (x v y) v (z v (y' v u)) = c_0. [para(1293(a,1),3712(a,1,2))]. given #371 (A,wt=13): 1344 (x ^ (y ^ z)) v (z v u) = z v u. [para(1238(a,1),1238(a,1,2)),rewrite(1238(7))]. given #372 (F,wt=12): 4189 (x v (y v z)) v (u v y') = c_0. [para(1293(a,1),3713(a,1,1))]. given #373 (F,wt=12): 4359 x v (y v (z v (u v x'))) = c_0. [para(1295(a,1),3232(a,1,2,2))]. given #374 (T,wt=12): 4360 x' v (y v (z v (u v x))) = c_0. [para(1295(a,1),3409(a,1,2,2))]. given #375 (T,wt=12): 4361 (x v (y v z')) v (z v u) = c_0. [para(1295(a,1),3679(a,1,1))]. given #376 (A,wt=13): 1349 ((x ^ y) ^ z) v (u v y) = u v y. [para(1240(a,1),1200(a,1,2)),rewrite(1240(7))]. given #377 (F,wt=12): 4362 (x' v y) v (z v (u v x)) = c_0. [para(1295(a,1),3679(a,1,2))]. given #378 (F,wt=12): 4363 (x v (y v z)) v (z' v u) = c_0. [para(1295(a,1),3684(a,1,1))]. given #379 (T,wt=12): 4364 (x v y) v (z v (u v x')) = c_0. [para(1295(a,1),3684(a,1,2))]. given #380 (T,wt=12): 4365 (x v y') v (z v (u v y)) = c_0. [para(1295(a,1),3686(a,1,2))]. given #381 (A,wt=13): 1350 (x v y) v ((z ^ y) ^ u) = x v y. [para(1240(a,1),1224(a,1,1)),rewrite(1240(7))]. given #382 (F,wt=12): 4366 (x v (y v z')) v (u v z) = c_0. [para(1295(a,1),3687(a,1,1))]. given #383 (F,wt=12): 4367 (x v y) v (z v (u v y')) = c_0. [para(1295(a,1),3712(a,1,2))]. given #384 (T,wt=12): 4368 (x v (y v z)) v (u v z') = c_0. [para(1295(a,1),3713(a,1,1))]. given #385 (T,wt=12): 4432 x v (y ^ (y' v (y ^ x))) = x. [para(2926(a,1),3099(a,1,2,2,2))]. given #386 (A,wt=13): 1351 (x ^ (y ^ z)) v (u v z) = u v z. [para(1240(a,1),1238(a,1,2)),rewrite(1240(7))]. given #387 (F,wt=13): 1362 x v (y ^ ((z ^ x) v (x ^ u))) = x. [para(936(a,1),1268(a,1,1)),rewrite(936(9))]. given #388 (F,wt=13): 1363 x v (y ^ ((x ^ z) v (x ^ u))) = x. [para(1001(a,1),1268(a,1,1)),rewrite(1001(9))]. given #389 (T,wt=13): 1364 x v (y ^ ((z ^ x) v (u ^ x))) = x. [para(1002(a,1),1268(a,1,1)),rewrite(1002(9))]. given #390 (T,wt=13): 1365 x v (y ^ ((x ^ z) v (u ^ x))) = x. [para(1056(a,1),1268(a,1,1)),rewrite(1056(9))]. given #391 (A,wt=15): 1370 x v (y ^ (((z ^ x) v (x ^ u)) ^ v)) = x. [para(935(a,1),1268(a,1,1)),rewrite(935(11))]. given #392 (F,wt=13): 1375 (x v y) v (z ^ (x ^ u)) = x v y. [para(1200(a,1),1268(a,1,1)),rewrite(1200(7))]. given #393 (F,wt=13): 1376 (x v y) v (z ^ (y ^ u)) = x v y. [para(1204(a,1),1268(a,1,1)),rewrite(1204(7))]. given #394 (T,wt=13): 1377 (x v y) v (z ^ (u ^ x)) = x v y. [para(1238(a,1),1268(a,1,1)),rewrite(1238(7))]. given #395 (T,wt=13): 1378 (x v y) v (z ^ (u ^ y)) = x v y. [para(1240(a,1),1268(a,1,1)),rewrite(1240(7))]. given #396 (A,wt=17): 1386 (x v y) v ((z ^ (x v y)) v (x ^ u)) = x v y. [para(1278(a,1),998(a,1,2,2))]. given #397 (F,wt=13): 1415 ((x v y) v z) ^ (x ^ u) = x ^ u. [para(1278(a,1),1278(a,1,2)),rewrite(1278(7))]. given #398 (F,wt=13): 1441 ((x v y) v z) ^ (y ^ u) = y ^ u. [para(1204(a,1),1383(a,1,1,1))]. given #399 (T,wt=13): 1444 ((x v y) v z) ^ (u ^ x) = u ^ x. [para(1238(a,1),1383(a,1,1,1))]. given #400 (T,wt=13): 1445 ((x v y) v z) ^ (u ^ y) = u ^ y. [para(1240(a,1),1383(a,1,1,1))]. given #401 (A,wt=21): 1389 x ^ (((x ^ y) v (x ^ z)) ^ u) = ((x ^ y) v (x ^ z)) ^ u. [para(1001(a,1),1278(a,1,1))]. given #402 (F,wt=13): 1526 (x ^ y) ^ ((x v z) v u) = x ^ y. [para(1200(a,1),1416(a,1,2,1))]. given #403 (F,wt=13): 1527 (x ^ y) ^ ((z v x) v u) = x ^ y. [para(1204(a,1),1416(a,1,2,1))]. given #404 (T,wt=13): 1528 (x ^ y) ^ ((y v z) v u) = x ^ y. [para(1238(a,1),1416(a,1,2,1))]. given #405 (T,wt=13): 1529 (x ^ y) ^ ((z v y) v u) = x ^ y. [para(1240(a,1),1416(a,1,2,1))]. given #406 (A,wt=21): 1390 x ^ (((y ^ x) v (z ^ x)) ^ u) = ((y ^ x) v (z ^ x)) ^ u. [para(1002(a,1),1278(a,1,1))]. given #407 (F,wt=13): 1555 (x v (y v z)) ^ (y ^ u) = y ^ u. [para(1200(a,1),1419(a,1,1,2))]. given #408 (F,wt=13): 1557 (x v (y v z)) ^ (z ^ u) = z ^ u. [para(1204(a,1),1419(a,1,1,2))]. given #409 (T,wt=13): 1560 (x v (y v z)) ^ (u ^ y) = u ^ y. [para(1238(a,1),1419(a,1,1,2))]. given #410 (T,wt=13): 1561 (x v (y v z)) ^ (u ^ z) = u ^ z. [para(1240(a,1),1419(a,1,1,2))]. given #411 (A,wt=17): 1391 (x v y) v ((x ^ z) v ((x v y) ^ u)) = x v y. [para(1278(a,1),1048(a,1,2,1))]. given #412 (F,wt=13): 1629 (x ^ y) ^ (z v (x v u)) = x ^ y. [para(1200(a,1),1513(a,1,2,2))]. given #413 (F,wt=13): 1630 (x ^ y) ^ (z v (u v x)) = x ^ y. [para(1204(a,1),1513(a,1,2,2))]. given #414 (T,wt=13): 1631 (x ^ y) ^ (z v (y v u)) = x ^ y. [para(1238(a,1),1513(a,1,2,2))]. given #415 (T,wt=13): 1632 (x ^ y) ^ (z v (u v y)) = x ^ y. [para(1240(a,1),1513(a,1,2,2))]. given #416 (A,wt=17): 1392 (x v y) v (((x v y) ^ z) v (x ^ u)) = x v y. [para(1278(a,1),1048(a,1,2,2))]. given #417 (F,wt=13): 1688 x v ((((x ^ y) ^ z) ^ u) ^ v) = x. [para(1286(a,1),1224(a,1,1)),rewrite(1286(9))]. given #418 (F,wt=13): 1690 x v (y ^ (((x ^ z) ^ u) ^ v)) = x. [para(1286(a,1),1268(a,1,1)),rewrite(1286(9))]. given #419 (T,wt=13): 1706 x v ((((y ^ x) ^ z) ^ u) ^ v) = x. [para(1287(a,1),1224(a,1,1)),rewrite(1287(9))]. given #420 (T,wt=13): 1708 x v (y ^ (((z ^ x) ^ u) ^ v)) = x. [para(1287(a,1),1268(a,1,1)),rewrite(1287(9))]. given #421 (A,wt=21): 1394 x ^ (((x ^ y) v (z ^ x)) ^ u) = ((x ^ y) v (z ^ x)) ^ u. [para(1056(a,1),1278(a,1,1))]. given #422 (F,wt=13): 1719 x v (((y ^ (x ^ z)) ^ u) ^ v) = x. [para(1288(a,1),1224(a,1,1)),rewrite(1288(9))]. given #423 (F,wt=13): 1721 x v (y ^ ((z ^ (x ^ u)) ^ v)) = x. [para(1288(a,1),1268(a,1,1)),rewrite(1288(9))]. given #424 (T,wt=13): 1737 x v (((y ^ (z ^ x)) ^ u) ^ v) = x. [para(1289(a,1),1224(a,1,1)),rewrite(1289(9))]. given #425 (T,wt=13): 1739 x v (y ^ ((z ^ (u ^ x)) ^ v)) = x. [para(1289(a,1),1268(a,1,1)),rewrite(1289(9))]. given #426 (A,wt=17): 1395 (x v y) v ((x ^ z) v (u ^ (x v y))) = x v y. [para(1278(a,1),1075(a,1,2,1))]. given #427 (F,wt=13): 1951 x v ((y ^ ((x ^ z) ^ u)) ^ v) = x. [para(1336(a,1),1224(a,1,1)),rewrite(1336(9))]. given #428 (F,wt=13): 1953 x v (y ^ (z ^ ((x ^ u) ^ v))) = x. [para(1336(a,1),1268(a,1,1)),rewrite(1336(9))]. given #429 (T,wt=13): 1973 x v ((y ^ ((z ^ x) ^ u)) ^ v) = x. [para(1337(a,1),1224(a,1,1)),rewrite(1337(9))]. given #430 (T,wt=13): 1975 x v (y ^ (z ^ ((u ^ x) ^ v))) = x. [para(1337(a,1),1268(a,1,1)),rewrite(1337(9))]. given #431 (A,wt=25): 1399 x ^ ((((y ^ x) v (x ^ z)) ^ u) ^ v) = (((y ^ x) v (x ^ z)) ^ u) ^ v. [para(935(a,1),1278(a,1,1))]. given #432 (F,wt=13): 1988 x v ((y ^ (z ^ (x ^ u))) ^ v) = x. [para(1338(a,1),1224(a,1,1)),rewrite(1338(9))]. given #433 (F,wt=13): 1990 x v (y ^ (z ^ (u ^ (x ^ v)))) = x. [para(1338(a,1),1268(a,1,1)),rewrite(1338(9))]. given #434 (T,wt=13): 2010 x v ((y ^ (z ^ (u ^ x))) ^ v) = x. [para(1339(a,1),1224(a,1,1)),rewrite(1339(9))]. given #435 (T,wt=13): 2012 x v (y ^ (z ^ (u ^ (v ^ x)))) = x. [para(1339(a,1),1268(a,1,1)),rewrite(1339(9))]. given #436 (A,wt=17): 1400 x ^ (((x ^ y) ^ z) ^ u) = ((x ^ y) ^ z) ^ u. [para(1188(a,1),1278(a,1,1))]. given #437 (F,wt=13): 2141 x ^ ((((x v y) v z) v u) v v) = x. [para(1447(a,1),1280(a,1,1)),rewrite(1447(9))]. given #438 (F,wt=13): 2151 x ^ (y v (((x v z) v u) v v)) = x. [para(1447(a,1),1294(a,1,1)),rewrite(1447(9))]. given #439 (T,wt=13): 2186 x ^ ((((y v x) v z) v u) v v) = x. [para(1510(a,1),1280(a,1,1)),rewrite(1510(9))]. given #440 (T,wt=13): 2191 x ^ (y v (((z v x) v u) v v)) = x. [para(1510(a,1),1294(a,1,1)),rewrite(1510(9))]. given #441 (A,wt=17): 1401 x ^ (((y ^ x) ^ z) ^ u) = ((y ^ x) ^ z) ^ u. [para(1189(a,1),1278(a,1,1))]. given #442 (F,wt=13): 2264 x ^ (((y v (x v z)) v u) v v) = x. [para(1563(a,1),1280(a,1,1)),rewrite(1563(9))]. given #443 (F,wt=13): 2274 x ^ (y v ((z v (x v u)) v v)) = x. [para(1563(a,1),1294(a,1,1)),rewrite(1563(9))]. given #444 (T,wt=13): 2292 (x v y) v ((y v x) ^ z) = x v y. [para(1573(a,1),1200(a,1,2)),rewrite(2291(4),1573(7))]. given #445 (T,wt=13): 2293 (x v y) v (z ^ (y v x)) = x v y. [para(1573(a,1),1238(a,1,2)),rewrite(2291(4),1573(7))]. given #446 (A,wt=17): 1403 x ^ ((y ^ (x ^ z)) ^ u) = (y ^ (x ^ z)) ^ u. [para(1203(a,1),1278(a,1,1))]. given #447 (F,wt=13): 2296 (x v y) ^ ((y v x) v z) = x v y. [para(1573(a,1),1416(a,1,2,1))]. given #448 (F,wt=13): 2298 (x v y) ^ (z v (y v x)) = x v y. [para(1573(a,1),1513(a,1,2,2))]. given #449 (T,wt=13): 2329 (x v y) v ((z ^ y) v x) = x v y. [back_rewrite(2069),rewrite(2291(4))]. given #450 (T,wt=13): 2332 (x v y) v (x v (z ^ y)) = x v y. [back_rewrite(2057),rewrite(2291(4))]. given #451 (A,wt=17): 1404 x ^ ((y ^ (z ^ x)) ^ u) = (y ^ (z ^ x)) ^ u. [para(1210(a,1),1278(a,1,1))]. given #452 (F,wt=13): 2334 (x v y) v (y v (z ^ x)) = x v y. [back_rewrite(2041),rewrite(2291(4))]. given #453 (F,wt=13): 2339 (x v y) v (y v (x ^ z)) = x v y. [back_rewrite(2028),rewrite(2291(4))]. given #454 (T,wt=13): 2348 (x v y) v ((z ^ x) v y) = x v y. [back_rewrite(1949),rewrite(2291(4))]. given #455 (T,wt=13): 2353 (x v y) v ((x ^ z) v y) = x v y. [back_rewrite(1943),rewrite(2291(4))]. given #456 (A,wt=15): 1406 (x ^ y) v ((x v z) v u) = (x v z) v u. [para(1278(a,1),1200(a,1,1))]. given #457 (F,wt=13): 2394 (x v y) v ((y ^ z) v x) = x v y. [back_rewrite(1808),rewrite(2291(4))]. given #458 (F,wt=13): 2397 (x v y) v (x v (y ^ z)) = x v y. [back_rewrite(1798),rewrite(2291(4))]. given #459 (T,wt=13): 2407 x v ((y ^ (z ^ x)) v (x ^ u)) = x. [back_rewrite(1757),rewrite(2291(5))]. given #460 (T,wt=13): 2408 x v ((y ^ (x ^ z)) v (x ^ u)) = x. [back_rewrite(1756),rewrite(2291(5))]. given #461 (A,wt=15): 1407 (x v y) ^ ((x ^ z) ^ u) = (x ^ z) ^ u. [para(1200(a,1),1278(a,1,1))]. given #462 (F,wt=13): 2409 x v (((y ^ x) ^ z) v (x ^ u)) = x. [back_rewrite(1755),rewrite(2291(5))]. given #463 (F,wt=13): 2410 x v (((x ^ y) ^ z) v (x ^ u)) = x. [back_rewrite(1754),rewrite(2291(5))]. given #464 (T,wt=13): 2442 x v ((y ^ x) v (z ^ (u ^ x))) = x. [back_rewrite(1582),rewrite(2291(5))]. given #465 (T,wt=13): 2443 x v ((y ^ x) v (z ^ (x ^ u))) = x. [back_rewrite(1581),rewrite(2291(5))]. given #466 (A,wt=15): 1408 (x ^ y) v (z v (x v u)) = z v (x v u). [para(1278(a,1),1204(a,1,1))]. given #467 (F,wt=13): 2444 x v ((y ^ x) v ((z ^ x) ^ u)) = x. [back_rewrite(1580),rewrite(2291(5))]. given #468 (F,wt=13): 2445 x v ((y ^ x) v ((x ^ z) ^ u)) = x. [back_rewrite(1579),rewrite(2291(5))]. given #469 (T,wt=13): 2524 x ^ (((y v (z v x)) v u) v v) = x. [para(1614(a,1),1280(a,1,1)),rewrite(1614(9))]. given #470 (T,wt=13): 2527 x ^ (y v ((z v (u v x)) v v)) = x. [para(1614(a,1),1294(a,1,1)),rewrite(1614(9))]. given #471 (A,wt=15): 1409 (x v y) ^ ((y ^ z) ^ u) = (y ^ z) ^ u. [para(1204(a,1),1278(a,1,1))]. given #472 (F,wt=13): 2646 x ^ ((y v ((x v z) v u)) v v) = x. [para(1790(a,1),1280(a,1,1)),rewrite(1790(9))]. given #473 (F,wt=13): 2649 x ^ (y v (z v ((x v u) v v))) = x. [para(1790(a,1),1294(a,1,1)),rewrite(1790(9))]. given #474 (T,wt=13): 2672 x ^ ((y v ((z v x) v u)) v v) = x. [para(1792(a,1),1280(a,1,1)),rewrite(1792(9))]. given #475 (T,wt=13): 2675 x ^ (y v (z v ((u v x) v v))) = x. [para(1792(a,1),1294(a,1,1)),rewrite(1792(9))]. given #476 (A,wt=15): 1410 ((x v y) v z) v (x ^ u) = (x v y) v z. [para(1278(a,1),1224(a,1,2))]. given #477 (F,wt=13): 2701 x ^ ((y v (z v (x v u))) v v) = x. [para(1793(a,1),1280(a,1,1)),rewrite(1793(9))]. given #478 (F,wt=13): 2704 x ^ (y v (z v (u v (x v v)))) = x. [para(1793(a,1),1294(a,1,1)),rewrite(1793(9))]. given #479 (T,wt=13): 2727 x ^ ((y v (z v (u v x))) v v) = x. [para(1794(a,1),1280(a,1,1)),rewrite(1794(9))]. given #480 (T,wt=13): 2730 x ^ (y v (z v (u v (v v x)))) = x. [para(1794(a,1),1294(a,1,1)),rewrite(1794(9))]. given #481 (A,wt=15): 1411 (x v (y v z)) v (y ^ u) = x v (y v z). [para(1278(a,1),1226(a,1,2))]. given #482 (F,wt=13): 2924 x v (y' ^ (y v (x ^ y'))) = x. [back_rewrite(1037),rewrite(2869(5,R))]. given #483 (F,wt=13): 2928 x v (y' ^ (y v (y' ^ x))) = x. [para(2869(a,2),1067(a,1,2,1,2)),rewrite(699(2),2926(5))]. given #484 (T,wt=13): 2966 x ^ (((y v x) ^ (x v z)) v u) = x. [back_rewrite(2745),rewrite(2926(5))]. given #485 (T,wt=13): 2983 (x ^ y) v (x ^ (x' v y')) = x. [back_rewrite(2511),rewrite(2926(5))]. given #486 (A,wt=15): 1412 (x v y) ^ ((z ^ x) ^ u) = (z ^ x) ^ u. [para(1238(a,1),1278(a,1,1))]. given #487 (F,wt=13): 2984 (x ^ y) v (y ^ (x' v y')) = y. [back_rewrite(2509),rewrite(2926(5))]. given #488 (F,wt=13): 3214 (x ^ y) v ((x' v y') v z) = c_0. [back_rewrite(3211),rewrite(3212(8))]. given #489 (T,wt=13): 3332 (x v y) v ((x' ^ y') v z) = c_0. [back_rewrite(3187),rewrite(3310(11))]. given #490 (T,wt=13): 3348 (x' ^ y') v ((x v y) v z) = c_0. [para(22(a,1),3230(a,1,1))]. given #491 (A,wt=15): 1413 (x v y) ^ ((z ^ y) ^ u) = (z ^ y) ^ u. [para(1240(a,1),1278(a,1,1))]. given #492 (F,wt=13): 3349 (x' v y') v ((x ^ y) v z) = c_0. [para(887(a,1),3230(a,1,1))]. given #493 (F,wt=13): 3357 (x v y) v (z v (x' ^ y')) = c_0. [para(22(a,1),3235(a,1,2,2))]. given #494 (T,wt=13): 3358 (x ^ y) v (z v (x' v y')) = c_0. [para(887(a,1),3235(a,1,2,2))]. given #495 (T,wt=13): 3361 x v (((x ^ y) ^ z) v (u ^ x)) = x. [para(1201(a,1),1079(a,1,1)),rewrite(1201(5),1201(8))]. given #496 (A,wt=19): 1418 (x v y) ^ ((z ^ x) v (x ^ u)) = (z ^ x) v (x ^ u). [para(936(a,1),1383(a,1,1,1))]. given #497 (F,wt=13): 3362 x v (((y ^ x) ^ z) v (u ^ x)) = x. [para(1208(a,1),1079(a,1,1)),rewrite(1208(5),1208(8))]. given #498 (F,wt=13): 3363 x v ((y ^ (x ^ z)) v (u ^ x)) = x. [para(1225(a,1),1079(a,1,1)),rewrite(1225(5),1225(8))]. given #499 (T,wt=13): 3364 x v ((y ^ (z ^ x)) v (u ^ x)) = x. [para(1243(a,1),1079(a,1,1)),rewrite(1243(5),1243(8))]. given #500 (T,wt=13): 3384 (x' ^ y') v (z v (x v y)) = c_0. [para(22(a,1),3350(a,1,1))]. given #501 (A,wt=19): 1423 (x v y) ^ ((x ^ z) v (x ^ u)) = (x ^ z) v (x ^ u). [para(1001(a,1),1383(a,1,1,1))]. Low Water (keep): wt=39, part=0.98, limit=37 given #502 (F,wt=13): 3385 (x' v y') v (z v (x ^ y)) = c_0. [para(887(a,1),3350(a,1,1))]. given #503 (F,wt=13): 3460 x' ^ ((y ^ x) v (x ^ z)) = c_0'. [para(996(a,1),3453(a,1,2))]. given #504 (T,wt=13): 3465 x' ^ ((x ^ y) v (x ^ z)) = c_0'. [para(1053(a,1),3453(a,1,2))]. given #505 (T,wt=13): 3466 x' ^ ((y ^ x) v (z ^ x)) = c_0'. [para(1059(a,1),3453(a,1,2))]. given #506 (A,wt=19): 1424 (x v y) ^ ((z ^ x) v (u ^ x)) = (z ^ x) v (u ^ x). [para(1002(a,1),1383(a,1,1,1))]. Low Water (keep): wt=35, part=0.97, limit=35 given #507 (F,wt=13): 3467 x' ^ ((x ^ y) v (z ^ x)) = c_0'. [para(1081(a,1),3453(a,1,2))]. given #508 (F,wt=13): 3597 (x' ^ y') v (z v (y v x)) = c_0. [para(1573(a,1),3409(a,1,2,2)),rewrite(22(2))]. given #509 (T,wt=13): 3628 (x' ^ y') v ((y v x) v z) = c_0. [para(1573(a,1),3448(a,1,2,1)),rewrite(22(2))]. given #510 (T,wt=13): 3692 (x v y) v ((y' ^ x') v z) = c_0. [para(1573(a,1),3679(a,1,2)),rewrite(22(2),2291(6))]. given #511 (A,wt=21): 1425 ((x v y) v z) v (x v (((x v y) v z) ^ u)) = (x v y) v z. [para(1383(a,1),1048(a,1,2,1))]. given #512 (F,wt=13): 3693 x v ((x ^ y) v ((x ^ z) ^ u)) = x. [para(1199(a,1),1048(a,1,2,2))]. given #513 (F,wt=13): 3726 (x v y) v (z v (y' ^ x')) = c_0. [para(1573(a,1),3686(a,1,2)),rewrite(22(2),2291(6))]. given #514 (T,wt=13): 3754 x v ((x ^ y) v ((z ^ x) ^ u)) = x. [para(1207(a,1),1048(a,1,2,2))]. Low Water (keep): wt=33, part=0.95, limit=33 given #515 (T,wt=13): 3807 x v ((x ^ y) v (z ^ (x ^ u))) = x. [para(1237(a,1),1048(a,1,2,2))]. given #516 (A,wt=19): 1428 (x v y) ^ ((x ^ z) v (u ^ x)) = (x ^ z) v (u ^ x). [para(1056(a,1),1383(a,1,1,1))]. given #517 (F,wt=13): 3847 x v ((x ^ y) v (z ^ (u ^ x))) = x. [para(1251(a,1),1048(a,1,2,2))]. given #518 (F,wt=13): 3876 x' ^ (((x ^ y) ^ z) ^ u) = c_0'. [para(1199(a,1),3704(a,1,2,1))]. given #519 (T,wt=13): 3877 x' ^ (((y ^ x) ^ z) ^ u) = c_0'. [para(1207(a,1),3704(a,1,2,1))]. given #520 (T,wt=13): 3878 x' ^ ((y ^ (x ^ z)) ^ u) = c_0'. [para(1207(a,1),3704(a,1,2))]. given #521 (A,wt=21): 1429 ((x v y) v z) v (x v (u ^ ((x v y) v z))) = (x v y) v z. [para(1383(a,1),1075(a,1,2,1))]. Low Water (keep): wt=31, part=0.93, limit=31 given #522 (F,wt=13): 3880 x' ^ (y ^ ((x ^ z) ^ u)) = c_0'. [para(1237(a,1),3704(a,1,2))]. given #523 (F,wt=13): 3882 x' ^ ((y ^ (z ^ x)) ^ u) = c_0'. [para(1251(a,1),3704(a,1,2,1))]. given #524 (T,wt=13): 3883 x' ^ (y ^ (z ^ (x ^ u))) = c_0'. [para(1251(a,1),3704(a,1,2))]. given #525 (T,wt=13): 3896 x ^ (((x' ^ y) ^ z) ^ u) = c_0'. [para(1199(a,1),3705(a,1,2,1))]. given #526 (A,wt=23): 1432 (x v y) ^ (((z ^ x) v (x ^ u)) ^ v) = ((z ^ x) v (x ^ u)) ^ v. [para(935(a,1),1383(a,1,1,1))]. given #527 (F,wt=13): 3897 x ^ (((y ^ x') ^ z) ^ u) = c_0'. [para(1207(a,1),3705(a,1,2,1))]. given #528 (F,wt=13): 3898 x ^ ((y ^ (x' ^ z)) ^ u) = c_0'. [para(1207(a,1),3705(a,1,2))]. given #529 (T,wt=13): 3900 x ^ (y ^ ((x' ^ z) ^ u)) = c_0'. [para(1237(a,1),3705(a,1,2))]. given #530 (T,wt=13): 3902 x ^ ((y ^ (z ^ x')) ^ u) = c_0'. [para(1251(a,1),3705(a,1,2,1))]. given #531 (A,wt=15): 1434 (x ^ y) v ((y v z) v u) = (y v z) v u. [para(1383(a,1),1203(a,1,1,2))]. Low Water (keep): wt=29, part=0.91, limit=29 given #532 (F,wt=13): 3903 x ^ (y ^ (z ^ (x' ^ u))) = c_0'. [para(1251(a,1),3705(a,1,2))]. given #533 (F,wt=13): 3931 x' ^ (y ^ ((z ^ x) ^ u)) = c_0'. [para(1237(a,1),3765(a,1,2))]. given #534 (T,wt=13): 3933 x' ^ (y ^ (z ^ (u ^ x))) = c_0'. [para(1251(a,1),3765(a,1,2))]. given #535 (T,wt=13): 3943 x ^ (y ^ ((z ^ x') ^ u)) = c_0'. [para(1237(a,1),3766(a,1,2))]. given #536 (A,wt=15): 1435 (x v y) ^ (z ^ (x ^ u)) = z ^ (x ^ u). [para(1203(a,1),1383(a,1,1,1))]. given #537 (F,wt=13): 3945 x ^ (y ^ (z ^ (u ^ x'))) = c_0'. [para(1251(a,1),3766(a,1,2))]. given #538 (F,wt=13): 4046 ((x ^ y) ^ z) ^ (x' ^ u) = c_0'. [para(1199(a,1),3879(a,1,1))]. given #539 (T,wt=13): 4047 (x ^ y) ^ ((x' ^ z) ^ u) = c_0'. [para(1199(a,1),3879(a,1,2))]. given #540 (T,wt=13): 4048 ((x ^ y) ^ z) ^ (y' ^ u) = c_0'. [para(1207(a,1),3879(a,1,1))]. given #541 (A,wt=15): 1436 (x v y) ^ (z ^ (u ^ x)) = z ^ (u ^ x). [para(1210(a,1),1383(a,1,1,1))]. given #542 (F,wt=13): 4049 (x ^ y) ^ ((z ^ x') ^ u) = c_0'. [para(1207(a,1),3879(a,1,2))]. given #543 (F,wt=13): 4050 (x ^ (y ^ z)) ^ (y' ^ u) = c_0'. [para(1237(a,1),3879(a,1,1))]. given #544 (T,wt=13): 4051 (x ^ y) ^ (z ^ (x' ^ u)) = c_0'. [para(1237(a,1),3879(a,1,2))]. given #545 (T,wt=13): 4052 (x ^ (y ^ z)) ^ (z' ^ u) = c_0'. [para(1251(a,1),3879(a,1,1))]. given #546 (A,wt=15): 1438 ((x v y) v z) v (u ^ x) = (x v y) v z. [para(1383(a,1),1225(a,1,2,2))]. given #547 (F,wt=13): 4053 (x ^ y) ^ (z ^ (u ^ x')) = c_0'. [para(1251(a,1),3879(a,1,2))]. given #548 (F,wt=13): 4063 ((x ^ y) ^ z) ^ (u ^ x') = c_0'. [para(1199(a,1),3881(a,1,1))]. given #549 (T,wt=13): 4064 ((x ^ y) ^ z) ^ (u ^ y') = c_0'. [para(1207(a,1),3881(a,1,1))]. given #550 (T,wt=13): 4065 (x ^ (y ^ z)) ^ (u ^ y') = c_0'. [para(1237(a,1),3881(a,1,1))]. given #551 (A,wt=17): 1439 x v (((x v y) v z) v u) = ((x v y) v z) v u. [para(1383(a,1),1200(a,1,1))]. given #552 (F,wt=13): 4066 (x ^ (y ^ z)) ^ (u ^ z') = c_0'. [para(1251(a,1),3881(a,1,1))]. given #553 (F,wt=13): 4082 ((x' ^ y) ^ z) ^ (x ^ u) = c_0'. [para(1199(a,1),3899(a,1,1))]. given #554 (T,wt=13): 4083 (x' ^ y) ^ ((x ^ z) ^ u) = c_0'. [para(1199(a,1),3899(a,1,2))]. given #555 (T,wt=13): 4084 ((x ^ y') ^ z) ^ (y ^ u) = c_0'. [para(1207(a,1),3899(a,1,1))]. given #556 (A,wt=17): 1440 x v (y v ((x v z) v u)) = y v ((x v z) v u). [para(1383(a,1),1204(a,1,1))]. given #557 (F,wt=13): 4085 (x' ^ y) ^ ((z ^ x) ^ u) = c_0'. [para(1207(a,1),3899(a,1,2))]. given #558 (F,wt=13): 4086 (x ^ (y' ^ z)) ^ (y ^ u) = c_0'. [para(1237(a,1),3899(a,1,1))]. given #559 (T,wt=13): 4087 (x' ^ y) ^ (z ^ (x ^ u)) = c_0'. [para(1237(a,1),3899(a,1,2))]. given #560 (T,wt=13): 4088 (x ^ (y ^ z')) ^ (z ^ u) = c_0'. [para(1251(a,1),3899(a,1,1))]. given #561 (A,wt=19): 1449 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(871(a,1),996(a,1,2,1)),rewrite(871(7))]. Low Water (keep): wt=27, part=0.86, limit=27 given #562 (F,wt=13): 4089 (x' ^ y) ^ (z ^ (u ^ x)) = c_0'. [para(1251(a,1),3899(a,1,2))]. given #563 (F,wt=13): 4108 ((x' ^ y) ^ z) ^ (u ^ x) = c_0'. [para(1199(a,1),3901(a,1,1))]. given #564 (T,wt=13): 4110 ((x ^ y') ^ z) ^ (u ^ y) = c_0'. [para(1207(a,1),3901(a,1,1))]. given #565 (T,wt=13): 4111 (x ^ (y' ^ z)) ^ (u ^ y) = c_0'. [para(1237(a,1),3901(a,1,1))]. given #566 (A,wt=19): 1453 (x v y) ^ (y v ((x v y) ^ z)) = y v ((x v y) ^ z). [para(1032(a,1),996(a,1,2,1)),rewrite(1032(7))]. given #567 (F,wt=13): 4113 (x ^ (y ^ z')) ^ (u ^ z) = c_0'. [para(1251(a,1),3901(a,1,1))]. given #568 (F,wt=13): 4144 (x ^ y) ^ ((y' ^ z) ^ u) = c_0'. [para(1199(a,1),3929(a,1,2))]. given #569 (T,wt=13): 4145 (x ^ y) ^ ((z ^ y') ^ u) = c_0'. [para(1207(a,1),3929(a,1,2))]. given #570 (T,wt=13): 4146 (x ^ y) ^ (z ^ (y' ^ u)) = c_0'. [para(1237(a,1),3929(a,1,2))]. given #571 (A,wt=15): 1454 x v ((y ^ x) v ((z ^ x) v (x ^ u))) = x. [para(996(a,1),998(a,1,2,2))]. given #572 (F,wt=13): 4147 (x ^ y) ^ (z ^ (u ^ y')) = c_0'. [para(1251(a,1),3929(a,1,2))]. given #573 (F,wt=13): 4171 (x ^ y') ^ ((y ^ z) ^ u) = c_0'. [para(1199(a,1),3942(a,1,2))]. given #574 (T,wt=13): 4172 (x ^ y') ^ ((z ^ y) ^ u) = c_0'. [para(1207(a,1),3942(a,1,2))]. given #575 (T,wt=13): 4173 (x ^ y') ^ (z ^ (y ^ u)) = c_0'. [para(1237(a,1),3942(a,1,2))]. given #576 (A,wt=15): 1457 x v (((y ^ x) v (x ^ z)) v (x ^ u)) = x. [para(996(a,1),1048(a,1,2,1))]. given #577 (F,wt=13): 4174 (x ^ y') ^ (z ^ (u ^ y)) = c_0'. [para(1251(a,1),3942(a,1,2))]. given #578 (F,wt=13): 4284 x ^ (y v ((z v x) ^ (x v u))) = x. [para(4201(a,1),1346(a,1,2)),rewrite(2926(5),4201(9))]. given #579 (T,wt=13): 4303 x ^ ((y v x) ^ ((x v z) v u)) = x. [para(1279(a,1),4201(a,1,2,2))]. given #580 (T,wt=13): 4304 x ^ ((y v x) ^ ((z v x) v u)) = x. [para(1281(a,1),4201(a,1,2,2))]. given #581 (A,wt=15): 1458 x v ((x ^ y) v ((z ^ x) v (x ^ u))) = x. [para(996(a,1),1048(a,1,2,2))]. given #582 (F,wt=13): 4306 x ^ ((y v x) ^ (z v (x v u))) = x. [para(1293(a,1),4201(a,1,2,2))]. given #583 (F,wt=13): 4307 (x v y) ^ (y v (x' ^ y')) = y. [back_rewrite(2989),rewrite(4252(7))]. given #584 (T,wt=12): 17521 x ^ (x' v (x ^ y)) = x ^ y. [para(790(a,1),4307(a,1,1)),rewrite(887(4),871(6),2291(3))]. given #585 (T,wt=12): 17525 x ^ (x' v (y ^ x)) = y ^ x. [para(945(a,1),4307(a,1,1)),rewrite(887(4),1032(6),2291(3))]. given #586 (A,wt=15): 1460 x v (((y ^ x) v (x ^ z)) v (u ^ x)) = x. [para(996(a,1),1075(a,1,2,1))]. given #587 (F,wt=13): 4336 x ^ (((y v x) ^ (z v x)) v u) = x. [para(4254(a,1),1328(a,1,2)),rewrite(2926(5),4254(9))]. given #588 (F,wt=13): 4337 x ^ (y v ((z v x) ^ (u v x))) = x. [para(4254(a,1),1346(a,1,2)),rewrite(2926(5),4254(9))]. given #589 (T,wt=13): 4370 x ^ ((y v x) ^ (z v (u v x))) = x. [para(1295(a,1),4201(a,1,2,2))]. given #590 (T,wt=13): 4385 x ^ (((x v y) ^ (x v z)) v u) = x. [para(4291(a,1),1328(a,1,2)),rewrite(2926(5),4291(9))]. given #591 (A,wt=15): 1470 ((x ^ y) v (y ^ z)) v (y v u) = y v u. [para(996(a,1),1200(a,1,1))]. given #592 (F,wt=13): 4386 x ^ (y v ((x v z) ^ (x v u))) = x. [para(4291(a,1),1346(a,1,2)),rewrite(2926(5),4291(9))]. given #593 (F,wt=13): 4394 x ^ (((x v y) v z) ^ (x v u)) = x. [para(1279(a,1),4291(a,1,2,1))]. given #594 (T,wt=13): 4395 x ^ ((x v y) ^ ((x v z) v u)) = x. [para(1279(a,1),4291(a,1,2,2))]. given #595 (T,wt=13): 4396 x ^ (((y v x) v z) ^ (x v u)) = x. [para(1281(a,1),4291(a,1,2,1))]. given #596 (A,wt=15): 1471 ((x ^ y) v (y ^ z)) v (u v y) = u v y. [para(996(a,1),1204(a,1,1))]. Low Water (keep): wt=25, part=0.78, limit=25 given #597 (F,wt=13): 4397 x ^ ((x v y) ^ ((z v x) v u)) = x. [para(1281(a,1),4291(a,1,2,2))]. given #598 (F,wt=13): 4400 x ^ ((y v (x v z)) ^ (x v u)) = x. [para(1293(a,1),4291(a,1,2,1))]. given #599 (T,wt=13): 4401 x ^ ((x v y) ^ (z v (x v u))) = x. [para(1293(a,1),4291(a,1,2,2))]. given #600 (T,wt=13): 4402 x ^ ((y v (z v x)) ^ (x v u)) = x. [para(1295(a,1),4291(a,1,2,1))]. given #601 (A,wt=15): 1472 (x v y) v ((z ^ x) v (x ^ u)) = x v y. [para(996(a,1),1224(a,1,2))]. given #602 (F,wt=13): 4403 x ^ ((x v y) ^ (z v (u v x))) = x. [para(1295(a,1),4291(a,1,2,2))]. given #603 (F,wt=13): 4406 (x v y) ^ (x v (x' ^ y')) = x. [back_rewrite(2988),rewrite(4371(7))]. given #604 (T,wt=13): 4417 x ^ (((x v y) ^ (z v x)) v u) = x. [para(4293(a,1),1328(a,1,2)),rewrite(2926(5),4293(9))]. given #605 (T,wt=13): 4418 x ^ (y v ((x v z) ^ (u v x))) = x. [para(4293(a,1),1346(a,1,2)),rewrite(2926(5),4293(9))]. given #606 (A,wt=15): 1473 (x v y) v ((z ^ y) v (y ^ u)) = x v y. [para(996(a,1),1226(a,1,2))]. given #607 (F,wt=13): 4426 x ^ (((x v y) v z) ^ (u v x)) = x. [para(1279(a,1),4293(a,1,2,1))]. given #608 (F,wt=13): 4427 x ^ (((y v x) v z) ^ (u v x)) = x. [para(1281(a,1),4293(a,1,2,1))]. given #609 (T,wt=13): 4429 x ^ ((y v (x v z)) ^ (u v x)) = x. [para(1293(a,1),4293(a,1,2,1))]. given #610 (T,wt=13): 4430 x ^ ((y v (z v x)) ^ (u v x)) = x. [para(1295(a,1),4293(a,1,2,1))]. given #611 (A,wt=23): 1474 (x v y) ^ ((z ^ (x v y)) v (x ^ u)) = (z ^ (x v y)) v (x ^ u). [para(1278(a,1),996(a,1,2,2)),rewrite(1278(11))]. given #612 (F,wt=13): 12386 x v ((y v x') ^ (x' v z)) = c_0. [para(2966(a,1),2464(a,1,2)),rewrite(3212(2),2291(7)),flip(a)]. given #613 (F,wt=12): 19034 x' v ((y v x) ^ (x v z)) = c_0. [para(699(a,1),12386(a,1,2,1,2)),rewrite(699(4))]. given #614 (T,wt=12): 19049 x' v ((y v x) ^ (z v x)) = c_0. [para(1031(a,1),19034(a,1,2,2))]. given #615 (T,wt=12): 19062 x' v ((x v y) ^ (x v z)) = c_0. [para(2291(a,1),19034(a,1,2,1))]. given #616 (A,wt=25): 1476 x ^ ((y ^ x) v ((z ^ x) v (x ^ u))) = (y ^ x) v ((z ^ x) v (x ^ u)). [para(996(a,1),996(a,1,2,2)),rewrite(996(11))]. given #617 (F,wt=12): 19063 x' v ((x v y) ^ (z v x)) = c_0. [para(2926(a,1),19034(a,1,2))]. given #618 (F,wt=13): 12512 (x ^ y') v (x ^ (x' v y)) = x. [para(699(a,1),2983(a,1,2,2,2))]. given #619 (T,wt=13): 12519 (x ^ y) v (x ^ (y' v x')) = x. [para(2291(a,1),2983(a,1,2,2))]. given #620 (T,wt=13): 12520 (x ^ y) v (y ^ (y' v x')) = y. [para(2926(a,1),2983(a,1,1))]. given #621 (A,wt=21): 1495 ((x v y) v z) v (y v (((x v y) v z) ^ u)) = (x v y) v z. [para(1385(a,1),1048(a,1,2,1))]. given #622 (F,wt=13): 12618 (x' ^ y) v (y ^ (x v y')) = y. [para(699(a,1),2984(a,1,2,2,1))]. given #623 (F,wt=13): 12658 (x' ^ y) v ((x v y') v z) = c_0. [para(699(a,1),3214(a,1,2,1,1))]. given #624 (T,wt=13): 12659 (x ^ y') v ((x' v y) v z) = c_0. [para(699(a,1),3214(a,1,2,1,2))]. given #625 (T,wt=13): 12663 (x ^ y) v ((y' v x') v z) = c_0. [para(2291(a,1),3214(a,1,2,1))]. given #626 (A,wt=21): 1498 ((x v y) v z) v (y v (u ^ ((x v y) v z))) = (x v y) v z. [para(1385(a,1),1075(a,1,2,1))]. given #627 (F,wt=13): 12674 (x' v y) v ((x ^ y') v z) = c_0. [para(699(a,1),3332(a,1,2,1,1))]. given #628 (F,wt=13): 12675 (x v y') v ((x' ^ y) v z) = c_0. [para(699(a,1),3332(a,1,2,1,2))]. given #629 (T,wt=13): 12813 (x' v y') v ((y ^ x) v z) = c_0. [para(2291(a,1),3349(a,1,1))]. given #630 (T,wt=13): 12824 (x' v y) v (z v (x ^ y')) = c_0. [para(699(a,1),3357(a,1,2,2,1))]. given #631 (A,wt=15): 1500 (x ^ y) v ((z v x) v u) = (z v x) v u. [para(1385(a,1),1188(a,1,1,1))]. given #632 (F,wt=13): 12825 (x v y') v (z v (x' ^ y)) = c_0. [para(699(a,1),3357(a,1,2,2,2))]. given #633 (F,wt=13): 12830 (x' ^ y) v (z v (x v y')) = c_0. [para(699(a,1),3358(a,1,2,2,1))]. given #634 (T,wt=13): 12831 (x ^ y') v (z v (x' v y)) = c_0. [para(699(a,1),3358(a,1,2,2,2))]. given #635 (T,wt=13): 12835 (x ^ y) v (z v (y' v x')) = c_0. [para(2291(a,1),3358(a,1,2,2))]. given #636 (A,wt=15): 1502 ((x v y) v z) v (y ^ u) = (x v y) v z. [para(1385(a,1),1201(a,1,2,1))]. given #637 (F,wt=13): 13479 (x' v y') v (z v (y ^ x)) = c_0. [para(2291(a,1),3385(a,1,1))]. given #638 (F,wt=13): 13831 (x ^ y') v (z v (y v x')) = c_0. [para(699(a,1),3597(a,1,1,1))]. given #639 (T,wt=13): 13832 (x' ^ y) v (z v (y' v x)) = c_0. [para(699(a,1),3597(a,1,1,2))]. given #640 (T,wt=13): 13841 (x ^ y') v ((y v x') v z) = c_0. [para(699(a,1),3628(a,1,1,1))]. given #641 (A,wt=15): 1503 (x ^ y) v ((z v y) v u) = (z v y) v u. [para(1385(a,1),1203(a,1,1,2))]. given #642 (F,wt=13): 13842 (x' ^ y) v ((y' v x) v z) = c_0. [para(699(a,1),3628(a,1,1,2))]. given #643 (F,wt=13): 13847 (x v y') v ((y ^ x') v z) = c_0. [para(699(a,1),3692(a,1,2,1,1))]. given #644 (T,wt=13): 13848 (x' v y) v ((y' ^ x) v z) = c_0. [para(699(a,1),3692(a,1,2,1,2))]. given #645 (T,wt=13): 14033 (x v y') v (z v (y ^ x')) = c_0. [para(699(a,1),3726(a,1,2,2,1))]. given #646 (A,wt=15): 1505 ((x v y) v z) v (u ^ y) = (x v y) v z. [para(1385(a,1),1225(a,1,2,2))]. given #647 (F,wt=13): 14034 (x' v y) v (z v (y' ^ x)) = c_0. [para(699(a,1),3726(a,1,2,2,2))]. given #648 (F,wt=13): 16351 x v (y v ((y v x) ^ z)) = y v x. [para(1449(a,1),1051(a,1,2,2)),rewrite(1635(6))]. Low Water (keep): wt=23, part=0.70, limit=23 given #649 (T,wt=11): 20070 x v (y v (x ^ z)) = y v x. [para(1292(a,1),16351(a,1,2,2))]. ============================== PROOF ================================= % Proof 3 at 10.95 (+ 0.10) seconds: A_SS. % Length of proof is 175. % Level of proof is 37. % Maximum clause weight is 38. % Given clauses 649. 1 f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS) # label(goal). [goal]. 4 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(f(y,y),z)),z))) = y # label(OML_Sh). [assumption]. 5 x v y = f(f(x,x),f(y,y)) # label(definition_join). [assumption]. 6 f(f(x,x),f(y,y)) = x v y. [copy(5),flip(a)]. 7 x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). [assumption]. 8 f(f(x,y),f(x,y)) = x ^ y. [copy(7),flip(a)]. 9 x' = f(x,x) # label(definition_complementation). [assumption]. 10 f(x,x) = x'. [copy(9),flip(a)]. 11 f(c1,f(f(c2,c3),f(c2,c3))) != f(c2,f(f(c1,c3),f(c1,c3))) # answer(A_SS). [deny(1)]. 12 f(c2,f(c1,c3)') != f(c1,f(c2,c3)') # answer(A_SS). [copy(11),rewrite(10(8),10(14)),flip(a)]. 16 f(x,y)' = x ^ y. [back_rewrite(8),rewrite(10(3))]. 17 f(x',y') = x v y. [back_rewrite(6),rewrite(10(1),10(2))]. 18 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(y',z)),z))) = y. [back_rewrite(4),rewrite(10(5))]. 19 f(c2,c1 ^ c3) != f(c1,c2 ^ c3) # answer(A_SS). [back_rewrite(12),rewrite(16(5),16(10))]. 20 x ^ x = x''. [para(10(a,1),16(a,1,1)),flip(a)]. 22 (x v y)' = x' ^ y'. [para(17(a,1),16(a,1,1))]. 23 f(x ^ y,z') = f(x,y) v z. [para(16(a,1),17(a,1,1))]. 24 f(x',y ^ z) = x v f(y,z). [para(16(a,1),17(a,1,2))]. 25 f(f(f(x',f(x,y)),z),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),18(a,1,1,1,1))]. 26 f(f(f(f(x,y),y'),z),f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),18(a,1,1,1,2))]. 27 f(f(x'',y),f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),18(a,1,1,1)),rewrite(10(1))]. 28 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(y',z)),z))) = y. [para(10(a,1),18(a,1,1)),rewrite(16(4))]. 29 f(f(f(f(x,y),f(y,y')),z),f(y,f(y v y',y'))) = y. [para(10(a,1),18(a,1,2,2,1,2)),rewrite(17(9))]. 34 f(f(f(f(x,y),f(y,z')),u),f(y,f(f(z',y v z),z'))) = y. [para(17(a,1),18(a,1,2,2,1,2))]. 35 f(f(x,y),f(x,f(f(f(f(z,f(x',z)),z),f(x',f(f(z,f(x',z)),z))),f(f(z,f(x',z)),z)))) = x. [para(18(a,1),18(a,1,1,1))]. 36 f(x,f(f(x,y),f(f(z,f(x ^ y,z)),z))) = f(x,y). [para(18(a,1),18(a,1,1)),rewrite(16(3))]. 44 f(x''',f(x,f(f(x,f(x',x)),x))) = x. [para(10(a,1),27(a,1,1))]. 45 f(x'',y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(27(a,1),16(a,1,1)),flip(a)]. 47 f(x' v y,f(x,f(f(x,f(x',x)),x))) = x. [para(17(a,1),27(a,1,1))]. 51 x''' ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(44(a,1),16(a,1,1)),flip(a)]. 57 f(x' ^ f(x,y),f(x,f(f(y,f(x',y)),y))) = x. [para(10(a,1),25(a,1,1)),rewrite(16(4))]. 68 f(x,f(x',f(f(y,f(x'',y)),y))) = x'. [para(27(a,1),25(a,1,1))]. 69 (x' v y) ^ f(x,f(f(x,f(x',x)),x)) = x'. [para(47(a,1),16(a,1,1)),flip(a)]. 75 x ^ f(x',f(f(y,f(x'',y)),y)) = x''. [para(68(a,1),16(a,1,1)),flip(a)]. 89 f(f(x,y) ^ y',f(y,f(f(y,f(y',y)),y))) = y. [para(10(a,1),26(a,1,1)),rewrite(16(4))]. 90 f(f(f(x,y),y'),z) ^ f(y,f(f(y,f(y',y)),y)) = y'. [para(26(a,1),16(a,1,1)),flip(a)]. 109 x ^ f(f(x,y),f(f(z,f(x ^ y,z)),z)) = x ^ y. [para(36(a,1),16(a,1,1)),rewrite(16(2)),flip(a)]. 117 f(f(x'',y),f(x,f(f(z,f(x',z)),z))) = x. [para(27(a,1),36(a,1,2,1)),rewrite(45(12),27(18))]. 118 f(x''',f(x,f(f(y,f(x',y)),y))) = x. [para(44(a,1),36(a,1,2,1)),rewrite(51(12),44(18))]. 120 f(x' v y,f(x,f(f(z,f(x',z)),z))) = x. [para(47(a,1),36(a,1,2,1)),rewrite(69(10),47(16))]. 121 f(f(f(f(x,y),y'),z),f(y,f(f(u,f(y',u)),u))) = y. [para(26(a,1),36(a,1,2,1)),rewrite(90(14),26(20))]. 123 (f(x,y) ^ f(y,z)) ^ f(y,f(f(z,f(y',z)),z)) = y'. [para(28(a,1),16(a,1,1)),flip(a)]. 127 f(f(x,y) ^ f(y,z'),f(y,f(f(z',y v z),z'))) = y. [para(17(a,1),28(a,1,2,2,1,2))]. 134 f(f(x,y) ^ f(y,z),f(y,f(f(u,f(y',u)),u))) = y. [para(28(a,1),36(a,1,2,1)),rewrite(123(12),28(18))]. 135 f(x''',f(x,f(x v x',x'))) = x. [para(10(a,1),118(a,1,2,2,1,2)),rewrite(17(7))]. 136 x''' ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(118(a,1),16(a,1,1)),flip(a)]. 148 x' ^ f(x'',f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x'''. [para(135(a,1),75(a,1,2,2,1,2))]. 151 (x' v y) ^ f(x,f(f(z,f(x',z)),z)) = x'. [para(120(a,1),16(a,1,1)),flip(a)]. 174 f(f(x'',y),f(x,f(f(z',x v z),z'))) = x. [para(17(a,1),117(a,1,2,2,1,2))]. 208 (x' v y) ^ f(x,f(f(z',x v z),z')) = x'. [para(17(a,1),151(a,1,2,2,1,2))]. 220 (x' ^ f(x,y)) ^ f(x,f(f(y,f(x',y)),y)) = x'. [para(57(a,1),16(a,1,1)),flip(a)]. 229 f(x' ^ f(x,y),f(x,f(f(z,f(x',z)),z))) = x. [para(57(a,1),36(a,1,2,1)),rewrite(220(12),57(18))]. 231 (f(x,y) ^ y') ^ f(y,f(f(y,f(y',y)),y)) = y'. [para(89(a,1),16(a,1,1)),flip(a)]. 238 f(f(x,y) ^ y',f(y,f(f(z,f(y',z)),z))) = y. [para(89(a,1),36(a,1,2,1)),rewrite(231(12),89(18))]. 284 f(x' ^ f(x,y),f(x,f(x v x',x'))) = x. [para(10(a,1),229(a,1,2,2,1,2)),rewrite(17(7))]. 307 f(x',f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x'))))) = f(x',f(x,y)). [para(284(a,1),36(a,1,2,2,1,2))]. 311 x' ^ f(f(x',f(x,y)),f(f(f(x,f(x v x',x')),x),f(x,f(x v x',x')))) = x' ^ f(x,y). [para(284(a,1),109(a,1,2,2,1,2))]. 341 f(f(x,y),f(y,f(y v y',y'))) = y. [para(35(a,1),29(a,1,1))]. 351 x' ^ f(f(x',f(x,y)),x) = x' ^ f(x,y). [back_rewrite(311),rewrite(341(16))]. 352 f(x',f(f(x',f(x,y)),x)) = f(x',f(x,y)). [back_rewrite(307),rewrite(341(16))]. 360 x' ^ f(x'',x) = x'''. [back_rewrite(148),rewrite(341(15))]. 380 x'' ^ (x'' v x) = x''''. [para(17(a,1),360(a,1,2))]. 393 f(x',f(x,f(x v x',x'))) = x. [para(10(a,1),341(a,1,1))]. 414 f(x,x'') = x'. [para(393(a,1),68(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 415 x ^ x'' = x''. [para(393(a,1),75(a,1,2,2,1,2)),rewrite(341(22),10(3))]. 417 x'' v x = x. [para(393(a,1),118(a,1,2,2,1,2)),rewrite(341(15),10(4),17(5))]. 418 f(x' v y,x') = x. [para(393(a,1),120(a,1,2,2,1,2)),rewrite(341(14),10(3))]. 420 x''' ^ x' = x'. [para(393(a,1),136(a,1,2,2,1,2)),rewrite(341(15),10(4))]. 421 (x' v y) ^ x' = x'. [para(393(a,1),151(a,1,2,2,1,2)),rewrite(341(14),10(3))]. 424 f(x',f(x,f(f(y',x v y),y'))) = x. [para(393(a,1),174(a,1,1))]. 428 f(f(x,y),y') v y = y. [para(393(a,1),238(a,1,2,2,1,2)),rewrite(341(15),10(4),23(5))]. 439 x'' ^ x = x''''. [back_rewrite(380),rewrite(417(5))]. 443 x''''' = x'. [back_rewrite(420),rewrite(439(5))]. 522 x'''' = x. [para(443(a,1),414(a,1,2)),rewrite(17(5),417(3)),flip(a)]. 533 x'' ^ x = x. [back_rewrite(439),rewrite(522(7))]. 535 f(x,y) = (x ^ y)'''. [para(16(a,1),522(a,1,1,1,1)),flip(a)]. 536 (x ^ y')''' = x''' v y. [para(522(a,1),17(a,1,1)),rewrite(535(2))]. 537 (x' ^ y)''' = x v y'''. [para(522(a,1),17(a,1,2)),rewrite(535(2))]. 539 (x ^ (y ^ z))''' = x''' v (y ^ z)'''. [para(522(a,1),24(a,1,1)),rewrite(535(2),535(9))]. 563 (x v y) ^ (x'' v ((z''' v (x ^ z)'') ^ z)'') = x. [para(522(a,1),151(a,1,1,1)),rewrite(522(8),535(5),535(9),536(12),535(12),535(16),536(19),522(5),522(19))]. 576 (x v y) ^ (x'' v ((z v (x ^ z')'') ^ z')'') = x. [para(522(a,1),208(a,1,1,1)),rewrite(535(10),537(13),22(9),522(8),535(11),536(14),22(10),536(10),535(14),537(17),22(13),537(12),22(8),522(7),522(18))]. 578 (((x ^ y)'' v (y ^ z)'') ^ u)'' v (y ^ ((z ^ (y v z'''))'' v z'''))'' = y. [para(522(a,1),34(a,1,1,1,2,2)),rewrite(535(1),535(5),535(9),536(12),522(5),535(8),522(15),535(16),522(23),535(20),537(23),535(23),535(27),536(30),522(12))]. 584 ((x v y) ^ x)''' = x'''. [para(522(a,1),418(a,1,1,1)),rewrite(522(5),535(2))]. 609 ((x ^ y)'' v y) v y = y. [back_rewrite(428),rewrite(535(1),535(6),536(9),522(5))]. 611 x v (x ^ ((y' ^ (x v y))'' v y))'' = x. [back_rewrite(424),rewrite(535(4),537(7),22(3),535(9),536(12),22(8),536(8),522(6),535(8),535(12),536(15),522(4))]. 625 x v (x ^ y)'' = x''. [back_rewrite(352),rewrite(535(3),535(7),536(10),522(5),535(6),584(9),535(5),415(5),522(4),535(4),535(8),536(11),522(6)),flip(a)]. 626 x' ^ (x ^ y)''' = x'''. [back_rewrite(351),rewrite(535(3),535(7),536(10),522(5),625(5),535(4),533(4),415(5),535(5)),flip(a)]. 680 ((x ^ y)'' v (y ^ z)'') v (y ^ ((u ^ (y v u'''))'' v u'''))'' = y. [back_rewrite(134),rewrite(535(1),535(5),535(11),537(14),535(14),535(18),537(21),535(21),535(25),536(28),536(12),522(5))]. 681 ((x ^ y)'' v (y ^ z')'') v (y ^ ((z' ^ (y v z))'' v z))'' = y. [back_rewrite(127),rewrite(535(1),535(6),536(9),535(12),537(15),22(11),535(17),536(20),22(16),536(16),522(14),535(16),535(20),536(23),537(12),22(8),522(7))]. 686 (((x ^ y)'' v y) ^ z)'' v (y ^ ((u ^ (y v u'''))'' v u'''))'' = y. [back_rewrite(121),rewrite(535(1),535(6),536(9),522(5),535(5),535(10),537(13),535(13),535(17),537(20),535(20),535(24),536(27),522(9))]. 695 c2''' v (c1 ^ c3)''' != c1''' v (c2 ^ c3)''' # answer(A_SS). [back_rewrite(19),rewrite(535(5),539(8),535(16),539(19))]. 699 x'' = x. [back_rewrite(611),rewrite(625(10))]. 746 c2' v (c1 ^ c3)' != c1' v (c2 ^ c3)' # answer(A_SS). [back_rewrite(695),rewrite(699(3),699(7),699(10),699(14))]. 753 (((x ^ y) v y) ^ z) v (y ^ ((u ^ (y v u')) v u')) = y. [back_rewrite(686),rewrite(699(3),699(5),699(5),699(8),699(8),699(11))]. 757 ((x ^ y) v (y ^ z')) v (y ^ ((z' ^ (y v z)) v z)) = y. [back_rewrite(681),rewrite(699(3),699(5),699(9),699(11))]. 758 ((x ^ y) v (y ^ z)) v (y ^ ((u ^ (y v u')) v u')) = y. [back_rewrite(680),rewrite(699(3),699(4),699(5),699(8),699(8),699(11))]. 789 x' ^ (x ^ y)' = x'. [back_rewrite(626),rewrite(699(4),699(6))]. 790 x v (x ^ y) = x. [back_rewrite(625),rewrite(699(3),699(4))]. 797 ((x ^ y) v y) v y = y. [back_rewrite(609),rewrite(699(3))]. 805 (((x ^ y) v (y ^ z)) ^ u) v (y ^ ((z ^ (y v z')) v z')) = y. [back_rewrite(578),rewrite(699(3),699(4),699(6),699(6),699(9),699(9),699(12))]. 807 (x v y) ^ (x v ((z v (x ^ z')) ^ z')) = x. [back_rewrite(576),rewrite(699(3),699(5),699(8))]. 812 (x v y) ^ (x v ((z' v (x ^ z)) ^ z)) = x. [back_rewrite(563),rewrite(699(3),699(3),699(5),699(7))]. 817 (x' ^ y)' = x v y'. [back_rewrite(537),rewrite(699(4),699(5))]. 821 x ^ x = x. [back_rewrite(20),rewrite(699(3))]. 823 (x v y) ^ x = x. [para(699(a,1),421(a,1,1,1)),rewrite(699(3),699(4))]. 829 (x v y) v x = x v y. [para(823(a,1),790(a,1,2))]. 866 x ^ (x v y') = x. [para(699(a,1),789(a,1,1)),rewrite(817(3),699(5))]. 871 x ^ (x v y) = x. [para(699(a,1),866(a,1,2,2))]. 887 (x ^ y)' = x' v y'. [para(699(a,1),817(a,1,1,1))]. 913 c2' v (c1' v c3') != c1' v (c2' v c3') # answer(A_SS). [back_rewrite(746),rewrite(887(6),887(14))]. 924 (x ^ y) v (y ^ ((z ^ (y v z')) v z')) = y. [para(823(a,1),753(a,1,1))]. 925 x ^ ((y ^ (x v y')) v y') = x. [para(753(a,1),797(a,1,1)),rewrite(790(7)),flip(a)]. 929 (((x ^ y) v y) ^ z) ^ y = ((x ^ y) v y) ^ z. [para(753(a,1),871(a,1,2))]. 933 (x ^ y) v x = x. [para(753(a,1),753(a,1,1,1)),rewrite(925(7),925(7),925(7),925(8))]. 934 (x ^ y) v y = y. [back_rewrite(924),rewrite(925(7))]. 935 (((x ^ y) v (y ^ z)) ^ u) v y = y. [back_rewrite(805),rewrite(925(10))]. 936 ((x ^ y) v (y ^ z)) v y = y. [back_rewrite(758),rewrite(925(9))]. 938 (x ^ y) ^ x = x ^ y. [back_rewrite(929),rewrite(934(2),934(4))]. 943 (x' v y') ^ y' = y'. [para(934(a,1),22(a,1,1)),rewrite(887(3)),flip(a)]. 945 x v (y ^ x) = x. [para(934(a,1),829(a,1,1)),rewrite(934(4))]. 951 ((x' v y') ^ (y' v z)) ^ (y' v ((z v (y' ^ z')) ^ z')) = y'. [para(757(a,1),22(a,1,1)),rewrite(22(6),887(3),887(7),699(7),887(13),22(13),887(12),699(10),22(10)),flip(a)]. 996 x ^ ((y ^ x) v (x ^ z)) = (y ^ x) v (x ^ z). [para(936(a,1),823(a,1,1))]. 997 ((x ^ (y v z)) v y) v (y v z) = y v z. [para(823(a,1),936(a,1,1,2))]. 998 x v ((y ^ x) v (x ^ z)) = x. [para(936(a,1),829(a,1,1)),rewrite(936(8))]. 1013 (x' v y) ^ y = y. [para(699(a,1),943(a,1,1,2)),rewrite(699(4),699(5))]. 1024 (x v y) ^ y = y. [para(699(a,1),1013(a,1,1,1))]. 1031 x v (y v x) = y v x. [para(1024(a,1),933(a,1,1))]. 1032 x ^ (y v x) = x. [para(1024(a,1),938(a,1,1)),rewrite(1024(4))]. 1034 ((x ^ (y v z)) v z) v (y v z) = y v z. [para(1024(a,1),936(a,1,1,2))]. 1037 x v ((y v (x ^ y')) ^ y') = x. [para(807(a,1),821(a,1)),flip(a)]. 1041 ((x' v y') ^ (y' v z)) ^ y' = y'. [back_rewrite(951),rewrite(1037(14))]. 1051 (x v y) v (y v ((x v y) ^ z)) = x v y. [para(1032(a,1),998(a,1,2,1))]. 1067 x v ((y' v (x ^ y)) ^ y) = x. [para(812(a,1),821(a,1)),flip(a)]. 1126 ((x' v (y ^ x)) ^ x) v y = y. [para(1067(a,1),1031(a,1,2)),rewrite(1067(10))]. 1142 (((x' ^ y') v x) ^ (x v y)) v x = x. [para(871(a,1),1126(a,1,1,1,2)),rewrite(22(2))]. 1146 (((x' ^ y') v y) ^ (x v y)) v y = y. [para(1032(a,1),1126(a,1,1,1,2)),rewrite(22(2))]. 1188 ((x ^ y) ^ z) v x = x. [para(933(a,1),935(a,1,1,1))]. 1200 (x ^ y) v (x v z) = x v z. [para(823(a,1),1188(a,1,1,1))]. 1204 (x ^ y) v (z v x) = z v x. [para(1024(a,1),1188(a,1,1,1))]. 1278 (x v y) ^ (x ^ z) = x ^ z. [para(1200(a,1),823(a,1,1))]. 1292 (x v y) ^ (y ^ z) = y ^ z. [para(1204(a,1),823(a,1,1))]. 1383 ((x v y) v z) ^ x = x. [para(823(a,1),1278(a,1,2)),rewrite(823(5))]. 1385 ((x v y) v z) ^ y = y. [para(1024(a,1),1278(a,1,2)),rewrite(1024(5))]. 1416 x ^ ((x v y) v z) = x. [para(1383(a,1),938(a,1,1)),rewrite(1383(6))]. 1449 (x v y) ^ (x v ((x v y) ^ z)) = x v ((x v y) ^ z). [para(871(a,1),996(a,1,2,1)),rewrite(871(7))]. 1489 x ^ ((y v x) v z) = x. [para(1385(a,1),938(a,1,1)),rewrite(1385(6))]. 1513 x ^ (y v (x v z)) = x. [para(1031(a,1),1416(a,1,2))]. 1565 x ^ (y v (z v x)) = x. [para(1031(a,1),1489(a,1,2))]. 1573 (x v y) v (y v x) = y v x. [para(1032(a,1),997(a,1,1,1))]. 1635 (x v y) v (y v (x v z)) = y v (x v z). [para(1513(a,1),997(a,1,1,1))]. 1641 (x v y) v (y v (z v x)) = y v (z v x). [para(1565(a,1),997(a,1,1,1))]. 1939 (x v y) v ((z v x) v y) = (z v x) v y. [para(1489(a,1),1034(a,1,1,1))]. 2291 x v y = y v x. [para(1573(a,1),829(a,1,1)),rewrite(1573(3),1573(4))]. 2499 x v ((x v (y' ^ x')) ^ (y v x)) = x. [back_rewrite(1146),rewrite(2291(4),2291(7))]. 2500 x v ((x v (x' ^ y')) ^ (x v y)) = x. [back_rewrite(1142),rewrite(2291(4),2291(7))]. 2515 x' ^ y' = y' ^ x'. [para(2291(a,1),22(a,1,1)),rewrite(22(2))]. 2536 ((x' v y) ^ (y v z)) ^ y = y. [para(699(a,1),1041(a,1,1,1,2)),rewrite(699(4),699(6),699(7))]. 2869 x' ^ y = y ^ x'. [para(699(a,1),2515(a,1,1)),rewrite(699(5)),flip(a)]. 2926 x ^ y = y ^ x. [para(699(a,1),2869(a,1,1)),rewrite(699(3))]. 2981 x ^ ((y' v x) ^ (x v z)) = x. [back_rewrite(2536),rewrite(2926(5))]. 2988 x v ((x v y) ^ (x v (x' ^ y'))) = x. [back_rewrite(2500),rewrite(2926(6))]. 2989 x v ((y v x) ^ (x v (y' ^ x'))) = x. [back_rewrite(2499),rewrite(2926(6))]. 4201 x ^ ((y v x) ^ (x v z)) = x. [para(699(a,1),2981(a,1,2,1,1))]. 4252 x v ((y v x) ^ (x v z)) = (y v x) ^ (x v z). [para(4201(a,1),945(a,1,2)),rewrite(2291(4))]. 4291 x ^ ((x v y) ^ (x v z)) = x. [para(2291(a,1),4201(a,1,2,1))]. 4307 (x v y) ^ (y v (x' ^ y')) = y. [back_rewrite(2989),rewrite(4252(7))]. 4371 x v ((x v y) ^ (x v z)) = (x v y) ^ (x v z). [para(4291(a,1),945(a,1,2)),rewrite(2291(4))]. 4406 (x v y) ^ (x v (x' ^ y')) = x. [back_rewrite(2988),rewrite(4371(7))]. 16351 x v (y v ((y v x) ^ z)) = y v x. [para(1449(a,1),1051(a,1,2,2)),rewrite(1635(6))]. 20070 x v (y v (x ^ z)) = y v x. [para(1292(a,1),16351(a,1,2,2))]. 20198 (x v y) v (z v y) = z v (x v y). [para(4307(a,1),20070(a,1,2,2))]. 20199 (x v y) v (z v x) = z v (x v y). [para(4406(a,1),20070(a,1,2,2))]. 20227 (x v y) v (y v z) = (x v y) v z. [back_rewrite(1939),rewrite(20198(4))]. 20264 x v (y v z) = z v (x v y). [back_rewrite(1641),rewrite(20227(4),20199(3))]. 21414 $F # answer(A_SS). [back_rewrite(913),rewrite(20264(8,R),2291(7)),xx(a)]. ============================== end of proof ========================== ============================== STATISTICS ============================ Given=649. Generated=306406. Kept=21401. proofs=3. Usable=349. Sos=11060. Demods=12552. Limbo=1150, Disabled=8849. Hints=0. Weight_deleted=2045. Literals_deleted=0. Forward_subsumed=275715. Back_subsumed=1327. Sos_limit_deleted=7242. Sos_displaced=0. Sos_removed=0. New_demodulators=21378 (5 lex), Back_demodulated=7513. Back_unit_deleted=0. Demod_attempts=4042027. Demod_rewrites=763177. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0. Megabytes=19.78. User_CPU=10.95, System_CPU=0.10, Wall_clock=11. ============================== end of statistics ===================== ============================== end of search ========================= THEOREM PROVED Exiting with 3 proofs. Process 3926 exit (max_proofs) Wed Nov 22 11:25:20 2006