%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL026+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:38 PM UTC 2026
% Result : Theorem 137.53s 38.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL026+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/20.67 % Computer : n010.cluster.edu
% 0.18/20.67 % Model : x86_64 x86_64
% 0.18/20.67 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/20.67 % Memory : 8046.5625MB
% 0.18/20.67 % OS : Linux 6.8.0-71-generic
% 0.18/20.68 % CPULimit : 300
% 0.18/20.68 % WCLimit : 300
% 0.18/20.68 % DateTime : Mon Sep 21 04:02:46 UTC 2026
% 0.18/20.68 % CPUTime :
% 0.18/20.69 % Drodi V4.1.1
% 137.53/38.15 % Refutation found
% 137.53/38.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 137.53/38.15 % SZS output start CNFRefutation for theBenchmark
% 137.53/38.15 fof(f1,axiom,(
% 137.53/38.15 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f2,axiom,(
% 137.53/38.15 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f3,axiom,(
% 137.53/38.15 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f4,axiom,(
% 137.53/38.15 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f5,axiom,(
% 137.53/38.15 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f6,axiom,(
% 137.53/38.15 (! [X0] : composition(X0,one) = X0 )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f7,axiom,(
% 137.53/38.15 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f8,axiom,(
% 137.53/38.15 (! [X0] : converse(converse(X0)) = X0 )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f9,axiom,(
% 137.53/38.15 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f10,axiom,(
% 137.53/38.15 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f11,axiom,(
% 137.53/38.15 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f12,axiom,(
% 137.53/38.15 (! [X0] : top = join(X0,complement(X0)) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f13,axiom,(
% 137.53/38.15 (! [X0] : zero = meet(X0,complement(X0)) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f15,axiom,(
% 137.53/38.15 (! [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) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f16,axiom,(
% 137.53/38.15 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f17,conjecture,(
% 137.53/38.15 (! [X0,X1] :( join(X0,one) = one=> meet(composition(X0,top),X1) = composition(X0,X1) ) )),
% 137.53/38.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 137.53/38.15 fof(f18,negated_conjecture,(
% 137.53/38.15 ~((! [X0,X1] :( join(X0,one) = one=> meet(composition(X0,top),X1) = composition(X0,X1) ) ))),
% 137.53/38.15 inference(negated_conjecture,[status(cth)],[f17])).
% 137.53/38.15 fof(f19,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f1])).
% 137.53/38.15 fof(f20,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f2])).
% 137.53/38.15 fof(f21,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f3])).
% 137.53/38.15 fof(f22,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f4])).
% 137.53/38.15 fof(f23,plain,(
% 137.53/38.15 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f5])).
% 137.53/38.15 fof(f24,plain,(
% 137.53/38.15 ![X0]: (composition(X0,one)=X0)),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f6])).
% 137.53/38.15 fof(f25,plain,(
% 137.53/38.15 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f7])).
% 137.53/38.15 fof(f26,plain,(
% 137.53/38.15 ![X0]: (converse(converse(X0))=X0)),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f8])).
% 137.53/38.15 fof(f27,plain,(
% 137.53/38.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f9])).
% 137.53/38.15 fof(f28,plain,(
% 137.53/38.15 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f10])).
% 137.53/38.15 fof(f29,plain,(
% 137.53/38.15 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f11])).
% 137.53/38.15 fof(f30,plain,(
% 137.53/38.15 ![X0]: (top=join(X0,complement(X0)))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f12])).
% 137.53/38.15 fof(f31,plain,(
% 137.53/38.15 ![X0]: (zero=meet(X0,complement(X0)))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f13])).
% 137.53/38.15 fof(f33,plain,(
% 137.53/38.15 ![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))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f15])).
% 137.53/38.15 fof(f34,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))=meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2))),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f16])).
% 137.53/38.15 fof(f35,plain,(
% 137.53/38.15 (?[X0,X1]: (join(X0,one)=one&~meet(composition(X0,top),X1)=composition(X0,X1)))),
% 137.53/38.15 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 137.53/38.15 fof(f36,plain,(
% 137.53/38.15 ?[X0]: (join(X0,one)=one&(?[X1]: ~meet(composition(X0,top),X1)=composition(X0,X1)))),
% 137.53/38.15 inference(miniscoping,[status(thm)],[f35])).
% 137.53/38.15 fof(f37,plain,(
% 137.53/38.15 (join(sK0_skl,one)=one&~meet(composition(sK0_skl,top),sK1_skl)=composition(sK0_skl,sK1_skl))),
% 137.53/38.15 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f36])).
% 137.53/38.15 fof(f38,plain,(
% 137.53/38.15 join(sK0_skl,one)=one),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f37])).
% 137.53/38.15 fof(f39,plain,(
% 137.53/38.15 ~meet(composition(sK0_skl,top),sK1_skl)=composition(sK0_skl,sK1_skl)),
% 137.53/38.15 inference(cnf_transformation,[status(thm)],[f37])).
% 137.53/38.15 fof(f40,definition,(
% 137.53/38.15 sF1_fnc=composition(sK0_skl,top)),
% 137.53/38.15 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 137.53/38.15 fof(f41,definition,(
% 137.53/38.15 sF0_fnc=meet(sF1_fnc,sK1_skl)),
% 137.53/38.15 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 137.53/38.15 fof(f42,definition,(
% 137.53/38.15 sF2_fnc=composition(sK0_skl,sK1_skl)),
% 137.53/38.15 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 137.53/38.15 fof(f43,plain,(
% 137.53/38.15 ~sF0_fnc=sF2_fnc),
% 137.53/38.15 inference(definition_folding,[],[f39,f42,f41,f40])).
% 137.53/38.15 fof(f44,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 137.53/38.15 fof(f45,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f22,f44])).
% 137.53/38.15 fof(f46,plain,(
% 137.53/38.15 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 137.53/38.15 fof(f47,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f45])).
% 137.53/38.15 fof(f55,plain,(
% 137.53/38.15 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f24,f23])).
% 137.53/38.15 fof(f69,plain,(
% 137.53/38.15 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f30,f47])).
% 137.53/38.15 fof(f70,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f19,f47])).
% 137.53/38.15 fof(f73,plain,(
% 137.53/38.15 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f69])).
% 137.53/38.15 fof(f75,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f19,f20])).
% 137.53/38.15 fof(f78,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f47,f20])).
% 137.53/38.15 fof(f80,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f30,f20])).
% 137.53/38.15 fof(f112,plain,(
% 137.53/38.15 ![X0,X1]: (converse(composition(X0,converse(X1)))=composition(X1,converse(X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f26,f28])).
% 137.53/38.15 fof(f113,plain,(
% 137.53/38.15 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f26,f28])).
% 137.53/38.15 fof(f117,plain,(
% 137.53/38.15 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f30,f22])).
% 137.53/38.15 fof(f118,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f19,f22])).
% 137.53/38.15 fof(f122,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f22,f47])).
% 137.53/38.15 fof(f126,plain,(
% 137.53/38.15 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f127,f73])).
% 137.53/38.15 fof(f127,plain,(
% 137.53/38.15 zero=complement(top)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f31,f117])).
% 137.53/38.15 fof(f128,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f122])).
% 137.53/38.15 fof(f134,plain,(
% 137.53/38.15 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f127,f22])).
% 137.53/38.15 fof(f135,plain,(
% 137.53/38.15 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f127,f22])).
% 137.53/38.15 fof(f139,plain,(
% 137.53/38.15 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f134])).
% 137.53/38.15 fof(f140,plain,(
% 137.53/38.15 top=join(zero,meet(top,complement(zero)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f127,f126])).
% 137.53/38.15 fof(f144,plain,(
% 137.53/38.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f19,f27])).
% 137.53/38.15 fof(f228,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0))=meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f40,f33])).
% 137.53/38.15 fof(f234,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one))=meet(composition(X0,meet(X1,composition(converse(X0),one))),one))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f24,f33])).
% 137.53/38.15 fof(f236,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(composition(converse(X0),meet(X1,composition(converse(converse(X0)),X2))),X2))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f26,f33])).
% 137.53/38.15 fof(f246,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one))=meet(composition(X0,meet(X1,converse(X0))),one))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f234])).
% 137.53/38.15 fof(f253,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f26,f236])).
% 137.53/38.15 fof(f331,plain,(
% 137.53/38.15 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f30,f80])).
% 137.53/38.15 fof(f338,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f80,f47])).
% 137.53/38.15 fof(f344,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f338])).
% 137.53/38.15 fof(f353,plain,(
% 137.53/38.15 ![X0,X1]: (converse(join(converse(X0),X1))=join(converse(X1),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f26,f144])).
% 137.53/38.15 fof(f358,plain,(
% 137.53/38.15 ![X0]: (meet(top,X0)=meet(X0,top))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f139,f135])).
% 137.53/38.15 fof(f370,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(complement(X0),meet(top,X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f135,f22])).
% 137.53/38.15 fof(f410,plain,(
% 137.53/38.15 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f358,f47])).
% 137.53/38.15 fof(f417,plain,(
% 137.53/38.15 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f410])).
% 137.53/38.15 fof(f443,plain,(
% 137.53/38.15 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f24,f113])).
% 137.53/38.15 fof(f463,plain,(
% 137.53/38.15 ![X0]: (X0=composition(converse(one),X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f26,f443])).
% 137.53/38.15 fof(f486,plain,(
% 137.53/38.15 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f55,f463])).
% 137.53/38.15 fof(f487,plain,(
% 137.53/38.15 one=converse(one)),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f24,f463])).
% 137.53/38.15 fof(f488,plain,(
% 137.53/38.15 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f463,f46])).
% 137.53/38.15 fof(f501,plain,(
% 137.53/38.15 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(composition(X0,X1),X1))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f463,f25])).
% 137.53/38.15 fof(f513,plain,(
% 137.53/38.15 ![X0]: (composition(one,X0)=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f463,f486])).
% 137.53/38.15 fof(f516,plain,(
% 137.53/38.15 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f513,f488])).
% 137.53/38.15 fof(f553,plain,(
% 137.53/38.15 ![X0,X1]: (composition(join(X0,one),X1)=join(composition(X0,X1),X1))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f487,f501])).
% 137.53/38.15 fof(f555,plain,(
% 137.53/38.15 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f553])).
% 137.53/38.15 fof(f648,plain,(
% 137.53/38.15 ![X0]: (join(meet(X0,top),complement(join(zero,complement(X0))))=complement(join(zero,complement(X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f139,f516])).
% 137.53/38.15 fof(f655,plain,(
% 137.53/38.15 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f516,f80])).
% 137.53/38.15 fof(f656,plain,(
% 137.53/38.15 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f516,f47])).
% 137.53/38.15 fof(f663,plain,(
% 137.53/38.15 ![X0]: (join(meet(X0,top),meet(top,X0))=complement(join(zero,complement(X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f135,f648])).
% 137.53/38.15 fof(f664,plain,(
% 137.53/38.15 ![X0]: (join(meet(X0,top),meet(top,X0))=meet(top,X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f135,f663])).
% 137.53/38.15 fof(f682,plain,(
% 137.53/38.15 ![X0]: (join(X0,top)=top)),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f684,f331])).
% 137.53/38.15 fof(f683,plain,(
% 137.53/38.15 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f684,f417])).
% 137.53/38.15 fof(f684,plain,(
% 137.53/38.15 ![X0]: (top=join(top,complement(X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f30,f655])).
% 137.53/38.15 fof(f685,plain,(
% 137.53/38.15 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f656])).
% 137.53/38.15 fof(f686,plain,(
% 137.53/38.15 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f31,f685])).
% 137.53/38.15 fof(f687,plain,(
% 137.53/38.15 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f686])).
% 137.53/38.15 fof(f689,plain,(
% 137.53/38.15 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f683])).
% 137.53/38.15 fof(f690,plain,(
% 137.53/38.15 top=complement(zero)),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f692,f140])).
% 137.53/38.15 fof(f692,plain,(
% 137.53/38.15 ![X0]: (X0=join(zero,meet(top,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f127,f689])).
% 137.53/38.15 fof(f714,plain,(
% 137.53/38.15 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))=join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f34,f20])).
% 137.53/38.15 fof(f752,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f22,f70])).
% 137.53/38.15 fof(f775,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f752])).
% 137.53/38.15 fof(f930,plain,(
% 137.53/38.15 ![X0]: (meet(X0,zero)=complement(join(complement(X0),top)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f690,f22])).
% 137.53/38.15 fof(f952,plain,(
% 137.53/38.15 ![X0]: (meet(X0,zero)=complement(join(top,complement(X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f930])).
% 137.53/38.15 fof(f953,plain,(
% 137.53/38.15 ![X0]: (meet(X0,zero)=complement(top))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f684,f952])).
% 137.53/38.15 fof(f961,plain,(
% 137.53/38.15 ![X0]: (meet(X0,zero)=zero)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f127,f953])).
% 137.53/38.15 fof(f1050,plain,(
% 137.53/38.15 ![X0,X1]: (join(top,X0)=join(X0,join(X1,complement(X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f80,f75])).
% 137.53/38.15 fof(f1148,plain,(
% 137.53/38.15 ![X0]: (join(top,X0)=join(X0,top))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f30,f1050])).
% 137.53/38.15 fof(f1165,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1170,f344])).
% 137.53/38.15 fof(f1170,plain,(
% 137.53/38.15 ![X0]: (join(top,X0)=top)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f682,f1148])).
% 137.53/38.15 fof(f1241,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f127,f1165])).
% 137.53/38.15 fof(f1250,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),X1)))=join(X0,complement(join(complement(X0),X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f516,f78])).
% 137.53/38.15 fof(f1294,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(X0,complement(join(complement(X0),X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f47,f1250])).
% 137.53/38.15 fof(f1334,plain,(
% 137.53/38.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f22,f687])).
% 137.53/38.15 fof(f1337,plain,(
% 137.53/38.15 ![X0]: (complement(X0)=join(meet(complement(X0),zero),complement(X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f687,f70])).
% 137.53/38.15 fof(f1346,plain,(
% 137.53/38.15 ![X0]: (complement(X0)=join(complement(X0),meet(complement(X0),zero)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f1337])).
% 137.53/38.15 fof(f1347,plain,(
% 137.53/38.15 ![X0]: (complement(X0)=join(complement(X0),zero))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f961,f1346])).
% 137.53/38.15 fof(f1348,plain,(
% 137.53/38.15 ![X0]: (X0=complement(complement(X0)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1373,f687])).
% 137.53/38.15 fof(f1349,plain,(
% 137.53/38.15 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1373,f135])).
% 137.53/38.15 fof(f1350,plain,(
% 137.53/38.15 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1373,f139])).
% 137.53/38.15 fof(f1351,plain,(
% 137.53/38.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1373,f1334])).
% 137.53/38.15 fof(f1362,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),meet(top,X1))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1373,f370])).
% 137.53/38.15 fof(f1373,plain,(
% 137.53/38.15 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f1347])).
% 137.53/38.15 fof(f1387,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(zero,meet(X0,join(X0,X1))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1348,f1241])).
% 137.53/38.15 fof(f1400,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(composition(sK0_skl,meet(top,composition(converse(sK0_skl),X0))),X0))=meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1412,f228])).
% 137.53/38.15 fof(f1409,plain,(
% 137.53/38.15 ![X0]: (X0=join(zero,X0))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1412,f692])).
% 137.53/38.15 fof(f1410,plain,(
% 137.53/38.15 ![X0]: (join(meet(X0,top),meet(top,X0))=X0)),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1412,f664])).
% 137.53/38.15 fof(f1412,plain,(
% 137.53/38.15 ![X0]: (meet(top,X0)=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1348,f1349])).
% 137.53/38.15 fof(f1421,plain,(
% 137.53/38.15 ![X0]: (meet(X0,top)=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1348,f1350])).
% 137.53/38.15 fof(f1429,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1351,f118])).
% 137.53/38.15 fof(f1468,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(X0,meet(X0,complement(X1))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1471,f1294])).
% 137.53/38.15 fof(f1471,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f1362])).
% 137.53/38.15 fof(f1519,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0))=meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f1400])).
% 137.53/38.15 fof(f1535,plain,(
% 137.53/38.15 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1409,f1387])).
% 137.53/38.15 fof(f1540,plain,(
% 137.53/38.15 ![X0]: (join(X0,meet(top,X0))=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1421,f1410])).
% 137.53/38.15 fof(f1543,plain,(
% 137.53/38.15 ![X0]: (join(X0,X0)=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f1540])).
% 137.53/38.15 fof(f1555,plain,(
% 137.53/38.15 sF0_fnc=meet(sK1_skl,sF1_fnc)),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1595,f41])).
% 137.53/38.15 fof(f1573,plain,(
% 137.53/38.15 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1595,f714])).
% 137.53/38.15 fof(f1580,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(composition(sK0_skl,composition(converse(sK0_skl),X0)),X0))=meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1595,f1519])).
% 137.53/38.15 fof(f1586,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(composition(converse(X0),meet(X1,composition(X0,X2))),X2))=meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1595,f253])).
% 137.53/38.15 fof(f1589,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(composition(X0,X1),one),meet(composition(X0,meet(X1,converse(X0))),one))=meet(one,composition(X0,meet(X1,converse(X0)))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f1595,f246])).
% 137.53/38.15 fof(f1595,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1348,f1429])).
% 137.53/38.15 fof(f1643,plain,(
% 137.53/38.15 ![X0,X1,X2,X3]: (join(meet(composition(X0,X1),X2),join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))=join(meet(X2,composition(meet(X0,composition(X2,converse(X1))),X1)),X3))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f1573])).
% 137.53/38.15 fof(f1650,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))))=meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f1580])).
% 137.53/38.15 fof(f1656,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(composition(converse(X0),X1),X2),meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))=meet(X2,composition(converse(X0),meet(X1,composition(X0,X2)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f1586])).
% 137.53/38.15 fof(f1659,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(one,composition(X0,X1)),meet(composition(X0,meet(X1,converse(X0))),one))=meet(one,composition(X0,meet(X1,converse(X0)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f1589])).
% 137.53/38.15 fof(f1660,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(one,composition(X0,X1)),meet(one,composition(X0,meet(X1,converse(X0)))))=meet(one,composition(X0,meet(X1,converse(X0)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f1659])).
% 137.53/38.15 fof(f1783,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1348,f1468])).
% 137.53/38.15 fof(f1817,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,join(meet(X0,X1),X2))=join(X2,X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1783,f75])).
% 137.53/38.15 fof(f1820,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,join(meet(X0,X1),X2))=join(X0,X2))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1783,f20])).
% 137.53/38.15 fof(f2121,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1543,f75])).
% 137.53/38.15 fof(f2142,plain,(
% 137.53/38.15 ![X0,X1]: (converse(X0)=meet(converse(X0),converse(join(X0,X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f27,f1535])).
% 137.53/38.15 fof(f2149,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f128,f1535])).
% 137.53/38.15 fof(f2159,plain,(
% 137.53/38.15 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f19,f1535])).
% 137.53/38.15 fof(f2170,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f2149])).
% 137.53/38.15 fof(f2701,plain,(
% 137.53/38.15 ![X0,X1]: (join(meet(X0,X1),X1)=join(meet(X1,complement(X0)),meet(X0,X1)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f775,f2121])).
% 137.53/38.15 fof(f2703,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f775,f1535])).
% 137.53/38.15 fof(f2731,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f2701])).
% 137.53/38.15 fof(f2732,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,meet(X1,X0))=join(meet(X1,X0),meet(X0,complement(X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f2731])).
% 137.53/38.15 fof(f2734,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f775,f2732])).
% 137.53/38.15 fof(f2736,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f2703])).
% 137.53/38.15 fof(f2833,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),X2))=join(X0,X2))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f2734,f20])).
% 137.53/38.15 fof(f6122,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1595,f2736])).
% 137.53/38.15 fof(f6124,plain,(
% 137.53/38.15 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1595,f2170])).
% 137.53/38.15 fof(f7067,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(X0,meet(X0,X1))=join(meet(X2,meet(X0,X1)),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f2734,f1817])).
% 137.53/38.15 fof(f7156,plain,(
% 137.53/38.15 ![X0,X1,X2]: (X0=join(meet(X1,meet(X0,X2)),X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1783,f7067])).
% 137.53/38.15 fof(f7157,plain,(
% 137.53/38.15 ![X0,X1,X2]: (X0=join(X0,meet(X1,meet(X0,X2))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f7156])).
% 137.53/38.15 fof(f7260,plain,(
% 137.53/38.15 ![X0,X1,X2]: (X0=join(X0,meet(X1,meet(X2,X0))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f6122,f7157])).
% 137.53/38.15 fof(f7342,plain,(
% 137.53/38.15 ![X0,X1,X2]: (X0=join(X0,meet(meet(X1,X0),X2)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f1595,f7260])).
% 137.53/38.15 fof(f9158,plain,(
% 137.53/38.15 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X0,X1),meet(meet(X1,X0),X2)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f6124,f7342])).
% 137.53/38.15 fof(f9679,plain,(
% 137.53/38.15 converse(sK0_skl)=meet(converse(sK0_skl),converse(one))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f38,f2142])).
% 137.53/38.15 fof(f9770,plain,(
% 137.53/38.15 converse(sK0_skl)=meet(converse(sK0_skl),one)),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f487,f9679])).
% 137.53/38.15 fof(f9771,plain,(
% 137.53/38.15 converse(sK0_skl)=meet(one,converse(sK0_skl))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f9770])).
% 137.53/38.15 fof(f18770,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f24,f1643])).
% 137.53/38.15 fof(f18923,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f18770])).
% 137.53/38.15 fof(f18924,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,composition(X1,one))),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f487,f18923])).
% 137.53/38.15 fof(f18925,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X2))=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f18924])).
% 137.53/38.15 fof(f18926,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,composition(meet(X0,composition(X1,converse(one))),one)),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f2833,f18925])).
% 137.53/38.15 fof(f18927,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,converse(one)))),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f18926])).
% 137.53/38.15 fof(f18928,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,composition(X1,one))),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f487,f18927])).
% 137.53/38.15 fof(f18929,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,meet(X0,X1)),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f18928])).
% 137.53/38.15 fof(f18930,plain,(
% 137.53/38.15 ![X0,X1,X2]: (join(meet(X0,X1),X2)=join(meet(X1,X0),X2))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f6124,f18929])).
% 137.53/38.15 fof(f19473,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f6124,f1650])).
% 137.53/38.15 fof(f19475,plain,(
% 137.53/38.15 ![X0]: (join(meet(X0,sF1_fnc),meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f2736,f1650])).
% 137.53/38.15 fof(f19523,plain,(
% 137.53/38.15 ![X0]: (meet(sF1_fnc,X0)=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f9158,f19473])).
% 137.53/38.15 fof(f19525,plain,(
% 137.53/38.15 ![X0]: (meet(X0,sF1_fnc)=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(converse(sK0_skl),meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1783,f19475])).
% 137.53/38.15 fof(f25121,plain,(
% 137.53/38.15 ![X0]: (join(meet(composition(converse(sK0_skl),X0),top),meet(top,composition(converse(sK0_skl),meet(X0,sF1_fnc))))=meet(top,composition(converse(sK0_skl),meet(X0,composition(sK0_skl,top)))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f40,f1656])).
% 137.53/38.15 fof(f25372,plain,(
% 137.53/38.15 ![X0]: (join(meet(top,composition(converse(sK0_skl),X0)),meet(top,composition(converse(sK0_skl),meet(X0,sF1_fnc))))=meet(top,composition(converse(sK0_skl),meet(X0,composition(sK0_skl,top)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f18930,f25121])).
% 137.53/38.15 fof(f25373,plain,(
% 137.53/38.15 ![X0]: (join(composition(converse(sK0_skl),X0),meet(top,composition(converse(sK0_skl),meet(X0,sF1_fnc))))=meet(top,composition(converse(sK0_skl),meet(X0,composition(sK0_skl,top)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f25372])).
% 137.53/38.15 fof(f25374,plain,(
% 137.53/38.15 ![X0]: (join(composition(converse(sK0_skl),X0),composition(converse(sK0_skl),meet(X0,sF1_fnc)))=meet(top,composition(converse(sK0_skl),meet(X0,composition(sK0_skl,top)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f25373])).
% 137.53/38.15 fof(f25375,plain,(
% 137.53/38.15 ![X0]: (join(composition(converse(sK0_skl),X0),composition(converse(sK0_skl),meet(X0,sF1_fnc)))=composition(converse(sK0_skl),meet(X0,composition(sK0_skl,top))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1412,f25374])).
% 137.53/38.15 fof(f25376,plain,(
% 137.53/38.15 ![X0]: (join(composition(converse(sK0_skl),X0),composition(converse(sK0_skl),meet(X0,sF1_fnc)))=composition(converse(sK0_skl),meet(X0,sF1_fnc)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f40,f25375])).
% 137.53/38.15 fof(f37898,plain,(
% 137.53/38.15 ![X0]: (composition(one,X0)=join(X0,composition(sK0_skl,X0)))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f38,f555])).
% 137.53/38.15 fof(f38058,plain,(
% 137.53/38.15 ![X0]: (X0=join(X0,composition(sK0_skl,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f513,f37898])).
% 137.53/38.15 fof(f39329,plain,(
% 137.53/38.15 ![X0]: (converse(converse(X0))=join(converse(composition(sK0_skl,converse(X0))),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f38058,f353])).
% 137.53/38.15 fof(f39346,plain,(
% 137.53/38.15 ![X0,X1]: (join(X0,meet(X0,X1))=join(X0,composition(sK0_skl,meet(X0,X1))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f38058,f1820])).
% 137.53/38.15 fof(f39384,plain,(
% 137.53/38.15 ![X0]: (composition(sK0_skl,X0)=meet(composition(sK0_skl,X0),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f38058,f2159])).
% 137.53/38.15 fof(f39421,plain,(
% 137.53/38.15 ![X0]: (X0=join(converse(composition(sK0_skl,converse(X0))),X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f26,f39329])).
% 137.53/38.15 fof(f39422,plain,(
% 137.53/38.15 ![X0]: (X0=join(X0,converse(composition(sK0_skl,converse(X0)))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f19,f39421])).
% 137.53/38.15 fof(f39423,plain,(
% 137.53/38.15 ![X0]: (X0=join(X0,composition(X0,converse(sK0_skl))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f112,f39422])).
% 137.53/38.15 fof(f39461,plain,(
% 137.53/38.15 ![X0,X1]: (X0=join(X0,composition(sK0_skl,meet(X0,X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1783,f39346])).
% 137.53/38.15 fof(f39495,plain,(
% 137.53/38.15 ![X0]: (composition(sK0_skl,X0)=meet(X0,composition(sK0_skl,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f39384])).
% 137.53/38.15 fof(f43382,plain,(
% 137.53/38.15 ![X0,X1]: (composition(sK0_skl,meet(X0,X1))=meet(composition(sK0_skl,meet(X0,X1)),X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f39461,f2159])).
% 137.53/38.15 fof(f43485,plain,(
% 137.53/38.15 ![X0,X1]: (composition(sK0_skl,meet(X0,X1))=meet(X0,composition(sK0_skl,meet(X0,X1))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f1595,f43382])).
% 137.53/38.15 fof(f44350,plain,(
% 137.53/38.15 join(composition(sK0_skl,one),meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))))=meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f39495,f1660])).
% 137.53/38.15 fof(f44479,plain,(
% 137.53/38.15 join(sK0_skl,meet(one,composition(sK0_skl,meet(one,converse(sK0_skl)))))=meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f24,f44350])).
% 137.53/38.15 fof(f44480,plain,(
% 137.53/38.15 join(sK0_skl,composition(sK0_skl,meet(one,converse(sK0_skl))))=meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f43485,f44479])).
% 137.53/38.15 fof(f44481,plain,(
% 137.53/38.15 join(sK0_skl,composition(sK0_skl,converse(sK0_skl)))=meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f9771,f44480])).
% 137.53/38.15 fof(f44482,plain,(
% 137.53/38.15 sK0_skl=meet(one,composition(sK0_skl,meet(one,converse(sK0_skl))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f39423,f44481])).
% 137.53/38.15 fof(f44483,plain,(
% 137.53/38.15 sK0_skl=composition(sK0_skl,meet(one,converse(sK0_skl)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f43485,f44482])).
% 137.53/38.15 fof(f44490,plain,(
% 137.53/38.15 sK0_skl=composition(sK0_skl,converse(sK0_skl))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f9771,f44483])).
% 137.53/38.15 fof(f44786,plain,(
% 137.53/38.15 converse(sK0_skl)=composition(sK0_skl,converse(sK0_skl))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f44490,f112])).
% 137.53/38.15 fof(f44841,plain,(
% 137.53/38.15 ![X0]: (composition(sK0_skl,composition(converse(sK0_skl),X0))=composition(sK0_skl,X0))),
% 137.53/38.15 inference(paramodulation,[status(thm)],[f44490,f23])).
% 137.53/38.15 fof(f44919,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(converse(sK0_skl),X0))))=meet(X0,composition(sK0_skl,composition(sK0_skl,X0))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f45327,f1650])).
% 137.53/38.15 fof(f45113,plain,(
% 137.53/38.15 ![X0]: (join(composition(converse(sK0_skl),X0),composition(converse(sK0_skl),meet(X0,sF1_fnc)))=composition(sK0_skl,meet(X0,sF1_fnc)))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f45327,f25376])).
% 137.53/38.15 fof(f45172,plain,(
% 137.53/38.15 ![X0]: (meet(X0,sF1_fnc)=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(sK0_skl,meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f45327,f19525])).
% 137.53/38.15 fof(f45174,plain,(
% 137.53/38.15 ![X0]: (meet(sF1_fnc,X0)=meet(meet(X0,sF1_fnc),composition(sK0_skl,composition(sK0_skl,meet(X0,sF1_fnc)))))),
% 137.53/38.15 inference(backward_demodulation,[status(thm)],[f45327,f19523])).
% 137.53/38.15 fof(f45327,plain,(
% 137.53/38.15 converse(sK0_skl)=sK0_skl),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f44490,f44786])).
% 137.53/38.15 fof(f45636,plain,(
% 137.53/38.15 ![X0]: (composition(sK0_skl,composition(sK0_skl,X0))=composition(sK0_skl,X0))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f45327,f44841])).
% 137.53/38.15 fof(f45709,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,composition(sK0_skl,X0))))=meet(X0,composition(sK0_skl,composition(sK0_skl,X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f45327,f44919])).
% 137.53/38.15 fof(f45710,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),meet(X0,composition(sK0_skl,X0)))=meet(X0,composition(sK0_skl,composition(sK0_skl,X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f45636,f45709])).
% 137.53/38.15 fof(f45711,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),composition(sK0_skl,X0))=meet(X0,composition(sK0_skl,composition(sK0_skl,X0))))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f39495,f45710])).
% 137.53/38.15 fof(f45712,plain,(
% 137.53/38.15 ![X0]: (join(meet(sF1_fnc,X0),composition(sK0_skl,X0))=meet(X0,composition(sK0_skl,X0)))),
% 137.53/38.15 inference(forward_demodulation,[status(thm)],[f45636,f45711])).
% 100.55/38.37 fof(f45713,plain,(
% 100.55/38.37 ![X0]: (join(meet(sF1_fnc,X0),composition(sK0_skl,X0))=composition(sK0_skl,X0))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f39495,f45712])).
% 100.55/38.37 fof(f46004,plain,(
% 100.55/38.37 ![X0]: (join(composition(sK0_skl,X0),composition(converse(sK0_skl),meet(X0,sF1_fnc)))=composition(sK0_skl,meet(X0,sF1_fnc)))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f45327,f45113])).
% 100.55/38.37 fof(f46005,plain,(
% 100.55/38.37 ![X0]: (join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc)))=composition(sK0_skl,meet(X0,sF1_fnc)))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f45327,f46004])).
% 100.55/38.37 fof(f46116,plain,(
% 100.55/38.37 ![X0]: (meet(X0,sF1_fnc)=meet(meet(X0,sF1_fnc),composition(sK0_skl,meet(X0,sF1_fnc))))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f45636,f45172])).
% 100.55/38.37 fof(f46117,plain,(
% 100.55/38.37 ![X0]: (join(composition(sK0_skl,X0),composition(sK0_skl,meet(X0,sF1_fnc)))=meet(X0,sF1_fnc))),
% 100.55/38.37 inference(backward_demodulation,[status(thm)],[f46120,f46005])).
% 100.55/38.37 fof(f46120,plain,(
% 100.55/38.37 ![X0]: (meet(X0,sF1_fnc)=composition(sK0_skl,meet(X0,sF1_fnc)))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f39495,f46116])).
% 100.55/38.37 fof(f46123,plain,(
% 100.55/38.37 ![X0]: (meet(sF1_fnc,X0)=meet(meet(X0,sF1_fnc),composition(sK0_skl,meet(X0,sF1_fnc))))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f45636,f45174])).
% 100.55/38.37 fof(f46124,plain,(
% 100.55/38.37 ![X0]: (meet(sF1_fnc,X0)=composition(sK0_skl,meet(X0,sF1_fnc)))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f39495,f46123])).
% 100.55/38.37 fof(f46329,plain,(
% 100.55/38.37 ![X0]: (join(composition(sK0_skl,X0),meet(sF1_fnc,X0))=meet(X0,sF1_fnc))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f46124,f46117])).
% 100.55/38.37 fof(f46330,plain,(
% 100.55/38.37 ![X0]: (meet(X0,sF1_fnc)=composition(sK0_skl,X0))),
% 100.55/38.37 inference(backward_demodulation,[status(thm)],[f46331,f45713])).
% 100.55/38.37 fof(f46331,plain,(
% 100.55/38.37 ![X0]: (join(meet(sF1_fnc,X0),composition(sK0_skl,X0))=meet(X0,sF1_fnc))),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f19,f46329])).
% 100.55/38.37 fof(f46342,plain,(
% 100.55/38.37 sF2_fnc=meet(sK1_skl,sF1_fnc)),
% 100.55/38.37 inference(backward_demodulation,[status(thm)],[f46330,f42])).
% 100.55/38.37 fof(f46768,plain,(
% 100.55/38.37 sF2_fnc=sF0_fnc),
% 100.55/38.37 inference(forward_demodulation,[status(thm)],[f1555,f46342])).
% 100.55/38.37 fof(f46769,plain,(
% 100.55/38.37 $false),
% 100.55/38.37 inference(forward_subsumption_resolution,[status(thm)],[f46768,f43])).
% 100.55/38.37 % SZS output end CNFRefutation for theBenchmark.p
% 14.36/38.43 % Elapsed time: 17.732917 seconds
% 14.36/38.43 % CPU time: 139.518848 seconds
% 14.36/38.43 % Total memory used: 950.231 MB
% 14.36/38.43 % Net memory used: 933.397 MB
%------------------------------------------------------------------------------