%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB088+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 : n018.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 130.19s 17.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB088+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.11/0.55 % Computer : n018.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Mon Sep 21 07:48:29 UTC 2026
% 0.11/0.56 % CPUTime :
% 0.15/0.60 % Drodi V4.1.1
% 130.19/17.08 % Refutation found
% 130.19/17.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 130.19/17.08 % SZS output start CNFRefutation for theBenchmark
% 130.19/17.08 fof(f159,axiom,(
% 130.19/17.08 (! [X] :( icext(uri_owl_Restriction,X)=> ic(X) ) )),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f227,axiom,(
% 130.19/17.08 (! [X,Y] :( iext(uri_owl_maxQualifiedCardinality,X,Y)=> ( icext(uri_owl_Restriction,X)& icext(uri_xml_nonNegativeInteger,Y) ) ) )),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f325,axiom,(
% 130.19/17.08 (! [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 ) )) )) )),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f326,axiom,(
% 130.19/17.08 (! [Z,P,C] :( ( iext(uri_owl_maxQualifiedCardinality,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,Y3] :( ( iext(P,X,Y1)& icext(C,Y1)& iext(P,X,Y2)& icext(C,Y2)& iext(P,X,Y3)& icext(C,Y3) )=> ( Y3 = Y1| Y3 = Y2 ) ) )) )) )),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f343,axiom,(
% 130.19/17.08 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f559,conjecture,(
% 130.19/17.08 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) ),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f560,negated_conjecture,(
% 130.19/17.08 ~(iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) )),
% 130.19/17.08 inference(negated_conjecture,[status(cth)],[f559])).
% 130.19/17.08 fof(f561,axiom,(
% 130.19/17.08 ( iext(uri_owl_maxQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_2,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_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_c) ) ),
% 130.19/17.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.19/17.08 fof(f853,plain,(
% 130.19/17.08 ![X]: (~icext(uri_owl_Restriction,X)|ic(X))),
% 130.19/17.08 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 130.19/17.08 fof(f854,plain,(
% 130.19/17.08 ![X0]: (~icext(uri_owl_Restriction,X0)|ic(X0))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f853])).
% 130.19/17.08 fof(f981,plain,(
% 130.19/17.08 ![X,Y]: (~iext(uri_owl_maxQualifiedCardinality,X,Y)|(icext(uri_owl_Restriction,X)&icext(uri_xml_nonNegativeInteger,Y)))),
% 130.19/17.08 inference(pre_NNF_transformation,[status(thm)],[f227])).
% 130.19/17.08 fof(f982,plain,(
% 130.19/17.08 ![X0,X1]: (~iext(uri_owl_maxQualifiedCardinality,X0,X1)|icext(uri_owl_Restriction,X0))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f981])).
% 130.19/17.08 fof(f1561,plain,(
% 130.19/17.08 ![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)))))),
% 130.19/17.08 inference(pre_NNF_transformation,[status(thm)],[f325])).
% 130.19/17.08 fof(f1562,plain,(
% 130.19/17.08 ![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))))))),
% 130.19/17.08 inference(NNF_transformation,[status(thm)],[f1561])).
% 130.19/17.08 fof(f1563,plain,(
% 130.19/17.08 ![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))))))),
% 130.19/17.08 inference(miniscoping,[status(thm)],[f1562])).
% 130.19/17.08 fof(f1564,plain,(
% 130.19/17.08 ![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))))))),
% 130.19/17.08 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])).
% 130.19/17.08 fof(f1565,plain,(
% 130.19/17.08 ![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)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.19/17.08 fof(f1571,plain,(
% 130.19/17.08 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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,Y3]: ((((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|~iext(P,X,Y3))|~icext(C,Y3))|(Y3=Y1|Y3=Y2))))))),
% 130.19/17.08 inference(pre_NNF_transformation,[status(thm)],[f326])).
% 130.19/17.08 fof(f1572,plain,(
% 130.19/17.08 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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,Y3]: ((((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|~iext(P,X,Y3))|~icext(C,Y3))|(Y3=Y1|Y3=Y2))))&(icext(Z,X)|(?[Y1,Y2,Y3]: ((((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&iext(P,X,Y3))&icext(C,Y3))&(~Y3=Y1&~Y3=Y2)))))))),
% 130.19/17.08 inference(NNF_transformation,[status(thm)],[f1571])).
% 130.19/17.08 fof(f1573,plain,(
% 130.19/17.08 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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,Y3]: ((((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|~iext(P,X,Y3))|~icext(C,Y3))|(Y3=Y1|Y3=Y2)))))&(![X]: (icext(Z,X)|(?[Y1,Y2,Y3]: ((((((iext(P,X,Y1)&icext(C,Y1))&iext(P,X,Y2))&icext(C,Y2))&iext(P,X,Y3))&icext(C,Y3))&(~Y3=Y1&~Y3=Y2)))))))),
% 130.19/17.08 inference(miniscoping,[status(thm)],[f1572])).
% 130.19/17.08 fof(f1574,plain,(
% 130.19/17.08 ![Z,P,C]: (((~iext(uri_owl_maxQualifiedCardinality,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,Y3]: ((((((~iext(P,X,Y1)|~icext(C,Y1))|~iext(P,X,Y2))|~icext(C,Y2))|~iext(P,X,Y3))|~icext(C,Y3))|(Y3=Y1|Y3=Y2)))))&(![X]: (icext(Z,X)|((((((iext(P,X,sK85_skl(X,C,P,Z))&icext(C,sK85_skl(X,C,P,Z)))&iext(P,X,sK86_skl(X,C,P,Z)))&icext(C,sK86_skl(X,C,P,Z)))&iext(P,X,sK87_skl(X,C,P,Z)))&icext(C,sK87_skl(X,C,P,Z)))&(~sK87_skl(X,C,P,Z)=sK85_skl(X,C,P,Z)&~sK87_skl(X,C,P,Z)=sK86_skl(X,C,P,Z)))))))),
% 130.19/17.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK85_skl,sK86_skl,sK87_skl]),skolemize(Y1,sK85_skl(X,C,P,Z)),skolemize(Y2,sK86_skl(X,C,P,Z)),skolemize(Y3,sK87_skl(X,C,P,Z))],[f1573])).
% 130.19/17.08 fof(f1578,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK86_skl(X3,X2,X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1574])).
% 130.19/17.08 fof(f1579,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK86_skl(X3,X2,X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1574])).
% 130.19/17.08 fof(f1580,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK87_skl(X3,X2,X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1574])).
% 130.19/17.08 fof(f1581,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,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,sK87_skl(X3,X2,X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1574])).
% 130.19/17.08 fof(f1583,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_maxQualifiedCardinality,X0,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,X0,X1)|~iext(uri_owl_onClass,X0,X2)|icext(X0,X3)|~sK87_skl(X3,X2,X1,X0)=sK86_skl(X3,X2,X1,X0))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1574])).
% 130.19/17.08 fof(f1731,plain,(
% 130.19/17.08 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 130.19/17.08 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 130.19/17.08 fof(f1732,plain,(
% 130.19/17.08 ![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))))))),
% 130.19/17.08 inference(NNF_transformation,[status(thm)],[f1731])).
% 130.19/17.08 fof(f1733,plain,(
% 130.19/17.08 (![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))))))),
% 130.19/17.08 inference(miniscoping,[status(thm)],[f1732])).
% 130.19/17.08 fof(f1734,plain,(
% 130.19/17.08 (![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))))))),
% 130.19/17.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 130.19/17.08 fof(f1738,plain,(
% 130.19/17.08 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1734])).
% 130.19/17.08 fof(f1739,plain,(
% 130.19/17.08 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f1734])).
% 130.19/17.08 fof(f2405,plain,(
% 130.19/17.08 ~iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f560])).
% 130.19/17.08 fof(f2406,plain,(
% 130.19/17.08 iext(uri_owl_maxQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f2407,plain,(
% 130.19/17.08 iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f2408,plain,(
% 130.19/17.08 iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f2409,plain,(
% 130.19/17.08 iext(uri_owl_maxQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f2410,plain,(
% 130.19/17.08 iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f2411,plain,(
% 130.19/17.08 iext(uri_owl_onClass,uri_ex_x1,uri_ex_c)),
% 130.19/17.08 inference(cnf_transformation,[status(thm)],[f561])).
% 130.19/17.08 fof(f5823,plain,(
% 130.19/17.08 icext(uri_owl_Restriction,uri_ex_x1)),
% 130.19/17.08 inference(resolution,[status(thm)],[f982,f2409])).
% 130.19/17.08 fof(f5824,plain,(
% 130.19/17.08 icext(uri_owl_Restriction,uri_ex_x2)),
% 130.19/17.08 inference(resolution,[status(thm)],[f982,f2406])).
% 130.19/17.08 fof(f5825,plain,(
% 130.19/17.08 ic(uri_ex_x1)),
% 130.19/17.08 inference(resolution,[status(thm)],[f5823,f854])).
% 130.19/17.08 fof(f5859,plain,(
% 130.19/17.08 ic(uri_ex_x2)),
% 130.19/17.08 inference(resolution,[status(thm)],[f5824,f854])).
% 130.19/17.08 fof(f16884,plain,(
% 130.19/17.08 ![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)),
% 130.19/17.08 inference(resolution,[status(thm)],[f1565,f2409])).
% 130.19/17.08 fof(f16892,plain,(
% 130.19/17.08 ![X0,X1,X2,X3]: (~iext(uri_owl_onProperty,uri_ex_x1,X0)|~icext(uri_ex_x1,X1)|~iext(X0,X1,X2)|~icext(uri_ex_c,X2)|~iext(X0,X1,X3)|~icext(uri_ex_c,X3)|X3=X2)),
% 130.19/17.08 inference(resolution,[status(thm)],[f16884,f2411])).
% 130.19/17.08 fof(f16893,plain,(
% 130.19/17.08 ![X0,X1,X2]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c,X1)|~iext(uri_ex_p,X0,X2)|~icext(uri_ex_c,X2)|X2=X1)),
% 130.19/17.08 inference(resolution,[status(thm)],[f16892,f2410])).
% 130.19/17.08 fof(f16976,plain,(
% 130.19/17.08 ![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,sK86_skl(X2,X1,X0,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f1578,f2406])).
% 130.19/17.08 fof(f16977,plain,(
% 130.19/17.08 ![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,sK86_skl(X2,X1,X0,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f1579,f2406])).
% 130.19/17.08 fof(f16978,plain,(
% 130.19/17.08 ![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,sK87_skl(X2,X1,X0,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f1580,f2406])).
% 130.19/17.08 fof(f16986,plain,(
% 130.19/17.08 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p,X1,sK86_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16976,f2407])).
% 130.19/17.08 fof(f16987,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p,X0,sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16986,f2408])).
% 130.19/17.08 fof(f16988,plain,(
% 130.19/17.08 ![X0,X1]: (icext(uri_ex_x2,X0)|~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c,X1)|~icext(uri_ex_c,sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2))|sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)=X1)),
% 130.19/17.08 inference(resolution,[status(thm)],[f16987,f16893])).
% 130.19/17.08 fof(f16993,plain,(
% 130.19/17.08 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK86_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16977,f2407])).
% 130.19/17.08 fof(f16994,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c,sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16993,f2408])).
% 130.19/17.08 fof(f16995,plain,(
% 130.19/17.08 ![X0,X1]: (icext(uri_ex_x2,X0)|~icext(uri_ex_x1,X0)|~iext(uri_ex_p,X0,X1)|~icext(uri_ex_c,X1)|sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)=X1)),
% 130.19/17.08 inference(backward_subsumption_resolution,[status(thm)],[f16988,f16994])).
% 130.19/17.08 fof(f16996,plain,(
% 130.19/17.08 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p,X1,sK87_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16978,f2407])).
% 130.19/17.08 fof(f16997,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p,X0,sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16996,f2408])).
% 130.19/17.08 fof(f17003,plain,(
% 130.19/17.08 ![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,sK87_skl(X2,X1,X0,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f1581,f2406])).
% 130.19/17.08 fof(f17017,plain,(
% 130.19/17.08 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK87_skl(X1,X0,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f17003,f2407])).
% 130.19/17.08 fof(f17018,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c,sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f17017,f2408])).
% 130.19/17.08 fof(f17180,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|~icext(uri_ex_x1,X0)|~icext(uri_ex_c,sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2))|sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)|icext(uri_ex_x2,X0))),
% 130.19/17.08 inference(resolution,[status(thm)],[f16995,f16997])).
% 130.19/17.08 fof(f17185,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|~icext(uri_ex_x1,X0)|~icext(uri_ex_c,sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2))|sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2))),
% 130.19/17.08 inference(duplicate_literals_removal,[status(thm)],[f17180])).
% 130.19/17.08 fof(f17186,plain,(
% 130.19/17.08 ![X0]: (icext(uri_ex_x2,X0)|~icext(uri_ex_x1,X0)|sK86_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(X0,uri_ex_c,uri_ex_p,uri_ex_x2))),
% 130.19/17.08 inference(forward_subsumption_resolution,[status(thm)],[f17185,f17018])).
% 130.19/17.08 fof(f19037,plain,(
% 130.19/17.08 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_x1,X0)|~ic(X0)|icext(uri_ex_x1,sK115_skl(X0,uri_ex_x1)))),
% 130.19/17.08 inference(resolution,[status(thm)],[f1738,f5825])).
% 130.19/17.08 fof(f21333,plain,(
% 130.19/17.08 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 130.19/17.08 inference(resolution,[status(thm)],[f19037,f5859])).
% 130.19/17.08 fof(f21372,plain,(
% 130.19/17.08 icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 130.19/17.08 inference(forward_subsumption_resolution,[status(thm)],[f21333,f2405])).
% 130.19/17.08 fof(f21373,plain,(
% 130.19/17.08 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))|sK86_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)),
% 45.77/17.16 inference(resolution,[status(thm)],[f21372,f17186])).
% 45.77/17.16 fof(f22510,plain,(
% 45.77/17.16 sK86_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)|iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 45.77/17.16 inference(resolution,[status(thm)],[f21373,f1739])).
% 45.77/17.16 fof(f22519,plain,(
% 45.77/17.16 sK86_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f22510,f2405])).
% 45.77/17.16 fof(f22520,plain,(
% 45.77/17.16 sK86_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)|~ic(uri_ex_x1)),
% 45.77/17.16 inference(resolution,[status(thm)],[f22519,f5859])).
% 45.77/17.16 fof(f22536,plain,(
% 45.77/17.16 sK86_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)=sK87_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p,uri_ex_x2)),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f22520,f5825])).
% 45.77/17.16 fof(f23040,plain,(
% 45.77/17.16 ~iext(uri_owl_maxQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_2,uri_xsd_nonNegativeInteger))|~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)|~iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 45.77/17.16 inference(resolution,[status(thm)],[f22536,f1583])).
% 45.77/17.16 fof(f23063,plain,(
% 45.77/17.16 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)|~iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f23040,f2406])).
% 45.77/17.16 fof(f23071,plain,(
% 45.77/17.16 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 45.77/17.16 inference(resolution,[status(thm)],[f23063,f2408])).
% 45.77/17.16 fof(f23072,plain,(
% 45.77/17.16 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f23071,f2407])).
% 45.77/17.16 fof(f23078,plain,(
% 45.77/17.16 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 45.77/17.16 inference(resolution,[status(thm)],[f23072,f1739])).
% 45.77/17.16 fof(f23087,plain,(
% 45.77/17.16 ~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f23078,f2405])).
% 45.77/17.16 fof(f23088,plain,(
% 45.77/17.16 ~ic(uri_ex_x1)),
% 45.77/17.16 inference(resolution,[status(thm)],[f23087,f5859])).
% 45.77/17.16 fof(f23089,plain,(
% 45.77/17.16 $false),
% 45.77/17.16 inference(forward_subsumption_resolution,[status(thm)],[f23088,f5825])).
% 45.77/17.16 % SZS output end CNFRefutation for theBenchmark.p
% 45.77/17.16 % Elapsed time: 16.588299 seconds
% 45.77/17.16 % CPU time: 131.121410 seconds
% 45.77/17.16 % Total memory used: 434.562 MB
% 45.77/17.16 % Net memory used: 401.963 MB
%------------------------------------------------------------------------------