%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL018+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:36 PM UTC 2026
% Result : Theorem 19.70s 8.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL018+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.60 % Computer : n013.cluster.edu
% 0.12/5.60 % Model : x86_64 x86_64
% 0.12/5.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.60 % Memory : 8046.5625MB
% 0.12/5.60 % OS : Linux 6.8.0-71-generic
% 0.12/5.60 % CPULimit : 300
% 0.12/5.60 % WCLimit : 300
% 0.12/5.60 % DateTime : Mon Sep 21 03:59:42 UTC 2026
% 0.12/5.60 % CPUTime :
% 0.12/5.61 % Drodi V4.1.1
% 19.70/8.15 % Refutation found
% 19.70/8.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.70/8.15 % SZS output start CNFRefutation for theBenchmark
% 19.70/8.15 fof(f1,axiom,(
% 19.70/8.15 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f2,axiom,(
% 19.70/8.15 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f3,axiom,(
% 19.70/8.15 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f4,axiom,(
% 19.70/8.15 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f5,axiom,(
% 19.70/8.15 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f6,axiom,(
% 19.70/8.15 (! [X0] : composition(X0,one) = X0 )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f7,axiom,(
% 19.70/8.15 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f8,axiom,(
% 19.70/8.15 (! [X0] : converse(converse(X0)) = X0 )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f9,axiom,(
% 19.70/8.15 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f10,axiom,(
% 19.70/8.15 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f11,axiom,(
% 19.70/8.15 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f12,axiom,(
% 19.70/8.15 (! [X0] : top = join(X0,complement(X0)) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f13,axiom,(
% 19.70/8.15 (! [X0] : zero = meet(X0,complement(X0)) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f14,conjecture,(
% 19.70/8.15 (! [X0] :( composition(X0,top) = X0=> composition(complement(X0),top) = complement(X0) ) )),
% 19.70/8.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.70/8.15 fof(f15,negated_conjecture,(
% 19.70/8.15 ~((! [X0] :( composition(X0,top) = X0=> composition(complement(X0),top) = complement(X0) ) ))),
% 19.70/8.15 inference(negated_conjecture,[status(cth)],[f14])).
% 19.70/8.15 fof(f16,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f1])).
% 19.70/8.15 fof(f17,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f2])).
% 19.70/8.15 fof(f18,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f3])).
% 19.70/8.15 fof(f19,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f4])).
% 19.70/8.15 fof(f20,plain,(
% 19.70/8.15 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f5])).
% 19.70/8.15 fof(f21,plain,(
% 19.70/8.15 ![X0]: (composition(X0,one)=X0)),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f6])).
% 19.70/8.15 fof(f22,plain,(
% 19.70/8.15 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f7])).
% 19.70/8.15 fof(f23,plain,(
% 19.70/8.15 ![X0]: (converse(converse(X0))=X0)),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f8])).
% 19.70/8.15 fof(f24,plain,(
% 19.70/8.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f9])).
% 19.70/8.15 fof(f25,plain,(
% 19.70/8.15 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f10])).
% 19.70/8.15 fof(f26,plain,(
% 19.70/8.15 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f11])).
% 19.70/8.15 fof(f27,plain,(
% 19.70/8.15 ![X0]: (top=join(X0,complement(X0)))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f12])).
% 19.70/8.15 fof(f28,plain,(
% 19.70/8.15 ![X0]: (zero=meet(X0,complement(X0)))),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f13])).
% 19.70/8.15 fof(f29,plain,(
% 19.70/8.15 (?[X0]: (composition(X0,top)=X0&~composition(complement(X0),top)=complement(X0)))),
% 19.70/8.15 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 19.70/8.15 fof(f30,plain,(
% 19.70/8.15 (composition(sK0_skl,top)=sK0_skl&~composition(complement(sK0_skl),top)=complement(sK0_skl))),
% 19.70/8.15 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f29])).
% 19.70/8.15 fof(f31,plain,(
% 19.70/8.15 composition(sK0_skl,top)=sK0_skl),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f30])).
% 19.70/8.15 fof(f32,plain,(
% 19.70/8.15 ~composition(complement(sK0_skl),top)=complement(sK0_skl)),
% 19.70/8.15 inference(cnf_transformation,[status(thm)],[f30])).
% 19.70/8.15 fof(f33,definition,(
% 19.70/8.15 sF1_fnc=complement(sK0_skl)),
% 19.70/8.15 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 19.70/8.15 fof(f34,definition,(
% 19.70/8.15 sF0_fnc=composition(sF1_fnc,top)),
% 19.70/8.15 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 19.70/8.15 fof(f35,plain,(
% 19.70/8.15 ~sF0_fnc=sF1_fnc),
% 19.70/8.15 inference(definition_folding,[],[f32,f34,f33])).
% 19.70/8.15 fof(f36,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 19.70/8.15 fof(f37,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f19,f36])).
% 19.70/8.15 fof(f38,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 19.70/8.15 fof(f39,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f37])).
% 19.70/8.15 fof(f40,plain,(
% 19.70/8.15 top=join(sK0_skl,sF1_fnc)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f33,f27])).
% 19.70/8.15 fof(f52,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f27,f39])).
% 19.70/8.15 fof(f54,plain,(
% 19.70/8.15 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f52])).
% 19.70/8.15 fof(f55,plain,(
% 19.70/8.15 sK0_skl=join(complement(top),meet(sK0_skl,complement(sF1_fnc)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f33,f54])).
% 19.70/8.15 fof(f67,plain,(
% 19.70/8.15 ![X0]: (composition(join(sK0_skl,X0),top)=join(sK0_skl,composition(X0,top)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f31,f22])).
% 19.70/8.15 fof(f144,plain,(
% 19.70/8.15 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f21,f20])).
% 19.70/8.15 fof(f161,plain,(
% 19.70/8.15 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f22,f16])).
% 19.70/8.15 fof(f172,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f39])).
% 19.70/8.15 fof(f208,plain,(
% 19.70/8.15 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f24])).
% 19.70/8.15 fof(f215,plain,(
% 19.70/8.15 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f23,f25])).
% 19.70/8.15 fof(f224,plain,(
% 19.70/8.15 ![X0,X1]: (converse(join(X0,converse(X1)))=join(X1,converse(X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f23,f208])).
% 19.70/8.15 fof(f229,plain,(
% 19.70/8.15 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f27,f19])).
% 19.70/8.15 fof(f230,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f19])).
% 19.70/8.15 fof(f232,plain,(
% 19.70/8.15 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f19,f19])).
% 19.70/8.15 fof(f236,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f19,f39])).
% 19.70/8.15 fof(f241,plain,(
% 19.70/8.15 sK0_skl=join(zero,meet(sK0_skl,complement(sF1_fnc)))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f244,f55])).
% 19.70/8.15 fof(f242,plain,(
% 19.70/8.15 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f244,f54])).
% 19.70/8.15 fof(f244,plain,(
% 19.70/8.15 zero=complement(top)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f28,f229])).
% 19.70/8.15 fof(f246,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f236])).
% 19.70/8.15 fof(f254,plain,(
% 19.70/8.15 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f244,f19])).
% 19.70/8.15 fof(f255,plain,(
% 19.70/8.15 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f244,f19])).
% 19.70/8.15 fof(f259,plain,(
% 19.70/8.15 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f254])).
% 19.70/8.15 fof(f263,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f27,f17])).
% 19.70/8.15 fof(f264,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f17])).
% 19.70/8.15 fof(f278,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f27,f17])).
% 19.70/8.15 fof(f279,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f17])).
% 19.70/8.15 fof(f303,plain,(
% 19.70/8.15 ![X0]: (join(sF1_fnc,composition(converse(X0),complement(composition(X0,sK0_skl))))=complement(sK0_skl))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f33,f38])).
% 19.70/8.15 fof(f312,plain,(
% 19.70/8.15 join(complement(top),composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f31,f38])).
% 19.70/8.15 fof(f319,plain,(
% 19.70/8.15 ![X0]: (join(sF1_fnc,composition(converse(X0),complement(composition(X0,sK0_skl))))=sF1_fnc)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f33,f303])).
% 19.70/8.15 fof(f327,plain,(
% 19.70/8.15 join(zero,composition(converse(sK0_skl),complement(sK0_skl)))=complement(top)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f312])).
% 19.70/8.15 fof(f328,plain,(
% 19.70/8.15 join(zero,composition(converse(sK0_skl),sF1_fnc))=complement(top)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f33,f327])).
% 19.70/8.15 fof(f329,plain,(
% 19.70/8.15 join(zero,composition(converse(sK0_skl),sF1_fnc))=zero),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f328])).
% 19.70/8.15 fof(f332,plain,(
% 19.70/8.15 composition(top,top)=join(sK0_skl,composition(sF1_fnc,top))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f40,f67])).
% 19.70/8.15 fof(f345,plain,(
% 19.70/8.15 composition(top,top)=join(sK0_skl,sF0_fnc)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f34,f332])).
% 19.70/8.15 fof(f360,plain,(
% 19.70/8.15 join(complement(top),composition(converse(top),complement(join(sK0_skl,sF0_fnc))))=complement(top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f345,f38])).
% 19.70/8.15 fof(f367,plain,(
% 19.70/8.15 join(zero,composition(converse(top),complement(join(sK0_skl,sF0_fnc))))=complement(top)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f360])).
% 19.70/8.15 fof(f368,plain,(
% 19.70/8.15 join(zero,composition(converse(top),complement(join(sK0_skl,sF0_fnc))))=zero),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f367])).
% 19.70/8.15 fof(f439,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,top),meet(X0,zero)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f244,f246])).
% 19.70/8.15 fof(f441,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,sK0_skl),meet(X0,sF1_fnc)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f33,f246])).
% 19.70/8.15 fof(f791,plain,(
% 19.70/8.15 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f21,f215])).
% 19.70/8.15 fof(f810,plain,(
% 19.70/8.15 ![X0]: (X0=composition(converse(one),X0))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f23,f791])).
% 19.70/8.15 fof(f822,plain,(
% 19.70/8.15 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f144,f810])).
% 19.70/8.15 fof(f824,plain,(
% 19.70/8.15 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f810,f38])).
% 19.70/8.15 fof(f845,plain,(
% 19.70/8.15 ![X0]: (composition(one,X0)=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f810,f822])).
% 19.70/8.15 fof(f847,plain,(
% 19.70/8.15 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f845,f824])).
% 19.70/8.15 fof(f921,plain,(
% 19.70/8.15 ![X0]: (join(meet(X0,top),complement(join(zero,complement(X0))))=complement(join(zero,complement(X0))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f259,f847])).
% 19.70/8.15 fof(f923,plain,(
% 19.70/8.15 ![X0,X1]: (join(meet(X0,X1),complement(join(complement(X0),complement(X1))))=complement(join(complement(X0),complement(X1))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f19,f847])).
% 19.70/8.15 fof(f931,plain,(
% 19.70/8.15 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f847,f19])).
% 19.70/8.15 fof(f932,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f847,f39])).
% 19.70/8.15 fof(f939,plain,(
% 19.70/8.15 ![X0]: (join(meet(X0,top),meet(top,X0))=complement(join(zero,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f255,f921])).
% 19.70/8.15 fof(f940,plain,(
% 19.70/8.15 ![X0]: (join(meet(X0,top),meet(top,X0))=meet(top,X0))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f255,f939])).
% 19.70/8.15 fof(f943,plain,(
% 19.70/8.15 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f19,f923])).
% 19.70/8.15 fof(f946,plain,(
% 19.70/8.15 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=meet(X0,X1))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f19,f943])).
% 19.70/8.15 fof(f972,plain,(
% 19.70/8.15 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f932])).
% 19.70/8.15 fof(f973,plain,(
% 19.70/8.15 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f28,f972])).
% 19.70/8.15 fof(f974,plain,(
% 19.70/8.15 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f973])).
% 19.70/8.15 fof(f1055,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f19,f172])).
% 19.70/8.15 fof(f1084,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f1055])).
% 19.70/8.15 fof(f1327,plain,(
% 19.70/8.15 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f974,f255])).
% 19.70/8.15 fof(f1353,plain,(
% 19.70/8.15 ![X0]: (top=join(meet(top,X0),complement(X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1327,f246])).
% 19.70/8.15 fof(f1355,plain,(
% 19.70/8.15 ![X0]: (top=join(complement(X0),complement(join(complement(X0),complement(top)))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1327,f172])).
% 19.70/8.15 fof(f1377,plain,(
% 19.70/8.15 ![X0]: (top=join(complement(X0),meet(top,X0)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f1353])).
% 19.70/8.15 fof(f1379,plain,(
% 19.70/8.15 ![X0]: (top=join(complement(X0),meet(X0,top)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f19,f1355])).
% 19.70/8.15 fof(f1444,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,meet(X0,top)),complement(top)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1379,f39])).
% 19.70/8.15 fof(f1458,plain,(
% 19.70/8.15 ![X0]: (X0=join(complement(top),meet(X0,meet(X0,top))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f1444])).
% 19.70/8.15 fof(f1460,plain,(
% 19.70/8.15 ![X0]: (X0=join(zero,meet(X0,meet(X0,top))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f1458])).
% 19.70/8.15 fof(f1485,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),join(meet(top,X0),X1))=join(top,X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1377,f17])).
% 19.70/8.15 fof(f1943,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f19,f230])).
% 19.70/8.15 fof(f1950,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,join(zero,complement(X1)))=complement(join(meet(X1,top),complement(X0))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f259,f230])).
% 19.70/8.15 fof(f2074,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,sK0_skl),meet(sF1_fnc,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1943,f441])).
% 19.70/8.15 fof(f2078,plain,(
% 19.70/8.15 ![X0]: (X0=join(meet(X0,top),meet(zero,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1943,f439])).
% 19.70/8.15 fof(f2082,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X1,X0),meet(complement(X1),X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1943,f1084])).
% 19.70/8.15 fof(f2083,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1943,f246])).
% 19.70/8.15 fof(f2129,plain,(
% 19.70/8.15 complement(sF1_fnc)=join(meet(complement(sF1_fnc),sK0_skl),zero)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f28,f2074])).
% 19.70/8.15 fof(f2141,plain,(
% 19.70/8.15 complement(sF1_fnc)=join(zero,meet(complement(sF1_fnc),sK0_skl))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f2129])).
% 19.70/8.15 fof(f2142,plain,(
% 19.70/8.15 complement(sF1_fnc)=join(zero,meet(sK0_skl,complement(sF1_fnc)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f2141])).
% 19.70/8.15 fof(f2155,plain,(
% 19.70/8.15 complement(sF1_fnc)=sK0_skl),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f241,f2142])).
% 19.70/8.15 fof(f2317,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(meet(join(complement(X0),complement(X1)),top))))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f232,f1460])).
% 19.70/8.15 fof(f2360,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(complement(join(meet(X0,X1),complement(top))))))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f232,f2317])).
% 19.70/8.15 fof(f2361,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(complement(join(complement(top),meet(X0,X1))))))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f2360])).
% 19.70/8.15 fof(f2362,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),complement(complement(join(zero,meet(X0,X1))))))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f2361])).
% 19.70/8.15 fof(f2848,plain,(
% 19.70/8.15 complement(zero)=join(meet(complement(zero),top),zero)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f28,f2078])).
% 19.70/8.15 fof(f2868,plain,(
% 19.70/8.15 complement(zero)=join(zero,meet(complement(zero),top))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f2848])).
% 19.70/8.15 fof(f2869,plain,(
% 19.70/8.15 complement(zero)=join(zero,meet(top,complement(zero)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f2868])).
% 19.70/8.15 fof(f2870,plain,(
% 19.70/8.15 complement(zero)=join(zero,complement(zero))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1327,f2869])).
% 19.70/8.15 fof(f2874,plain,(
% 19.70/8.15 complement(zero)=top),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f27,f2870])).
% 19.70/8.15 fof(f3245,plain,(
% 19.70/8.15 ![X0]: (complement(complement(X0))=join(meet(X0,complement(complement(X0))),zero))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f28,f2082])).
% 19.70/8.15 fof(f3248,plain,(
% 19.70/8.15 ![X0]: (complement(X0)=join(meet(X0,complement(X0)),complement(complement(complement(X0)))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f931,f2082])).
% 19.70/8.15 fof(f3286,plain,(
% 19.70/8.15 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f3245])).
% 19.70/8.15 fof(f3287,plain,(
% 19.70/8.15 ![X0]: (X0=join(zero,X0))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3304,f974])).
% 19.70/8.15 fof(f3288,plain,(
% 19.70/8.15 ![X0]: (meet(X0,X0)=X0)),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3304,f931])).
% 19.70/8.15 fof(f3291,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(meet(X0,X1),join(zero,meet(X0,X1))))))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3304,f2362])).
% 19.70/8.15 fof(f3304,plain,(
% 19.70/8.15 ![X0]: (complement(complement(X0))=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f242,f3286])).
% 19.70/8.15 fof(f3305,plain,(
% 19.70/8.15 ![X0]: (complement(X0)=join(complement(complement(complement(X0))),meet(X0,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f3248])).
% 19.70/8.15 fof(f3306,plain,(
% 19.70/8.15 ![X0]: (complement(X0)=join(complement(X0),meet(X0,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3304,f3305])).
% 19.70/8.15 fof(f3307,plain,(
% 19.70/8.15 ![X0]: (complement(X0)=join(complement(X0),zero))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f28,f3306])).
% 19.70/8.15 fof(f3308,plain,(
% 19.70/8.15 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3347,f255])).
% 19.70/8.15 fof(f3309,plain,(
% 19.70/8.15 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3347,f259])).
% 19.70/8.15 fof(f3325,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(meet(X1,top),complement(X0))))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3347,f1950])).
% 19.70/8.15 fof(f3347,plain,(
% 19.70/8.15 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f3307])).
% 19.70/8.15 fof(f3364,plain,(
% 19.70/8.15 composition(converse(sK0_skl),sF1_fnc)=zero),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3287,f329])).
% 19.70/8.15 fof(f3369,plain,(
% 19.70/8.15 composition(converse(top),complement(join(sK0_skl,sF0_fnc)))=zero),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3287,f368])).
% 19.70/8.15 fof(f3399,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(meet(X0,X1),join(zero,meet(X0,X1)))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3347,f3291])).
% 19.70/8.15 fof(f3400,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(zero,join(meet(X0,X1),meet(X0,X1)))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f264,f3399])).
% 19.70/8.15 fof(f3401,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(join(meet(X0,X1),meet(X0,X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3287,f3400])).
% 19.70/8.15 fof(f3437,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f946,f3401])).
% 19.70/8.15 fof(f3470,plain,(
% 19.70/8.15 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3475,f1485])).
% 19.70/8.15 fof(f3472,plain,(
% 19.70/8.15 ![X0]: (join(meet(X0,top),meet(top,X0))=X0)),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f3475,f940])).
% 19.70/8.15 fof(f3475,plain,(
% 19.70/8.15 ![X0]: (meet(top,X0)=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3304,f3308])).
% 19.70/8.15 fof(f3488,plain,(
% 19.70/8.15 ![X0]: (meet(X0,top)=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3304,f3309])).
% 19.70/8.15 fof(f3554,plain,(
% 19.70/8.15 ![X0,X1]: (meet(X0,complement(X1))=complement(join(X1,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3488,f3325])).
% 19.70/8.15 fof(f3699,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f264,f3470])).
% 19.70/8.15 fof(f3700,plain,(
% 19.70/8.15 ![X0]: (join(X0,meet(top,X0))=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3488,f3472])).
% 19.70/8.15 fof(f3707,plain,(
% 19.70/8.15 ![X0]: (join(X0,X0)=X0)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3475,f3700])).
% 19.70/8.15 fof(f4018,plain,(
% 19.70/8.15 ![X0]: (X0=join(X0,meet(complement(X0),X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3288,f2082])).
% 19.70/8.15 fof(f4064,plain,(
% 19.70/8.15 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f4018])).
% 19.70/8.15 fof(f4070,plain,(
% 19.70/8.15 ![X0]: (X0=join(X0,zero))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f28,f4064])).
% 19.70/8.15 fof(f4078,plain,(
% 19.70/8.15 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3287,f224])).
% 19.70/8.15 fof(f4090,plain,(
% 19.70/8.15 ![X0]: (X0=join(X0,converse(zero)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f23,f4078])).
% 19.70/8.15 fof(f4233,plain,(
% 19.70/8.15 ![X0]: (join(X0,join(X0,complement(X0)))=top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3707,f263])).
% 19.70/8.15 fof(f4234,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3707,f17])).
% 19.70/8.15 fof(f4283,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(complement(X0),X1))=top)),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f4284,f278])).
% 19.70/8.15 fof(f4284,plain,(
% 19.70/8.15 ![X0]: (join(top,X0)=top)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3699,f4233])).
% 19.70/8.15 fof(f4338,plain,(
% 19.70/8.15 ![X0]: (converse(top)=join(X0,converse(top)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f4284,f224])).
% 19.70/8.15 fof(f4515,plain,(
% 19.70/8.15 zero=converse(zero)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3287,f4090])).
% 19.70/8.15 fof(f4596,plain,(
% 19.70/8.15 converse(zero)=composition(converse(sF1_fnc),sK0_skl)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3364,f215])).
% 19.70/8.15 fof(f4611,plain,(
% 19.70/8.15 zero=composition(converse(sF1_fnc),sK0_skl)),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f4515,f4596])).
% 19.70/8.15 fof(f4681,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3707,f264])).
% 19.70/8.15 fof(f4727,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3707,f264])).
% 19.70/8.15 fof(f5086,plain,(
% 19.70/8.15 join(sF1_fnc,composition(converse(converse(sF1_fnc)),complement(zero)))=sF1_fnc),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f4611,f319])).
% 19.70/8.15 fof(f5102,plain,(
% 19.70/8.15 join(sF1_fnc,composition(sF1_fnc,complement(zero)))=sF1_fnc),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f23,f5086])).
% 19.70/8.15 fof(f5103,plain,(
% 19.70/8.15 join(sF1_fnc,composition(sF1_fnc,top))=sF1_fnc),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f2874,f5102])).
% 19.70/8.15 fof(f5104,plain,(
% 19.70/8.15 join(sF1_fnc,sF0_fnc)=sF1_fnc),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f34,f5103])).
% 19.70/8.15 fof(f5105,plain,(
% 19.70/8.15 join(sF0_fnc,sF1_fnc)=sF1_fnc),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f16,f5104])).
% 19.70/8.15 fof(f5391,plain,(
% 19.70/8.15 converse(top)=top),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f4284,f4338])).
% 19.70/8.15 fof(f5429,plain,(
% 19.70/8.15 composition(top,complement(join(sK0_skl,sF0_fnc)))=zero),
% 19.70/8.15 inference(backward_demodulation,[status(thm)],[f5391,f3369])).
% 19.70/8.15 fof(f8096,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,complement(X1))=complement(meet(complement(X0),X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3304,f3437])).
% 19.70/8.15 fof(f8111,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,complement(meet(X0,X1)))=top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3437,f4283])).
% 19.70/8.15 fof(f8389,plain,(
% 19.70/8.15 ![X0,X1]: (complement(meet(X0,meet(complement(X0),X1)))=top)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3437,f8111])).
% 19.70/8.15 fof(f8911,plain,(
% 19.70/8.15 ![X0,X1]: (complement(top)=meet(X0,meet(complement(X0),X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f8389,f3304])).
% 19.70/8.15 fof(f8948,plain,(
% 19.70/8.15 ![X0,X1]: (zero=meet(X0,meet(complement(X0),X1)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f244,f8911])).
% 19.70/8.15 fof(f8973,plain,(
% 19.70/8.15 ![X0,X1]: (zero=meet(complement(X0),meet(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3304,f8948])).
% 19.70/8.15 fof(f8999,plain,(
% 19.70/8.15 ![X0,X1]: (X0=join(zero,meet(complement(meet(complement(X0),X1)),X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f8948,f2083])).
% 19.70/8.15 fof(f9055,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(complement(meet(complement(X0),X1)),X0))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3287,f8999])).
% 19.70/8.15 fof(f9056,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(X0,complement(meet(complement(X0),X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f9055])).
% 19.70/8.15 fof(f9058,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(X0,join(X0,complement(X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f8096,f9056])).
% 19.70/8.15 fof(f9085,plain,(
% 19.70/8.15 ![X0,X1]: (zero=meet(complement(X0),meet(X1,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f1943,f8973])).
% 19.70/8.15 fof(f9517,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(X0,join(complement(X1),X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f16,f9058])).
% 19.70/8.15 fof(f9522,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3304,f9058])).
% 19.70/8.15 fof(f9737,plain,(
% 19.70/8.15 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f3304,f9517])).
% 19.70/8.15 fof(f11539,plain,(
% 19.70/8.15 sF0_fnc=meet(sF0_fnc,sF1_fnc)),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f5105,f9522])).
% 19.70/8.15 fof(f11707,plain,(
% 19.70/8.15 sF1_fnc=join(sF0_fnc,meet(complement(sF0_fnc),sF1_fnc))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f11539,f2082])).
% 19.70/8.15 fof(f11723,plain,(
% 19.70/8.15 sF1_fnc=join(sF0_fnc,meet(sF1_fnc,complement(sF0_fnc)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f11707])).
% 19.70/8.15 fof(f11983,plain,(
% 19.70/8.15 ![X0,X1]: (zero=meet(complement(join(X0,X1)),X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f9737,f9085])).
% 19.70/8.15 fof(f12058,plain,(
% 19.70/8.15 ![X0,X1]: (zero=meet(X0,complement(join(X1,X0))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f1943,f11983])).
% 19.70/8.15 fof(f12402,plain,(
% 19.70/8.15 ![X0,X1]: (complement(join(X0,X1))=join(zero,meet(complement(X1),complement(join(X0,X1)))))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f12058,f2082])).
% 19.70/8.15 fof(f12541,plain,(
% 19.70/8.15 ![X0,X1]: (complement(join(X0,X1))=meet(complement(X1),complement(join(X0,X1))))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f3287,f12402])).
% 19.70/8.15 fof(f13068,plain,(
% 19.70/8.15 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f264,f4234])).
% 19.70/8.15 fof(f13184,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(join(X0,X1),X2))=join(X2,join(X0,X1)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f4234,f264])).
% 19.70/8.15 fof(f13347,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(X1,join(X0,X2)))=join(X2,join(X0,X1)))),
% 19.70/8.15 inference(forward_demodulation,[status(thm)],[f279,f13184])).
% 19.70/8.15 fof(f13356,plain,(
% 19.70/8.15 ![X0,X1,X2]: (join(X0,join(X1,join(join(X1,X0),X2)))=join(X2,join(X1,X0)))),
% 19.70/8.15 inference(paramodulation,[status(thm)],[f279,f4727])).
% 19.70/8.22 fof(f13490,plain,(
% 19.70/8.22 ![X0,X1,X2]: (join(X0,join(X1,join(X0,join(X1,X2))))=join(X2,join(X1,X0)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f279,f13356])).
% 19.70/8.22 fof(f13491,plain,(
% 19.70/8.22 ![X0,X1,X2]: (join(join(X0,X1),join(X2,X0))=join(X1,join(X0,X2)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f13347,f13490])).
% 19.70/8.22 fof(f13492,plain,(
% 19.70/8.22 ![X0,X1,X2]: (join(X0,join(X1,join(X2,X1)))=join(X0,join(X1,X2)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f279,f13491])).
% 19.70/8.22 fof(f13493,plain,(
% 19.70/8.22 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f4681,f13492])).
% 19.70/8.22 fof(f16183,plain,(
% 19.70/8.22 ![X0]: (composition(join(top,X0),complement(join(sK0_skl,sF0_fnc)))=join(composition(X0,complement(join(sK0_skl,sF0_fnc))),zero))),
% 19.70/8.22 inference(paramodulation,[status(thm)],[f5429,f161])).
% 19.70/8.22 fof(f16241,plain,(
% 19.70/8.22 ![X0]: (composition(top,complement(join(sK0_skl,sF0_fnc)))=join(composition(X0,complement(join(sK0_skl,sF0_fnc))),zero))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f4284,f16183])).
% 19.70/8.22 fof(f16242,plain,(
% 19.70/8.22 ![X0]: (zero=join(composition(X0,complement(join(sK0_skl,sF0_fnc))),zero))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f5429,f16241])).
% 19.70/8.22 fof(f16251,plain,(
% 19.70/8.22 ![X0]: (zero=composition(X0,complement(join(sK0_skl,sF0_fnc))))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f4070,f16242])).
% 19.70/8.22 fof(f18849,plain,(
% 19.70/8.22 zero=complement(join(sK0_skl,sF0_fnc))),
% 19.70/8.22 inference(paramodulation,[status(thm)],[f845,f16251])).
% 19.70/8.22 fof(f19039,plain,(
% 19.70/8.22 join(sK0_skl,join(sF0_fnc,zero))=top),
% 19.70/8.22 inference(paramodulation,[status(thm)],[f18849,f263])).
% 19.70/8.22 fof(f19062,plain,(
% 19.70/8.22 join(sK0_skl,join(zero,sF0_fnc))=top),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f13493,f19039])).
% 19.70/8.22 fof(f19122,plain,(
% 19.70/8.22 join(sK0_skl,sF0_fnc)=top),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f3287,f19062])).
% 19.70/8.22 fof(f22086,plain,(
% 19.70/8.22 ![X0,X1]: (meet(complement(X0),complement(X1))=complement(join(X1,X0)))),
% 19.70/8.22 inference(paramodulation,[status(thm)],[f3304,f3554])).
% 19.70/8.22 fof(f22088,plain,(
% 19.70/8.22 ![X0]: (meet(sF1_fnc,complement(X0))=complement(join(X0,sK0_skl)))),
% 19.70/8.22 inference(paramodulation,[status(thm)],[f2155,f3554])).
% 19.70/8.22 fof(f22178,plain,(
% 19.70/8.22 ![X0,X1]: (complement(join(X0,X1))=complement(join(join(X0,X1),X1)))),
% 19.70/8.22 inference(backward_demodulation,[status(thm)],[f22086,f12541])).
% 19.70/8.22 fof(f22187,plain,(
% 19.70/8.22 sF1_fnc=join(sF0_fnc,complement(join(sF0_fnc,sK0_skl)))),
% 19.70/8.22 inference(backward_demodulation,[status(thm)],[f22088,f11723])).
% 19.70/8.22 fof(f22239,plain,(
% 19.70/8.22 ![X0,X1]: (complement(join(X0,X1))=complement(join(X1,join(X0,X1))))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f279,f22178])).
% 19.70/8.22 fof(f22240,plain,(
% 19.70/8.22 ![X0,X1]: (complement(join(X0,X1))=complement(join(X1,X0)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f13068,f22239])).
% 19.70/8.22 fof(f22251,plain,(
% 19.70/8.22 sF1_fnc=join(sF0_fnc,complement(join(sK0_skl,sF0_fnc)))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f22240,f22187])).
% 19.70/8.22 fof(f22252,plain,(
% 19.70/8.22 sF1_fnc=join(sF0_fnc,complement(top))),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f19122,f22251])).
% 19.70/8.22 fof(f22253,plain,(
% 19.70/8.22 sF1_fnc=join(sF0_fnc,zero)),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f244,f22252])).
% 19.70/8.22 fof(f22254,plain,(
% 19.70/8.22 sF1_fnc=sF0_fnc),
% 19.70/8.22 inference(forward_demodulation,[status(thm)],[f4070,f22253])).
% 19.70/8.22 fof(f22255,plain,(
% 19.70/8.22 $false),
% 19.70/8.22 inference(forward_subsumption_resolution,[status(thm)],[f22254,f35])).
% 19.70/8.22 % SZS output end CNFRefutation for theBenchmark.p
% 4.71/8.23 % Elapsed time: 2.611699 seconds
% 4.71/8.23 % CPU time: 20.486309 seconds
% 4.71/8.23 % Total memory used: 182.801 MB
% 4.71/8.23 % Net memory used: 177.888 MB
%------------------------------------------------------------------------------