============================== Prover9 ===============================
Prover9 (32) version June-2006C, June 2006.
Process 13067 was started by mccune on cleo.thornwood,
Mon Jun 19 16:40:53 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]).

clauses(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).
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.

clauses(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).
x v y = y v x # answer(commutativity_join).
x v y = y v x # 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 GOALS =========================

% Each goal clause was negated; the result (to be placed in sos):

clauses(negated_goals).
c1 v (c1 ^ c2) != c1 # answer(B1).
c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM).
c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ).
c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM).
f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS).
c12 v c12 != c12 # answer(idempotence_join).
c13 ^ c13 != c13 # answer(idempotence_meet).
c(c(c14)) != c14 # answer(cc).
c16 v c15 != c15 v c16 # answer(commutativity_join).
c18 v c17 != c17 v c18 # answer(commutativity_meet).
c20 v c(c20) != c19 v c(c19) # answer(1).
c22 ^ c(c22) != c21 ^ c(c21) # answer(0).
(c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join).
(c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet).
end_of_list.

============================== end of process goals ==================

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

% Clauses before input processing:

clauses(usable).
end_of_list.

clauses(sos).
1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
5 c1 v (c1 ^ c2) != c1 # answer(B1).  [clausify].
6 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM).  [clausify].
7 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ).  [clausify].
8 c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM).  [clausify].
9 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS).  [clausify].
10 c12 v c12 != c12 # answer(idempotence_join).  [clausify].
11 c13 ^ c13 != c13 # answer(idempotence_meet).  [clausify].
12 c(c(c14)) != c14 # answer(cc).  [clausify].
13 c16 v c15 != c15 v c16 # answer(commutativity_join).  [clausify].
14 c18 v c17 != c17 v c18 # answer(commutativity_meet).  [clausify].
15 c20 v c(c20) != c19 v c(c19) # answer(1).  [clausify].
16 c22 ^ c(c22) != c21 ^ c(c21) # answer(0).  [clausify].
17 (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join).  [clausify].
18 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet).  [clausify].
end_of_list.

clauses(demodulators).
end_of_list.

Predicate elimination: (none).

Auto_denials:
  % assign(max_proofs, 14).  % (Horn set with more than one neg. clause)
    % assign(max_proofs, 14) -> set(restrict_denials).

% Restrict denials; moving clauses to denials list:

clauses(denials).
5 c1 v (c1 ^ c2) != c1 # answer(B1).  [clausify].
6 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM).  [clausify].
7 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ).  [clausify].
8 c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM).  [clausify].
9 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS).  [clausify].
10 c12 v c12 != c12 # answer(idempotence_join).  [clausify].
11 c13 ^ c13 != c13 # answer(idempotence_meet).  [clausify].
12 c(c(c14)) != c14 # answer(cc).  [clausify].
13 c16 v c15 != c15 v c16 # answer(commutativity_join).  [clausify].
14 c18 v c17 != c17 v c18 # answer(commutativity_meet).  [clausify].
15 c20 v c(c20) != c19 v c(c19) # answer(1).  [clausify].
16 c22 ^ c(c22) != c21 ^ c(c21) # answer(0).  [clausify].
17 (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join).  [clausify].
18 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet).  [clausify].
end_of_list.

Term ordering decisions:

WARNING, function symbols not in lex command: c1 c2 c3 c4 c6 c5 c7 c8 c9 c10 c11 c12 c13 c14 c16 c15 c18 c17 c20 c19 c22 c21 c23 c24 c25 c26 c27 c28.
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:

clauses(usable).
end_of_list.

clauses(sos).
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
end_of_list.

clauses(demodulators).
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
end_of_list.

clauses(denials).
26 c1 v (c1 ^ c2) != c1 # answer(B1).  [clausify].
27 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM).  [clausify].
28 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ).  [clausify].
29 c8 ^ c9 != c(c(c8) v c(c9)) # answer(DM).  [copy(8),flip(a)].
30 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS).  [clausify].
31 c12 v c12 != c12 # answer(idempotence_join).  [clausify].
32 c13 ^ c13 != c13 # answer(idempotence_meet).  [clausify].
33 c(c(c14)) != c14 # answer(cc).  [clausify].
34 c16 v c15 != c15 v c16 # answer(commutativity_join).  [clausify].
35 c18 v c17 != c17 v c18 # answer(commutativity_meet).  [clausify].
36 c20 v c(c20) != c19 v c(c19) # answer(1).  [clausify].
37 c22 ^ c(c22) != c21 ^ c(c21) # answer(0).  [clausify].
38 (c23 v c24) v c25 != c23 v (c24 v c25) # answer(assoc_join).  [clausify].
39 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet).  [clausify].
end_of_list.

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

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

% Starting search at 0.00 seconds.

given #1 (I,wt=6): 22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].

given #2 (I,wt=8): 23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].

given #3 (I,wt=9): 24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].

given #4 (I,wt=22): 25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].

given #5 (T,wt=7): 42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].

given #6 (A,wt=10): 43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].

given #7 (F,wt=7): 47 x ^ x = x v x.  [back_demod(40),demod(42(3))].

given #8 (F,wt=10): 65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].

given #9 (T,wt=11): 62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].

given #10 (T,wt=11): 63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].

given #11 (A,wt=12): 44 f(x ^ y,c(z)) = f(x,y) v z.  [para(23(a,1),24(a,1,1))].

given #12 (F,wt=12): 45 f(c(x),y ^ z) = x v f(y,z).  [para(23(a,1),24(a,1,2))].

given #13 (F,wt=12): 61 f(x,y) v f(x,y) = c(x ^ y).  [para(23(a,1),42(a,1,1)),flip(a)].

given #14 (T,wt=12): 69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].

given #15 (T,wt=12): 70 c(x) ^ (y v y) = c(x v c(y)).  [para(42(a,1),43(a,1,2))].

given #16 (A,wt=21): 49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].

given #17 (F,wt=13): 67 c(f(x,y) v z) = (x ^ y) ^ c(z).  [para(23(a,1),43(a,1,1)),flip(a)].

given #18 (F,wt=13): 68 c(x v f(y,z)) = c(x) ^ (y ^ z).  [para(23(a,1),43(a,1,2)),flip(a)].

given #19 (T,wt=13): 74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].

given #20 (T,wt=14): 72 f(x v x,y ^ z) = c(x) v f(y,z).  [para(23(a,1),62(a,1,2))].

given #21 (A,wt=21): 50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].

given #22 (F,wt=14): 75 f(x ^ y,z v z) = f(x,y) v c(z).  [para(23(a,1),63(a,1,1))].

given #23 (F,wt=14): 92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].

given #24 (T,wt=15): 79 f(x ^ y,z ^ u) = f(x,y) v f(z,u).  [para(23(a,1),44(a,1,2))].

given #25 (T,wt=15): 91 c(c(x) v f(y,z)) = (x v x) ^ (y ^ z).  [para(23(a,1),69(a,1,2)),flip(a)].

given #26 (A,wt=18): 51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].

given #27 (F,wt=15): 93 c(f(x,y) v c(z)) = (x ^ y) ^ (z v z).  [para(23(a,1),70(a,1,1)),flip(a)].

given #28 (F,wt=16): 85 f(c(x),y ^ z) v u = (x v f(y,z)) v u.  [para(45(a,1),44(a,2,1)),demod(44(5))].

given #29 (T,wt=16): 106 c(f(x,y) v f(z,u)) = (x ^ y) ^ (z ^ u).  [para(23(a,1),67(a,2,2))].

given #30 (T,wt=16): 137 x v f(c(y),z ^ u) = x v (y v f(z,u)).  [para(68(a,2),45(a,1,2)),demod(24(5)),flip(a)].

given #31 (A,wt=20): 52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].

given #32 (F,wt=17): 84 f(c(x) v c(x),y ^ z) = (x v x) v f(y,z).  [para(65(a,1),45(a,1,1))].

given #33 (F,wt=17): 86 f(c(x),(y ^ z) ^ c(u)) = x v (f(y,z) v u).  [para(44(a,1),45(a,2,2))].

given #34 (T,wt=17): 87 f(c(x),c(y) ^ (z ^ u)) = x v (y v f(z,u)).  [para(45(a,1),45(a,2,2))].

given #35 (T,wt=17): 114 c(f(x,y) v z) v u = ((x ^ y) ^ c(z)) v u.  [para(67(a,1),62(a,2,1)),demod(62(7))].

given #36 (A,wt=23): 54 f(f(f(x,y),f(y,z)),u) ^ f(y,f(f(z,f(c(y),z)),z)) = c(y).  [para(25(a,1),23(a,1,1)),flip(a)].

given #37 (F,wt=17): 115 x v c(f(y,z) v u) = x v ((y ^ z) ^ c(u)).  [para(67(a,1),63(a,2,2)),demod(63(7))].

given #38 (F,wt=17): 133 c(x v f(y,z)) v u = (c(x) ^ (y ^ z)) v u.  [para(68(a,1),62(a,2,1)),demod(62(7))].

given #39 (T,wt=17): 134 x v c(y v f(z,u)) = x v (c(y) ^ (z ^ u)).  [para(68(a,1),63(a,2,2)),demod(63(7))].

given #40 (T,wt=17): 167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].

given #41 (A,wt=31): 55 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(23(a,1),25(a,1,2,2,1,2,1))].

given #42 (F,wt=17): 225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].

given #43 (F,wt=18): 108 c((f(x,y) v z) v u) = ((x ^ y) ^ c(z)) ^ c(u).  [para(67(a,1),43(a,1,1)),flip(a)].

given #44 (T,wt=18): 109 c(x v (f(y,z) v u)) = c(x) ^ ((y ^ z) ^ c(u)).  [para(67(a,1),43(a,1,2)),flip(a)].

given #45 (T,wt=18): 112 c(f(x,y) v (z v z)) = (x ^ y) ^ (c(z) v c(z)).  [para(65(a,1),67(a,2,2))].

given #46 (A,wt=26): 56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].

given #47 (F,wt=18): 118 c((x v f(y,z)) v u) = (c(x) ^ (y ^ z)) ^ c(u).  [para(45(a,1),67(a,1,1,1))].

given #48 (F,wt=18): 128 c(x v (y v f(z,u))) = c(x) ^ (c(y) ^ (z ^ u)).  [para(68(a,1),43(a,1,2)),flip(a)].

given #49 (T,wt=18): 131 c((x v x) v f(y,z)) = (c(x) v c(x)) ^ (y ^ z).  [para(65(a,1),68(a,2,1))].

given #50 (T,wt=18): 145 c(f(c(x),y ^ z) v u) = c((x v f(y,z)) v u).  [para(68(a,2),67(a,2,1)),demod(43(10))].

given #51 (A,wt=24): 58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].

given #52 (F,wt=18): 148 c(x v f(c(y),z ^ u)) = c(x v (y v f(z,u))).  [para(68(a,2),68(a,2,2)),demod(43(10))].

given #53 (F,wt=18): 153 f(x v x,y ^ z) v u = (c(x) v f(y,z)) v u.  [para(72(a,1),44(a,2,1)),demod(44(5))].

given #54 (T,wt=18): 202 x v f(y v y,z ^ u) = x v (c(y) v f(z,u)).  [para(91(a,2),45(a,1,2)),demod(24(6)),flip(a)].

given #55 (T,wt=18): 573 x ^ f(c(x),f(f(y,f(x v x,y)),y)) = x v x.  [para(50(a,1),54(a,1,1)),demod(42(3),42(9))].

given #56 (A,wt=37): 59 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(25(a,1),25(a,1,1,1))].

given #57 (F,wt=12): 1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].

given #58 (F,wt=14): 1648 c(x) ^ f(x v x,x) = c(x) v c(x).  [back_demod(1636),demod(1641(14))].

given #59 (T,wt=15): 1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(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 59.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
33 c(c(c14)) != c14 # answer(cc).  [clausify].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
48 c14 v c14 != c14 # answer(cc).  [back_demod(33),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
59 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(25(a,1),25(a,1,1,1))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1758 $F # answer(cc).  [resolve(1757,a,48,a)].

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

NOTE: Disabling denial clause 48.

============================== 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 59.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
32 c13 ^ c13 != c13 # answer(idempotence_meet).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
41 c(c(c13)) != c13 # answer(idempotence_meet).  [back_demod(32),demod(40(3))].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
46 c13 v c13 != c13 # answer(idempotence_meet).  [back_demod(41),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
59 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(25(a,1),25(a,1,1,1))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1759 $F # answer(idempotence_meet).  [resolve(1757,a,46,a)].

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

NOTE: Disabling denial clause 46.

============================== 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 59.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
31 c12 v c12 != c12 # answer(idempotence_join).  [clausify].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
59 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(25(a,1),25(a,1,1,1))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1760 $F # answer(idempotence_join).  [resolve(1757,a,31,a)].

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

NOTE: Disabling denial clause 31.

