%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB031+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 : n013.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:40 PM UTC 2026
% Result : Unsatisfiable 95.70s 12.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB031+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.39 % Computer : n013.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.39 % CPULimit : 300
% 0.15/0.39 % WCLimit : 300
% 0.15/0.39 % DateTime : Mon Sep 21 07:42:06 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.19/0.43 % Drodi V4.1.1
% 95.70/12.61 % Refutation found
% 95.70/12.61 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 95.70/12.61 % SZS output start CNFRefutation for theBenchmark
% 95.70/12.61 fof(f2,axiom,(
% 95.70/12.61 (! [X] : ir(X) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f4,axiom,(
% 95.70/12.61 iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f13,axiom,(
% 95.70/12.61 (! [P] :( iext(uri_rdf_type,P,uri_rdf_Property)<=> ip(P) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f147,axiom,(
% 95.70/12.61 (! [X] :( icext(uri_owl_ObjectProperty,X)<=> ip(X) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f163,axiom,(
% 95.70/12.61 (! [X] :( icext(uri_owl_Thing,X)<=> ir(X) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f295,axiom,(
% 95.70/12.61 (! [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 ) )) ) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f351,axiom,(
% 95.70/12.61 (! [C1,C2] :( iext(uri_owl_equivalentClass,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)<=> icext(C2,X) ) )) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f395,axiom,(
% 95.70/12.61 (! [P] :( icext(uri_owl_IrreflexiveReflexiveProperty,P)<=> ( ip(P)& (! [X] : ~ iext(P,X,X) )) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f559,axiom,(
% 95.70/12.61 (? [BNODE_x,BNODE_l] :( iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x)& iext(uri_owl_oneOf,BNODE_x,BNODE_l)& iext(uri_rdf_first,BNODE_l,uri_ex_w)& iext(uri_rdf_rest,BNODE_l,uri_rdf_nil) ) )),
% 95.70/12.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 95.70/12.61 fof(f563,plain,(
% 95.70/12.61 ![X0]: (ir(X0))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2])).
% 95.70/12.61 fof(f566,plain,(
% 95.70/12.61 iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f4])).
% 95.70/12.61 fof(f575,plain,(
% 95.70/12.61 ![P]: ((~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P))&(iext(uri_rdf_type,P,uri_rdf_Property)|~ip(P)))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f13])).
% 95.70/12.61 fof(f576,plain,(
% 95.70/12.61 (![P]: (~iext(uri_rdf_type,P,uri_rdf_Property)|ip(P)))&(![P]: (iext(uri_rdf_type,P,uri_rdf_Property)|~ip(P)))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f575])).
% 95.70/12.61 fof(f577,plain,(
% 95.70/12.61 ![X0]: (~iext(uri_rdf_type,X0,uri_rdf_Property)|ip(X0))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f576])).
% 95.70/12.61 fof(f823,plain,(
% 95.70/12.61 ![X]: ((~icext(uri_owl_ObjectProperty,X)|ip(X))&(icext(uri_owl_ObjectProperty,X)|~ip(X)))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f147])).
% 95.70/12.61 fof(f824,plain,(
% 95.70/12.61 (![X]: (~icext(uri_owl_ObjectProperty,X)|ip(X)))&(![X]: (icext(uri_owl_ObjectProperty,X)|~ip(X)))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f823])).
% 95.70/12.61 fof(f826,plain,(
% 95.70/12.61 ![X0]: (icext(uri_owl_ObjectProperty,X0)|~ip(X0))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f824])).
% 95.70/12.61 fof(f857,plain,(
% 95.70/12.61 ![X]: ((~icext(uri_owl_Thing,X)|ir(X))&(icext(uri_owl_Thing,X)|~ir(X)))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f163])).
% 95.70/12.61 fof(f858,plain,(
% 95.70/12.61 (![X]: (~icext(uri_owl_Thing,X)|ir(X)))&(![X]: (icext(uri_owl_Thing,X)|~ir(X)))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f857])).
% 95.70/12.61 fof(f860,plain,(
% 95.70/12.61 ![X0]: (icext(uri_owl_Thing,X0)|~ir(X0))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f858])).
% 95.70/12.61 fof(f1209,plain,(
% 95.70/12.61 ![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)))))),
% 95.70/12.61 inference(pre_NNF_transformation,[status(thm)],[f295])).
% 95.70/12.61 fof(f1210,plain,(
% 95.70/12.61 ![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)))))))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f1209])).
% 95.70/12.61 fof(f1211,plain,(
% 95.70/12.61 ![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))))))))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f1210])).
% 95.70/12.61 fof(f1212,plain,(
% 95.70/12.61 ![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)))))))),
% 95.70/12.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1211])).
% 95.70/12.61 fof(f1214,plain,(
% 95.70/12.61 ![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)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f1212])).
% 95.70/12.61 fof(f1803,plain,(
% 95.70/12.61 ![C1,C2]: ((~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&(![X]: ((~icext(C1,X)|icext(C2,X))&(icext(C1,X)|~icext(C2,X))))))&(iext(uri_owl_equivalentClass,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: ((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f351])).
% 95.70/12.61 fof(f1804,plain,(
% 95.70/12.61 (![C1,C2]: (~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&((![X]: (~icext(C1,X)|icext(C2,X)))&(![X]: (icext(C1,X)|~icext(C2,X)))))))&(![C1,C2]: (iext(uri_owl_equivalentClass,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: ((~icext(C1,X)|~icext(C2,X))&(icext(C1,X)|icext(C2,X)))))))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f1803])).
% 95.70/12.61 fof(f1805,plain,(
% 95.70/12.61 (![C1,C2]: (~iext(uri_owl_equivalentClass,C1,C2)|((ic(C1)&ic(C2))&((![X]: (~icext(C1,X)|icext(C2,X)))&(![X]: (icext(C1,X)|~icext(C2,X)))))))&(![C1,C2]: (iext(uri_owl_equivalentClass,C1,C2)|((~ic(C1)|~ic(C2))|((~icext(C1,sK123_skl(C2,C1))|~icext(C2,sK123_skl(C2,C1)))&(icext(C1,sK123_skl(C2,C1))|icext(C2,sK123_skl(C2,C1)))))))),
% 95.70/12.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(X,sK123_skl(C2,C1))],[f1804])).
% 95.70/12.61 fof(f1808,plain,(
% 95.70/12.61 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f1805])).
% 95.70/12.61 fof(f2032,plain,(
% 95.70/12.61 ![P]: ((~icext(uri_owl_IrreflexiveReflexiveProperty,P)|(ip(P)&(![X]: ~iext(P,X,X))))&(icext(uri_owl_IrreflexiveReflexiveProperty,P)|(~ip(P)|(?[X]: iext(P,X,X)))))),
% 95.70/12.61 inference(NNF_transformation,[status(thm)],[f395])).
% 95.70/12.61 fof(f2033,plain,(
% 95.70/12.61 (![P]: (~icext(uri_owl_IrreflexiveReflexiveProperty,P)|(ip(P)&(![X]: ~iext(P,X,X)))))&(![P]: (icext(uri_owl_IrreflexiveReflexiveProperty,P)|(~ip(P)|(?[X]: iext(P,X,X)))))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f2032])).
% 95.70/12.61 fof(f2034,plain,(
% 95.70/12.61 (![P]: (~icext(uri_owl_IrreflexiveReflexiveProperty,P)|(ip(P)&(![X]: ~iext(P,X,X)))))&(![P]: (icext(uri_owl_IrreflexiveReflexiveProperty,P)|(~ip(P)|iext(P,sK176_skl(P),sK176_skl(P)))))),
% 95.70/12.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK176_skl]),skolemize(X,sK176_skl(P))],[f2033])).
% 95.70/12.61 fof(f2036,plain,(
% 95.70/12.61 ![X0,X1]: (~icext(uri_owl_IrreflexiveReflexiveProperty,X0)|~iext(X0,X1,X1))),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2034])).
% 95.70/12.61 fof(f2403,plain,(
% 95.70/12.61 ?[BNODE_l]: (((?[BNODE_x]: (iext(uri_owl_equivalentClass,uri_owl_Thing,BNODE_x)&iext(uri_owl_oneOf,BNODE_x,BNODE_l)))&iext(uri_rdf_first,BNODE_l,uri_ex_w))&iext(uri_rdf_rest,BNODE_l,uri_rdf_nil))),
% 95.70/12.61 inference(miniscoping,[status(thm)],[f559])).
% 95.70/12.61 fof(f2404,plain,(
% 95.70/12.61 (((iext(uri_owl_equivalentClass,uri_owl_Thing,sK200_skl)&iext(uri_owl_oneOf,sK200_skl,sK199_skl))&iext(uri_rdf_first,sK199_skl,uri_ex_w))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))),
% 95.70/12.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(BNODE_l,sK199_skl),skolemize(BNODE_x,sK200_skl)],[f2403])).
% 95.70/12.61 fof(f2405,plain,(
% 95.70/12.61 iext(uri_owl_equivalentClass,uri_owl_Thing,sK200_skl)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2404])).
% 95.70/12.61 fof(f2406,plain,(
% 95.70/12.61 iext(uri_owl_oneOf,sK200_skl,sK199_skl)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2404])).
% 95.70/12.61 fof(f2407,plain,(
% 95.70/12.61 iext(uri_rdf_first,sK199_skl,uri_ex_w)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2404])).
% 95.70/12.61 fof(f2408,plain,(
% 95.70/12.61 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 95.70/12.61 inference(cnf_transformation,[status(thm)],[f2404])).
% 95.70/12.61 fof(f2537,plain,(
% 95.70/12.61 ip(uri_rdf_first)),
% 96.42/12.68 inference(resolution,[status(thm)],[f577,f566])).
% 96.42/12.68 fof(f4338,plain,(
% 96.42/12.68 icext(uri_owl_ObjectProperty,uri_rdf_first)),
% 96.42/12.68 inference(resolution,[status(thm)],[f826,f2537])).
% 96.42/12.68 fof(f4667,plain,(
% 96.42/12.68 ![X0]: (icext(uri_owl_Thing,X0))),
% 96.42/12.68 inference(forward_subsumption_resolution,[status(thm)],[f860,f563])).
% 96.42/12.68 fof(f8460,plain,(
% 96.42/12.68 ![X0,X1]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK199_skl)|~icext(X0,X1)|X1=uri_ex_w)),
% 96.42/12.68 inference(resolution,[status(thm)],[f1214,f2407])).
% 96.42/12.68 fof(f8461,plain,(
% 96.42/12.68 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK199_skl)|~icext(X0,X1)|X1=uri_ex_w)),
% 96.42/12.68 inference(forward_subsumption_resolution,[status(thm)],[f8460,f2408])).
% 96.42/12.68 fof(f10432,plain,(
% 96.42/12.68 ![X0]: (~icext(uri_owl_Thing,X0)|icext(sK200_skl,X0))),
% 96.42/12.68 inference(resolution,[status(thm)],[f1808,f2405])).
% 96.42/12.68 fof(f10433,plain,(
% 96.42/12.68 ![X0]: (icext(sK200_skl,X0))),
% 96.42/12.68 inference(forward_subsumption_resolution,[status(thm)],[f10432,f4667])).
% 96.42/12.68 fof(f30567,plain,(
% 96.42/12.68 ![X0]: (~icext(sK200_skl,X0)|X0=uri_ex_w)),
% 96.42/12.68 inference(resolution,[status(thm)],[f8461,f2406])).
% 96.42/12.68 fof(f30568,plain,(
% 96.42/12.68 ![X0]: (X0=uri_ex_w)),
% 96.42/12.68 inference(forward_subsumption_resolution,[status(thm)],[f30567,f10433])).
% 96.42/12.68 fof(f30572,plain,(
% 96.42/12.68 ![X0,X1]: (X0=X1)),
% 96.42/12.68 inference(paramodulation,[status(thm)],[f30568,f30568])).
% 96.42/12.68 fof(f30573,plain,(
% 96.42/12.68 ![X0]: (iext(uri_rdf_first,sK199_skl,X0))),
% 96.42/12.68 inference(paramodulation,[status(thm)],[f30568,f2407])).
% 96.42/12.68 fof(f30969,plain,(
% 96.42/12.68 ~icext(uri_owl_IrreflexiveReflexiveProperty,uri_rdf_first)),
% 96.42/12.68 inference(resolution,[status(thm)],[f30573,f2036])).
% 96.42/12.68 fof(f31252,plain,(
% 96.42/12.68 ![X0]: (~icext(X0,uri_rdf_first))),
% 96.42/12.68 inference(paramodulation,[status(thm)],[f30572,f30969])).
% 96.42/12.68 fof(f31257,plain,(
% 96.42/12.68 $false),
% 96.42/12.68 inference(backward_subsumption_resolution,[status(thm)],[f4338,f31252])).
% 96.42/12.68 % SZS output end CNFRefutation for theBenchmark.p
% 5.86/12.75 % Elapsed time: 12.330819 seconds
% 5.86/12.75 % CPU time: 96.942477 seconds
% 5.86/12.75 % Total memory used: 393.567 MB
% 5.86/12.75 % Net memory used: 370.169 MB
%------------------------------------------------------------------------------