%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL050+3 : 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 : n015.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:46 PM UTC 2026
% Result : Theorem 28.69s 4.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050+3 : 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.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 04:12:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 28.69/4.03 % Refutation found
% 28.69/4.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.69/4.03 % SZS output start CNFRefutation for theBenchmark
% 28.69/4.03 fof(f1,axiom,(
% 28.69/4.03 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f2,axiom,(
% 28.69/4.03 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f3,axiom,(
% 28.69/4.03 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f4,axiom,(
% 28.69/4.03 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f5,axiom,(
% 28.69/4.03 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f6,axiom,(
% 28.69/4.03 (! [X0] : composition(X0,one) = X0 )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f7,axiom,(
% 28.69/4.03 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f8,axiom,(
% 28.69/4.03 (! [X0] : converse(converse(X0)) = X0 )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f9,axiom,(
% 28.69/4.03 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f10,axiom,(
% 28.69/4.03 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f11,axiom,(
% 28.69/4.03 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f12,axiom,(
% 28.69/4.03 (! [X0] : top = join(X0,complement(X0)) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f13,axiom,(
% 28.69/4.03 (! [X0] : zero = meet(X0,complement(X0)) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f15,axiom,(
% 28.69/4.03 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2)) = meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f16,axiom,(
% 28.69/4.03 (! [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) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f17,conjecture,(
% 28.69/4.03 (! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top) )),
% 28.69/4.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.69/4.03 fof(f18,negated_conjecture,(
% 28.69/4.03 ~((! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top) ))),
% 28.69/4.03 inference(negated_conjecture,[status(cth)],[f17])).
% 28.69/4.03 fof(f19,plain,(
% 28.69/4.03 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f1])).
% 28.69/4.03 fof(f20,plain,(
% 28.69/4.03 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f2])).
% 28.69/4.03 fof(f21,plain,(
% 28.69/4.03 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f3])).
% 28.69/4.03 fof(f22,plain,(
% 28.69/4.03 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f4])).
% 28.69/4.03 fof(f23,plain,(
% 28.69/4.03 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f5])).
% 28.69/4.03 fof(f24,plain,(
% 28.69/4.03 ![X0]: (composition(X0,one)=X0)),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f6])).
% 28.69/4.03 fof(f25,plain,(
% 28.69/4.03 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f7])).
% 28.69/4.03 fof(f26,plain,(
% 28.69/4.03 ![X0]: (converse(converse(X0))=X0)),
% 28.69/4.03 inference(cnf_transformation,[status(thm)],[f8])).
% 28.69/4.03 fof(f27,plain,(
% 28.69/4.03 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f9])).
% 28.69/4.05 fof(f28,plain,(
% 28.69/4.05 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f10])).
% 28.69/4.05 fof(f29,plain,(
% 28.69/4.05 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f11])).
% 28.69/4.05 fof(f30,plain,(
% 28.69/4.05 ![X0]: (top=join(X0,complement(X0)))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f12])).
% 28.69/4.05 fof(f31,plain,(
% 28.69/4.05 ![X0]: (zero=meet(X0,complement(X0)))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f13])).
% 28.69/4.05 fof(f33,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f15])).
% 28.69/4.05 fof(f34,plain,(
% 28.69/4.05 ![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))),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f16])).
% 28.69/4.05 fof(f35,plain,(
% 28.69/4.05 (?[X0]: ~complement(composition(X0,top))=composition(complement(composition(X0,top)),top))),
% 28.69/4.05 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 28.69/4.05 fof(f36,plain,(
% 28.69/4.05 ~complement(composition(sK0_skl,top))=composition(complement(composition(sK0_skl,top)),top)),
% 28.69/4.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f35])).
% 28.69/4.05 fof(f37,plain,(
% 28.69/4.05 ~complement(composition(sK0_skl,top))=composition(complement(composition(sK0_skl,top)),top)),
% 28.69/4.05 inference(cnf_transformation,[status(thm)],[f36])).
% 28.69/4.05 fof(f38,definition,(
% 28.69/4.05 sF1_fnc=composition(sK0_skl,top)),
% 28.69/4.05 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 28.69/4.05 fof(f39,definition,(
% 28.69/4.05 sF0_fnc=complement(sF1_fnc)),
% 28.69/4.05 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 28.69/4.05 fof(f40,definition,(
% 28.69/4.05 sF3_fnc=complement(sF1_fnc)),
% 28.69/4.05 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 28.69/4.05 fof(f41,definition,(
% 28.69/4.05 sF2_fnc=composition(sF3_fnc,top)),
% 28.69/4.05 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 28.69/4.05 fof(f42,plain,(
% 28.69/4.05 ~sF0_fnc=sF2_fnc),
% 28.69/4.05 inference(definition_folding,[],[f37,f41,f40,f39,f38])).
% 28.69/4.05 fof(f43,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 28.69/4.05 fof(f44,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f22,f43])).
% 28.69/4.05 fof(f45,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 28.69/4.05 fof(f46,plain,(
% 28.69/4.05 sF3_fnc=sF0_fnc),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f39,f40])).
% 28.69/4.05 fof(f47,plain,(
% 28.69/4.05 sF2_fnc=composition(sF0_fnc,top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f46,f41])).
% 28.69/4.05 fof(f48,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f44])).
% 28.69/4.05 fof(f49,plain,(
% 28.69/4.05 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f22,f22])).
% 28.69/4.05 fof(f50,plain,(
% 28.69/4.05 ![X0]: (meet(sF1_fnc,X0)=complement(join(sF0_fnc,complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f39,f22])).
% 28.69/4.05 fof(f52,plain,(
% 28.69/4.05 ![X0]: (meet(X0,sF1_fnc)=complement(join(complement(X0),sF0_fnc)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f39,f22])).
% 28.69/4.05 fof(f53,plain,(
% 28.69/4.05 ![X0]: (meet(X0,sF1_fnc)=complement(join(sF0_fnc,complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f52])).
% 28.69/4.05 fof(f54,plain,(
% 28.69/4.05 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f22,f30])).
% 28.69/4.05 fof(f56,plain,(
% 28.69/4.05 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f30,f22])).
% 28.69/4.05 fof(f57,plain,(
% 28.69/4.05 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f20,f54])).
% 28.69/4.05 fof(f59,plain,(
% 28.69/4.05 zero=complement(top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f31,f56])).
% 28.69/4.05 fof(f60,plain,(
% 28.69/4.05 top=join(top,zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f30])).
% 28.69/4.05 fof(f61,plain,(
% 28.69/4.05 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f22])).
% 28.69/4.05 fof(f62,plain,(
% 28.69/4.05 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f22])).
% 28.69/4.05 fof(f63,plain,(
% 28.69/4.05 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f61])).
% 28.69/4.05 fof(f65,plain,(
% 28.69/4.05 ![X0]: (composition(sF0_fnc,composition(top,X0))=composition(sF2_fnc,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f47,f23])).
% 28.69/4.05 fof(f96,plain,(
% 28.69/4.05 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f45])).
% 28.69/4.05 fof(f103,plain,(
% 28.69/4.05 join(complement(top),composition(converse(sF0_fnc),complement(sF2_fnc)))=complement(top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f47,f45])).
% 28.69/4.05 fof(f105,plain,(
% 28.69/4.05 join(complement(top),composition(converse(sK0_skl),complement(sF1_fnc)))=complement(top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f38,f45])).
% 28.69/4.05 fof(f106,plain,(
% 28.69/4.05 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f96])).
% 28.69/4.05 fof(f111,plain,(
% 28.69/4.05 join(zero,composition(converse(sF0_fnc),complement(sF2_fnc)))=complement(top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f103])).
% 28.69/4.05 fof(f112,plain,(
% 28.69/4.05 join(zero,composition(converse(sF0_fnc),complement(sF2_fnc)))=zero),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f111])).
% 28.69/4.05 fof(f113,plain,(
% 28.69/4.05 join(zero,composition(converse(sK0_skl),complement(sF1_fnc)))=complement(top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f105])).
% 28.69/4.05 fof(f114,plain,(
% 28.69/4.05 join(zero,composition(converse(sK0_skl),sF0_fnc))=complement(top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f39,f113])).
% 28.69/4.05 fof(f115,plain,(
% 28.69/4.05 join(zero,composition(converse(sK0_skl),sF0_fnc))=zero),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f114])).
% 28.69/4.05 fof(f123,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f22,f48])).
% 28.69/4.05 fof(f132,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),meet(join(complement(X0),complement(X1)),X2)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f123])).
% 28.69/4.05 fof(f133,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),complement(join(meet(X0,X1),complement(X2)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f49,f132])).
% 28.69/4.05 fof(f141,plain,(
% 28.69/4.05 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f24,f23])).
% 28.69/4.05 fof(f149,plain,(
% 28.69/4.05 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f31,f48])).
% 28.69/4.05 fof(f153,plain,(
% 28.69/4.05 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f22,f149])).
% 28.69/4.05 fof(f161,plain,(
% 28.69/4.05 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f22])).
% 28.69/4.05 fof(f162,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f48])).
% 28.69/4.05 fof(f202,plain,(
% 28.69/4.05 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f26,f28])).
% 28.69/4.05 fof(f203,plain,(
% 28.69/4.05 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f26,f28])).
% 28.69/4.05 fof(f207,plain,(
% 28.69/4.05 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f27])).
% 28.69/4.05 fof(f210,plain,(
% 28.69/4.05 ![X0,X1]: (converse(join(X0,converse(X1)))=join(converse(X0),X1))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f26,f27])).
% 28.69/4.05 fof(f226,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f30,f20])).
% 28.69/4.05 fof(f227,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f20])).
% 28.69/4.05 fof(f239,plain,(
% 28.69/4.05 ![X0]: (join(top,join(zero,X0))=join(top,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f60,f20])).
% 28.69/4.05 fof(f241,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f30,f20])).
% 28.69/4.05 fof(f242,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f20])).
% 28.69/4.05 fof(f335,plain,(
% 28.69/4.05 ![X0]: (meet(X0,sF1_fnc)=meet(sF1_fnc,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f50,f53])).
% 28.69/4.05 fof(f391,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(sF1_fnc,X0),complement(join(complement(X0),sF1_fnc))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f335,f48])).
% 28.69/4.05 fof(f398,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(sF1_fnc,X0),complement(join(sF1_fnc,complement(X0)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f391])).
% 28.69/4.05 fof(f437,plain,(
% 28.69/4.05 ![X0]: (join(top,X0)=join(top,meet(X0,X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f153,f239])).
% 28.69/4.05 fof(f512,plain,(
% 28.69/4.05 ![X0,X1]: (meet(join(zero,complement(X0)),X1)=complement(join(meet(top,X0),complement(X1))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f49])).
% 28.69/4.05 fof(f688,plain,(
% 28.69/4.05 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f24,f203])).
% 28.69/4.05 fof(f708,plain,(
% 28.69/4.05 ![X0]: (X0=composition(converse(one),X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f26,f688])).
% 28.69/4.05 fof(f727,plain,(
% 28.69/4.05 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f141,f708])).
% 28.69/4.05 fof(f728,plain,(
% 28.69/4.05 one=converse(one)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f24,f708])).
% 28.69/4.05 fof(f731,plain,(
% 28.69/4.05 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f708,f45])).
% 28.69/4.05 fof(f741,plain,(
% 28.69/4.05 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f708,f25])).
% 28.69/4.05 fof(f750,plain,(
% 28.69/4.05 ![X0]: (composition(one,X0)=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f708,f727])).
% 28.69/4.05 fof(f769,plain,(
% 28.69/4.05 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f750,f731])).
% 28.69/4.05 fof(f794,plain,(
% 28.69/4.05 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f728,f741])).
% 28.69/4.05 fof(f856,plain,(
% 28.69/4.05 ![X0]: (converse(join(one,X0))=join(converse(X0),one))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f728,f207])).
% 28.69/4.05 fof(f869,plain,(
% 28.69/4.05 ![X0]: (converse(join(one,X0))=join(one,converse(X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f856])).
% 28.69/4.05 fof(f924,plain,(
% 28.69/4.05 join(zero,complement(top))=complement(top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f769])).
% 28.69/4.05 fof(f929,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f22,f769])).
% 28.69/4.05 fof(f940,plain,(
% 28.69/4.05 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f769,f22])).
% 28.69/4.05 fof(f941,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f769,f48])).
% 28.69/4.05 fof(f943,plain,(
% 28.69/4.05 join(zero,zero)=complement(top)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f924])).
% 28.69/4.05 fof(f945,plain,(
% 28.69/4.05 join(zero,zero)=zero),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f943])).
% 28.69/4.05 fof(f955,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f22,f929])).
% 28.69/4.05 fof(f960,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f22,f955])).
% 28.69/4.05 fof(f985,plain,(
% 28.69/4.05 ![X0]: (join(top,X0)=join(top,complement(complement(X0))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f940,f437])).
% 28.69/4.05 fof(f991,plain,(
% 28.69/4.05 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f941])).
% 28.69/4.05 fof(f992,plain,(
% 28.69/4.05 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f31,f991])).
% 28.69/4.05 fof(f993,plain,(
% 28.69/4.05 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f992])).
% 28.69/4.05 fof(f996,plain,(
% 28.69/4.05 ![X0]: (join(zero,join(zero,X0))=join(zero,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f945,f20])).
% 28.69/4.05 fof(f1242,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f57,f48])).
% 28.69/4.05 fof(f1269,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f1242])).
% 28.69/4.05 fof(f1270,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(X1),meet(X0,X1)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f1269])).
% 28.69/4.05 fof(f1327,plain,(
% 28.69/4.05 ![X0]: (meet(complement(X0),top)=complement(X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f993,f63])).
% 28.69/4.05 fof(f1347,plain,(
% 28.69/4.05 ![X0]: (complement(X0)=join(complement(X0),complement(join(complement(complement(X0)),top))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f1327,f48])).
% 28.69/4.05 fof(f1364,plain,(
% 28.69/4.05 ![X0]: (complement(X0)=join(complement(X0),complement(join(top,complement(complement(X0))))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f1347])).
% 28.69/4.05 fof(f1365,plain,(
% 28.69/4.05 ![X0]: (complement(X0)=join(complement(X0),complement(join(top,X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f985,f1364])).
% 28.69/4.05 fof(f2243,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),top)),complement(join(meet(X0,X1),zero))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f59,f133])).
% 28.69/4.05 fof(f2398,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),complement(join(meet(X0,X1),zero))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f2243])).
% 28.69/4.05 fof(f2399,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),complement(join(zero,meet(X0,X1)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f2398])).
% 28.69/4.05 fof(f2690,plain,(
% 28.69/4.05 ![X0]: (join(zero,X0)=join(zero,complement(complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f993,f996])).
% 28.69/4.05 fof(f2692,plain,(
% 28.69/4.05 join(zero,zero)=join(zero,composition(converse(sF0_fnc),complement(sF2_fnc)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f112,f996])).
% 28.69/4.05 fof(f2693,plain,(
% 28.69/4.05 join(zero,zero)=join(zero,composition(converse(sK0_skl),sF0_fnc))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f115,f996])).
% 28.69/4.05 fof(f2700,plain,(
% 28.69/4.05 ![X0]: (join(zero,join(X0,zero))=join(zero,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f996])).
% 28.69/4.05 fof(f2711,plain,(
% 28.69/4.05 ![X0]: (X0=complement(complement(X0)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f993])).
% 28.69/4.05 fof(f2713,plain,(
% 28.69/4.05 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f62])).
% 28.69/4.05 fof(f2734,plain,(
% 28.69/4.05 ![X0,X1]: (X0=meet(X0,join(complement(X1),meet(X0,X1))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f1270])).
% 28.69/4.05 fof(f2738,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),complement(meet(X0,X1))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f2399])).
% 28.69/4.05 fof(f2748,plain,(
% 28.69/4.05 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f106])).
% 28.69/4.05 fof(f2807,plain,(
% 28.69/4.05 ![X0,X1]: (meet(complement(X0),X1)=complement(join(meet(top,X0),complement(X1))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f2818,f512])).
% 28.69/4.05 fof(f2818,plain,(
% 28.69/4.05 ![X0]: (join(zero,X0)=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f993,f2690])).
% 28.69/4.05 fof(f2834,plain,(
% 28.69/4.05 zero=join(zero,composition(converse(sF0_fnc),complement(sF2_fnc)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f945,f2692])).
% 28.69/4.05 fof(f2837,plain,(
% 28.69/4.05 zero=composition(converse(sF0_fnc),complement(sF2_fnc))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f2834])).
% 28.69/4.05 fof(f2838,plain,(
% 28.69/4.05 zero=join(zero,composition(converse(sK0_skl),sF0_fnc))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f945,f2693])).
% 28.69/4.05 fof(f2842,plain,(
% 28.69/4.05 zero=composition(converse(sK0_skl),sF0_fnc)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f2838])).
% 28.69/4.05 fof(f2866,plain,(
% 28.69/4.05 ![X0]: (join(X0,zero)=join(zero,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f2700])).
% 28.69/4.05 fof(f2870,plain,(
% 28.69/4.05 ![X0]: (join(X0,zero)=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f2866])).
% 28.69/4.05 fof(f2934,plain,(
% 28.69/4.05 ![X0]: (meet(top,X0)=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2711,f2713])).
% 28.69/4.05 fof(f2979,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(meet(X0,X1)),complement(join(top,meet(X0,X1)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f2738])).
% 28.69/4.05 fof(f3002,plain,(
% 28.69/4.05 ![X0]: (complement(X0)=complement(meet(X0,join(top,X0))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3020,f1365])).
% 28.69/4.05 fof(f3019,plain,(
% 28.69/4.05 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3020,f161])).
% 28.69/4.05 fof(f3020,plain,(
% 28.69/4.05 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f1365,f2979])).
% 28.69/4.05 fof(f3134,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(sF1_fnc,X0),meet(complement(sF1_fnc),X0)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3148,f398])).
% 28.69/4.05 fof(f3147,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3148,f162])).
% 28.69/4.05 fof(f3148,plain,(
% 28.69/4.05 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2934,f2807])).
% 28.69/4.05 fof(f3293,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3346,f34])).
% 28.69/4.05 fof(f3294,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(X0,meet(X1,composition(converse(X0),X2))),X2))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f3346,f33])).
% 28.69/4.05 fof(f3346,plain,(
% 28.69/4.05 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2711,f3019])).
% 28.69/4.05 fof(f3349,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(sF1_fnc,X0),meet(sF0_fnc,X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f39,f3134])).
% 28.69/4.05 fof(f3350,plain,(
% 28.69/4.05 ![X0]: (X0=join(meet(sF0_fnc,X0),meet(sF1_fnc,X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f3349])).
% 28.69/4.05 fof(f3356,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))=meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3346,f3293])).
% 28.69/4.05 fof(f3357,plain,(
% 28.69/4.05 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))=meet(X2,composition(X0,meet(X1,composition(converse(X0),X2)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3346,f3294])).
% 28.69/4.05 fof(f3494,plain,(
% 28.69/4.05 top=complement(zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f30,f2818])).
% 28.69/4.05 fof(f3498,plain,(
% 28.69/4.05 ![X0]: (converse(converse(X0))=join(converse(zero),X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2818,f210])).
% 28.69/4.05 fof(f3511,plain,(
% 28.69/4.05 ![X0]: (X0=join(converse(zero),X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f26,f3498])).
% 28.69/4.05 fof(f3792,plain,(
% 28.69/4.05 zero=converse(zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2870,f3511])).
% 28.69/4.05 fof(f3823,plain,(
% 28.69/4.05 ![X0]: (converse(composition(zero,X0))=composition(converse(X0),zero))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3792,f203])).
% 28.69/4.05 fof(f3901,plain,(
% 28.69/4.05 converse(zero)=composition(converse(sF0_fnc),sK0_skl)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2842,f203])).
% 28.69/4.05 fof(f3914,plain,(
% 28.69/4.05 zero=composition(converse(sF0_fnc),sK0_skl)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3792,f3901])).
% 28.69/4.05 fof(f3934,plain,(
% 28.69/4.05 ![X0]: (join(meet(composition(sF0_fnc,X0),sK0_skl),meet(sK0_skl,composition(sF0_fnc,meet(X0,zero))))=meet(sK0_skl,composition(sF0_fnc,meet(X0,composition(converse(sF0_fnc),sK0_skl)))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3914,f3357])).
% 28.69/4.05 fof(f3946,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,composition(sF0_fnc,meet(X0,zero))))=meet(sK0_skl,composition(sF0_fnc,meet(X0,composition(converse(sF0_fnc),sK0_skl)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3346,f3934])).
% 28.69/4.05 fof(f3947,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,composition(sF0_fnc,meet(X0,zero))))=meet(sK0_skl,composition(sF0_fnc,meet(X0,zero))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3914,f3946])).
% 28.69/4.05 fof(f4185,plain,(
% 28.69/4.05 ![X0]: (join(meet(composition(sF0_fnc,X0),complement(sF2_fnc)),meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,zero))))=meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,composition(converse(sF0_fnc),complement(sF2_fnc))))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2837,f3357])).
% 28.69/4.05 fof(f4202,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,zero))))=meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,composition(converse(sF0_fnc),complement(sF2_fnc))))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3346,f4185])).
% 28.69/4.05 fof(f4203,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,zero))))=meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,zero))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2837,f4202])).
% 28.69/4.05 fof(f4440,plain,(
% 28.69/4.05 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3346,f3147])).
% 28.69/4.05 fof(f4614,plain,(
% 28.69/4.05 ![X0]: (meet(X0,join(top,X0))=complement(complement(X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3002,f2711])).
% 28.69/4.05 fof(f4662,plain,(
% 28.69/4.05 ![X0]: (meet(X0,join(top,X0))=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2711,f4614])).
% 28.69/4.05 fof(f4948,plain,(
% 28.69/4.05 ![X0]: (meet(X0,join(X0,top))=X0)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f4662])).
% 28.69/4.05 fof(f5039,plain,(
% 28.69/4.05 ![X0]: (top=join(complement(X0),join(complement(join(X0,top)),X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f4948,f57])).
% 28.69/4.05 fof(f5108,plain,(
% 28.69/4.05 ![X0]: (top=join(X0,join(complement(X0),complement(join(X0,top)))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f227,f5039])).
% 28.69/4.05 fof(f5109,plain,(
% 28.69/4.05 ![X0]: (top=join(top,complement(join(X0,top))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f241,f5108])).
% 28.69/4.05 fof(f5116,plain,(
% 28.69/4.05 ![X0]: (join(X0,top)=top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f5109,f226])).
% 28.69/4.05 fof(f5136,plain,(
% 28.69/4.05 ![X0]: (join(top,X0)=top)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f19,f5116])).
% 28.69/4.05 fof(f6664,plain,(
% 28.69/4.05 ![X0]: (join(complement(X0),top)=complement(meet(X0,zero)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3494,f3020])).
% 28.69/4.05 fof(f6698,plain,(
% 28.69/4.05 ![X0]: (top=complement(meet(X0,zero)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f5116,f6664])).
% 28.69/4.05 fof(f6751,plain,(
% 28.69/4.05 ![X0]: (meet(X0,zero)=complement(top))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f6698,f2711])).
% 28.69/4.05 fof(f6788,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),composition(sF0_fnc,meet(X0,zero))))=meet(complement(sF2_fnc),composition(sF0_fnc,zero)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f6795,f4203])).
% 28.69/4.05 fof(f6790,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,composition(sF0_fnc,meet(X0,zero))))=meet(sK0_skl,composition(sF0_fnc,zero)))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f6795,f3947])).
% 28.69/4.05 fof(f6795,plain,(
% 28.69/4.05 ![X0]: (meet(X0,zero)=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f6751])).
% 28.69/4.05 fof(f6816,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),composition(sF0_fnc,zero)))=meet(complement(sF2_fnc),composition(sF0_fnc,zero)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f6788])).
% 28.69/4.05 fof(f6818,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,composition(sF0_fnc,zero)))=meet(sK0_skl,composition(sF0_fnc,zero)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f6790])).
% 28.69/4.05 fof(f9837,plain,(
% 28.69/4.05 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2711,f2734])).
% 28.69/4.05 fof(f12687,plain,(
% 28.69/4.05 ![X0]: (join(X0,meet(top,X0))=meet(top,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f2934,f960])).
% 28.69/4.05 fof(f12765,plain,(
% 28.69/4.05 ![X0]: (join(X0,X0)=meet(top,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2934,f12687])).
% 28.69/4.05 fof(f12772,plain,(
% 28.69/4.05 ![X0]: (join(X0,X0)=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2934,f12765])).
% 28.69/4.05 fof(f12880,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(join(X1,X0),X1))=join(X1,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f227,f12772])).
% 28.69/4.05 fof(f12926,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(X0,join(X1,X1)))=join(X1,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f242,f12880])).
% 28.69/4.05 fof(f12938,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f12772,f12926])).
% 28.69/4.05 fof(f13022,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(complement(X0),X1),meet(X0,X1)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f4440,f12938])).
% 28.69/4.05 fof(f13023,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(complement(X1),X0),meet(X0,X1)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f3147,f12938])).
% 28.69/4.05 fof(f13171,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(complement(X1),X0),meet(X1,X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f13022])).
% 28.69/4.05 fof(f13172,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(complement(X1),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f13171])).
% 28.69/4.05 fof(f13177,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f4440,f13172])).
% 28.69/4.05 fof(f13178,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(complement(X1),X0),meet(X0,X1)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f13023])).
% 28.69/4.05 fof(f13179,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(complement(X1),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f13178])).
% 28.69/4.05 fof(f13204,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3147,f13179])).
% 28.69/4.05 fof(f13365,plain,(
% 28.69/4.05 ![X0,X1]: (join(join(X0,meet(X1,complement(X0))),X1)=join(X0,meet(X1,complement(X0))))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f9837,f13177])).
% 28.69/4.05 fof(f13517,plain,(
% 28.69/4.05 ![X0,X1]: (join(meet(X0,complement(X1)),join(X1,X0))=join(X1,meet(X0,complement(X1))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f242,f13365])).
% 28.69/4.05 fof(f13518,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,join(X1,meet(X1,complement(X0))))=join(X0,meet(X1,complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f227,f13517])).
% 28.69/4.05 fof(f13530,plain,(
% 28.69/4.05 ![X0,X1]: (join(X0,X1)=join(X0,meet(X1,complement(X0))))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f13204,f13518])).
% 28.69/4.05 fof(f17093,plain,(
% 28.69/4.05 ![X0]: (composition(join(one,converse(X0)),complement(composition(join(one,X0),top)))=zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f869,f2748])).
% 28.69/4.05 fof(f17155,plain,(
% 28.69/4.05 ![X0]: (composition(join(one,converse(X0)),complement(join(top,composition(X0,top))))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f794,f17093])).
% 28.69/4.05 fof(f17156,plain,(
% 28.69/4.05 ![X0]: (composition(join(one,converse(X0)),complement(top))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f5136,f17155])).
% 28.69/4.05 fof(f17157,plain,(
% 28.69/4.05 ![X0]: (composition(join(one,converse(X0)),zero)=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f59,f17156])).
% 28.69/4.05 fof(f17158,plain,(
% 28.69/4.05 ![X0]: (join(zero,composition(converse(X0),zero))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f794,f17157])).
% 28.69/4.05 fof(f17163,plain,(
% 28.69/4.05 ![X0]: (converse(composition(zero,X0))=zero)),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f17164,f3823])).
% 28.69/4.05 fof(f17164,plain,(
% 28.69/4.05 ![X0]: (composition(converse(X0),zero)=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f17158])).
% 28.69/4.05 fof(f17321,plain,(
% 28.69/4.05 ![X0]: (composition(X0,converse(zero))=zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f202,f17163])).
% 28.69/4.05 fof(f17370,plain,(
% 28.69/4.05 ![X0]: (converse(zero)=composition(zero,X0))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f17163,f26])).
% 28.69/4.05 fof(f17373,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,composition(sF0_fnc,zero)))=meet(sK0_skl,zero))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f17421,f6818])).
% 28.69/4.05 fof(f17374,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),composition(sF0_fnc,zero)))=meet(complement(sF2_fnc),zero))),
% 28.69/4.05 inference(backward_demodulation,[status(thm)],[f17421,f6816])).
% 28.69/4.05 fof(f17421,plain,(
% 28.69/4.05 ![X0]: (composition(X0,zero)=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3792,f17321])).
% 28.69/4.05 fof(f17608,plain,(
% 28.69/4.05 ![X0]: (zero=composition(zero,X0))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f3792,f17370])).
% 28.69/4.05 fof(f17615,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,composition(sF0_fnc,X0)),meet(sK0_skl,zero))=meet(sK0_skl,zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f17421,f17373])).
% 28.69/4.05 fof(f17616,plain,(
% 28.69/4.05 ![X0]: (join(meet(sK0_skl,zero),meet(sK0_skl,composition(sF0_fnc,X0)))=meet(sK0_skl,zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f17615])).
% 28.69/4.05 fof(f17617,plain,(
% 28.69/4.05 ![X0]: (join(zero,meet(sK0_skl,composition(sF0_fnc,X0)))=meet(sK0_skl,zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f17616])).
% 28.69/4.05 fof(f17618,plain,(
% 28.69/4.05 ![X0]: (meet(sK0_skl,composition(sF0_fnc,X0))=meet(sK0_skl,zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f17617])).
% 28.69/4.05 fof(f17619,plain,(
% 28.69/4.05 ![X0]: (meet(sK0_skl,composition(sF0_fnc,X0))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f17618])).
% 28.69/4.05 fof(f17620,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),composition(sF0_fnc,X0)),meet(complement(sF2_fnc),zero))=meet(complement(sF2_fnc),zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f17421,f17374])).
% 28.69/4.05 fof(f17621,plain,(
% 28.69/4.05 ![X0]: (join(meet(complement(sF2_fnc),zero),meet(complement(sF2_fnc),composition(sF0_fnc,X0)))=meet(complement(sF2_fnc),zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f17620])).
% 28.69/4.05 fof(f17622,plain,(
% 28.69/4.05 ![X0]: (join(zero,meet(complement(sF2_fnc),composition(sF0_fnc,X0)))=meet(complement(sF2_fnc),zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f17621])).
% 28.69/4.05 fof(f17623,plain,(
% 28.69/4.05 ![X0]: (meet(complement(sF2_fnc),composition(sF0_fnc,X0))=meet(complement(sF2_fnc),zero))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f17622])).
% 28.69/4.05 fof(f17624,plain,(
% 28.69/4.05 ![X0]: (meet(complement(sF2_fnc),composition(sF0_fnc,X0))=zero)),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f17623])).
% 28.69/4.05 fof(f18236,plain,(
% 28.69/4.05 ![X0]: (meet(sK0_skl,composition(sF2_fnc,X0))=zero)),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f65,f17619])).
% 28.69/4.05 fof(f18468,plain,(
% 28.69/4.05 ![X0]: (join(meet(composition(sK0_skl,X0),sF2_fnc),meet(sF2_fnc,composition(zero,X0)))=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 28.69/4.05 inference(paramodulation,[status(thm)],[f18236,f3356])).
% 28.69/4.05 fof(f18491,plain,(
% 28.69/4.05 ![X0]: (join(meet(sF2_fnc,composition(zero,X0)),meet(composition(sK0_skl,X0),sF2_fnc))=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f19,f18468])).
% 28.69/4.05 fof(f18492,plain,(
% 28.69/4.05 ![X0]: (join(meet(sF2_fnc,zero),meet(composition(sK0_skl,X0),sF2_fnc))=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f17608,f18491])).
% 28.69/4.05 fof(f18493,plain,(
% 28.69/4.05 ![X0]: (join(zero,meet(composition(sK0_skl,X0),sF2_fnc))=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f6795,f18492])).
% 28.69/4.05 fof(f18494,plain,(
% 28.69/4.05 ![X0]: (meet(composition(sK0_skl,X0),sF2_fnc)=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 28.69/4.05 inference(forward_demodulation,[status(thm)],[f2818,f18493])).
% 28.69/4.05 fof(f18495,plain,(
% 19.50/4.12 ![X0]: (meet(sF2_fnc,composition(sK0_skl,X0))=meet(sF2_fnc,composition(meet(sK0_skl,composition(sF2_fnc,converse(X0))),X0)))),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f3346,f18494])).
% 19.50/4.12 fof(f18496,plain,(
% 19.50/4.12 ![X0]: (meet(sF2_fnc,composition(sK0_skl,X0))=meet(sF2_fnc,composition(zero,X0)))),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f18236,f18495])).
% 19.50/4.12 fof(f18497,plain,(
% 19.50/4.12 ![X0]: (meet(sF2_fnc,composition(sK0_skl,X0))=meet(sF2_fnc,zero))),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f17608,f18496])).
% 19.50/4.12 fof(f18498,plain,(
% 19.50/4.12 ![X0]: (meet(sF2_fnc,composition(sK0_skl,X0))=zero)),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f6795,f18497])).
% 19.50/4.12 fof(f18520,plain,(
% 19.50/4.12 meet(sF2_fnc,sF1_fnc)=zero),
% 19.50/4.12 inference(paramodulation,[status(thm)],[f38,f18498])).
% 19.50/4.12 fof(f18542,plain,(
% 19.50/4.12 meet(sF1_fnc,sF2_fnc)=zero),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f3346,f18520])).
% 19.50/4.12 fof(f18584,plain,(
% 19.50/4.12 sF2_fnc=join(meet(sF0_fnc,sF2_fnc),zero)),
% 19.50/4.12 inference(paramodulation,[status(thm)],[f18542,f3350])).
% 19.50/4.12 fof(f18603,plain,(
% 19.50/4.12 sF2_fnc=meet(sF0_fnc,sF2_fnc)),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f2870,f18584])).
% 19.50/4.12 fof(f19961,plain,(
% 19.50/4.12 join(sF0_fnc,sF2_fnc)=sF0_fnc),
% 19.50/4.12 inference(paramodulation,[status(thm)],[f18603,f13204])).
% 19.50/4.12 fof(f23715,plain,(
% 19.50/4.12 meet(complement(sF2_fnc),sF0_fnc)=zero),
% 19.50/4.12 inference(paramodulation,[status(thm)],[f24,f17624])).
% 19.50/4.12 fof(f23744,plain,(
% 19.50/4.12 meet(sF0_fnc,complement(sF2_fnc))=zero),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f3346,f23715])).
% 19.50/4.12 fof(f23820,plain,(
% 19.50/4.12 join(sF2_fnc,sF0_fnc)=join(sF2_fnc,zero)),
% 19.50/4.12 inference(paramodulation,[status(thm)],[f23744,f13530])).
% 19.50/4.12 fof(f23919,plain,(
% 19.50/4.12 join(sF0_fnc,sF2_fnc)=join(sF2_fnc,zero)),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f19,f23820])).
% 19.50/4.12 fof(f23920,plain,(
% 19.50/4.12 sF0_fnc=join(sF2_fnc,zero)),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f19961,f23919])).
% 19.50/4.12 fof(f23921,plain,(
% 19.50/4.12 sF0_fnc=sF2_fnc),
% 19.50/4.12 inference(forward_demodulation,[status(thm)],[f2870,f23920])).
% 19.50/4.12 fof(f23922,plain,(
% 19.50/4.12 $false),
% 19.50/4.12 inference(forward_subsumption_resolution,[status(thm)],[f23921,f42])).
% 19.50/4.12 % SZS output end CNFRefutation for theBenchmark.p
% 19.50/4.15 % Elapsed time: 3.775656 seconds
% 19.50/4.15 % CPU time: 29.701853 seconds
% 19.50/4.15 % Total memory used: 413.138 MB
% 19.50/4.15 % Net memory used: 405.930 MB
%------------------------------------------------------------------------------