%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL019+2 : 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 : n003.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 : Theorem 164.07s 21.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL019+2 : 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.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:02:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 164.07/21.15 % Refutation found
% 164.07/21.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 164.07/21.15 % SZS output start CNFRefutation for theBenchmark
% 164.07/21.15 fof(f1,axiom,(
% 164.07/21.15 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f2,axiom,(
% 164.07/21.15 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f3,axiom,(
% 164.07/21.15 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f4,axiom,(
% 164.07/21.15 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f5,axiom,(
% 164.07/21.15 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f6,axiom,(
% 164.07/21.15 (! [X0] : composition(X0,one) = X0 )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f7,axiom,(
% 164.07/21.15 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f8,axiom,(
% 164.07/21.15 (! [X0] : converse(converse(X0)) = X0 )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f9,axiom,(
% 164.07/21.15 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f10,axiom,(
% 164.07/21.15 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f11,axiom,(
% 164.07/21.15 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f12,axiom,(
% 164.07/21.15 (! [X0] : top = join(X0,complement(X0)) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f13,axiom,(
% 164.07/21.15 (! [X0] : zero = meet(X0,complement(X0)) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f16,axiom,(
% 164.07/21.15 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f17,conjecture,(
% 164.07/21.15 (! [X0,X1] :( ( composition(X0,top) = X0& composition(X1,top) = X1 )=> composition(meet(X0,X1),top) = meet(X0,X1) ) )),
% 164.07/21.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 164.07/21.15 fof(f18,negated_conjecture,(
% 164.07/21.15 ~((! [X0,X1] :( ( composition(X0,top) = X0& composition(X1,top) = X1 )=> composition(meet(X0,X1),top) = meet(X0,X1) ) ))),
% 164.07/21.15 inference(negated_conjecture,[status(cth)],[f17])).
% 164.07/21.15 fof(f19,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f1])).
% 164.07/21.15 fof(f20,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f2])).
% 164.07/21.15 fof(f21,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f3])).
% 164.07/21.15 fof(f22,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f4])).
% 164.07/21.15 fof(f23,plain,(
% 164.07/21.15 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f5])).
% 164.07/21.15 fof(f24,plain,(
% 164.07/21.15 ![X0]: (composition(X0,one)=X0)),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f6])).
% 164.07/21.15 fof(f25,plain,(
% 164.07/21.15 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f7])).
% 164.07/21.15 fof(f26,plain,(
% 164.07/21.15 ![X0]: (converse(converse(X0))=X0)),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f8])).
% 164.07/21.15 fof(f27,plain,(
% 164.07/21.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f9])).
% 164.07/21.15 fof(f28,plain,(
% 164.07/21.15 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f10])).
% 164.07/21.15 fof(f29,plain,(
% 164.07/21.15 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f11])).
% 164.07/21.15 fof(f30,plain,(
% 164.07/21.15 ![X0]: (top=join(X0,complement(X0)))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f12])).
% 164.07/21.15 fof(f31,plain,(
% 164.07/21.15 ![X0]: (zero=meet(X0,complement(X0)))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f13])).
% 164.07/21.15 fof(f34,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f16])).
% 164.07/21.15 fof(f35,plain,(
% 164.07/21.15 (?[X0,X1]: ((composition(X0,top)=X0&composition(X1,top)=X1)&~composition(meet(X0,X1),top)=meet(X0,X1)))),
% 164.07/21.15 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 164.07/21.15 fof(f36,plain,(
% 164.07/21.15 ((composition(sK0_skl,top)=sK0_skl&composition(sK1_skl,top)=sK1_skl)&~composition(meet(sK0_skl,sK1_skl),top)=meet(sK0_skl,sK1_skl))),
% 164.07/21.15 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f35])).
% 164.07/21.15 fof(f37,plain,(
% 164.07/21.15 composition(sK0_skl,top)=sK0_skl),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f36])).
% 164.07/21.15 fof(f38,plain,(
% 164.07/21.15 composition(sK1_skl,top)=sK1_skl),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f36])).
% 164.07/21.15 fof(f39,plain,(
% 164.07/21.15 ~composition(meet(sK0_skl,sK1_skl),top)=meet(sK0_skl,sK1_skl)),
% 164.07/21.15 inference(cnf_transformation,[status(thm)],[f36])).
% 164.07/21.15 fof(f40,definition,(
% 164.07/21.15 sF1_fnc=meet(sK0_skl,sK1_skl)),
% 164.07/21.15 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 164.07/21.15 fof(f41,definition,(
% 164.07/21.15 sF0_fnc=composition(sF1_fnc,top)),
% 164.07/21.15 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 164.07/21.15 fof(f42,plain,(
% 164.07/21.15 ~sF0_fnc=sF1_fnc),
% 164.07/21.15 inference(definition_folding,[],[f39,f41,f40])).
% 164.07/21.15 fof(f43,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f22,f21])).
% 164.07/21.15 fof(f65,plain,(
% 164.07/21.15 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f24,f23])).
% 164.07/21.15 fof(f89,plain,(
% 164.07/21.15 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f26,f28])).
% 164.07/21.15 fof(f108,plain,(
% 164.07/21.15 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f22])).
% 164.07/21.15 fof(f109,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f22])).
% 164.07/21.15 fof(f115,plain,(
% 164.07/21.15 zero=complement(top)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f31,f108])).
% 164.07/21.15 fof(f119,plain,(
% 164.07/21.15 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f115,f22])).
% 164.07/21.15 fof(f120,plain,(
% 164.07/21.15 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f115,f22])).
% 164.07/21.15 fof(f131,plain,(
% 164.07/21.15 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f119])).
% 164.07/21.15 fof(f138,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(complement(X1),zero))=complement(join(complement(X0),meet(X1,top))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f119,f22])).
% 164.07/21.15 fof(f139,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(complement(X0),zero),X1)=complement(join(meet(X0,top),complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f119,f22])).
% 164.07/21.15 fof(f144,plain,(
% 164.07/21.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f27])).
% 164.07/21.15 fof(f146,plain,(
% 164.07/21.15 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f26,f27])).
% 164.07/21.15 fof(f172,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f20])).
% 164.07/21.15 fof(f173,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f20])).
% 164.07/21.15 fof(f178,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f20])).
% 164.07/21.15 fof(f179,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f20])).
% 164.07/21.15 fof(f209,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(top,X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f120,f22])).
% 164.07/21.15 fof(f210,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(meet(top,X0),complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f120,f22])).
% 164.07/21.15 fof(f220,plain,(
% 164.07/21.15 ![X0]: (meet(join(zero,complement(X0)),top)=complement(join(zero,meet(top,X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f120,f131])).
% 164.07/21.15 fof(f228,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(X1,top))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f131,f22])).
% 164.07/21.15 fof(f229,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(meet(X0,top),complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f131,f22])).
% 164.07/21.15 fof(f239,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(complement(X1),zero))=meet(X0,join(zero,complement(X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f228,f138])).
% 164.07/21.15 fof(f240,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(complement(X0),zero),X1)=meet(join(zero,complement(X0)),X1))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f229,f139])).
% 164.07/21.15 fof(f256,plain,(
% 164.07/21.15 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f146])).
% 164.07/21.15 fof(f291,plain,(
% 164.07/21.15 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f24,f89])).
% 164.07/21.15 fof(f313,plain,(
% 164.07/21.15 ![X0]: (X0=composition(converse(one),X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f26,f291])).
% 164.07/21.15 fof(f329,plain,(
% 164.07/21.15 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f65,f313])).
% 164.07/21.15 fof(f330,plain,(
% 164.07/21.15 one=converse(one)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f24,f313])).
% 164.07/21.15 fof(f341,plain,(
% 164.07/21.15 ![X0]: (composition(one,X0)=X0)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f313,f329])).
% 164.07/21.15 fof(f406,plain,(
% 164.07/21.15 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f178])).
% 164.07/21.15 fof(f489,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f30,f179])).
% 164.07/21.15 fof(f518,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f22,f109])).
% 164.07/21.15 fof(f524,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(meet(top,X1),complement(X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f120,f109])).
% 164.07/21.15 fof(f528,plain,(
% 164.07/21.15 ![X0]: (meet(top,X0)=complement(join(complement(X0),zero)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f115,f109])).
% 164.07/21.15 fof(f530,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(complement(X1),meet(top,X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f120,f109])).
% 164.07/21.15 fof(f583,plain,(
% 164.07/21.15 ![X0]: (composition(join(sF1_fnc,X0),top)=join(sF0_fnc,composition(X0,top)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f41,f25])).
% 164.07/21.15 fof(f622,plain,(
% 164.07/21.15 ![X0]: (join(composition(one,complement(composition(one,X0))),complement(X0))=complement(X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f330,f29])).
% 164.07/21.15 fof(f650,plain,(
% 164.07/21.15 ![X0]: (join(complement(composition(one,X0)),complement(X0))=complement(X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f341,f622])).
% 164.07/21.15 fof(f651,plain,(
% 164.07/21.15 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f341,f650])).
% 164.07/21.15 fof(f871,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f22,f651])).
% 164.07/21.15 fof(f878,plain,(
% 164.07/21.15 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f651,f109])).
% 164.07/21.15 fof(f880,plain,(
% 164.07/21.15 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f651,f178])).
% 164.07/21.15 fof(f896,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=complement(join(complement(X0),complement(X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f109,f871])).
% 164.07/21.15 fof(f898,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f109,f896])).
% 164.07/21.15 fof(f911,plain,(
% 164.07/21.15 ![X0]: (join(X0,top)=top)),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f918,f406])).
% 164.07/21.15 fof(f918,plain,(
% 164.07/21.15 ![X0]: (top=join(top,complement(X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f30,f880])).
% 164.07/21.15 fof(f952,plain,(
% 164.07/21.15 ![X0]: (join(top,X0)=top)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f911])).
% 164.07/21.15 fof(f958,plain,(
% 164.07/21.15 ![X0]: (converse(top)=join(X0,converse(top)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f911,f146])).
% 164.07/21.15 fof(f988,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),join(X0,X1))=top)),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f952,f489])).
% 164.07/21.15 fof(f1030,plain,(
% 164.07/21.15 converse(top)=top),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f952,f958])).
% 164.07/21.15 fof(f1058,plain,(
% 164.07/21.15 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f1030,f256])).
% 164.07/21.15 fof(f1202,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sK1_skl,sK0_skl))=meet(sK1_skl,sK0_skl)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f40,f898])).
% 164.07/21.15 fof(f1206,plain,(
% 164.07/21.15 join(meet(sK1_skl,sK0_skl),sF1_fnc)=meet(sK0_skl,sK1_skl)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f40,f898])).
% 164.07/21.15 fof(f1223,plain,(
% 164.07/21.15 join(meet(sK1_skl,sK0_skl),sF1_fnc)=sF1_fnc),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f40,f1206])).
% 164.07/21.15 fof(f1335,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sK1_skl,sK0_skl))=sF1_fnc),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f1223])).
% 164.07/21.15 fof(f1344,plain,(
% 164.07/21.15 sF1_fnc=meet(sK1_skl,sK0_skl)),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f1335,f1202])).
% 164.07/21.15 fof(f1355,plain,(
% 164.07/21.15 ![X0]: (top=converse(join(complement(converse(converse(X0))),X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f144,f1058])).
% 164.07/21.15 fof(f1376,plain,(
% 164.07/21.15 ![X0]: (top=converse(join(complement(X0),X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f26,f1355])).
% 164.07/21.15 fof(f1427,plain,(
% 164.07/21.15 ![X0]: (converse(top)=join(complement(X0),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f1376,f26])).
% 164.07/21.15 fof(f1462,plain,(
% 164.07/21.15 ![X0]: (top=join(complement(X0),X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1030,f1427])).
% 164.07/21.15 fof(f2343,plain,(
% 164.07/21.15 ![X0]: (join(meet(sK1_skl,X0),meet(composition(meet(sK1_skl,composition(X0,converse(top))),top),X0))=meet(composition(meet(sK1_skl,composition(X0,converse(top))),top),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f38,f34])).
% 164.07/21.15 fof(f2389,plain,(
% 164.07/21.15 ![X0]: (join(meet(sK1_skl,X0),meet(composition(meet(sK1_skl,composition(X0,top)),top),X0))=meet(composition(meet(sK1_skl,composition(X0,converse(top))),top),X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1030,f2343])).
% 164.07/21.15 fof(f2390,plain,(
% 164.07/21.15 ![X0]: (join(meet(sK1_skl,X0),meet(composition(meet(sK1_skl,composition(X0,top)),top),X0))=meet(composition(meet(sK1_skl,composition(X0,top)),top),X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1030,f2389])).
% 164.07/21.15 fof(f2430,plain,(
% 164.07/21.15 sK0_skl=join(sF1_fnc,complement(join(complement(sK0_skl),sK1_skl)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f40,f43])).
% 164.07/21.15 fof(f2431,plain,(
% 164.07/21.15 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f31,f43])).
% 164.07/21.15 fof(f2432,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X1,X0),complement(join(complement(X0),X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f518,f43])).
% 164.07/21.15 fof(f2434,plain,(
% 164.07/21.15 ![X0]: (X0=join(complement(complement(X0)),complement(join(complement(X0),X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f878,f43])).
% 164.07/21.15 fof(f2441,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,join(X0,X1)),complement(top)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f988,f43])).
% 164.07/21.15 fof(f2447,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),complement(top)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f172,f43])).
% 164.07/21.15 fof(f2453,plain,(
% 164.07/21.15 ![X0,X1]: (join(zero,complement(X0))=join(meet(join(zero,complement(X0)),X1),complement(join(meet(X0,top),X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f131,f43])).
% 164.07/21.15 fof(f2465,plain,(
% 164.07/21.15 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f109,f2431])).
% 164.07/21.15 fof(f2466,plain,(
% 164.07/21.15 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f878,f2465])).
% 164.07/21.15 fof(f2467,plain,(
% 164.07/21.15 ![X0]: (X0=join(complement(complement(X0)),complement(top)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1462,f2434])).
% 164.07/21.15 fof(f2468,plain,(
% 164.07/21.15 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f115,f2467])).
% 164.07/21.15 fof(f2472,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,join(X0,X1)),zero))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f115,f2441])).
% 164.07/21.15 fof(f2479,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),zero))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f115,f2447])).
% 164.07/21.15 fof(f2692,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f22,f2466])).
% 164.07/21.15 fof(f2693,plain,(
% 164.07/21.15 ![X0]: (meet(complement(X0),top)=complement(X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2466,f131])).
% 164.07/21.15 fof(f2717,plain,(
% 164.07/21.15 ![X0]: (complement(X0)=join(complement(X0),complement(join(complement(complement(X0)),top))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2693,f43])).
% 164.07/21.15 fof(f2733,plain,(
% 164.07/21.15 ![X0]: (complement(X0)=join(complement(X0),complement(top)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f911,f2717])).
% 164.07/21.15 fof(f2734,plain,(
% 164.07/21.15 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2744,f119])).
% 164.07/21.15 fof(f2737,plain,(
% 164.07/21.15 ![X0]: (X0=complement(complement(X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2744,f2468])).
% 164.07/21.15 fof(f2741,plain,(
% 164.07/21.15 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2744,f528])).
% 164.07/21.15 fof(f2742,plain,(
% 164.07/21.15 ![X0,X1]: (meet(complement(X0),X1)=meet(join(zero,complement(X0)),X1))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2744,f240])).
% 164.07/21.15 fof(f2743,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,complement(X1))=meet(X0,join(zero,complement(X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2744,f239])).
% 164.07/21.15 fof(f2744,plain,(
% 164.07/21.15 ![X0]: (complement(X0)=join(complement(X0),zero))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f115,f2733])).
% 164.07/21.15 fof(f2757,plain,(
% 164.07/21.15 ![X0]: (complement(complement(join(zero,complement(X0))))=complement(join(zero,meet(top,X0))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2734,f220])).
% 164.07/21.15 fof(f2764,plain,(
% 164.07/21.15 ![X0,X1]: (join(zero,complement(X0))=join(meet(join(zero,complement(X0)),X1),complement(join(complement(complement(X0)),X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2734,f2453])).
% 164.07/21.15 fof(f2789,plain,(
% 164.07/21.15 ![X0]: (meet(X0,X0)=X0)),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2737,f878])).
% 164.07/21.15 fof(f2844,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(complement(X1),X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2853,f530])).
% 164.07/21.15 fof(f2845,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(X1,complement(X0))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2853,f524])).
% 164.07/21.15 fof(f2848,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(X0,complement(X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2853,f210])).
% 164.07/21.15 fof(f2849,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),X1)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2853,f209])).
% 164.07/21.15 fof(f2853,plain,(
% 164.07/21.15 ![X0]: (meet(top,X0)=X0)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2737,f2741])).
% 164.07/21.15 fof(f2855,plain,(
% 164.07/21.15 ![X0]: (join(zero,complement(X0))=complement(join(zero,meet(top,X0))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2737,f2757])).
% 164.07/21.15 fof(f2856,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(zero,meet(X0,X1))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2861,f2692])).
% 164.07/21.15 fof(f2861,plain,(
% 164.07/21.15 ![X0]: (join(zero,complement(X0))=complement(join(zero,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2853,f2855])).
% 164.07/21.15 fof(f2876,plain,(
% 164.07/21.15 ![X0,X1]: (complement(join(zero,X0))=join(meet(join(zero,complement(X0)),X1),complement(join(complement(complement(X0)),X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2861,f2764])).
% 164.07/21.15 fof(f2877,plain,(
% 164.07/21.15 ![X0,X1]: (complement(join(zero,X0))=join(meet(complement(X0),X1),complement(join(complement(complement(X0)),X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2742,f2876])).
% 164.07/21.15 fof(f2882,plain,(
% 164.07/21.15 ![X0]: (complement(join(zero,X0))=complement(X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f43,f2877])).
% 164.07/21.15 fof(f2979,plain,(
% 164.07/21.15 sK0_skl=join(sF1_fnc,meet(complement(sK1_skl),sK0_skl))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2995,f2430])).
% 164.07/21.15 fof(f2982,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2995,f43])).
% 164.07/21.15 fof(f2993,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X0,join(X1,meet(complement(X1),X0))),zero))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2995,f2479])).
% 164.07/21.15 fof(f2994,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f2995,f2432])).
% 164.07/21.15 fof(f2995,plain,(
% 164.07/21.15 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2742,f2844])).
% 164.07/21.15 fof(f3009,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2743,f2845])).
% 164.07/21.15 fof(f3011,plain,(
% 164.07/21.15 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2742,f2848])).
% 164.07/21.15 fof(f3012,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2743,f2849])).
% 164.07/21.15 fof(f3024,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2882,f2856])).
% 164.07/21.15 fof(f3088,plain,(
% 164.07/21.15 ![X0]: (join(meet(X0,X0),X0)=meet(X0,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2789,f898])).
% 164.07/21.15 fof(f3112,plain,(
% 164.07/21.15 ![X0]: (join(X0,X0)=meet(X0,X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2789,f3088])).
% 164.07/21.15 fof(f3119,plain,(
% 164.07/21.15 ![X0]: (join(X0,X0)=X0)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2789,f3112])).
% 164.07/21.15 fof(f3208,plain,(
% 164.07/21.15 ![X0]: (complement(complement(X0))=join(X0,zero))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2737,f2744])).
% 164.07/21.15 fof(f3224,plain,(
% 164.07/21.15 ![X0,X1]: (X0=meet(X0,join(X1,meet(complement(X1),X0))))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f3236,f2993])).
% 164.07/21.15 fof(f3226,plain,(
% 164.07/21.15 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f3236,f2472])).
% 164.07/21.15 fof(f3236,plain,(
% 164.07/21.15 ![X0]: (X0=join(X0,zero))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2737,f3208])).
% 164.07/21.15 fof(f3326,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,join(X1,X0)))=join(X1,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f179,f3119])).
% 164.07/21.15 fof(f3354,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3119,f179])).
% 164.07/21.15 fof(f3375,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,X0))=join(X1,X0))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f3354,f3326])).
% 164.07/21.15 fof(f3814,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2982,f3226])).
% 164.07/21.15 fof(f3870,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X0),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f518,f3814])).
% 164.07/21.15 fof(f3954,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(X0,X1),X0)=meet(X0,join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3226,f3870])).
% 164.07/21.15 fof(f3986,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f3226,f3954])).
% 164.07/21.15 fof(f4089,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f3986])).
% 164.07/21.15 fof(f4376,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f173])).
% 164.07/21.15 fof(f4466,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3119,f173])).
% 164.07/21.15 fof(f4515,plain,(
% 164.07/21.15 ![X0,X1,X2]: (meet(join(X0,join(X1,X2)),X2)=X2)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f173,f3986])).
% 164.07/21.15 fof(f5254,plain,(
% 164.07/21.15 join(meet(sK1_skl,sK0_skl),meet(composition(meet(sK1_skl,sK0_skl),top),sK0_skl))=meet(composition(meet(sK1_skl,composition(sK0_skl,top)),top),sK0_skl)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f37,f2390])).
% 164.07/21.15 fof(f5322,plain,(
% 164.07/21.15 join(sF1_fnc,meet(composition(meet(sK1_skl,sK0_skl),top),sK0_skl))=meet(composition(meet(sK1_skl,composition(sK0_skl,top)),top),sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1344,f5254])).
% 164.07/21.15 fof(f5323,plain,(
% 164.07/21.15 join(sF1_fnc,meet(composition(sF1_fnc,top),sK0_skl))=meet(composition(meet(sK1_skl,composition(sK0_skl,top)),top),sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1344,f5322])).
% 164.07/21.15 fof(f5324,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sF0_fnc,sK0_skl))=meet(composition(meet(sK1_skl,composition(sK0_skl,top)),top),sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f41,f5323])).
% 164.07/21.15 fof(f5325,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sF0_fnc,sK0_skl))=meet(composition(meet(sK1_skl,sK0_skl),top),sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f37,f5324])).
% 164.07/21.15 fof(f5326,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sF0_fnc,sK0_skl))=meet(composition(sF1_fnc,top),sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f1344,f5325])).
% 164.07/21.15 fof(f5327,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sF0_fnc,sK0_skl))=meet(sF0_fnc,sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f41,f5326])).
% 164.07/21.15 fof(f5358,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f518,f2994])).
% 164.07/21.15 fof(f5361,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X1,X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2737,f2994])).
% 164.07/21.15 fof(f5368,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2994,f3226])).
% 164.07/21.15 fof(f5474,plain,(
% 164.07/21.15 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(meet(X1,X0),X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3870,f5368])).
% 164.07/21.15 fof(f5512,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X0),X1))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f5368,f5474])).
% 164.07/21.15 fof(f5940,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(X0,meet(complement(X0),X1)),X1)=meet(X1,X1))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3224,f5512])).
% 164.07/21.15 fof(f5970,plain,(
% 164.07/21.15 ![X0,X1]: (meet(join(X0,meet(complement(X0),X1)),X1)=X1)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2789,f5940])).
% 164.07/21.15 fof(f6091,plain,(
% 164.07/21.15 ![X0,X1]: (X0=join(meet(complement(X1),X0),meet(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2737,f5358])).
% 164.07/21.15 fof(f8235,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(complement(X1),X0),meet(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f6091,f3375])).
% 164.07/21.15 fof(f8236,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(complement(X0),X1),meet(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f5361,f3375])).
% 164.07/21.15 fof(f8255,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,join(X2,X0)))=join(join(X2,X1),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f179,f3375])).
% 164.07/21.15 fof(f8274,plain,(
% 164.07/21.15 ![X0,X1]: (join(join(X0,X1),join(X0,X1))=join(X1,join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3375,f3375])).
% 164.07/21.15 fof(f8275,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(join(X0,X1),join(X0,join(X1,X2)))=join(X2,join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f173,f3375])).
% 164.07/21.15 fof(f8276,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(join(X0,X1),join(X1,join(X2,X0)))=join(X2,join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f173,f3375])).
% 164.07/21.15 fof(f8331,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),X0)=X0)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f6091,f8235])).
% 164.07/21.15 fof(f8344,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f5361,f8236])).
% 164.07/21.15 fof(f8373,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,join(X2,X0)))=join(X1,join(X2,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8255])).
% 164.07/21.15 fof(f8417,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,join(X1,X0)))=join(X0,join(X1,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8274])).
% 164.07/21.15 fof(f8418,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,join(X0,X1)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8373,f8417])).
% 164.07/21.15 fof(f8419,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f4466,f8418])).
% 164.07/21.15 fof(f8420,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,join(X1,join(X0,X2))))=join(X2,join(X1,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8275])).
% 164.07/21.15 fof(f8421,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(join(X0,X1),X2))=join(X1,join(X2,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f4466,f8420])).
% 164.07/21.15 fof(f8423,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,join(X0,X2)))=join(X1,join(X2,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8421])).
% 164.07/21.15 fof(f8424,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X1,join(X0,join(X2,X1))))=join(X2,join(X1,X0)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8276])).
% 164.07/21.15 fof(f8425,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(join(X1,X0),X2))=join(X1,join(X0,X2)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8423,f8424])).
% 164.07/21.15 fof(f8426,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,join(X0,join(X1,X2)))=join(X1,join(X0,X2)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f8425])).
% 164.07/21.15 fof(f8427,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X2,X1)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f4466,f8426])).
% 164.07/21.15 fof(f8474,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,meet(complement(X1),X0)))=join(X1,meet(complement(X1),X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f5970,f8331])).
% 164.07/21.15 fof(f8485,plain,(
% 164.07/21.15 join(sF1_fnc,sK0_skl)=sK0_skl),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f40,f8331])).
% 164.07/21.15 fof(f8688,plain,(
% 164.07/21.15 composition(sK0_skl,top)=join(sF0_fnc,composition(sK0_skl,top))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8485,f583])).
% 164.07/21.15 fof(f8704,plain,(
% 164.07/21.15 sK0_skl=join(sF0_fnc,composition(sK0_skl,top))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f37,f8688])).
% 164.07/21.15 fof(f8705,plain,(
% 164.07/21.15 sK0_skl=join(sF0_fnc,sK0_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f37,f8704])).
% 164.07/21.15 fof(f8716,plain,(
% 164.07/21.15 sF0_fnc=meet(sF0_fnc,sK0_skl)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8705,f3226])).
% 164.07/21.15 fof(f8726,plain,(
% 164.07/21.15 join(sF1_fnc,meet(sF0_fnc,sK0_skl))=sF0_fnc),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f8716,f5327])).
% 164.07/21.15 fof(f8728,plain,(
% 164.07/21.15 join(sF1_fnc,sF0_fnc)=sF0_fnc),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8716,f8726])).
% 164.07/21.15 fof(f8764,plain,(
% 164.07/21.15 join(sF0_fnc,sF1_fnc)=sF0_fnc),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f8728])).
% 164.07/21.15 fof(f8777,plain,(
% 164.07/21.15 ![X0]: (join(sF0_fnc,join(sF1_fnc,X0))=join(sF0_fnc,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8728,f179])).
% 164.07/21.15 fof(f9936,plain,(
% 164.07/21.15 join(sF1_fnc,sK1_skl)=sK1_skl),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f40,f8344])).
% 164.07/21.15 fof(f9964,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(X0,X1)=join(X1,join(X0,meet(X2,X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8344,f173])).
% 164.07/21.15 fof(f9973,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(meet(X0,X1),join(X1,X2))=join(X1,X2))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8344,f20])).
% 164.07/21.15 fof(f10005,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,X1)=join(X0,meet(complement(X0),X1)))),
% 164.07/21.15 inference(backward_demodulation,[status(thm)],[f9964,f8474])).
% 164.07/21.15 fof(f10172,plain,(
% 164.07/21.15 composition(sK1_skl,top)=join(sF0_fnc,composition(sK1_skl,top))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f9936,f583])).
% 164.07/21.15 fof(f10188,plain,(
% 164.07/21.15 sK1_skl=join(sF0_fnc,composition(sK1_skl,top))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f38,f10172])).
% 164.07/21.15 fof(f10189,plain,(
% 164.07/21.15 sK1_skl=join(sF0_fnc,sK1_skl)),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f38,f10188])).
% 164.07/21.15 fof(f10196,plain,(
% 164.07/21.15 ![X0]: (join(sF0_fnc,join(sK1_skl,X0))=join(X0,sK1_skl))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f10189,f173])).
% 164.07/21.15 fof(f12492,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(meet(complement(X0),X1),join(X0,X2))=join(join(X0,X1),X2))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f10005,f179])).
% 164.07/21.15 fof(f12530,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(meet(complement(X0),X1),join(X0,X2))=join(X1,join(X0,X2)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f179,f12492])).
% 164.07/21.15 fof(f12602,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(complement(X0),X1),X0)=join(meet(complement(X0),X1),join(X0,X1)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f10005,f8419])).
% 164.07/21.15 fof(f12766,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(complement(X0),X1),X0)=join(X1,join(X0,X1)))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f12530,f12602])).
% 164.07/21.15 fof(f12777,plain,(
% 164.07/21.15 ![X0,X1]: (join(meet(complement(X0),X1),X0)=join(X1,X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8419,f12766])).
% 164.07/21.15 fof(f12925,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,join(X1,X0))=join(meet(complement(X0),X1),X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f12777,f3375])).
% 164.07/21.15 fof(f12967,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,X1)=join(meet(complement(X0),X1),X0))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8419,f12925])).
% 164.07/21.15 fof(f15639,plain,(
% 164.07/21.15 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2737,f3009])).
% 164.07/21.15 fof(f15878,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f19,f3024])).
% 164.07/21.15 fof(f15888,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),X1)=complement(meet(X0,complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2737,f3024])).
% 164.07/21.15 fof(f16538,plain,(
% 164.07/21.15 ![X0,X1]: (join(complement(X0),X1)=complement(meet(complement(X1),X0)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2995,f2737])).
% 164.07/21.15 fof(f20526,plain,(
% 164.07/21.15 ![X0]: (join(sF0_fnc,X0)=join(sF1_fnc,join(X0,sF0_fnc)))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f8764,f4376])).
% 164.07/21.15 fof(f25647,plain,(
% 164.07/21.15 join(sF0_fnc,sK0_skl)=join(sF0_fnc,meet(complement(sK1_skl),sK0_skl))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f2979,f8777])).
% 164.07/21.15 fof(f25731,plain,(
% 164.07/21.15 sK0_skl=join(sF0_fnc,meet(complement(sK1_skl),sK0_skl))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f8705,f25647])).
% 164.07/21.15 fof(f26221,plain,(
% 164.07/21.15 ![X0]: (meet(join(X0,sK1_skl),sF0_fnc)=sF0_fnc)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f10196,f3986])).
% 164.07/21.15 fof(f26347,plain,(
% 164.07/21.15 ![X0]: (meet(join(sK1_skl,X0),sF0_fnc)=sF0_fnc)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f12967,f26221])).
% 164.07/21.15 fof(f26445,plain,(
% 164.07/21.15 ![X0]: (meet(sF0_fnc,join(sK1_skl,X0))=sF0_fnc)),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f518,f26347])).
% 164.07/21.15 fof(f28570,plain,(
% 164.07/21.15 ![X0,X1,X2]: (meet(join(X0,X1),meet(X2,X0))=meet(X2,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f9973,f3986])).
% 164.07/21.15 fof(f31410,plain,(
% 164.07/21.15 ![X0,X1]: (join(X0,complement(X1))=join(X0,complement(join(X1,X0))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f15639,f10005])).
% 164.07/21.15 fof(f36192,plain,(
% 164.07/21.15 ![X0,X1,X2]: (join(meet(complement(X0),X1),complement(X2))=complement(meet(X2,join(X0,complement(X1)))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f3011,f15878])).
% 164.07/21.15 fof(f47229,plain,(
% 164.07/21.15 ![X0,X1,X2]: (meet(join(X0,X1),meet(X0,X2))=meet(X2,X0))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f518,f28570])).
% 164.07/21.15 fof(f65671,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,complement(complement(join(X1,complement(X0)))))=complement(join(complement(X0),complement(X1))))),
% 164.07/21.15 inference(paramodulation,[status(thm)],[f31410,f3012])).
% 164.07/21.15 fof(f66298,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=complement(join(complement(X0),complement(X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f2737,f65671])).
% 164.07/21.15 fof(f66299,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=meet(X0,complement(complement(X1))))),
% 164.07/21.15 inference(forward_demodulation,[status(thm)],[f3012,f66298])).
% 164.07/21.15 fof(f66302,plain,(
% 164.07/21.15 ![X0,X1]: (meet(X0,join(X1,complement(X0)))=meet(X0,X1))),
% 164.07/21.17 inference(forward_demodulation,[status(thm)],[f2737,f66299])).
% 164.07/21.17 fof(f66459,plain,(
% 164.07/21.17 ![X0,X1]: (meet(join(X0,X1),join(X1,complement(X0)))=meet(join(X0,X1),X1))),
% 164.07/21.17 inference(paramodulation,[status(thm)],[f31410,f66302])).
% 164.07/21.17 fof(f66549,plain,(
% 164.07/21.17 ![X0,X1,X2]: (meet(join(X0,X1),meet(X0,X2))=meet(join(X2,complement(X0)),X0))),
% 164.07/21.17 inference(paramodulation,[status(thm)],[f66302,f47229])).
% 164.07/21.17 fof(f66669,plain,(
% 164.07/21.17 ![X0,X1]: (meet(join(X0,X1),join(X1,complement(X0)))=X1)),
% 164.07/21.17 inference(forward_demodulation,[status(thm)],[f4089,f66459])).
% 164.07/21.17 fof(f66727,plain,(
% 164.07/21.17 ![X0,X1]: (meet(X0,X1)=meet(join(X0,complement(X1)),X1))),
% 164.07/21.17 inference(forward_demodulation,[status(thm)],[f47229,f66549])).
% 164.07/21.17 fof(f67251,plain,(
% 164.07/21.17 meet(sK0_skl,join(meet(complement(sK1_skl),sK0_skl),complement(sF0_fnc)))=meet(complement(sK1_skl),sK0_skl)),
% 164.07/21.17 inference(paramodulation,[status(thm)],[f25731,f66669])).
% 164.07/21.17 fof(f67476,plain,(
% 164.07/21.17 ![X0,X1,X2]: (meet(join(join(X0,X1),X2),X1)=meet(join(X1,complement(X0)),join(X0,X1)))),
% 164.07/21.17 inference(paramodulation,[status(thm)],[f66669,f47229])).
% 104.92/21.41 fof(f67562,plain,(
% 104.92/21.41 meet(sK0_skl,complement(meet(sF0_fnc,join(sK1_skl,complement(sK0_skl)))))=meet(complement(sK1_skl),sK0_skl)),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f36192,f67251])).
% 104.92/21.41 fof(f67564,plain,(
% 104.92/21.41 sK0_skl=join(sF1_fnc,meet(sK0_skl,complement(sF0_fnc)))),
% 104.92/21.41 inference(backward_demodulation,[status(thm)],[f67580,f2979])).
% 104.92/21.41 fof(f67580,plain,(
% 104.92/21.41 meet(sK0_skl,complement(sF0_fnc))=meet(complement(sK1_skl),sK0_skl)),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f26445,f67562])).
% 104.92/21.41 fof(f67857,plain,(
% 104.92/21.41 ![X0,X1,X2]: (meet(join(X0,join(X1,X2)),X2)=meet(join(X2,complement(X0)),join(X0,X2)))),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f8427,f67476])).
% 104.92/21.41 fof(f67859,plain,(
% 104.92/21.41 ![X0,X1]: (X0=meet(join(X0,complement(X1)),join(X1,X0)))),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f4515,f67857])).
% 104.92/21.41 fof(f68100,plain,(
% 104.92/21.41 ![X0,X1]: (X0=meet(join(X0,complement(meet(complement(X0),X1))),join(X0,X1)))),
% 104.92/21.41 inference(paramodulation,[status(thm)],[f12967,f67859])).
% 104.92/21.41 fof(f68421,plain,(
% 104.92/21.41 ![X0,X1]: (X0=meet(join(X0,join(complement(X1),X0)),join(X0,X1)))),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f16538,f68100])).
% 104.92/21.41 fof(f68423,plain,(
% 104.92/21.41 ![X0,X1]: (X0=meet(join(X0,complement(X1)),join(X0,X1)))),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f8419,f68421])).
% 104.92/21.41 fof(f70593,plain,(
% 104.92/21.41 sF1_fnc=meet(join(sF1_fnc,complement(meet(sK0_skl,complement(sF0_fnc)))),sK0_skl)),
% 104.92/21.41 inference(paramodulation,[status(thm)],[f67564,f68423])).
% 104.92/21.41 fof(f70654,plain,(
% 104.92/21.41 sF1_fnc=meet(join(sF1_fnc,join(complement(sK0_skl),sF0_fnc)),sK0_skl)),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f15888,f70593])).
% 104.92/21.41 fof(f70655,plain,(
% 104.92/21.41 sF1_fnc=meet(join(sF0_fnc,complement(sK0_skl)),sK0_skl)),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f20526,f70654])).
% 104.92/21.41 fof(f70656,plain,(
% 104.92/21.41 sF1_fnc=meet(sF0_fnc,sK0_skl)),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f66727,f70655])).
% 104.92/21.41 fof(f70657,plain,(
% 104.92/21.41 sF1_fnc=sF0_fnc),
% 104.92/21.41 inference(forward_demodulation,[status(thm)],[f8716,f70656])).
% 104.92/21.41 fof(f70658,plain,(
% 104.92/21.41 $false),
% 104.92/21.41 inference(forward_subsumption_resolution,[status(thm)],[f70657,f42])).
% 104.92/21.41 % SZS output end CNFRefutation for theBenchmark.p
% 104.92/21.48 % Elapsed time: 21.099652 seconds
% 104.92/21.48 % CPU time: 166.696451 seconds
% 104.92/21.48 % Total memory used: 1.234 GB
% 104.92/21.48 % Net memory used: 1.212 GB
%------------------------------------------------------------------------------