%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB093+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 : n020.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 42.87s 5.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB093+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 07:47:35 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 42.87/5.98 % Refutation found
% 42.87/5.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 42.87/5.98 % SZS output start CNFRefutation for theBenchmark
% 42.87/5.98 fof(f159,axiom,(
% 42.87/5.98 (! [X] :( icext(uri_owl_Restriction,X)=> ic(X) ) )),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f233,axiom,(
% 42.87/5.98 (! [X,Y] :( iext(uri_owl_minQualifiedCardinality,X,Y)=> ( icext(uri_owl_Restriction,X)& icext(uri_xml_nonNegativeInteger,Y) ) ) )),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f337,axiom,(
% 42.87/5.98 (! [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) ) )) )) )),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f338,axiom,(
% 42.87/5.98 (! [Z,P,C] :( ( iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,Z,P)& iext(uri_owl_onClass,Z,C) )=> (! [X] :( icext(Z,X)<=> (? [Y1,Y2] :( iext(P,X,Y1)& icext(C,Y1)& iext(P,X,Y2)& icext(C,Y2)& Y1 != Y2 ) )) )) )),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f343,axiom,(
% 42.87/5.98 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f559,conjecture,(
% 42.87/5.98 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) ),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f560,negated_conjecture,(
% 42.87/5.98 ~(iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) )),
% 42.87/5.98 inference(negated_conjecture,[status(cth)],[f559])).
% 42.87/5.98 fof(f561,axiom,(
% 42.87/5.98 ( iext(uri_owl_minQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)& iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)& iext(uri_owl_minQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p)& iext(uri_owl_onClass,uri_ex_x1,uri_ex_c) ) ),
% 42.87/5.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 42.87/5.98 fof(f853,plain,(
% 42.87/5.98 ![X]: (~icext(uri_owl_Restriction,X)|ic(X))),
% 42.87/5.98 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 42.87/5.98 fof(f854,plain,(
% 42.87/5.98 ![X0]: (~icext(uri_owl_Restriction,X0)|ic(X0))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f853])).
% 42.87/5.98 fof(f993,plain,(
% 42.87/5.98 ![X,Y]: (~iext(uri_owl_minQualifiedCardinality,X,Y)|(icext(uri_owl_Restriction,X)&icext(uri_xml_nonNegativeInteger,Y)))),
% 42.87/5.98 inference(pre_NNF_transformation,[status(thm)],[f233])).
% 42.87/5.98 fof(f994,plain,(
% 42.87/5.98 ![X0,X1]: (~iext(uri_owl_minQualifiedCardinality,X0,X1)|icext(uri_owl_Restriction,X0))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f993])).
% 42.87/5.98 fof(f1675,plain,(
% 42.87/5.98 ![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))))))),
% 42.87/5.98 inference(pre_NNF_transformation,[status(thm)],[f337])).
% 42.87/5.98 fof(f1676,plain,(
% 42.87/5.98 ![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)))))))),
% 42.87/5.98 inference(NNF_transformation,[status(thm)],[f1675])).
% 42.87/5.98 fof(f1677,plain,(
% 42.87/5.98 ![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)))))))),
% 42.87/5.98 inference(miniscoping,[status(thm)],[f1676])).
% 42.87/5.98 fof(f1678,plain,(
% 42.87/5.98 ![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)))))))),
% 42.87/5.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK104_skl]),skolemize(Y,sK104_skl(X,C,P,Z))],[f1677])).
% 42.87/5.98 fof(f1681,plain,(
% 42.87/5.98 ![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))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f1678])).
% 42.87/5.98 fof(f1682,plain,(
% 42.87/5.98 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|(![X]: (icext(Z,X)<=>(?[Y1,Y2]: ((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&~Y1=Y2)))))),
% 42.87/5.98 inference(pre_NNF_transformation,[status(thm)],[f338])).
% 42.87/5.98 fof(f1683,plain,(
% 42.87/5.98 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|(![X]: ((~icext(Z,X)|(?[Y1,Y2]: ((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&~Y1=Y2)))&(icext(Z,X)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y1=Y2))))))),
% 42.87/5.98 inference(NNF_transformation,[status(thm)],[f1682])).
% 42.87/5.98 fof(f1684,plain,(
% 42.87/5.98 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|((![X]: (~icext(Z,X)|(?[Y1,Y2]: ((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&~Y1=Y2))))&(![X]: (icext(Z,X)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y1=Y2))))))),
% 42.87/5.98 inference(miniscoping,[status(thm)],[f1683])).
% 42.87/5.98 fof(f1685,plain,(
% 42.87/5.98 ![Z,P,C]: (((~iext(uri_owl_minQualifiedCardinality,Z,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,Z,P))|~iext(uri_owl_onClass,Z,C))|((![X]: (~icext(Z,X)|((((iext(P,X,sK105_skl(X,C,P,Z))&icext(C,sK105_skl(X,C,P,Z)))&iext(P,X,sK106_skl(X,C,P,Z)))&icext(C,sK106_skl(X,C,P,Z)))&~sK105_skl(X,C,P,Z)=sK106_skl(X,C,P,Z))))&(![X]: (icext(Z,X)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y1=Y2))))))),
% 42.87/5.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK105_skl,sK106_skl]),skolemize(Y1,sK105_skl(X,C,P,Z)),skolemize(Y2,sK106_skl(X,C,P,Z))],[f1684])).
% 42.87/5.98 fof(f1688,plain,(
% 42.87/5.98 ![X0,X1,X2,X3]: (~iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|~icext(X0,X3)|iext(X1,X3,sK106_skl(X3,X2,X1,X0)))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f1685])).
% 42.87/5.98 fof(f1689,plain,(
% 42.87/5.98 ![X0,X1,X2,X3]: (~iext(uri_owl_minQualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|~icext(X0,X3)|icext(X2,sK106_skl(X3,X2,X1,X0)))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f1685])).
% 42.87/5.98 fof(f1731,plain,(
% 42.87/5.98 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 42.87/5.98 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 42.87/5.98 fof(f1732,plain,(
% 42.87/5.98 ![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))))))),
% 42.87/5.98 inference(NNF_transformation,[status(thm)],[f1731])).
% 42.87/5.98 fof(f1733,plain,(
% 42.87/5.98 (![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))))))),
% 42.87/5.98 inference(miniscoping,[status(thm)],[f1732])).
% 42.87/5.98 fof(f1734,plain,(
% 42.87/5.98 (![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))))))),
% 42.87/5.98 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 42.87/5.98 fof(f1738,plain,(
% 42.87/5.98 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f1734])).
% 42.87/5.98 fof(f1739,plain,(
% 42.87/5.98 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f1734])).
% 42.87/5.98 fof(f2405,plain,(
% 42.87/5.98 ~iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f560])).
% 42.87/5.98 fof(f2406,plain,(
% 42.87/5.98 iext(uri_owl_minQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f2407,plain,(
% 42.87/5.98 iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f2408,plain,(
% 42.87/5.98 iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f2409,plain,(
% 42.87/5.98 iext(uri_owl_minQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f2410,plain,(
% 42.87/5.98 iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p)),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f2411,plain,(
% 42.87/5.98 iext(uri_owl_onClass,uri_ex_x1,uri_ex_c)),
% 42.87/5.98 inference(cnf_transformation,[status(thm)],[f561])).
% 42.87/5.98 fof(f5960,plain,(
% 42.87/5.98 icext(uri_owl_Restriction,uri_ex_x1)),
% 42.87/5.98 inference(resolution,[status(thm)],[f994,f2409])).
% 42.87/5.98 fof(f5961,plain,(
% 42.87/5.98 icext(uri_owl_Restriction,uri_ex_x2)),
% 42.87/5.98 inference(resolution,[status(thm)],[f994,f2406])).
% 42.87/5.98 fof(f5964,plain,(
% 42.87/5.98 ic(uri_ex_x1)),
% 42.87/5.98 inference(resolution,[status(thm)],[f5960,f854])).
% 42.87/5.98 fof(f5998,plain,(
% 42.87/5.98 ic(uri_ex_x2)),
% 42.87/5.98 inference(resolution,[status(thm)],[f5961,f854])).
% 42.87/5.98 fof(f16906,plain,(
% 42.87/5.98 ![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))),
% 42.87/5.98 inference(resolution,[status(thm)],[f1681,f2406])).
% 42.87/5.98 fof(f16908,plain,(
% 42.87/5.98 ![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))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16906,f2408])).
% 42.87/5.98 fof(f16909,plain,(
% 42.87/5.98 ![X0,X1]: (icext(uri_ex_x2,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c,X1))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16908,f2407])).
% 42.87/5.98 fof(f16942,plain,(
% 42.87/5.98 ![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,sK106_skl(X2,X1,X0,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f1688,f2409])).
% 42.87/5.98 fof(f16943,plain,(
% 42.87/5.98 ![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,sK106_skl(X2,X1,X0,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f1689,f2409])).
% 42.87/5.98 fof(f16976,plain,(
% 42.87/5.98 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|iext(uri_ex_p,X1,sK106_skl(X1,X0,uri_ex_p,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16942,f2410])).
% 42.87/5.98 fof(f16977,plain,(
% 42.87/5.98 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|icext(X0,sK106_skl(X1,X0,uri_ex_p,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16943,f2410])).
% 42.87/5.98 fof(f16979,plain,(
% 42.87/5.98 ![X0]: (~icext(uri_ex_x1,X0)|icext(uri_ex_c,sK106_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16977,f2411])).
% 42.87/5.98 fof(f16999,plain,(
% 42.87/5.98 ![X0]: (~icext(uri_ex_x1,X0)|iext(uri_ex_p,X0,sK106_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f16976,f2411])).
% 42.87/5.98 fof(f17940,plain,(
% 42.87/5.98 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_x1,X0)|~ic(X0)|icext(uri_ex_x1,sK115_skl(X0,uri_ex_x1)))),
% 42.87/5.98 inference(resolution,[status(thm)],[f1738,f5964])).
% 42.87/5.98 fof(f20188,plain,(
% 42.87/5.98 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 42.87/5.98 inference(resolution,[status(thm)],[f17940,f5998])).
% 42.87/5.98 fof(f20227,plain,(
% 42.87/5.98 icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 42.87/5.98 inference(forward_subsumption_resolution,[status(thm)],[f20188,f2405])).
% 42.87/5.98 fof(f20228,plain,(
% 42.87/5.98 iext(uri_ex_p,sK115_skl(uri_ex_x2,uri_ex_x1),sK106_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x1))),
% 42.87/5.98 inference(resolution,[status(thm)],[f20227,f16999])).
% 42.87/5.98 fof(f20229,plain,(
% 42.87/5.98 icext(uri_ex_c,sK106_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x1))),
% 42.87/5.98 inference(resolution,[status(thm)],[f20227,f16979])).
% 42.87/5.98 fof(f20529,plain,(
% 42.87/5.98 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))|~icext(uri_ex_c,sK106_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x1))),
% 42.87/6.01 inference(resolution,[status(thm)],[f20228,f16909])).
% 42.87/6.01 fof(f20534,plain,(
% 42.87/6.01 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 42.87/6.01 inference(forward_subsumption_resolution,[status(thm)],[f20529,f20229])).
% 42.87/6.01 fof(f20873,plain,(
% 42.87/6.01 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 42.87/6.01 inference(resolution,[status(thm)],[f20534,f1739])).
% 42.87/6.01 fof(f20882,plain,(
% 42.87/6.01 ~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 42.87/6.01 inference(forward_subsumption_resolution,[status(thm)],[f20873,f2405])).
% 42.87/6.01 fof(f20883,plain,(
% 42.87/6.01 ~ic(uri_ex_x1)),
% 42.87/6.01 inference(resolution,[status(thm)],[f20882,f5998])).
% 42.87/6.01 fof(f20884,plain,(
% 42.87/6.01 $false),
% 42.87/6.01 inference(forward_subsumption_resolution,[status(thm)],[f20883,f5964])).
% 42.87/6.01 % SZS output end CNFRefutation for theBenchmark.p
% 13.23/6.06 % Elapsed time: 5.674016 seconds
% 13.23/6.06 % CPU time: 43.701030 seconds
% 13.23/6.06 % Total memory used: 242.819 MB
% 13.23/6.06 % Net memory used: 229.821 MB
%------------------------------------------------------------------------------