%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB056+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 : n001.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:43 PM UTC 2026
% Result : Theorem 7.04s 1.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB056+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:49:43 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.41 % Drodi V4.1.1
% 7.04/1.66 % Refutation found
% 7.04/1.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.04/1.66 % SZS output start CNFRefutation for theBenchmark
% 7.04/1.66 fof(f25,axiom,(
% 7.04/1.66 (! [X,C] :( iext(uri_rdf_type,X,C)<=> icext(C,X) ) )),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f296,axiom,(
% 7.04/1.66 (! [Z,S1,A1,S2,A2] :( ( iext(uri_rdf_first,S1,A1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,A2)& iext(uri_rdf_rest,S2,uri_rdf_nil) )=> ( iext(uri_owl_oneOf,Z,S1)<=> ( ic(Z)& (! [X] :( icext(Z,X)<=> ( X = A1| X = A2 ) ) )) ) ) )),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f345,axiom,(
% 7.04/1.66 (! [X,Y] :( iext(uri_owl_differentFrom,X,Y)<=> X != Y ) )),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f354,axiom,(
% 7.04/1.66 (! [X,Y] :( iext(uri_owl_sameAs,X,Y)<=> X = Y ) )),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f559,conjecture,(
% 7.04/1.66 iext(uri_owl_sameAs,uri_ex_z,uri_ex_y) ),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f560,negated_conjecture,(
% 7.04/1.66 ~(iext(uri_owl_sameAs,uri_ex_z,uri_ex_y) )),
% 7.04/1.66 inference(negated_conjecture,[status(cth)],[f559])).
% 7.04/1.66 fof(f561,axiom,(
% 7.04/1.66 (? [X0,X1] :( iext(uri_rdf_type,uri_ex_z,uri_ex_e)& iext(uri_owl_differentFrom,uri_ex_z,uri_ex_x)& iext(uri_owl_oneOf,uri_ex_e,X0)& iext(uri_rdf_first,X0,uri_ex_x)& iext(uri_rdf_rest,X0,X1)& iext(uri_rdf_first,X1,uri_ex_y)& iext(uri_rdf_rest,X1,uri_rdf_nil) ) )),
% 7.04/1.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.04/1.66 fof(f592,plain,(
% 7.04/1.66 ![X,C]: ((~iext(uri_rdf_type,X,C)|icext(C,X))&(iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 7.04/1.66 inference(NNF_transformation,[status(thm)],[f25])).
% 7.04/1.66 fof(f593,plain,(
% 7.04/1.66 (![X,C]: (~iext(uri_rdf_type,X,C)|icext(C,X)))&(![X,C]: (iext(uri_rdf_type,X,C)|~icext(C,X)))),
% 7.04/1.66 inference(miniscoping,[status(thm)],[f592])).
% 7.04/1.66 fof(f594,plain,(
% 7.04/1.66 ![X0,X1]: (~iext(uri_rdf_type,X0,X1)|icext(X1,X0))),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f593])).
% 7.04/1.66 fof(f1220,plain,(
% 7.04/1.66 ![Z,S1,A1,S2,A2]: ((((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]: (icext(Z,X)<=>(X=A1|X=A2))))))),
% 7.04/1.66 inference(pre_NNF_transformation,[status(thm)],[f296])).
% 7.04/1.66 fof(f1221,plain,(
% 7.04/1.66 ![Z,S1,A1,S2,A2]: ((((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]: ((~icext(Z,X)|(X=A1|X=A2))&(icext(Z,X)|(~X=A1&~X=A2))))))&(iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|(~X=A1&~X=A2))&(icext(Z,X)|(X=A1|X=A2))))))))),
% 7.04/1.66 inference(NNF_transformation,[status(thm)],[f1220])).
% 7.04/1.66 fof(f1222,plain,(
% 7.04/1.66 ![S1,A1,A2]: ((![S2]: (((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|(X=A1|X=A2)))&(![X]: (icext(Z,X)|(~X=A1&~X=A2)))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|(~X=A1&~X=A2))&(icext(Z,X)|(X=A1|X=A2)))))))))),
% 7.04/1.66 inference(miniscoping,[status(thm)],[f1221])).
% 7.04/1.66 fof(f1223,plain,(
% 7.04/1.66 ![S1,A1,A2]: ((![S2]: (((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|(X=A1|X=A2)))&(![X]: (icext(Z,X)|(~X=A1&~X=A2)))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|((~icext(Z,sK11_skl(Z,A2,A1,S1))|(~sK11_skl(Z,A2,A1,S1)=A1&~sK11_skl(Z,A2,A1,S1)=A2))&(icext(Z,sK11_skl(Z,A2,A1,S1))|(sK11_skl(Z,A2,A1,S1)=A1|sK11_skl(Z,A2,A1,S1)=A2))))))))),
% 7.04/1.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X,sK11_skl(Z,A2,A1,S1))],[f1222])).
% 7.04/1.66 fof(f1225,plain,(
% 7.04/1.66 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|~iext(uri_owl_oneOf,X4,X0)|~icext(X4,X5)|X5=X1|X5=X3)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f1223])).
% 7.04/1.66 fof(f1749,plain,(
% 7.04/1.66 ![X,Y]: ((~iext(uri_owl_differentFrom,X,Y)|~X=Y)&(iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 7.04/1.66 inference(NNF_transformation,[status(thm)],[f345])).
% 7.04/1.66 fof(f1750,plain,(
% 7.04/1.66 (![X,Y]: (~iext(uri_owl_differentFrom,X,Y)|~X=Y))&(![X,Y]: (iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 7.04/1.66 inference(miniscoping,[status(thm)],[f1749])).
% 7.04/1.66 fof(f1751,plain,(
% 7.04/1.66 ![X0,X1]: (~iext(uri_owl_differentFrom,X0,X1)|~X0=X1)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f1750])).
% 7.04/1.66 fof(f1832,plain,(
% 7.04/1.66 ![X,Y]: ((~iext(uri_owl_sameAs,X,Y)|X=Y)&(iext(uri_owl_sameAs,X,Y)|~X=Y))),
% 7.04/1.66 inference(NNF_transformation,[status(thm)],[f354])).
% 7.04/1.66 fof(f1833,plain,(
% 7.04/1.66 (![X,Y]: (~iext(uri_owl_sameAs,X,Y)|X=Y))&(![X,Y]: (iext(uri_owl_sameAs,X,Y)|~X=Y))),
% 7.04/1.66 inference(miniscoping,[status(thm)],[f1832])).
% 7.04/1.66 fof(f1835,plain,(
% 7.04/1.66 ![X0,X1]: (iext(uri_owl_sameAs,X0,X1)|~X0=X1)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f1833])).
% 7.04/1.66 fof(f2405,plain,(
% 7.04/1.66 ~iext(uri_owl_sameAs,uri_ex_z,uri_ex_y)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f560])).
% 7.04/1.66 fof(f2406,plain,(
% 7.04/1.66 ?[X1]: (((?[X0]: ((((iext(uri_rdf_type,uri_ex_z,uri_ex_e)&iext(uri_owl_differentFrom,uri_ex_z,uri_ex_x))&iext(uri_owl_oneOf,uri_ex_e,X0))&iext(uri_rdf_first,X0,uri_ex_x))&iext(uri_rdf_rest,X0,X1)))&iext(uri_rdf_first,X1,uri_ex_y))&iext(uri_rdf_rest,X1,uri_rdf_nil))),
% 7.04/1.66 inference(miniscoping,[status(thm)],[f561])).
% 7.04/1.66 fof(f2407,plain,(
% 7.04/1.66 ((((((iext(uri_rdf_type,uri_ex_z,uri_ex_e)&iext(uri_owl_differentFrom,uri_ex_z,uri_ex_x))&iext(uri_owl_oneOf,uri_ex_e,sK200_skl))&iext(uri_rdf_first,sK200_skl,uri_ex_x))&iext(uri_rdf_rest,sK200_skl,sK199_skl))&iext(uri_rdf_first,sK199_skl,uri_ex_y))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))),
% 7.04/1.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(X1,sK199_skl),skolemize(X0,sK200_skl)],[f2406])).
% 7.04/1.66 fof(f2408,plain,(
% 7.04/1.66 iext(uri_rdf_type,uri_ex_z,uri_ex_e)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2409,plain,(
% 7.04/1.66 iext(uri_owl_differentFrom,uri_ex_z,uri_ex_x)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2410,plain,(
% 7.04/1.66 iext(uri_owl_oneOf,uri_ex_e,sK200_skl)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2411,plain,(
% 7.04/1.66 iext(uri_rdf_first,sK200_skl,uri_ex_x)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2412,plain,(
% 7.04/1.66 iext(uri_rdf_rest,sK200_skl,sK199_skl)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2413,plain,(
% 7.04/1.66 iext(uri_rdf_first,sK199_skl,uri_ex_y)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2414,plain,(
% 7.04/1.66 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 7.04/1.66 inference(cnf_transformation,[status(thm)],[f2407])).
% 7.04/1.66 fof(f2514,plain,(
% 7.04/1.66 ![X0]: (~iext(uri_owl_differentFrom,X0,X0))),
% 7.04/1.66 inference(destructive_equality_resolution,[status(thm)],[f1751])).
% 7.04/1.66 fof(f2515,plain,(
% 7.04/1.66 ![X0]: (iext(uri_owl_sameAs,X0,X0))),
% 7.04/1.66 inference(destructive_equality_resolution,[status(thm)],[f1835])).
% 7.04/1.66 fof(f5008,plain,(
% 7.04/1.66 icext(uri_ex_e,uri_ex_z)),
% 7.04/1.66 inference(resolution,[status(thm)],[f2408,f594])).
% 7.04/1.66 fof(f9269,plain,(
% 7.04/1.66 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK199_skl)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X2,X0)|~icext(X2,X3)|X3=X1|X3=uri_ex_y)),
% 7.04/1.66 inference(resolution,[status(thm)],[f1225,f2413])).
% 7.04/1.66 fof(f9270,plain,(
% 7.04/1.66 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK199_skl)|~iext(uri_owl_oneOf,X2,X0)|~icext(X2,X3)|X3=X1|X3=uri_ex_y)),
% 7.04/1.66 inference(forward_subsumption_resolution,[status(thm)],[f9269,f2414])).
% 7.04/1.66 fof(f9285,plain,(
% 7.04/1.66 ![X0,X1]: (~iext(uri_rdf_rest,sK200_skl,sK199_skl)|~iext(uri_owl_oneOf,X0,sK200_skl)|~icext(X0,X1)|X1=uri_ex_x|X1=uri_ex_y)),
% 7.04/1.66 inference(resolution,[status(thm)],[f9270,f2411])).
% 7.04/1.66 fof(f9287,plain,(
% 7.04/1.66 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK200_skl)|~icext(X0,X1)|X1=uri_ex_x|X1=uri_ex_y)),
% 7.04/1.66 inference(forward_subsumption_resolution,[status(thm)],[f9285,f2412])).
% 7.04/1.66 fof(f9289,plain,(
% 7.04/1.66 ![X0]: (~icext(uri_ex_e,X0)|X0=uri_ex_x|X0=uri_ex_y)),
% 7.04/1.66 inference(resolution,[status(thm)],[f9287,f2410])).
% 7.04/1.66 fof(f9292,plain,(
% 7.04/1.66 uri_ex_z=uri_ex_x|uri_ex_z=uri_ex_y),
% 7.04/1.66 inference(resolution,[status(thm)],[f9289,f5008])).
% 7.04/1.66 fof(f9297,plain,(
% 7.04/1.66 ~iext(uri_owl_sameAs,uri_ex_y,uri_ex_y)|uri_ex_z=uri_ex_x),
% 7.04/1.66 inference(paramodulation,[status(thm)],[f9292,f2405])).
% 7.04/1.66 fof(f9299,plain,(
% 7.04/1.67 uri_ex_z=uri_ex_x),
% 7.04/1.67 inference(forward_subsumption_resolution,[status(thm)],[f9297,f2515])).
% 7.04/1.67 fof(f9301,plain,(
% 7.04/1.67 iext(uri_owl_differentFrom,uri_ex_x,uri_ex_x)),
% 7.04/1.67 inference(backward_demodulation,[status(thm)],[f9299,f2409])).
% 7.04/1.67 fof(f9305,plain,(
% 7.04/1.67 $false),
% 7.04/1.67 inference(forward_subsumption_resolution,[status(thm)],[f9301,f2514])).
% 7.04/1.67 % SZS output end CNFRefutation for theBenchmark.p
% 0.37/1.69 % Elapsed time: 1.307336 seconds
% 0.37/1.69 % CPU time: 9.831445 seconds
% 0.37/1.69 % Total memory used: 180.202 MB
% 0.37/1.69 % Net memory used: 172.781 MB
%------------------------------------------------------------------------------