%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL012+2 : 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 : n014.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:34 PM UTC 2026
% Result : Theorem 30.27s 4.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL012+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 03:58:34 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 30.27/4.39 % Refutation found
% 30.27/4.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 30.27/4.39 % SZS output start CNFRefutation for theBenchmark
% 30.27/4.39 fof(f1,axiom,(
% 30.27/4.39 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f2,axiom,(
% 30.27/4.39 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f3,axiom,(
% 30.27/4.39 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f4,axiom,(
% 30.27/4.39 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f5,axiom,(
% 30.27/4.39 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f6,axiom,(
% 30.27/4.39 (! [X0] : composition(X0,one) = X0 )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f7,axiom,(
% 30.27/4.39 (! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f8,axiom,(
% 30.27/4.39 (! [X0] : converse(converse(X0)) = X0 )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f9,axiom,(
% 30.27/4.39 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f10,axiom,(
% 30.27/4.39 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f11,axiom,(
% 30.27/4.39 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f12,axiom,(
% 30.27/4.39 (! [X0] : top = join(X0,complement(X0)) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f13,axiom,(
% 30.27/4.39 (! [X0] : zero = meet(X0,complement(X0)) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f14,axiom,(
% 30.27/4.39 (! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f17,conjecture,(
% 30.27/4.39 (! [X0,X1] : join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0)) = complement(X0) )),
% 30.27/4.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.27/4.39 fof(f18,negated_conjecture,(
% 30.27/4.39 ~((! [X0,X1] : join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0)) = complement(X0) ))),
% 30.27/4.39 inference(negated_conjecture,[status(cth)],[f17])).
% 30.27/4.39 fof(f19,plain,(
% 30.27/4.39 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f1])).
% 30.27/4.39 fof(f20,plain,(
% 30.27/4.39 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f2])).
% 30.27/4.39 fof(f21,plain,(
% 30.27/4.39 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f3])).
% 30.27/4.39 fof(f22,plain,(
% 30.27/4.39 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f4])).
% 30.27/4.39 fof(f23,plain,(
% 30.27/4.39 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f5])).
% 30.27/4.39 fof(f24,plain,(
% 30.27/4.39 ![X0]: (composition(X0,one)=X0)),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f6])).
% 30.27/4.39 fof(f25,plain,(
% 30.27/4.39 ![X0,X1,X2]: (composition(join(X0,X1),X2)=join(composition(X0,X2),composition(X1,X2)))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f7])).
% 30.27/4.39 fof(f26,plain,(
% 30.27/4.39 ![X0]: (converse(converse(X0))=X0)),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f8])).
% 30.27/4.39 fof(f27,plain,(
% 30.27/4.39 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 30.27/4.39 inference(cnf_transformation,[status(thm)],[f9])).
% 30.27/4.39 fof(f28,plain,(
% 30.27/4.39 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f10])).
% 30.27/4.40 fof(f29,plain,(
% 30.27/4.40 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f11])).
% 30.27/4.40 fof(f30,plain,(
% 30.27/4.40 ![X0]: (top=join(X0,complement(X0)))),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f12])).
% 30.27/4.40 fof(f31,plain,(
% 30.27/4.40 ![X0]: (zero=meet(X0,complement(X0)))),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f13])).
% 30.27/4.40 fof(f32,plain,(
% 30.27/4.40 ![X0,X1,X2]: (join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))=composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))))),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f14])).
% 30.27/4.40 fof(f35,plain,(
% 30.27/4.40 (?[X0,X1]: ~join(composition(complement(composition(X0,X1)),converse(X1)),complement(X0))=complement(X0))),
% 30.27/4.40 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 30.27/4.40 fof(f36,plain,(
% 30.27/4.40 ~join(composition(complement(composition(sK0_skl,sK1_skl)),converse(sK1_skl)),complement(sK0_skl))=complement(sK0_skl)),
% 30.27/4.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f35])).
% 30.27/4.40 fof(f37,plain,(
% 30.27/4.40 ~join(composition(complement(composition(sK0_skl,sK1_skl)),converse(sK1_skl)),complement(sK0_skl))=complement(sK0_skl)),
% 30.27/4.40 inference(cnf_transformation,[status(thm)],[f36])).
% 30.27/4.40 fof(f38,definition,(
% 30.27/4.40 sF3_fnc=composition(sK0_skl,sK1_skl)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 30.27/4.40 fof(f39,definition,(
% 30.27/4.40 sF2_fnc=complement(sF3_fnc)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 30.27/4.40 fof(f40,definition,(
% 30.27/4.40 sF4_fnc=converse(sK1_skl)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 30.27/4.40 fof(f41,definition,(
% 30.27/4.40 sF1_fnc=composition(sF2_fnc,sF4_fnc)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 30.27/4.40 fof(f42,definition,(
% 30.27/4.40 sF5_fnc=complement(sK0_skl)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 30.27/4.40 fof(f43,definition,(
% 30.27/4.40 sF0_fnc=join(sF1_fnc,sF5_fnc)),
% 30.27/4.40 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 30.27/4.40 fof(f44,plain,(
% 30.27/4.40 ~sF0_fnc=sF5_fnc),
% 30.27/4.40 inference(definition_folding,[],[f37,f43,f42,f41,f40,f39,f38])).
% 30.27/4.40 fof(f45,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f21])).
% 30.27/4.40 fof(f46,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f22,f45])).
% 30.27/4.40 fof(f47,plain,(
% 30.27/4.40 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f29])).
% 30.27/4.40 fof(f48,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f46])).
% 30.27/4.40 fof(f50,plain,(
% 30.27/4.40 converse(sF4_fnc)=sK1_skl),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f40,f26])).
% 30.27/4.40 fof(f67,plain,(
% 30.27/4.40 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f22])).
% 30.27/4.40 fof(f69,plain,(
% 30.27/4.40 ![X0,X1,X2]: (meet(join(complement(X0),complement(X1)),X2)=complement(join(meet(X0,X1),complement(X2))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f22,f22])).
% 30.27/4.40 fof(f71,plain,(
% 30.27/4.40 ![X0]: (meet(sF3_fnc,X0)=complement(join(sF2_fnc,complement(X0))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f39,f22])).
% 30.27/4.40 fof(f73,plain,(
% 30.27/4.40 ![X0]: (meet(X0,sK0_skl)=complement(join(complement(X0),sF5_fnc)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f42,f22])).
% 30.27/4.40 fof(f74,plain,(
% 30.27/4.40 ![X0]: (meet(X0,sF3_fnc)=complement(join(complement(X0),sF2_fnc)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f39,f22])).
% 30.27/4.40 fof(f75,plain,(
% 30.27/4.40 ![X0]: (meet(X0,sK0_skl)=complement(join(sF5_fnc,complement(X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f73])).
% 30.27/4.40 fof(f76,plain,(
% 30.27/4.40 ![X0]: (meet(X0,sF3_fnc)=complement(join(sF2_fnc,complement(X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f74])).
% 30.27/4.40 fof(f77,plain,(
% 30.27/4.40 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f20])).
% 30.27/4.40 fof(f81,plain,(
% 30.27/4.40 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),X2))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f20])).
% 30.27/4.40 fof(f91,plain,(
% 30.27/4.40 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f26,f28])).
% 30.27/4.40 fof(f122,plain,(
% 30.27/4.40 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f26,f27])).
% 30.27/4.40 fof(f138,plain,(
% 30.27/4.40 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f24,f23])).
% 30.27/4.40 fof(f143,plain,(
% 30.27/4.40 ![X0,X1]: (zero=meet(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f22,f31])).
% 30.27/4.40 fof(f146,plain,(
% 30.27/4.40 ![X0,X1]: (zero=complement(join(meet(X0,X1),complement(meet(X0,X1)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f69,f143])).
% 30.27/4.40 fof(f147,plain,(
% 30.27/4.40 zero=complement(top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f30,f146])).
% 30.27/4.40 fof(f152,plain,(
% 30.27/4.40 ![X0,X1]: (top=join(X0,join(X1,complement(join(X0,X1)))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f20,f30])).
% 30.27/4.40 fof(f156,plain,(
% 30.27/4.40 top=join(sF3_fnc,sF2_fnc)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f39,f30])).
% 30.27/4.40 fof(f161,plain,(
% 30.27/4.40 top=join(sF2_fnc,sF3_fnc)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f156])).
% 30.27/4.40 fof(f206,plain,(
% 30.27/4.40 meet(sF3_fnc,sF3_fnc)=complement(join(sF2_fnc,sF2_fnc))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f39,f71])).
% 30.27/4.40 fof(f224,plain,(
% 30.27/4.40 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=complement(top))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f147,f47])).
% 30.27/4.40 fof(f242,plain,(
% 30.27/4.40 ![X0]: (join(zero,composition(converse(X0),complement(composition(X0,top))))=zero)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f147,f224])).
% 30.27/4.40 fof(f254,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,converse(sF4_fnc))),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,converse(sF4_fnc))),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f41,f32])).
% 30.27/4.40 fof(f256,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),composition(meet(sK0_skl,composition(X0,converse(sK1_skl))),meet(sK1_skl,composition(converse(sK0_skl),X0))))=composition(meet(sK0_skl,composition(X0,converse(sK1_skl))),meet(sK1_skl,composition(converse(sK0_skl),X0))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f38,f32])).
% 30.27/4.40 fof(f277,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,converse(sF4_fnc))),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f50,f254])).
% 30.27/4.40 fof(f278,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF1_fnc,X0),composition(meet(sF2_fnc,composition(X0,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))=composition(meet(sF2_fnc,composition(X0,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f50,f277])).
% 30.27/4.40 fof(f281,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))))=composition(meet(sK0_skl,composition(X0,converse(sK1_skl))),meet(sK1_skl,composition(converse(sK0_skl),X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f40,f256])).
% 30.27/4.40 fof(f282,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))))=composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f40,f281])).
% 30.27/4.40 fof(f597,plain,(
% 30.27/4.40 meet(sF2_fnc,sF3_fnc)=complement(top)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f30,f76])).
% 30.27/4.40 fof(f617,plain,(
% 30.27/4.40 meet(sF2_fnc,sF3_fnc)=zero),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f147,f597])).
% 30.27/4.40 fof(f709,plain,(
% 30.27/4.40 ![X0,X1]: (join(X0,join(X1,complement(join(X1,X0))))=top)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f30,f81])).
% 30.27/4.40 fof(f758,plain,(
% 30.27/4.40 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f31,f48])).
% 30.27/4.40 fof(f759,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f22,f48])).
% 30.27/4.40 fof(f761,plain,(
% 30.27/4.40 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f30,f48])).
% 30.27/4.40 fof(f785,plain,(
% 30.27/4.40 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f22,f758])).
% 30.27/4.40 fof(f786,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f759])).
% 30.27/4.40 fof(f788,plain,(
% 30.27/4.40 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f761])).
% 30.27/4.40 fof(f789,plain,(
% 30.27/4.40 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f147,f788])).
% 30.27/4.40 fof(f797,plain,(
% 30.27/4.40 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f22,f67])).
% 30.27/4.40 fof(f946,plain,(
% 30.27/4.40 top=join(zero,meet(top,complement(zero)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f147,f789])).
% 30.27/4.40 fof(f971,plain,(
% 30.27/4.40 ![X0,X1]: (X0=join(meet(X0,X1),meet(complement(X1),X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f797,f786])).
% 30.27/4.40 fof(f973,plain,(
% 30.27/4.40 ![X0]: (X0=join(meet(X0,top),meet(X0,zero)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f147,f786])).
% 30.27/4.40 fof(f999,plain,(
% 30.27/4.40 ![X0]: (X0=join(meet(X0,top),meet(zero,X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f797,f973])).
% 30.27/4.40 fof(f1024,plain,(
% 30.27/4.40 ![X0]: (X0=join(meet(zero,X0),meet(X0,top)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f999])).
% 30.27/4.40 fof(f1028,plain,(
% 30.27/4.40 complement(zero)=join(meet(complement(zero),top),zero)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f31,f999])).
% 30.27/4.40 fof(f1036,plain,(
% 30.27/4.40 complement(zero)=join(zero,meet(complement(zero),top))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f1028])).
% 30.27/4.40 fof(f1037,plain,(
% 30.27/4.40 complement(zero)=join(zero,meet(top,complement(zero)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f1036])).
% 30.27/4.40 fof(f1039,plain,(
% 30.27/4.40 complement(zero)=top),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f946,f1037])).
% 30.27/4.40 fof(f1792,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=join(meet(complement(complement(X0)),X0),zero))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f31,f971])).
% 30.27/4.40 fof(f1819,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=join(zero,meet(complement(complement(X0)),X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f1792])).
% 30.27/4.40 fof(f1820,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=join(zero,meet(X0,complement(complement(X0)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f1819])).
% 30.27/4.40 fof(f1827,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=X0)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f789,f1820])).
% 30.27/4.40 fof(f1846,plain,(
% 30.27/4.40 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X1),complement(X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f67,f1827])).
% 30.27/4.40 fof(f1847,plain,(
% 30.27/4.40 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f22,f1827])).
% 30.27/4.40 fof(f1854,plain,(
% 30.27/4.40 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f1827,f67])).
% 30.27/4.40 fof(f1857,plain,(
% 30.27/4.40 ![X0]: (meet(complement(X0),sF3_fnc)=complement(join(sF2_fnc,X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f1827,f76])).
% 30.27/4.40 fof(f1858,plain,(
% 30.27/4.40 ![X0]: (meet(complement(X0),sK0_skl)=complement(join(sF5_fnc,X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f1827,f75])).
% 30.27/4.40 fof(f1959,plain,(
% 30.27/4.40 ![X0]: (meet(sF3_fnc,complement(X0))=complement(join(sF2_fnc,X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f1857])).
% 30.27/4.40 fof(f1960,plain,(
% 30.27/4.40 ![X0]: (meet(sK0_skl,complement(X0))=complement(join(sF5_fnc,X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f1858])).
% 30.27/4.40 fof(f2100,plain,(
% 30.27/4.40 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f77])).
% 30.27/4.40 fof(f2266,plain,(
% 30.27/4.40 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f24,f91])).
% 30.27/4.40 fof(f2308,plain,(
% 30.27/4.40 ![X0]: (X0=composition(converse(one),X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f26,f2266])).
% 30.27/4.40 fof(f2348,plain,(
% 30.27/4.40 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f138,f2308])).
% 30.27/4.40 fof(f2349,plain,(
% 30.27/4.40 one=converse(one)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f24,f2308])).
% 30.27/4.40 fof(f2350,plain,(
% 30.27/4.40 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2308,f47])).
% 30.27/4.40 fof(f2368,plain,(
% 30.27/4.40 ![X0,X1]: (composition(join(converse(one),X0),X1)=join(X1,composition(X0,X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2308,f25])).
% 30.27/4.40 fof(f2389,plain,(
% 30.27/4.40 ![X0]: (composition(one,X0)=X0)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2308,f2348])).
% 30.27/4.40 fof(f2399,plain,(
% 30.27/4.40 ![X0]: (complement(meet(X0,composition(one,X0)))=complement(X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1847,f2350])).
% 30.27/4.40 fof(f2400,plain,(
% 30.27/4.40 ![X0]: (complement(meet(X0,X0))=complement(X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2389,f2399])).
% 30.27/4.40 fof(f2453,plain,(
% 30.27/4.40 ![X0,X1]: (composition(join(one,X0),X1)=join(X1,composition(X0,X1)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2349,f2368])).
% 30.27/4.40 fof(f2498,plain,(
% 30.27/4.40 ![X0]: (converse(join(one,X0))=join(one,converse(X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2349,f27])).
% 30.27/4.40 fof(f2580,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=meet(X0,X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2400,f1827])).
% 30.27/4.40 fof(f2589,plain,(
% 30.27/4.40 ![X0]: (X0=join(zero,X0))),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f2596,f785])).
% 30.27/4.40 fof(f2590,plain,(
% 30.27/4.40 sF3_fnc=complement(join(sF2_fnc,sF2_fnc))),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f2596,f206])).
% 30.27/4.40 fof(f2596,plain,(
% 30.27/4.40 ![X0]: (X0=meet(X0,X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1827,f2580])).
% 30.27/4.40 fof(f2617,plain,(
% 30.27/4.40 ![X0]: (composition(converse(X0),complement(composition(X0,top)))=zero)),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f2589,f242])).
% 30.27/4.40 fof(f2641,plain,(
% 30.27/4.40 ![X0]: (X0=join(X0,zero))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f19,f2589])).
% 30.27/4.40 fof(f2906,plain,(
% 30.27/4.40 top=join(join(sF2_fnc,sF2_fnc),sF3_fnc)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2590,f30])).
% 30.27/4.40 fof(f2922,plain,(
% 30.27/4.40 top=join(sF2_fnc,join(sF2_fnc,sF3_fnc))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f81,f2906])).
% 30.27/4.40 fof(f2923,plain,(
% 30.27/4.40 top=join(sF2_fnc,top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f161,f2922])).
% 30.27/4.40 fof(f2925,plain,(
% 30.27/4.40 top=join(top,sF2_fnc)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f2923])).
% 30.27/4.40 fof(f2932,plain,(
% 30.27/4.40 ![X0]: (join(top,join(sF2_fnc,X0))=join(X0,top))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2925,f77])).
% 30.27/4.40 fof(f4723,plain,(
% 30.27/4.40 ![X0]: (converse(converse(X0))=join(X0,converse(zero)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2641,f122])).
% 30.27/4.40 fof(f4780,plain,(
% 30.27/4.40 ![X0]: (X0=join(X0,converse(zero)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f26,f4723])).
% 30.27/4.40 fof(f4843,plain,(
% 30.27/4.40 zero=converse(zero)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2589,f4780])).
% 30.27/4.40 fof(f4912,plain,(
% 30.27/4.40 ![X0]: (converse(composition(zero,X0))=composition(converse(X0),zero))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f4843,f91])).
% 30.27/4.40 fof(f5927,plain,(
% 30.27/4.40 ![X0]: (complement(meet(X0,top))=join(zero,complement(X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f147,f1846])).
% 30.27/4.40 fof(f5940,plain,(
% 30.27/4.40 ![X0]: (complement(meet(zero,X0))=join(complement(X0),top))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f1039,f1846])).
% 30.27/4.40 fof(f5973,plain,(
% 30.27/4.40 ![X0]: (complement(meet(X0,top))=complement(X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2589,f5927])).
% 30.27/4.40 fof(f5988,plain,(
% 30.27/4.40 ![X0]: (complement(meet(zero,X0))=join(top,complement(X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f5940])).
% 30.27/4.40 fof(f6017,plain,(
% 30.27/4.40 ![X0]: (complement(complement(X0))=meet(X0,top))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f5973,f1827])).
% 30.27/4.40 fof(f6040,plain,(
% 30.27/4.40 ![X0]: (X0=join(meet(zero,X0),X0))),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f6060,f1024])).
% 30.27/4.40 fof(f6060,plain,(
% 30.27/4.40 ![X0]: (X0=meet(X0,top))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1827,f6017])).
% 30.27/4.40 fof(f6076,plain,(
% 30.27/4.40 ![X0]: (X0=join(X0,meet(zero,X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f6040])).
% 30.27/4.40 fof(f6086,plain,(
% 30.27/4.40 ![X0]: (X0=meet(top,X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f797,f6060])).
% 30.27/4.40 fof(f6678,plain,(
% 30.27/4.40 ![X0]: (meet(complement(meet(zero,complement(X0))),X0)=complement(complement(X0)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f6076,f1854])).
% 30.27/4.40 fof(f6726,plain,(
% 30.27/4.40 ![X0]: (meet(X0,complement(meet(zero,complement(X0))))=complement(complement(X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f6678])).
% 30.27/4.40 fof(f6727,plain,(
% 30.27/4.40 ![X0]: (meet(X0,join(top,complement(complement(X0))))=complement(complement(X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f5988,f6726])).
% 30.27/4.40 fof(f6728,plain,(
% 30.27/4.40 ![X0]: (meet(X0,join(top,X0))=complement(complement(X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1827,f6727])).
% 30.27/4.40 fof(f6730,plain,(
% 30.27/4.40 ![X0]: (meet(X0,join(top,X0))=X0)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1827,f6728])).
% 30.27/4.40 fof(f6773,plain,(
% 30.27/4.40 join(top,top)=top),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f6086,f6730])).
% 30.27/4.40 fof(f8809,plain,(
% 30.27/4.40 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f81,f2100])).
% 30.27/4.40 fof(f10376,plain,(
% 30.27/4.40 ![X0]: (join(top,top)=join(join(X0,complement(join(sF2_fnc,X0))),top))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f152,f2932])).
% 30.27/4.40 fof(f10429,plain,(
% 30.27/4.40 ![X0]: (top=join(join(X0,complement(join(sF2_fnc,X0))),top))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f6773,f10376])).
% 30.27/4.40 fof(f10430,plain,(
% 30.27/4.40 ![X0]: (top=join(complement(join(sF2_fnc,X0)),join(top,X0)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2100,f10429])).
% 30.27/4.40 fof(f10431,plain,(
% 30.27/4.40 ![X0]: (top=join(top,join(X0,complement(join(sF2_fnc,X0)))))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f77,f10430])).
% 30.27/4.40 fof(f10576,plain,(
% 30.27/4.40 join(meet(sF1_fnc,sK0_skl),composition(meet(sF2_fnc,sF3_fnc),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=composition(meet(sF2_fnc,composition(sK0_skl,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl)))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f38,f278])).
% 30.27/4.40 fof(f10607,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),composition(meet(sF2_fnc,sF3_fnc),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=composition(meet(sF2_fnc,composition(sK0_skl,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f10576])).
% 30.27/4.40 fof(f10608,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),composition(zero,meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=composition(meet(sF2_fnc,composition(sK0_skl,sK1_skl)),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f617,f10607])).
% 30.27/4.40 fof(f10609,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),composition(zero,meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=composition(meet(sF2_fnc,sF3_fnc),meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f38,f10608])).
% 30.27/4.40 fof(f10610,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),composition(zero,meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=composition(zero,meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl)))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f617,f10609])).
% 30.27/4.40 fof(f10627,plain,(
% 30.27/4.40 ![X0]: (composition(join(one,converse(X0)),complement(composition(join(one,X0),top)))=zero)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f2498,f2617])).
% 30.27/4.40 fof(f10677,plain,(
% 30.27/4.40 ![X0]: (composition(join(one,converse(X0)),complement(join(top,composition(X0,top))))=zero)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2453,f10627])).
% 30.27/4.40 fof(f14577,plain,(
% 30.27/4.40 ![X0]: (join(composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))),join(meet(sF3_fnc,X0),complement(composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))))))=top)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f282,f709])).
% 30.27/4.40 fof(f14616,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),join(complement(composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0)))),composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0)))))=top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f77,f14577])).
% 30.27/4.40 fof(f14617,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),join(composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))),complement(composition(meet(sK0_skl,composition(X0,sF4_fnc)),meet(sK1_skl,composition(converse(sK0_skl),X0))))))=top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f8809,f14616])).
% 30.27/4.40 fof(f14618,plain,(
% 30.27/4.40 ![X0]: (join(meet(sF3_fnc,X0),top)=top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f30,f14617])).
% 30.27/4.40 fof(f14619,plain,(
% 30.27/4.40 ![X0]: (join(top,meet(sF3_fnc,X0))=top)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f14618])).
% 30.27/4.40 fof(f15531,plain,(
% 30.27/4.40 ![X0]: (join(top,complement(join(sF2_fnc,X0)))=top)),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f1959,f14619])).
% 30.27/4.40 fof(f15613,plain,(
% 30.27/4.40 ![X0,X1]: (join(complement(join(sF2_fnc,X0)),join(top,X1))=join(top,X1))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f15531,f81])).
% 30.27/4.40 fof(f15635,plain,(
% 30.27/4.40 ![X0]: (top=join(top,X0))),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f15636,f10431])).
% 30.27/4.40 fof(f15636,plain,(
% 30.27/4.40 ![X0,X1]: (join(top,join(X0,complement(join(sF2_fnc,X1))))=join(top,X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f77,f15613])).
% 30.27/4.40 fof(f15681,plain,(
% 30.27/4.40 ![X0]: (composition(join(one,converse(X0)),complement(top))=zero)),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f15635,f10677])).
% 30.27/4.40 fof(f15884,plain,(
% 30.27/4.40 ![X0]: (composition(join(one,converse(X0)),zero)=zero)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f147,f15681])).
% 30.27/4.40 fof(f15885,plain,(
% 30.27/4.40 ![X0]: (join(zero,composition(converse(X0),zero))=zero)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2453,f15884])).
% 30.27/4.40 fof(f15889,plain,(
% 30.27/4.40 ![X0]: (converse(composition(zero,X0))=zero)),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f15890,f4912])).
% 30.27/4.40 fof(f15890,plain,(
% 30.27/4.40 ![X0]: (composition(converse(X0),zero)=zero)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2589,f15885])).
% 30.27/4.40 fof(f16645,plain,(
% 30.27/4.40 ![X0]: (converse(zero)=composition(zero,X0))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f15889,f26])).
% 30.27/4.40 fof(f16819,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),composition(zero,meet(sF4_fnc,composition(converse(sF2_fnc),sK0_skl))))=zero),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f16840,f10610])).
% 30.27/4.40 fof(f16840,plain,(
% 30.27/4.40 ![X0]: (zero=composition(zero,X0))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f4843,f16645])).
% 30.27/4.40 fof(f16927,plain,(
% 30.27/4.40 join(meet(sK0_skl,sF1_fnc),zero)=zero),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f16840,f16819])).
% 30.27/4.40 fof(f16928,plain,(
% 30.27/4.40 meet(sK0_skl,sF1_fnc)=zero),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2641,f16927])).
% 30.27/4.40 fof(f16957,plain,(
% 30.27/4.40 sK0_skl=join(zero,meet(complement(sF1_fnc),sK0_skl))),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f16928,f971])).
% 30.27/4.40 fof(f16973,plain,(
% 30.27/4.40 sK0_skl=meet(complement(sF1_fnc),sK0_skl)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f2589,f16957])).
% 30.27/4.40 fof(f16974,plain,(
% 30.27/4.40 sK0_skl=meet(sK0_skl,complement(sF1_fnc))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f797,f16973])).
% 30.27/4.40 fof(f16975,plain,(
% 30.27/4.40 sK0_skl=complement(join(sF5_fnc,sF1_fnc))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f1960,f16974])).
% 30.27/4.40 fof(f16976,plain,(
% 30.27/4.40 sK0_skl=complement(join(sF1_fnc,sF5_fnc))),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f19,f16975])).
% 30.27/4.40 fof(f16978,plain,(
% 30.27/4.40 sK0_skl=complement(sF0_fnc)),
% 30.27/4.40 inference(forward_demodulation,[status(thm)],[f43,f16976])).
% 30.27/4.40 fof(f17001,plain,(
% 30.27/4.40 complement(sK0_skl)=sF0_fnc),
% 30.27/4.40 inference(paramodulation,[status(thm)],[f16978,f1827])).
% 30.27/4.40 fof(f17022,plain,(
% 30.27/4.40 sF5_fnc=sF0_fnc),
% 30.27/4.40 inference(backward_demodulation,[status(thm)],[f17001,f42])).
% 30.27/4.40 fof(f17028,plain,(
% 30.27/4.40 $false),
% 30.27/4.40 inference(forward_subsumption_resolution,[status(thm)],[f17022,f44])).
% 30.27/4.40 % SZS output end CNFRefutation for theBenchmark.p
% 22.96/4.52 % Elapsed time: 4.055367 seconds
% 22.96/4.52 % CPU time: 31.500085 seconds
% 22.96/4.52 % Total memory used: 300.911 MB
% 22.96/4.52 % Net memory used: 295.033 MB
%------------------------------------------------------------------------------