%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB090+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 : n008.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.34s 16.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB090+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.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 07:47:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 130.34/16.96 % Refutation found
% 130.34/16.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 130.34/16.96 % SZS output start CNFRefutation for theBenchmark
% 130.34/16.96 fof(f73,axiom,(
% 130.34/16.96 (! [P,Q] :( iext(uri_rdfs_subPropertyOf,P,Q)=> ( ip(P)& ip(Q)& (! [X,Y] :( iext(P,X,Y)=> iext(Q,X,Y) ) )) ) )),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f159,axiom,(
% 130.34/16.96 (! [X] :( icext(uri_owl_Restriction,X)=> ic(X) ) )),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f227,axiom,(
% 130.34/16.96 (! [X,Y] :( iext(uri_owl_maxQualifiedCardinality,X,Y)=> ( icext(uri_owl_Restriction,X)& icext(uri_xml_nonNegativeInteger,Y) ) ) )),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f325,axiom,(
% 130.34/16.96 (! [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.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f343,axiom,(
% 130.34/16.96 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f559,conjecture,(
% 130.34/16.96 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) ),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f560,negated_conjecture,(
% 130.34/16.96 ~(iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2) )),
% 130.34/16.96 inference(negated_conjecture,[status(cth)],[f559])).
% 130.34/16.96 fof(f561,axiom,(
% 130.34/16.96 ( iext(uri_owl_maxQualifiedCardinality,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_maxQualifiedCardinality,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_p2,uri_ex_p1) ) ),
% 130.34/16.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 130.34/16.96 fof(f665,plain,(
% 130.34/16.96 ![P,Q]: (~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X,Y]: (~iext(P,X,Y)|iext(Q,X,Y)))))),
% 130.34/16.96 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 130.34/16.96 fof(f668,plain,(
% 130.34/16.96 ![X0,X1,X2,X3]: (~iext(uri_rdfs_subPropertyOf,X0,X1)|~iext(X0,X2,X3)|iext(X1,X2,X3))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f665])).
% 130.34/16.96 fof(f853,plain,(
% 130.34/16.96 ![X]: (~icext(uri_owl_Restriction,X)|ic(X))),
% 130.34/16.96 inference(pre_NNF_transformation,[status(thm)],[f159])).
% 130.34/16.96 fof(f854,plain,(
% 130.34/16.96 ![X0]: (~icext(uri_owl_Restriction,X0)|ic(X0))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f853])).
% 130.34/16.96 fof(f981,plain,(
% 130.34/16.96 ![X,Y]: (~iext(uri_owl_maxQualifiedCardinality,X,Y)|(icext(uri_owl_Restriction,X)&icext(uri_xml_nonNegativeInteger,Y)))),
% 130.34/16.96 inference(pre_NNF_transformation,[status(thm)],[f227])).
% 130.34/16.96 fof(f982,plain,(
% 130.34/16.96 ![X0,X1]: (~iext(uri_owl_maxQualifiedCardinality,X0,X1)|icext(uri_owl_Restriction,X0))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f981])).
% 130.34/16.96 fof(f1561,plain,(
% 130.34/16.96 ![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.34/16.96 inference(pre_NNF_transformation,[status(thm)],[f325])).
% 130.34/16.96 fof(f1562,plain,(
% 130.34/16.96 ![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.34/16.96 inference(NNF_transformation,[status(thm)],[f1561])).
% 130.34/16.96 fof(f1563,plain,(
% 130.34/16.96 ![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.34/16.96 inference(miniscoping,[status(thm)],[f1562])).
% 130.34/16.96 fof(f1564,plain,(
% 130.34/16.96 ![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.34/16.96 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.34/16.96 fof(f1565,plain,(
% 130.34/16.96 ![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.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1566,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1567,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1568,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1569,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1570,plain,(
% 130.34/16.96 ![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))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1564])).
% 130.34/16.96 fof(f1731,plain,(
% 130.34/16.96 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 130.34/16.96 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 130.34/16.96 fof(f1732,plain,(
% 130.34/16.96 ![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.34/16.96 inference(NNF_transformation,[status(thm)],[f1731])).
% 130.34/16.96 fof(f1733,plain,(
% 130.34/16.96 (![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.34/16.96 inference(miniscoping,[status(thm)],[f1732])).
% 130.34/16.96 fof(f1734,plain,(
% 130.34/16.96 (![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.34/16.96 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 130.34/16.96 fof(f1738,plain,(
% 130.34/16.96 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1734])).
% 130.34/16.96 fof(f1739,plain,(
% 130.34/16.96 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f1734])).
% 130.34/16.96 fof(f2405,plain,(
% 130.34/16.96 ~iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f560])).
% 130.34/16.96 fof(f2406,plain,(
% 130.34/16.96 iext(uri_owl_maxQualifiedCardinality,uri_ex_x2,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2407,plain,(
% 130.34/16.96 iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p2)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2408,plain,(
% 130.34/16.96 iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2409,plain,(
% 130.34/16.96 iext(uri_owl_maxQualifiedCardinality,uri_ex_x1,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2410,plain,(
% 130.34/16.96 iext(uri_owl_onProperty,uri_ex_x1,uri_ex_p1)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2411,plain,(
% 130.34/16.96 iext(uri_owl_onClass,uri_ex_x1,uri_ex_c)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2412,plain,(
% 130.34/16.96 iext(uri_rdfs_subPropertyOf,uri_ex_p2,uri_ex_p1)),
% 130.34/16.96 inference(cnf_transformation,[status(thm)],[f561])).
% 130.34/16.96 fof(f2982,plain,(
% 130.34/16.96 ![X0,X1]: (~iext(uri_ex_p2,X0,X1)|iext(uri_ex_p1,X0,X1))),
% 130.34/16.96 inference(resolution,[status(thm)],[f668,f2412])).
% 130.34/16.96 fof(f5832,plain,(
% 130.34/16.96 icext(uri_owl_Restriction,uri_ex_x1)),
% 130.34/16.96 inference(resolution,[status(thm)],[f982,f2409])).
% 130.34/16.96 fof(f5833,plain,(
% 130.34/16.96 icext(uri_owl_Restriction,uri_ex_x2)),
% 130.34/16.96 inference(resolution,[status(thm)],[f982,f2406])).
% 130.34/16.96 fof(f5834,plain,(
% 130.34/16.96 ic(uri_ex_x1)),
% 130.34/16.96 inference(resolution,[status(thm)],[f5832,f854])).
% 130.34/16.96 fof(f5868,plain,(
% 130.34/16.96 ic(uri_ex_x2)),
% 130.34/16.96 inference(resolution,[status(thm)],[f5833,f854])).
% 130.34/16.96 fof(f16872,plain,(
% 130.34/16.96 ![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.34/16.96 inference(resolution,[status(thm)],[f1565,f2409])).
% 130.34/16.96 fof(f16875,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f1566,f2406])).
% 130.34/16.96 fof(f16882,plain,(
% 130.34/16.96 ![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.34/16.96 inference(resolution,[status(thm)],[f16872,f2411])).
% 130.34/16.96 fof(f16883,plain,(
% 130.34/16.96 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p2,X1,sK83_skl(X1,X0,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f16875,f2407])).
% 130.34/16.96 fof(f16884,plain,(
% 130.34/16.96 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p2,X0,sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f16883,f2408])).
% 130.34/16.96 fof(f16885,plain,(
% 130.34/16.96 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p1,X0,sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f16884,f2982])).
% 130.34/16.96 fof(f16895,plain,(
% 130.34/16.96 ![X0,X1,X2]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p1,X0,X1)|~icext(uri_ex_c,X1)|~iext(uri_ex_p1,X0,X2)|~icext(uri_ex_c,X2)|X2=X1)),
% 130.34/16.96 inference(resolution,[status(thm)],[f16882,f2410])).
% 130.34/16.96 fof(f16897,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f1567,f2406])).
% 130.34/16.96 fof(f16899,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f1568,f2406])).
% 130.34/16.96 fof(f16901,plain,(
% 130.34/16.96 ![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)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f1569,f2406])).
% 130.34/16.96 fof(f16917,plain,(
% 130.34/16.96 ![X0,X1]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p1,X0,X1)|~icext(uri_ex_c,X1)|~icext(uri_ex_c,sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2))|sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)=X1|icext(uri_ex_x2,X0))),
% 130.34/16.96 inference(resolution,[status(thm)],[f16895,f16885])).
% 130.34/16.96 fof(f16919,plain,(
% 130.34/16.96 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK83_skl(X1,X0,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.96 inference(resolution,[status(thm)],[f16897,f2407])).
% 130.34/16.96 fof(f16920,plain,(
% 130.34/16.97 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c,sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16919,f2408])).
% 130.34/16.97 fof(f16921,plain,(
% 130.34/16.97 ![X0,X1]: (~icext(uri_ex_x1,X0)|~iext(uri_ex_p1,X0,X1)|~icext(uri_ex_c,X1)|sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)=X1|icext(uri_ex_x2,X0))),
% 130.34/16.97 inference(backward_subsumption_resolution,[status(thm)],[f16917,f16920])).
% 130.34/16.97 fof(f16923,plain,(
% 130.34/16.97 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|iext(uri_ex_p2,X1,sK84_skl(X1,X0,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16899,f2407])).
% 130.34/16.97 fof(f16958,plain,(
% 130.34/16.97 ![X0,X1]: (~iext(uri_owl_onClass,uri_ex_x2,X0)|icext(uri_ex_x2,X1)|icext(X0,sK84_skl(X1,X0,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16901,f2407])).
% 130.34/16.97 fof(f16960,plain,(
% 130.34/16.97 ![X0]: (icext(uri_ex_x2,X0)|icext(uri_ex_c,sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16958,f2408])).
% 130.34/16.97 fof(f16974,plain,(
% 130.34/16.97 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p2,X0,sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16923,f2408])).
% 130.34/16.97 fof(f16975,plain,(
% 130.34/16.97 ![X0]: (icext(uri_ex_x2,X0)|iext(uri_ex_p1,X0,sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16974,f2982])).
% 130.34/16.97 fof(f17034,plain,(
% 130.34/16.97 ![X0]: (~icext(uri_ex_x1,X0)|~icext(uri_ex_c,sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2))|sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)|icext(uri_ex_x2,X0)|icext(uri_ex_x2,X0))),
% 130.34/16.97 inference(resolution,[status(thm)],[f16921,f16975])).
% 130.34/16.97 fof(f17038,plain,(
% 130.34/16.97 ![X0]: (~icext(uri_ex_x1,X0)|~icext(uri_ex_c,sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2))|sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)|icext(uri_ex_x2,X0))),
% 130.34/16.97 inference(duplicate_literals_removal,[status(thm)],[f17034])).
% 130.34/16.97 fof(f17039,plain,(
% 130.34/16.97 ![X0]: (~icext(uri_ex_x1,X0)|sK83_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(X0,uri_ex_c,uri_ex_p2,uri_ex_x2)|icext(uri_ex_x2,X0))),
% 130.34/16.97 inference(forward_subsumption_resolution,[status(thm)],[f17038,f16960])).
% 130.34/16.97 fof(f18243,plain,(
% 130.34/16.97 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_x1,X0)|~ic(X0)|icext(uri_ex_x1,sK115_skl(X0,uri_ex_x1)))),
% 130.34/16.97 inference(resolution,[status(thm)],[f1738,f5834])).
% 130.34/16.97 fof(f20533,plain,(
% 130.34/16.97 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 130.34/16.97 inference(resolution,[status(thm)],[f18243,f5868])).
% 130.34/16.97 fof(f20572,plain,(
% 130.34/16.97 icext(uri_ex_x1,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 130.34/16.97 inference(forward_subsumption_resolution,[status(thm)],[f20533,f2405])).
% 130.34/16.97 fof(f20573,plain,(
% 130.34/16.97 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 130.34/16.97 inference(resolution,[status(thm)],[f20572,f17039])).
% 130.34/16.97 fof(f21774,plain,(
% 130.34/16.97 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)|iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 130.34/16.97 inference(resolution,[status(thm)],[f20573,f1739])).
% 130.34/16.97 fof(f21783,plain,(
% 130.34/16.97 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 130.34/16.97 inference(forward_subsumption_resolution,[status(thm)],[f21774,f2405])).
% 130.34/16.97 fof(f21784,plain,(
% 130.34/16.97 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)|~ic(uri_ex_x1)),
% 130.34/16.97 inference(resolution,[status(thm)],[f21783,f5868])).
% 130.34/16.97 fof(f21799,plain,(
% 130.34/16.97 sK83_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)=sK84_skl(sK115_skl(uri_ex_x2,uri_ex_x1),uri_ex_c,uri_ex_p2,uri_ex_x2)),
% 130.34/16.97 inference(forward_subsumption_resolution,[status(thm)],[f21784,f5834])).
% 130.34/16.97 fof(f22383,plain,(
% 130.34/16.97 ~iext(uri_owl_maxQualifiedCardinality,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)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 46.85/17.05 inference(resolution,[status(thm)],[f21799,f1570])).
% 46.85/17.05 fof(f22407,plain,(
% 46.85/17.05 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p2)|~iext(uri_owl_onClass,uri_ex_x2,uri_ex_c)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 46.85/17.05 inference(forward_subsumption_resolution,[status(thm)],[f22383,f2406])).
% 46.85/17.05 fof(f22415,plain,(
% 46.85/17.05 ~iext(uri_owl_onProperty,uri_ex_x2,uri_ex_p2)|icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 46.85/17.05 inference(resolution,[status(thm)],[f22407,f2408])).
% 46.85/17.05 fof(f22416,plain,(
% 46.85/17.05 icext(uri_ex_x2,sK115_skl(uri_ex_x2,uri_ex_x1))),
% 46.85/17.05 inference(forward_subsumption_resolution,[status(thm)],[f22415,f2407])).
% 46.85/17.05 fof(f22421,plain,(
% 46.85/17.05 iext(uri_rdfs_subClassOf,uri_ex_x1,uri_ex_x2)|~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 46.85/17.05 inference(resolution,[status(thm)],[f22416,f1739])).
% 46.85/17.05 fof(f22430,plain,(
% 46.85/17.05 ~ic(uri_ex_x1)|~ic(uri_ex_x2)),
% 46.85/17.05 inference(forward_subsumption_resolution,[status(thm)],[f22421,f2405])).
% 46.85/17.05 fof(f22431,plain,(
% 46.85/17.05 ~ic(uri_ex_x1)),
% 46.85/17.05 inference(resolution,[status(thm)],[f22430,f5868])).
% 46.85/17.05 fof(f22432,plain,(
% 46.85/17.05 $false),
% 46.85/17.05 inference(forward_subsumption_resolution,[status(thm)],[f22431,f5834])).
% 46.85/17.05 % SZS output end CNFRefutation for theBenchmark.p
% 46.85/17.07 % Elapsed time: 16.677009 seconds
% 46.85/17.07 % CPU time: 131.245012 seconds
% 46.85/17.07 % Total memory used: 400.283 MB
% 46.85/17.07 % Net memory used: 372.997 MB
%------------------------------------------------------------------------------