%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB023+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 : n006.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:35 PM UTC 2026
% Result : Theorem 5.21s 6.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB023+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/5.58 % Computer : n006.cluster.edu
% 0.11/5.58 % Model : x86_64 x86_64
% 0.11/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.58 % Memory : 8046.5625MB
% 0.11/5.58 % OS : Linux 6.8.0-71-generic
% 0.11/5.58 % CPULimit : 300
% 0.11/5.58 % WCLimit : 300
% 0.11/5.58 % DateTime : Mon Sep 21 07:40:53 UTC 2026
% 0.11/5.58 % CPUTime :
% 0.14/5.63 % Drodi V4.1.1
% 5.21/6.41 % Refutation found
% 5.21/6.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.21/6.41 % SZS output start CNFRefutation for theBenchmark
% 5.21/6.41 fof(f25,axiom,(
% 5.21/6.41 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 5.21/6.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.41 fof(f295,axiom,(
% 5.21/6.41 (! [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 ) )) ) ) )),
% 5.21/6.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.41 fof(f354,axiom,(
% 5.21/6.41 (! [X,Y] :( iext(uri_owl_sameAs,X,Y)<=> X = Y ) )),
% 5.21/6.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.41 fof(f559,conjecture,(
% 5.21/6.41 ( iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)& iext(uri_owl_sameAs,uri_ex_w,uri_ex_v) ) ),
% 5.21/6.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.41 fof(f560,negated_conjecture,(
% 5.21/6.41 ~(( iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)& iext(uri_owl_sameAs,uri_ex_w,uri_ex_v) ) )),
% 5.21/6.41 inference(negated_conjecture,[status(cth)],[f559])).
% 5.21/6.41 fof(f561,axiom,(
% 5.21/6.41 (? [BNODE_o,BNODE_l] :( iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)& iext(uri_rdf_type,uri_ex_w,BNODE_o)& iext(uri_rdf_type,BNODE_o,uri_owl_Class)& iext(uri_owl_oneOf,BNODE_o,BNODE_l)& iext(uri_rdf_first,BNODE_l,uri_ex_u)& iext(uri_rdf_first,BNODE_l,uri_ex_v)& iext(uri_rdf_rest,BNODE_l,uri_rdf_nil) ) )),
% 5.21/6.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.21/6.41 fof(f592,plain,(
% 5.21/6.41 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 5.21/6.41 inference(NNF_transformation,[status(thm)],[f25])).
% 5.21/6.41 fof(f593,plain,(
% 5.21/6.41 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 5.21/6.41 inference(miniscoping,[status(thm)],[f592])).
% 5.21/6.41 fof(f594,plain,(
% 5.21/6.41 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 5.21/6.41 inference(cnf_transformation,[status(thm)],[f593])).
% 5.21/6.41 fof(f1211,plain,(
% 5.21/6.41 ![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)))))),
% 5.21/6.41 inference(pre_NNF_transformation,[status(thm)],[f295])).
% 5.21/6.41 fof(f1212,plain,(
% 5.21/6.41 ![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)))))))),
% 5.21/6.41 inference(NNF_transformation,[status(thm)],[f1211])).
% 5.21/6.41 fof(f1213,plain,(
% 5.21/6.41 ![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))))))))),
% 5.21/6.41 inference(miniscoping,[status(thm)],[f1212])).
% 5.21/6.41 fof(f1214,plain,(
% 5.21/6.41 ![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)))))))),
% 5.21/6.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213])).
% 5.21/6.41 fof(f1216,plain,(
% 5.21/6.41 ![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)),
% 5.21/6.41 inference(cnf_transformation,[status(thm)],[f1214])).
% 5.21/6.41 fof(f1217,plain,(
% 5.21/6.41 ![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)),
% 5.21/6.41 inference(cnf_transformation,[status(thm)],[f1214])).
% 5.21/6.41 fof(f1832,plain,(
% 5.21/6.41 ![X,Y]: ((~iext(uri_owl_sameAs,X,Y)|X=Y)&(iext(uri_owl_sameAs,X,Y)|~X=Y))),
% 5.21/6.41 inference(NNF_transformation,[status(thm)],[f354])).
% 5.21/6.41 fof(f1833,plain,(
% 5.21/6.41 (![X,Y]: (~iext(uri_owl_sameAs,X,Y)|X=Y))&(![X,Y]: (iext(uri_owl_sameAs,X,Y)|~X=Y))),
% 5.21/6.41 inference(miniscoping,[status(thm)],[f1832])).
% 5.21/6.41 fof(f1835,plain,(
% 5.21/6.41 ![X0,X1]: (iext(uri_owl_sameAs,X0,X1)|~X0=X1)),
% 5.21/6.41 inference(cnf_transformation,[status(thm)],[f1833])).
% 5.21/6.41 fof(f2405,plain,(
% 5.21/6.41 (~iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)|~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v))),
% 6.07/6.44 inference(pre_NNF_transformation,[status(thm)],[f560])).
% 6.07/6.44 fof(f2406,plain,(
% 6.07/6.44 ~iext(uri_owl_sameAs,uri_ex_w,uri_ex_u)|~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2405])).
% 6.07/6.44 fof(f2407,plain,(
% 6.07/6.44 ?[BNODE_l]: ((((?[BNODE_o]: (((iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_w,BNODE_o))&iext(uri_rdf_type,BNODE_o,uri_owl_Class))&iext(uri_owl_oneOf,BNODE_o,BNODE_l)))&iext(uri_rdf_first,BNODE_l,uri_ex_u))&iext(uri_rdf_first,BNODE_l,uri_ex_v))&iext(uri_rdf_rest,BNODE_l,uri_rdf_nil))),
% 6.07/6.44 inference(miniscoping,[status(thm)],[f561])).
% 6.07/6.44 fof(f2408,plain,(
% 6.07/6.44 ((((((iext(uri_rdf_type,uri_rdf_first,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_w,sK200_skl))&iext(uri_rdf_type,sK200_skl,uri_owl_Class))&iext(uri_owl_oneOf,sK200_skl,sK199_skl))&iext(uri_rdf_first,sK199_skl,uri_ex_u))&iext(uri_rdf_first,sK199_skl,uri_ex_v))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))),
% 6.07/6.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(BNODE_l,sK199_skl),skolemize(BNODE_o,sK200_skl)],[f2407])).
% 6.07/6.44 fof(f2410,plain,(
% 6.07/6.44 iext(uri_rdf_type,uri_ex_w,sK200_skl)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2408])).
% 6.07/6.44 fof(f2412,plain,(
% 6.07/6.44 iext(uri_owl_oneOf,sK200_skl,sK199_skl)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2408])).
% 6.07/6.44 fof(f2413,plain,(
% 6.07/6.44 iext(uri_rdf_first,sK199_skl,uri_ex_u)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2408])).
% 6.07/6.44 fof(f2414,plain,(
% 6.07/6.44 iext(uri_rdf_first,sK199_skl,uri_ex_v)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2408])).
% 6.07/6.44 fof(f2415,plain,(
% 6.07/6.44 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 6.07/6.44 inference(cnf_transformation,[status(thm)],[f2408])).
% 6.07/6.44 fof(f2512,plain,(
% 6.07/6.44 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~iext(uri_owl_oneOf,X2,X0)|icext(X2,X1))),
% 6.07/6.44 inference(destructive_equality_resolution,[status(thm)],[f1217])).
% 6.07/6.44 fof(f2516,plain,(
% 6.07/6.44 ![X0]: (iext(uri_owl_sameAs,X0,X0))),
% 6.07/6.44 inference(destructive_equality_resolution,[status(thm)],[f1835])).
% 6.07/6.44 fof(f2618,plain,(
% 6.07/6.44 icext(sK200_skl,uri_ex_w)),
% 6.07/6.44 inference(resolution,[status(thm)],[f594,f2410])).
% 6.07/6.44 fof(f9122,plain,(
% 6.07/6.44 ![X0,X1]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK199_skl)|~icext(X0,X1)|X1=uri_ex_v)),
% 6.07/6.44 inference(resolution,[status(thm)],[f1216,f2414])).
% 6.07/6.44 fof(f9124,plain,(
% 6.07/6.44 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK199_skl)|~icext(X0,X1)|X1=uri_ex_v)),
% 6.07/6.44 inference(forward_subsumption_resolution,[status(thm)],[f9122,f2415])).
% 6.07/6.44 fof(f9127,plain,(
% 6.07/6.44 ![X0]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK199_skl)|icext(X0,uri_ex_u))),
% 6.07/6.44 inference(resolution,[status(thm)],[f2512,f2413])).
% 6.07/6.44 fof(f9129,plain,(
% 6.07/6.44 ![X0]: (~iext(uri_owl_oneOf,X0,sK199_skl)|icext(X0,uri_ex_u))),
% 6.07/6.44 inference(forward_subsumption_resolution,[status(thm)],[f9127,f2415])).
% 6.07/6.44 fof(f9138,plain,(
% 6.07/6.44 icext(sK200_skl,uri_ex_u)),
% 6.07/6.44 inference(resolution,[status(thm)],[f9129,f2412])).
% 6.07/6.44 fof(f9149,plain,(
% 6.07/6.44 ![X0]: (~icext(sK200_skl,X0)|X0=uri_ex_v)),
% 6.07/6.44 inference(resolution,[status(thm)],[f9124,f2412])).
% 6.07/6.44 fof(f9150,plain,(
% 6.07/6.44 uri_ex_u=uri_ex_v),
% 6.07/6.44 inference(resolution,[status(thm)],[f9149,f9138])).
% 6.07/6.44 fof(f9152,plain,(
% 6.07/6.44 uri_ex_w=uri_ex_v),
% 6.07/6.44 inference(resolution,[status(thm)],[f9149,f2618])).
% 6.07/6.44 fof(f9276,plain,(
% 6.07/6.44 ~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)|~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)),
% 6.07/6.44 inference(backward_demodulation,[status(thm)],[f9150,f2406])).
% 6.07/6.44 fof(f9544,plain,(
% 6.07/6.44 ~iext(uri_owl_sameAs,uri_ex_w,uri_ex_v)),
% 6.07/6.44 inference(duplicate_literals_removal,[status(thm)],[f9276])).
% 6.07/6.44 fof(f9548,plain,(
% 6.07/6.44 ~iext(uri_owl_sameAs,uri_ex_v,uri_ex_v)),
% 6.07/6.44 inference(forward_demodulation,[status(thm)],[f9152,f9544])).
% 6.07/6.44 fof(f9549,plain,(
% 6.07/6.44 $false),
% 6.07/6.44 inference(forward_subsumption_resolution,[status(thm)],[f9548,f2516])).
% 6.07/6.44 % SZS output end CNFRefutation for theBenchmark.p
% 6.07/6.44 % Elapsed time: 0.853186 seconds
% 6.07/6.44 % CPU time: 6.277515 seconds
% 6.07/6.44 % Total memory used: 178.712 MB
% 6.07/6.44 % Net memory used: 172.224 MB
%------------------------------------------------------------------------------