%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB080+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:45 PM UTC 2026
% Result : Theorem 30.76s 14.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB080+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.57 % Computer : n004.cluster.edu
% 0.10/10.57 % Model : x86_64 x86_64
% 0.10/10.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.57 % Memory : 8046.5625MB
% 0.10/10.57 % OS : Linux 6.8.0-71-generic
% 0.10/10.57 % CPULimit : 300
% 0.10/10.57 % WCLimit : 300
% 0.10/10.57 % DateTime : Mon Sep 21 07:46:16 UTC 2026
% 0.10/10.57 % CPUTime :
% 0.10/10.59 % Drodi V4.1.1
% 30.76/14.57 % Refutation found
% 30.76/14.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 30.76/14.57 % SZS output start CNFRefutation for theBenchmark
% 30.76/14.57 fof(f1,axiom,(
% 30.76/14.57 (! [S,P,O] :( iext(P,S,O)=> ip(P) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f52,axiom,(
% 30.76/14.57 (! [P,C,X,Y] :( ( iext(uri_rdfs_domain,P,C)& iext(P,X,Y) )=> icext(C,X) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f59,axiom,(
% 30.76/14.57 (! [P,C,X,Y] :( ( iext(uri_rdfs_range,P,C)& iext(P,X,Y) )=> icext(C,Y) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f295,axiom,(
% 30.76/14.57 (! [Z,S1,A1] :( ( iext(uri_rdf_first,S1,A1)& iext(uri_rdf_rest,S1,uri_rdf_nil) )=> ( iext(uri_owl_oneOf,Z,S1)<=> ( ic(Z)& (! [X] :( icext(Z,X)<=> X = A1 ) )) ) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f344,axiom,(
% 30.76/14.57 (! [P1,P2] :( iext(uri_rdfs_subPropertyOf,P1,P2)<=> ( ip(P1)& ip(P2)& (! [X,Y] :( iext(P1,X,Y)=> iext(P2,X,Y) ) )) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f559,conjecture,(
% 30.76/14.57 iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2) ),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f560,negated_conjecture,(
% 30.76/14.57 ~(iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2) )),
% 30.76/14.57 inference(negated_conjecture,[status(cth)],[f559])).
% 30.76/14.57 fof(f561,axiom,(
% 30.76/14.57 (? [X8,X4,X2,X5,X1,X6,X3,X7,X0] :( iext(uri_rdfs_domain,uri_ex_p1,X0)& iext(uri_rdfs_range,uri_ex_p1,X1)& iext(uri_rdf_first,X2,uri_ex_u)& iext(uri_rdf_rest,X2,uri_rdf_nil)& iext(uri_rdf_first,X3,uri_ex_w)& iext(uri_rdf_rest,X3,uri_rdf_nil)& iext(uri_rdf_first,X4,uri_ex_w)& iext(uri_rdf_rest,X4,uri_rdf_nil)& iext(uri_rdfs_domain,uri_ex_p2,X5)& iext(uri_rdfs_range,uri_ex_p2,X6)& iext(uri_owl_oneOf,X1,X2)& iext(uri_rdf_first,X7,uri_ex_u)& iext(uri_rdf_rest,X7,X8)& iext(uri_owl_oneOf,X0,X3)& iext(uri_owl_oneOf,X6,X7)& iext(uri_owl_oneOf,X5,X4)& iext(uri_rdf_first,X8,uri_ex_w)& iext(uri_rdf_rest,X8,uri_rdf_nil)& iext(uri_ex_p1,uri_ex_w,uri_ex_u)& iext(uri_ex_p2,uri_ex_w,uri_ex_u)& iext(uri_ex_p2,uri_ex_w,uri_ex_w) ) )),
% 30.76/14.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.76/14.57 fof(f562,plain,(
% 30.76/14.57 ![S,P,O]: (~iext(P,S,O)|ip(P))),
% 30.76/14.57 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 30.76/14.57 fof(f563,plain,(
% 30.76/14.57 ![P]: ((![S,O]: ~iext(P,S,O))|ip(P))),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f562])).
% 30.76/14.57 fof(f564,plain,(
% 30.76/14.57 ![X0,X1,X2]: (~iext(X0,X1,X2)|ip(X0))),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f563])).
% 30.76/14.57 fof(f625,plain,(
% 30.76/14.57 ![P,C,X,Y]: ((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X))),
% 30.76/14.57 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 30.76/14.57 fof(f626,plain,(
% 30.76/14.57 ![C,X]: ((![P]: (~iext(uri_rdfs_domain,P,C)|(![Y]: ~iext(P,X,Y))))|icext(C,X))),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f625])).
% 30.76/14.57 fof(f627,plain,(
% 30.76/14.57 ![X0,X1,X2,X3]: (~iext(uri_rdfs_domain,X0,X1)|~iext(X0,X2,X3)|icext(X1,X2))),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f626])).
% 30.76/14.57 fof(f643,plain,(
% 30.76/14.57 ![P,C,X,Y]: ((~iext(uri_rdfs_range,P,C)|~iext(P,X,Y))|icext(C,Y))),
% 30.76/14.57 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 30.76/14.57 fof(f644,plain,(
% 30.76/14.57 ![C,Y]: ((![P]: (~iext(uri_rdfs_range,P,C)|(![X]: ~iext(P,X,Y))))|icext(C,Y))),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f643])).
% 30.76/14.57 fof(f645,plain,(
% 30.76/14.57 ![X0,X1,X2,X3]: (~iext(uri_rdfs_range,X0,X1)|~iext(X0,X2,X3)|icext(X1,X3))),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f644])).
% 30.76/14.57 fof(f1211,plain,(
% 30.76/14.57 ![Z,S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]: (icext(Z,X)<=>X=A1)))))),
% 30.76/14.57 inference(pre_NNF_transformation,[status(thm)],[f295])).
% 30.76/14.57 fof(f1212,plain,(
% 30.76/14.57 ![Z,S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]: ((~icext(Z,X)|X=A1)&(icext(Z,X)|~X=A1)))))&(iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~X=A1)&(icext(Z,X)|X=A1)))))))),
% 30.76/14.57 inference(NNF_transformation,[status(thm)],[f1211])).
% 30.76/14.57 fof(f1213,plain,(
% 30.76/14.57 ![S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|X=A1))&(![X]: (icext(Z,X)|~X=A1))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~X=A1)&(icext(Z,X)|X=A1))))))))),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f1212])).
% 30.76/14.57 fof(f1214,plain,(
% 30.76/14.57 ![S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|X=A1))&(![X]: (icext(Z,X)|~X=A1))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|((~icext(Z,sK10_skl(Z,A1,S1))|~sK10_skl(Z,A1,S1)=A1)&(icext(Z,sK10_skl(Z,A1,S1))|sK10_skl(Z,A1,S1)=A1)))))))),
% 30.76/14.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213])).
% 30.76/14.57 fof(f1216,plain,(
% 30.76/14.57 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~iext(uri_owl_oneOf,X2,X0)|~icext(X2,X3)|X3=X1)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f1214])).
% 30.76/14.57 fof(f1740,plain,(
% 30.76/14.57 ![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)<=>((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))))),
% 30.76/14.57 inference(pre_NNF_transformation,[status(thm)],[f344])).
% 30.76/14.57 fof(f1741,plain,(
% 30.76/14.57 ![P1,P2]: ((~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y)))))&(iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: (iext(P1,X,Y)&~iext(P2,X,Y))))))),
% 30.76/14.57 inference(NNF_transformation,[status(thm)],[f1740])).
% 30.76/14.57 fof(f1742,plain,(
% 30.76/14.57 (![P1,P2]: (~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y))))))&(![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(?[X,Y]: (iext(P1,X,Y)&~iext(P2,X,Y))))))),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f1741])).
% 30.76/14.57 fof(f1743,plain,(
% 30.76/14.57 (![P1,P2]: (~iext(uri_rdfs_subPropertyOf,P1,P2)|((ip(P1)&ip(P2))&(![X,Y]: (~iext(P1,X,Y)|iext(P2,X,Y))))))&(![P1,P2]: (iext(uri_rdfs_subPropertyOf,P1,P2)|((~ip(P1)|~ip(P2))|(iext(P1,sK116_skl(P2,P1),sK117_skl(P2,P1))&~iext(P2,sK116_skl(P2,P1),sK117_skl(P2,P1))))))),
% 30.76/14.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl,sK117_skl]),skolemize(X,sK116_skl(P2,P1)),skolemize(Y,sK117_skl(P2,P1))],[f1742])).
% 30.76/14.57 fof(f1747,plain,(
% 30.76/14.57 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~ip(X1)|iext(X0,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f1743])).
% 30.76/14.57 fof(f1748,plain,(
% 30.76/14.57 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~ip(X1)|~iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f1743])).
% 30.76/14.57 fof(f2405,plain,(
% 30.76/14.57 ~iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f560])).
% 30.76/14.57 fof(f2406,plain,(
% 30.76/14.57 (((?[X8]: (((?[X4,X5]: ((?[X6,X7]: ((?[X3,X0]: ((((?[X2,X1]: ((((((((((iext(uri_rdfs_domain,uri_ex_p1,X0)&iext(uri_rdfs_range,uri_ex_p1,X1))&iext(uri_rdf_first,X2,uri_ex_u))&iext(uri_rdf_rest,X2,uri_rdf_nil))&iext(uri_rdf_first,X3,uri_ex_w))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_rdf_first,X4,uri_ex_w))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_rdfs_domain,uri_ex_p2,X5))&iext(uri_rdfs_range,uri_ex_p2,X6))&iext(uri_owl_oneOf,X1,X2)))&iext(uri_rdf_first,X7,uri_ex_u))&iext(uri_rdf_rest,X7,X8))&iext(uri_owl_oneOf,X0,X3)))&iext(uri_owl_oneOf,X6,X7)))&iext(uri_owl_oneOf,X5,X4)))&iext(uri_rdf_first,X8,uri_ex_w))&iext(uri_rdf_rest,X8,uri_rdf_nil)))&iext(uri_ex_p1,uri_ex_w,uri_ex_u))&iext(uri_ex_p2,uri_ex_w,uri_ex_u))&iext(uri_ex_p2,uri_ex_w,uri_ex_w)),
% 30.76/14.57 inference(miniscoping,[status(thm)],[f561])).
% 30.76/14.57 fof(f2407,plain,(
% 30.76/14.57 (((((((((((((((((((iext(uri_rdfs_domain,uri_ex_p1,sK205_skl)&iext(uri_rdfs_range,uri_ex_p1,sK207_skl))&iext(uri_rdf_first,sK206_skl,uri_ex_u))&iext(uri_rdf_rest,sK206_skl,uri_rdf_nil))&iext(uri_rdf_first,sK204_skl,uri_ex_w))&iext(uri_rdf_rest,sK204_skl,uri_rdf_nil))&iext(uri_rdf_first,sK200_skl,uri_ex_w))&iext(uri_rdf_rest,sK200_skl,uri_rdf_nil))&iext(uri_rdfs_domain,uri_ex_p2,sK201_skl))&iext(uri_rdfs_range,uri_ex_p2,sK202_skl))&iext(uri_owl_oneOf,sK207_skl,sK206_skl))&iext(uri_rdf_first,sK203_skl,uri_ex_u))&iext(uri_rdf_rest,sK203_skl,sK199_skl))&iext(uri_owl_oneOf,sK205_skl,sK204_skl))&iext(uri_owl_oneOf,sK202_skl,sK203_skl))&iext(uri_owl_oneOf,sK201_skl,sK200_skl))&iext(uri_rdf_first,sK199_skl,uri_ex_w))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))&iext(uri_ex_p1,uri_ex_w,uri_ex_u))&iext(uri_ex_p2,uri_ex_w,uri_ex_u))&iext(uri_ex_p2,uri_ex_w,uri_ex_w)),
% 30.76/14.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl,sK202_skl,sK203_skl,sK204_skl,sK205_skl,sK206_skl,sK207_skl]),skolemize(X8,sK199_skl),skolemize(X4,sK200_skl),skolemize(X5,sK201_skl),skolemize(X6,sK202_skl),skolemize(X7,sK203_skl),skolemize(X3,sK204_skl),skolemize(X0,sK205_skl),skolemize(X2,sK206_skl),skolemize(X1,sK207_skl)],[f2406])).
% 30.76/14.57 fof(f2408,plain,(
% 30.76/14.57 iext(uri_rdfs_domain,uri_ex_p1,sK205_skl)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2409,plain,(
% 30.76/14.57 iext(uri_rdfs_range,uri_ex_p1,sK207_skl)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2410,plain,(
% 30.76/14.57 iext(uri_rdf_first,sK206_skl,uri_ex_u)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2411,plain,(
% 30.76/14.57 iext(uri_rdf_rest,sK206_skl,uri_rdf_nil)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2412,plain,(
% 30.76/14.57 iext(uri_rdf_first,sK204_skl,uri_ex_w)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2413,plain,(
% 30.76/14.57 iext(uri_rdf_rest,sK204_skl,uri_rdf_nil)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2418,plain,(
% 30.76/14.57 iext(uri_owl_oneOf,sK207_skl,sK206_skl)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2421,plain,(
% 30.76/14.57 iext(uri_owl_oneOf,sK205_skl,sK204_skl)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2426,plain,(
% 30.76/14.57 iext(uri_ex_p1,uri_ex_w,uri_ex_u)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2427,plain,(
% 30.76/14.57 iext(uri_ex_p2,uri_ex_w,uri_ex_u)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2428,plain,(
% 30.76/14.57 iext(uri_ex_p2,uri_ex_w,uri_ex_w)),
% 30.76/14.57 inference(cnf_transformation,[status(thm)],[f2407])).
% 30.76/14.57 fof(f2535,plain,(
% 30.76/14.57 ![X0,X1]: (iext(uri_rdfs_subPropertyOf,X0,X1)|~ip(X0)|~iext(X1,sK116_skl(X1,X0),sK117_skl(X1,X0)))),
% 30.76/14.57 inference(forward_subsumption_resolution,[status(thm)],[f1748,f564])).
% 30.76/14.57 fof(f2568,plain,(
% 30.76/14.57 ip(uri_ex_p1)),
% 30.76/14.57 inference(resolution,[status(thm)],[f564,f2426])).
% 30.76/14.57 fof(f2574,plain,(
% 30.76/14.57 ip(uri_ex_p2)),
% 30.76/14.57 inference(resolution,[status(thm)],[f2428,f564])).
% 30.76/14.57 fof(f4371,plain,(
% 30.76/14.57 ![X0,X1,X2]: (~iext(uri_rdf_first,sK204_skl,X0)|~iext(uri_owl_oneOf,X1,sK204_skl)|~icext(X1,X2)|X2=X0)),
% 30.76/14.57 inference(resolution,[status(thm)],[f1216,f2413])).
% 30.76/14.57 fof(f4372,plain,(
% 30.76/14.57 ![X0,X1,X2]: (~iext(uri_rdf_first,sK206_skl,X0)|~iext(uri_owl_oneOf,X1,sK206_skl)|~icext(X1,X2)|X2=X0)),
% 30.76/14.57 inference(resolution,[status(thm)],[f1216,f2411])).
% 30.76/14.57 fof(f4539,plain,(
% 30.76/14.57 ![X0,X1]: (~iext(uri_rdf_first,sK204_skl,X0)|~icext(sK205_skl,X1)|X1=X0)),
% 30.76/14.57 inference(resolution,[status(thm)],[f4371,f2421])).
% 30.76/14.57 fof(f4540,plain,(
% 30.76/14.57 ![X0]: (~icext(sK205_skl,X0)|X0=uri_ex_w)),
% 30.76/14.57 inference(resolution,[status(thm)],[f4539,f2412])).
% 30.76/14.57 fof(f4544,plain,(
% 30.76/14.57 ![X0,X1,X2]: (X0=uri_ex_w|~iext(uri_rdfs_domain,X1,sK205_skl)|~iext(X1,X0,X2))),
% 30.76/14.57 inference(resolution,[status(thm)],[f4540,f627])).
% 30.76/14.57 fof(f4603,plain,(
% 30.76/14.57 ![X0,X1]: (X0=uri_ex_w|~iext(uri_ex_p1,X0,X1))),
% 30.76/14.57 inference(resolution,[status(thm)],[f4544,f2408])).
% 30.76/14.57 fof(f4654,plain,(
% 30.76/14.57 ![X0,X1]: (~iext(uri_rdf_first,sK206_skl,X0)|~icext(sK207_skl,X1)|X1=X0)),
% 30.76/14.57 inference(resolution,[status(thm)],[f4372,f2418])).
% 30.76/14.57 fof(f4655,plain,(
% 30.76/14.57 ![X0]: (~icext(sK207_skl,X0)|X0=uri_ex_u)),
% 30.76/14.57 inference(resolution,[status(thm)],[f4654,f2410])).
% 30.76/14.57 fof(f4658,plain,(
% 30.76/14.57 ![X0,X1,X2]: (X0=uri_ex_u|~iext(uri_rdfs_range,X1,sK207_skl)|~iext(X1,X2,X0))),
% 30.76/14.57 inference(resolution,[status(thm)],[f4655,f645])).
% 30.76/14.57 fof(f4718,plain,(
% 30.76/14.57 ![X0,X1]: (X0=uri_ex_u|~iext(uri_ex_p1,X1,X0))),
% 30.76/14.57 inference(resolution,[status(thm)],[f4658,f2409])).
% 30.76/14.57 fof(f7756,plain,(
% 30.76/14.57 ![X0]: (iext(uri_rdfs_subPropertyOf,X0,uri_ex_p2)|~ip(X0)|iext(X0,sK116_skl(uri_ex_p2,X0),sK117_skl(uri_ex_p2,X0)))),
% 30.76/14.57 inference(resolution,[status(thm)],[f1747,f2574])).
% 30.76/14.57 fof(f8219,plain,(
% 30.76/14.57 iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2)|iext(uri_ex_p1,sK116_skl(uri_ex_p2,uri_ex_p1),sK117_skl(uri_ex_p2,uri_ex_p1))),
% 30.76/14.57 inference(resolution,[status(thm)],[f7756,f2568])).
% 30.76/14.57 fof(f8222,plain,(
% 30.76/14.57 iext(uri_ex_p1,sK116_skl(uri_ex_p2,uri_ex_p1),sK117_skl(uri_ex_p2,uri_ex_p1))),
% 30.76/14.57 inference(forward_subsumption_resolution,[status(thm)],[f8219,f2405])).
% 30.76/14.60 fof(f8264,plain,(
% 30.76/14.60 sK117_skl(uri_ex_p2,uri_ex_p1)=uri_ex_u),
% 30.76/14.60 inference(resolution,[status(thm)],[f8222,f4718])).
% 30.76/14.60 fof(f8265,plain,(
% 30.76/14.60 sK116_skl(uri_ex_p2,uri_ex_p1)=uri_ex_w),
% 30.76/14.60 inference(resolution,[status(thm)],[f8222,f4603])).
% 30.76/14.60 fof(f8269,plain,(
% 30.76/14.60 iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2)|~ip(uri_ex_p1)|~iext(uri_ex_p2,sK116_skl(uri_ex_p2,uri_ex_p1),uri_ex_u)),
% 30.76/14.60 inference(paramodulation,[status(thm)],[f8264,f2535])).
% 30.76/14.60 fof(f8270,plain,(
% 30.76/14.60 iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p2)|~ip(uri_ex_p1)|~iext(uri_ex_p2,uri_ex_w,uri_ex_u)),
% 30.76/14.60 inference(forward_demodulation,[status(thm)],[f8265,f8269])).
% 30.76/14.60 fof(f8271,plain,(
% 30.76/14.60 ~ip(uri_ex_p1)|~iext(uri_ex_p2,uri_ex_w,uri_ex_u)),
% 30.76/14.60 inference(forward_subsumption_resolution,[status(thm)],[f8270,f2405])).
% 30.76/14.60 fof(f8274,plain,(
% 30.76/14.60 ~iext(uri_ex_p2,uri_ex_w,uri_ex_u)),
% 30.76/14.60 inference(resolution,[status(thm)],[f8271,f2568])).
% 30.76/14.60 fof(f8275,plain,(
% 30.76/14.60 $false),
% 30.76/14.60 inference(forward_subsumption_resolution,[status(thm)],[f8274,f2427])).
% 30.76/14.60 % SZS output end CNFRefutation for theBenchmark.p
% 7.06/14.61 % Elapsed time: 4.035603 seconds
% 7.06/14.61 % CPU time: 31.641388 seconds
% 7.06/14.61 % Total memory used: 261.952 MB
% 7.06/14.61 % Net memory used: 249.806 MB
%------------------------------------------------------------------------------