%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL050+1 : 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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:03:46 PM UTC 2026
% Result : Theorem 2.67s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL050+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n011.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:08:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 2.67/0.83 % Refutation found
% 2.67/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.67/0.83 % SZS output start CNFRefutation for theBenchmark
% 2.67/0.83 fof(f1,axiom,(
% 2.67/0.83 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f2,axiom,(
% 2.67/0.83 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f3,axiom,(
% 2.67/0.83 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f4,axiom,(
% 2.67/0.83 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f5,axiom,(
% 2.67/0.83 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f6,axiom,(
% 2.67/0.83 (! [X0] : composition(X0,one) = X0 )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f7,axiom,(
% 2.67/0.83 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f8,axiom,(
% 2.67/0.83 (! [X0] : converse(converse(X0)) = X0 )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f9,axiom,(
% 2.67/0.83 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f10,axiom,(
% 2.67/0.83 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f11,axiom,(
% 2.67/0.83 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f12,axiom,(
% 2.67/0.83 (! [X0] : top = join(X0,complement(X0)) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f13,axiom,(
% 2.67/0.83 (! [X0] : zero = meet(X0,complement(X0)) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f14,conjecture,(
% 2.67/0.83 (! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top) )),
% 2.67/0.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.67/0.83 fof(f15,negated_conjecture,(
% 2.67/0.83 ~((! [X0] : complement(composition(X0,top)) = composition(complement(composition(X0,top)),top) ))),
% 2.67/0.83 inference(negated_conjecture,[status(cth)],[f14])).
% 2.67/0.83 fof(f16,plain,(
% 2.67/0.83 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f1])).
% 2.67/0.83 fof(f17,plain,(
% 2.67/0.83 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f2])).
% 2.67/0.83 fof(f18,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f3])).
% 2.67/0.83 fof(f19,plain,(
% 2.67/0.83 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f4])).
% 2.67/0.83 fof(f20,plain,(
% 2.67/0.83 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f5])).
% 2.67/0.83 fof(f21,plain,(
% 2.67/0.83 ![X0]: (composition(X0,one)=X0)),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f6])).
% 2.67/0.83 fof(f22,plain,(
% 2.67/0.83 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f7])).
% 2.67/0.83 fof(f23,plain,(
% 2.67/0.83 ![X0]: (converse(converse(X0))=X0)),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f8])).
% 2.67/0.83 fof(f24,plain,(
% 2.67/0.83 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f9])).
% 2.67/0.83 fof(f25,plain,(
% 2.67/0.83 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f10])).
% 2.67/0.83 fof(f26,plain,(
% 2.67/0.83 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f11])).
% 2.67/0.83 fof(f27,plain,(
% 2.67/0.83 ![X0]: (top=join(X0,complement(X0)))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f12])).
% 2.67/0.83 fof(f28,plain,(
% 2.67/0.83 ![X0]: (zero=meet(X0,complement(X0)))),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f13])).
% 2.67/0.83 fof(f29,plain,(
% 2.67/0.83 (?[X0]: ~complement(composition(X0,top))=composition(complement(composition(X0,top)),top))),
% 2.67/0.83 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 2.67/0.83 fof(f30,plain,(
% 2.67/0.83 ~complement(composition(sK0_skl,top))=composition(complement(composition(sK0_skl,top)),top)),
% 2.67/0.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f29])).
% 2.67/0.83 fof(f31,plain,(
% 2.67/0.83 ~complement(composition(sK0_skl,top))=composition(complement(composition(sK0_skl,top)),top)),
% 2.67/0.83 inference(cnf_transformation,[status(thm)],[f30])).
% 2.67/0.83 fof(f32,definition,(
% 2.67/0.83 sF1_fnc=composition(sK0_skl,top)),
% 2.67/0.83 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 2.67/0.83 fof(f33,definition,(
% 2.67/0.83 sF0_fnc=complement(sF1_fnc)),
% 2.67/0.83 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 2.67/0.83 fof(f34,definition,(
% 2.67/0.83 sF3_fnc=complement(sF1_fnc)),
% 2.67/0.83 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 2.67/0.83 fof(f35,definition,(
% 2.67/0.83 sF2_fnc=composition(sF3_fnc,top)),
% 2.67/0.83 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 2.67/0.83 fof(f36,plain,(
% 2.67/0.83 ~sF0_fnc=sF2_fnc),
% 2.67/0.83 inference(definition_folding,[],[f31,f35,f34,f33,f32])).
% 2.67/0.83 fof(f37,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 2.67/0.83 fof(f38,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f19,f37])).
% 2.67/0.83 fof(f39,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 2.67/0.83 fof(f40,plain,(
% 2.67/0.83 sF3_fnc=sF0_fnc),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f33,f34])).
% 2.67/0.83 fof(f41,plain,(
% 2.67/0.83 sF2_fnc=composition(sF0_fnc,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f40,f35])).
% 2.67/0.83 fof(f42,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f38])).
% 2.67/0.83 fof(f43,plain,(
% 2.67/0.83 top=join(sF1_fnc,sF0_fnc)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f33,f27])).
% 2.67/0.83 fof(f44,plain,(
% 2.67/0.83 top=join(sF0_fnc,sF1_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f43])).
% 2.67/0.83 fof(f47,plain,(
% 2.67/0.83 ![X0]: (composition(sK0_skl,composition(top,X0))=composition(sF1_fnc,X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f32,f20])).
% 2.67/0.83 fof(f57,plain,(
% 2.67/0.83 ![X0]: (sF1_fnc=join(meet(sF1_fnc,X0),complement(join(sF0_fnc,X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f33,f42])).
% 2.67/0.83 fof(f76,plain,(
% 2.67/0.83 ![X0]: (composition(join(sF0_fnc,X0),top)=join(sF2_fnc,composition(X0,top)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f41,f22])).
% 2.67/0.83 fof(f81,plain,(
% 2.67/0.83 ![X0]: (composition(join(X0,sF0_fnc),top)=join(composition(X0,top),sF2_fnc))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f41,f22])).
% 2.67/0.83 fof(f83,plain,(
% 2.67/0.83 ![X0]: (composition(join(X0,sK0_skl),top)=join(composition(X0,top),sF1_fnc))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f32,f22])).
% 2.67/0.83 fof(f90,plain,(
% 2.67/0.83 ![X0]: (composition(join(X0,sF0_fnc),top)=join(sF2_fnc,composition(X0,top)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f81])).
% 2.67/0.83 fof(f95,plain,(
% 2.67/0.83 ![X0]: (composition(join(X0,sK0_skl),top)=join(sF1_fnc,composition(X0,top)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f83])).
% 2.67/0.83 fof(f103,plain,(
% 2.67/0.83 composition(join(sF0_fnc,sF0_fnc),top)=join(sF2_fnc,sF2_fnc)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f41,f76])).
% 2.67/0.83 fof(f151,plain,(
% 2.67/0.83 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f21,f20])).
% 2.67/0.83 fof(f158,plain,(
% 2.67/0.83 zero=meet(sF1_fnc,sF0_fnc)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f33,f28])).
% 2.67/0.83 fof(f195,plain,(
% 2.67/0.83 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X1,X2),composition(X0,X2)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f22,f16])).
% 2.67/0.83 fof(f204,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(X1,complement(X0)))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f16,f42])).
% 2.67/0.83 fof(f212,plain,(
% 2.67/0.83 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f23,f24])).
% 2.67/0.83 fof(f217,plain,(
% 2.67/0.83 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f23,f25])).
% 2.67/0.83 fof(f231,plain,(
% 2.67/0.83 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f27,f19])).
% 2.67/0.83 fof(f232,plain,(
% 2.67/0.83 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f16,f19])).
% 2.67/0.83 fof(f238,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f19,f42])).
% 2.67/0.83 fof(f241,plain,(
% 2.67/0.83 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(meet(join(complement(X0),complement(X1)),X2),complement(join(meet(X0,X1),X2))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f19,f42])).
% 2.67/0.83 fof(f248,plain,(
% 2.67/0.83 zero=complement(top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f28,f231])).
% 2.67/0.83 fof(f250,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f238])).
% 2.67/0.83 fof(f252,plain,(
% 2.67/0.83 ![X0,X1,X2]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),X2)),meet(join(complement(X0),complement(X1)),X2)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f241])).
% 2.67/0.83 fof(f254,plain,(
% 2.67/0.83 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f19])).
% 2.67/0.83 fof(f255,plain,(
% 2.67/0.83 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f19])).
% 2.67/0.83 fof(f258,plain,(
% 2.67/0.83 top=join(top,zero)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f27])).
% 2.67/0.83 fof(f259,plain,(
% 2.67/0.83 ![X0]: (meet(X0,top)=complement(join(zero,complement(X0))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f254])).
% 2.67/0.83 fof(f260,plain,(
% 2.67/0.83 top=join(zero,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f258])).
% 2.67/0.83 fof(f280,plain,(
% 2.67/0.83 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f16,f17])).
% 2.67/0.83 fof(f299,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,join(sF1_fnc,X0))=join(top,X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f44,f17])).
% 2.67/0.83 fof(f300,plain,(
% 2.67/0.83 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f27,f17])).
% 2.67/0.83 fof(f312,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,composition(converse(X0),complement(composition(X0,sF1_fnc))))=complement(sF1_fnc))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f33,f39])).
% 2.67/0.83 fof(f326,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,composition(converse(X0),complement(composition(X0,sF1_fnc))))=sF0_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f33,f312])).
% 2.67/0.83 fof(f443,plain,(
% 2.67/0.83 meet(top,top)=complement(join(zero,zero))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f259])).
% 2.67/0.83 fof(f545,plain,(
% 2.67/0.83 ![X0]: (meet(top,X0)=meet(X0,top))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f259,f255])).
% 2.67/0.83 fof(f554,plain,(
% 2.67/0.83 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X0,X1))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f19,f255])).
% 2.67/0.83 fof(f596,plain,(
% 2.67/0.83 ![X0]: (top=join(meet(X0,top),meet(top,complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f545,f250])).
% 2.67/0.83 fof(f601,plain,(
% 2.67/0.83 ![X0]: (X0=join(meet(top,X0),complement(join(complement(X0),top))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f545,f42])).
% 2.67/0.83 fof(f606,plain,(
% 2.67/0.83 ![X0]: (X0=join(meet(top,X0),complement(join(top,complement(X0)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f601])).
% 2.67/0.83 fof(f639,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,composition(join(X0,sK0_skl),top))=join(top,composition(X0,top)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f95,f299])).
% 2.67/0.83 fof(f643,plain,(
% 2.67/0.83 ![X0,X1,X2]: (composition(join(X0,X1),X2)=composition(join(X1,X0),X2))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f22,f195])).
% 2.67/0.83 fof(f755,plain,(
% 2.67/0.83 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f21,f217])).
% 2.67/0.83 fof(f774,plain,(
% 2.67/0.83 ![X0]: (X0=composition(converse(one),X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f23,f755])).
% 2.67/0.83 fof(f786,plain,(
% 2.67/0.83 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f151,f774])).
% 2.67/0.83 fof(f787,plain,(
% 2.67/0.83 one=converse(one)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f21,f774])).
% 2.67/0.83 fof(f788,plain,(
% 2.67/0.83 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f774,f39])).
% 2.67/0.83 fof(f797,plain,(
% 2.67/0.83 composition(join(converse(one),sF0_fnc),top)=join(sF2_fnc,top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f774,f90])).
% 2.67/0.83 fof(f800,plain,(
% 2.67/0.83 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(composition(X0,X1),X1))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f774,f195])).
% 2.67/0.83 fof(f801,plain,(
% 2.67/0.83 ![X0,X1]: (composition(join(X0,converse(one)),X1)=join(X1,composition(X0,X1)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f774,f195])).
% 2.67/0.83 fof(f813,plain,(
% 2.67/0.83 ![X0]: (composition(one,X0)=X0)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f774,f786])).
% 2.67/0.83 fof(f815,plain,(
% 2.67/0.83 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f813,f788])).
% 2.67/0.83 fof(f826,plain,(
% 2.67/0.83 composition(join(sF0_fnc,converse(one)),top)=join(sF2_fnc,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f643,f797])).
% 2.67/0.83 fof(f827,plain,(
% 2.67/0.83 composition(join(sF0_fnc,one),top)=join(sF2_fnc,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f787,f826])).
% 2.67/0.83 fof(f828,plain,(
% 2.67/0.83 composition(join(one,sF0_fnc),top)=join(sF2_fnc,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f643,f827])).
% 2.67/0.83 fof(f829,plain,(
% 2.67/0.83 composition(join(one,sF0_fnc),top)=join(top,sF2_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f828])).
% 2.67/0.83 fof(f836,plain,(
% 2.67/0.83 ![X0,X1]: (composition(join(one,X0),X1)=join(composition(X0,X1),X1))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f787,f800])).
% 2.67/0.83 fof(f837,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,composition(join(X0,sK0_skl),top))=composition(join(one,X0),top))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f839,f639])).
% 2.67/0.83 fof(f839,plain,(
% 2.67/0.83 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f836])).
% 2.67/0.83 fof(f840,plain,(
% 2.67/0.83 ![X0,X1]: (composition(join(X0,one),X1)=join(X1,composition(X0,X1)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f787,f801])).
% 2.67/0.83 fof(f913,plain,(
% 2.67/0.83 join(zero,complement(top))=complement(top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f815])).
% 2.67/0.83 fof(f914,plain,(
% 2.67/0.83 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f443,f815])).
% 2.67/0.83 fof(f920,plain,(
% 2.67/0.83 join(sF0_fnc,complement(sF1_fnc))=complement(sF1_fnc)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f33,f815])).
% 2.67/0.83 fof(f922,plain,(
% 2.67/0.83 join(complement(join(zero,zero)),meet(top,top))=complement(join(zero,zero))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f443,f815])).
% 2.67/0.83 fof(f930,plain,(
% 2.67/0.83 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f815,f42])).
% 2.67/0.83 fof(f932,plain,(
% 2.67/0.83 join(zero,zero)=complement(top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f913])).
% 2.67/0.83 fof(f939,plain,(
% 2.67/0.83 join(zero,zero)=zero),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f932])).
% 2.67/0.83 fof(f940,plain,(
% 2.67/0.83 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f443,f914])).
% 2.67/0.83 fof(f941,plain,(
% 2.67/0.83 join(meet(top,top),meet(top,top))=meet(top,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f443,f940])).
% 2.67/0.83 fof(f956,plain,(
% 2.67/0.83 join(sF0_fnc,sF0_fnc)=complement(sF1_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f33,f920])).
% 2.67/0.83 fof(f963,plain,(
% 2.67/0.83 composition(sF0_fnc,top)=join(sF2_fnc,sF2_fnc)),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f964,f103])).
% 2.67/0.83 fof(f964,plain,(
% 2.67/0.83 join(sF0_fnc,sF0_fnc)=sF0_fnc),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f33,f956])).
% 2.67/0.83 fof(f968,plain,(
% 2.67/0.83 join(meet(top,top),complement(join(zero,zero)))=complement(join(zero,zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f922])).
% 2.67/0.83 fof(f969,plain,(
% 2.67/0.83 join(meet(top,top),meet(top,top))=complement(join(zero,zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f443,f968])).
% 2.67/0.83 fof(f970,plain,(
% 2.67/0.83 meet(top,top)=complement(join(zero,zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f941,f969])).
% 2.67/0.83 fof(f971,plain,(
% 2.67/0.83 meet(top,top)=complement(zero)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f939,f970])).
% 2.67/0.83 fof(f995,plain,(
% 2.67/0.83 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f930])).
% 2.67/0.83 fof(f996,plain,(
% 2.67/0.83 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f28,f995])).
% 2.67/0.83 fof(f997,plain,(
% 2.67/0.83 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f996])).
% 2.67/0.83 fof(f1016,plain,(
% 2.67/0.83 sF2_fnc=join(sF2_fnc,sF2_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f41,f963])).
% 2.67/0.83 fof(f1023,plain,(
% 2.67/0.83 ![X0]: (join(sF2_fnc,join(sF2_fnc,X0))=join(sF2_fnc,X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1016,f17])).
% 2.67/0.83 fof(f1024,plain,(
% 2.67/0.83 sF1_fnc=join(meet(sF1_fnc,sF0_fnc),complement(sF0_fnc))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f964,f57])).
% 2.67/0.83 fof(f1026,plain,(
% 2.67/0.83 sF1_fnc=join(complement(sF0_fnc),meet(sF1_fnc,sF0_fnc))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1024])).
% 2.67/0.83 fof(f1027,plain,(
% 2.67/0.83 sF1_fnc=join(complement(sF0_fnc),zero)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f158,f1026])).
% 2.67/0.83 fof(f1028,plain,(
% 2.67/0.83 sF1_fnc=join(zero,complement(sF0_fnc))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1027])).
% 2.67/0.83 fof(f1094,plain,(
% 2.67/0.83 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f997,f255])).
% 2.67/0.83 fof(f1105,plain,(
% 2.67/0.83 ![X0]: (top=join(meet(X0,top),complement(X0)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f1094,f596])).
% 2.67/0.83 fof(f1109,plain,(
% 2.67/0.83 ![X0]: (top=join(complement(X0),meet(X0,top)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1105])).
% 2.67/0.83 fof(f1115,plain,(
% 2.67/0.83 ![X0,X1]: (meet(top,meet(X0,X1))=complement(join(complement(X0),complement(X1))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f19,f1094])).
% 2.67/0.83 fof(f1136,plain,(
% 2.67/0.83 ![X0,X1]: (meet(top,meet(X0,X1))=meet(X0,X1))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f19,f1115])).
% 2.67/0.83 fof(f1157,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X1,X0)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f19,f204])).
% 2.67/0.83 fof(f1188,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X1,X0),meet(X0,complement(X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1157])).
% 2.67/0.83 fof(f1374,plain,(
% 2.67/0.83 join(sF2_fnc,top)=join(sF2_fnc,complement(sF2_fnc))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f27,f1023])).
% 2.67/0.83 fof(f1384,plain,(
% 2.67/0.83 join(top,sF2_fnc)=join(sF2_fnc,complement(sF2_fnc))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1374])).
% 2.67/0.83 fof(f1385,plain,(
% 2.67/0.83 composition(join(one,sF0_fnc),top)=top),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f1386,f829])).
% 2.67/0.83 fof(f1386,plain,(
% 2.67/0.83 join(top,sF2_fnc)=top),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f27,f1384])).
% 2.67/0.83 fof(f1487,plain,(
% 2.67/0.83 ![X0]: (composition(join(join(one,sF0_fnc),X0),top)=join(composition(X0,top),top))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1385,f195])).
% 2.67/0.83 fof(f1511,plain,(
% 2.67/0.83 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=join(composition(X0,top),top))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f17,f1487])).
% 2.67/0.83 fof(f1512,plain,(
% 2.67/0.83 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=join(top,composition(X0,top)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1511])).
% 2.67/0.83 fof(f1513,plain,(
% 2.67/0.83 ![X0]: (composition(join(one,join(sF0_fnc,X0)),top)=composition(join(X0,one),top))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f840,f1512])).
% 2.67/0.83 fof(f1543,plain,(
% 2.67/0.83 ![X0]: (X0=join(meet(X0,meet(X0,top)),complement(top)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1109,f42])).
% 2.67/0.83 fof(f1556,plain,(
% 2.67/0.83 ![X0]: (X0=join(complement(top),meet(X0,meet(X0,top))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1543])).
% 2.67/0.83 fof(f1557,plain,(
% 2.67/0.83 ![X0]: (X0=join(zero,meet(X0,meet(X0,top))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f1556])).
% 2.67/0.83 fof(f1561,plain,(
% 2.67/0.83 ![X0]: (X0=join(zero,meet(X0,meet(top,X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f545,f1557])).
% 2.67/0.83 fof(f1807,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(meet(X0,X1),top)),meet(top,join(complement(X0),complement(X1)))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f545,f252])).
% 2.67/0.83 fof(f1903,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),meet(top,join(complement(X0),complement(X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1807])).
% 2.67/0.83 fof(f1904,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(top,meet(X0,X1))),complement(join(zero,meet(X0,X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f554,f1903])).
% 2.67/0.83 fof(f1905,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(zero,meet(X0,X1))),complement(join(top,meet(X0,X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f1904])).
% 2.67/0.83 fof(f2295,plain,(
% 2.67/0.83 ![X0]: (join(X0,complement(X0))=join(top,complement(X0)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f815,f300])).
% 2.67/0.83 fof(f2299,plain,(
% 2.67/0.83 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f27,f300])).
% 2.67/0.83 fof(f2303,plain,(
% 2.67/0.83 ![X0]: (join(top,join(zero,X0))=join(top,X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f248,f300])).
% 2.67/0.83 fof(f2317,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f300,f42])).
% 2.67/0.83 fof(f2329,plain,(
% 2.67/0.83 ![X0]: (X0=join(meet(top,X0),complement(top)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2330,f606])).
% 2.67/0.83 fof(f2330,plain,(
% 2.67/0.83 ![X0]: (top=join(top,complement(X0)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f27,f2295])).
% 2.67/0.83 fof(f2339,plain,(
% 2.67/0.83 ![X0]: (join(X0,top)=top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2330,f2299])).
% 2.67/0.83 fof(f2340,plain,(
% 2.67/0.83 ![X0]: (join(zero,join(X0,top))=join(top,X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f280,f2303])).
% 2.67/0.83 fof(f2341,plain,(
% 2.67/0.83 ![X0]: (join(zero,top)=join(top,X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2339,f2340])).
% 2.67/0.83 fof(f2347,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,join(sF1_fnc,X0))=top)),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2370,f299])).
% 2.67/0.83 fof(f2350,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(join(zero,meet(X0,X1))),complement(top)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2370,f1905])).
% 2.67/0.83 fof(f2370,plain,(
% 2.67/0.83 ![X0]: (top=join(top,X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f260,f2341])).
% 2.67/0.83 fof(f2400,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(complement(join(top,X1)),meet(X0,join(complement(complement(X0)),X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f2317])).
% 2.67/0.83 fof(f2401,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(complement(top),meet(X0,join(complement(complement(X0)),X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2370,f2400])).
% 2.67/0.83 fof(f2402,plain,(
% 2.67/0.83 ![X0,X1]: (X0=join(zero,meet(X0,join(complement(complement(X0)),X1))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f2401])).
% 2.67/0.83 fof(f2417,plain,(
% 2.67/0.83 ![X0]: (X0=join(complement(top),meet(top,X0)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f2329])).
% 2.67/0.83 fof(f2420,plain,(
% 2.67/0.83 ![X0]: (X0=join(zero,meet(top,X0)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f2417])).
% 2.67/0.83 fof(f2425,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(complement(top),complement(join(zero,meet(X0,X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f2350])).
% 2.67/0.83 fof(f2426,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(join(zero,meet(X0,X1)))))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f2425])).
% 2.67/0.83 fof(f2505,plain,(
% 2.67/0.83 meet(top,top)=top),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1561,f2420])).
% 2.67/0.83 fof(f2510,plain,(
% 2.67/0.83 ![X0,X1]: (meet(X0,X1)=join(zero,meet(X0,X1)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1136,f2420])).
% 2.67/0.83 fof(f2511,plain,(
% 2.67/0.83 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f1094,f2420])).
% 2.67/0.83 fof(f2524,plain,(
% 2.67/0.83 top=complement(zero)),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2505,f971])).
% 2.67/0.83 fof(f2526,plain,(
% 2.67/0.83 ![X0]: (X0=meet(top,X0))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2510,f2420])).
% 2.67/0.83 fof(f2529,plain,(
% 2.67/0.83 ![X0]: (X0=meet(X0,meet(top,X0)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2510,f1561])).
% 2.67/0.83 fof(f2550,plain,(
% 2.67/0.83 ![X0,X1]: (X0=meet(X0,join(complement(complement(X0)),X1)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2510,f2402])).
% 2.67/0.83 fof(f2553,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,complement(meet(X0,X1))))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2510,f2426])).
% 2.67/0.83 fof(f2556,plain,(
% 2.67/0.83 ![X0]: (X0=complement(complement(X0)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2511,f997])).
% 2.67/0.83 fof(f2557,plain,(
% 2.67/0.83 sF1_fnc=complement(sF0_fnc)),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2511,f1028])).
% 2.67/0.83 fof(f2650,plain,(
% 2.67/0.83 ![X0]: (X0=meet(X0,X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2526,f2529])).
% 2.67/0.83 fof(f2726,plain,(
% 2.67/0.83 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2727,f232])).
% 2.67/0.83 fof(f2727,plain,(
% 2.67/0.83 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2511,f2553])).
% 2.67/0.83 fof(f2730,plain,(
% 2.67/0.83 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f2556,f2550])).
% 2.67/0.83 fof(f2903,plain,(
% 2.67/0.83 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f2556,f2726])).
% 2.67/0.83 fof(f2920,plain,(
% 2.67/0.83 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f2650,f1188])).
% 2.67/0.83 fof(f2952,plain,(
% 2.67/0.83 ![X0]: (X0=join(X0,zero))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f28,f2920])).
% 2.67/0.83 fof(f3027,plain,(
% 2.67/0.83 ![X0]: (X0=join(zero,X0))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f16,f2952])).
% 2.67/0.83 fof(f3032,plain,(
% 2.67/0.83 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f2952,f212])).
% 2.67/0.83 fof(f3050,plain,(
% 2.67/0.83 ![X0]: (X0=join(X0,converse(zero)))),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f23,f3032])).
% 2.67/0.83 fof(f3717,plain,(
% 2.67/0.83 ![X0]: (join(sF0_fnc,composition(join(X0,sK0_skl),top))=top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f95,f2347])).
% 2.67/0.83 fof(f3736,plain,(
% 2.67/0.83 ![X0]: (top=composition(join(one,X0),top))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f3717,f837])).
% 2.67/0.83 fof(f3748,plain,(
% 2.67/0.83 ![X0]: (top=composition(join(X0,one),top))),
% 2.67/0.83 inference(backward_demodulation,[status(thm)],[f3736,f1513])).
% 2.67/0.83 fof(f3753,plain,(
% 2.67/0.83 top=composition(top,top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f2370,f3748])).
% 2.67/0.83 fof(f3893,plain,(
% 2.67/0.83 composition(sK0_skl,top)=composition(sF1_fnc,top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f3753,f47])).
% 2.67/0.83 fof(f3911,plain,(
% 2.67/0.83 sF1_fnc=composition(sF1_fnc,top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f32,f3893])).
% 2.67/0.83 fof(f3953,plain,(
% 2.67/0.83 composition(join(sF1_fnc,sF0_fnc),top)=join(sF2_fnc,sF1_fnc)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f3911,f90])).
% 2.67/0.83 fof(f3962,plain,(
% 2.67/0.83 join(complement(top),composition(converse(sF1_fnc),complement(sF1_fnc)))=complement(top)),
% 2.67/0.83 inference(paramodulation,[status(thm)],[f3911,f39])).
% 2.67/0.83 fof(f3970,plain,(
% 2.67/0.83 composition(join(sF0_fnc,sF1_fnc),top)=join(sF2_fnc,sF1_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f643,f3953])).
% 2.67/0.83 fof(f3971,plain,(
% 2.67/0.83 composition(top,top)=join(sF2_fnc,sF1_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f44,f3970])).
% 2.67/0.83 fof(f3972,plain,(
% 2.67/0.83 top=join(sF2_fnc,sF1_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f3753,f3971])).
% 2.67/0.83 fof(f3974,plain,(
% 2.67/0.83 top=join(sF1_fnc,sF2_fnc)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f16,f3972])).
% 2.67/0.83 fof(f3988,plain,(
% 2.67/0.83 join(zero,composition(converse(sF1_fnc),complement(sF1_fnc)))=complement(top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f248,f3962])).
% 2.67/0.83 fof(f3989,plain,(
% 2.67/0.83 composition(converse(sF1_fnc),complement(sF1_fnc))=complement(top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f3027,f3988])).
% 2.67/0.83 fof(f3990,plain,(
% 2.67/0.83 composition(converse(sF1_fnc),sF0_fnc)=complement(top)),
% 2.67/0.83 inference(forward_demodulation,[status(thm)],[f33,f3989])).
% 3.48/0.85 fof(f3991,plain,(
% 3.48/0.85 composition(converse(sF1_fnc),sF0_fnc)=zero),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f248,f3990])).
% 3.48/0.85 fof(f4052,plain,(
% 3.48/0.85 zero=converse(zero)),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f3027,f3050])).
% 3.48/0.85 fof(f4146,plain,(
% 3.48/0.85 converse(zero)=composition(converse(sF0_fnc),sF1_fnc)),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f3991,f217])).
% 3.48/0.85 fof(f4160,plain,(
% 3.48/0.85 zero=composition(converse(sF0_fnc),sF1_fnc)),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f4052,f4146])).
% 3.48/0.85 fof(f4215,plain,(
% 3.48/0.85 join(sF0_fnc,composition(converse(converse(sF0_fnc)),complement(zero)))=sF0_fnc),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f4160,f326])).
% 3.48/0.85 fof(f4230,plain,(
% 3.48/0.85 join(sF0_fnc,composition(sF0_fnc,complement(zero)))=sF0_fnc),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f23,f4215])).
% 3.48/0.85 fof(f4231,plain,(
% 3.48/0.85 join(sF0_fnc,composition(sF0_fnc,top))=sF0_fnc),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f2524,f4230])).
% 3.48/0.85 fof(f4232,plain,(
% 3.48/0.85 join(sF0_fnc,sF2_fnc)=sF0_fnc),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f41,f4231])).
% 3.48/0.85 fof(f4591,plain,(
% 3.48/0.85 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f16,f2730])).
% 3.48/0.85 fof(f4657,plain,(
% 3.48/0.85 sF2_fnc=meet(sF2_fnc,sF0_fnc)),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f4232,f4591])).
% 3.48/0.85 fof(f4691,plain,(
% 3.48/0.85 sF2_fnc=meet(sF0_fnc,sF2_fnc)),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f2903,f4657])).
% 3.48/0.85 fof(f4710,plain,(
% 3.48/0.85 sF0_fnc=join(sF2_fnc,complement(join(sF2_fnc,complement(sF0_fnc))))),
% 3.48/0.85 inference(paramodulation,[status(thm)],[f4691,f204])).
% 3.48/0.85 fof(f4726,plain,(
% 3.48/0.85 sF0_fnc=join(sF2_fnc,complement(join(sF2_fnc,sF1_fnc)))),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f2557,f4710])).
% 3.48/0.85 fof(f4727,plain,(
% 3.48/0.85 sF0_fnc=join(sF2_fnc,complement(join(sF1_fnc,sF2_fnc)))),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f16,f4726])).
% 3.48/0.85 fof(f4728,plain,(
% 3.48/0.85 sF0_fnc=join(sF2_fnc,complement(top))),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f3974,f4727])).
% 3.48/0.85 fof(f4729,plain,(
% 3.48/0.85 sF0_fnc=join(sF2_fnc,zero)),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f248,f4728])).
% 3.48/0.85 fof(f4730,plain,(
% 3.48/0.85 sF0_fnc=sF2_fnc),
% 3.48/0.85 inference(forward_demodulation,[status(thm)],[f2952,f4729])).
% 3.48/0.85 fof(f4731,plain,(
% 3.48/0.85 $false),
% 3.48/0.85 inference(forward_subsumption_resolution,[status(thm)],[f4730,f36])).
% 3.48/0.85 % SZS output end CNFRefutation for theBenchmark.p
% 3.48/0.87 % Elapsed time: 0.496908 seconds
% 3.48/0.87 % CPU time: 3.728025 seconds
% 3.48/0.87 % Total memory used: 70.330 MB
% 3.48/0.87 % Net memory used: 68.341 MB
%------------------------------------------------------------------------------