%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB095+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:37:46 PM UTC 2026
% Result : Theorem 118.49s 15.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB095+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 07:46:35 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.26/0.52 % Drodi V4.1.1
% 118.49/15.72 % Refutation found
% 118.49/15.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 118.49/15.72 % SZS output start CNFRefutation for theBenchmark
% 118.49/15.72 fof(f73,axiom,(
% 118.49/15.72 (! [P,Q] :( iext(uri_rdfs_subPropertyOf,P,Q)=> ( ip(P)& ip(Q)& (! [X,Y] :( iext(P,X,Y)=> iext(Q,X,Y) ) )) ) )),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f159,axiom,(
% 118.49/15.72 (! [X] :( icext(uri_owl_Restriction,X)=> ic(X) ) )),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f233,axiom,(
% 118.49/15.72 (! [X,Y] :( iext(uri_owl_minQualifiedCardinality,X,Y)=> ( icext(uri_owl_Restriction,X)& icext(uri_xml_nonNegativeInteger,Y) ) ) )),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f337,axiom,(
% 118.49/15.72 (! [Z,P,C] :( ( iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,Z,P)& iext(uri_owl_onClass,Z,C) )=> (! [X] :( icext(Z,X)<=> (? [Y] :( iext(P,X,Y)& icext(C,Y) ) )) )) )),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f343,axiom,(
% 118.49/15.72 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f559,conjecture,(
% 118.49/15.72 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) ),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f560,negated_conjecture,(
% 118.49/15.72 ~(iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) )),
% 118.49/15.72 inference(negated_conjecture,[status(cth)],[f559])).
% 118.49/15.72 fof(f561,axiom,(
% 118.49/15.72 ( iext(uri_owl_minQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p2)& iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)& iext(uri_owl_minQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p1)& iext(uri_owl_onClass,uri_ex_x1,uri_ex_c)& iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2) ) ),
% 118.49/15.72 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 118.49/15.72 fof(f665,plain,(
% 118.49/15.72 ![P,Q]: (~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X,Y]: (~iext(P,X,Y)|iext(Q,X,Y)))))),
% 118.49/15.72 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 118.49/15.72 fof(f668,plain,(
% 118.49/15.72 ![X0,X1,X2,X3]: (~iext(uri_rdfs_subPropertyOf,X0,X1)|~iext(X0,X2,X3)|iext(X1,X2,X3))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f665])).
% 118.49/15.72 fof(f853,plain,(
% 118.49/15.72 ![X]: (~icext(uri_owl_Restriction,X)|ic(X))),
% 118.49/15.72 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 118.49/15.72 fof(f854,plain,(
% 118.49/15.72 ![X0]: (~icext(uri_owl_Restriction,X0)|ic(X0))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f853])).
% 118.49/15.72 fof(f993,plain,(
% 118.49/15.72 ![X,Y]: (~iext(uri_owl_minQualifiedCardinality,X,Y)|(icext(uri_owl_Restriction,X)&icext(uri_xml_nonNegativeInteger,Y)))),
% 118.49/15.72 inference(pre_NNF_transformation,[status(thm)],[f233])).
% 118.49/15.72 fof(f994,plain,(
% 118.49/15.72 ![X0,X1]: (~iext(uri_owl_minQualifiedCardinality,X0,X1)|icext(uri_owl_Restriction,X0))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f993])).
% 118.49/15.72 fof(f1675,plain,(
% 118.49/15.72 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|(![X]: (icext(Z,X)<=>(?[Y]: (iext(P,X,Y)&icext(C,Y))))))),
% 118.49/15.72 inference(pre_NNF_transformation,[status(thm)],[f337])).
% 118.49/15.72 fof(f1676,plain,(
% 118.49/15.72 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|(![X]: ((~icext(Z,X)|(?[Y]: (iext(P,X,Y)&icext(C,Y))))&(icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 118.49/15.72 inference(NNF_transformation,[status(thm)],[f1675])).
% 118.49/15.72 fof(f1677,plain,(
% 118.49/15.72 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|((![X]: (~icext(Z,X)|(?[Y]: (iext(P,X,Y)&icext(C,Y)))))&(![X]: (icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 118.49/15.72 inference(miniscoping,[status(thm)],[f1676])).
% 118.49/15.72 fof(f1678,plain,(
% 118.49/15.72 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|((![X]: (~icext(Z,X)|(iext(P,X,sK104_skl(X,C,P,Z))&icext(C,sK104_skl(X,C,P,Z)))))&(![X]: (icext(Z,X)|(![Y]: (~iext(P,X,Y)|~icext(C,Y)))))))),
% 118.49/15.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK104_skl]),skolemize(Y,sK104_skl(X,C,P,Z))],[f1677])).
% 118.49/15.72 fof(f1679,plain,(
% 118.49/15.72 ![X0,X1,X2,X3]: (~iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|~icext(X0,X3)|iext(X1,X3,sK104_skl(X3,X2,X1,X0)))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f1678])).
% 118.49/15.72 fof(f1680,plain,(
% 118.49/15.72 ![X0,X1,X2,X3]: (~iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|~icext(X0,X3)|icext(X2,sK104_skl(X3,X2,X1,X0)))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f1678])).
% 118.49/15.72 fof(f1681,plain,(
% 118.49/15.72 ![X0,X1,X2,X3,X4]: (~iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|icext(X0,X3)|~iext(X1,X3,X4)|~icext(X2,X4))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f1678])).
% 118.49/15.72 fof(f1731,plain,(
% 118.49/15.72 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 118.49/15.72 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 118.49/15.72 fof(f1732,plain,(
% 118.49/15.72 ![C1,C2]: ((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))&(iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 118.49/15.72 inference(NNF_transformation,[status(thm)],[f1731])).
% 118.49/15.72 fof(f1733,plain,(
% 118.49/15.72 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 118.49/15.72 inference(miniscoping,[status(thm)],[f1732])).
% 118.49/15.72 fof(f1734,plain,(
% 118.49/15.72 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(icext(C1,sK115_skl(C2,C1))&~icext(C2,sK115_skl(C2,C1))))))),
% 118.49/15.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 118.49/15.72 fof(f1738,plain,(
% 118.49/15.72 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f1734])).
% 118.49/15.72 fof(f1739,plain,(
% 118.49/15.72 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f1734])).
% 118.49/15.72 fof(f2405,plain,(
% 118.49/15.72 ~iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f560])).
% 118.49/15.72 fof(f2406,plain,(
% 118.49/15.72 iext(uri_owl_minQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2407,plain,(
% 118.49/15.72 iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p2)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2408,plain,(
% 118.49/15.72 iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2409,plain,(
% 118.49/15.72 iext(uri_owl_minQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2410,plain,(
% 118.49/15.72 iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p1)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2411,plain,(
% 118.49/15.72 iext(uri_owl_onClass,uri_ex_x1,uri_ex_c)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2412,plain,(
% 118.49/15.72 iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2)),
% 118.49/15.72 inference(cnf_transformation,[status(thm)],[f561])).
% 118.49/15.72 fof(f2982,plain,(
% 118.49/15.72 ![X0,X1]: (~iext(uri_ex_p1,X0,X1)|iext(uri_ex_p2,X0,X1))),
% 118.49/15.72 inference(resolution,[status(thm)],[f668,f2412])).
% 118.49/15.72 fof(f5969,plain,(
% 118.49/15.72 icext(uri_owl_Restriction,uri_ex_x1)),
% 118.49/15.72 inference(resolution,[status(thm)],[f994,f2409])).
% 118.49/15.72 fof(f5970,plain,(
% 118.49/15.72 icext(uri_owl_Restriction,uri_ex_x2)),
% 118.49/15.72 inference(resolution,[status(thm)],[f994,f2406])).
% 118.49/15.72 fof(f5973,plain,(
% 118.49/15.72 ic(uri_ex_x1)),
% 118.49/15.72 inference(resolution,[status(thm)],[f5969,f854])).
% 118.49/15.72 fof(f6007,plain,(
% 118.49/15.80 ic(uri_ex_x2)),
% 118.49/15.80 inference(resolution,[status(thm)],[f5970,f854])).
% 118.49/15.80 fof(f16876,plain,(
% 118.49/15.80 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x1,X0)|~iext(uri_owl_onClass,uri_ex_x1,X1)|~icext(uri_ex_x1,X2)|iext(X0,X2,sK104_skl(X2,X1,X0,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f1679,f2409])).
% 118.49/15.80 fof(f16878,plain,(
% 118.49/15.80 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|iext(uri_ex_p1,X1,sK104_skl(X1,X0,uri_ex_p1,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16876,f2410])).
% 118.49/15.80 fof(f16900,plain,(
% 118.49/15.80 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x1,X0)|~iext(uri_owl_onClass,uri_ex_x1,X1)|~icext(uri_ex_x1,X2)|icext(X1,sK104_skl(X2,X1,X0,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f1680,f2409])).
% 118.49/15.80 fof(f16903,plain,(
% 118.49/15.80 ![X0,X1,X2,X3]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|~iext(uri_owl_onClass,uri_ex_x2,X1)|icext(uri_ex_x2,X2)|~iext(X0,X2,X3)|~icext(X1,X3))),
% 118.49/15.80 inference(resolution,[status(thm)],[f1681,f2406])).
% 118.49/15.80 fof(f16905,plain,(
% 118.49/15.80 ![X0]: (~icext(uri_ex_x1,X0)|iext(uri_ex_p1,X0,sK104_skl(X0,uri_ex_c,uri_ex_p1,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16878,f2411])).
% 118.49/15.80 fof(f16914,plain,(
% 118.49/15.80 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|~iext(X0,X1,X2)|~icext(uri_ex_c,X2))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16903,f2408])).
% 118.49/15.80 fof(f16915,plain,(
% 118.49/15.80 ![X0,X1]: (icext(uri_ex_x2,X0)|~iext(uri_ex_p2,X0,X1)|~icext(uri_ex_c,X1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16914,f2407])).
% 118.49/15.80 fof(f16916,plain,(
% 118.49/15.80 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|icext(X0,sK104_skl(X1,X0,uri_ex_p1,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16900,f2410])).
% 118.49/15.80 fof(f16918,plain,(
% 118.49/15.80 ![X0]: (~icext(uri_ex_x1,X0)|icext(uri_ex_c,sK104_skl(X0,uri_ex_c,uri_ex_p1,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f16916,f2411])).
% 118.49/15.80 fof(f18009,plain,(
% 118.49/15.80 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_x1,X0)|~ic(X0)|icext(uri_ex_x1,sK115_skl(X0,uri_ex_x1)))),
% 118.49/15.80 inference(resolution,[status(thm)],[f1738,f5973])).
% 118.49/15.80 fof(f20284,plain,(
% 118.49/15.80 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f18009,f6007])).
% 118.49/15.80 fof(f20323,plain,(
% 118.49/15.80 icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 118.49/15.80 inference(forward_subsumption_resolution,[status(thm)],[f20284,f2405])).
% 118.49/15.80 fof(f20324,plain,(
% 118.49/15.80 icext(uri_ex_c,sK104_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p1,uri_ex_x1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f20323,f16918])).
% 118.49/15.80 fof(f20325,plain,(
% 118.49/15.80 iext(uri_ex_p1,sK115_skl(uri_ex_x2,uri_ex_x1),sK104_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p1,uri_ex_x1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f20323,f16905])).
% 118.49/15.80 fof(f20620,plain,(
% 118.49/15.80 iext(uri_ex_p2,sK115_skl(uri_ex_x2,uri_ex_x1),sK104_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p1,uri_ex_x1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f20325,f2982])).
% 118.49/15.80 fof(f22710,plain,(
% 118.49/15.80 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))|~icext(uri_ex_c,sK104_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p1,uri_ex_x1))),
% 118.49/15.80 inference(resolution,[status(thm)],[f20620,f16915])).
% 118.49/15.80 fof(f22715,plain,(
% 118.49/15.80 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 118.49/15.80 inference(forward_subsumption_resolution,[status(thm)],[f22710,f20324])).
% 118.49/15.80 fof(f22725,plain,(
% 118.49/15.80 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 118.49/15.80 inference(resolution,[status(thm)],[f22715,f1739])).
% 118.49/15.80 fof(f22734,plain,(
% 118.49/15.80 ~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 118.49/15.80 inference(forward_subsumption_resolution,[status(thm)],[f22725,f2405])).
% 118.49/15.80 fof(f22735,plain,(
% 118.49/15.80 ~ic(uri_ex_x1)),
% 118.49/15.80 inference(resolution,[status(thm)],[f22734,f6007])).
% 118.49/15.80 fof(f22736,plain,(
% 118.49/15.80 $false),
% 118.49/15.80 inference(forward_subsumption_resolution,[status(thm)],[f22735,f5973])).
% 118.49/15.80 % SZS output end CNFRefutation for theBenchmark.p
% 7.36/15.82 % Elapsed time: 15.349975 seconds
% 7.36/15.82 % CPU time: 120.560641 seconds
% 7.36/15.82 % Total memory used: 373.114 MB
% 7.36/15.82 % Net memory used: 345.579 MB
%------------------------------------------------------------------------------