============================== 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 59.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
8 c(c(c8) v c(c9)) != c8 ^ c9 # answer(DM).  [clausify].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
29 c8 ^ c9 != c(c(c8) v c(c9)) # answer(DM).  [copy(8),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
59 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(25(a,1),25(a,1,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2410 $F # answer(DM).  [resolve(2409,a,29,a)].

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

NOTE: Disabling denial clause 29.

============================== 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 59.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
30 f(c10,c11) != c(c10) v c(c11) # answer(DEF_SS).  [clausify].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2420 $F # answer(DEF_SS).  [resolve(2419,a,30,a)].

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

NOTE: Disabling denial clause 30.

given #60 (T,wt=5): 1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].

given #61 (A,wt=10): 2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].

given #62 (F,wt=5): 2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].

given #63 (F,wt=9): 2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].

given #64 (T,wt=16): 2498 x v c(c(x) v c(c(x v c(x)) v x)) = x.  [back_demod(1761),demod(2419(3),2425(3),2419(5),2425(6),2419(6),2419(9),2425(2))].

given #65 (T,wt=18): 2484 c(x) v c(x v c(c(c(x) v x) v c(x))) = c(x).  [back_demod(2179),demod(2419(4),2419(7),2425(2),2419(8))].

given #66 (A,wt=31): 2433 (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_demod(2334),demod(2419(3),2425(3),2409(4),2419(9),2419(12),2419(15),2419(18),2425(9),2419(19),2425(8))].

given #67 (F,wt=18): 2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].

given #68 (F,wt=20): 2506 c(x) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [back_demod(741),demod(2419(5),2425(3),2419(7),2425(8),2419(8),2425(2),2419(9))].

given #69 (T,wt=22): 2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].

given #70 (T,wt=10): 2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].

given #71 (A,wt=29): 2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].

given #72 (F,wt=9): 2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].

given #73 (F,wt=9): 2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].

given #74 (T,wt=14): 2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].

given #75 (T,wt=12): 2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].

given #76 (A,wt=29): 2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].

given #77 (F,wt=11): 2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].

given #78 (F,wt=11): 2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].

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

% Proof 6 at 0.44 (+ 0.01) seconds: B1.
% Length of proof is 57.
% Level of proof is 15.
% Maximum clause weight is 37.
% Given clauses 78.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
26 c1 v (c1 ^ c2) != c1 # answer(B1).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2477 c1 v c(c(c1) v c(c2)) != c1 # answer(B1).  [back_demod(26),demod(2409(4))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2561 x v c(c(x) v c(y)) = x.  [para(2425(a,1),2552(a,1,1)),demod(2425(7))].
2562 $F # answer(B1).  [resolve(2561,a,2477,a)].

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

NOTE: Disabling denial clause 2477.

given #79 (T,wt=9): 2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].

given #80 (T,wt=9): 2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].

given #81 (A,wt=31): 2479 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_demod(1348),demod(2419(1),2419(5),2419(9),2425(5),2419(11),2425(12),2419(12),2419(15),2419(18))].

given #82 (F,wt=10): 2563 c(x) v c(x v y) = c(x).  [para(2425(a,1),2552(a,1,2,1,2))].

given #83 (F,wt=11): 2568 x v (c(y v c(x)) v x) = x.  [para(2542(a,1),2564(a,1,1)),demod(2542(10))].

given #84 (T,wt=13): 2534 (c(x v y) v c(y)) v c(y) = c(y).  [para(2425(a,1),2520(a,1,1,1,1,1))].

given #85 (T,wt=13): 2580 c(x) v (c(y v x) v c(x)) = c(x).  [para(2425(a,1),2568(a,1,2,1,1,2))].

given #86 (A,wt=33): 2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].

given #87 (F,wt=9): 2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].

given #88 (F,wt=9): 2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].

given #89 (T,wt=10): 2617 c(x v y) v c(y) = c(y).  [para(2425(a,1),2608(a,1,1,1,2))].

given #90 (T,wt=9): 2625 x v (y v x) = y v x.  [para(2617(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].

given #91 (A,wt=25): 2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].

given #92 (F,wt=9): 2626 (x v y) v y = x v y.  [para(2617(a,1),2567(a,1,2,1)),demod(2425(3))].

given #93 (F,wt=10): 2624 c(x) v c(y v x) = c(x).  [para(2425(a,1),2619(a,1,2,1,2))].

given #94 (T,wt=12): 2609 c((c(x) v y) v c(z)) v x = x.  [back_demod(2586),demod(2594(14))].

given #95 (T,wt=11): 2633 c((c(x) v y) v z) v x = x.  [para(2425(a,1),2609(a,1,1,1,2))].

given #96 (A,wt=32): 2505 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_demod(987),demod(2419(3),2419(6),2419(13),2425(11),2419(15),2425(16),2419(16),2425(10),2419(17))].

given #97 (F,wt=11): 2648 x v c((c(x) v y) v z) = x.  [para(2633(a,1),2564(a,1,1)),demod(2633(10))].

given #98 (F,wt=11): 2652 c((x v c(y)) v z) v y = y.  [para(2625(a,1),2633(a,1,1,1,1))].

given #99 (T,wt=11): 2653 c(x v (c(y) v z)) v y = y.  [para(2625(a,1),2633(a,1,1,1))].

given #100 (T,wt=11): 2683 x v c((y v c(x)) v z) = x.  [para(2625(a,1),2648(a,1,2,1,1))].

given #101 (A,wt=30): 2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].

given #102 (F,wt=11): 2684 x v c(y v (c(x) v z)) = x.  [para(2625(a,1),2648(a,1,2,1))].

given #103 (F,wt=11): 2690 c(x v (y v c(z))) v z = z.  [para(2625(a,1),2652(a,1,1,1))].

given #104 (T,wt=11): 2708 x v c(y v (z v c(x))) = x.  [para(2625(a,1),2683(a,1,2,1))].

given #105 (T,wt=12): 2644 c((x v y) v z) v c(x) = c(x).  [para(2425(a,1),2633(a,1,1,1,1,1))].

given #106 (A,wt=36): 2578 c(x) v (c(c(c(c(x) v c(y)) v z) v c(c(x) v c(y))) v c(c(c(x) v c(y)) v z)) = c(x) v c(y).  [para(2567(a,1),2479(a,1,2,1,2,1,1,1,2,1)),demod(2527(26),2425(22))].

given #107 (F,wt=12): 2678 c(x) v c((x v y) v z) = c(x).  [para(2425(a,1),2648(a,1,2,1,1,1))].

given #108 (F,wt=12): 2687 c((x v y) v z) v c(y) = c(y).  [para(2425(a,1),2652(a,1,1,1,1,2))].

given #109 (T,wt=12): 2694 c(x v (y v z)) v c(y) = c(y).  [para(2425(a,1),2653(a,1,1,1,2,1))].

given #110 (T,wt=12): 2707 c(x) v c((y v x) v z) = c(x).  [para(2425(a,1),2683(a,1,2,1,1,2))].

given #111 (A,wt=16): 2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].

given #112 (F,wt=12): 2731 c(x) v c(y v (x v z)) = c(x).  [para(2425(a,1),2684(a,1,2,1,2,1))].

given #113 (F,wt=12): 2740 c(x v (y v z)) v c(z) = c(z).  [para(2425(a,1),2690(a,1,1,1,2,2))].

given #114 (T,wt=12): 2748 c(x) v c(y v (z v x)) = c(x).  [para(2425(a,1),2708(a,1,2,1,2,2))].

given #115 (T,wt=13): 2646 c(c(x) v y) v (x v z) = x v z.  [para(2516(a,1),2633(a,1,1,1,1))].

given #116 (A,wt=20): 2595 x v c(c(c(y v c(x)) v c(c(x) v z)) v c(u)) = x.  [para(2489(a,1),2564(a,1,1)),demod(2594(32),2591(24))].

given #117 (F,wt=13): 2651 c(c(x) v y) v (z v x) = z v x.  [para(2617(a,1),2633(a,1,1,1,1))].

given #118 (F,wt=13): 2679 (x v y) v c(c(x) v z) = x v y.  [para(2516(a,1),2648(a,1,2,1,1))].

given #119 (T,wt=13): 2682 (x v y) v c(c(y) v z) = x v y.  [para(2617(a,1),2648(a,1,2,1,1))].

given #120 (T,wt=13): 2696 c(x v c(y)) v (y v z) = y v z.  [para(2516(a,1),2653(a,1,1,1,2))].

given #121 (A,wt=20): 2596 c(c(c(c(x) v y) v c(c(x) v z)) v c(u)) v x = x.  [para(2564(a,1),2489(a,1,1,1,1,1,1,1)),demod(2594(20))].

given #122 (F,wt=13): 2700 c(x v c(y)) v (z v y) = z v y.  [para(2617(a,1),2653(a,1,1,1,2))].

given #123 (F,wt=13): 2732 (x v y) v c(z v c(x)) = x v y.  [para(2516(a,1),2684(a,1,2,1,2))].

given #124 (T,wt=13): 2735 (x v y) v c(z v c(y)) = x v y.  [para(2617(a,1),2684(a,1,2,1,2))].

given #125 (T,wt=13): 2749 x v ((x v y) v z) = (x v y) v z.  [para(2644(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].

given #126 (A,wt=15): 2600 (c(x v c(y)) v c(c(y) v z)) v y = y.  [para(2567(a,1),2489(a,1,1,1)),demod(2425(9),2594(16))].

given #127 (F,wt=13): 2750 ((x v y) v z) v x = (x v y) v z.  [para(2644(a,1),2567(a,1,2,1)),demod(2425(4))].

given #128 (F,wt=13): 2765 x v ((y v x) v z) = (y v x) v z.  [para(2687(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].

given #129 (T,wt=13): 2766 ((x v y) v z) v y = (x v y) v z.  [para(2687(a,1),2567(a,1,2,1)),demod(2425(4))].

given #130 (T,wt=13): 2771 x v (y v (x v z)) = y v (x v z).  [para(2694(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].

given #131 (A,wt=22): 2602 c(c(x v c(c(x v y) v z)) v c(u)) v (x v y) = x v y.  [para(2563(a,1),2489(a,1,1,1,1,1,1,1)),demod(2425(2),2594(20))].

given #132 (F,wt=13): 2772 (x v (y v z)) v y = x v (y v z).  [para(2694(a,1),2567(a,1,2,1)),demod(2425(4))].

given #133 (F,wt=13): 2798 x v (y v (z v x)) = y v (z v x).  [para(2740(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].

given #134 (T,wt=13): 2799 (x v (y v z)) v z = x v (y v z).  [para(2740(a,1),2567(a,1,2,1)),demod(2425(4))].

given #135 (T,wt=13): 2806 c(((c(x) v y) v z) v u) v x = x.  [para(2633(a,1),2646(a,1,2)),demod(2425(5),2633(11))].

given #136 (A,wt=22): 2610 c(c(c(x v c(y v z)) v y) v c(u)) v (y v z) = y v z.  [back_demod(2585),demod(2594(23))].

given #137 (F,wt=13): 2809 c(((x v c(y)) v z) v u) v y = y.  [para(2652(a,1),2646(a,1,2)),demod(2425(5),2652(11))].

given #138 (F,wt=13): 2812 c((x v (c(y) v z)) v u) v y = y.  [para(2653(a,1),2646(a,1,2)),demod(2425(5),2653(11))].

given #139 (T,wt=13): 2815 c((x v (y v c(z))) v u) v z = z.  [para(2690(a,1),2646(a,1,2)),demod(2425(5),2690(11))].

given #140 (T,wt=13): 2870 x v c(((c(x) v y) v z) v u) = x.  [para(2633(a,1),2679(a,1,1)),demod(2425(5),2633(11))].

given #141 (A,wt=19): 2611 c(c(c(x v c(y)) v c(c(y) v z)) v u) v y = y.  [back_demod(2583),demod(2594(19))].

given #142 (F,wt=13): 2872 x v c(((y v c(x)) v z) v u) = x.  [para(2652(a,1),2679(a,1,1)),demod(2425(5),2652(11))].

given #143 (F,wt=13): 2874 x v c((y v (c(x) v z)) v u) = x.  [para(2653(a,1),2679(a,1,1)),demod(2425(5),2653(11))].

given #144 (T,wt=13): 2876 x v c((y v (z v c(x))) v u) = x.  [para(2690(a,1),2679(a,1,1)),demod(2425(5),2690(11))].

given #145 (T,wt=13): 2897 c(x v ((c(y) v z) v u)) v y = y.  [para(2633(a,1),2696(a,1,2)),demod(2425(5),2633(11))].

given #146 (A,wt=14): 2647 c(x v y) v (c(x) v z) = c(x) v z.  [para(2521(a,1),2633(a,1,1,1,1))].

given #147 (F,wt=13): 2899 c(x v ((y v c(z)) v u)) v z = z.  [para(2652(a,1),2696(a,1,2)),demod(2425(5),2652(11))].

given #148 (F,wt=13): 2901 c(x v (y v (c(z) v u))) v z = z.  [para(2653(a,1),2696(a,1,2)),demod(2425(5),2653(11))].

given #149 (T,wt=13): 2903 c(x v (y v (z v c(u)))) v u = u.  [para(2690(a,1),2696(a,1,2)),demod(2425(5),2690(11))].

given #150 (T,wt=13): 2961 x v c(y v ((c(x) v z) v u)) = x.  [para(2633(a,1),2732(a,1,1)),demod(2425(5),2633(11))].

given #151 (A,wt=14): 2650 c(x v y) v (z v c(x)) = z v c(x).  [para(2608(a,1),2633(a,1,1,1,1))].

given #152 (F,wt=13): 2962 x v c(y v ((z v c(x)) v u)) = x.  [para(2652(a,1),2732(a,1,1)),demod(2425(5),2652(11))].

given #153 (F,wt=13): 2963 x v c(y v (z v (c(x) v u))) = x.  [para(2653(a,1),2732(a,1,1)),demod(2425(5),2653(11))].

given #154 (T,wt=13): 2964 x v c(y v (z v (u v c(x)))) = x.  [para(2690(a,1),2732(a,1,1)),demod(2425(5),2690(11))].

given #155 (T,wt=14): 2680 (c(x) v y) v c(x v z) = c(x) v y.  [para(2521(a,1),2648(a,1,2,1,1))].

given #156 (A,wt=18): 2654 c(x v y) v ((c(x) v z) v u) = (c(x) v z) v u.  [para(2633(a,1),2633(a,1,1,1,1))].

given #157 (F,wt=14): 2681 (x v c(y)) v c(y v z) = x v c(y).  [para(2608(a,1),2648(a,1,2,1,1))].

given #158 (F,wt=14): 2697 c(x v y) v (c(y) v z) = c(y) v z.  [para(2521(a,1),2653(a,1,1,1,2))].

given #159 (T,wt=14): 2699 c(x v y) v (z v c(y)) = z v c(y).  [para(2608(a,1),2653(a,1,1,1,2))].

given #160 (T,wt=14): 2733 (c(x) v y) v c(z v x) = c(x) v y.  [para(2521(a,1),2684(a,1,2,1,2))].

given #161 (A,wt=29): 2656 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(2505(a,1),2516(a,1,1,1)),demod(2425(2),2425(10),2425(19))].

given #162 (F,wt=14): 2734 (x v c(y)) v c(z v y) = x v c(y).  [para(2608(a,1),2684(a,1,2,1,2))].

given #163 (F,wt=14): 2817 c(((x v y) v z) v u) v c(x) = c(x).  [para(2644(a,1),2646(a,1,2)),demod(2425(4),2644(11))].

given #164 (T,wt=14): 2819 c(((x v y) v z) v u) v c(y) = c(y).  [para(2687(a,1),2646(a,1,2)),demod(2425(4),2687(11))].

given #165 (T,wt=14): 2821 c((x v (y v z)) v u) v c(y) = c(y).  [para(2694(a,1),2646(a,1,2)),demod(2425(4),2694(11))].

given #166 (A,wt=20): 2661 c(x) v c(c(c(y v x) v c(x v z)) v c(u)) = c(x).  [para(2505(a,1),2564(a,1,1)),demod(2655(30))].

given #167 (F,wt=14): 2823 c((x v (y v z)) v u) v c(z) = c(z).  [para(2740(a,1),2646(a,1,2)),demod(2425(4),2740(11))].

given #168 (F,wt=14): 2878 c(x) v c(((x v y) v z) v u) = c(x).  [para(2644(a,1),2679(a,1,1)),demod(2425(5),2644(11))].

given #169 (T,wt=14): 2880 c(x) v c(((y v x) v z) v u) = c(x).  [para(2687(a,1),2679(a,1,1)),demod(2425(5),2687(11))].

given #170 (T,wt=14): 2882 c(x) v c((y v (x v z)) v u) = c(x).  [para(2694(a,1),2679(a,1,1)),demod(2425(5),2694(11))].

given #171 (A,wt=29): 2663 (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(2505(a,1),2567(a,1,2,1)),demod(2425(10))].

given #172 (F,wt=14): 2884 c(x) v c((y v (z v x)) v u) = c(x).  [para(2740(a,1),2679(a,1,1)),demod(2425(5),2740(11))].

given #173 (F,wt=14): 2904 c(x v ((y v z) v u)) v c(y) = c(y).  [para(2644(a,1),2696(a,1,2)),demod(2425(4),2644(11))].

given #174 (T,wt=14): 2905 c(x v ((y v z) v u)) v c(z) = c(z).  [para(2687(a,1),2696(a,1,2)),demod(2425(4),2687(11))].

given #175 (T,wt=14): 2906 c(x v (y v (z v u))) v c(z) = c(z).  [para(2694(a,1),2696(a,1,2)),demod(2425(4),2694(11))].

given #176 (A,wt=17): 2664 c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2505(a,1),2608(a,1)),flip(a)].

given #177 (F,wt=14): 2907 c(x v (y v (z v u))) v c(u) = c(u).  [para(2740(a,1),2696(a,1,2)),demod(2425(4),2740(11))].

given #178 (F,wt=14): 2965 c(x) v c(y v ((x v z) v u)) = c(x).  [para(2644(a,1),2732(a,1,1)),demod(2425(5),2644(11))].

given #179 (T,wt=14): 2966 c(x) v c(y v ((z v x) v u)) = c(x).  [para(2687(a,1),2732(a,1,1)),demod(2425(5),2687(11))].

given #180 (T,wt=14): 2967 c(x) v c(y v (z v (x v u))) = c(x).  [para(2694(a,1),2732(a,1,1)),demod(2425(5),2694(11))].

given #181 (A,wt=15): 2668 (c(x v y) v c(y v z)) v c(y) = c(y).  [para(2619(a,1),2505(a,1,1,1)),demod(2425(7),2664(14))].

given #182 (F,wt=14): 2968 c(x) v c(y v (z v (u v x))) = c(x).  [para(2740(a,1),2732(a,1,1)),demod(2425(5),2740(11))].

given #183 (F,wt=15): 2780 c(c(x v y) v x) v c(x v y) = c(x).  [para(2563(a,1),2594(a,1,1,2,1,1,1,2,1)),demod(2425(2),2425(4),2709(9),2425(9))].

given #184 (T,wt=13): 4078 c(x v c(x v y)) v x = x v y.  [para(2516(a,1),2780(a,1,1,1,1,1)),demod(2425(2),2516(8),2425(6),2425(8))].

given #185 (T,wt=9): 4123 c(x) v x = x v c(x).  [para(2619(a,1),4078(a,1,1,1))].

given #186 (A,wt=20): 2671 c(c(c(x v y) v c(z v y)) v c(u)) v c(y) = c(y).  [para(2625(a,1),2505(a,1,1,1,1,1,2,1)),demod(2664(21))].

given #187 (F,wt=9): 4167 c(x v c(x)) v y = y.  [para(4123(a,1),2815(a,1,1,1,1)),demod(4128(6),4164(4),4166(3))].

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

% Proof 7 at 0.80 (+ 0.02) seconds: 1.
% Length of proof is 110.
% Level of proof is 27.
% Maximum clause weight is 37.
% Given clauses 187.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
36 c20 v c(c20) != c19 v c(c19) # answer(1).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2563 c(x) v c(x v y) = c(x).  [para(2425(a,1),2552(a,1,2,1,2))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2586 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(2516(a,1),2489(a,1,1,1,1,1)),demod(2425(4))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2609 c((c(x) v y) v c(z)) v x = x.  [back_demod(2586),demod(2594(14))].
2617 c(x v y) v c(y) = c(y).  [para(2425(a,1),2608(a,1,1,1,2))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2625 x v (y v x) = y v x.  [para(2617(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2633 c((c(x) v y) v z) v x = x.  [para(2425(a,1),2609(a,1,1,1,2))].
2646 c(c(x) v y) v (x v z) = x v z.  [para(2516(a,1),2633(a,1,1,1,1))].
2648 x v c((c(x) v y) v z) = x.  [para(2633(a,1),2564(a,1,1)),demod(2633(10))].
2652 c((x v c(y)) v z) v y = y.  [para(2625(a,1),2633(a,1,1,1,1))].
2653 c(x v (c(y) v z)) v y = y.  [para(2625(a,1),2633(a,1,1,1))].
2679 (x v y) v c(c(x) v z) = x v y.  [para(2516(a,1),2648(a,1,2,1,1))].
2683 x v c((y v c(x)) v z) = x.  [para(2625(a,1),2648(a,1,2,1,1))].
2684 x v c(y v (c(x) v z)) = x.  [para(2625(a,1),2648(a,1,2,1))].
2690 c(x v (y v c(z))) v z = z.  [para(2625(a,1),2652(a,1,1,1))].
2694 c(x v (y v z)) v c(y) = c(y).  [para(2425(a,1),2653(a,1,1,1,2,1))].
2708 x v c(y v (z v c(x))) = x.  [para(2625(a,1),2683(a,1,2,1))].
2709 x v c(c(c(y) v x) v c(x v z)) = c(c(c(y) v x) v c(x v z)).  [para(2425(a,1),2527(a,1,1)),demod(2425(3),2425(5),2425(11),2425(13))].
2732 (x v y) v c(z v c(x)) = x v y.  [para(2516(a,1),2684(a,1,2,1,2))].
2740 c(x v (y v z)) v c(z) = c(z).  [para(2425(a,1),2690(a,1,1,1,2,2))].
2771 x v (y v (x v z)) = y v (x v z).  [para(2694(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].
2780 c(c(x v y) v x) v c(x v y) = c(x).  [para(2563(a,1),2594(a,1,1,2,1,1,1,2,1)),demod(2425(2),2425(4),2709(9),2425(9))].
2799 (x v (y v z)) v z = x v (y v z).  [para(2740(a,1),2567(a,1,2,1)),demod(2425(4))].
2815 c((x v (y v c(z))) v u) v z = z.  [para(2690(a,1),2646(a,1,2)),demod(2425(5),2690(11))].
2876 x v c((y v (z v c(x))) v u) = x.  [para(2690(a,1),2679(a,1,1)),demod(2425(5),2690(11))].
4078 c(x v c(x v y)) v x = x v y.  [para(2516(a,1),2780(a,1,1,1,1,1)),demod(2425(2),2516(8),2425(6),2425(8))].
4123 c(x) v x = x v c(x).  [para(2619(a,1),4078(a,1,1,1))].
4125 x v (y v c(x)) = x v c(x).  [para(2708(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].
4128 (x v y) v c(x v y) = (x v y) v c(x).  [para(2732(a,1),4078(a,1,1,1)),demod(4123(4))].
4164 (x v y) v c(x) = x v c(x).  [para(4123(a,1),2771(a,1,2)),demod(4128(4),4125(4),4123(6),4128(6)),flip(a)].
4166 (x v c(x)) v y = x v c(x).  [para(4123(a,1),2799(a,1,1)),demod(4128(4),4164(3),4123(7),4128(7),4164(6))].
4167 c(x v c(x)) v y = y.  [para(4123(a,1),2815(a,1,1,1,1)),demod(4128(6),4164(4),4166(3))].
4168 x v c(y v c(y)) = x.  [para(4123(a,1),2876(a,1,2,1,1)),demod(4128(6),4164(4),4166(3))].
4241 x v c(x) = y v c(y).  [para(4167(a,1),2780(a,1,1,1,1,1)),demod(4168(5),2425(2),4167(4),2425(6))].
4242 $F # answer(1).  [resolve(4241,a,36,a)].

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

NOTE: Disabling denial clause 36.

given #188 (F,wt=9): 4168 x v c(y v c(y)) = x.  [para(4123(a,1),2876(a,1,2,1,1)),demod(4128(6),4164(4),4166(3))].

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

% Proof 8 at 0.80 (+ 0.02) seconds: 0.
% Length of proof is 112.
% Level of proof is 27.
% Maximum clause weight is 37.
% Given clauses 188.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
37 c22 ^ c(c22) != c21 ^ c(c21) # answer(0).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2475 c(c(c22) v c22) != c(c(c21) v c21) # answer(0).  [back_demod(37),demod(2409(4),2425(5),2409(9),2425(10))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2563 c(x) v c(x v y) = c(x).  [para(2425(a,1),2552(a,1,2,1,2))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2586 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(2516(a,1),2489(a,1,1,1,1,1)),demod(2425(4))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2609 c((c(x) v y) v c(z)) v x = x.  [back_demod(2586),demod(2594(14))].
2617 c(x v y) v c(y) = c(y).  [para(2425(a,1),2608(a,1,1,1,2))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2625 x v (y v x) = y v x.  [para(2617(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2633 c((c(x) v y) v z) v x = x.  [para(2425(a,1),2609(a,1,1,1,2))].
2646 c(c(x) v y) v (x v z) = x v z.  [para(2516(a,1),2633(a,1,1,1,1))].
2648 x v c((c(x) v y) v z) = x.  [para(2633(a,1),2564(a,1,1)),demod(2633(10))].
2652 c((x v c(y)) v z) v y = y.  [para(2625(a,1),2633(a,1,1,1,1))].
2653 c(x v (c(y) v z)) v y = y.  [para(2625(a,1),2633(a,1,1,1))].
2679 (x v y) v c(c(x) v z) = x v y.  [para(2516(a,1),2648(a,1,2,1,1))].
2683 x v c((y v c(x)) v z) = x.  [para(2625(a,1),2648(a,1,2,1,1))].
2684 x v c(y v (c(x) v z)) = x.  [para(2625(a,1),2648(a,1,2,1))].
2690 c(x v (y v c(z))) v z = z.  [para(2625(a,1),2652(a,1,1,1))].
2694 c(x v (y v z)) v c(y) = c(y).  [para(2425(a,1),2653(a,1,1,1,2,1))].
2708 x v c(y v (z v c(x))) = x.  [para(2625(a,1),2683(a,1,2,1))].
2709 x v c(c(c(y) v x) v c(x v z)) = c(c(c(y) v x) v c(x v z)).  [para(2425(a,1),2527(a,1,1)),demod(2425(3),2425(5),2425(11),2425(13))].
2732 (x v y) v c(z v c(x)) = x v y.  [para(2516(a,1),2684(a,1,2,1,2))].
2740 c(x v (y v z)) v c(z) = c(z).  [para(2425(a,1),2690(a,1,1,1,2,2))].
2771 x v (y v (x v z)) = y v (x v z).  [para(2694(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].
2780 c(c(x v y) v x) v c(x v y) = c(x).  [para(2563(a,1),2594(a,1,1,2,1,1,1,2,1)),demod(2425(2),2425(4),2709(9),2425(9))].
2799 (x v (y v z)) v z = x v (y v z).  [para(2740(a,1),2567(a,1,2,1)),demod(2425(4))].
2815 c((x v (y v c(z))) v u) v z = z.  [para(2690(a,1),2646(a,1,2)),demod(2425(5),2690(11))].
2876 x v c((y v (z v c(x))) v u) = x.  [para(2690(a,1),2679(a,1,1)),demod(2425(5),2690(11))].
4078 c(x v c(x v y)) v x = x v y.  [para(2516(a,1),2780(a,1,1,1,1,1)),demod(2425(2),2516(8),2425(6),2425(8))].
4123 c(x) v x = x v c(x).  [para(2619(a,1),4078(a,1,1,1))].
4125 x v (y v c(x)) = x v c(x).  [para(2708(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].
4128 (x v y) v c(x v y) = (x v y) v c(x).  [para(2732(a,1),4078(a,1,1,1)),demod(4123(4))].
4163 c(c22 v c(c22)) != c(c21 v c(c21)) # answer(0).  [back_demod(2475),demod(4123(4),4123(9))].
4164 (x v y) v c(x) = x v c(x).  [para(4123(a,1),2771(a,1,2)),demod(4128(4),4125(4),4123(6),4128(6)),flip(a)].
4166 (x v c(x)) v y = x v c(x).  [para(4123(a,1),2799(a,1,1)),demod(4128(4),4164(3),4123(7),4128(7),4164(6))].
4167 c(x v c(x)) v y = y.  [para(4123(a,1),2815(a,1,1,1,1)),demod(4128(6),4164(4),4166(3))].
4168 x v c(y v c(y)) = x.  [para(4123(a,1),2876(a,1,2,1,1)),demod(4128(6),4164(4),4166(3))].
4243 c(x v c(x)) = c(y v c(y)).  [para(4168(a,1),4167(a,1))].
4244 $F # answer(0).  [resolve(4243,a,4163,a)].

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

NOTE: Disabling denial clause 4163.

given #189 (T,wt=9): 4241 x v c(x) = y v c(y).  [para(4167(a,1),2780(a,1,1,1,1,1)),demod(4168(5),2425(2),4167(4),2425(6))].

given #190 (T,wt=11): 4124 x v (c(x) v y) = x v c(x).  [para(2684(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #191 (A,wt=33): 2673 c(c(x) v y) v (c(c(z v x) v c(x v u)) v c(v)) = c(c(z v x) v c(x v u)) v c(v).  [para(2505(a,1),2633(a,1,1,1,1))].

given #192 (F,wt=11): 4125 x v (y v c(x)) = x v c(x).  [para(2708(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #193 (F,wt=11): 4126 c(x) v (x v y) = x v c(x).  [para(2731(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #194 (T,wt=11): 4127 c(x) v (y v x) = x v c(x).  [para(2748(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #195 (T,wt=11): 4164 (x v y) v c(x) = x v c(x).  [para(4123(a,1),2771(a,1,2)),demod(4128(4),4125(4),4123(6),4128(6)),flip(a)].

given #196 (A,wt=20): 2675 c(c(c(x v y) v c(x v z)) v c(u)) v c(x) = c(x).  [back_demod(2662),demod(2664(18))].

given #197 (F,wt=11): 4165 x v (y v c(y)) = y v c(y).  [para(4123(a,1),2798(a,1,2)),demod(4128(4),4164(3),4123(7),4128(7),4164(6))].

given #198 (F,wt=11): 4166 (x v c(x)) v y = x v c(x).  [para(4123(a,1),2799(a,1,1)),demod(4128(4),4164(3),4123(7),4128(7),4164(6))].

given #199 (T,wt=11): 4243 c(x v c(x)) = c(y v c(y)).  [para(4168(a,1),4167(a,1))].

given #200 (T,wt=11): 4261 (x v y) v c(y) = y v c(y).  [para(4124(a,1),2765(a,1,2)),demod(4247(4),4125(4),4124(7),4247(6)),flip(a)].

given #201 (A,wt=19): 2676 c(c(c(x v y) v c(y v z)) v u) v c(y) = c(y).  [back_demod(2655),demod(2664(17))].

given #202 (F,wt=11): 4408 (c(x) v y) v x = x v c(x).  [para(4125(a,1),2646(a,1)),demod(2425(7),4123(6),4399(6),2425(7),4124(6))].

given #203 (F,wt=11): 4411 (x v c(y)) v y = y v c(y).  [para(4125(a,1),2696(a,1)),demod(2425(7),4123(6),4400(6),2425(7),4125(6))].

given #204 (T,wt=13): 4080 c(x v c(y v x)) v x = y v x.  [para(2617(a,1),2780(a,1,1,1,1,1)),demod(2425(2),2617(8),2425(6),2425(8))].

given #205 (T,wt=13): 4122 x v c(c(x v y) v x) = x v y.  [para(2780(a,1),2780(a,1,1,1)),demod(2425(2),2425(8))].

given #206 (A,wt=18): 2685 ((c(x) v y) v z) v c(x v u) = (c(x) v y) v z.  [para(2633(a,1),2648(a,1,2,1,1))].

given #207 (F,wt=13): 4140 x v ((c(x) v y) v z) = x v c(x).  [para(2961(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #208 (F,wt=13): 4141 x v ((y v c(x)) v z) = x v c(x).  [para(2962(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #209 (T,wt=13): 4142 x v (y v (c(x) v z)) = x v c(x).  [para(2963(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #210 (T,wt=13): 4143 x v (y v (z v c(x))) = x v c(x).  [para(2964(a,1),4078(a,1,1,1)),demod(4123(2)),flip(a)].

given #211 (A,wt=18): 2691 c(x v y) v ((z v c(x)) v u) = (z v c(x)) v u.  [para(2652(a,1),2633(a,1,1,1,1))].

given #212 (F,wt=13): 4154 c(x) v ((x v y) v z) = x v c(x).  [para(2965(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #213 (F,wt=13): 4155 c(x) v ((y v x) v z) = x v c(x).  [para(2966(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #214 (T,wt=13): 4156 c(x) v (y v (x v z)) = x v c(x).  [para(2967(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #215 (T,wt=13): 4158 c(x) v (y v (z v x)) = x v c(x).  [para(2968(a,1),4078(a,1,1,1)),demod(2425(2)),flip(a)].

given #216 (A,wt=18): 2692 ((x v c(y)) v z) v c(y v u) = (x v c(y)) v z.  [para(2652(a,1),2648(a,1,2,1,1))].

given #217 (F,wt=13): 4274 (x v y) v (c(y) v z) = y v c(y).  [para(2697(a,1),4124(a,1,2)),demod(4247(8),4261(7))].

given #218 (F,wt=13): 4275 (x v y) v (z v c(y)) = y v c(y).  [para(2699(a,1),4124(a,1,2)),demod(4247(8),4261(7))].

given #219 (T,wt=13): 4409 (c(x) v y) v (x v z) = x v c(x).  [para(2679(a,1),4125(a,1,2)),demod(4399(10),4408(7))].

given #220 (T,wt=13): 4410 (c(x) v y) v (z v x) = x v c(x).  [para(2682(a,1),4125(a,1,2)),demod(4399(10),4408(7))].

given #221 (A,wt=18): 2701 c(x v y) v (z v (c(x) v u)) = z v (c(x) v u).  [para(2653(a,1),2633(a,1,1,1,1))].

given #222 (F,wt=13): 4433 (x v (y v c(z))) v z = z v c(z).  [back_demod(4285),demod(4411(7))].

given #223 (F,wt=13): 4435 (x v c(y)) v (z v y) = y v c(y).  [back_demod(4260),demod(4411(7))].

given #224 (T,wt=13): 4436 (x v c(y)) v (y v z) = y v c(y).  [back_demod(4259),demod(4411(7))].

given #225 (T,wt=13): 4443 ((c(x) v y) v z) v x = x v c(x).  [para(2633(a,1),4164(a,1,1)),demod(2425(5),4140(4),2425(11),4123(10),4405(10),2425(7)),flip(a)].

given #226 (A,wt=18): 2702 c(x v y) v ((c(y) v z) v u) = (c(y) v z) v u.  [para(2633(a,1),2653(a,1,1,1,2))].

given #227 (F,wt=13): 4445 (x v (c(y) v z)) v y = y v c(y).  [para(2653(a,1),4164(a,1,1)),demod(2425(5),4142(4),2425(11),4123(10),4407(10),2425(7)),flip(a)].

given #228 (F,wt=13): 4446 ((x v y) v z) v c(x) = x v c(x).  [para(2644(a,1),4164(a,1,1)),demod(2425(5),4154(4),2425(9),4123(8),4405(8)),flip(a)].

given #229 (T,wt=13): 4447 (x v (y v z)) v c(y) = y v c(y).  [para(2694(a,1),4164(a,1,1)),demod(2425(5),4156(4),2425(9),4123(8),4407(8)),flip(a)].

given #230 (T,wt=13): 4451 ((x v y) v z) v c(y) = y v c(y).  [para(2765(a,1),4164(a,1,1))].

given #231 (A,wt=18): 2703 (x v (c(y) v z)) v c(y v u) = x v (c(y) v z).  [para(2653(a,1),2648(a,1,2,1,1))].

given #232 (F,wt=13): 4452 (x v (y v z)) v c(z) = z v c(z).  [para(2798(a,1),4164(a,1,1))].

given #233 (F,wt=13): 4611 ((x v c(y)) v z) v y = y v c(y).  [para(2765(a,1),4408(a,1,1))].

given #234 (T,wt=13): 4613 x v c(c(y v x) v x) = y v x.  [para(2625(a,1),4122(a,1,2,1,1,1)),demod(2625(7))].

given #235 (T,wt=13): 4752 (x v y) v (c(x) v z) = x v c(x).  [para(4142(a,1),2749(a,1)),flip(a)].

given #236 (A,wt=18): 2704 c(x v y) v ((z v c(y)) v u) = (z v c(y)) v u.  [para(2652(a,1),2653(a,1,1,1,2))].

given #237 (F,wt=13): 4777 (x v y) v (z v c(x)) = x v c(x).  [para(4143(a,1),2749(a,1)),flip(a)].

given #238 (F,wt=15): 2824 c((c(x) v y) v z) v (x v u) = x v u.  [para(2646(a,1),2646(a,1,2)),demod(2425(4),2646(11))].

given #239 (T,wt=15): 2825 x v (c(y v c(x)) v c(c(x) v z)) = x.  [para(1757(a,1),2595(a,1,2,1)),demod(2425(9))].

given #240 (T,wt=15): 2869 c((c(x) v y) v z) v (u v x) = u v x.  [para(2651(a,1),2646(a,1,2)),demod(2425(4),2651(11))].

given #241 (A,wt=18): 2705 c(x v y) v (z v (c(y) v u)) = z v (c(y) v u).  [para(2653(a,1),2653(a,1,1,1,2))].

given #242 (F,wt=15): 2886 (x v y) v c((c(x) v z) v u) = x v y.  [para(2646(a,1),2679(a,1,1)),demod(2425(5),2646(11))].

given #243 (F,wt=15): 2887 (x v y) v c((c(y) v z) v u) = x v y.  [para(2651(a,1),2679(a,1,1)),demod(2425(5),2651(11))].

given #244 (T,wt=15): 2908 c((x v c(y)) v z) v (y v u) = y v u.  [para(2696(a,1),2646(a,1,2)),demod(2425(4),2696(11))].

given #245 (T,wt=15): 2909 c(x v (c(y) v z)) v (y v u) = y v u.  [para(2646(a,1),2696(a,1,2)),demod(2425(4),2646(11))].

given #246 (A,wt=28): 2711 c(x v y) v c(c(c(z) v c(x v y)) v x) = c(c(c(z) v c(x v y)) v x).  [para(2516(a,1),2527(a,1,2,1,2,1)),demod(2425(9),2516(19),2425(17))].

given #247 (F,wt=14): 5662 c(x v y) v c(y v x) = c(y v x).  [para(2619(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(8),2624(9),2425(7))].

% Operation v is commutative; redundancy checks enabled.

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

% Proof 9 at 1.31 (+ 0.04) seconds: commutativity_meet.
% Length of proof is 82.
% Level of proof is 23.
% Maximum clause weight is 37.
% Given clauses 247.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
35 c18 v c17 != c17 v c18 # answer(commutativity_meet).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2624 c(x) v c(y v x) = c(x).  [para(2425(a,1),2619(a,1,2,1,2))].
2711 c(x v y) v c(c(c(z) v c(x v y)) v x) = c(c(c(z) v c(x v y)) v x).  [para(2516(a,1),2527(a,1,2,1,2,1)),demod(2425(9),2516(19),2425(17))].
5662 c(x v y) v c(y v x) = c(y v x).  [para(2619(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(8),2624(9),2425(7))].
5783 (x v y) v (y v x) = y v x.  [para(5662(a,1),2516(a,1,1,1)),demod(2425(3),2425(4),2425(6))].
5785 x v y = y v x.  [para(5662(a,1),2567(a,1,2,1)),demod(2425(4),5783(3))].
5786 $F # answer(commutativity_meet).  [resolve(5785,a,35,a)].

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

NOTE: Disabling denial clause 35.

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

% Proof 10 at 1.31 (+ 0.04) seconds: commutativity_join.
% Length of proof is 82.
% Level of proof is 23.
% Maximum clause weight is 37.
% Given clauses 247.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
34 c16 v c15 != c15 v c16 # answer(commutativity_join).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2624 c(x) v c(y v x) = c(x).  [para(2425(a,1),2619(a,1,2,1,2))].
2711 c(x v y) v c(c(c(z) v c(x v y)) v x) = c(c(c(z) v c(x v y)) v x).  [para(2516(a,1),2527(a,1,2,1,2,1)),demod(2425(9),2516(19),2425(17))].
5662 c(x v y) v c(y v x) = c(y v x).  [para(2619(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(8),2624(9),2425(7))].
5783 (x v y) v (y v x) = y v x.  [para(5662(a,1),2516(a,1,1,1)),demod(2425(3),2425(4),2425(6))].
5785 x v y = y v x.  [para(5662(a,1),2567(a,1,2,1)),demod(2425(4),5783(3))].
5787 $F # answer(commutativity_join).  [resolve(5785,a,34,a)].

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

NOTE: Disabling denial clause 34.

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

% Proof 11 at 1.34 (+ 0.04) seconds: OM.
% Length of proof is 88.
% Level of proof is 24.
% Maximum clause weight is 37.
% Given clauses 247.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
27 c3 v (c(c3) ^ (c3 v c4)) != c3 v c4 # answer(OM).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2476 c3 v c(c3 v c(c3 v c4)) != c3 v c4 # answer(OM).  [back_demod(27),demod(2409(7),2425(4))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2563 c(x) v c(x v y) = c(x).  [para(2425(a,1),2552(a,1,2,1,2))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2624 c(x) v c(y v x) = c(x).  [para(2425(a,1),2619(a,1,2,1,2))].
2709 x v c(c(c(y) v x) v c(x v z)) = c(c(c(y) v x) v c(x v z)).  [para(2425(a,1),2527(a,1,1)),demod(2425(3),2425(5),2425(11),2425(13))].
2711 c(x v y) v c(c(c(z) v c(x v y)) v x) = c(c(c(z) v c(x v y)) v x).  [para(2516(a,1),2527(a,1,2,1,2,1)),demod(2425(9),2516(19),2425(17))].
2780 c(c(x v y) v x) v c(x v y) = c(x).  [para(2563(a,1),2594(a,1,1,2,1,1,1,2,1)),demod(2425(2),2425(4),2709(9),2425(9))].
4122 x v c(c(x v y) v x) = x v y.  [para(2780(a,1),2780(a,1,1,1)),demod(2425(2),2425(8))].
5662 c(x v y) v c(y v x) = c(y v x).  [para(2619(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(8),2624(9),2425(7))].
5783 (x v y) v (y v x) = y v x.  [para(5662(a,1),2516(a,1,1,1)),demod(2425(3),2425(4),2425(6))].
5785 x v y = y v x.  [para(5662(a,1),2567(a,1,2,1)),demod(2425(4),5783(3))].
5906 x v c(x v c(x v y)) = x v y.  [back_demod(4122),demod(5785(3))].
5907 $F # answer(OM).  [resolve(5906,a,2476,a)].

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

NOTE: Disabling denial clause 2476.

given #248 (F,wt=7): 5785 x v y = y v x.  [para(5662(a,1),2567(a,1,2,1)),demod(2425(4),5783(3))].

given #249 (T,wt=9): 5784 c(x v y) = c(y v x).  [para(5662(a,1),2564(a,1,1)),demod(5662(5),5662(7))].

given #250 (T,wt=11): 5783 (x v y) v (y v x) = y v x.  [para(5662(a,1),2516(a,1,1,1)),demod(2425(3),2425(4),2425(6))].

given #251 (A,wt=26): 2714 c(x v y) v c(x v c(c(x v y) v z)) = c(x v c(c(x v y) v z)).  [para(2567(a,1),2527(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(4),2425(12),2563(13),2425(11),2425(11))].

given #252 (F,wt=13): 5879 x v c(x v c(y v x)) = y v x.  [back_demod(4613),demod(5785(3))].

given #253 (F,wt=13): 5906 x v c(x v c(x v y)) = x v y.  [back_demod(4122),demod(5785(3))].

given #254 (T,wt=13): 6218 c((x v y) v c(y v x)) v z = z.  [para(5784(a,1),4167(a,1,1,1,2))].

given #255 (T,wt=13): 6219 x v c((y v z) v c(z v y)) = x.  [para(5784(a,1),4168(a,1,2,1,2))].

given #256 (A,wt=26): 2716 c(x v y) v c(y v c(c(x v y) v z)) = c(y v c(c(x v y) v z)).  [para(2619(a,1),2527(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(4),2425(12),2624(13),2425(11),2425(11))].

given #257 (F,wt=13): 6220 (x v y) v c(y v x) = z v c(z).  [para(5784(a,1),4241(a,1,2))].

given #258 (F,wt=15): 2910 c(x v (c(y) v z)) v (u v y) = u v y.  [para(2651(a,1),2696(a,1,2)),demod(2425(4),2651(11))].

given #259 (T,wt=15): 2911 (x v y) v c((z v c(x)) v u) = x v y.  [para(2696(a,1),2679(a,1,1)),demod(2425(5),2696(11))].

given #260 (T,wt=15): 2912 c(x v (y v c(z))) v (z v u) = z v u.  [para(2696(a,1),2696(a,1,2)),demod(2425(4),2696(11))].

given #261 (A,wt=32): 2721 c((x v y) v z) v c(x v c(c((x v y) v z) v u)) = c(x v c(c((x v y) v z) v u)).  [para(2648(a,1),2527(a,1,2,1,1,1)),demod(2425(2),2425(5),2425(5),2425(14),2678(16),2425(13),2425(13))].

given #262 (F,wt=15): 2958 c((x v c(y)) v z) v (u v y) = u v y.  [para(2700(a,1),2646(a,1,2)),demod(2425(4),2700(11))].

given #263 (F,wt=15): 2959 (x v y) v c((z v c(y)) v u) = x v y.  [para(2700(a,1),2679(a,1,1)),demod(2425(5),2700(11))].

given #264 (T,wt=15): 2960 c(x v (y v c(z))) v (u v z) = u v z.  [para(2700(a,1),2696(a,1,2)),demod(2425(4),2700(11))].

given #265 (T,wt=15): 2969 (x v y) v c(z v (c(x) v u)) = x v y.  [para(2646(a,1),2732(a,1,1)),demod(2425(5),2646(11))].

given #266 (A,wt=32): 2725 c((x v y) v z) v c(y v c(c((x v y) v z) v u)) = c(y v c(c((x v y) v z) v u)).  [para(2683(a,1),2527(a,1,2,1,1,1)),demod(2425(2),2425(5),2425(5),2425(14),2707(16),2425(13),2425(13))].

given #267 (F,wt=15): 2970 (x v y) v c(z v (c(y) v u)) = x v y.  [para(2651(a,1),2732(a,1,1)),demod(2425(5),2651(11))].

given #268 (F,wt=15): 2971 (x v y) v c(z v (u v c(x))) = x v y.  [para(2696(a,1),2732(a,1,1)),demod(2425(5),2696(11))].

given #269 (T,wt=15): 2972 (x v y) v c(z v (u v c(y))) = x v y.  [para(2700(a,1),2732(a,1,1)),demod(2425(5),2700(11))].

given #270 (T,wt=15): 3085 x v c((((c(x) v y) v z) v u) v v) = x.  [para(2806(a,1),2679(a,1,1)),demod(2425(6),2806(13))].

given #271 (A,wt=18): 2736 ((c(x) v y) v z) v c(u v x) = (c(x) v y) v z.  [para(2633(a,1),2684(a,1,2,1,2))].

given #272 (F,wt=15): 3091 x v c(y v (((c(x) v z) v u) v v)) = x.  [para(2806(a,1),2732(a,1,1)),demod(2425(6),2806(13))].

given #273 (F,wt=15): 3163 x v c((((y v c(x)) v z) v u) v v) = x.  [para(2809(a,1),2679(a,1,1)),demod(2425(6),2809(13))].

given #274 (T,wt=15): 3167 x v c(y v (((z v c(x)) v u) v v)) = x.  [para(2809(a,1),2732(a,1,1)),demod(2425(6),2809(13))].

given #275 (T,wt=15): 3193 x v c(((y v (c(x) v z)) v u) v v) = x.  [para(2812(a,1),2679(a,1,1)),demod(2425(6),2812(13))].

given #276 (A,wt=18): 2737 ((x v c(y)) v z) v c(u v y) = (x v c(y)) v z.  [para(2652(a,1),2684(a,1,2,1,2))].

given #277 (F,wt=15): 3199 x v c(y v ((z v (c(x) v u)) v v)) = x.  [para(2812(a,1),2732(a,1,1)),demod(2425(6),2812(13))].

given #278 (F,wt=15): 3216 x v c(((y v (z v c(x))) v u) v v) = x.  [para(2815(a,1),2679(a,1,1)),demod(2425(6),2815(13))].

given #279 (T,wt=15): 3220 x v c(y v ((z v (u v c(x))) v v)) = x.  [para(2815(a,1),2732(a,1,1)),demod(2425(6),2815(13))].

given #280 (T,wt=15): 3242 x v c((y v ((c(x) v z) v u)) v v) = x.  [para(2765(a,1),2870(a,1,2,1))].

given #281 (A,wt=18): 2738 (x v (c(y) v z)) v c(u v y) = x v (c(y) v z).  [para(2653(a,1),2684(a,1,2,1,2))].

given #282 (F,wt=15): 3243 x v c((y v (z v (c(x) v u))) v v) = x.  [para(2798(a,1),2870(a,1,2,1,1))].

given #283 (F,wt=15): 3244 x v c(y v (z v ((c(x) v u) v v))) = x.  [para(2798(a,1),2870(a,1,2,1))].

given #284 (T,wt=15): 3315 x v c((y v ((z v c(x)) v u)) v v) = x.  [para(2765(a,1),2872(a,1,2,1))].

given #285 (T,wt=15): 3316 x v c((y v (z v (u v c(x)))) v v) = x.  [para(2798(a,1),2872(a,1,2,1,1))].

given #286 (A,wt=18): 2743 c(x v y) v (z v (u v c(x))) = z v (u v c(x)).  [para(2690(a,1),2633(a,1,1,1,1))].

given #287 (F,wt=15): 3317 x v c(y v (z v ((u v c(x)) v v))) = x.  [para(2798(a,1),2872(a,1,2,1))].

given #288 (F,wt=15): 3332 x v c(y v (z v (u v (c(x) v v)))) = x.  [para(2798(a,1),2874(a,1,2,1))].

given #289 (T,wt=15): 3340 x v c(y v (z v (u v (v v c(x))))) = x.  [para(2798(a,1),2876(a,1,2,1))].

given #290 (T,wt=15): 3755 c(x) v (c(y v x) v c(x v z)) = c(x).  [para(1757(a,1),2661(a,1,2,1)),demod(2425(8))].

given #291 (A,wt=18): 2744 (x v (y v c(z))) v c(z v u) = x v (y v c(z)).  [para(2690(a,1),2648(a,1,2,1,1))].

given #292 (F,wt=15): 4159 c(x v y) v c(x v c(x v y)) = c(x).  [para(4078(a,1),2780(a,1,1,1))].

given #293 (F,wt=15): 4283 (x v (y v (z v u))) v c(u) = u v c(u).  [para(2907(a,1),4124(a,1,2)),demod(4247(13),4261(12),4247(11),4261(10),4247(9),4261(8))].

given #294 (T,wt=15): 4612 c(x v y) v c(y v c(x v y)) = c(y).  [para(4080(a,1),2780(a,1,1,1))].

given #295 (T,wt=15): 4703 x v (((c(x) v y) v z) v u) = x v c(x).  [para(2749(a,1),4140(a,1,2,1))].

given #296 (A,wt=18): 2745 c(x v y) v (z v (u v c(y))) = z v (u v c(y)).  [para(2690(a,1),2653(a,1,1,1,2))].

given #297 (F,wt=15): 4704 x v (((y v c(x)) v z) v u) = x v c(x).  [para(2765(a,1),4140(a,1,2,1))].

given #298 (F,wt=15): 4705 x v ((y v (c(x) v z)) v u) = x v c(x).  [para(2765(a,1),4140(a,1,2))].

given #299 (T,wt=15): 4706 x v (y v ((c(x) v z) v u)) = x v c(x).  [para(2771(a,1),4140(a,1,2))].

given #300 (T,wt=15): 4707 x v ((y v (z v c(x))) v u) = x v c(x).  [para(2798(a,1),4140(a,1,2,1))].

given #301 (A,wt=18): 2746 (x v (y v c(z))) v c(u v z) = x v (y v c(z)).  [para(2690(a,1),2684(a,1,2,1,2))].

given #302 (F,wt=15): 4708 x v (y v (z v (c(x) v u))) = x v c(x).  [para(2798(a,1),4140(a,1,2))].

given #303 (F,wt=15): 4735 x v (y v ((z v c(x)) v u)) = x v c(x).  [para(2771(a,1),4141(a,1,2))].

given #304 (T,wt=15): 4736 x v (y v (z v (u v c(x)))) = x v c(x).  [para(2798(a,1),4141(a,1,2))].

given #305 (T,wt=15): 4813 c(x) v (((x v y) v z) v u) = x v c(x).  [para(2749(a,1),4154(a,1,2,1))].

given #306 (A,wt=17): 2751 c(c(x) v y) v ((x v z) v u) = (x v z) v u.  [para(2644(a,1),2633(a,1,1,1,1))].

given #307 (F,wt=15): 4815 c(x) v (((y v x) v z) v u) = x v c(x).  [para(2765(a,1),4154(a,1,2,1))].

given #308 (F,wt=15): 4816 c(x) v ((y v (x v z)) v u) = x v c(x).  [para(2765(a,1),4154(a,1,2))].

given #309 (T,wt=15): 4817 c(x) v (y v ((x v z) v u)) = x v c(x).  [para(2771(a,1),4154(a,1,2))].

given #310 (T,wt=15): 4818 c(x) v ((y v (z v x)) v u) = x v c(x).  [para(2798(a,1),4154(a,1,2,1))].

given #311 (A,wt=17): 2752 ((x v y) v z) v c(c(x) v u) = (x v y) v z.  [para(2644(a,1),2648(a,1,2,1,1))].

given #312 (F,wt=15): 4819 c(x) v (y v (z v (x v u))) = x v c(x).  [para(2798(a,1),4154(a,1,2))].

given #313 (F,wt=15): 4841 c(x) v (y v ((z v x) v u)) = x v c(x).  [para(2771(a,1),4155(a,1,2))].

given #314 (T,wt=15): 4842 c(x) v (y v (z v (u v x))) = x v c(x).  [para(2798(a,1),4155(a,1,2))].

given #315 (T,wt=15): 4891 (x v y) v ((c(y) v z) v u) = y v c(y).  [para(2749(a,1),4274(a,1,2))].

given #316 (A,wt=17): 2753 c(x v c(y)) v ((y v z) v u) = (y v z) v u.  [para(2644(a,1),2653(a,1,1,1,2))].

given #317 (F,wt=15): 4892 ((x v y) v z) v (c(x) v u) = x v c(x).  [para(2750(a,1),4274(a,1,1))].

given #318 (F,wt=15): 4893 (x v y) v ((z v c(y)) v u) = y v c(y).  [para(2765(a,1),4274(a,1,2))].

given #319 (T,wt=15): 4894 ((x v y) v z) v (c(y) v u) = y v c(y).  [para(2766(a,1),4274(a,1,1))].

given #320 (T,wt=15): 4895 (x v y) v (z v (c(y) v u)) = y v c(y).  [para(2771(a,1),4274(a,1,2))].

given #321 (A,wt=17): 2754 ((x v y) v z) v c(u v c(x)) = (x v y) v z.  [para(2644(a,1),2684(a,1,2,1,2))].

given #322 (F,wt=15): 4896 (x v (y v z)) v (c(y) v u) = y v c(y).  [para(2772(a,1),4274(a,1,1))].

given #323 (F,wt=15): 4897 (x v y) v (z v (u v c(y))) = y v c(y).  [para(2798(a,1),4274(a,1,2))].

given #324 (T,wt=15): 4898 (x v (y v z)) v (c(z) v u) = z v c(z).  [para(2799(a,1),4274(a,1,1))].

given #325 (T,wt=15): 4943 ((x v y) v z) v (u v c(x)) = x v c(x).  [para(2750(a,1),4275(a,1,1))].

given #326 (A,wt=17): 2767 c(c(x) v y) v ((z v x) v u) = (z v x) v u.  [para(2687(a,1),2633(a,1,1,1,1))].

given #327 (F,wt=15): 4944 ((x v y) v z) v (u v c(y)) = y v c(y).  [para(2766(a,1),4275(a,1,1))].

given #328 (F,wt=15): 4945 (x v (y v z)) v (u v c(y)) = y v c(y).  [para(2772(a,1),4275(a,1,1))].

given #329 (T,wt=15): 4946 (x v (y v z)) v (u v c(z)) = z v c(z).  [para(2799(a,1),4275(a,1,1))].

given #330 (T,wt=15): 4979 ((c(x) v y) v z) v (x v u) = x v c(x).  [para(2749(a,1),4409(a,1,1))].

given #331 (A,wt=17): 2768 ((x v y) v z) v c(c(y) v u) = (x v y) v z.  [para(2687(a,1),2648(a,1,2,1,1))].

given #332 (F,wt=15): 4980 (c(x) v y) v ((x v z) v u) = x v c(x).  [para(2749(a,1),4409(a,1,2))].

given #333 (F,wt=15): 4982 ((x v c(y)) v z) v (y v u) = y v c(y).  [para(2765(a,1),4409(a,1,1))].

given #334 (T,wt=15): 4983 (c(x) v y) v ((z v x) v u) = x v c(x).  [para(2765(a,1),4409(a,1,2))].

given #335 (T,wt=15): 4984 (x v (c(y) v z)) v (y v u) = y v c(y).  [para(2771(a,1),4409(a,1,1))].

given #336 (A,wt=17): 2769 c(x v c(y)) v ((z v y) v u) = (z v y) v u.  [para(2687(a,1),2653(a,1,1,1,2))].

given #337 (F,wt=15): 4985 (c(x) v y) v (z v (x v u)) = x v c(x).  [para(2771(a,1),4409(a,1,2))].

given #338 (F,wt=15): 4986 (x v (y v c(z))) v (z v u) = z v c(z).  [para(2798(a,1),4409(a,1,1))].

given #339 (T,wt=15): 4987 (c(x) v y) v (z v (u v x)) = x v c(x).  [para(2798(a,1),4409(a,1,2))].

given #340 (T,wt=15): 5021 ((c(x) v y) v z) v (u v x) = x v c(x).  [para(2749(a,1),4410(a,1,1))].

given #341 (A,wt=17): 2770 ((x v y) v z) v c(u v c(y)) = (x v y) v z.  [para(2687(a,1),2684(a,1,2,1,2))].

given #342 (F,wt=15): 5022 ((x v c(y)) v z) v (u v y) = y v c(y).  [para(2765(a,1),4410(a,1,1))].

given #343 (F,wt=15): 5023 (x v (c(y) v z)) v (u v y) = y v c(y).  [para(2771(a,1),4410(a,1,1))].

given #344 (T,wt=15): 5024 (x v (y v c(z))) v (u v z) = z v c(z).  [para(2798(a,1),4410(a,1,1))].

given #345 (T,wt=15): 5105 (x v c(y)) v ((y v z) v u) = y v c(y).  [para(2750(a,1),4435(a,1,2))].

given #346 (A,wt=17): 2773 c(c(x) v y) v (z v (x v u)) = z v (x v u).  [para(2694(a,1),2633(a,1,1,1,1))].

given #347 (F,wt=15): 5106 (x v c(y)) v ((z v y) v u) = y v c(y).  [para(2766(a,1),4435(a,1,2))].

given #348 (F,wt=15): 5107 (x v c(y)) v (z v (y v u)) = y v c(y).  [para(2772(a,1),4435(a,1,2))].

given #349 (T,wt=15): 5108 (x v c(y)) v (z v (u v y)) = y v c(y).  [para(2799(a,1),4435(a,1,2))].

given #350 (T,wt=15): 5180 (((x v y) v z) v u) v c(x) = x v c(x).  [para(2749(a,1),4446(a,1,1,1))].

given #351 (A,wt=17): 2774 (x v (y v z)) v c(c(y) v u) = x v (y v z).  [para(2694(a,1),2648(a,1,2,1,1))].

given #352 (F,wt=15): 5182 (((x v y) v z) v u) v c(y) = y v c(y).  [para(2765(a,1),4446(a,1,1,1))].

given #353 (F,wt=15): 5183 ((x v (y v z)) v u) v c(y) = y v c(y).  [para(2765(a,1),4446(a,1,1))].

given #354 (T,wt=15): 5184 (x v ((y v z) v u)) v c(y) = y v c(y).  [para(2771(a,1),4446(a,1,1))].

given #355 (T,wt=15): 5185 ((x v (y v z)) v u) v c(z) = z v c(z).  [para(2798(a,1),4446(a,1,1,1))].

given #356 (A,wt=17): 2775 c(x v c(y)) v (z v (y v u)) = z v (y v u).  [para(2694(a,1),2653(a,1,1,1,2))].

given #357 (F,wt=15): 5186 (x v (y v (z v u))) v c(z) = z v c(z).  [para(2798(a,1),4446(a,1,1))].

given #358 (F,wt=15): 5192 (x v ((y v z) v u)) v c(z) = z v c(z).  [para(2765(a,1),4447(a,1,1,2))].

given #359 (T,wt=15): 5230 (x v y) v ((c(x) v z) v u) = x v c(x).  [para(2749(a,1),4752(a,1,2))].

given #360 (T,wt=15): 5232 (x v y) v ((z v c(x)) v u) = x v c(x).  [para(2765(a,1),4752(a,1,2))].

given #361 (A,wt=17): 2776 (x v (y v z)) v c(u v c(y)) = x v (y v z).  [para(2694(a,1),2684(a,1,2,1,2))].

given #362 (F,wt=15): 5233 (x v y) v (z v (c(x) v u)) = x v c(x).  [para(2771(a,1),4752(a,1,2))].

given #363 (F,wt=15): 5234 (x v y) v (z v (u v c(x))) = x v c(x).  [para(2798(a,1),4752(a,1,2))].

given #364 (T,wt=15): 5325 x v (c(c(x) v y) v c(c(x) v z)) = x.  [para(2564(a,1),2825(a,1,2,1,1))].

given #365 (T,wt=15): 5331 x v (c(y v c(x)) v c(z v c(x))) = x.  [para(2625(a,1),2825(a,1,2,2,1))].

given #366 (A,wt=17): 2800 c(c(x) v y) v (z v (u v x)) = z v (u v x).  [para(2740(a,1),2633(a,1,1,1,1))].

given #367 (F,wt=15): 5788 (x v y) v c(c(y v x) v z) = x v y.  [para(5662(a,1),2633(a,1,1,1,1)),demod(5785(6))].

given #368 (F,wt=15): 5789 (x v y) v c(z v c(y v x)) = x v y.  [para(5662(a,1),2653(a,1,1,1,2)),demod(5785(6))].

given #369 (T,wt=15): 5790 (x v y) v ((y v x) v z) = (y v x) v z.  [para(5662(a,1),2646(a,1,1,1)),demod(2425(3))].

given #370 (T,wt=15): 5792 (x v y) v (z v (y v x)) = z v (y v x).  [para(5662(a,1),2651(a,1,1,1)),demod(2425(3))].

given #371 (A,wt=17): 2801 (x v (y v z)) v c(c(z) v u) = x v (y v z).  [para(2740(a,1),2648(a,1,2,1,1))].

given #372 (F,wt=15): 5793 (x v (y v z)) v (z v y) = x v (y v z).  [para(5662(a,1),2682(a,1,2,1)),demod(2425(5))].

given #373 (F,wt=15): 5802 x v (c(c(x) v y) v c(z v c(x))) = x.  [para(5662(a,1),2611(a,1,1,1)),demod(2425(9),5785(8))].

given #374 (T,wt=15): 5809 c(x) v (c(x v y) v c(z v x)) = c(x).  [para(5662(a,1),2676(a,1,1,1)),demod(2425(7),5785(7))].

given #375 (T,wt=15): 6124 c(x) v (c(y v x) v c(z v x)) = c(x).  [back_demod(4044),demod(5785(7))].

given #376 (A,wt=17): 2802 c(x v c(y)) v (z v (u v y)) = z v (u v y).  [para(2740(a,1),2653(a,1,1,1,2))].

given #377 (F,wt=15): 6125 c(x) v (c(x v y) v c(x v z)) = c(x).  [back_demod(4043),demod(5785(7))].

given #378 (F,wt=15): 6223 c((x v y) v c(y v x)) = c(z v c(z)).  [para(5784(a,1),4243(a,1,1,2))].

given #379 (T,wt=15): 7896 c(x v y) v c(y v c(y v x)) = c(y).  [para(5785(a,1),4159(a,1,1,1))].

given #380 (T,wt=15): 7897 c(x v y) v c(x v c(y v x)) = c(x).  [para(5785(a,1),4159(a,1,2,1,2,1))].

given #381 (A,wt=17): 2803 (x v (y v z)) v c(u v c(z)) = x v (y v z).  [para(2740(a,1),2684(a,1,2,1,2))].

given #382 (F,wt=15): 10470 (x v y) v (y v c(y v x)) = y v c(y).  [para(7896(a,1),4125(a,1,2)),demod(5785(5),4126(5),9950(10)),flip(a)].

given #383 (F,wt=15): 10471 (x v y) v (x v c(y v x)) = x v c(x).  [para(7897(a,1),4125(a,1,2)),demod(5785(5),4126(5),9950(10)),flip(a)].

given #384 (T,wt=16): 2804 c((x v y) v z) v (c(x) v u) = c(x) v u.  [para(2646(a,1),2633(a,1,1,1,1))].

given #385 (T,wt=16): 2807 (c(x) v y) v c((x v z) v u) = c(x) v y.  [para(2646(a,1),2648(a,1,2,1,1))].

given #386 (A,wt=16): 2810 c(x v (y v z)) v (c(y) v u) = c(y) v u.  [para(2646(a,1),2653(a,1,1,1,2))].

given #387 (F,wt=16): 2813 (c(x) v y) v c(z v (x v u)) = c(x) v y.  [para(2646(a,1),2684(a,1,2,1,2))].

given #388 (F,wt=16): 2857 c((x v y) v z) v (c(y) v u) = c(y) v u.  [para(2651(a,1),2633(a,1,1,1,1))].

given #389 (T,wt=16): 2859 (c(x) v y) v c((z v x) v u) = c(x) v y.  [para(2651(a,1),2648(a,1,2,1,1))].

given #390 (T,wt=16): 2861 c(x v (y v z)) v (c(z) v u) = c(z) v u.  [para(2651(a,1),2653(a,1,1,1,2))].

given #391 (A,wt=17): 2816 x v (((x v y) v z) v u) = ((x v y) v z) v u.  [para(2644(a,1),2646(a,1,1,1)),demod(2425(2))].

given #392 (F,wt=16): 2863 (c(x) v y) v c(z v (u v x)) = c(x) v y.  [para(2651(a,1),2684(a,1,2,1,2))].

given #393 (F,wt=16): 2896 c((x v y) v z) v (u v c(x)) = u v c(x).  [para(2696(a,1),2633(a,1,1,1,1))].

given #394 (T,wt=16): 2898 (x v c(y)) v c((y v z) v u) = x v c(y).  [para(2696(a,1),2648(a,1,2,1,1))].

given #395 (T,wt=16): 2900 c(x v (y v z)) v (u v c(y)) = u v c(y).  [para(2696(a,1),2653(a,1,1,1,2))].

given #396 (A,wt=17): 2818 x v (((y v x) v z) v u) = ((y v x) v z) v u.  [para(2687(a,1),2646(a,1,1,1)),demod(2425(2))].

given #397 (F,wt=16): 2902 (x v c(y)) v c(z v (y v u)) = x v c(y).  [para(2696(a,1),2684(a,1,2,1,2))].

given #398 (F,wt=16): 2954 c((x v y) v z) v (u v c(y)) = u v c(y).  [para(2700(a,1),2633(a,1,1,1,1))].

given #399 (T,wt=16): 2955 (x v c(y)) v c((z v y) v u) = x v c(y).  [para(2700(a,1),2648(a,1,2,1,1))].

given #400 (T,wt=16): 2956 c(x v (y v z)) v (u v c(z)) = u v c(z).  [para(2700(a,1),2653(a,1,1,1,2))].

given #401 (A,wt=17): 2820 x v ((y v (x v z)) v u) = (y v (x v z)) v u.  [para(2694(a,1),2646(a,1,1,1)),demod(2425(2))].

given #402 (F,wt=16): 2957 (x v c(y)) v c(z v (u v y)) = x v c(y).  [para(2700(a,1),2684(a,1,2,1,2))].

given #403 (F,wt=16): 3685 c(x) v c((((x v y) v z) v u) v v) = c(x).  [para(2817(a,1),2679(a,1,1)),demod(2425(6),2817(13))].

given #404 (T,wt=16): 3689 c(x) v c(y v (((x v z) v u) v v)) = c(x).  [para(2817(a,1),2732(a,1,1)),demod(2425(6),2817(13))].

given #405 (T,wt=16): 3711 c(x) v c((((y v x) v z) v u) v v) = c(x).  [para(2819(a,1),2679(a,1,1)),demod(2425(6),2819(13))].

given #406 (A,wt=17): 2822 x v ((y v (z v x)) v u) = (y v (z v x)) v u.  [para(2740(a,1),2646(a,1,1,1)),demod(2425(2))].

given #407 (F,wt=16): 3715 c(x) v c(y v (((z v x) v u) v v)) = c(x).  [para(2819(a,1),2732(a,1,1)),demod(2425(6),2819(13))].

given #408 (F,wt=16): 3736 c(x) v c(((y v (x v z)) v u) v v) = c(x).  [para(2821(a,1),2679(a,1,1)),demod(2425(6),2821(13))].

given #409 (T,wt=16): 3740 c(x) v c(y v ((z v (x v u)) v v)) = c(x).  [para(2821(a,1),2732(a,1,1)),demod(2425(6),2821(13))].

given #410 (T,wt=16): 3817 c(x) v c(((y v (z v x)) v u) v v) = c(x).  [para(2823(a,1),2679(a,1,1)),demod(2425(6),2823(13))].

given #411 (A,wt=19): 2826 x v c(c(c(y v c(x)) v c(c(x) v z)) v u) = x.  [para(2425(a,1),2595(a,1,2,1,2))].

given #412 (F,wt=16): 3821 c(x) v c(y v ((z v (u v x)) v v)) = c(x).  [para(2823(a,1),2732(a,1,1)),demod(2425(6),2823(13))].

given #413 (F,wt=16): 3837 c(x) v c((y v ((x v z) v u)) v v) = c(x).  [para(2765(a,1),2878(a,1,2,1))].

given #414 (T,wt=16): 3838 c(x) v c((y v (z v (x v u))) v v) = c(x).  [para(2798(a,1),2878(a,1,2,1,1))].

given #415 (T,wt=16): 3839 c(x) v c(y v (z v ((x v u) v v))) = c(x).  [para(2798(a,1),2878(a,1,2,1))].

given #416 (A,wt=17): 2865 x v (y v ((x v z) v u)) = y v ((x v z) v u).  [para(2644(a,1),2651(a,1,1,1)),demod(2425(2))].

given #417 (F,wt=16): 3842 c(x) v c((y v ((z v x) v u)) v v) = c(x).  [para(2765(a,1),2880(a,1,2,1))].

given #418 (F,wt=16): 3843 c(x) v c((y v (z v (u v x))) v v) = c(x).  [para(2798(a,1),2880(a,1,2,1,1))].

given #419 (T,wt=16): 3844 c(x) v c(y v (z v ((u v x) v v))) = c(x).  [para(2798(a,1),2880(a,1,2,1))].

given #420 (T,wt=16): 3848 c(x) v c(y v (z v (u v (x v v)))) = c(x).  [para(2798(a,1),2882(a,1,2,1))].

given #421 (A,wt=17): 2866 x v (y v ((z v x) v u)) = y v ((z v x) v u).  [para(2687(a,1),2651(a,1,1,1)),demod(2425(2))].

given #422 (F,wt=16): 3932 c(x) v c(y v (z v (u v (v v x)))) = c(x).  [para(2798(a,1),2884(a,1,2,1))].

given #423 (F,wt=16): 5670 c(x v (y v z)) v c(y v x) = c(y v x).  [para(2684(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(5),2425(9),2731(11),2425(8))].

given #424 (T,wt=15): 12548 (x v (y v z)) v (y v x) = x v (y v z).  [para(5670(a,1),2567(a,1,2,1)),demod(2425(5))].

given #425 (T,wt=15): 12684 (x v y) v ((x v z) v y) = (x v z) v y.  [para(5670(a,1),5788(a,1,2,1)),demod(2425(5),5785(4))].

given #426 (A,wt=17): 2867 x v (y v (z v (x v u))) = y v (z v (x v u)).  [para(2694(a,1),2651(a,1,1,1)),demod(2425(2))].

given #427 (F,wt=13): 13060 x v (y v c(y v x)) = y v c(y).  [para(10470(a,1),12684(a,1,1)),demod(8992(8),12912(6),4166(7),8992(8),12912(6)),flip(a)].

given #428 (F,wt=13): 13099 (x v y) v (x v z) = (x v y) v z.  [para(12684(a,1),12548(a,1,1)),demod(12729(6),12684(7))].

% Operation v is associative-commutative; redundancy checks enabled.

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

% Proof 12 at 7.15 (+ 0.10) seconds: AJ.
% Length of proof is 110.
% Level of proof is 29.
% Maximum clause weight is 37.
% Given clauses 428.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
28 c6 v (c5 v c7) != c5 v (c6 v c7) # answer(AJ).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2419(15),2425(16),2419(16),2419(19))].
2490 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_demod(1816),demod(2419(3),2419(6),2419(9),2419(12),2425(3),2419(13))].
2501 x v c(c(x) v c(c(y v c(x v y)) v y)) = x.  [back_demod(1711),demod(2419(4),2425(3),2419(6),2425(7),2419(7),2419(10),2425(2))].
2514 c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [para(2486(a,1),1757(a,1)),flip(a)].
2516 c(x v y) v c(x) = c(x).  [para(2486(a,1),2419(a,2)),demod(2419(10),2514(11))].
2520 (c(c(x) v y) v c(y)) v c(y) = c(y).  [back_demod(2448),demod(2514(14))].
2521 c(c(x) v y) v x = x.  [para(2425(a,1),2516(a,1,2)),demod(2425(6))].
2522 x v (x v y) = x v y.  [para(2516(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2527 c(x) v c(c(c(y) v c(x)) v c(c(x) v z)) = c(c(c(y) v c(x)) v c(c(x) v z)).  [para(2434(a,1),2516(a,1,1,1))].
2535 (c(c(x) v c(y)) v y) v y = y.  [para(2425(a,1),2520(a,1,1,2)),demod(2425(7),2425(8))].
2542 (c(x v c(y)) v y) v y = y.  [para(2425(a,1),2535(a,1,1,1,1,1))].
2546 (c(x) v c(x v y)) v c(x v c(c(y v c(c(x) v y)) v y)) = c(x).  [para(2425(a,1),2447(a,1,1,2,1,2)),demod(2425(6),2425(7),2425(11))].
2548 (c(x) v c(x v c(y))) v c(x) = c(x) v c(x v c(y)).  [para(2447(a,1),2501(a,1,2,1,2,1,1,1,2,1)),demod(2425(25),2490(38),2425(13),2521(12))].
2552 c(x) v c(x v c(y)) = c(x).  [para(2447(a,1),2522(a,1,2)),demod(2548(7),2546(23))].
2564 (x v y) v x = x v y.  [para(2516(a,1),2552(a,1,2,1)),demod(2425(3),2425(3),2425(5))].
2567 x v c(c(x) v y) = x.  [para(2521(a,1),2564(a,1,1)),demod(2521(8))].
2586 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(2516(a,1),2489(a,1,1,1,1,1)),demod(2425(4))].
2587 c(x v c(y)) v c(c(y) v c(c(z v c(y v z)) v z)) = y.  [para(2516(a,1),2489(a,1,1,1)),demod(2425(4))].
2594 c(c(x) v c(c(y v c(x v y)) v y)) = x.  [para(2489(a,1),2542(a,1,1)),demod(2567(10)),flip(a)].
2608 c(x v c(y)) v y = y.  [back_demod(2587),demod(2594(12))].
2609 c((c(x) v y) v c(z)) v x = x.  [back_demod(2586),demod(2594(14))].
2617 c(x v y) v c(y) = c(y).  [para(2425(a,1),2608(a,1,1,1,2))].
2619 x v c(y v c(x)) = x.  [para(2608(a,1),2564(a,1,1)),demod(2608(8))].
2624 c(x) v c(y v x) = c(x).  [para(2425(a,1),2619(a,1,2,1,2))].
2625 x v (y v x) = y v x.  [para(2617(a,1),2516(a,1,1,1)),demod(2425(2),2425(3),2425(5))].
2633 c((c(x) v y) v z) v x = x.  [para(2425(a,1),2609(a,1,1,1,2))].
2646 c(c(x) v y) v (x v z) = x v z.  [para(2516(a,1),2633(a,1,1,1,1))].
2648 x v c((c(x) v y) v z) = x.  [para(2633(a,1),2564(a,1,1)),demod(2633(10))].
2651 c(c(x) v y) v (z v x) = z v x.  [para(2617(a,1),2633(a,1,1,1,1))].
2652 c((x v c(y)) v z) v y = y.  [para(2625(a,1),2633(a,1,1,1,1))].
2653 c(x v (c(y) v z)) v y = y.  [para(2625(a,1),2633(a,1,1,1))].
2684 x v c(y v (c(x) v z)) = x.  [para(2625(a,1),2648(a,1,2,1))].
2690 c(x v (y v c(z))) v z = z.  [para(2625(a,1),2652(a,1,1,1))].
2694 c(x v (y v z)) v c(y) = c(y).  [para(2425(a,1),2653(a,1,1,1,2,1))].
2711 c(x v y) v c(c(c(z) v c(x v y)) v x) = c(c(c(z) v c(x v y)) v x).  [para(2516(a,1),2527(a,1,2,1,2,1)),demod(2425(9),2516(19),2425(17))].
2731 c(x) v c(y v (x v z)) = c(x).  [para(2425(a,1),2684(a,1,2,1,2,1))].
2740 c(x v (y v z)) v c(z) = c(z).  [para(2425(a,1),2690(a,1,1,1,2,2))].
2771 x v (y v (x v z)) = y v (x v z).  [para(2694(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].
2798 x v (y v (z v x)) = y v (z v x).  [para(2740(a,1),2516(a,1,1,1)),demod(2425(2),2425(4),2425(7))].
5662 c(x v y) v c(y v x) = c(y v x).  [para(2619(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(4),2425(8),2624(9),2425(7))].
5670 c(x v (y v z)) v c(y v x) = c(y v x).  [para(2684(a,1),2711(a,1,2,1,1,1)),demod(2425(2),2425(5),2425(9),2731(11),2425(8))].
5783 (x v y) v (y v x) = y v x.  [para(5662(a,1),2516(a,1,1,1)),demod(2425(3),2425(4),2425(6))].
5785 x v y = y v x.  [para(5662(a,1),2567(a,1,2,1)),demod(2425(4),5783(3))].
5788 (x v y) v c(c(y v x) v z) = x v y.  [para(5662(a,1),2633(a,1,1,1,1)),demod(5785(6))].
12548 (x v (y v z)) v (y v x) = x v (y v z).  [para(5670(a,1),2567(a,1,2,1)),demod(2425(5))].
12684 (x v y) v ((x v z) v y) = (x v z) v y.  [para(5670(a,1),5788(a,1,2,1)),demod(2425(5),5785(4))].
12717 c(c(x v y) v z) v (y v (x v u)) = y v (x v u).  [para(12548(a,1),2651(a,1,2)),demod(12548(11))].
12727 (x v y) v (x v (y v z)) = x v (y v z).  [para(2771(a,1),12548(a,1,1)),demod(5785(4),2771(7))].
12729 (x v y) v (x v (z v y)) = x v (z v y).  [para(2798(a,1),12548(a,1,1)),demod(5785(4),2798(7))].
13099 (x v y) v (x v z) = (x v y) v z.  [para(12684(a,1),12548(a,1,1)),demod(12729(6),12684(7))].
14074 (x v y) v (y v z) = x v (y v z).  [back_demod(12727),demod(13099(4))].
14131 (x v y) v z = x v (y v z).  [para(2625(a,1),13099(a,1,1)),demod(14074(3),2625(4)),flip(a)].
14142 x v (y v z) = y v (x v z).  [para(13099(a,1),2646(a,2)),demod(14131(7),2771(7),12717(7),14131(4))].
14143 $F # answer(AJ).  [resolve(14142,a,28,a)].

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

NOTE: Disabling denial clause 28.

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

% Proof 13 at 8.05 (+ 0.11) seconds: assoc_meet.
% Length of proof is 107.
% Level of proof is 28.
% Maximum clause weight is 37.
% Given clauses 428.

1 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).  [input].
2 x v y = f(f(x,x),f(y,y)) # label(Def_join).  [input].
3 x ^ y = f(f(x,y),f(x,y)) # label(Def_meet).  [input].
4 c(x) = f(x,x) # label(Def_complement).  [input].
19 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).  [copy(1)].
20 f(f(x,x),f(y,y)) = x v y # label(Def_join).  [copy(2),flip(a)].
21 f(f(x,y),f(x,y)) = x ^ y # label(Def_meet).  [copy(3),flip(a)].
22 f(x,x) = c(x) # label(Def_complement).  [copy(4),flip(a)].
23 c(f(x,y)) = x ^ y.  [back_demod(21),demod(22(3))].
24 f(c(x),c(y)) = x v y.  [back_demod(20),demod(22(1),22(2))].
25 f(f(f(f(x,y),f(y,z)),u),f(y,f(f(z,f(c(y),z)),z))) = y.  [back_demod(19),demod(22(5))].
39 (c26 ^ c27) ^ c28 != c26 ^ (c27 ^ c28) # answer(assoc_meet).  [clausify].
40 x ^ x = c(c(x)).  [para(22(a,1),23(a,1,1)),flip(a)].
42 c(c(x)) = x v x.  [para(24(a,1),22(a,1)),flip(a)].
43 c(x) ^ c(y) = c(x v y).  [para(24(a,1),23(a,1,1)),flip(a)].
47 x ^ x = x v x.  [back_demod(40),demod(42(3))].
49 f(f(f(c(x),f(x,y)),z),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(22(a,1),25(a,1,1,1,1))].
50 f(f(f(f(x,y),c(y)),z),f(y,f(f(y,f(c(y),y)),y))) = y.  [para(22(a,1),25(a,1,1,1,2))].
51 f(f(x v x,y),f(x,f(f(x,f(c(x),x)),x))) = x.  [para(22(a,1),25(a,1,1,1)),demod(22(1),42(2))].
52 f(f(x,y) ^ f(y,z),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(22(a,1),25(a,1,1)),demod(23(4))].
56 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(24(a,1),25(a,1,1,1,1)),demod(42(8))].
58 f(f(f(f(x,y),f(y,c(z))),u),f(y,f(f(c(z),y v z),c(z)))) = y.  [para(24(a,1),25(a,1,2,2,1,2))].
59 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(25(a,1),25(a,1,1,1))].
62 f(x v x,c(y)) = c(x) v y.  [para(42(a,1),24(a,1,1))].
63 f(c(x),y v y) = x v c(y).  [para(42(a,1),24(a,1,2))].
65 c(x v x) = c(x) v c(x).  [para(42(a,1),42(a,1,1))].
69 (x v x) ^ c(y) = c(c(x) v y).  [para(42(a,1),43(a,1,1))].
74 f(x v x,y v y) = c(x) v c(y).  [para(42(a,1),62(a,1,2))].
92 (x v x) ^ (y v y) = c(c(x) v c(y)).  [para(42(a,1),69(a,1,2))].
167 f(x,f(c(x),f(f(y,f(x v x,y)),y))) = c(x).  [para(50(a,1),25(a,1,1)),demod(42(3))].
225 f(c(x) v y,f(x,f(f(x,f(c(x),x)),x))) = x.  [para(62(a,1),51(a,1,1))].
318 f(f(x,y v y) ^ (c(y) v z),f(y v y,f(f(c(z),(y v y) v z),c(z)))) = y v y.  [para(62(a,1),52(a,1,1,2)),demod(65(9),62(12),42(9))].
773 f((x v x) v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [para(24(a,1),225(a,1,2,2,1,2)),demod(42(2))].
782 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(225(a,1),167(a,1,2,2,1,2)),demod(42(3),42(18))].
1350 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(63(a,1),58(a,1,1,1,1)),demod(62(5))].
1641 f(f(x,y),f(y,f(f(z,f(c(y),z)),z))) = y.  [para(59(a,1),25(a,1,1))].
1643 f(c(x),f(x,f(f(y,f(c(x),y)),y))) = x.  [para(59(a,1),49(a,1,1))].
1646 f(x v y,f(c(y),f(f(z,f(y v y,z)),z))) = c(y).  [para(59(a,1),56(a,1,1))].
1649 f(c(x),f(x v x,x)) = x v x.  [back_demod(782),demod(1641(14))].
1665 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(1649(a,1),52(a,1,1,1)),demod(23(10))].
1666 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(1649(a,1),52(a,1,1,2)),demod(42(9))].
1711 f(c(x),f(x,f(f(c(y),x v y),c(y)))) = x.  [para(24(a,1),1643(a,1,2,2,1,2))].
1757 x v x = x.  [para(1643(a,1),1643(a,1,2,2,1,2)),demod(1641(13),22(2),22(3),42(2))].
1804 f(f(x,c(y)) ^ y,f(c(y),f(f(c(y),f(y,c(y))),c(y)))) = c(y).  [back_demod(1666),demod(1757(3),1757(5),22(5),1757(6),1757(6),22(6),1757(9),22(9))].
1805 f(x ^ f(c(x),y),f(c(x),f(f(y,f(x,y)),y))) = c(x).  [back_demod(1665),demod(1757(1),1757(1),22(1),1757(4),22(4),1757(5),47(5),1757(5),1757(10),22(10))].
1816 f(x v y,f(c(y),f(f(z,f(y,z)),z))) = c(y).  [back_demod(1646),demod(1757(3))].
1969 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_demod(1350),demod(1757(7),1757(8),1757(14))].
2166 f(x v y,f(c(x),f(f(c(x),c(x) v x),c(x)))) = c(x).  [back_demod(773),demod(1757(1))].
2332 f(f(x,y) ^ (c(y) v z),f(y,f(f(c(z),y v z),c(z)))) = y.  [back_demod(318),demod(1757(1),1757(5),1757(6),1757(12))].
2409 x ^ y = c(c(x) v c(y)).  [back_demod(92),demod(1757(1),1757(1))].
2419 f(x,y) = c(x) v c(y).  [back_demod(74),demod(1757(1),1757(1))].
2425 c(c(x)) = x.  [back_demod(42),demod(1757(3))].
2434 (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_demod(2332),demod(2419(1),2409(6),2419(12),2425(11),2419(14),2425(15),2419(15),2419(18),2425(10))].
2447 (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_demod(1805),demod(2419(2),2425(2),2409(3),2419(8),2419(11),2419(14),2419(17),2425(8),2419(18),2425(7))].
2448 (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_demod(1804),demod(2419(2),2425(3),2409(3),2419(10),2425(11),2419(11),2425(9),2419(13),2425(14),2419(14),2425(8),2419(15),2425(7))].
2474 c((c(c26) v c(c27)) v c(c28)) != c(c(c26) v (c(c27) v c(c28))) # answer(assoc_meet).  [back_demod(39),demod(2409(3),2409(8),2425(7),2409(13),2409(17),2425(18))].
2486 c(x v y) v c(x v c(c(x v c(c(x) v x)) v x)) = c(x).  [back_demod(2166),demod(2419(6),2425(4),2419(8),2425(9),2419(9),2425(3),2419(10))].
2489 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_demod(1969),demod(2419(5),2419(8),2419(13),2425(12),2