%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL018-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:36 PM UTC 2026
% Result : Unsatisfiable 34.85s 5.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL018-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 04:02:53 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 34.85/5.21 % Refutation found
% 34.85/5.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 34.85/5.21 % SZS output start CNFRefutation for theBenchmark
% 34.85/5.21 fof(f1,axiom,(
% 34.85/5.21 (![A,B]: (join(A,B) = join(B,A) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f2,axiom,(
% 34.85/5.21 (![A,B,C]: (join(A,join(B,C)) = join(join(A,B),C) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f3,axiom,(
% 34.85/5.21 (![A,B]: (A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f4,axiom,(
% 34.85/5.21 (![A,B]: (meet(A,B) = complement(join(complement(A),complement(B))) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f5,axiom,(
% 34.85/5.21 (![A,B,C]: (composition(A,composition(B,C)) = composition(composition(A,B),C) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f6,axiom,(
% 34.85/5.21 (![A]: (composition(A,one) = A ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f7,axiom,(
% 34.85/5.21 (![A,B,C]: (composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f8,axiom,(
% 34.85/5.21 (![A]: (converse(converse(A)) = A ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f9,axiom,(
% 34.85/5.21 (![A,B]: (converse(join(A,B)) = join(converse(A),converse(B)) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f10,axiom,(
% 34.85/5.21 (![A,B]: (converse(composition(A,B)) = composition(converse(B),converse(A)) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f11,axiom,(
% 34.85/5.21 (![A,B]: (join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f12,axiom,(
% 34.85/5.21 (![A]: (top = join(A,complement(A)) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f13,axiom,(
% 34.85/5.21 (![A]: (zero = meet(A,complement(A)) ))),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f14,negated_conjecture,(
% 34.85/5.21 composition(sk1,top) = sk1 ),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f15,negated_conjecture,(
% 34.85/5.21 composition(complement(sk1),top) != complement(sk1) ),
% 34.85/5.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.85/5.21 fof(f16,plain,(
% 34.85/5.21 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f1])).
% 34.85/5.21 fof(f17,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f2])).
% 34.85/5.21 fof(f18,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f3])).
% 34.85/5.21 fof(f19,plain,(
% 34.85/5.21 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f4])).
% 34.85/5.21 fof(f20,plain,(
% 34.85/5.21 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f5])).
% 34.85/5.21 fof(f21,plain,(
% 34.85/5.21 ![X0]: (composition(X0,one)=X0)),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f6])).
% 34.85/5.21 fof(f22,plain,(
% 34.85/5.21 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f7])).
% 34.85/5.21 fof(f23,plain,(
% 34.85/5.21 ![X0]: (converse(converse(X0))=X0)),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f8])).
% 34.85/5.21 fof(f24,plain,(
% 34.85/5.21 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f9])).
% 34.85/5.21 fof(f25,plain,(
% 34.85/5.21 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f10])).
% 34.85/5.21 fof(f26,plain,(
% 34.85/5.21 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f11])).
% 34.85/5.21 fof(f27,plain,(
% 34.85/5.21 ![X0]: (top=join(X0,complement(X0)))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f12])).
% 34.85/5.21 fof(f28,plain,(
% 34.85/5.21 ![X0]: (zero=meet(X0,complement(X0)))),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f13])).
% 34.85/5.21 fof(f29,plain,(
% 34.85/5.21 composition(sk1,top)=sk1),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f14])).
% 34.85/5.21 fof(f30,plain,(
% 34.85/5.21 ~composition(complement(sk1),top)=complement(sk1)),
% 34.85/5.21 inference(cnf_transformation,[status(thm)],[f15])).
% 34.85/5.21 fof(f31,definition,(
% 34.85/5.21 sF1_fnc=complement(sk1)),
% 34.85/5.21 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 34.85/5.21 fof(f32,definition,(
% 34.85/5.21 sF0_fnc=composition(sF1_fnc,top)),
% 34.85/5.21 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 34.85/5.21 fof(f33,plain,(
% 34.85/5.21 ~sF0_fnc=sF1_fnc),
% 34.85/5.21 inference(definition_folding,[],[f30,f32,f31])).
% 34.85/5.21 fof(f34,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 34.85/5.21 fof(f35,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 34.85/5.21 inference(backward_demodulation,[status(thm)],[f19,f34])).
% 34.85/5.21 fof(f36,plain,(
% 34.85/5.21 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 34.85/5.21 fof(f37,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f35])).
% 34.85/5.21 fof(f38,plain,(
% 34.85/5.21 top=join(sk1,sF1_fnc)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f31,f27])).
% 34.85/5.21 fof(f40,plain,(
% 34.85/5.21 ![X0]: (composition(sF1_fnc,composition(top,X0))=composition(sF0_fnc,X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f32,f20])).
% 34.85/5.21 fof(f50,plain,(
% 34.85/5.21 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f27,f37])).
% 34.85/5.21 fof(f52,plain,(
% 34.85/5.21 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f50])).
% 34.85/5.21 fof(f68,plain,(
% 34.85/5.21 ![X0]: (composition(join(X0,sF1_fnc),top)=join(composition(X0,top),sF0_fnc))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f32,f22])).
% 34.85/5.21 fof(f70,plain,(
% 34.85/5.21 ![X0]: (composition(join(X0,sk1),top)=join(composition(X0,top),sk1))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f29,f22])).
% 34.85/5.21 fof(f77,plain,(
% 34.85/5.21 ![X0]: (composition(join(X0,sF1_fnc),top)=join(sF0_fnc,composition(X0,top)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f68])).
% 34.85/5.21 fof(f82,plain,(
% 34.85/5.21 ![X0]: (composition(join(X0,sk1),top)=join(sk1,composition(X0,top)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f70])).
% 34.85/5.21 fof(f185,plain,(
% 34.85/5.21 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f21,f20])).
% 34.85/5.21 fof(f240,plain,(
% 34.85/5.21 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f22,f16])).
% 34.85/5.21 fof(f252,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f37])).
% 34.85/5.21 fof(f258,plain,(
% 34.85/5.21 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f24])).
% 34.85/5.21 fof(f260,plain,(
% 34.85/5.21 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f23,f24])).
% 34.85/5.21 fof(f264,plain,(
% 34.85/5.21 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f24,f258])).
% 34.85/5.21 fof(f273,plain,(
% 34.85/5.21 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f23,f25])).
% 34.85/5.21 fof(f281,plain,(
% 34.85/5.21 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f27,f19])).
% 34.85/5.21 fof(f282,plain,(
% 34.85/5.21 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f19])).
% 34.85/5.21 fof(f285,plain,(
% 34.85/5.21 ![X0]: (meet(sk1,X0)=complement(join(sF1_fnc,complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f31,f19])).
% 34.85/5.21 fof(f286,plain,(
% 34.85/5.21 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f19])).
% 34.85/5.21 fof(f288,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f37])).
% 34.85/5.21 fof(f291,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f37])).
% 34.85/5.21 fof(f294,plain,(
% 34.85/5.21 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 34.85/5.21 inference(backward_demodulation,[status(thm)],[f296,f52])).
% 34.85/5.21 fof(f296,plain,(
% 34.85/5.21 zero=complement(top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f28,f281])).
% 34.85/5.21 fof(f298,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f288])).
% 34.85/5.21 fof(f300,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),meet(join(complement(X0),complement(X1)),X2)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f291])).
% 34.85/5.21 fof(f302,plain,(
% 34.85/5.21 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f296,f19])).
% 34.85/5.21 fof(f303,plain,(
% 34.85/5.21 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f296,f19])).
% 34.85/5.21 fof(f306,plain,(
% 34.85/5.21 top=join(top,zero)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f296,f27])).
% 34.85/5.21 fof(f307,plain,(
% 34.85/5.21 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f302])).
% 34.85/5.21 fof(f308,plain,(
% 34.85/5.21 top=join(zero,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f306])).
% 34.85/5.21 fof(f326,plain,(
% 34.85/5.21 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f27,f17])).
% 34.85/5.21 fof(f327,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f17])).
% 34.85/5.21 fof(f340,plain,(
% 34.85/5.21 ![X0,X1,X2,X3]: (join(composition(X0,X1),join(composition(X2,X1),X3))=join(composition(join(X0,X2),X1),X3))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f22,f17])).
% 34.85/5.21 fof(f344,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f37,f17])).
% 34.85/5.21 fof(f347,plain,(
% 34.85/5.21 ![X0]: (join(sk1,join(sF1_fnc,X0))=join(top,X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f38,f17])).
% 34.85/5.21 fof(f348,plain,(
% 34.85/5.21 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f27,f17])).
% 34.85/5.21 fof(f349,plain,(
% 34.85/5.21 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f17])).
% 34.85/5.21 fof(f368,plain,(
% 34.85/5.21 ![X0,X1]: (join(complement(converse(X0)),composition(converse(converse(X1)),complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f25,f36])).
% 34.85/5.21 fof(f374,plain,(
% 34.85/5.21 join(complement(top),composition(converse(sk1),complement(sk1)))=complement(top)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f29,f36])).
% 34.85/5.21 fof(f382,plain,(
% 34.85/5.21 ![X0,X1]: (join(complement(converse(X0)),composition(X1,complement(converse(composition(X0,X1)))))=complement(converse(X0)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f23,f368])).
% 34.85/5.21 fof(f387,plain,(
% 34.85/5.21 join(zero,composition(converse(sk1),complement(sk1)))=complement(top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f296,f374])).
% 34.85/5.21 fof(f388,plain,(
% 34.85/5.21 join(zero,composition(converse(sk1),sF1_fnc))=complement(top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f31,f387])).
% 34.85/5.21 fof(f389,plain,(
% 34.85/5.21 join(zero,composition(converse(sk1),sF1_fnc))=zero),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f296,f388])).
% 34.85/5.21 fof(f409,plain,(
% 34.85/5.21 ![X0]: (join(sk1,join(X0,sF1_fnc))=join(top,X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f16,f347])).
% 34.85/5.21 fof(f444,plain,(
% 34.85/5.21 meet(sk1,sk1)=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f31,f285])).
% 34.85/5.21 fof(f474,plain,(
% 34.85/5.21 meet(top,top)=complement(join(zero,zero))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f296,f307])).
% 34.85/5.21 fof(f535,plain,(
% 34.85/5.21 top=join(join(sF1_fnc,sF1_fnc),meet(sk1,sk1))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f444,f27])).
% 34.85/5.21 fof(f545,plain,(
% 34.85/5.21 top=join(sF1_fnc,join(sF1_fnc,meet(sk1,sk1)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f17,f535])).
% 34.85/5.21 fof(f577,plain,(
% 34.85/5.21 ![X0]: (meet(top,X0)=meet(X0,top))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f307,f303])).
% 34.85/5.21 fof(f586,plain,(
% 34.85/5.21 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X0,X1))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f303])).
% 34.85/5.21 fof(f593,plain,(
% 34.85/5.21 ![X0]: (join(zero,complement(X0))=join(zero,meet(join(zero,complement(X0)),complement(meet(top,X0)))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f303,f294])).
% 34.85/5.21 fof(f633,plain,(
% 34.85/5.21 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f577,f37])).
% 34.85/5.21 fof(f638,plain,(
% 34.85/5.21 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f633])).
% 34.85/5.21 fof(f652,plain,(
% 34.85/5.21 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f22,f240])).
% 34.85/5.21 fof(f719,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f252])).
% 34.85/5.21 fof(f742,plain,(
% 34.85/5.21 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f719])).
% 34.85/5.21 fof(f879,plain,(
% 34.85/5.21 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f21,f273])).
% 34.85/5.21 fof(f898,plain,(
% 34.85/5.21 ![X0]: (X0=composition(converse(one),X0))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f23,f879])).
% 34.85/5.21 fof(f910,plain,(
% 34.85/5.21 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f185,f898])).
% 34.85/5.21 fof(f911,plain,(
% 34.85/5.21 one=converse(one)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f21,f898])).
% 34.85/5.21 fof(f912,plain,(
% 34.85/5.21 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f898,f36])).
% 34.85/5.21 fof(f920,plain,(
% 34.85/5.21 composition(join(converse(one),sk1),top)=join(sk1,top)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f898,f82])).
% 34.85/5.21 fof(f925,plain,(
% 34.85/5.21 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(X1,composition(X0,X1)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f898,f240])).
% 34.85/5.21 fof(f937,plain,(
% 34.85/5.21 ![X0]: (composition(one,X0)=X0)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f898,f910])).
% 34.85/5.21 fof(f939,plain,(
% 34.85/5.21 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f937,f912])).
% 34.85/5.21 fof(f946,plain,(
% 34.85/5.21 composition(join(sk1,converse(one)),top)=join(sk1,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f652,f920])).
% 34.85/5.21 fof(f947,plain,(
% 34.85/5.21 composition(join(sk1,one),top)=join(sk1,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f911,f946])).
% 34.85/5.21 fof(f948,plain,(
% 34.85/5.21 composition(join(one,sk1),top)=join(sk1,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f652,f947])).
% 34.85/5.21 fof(f949,plain,(
% 34.85/5.21 composition(join(one,sk1),top)=join(top,sk1)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f948])).
% 34.85/5.21 fof(f962,plain,(
% 34.85/5.21 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f911,f925])).
% 34.85/5.21 fof(f985,plain,(
% 34.85/5.21 ![X0]: (converse(join(X0,one))=join(one,converse(X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f911,f258])).
% 34.85/5.21 fof(f1035,plain,(
% 34.85/5.21 join(zero,complement(top))=complement(top)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f296,f939])).
% 34.85/5.21 fof(f1036,plain,(
% 34.85/5.21 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f474,f939])).
% 34.85/5.21 fof(f1038,plain,(
% 34.85/5.21 ![X0]: (join(meet(X0,top),complement(join(zero,complement(X0))))=complement(join(zero,complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f307,f939])).
% 34.85/5.21 fof(f1039,plain,(
% 34.85/5.21 join(meet(sk1,sk1),complement(join(sF1_fnc,sF1_fnc)))=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f444,f939])).
% 34.85/5.21 fof(f1042,plain,(
% 34.85/5.21 join(sF1_fnc,complement(sk1))=complement(sk1)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f31,f939])).
% 34.85/5.21 fof(f1044,plain,(
% 34.85/5.21 join(complement(join(zero,zero)),meet(top,top))=complement(join(zero,zero))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f474,f939])).
% 34.85/5.21 fof(f1047,plain,(
% 34.85/5.21 join(complement(join(sF1_fnc,sF1_fnc)),meet(sk1,sk1))=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f444,f939])).
% 34.85/5.21 fof(f1051,plain,(
% 34.85/5.21 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f939,f19])).
% 34.85/5.21 fof(f1052,plain,(
% 34.85/5.21 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f939,f37])).
% 34.85/5.21 fof(f1055,plain,(
% 34.85/5.21 join(zero,zero)=complement(top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f296,f1035])).
% 34.85/5.21 fof(f1064,plain,(
% 34.85/5.21 join(zero,zero)=zero),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f296,f1055])).
% 34.85/5.21 fof(f1065,plain,(
% 34.85/5.21 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f474,f1036])).
% 34.85/5.21 fof(f1066,plain,(
% 34.85/5.21 join(meet(top,top),meet(top,top))=meet(top,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f474,f1065])).
% 34.85/5.21 fof(f1070,plain,(
% 34.85/5.21 ![X0]: (join(meet(X0,top),meet(top,X0))=complement(join(zero,complement(X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f303,f1038])).
% 34.85/5.21 fof(f1071,plain,(
% 34.85/5.21 ![X0]: (join(meet(X0,top),meet(top,X0))=meet(top,X0))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f303,f1070])).
% 34.85/5.21 fof(f1072,plain,(
% 34.85/5.21 join(meet(sk1,sk1),meet(sk1,sk1))=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f444,f1039])).
% 34.85/5.21 fof(f1073,plain,(
% 34.85/5.21 join(meet(sk1,sk1),meet(sk1,sk1))=meet(sk1,sk1)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f444,f1072])).
% 34.85/5.21 fof(f1081,plain,(
% 34.85/5.21 join(sF1_fnc,sF1_fnc)=complement(sk1)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f31,f1042])).
% 34.85/5.21 fof(f1098,plain,(
% 34.85/5.21 join(sF1_fnc,sF1_fnc)=sF1_fnc),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f31,f1081])).
% 34.85/5.21 fof(f1102,plain,(
% 34.85/5.21 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1044])).
% 34.85/5.21 fof(f1103,plain,(
% 34.85/5.21 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f474,f1102])).
% 34.85/5.21 fof(f1104,plain,(
% 34.85/5.21 meet(top,top)=complement(join(zero,zero))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f1066,f1103])).
% 34.85/5.21 fof(f1105,plain,(
% 34.85/5.21 meet(top,top)=complement(zero)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f1064,f1104])).
% 34.85/5.21 fof(f1112,plain,(
% 34.85/5.21 join(meet(sk1,sk1),complement(join(sF1_fnc,sF1_fnc)))=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1047])).
% 34.85/5.21 fof(f1113,plain,(
% 34.85/5.21 join(meet(sk1,sk1),meet(sk1,sk1))=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f444,f1112])).
% 34.85/5.21 fof(f1114,plain,(
% 34.85/5.21 meet(sk1,sk1)=complement(join(sF1_fnc,sF1_fnc))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f1073,f1113])).
% 34.85/5.21 fof(f1115,plain,(
% 34.85/5.21 top=join(sF1_fnc,join(sF1_fnc,complement(sF1_fnc)))),
% 34.85/5.21 inference(backward_demodulation,[status(thm)],[f1116,f545])).
% 34.85/5.21 fof(f1116,plain,(
% 34.85/5.21 meet(sk1,sk1)=complement(sF1_fnc)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f1098,f1114])).
% 34.85/5.21 fof(f1126,plain,(
% 34.85/5.21 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1052])).
% 34.85/5.21 fof(f1127,plain,(
% 34.85/5.21 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f28,f1126])).
% 34.85/5.21 fof(f1128,plain,(
% 34.85/5.21 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1127])).
% 34.85/5.21 fof(f1166,plain,(
% 34.85/5.21 top=join(sF1_fnc,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f27,f1115])).
% 34.85/5.21 fof(f1168,plain,(
% 34.85/5.21 top=join(top,sF1_fnc)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1166])).
% 34.85/5.21 fof(f1175,plain,(
% 34.85/5.21 join(sk1,top)=join(top,top)),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f1168,f409])).
% 34.85/5.21 fof(f1179,plain,(
% 34.85/5.21 composition(join(one,sk1),top)=join(top,top)),
% 34.85/5.21 inference(backward_demodulation,[status(thm)],[f1182,f949])).
% 34.85/5.21 fof(f1182,plain,(
% 34.85/5.21 join(top,sk1)=join(top,top)),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1175])).
% 34.85/5.21 fof(f1372,plain,(
% 34.85/5.21 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f282])).
% 34.85/5.21 fof(f1398,plain,(
% 34.85/5.21 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X1,X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f282,f303])).
% 34.85/5.21 fof(f1405,plain,(
% 34.85/5.21 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X1,X0),complement(X2))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f282,f19])).
% 34.85/5.21 fof(f1413,plain,(
% 34.85/5.21 ![X0]: (join(zero,complement(X0))=join(zero,meet(complement(meet(top,X0)),join(zero,complement(X0)))))),
% 34.85/5.21 inference(backward_demodulation,[status(thm)],[f1372,f593])).
% 34.85/5.21 fof(f1582,plain,(
% 34.85/5.21 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f1128,f303])).
% 34.85/5.21 fof(f1604,plain,(
% 34.85/5.21 ![X0,X1]: (meet(top,meet(X0,X1))=complement(join(complement(X1),complement(X0))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f282,f1582])).
% 34.85/5.21 fof(f1611,plain,(
% 34.85/5.21 ![X0]: (top=join(meet(top,X0),complement(X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f1582,f298])).
% 34.85/5.21 fof(f1632,plain,(
% 34.85/5.21 ![X0,X1]: (meet(top,meet(X0,X1))=meet(X0,X1))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f282,f1604])).
% 34.85/5.21 fof(f1641,plain,(
% 34.85/5.21 ![X0]: (top=join(complement(X0),meet(top,X0)))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1611])).
% 34.85/5.21 fof(f1729,plain,(
% 34.85/5.21 ![X0]: (X0=join(meet(X0,meet(top,X0)),complement(top)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f1641,f37])).
% 34.85/5.21 fof(f1740,plain,(
% 34.85/5.21 ![X0]: (X0=join(complement(top),meet(X0,meet(top,X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f16,f1729])).
% 34.85/5.21 fof(f1742,plain,(
% 34.85/5.21 ![X0]: (X0=join(zero,meet(X0,meet(top,X0))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f296,f1740])).
% 34.85/5.21 fof(f1789,plain,(
% 34.85/5.21 ![X0]: (zero=meet(complement(X0),meet(X0,X0)))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f1051,f28])).
% 34.85/5.21 fof(f1831,plain,(
% 34.85/5.21 ![X0,X1]: (zero=meet(meet(X0,X1),meet(join(complement(X0),complement(X1)),join(complement(X0),complement(X1)))))),
% 34.85/5.21 inference(paramodulation,[status(thm)],[f19,f1789])).
% 34.85/5.21 fof(f1853,plain,(
% 34.85/5.21 ![X0,X1]: (zero=meet(meet(X0,X1),complement(complement(join(complement(X0),complement(X1))))))),
% 34.85/5.21 inference(forward_demodulation,[status(thm)],[f1051,f1831])).
% 37.62/5.23 fof(f1856,plain,(
% 37.62/5.23 ![X0,X1]: (zero=meet(meet(X0,X1),complement(meet(X1,X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f282,f1853])).
% 37.62/5.23 fof(f1943,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),complement(join(complement(X0),complement(X1))))),zero))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f28,f300])).
% 37.62/5.23 fof(f1949,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(complement(complement(X0)),complement(X1))=join(complement(join(meet(complement(X0),X1),X2)),meet(join(meet(X0,X0),complement(X1)),X2)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f1051,f300])).
% 37.62/5.23 fof(f1952,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(complement(join(zero,complement(X0))),complement(X1))=join(complement(join(meet(join(zero,complement(X0)),X1),X2)),meet(join(meet(X0,top),complement(X1)),X2)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f307,f300])).
% 37.62/5.23 fof(f2035,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(join(complement(X0),complement(X1)))))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f1943])).
% 37.62/5.23 fof(f2036,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(join(complement(X1),complement(X0)),join(complement(X0),complement(X1)))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1405,f2035])).
% 37.62/5.23 fof(f2049,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(meet(top,X0),complement(X1))=join(complement(join(meet(join(zero,complement(X0)),X1),X2)),meet(join(meet(X0,top),complement(X1)),X2)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f303,f1952])).
% 37.62/5.23 fof(f2050,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(meet(top,X0),complement(X1))=join(meet(join(meet(X0,top),complement(X1)),X2),complement(join(meet(join(zero,complement(X0)),X1),X2))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2049])).
% 37.62/5.23 fof(f2158,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),complement(top)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f326,f37])).
% 37.62/5.23 fof(f2234,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2158])).
% 37.62/5.23 fof(f2235,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f296,f2234])).
% 37.62/5.23 fof(f2374,plain,(
% 37.62/5.23 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f939,f348])).
% 37.62/5.23 fof(f2378,plain,(
% 37.62/5.23 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f27,f348])).
% 37.62/5.23 fof(f2379,plain,(
% 37.62/5.23 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f16,f348])).
% 37.62/5.23 fof(f2382,plain,(
% 37.62/5.23 ![X0]: (join(top,join(zero,X0))=join(top,X0))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f296,f348])).
% 37.62/5.23 fof(f2397,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f348,f37])).
% 37.62/5.23 fof(f2409,plain,(
% 37.62/5.23 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2410,f638])).
% 37.62/5.23 fof(f2410,plain,(
% 37.62/5.23 ![X0]: (top=join(top,complement(X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f27,f2374])).
% 37.62/5.23 fof(f2418,plain,(
% 37.62/5.23 composition(join(one,sk1),top)=top),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2424,f1179])).
% 37.62/5.23 fof(f2424,plain,(
% 37.62/5.23 ![X0]: (join(X0,top)=top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2410,f2378])).
% 37.62/5.23 fof(f2425,plain,(
% 37.62/5.23 ![X0]: (join(zero,join(X0,top))=join(top,X0))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f327,f2382])).
% 37.62/5.23 fof(f2426,plain,(
% 37.62/5.23 ![X0]: (join(zero,top)=join(top,X0))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2424,f2425])).
% 37.62/5.23 fof(f2445,plain,(
% 37.62/5.23 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2452,f2379])).
% 37.62/5.23 fof(f2452,plain,(
% 37.62/5.23 ![X0]: (top=join(top,X0))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f308,f2426])).
% 37.62/5.23 fof(f2483,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2397])).
% 37.62/5.23 fof(f2484,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2452,f2483])).
% 37.62/5.23 fof(f2485,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f296,f2484])).
% 37.62/5.23 fof(f2499,plain,(
% 37.62/5.23 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2409])).
% 37.62/5.23 fof(f2502,plain,(
% 37.62/5.23 ![X0]: (X0=join(zero,meet(top,X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f296,f2499])).
% 37.62/5.23 fof(f2542,plain,(
% 37.62/5.23 ![X0]: (converse(top)=join(X0,converse(top)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2424,f260])).
% 37.62/5.23 fof(f2544,plain,(
% 37.62/5.23 ![X0]: (X0=join(meet(X0,top),complement(top)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2424,f37])).
% 37.62/5.23 fof(f2555,plain,(
% 37.62/5.23 ![X0]: (X0=join(complement(top),meet(X0,top)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2544])).
% 37.62/5.23 fof(f2557,plain,(
% 37.62/5.23 ![X0]: (X0=join(zero,meet(X0,top)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f296,f2555])).
% 37.62/5.23 fof(f2638,plain,(
% 37.62/5.23 meet(top,top)=top),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f1742,f2502])).
% 37.62/5.23 fof(f2644,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,X1)=join(zero,meet(X0,X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f1632,f2502])).
% 37.62/5.23 fof(f2645,plain,(
% 37.62/5.23 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f1582,f2502])).
% 37.62/5.23 fof(f2657,plain,(
% 37.62/5.23 top=complement(zero)),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2638,f1105])).
% 37.62/5.23 fof(f2659,plain,(
% 37.62/5.23 ![X0]: (X0=meet(top,X0))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f2502])).
% 37.62/5.23 fof(f2661,plain,(
% 37.62/5.23 ![X0]: (X0=meet(X0,top))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f2557])).
% 37.62/5.23 fof(f2662,plain,(
% 37.62/5.23 ![X0]: (X0=meet(X0,meet(top,X0)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f1742])).
% 37.62/5.23 fof(f2669,plain,(
% 37.62/5.23 ![X0]: (join(zero,complement(X0))=meet(complement(meet(top,X0)),join(zero,complement(X0))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f1413])).
% 37.62/5.23 fof(f2680,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=meet(join(complement(X1),complement(X0)),join(complement(X0),complement(X1))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f2036])).
% 37.62/5.23 fof(f2682,plain,(
% 37.62/5.23 ![X0,X1]: (X0=meet(X0,join(complement(complement(X0)),X1)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f2485])).
% 37.62/5.23 fof(f2683,plain,(
% 37.62/5.23 ![X0,X1]: (X0=meet(X0,join(X1,complement(join(complement(X0),X1)))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f2235])).
% 37.62/5.23 fof(f2687,plain,(
% 37.62/5.23 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(meet(X1,X0)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f1398])).
% 37.62/5.23 fof(f2688,plain,(
% 37.62/5.23 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(meet(X0,X1)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2644,f586])).
% 37.62/5.23 fof(f2689,plain,(
% 37.62/5.23 ![X0]: (X0=complement(complement(X0)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2645,f1128])).
% 37.62/5.23 fof(f2699,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(meet(top,X0),complement(X1))=join(meet(join(meet(X0,top),complement(X1)),X2),complement(join(meet(complement(X0),X1),X2))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2645,f2050])).
% 37.62/5.23 fof(f2734,plain,(
% 37.62/5.23 ![X0]: (join(meet(X0,top),meet(top,X0))=X0)),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2659,f1071])).
% 37.62/5.23 fof(f2757,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(complement(complement(X0)),complement(X1))=join(complement(join(meet(complement(X0),X1),X2)),meet(join(X0,complement(X1)),X2)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2771,f1949])).
% 37.62/5.23 fof(f2771,plain,(
% 37.62/5.23 ![X0]: (X0=meet(X0,X0))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2662])).
% 37.62/5.23 fof(f2778,plain,(
% 37.62/5.23 ![X0]: (complement(X0)=meet(complement(meet(top,X0)),join(zero,complement(X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2645,f2669])).
% 37.62/5.23 fof(f2779,plain,(
% 37.62/5.23 ![X0]: (complement(X0)=meet(complement(X0),join(zero,complement(X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2778])).
% 37.62/5.23 fof(f2780,plain,(
% 37.62/5.23 ![X0]: (complement(X0)=meet(complement(X0),complement(X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2645,f2779])).
% 37.62/5.23 fof(f2781,plain,(
% 37.62/5.23 ![X0]: (complement(X0)=complement(complement(complement(X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1051,f2780])).
% 37.62/5.23 fof(f2821,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=meet(join(complement(X1),complement(X0)),complement(meet(X1,X0))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2856,f2680])).
% 37.62/5.23 fof(f2854,plain,(
% 37.62/5.23 ![X0,X1,X2]: (meet(X0,complement(meet(X1,X2)))=complement(join(complement(X0),meet(X2,X1))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2856,f286])).
% 37.62/5.23 fof(f2856,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2687])).
% 37.62/5.23 fof(f2857,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2688])).
% 37.62/5.23 fof(f2859,plain,(
% 37.62/5.23 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f2689,f2682])).
% 37.62/5.23 fof(f2878,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(X0,complement(X1))=join(meet(join(meet(X0,top),complement(X1)),X2),complement(join(meet(complement(X0),X1),X2))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2699])).
% 37.62/5.23 fof(f2879,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(X0,complement(X1))=join(complement(join(meet(complement(X0),X1),X2)),meet(join(meet(X0,top),complement(X1)),X2)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2878])).
% 37.62/5.23 fof(f2880,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(X0,complement(X1))=join(complement(join(meet(complement(X0),X1),X2)),meet(join(X0,complement(X1)),X2)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2661,f2879])).
% 37.62/5.23 fof(f2881,plain,(
% 37.62/5.23 ![X0,X1,X2]: (join(X0,complement(X1))=join(meet(join(X0,complement(X1)),X2),complement(join(meet(complement(X0),X1),X2))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2880])).
% 37.62/5.23 fof(f2939,plain,(
% 37.62/5.23 ![X0]: (join(X0,meet(top,X0))=X0)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2661,f2734])).
% 37.62/5.23 fof(f2947,plain,(
% 37.62/5.23 ![X0]: (join(X0,X0)=X0)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2659,f2939])).
% 37.62/5.23 fof(f2962,plain,(
% 37.62/5.23 ![X0,X1,X2]: (complement(meet(complement(X0),X1))=join(complement(join(meet(complement(X0),X1),X2)),meet(join(X0,complement(X1)),X2)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2857,f2757])).
% 37.62/5.23 fof(f2963,plain,(
% 37.62/5.23 ![X0,X1,X2]: (complement(meet(complement(X0),X1))=join(meet(join(X0,complement(X1)),X2),complement(join(meet(complement(X0),X1),X2))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f2962])).
% 37.62/5.23 fof(f2964,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(complement(X0),X1))=join(X0,complement(X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2881,f2963])).
% 37.62/5.23 fof(f3010,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(X0,X1))=meet(join(complement(X1),complement(X0)),complement(meet(X1,X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2857,f2821])).
% 37.62/5.23 fof(f3011,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(X0,X1))=meet(complement(meet(X1,X0)),join(complement(X1),complement(X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1372,f3010])).
% 37.62/5.23 fof(f3012,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(X0,X1))=meet(complement(meet(X1,X0)),complement(meet(X1,X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2857,f3011])).
% 37.62/5.23 fof(f3013,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(X0,X1))=complement(complement(complement(meet(X1,X0)))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1051,f3012])).
% 37.62/5.23 fof(f3014,plain,(
% 37.62/5.23 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2781,f3013])).
% 37.62/5.23 fof(f3053,plain,(
% 37.62/5.23 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2771,f742])).
% 37.62/5.23 fof(f3082,plain,(
% 37.62/5.23 ![X0]: (X0=join(X0,zero))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f28,f3053])).
% 37.62/5.23 fof(f3166,plain,(
% 37.62/5.23 ![X0]: (X0=join(zero,X0))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f16,f3082])).
% 37.62/5.23 fof(f3171,plain,(
% 37.62/5.23 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3082,f260])).
% 37.62/5.23 fof(f3178,plain,(
% 37.62/5.23 composition(converse(sk1),sF1_fnc)=zero),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f3166,f389])).
% 37.62/5.23 fof(f3188,plain,(
% 37.62/5.23 ![X0]: (X0=join(X0,converse(zero)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f23,f3171])).
% 37.62/5.23 fof(f3309,plain,(
% 37.62/5.23 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2947,f327])).
% 37.62/5.23 fof(f3582,plain,(
% 37.62/5.23 ![X0,X1,X2,X3]: (join(composition(X0,X1),composition(join(X2,X3),X1))=join(composition(join(X0,X2),X1),composition(X3,X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f22,f340])).
% 37.62/5.23 fof(f3637,plain,(
% 37.62/5.23 ![X0,X1,X2,X3]: (composition(join(join(X0,X1),X2),X3)=join(composition(join(X2,X0),X3),composition(X1,X3)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f240,f3582])).
% 37.62/5.23 fof(f3638,plain,(
% 37.62/5.23 ![X0,X1,X2,X3]: (composition(join(X0,join(X1,X2)),X3)=join(composition(join(X2,X0),X3),composition(X1,X3)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f17,f3637])).
% 37.62/5.23 fof(f3639,plain,(
% 37.62/5.23 ![X0,X1,X2,X3]: (composition(join(X0,join(X1,X2)),X3)=composition(join(X1,join(X2,X0)),X3))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f240,f3638])).
% 37.62/5.23 fof(f3680,plain,(
% 37.62/5.23 converse(zero)=composition(converse(sF1_fnc),sk1)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3178,f273])).
% 37.62/5.23 fof(f3751,plain,(
% 37.62/5.23 join(complement(sk1),composition(converse(converse(sF1_fnc)),complement(converse(zero))))=complement(sk1)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3680,f36])).
% 37.62/5.23 fof(f3769,plain,(
% 37.62/5.23 join(sF1_fnc,composition(converse(converse(sF1_fnc)),complement(converse(zero))))=complement(sk1)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f31,f3751])).
% 37.62/5.23 fof(f3770,plain,(
% 37.62/5.23 join(sF1_fnc,composition(sF1_fnc,complement(converse(zero))))=complement(sk1)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f23,f3769])).
% 37.62/5.23 fof(f3771,plain,(
% 37.62/5.23 join(sF1_fnc,composition(sF1_fnc,complement(converse(zero))))=sF1_fnc),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f31,f3770])).
% 37.62/5.23 fof(f3810,plain,(
% 37.62/5.23 composition(join(join(one,sk1),sF1_fnc),top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2418,f77])).
% 37.62/5.23 fof(f3829,plain,(
% 37.62/5.23 composition(join(sF1_fnc,join(one,sk1)),top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f652,f3810])).
% 37.62/5.23 fof(f3830,plain,(
% 37.62/5.23 composition(join(sk1,join(sF1_fnc,one)),top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f3639,f3829])).
% 37.62/5.23 fof(f3831,plain,(
% 37.62/5.23 composition(join(one,join(sk1,sF1_fnc)),top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f3639,f3830])).
% 37.62/5.23 fof(f3832,plain,(
% 37.62/5.23 composition(join(one,top),top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f38,f3831])).
% 37.62/5.23 fof(f3833,plain,(
% 37.62/5.23 composition(top,top)=join(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2424,f3832])).
% 37.62/5.23 fof(f3838,plain,(
% 37.62/5.23 composition(top,top)=top),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2424,f3833])).
% 37.62/5.23 fof(f4013,plain,(
% 37.62/5.23 composition(sF1_fnc,top)=composition(sF0_fnc,top)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3838,f40])).
% 37.62/5.23 fof(f4029,plain,(
% 37.62/5.23 ![X0]: (composition(top,composition(top,X0))=composition(top,X0))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3838,f20])).
% 37.62/5.23 fof(f4030,plain,(
% 37.62/5.23 sF0_fnc=composition(sF0_fnc,top)),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f32,f4013])).
% 37.62/5.23 fof(f4117,plain,(
% 37.62/5.23 zero=converse(zero)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f3166,f3188])).
% 37.62/5.23 fof(f4150,plain,(
% 37.62/5.23 join(sF1_fnc,composition(sF1_fnc,complement(zero)))=sF1_fnc),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f4117,f3771])).
% 37.62/5.23 fof(f4171,plain,(
% 37.62/5.23 join(sF1_fnc,composition(sF1_fnc,top))=sF1_fnc),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2657,f4150])).
% 37.62/5.23 fof(f4172,plain,(
% 37.62/5.23 join(sF1_fnc,sF0_fnc)=sF1_fnc),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f32,f4171])).
% 37.62/5.23 fof(f4173,plain,(
% 37.62/5.23 join(sF0_fnc,sF1_fnc)=sF1_fnc),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f4172])).
% 37.62/5.23 fof(f4356,plain,(
% 37.62/5.23 ![X0,X1]: (converse(X0)=meet(converse(X0),converse(join(X0,X1))))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f24,f2859])).
% 37.62/5.23 fof(f4365,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f742,f2859])).
% 37.62/5.23 fof(f4397,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1372,f4365])).
% 37.62/5.23 fof(f4705,plain,(
% 37.62/5.23 converse(top)=top),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2452,f2542])).
% 37.62/5.23 fof(f4816,plain,(
% 37.62/5.23 ![X0]: (join(complement(X0),composition(top,complement(composition(top,X0))))=complement(X0))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f4705,f36])).
% 37.62/5.23 fof(f5024,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f1372,f4397])).
% 37.62/5.23 fof(f5112,plain,(
% 37.62/5.23 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=top)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f344,f2445])).
% 37.62/5.23 fof(f5494,plain,(
% 37.62/5.23 ![X0,X1]: (join(X0,complement(meet(X1,X0)))=top)),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f5024,f5112])).
% 37.62/5.23 fof(f6011,plain,(
% 37.62/5.23 join(complement(converse(sF0_fnc)),composition(top,complement(converse(sF0_fnc))))=complement(converse(sF0_fnc))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f4030,f382])).
% 37.62/5.23 fof(f6022,plain,(
% 37.62/5.23 join(complement(converse(sF1_fnc)),composition(top,complement(converse(sF0_fnc))))=complement(converse(sF1_fnc))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f32,f382])).
% 37.62/5.23 fof(f6068,plain,(
% 37.62/5.23 composition(join(top,one),complement(converse(sF0_fnc)))=complement(converse(sF0_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f962,f6011])).
% 37.62/5.23 fof(f6069,plain,(
% 37.62/5.23 composition(join(one,top),complement(converse(sF0_fnc)))=complement(converse(sF0_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f652,f6068])).
% 37.62/5.23 fof(f6070,plain,(
% 37.62/5.23 composition(top,complement(converse(sF0_fnc)))=complement(converse(sF0_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2424,f6069])).
% 37.62/5.23 fof(f6116,plain,(
% 37.62/5.23 join(complement(converse(sF1_fnc)),complement(converse(sF0_fnc)))=complement(converse(sF1_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f6070,f6022])).
% 37.62/5.23 fof(f6117,plain,(
% 37.62/5.23 join(complement(converse(sF0_fnc)),complement(converse(sF1_fnc)))=complement(converse(sF1_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f6116])).
% 37.62/5.23 fof(f6118,plain,(
% 37.62/5.23 complement(meet(converse(sF0_fnc),converse(sF1_fnc)))=complement(converse(sF1_fnc))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2857,f6117])).
% 37.62/5.23 fof(f7341,plain,(
% 37.62/5.23 ![X0,X1]: (join(complement(join(complement(X0),X1)),meet(X0,X1))=join(X0,meet(X0,X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f344,f3309])).
% 37.62/5.23 fof(f7440,plain,(
% 37.62/5.23 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),X1)))=join(X0,meet(X0,X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f16,f7341])).
% 37.62/5.23 fof(f7448,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f37,f7440])).
% 37.62/5.23 fof(f7632,plain,(
% 37.62/5.23 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f5024,f7448])).
% 37.62/5.23 fof(f15094,plain,(
% 37.62/5.23 ![X0,X1]: (top=complement(meet(meet(X0,complement(X1)),X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f5494,f2856])).
% 37.62/5.23 fof(f15147,plain,(
% 37.62/5.23 ![X0,X1]: (top=complement(meet(X0,meet(X1,complement(X0)))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f3014,f15094])).
% 37.62/5.23 fof(f15251,plain,(
% 37.62/5.23 ![X0,X1]: (zero=meet(meet(meet(X0,complement(X1)),X1),top))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f15147,f1856])).
% 37.62/5.23 fof(f15312,plain,(
% 37.62/5.23 ![X0,X1]: (zero=meet(meet(X0,complement(X1)),X1))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2661,f15251])).
% 37.62/5.23 fof(f15317,plain,(
% 37.62/5.23 ![X0,X1]: (zero=meet(X0,meet(X1,complement(X0))))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f1372,f15312])).
% 37.62/5.23 fof(f15410,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,complement(meet(X1,top)))=complement(join(complement(X0),X1)))),
% 37.62/5.23 inference(paramodulation,[status(thm)],[f2659,f2854])).
% 37.62/5.23 fof(f15562,plain,(
% 37.62/5.23 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 37.62/5.23 inference(backward_demodulation,[status(thm)],[f15563,f2683])).
% 37.62/5.23 fof(f15563,plain,(
% 37.62/5.23 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 37.62/5.23 inference(forward_demodulation,[status(thm)],[f2661,f15410])).
% 37.62/5.24 fof(f16600,plain,(
% 37.62/5.24 ![X0]: (join(complement(composition(top,X0)),composition(converse(top),complement(composition(top,X0))))=complement(composition(top,X0)))),
% 37.62/5.24 inference(paramodulation,[status(thm)],[f4029,f36])).
% 37.62/5.24 fof(f16655,plain,(
% 37.62/5.24 ![X0]: (composition(join(converse(top),one),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f962,f16600])).
% 37.62/5.24 fof(f16656,plain,(
% 37.62/5.24 ![X0]: (composition(join(one,converse(top)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f652,f16655])).
% 37.62/5.24 fof(f16657,plain,(
% 37.62/5.24 ![X0]: (composition(converse(join(top,one)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f985,f16656])).
% 37.62/5.24 fof(f16658,plain,(
% 37.62/5.24 ![X0]: (composition(converse(join(one,top)),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f264,f16657])).
% 37.62/5.24 fof(f16659,plain,(
% 37.62/5.24 ![X0]: (composition(converse(top),complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f2424,f16658])).
% 37.62/5.24 fof(f16664,plain,(
% 37.62/5.24 ![X0]: (join(complement(X0),complement(composition(top,X0)))=complement(X0))),
% 37.62/5.24 inference(backward_demodulation,[status(thm)],[f16665,f4816])).
% 37.62/5.24 fof(f16665,plain,(
% 37.62/5.24 ![X0]: (composition(top,complement(composition(top,X0)))=complement(composition(top,X0)))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f4705,f16659])).
% 37.62/5.24 fof(f16689,plain,(
% 37.62/5.24 ![X0]: (complement(meet(composition(top,X0),X0))=complement(X0))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f2856,f16664])).
% 37.62/5.24 fof(f16692,plain,(
% 37.62/5.24 ![X0]: (complement(meet(X0,composition(top,X0)))=complement(X0))),
% 37.62/5.24 inference(forward_demodulation,[status(thm)],[f3014,f16689])).
% 37.62/5.24 fof(f16821,plain,(
% 37.62/5.24 ![X0]: (meet(X0,composition(top,X0))=complement(complement(X0)))),
% 37.62/5.24 inference(paramodulation,[status(thm)],[f16692,f2689])).
% 37.62/5.24 fof(f16866,plain,(
% 37.62/5.29 ![X0]: (meet(X0,composition(top,X0))=X0)),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f2689,f16821])).
% 37.62/5.29 fof(f17307,plain,(
% 37.62/5.29 ![X0,X1]: (zero=meet(complement(X0),meet(X1,X0)))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f2689,f15317])).
% 37.62/5.29 fof(f17467,plain,(
% 37.62/5.29 ![X0]: (zero=meet(complement(composition(top,X0)),X0))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f16866,f17307])).
% 37.62/5.29 fof(f17522,plain,(
% 37.62/5.29 ![X0]: (zero=meet(X0,complement(composition(top,X0))))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f1372,f17467])).
% 37.62/5.29 fof(f19300,plain,(
% 37.62/5.29 ![X0,X1]: (X0=meet(X0,join(X1,meet(complement(X1),X0))))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f1372,f15562])).
% 37.62/5.29 fof(f19516,plain,(
% 37.62/5.29 ![X0,X1]: (join(X0,meet(complement(X0),X1))=join(join(X0,meet(complement(X0),X1)),X1))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f19300,f7632])).
% 37.62/5.29 fof(f19621,plain,(
% 37.62/5.29 ![X0,X1]: (join(X0,meet(complement(X0),X1))=join(meet(complement(X0),X1),join(X0,X1)))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f349,f19516])).
% 37.62/5.29 fof(f19622,plain,(
% 37.62/5.29 ![X0,X1]: (join(X0,meet(complement(X0),X1))=join(X0,join(X1,meet(complement(X0),X1))))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f327,f19621])).
% 37.62/5.29 fof(f19637,plain,(
% 37.62/5.29 ![X0,X1]: (join(X0,meet(complement(X0),X1))=join(X0,X1))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f7632,f19622])).
% 37.62/5.29 fof(f20581,plain,(
% 37.62/5.29 ![X0]: (join(X0,zero)=join(X0,complement(composition(top,complement(X0)))))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f17522,f19637])).
% 37.62/5.29 fof(f20652,plain,(
% 37.62/5.29 ![X0]: (X0=join(X0,complement(composition(top,complement(X0)))))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f3082,f20581])).
% 37.62/5.29 fof(f28262,plain,(
% 37.62/5.29 converse(sF0_fnc)=meet(converse(sF0_fnc),converse(sF1_fnc))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f4173,f4356])).
% 37.62/5.29 fof(f28419,plain,(
% 37.62/5.29 complement(converse(sF0_fnc))=complement(converse(sF1_fnc))),
% 37.62/5.29 inference(backward_demodulation,[status(thm)],[f28262,f6118])).
% 37.62/5.29 fof(f28529,plain,(
% 37.62/5.29 ![X0]: (complement(meet(complement(converse(sF0_fnc)),X0))=join(converse(sF1_fnc),complement(X0)))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f28419,f2964])).
% 37.62/5.29 fof(f28534,plain,(
% 37.62/5.29 converse(sF1_fnc)=join(converse(sF1_fnc),complement(composition(top,complement(converse(sF0_fnc)))))),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f28419,f20652])).
% 37.62/5.29 fof(f28563,plain,(
% 37.62/5.29 ![X0]: (join(converse(sF0_fnc),complement(X0))=join(converse(sF1_fnc),complement(X0)))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f2964,f28529])).
% 37.62/5.29 fof(f28569,plain,(
% 37.62/5.29 converse(sF1_fnc)=join(converse(sF0_fnc),complement(composition(top,complement(converse(sF0_fnc)))))),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f28563,f28534])).
% 37.62/5.29 fof(f28610,plain,(
% 37.62/5.29 converse(sF1_fnc)=converse(sF0_fnc)),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f20652,f28569])).
% 37.62/5.29 fof(f28692,plain,(
% 37.62/5.29 converse(converse(sF0_fnc))=sF1_fnc),
% 37.62/5.29 inference(paramodulation,[status(thm)],[f28610,f23])).
% 37.62/5.29 fof(f28770,plain,(
% 37.62/5.29 sF0_fnc=sF1_fnc),
% 37.62/5.29 inference(forward_demodulation,[status(thm)],[f23,f28692])).
% 37.62/5.29 fof(f28771,plain,(
% 37.62/5.29 $false),
% 37.62/5.29 inference(forward_subsumption_resolution,[status(thm)],[f28770,f33])).
% 37.62/5.29 % SZS output end CNFRefutation for theBenchmark.p
% 1.37/5.31 % Elapsed time: 4.910289 seconds
% 1.37/5.31 % CPU time: 38.550887 seconds
% 1.37/5.31 % Total memory used: 260.671 MB
% 1.37/5.31 % Net memory used: 253.747 MB
%------------------------------------------------------------------------------