%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB089+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 : 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:37:46 PM UTC 2026
% Result : Theorem 76.28s 35.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB089+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.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/25.32 % CPULimit : 300
% 0.08/25.32 % WCLimit : 300
% 0.08/25.32 % DateTime : Mon Sep 21 07:46:31 UTC 2026
% 0.08/25.32 % CPUTime :
% 0.08/25.37 % Drodi V4.1.1
% 76.28/35.06 % Refutation found
% 76.28/35.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.28/35.06 % SZS output start CNFRefutation for theBenchmark
% 76.28/35.06 fof(f68,axiom,(
% 76.28/35.06 (! [C,D] :( iext(uri_rdfs_subClassOf,C,D)=> ( ic(C)& ic(D)& (! [X] :( icext(C,X)=> icext(D,X) ) )) ) )),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f159,axiom,(
% 76.28/35.06 (! [X] :( icext(uri_owl_Restriction,X)=> ic(X) ) )),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f227,axiom,(
% 76.28/35.06 (! [X,Y] :( iext(uri_owl_maxQualifiedCardinality,X,Y)=> ( icext(uri_owl_Restriction,X)& icext(uri_xml_nonNegativeInteger,Y) ) ) )),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f325,axiom,(
% 76.28/35.06 (! [Z,P,C] :( ( iext(uri_owl_maxQualifiedCardinality,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)<=> (! [Y1,Y2] :( ( iext(P,X,Y1)& icext(C,Y1)& iext(P,X,Y2)& icext(C,Y2) )=> Y2 = Y1 ) )) )) )),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f343,axiom,(
% 76.28/35.06 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f559,conjecture,(
% 76.28/35.06 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) ),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f560,negated_conjecture,(
% 76.28/35.06 ~(iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) )),
% 76.28/35.06 inference(negated_conjecture,[status(cth)],[f559])).
% 76.28/35.06 fof(f561,axiom,(
% 76.28/35.06 ( iext(uri_owl_maxQualifiedCardinality,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_c2)& iext(uri_rdfs_subClassOf,uri_ex_c2,uri_ex_c1)& iext(uri_owl_maxQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))& iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p)& iext(uri_owl_onClass,uri_ex_x1,uri_ex_c1) ) ),
% 76.28/35.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 76.28/35.06 fof(f654,plain,(
% 76.28/35.06 ![C,D]: (~iext(uri_rdfs_subClassOf,C,D)|((ic(C)&ic(D))&(![X]: (~icext(C,X)|icext(D,X)))))),
% 76.28/35.06 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 76.28/35.06 fof(f657,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f654])).
% 76.28/35.06 fof(f853,plain,(
% 76.28/35.06 ![X]: (~icext(uri_owl_Restriction,X)|ic(X))),
% 76.28/35.06 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 76.28/35.06 fof(f854,plain,(
% 76.28/35.06 ![X0]: (~icext(uri_owl_Restriction,X0)|ic(X0))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f853])).
% 76.28/35.06 fof(f981,plain,(
% 76.28/35.06 ![X,Y]: (~iext(uri_owl_maxQualifiedCardinality,X,Y)|(icext(uri_owl_Restriction,X)&icext(uri_xml_nonNegativeInteger,Y)))),
% 76.28/35.06 inference(pre_NNF_transformation,[status(thm)],[f227])).
% 76.28/35.06 fof(f982,plain,(
% 76.28/35.06 ![X0,X1]: (~iext(uri_owl_maxQualifiedCardinality,X0,X1)|icext(uri_owl_Restriction,X0))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f981])).
% 76.28/35.06 fof(f1561,plain,(
% 76.28/35.06 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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)<=>(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y2=Y1)))))),
% 76.28/35.06 inference(pre_NNF_transformation,[status(thm)],[f325])).
% 76.28/35.06 fof(f1562,plain,(
% 76.28/35.06 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y2=Y1)))&(icext(Z,X)|(?[Y1,Y2]: ((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&~Y2=Y1))))))),
% 76.28/35.06 inference(NNF_transformation,[status(thm)],[f1561])).
% 76.28/35.06 fof(f1563,plain,(
% 76.28/35.06 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y2=Y1))))&(![X]: (icext(Z,X)|(?[Y1,Y2]: ((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&~Y2=Y1))))))),
% 76.28/35.06 inference(miniscoping,[status(thm)],[f1562])).
% 76.28/35.06 fof(f1564,plain,(
% 76.28/35.06 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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)|(![Y1,Y2]: ((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|Y2=Y1))))&(![X]: (icext(Z,X)|((((iext(P,X,sK83_skl(X,C,P,Z))&icext(C,sK83_skl(X,C,P,Z)))&iext(P,X,sK84_skl(X,C,P,Z)))&icext(C,sK84_skl(X,C,P,Z)))&~sK84_skl(X,C,P,Z)=sK83_skl(X,C,P,Z))))))),
% 76.28/35.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK83_skl,sK84_skl]),skolemize(Y1,sK83_skl(X,C,P,Z)),skolemize(Y2,sK84_skl(X,C,P,Z))],[f1563])).
% 76.28/35.06 fof(f1565,plain,(
% 76.28/35.06 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_owl_maxQualifiedCardinality,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)|~iext(X1,X3,X5)|~icext(X2,X5)|X5=X4)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1566,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK83_skl(X3,X2,X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1567,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK83_skl(X3,X2,X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1568,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK84_skl(X3,X2,X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1569,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK84_skl(X3,X2,X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1570,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|icext(X0,X3)|~sK84_skl(X3,X2,X1,X0)=sK83_skl(X3,X2,X1,X0))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1564])).
% 76.28/35.06 fof(f1731,plain,(
% 76.28/35.06 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 76.28/35.06 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 76.28/35.06 fof(f1732,plain,(
% 76.28/35.06 ![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))))))),
% 76.28/35.06 inference(NNF_transformation,[status(thm)],[f1731])).
% 76.28/35.06 fof(f1733,plain,(
% 76.28/35.06 (![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))))))),
% 76.28/35.06 inference(miniscoping,[status(thm)],[f1732])).
% 76.28/35.06 fof(f1734,plain,(
% 76.28/35.06 (![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))))))),
% 76.28/35.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 76.28/35.06 fof(f1738,plain,(
% 76.28/35.06 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1734])).
% 76.28/35.06 fof(f1739,plain,(
% 76.28/35.06 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f1734])).
% 76.28/35.06 fof(f2405,plain,(
% 76.28/35.06 ~iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f560])).
% 76.28/35.06 fof(f2406,plain,(
% 76.28/35.06 iext(uri_owl_maxQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2407,plain,(
% 76.28/35.06 iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2408,plain,(
% 76.28/35.06 iext(uri_owl_onClass,uri_ex_x2,uri_ex_c2)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2409,plain,(
% 76.28/35.06 iext(uri_rdfs_subClassOf,uri_ex_c2,uri_ex_c1)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2410,plain,(
% 76.28/35.06 iext(uri_owl_maxQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2411,plain,(
% 76.28/35.06 iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2412,plain,(
% 76.28/35.06 iext(uri_owl_onClass,uri_ex_x1,uri_ex_c1)),
% 76.28/35.06 inference(cnf_transformation,[status(thm)],[f561])).
% 76.28/35.06 fof(f2766,plain,(
% 76.28/35.06 ![X0]: (~icext(uri_ex_c2,X0)|icext(uri_ex_c1,X0))),
% 76.28/35.06 inference(resolution,[status(thm)],[f2409,f657])).
% 76.28/35.06 fof(f6076,plain,(
% 76.28/35.06 icext(uri_owl_Restriction,uri_ex_x1)),
% 76.28/35.06 inference(resolution,[status(thm)],[f982,f2410])).
% 76.28/35.06 fof(f6077,plain,(
% 76.28/35.06 icext(uri_owl_Restriction,uri_ex_x2)),
% 76.28/35.06 inference(resolution,[status(thm)],[f982,f2406])).
% 76.28/35.06 fof(f6083,plain,(
% 76.28/35.06 ic(uri_ex_x1)),
% 76.28/35.06 inference(resolution,[status(thm)],[f6076,f854])).
% 76.28/35.06 fof(f6117,plain,(
% 76.28/35.06 ic(uri_ex_x2)),
% 76.28/35.06 inference(resolution,[status(thm)],[f6077,f854])).
% 76.28/35.06 fof(f17370,plain,(
% 76.28/35.06 ![X0,X1,X2,X3,X4]: (~iext(uri_owl_onProperty,uri_ex_x1,X0)|~iext(uri_owl_onClass,uri_ex_x1,X1)|~icext(uri_ex_x1,X2)|~iext(X0,X2,X3)|~icext(X1,X3)|~iext(X0,X2,X4)|~icext(X1,X4)|X4=X3)),
% 76.28/35.06 inference(resolution,[status(thm)],[f1565,f2410])).
% 76.28/35.06 fof(f17373,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|~iext(uri_owl_onClass,uri_ex_x2,X1)|icext(uri_ex_x2,X2)|iext(X0,X2,sK83_skl(X2,X1,X0,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f1566,f2406])).
% 76.28/35.06 fof(f17380,plain,(
% 76.28/35.06 ![X0,X1,X2,X3]: (~iext(uri_owl_onProperty,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|~iext(X0,X1,X2)|~icext(uri_ex_c1,X2)|~iext(X0,X1,X3)|~icext(uri_ex_c1,X3)|X3=X2)),
% 76.28/35.06 inference(resolution,[status(thm)],[f17370,f2412])).
% 76.28/35.06 fof(f17381,plain,(
% 76.28/35.06 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p,X1,sK83_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17373,f2407])).
% 76.28/35.06 fof(f17382,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p,X0,sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17381,f2408])).
% 76.28/35.06 fof(f17388,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c1,X1)|~iext(uri_ex_p,X0,X2)|~icext(uri_ex_c1,X2)|X2=X1)),
% 76.28/35.06 inference(resolution,[status(thm)],[f17380,f2411])).
% 76.28/35.06 fof(f17390,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|~iext(uri_owl_onClass,uri_ex_x2,X1)|icext(uri_ex_x2,X2)|icext(X1,sK83_skl(X2,X1,X0,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f1567,f2406])).
% 76.28/35.06 fof(f17392,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|~iext(uri_owl_onClass,uri_ex_x2,X1)|icext(uri_ex_x2,X2)|iext(X0,X2,sK84_skl(X2,X1,X0,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f1568,f2406])).
% 76.28/35.06 fof(f17394,plain,(
% 76.28/35.06 ![X0,X1,X2]: (~iext(uri_owl_onProperty,uri_ex_x2,X0)|~iext(uri_owl_onClass,uri_ex_x2,X1)|icext(uri_ex_x2,X2)|icext(X1,sK84_skl(X2,X1,X0,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f1569,f2406])).
% 76.28/35.06 fof(f17395,plain,(
% 76.28/35.06 ![X0,X1]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c1,X1)|~icext(uri_ex_c1,sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2))|sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)=X1|icext(uri_ex_x2,X0))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17388,f17382])).
% 76.28/35.06 fof(f17407,plain,(
% 76.28/35.06 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK83_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17390,f2407])).
% 76.28/35.06 fof(f17413,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c2,sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17407,f2408])).
% 76.28/35.06 fof(f17414,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c1,sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17413,f2766])).
% 76.28/35.06 fof(f17423,plain,(
% 76.28/35.06 ![X0,X1]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c1,X1)|sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)=X1|icext(uri_ex_x2,X0))),
% 76.28/35.06 inference(backward_subsumption_resolution,[status(thm)],[f17395,f17414])).
% 76.28/35.06 fof(f17438,plain,(
% 76.28/35.06 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p,X1,sK84_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17392,f2407])).
% 76.28/35.06 fof(f17465,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p,X0,sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17438,f2408])).
% 76.28/35.06 fof(f17466,plain,(
% 76.28/35.06 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK84_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17394,f2407])).
% 76.28/35.06 fof(f17473,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c2,sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17466,f2408])).
% 76.28/35.06 fof(f17474,plain,(
% 76.28/35.06 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c1,sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17473,f2766])).
% 76.28/35.06 fof(f17614,plain,(
% 76.28/35.06 ![X0]: (~icext(uri_ex_x1,X0)|~icext(uri_ex_c1,sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2))|sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)|icext(uri_ex_x2,X0)|icext(uri_ex_x2,X0))),
% 76.28/35.06 inference(resolution,[status(thm)],[f17423,f17465])).
% 76.28/35.06 fof(f17618,plain,(
% 76.28/35.06 ![X0]: (~icext(uri_ex_x1,X0)|~icext(uri_ex_c1,sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2))|sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)|icext(uri_ex_x2,X0))),
% 76.28/35.06 inference(duplicate_literals_removal,[status(thm)],[f17614])).
% 76.28/35.06 fof(f17619,plain,(
% 76.28/35.06 ![X0]: (~icext(uri_ex_x1,X0)|sK83_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(X0,uri_ex_c2,uri_ex_p,uri_ex_x2)|icext(uri_ex_x2,X0))),
% 76.28/35.06 inference(forward_subsumption_resolution,[status(thm)],[f17618,f17474])).
% 76.28/35.06 fof(f18662,plain,(
% 76.28/35.06 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_x1,X0)|~ic(X0)|icext(uri_ex_x1,sK115_skl(X0,uri_ex_x1)))),
% 76.28/35.06 inference(resolution,[status(thm)],[f1738,f6083])).
% 76.28/35.06 fof(f21680,plain,(
% 76.28/35.06 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 76.28/35.06 inference(resolution,[status(thm)],[f18662,f6117])).
% 76.28/35.06 fof(f21721,plain,(
% 76.28/35.06 icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 76.28/35.06 inference(forward_subsumption_resolution,[status(thm)],[f21680,f2405])).
% 76.28/35.06 fof(f21722,plain,(
% 76.28/35.06 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 76.28/35.06 inference(resolution,[status(thm)],[f21721,f17619])).
% 76.28/35.06 fof(f23120,plain,(
% 76.28/35.06 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)|iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 76.28/35.06 inference(resolution,[status(thm)],[f21722,f1739])).
% 76.28/35.06 fof(f23129,plain,(
% 76.28/35.06 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 76.28/35.06 inference(forward_subsumption_resolution,[status(thm)],[f23120,f2405])).
% 76.28/35.06 fof(f23130,plain,(
% 76.28/35.06 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)|~ic(uri_ex_x1)),
% 76.28/35.06 inference(resolution,[status(thm)],[f23129,f6117])).
% 76.28/35.06 fof(f23145,plain,(
% 76.28/35.06 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c2,uri_ex_p,uri_ex_x2)),
% 76.28/35.06 inference(forward_subsumption_resolution,[status(thm)],[f23130,f6083])).
% 76.28/35.06 fof(f23450,plain,(
% 76.28/35.06 ~iext(uri_owl_maxQualifiedCardinality,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_c2)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 14.41/35.14 inference(resolution,[status(thm)],[f23145,f1570])).
% 14.41/35.14 fof(f23501,plain,(
% 14.41/35.14 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)|~iext(uri_owl_onClass,uri_ex_x2,uri_ex_c2)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 14.41/35.14 inference(forward_subsumption_resolution,[status(thm)],[f23450,f2406])).
% 14.41/35.14 fof(f23515,plain,(
% 14.41/35.14 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 14.41/35.14 inference(resolution,[status(thm)],[f23501,f2408])).
% 14.41/35.14 fof(f23516,plain,(
% 14.41/35.14 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 14.41/35.14 inference(forward_subsumption_resolution,[status(thm)],[f23515,f2407])).
% 14.41/35.14 fof(f23521,plain,(
% 14.41/35.14 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 14.41/35.14 inference(resolution,[status(thm)],[f23516,f1739])).
% 14.41/35.14 fof(f23530,plain,(
% 14.41/35.14 ~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 14.41/35.14 inference(forward_subsumption_resolution,[status(thm)],[f23521,f2405])).
% 14.41/35.14 fof(f23531,plain,(
% 14.41/35.14 ~ic(uri_ex_x1)),
% 14.41/35.14 inference(resolution,[status(thm)],[f23530,f6117])).
% 14.41/35.14 fof(f23532,plain,(
% 14.41/35.14 $false),
% 14.41/35.14 inference(forward_subsumption_resolution,[status(thm)],[f23531,f6083])).
% 14.41/35.14 % SZS output end CNFRefutation for theBenchmark.p
% 14.41/35.15 % Elapsed time: 9.812300 seconds
% 14.41/35.15 % CPU time: 77.014938 seconds
% 14.41/35.15 % Total memory used: 343.972 MB
% 14.41/35.15 % Net memory used: 318.744 MB
%------------------------------------------------------------------------------