%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL034+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:41 PM UTC 2026
% Result : Theorem 112.62s 14.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL034+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n018.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 21 04:07:44 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.47 % Drodi V4.1.1
% 112.62/14.82 % Refutation found
% 112.62/14.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 112.62/14.82 % SZS output start CNFRefutation for theBenchmark
% 112.62/14.82 fof(f1,axiom,(
% 112.62/14.82 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f2,axiom,(
% 112.62/14.82 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f3,axiom,(
% 112.62/14.82 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f4,axiom,(
% 112.62/14.82 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f5,axiom,(
% 112.62/14.82 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f6,axiom,(
% 112.62/14.82 (! [X0] : composition(X0,one) = X0 )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f7,axiom,(
% 112.62/14.82 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f8,axiom,(
% 112.62/14.82 (! [X0] : converse(converse(X0)) = X0 )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f9,axiom,(
% 112.62/14.82 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f10,axiom,(
% 112.62/14.82 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f11,axiom,(
% 112.62/14.82 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f12,axiom,(
% 112.62/14.82 (! [X0] : top = join(X0,complement(X0)) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f13,axiom,(
% 112.62/14.82 (! [X0] : zero = meet(X0,complement(X0)) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f14,conjecture,(
% 112.62/14.82 (! [X0,X1,X2] :( composition(X0,top) = X0=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ) )),
% 112.62/14.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 112.62/14.82 fof(f15,negated_conjecture,(
% 112.62/14.82 ~((! [X0,X1,X2] :( composition(X0,top) = X0=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ) ))),
% 112.62/14.82 inference(negated_conjecture,[status(cth)],[f14])).
% 112.62/14.82 fof(f16,plain,(
% 112.62/14.82 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f1])).
% 112.62/14.82 fof(f17,plain,(
% 112.62/14.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f2])).
% 112.62/14.82 fof(f18,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f3])).
% 112.62/14.82 fof(f19,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f4])).
% 112.62/14.82 fof(f20,plain,(
% 112.62/14.82 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f5])).
% 112.62/14.82 fof(f21,plain,(
% 112.62/14.82 ![X0]: (composition(X0,one)=X0)),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f6])).
% 112.62/14.82 fof(f22,plain,(
% 112.62/14.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f7])).
% 112.62/14.82 fof(f23,plain,(
% 112.62/14.82 ![X0]: (converse(converse(X0))=X0)),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f8])).
% 112.62/14.82 fof(f24,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f9])).
% 112.62/14.82 fof(f25,plain,(
% 112.62/14.82 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f10])).
% 112.62/14.82 fof(f26,plain,(
% 112.62/14.82 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f11])).
% 112.62/14.82 fof(f27,plain,(
% 112.62/14.82 ![X0]: (top=join(X0,complement(X0)))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f12])).
% 112.62/14.82 fof(f28,plain,(
% 112.62/14.82 ![X0]: (zero=meet(X0,complement(X0)))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f13])).
% 112.62/14.82 fof(f29,plain,(
% 112.62/14.82 (?[X0,X1,X2]: (composition(X0,top)=X0&~join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2)))=composition(meet(X1,converse(X0)),meet(X0,X2))))),
% 112.62/14.82 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 112.62/14.82 fof(f30,plain,(
% 112.62/14.82 ?[X0]: (composition(X0,top)=X0&(?[X1,X2]: ~join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2)))=composition(meet(X1,converse(X0)),meet(X0,X2))))),
% 112.62/14.82 inference(miniscoping,[status(thm)],[f29])).
% 112.62/14.82 fof(f31,plain,(
% 112.62/14.82 (composition(sK0_skl,top)=sK0_skl&~join(composition(sK1_skl,meet(sK0_skl,sK2_skl)),composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))=composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))),
% 112.62/14.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl)],[f30])).
% 112.62/14.82 fof(f32,plain,(
% 112.62/14.82 composition(sK0_skl,top)=sK0_skl),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f31])).
% 112.62/14.82 fof(f33,plain,(
% 112.62/14.82 ~join(composition(sK1_skl,meet(sK0_skl,sK2_skl)),composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl)))=composition(meet(sK1_skl,converse(sK0_skl)),meet(sK0_skl,sK2_skl))),
% 112.62/14.82 inference(cnf_transformation,[status(thm)],[f31])).
% 112.62/14.82 fof(f34,definition,(
% 112.62/14.82 sF2_fnc=meet(sK0_skl,sK2_skl)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 112.62/14.82 fof(f35,definition,(
% 112.62/14.82 sF1_fnc=composition(sK1_skl,sF2_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 112.62/14.82 fof(f36,definition,(
% 112.62/14.82 sF5_fnc=converse(sK0_skl)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 112.62/14.82 fof(f37,definition,(
% 112.62/14.82 sF4_fnc=meet(sK1_skl,sF5_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 112.62/14.82 fof(f38,definition,(
% 112.62/14.82 sF3_fnc=composition(sF4_fnc,sF2_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 112.62/14.82 fof(f39,definition,(
% 112.62/14.82 sF0_fnc=join(sF1_fnc,sF3_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 112.62/14.82 fof(f40,definition,(
% 112.62/14.82 sF7_fnc=meet(sK1_skl,sF5_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 112.62/14.82 fof(f41,definition,(
% 112.62/14.82 sF6_fnc=composition(sF7_fnc,sF2_fnc)),
% 112.62/14.82 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 112.62/14.82 fof(f42,plain,(
% 112.62/14.82 ~sF0_fnc=sF6_fnc),
% 112.62/14.82 inference(definition_folding,[],[f33,f41,f40,f39,f38,f37,f36,f35,f34])).
% 112.62/14.82 fof(f43,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 112.62/14.82 fof(f44,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f19,f43])).
% 112.62/14.82 fof(f45,plain,(
% 112.62/14.82 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 112.62/14.82 fof(f46,plain,(
% 112.62/14.82 sF7_fnc=sF4_fnc),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f37,f40])).
% 112.62/14.82 fof(f47,plain,(
% 112.62/14.82 sF6_fnc=composition(sF4_fnc,sF2_fnc)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f46,f41])).
% 112.62/14.82 fof(f48,plain,(
% 112.62/14.82 sF6_fnc=sF3_fnc),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f38,f47])).
% 112.62/14.82 fof(f49,plain,(
% 112.62/14.82 ~sF0_fnc=sF3_fnc),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f48,f42])).
% 112.62/14.82 fof(f50,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f44])).
% 112.62/14.82 fof(f52,plain,(
% 112.62/14.82 converse(sF5_fnc)=sK0_skl),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f36,f23])).
% 112.62/14.82 fof(f73,plain,(
% 112.62/14.82 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f27,f19])).
% 112.62/14.82 fof(f74,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f19])).
% 112.62/14.82 fof(f76,plain,(
% 112.62/14.82 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f19])).
% 112.62/14.82 fof(f77,plain,(
% 112.62/14.82 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f19])).
% 112.62/14.82 fof(f78,plain,(
% 112.62/14.82 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f27])).
% 112.62/14.82 fof(f79,plain,(
% 112.62/14.82 zero=complement(top)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f28,f73])).
% 112.62/14.82 fof(f80,plain,(
% 112.62/14.82 ![X0,X1]: (top=join(meet(X0,X1),join(complement(X0),complement(X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f78])).
% 112.62/14.82 fof(f81,plain,(
% 112.62/14.82 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f27,f17])).
% 112.62/14.82 fof(f82,plain,(
% 112.62/14.82 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f17])).
% 112.62/14.82 fof(f86,plain,(
% 112.62/14.82 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f27,f17])).
% 112.62/14.82 fof(f92,plain,(
% 112.62/14.82 ![X0,X1]: (top=join(complement(X0),join(meet(X1,X0),complement(X1))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f82,f80])).
% 112.62/14.82 fof(f95,plain,(
% 112.62/14.82 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X1,X0))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f92])).
% 112.62/14.82 fof(f96,plain,(
% 112.62/14.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f22])).
% 112.62/14.82 fof(f100,plain,(
% 112.62/14.82 ![X0]: (composition(join(sF4_fnc,X0),sF2_fnc)=join(sF3_fnc,composition(X0,sF2_fnc)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f38,f22])).
% 112.62/14.82 fof(f102,plain,(
% 112.62/14.82 ![X0]: (composition(join(sK1_skl,X0),sF2_fnc)=join(sF1_fnc,composition(X0,sF2_fnc)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f35,f22])).
% 112.62/14.82 fof(f107,plain,(
% 112.62/14.82 ![X0]: (composition(join(X0,sF4_fnc),sF2_fnc)=join(composition(X0,sF2_fnc),sF3_fnc))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f38,f22])).
% 112.62/14.82 fof(f122,plain,(
% 112.62/14.82 ![X0]: (composition(join(X0,sF4_fnc),sF2_fnc)=join(sF3_fnc,composition(X0,sF2_fnc)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f107])).
% 112.62/14.82 fof(f139,plain,(
% 112.62/14.82 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f79,f19])).
% 112.62/14.82 fof(f142,plain,(
% 112.62/14.82 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f139])).
% 112.62/14.82 fof(f151,plain,(
% 112.62/14.82 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f21,f20])).
% 112.62/14.82 fof(f185,plain,(
% 112.62/14.82 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f23,f25])).
% 112.62/14.82 fof(f197,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f24])).
% 112.62/14.82 fof(f200,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f23,f24])).
% 112.62/14.82 fof(f210,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f74])).
% 112.62/14.82 fof(f226,plain,(
% 112.62/14.82 sF2_fnc=meet(sK2_skl,sK0_skl)),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f210,f34])).
% 112.62/14.82 fof(f340,plain,(
% 112.62/14.82 join(complement(top),composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f32,f45])).
% 112.62/14.82 fof(f354,plain,(
% 112.62/14.82 join(zero,composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f340])).
% 112.62/14.82 fof(f355,plain,(
% 112.62/14.82 join(zero,composition(sF5_fnc,complement(sK0_skl)))=complement(top)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f36,f354])).
% 112.62/14.82 fof(f356,plain,(
% 112.62/14.82 join(zero,composition(sF5_fnc,complement(sK0_skl)))=zero),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f355])).
% 112.62/14.82 fof(f361,plain,(
% 112.62/14.82 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f28,f50])).
% 112.62/14.82 fof(f364,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f74,f50])).
% 112.62/14.82 fof(f365,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f50])).
% 112.62/14.82 fof(f367,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f86,f50])).
% 112.62/14.82 fof(f368,plain,(
% 112.62/14.82 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f27,f50])).
% 112.62/14.82 fof(f379,plain,(
% 112.62/14.82 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f74,f361])).
% 112.62/14.82 fof(f380,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f364])).
% 112.62/14.82 fof(f381,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f365])).
% 112.62/14.82 fof(f383,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f367])).
% 112.62/14.82 fof(f384,plain,(
% 112.62/14.82 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f368])).
% 112.62/14.82 fof(f385,plain,(
% 112.62/14.82 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f384])).
% 112.62/14.82 fof(f388,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(complement(X0),complement(X1)),join(complement(X0),X1))=complement(X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f50,f76])).
% 112.62/14.82 fof(f413,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(complement(X0),X1),join(complement(X0),complement(X1)))=complement(X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f388])).
% 112.62/14.82 fof(f498,plain,(
% 112.62/14.82 composition(join(sF4_fnc,sK1_skl),sF2_fnc)=join(sF3_fnc,sF1_fnc)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f35,f100])).
% 112.62/14.82 fof(f501,plain,(
% 112.62/14.82 composition(join(sK1_skl,sF4_fnc),sF2_fnc)=join(sF3_fnc,sF1_fnc)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f498])).
% 112.62/14.82 fof(f502,plain,(
% 112.62/14.82 composition(join(sK1_skl,sF4_fnc),sF2_fnc)=join(sF1_fnc,sF3_fnc)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f501])).
% 112.62/14.82 fof(f503,plain,(
% 112.62/14.82 composition(join(sK1_skl,sF4_fnc),sF2_fnc)=sF0_fnc),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f39,f502])).
% 112.62/14.82 fof(f518,plain,(
% 112.62/14.82 top=join(zero,meet(top,complement(zero)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f79,f385])).
% 112.62/14.82 fof(f534,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f380])).
% 112.62/14.82 fof(f536,plain,(
% 112.62/14.82 ![X0]: (X0=join(meet(top,X0),meet(X0,zero)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f79,f380])).
% 112.62/14.82 fof(f551,plain,(
% 112.62/14.82 ![X0]: (X0=join(meet(top,X0),meet(zero,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f536])).
% 112.62/14.82 fof(f561,plain,(
% 112.62/14.82 ![X0]: (X0=join(meet(zero,X0),meet(top,X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f551])).
% 112.62/14.82 fof(f588,plain,(
% 112.62/14.82 complement(zero)=join(zero,meet(top,complement(zero)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f28,f561])).
% 112.62/14.82 fof(f598,plain,(
% 112.62/14.82 complement(zero)=top),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f518,f588])).
% 112.62/14.82 fof(f605,plain,(
% 112.62/14.82 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f598,f50])).
% 112.62/14.82 fof(f672,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f381])).
% 112.62/14.82 fof(f779,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(join(complement(X0),X1)))),complement(top)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f81,f50])).
% 112.62/14.82 fof(f820,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f779])).
% 112.62/14.82 fof(f821,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(join(complement(X0),X1))))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f820])).
% 112.62/14.82 fof(f832,plain,(
% 112.62/14.82 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f28,f534])).
% 112.62/14.82 fof(f849,plain,(
% 112.62/14.82 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f832])).
% 112.62/14.82 fof(f852,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(X0,X1))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f856,f383])).
% 112.62/14.82 fof(f856,plain,(
% 112.62/14.82 ![X0]: (complement(complement(X0))=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f385,f849])).
% 112.62/14.82 fof(f868,plain,(
% 112.62/14.82 ![X0]: (complement(meet(X0,top))=join(zero,complement(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f142,f856])).
% 112.62/14.82 fof(f870,plain,(
% 112.62/14.82 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f74,f856])).
% 112.62/14.82 fof(f871,plain,(
% 112.62/14.82 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f19,f856])).
% 112.62/14.82 fof(f873,plain,(
% 112.62/14.82 ![X0,X1,X2]: (meet(complement(X0),join(complement(X1),complement(X2)))=complement(join(X0,meet(X1,X2))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f77])).
% 112.62/14.82 fof(f881,plain,(
% 112.62/14.82 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f74])).
% 112.62/14.82 fof(f884,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f19])).
% 112.62/14.82 fof(f946,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(complement(X0),X1),complement(meet(X1,X0)))=complement(X0))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f870,f413])).
% 112.62/14.82 fof(f962,plain,(
% 112.62/14.82 ![X0,X1,X2]: (meet(complement(X0),complement(meet(X1,X2)))=complement(join(X0,meet(X1,X2))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f871,f873])).
% 112.62/14.82 fof(f973,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,meet(complement(X1),X0)))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f881,f821])).
% 112.62/14.82 fof(f1027,plain,(
% 112.62/14.82 ![X0,X1]: (meet(complement(meet(X0,X1)),join(complement(X1),X0))=complement(X1))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f946])).
% 112.62/14.82 fof(f1111,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(X0,X1))=converse(join(X1,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f24,f197])).
% 112.62/14.82 fof(f1116,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(X0,converse(X1)))=join(X1,converse(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f23,f197])).
% 112.62/14.82 fof(f1120,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f23,f197])).
% 112.62/14.82 fof(f1135,plain,(
% 112.62/14.82 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f21,f185])).
% 112.62/14.82 fof(f1162,plain,(
% 112.62/14.82 ![X0]: (X0=composition(converse(one),X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f23,f1135])).
% 112.62/14.82 fof(f1182,plain,(
% 112.62/14.82 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f151,f1162])).
% 112.62/14.82 fof(f1186,plain,(
% 112.62/14.82 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1162,f45])).
% 112.62/14.82 fof(f1202,plain,(
% 112.62/14.82 ![X0]: (composition(one,X0)=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1162,f1182])).
% 112.62/14.82 fof(f1206,plain,(
% 112.62/14.82 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f871,f1186])).
% 112.62/14.82 fof(f1207,plain,(
% 112.62/14.82 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1202,f1206])).
% 112.62/14.82 fof(f1273,plain,(
% 112.62/14.82 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1207,f856])).
% 112.62/14.82 fof(f1283,plain,(
% 112.62/14.82 ![X0]: (X0=join(zero,X0))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f1286,f379])).
% 112.62/14.82 fof(f1286,plain,(
% 112.62/14.82 ![X0]: (X0=meet(X0,X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f1273])).
% 112.62/14.82 fof(f1309,plain,(
% 112.62/14.82 composition(sF5_fnc,complement(sK0_skl))=zero),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f1283,f356])).
% 112.62/14.82 fof(f1311,plain,(
% 112.62/14.82 ![X0,X1]: (X0=meet(X0,join(X1,meet(complement(X1),X0))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f1283,f973])).
% 112.62/14.82 fof(f1315,plain,(
% 112.62/14.82 ![X0]: (complement(meet(X0,top))=complement(X0))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f1283,f868])).
% 112.62/14.82 fof(f1321,plain,(
% 112.62/14.82 ![X0]: (X0=join(X0,zero))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f1283])).
% 112.62/14.82 fof(f1413,plain,(
% 112.62/14.82 ![X0]: (composition(join(sF5_fnc,X0),complement(sK0_skl))=join(zero,composition(X0,complement(sK0_skl))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1309,f22])).
% 112.62/14.82 fof(f1421,plain,(
% 112.62/14.82 ![X0]: (composition(join(sF5_fnc,X0),complement(sK0_skl))=composition(X0,complement(sK0_skl)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1283,f1413])).
% 112.62/14.82 fof(f1431,plain,(
% 112.62/14.82 ![X0]: (complement(complement(X0))=meet(X0,top))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1315,f856])).
% 112.62/14.82 fof(f1453,plain,(
% 112.62/14.82 ![X0]: (X0=meet(X0,top))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f1431])).
% 112.62/14.82 fof(f1482,plain,(
% 112.62/14.82 ![X0]: (X0=meet(top,X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f1453])).
% 112.62/14.82 fof(f1558,plain,(
% 112.62/14.82 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f82])).
% 112.62/14.82 fof(f1811,plain,(
% 112.62/14.82 ![X0]: (top=join(complement(X0),join(complement(X0),X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1286,f95])).
% 112.62/14.82 fof(f1854,plain,(
% 112.62/14.82 ![X0]: (top=join(complement(X0),join(X0,complement(X0))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f82,f1811])).
% 112.62/14.82 fof(f1855,plain,(
% 112.62/14.82 ![X0]: (top=join(X0,join(complement(X0),complement(X0))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f82,f1854])).
% 112.62/14.82 fof(f1856,plain,(
% 112.62/14.82 ![X0]: (top=join(top,complement(X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f86,f1855])).
% 112.62/14.82 fof(f2067,plain,(
% 112.62/14.82 ![X0]: (top=join(top,X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f1856])).
% 112.62/14.82 fof(f2070,plain,(
% 112.62/14.82 ![X0]: (join(X0,top)=top)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1856,f81])).
% 112.62/14.82 fof(f2100,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X0,X1))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f2067,f852])).
% 112.62/14.82 fof(f2101,plain,(
% 112.62/14.82 ![X0]: (zero=join(meet(zero,X0),complement(top)))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f2067,f605])).
% 112.62/14.82 fof(f2119,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f2100])).
% 112.62/14.82 fof(f2120,plain,(
% 112.62/14.82 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1283,f2119])).
% 112.62/14.82 fof(f2121,plain,(
% 112.62/14.82 ![X0]: (zero=join(complement(top),meet(zero,X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f2101])).
% 112.62/14.82 fof(f2122,plain,(
% 112.62/14.82 ![X0]: (zero=join(zero,meet(zero,X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f79,f2121])).
% 112.62/14.82 fof(f2127,plain,(
% 112.62/14.82 ![X0]: (zero=meet(zero,X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1283,f2122])).
% 112.62/14.82 fof(f2159,plain,(
% 112.62/14.82 ![X0]: (zero=meet(X0,zero))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f2127])).
% 112.62/14.82 fof(f2291,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f672,f2120])).
% 112.62/14.82 fof(f2292,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f534,f2120])).
% 112.62/14.82 fof(f2297,plain,(
% 112.62/14.82 ![X0,X1]: (converse(X0)=meet(converse(X0),converse(join(X1,X0))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f197,f2120])).
% 112.62/14.82 fof(f2312,plain,(
% 112.62/14.82 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f16,f2120])).
% 112.62/14.82 fof(f2323,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f2291])).
% 112.62/14.82 fof(f2324,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f2292])).
% 112.62/14.82 fof(f2433,plain,(
% 112.62/14.82 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f22,f96])).
% 112.62/14.82 fof(f2639,plain,(
% 112.62/14.82 meet(sK1_skl,sF5_fnc)=meet(sK1_skl,sF4_fnc)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f37,f2323])).
% 112.62/14.82 fof(f2661,plain,(
% 112.62/14.82 sF4_fnc=meet(sK1_skl,sF4_fnc)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f37,f2639])).
% 112.62/14.82 fof(f2702,plain,(
% 112.62/14.82 meet(sK2_skl,sK0_skl)=meet(sK0_skl,sF2_fnc)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f226,f2324])).
% 112.62/14.82 fof(f2713,plain,(
% 112.62/14.82 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f2324])).
% 112.62/14.82 fof(f2733,plain,(
% 112.62/14.82 sF2_fnc=meet(sK0_skl,sF2_fnc)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f226,f2702])).
% 112.62/14.82 fof(f3643,plain,(
% 112.62/14.82 ![X0,X1]: (X0=meet(X0,join(X1,meet(X0,complement(X1)))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f210,f1311])).
% 112.62/14.82 fof(f3927,plain,(
% 112.62/14.82 ![X0,X1]: (X0=meet(X0,join(complement(X1),meet(X0,X1))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f3643])).
% 112.62/14.82 fof(f4118,plain,(
% 112.62/14.82 sK1_skl=meet(sK1_skl,join(complement(sF5_fnc),sF4_fnc))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f37,f3927])).
% 112.62/14.82 fof(f4171,plain,(
% 112.62/14.82 sK1_skl=meet(sK1_skl,join(sF4_fnc,complement(sF5_fnc)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f4118])).
% 112.62/14.82 fof(f4205,plain,(
% 112.62/14.82 ![X0]: (converse(top)=join(X0,converse(top)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f2070,f200])).
% 112.62/14.82 fof(f4206,plain,(
% 112.62/14.82 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1321,f200])).
% 112.62/14.82 fof(f4212,plain,(
% 112.62/14.82 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f27,f200])).
% 112.62/14.82 fof(f4247,plain,(
% 112.62/14.82 ![X0]: (X0=join(X0,converse(zero)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f23,f4206])).
% 112.62/14.82 fof(f4269,plain,(
% 112.62/14.82 zero=converse(zero)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f1283,f4247])).
% 112.62/14.82 fof(f4362,plain,(
% 112.62/14.82 converse(top)=top),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f2067,f4205])).
% 112.62/14.82 fof(f4402,plain,(
% 112.62/14.82 ![X0]: (top=join(X0,converse(complement(converse(X0)))))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f4362,f4212])).
% 112.62/14.82 fof(f6487,plain,(
% 112.62/14.82 ![X0,X1]: (complement(meet(X0,complement(X1)))=join(X1,complement(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f856,f870])).
% 112.62/14.82 fof(f6505,plain,(
% 112.62/14.82 ![X0,X1]: (complement(X0)=meet(complement(X0),complement(meet(X0,X1))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f870,f2312])).
% 112.62/14.82 fof(f6531,plain,(
% 112.62/14.82 ![X0,X1]: (complement(X0)=complement(join(X0,meet(X0,X1))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f962,f6505])).
% 112.62/14.82 fof(f6615,plain,(
% 112.62/14.82 ![X0,X1]: (complement(complement(X0))=join(X0,meet(X0,X1)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f6531,f856])).
% 112.62/14.82 fof(f6690,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f6615])).
% 112.62/14.82 fof(f6980,plain,(
% 112.62/14.82 sK0_skl=join(sK0_skl,sF2_fnc)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f2733,f6690])).
% 112.62/14.82 fof(f6989,plain,(
% 112.62/14.82 sK1_skl=join(sK1_skl,sF4_fnc)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f2661,f6690])).
% 112.62/14.82 fof(f6991,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f2713,f6690])).
% 112.62/14.82 fof(f7046,plain,(
% 112.62/14.82 composition(sK1_skl,sF2_fnc)=sF0_fnc),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f6989,f503])).
% 112.62/14.82 fof(f7077,plain,(
% 112.62/14.82 sF1_fnc=sF0_fnc),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f7046,f35])).
% 112.62/14.82 fof(f7089,plain,(
% 112.62/14.82 ![X0]: (composition(join(sK1_skl,X0),sF2_fnc)=join(sF0_fnc,composition(X0,sF2_fnc)))),
% 112.62/14.82 inference(backward_demodulation,[status(thm)],[f7077,f102])).
% 112.62/14.82 fof(f7480,plain,(
% 112.62/14.82 ![X0]: (join(sK1_skl,join(sF4_fnc,X0))=join(sK1_skl,X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f6989,f17])).
% 112.62/14.82 fof(f7598,plain,(
% 112.62/14.82 ![X0,X1]: (converse(converse(X0))=join(X0,converse(meet(X1,converse(X0)))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f6991,f200])).
% 112.62/14.82 fof(f7739,plain,(
% 112.62/14.82 ![X0,X1]: (X0=join(X0,converse(meet(X1,converse(X0)))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f23,f7598])).
% 112.62/14.82 fof(f27774,plain,(
% 112.62/14.82 converse(sF2_fnc)=meet(converse(sF2_fnc),converse(sK0_skl))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f6980,f2297])).
% 112.62/14.82 fof(f27994,plain,(
% 112.62/14.82 converse(sF2_fnc)=meet(converse(sK0_skl),converse(sF2_fnc))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f27774])).
% 112.62/14.82 fof(f27995,plain,(
% 112.62/14.82 converse(sF2_fnc)=meet(sF5_fnc,converse(sF2_fnc))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f36,f27994])).
% 112.62/14.82 fof(f30022,plain,(
% 112.62/14.82 join(sF4_fnc,complement(sF5_fnc))=join(join(sF4_fnc,complement(sF5_fnc)),sK1_skl)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f4171,f6991])).
% 112.62/14.82 fof(f30065,plain,(
% 112.62/14.82 join(sF4_fnc,complement(sF5_fnc))=join(complement(sF5_fnc),join(sK1_skl,sF4_fnc))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1558,f30022])).
% 112.62/14.82 fof(f30066,plain,(
% 112.62/14.82 join(sF4_fnc,complement(sF5_fnc))=join(sK1_skl,join(sF4_fnc,complement(sF5_fnc)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f82,f30065])).
% 112.62/14.82 fof(f30070,plain,(
% 112.62/14.82 join(sF4_fnc,complement(sF5_fnc))=join(sK1_skl,complement(sF5_fnc))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f7480,f30066])).
% 112.62/14.82 fof(f101188,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(X0,complement(X1)),join(complement(complement(X0)),X1))=complement(complement(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f6487,f1027])).
% 112.62/14.82 fof(f101524,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(X0,complement(X1)),join(X0,X1))=complement(complement(X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f101188])).
% 112.62/14.82 fof(f101525,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(X0,X1),join(X0,complement(X1)))=complement(complement(X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f101524])).
% 112.62/14.82 fof(f101527,plain,(
% 112.62/14.82 ![X0,X1]: (meet(join(X0,X1),join(X0,complement(X1)))=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f101525])).
% 112.62/14.82 fof(f102804,plain,(
% 112.62/14.82 ![X0]: (meet(top,join(X0,complement(converse(complement(converse(X0))))))=X0)),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f4402,f101527])).
% 112.62/14.82 fof(f103105,plain,(
% 112.62/14.82 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1482,f102804])).
% 112.62/14.82 fof(f103477,plain,(
% 112.62/14.82 ![X0]: (converse(converse(X0))=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f103105,f1120])).
% 112.62/14.82 fof(f103501,plain,(
% 112.62/14.82 ![X0]: (meet(X0,complement(complement(converse(complement(converse(complement(X0)))))))=complement(complement(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f103105,f884])).
% 112.62/14.82 fof(f103626,plain,(
% 112.62/14.82 ![X0]: (X0=join(converse(complement(converse(complement(converse(converse(X0)))))),X0))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f23,f103477])).
% 112.62/14.82 fof(f103627,plain,(
% 112.62/14.82 ![X0]: (X0=join(X0,converse(complement(converse(complement(converse(converse(X0))))))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f16,f103626])).
% 112.62/14.82 fof(f103628,plain,(
% 112.62/14.82 ![X0]: (X0=join(X0,converse(complement(converse(complement(X0))))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f23,f103627])).
% 112.62/14.82 fof(f103647,plain,(
% 112.62/14.82 ![X0]: (meet(X0,converse(complement(converse(complement(X0)))))=complement(complement(X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f103501])).
% 112.62/14.82 fof(f103649,plain,(
% 112.62/14.82 ![X0]: (meet(X0,converse(complement(converse(complement(X0)))))=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f856,f103647])).
% 112.62/14.82 fof(f103849,plain,(
% 112.62/14.82 ![X0]: (converse(complement(converse(complement(X0))))=meet(converse(complement(converse(complement(X0)))),X0))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f103628,f2312])).
% 112.62/14.82 fof(f104010,plain,(
% 112.62/14.82 ![X0]: (converse(complement(converse(complement(X0))))=meet(X0,converse(complement(converse(complement(X0))))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f210,f103849])).
% 112.62/14.82 fof(f104041,plain,(
% 112.62/14.82 ![X0]: (converse(complement(converse(complement(X0))))=X0)),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f103649,f104010])).
% 112.62/14.82 fof(f104144,plain,(
% 112.62/14.82 ![X0,X1]: (converse(join(X0,X1))=join(complement(converse(complement(X1))),converse(X0)))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f104041,f1116])).
% 112.62/14.82 fof(f104151,plain,(
% 112.62/14.82 ![X0,X1]: (complement(converse(complement(X0)))=join(complement(converse(complement(X0))),converse(meet(X1,X0))))),
% 112.62/14.82 inference(paramodulation,[status(thm)],[f104041,f7739])).
% 112.62/14.82 fof(f104240,plain,(
% 112.62/14.82 ![X0,X1]: (complement(converse(complement(X0)))=converse(join(meet(X1,X0),X0)))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f104144,f104151])).
% 112.62/14.82 fof(f104241,plain,(
% 112.62/14.82 ![X0,X1]: (complement(converse(complement(X0)))=converse(join(X0,meet(X1,X0))))),
% 112.62/14.82 inference(forward_demodulation,[status(thm)],[f1111,f104240])).
% 18.34/15.02 fof(f104287,plain,(
% 18.34/15.02 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f6991,f104241])).
% 18.34/15.02 fof(f104549,plain,(
% 18.34/15.02 ![X0]: (complement(converse(X0))=converse(complement(X0)))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f856,f104287])).
% 18.34/15.02 fof(f105257,plain,(
% 18.34/15.02 complement(sK0_skl)=converse(complement(sF5_fnc))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f52,f104549])).
% 18.34/15.02 fof(f105581,plain,(
% 18.34/15.02 ![X0]: (converse(composition(complement(sF5_fnc),X0))=composition(converse(X0),complement(sK0_skl)))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f105257,f25])).
% 18.34/15.02 fof(f156718,plain,(
% 18.34/15.02 ![X0]: (composition(sF5_fnc,complement(sK0_skl))=composition(meet(sF5_fnc,X0),complement(sK0_skl)))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f6690,f1421])).
% 18.34/15.02 fof(f156811,plain,(
% 18.34/15.02 ![X0]: (zero=composition(meet(sF5_fnc,X0),complement(sK0_skl)))),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f1309,f156718])).
% 18.34/15.02 fof(f160215,plain,(
% 18.34/15.02 zero=composition(converse(sF2_fnc),complement(sK0_skl))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f27995,f156811])).
% 18.34/15.02 fof(f160281,plain,(
% 18.34/15.02 zero=converse(composition(complement(sF5_fnc),sF2_fnc))),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f105581,f160215])).
% 18.34/15.02 fof(f160365,plain,(
% 18.34/15.02 ![X0]: (converse(join(X0,zero))=join(composition(complement(sF5_fnc),sF2_fnc),converse(X0)))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f160281,f1116])).
% 18.34/15.02 fof(f160372,plain,(
% 18.34/15.02 ![X0]: (composition(complement(sF5_fnc),sF2_fnc)=join(composition(complement(sF5_fnc),sF2_fnc),converse(meet(X0,zero))))),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f160281,f7739])).
% 18.34/15.02 fof(f160465,plain,(
% 18.34/15.02 ![X0]: (converse(X0)=join(composition(complement(sF5_fnc),sF2_fnc),converse(X0)))),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f1321,f160365])).
% 18.34/15.02 fof(f160480,plain,(
% 18.34/15.02 ![X0]: (composition(complement(sF5_fnc),sF2_fnc)=converse(meet(X0,zero)))),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f160465,f160372])).
% 18.34/15.02 fof(f160481,plain,(
% 18.34/15.02 composition(complement(sF5_fnc),sF2_fnc)=converse(zero)),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f2159,f160480])).
% 18.34/15.02 fof(f160497,plain,(
% 18.34/15.02 composition(complement(sF5_fnc),sF2_fnc)=zero),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f4269,f160481])).
% 18.34/15.02 fof(f160591,plain,(
% 18.34/15.02 composition(join(sK1_skl,complement(sF5_fnc)),sF2_fnc)=join(sF0_fnc,zero)),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f160497,f7089])).
% 18.34/15.02 fof(f160592,plain,(
% 18.34/15.02 composition(join(complement(sF5_fnc),sF4_fnc),sF2_fnc)=join(sF3_fnc,zero)),
% 18.34/15.02 inference(paramodulation,[status(thm)],[f160497,f122])).
% 18.34/15.02 fof(f160616,plain,(
% 18.34/15.02 composition(join(sK1_skl,complement(sF5_fnc)),sF2_fnc)=sF0_fnc),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f1321,f160591])).
% 18.34/15.02 fof(f160617,plain,(
% 18.34/15.02 composition(join(sF4_fnc,complement(sF5_fnc)),sF2_fnc)=join(sF3_fnc,zero)),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f2433,f160592])).
% 18.34/15.02 fof(f160618,plain,(
% 18.34/15.02 composition(join(sK1_skl,complement(sF5_fnc)),sF2_fnc)=join(sF3_fnc,zero)),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f30070,f160617])).
% 18.34/15.02 fof(f160619,plain,(
% 18.34/15.02 sF0_fnc=join(sF3_fnc,zero)),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f160616,f160618])).
% 18.34/15.02 fof(f160620,plain,(
% 18.34/15.02 sF0_fnc=sF3_fnc),
% 18.34/15.02 inference(forward_demodulation,[status(thm)],[f1321,f160619])).
% 18.34/15.02 fof(f160621,plain,(
% 18.34/15.02 $false),
% 18.34/15.02 inference(forward_subsumption_resolution,[status(thm)],[f160620,f49])).
% 18.34/15.02 % SZS output end CNFRefutation for theBenchmark.p
% 18.34/15.05 % Elapsed time: 14.561229 seconds
% 18.34/15.05 % CPU time: 114.662525 seconds
% 18.34/15.05 % Total memory used: 483.141 MB
% 18.34/15.05 % Net memory used: 472.603 MB
%------------------------------------------------------------------------------