%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB058+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 : n009.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 75.33s 10.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB058+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.41 % Computer : n009.cluster.edu
% 0.18/0.41 % Model : x86_64 x86_64
% 0.18/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.41 % Memory : 8046.5625MB
% 0.18/0.41 % OS : Linux 6.8.0-71-generic
% 0.18/0.41 % CPULimit : 300
% 0.18/0.41 % WCLimit : 300
% 0.18/0.41 % DateTime : Mon Sep 21 07:44:27 UTC 2026
% 0.18/0.41 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 75.33/10.03 % Refutation found
% 75.33/10.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.33/10.03 % SZS output start CNFRefutation for theBenchmark
% 75.33/10.03 fof(f241,axiom,(
% 75.33/10.03 (! [X,Y] :( iext(uri_owl_oneOf,X,Y)=> ( ic(X)& icext(uri_rdf_List,Y) ) ) )),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f295,axiom,(
% 75.33/10.03 (! [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 ) )) ) ) )),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f345,axiom,(
% 75.33/10.03 (! [X,Y] :( iext(uri_owl_differentFrom,X,Y)<=> X != Y ) )),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f350,axiom,(
% 75.33/10.03 (! [C1,C2] :( iext(uri_owl_disjointWith,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :~ ( icext(C1,X)& icext(C2,X) ) )) ) )),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f559,conjecture,(
% 75.33/10.03 iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2) ),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f560,negated_conjecture,(
% 75.33/10.03 ~(iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2) )),
% 75.33/10.03 inference(negated_conjecture,[status(cth)],[f559])).
% 75.33/10.03 fof(f561,axiom,(
% 75.33/10.03 (? [X1,X0] :( iext(uri_owl_oneOf,uri_ex_c2,X0)& iext(uri_rdf_first,X1,uri_ex_x)& iext(uri_rdf_rest,X1,uri_rdf_nil)& iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)& iext(uri_owl_oneOf,uri_ex_c1,X1)& iext(uri_rdf_first,X0,uri_ex_y)& iext(uri_rdf_rest,X0,uri_rdf_nil) ) )),
% 75.33/10.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 75.33/10.03 fof(f1009,plain,(
% 75.33/10.03 ![X,Y]: (~iext(uri_owl_oneOf,X,Y)|(ic(X)&icext(uri_rdf_List,Y)))),
% 75.33/10.03 inference(pre_NNF_transformation,[status(thm)],[f241])).
% 75.33/10.03 fof(f1010,plain,(
% 75.33/10.03 ![X0,X1]: (~iext(uri_owl_oneOf,X0,X1)|ic(X0))),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f1009])).
% 75.33/10.03 fof(f1211,plain,(
% 75.33/10.03 ![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)))))),
% 75.33/10.03 inference(pre_NNF_transformation,[status(thm)],[f295])).
% 75.33/10.03 fof(f1212,plain,(
% 75.33/10.03 ![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)))))))),
% 75.33/10.03 inference(NNF_transformation,[status(thm)],[f1211])).
% 75.33/10.03 fof(f1213,plain,(
% 75.33/10.03 ![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))))))))),
% 75.33/10.03 inference(miniscoping,[status(thm)],[f1212])).
% 75.33/10.03 fof(f1214,plain,(
% 75.33/10.03 ![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)))))))),
% 75.33/10.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213])).
% 75.33/10.03 fof(f1216,plain,(
% 75.33/10.03 ![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)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f1214])).
% 75.33/10.03 fof(f1749,plain,(
% 75.33/10.03 ![X,Y]: ((~iext(uri_owl_differentFrom,X,Y)|~X=Y)&(iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 75.33/10.03 inference(NNF_transformation,[status(thm)],[f345])).
% 75.33/10.03 fof(f1750,plain,(
% 75.33/10.03 (![X,Y]: (~iext(uri_owl_differentFrom,X,Y)|~X=Y))&(![X,Y]: (iext(uri_owl_differentFrom,X,Y)|X=Y))),
% 75.33/10.03 inference(miniscoping,[status(thm)],[f1749])).
% 75.33/10.03 fof(f1751,plain,(
% 75.33/10.03 ![X0,X1]: (~iext(uri_owl_differentFrom,X0,X1)|~X0=X1)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f1750])).
% 75.33/10.03 fof(f1796,plain,(
% 75.33/10.03 ![C1,C2]: (iext(uri_owl_disjointWith,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|~icext(C2,X)))))),
% 75.33/10.03 inference(pre_NNF_transformation,[status(thm)],[f350])).
% 75.33/10.03 fof(f1797,plain,(
% 75.33/10.03 ![C1,C2]: ((~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|~icext(C2,X)))))&(iext(uri_owl_disjointWith,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&icext(C2,X))))))),
% 75.33/10.03 inference(NNF_transformation,[status(thm)],[f1796])).
% 75.33/10.03 fof(f1798,plain,(
% 75.33/10.03 (![C1,C2]: (~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|~icext(C2,X))))))&(![C1,C2]: (iext(uri_owl_disjointWith,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&icext(C2,X))))))),
% 75.33/10.03 inference(miniscoping,[status(thm)],[f1797])).
% 75.33/10.03 fof(f1799,plain,(
% 75.33/10.03 (![C1,C2]: (~iext(uri_owl_disjointWith,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|~icext(C2,X))))))&(![C1,C2]: (iext(uri_owl_disjointWith,C1,C2)|((~ic(C1)|~ic(C2))|(icext(C1,sK122_skl(C2,C1))&icext(C2,sK122_skl(C2,C1))))))),
% 75.33/10.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK122_skl]),skolemize(X,sK122_skl(C2,C1))],[f1798])).
% 75.33/10.03 fof(f1803,plain,(
% 75.33/10.03 ![X0,X1]: (iext(uri_owl_disjointWith,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK122_skl(X1,X0)))),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f1799])).
% 75.33/10.03 fof(f1804,plain,(
% 75.33/10.03 ![X0,X1]: (iext(uri_owl_disjointWith,X0,X1)|~ic(X0)|~ic(X1)|icext(X1,sK122_skl(X1,X0)))),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f1799])).
% 75.33/10.03 fof(f2405,plain,(
% 75.33/10.03 ~iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f560])).
% 75.33/10.03 fof(f2406,plain,(
% 75.33/10.03 ?[X0]: (((?[X1]: ((((iext(uri_owl_oneOf,uri_ex_c2,X0)&iext(uri_rdf_first,X1,uri_ex_x))&iext(uri_rdf_rest,X1,uri_rdf_nil))&iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y))&iext(uri_owl_oneOf,uri_ex_c1,X1)))&iext(uri_rdf_first,X0,uri_ex_y))&iext(uri_rdf_rest,X0,uri_rdf_nil))),
% 75.33/10.03 inference(miniscoping,[status(thm)],[f561])).
% 75.33/10.03 fof(f2407,plain,(
% 75.33/10.03 ((((((iext(uri_owl_oneOf,uri_ex_c2,sK199_skl)&iext(uri_rdf_first,sK200_skl,uri_ex_x))&iext(uri_rdf_rest,sK200_skl,uri_rdf_nil))&iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y))&iext(uri_owl_oneOf,uri_ex_c1,sK200_skl))&iext(uri_rdf_first,sK199_skl,uri_ex_y))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))),
% 75.33/10.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl]),skolemize(X0,sK199_skl),skolemize(X1,sK200_skl)],[f2406])).
% 75.33/10.03 fof(f2408,plain,(
% 75.33/10.03 iext(uri_owl_oneOf,uri_ex_c2,sK199_skl)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2409,plain,(
% 75.33/10.03 iext(uri_rdf_first,sK200_skl,uri_ex_x)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2410,plain,(
% 75.33/10.03 iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2411,plain,(
% 75.33/10.03 iext(uri_owl_differentFrom,uri_ex_x,uri_ex_y)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2412,plain,(
% 75.33/10.03 iext(uri_owl_oneOf,uri_ex_c1,sK200_skl)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2413,plain,(
% 75.33/10.03 iext(uri_rdf_first,sK199_skl,uri_ex_y)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2414,plain,(
% 75.33/10.03 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 75.33/10.03 inference(cnf_transformation,[status(thm)],[f2407])).
% 75.33/10.03 fof(f2522,plain,(
% 75.33/10.03 ![X0]: (~iext(uri_owl_differentFrom,X0,X0))),
% 75.33/10.03 inference(destructive_equality_resolution,[status(thm)],[f1751])).
% 75.33/10.03 fof(f3183,plain,(
% 75.33/10.03 ![X0,X1,X2]: (~iext(uri_rdf_first,sK200_skl,X0)|~iext(uri_owl_oneOf,X1,sK200_skl)|~icext(X1,X2)|X2=X0)),
% 75.33/10.03 inference(resolution,[status(thm)],[f2410,f1216])).
% 75.33/10.03 fof(f3324,plain,(
% 75.33/10.03 ![X0,X1,X2]: (~iext(uri_rdf_first,sK199_skl,X0)|~iext(uri_owl_oneOf,X1,sK199_skl)|~icext(X1,X2)|X2=X0)),
% 75.33/10.03 inference(resolution,[status(thm)],[f2414,f1216])).
% 75.33/10.03 fof(f4019,plain,(
% 75.33/10.03 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK200_skl)|~icext(X0,X1)|X1=uri_ex_x)),
% 75.33/10.03 inference(resolution,[status(thm)],[f3183,f2409])).
% 75.33/10.03 fof(f4081,plain,(
% 75.33/10.03 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK199_skl)|~icext(X0,X1)|X1=uri_ex_y)),
% 75.33/10.03 inference(resolution,[status(thm)],[f3324,f2413])).
% 75.33/10.03 fof(f4624,plain,(
% 75.33/10.03 ![X0]: (~icext(uri_ex_c1,X0)|X0=uri_ex_x)),
% 75.33/10.03 inference(resolution,[status(thm)],[f4019,f2412])).
% 75.33/10.03 fof(f4794,plain,(
% 75.33/10.03 ![X0]: (~icext(uri_ex_c2,X0)|X0=uri_ex_y)),
% 75.33/10.03 inference(resolution,[status(thm)],[f4081,f2408])).
% 75.33/10.03 fof(f5686,plain,(
% 75.33/10.03 ic(uri_ex_c1)),
% 75.33/10.03 inference(resolution,[status(thm)],[f1010,f2412])).
% 75.33/10.03 fof(f5687,plain,(
% 75.33/10.03 ic(uri_ex_c2)),
% 75.33/10.03 inference(resolution,[status(thm)],[f1010,f2408])).
% 75.33/10.03 fof(f5697,plain,(
% 75.33/10.03 ![X0]: (iext(uri_owl_disjointWith,X0,uri_ex_c2)|~ic(X0)|icext(uri_ex_c2,sK122_skl(uri_ex_c2,X0)))),
% 75.33/10.07 inference(resolution,[status(thm)],[f5687,f1804])).
% 75.33/10.07 fof(f5698,plain,(
% 75.33/10.07 ![X0]: (iext(uri_owl_disjointWith,X0,uri_ex_c2)|~ic(X0)|icext(X0,sK122_skl(uri_ex_c2,X0)))),
% 75.33/10.07 inference(resolution,[status(thm)],[f5687,f1803])).
% 75.33/10.07 fof(f6067,plain,(
% 75.33/10.07 iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)|icext(uri_ex_c2,sK122_skl(uri_ex_c2,uri_ex_c1))),
% 75.33/10.07 inference(resolution,[status(thm)],[f5697,f5686])).
% 75.33/10.07 fof(f6098,plain,(
% 75.33/10.07 icext(uri_ex_c2,sK122_skl(uri_ex_c2,uri_ex_c1))),
% 75.33/10.07 inference(forward_subsumption_resolution,[status(thm)],[f6067,f2405])).
% 75.33/10.07 fof(f6124,plain,(
% 75.33/10.07 iext(uri_owl_disjointWith,uri_ex_c1,uri_ex_c2)|icext(uri_ex_c1,sK122_skl(uri_ex_c2,uri_ex_c1))),
% 75.33/10.07 inference(resolution,[status(thm)],[f5698,f5686])).
% 75.33/10.07 fof(f6155,plain,(
% 75.33/10.07 icext(uri_ex_c1,sK122_skl(uri_ex_c2,uri_ex_c1))),
% 75.33/10.07 inference(forward_subsumption_resolution,[status(thm)],[f6124,f2405])).
% 75.33/10.07 fof(f6236,plain,(
% 75.33/10.07 sK122_skl(uri_ex_c2,uri_ex_c1)=uri_ex_y),
% 75.33/10.07 inference(resolution,[status(thm)],[f6098,f4794])).
% 75.33/10.07 fof(f6254,plain,(
% 75.33/10.07 icext(uri_ex_c1,uri_ex_y)),
% 75.33/10.07 inference(backward_demodulation,[status(thm)],[f6236,f6155])).
% 75.33/10.07 fof(f6381,plain,(
% 75.33/10.07 uri_ex_y=uri_ex_x),
% 75.33/10.07 inference(resolution,[status(thm)],[f6254,f4624])).
% 75.33/10.07 fof(f6417,plain,(
% 75.33/10.07 iext(uri_owl_differentFrom,uri_ex_x,uri_ex_x)),
% 75.33/10.07 inference(backward_demodulation,[status(thm)],[f6381,f2411])).
% 75.33/10.07 fof(f6464,plain,(
% 75.33/10.07 $false),
% 75.33/10.07 inference(forward_subsumption_resolution,[status(thm)],[f6417,f2522])).
% 75.33/10.07 % SZS output end CNFRefutation for theBenchmark.p
% 75.33/10.10 % Elapsed time: 9.670197 seconds
% 75.33/10.10 % CPU time: 75.827596 seconds
% 75.33/10.10 % Total memory used: 331.454 MB
% 75.33/10.10 % Net memory used: 310.487 MB
%------------------------------------------------------------------------------