============================== Prover9 =============================== Prover9 (32) version August-2006A, August 2006. Process 10729 was started by mccune on cleo.thornwood, Sat Aug 12 20:58:29 2006 The command was "/home/mccune/bin/prover9 -f oml6.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file oml6.in assign(max_weight,50). lex([v,c,^,f]). 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(Def_join). x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). c(x) = f(x,x) # label(Def_complement). end_of_list. formulas(goals). x v (x ^ y) = x # answer(B1). x v (c(x) ^ (x v y)) = x v y # answer(OM). x v (y v z) = y v (x v z) # answer(AJ). x ^ y = c(c(x) v c(y)) # answer(DM). f(x,y) = c(x) v c(y) # answer(DEF_SS). x v x = x # answer(idempotence_join). x ^ x = x # answer(idempotence_meet). c(c(x)) = x # answer(cc). y v x = x v y # answer(commutativity_join). y v x = x v y # answer(commutativity_meet). x v c(x) = y v c(y) # answer(1). x ^ c(x) = y ^ c(y) # answer(0). (x v y) v z = x v (y v z) # answer(assoc_join). (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet). end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 x v (x ^ y) = x # answer(B1). [goal]. 2 x v (c(x) ^ (x v y)) = x v y # answer(OM). [goal]. 3 x v (y v z) = y v (x v z) # answer(AJ). [goal]. 4 x ^ y = c(c(x) v c(y)) # answer(DM). [goal]. 5 f(x,y) = c(x) v c(y) # answer(DEF_SS). [goal]. 6 x v x = x # answer(idempotence_join). [goal]. 7 x ^ x = x # answer(idempotence_meet). [goal]. 8 c(c(x)) = x # answer(cc). [goal]. 9 y v x = x v y # answer(commutativity_join). [goal]. 10 y v x = x v y # answer(commutativity_meet). [goal]. 11 x v c(x) = y v c(y) # answer(1). [goal]. 12 x ^ c(x) = y ^ c(y) # answer(0). [goal]. 13 (x v y) v z = x v (y v z) # answer(assoc_join). [goal]. 14 (x ^ y) ^ z = x ^ (y ^ z) # answer(assoc_meet). [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(Def_join). [assumption]. x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. c(x) = f(x,x) # label(Def_complement). [assumption]. c1 v (c1 ^ c2) != c1 # answer(B1). [deny(1)]. c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM). [deny(2)]. c5 v (c6 v c7) != c6 v (c5 v c7) # answer(AJ). [deny(3)]. c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM). [deny(4)]. f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS). [deny(5)]. c12 v c12 != c12 # answer(idempotence_join). [deny(6)]. c13 ^ c13 != c13 # answer(idempotence_meet). [deny(7)]. c(c(c14)) != c14 # answer(cc). [deny(8)]. c16 v c15 != c15 v c16 # answer(commutativity_join). [deny(9)]. c18 v c17 != c17 v c18 # answer(commutativity_meet). [deny(10)]. c19 v c(c19) != c20 v c(c20) # answer(1). [deny(11)]. c21 ^ c(c21) != c22 ^ c(c22) # answer(0). [deny(12)]. (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join). [deny(13)]. (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet). [deny(14)]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= No predicates eliminated. ============================== end predicate elimination ============= Auto_denials: % assign(max_proofs, 14). % (Horn set with more than one neg. clause) Term ordering decisions: Relation symbol precedence: lex([ = ]). Function symbol precedence: lex([ c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, v, c, ^, f ]). Skipping inverse_order, because there is a lex command. Skipping unfold_eq, becaure there is a lex command. 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). 21 f(x,x) = c(x). [copy(20),flip(a)]. 22 c1 v (c1 ^ c2) != c1 # answer(B1). [deny(1)]. 23 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM). [deny(2)]. 25 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ). [copy(24),flip(a)]. 27 c8 ^ c9 != c(c(c8) v c(c9)) # answer(DM). [copy(26),flip(a)]. 28 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS). [deny(5)]. 29 c12 v c12 != c12 # answer(idempotence_join). [deny(6)]. 30 c13 ^ c13 != c13 # answer(idempotence_meet). [deny(7)]. 31 c(c(c14)) != c14 # answer(cc). [deny(8)]. 32 c16 v c15 != c15 v c16 # answer(commutativity_join). [deny(9)]. 33 c18 v c17 != c17 v c18 # answer(commutativity_meet). [deny(10)]. 35 c20 v c(c20) != c19 v c(c19) # answer(1). [copy(34),flip(a)]. 37 c22 ^ c(c22) != c21 ^ c(c21) # answer(0). [copy(36),flip(a)]. 38 (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join). [deny(13)]. 39 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet). [deny(14)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. end_of_list. formulas(demodulators). 21 f(x,x) = c(x). [copy(20),flip(a)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.00 seconds. given #1 (I,wt=6): 21 f(x,x) = c(x). [copy(20),flip(a)]. given #2 (I,wt=7): 22 c1 v (c1 ^ c2) != c1 # answer(B1). [deny(1)]. given #3 (I,wt=12): 23 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM). [deny(2)]. given #4 (I,wt=11): 25 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ). [copy(24),flip(a)]. given #5 (I,wt=10): 27 c8 ^ c9 != c(c(c8) v c(c9)) # answer(DM). [copy(26),flip(a)]. given #6 (I,wt=9): 28 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS). [deny(5)]. given #7 (I,wt=5): 29 c12 v c12 != c12 # answer(idempotence_join). [deny(6)]. given #8 (I,wt=5): 30 c13 ^ c13 != c13 # answer(idempotence_meet). [deny(7)]. given #9 (I,wt=5): 31 c(c(c14)) != c14 # answer(cc). [deny(8)]. given #10 (I,wt=7): 32 c16 v c15 != c15 v c16 # answer(commutativity_join). [deny(9)]. given #11 (I,wt=7): 33 c18 v c17 != c17 v c18 # answer(commutativity_meet). [deny(10)]. given #12 (I,wt=9): 35 c20 v c(c20) != c19 v c(c19) # answer(1). [copy(34),flip(a)]. given #13 (I,wt=9): 37 c22 ^ c(c22) != c21 ^ c(c21) # answer(0). [copy(36),flip(a)]. given #14 (I,wt=11): 38 (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join). [deny(13)]. given #15 (I,wt=11): 39 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet). [deny(14)]. given #16 (I,wt=8): 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. given #17 (I,wt=9): 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. given #18 (I,wt=22): 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. given #19 (T,wt=7): 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. given #20 (T,wt=7): 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. given #21 (A,wt=10): 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. given #22 (F,wt=5): 49 c13 v c13 != c13 # answer(idempotence_meet). [back_rewrite(44),rewrite(45(3))]. given #23 (F,wt=5): 51 c14 v c14 != c14 # answer(cc). [back_rewrite(31),rewrite(45(3))]. given #24 (T,wt=10): 68 c(x v x) = c(x) v c(x). [para(45(a,1),45(a,1,1))]. given #25 (T,wt=11): 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. given #26 (A,wt=12): 47 f(x ^ y,c(z)) = f(x,y) v z. [para(40(a,1),41(a,1,1))]. given #27 (F,wt=11): 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. given #28 (F,wt=12): 48 f(c(x),y ^ z) = x v f(y,z). [para(40(a,1),41(a,1,2))]. given #29 (T,wt=12): 64 f(x,y) v f(x,y) = c(x ^ y). [para(40(a,1),45(a,1,1)),flip(a)]. given #30 (T,wt=12): 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. given #31 (A,wt=21): 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. given #32 (F,wt=12): 73 c(x) ^ (y v y) = c(x v c(y)). [para(45(a,1),46(a,1,2))]. given #33 (F,wt=13): 70 c(f(x,y) v z) = (x ^ y) ^ c(z). [para(40(a,1),46(a,1,1)),flip(a)]. given #34 (T,wt=13): 71 c(x v f(y,z)) = c(x) ^ (y ^ z). [para(40(a,1),46(a,1,2)),flip(a)]. given #35 (T,wt=13): 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. given #36 (A,wt=21): 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. given #37 (F,wt=14): 75 f(x v x,y ^ z) = c(x) v f(y,z). [para(40(a,1),65(a,1,2))]. given #38 (F,wt=14): 80 f(x ^ y,z v z) = f(x,y) v c(z). [para(45(a,1),47(a,1,2))]. given #39 (T,wt=14): 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. given #40 (T,wt=15): 78 f(x ^ y,z ^ u) = f(x,y) v f(z,u). [para(40(a,1),47(a,1,2))]. given #41 (A,wt=18): 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. given #42 (F,wt=15): 94 c(c(x) v f(y,z)) = (x v x) ^ (y ^ z). [para(40(a,1),72(a,1,2)),flip(a)]. given #43 (F,wt=15): 108 c(f(x,y) v c(z)) = (x ^ y) ^ (z v z). [para(40(a,1),73(a,1,1)),flip(a)]. given #44 (T,wt=16): 88 f(c(x),y ^ z) v u = (x v f(y,z)) v u. [para(48(a,1),47(a,2,1)),rewrite(47(5))]. given #45 (T,wt=16): 109 c(f(x,y) v f(z,u)) = (x ^ y) ^ (z ^ u). [para(40(a,1),70(a,2,2))]. given #46 (A,wt=20): 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. given #47 (F,wt=16): 140 x v f(c(y),z ^ u) = x v (y v f(z,u)). [para(71(a,2),48(a,1,2)),rewrite(41(5)),flip(a)]. given #48 (F,wt=17): 87 f(c(x) v c(x),y ^ z) = (x v x) v f(y,z). [para(68(a,1),48(a,1,1))]. given #49 (T,wt=17): 89 f(c(x),(y ^ z) ^ c(u)) = x v (f(y,z) v u). [para(47(a,1),48(a,2,2))]. given #50 (T,wt=17): 90 f(c(x),c(y) ^ (z ^ u)) = x v (y v f(z,u)). [para(48(a,1),48(a,2,2))]. given #51 (A,wt=23): 57 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(z,f(c(y),z)),z)) = c(y). [para(42(a,1),40(a,1,1)),flip(a)]. given #52 (F,wt=17): 117 c(f(x,y) v z) v u = ((x ^ y) ^ c(z)) v u. [para(70(a,1),65(a,2,1)),rewrite(65(7))]. given #53 (F,wt=17): 119 x v c(f(y,z) v u) = x v ((y ^ z) ^ c(u)). [para(70(a,1),66(a,2,2)),rewrite(66(7))]. given #54 (T,wt=17): 136 c(x v f(y,z)) v u = (c(x) ^ (y ^ z)) v u. [para(71(a,1),65(a,2,1)),rewrite(65(7))]. given #55 (T,wt=17): 138 x v c(y v f(z,u)) = x v (c(y) ^ (z ^ u)). [para(71(a,1),66(a,2,2)),rewrite(66(7))]. given #56 (A,wt=31): 58 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(40(a,1),42(a,1,2,2,1,2,1))]. given #57 (F,wt=17): 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. given #58 (F,wt=17): 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. given #59 (T,wt=18): 111 c((f(x,y) v z) v u) = ((x ^ y) ^ c(z)) ^ c(u). [para(70(a,1),46(a,1,1)),flip(a)]. given #60 (T,wt=18): 112 c(x v (f(y,z) v u)) = c(x) ^ ((y ^ z) ^ c(u)). [para(70(a,1),46(a,1,2)),flip(a)]. given #61 (A,wt=26): 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. given #62 (F,wt=18): 115 c(f(x,y) v (z v z)) = (x ^ y) ^ (c(z) v c(z)). [para(68(a,1),70(a,2,2))]. given #63 (F,wt=18): 121 c((x v f(y,z)) v u) = (c(x) ^ (y ^ z)) ^ c(u). [para(48(a,1),70(a,1,1,1))]. given #64 (T,wt=18): 131 c(x v (y v f(z,u))) = c(x) ^ (c(y) ^ (z ^ u)). [para(71(a,1),46(a,1,2)),flip(a)]. given #65 (T,wt=18): 134 c((x v x) v f(y,z)) = (c(x) v c(x)) ^ (y ^ z). [para(68(a,1),71(a,2,1))]. given #66 (A,wt=24): 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. given #67 (F,wt=18): 148 c(f(c(x),y ^ z) v u) = c((x v f(y,z)) v u). [para(71(a,2),70(a,2,1)),rewrite(46(10))]. given #68 (F,wt=18): 151 c(x v f(c(y),z ^ u)) = c(x v (y v f(z,u))). [para(71(a,2),71(a,2,2)),rewrite(46(10))]. given #69 (T,wt=18): 165 f(x v x,y ^ z) v u = (c(x) v f(y,z)) v u. [para(75(a,1),47(a,2,1)),rewrite(47(5))]. given #70 (T,wt=18): 214 x v f(y v y,z ^ u) = x v (c(y) v f(z,u)). [para(94(a,2),48(a,1,2)),rewrite(41(6)),flip(a)]. given #71 (A,wt=37): 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. given #72 (F,wt=12): 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. given #73 (F,wt=14): 1631 c(x) ^ f(x v x,x) = c(x) v c(x). [para(1630(a,1),40(a,1,1)),rewrite(68(2)),flip(a)]. given #74 (T,wt=15): 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. ============================== PROOF ================================= % Proof 1 at 0.20 (+ 0.01) seconds: cc. % Length of proof is 17. % Level of proof is 6. % Maximum clause weight is 37. % Given clauses 74. 8 c(c(x)) = x # answer(cc). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 31 c(c(c14)) != c14 # answer(cc). [deny(8)]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 51 c14 v c14 != c14 # answer(cc). [back_rewrite(31),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1740 $F # answer(cc). [resolve(1739,a,51,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 2 at 0.20 (+ 0.01) seconds: idempotence_meet. % Length of proof is 22. % Level of proof is 6. % Maximum clause weight is 37. % Given clauses 74. 7 x ^ x = x # answer(idempotence_meet). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 30 c13 ^ c13 != c13 # answer(idempotence_meet). [deny(7)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 44 c(c(c13)) != c13 # answer(idempotence_meet). [back_rewrite(30),rewrite(43(3))]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 49 c13 v c13 != c13 # answer(idempotence_meet). [back_rewrite(44),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1741 $F # answer(idempotence_meet). [resolve(1739,a,49,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 3 at 0.20 (+ 0.01) seconds: idempotence_join. % Length of proof is 16. % Level of proof is 6. % Maximum clause weight is 37. % Given clauses 74. 6 x v x = x # answer(idempotence_join). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 29 c12 v c12 != c12 # answer(idempotence_join). [deny(6)]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1742 $F # answer(idempotence_join). [resolve(1739,a,29,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 4 at 0.28 (+ 0.01) seconds: DM. % Length of proof is 24. % Level of proof is 7. % Maximum clause weight is 37. % Given clauses 74. 4 x ^ y = c(c(x) v c(y)) # answer(DM). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 26 c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM). [deny(4)]. 27 c8 ^ c9 != c(c(c8) v c(c9)) # answer(DM). [copy(26),flip(a)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2375 $F # answer(DM). [resolve(2374,a,27,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 5 at 0.28 (+ 0.01) seconds: DEF_SS. % Length of proof is 19. % Level of proof is 7. % Maximum clause weight is 37. % Given clauses 74. 5 f(x,y) = c(x) v c(y) # answer(DEF_SS). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 28 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS). [deny(5)]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2385 $F # answer(DEF_SS). [resolve(2384,a,28,a)]. ============================== end of proof ========================== % Redundant proof: 2390 $F # answer(cc). [back_rewrite(51),rewrite(1739(3)),xx(a)]. % Redundant proof: 2391 $F # answer(idempotence_meet). [back_rewrite(49),rewrite(1739(3)),xx(a)]. % Redundant proof: 2393 $F # answer(idempotence_join). [back_rewrite(29),rewrite(1739(3)),xx(a)]. % Redundant proof: 2439 $F # answer(DM). [back_rewrite(27),rewrite(2374(3)),xx(a)]. % Redundant proof: 2472 $F # answer(DEF_SS). [back_rewrite(28),rewrite(2384(3)),xx(a)]. % Disable descendants: 28x 26x 27x 29x 30x 44x 49x 31x 51x given #75 (T,wt=5): 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. given #76 (A,wt=10): 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. given #77 (F,wt=10): 2441 c1 v c(c(c1) v c(c2)) != c1 # answer(B1). [back_rewrite(22),rewrite(2374(4))]. given #78 (F,wt=11): 2438 c(c(c22) v c22) != c(c(c21) v c21) # answer(0). [back_rewrite(37),rewrite(2374(4),2392(5),2374(9),2392(10))]. given #79 (T,wt=5): 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. given #80 (T,wt=9): 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. given #81 (A,wt=31): 2399 (c(x v y) v c(y v c(z))) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z))) = c(y). [back_rewrite(2304),rewrite(2384(3),2392(3),2374(4),2384(9),2384(12),2384(15),2384(18),2392(9),2384(19),2392(8))]. given #82 (F,wt=13): 2440 c3 v c(c3 v c(c3 v c4)) != c3 v c4 # answer(OM). [back_rewrite(23),rewrite(2374(7),2392(4))]. given #83 (F,wt=19): 2437 c((c(c26) v c(c27)) v c(c28)) != c(c(c26) v (c(c27) v c(c28))) # answer(assoc_meet). [back_rewrite(39),rewrite(2374(3),2374(8),2392(7),2374(13),2374(17),2392(18))]. given #84 (T,wt=16): 2462 x v c(c(x) v c(c(x v c(x)) v x)) = x. [back_rewrite(1743),rewrite(2384(3),2392(3),2384(5),2392(6),2384(6),2384(9),2392(2))]. given #85 (T,wt=18): 2448 c(x) v c(x v c(c(c(x) v x) v c(x))) = c(x). [back_rewrite(2140),rewrite(2384(4),2384(7),2392(2),2384(8))]. given #86 (A,wt=29): 2400 (c(c(x) v c(y)) v c(c(y) v z)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(2302),rewrite(2384(1),2374(6),2384(12),2392(11),2384(14),2392(15),2384(15),2384(18),2392(10))]. given #87 (F,wt=18): 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. given #88 (F,wt=20): 2470 c(x) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x). [back_rewrite(754),rewrite(2384(5),2392(3),2384(7),2392(8),2384(8),2392(2),2384(9))]. given #89 (T,wt=22): 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. given #90 (T,wt=10): 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. given #91 (A,wt=29): 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. given #92 (F,wt=9): 2488 c(c(x) v y) v x = x. [para(2392(a,1),2483(a,1,2)),rewrite(2392(6))]. given #93 (F,wt=9): 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. given #94 (T,wt=14): 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. given #95 (T,wt=12): 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. given #96 (A,wt=27): 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. given #97 (F,wt=11): 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. given #98 (F,wt=11): 2522 x v (c(x v c(x)) v x) = x. [back_rewrite(2462),rewrite(2517(7),2392(6))]. given #99 (T,wt=13): 2499 (c(x v y) v c(y)) v c(y) = c(y). [para(2392(a,1),2487(a,1,1,1,1,1))]. given #100 (T,wt=14): 2507 c(x) v (c(c(x) v x) v c(x)) = c(x). [back_rewrite(2448),rewrite(2502(8),2392(8))]. given #101 (A,wt=32): 2442 (c(c(x) v c(y)) v c(c(y) v c(c(y) v c(c(c(z) v c(y v c(z))) v c(z))))) v y = y. [back_rewrite(1711),rewrite(2384(1),2384(5),2392(5),2384(6),2384(9),2384(12),2384(15),2384(18))]. given #102 (F,wt=15): 2518 c(c(x) v x) v (c(x v c(x)) v x) = x. [back_rewrite(2514),rewrite(2517(10),2392(9))]. given #103 (F,wt=16): 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. given #104 (T,wt=11): 2535 (x v c(c(x) v x)) v x = x. [para(1739(a,1),2515(a,1,1,1,1)),rewrite(2392(2))]. given #105 (T,wt=11): 2539 c(x) v c(x v c(x)) = c(x). [para(2392(a,1),2535(a,1,1,2,1,1)),rewrite(2492(7))]. given #106 (A,wt=31): 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. given #107 (F,wt=9): 2543 x v c(c(x) v x) = x. [para(2392(a,1),2539(a,1,1)),rewrite(2392(3),2392(6))]. given #108 (F,wt=15): 2536 (c(x v c(y)) v c(c(y) v y)) v y = y. [para(2392(a,1),2515(a,1,1,1,1,1))]. given #109 (T,wt=15): 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. given #110 (T,wt=11): 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. given #111 (A,wt=33): 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. given #112 (F,wt=9): 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. given #113 (F,wt=10): 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. given #114 (T,wt=10): 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. given #115 (T,wt=9): 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. given #116 (A,wt=25): 2454 c(x v y) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z))) = c(y). [back_rewrite(1798),rewrite(2384(3),2384(6),2384(9),2384(12),2392(3),2384(13))]. given #117 (F,wt=10): 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. ============================== PROOF ================================= % Proof 6 at 0.47 (+ 0.01) seconds: B1. % Length of proof is 58. % Level of proof is 16. % Maximum clause weight is 37. % Given clauses 117. 1 x v (x ^ y) = x # answer(B1). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 22 c1 v (c1 ^ c2) != c1 # answer(B1). [deny(1)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2441 c1 v c(c(c1) v c(c2)) != c1 # answer(B1). [back_rewrite(22),rewrite(2374(4))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2615 x v c(c(x) v y) = x. [para(2392(a,1),2608(a,1,1)),rewrite(2392(6))]. 2616 $F # answer(B1). [resolve(2615,a,2441,a)]. ============================== end of proof ========================== % Redundant proof: 2621 $F # answer(B1). [back_rewrite(2441),rewrite(2615(8)),xx(a)]. % Disable descendants: 22x 2441x given #118 (F,wt=9): 2615 x v c(c(x) v y) = x. [para(2392(a,1),2608(a,1,1)),rewrite(2392(6))]. given #119 (T,wt=9): 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. given #120 (T,wt=9): 2619 (x v y) v y = x v y. [para(2603(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. given #121 (A,wt=32): 2469 c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(z v c(c(y) v z)) v z)) = c(y). [back_rewrite(929),rewrite(2384(3),2384(6),2384(13),2392(11),2384(15),2392(16),2384(16),2392(10),2384(17))]. given #122 (F,wt=9): 2622 x v c(y v c(x)) = x. [para(2611(a,1),2615(a,1,2,1))]. given #123 (F,wt=10): 2620 c(x) v c(y v x) = c(x). [para(2611(a,1),2608(a,1,2,1))]. given #124 (T,wt=12): 2597 c((c(x) v y) v c(z)) v x = x. [back_rewrite(2577),rewrite(2585(14))]. given #125 (T,wt=11): 2640 c((c(x) v y) v z) v x = x. [para(2392(a,1),2597(a,1,1,1,2))]. given #126 (A,wt=28): 2556 c(x) v c(c(y v c(x)) v c(c(x) v x)) = c(c(y v c(x)) v c(c(x) v x)). [para(2536(a,1),2483(a,1,1,1))]. given #127 (F,wt=11): 2657 c((x v c(y)) v z) v y = y. [para(2611(a,1),2640(a,1,1,1,1))]. given #128 (F,wt=11): 2658 c(x v (c(y) v z)) v y = y. [para(2611(a,1),2640(a,1,1,1))]. given #129 (T,wt=11): 2660 x v c((c(x) v y) v z) = x. [para(2640(a,1),2617(a,1,1)),rewrite(2640(10))]. given #130 (T,wt=11): 2672 c(x v (y v c(z))) v z = z. [para(2611(a,1),2657(a,1,1,1))]. given #131 (A,wt=23): 2569 (x v c(c(x v c(y)) v (x v c(y)))) v (x v c(y)) = x v c(y). [para(2559(a,1),2536(a,1,1,1))]. given #132 (F,wt=11): 2674 x v c((y v c(x)) v z) = x. [para(2657(a,1),2617(a,1,1)),rewrite(2657(10))]. given #133 (F,wt=11): 2684 x v c(y v (c(x) v z)) = x. [para(2658(a,1),2617(a,1,1)),rewrite(2658(10))]. given #134 (T,wt=11): 2705 x v c(y v (z v c(x))) = x. [para(2672(a,1),2617(a,1,1)),rewrite(2672(10))]. given #135 (T,wt=12): 2651 c((x v y) v z) v c(x) = c(x). [para(2392(a,1),2640(a,1,1,1,1,1))]. given #136 (A,wt=25): 2570 c(c(c(x v y) v c(y v c(y))) v y) = c(x v y) v c(y v c(y)). [para(2536(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(4),2392(9),2392(11),2392(13))]. given #137 (F,wt=12): 2670 c((x v y) v z) v c(y) = c(y). [para(2392(a,1),2657(a,1,1,1,1,2))]. given #138 (F,wt=12): 2677 c(x v (y v z)) v c(y) = c(y). [para(2392(a,1),2658(a,1,1,1,2,1))]. given #139 (T,wt=12): 2691 c(x) v c((x v y) v z) = c(x). [para(2392(a,1),2660(a,1,2,1,1,1))]. given #140 (T,wt=12): 2702 c(x v (y v z)) v c(z) = c(z). [para(2392(a,1),2672(a,1,1,1,2,2))]. given #141 (A,wt=16): 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. given #142 (F,wt=12): 2718 c(x) v c((y v x) v z) = c(x). [para(2392(a,1),2674(a,1,2,1,1,2))]. given #143 (F,wt=12): 2721 c(x) v c(y v (x v z)) = c(x). [para(2392(a,1),2684(a,1,2,1,2,1))]. given #144 (T,wt=12): 2733 c(x) v c(y v (z v x)) = c(x). [para(2392(a,1),2705(a,1,2,1,2,2))]. given #145 (T,wt=13): 2653 c(c(x) v y) v (x v z) = x v z. [para(2483(a,1),2640(a,1,1,1,1))]. given #146 (A,wt=15): 2591 (c(x v c(y)) v c(c(y) v z)) v y = y. [para(2543(a,1),2453(a,1,1,1)),rewrite(2392(9),2585(16))]. given #147 (F,wt=13): 2656 c(c(x) v y) v (z v x) = z v x. [para(2603(a,1),2640(a,1,1,1,1))]. given #148 (F,wt=13): 2679 c(x v c(y)) v (y v z) = y v z. [para(2483(a,1),2658(a,1,1,1,2))]. given #149 (T,wt=13): 2682 c(x v c(y)) v (z v y) = z v y. [para(2603(a,1),2658(a,1,1,1,2))]. given #150 (T,wt=13): 2692 (x v y) v c(c(x) v z) = x v y. [para(2483(a,1),2660(a,1,2,1,1))]. given #151 (A,wt=22): 2598 c(c(c(x v c(y v z)) v y) v c(u)) v (y v z) = y v z. [back_rewrite(2576),rewrite(2585(23))]. given #152 (F,wt=13): 2695 (x v y) v c(c(y) v z) = x v y. [para(2603(a,1),2660(a,1,2,1,1))]. given #153 (F,wt=13): 2722 (x v y) v c(z v c(x)) = x v y. [para(2483(a,1),2684(a,1,2,1,2))]. given #154 (T,wt=13): 2725 (x v y) v c(z v c(y)) = x v y. [para(2603(a,1),2684(a,1,2,1,2))]. given #155 (T,wt=13): 2735 x v ((x v y) v z) = (x v y) v z. [para(2651(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. given #156 (A,wt=19): 2599 c(c(c(x v c(y)) v c(c(y) v z)) v u) v y = y. [back_rewrite(2573),rewrite(2585(19))]. given #157 (F,wt=13): 2736 ((x v y) v z) v x = (x v y) v z. [para(2651(a,1),2608(a,1,2,1)),rewrite(2392(4),2392(4),2392(7))]. given #158 (F,wt=13): 2755 x v ((y v x) v z) = (y v x) v z. [para(2670(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. given #159 (T,wt=13): 2756 ((x v y) v z) v y = (x v y) v z. [para(2670(a,1),2608(a,1,2,1)),rewrite(2392(4),2392(4),2392(7))]. given #160 (T,wt=13): 2761 x v (y v (x v z)) = y v (x v z). [para(2677(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. given #161 (A,wt=29): 2624 x v (c(c(y v x) v c(x v z)) v c(u)) = c(c(y v x) v c(x v z)) v c(u). [para(2469(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(10),2392(19))]. given #162 (F,wt=13): 2762 (x v (y v z)) v y = x v (y v z). [para(2677(a,1),2608(a,1,2,1)),rewrite(2392(4),2392(4),2392(7))]. given #163 (F,wt=13): 2768 x v (y v (z v x)) = y v (z v x). [para(2702(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. given #164 (T,wt=13): 2769 (x v (y v z)) v z = x v (y v z). [para(2702(a,1),2608(a,1,2,1)),rewrite(2392(4),2392(4),2392(7))]. given #165 (T,wt=13): 2794 c(((c(x) v y) v z) v u) v x = x. [para(2640(a,1),2653(a,1,2)),rewrite(2392(5),2640(11))]. given #166 (A,wt=17): 2628 c(x v c(c(y v c(c(x) v y)) v y)) = c(x). [para(2469(a,1),2596(a,1)),flip(a)]. given #167 (F,wt=13): 2796 c(((x v c(y)) v z) v u) v y = y. [para(2657(a,1),2653(a,1,2)),rewrite(2392(5),2657(11))]. given #168 (F,wt=13): 2799 c((x v (c(y) v z)) v u) v y = y. [para(2658(a,1),2653(a,1,2)),rewrite(2392(5),2658(11))]. given #169 (T,wt=13): 2802 c((x v (y v c(z))) v u) v z = z. [para(2672(a,1),2653(a,1,2)),rewrite(2392(5),2672(11))]. given #170 (T,wt=13): 2860 c(x v ((c(y) v z) v u)) v y = y. [para(2640(a,1),2679(a,1,2)),rewrite(2392(5),2640(11))]. given #171 (A,wt=20): 2631 c(c(c(x v y) v c(z v y)) v c(u)) v c(y) = c(y). [para(2611(a,1),2469(a,1,1,1,1,1,2,1)),rewrite(2628(21))]. given #172 (F,wt=13): 2861 c(x v ((y v c(z)) v u)) v z = z. [para(2657(a,1),2679(a,1,2)),rewrite(2392(5),2657(11))]. given #173 (F,wt=13): 2863 c(x v (y v (c(z) v u))) v z = z. [para(2658(a,1),2679(a,1,2)),rewrite(2392(5),2658(11))]. given #174 (T,wt=13): 2865 c(x v (y v (z v c(u)))) v u = u. [para(2672(a,1),2679(a,1,2)),rewrite(2392(5),2672(11))]. given #175 (T,wt=13): 2884 x v c(((c(x) v y) v z) v u) = x. [para(2640(a,1),2692(a,1,1)),rewrite(2392(5),2640(11))]. given #176 (A,wt=29): 2632 (c(c(x v y) v c(y v z)) v c(u)) v y = c(c(x v y) v c(y v z)) v c(u). [para(2469(a,1),2608(a,1,2,1)),rewrite(2392(10),2392(10),2392(19))]. given #177 (F,wt=13): 2886 x v c(((y v c(x)) v z) v u) = x. [para(2657(a,1),2692(a,1,1)),rewrite(2392(5),2657(11))]. given #178 (F,wt=13): 2888 x v c((y v (c(x) v z)) v u) = x. [para(2658(a,1),2692(a,1,1)),rewrite(2392(5),2658(11))]. given #179 (T,wt=13): 2890 x v c((y v (z v c(x))) v u) = x. [para(2672(a,1),2692(a,1,1)),rewrite(2392(5),2672(11))]. given #180 (T,wt=13): 2952 x v c(y v ((c(x) v z) v u)) = x. [para(2640(a,1),2722(a,1,1)),rewrite(2392(5),2640(11))]. given #181 (A,wt=15): 2634 (c(x v y) v c(y v z)) v c(y) = c(y). [para(2608(a,1),2469(a,1,1,1)),rewrite(2392(7),2628(14))]. given #182 (F,wt=13): 2953 x v c(y v ((z v c(x)) v u)) = x. [para(2657(a,1),2722(a,1,1)),rewrite(2392(5),2657(11))]. given #183 (F,wt=13): 2954 x v c(y v (z v (c(x) v u))) = x. [para(2658(a,1),2722(a,1,1)),rewrite(2392(5),2658(11))]. given #184 (T,wt=13): 2955 x v c(y v (z v (u v c(x)))) = x. [para(2672(a,1),2722(a,1,1)),rewrite(2392(5),2672(11))]. given #185 (T,wt=13): 3155 x v c(c(x v y) v (x v y)) = x. [back_rewrite(2742),rewrite(3150(7),2608(4),2392(2)),flip(a)]. given #186 (A,wt=20): 2637 c(c(c(x v y) v c(x v z)) v c(u)) v c(x) = c(x). [para(2617(a,1),2469(a,1,1,1,1,1,1,1)),rewrite(2628(18))]. given #187 (F,wt=13): 3156 x v c(c(y v x) v (y v x)) = x. [back_rewrite(2746),rewrite(3151(7),2620(4),2392(2)),flip(a)]. given #188 (F,wt=13): 3583 c(c(x v y) v (x v y)) v x = x. [para(3155(a,1),2611(a,1,2)),rewrite(3155(12))]. given #189 (T,wt=9): 3766 c(c(x) v x) v y = y. [back_rewrite(3754),rewrite(3764(7))]. given #190 (T,wt=9): 3772 x v c(c(y) v y) = x. [back_rewrite(3619),rewrite(3764(7))]. ============================== PROOF ================================= % Proof 7 at 0.70 (+ 0.01) seconds: 0. % Length of proof is 108. % Level of proof is 25. % Maximum clause weight is 37. % Given clauses 190. 12 x ^ c(x) = y ^ c(y) # answer(0). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 36 c21 ^ c(c21) != c22 ^ c(c22) # answer(0). [deny(12)]. 37 c22 ^ c(c22) != c21 ^ c(c21) # answer(0). [copy(36),flip(a)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 929 f(f(f(x v y,y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z)))) = c(y). [para(41(a,1),59(a,1,1,1,2)),rewrite(65(9))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1263 f(f(f(x v c(y),c(y) v z),u),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y. [para(66(a,1),61(a,1,1,1,1)),rewrite(65(5))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1648 f(f(x,c(y)) ^ (y v y),f(c(y),f(f(f(y v y,y),f(y v y,f(y v y,y))),f(y v y,y)))) = c(y). [para(1630(a,1),55(a,1,1,2)),rewrite(45(9))]. 1649 f(f(x,y) ^ f(y,f(y v y,y)),f(y,f(f(f(y v y,y),y v y),f(y v y,y)))) = y. [para(1630(a,1),55(a,1,2,2,1,2))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1785 f(f(x,y) ^ f(y,c(y)),f(y,f(f(c(y),y),c(y)))) = y. [back_rewrite(1649),rewrite(1739(2),21(2),1739(5),21(5),1739(6),1739(7),21(7))]. 1786 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y). [back_rewrite(1648),rewrite(1739(3),1739(5),21(5),1739(6),1739(6),21(6),1739(9),21(9))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 1958 f(f(f(x v c(y),c(y) v z),u),f(y,f(f(c(z),y v z),c(z)))) = y. [back_rewrite(1263),rewrite(1739(7),1739(8),1739(14))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2411 (c(c(x) v y) v c(y)) v c(y v c(c(y v c(c(y) v y)) v y)) = c(y). [back_rewrite(1786),rewrite(2384(2),2392(3),2374(3),2384(10),2392(11),2384(11),2392(9),2384(13),2392(14),2384(14),2392(8),2384(15),2392(7))]. 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. 2438 c(c(c22) v c22) != c(c(c21) v c21) # answer(0). [back_rewrite(37),rewrite(2374(4),2392(5),2374(9),2392(10))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2469 c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(z v c(c(y) v z)) v z)) = c(y). [back_rewrite(929),rewrite(2384(3),2384(6),2384(13),2392(11),2384(15),2392(16),2384(16),2392(10),2384(17))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. 2512 (c(x v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [para(2392(a,1),2412(a,1,1,1,1,1))]. 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. 2536 (c(x v c(y)) v c(c(y) v y)) v y = y. [para(2392(a,1),2515(a,1,1,1,1,1))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2568 c(c(c(x v y) v c(y)) v y) = c(x v y) v c(y). [para(2508(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(7),2392(9))]. 2570 c(c(c(x v y) v c(y v c(y))) v y) = c(x v y) v c(y v c(y)). [para(2536(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(4),2392(9),2392(11),2392(13))]. 2577 c((c(x) v y) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2483(a,1),2453(a,1,1,1,1,1)),rewrite(2392(4))]. 2578 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [para(2483(a,1),2453(a,1,1,1)),rewrite(2392(4))]. 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. 2597 c((c(x) v y) v c(z)) v x = x. [back_rewrite(2577),rewrite(2585(14))]. 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. 2628 c(x v c(c(y v c(c(x) v y)) v y)) = c(x). [para(2469(a,1),2596(a,1)),flip(a)]. 2640 c((c(x) v y) v z) v x = x. [para(2392(a,1),2597(a,1,1,1,2))]. 2653 c(c(x) v y) v (x v z) = x v z. [para(2483(a,1),2640(a,1,1,1,1))]. 2657 c((x v c(y)) v z) v y = y. [para(2611(a,1),2640(a,1,1,1,1))]. 2660 x v c((c(x) v y) v z) = x. [para(2640(a,1),2617(a,1,1)),rewrite(2640(10))]. 2672 c(x v (y v c(z))) v z = z. [para(2611(a,1),2657(a,1,1,1))]. 2692 (x v y) v c(c(x) v z) = x v y. [para(2483(a,1),2660(a,1,2,1,1))]. 2702 c(x v (y v z)) v c(z) = c(z). [para(2392(a,1),2672(a,1,1,1,2,2))]. 2742 c(c(x v c(c(x v y) v (x v y))) v c(x v y)) = x v c(c(x v y) v (x v y)). [para(2608(a,1),2570(a,1,1,1,1,1,1)),rewrite(2392(2),2392(5),2608(15),2392(13),2392(16))]. 2768 x v (y v (z v x)) = y v (z v x). [para(2702(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. 3150 c(x v c(c(x v y) v (x v y))) = c(x). [para(2692(a,1),2628(a,1,1,2,1,1,1))]. 3155 x v c(c(x v y) v (x v y)) = x. [back_rewrite(2742),rewrite(3150(7),2608(4),2392(2)),flip(a)]. 3583 c(c(x v y) v (x v y)) v x = x. [para(3155(a,1),2611(a,1,2)),rewrite(3155(12))]. 3597 c(c(x) v y) v c(c(x v z) v (x v z)) = c(c(x) v y). [para(2653(a,1),3155(a,1,2,1,1,1)),rewrite(2653(10))]. 3619 x v c(c(y v (z v x)) v (y v (z v x))) = x. [para(2768(a,1),3155(a,1,2,1,1,1)),rewrite(2768(6))]. 3754 c(c(x v (y v z)) v (x v (y v z))) v z = z. [para(2768(a,1),3583(a,1,1,1,1,1)),rewrite(2768(6))]. 3764 c(c(x v y) v (x v y)) = c(c(x) v x). [para(3583(a,1),3583(a,1,1,1,1,1)),rewrite(3583(7),3597(9)),flip(a)]. 3766 c(c(x) v x) v y = y. [back_rewrite(3754),rewrite(3764(7))]. 3772 x v c(c(y) v y) = x. [back_rewrite(3619),rewrite(3764(7))]. 3800 c(c(x) v x) = c(c(y) v y). [para(3772(a,1),3766(a,1))]. 3801 $F # answer(0). [resolve(3800,a,2438,a)]. ============================== end of proof ========================== % Disable descendants: 36x 37x 2438 given #191 (A,wt=19): 2639 c(c(c(x v y) v c(y v z)) v u) v c(y) = c(y). [back_rewrite(2623),rewrite(2628(17))]. given #192 (F,wt=9): 3777 c(x v c(x)) v y = y. [para(2392(a,1),3766(a,1,1,1,1))]. given #193 (F,wt=9): 3799 x v c(y v c(y)) = x. [para(2392(a,1),3772(a,1,2,1,1))]. given #194 (T,wt=11): 3800 c(c(x) v x) = c(c(y) v y). [para(3772(a,1),3766(a,1))]. given #195 (T,wt=9): 3863 c(x) v x = c(y) v y. [para(3800(a,1),2392(a,1,1)),rewrite(2392(4))]. given #196 (A,wt=14): 2654 c(x v y) v (c(x) v z) = c(x) v z. [para(2488(a,1),2640(a,1,1,1,1))]. given #197 (F,wt=9): 3864 c(x) v x = y v c(y). [para(2392(a,1),3863(a,1,1)),flip(a)]. ============================== PROOF ================================= % Proof 8 at 0.72 (+ 0.01) seconds: 1. % Length of proof is 110. % Level of proof is 28. % Maximum clause weight is 37. % Given clauses 197. 11 x v c(x) = y v c(y) # answer(1). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 34 c19 v c(c19) != c20 v c(c20) # answer(1). [deny(11)]. 35 c20 v c(c20) != c19 v c(c19) # answer(1). [copy(34),flip(a)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 929 f(f(f(x v y,y v z),u),f(c(y),f(f(c(z),c(y) v z),c(z)))) = c(y). [para(41(a,1),59(a,1,1,1,2)),rewrite(65(9))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1263 f(f(f(x v c(y),c(y) v z),u),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y. [para(66(a,1),61(a,1,1,1,1)),rewrite(65(5))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1648 f(f(x,c(y)) ^ (y v y),f(c(y),f(f(f(y v y,y),f(y v y,f(y v y,y))),f(y v y,y)))) = c(y). [para(1630(a,1),55(a,1,1,2)),rewrite(45(9))]. 1649 f(f(x,y) ^ f(y,f(y v y,y)),f(y,f(f(f(y v y,y),y v y),f(y v y,y)))) = y. [para(1630(a,1),55(a,1,2,2,1,2))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1785 f(f(x,y) ^ f(y,c(y)),f(y,f(f(c(y),y),c(y)))) = y. [back_rewrite(1649),rewrite(1739(2),21(2),1739(5),21(5),1739(6),1739(7),21(7))]. 1786 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y). [back_rewrite(1648),rewrite(1739(3),1739(5),21(5),1739(6),1739(6),21(6),1739(9),21(9))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 1958 f(f(f(x v c(y),c(y) v z),u),f(y,f(f(c(z),y v z),c(z)))) = y. [back_rewrite(1263),rewrite(1739(7),1739(8),1739(14))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2411 (c(c(x) v y) v c(y)) v c(y v c(c(y v c(c(y) v y)) v y)) = c(y). [back_rewrite(1786),rewrite(2384(2),2392(3),2374(3),2384(10),2392(11),2384(11),2392(9),2384(13),2392(14),2384(14),2392(8),2384(15),2392(7))]. 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2469 c(c(c(x v y) v c(y v z)) v c(u)) v c(y v c(c(z v c(c(y) v z)) v z)) = c(y). [back_rewrite(929),rewrite(2384(3),2384(6),2384(13),2392(11),2384(15),2392(16),2384(16),2392(10),2384(17))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. 2512 (c(x v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [para(2392(a,1),2412(a,1,1,1,1,1))]. 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. 2536 (c(x v c(y)) v c(c(y) v y)) v y = y. [para(2392(a,1),2515(a,1,1,1,1,1))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2568 c(c(c(x v y) v c(y)) v y) = c(x v y) v c(y). [para(2508(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(7),2392(9))]. 2570 c(c(c(x v y) v c(y v c(y))) v y) = c(x v y) v c(y v c(y)). [para(2536(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(4),2392(9),2392(11),2392(13))]. 2577 c((c(x) v y) v c(z)) v c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2483(a,1),2453(a,1,1,1,1,1)),rewrite(2392(4))]. 2578 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [para(2483(a,1),2453(a,1,1,1)),rewrite(2392(4))]. 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. 2597 c((c(x) v y) v c(z)) v x = x. [back_rewrite(2577),rewrite(2585(14))]. 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. 2628 c(x v c(c(y v c(c(x) v y)) v y)) = c(x). [para(2469(a,1),2596(a,1)),flip(a)]. 2640 c((c(x) v y) v z) v x = x. [para(2392(a,1),2597(a,1,1,1,2))]. 2653 c(c(x) v y) v (x v z) = x v z. [para(2483(a,1),2640(a,1,1,1,1))]. 2657 c((x v c(y)) v z) v y = y. [para(2611(a,1),2640(a,1,1,1,1))]. 2660 x v c((c(x) v y) v z) = x. [para(2640(a,1),2617(a,1,1)),rewrite(2640(10))]. 2672 c(x v (y v c(z))) v z = z. [para(2611(a,1),2657(a,1,1,1))]. 2692 (x v y) v c(c(x) v z) = x v y. [para(2483(a,1),2660(a,1,2,1,1))]. 2702 c(x v (y v z)) v c(z) = c(z). [para(2392(a,1),2672(a,1,1,1,2,2))]. 2742 c(c(x v c(c(x v y) v (x v y))) v c(x v y)) = x v c(c(x v y) v (x v y)). [para(2608(a,1),2570(a,1,1,1,1,1,1)),rewrite(2392(2),2392(5),2608(15),2392(13),2392(16))]. 2768 x v (y v (z v x)) = y v (z v x). [para(2702(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(4),2392(7))]. 3150 c(x v c(c(x v y) v (x v y))) = c(x). [para(2692(a,1),2628(a,1,1,2,1,1,1))]. 3155 x v c(c(x v y) v (x v y)) = x. [back_rewrite(2742),rewrite(3150(7),2608(4),2392(2)),flip(a)]. 3583 c(c(x v y) v (x v y)) v x = x. [para(3155(a,1),2611(a,1,2)),rewrite(3155(12))]. 3597 c(c(x) v y) v c(c(x v z) v (x v z)) = c(c(x) v y). [para(2653(a,1),3155(a,1,2,1,1,1)),rewrite(2653(10))]. 3619 x v c(c(y v (z v x)) v (y v (z v x))) = x. [para(2768(a,1),3155(a,1,2,1,1,1)),rewrite(2768(6))]. 3754 c(c(x v (y v z)) v (x v (y v z))) v z = z. [para(2768(a,1),3583(a,1,1,1,1,1)),rewrite(2768(6))]. 3764 c(c(x v y) v (x v y)) = c(c(x) v x). [para(3583(a,1),3583(a,1,1,1,1,1)),rewrite(3583(7),3597(9)),flip(a)]. 3766 c(c(x) v x) v y = y. [back_rewrite(3754),rewrite(3764(7))]. 3772 x v c(c(y) v y) = x. [back_rewrite(3619),rewrite(3764(7))]. 3800 c(c(x) v x) = c(c(y) v y). [para(3772(a,1),3766(a,1))]. 3863 c(x) v x = c(y) v y. [para(3800(a,1),2392(a,1,1)),rewrite(2392(4))]. 3864 c(x) v x = y v c(y). [para(2392(a,1),3863(a,1,1)),flip(a)]. 3879 c(x) v x != c19 v c(c19) # answer(1). [para(3864(a,2),35(a,1))]. 3880 $F # answer(1). [resolve(3879,a,3864,a)]. ============================== end of proof ========================== % Redundant proof: 3881 $F # answer(1). [resolve(3879,a,3840,a)]. % Redundant proof: 3882 $F # answer(1). [resolve(3879,a,3777,a)]. % Redundant proof: 3883 $F # answer(1). [resolve(3879,a,2679,a)]. % Redundant proof: 3884 $F # answer(1). [resolve(3879,a,2655,a)]. % Redundant proof: 3886 $F # answer(1). [resolve(3885,a,3864,a)]. % Redundant proof: 3887 $F # answer(1). [resolve(3885,a,3840,a)]. % Redundant proof: 3888 $F # answer(1). [resolve(3885,a,3777,a)]. % Redundant proof: 3889 $F # answer(1). [resolve(3885,a,2679,a)]. % Redundant proof: 3890 $F # answer(1). [resolve(3885,a,2655,a)]. % Redundant proof: 3892 $F # answer(1). [resolve(3891,a,35,a)]. % Disable descendants: 34x 35 3879 3885 given #198 (F,wt=9): 3891 x v c(x) = y v c(y). [para(2392(a,1),3864(a,1,1))]. given #199 (T,wt=11): 3861 c(c(x) v x) = c(y v c(y)). [para(3777(a,1),3772(a,1))]. given #200 (T,wt=11): 3862 c(x v c(x)) = c(y v c(y)). [para(3799(a,1),3777(a,1))]. given #201 (A,wt=14): 2655 c(x v y) v (z v c(x)) = z v c(x). [para(2596(a,1),2640(a,1,1,1,1))]. given #202 (F,wt=11): 3865 c(x) v x = x v (c(y) v y). [para(3863(a,1),2611(a,1,2)),flip(a)]. given #203 (F,wt=11): 3895 (c(x) v x) v y = y v c(y). [para(3864(a,2),2617(a,1,1))]. given #204 (T,wt=11): 3915 x v c(x) = x v (y v c(y)). [para(3891(a,1),2489(a,1,2)),flip(a)]. given #205 (T,wt=11): 3916 (x v c(x)) v y = y v c(y). [para(3891(a,1),2617(a,1,1))]. given #206 (A,wt=18): 2661 c(x v y) v ((c(x) v z) v u) = (c(x) v z) v u. [para(2640(a,1),2640(a,1,1,1,1))]. given #207 (F,wt=11): 3950 c(x) v x = (y v c(y)) v z. [back_rewrite(3923),rewrite(3933(7)),flip(a)]. given #208 (F,wt=11): 3954 x v (c(y) v y) = c(y) v y. [para(3895(a,2),2695(a,1)),rewrite(3932(5))]. given #209 (T,wt=11): 3966 (c(x) v x) v y = c(x) v x. [back_rewrite(3939),rewrite(3954(6),3954(5)),flip(a)]. given #210 (T,wt=11): 3988 x v (y v c(y)) = y v c(y). [para(3916(a,2),2722(a,1)),rewrite(3972(5))]. given #211 (A,wt=18): 2675 c(x v y) v ((z v c(x)) v u) = (z v c(x)) v u. [para(2657(a,1),2640(a,1,1,1,1))]. given #212 (F,wt=11): 3994 (x v c(x)) v y = z v c(z). [para(3916(a,1),2736(a,2,1)),rewrite(3991(4),1739(5)),flip(a)]. given #213 (F,wt=13): 3842 c((x v c(x)) v y) = c(x v c(x)). [para(3777(a,1),2608(a,1))]. given #214 (T,wt=13): 3933 (x v y) v c(x v y) = c(x) v x. [para(3865(a,2),2653(a,1)),rewrite(2392(2),2392(3),2392(3))]. given #215 (T,wt=13): 3991 ((x v c(x)) v y) v z = x v c(x). [para(3916(a,1),2736(a,1,1,1)),rewrite(3988(6)),flip(a)]. given #216 (A,wt=14): 2680 c(x v y) v (c(y) v z) = c(y) v z. [para(2488(a,1),2658(a,1,1,1,2))]. given #217 (F,wt=13): 3996 x v ((y v c(y)) v z) = y v c(y). [para(3916(a,1),2762(a,1,1,2)),rewrite(3988(3),3988(5)),flip(a)]. given #218 (F,wt=13): 4032 (x v c(x)) v y = (z v c(z)) v u. [para(3950(a,1),3950(a,1))]. given #219 (T,wt=14): 2681 c(x v y) v (z v c(y)) = z v c(y). [para(2596(a,1),2658(a,1,1,1,2))]. given #220 (T,wt=14): 2693 (c(x) v y) v c(x v z) = c(x) v y. [para(2488(a,1),2660(a,1,2,1,1))]. given #221 (A,wt=18): 2685 c(x v y) v (z v (c(x) v u)) = z v (c(x) v u). [para(2658(a,1),2640(a,1,1,1,1))]. given #222 (F,wt=11): 4103 c(x v (c(x) v y)) v z = z. [para(2685(a,1),3766(a,1,1,1))]. given #223 (F,wt=11): 4104 x v c(y v (c(y) v z)) = x. [para(2685(a,1),3772(a,1,2,1))]. given #224 (T,wt=11): 4108 c(x) v x = y v (c(y) v z). [para(2685(a,1),3863(a,1)),flip(a)]. given #225 (T,wt=11): 4110 x v c(x) = y v (c(y) v z). [para(2685(a,1),3864(a,1)),flip(a)]. given #226 (A,wt=18): 2686 c(x v y) v ((c(y) v z) v u) = (c(y) v z) v u. [para(2640(a,1),2658(a,1,1,1,2))]. given #227 (F,wt=11): 4123 c(c(x) v (x v y)) v z = z. [para(2392(a,1),4103(a,1,1,1,2,1))]. given #228 (F,wt=11): 4124 c((x v y) v c(x)) v z = z. [para(2483(a,1),4103(a,1,1,1,2))]. given #229 (T,wt=11): 4125 c((c(x) v y) v x) v z = z. [para(2488(a,1),4103(a,1,1,1,2))]. given #230 (T,wt=11): 4126 c((x v c(y)) v y) v z = z. [para(2596(a,1),4103(a,1,1,1,2))]. given #231 (A,wt=18): 2688 c(x v y) v ((z v c(y)) v u) = (z v c(y)) v u. [para(2657(a,1),2658(a,1,1,1,2))]. given #232 (F,wt=11): 4127 c((x v y) v c(y)) v z = z. [para(2603(a,1),4103(a,1,1,1,2))]. given #233 (F,wt=11): 4128 c(x v (y v c(x))) v z = z. [para(2611(a,1),4103(a,1,1,1,2))]. given #234 (T,wt=11): 4146 c(c(x) v (y v x)) v z = z. [para(2768(a,1),4103(a,1,1,1))]. given #235 (T,wt=11): 4163 x v c(c(y) v (y v z)) = x. [para(2392(a,1),4104(a,1,2,1,2,1))]. given #236 (A,wt=18): 2689 c(x v y) v (z v (c(y) v u)) = z v (c(y) v u). [para(2658(a,1),2658(a,1,1,1,2))]. given #237 (F,wt=11): 4164 x v c((y v z) v c(y)) = x. [para(2483(a,1),4104(a,1,2,1,2))]. given #238 (F,wt=11): 4165 x v c((c(y) v z) v y) = x. [para(2488(a,1),4104(a,1,2,1,2))]. given #239 (T,wt=11): 4166 x v c((y v c(z)) v z) = x. [para(2596(a,1),4104(a,1,2,1,2))]. given #240 (T,wt=11): 4167 x v c((y v z) v c(z)) = x. [para(2603(a,1),4104(a,1,2,1,2))]. given #241 (A,wt=14): 2694 (x v c(y)) v c(y v z) = x v c(y). [para(2596(a,1),2660(a,1,2,1,1))]. given #242 (F,wt=11): 4168 x v c(y v (z v c(y))) = x. [para(2611(a,1),4104(a,1,2,1,2))]. given #243 (F,wt=11): 4186 x v c(c(y) v (z v y)) = x. [para(2768(a,1),4104(a,1,2,1))]. given #244 (T,wt=11): 4204 c(x) v (x v y) = c(z) v z. [para(2392(a,1),4108(a,2,2,1)),flip(a)]. given #245 (T,wt=11): 4205 c(x) v x = (y v z) v c(y). [para(2483(a,1),4108(a,2,2))]. given #246 (A,wt=18): 2696 ((c(x) v y) v z) v c(x v u) = (c(x) v y) v z. [para(2640(a,1),2660(a,1,2,1,1))]. given #247 (F,wt=11): 4206 c(x) v x = (c(y) v z) v y. [para(2488(a,1),4108(a,2,2))]. given #248 (F,wt=11): 4207 c(x) v x = (y v c(z)) v z. [para(2596(a,1),4108(a,2,2))]. given #249 (T,wt=11): 4208 c(x) v x = (y v z) v c(z). [para(2603(a,1),4108(a,2,2))]. given #250 (T,wt=11): 4209 c(x) v x = y v (z v c(y)). [para(2611(a,1),4108(a,2,2))]. given #251 (A,wt=18): 2699 ((x v c(y)) v z) v c(y v u) = (x v c(y)) v z. [para(2657(a,1),2660(a,1,2,1,1))]. given #252 (F,wt=11): 4226 c(x) v (y v x) = c(z) v z. [para(4108(a,2),2768(a,1)),flip(a)]. given #253 (F,wt=11): 4247 c(x) v (x v y) = z v c(z). [para(2392(a,1),4110(a,2,2,1)),flip(a)]. given #254 (T,wt=11): 4248 (x v y) v c(x) = z v c(z). [para(2483(a,1),4110(a,2,2)),flip(a)]. given #255 (T,wt=11): 4249 (c(x) v y) v x = z v c(z). [para(2488(a,1),4110(a,2,2)),flip(a)]. given #256 (A,wt=18): 2700 (x v (c(y) v z)) v c(y v u) = x v (c(y) v z). [para(2658(a,1),2660(a,1,2,1,1))]. given #257 (F,wt=11): 4250 (x v c(y)) v y = z v c(z). [para(2596(a,1),4110(a,2,2)),flip(a)]. given #258 (F,wt=11): 4251 (x v y) v c(y) = z v c(z). [para(2603(a,1),4110(a,2,2)),flip(a)]. given #259 (T,wt=11): 4252 x v c(x) = y v (z v c(y)). [para(2611(a,1),4110(a,2,2))]. given #260 (T,wt=11): 4265 x v (c(x) v y) = x v c(x). [para(4110(a,2),2692(a,1,1)),rewrite(4072(6),2392(2)),flip(a)]. given #261 (A,wt=18): 2706 c(x v y) v (z v (u v c(x))) = z v (u v c(x)). [para(2672(a,1),2640(a,1,1,1,1))]. given #262 (F,wt=11): 4270 c(x) v (y v x) = z v c(z). [para(4110(a,2),2768(a,1)),flip(a)]. given #263 (F,wt=11): 4696 (x v c(x)) v y = c(x) v x. [para(3950(a,1),2699(a,1,1,1)),rewrite(3991(4),4072(5),2392(4)),flip(a)]. given #264 (T,wt=11): 4764 x v (y v c(x)) = x v c(x). [para(2611(a,1),4265(a,1,2))]. given #265 (T,wt=13): 4129 c(((c(x) v y) v z) v x) v u = u. [para(2640(a,1),4103(a,1,1,1,2))]. given #266 (A,wt=18): 2707 c(x v y) v (z v (u v c(y))) = z v (u v c(y)). [para(2672(a,1),2658(a,1,1,1,2))]. given #267 (F,wt=13): 4130 c(((x v c(y)) v z) v y) v u = u. [para(2657(a,1),4103(a,1,1,1,2))]. given #268 (F,wt=13): 4131 c((x v (c(y) v z)) v y) v u = u. [para(2658(a,1),4103(a,1,1,1,2))]. given #269 (T,wt=13): 4132 c((x v (y v c(z))) v z) v u = u. [para(2672(a,1),4103(a,1,1,1,2))]. given #270 (T,wt=13): 4133 c(((x v y) v z) v c(x)) v u = u. [para(2651(a,1),4103(a,1,1,1,2))]. given #271 (A,wt=18): 2708 (x v (y v c(z))) v c(z v u) = x v (y v c(z)). [para(2672(a,1),2660(a,1,2,1,1))]. given #272 (F,wt=13): 4134 c(((x v y) v z) v c(y)) v u = u. [para(2670(a,1),4103(a,1,1,1,2))]. given #273 (F,wt=13): 4135 c((x v (y v z)) v c(y)) v u = u. [para(2677(a,1),4103(a,1,1,1,2))]. given #274 (T,wt=13): 4136 c((x v (y v z)) v c(z)) v u = u. [para(2702(a,1),4103(a,1,1,1,2))]. given #275 (T,wt=13): 4137 c((c(x) v y) v (x v z)) v u = u. [para(2653(a,1),4103(a,1,1,1,2))]. given #276 (A,wt=14): 2723 (c(x) v y) v c(z v x) = c(x) v y. [para(2488(a,1),2684(a,1,2,1,2))]. given #277 (F,wt=13): 4138 c((c(x) v y) v (z v x)) v u = u. [para(2656(a,1),4103(a,1,1,1,2))]. given #278 (F,wt=13): 4139 c((x v c(y)) v (y v z)) v u = u. [para(2679(a,1),4103(a,1,1,1,2))]. given #279 (T,wt=13): 4140 c((x v c(y)) v (z v y)) v u = u. [para(2682(a,1),4103(a,1,1,1,2))]. given #280 (T,wt=13): 4156 c((x v y) v (c(x) v z)) v u = u. [para(2654(a,1),4103(a,1,1,1,2))]. given #281 (A,wt=14): 2724 (x v c(y)) v c(z v y) = x v c(y). [para(2596(a,1),2684(a,1,2,1,2))]. given #282 (F,wt=13): 4157 c((x v y) v (z v c(x))) v u = u. [para(2655(a,1),4103(a,1,1,1,2))]. given #283 (F,wt=13): 4160 c((x v y) v (c(y) v z)) v u = u. [para(2680(a,1),4103(a,1,1,1,2))]. given #284 (T,wt=13): 4161 c((x v y) v (z v c(y))) v u = u. [para(2681(a,1),4103(a,1,1,1,2))]. given #285 (T,wt=13): 4169 x v c(((c(y) v z) v u) v y) = x. [para(2640(a,1),4104(a,1,2,1,2))]. given #286 (A,wt=18): 2726 ((c(x) v y) v z) v c(u v x) = (c(x) v y) v z. [para(2640(a,1),2684(a,1,2,1,2))]. given #287 (F,wt=13): 4170 x v c(((y v c(z)) v u) v z) = x. [para(2657(a,1),4104(a,1,2,1,2))]. given #288 (F,wt=13): 4171 x v c((y v (c(z) v u)) v z) = x. [para(2658(a,1),4104(a,1,2,1,2))]. given #289 (T,wt=13): 4172 x v c((y v (z v c(u))) v u) = x. [para(2672(a,1),4104(a,1,2,1,2))]. given #290 (T,wt=13): 4173 x v c(((y v z) v u) v c(y)) = x. [para(2651(a,1),4104(a,1,2,1,2))]. given #291 (A,wt=18): 2729 ((x v c(y)) v z) v c(u v y) = (x v c(y)) v z. [para(2657(a,1),2684(a,1,2,1,2))]. given #292 (F,wt=13): 4174 x v c(((y v z) v u) v c(z)) = x. [para(2670(a,1),4104(a,1,2,1,2))]. given #293 (F,wt=13): 4175 x v c((y v (z v u)) v c(z)) = x. [para(2677(a,1),4104(a,1,2,1,2))]. given #294 (T,wt=13): 4176 x v c((y v (z v u)) v c(u)) = x. [para(2702(a,1),4104(a,1,2,1,2))]. given #295 (T,wt=13): 4177 x v c((c(y) v z) v (y v u)) = x. [para(2653(a,1),4104(a,1,2,1,2))]. given #296 (A,wt=18): 2730 (x v (c(y) v z)) v c(u v y) = x v (c(y) v z). [para(2658(a,1),2684(a,1,2,1,2))]. given #297 (F,wt=13): 4178 x v c((c(y) v z) v (u v y)) = x. [para(2656(a,1),4104(a,1,2,1,2))]. given #298 (F,wt=13): 4179 x v c((y v c(z)) v (z v u)) = x. [para(2679(a,1),4104(a,1,2,1,2))]. given #299 (T,wt=13): 4180 x v c((y v c(z)) v (u v z)) = x. [para(2682(a,1),4104(a,1,2,1,2))]. given #300 (T,wt=13): 4196 x v c((y v z) v (c(y) v u)) = x. [para(2654(a,1),4104(a,1,2,1,2))]. given #301 (A,wt=18): 2731 (x v (y v c(z))) v c(u v z) = x v (y v c(z)). [para(2672(a,1),2684(a,1,2,1,2))]. given #302 (F,wt=13): 4197 x v c((y v z) v (u v c(y))) = x. [para(2655(a,1),4104(a,1,2,1,2))]. given #303 (F,wt=13): 4200 x v c((y v z) v (c(z) v u)) = x. [para(2680(a,1),4104(a,1,2,1,2))]. given #304 (T,wt=13): 4201 x v c((y v z) v (u v c(z))) = x. [para(2681(a,1),4104(a,1,2,1,2))]. given #305 (T,wt=13): 4210 c(x) v x = ((c(y) v z) v u) v y. [para(2640(a,1),4108(a,2,2))]. given #306 (A,wt=17): 2737 c(c(x) v y) v ((x v z) v u) = (x v z) v u. [para(2651(a,1),2640(a,1,1,1,1))]. given #307 (F,wt=13): 4211 c(x) v x = ((y v c(z)) v u) v z. [para(2657(a,1),4108(a,2,2))]. given #308 (F,wt=13): 4212 c(x) v x = (y v (c(z) v u)) v z. [para(2658(a,1),4108(a,2,2))]. given #309 (T,wt=13): 4213 c(x) v x = (y v (z v c(u))) v u. [para(2672(a,1),4108(a,2,2))]. given #310 (T,wt=13): 4214 c(x) v x = ((y v z) v u) v c(y). [para(2651(a,1),4108(a,2,2))]. given #311 (A,wt=17): 2738 c(x v c(y)) v ((y v z) v u) = (y v z) v u. [para(2651(a,1),2658(a,1,1,1,2))]. given #312 (F,wt=13): 4215 c(x) v x = ((y v z) v u) v c(z). [para(2670(a,1),4108(a,2,2))]. given #313 (F,wt=13): 4216 c(x) v x = (y v (z v u)) v c(z). [para(2677(a,1),4108(a,2,2))]. given #314 (T,wt=13): 4217 c(x) v x = (y v (z v u)) v c(u). [para(2702(a,1),4108(a,2,2))]. given #315 (T,wt=13): 4218 c(x) v x = (c(y) v z) v (y v u). [para(2653(a,1),4108(a,2,2))]. given #316 (A,wt=17): 2739 ((x v y) v z) v c(c(x) v u) = (x v y) v z. [para(2651(a,1),2660(a,1,2,1,1))]. given #317 (F,wt=13): 4219 c(x) v x = (c(y) v z) v (u v y). [para(2656(a,1),4108(a,2,2))]. given #318 (F,wt=13): 4220 c(x) v x = (y v c(z)) v (z v u). [para(2679(a,1),4108(a,2,2))]. given #319 (T,wt=13): 4221 c(x) v x = (y v c(z)) v (u v z). [para(2682(a,1),4108(a,2,2))]. given #320 (T,wt=13): 4237 c(x) v x = (y v z) v (c(y) v u). [para(2654(a,1),4108(a,2,2))]. given #321 (A,wt=17): 2740 ((x v y) v z) v c(u v c(x)) = (x v y) v z. [para(2651(a,1),2684(a,1,2,1,2))]. given #322 (F,wt=13): 4238 c(x) v x = (y v z) v (u v c(y)). [para(2655(a,1),4108(a,2,2))]. given #323 (F,wt=13): 4242 c(x) v x = (y v z) v (c(z) v u). [para(2680(a,1),4108(a,2,2))]. given #324 (T,wt=13): 4243 c(x) v x = (y v z) v (u v c(z)). [para(2681(a,1),4108(a,2,2))]. given #325 (T,wt=13): 4253 ((c(x) v y) v z) v x = u v c(u). [para(2640(a,1),4110(a,2,2)),flip(a)]. given #326 (A,wt=17): 2757 c(c(x) v y) v ((z v x) v u) = (z v x) v u. [para(2670(a,1),2640(a,1,1,1,1))]. given #327 (F,wt=13): 4254 ((x v c(y)) v z) v y = u v c(u). [para(2657(a,1),4110(a,2,2)),flip(a)]. given #328 (F,wt=13): 4255 (x v (c(y) v z)) v y = u v c(u). [para(2658(a,1),4110(a,2,2)),flip(a)]. given #329 (T,wt=13): 4256 (x v (y v c(z))) v z = u v c(u). [para(2672(a,1),4110(a,2,2)),flip(a)]. given #330 (T,wt=13): 4257 ((x v y) v z) v c(x) = u v c(u). [para(2651(a,1),4110(a,2,2)),flip(a)]. given #331 (A,wt=17): 2758 c(x v c(y)) v ((z v y) v u) = (z v y) v u. [para(2670(a,1),2658(a,1,1,1,2))]. given #332 (F,wt=13): 4258 ((x v y) v z) v c(y) = u v c(u). [para(2670(a,1),4110(a,2,2)),flip(a)]. given #333 (F,wt=13): 4259 (x v (y v z)) v c(y) = u v c(u). [para(2677(a,1),4110(a,2,2)),flip(a)]. given #334 (T,wt=13): 4260 (x v (y v z)) v c(z) = u v c(u). [para(2702(a,1),4110(a,2,2)),flip(a)]. given #335 (T,wt=13): 4261 (c(x) v y) v (x v z) = u v c(u). [para(2653(a,1),4110(a,2,2)),flip(a)]. given #336 (A,wt=17): 2759 ((x v y) v z) v c(c(y) v u) = (x v y) v z. [para(2670(a,1),2660(a,1,2,1,1))]. given #337 (F,wt=13): 4262 (c(x) v y) v (z v x) = u v c(u). [para(2656(a,1),4110(a,2,2)),flip(a)]. given #338 (F,wt=13): 4263 (x v c(y)) v (y v z) = u v c(u). [para(2679(a,1),4110(a,2,2)),flip(a)]. given #339 (T,wt=13): 4264 (x v c(y)) v (z v y) = u v c(u). [para(2682(a,1),4110(a,2,2)),flip(a)]. given #340 (T,wt=13): 4281 (x v y) v (c(x) v z) = u v c(u). [para(2654(a,1),4110(a,2,2)),flip(a)]. given #341 (A,wt=17): 2760 ((x v y) v z) v c(u v c(y)) = (x v y) v z. [para(2670(a,1),2684(a,1,2,1,2))]. given #342 (F,wt=13): 4282 (x v y) v (z v c(x)) = u v c(u). [para(2655(a,1),4110(a,2,2)),flip(a)]. given #343 (F,wt=13): 4287 (x v y) v (c(y) v z) = u v c(u). [para(2680(a,1),4110(a,2,2)),flip(a)]. given #344 (T,wt=13): 4288 (x v y) v (z v c(y)) = u v c(u). [para(2681(a,1),4110(a,2,2)),flip(a)]. given #345 (T,wt=13): 4303 c(c(x) v x) = c((c(y) v z) v y). [para(2686(a,1),3800(a,1,1)),flip(a)]. given #346 (A,wt=17): 2763 c(c(x) v y) v (z v (x v u)) = z v (x v u). [para(2677(a,1),2640(a,1,1,1,1))]. given #347 (F,wt=13): 4304 c((c(x) v y) v x) = c(z v c(z)). [para(2686(a,1),3861(a,1,1))]. given #348 (F,wt=13): 4325 c(c(x) v ((x v y) v z)) v u = u. [para(2735(a,1),4123(a,1,1,1,2))]. given #349 (T,wt=13): 4326 c(c(x) v ((y v x) v z)) v u = u. [para(2755(a,1),4123(a,1,1,1,2))]. given #350 (T,wt=13): 4327 c(c(x) v (y v (x v z))) v u = u. [para(2761(a,1),4123(a,1,1,1,2))]. given #351 (A,wt=17): 2764 c(x v c(y)) v (z v (y v u)) = z v (y v u). [para(2677(a,1),2658(a,1,1,1,2))]. given #352 (F,wt=13): 4328 c(c(x) v (y v (z v x))) v u = u. [para(2768(a,1),4123(a,1,1,1,2))]. given #353 (F,wt=13): 4338 c(c(x) v (x v y)) = c(c(z) v z). [para(4123(a,1),3772(a,1)),flip(a)]. given #354 (T,wt=13): 4339 c(c(x) v (x v y)) = c(z v c(z)). [para(4123(a,1),3799(a,1)),flip(a)]. given #355 (T,wt=13): 4377 c(c(x) v x) = c((y v z) v c(y)). [para(4124(a,1),3772(a,1))]. given #356 (A,wt=17): 2765 (x v (y v z)) v c(c(y) v u) = x v (y v z). [para(2677(a,1),2660(a,1,2,1,1))]. given #357 (F,wt=13): 4379 c((x v y) v c(x)) = c(z v c(z)). [para(4124(a,1),3799(a,1)),flip(a)]. given #358 (F,wt=13): 4410 c(c(x) v x) = c((y v c(z)) v z). [para(4126(a,1),3772(a,1))]. given #359 (T,wt=13): 4411 c((x v c(y)) v y) = c(z v c(z)). [para(4126(a,1),3799(a,1)),flip(a)]. given #360 (T,wt=13): 4451 c(c(x) v x) = c((y v z) v c(z)). [para(4127(a,1),3772(a,1))]. given #361 (A,wt=17): 2766 (x v (y v z)) v c(u v c(y)) = x v (y v z). [para(2677(a,1),2684(a,1,2,1,2))]. given #362 (F,wt=13): 4452 c((x v y) v c(y)) = c(z v c(z)). [para(4127(a,1),3799(a,1)),flip(a)]. given #363 (F,wt=13): 4507 c(c(x) v (y v x)) = c(c(z) v z). [para(4146(a,1),3772(a,1)),flip(a)]. given #364 (T,wt=13): 4508 c(c(x) v (y v x)) = c(z v c(z)). [para(4146(a,1),3799(a,1)),flip(a)]. given #365 (T,wt=13): 4515 x v c(c(y) v ((y v z) v u)) = x. [para(2735(a,1),4163(a,1,2,1,2))]. given #366 (A,wt=17): 2770 c(c(x) v y) v (z v (u v x)) = z v (u v x). [para(2702(a,1),2640(a,1,1,1,1))]. given #367 (F,wt=13): 4516 x v c(c(y) v ((z v y) v u)) = x. [para(2755(a,1),4163(a,1,2,1,2))]. given #368 (F,wt=13): 4517 x v c(c(y) v (z v (y v u))) = x. [para(2761(a,1),4163(a,1,2,1,2))]. given #369 (T,wt=13): 4518 x v c(c(y) v (z v (u v y))) = x. [para(2768(a,1),4163(a,1,2,1,2))]. given #370 (T,wt=13): 4591 c(x) v ((x v y) v z) = c(u) v u. [para(2735(a,1),4204(a,1,2))]. given #371 (A,wt=17): 2771 c(x v c(y)) v (z v (u v y)) = z v (u v y). [para(2702(a,1),2658(a,1,1,1,2))]. given #372 (F,wt=13): 4592 c(x) v ((y v x) v z) = c(u) v u. [para(2755(a,1),4204(a,1,2))]. given #373 (F,wt=13): 4594 c(x) v (y v (x v z)) = c(u) v u. [para(2761(a,1),4204(a,1,2))]. given #374 (T,wt=13): 4595 c(x) v (y v (z v x)) = c(u) v u. [para(2768(a,1),4204(a,1,2))]. given #375 (T,wt=13): 4597 c(x) v (x v y) = (c(z) v u) v z. [para(4204(a,2),2686(a,1))]. given #376 (A,wt=17): 2772 (x v (y v z)) v c(c(z) v u) = x v (y v z). [para(2702(a,1),2660(a,1,2,1,1))]. given #377 (F,wt=13): 4599 c(x) v (x v y) = c(z) v (z v u). [para(4204(a,2),4123(a,1))]. given #378 (F,wt=13): 4600 c(x) v (x v y) = (z v u) v c(z). [para(4204(a,2),4124(a,1))]. given #379 (T,wt=13): 4601 c(x) v (x v y) = (z v c(u)) v u. [para(4204(a,2),4126(a,1))]. given #380 (T,wt=13): 4603 c(x) v (x v y) = (z v u) v c(u). [para(4204(a,2),4127(a,1))]. given #381 (A,wt=17): 2773 (x v (y v z)) v c(u v c(z)) = x v (y v z). [para(2702(a,1),2684(a,1,2,1,2))]. given #382 (F,wt=13): 4605 c(x) v (y v x) = c(z) v (z v u). [para(4204(a,2),4146(a,1)),flip(a)]. given #383 (F,wt=13): 4622 (c(x) v y) v x = (z v u) v c(z). [para(4205(a,1),2686(a,1)),flip(a)]. given #384 (T,wt=13): 4624 (x v y) v c(x) = (z v u) v c(z). [para(4205(a,1),4124(a,1))]. given #385 (T,wt=13): 4625 (x v c(y)) v y = (z v u) v c(z). [para(4205(a,1),4126(a,1)),flip(a)]. given #386 (A,wt=16): 2774 c(x) v c(c(y v c(x v y)) v y) = c(x). [para(2585(a,1),2392(a,1,1)),flip(a)]. given #387 (F,wt=13): 4627 (x v y) v c(y) = (z v u) v c(z). [para(4205(a,1),4127(a,1)),flip(a)]. given #388 (F,wt=13): 4629 c(x) v (y v x) = (z v u) v c(z). [para(4205(a,1),4146(a,1)),flip(a)]. given #389 (T,wt=13): 4661 (c(x) v y) v x = (c(z) v u) v z. [para(4206(a,1),2686(a,1))]. given #390 (T,wt=13): 4662 (c(x) v y) v x = (z v c(u)) v u. [para(4206(a,1),4126(a,1))]. given #391 (A,wt=21): 2775 x v (c(y v c(x v y)) v y) = c(y v c(x v y)) v y. [para(2585(a,1),2596(a,1,1))]. given #392 (F,wt=13): 4663 (c(x) v y) v x = (z v u) v c(u). [para(4206(a,1),4127(a,1))]. given #393 (F,wt=13): 4665 c(x) v (y v x) = (c(z) v u) v z. [para(4206(a,1),4146(a,1)),flip(a)]. given #394 (T,wt=13): 4666 (x v c(y)) v y = (z v c(u)) v u. [para(4207(a,1),4126(a,1))]. given #395 (T,wt=13): 4667 (x v c(y)) v y = (z v u) v c(u). [para(4207(a,1),4127(a,1))]. given #396 (A,wt=21): 2779 (c(x v c(y v x)) v x) v y = c(x v c(y v x)) v x. [para(2585(a,1),2622(a,1,2))]. given #397 (F,wt=13): 4669 c(x) v (y v x) = (z v c(u)) v u. [para(4207(a,1),4146(a,1)),flip(a)]. given #398 (F,wt=13): 4670 (x v y) v c(y) = (z v u) v c(u). [para(4208(a,1),4127(a,1))]. given #399 (T,wt=13): 4672 c(x) v (y v x) = (z v u) v c(u). [para(4208(a,1),4146(a,1)),flip(a)]. given #400 (T,wt=13): 4705 c(x) v (y v x) = c(z) v (u v z). [para(4226(a,2),4146(a,1))]. given #401 (A,wt=16): 2792 c((x v y) v z) v (c(x) v u) = c(x) v u. [para(2653(a,1),2640(a,1,1,1,1))]. given #402 (F,wt=13): 4707 c(x) v ((x v y) v z) = u v c(u). [para(2735(a,1),4247(a,1,2))]. given #403 (F,wt=13): 4708 c(x) v ((y v x) v z) = u v c(u). [para(2755(a,1),4247(a,1,2))]. given #404 (T,wt=13): 4709 c(x) v (y v (x v z)) = u v c(u). [para(2761(a,1),4247(a,1,2))]. given #405 (T,wt=13): 4710 c(x) v (y v (z v x)) = u v c(u). [para(2768(a,1),4247(a,1,2))]. given #406 (A,wt=16): 2797 c(x v (y v z)) v (c(y) v u) = c(y) v u. [para(2653(a,1),2658(a,1,1,1,2))]. given #407 (F,wt=13): 4765 x v ((c(x) v y) v z) = x v c(x). [para(2735(a,1),4265(a,1,2))]. given #408 (F,wt=13): 4767 x v ((y v c(x)) v z) = x v c(x). [para(2755(a,1),4265(a,1,2))]. given #409 (T,wt=13): 4768 x v (y v (c(x) v z)) = x v c(x). [para(2761(a,1),4265(a,1,2))]. given #410 (T,wt=13): 4769 x v (y v (z v c(x))) = x v c(x). [para(2768(a,1),4265(a,1,2))]. given #411 (A,wt=16): 2800 (c(x) v y) v c((x v z) v u) = c(x) v y. [para(2653(a,1),2660(a,1,2,1,1))]. given #412 (F,wt=13): 7671 c(x v c(x v y)) v x = x v y. [para(2617(a,1),2779(a,1,1,1,1,2,1)),rewrite(2814(7),2617(3)),flip(a)]. given #413 (F,wt=13): 7672 c(x v c(y v x)) v x = y v x. [para(2619(a,1),2779(a,1,1,1,1,2,1)),rewrite(2816(7),2619(3)),flip(a)]. given #414 (T,wt=11): 7978 (c(x) v y) v x = c(x) v x. [para(2660(a,1),7672(a,1,1,1)),flip(a)]. given #415 (T,wt=11): 7979 (x v c(y)) v y = c(y) v y. [para(2674(a,1),7672(a,1,1,1)),flip(a)]. given #416 (A,wt=16): 2803 (c(x) v y) v c(z v (x v u)) = c(x) v y. [para(2653(a,1),2684(a,1,2,1,2))]. given #417 (F,wt=13): 7980 ((c(x) v y) v z) v x = c(x) v x. [para(2884(a,1),7672(a,1,1,1)),flip(a)]. given #418 (F,wt=13): 7981 ((x v c(y)) v z) v y = c(y) v y. [para(2886(a,1),7672(a,1,1,1)),flip(a)]. given #419 (T,wt=13): 7982 (x v (c(y) v z)) v y = c(y) v y. [para(2888(a,1),7672(a,1,1,1)),flip(a)]. given #420 (T,wt=13): 7983 (x v (y v c(z))) v z = c(z) v z. [para(2890(a,1),7672(a,1,1,1)),flip(a)]. given #421 (A,wt=17): 2804 x v (((x v y) v z) v u) = ((x v y) v z) v u. [para(2651(a,1),2653(a,1,1,1)),rewrite(2392(2))]. given #422 (F,wt=13): 7987 (c(x) v y) v (x v z) = c(x) v x. [para(7979(a,1),2696(a,1)),rewrite(2392(3),3933(4),2392(7)),flip(a)]. given #423 (F,wt=13): 7988 (x v c(y)) v (y v z) = c(y) v y. [para(7979(a,1),2699(a,1)),rewrite(2392(3),3933(4),2392(7)),flip(a)]. given #424 (T,wt=13): 8040 (c(x) v y) v (z v x) = c(x) v x. [para(7980(a,1),2769(a,1)),flip(a)]. given #425 (T,wt=13): 8044 (x v c(y)) v (z v y) = c(y) v y. [para(7981(a,1),2769(a,1)),flip(a)]. given #426 (A,wt=14): 2805 c(((x v y) v z) v u) v c(x) = c(x). [para(2651(a,1),2653(a,1,2)),rewrite(2392(4),2651(11))]. given #427 (F,wt=14): 2807 c(((x v y) v z) v u) v c(y) = c(y). [para(2670(a,1),2653(a,1,2)),rewrite(2392(4),2670(11))]. given #428 (F,wt=14): 2809 c((x v (y v z)) v u) v c(y) = c(y). [para(2677(a,1),2653(a,1,2)),rewrite(2392(4),2677(11))]. given #429 (T,wt=14): 2811 c((x v (y v z)) v u) v c(z) = c(z). [para(2702(a,1),2653(a,1,2)),rewrite(2392(4),2702(11))]. given #430 (T,wt=14): 2867 c(x v ((y v z) v u)) v c(y) = c(y). [para(2651(a,1),2679(a,1,2)),rewrite(2392(4),2651(11))]. given #431 (A,wt=17): 2806 x v (((y v x) v z) v u) = ((y v x) v z) v u. [para(2670(a,1),2653(a,1,1,1)),rewrite(2392(2))]. given #432 (F,wt=14): 2868 c(x v ((y v z) v u)) v c(z) = c(z). [para(2670(a,1),2679(a,1,2)),rewrite(2392(4),2670(11))]. given #433 (F,wt=14): 2869 c(x v (y v (z v u))) v c(z) = c(z). [para(2677(a,1),2679(a,1,2)),rewrite(2392(4),2677(11))]. given #434 (T,wt=14): 2870 c(x v (y v (z v u))) v c(u) = c(u). [para(2702(a,1),2679(a,1,2)),rewrite(2392(4),2702(11))]. given #435 (T,wt=14): 2892 c(x) v c(((x v y) v z) v u) = c(x). [para(2651(a,1),2692(a,1,1)),rewrite(2392(5),2651(11))]. given #436 (A,wt=17): 2808 x v ((y v (x v z)) v u) = (y v (x v z)) v u. [para(2677(a,1),2653(a,1,1,1)),rewrite(2392(2))]. given #437 (F,wt=14): 2894 c(x) v c(((y v x) v z) v u) = c(x). [para(2670(a,1),2692(a,1,1)),rewrite(2392(5),2670(11))]. given #438 (F,wt=14): 2896 c(x) v c((y v (x v z)) v u) = c(x). [para(2677(a,1),2692(a,1,1)),rewrite(2392(5),2677(11))]. given #439 (T,wt=14): 2898 c(x) v c((y v (z v x)) v u) = c(x). [para(2702(a,1),2692(a,1,1)),rewrite(2392(5),2702(11))]. given #440 (T,wt=14): 2956 c(x) v c(y v ((x v z) v u)) = c(x). [para(2651(a,1),2722(a,1,1)),rewrite(2392(5),2651(11))]. given #441 (A,wt=17): 2810 x v ((y v (z v x)) v u) = (y v (z v x)) v u. [para(2702(a,1),2653(a,1,1,1)),rewrite(2392(2))]. given #442 (F,wt=14): 2957 c(x) v c(y v ((z v x) v u)) = c(x). [para(2670(a,1),2722(a,1,1)),rewrite(2392(5),2670(11))]. given #443 (F,wt=14): 2958 c(x) v c(y v (z v (x v u))) = c(x). [para(2677(a,1),2722(a,1,1)),rewrite(2392(5),2677(11))]. given #444 (T,wt=14): 2959 c(x) v c(y v (z v (u v x))) = c(x). [para(2702(a,1),2722(a,1,1)),rewrite(2392(5),2702(11))]. given #445 (T,wt=14): 7408 (x v c(y)) v c(x) = (z v u) v c(u). [para(4627(a,2),2675(a,1,2)),rewrite(4456(6)),flip(a)]. given #446 (A,wt=15): 2812 c((c(x) v y) v z) v (x v u) = x v u. [para(2653(a,1),2653(a,1,2)),rewrite(2392(4),2653(11))]. given #447 (F,wt=15): 2817 (c(x v c(y)) v c(z v c(y))) v y = y. [para(2611(a,1),2591(a,1,1,2,1))]. given #448 (F,wt=15): 2820 x v (c(y v c(x)) v c(c(x) v z)) = x. [para(2591(a,1),2617(a,1,1)),rewrite(2591(16))]. given #449 (T,wt=15): 2821 (c(c(x) v y) v c(c(x) v z)) v x = x. [para(2617(a,1),2591(a,1,1,1,1))]. given #450 (T,wt=15): 2857 c((c(x) v y) v z) v (u v x) = u v x. [para(2656(a,1),2653(a,1,2)),rewrite(2392(4),2656(11))]. given #451 (A,wt=17): 2814 (c(x v c(y v z)) v y) v (y v z) = y v z. [para(2483(a,1),2591(a,1,1,2,1)),rewrite(2392(6))]. given #452 (F,wt=11): 9175 (x v y) v (y v x) = y v x. [para(2620(a,1),2814(a,1,1,1,1)),rewrite(2392(2))]. % Operation v is commutative; C redundancy checks enabled. ============================== PROOF ================================= % Proof 9 at 4.24 (+ 0.14) seconds: commutativity_meet. % Length of proof is 93. % Level of proof is 21. % Maximum clause weight is 37. % Given clauses 452. 10 y v x = x v y # answer(commutativity_meet). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 33 c18 v c17 != c17 v c18 # answer(commutativity_meet). [deny(10)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1263 f(f(f(x v c(y),c(y) v z),u),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y. [para(66(a,1),61(a,1,1,1,1)),rewrite(65(5))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1628 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(62(a,1),59(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1648 f(f(x,c(y)) ^ (y v y),f(c(y),f(f(f(y v y,y),f(y v y,f(y v y,y))),f(y v y,y)))) = c(y). [para(1630(a,1),55(a,1,1,2)),rewrite(45(9))]. 1649 f(f(x,y) ^ f(y,f(y v y,y)),f(y,f(f(f(y v y,y),y v y),f(y v y,y)))) = y. [para(1630(a,1),55(a,1,2,2,1,2))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1785 f(f(x,y) ^ f(y,c(y)),f(y,f(f(c(y),y),c(y)))) = y. [back_rewrite(1649),rewrite(1739(2),21(2),1739(5),21(5),1739(6),1739(7),21(7))]. 1786 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y). [back_rewrite(1648),rewrite(1739(3),1739(5),21(5),1739(6),1739(6),21(6),1739(9),21(9))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 1798 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y). [back_rewrite(1628),rewrite(1739(3))]. 1958 f(f(f(x v c(y),c(y) v z),u),f(y,f(f(c(z),y v z),c(z)))) = y. [back_rewrite(1263),rewrite(1739(7),1739(8),1739(14))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2411 (c(c(x) v y) v c(y)) v c(y v c(c(y v c(c(y) v y)) v y)) = c(y). [back_rewrite(1786),rewrite(2384(2),2392(3),2374(3),2384(10),2392(11),2384(11),2392(9),2384(13),2392(14),2384(14),2392(8),2384(15),2392(7))]. 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. 2454 c(x v y) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z))) = c(y). [back_rewrite(1798),rewrite(2384(3),2384(6),2384(9),2384(12),2392(3),2384(13))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. 2488 c(c(x) v y) v x = x. [para(2392(a,1),2483(a,1,2)),rewrite(2392(6))]. 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2492 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)). [para(2410(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(25),2454(38),2392(13),2488(12))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. 2512 (c(x v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [para(2392(a,1),2412(a,1,1,1,1,1))]. 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. 2535 (x v c(c(x) v x)) v x = x. [para(1739(a,1),2515(a,1,1,1,1)),rewrite(2392(2))]. 2539 c(x) v c(x v c(x)) = c(x). [para(2392(a,1),2535(a,1,1,2,1,1)),rewrite(2492(7))]. 2543 x v c(c(x) v x) = x. [para(2392(a,1),2539(a,1,1)),rewrite(2392(3),2392(6))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2568 c(c(c(x v y) v c(y)) v y) = c(x v y) v c(y). [para(2508(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(7),2392(9))]. 2578 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [para(2483(a,1),2453(a,1,1,1)),rewrite(2392(4))]. 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. 2591 (c(x v c(y)) v c(c(y) v z)) v y = y. [para(2543(a,1),2453(a,1,1,1)),rewrite(2392(9),2585(16))]. 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. 2620 c(x) v c(y v x) = c(x). [para(2611(a,1),2608(a,1,2,1))]. 2814 (c(x v c(y v z)) v y) v (y v z) = y v z. [para(2483(a,1),2591(a,1,1,2,1)),rewrite(2392(6))]. 9175 (x v y) v (y v x) = y v x. [para(2620(a,1),2814(a,1,1,1,1)),rewrite(2392(2))]. 9329 x v y = y v x. [para(9175(a,1),2617(a,1,1)),rewrite(9175(3),9175(4))]. 9330 $F # answer(commutativity_meet). [resolve(9329,a,33,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 10 at 4.24 (+ 0.14) seconds: commutativity_join. % Length of proof is 93. % Level of proof is 21. % Maximum clause weight is 37. % Given clauses 452. 9 y v x = x v y # answer(commutativity_join). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 32 c16 v c15 != c15 v c16 # answer(commutativity_join). [deny(9)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1263 f(f(f(x v c(y),c(y) v z),u),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y. [para(66(a,1),61(a,1,1,1,1)),rewrite(65(5))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1628 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(62(a,1),59(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1648 f(f(x,c(y)) ^ (y v y),f(c(y),f(f(f(y v y,y),f(y v y,f(y v y,y))),f(y v y,y)))) = c(y). [para(1630(a,1),55(a,1,1,2)),rewrite(45(9))]. 1649 f(f(x,y) ^ f(y,f(y v y,y)),f(y,f(f(f(y v y,y),y v y),f(y v y,y)))) = y. [para(1630(a,1),55(a,1,2,2,1,2))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1785 f(f(x,y) ^ f(y,c(y)),f(y,f(f(c(y),y),c(y)))) = y. [back_rewrite(1649),rewrite(1739(2),21(2),1739(5),21(5),1739(6),1739(7),21(7))]. 1786 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y). [back_rewrite(1648),rewrite(1739(3),1739(5),21(5),1739(6),1739(6),21(6),1739(9),21(9))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 1798 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y). [back_rewrite(1628),rewrite(1739(3))]. 1958 f(f(f(x v c(y),c(y) v z),u),f(y,f(f(c(z),y v z),c(z)))) = y. [back_rewrite(1263),rewrite(1739(7),1739(8),1739(14))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2411 (c(c(x) v y) v c(y)) v c(y v c(c(y v c(c(y) v y)) v y)) = c(y). [back_rewrite(1786),rewrite(2384(2),2392(3),2374(3),2384(10),2392(11),2384(11),2392(9),2384(13),2392(14),2384(14),2392(8),2384(15),2392(7))]. 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. 2454 c(x v y) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z))) = c(y). [back_rewrite(1798),rewrite(2384(3),2384(6),2384(9),2384(12),2392(3),2384(13))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. 2488 c(c(x) v y) v x = x. [para(2392(a,1),2483(a,1,2)),rewrite(2392(6))]. 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2492 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)). [para(2410(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(25),2454(38),2392(13),2488(12))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. 2512 (c(x v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [para(2392(a,1),2412(a,1,1,1,1,1))]. 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. 2535 (x v c(c(x) v x)) v x = x. [para(1739(a,1),2515(a,1,1,1,1)),rewrite(2392(2))]. 2539 c(x) v c(x v c(x)) = c(x). [para(2392(a,1),2535(a,1,1,2,1,1)),rewrite(2492(7))]. 2543 x v c(c(x) v x) = x. [para(2392(a,1),2539(a,1,1)),rewrite(2392(3),2392(6))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2568 c(c(c(x v y) v c(y)) v y) = c(x v y) v c(y). [para(2508(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(7),2392(9))]. 2578 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [para(2483(a,1),2453(a,1,1,1)),rewrite(2392(4))]. 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. 2591 (c(x v c(y)) v c(c(y) v z)) v y = y. [para(2543(a,1),2453(a,1,1,1)),rewrite(2392(9),2585(16))]. 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. 2620 c(x) v c(y v x) = c(x). [para(2611(a,1),2608(a,1,2,1))]. 2814 (c(x v c(y v z)) v y) v (y v z) = y v z. [para(2483(a,1),2591(a,1,1,2,1)),rewrite(2392(6))]. 9175 (x v y) v (y v x) = y v x. [para(2620(a,1),2814(a,1,1,1,1)),rewrite(2392(2))]. 9329 x v y = y v x. [para(9175(a,1),2617(a,1,1)),rewrite(9175(3),9175(4))]. 9331 $F # answer(commutativity_join). [resolve(9329,a,32,a)]. ============================== end of proof ========================== ============================== PROOF ================================= % Proof 11 at 4.26 (+ 0.14) seconds: OM. % Length of proof is 99. % Level of proof is 22. % Maximum clause weight is 37. % Given clauses 452. 2 x v (c(x) ^ (x v y)) = x v y # answer(OM). [goal]. 15 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]. 16 x v y = f(f(x,x),f(y,y)) # label(Def_join). [assumption]. 17 f(f(x,x),f(y,y)) = x v y. [copy(16),flip(a)]. 18 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet). [assumption]. 19 f(f(x,y),f(x,y)) = x ^ y. [copy(18),flip(a)]. 20 c(x) = f(x,x) # label(Def_complement). [assumption]. 21 f(x,x) = c(x). [copy(20),flip(a)]. 23 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM). [deny(2)]. 40 c(f(x,y)) = x ^ y. [back_rewrite(19),rewrite(21(3))]. 41 f(c(x),c(y)) = x v y. [back_rewrite(17),rewrite(21(1),21(2))]. 42 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y. [back_rewrite(15),rewrite(21(5))]. 43 x ^ x = c(c(x)). [para(21(a,1),40(a,1,1)),flip(a)]. 45 c(c(x)) = x v x. [para(41(a,1),21(a,1)),flip(a)]. 46 c(x) ^ c(y) = c(x v y). [para(41(a,1),40(a,1,1)),flip(a)]. 50 x ^ x = x v x. [back_rewrite(43),rewrite(45(3))]. 52 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x. [para(21(a,1),42(a,1,1,1,1))]. 53 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y. [para(21(a,1),42(a,1,1,1,2))]. 54 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x. [para(21(a,1),42(a,1,1,1)),rewrite(21(1),45(2))]. 55 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y. [para(21(a,1),42(a,1,1)),rewrite(40(4))]. 59 f(f(f(x v y,f(c(y),z)),u),f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(41(a,1),42(a,1,1,1,1)),rewrite(45(8))]. 61 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y. [para(41(a,1),42(a,1,2,2,1,2))]. 62 f(f(x,y),f(x,f(f(f(f(z,f(c(x),z)),z),f(c(x),f(f(z,f(c(x),z)),z))),f(f(z,f(c(x),z)),z)))) = x. [para(42(a,1),42(a,1,1,1))]. 65 f(x v x,c(y)) = c(x) v y. [para(45(a,1),41(a,1,1))]. 66 f(c(x),y v y) = x v c(y). [para(45(a,1),41(a,1,2))]. 72 (x v x) ^ c(y) = c(c(x) v y). [para(45(a,1),46(a,1,1))]. 77 f(x v x,y v y) = c(x) v c(y). [para(45(a,1),65(a,1,2))]. 95 (x v x) ^ (y v y) = c(c(x) v c(y)). [para(45(a,1),72(a,1,2))]. 158 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x). [para(53(a,1),42(a,1,1)),rewrite(45(3))]. 203 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x. [para(65(a,1),54(a,1,1))]. 776 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [para(41(a,1),203(a,1,2,2,1,2)),rewrite(45(2))]. 785 f(c(x),f(x v x,f(f(f(x,f(f(x,f(c(x),x)),x)),x),f(x,f(f(x,f(c(x),x)),x))))) = x v x. [para(203(a,1),158(a,1,2,2,1,2)),rewrite(45(3),45(18))]. 1261 f(x,f(f(x,y),f(f(c(z),f(x,y) v z),c(z)))) = f(x,y). [para(42(a,1),61(a,1,1))]. 1263 f(f(f(x v c(y),c(y) v z),u),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y. [para(66(a,1),61(a,1,1,1,1)),rewrite(65(5))]. 1623 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y. [para(62(a,1),42(a,1,1))]. 1625 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x. [para(62(a,1),52(a,1,1))]. 1628 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y). [para(62(a,1),59(a,1,1))]. 1629 f(f(x,y),f(y,f(f(c(z),y v z),c(z)))) = y. [para(62(a,1),61(a,1,1))]. 1630 f(c(x),f(x v x,x)) = x v x. [back_rewrite(785),rewrite(1623(14))]. 1647 f((x v x) ^ f(f(x v x,x),y),f(f(x v x,x),f(f(y,f((x v x) ^ x,y)),y))) = f(x v x,x). [para(1630(a,1),55(a,1,1,1)),rewrite(40(10))]. 1648 f(f(x,c(y)) ^ (y v y),f(c(y),f(f(f(y v y,y),f(y v y,f(y v y,y))),f(y v y,y)))) = c(y). [para(1630(a,1),55(a,1,1,2)),rewrite(45(9))]. 1649 f(f(x,y) ^ f(y,f(y v y,y)),f(y,f(f(f(y v y,y),y v y),f(y v y,y)))) = y. [para(1630(a,1),55(a,1,2,2,1,2))]. 1693 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x. [para(41(a,1),1625(a,1,2,2,1,2))]. 1739 x v x = x. [para(1625(a,1),1625(a,1,2,2,1,2)),rewrite(1623(13),21(2),21(3),45(2))]. 1785 f(f(x,y) ^ f(y,c(y)),f(y,f(f(c(y),y),c(y)))) = y. [back_rewrite(1649),rewrite(1739(2),21(2),1739(5),21(5),1739(6),1739(7),21(7))]. 1786 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y). [back_rewrite(1648),rewrite(1739(3),1739(5),21(5),1739(6),1739(6),21(6),1739(9),21(9))]. 1787 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x). [back_rewrite(1647),rewrite(1739(1),1739(1),21(1),1739(4),21(4),1739(5),50(5),1739(5),1739(10),21(10))]. 1798 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y). [back_rewrite(1628),rewrite(1739(3))]. 1958 f(f(f(x v c(y),c(y) v z),u),f(y,f(f(c(z),y v z),c(z)))) = y. [back_rewrite(1263),rewrite(1739(7),1739(8),1739(14))]. 2130 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x). [back_rewrite(776),rewrite(1739(1))]. 2374 x ^ y = c(c(x) v c(y)). [back_rewrite(95),rewrite(1739(1),1739(1))]. 2384 f(x,y) = c(x) v c(y). [back_rewrite(77),rewrite(1739(1),1739(1))]. 2392 c(c(x)) = x. [back_rewrite(45),rewrite(1739(3))]. 2410 (c(x) v c(x v c(y))) v c(x v c(c(c(y) v c(c(x) v c(y))) v c(y))) = c(x). [back_rewrite(1787),rewrite(2384(2),2392(2),2374(3),2384(8),2384(11),2384(14),2384(17),2392(8),2384(18),2392(7))]. 2411 (c(c(x) v y) v c(y)) v c(y v c(c(y v c(c(y) v y)) v y)) = c(y). [back_rewrite(1786),rewrite(2384(2),2392(3),2374(3),2384(10),2392(11),2384(11),2392(9),2384(13),2392(14),2384(14),2392(8),2384(15),2392(7))]. 2412 (c(c(x) v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [back_rewrite(1785),rewrite(2384(1),2384(5),2392(6),2374(6),2384(11),2392(11),2384(13),2392(14),2384(14),2384(17),2392(10))]. 2440 c3 v c(c3 v c(c3 v c4)) != c3 v c4 # answer(OM). [back_rewrite(23),rewrite(2374(7),2392(4))]. 2443 c(x) v c(c(c(x) v c(y)) v c(c(z v c((c(x) v c(y)) v z)) v z)) = c(x) v c(y). [back_rewrite(1261),rewrite(2384(1),2384(5),2384(9),2392(5),2384(11),2392(12),2384(12),2384(15),2384(18))]. 2450 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [back_rewrite(2130),rewrite(2384(6),2392(4),2384(8),2392(9),2384(9),2392(3),2384(10))]. 2453 c(c(c(x v c(y)) v c(c(y) v z)) v c(u)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1958),rewrite(2384(5),2384(8),2384(13),2392(12),2384(15),2392(16),2384(16),2384(19))]. 2454 c(x v y) v c(y v c(c(c(z) v c(c(y) v c(z))) v c(z))) = c(y). [back_rewrite(1798),rewrite(2384(3),2384(6),2384(9),2384(12),2392(3),2384(13))]. 2465 x v c(c(x) v c(c(y v c(x v y)) v y)) = x. [back_rewrite(1693),rewrite(2384(4),2392(3),2384(6),2392(7),2384(7),2384(10),2392(2))]. 2466 c(c(x) v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [back_rewrite(1629),rewrite(2384(1),2384(6),2392(5),2384(8),2392(9),2384(9),2384(12))]. 2481 c(x v c(c(x v c(c(x) v x)) v x)) = c(x). [para(2450(a,1),1739(a,1)),flip(a)]. 2483 c(x v y) v c(x) = c(x). [para(2450(a,1),2384(a,2)),rewrite(2384(10),2481(11))]. 2487 (c(c(x) v y) v c(y)) v c(y) = c(y). [back_rewrite(2411),rewrite(2481(14))]. 2488 c(c(x) v y) v x = x. [para(2392(a,1),2483(a,1,2)),rewrite(2392(6))]. 2489 x v (x v y) = x v y. [para(2483(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2492 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)). [para(2410(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(25),2454(38),2392(13),2488(12))]. 2493 x v c(c(x) v c(x v c(y))) = c(c(x) v c(x v c(y))). [para(2410(a,1),2483(a,1,1,1)),rewrite(2392(2))]. 2500 (c(c(x) v c(y)) v y) v y = y. [para(2392(a,1),2487(a,1,1,2)),rewrite(2392(7),2392(8))]. 2508 (c(x v c(y)) v y) v y = y. [para(2392(a,1),2500(a,1,1,1,1,1))]. 2512 (c(x v c(y)) v c(c(y) v y)) v c(c(y) v c(c(y v c(y)) v y)) = y. [para(2392(a,1),2412(a,1,1,1,1,1))]. 2515 (c(c(x) v c(y)) v c(c(y) v y)) v y = y. [para(2412(a,1),2489(a,1,2)),rewrite(2512(26))]. 2535 (x v c(c(x) v x)) v x = x. [para(1739(a,1),2515(a,1,1,1,1)),rewrite(2392(2))]. 2539 c(x) v c(x v c(x)) = c(x). [para(2392(a,1),2535(a,1,1,2,1,1)),rewrite(2492(7))]. 2543 x v c(c(x) v x) = x. [para(2392(a,1),2539(a,1,1)),rewrite(2392(3),2392(6))]. 2549 c(x) v c(x v c(c(x) v c(y))) = c(x). [para(2443(a,1),2465(a,1,2,1,2,1,1,1,2,1)),rewrite(2392(3),2466(38))]. 2559 c(c(x) v c(x v c(y))) = x. [para(2392(a,1),2549(a,1,1)),rewrite(2392(3),2493(7),2392(8))]. 2566 c(c(x) v c(x v y)) = x. [para(2392(a,1),2559(a,1,1,2,1,2))]. 2568 c(c(c(x v y) v c(y)) v y) = c(x v y) v c(y). [para(2508(a,1),2559(a,1,1,2,1)),rewrite(2392(2),2392(7),2392(9))]. 2578 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y. [para(2483(a,1),2453(a,1,1,1)),rewrite(2392(4))]. 2585 c(c(x) v c(c(y v c(x v y)) v y)) = x. [para(2453(a,1),2508(a,1,1)),rewrite(2465(10)),flip(a)]. 2591 (c(x v c(y)) v c(c(y) v z)) v y = y. [para(2543(a,1),2453(a,1,1,1)),rewrite(2392(9),2585(16))]. 2596 c(x v c(y)) v y = y. [back_rewrite(2578),rewrite(2585(12))]. 2603 c(x v y) v c(y) = c(y). [back_rewrite(2568),rewrite(2596(6)),flip(a)]. 2608 c(x) v c(x v y) = c(x). [para(2566(a,1),2392(a,1,1)),flip(a)]. 2611 x v (y v x) = y v x. [para(2603(a,1),2483(a,1,1,1)),rewrite(2392(2),2392(3),2392(5))]. 2615 x v c(c(x) v y) = x. [para(2392(a,1),2608(a,1,1)),rewrite(2392(6))]. 2617 (x v y) v x = x v y. [para(2483(a,1),2608(a,1,2,1)),rewrite(2392(3),2392(3),2392(5))]. 2620 c(x) v c(y v x) = c(x). [para(2611(a,1),2608(a,1,2,1))]. 2622 x v c(y v c(x)) = x. [para(2611(a,1),2615(a,1,2,1))]. 2779 (c(x v c(y v x)) v x) v y = c(x v c(y v x)) v x. [para(2585(a,1),2622(a,1,2))]. 2814 (c(x v c(y v z)) v y) v (y v z) = y v z. [para(2483(a,1),2591(a,1,1,2,1)),rewrite(2392(6))]. 7671 c(x v c(x v y)) v x = x v y. [para(2617(a,1),2779(a,1,1,1,1,2,1)),rewrite(2814(7),2617(3)),flip(a)]. 9175 (x v y) v (y v x) = y v x. [para(2620(a,1),2814(a,1,1,1,1)),rewrite(2392(2))]. 9329 x v y = y v x. [para(9175(a,1),2617(a,1,1)),rewrite(9175(3),9175(4))]. 9390 x v c(x v c(x v y)) = x v y. [para(7671(a,1),9175(a,2)),rewrite(9329(10),1739(11))]. 9391 $F # answer(OM). [resolve(9390,a,2440,a)]. ============================== end of proof ========================== % Redundant proof: 9911 $F # answer(commutativity_meet). [back_rewrite(33),rewrite(9329(3)),xx(a)]. % Redundant proof: 9912 $F # answer(commutativity_join). [back_rewrite(32),rewrite(9329(3)),xx(a)]. % back CAC tautology: 9328 c(x v y) = c(y v x). [para(9175(a,1),2608(a,1,2,1)),rewrite(9327(5))]. % Redundant proof: 9913 $F # answer(OM). [back_rewrite(2440),rewrite(9390(9)),xx(a)]. % Disable descendants: 23x 2440x 32x 33x given #453 (F,wt=11): 9910 c25 v (c23 v c24) != c23 v (c24 v c25) # answer(assoc_join). [back_rewrite(38),rewrite(9329(5))]. given #454 (T,wt=7): 9329 x v y = y v x. [para(9175(a,1),2617(a,1,1)),rewrite(9175(3),9175(4))]. given #455 (T,wt=11): 9810 (x v c(x)) v y = x v c(x). [back_rewrite(4696),rewrite(9329(5))]. given #456 (A,wt=30): 2832 c(x v y) v c(c(z v c(x)) v c(c(x) v u)) = c(c(z v c(x)) v c(c(x) v u)). [para(2591(a,1),2651(a,1,1,1,1))]. given #457 (F,wt=13): 9346 c((x v y) v c(y v x)) v z = z. [para(9175(a,1),4123(a,1,1,1,2)),rewrite(9329(4))]. given #458 (F,wt=13): 9347 x v c((y v z) v c(z v y)) = x. [para(9175(a,1),4163(a,1,2,1,2)),rewrite(9329(4))]. given #459 (T,wt=13): 9349 (x v y) v c(y v x) = z v c(z). [para(9175(a,1),4204(a,1,2)),rewrite(9329(4),9329(6))]. given #460 (T,wt=13): 9390 x v c(x v c(x v y)) = x v y. [para(7671(a,1),9175(a,2)),rewrite(9329(10),1739(11))]. given #461 (A,wt=30): 2835 c(x v y) v c(c(z v c(y)) v c(c(y) v u)) = c(c(z v c(y)) v c(c(y) v u)). [para(2591(a,1),2677(a,1,1,1,2))]. given #462 (F,wt=13): 9393 x v c(x v c(y v x)) = y v x. [para(7672(a,1),9175(a,2)),rewrite(9329(10),1739(11))]. given #463 (F,wt=13): 9734 (x v c(y)) v (z v y) = y v c(y). [back_rewrite(8044),rewrite(9329(6))]. given #464 (T,wt=13): 9735 (c(x) v y) v (z v x) = x v c(x). [back_rewrite(8040),rewrite(9329(6))]. given #465 (T,wt=13): 9737 (x v c(y)) v (y v z) = y v c(y). [back_rewrite(7988),rewrite(9329(6))]. given #466 (A,wt=30): 2837 c(c(x v c(y)) v c(c(y) v z)) v c(y v u) = c(c(x v c(y)) v c(c(y) v z)). [para(2591(a,1),2691(a,1,2,1,1))]. given #467 (F,wt=13): 9738 (c(x) v y) v (x v z) = x v c(x). [back_rewrite(7987),rewrite(9329(6))]. given #468 (F,wt=14): 9327 c(x v y) v c(y v x) = c(y v x). [para(9175(a,1),2483(a,1,1,1))]. given #469 (T,wt=15): 2871 c((x v c(y)) v z) v (y v u) = y v u. [para(2679(a,1),2653(a,1,2)),rewrite(2392(4),2679(11))]. given #470 (T,wt=15): 2872 c(x v (c(y) v z)) v (y v u) = y v u. [para(2653(a,1),2679(a,1,2)),rewrite(2392(4),2653(11))]. given #471 (A,wt=30): 2841 c(c(x v c(y)) v c(c(y) v z)) v c(u v y) = c(c(x v c(y)) v c(c(y) v z)). [para(2591(a,1),2721(a,1,2,1,2))]. given #472 (F,wt=15): 2875 c(x v (c(y) v z)) v (u v y) = u v y. [para(2656(a,1),2679(a,1,2)),rewrite(2392(4),2656(11))]. given #473 (F,wt=15): 2876 c(x v (y v c(z))) v (z v u) = z v u. [para(2679(a,1),2679(a,1,2)),rewrite(2392(4),2679(11))]. given #474 (T,wt=15): 2881 c((x v c(y)) v z) v (u v y) = u v y. [para(2682(a,1),2653(a,1,2)),rewrite(2392(4),2682(11))]. given #475 (T,wt=15): 2883 c(x v (y v c(z))) v (u v z) = u v z. [para(2682(a,1),2679(a,1,2)),rewrite(2392(4),2682(11))]. given #476 (A,wt=16): 2845 c((x v y) v z) v (c(y) v u) = c(y) v u. [para(2656(a,1),2640(a,1,1,1,1))]. given #477 (F,wt=15): 2900 (x v y) v c((c(x) v z) v u) = x v y. [para(2653(a,1),2692(a,1,1)),rewrite(2392(5),2653(11))]. given #478 (F,wt=15): 2903 (x v y) v c((c(y) v z) v u) = x v y. [para(2656(a,1),2692(a,1,1)),rewrite(2392(5),2656(11))]. given #479 (T,wt=15): 2904 (x v y) v c((z v c(x)) v u) = x v y. [para(2679(a,1),2692(a,1,1)),rewrite(2392(5),2679(11))]. given #480 (T,wt=15): 2905 (x v y) v c((z v c(y)) v u) = x v y. [para(2682(a,1),2692(a,1,1)),rewrite(2392(5),2682(11))]. given #481 (A,wt=16): 2848 c(x v (y v z)) v (c(z) v u) = c(z) v u. [para(2656(a,1),2658(a,1,1,1,2))]. given #482 (F,wt=15): 2960 (x v y) v c(z v (c(x) v u)) = x v y. [para(2653(a,1),2722(a,1,1)),rewrite(2392(5),2653(11))]. given #483 (F,wt=15): 2963 (x v y) v c(z v (c(y) v u)) = x v y. [para(2656(a,1),2722(a,1,1)),rewrite(2392(5),2656(11))]. given #484 (T,wt=15): 2964 (x v y) v c(z v (u v c(x))) = x v y. [para(2679(a,1),2722(a,1,1)),rewrite(2392(5),2679(11))]. given #485 (T,wt=15): 2965 (x v y) v c(z v (u v c(y))) = x v y. [para(2682(a,1),2722(a,1,1)),rewrite(2392(5),2682(11))]. given #486 (A,wt=16): 2850 (c(x) v y) v c((z v x) v u) = c(x) v y. [para(2656(a,1),2660(a,1,2,1,1))]. given #487 (F,wt=15): 3126 x v c((((c(x) v y) v z) v u) v v) = x. [para(2794(a,1),2692(a,1,1)),rewrite(2392(6),2794(13))]. given #488 (F,wt=15): 3129 x v c(y v (((c(x) v z) v u) v v)) = x. [para(2794(a,1),2722(a,1,1)),rewrite(2392(6),2794(13))]. given #489 (T,wt=15): 3165 x v c((((y v c(x)) v z) v u) v v) = x. [para(2796(a,1),2692(a,1,1)),rewrite(2392(6),2796(13))]. given #490 (T,wt=15): 3168 x v c(y v (((z v c(x)) v u) v v)) = x. [para(2796(a,1),2722(a,1,1)),rewrite(2392(6),2796(13))]. given #491 (A,wt=16): 2852 (c(x) v y) v c(z v (u v x)) = c(x) v y. [para(2656(a,1),2684(a,1,2,1,2))]. given #492 (F,wt=15): 3198 x v c(((y v (c(x) v z)) v u) v v) = x. [para(2799(a,1),2692(a,1,1)),rewrite(2392(6),2799(13))]. given #493 (F,wt=15): 3201 x v c(y v ((z v (c(x) v u)) v v)) = x. [para(2799(a,1),2722(a,1,1)),rewrite(2392(6),2799(13))]. given #494 (T,wt=15): 3221 x v c(((y v (z v c(x))) v u) v v) = x. [para(2802(a,1),2692(a,1,1)),rewrite(2392(6),2802(13))]. given #495 (T,wt=15): 3224 x v c(y v ((z v (u v c(x))) v v)) = x. [para(2802(a,1),2722(a,1,1)),rewrite(2392(6),2802(13))]. given #496 (A,wt=17): 2853 x v (y v ((x v z) v u)) = y v ((x v z) v u). [para(2651(a,1),2656(a,1,1,1)),rewrite(2392(2))]. given #497 (F,wt=15): 3252 x v c((y v ((c(x) v z) v u)) v v) = x. [para(2860(a,1),2692(a,1,1)),rewrite(2392(6),2860(13))]. given #498 (F,wt=15): 3255 x v c(y v (z v ((c(x) v u) v v))) = x. [para(2860(a,1),2722(a,1,1)),rewrite(2392(6),2860(13))]. given #499 (T,wt=15): 3320 x v c((y v ((z v c(x)) v u)) v v) = x. [para(2861(a,1),2692(a,1,1)),rewrite(2392(6),2861(13))]. given #500 (T,wt=15): 3323 x v c(y v (z v ((u v c(x)) v v))) = x. [para(2861(a,1),2722(a,1,1)),rewrite(2392(6),2861(13))]. given #501 (A,wt=17): 2854 x v (y v ((z v x) v u)) = y v ((z v x) v u). [para(2670(a,1),2656(a,1,1,1)),rewrite(2392(2))]. given #502 (F,wt=15): 3351 x v c((y v (z v (c(x) v u))) v v) = x. [para(2863(a,1),2692(a,1,1)),rewrite(2392(6),2863(13))]. given #503 (F,wt=15): 3354 x v c(y v (z v (u v (c(x) v v)))) = x. [para(2863(a,1),2722(a,1,1)),rewrite(2392(6),2863(13))]. given #504 (T,wt=15): 3378 x v c((y v (z v (u v c(x)))) v v) = x. [para(2865(a,1),2692(a,1,1)),rewrite(2392(6),2865(13))]. given #505 (T,wt=15): 3381 x v c(y v (z v (u v (v v c(x))))) = x. [para(2865(a,1),2722(a,1,1)),rewrite(2392(6),2865(13))]. given #506 (A,wt=17): 2855 x v (y v (z v (x v u))) = y v (z v (x v u)). [para(2677(a,1),2656(a,1,1,1)),rewrite(2392(2))]. given #507 (F,wt=15): 3529 c(x) v (c(y v x) v c(x v z)) = c(x). [para(2634(a,1),2617(a,1,1)),rewrite(2634(14))]. given #508 (F,wt=15): 4162 c((x v y) v (z v (c(x) v u))) v v = v. [para(2685(a,1),4103(a,1,1,1,2))]. given #509 (T,wt=15): 4202 x v c((y v z) v (u v (c(y) v v))) = x. [para(2685(a,1),4104(a,1,2,1,2))]. given #510 (T,wt=15): 4342 x v (c(y) v (y v z)) = c(y) v (y v z). [para(4123(a,1),3954(a,1,2)),rewrite(4311(12))]. given #511 (A,wt=17): 2856 x v (y v (z v (u v x))) = y v (z v (u v x)). [para(2702(a,1),2656(a,1,1,1)),rewrite(2392(2))]. given #512 (F,wt=15): 4343 (c(x) v (x v y)) v z = c(x) v (x v y). [para(4123(a,1),3966(a,1,1)),rewrite(4342(12))]. given #513 (F,wt=15): 4344 c((x v y) v ((c(y) v z) v u)) v v = v. [para(2686(a,1),4123(a,1,1,1,2)),rewrite(2392(3))]. given #514 (T,wt=15): 4384 x v ((y v z) v c(y)) = (y v z) v c(y). [para(4124(a,1),3954(a,1,2)),rewrite(4345(12))]. given #515 (T,wt=15): 4385 ((x v y) v c(x)) v z = (x v y) v c(x). [para(4124(a,1),3966(a,1,1)),rewrite(4384(12))]. given #516 (A,wt=16): 2859 c((x v y) v z) v (u v c(x)) = u v c(x). [para(2679(a,1),2640(a,1,1,1,1))]. given #517 (F,wt=15): 4428 c((x v y) v ((z v c(y)) v u)) v v = v. [para(2688(a,1),4123(a,1,1,1,2)),rewrite(2392(3))]. given #518 (F,wt=15): 4456 x v ((y v z) v c(z)) = (y v z) v c(z). [para(4127(a,1),3954(a,1,2)),rewrite(4430(12))]. given #519 (T,wt=15): 4457 ((x v y) v c(y)) v z = (x v y) v c(y). [para(4127(a,1),3966(a,1,1)),rewrite(4456(12))]. given #520 (T,wt=15): 4512 x v (c(y) v (z v y)) = c(y) v (z v y). [para(4146(a,1),3954(a,1,2)),rewrite(4486(12))]. given #521 (A,wt=16): 2862 c(x v (y v z)) v (u v c(y)) = u v c(y). [para(2679(a,1),2658(a,1,1,1,2))]. given #522 (F,wt=15): 4513 (c(x) v (y v x)) v z = c(x) v (y v x). [para(4146(a,1),3966(a,1,1)),rewrite(4512(12))]. given #523 (F,wt=15): 4520 x v c((y v z) v ((c(z) v u) v v)) = x. [para(2686(a,1),4163(a,1,2,1,2)),rewrite(2392(3))]. given #524 (T,wt=15): 4521 c(c(x) v (x v y)) = c(c(z) v (z v u)). [para(4163(a,1),4123(a,1))]. given #525 (T,wt=15): 4522 c(c(x) v (x v y)) = c((z v u) v c(z)). [para(4163(a,1),4124(a,1)),flip(a)]. given #526 (A,wt=16): 2864 (x v c(y)) v c((y v z) v u) = x v c(y). [para(2679(a,1),2660(a,1,2,1,1))]. given #527 (F,wt=15): 4525 x v c((y v z) v ((u v c(z)) v v)) = x. [para(2688(a,1),4163(a,1,2,1,2)),rewrite(2392(3))]. given #528 (F,wt=15): 4526 c(c(x) v (x v y)) = c((z v u) v c(u)). [para(4163(a,1),4127(a,1)),flip(a)]. given #529 (T,wt=15): 4528 c(c(x) v (y v x)) = c(c(z) v (z v u)). [para(4163(a,1),4146(a,1))]. given #530 (T,wt=15): 4544 c((x v y) v (z v (c(y) v u))) v v = v. [para(2689(a,1),4123(a,1,1,1,2)),rewrite(2392(3))]. given #531 (A,wt=16): 2866 (x v c(y)) v c(z v (y v u)) = x v c(y). [para(2679(a,1),2684(a,1,2,1,2))]. given #532 (F,wt=15): 4546 x v c((y v z) v (u v (c(z) v v))) = x. [para(2689(a,1),4163(a,1,2,1,2)),rewrite(2392(3))]. given #533 (F,wt=15): 4563 c((x v y) v c(x)) = c((z v u) v c(z)). [para(4164(a,1),4124(a,1))]. given #534 (T,wt=15): 4567 c((x v y) v c(y)) = c((z v u) v c(z)). [para(4164(a,1),4127(a,1))]. given #535 (T,wt=15): 4569 c(c(x) v (y v x)) = c((z v u) v c(z)). [para(4164(a,1),4146(a,1))]. given #536 (A,wt=16): 2877 c((x v y) v z) v (u v c(y)) = u v c(y). [para(2682(a,1),2640(a,1,1,1,1))]. given #537 (F,wt=15): 4580 c((x v y) v c(y)) = c((z v u) v c(u)). [para(4167(a,1),4127(a,1))]. given #538 (F,wt=15): 4582 c(c(x) v (y v x)) = c((z v u) v c(u)). [para(4167(a,1),4146(a,1))]. given #539 (T,wt=15): 4589 c(c(x) v (y v x)) = c(c(z) v (u v z)). [para(4186(a,1),4146(a,1))]. given #540 (T,wt=15): 4712 (x v y) v ((c(y) v z) v u) = v v c(v). [para(2686(a,1),4247(a,1,2)),rewrite(2392(3))]. given #541 (A,wt=16): 2878 c(x v (y v z)) v (u v c(z)) = u v c(z). [para(2682(a,1),2658(a,1,1,1,2))]. given #542 (F,wt=15): 4713 (x v y) v ((z v c(y)) v u) = v v c(v). [para(2688(a,1),4247(a,1,2)),rewrite(2392(3))]. given #543 (F,wt=15): 4714 (x v y) v (z v (c(y) v u)) = v v c(v). [para(2689(a,1),4247(a,1,2)),rewrite(2392(3))]. given #544 (T,wt=15): 4804 c((x v y) v (z v (u v c(x)))) v v = v. [para(2706(a,1),4123(a,1,1,1,2)),rewrite(2392(3))]. given #545 (T,wt=15): 4807 x v c((y v z) v (u v (v v c(y)))) = x. [para(2706(a,1),4163(a,1,2,1,2)),rewrite(2392(3))]. given #546 (A,wt=16): 2879 (x v c(y)) v c((z v y) v u) = x v c(y). [para(2682(a,1),2660(a,1,2,1,1))]. given #547 (F,wt=15): 4831 c(((x v y) v z) v (c(x) v u)) v v = v. [para(2653(a,1),4129(a,1,1,1,1,1))]. given #548 (F,wt=15): 4834 c(((x v y) v z) v (c(y) v u)) v v = v. [para(2656(a,1),4129(a,1,1,1,1,1))]. given #549 (T,wt=15): 4836 c(((x v y) v z) v (u v c(y))) v v = v. [para(2682(a,1),4129(a,1,1,1,1,1))]. given #550 (T,wt=15): 4888 c((x v y) v (z v (u v c(y)))) v v = v. [para(2707(a,1),4123(a,1,1,1,2)),rewrite(2392(3))]. given #551 (A,wt=16): 2880 (x v c(y)) v c(z v (u v y)) = x v c(y). [para(2682(a,1),2684(a,1,2,1,2))]. given #552 (F,wt=15): 4890 x v c((y v z) v (u v (v v c(z)))) = x. [para(2707(a,1),4163(a,1,2,1,2)),rewrite(2392(3))]. given #553 (F,wt=15): 4896 (x v y) v (z v (u v c(y))) = v v c(v). [para(2707(a,1),4247(a,1,2)),rewrite(2392(3))]. given #554 (T,wt=15): 4939 c((x v (y v z)) v (c(y) v u)) v v = v. [para(2700(a,1),4130(a,1,1,1)),rewrite(2392(3))]. given #555 (T,wt=15): 4955 c((x v (y v z)) v (c(z) v u)) v v = v. [para(2656(a,1),4131(a,1,1,1,1,2))]. given #556 (A,wt=19): 2902 x v c(c(c(y v c(x)) v c(c(x) v z)) v u) = x. [para(2591(a,1),2692(a,1,1)),rewrite(2591(19))]. given #557 (F,wt=15): 4956 c((x v (y v z)) v (u v c(y))) v v = v. [para(2679(a,1),4131(a,1,1,1,1,2))]. given #558 (F,wt=15): 4957 c((x v (y v z)) v (u v c(z))) v v = v. [para(2682(a,1),4131(a,1,1,1,1,2))]. given #559 (T,wt=15): 5056 c((((x v y) v z) v u) v c(y)) v v = v. [para(2755(a,1),4133(a,1,1,1,1,1))]. given #560 (T,wt=15): 5057