%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB055+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 : n026.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 81.74s 10.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWB055+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.16/0.43 % Computer : n026.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 07:46:52 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.26/0.51 % Drodi V4.1.1
% 81.74/10.92 % Refutation found
% 81.74/10.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 81.74/10.92 % SZS output start CNFRefutation for theBenchmark
% 81.74/10.92 fof(f202,axiom,(
% 81.74/10.92 (! [X,Y] :( iext(uri_owl_equivalentClass,X,Y)=> ( ic(X)& ic(Y) ) ) )),
% 81.74/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 81.74/10.92 fof(f296,axiom,(
% 81.74/10.92 (! [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 ) ) )) ) ) )),
% 81.74/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 81.74/10.92 fof(f351,axiom,(
% 81.74/10.92 (! [C1,C2] :( iext(uri_owl_equivalentClass,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)<=> icext(C2,X) ) )) ) )),
% 81.74/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 81.74/10.92 fof(f559,conjecture,(
% 81.74/10.92 (? [X0,X1] :( iext(uri_rdf_first,X0,uri_ex_y)& iext(uri_rdf_rest,X0,uri_rdf_nil)& iext(uri_owl_oneOf,uri_ex_e,X1)& iext(uri_rdf_first,X1,uri_ex_x)& iext(uri_rdf_rest,X1,X0) ) )),
% 81.74/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 81.74/10.92 fof(f560,negated_conjecture,(
% 81.74/10.92 ~((? [X0,X1] :( iext(uri_rdf_first,X0,uri_ex_y)& iext(uri_rdf_rest,X0,uri_rdf_nil)& iext(uri_owl_oneOf,uri_ex_e,X1)& iext(uri_rdf_first,X1,uri_ex_x)& iext(uri_rdf_rest,X1,X0) ) ))),
% 81.74/10.92 inference(negated_conjecture,[status(cth)],[f559])).
% 81.74/10.92 fof(f561,axiom,(
% 81.74/10.92 (? [X0,X2,X1] :( iext(uri_owl_oneOf,X0,X1)& iext(uri_owl_equivalentClass,uri_ex_e,X0)& iext(uri_rdf_first,X1,uri_ex_x)& iext(uri_rdf_rest,X1,X2)& iext(uri_rdf_first,X2,uri_ex_y)& iext(uri_rdf_rest,X2,uri_rdf_nil) ) )),
% 81.74/10.92 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 81.74/10.92 fof(f932,plain,(
% 81.74/10.92 ![X,Y]: (~iext(uri_owl_equivalentClass,X,Y)|(ic(X)&ic(Y)))),
% 81.74/10.92 inference(pre_NNF_transformation,[status(thm)],[f202])).
% 81.74/10.92 fof(f933,plain,(
% 81.74/10.92 ![X0,X1]: (~iext(uri_owl_equivalentClass,X0,X1)|ic(X0))),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f932])).
% 81.74/10.92 fof(f1220,plain,(
% 81.74/10.92 ![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))))))),
% 81.74/10.92 inference(pre_NNF_transformation,[status(thm)],[f296])).
% 81.74/10.92 fof(f1221,plain,(
% 81.74/10.92 ![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))))))))),
% 81.74/10.92 inference(NNF_transformation,[status(thm)],[f1220])).
% 81.74/10.92 fof(f1222,plain,(
% 81.74/10.92 ![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)))))))))),
% 81.74/10.92 inference(miniscoping,[status(thm)],[f1221])).
% 81.74/10.92 fof(f1223,plain,(
% 81.74/10.92 ![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))))))))),
% 81.74/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X,sK11_skl(Z,A2,A1,S1))],[f1222])).
% 81.74/10.92 fof(f1225,plain,(
% 81.74/10.92 ![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)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1226,plain,(
% 81.74/10.92 ![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)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1227,plain,(
% 81.74/10.92 ![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=X3)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1228,plain,(
% 81.74/10.92 ![X0,X1,X2,X3,X4]: (~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)|~ic(X4)|~icext(X4,sK11_skl(X4,X3,X1,X0))|~sK11_skl(X4,X3,X1,X0)=X1)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1229,plain,(
% 81.74/10.92 ![X0,X1,X2,X3,X4]: (~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)|~ic(X4)|~icext(X4,sK11_skl(X4,X3,X1,X0))|~sK11_skl(X4,X3,X1,X0)=X3)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1230,plain,(
% 81.74/10.92 ![X0,X1,X2,X3,X4]: (~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)|~ic(X4)|icext(X4,sK11_skl(X4,X3,X1,X0))|sK11_skl(X4,X3,X1,X0)=X1|sK11_skl(X4,X3,X1,X0)=X3)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1223])).
% 81.74/10.92 fof(f1805,plain,(
% 81.74/10.92 ![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)))))))),
% 81.74/10.92 inference(NNF_transformation,[status(thm)],[f351])).
% 81.74/10.92 fof(f1806,plain,(
% 81.74/10.92 (![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)))))))),
% 81.74/10.92 inference(miniscoping,[status(thm)],[f1805])).
% 81.74/10.92 fof(f1807,plain,(
% 81.74/10.92 (![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)))))))),
% 81.74/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(X,sK123_skl(C2,C1))],[f1806])).
% 81.74/10.92 fof(f1810,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1807])).
% 81.74/10.92 fof(f1811,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|icext(X0,X2)|~icext(X1,X2))),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f1807])).
% 81.74/10.92 fof(f2405,plain,(
% 81.74/10.92 (![X0,X1]: ((((~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil))|~iext(uri_owl_oneOf,uri_ex_e,X1))|~iext(uri_rdf_first,X1,uri_ex_x))|~iext(uri_rdf_rest,X1,X0)))),
% 81.74/10.92 inference(pre_NNF_transformation,[status(thm)],[f560])).
% 81.74/10.92 fof(f2406,plain,(
% 81.74/10.92 ![X0,X1]: (~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~iext(uri_owl_oneOf,uri_ex_e,X1)|~iext(uri_rdf_first,X1,uri_ex_x)|~iext(uri_rdf_rest,X1,X0))),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2405])).
% 81.74/10.92 fof(f2407,plain,(
% 81.74/10.92 ?[X2]: (((?[X1]: (((?[X0]: (iext(uri_owl_oneOf,X0,X1)&iext(uri_owl_equivalentClass,uri_ex_e,X0)))&iext(uri_rdf_first,X1,uri_ex_x))&iext(uri_rdf_rest,X1,X2)))&iext(uri_rdf_first,X2,uri_ex_y))&iext(uri_rdf_rest,X2,uri_rdf_nil))),
% 81.74/10.92 inference(miniscoping,[status(thm)],[f561])).
% 81.74/10.92 fof(f2408,plain,(
% 81.74/10.92 (((((iext(uri_owl_oneOf,sK201_skl,sK200_skl)&iext(uri_owl_equivalentClass,uri_ex_e,sK201_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))),
% 81.74/10.92 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl]),skolemize(X2,sK199_skl),skolemize(X1,sK200_skl),skolemize(X0,sK201_skl)],[f2407])).
% 81.74/10.92 fof(f2409,plain,(
% 81.74/10.92 iext(uri_owl_oneOf,sK201_skl,sK200_skl)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2410,plain,(
% 81.74/10.92 iext(uri_owl_equivalentClass,uri_ex_e,sK201_skl)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2411,plain,(
% 81.74/10.92 iext(uri_rdf_first,sK200_skl,uri_ex_x)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2412,plain,(
% 81.74/10.92 iext(uri_rdf_rest,sK200_skl,sK199_skl)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2413,plain,(
% 81.74/10.92 iext(uri_rdf_first,sK199_skl,uri_ex_y)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2414,plain,(
% 81.74/10.92 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 81.74/10.92 inference(cnf_transformation,[status(thm)],[f2408])).
% 81.74/10.92 fof(f2512,plain,(
% 81.74/10.92 ![X0,X1,X2,X3,X4]: (~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,X1))),
% 81.74/10.92 inference(destructive_equality_resolution,[status(thm)],[f1226])).
% 81.74/10.92 fof(f2513,plain,(
% 81.74/10.92 ![X0,X1,X2,X3,X4]: (~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,X3))),
% 81.74/10.92 inference(destructive_equality_resolution,[status(thm)],[f1227])).
% 81.74/10.92 fof(f2527,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,uri_ex_e,X0)|~iext(uri_rdf_first,X0,uri_ex_x)|~iext(uri_rdf_rest,X0,sK199_skl))),
% 81.74/10.92 inference(resolution,[status(thm)],[f2413,f2406])).
% 81.74/10.92 fof(f2528,plain,(
% 81.74/10.92 ~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,sK199_skl)),
% 81.74/10.92 inference(resolution,[status(thm)],[f2527,f2411])).
% 81.74/10.92 fof(f2533,plain,(
% 81.74/10.92 ![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)),
% 81.74/10.92 inference(resolution,[status(thm)],[f1225,f2413])).
% 81.74/10.92 fof(f2541,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~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,X1))),
% 81.74/10.92 inference(resolution,[status(thm)],[f2512,f2413])).
% 81.74/10.92 fof(f2544,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK200_skl,sK199_skl)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_x))),
% 81.74/10.92 inference(resolution,[status(thm)],[f2541,f2411])).
% 81.74/10.92 fof(f2547,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~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,uri_ex_y))),
% 81.74/10.92 inference(resolution,[status(thm)],[f2513,f2413])).
% 81.74/10.92 fof(f2550,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK200_skl,sK199_skl)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_y))),
% 81.74/10.92 inference(resolution,[status(thm)],[f2547,f2411])).
% 81.74/10.92 fof(f5147,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_y))),
% 81.74/10.92 inference(backward_subsumption_resolution,[status(thm)],[f2550,f2412])).
% 81.74/10.92 fof(f5148,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_x))),
% 81.74/10.92 inference(backward_subsumption_resolution,[status(thm)],[f2544,f2412])).
% 81.74/10.92 fof(f5149,plain,(
% 81.74/10.92 ~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~iext(uri_owl_oneOf,uri_ex_e,sK200_skl)),
% 81.74/10.92 inference(backward_subsumption_resolution,[status(thm)],[f2528,f2412])).
% 81.74/10.92 fof(f5156,plain,(
% 81.74/10.92 ![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)),
% 81.74/10.92 inference(backward_subsumption_resolution,[status(thm)],[f2533,f2414])).
% 81.74/10.92 fof(f5245,plain,(
% 81.74/10.92 ~iext(uri_owl_oneOf,uri_ex_e,sK200_skl)),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f5149,f2414])).
% 81.74/10.92 fof(f5252,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_y))),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f5147,f2414])).
% 81.74/10.92 fof(f5253,plain,(
% 81.74/10.92 icext(sK201_skl,uri_ex_y)),
% 81.74/10.92 inference(resolution,[status(thm)],[f5252,f2409])).
% 81.74/10.92 fof(f5261,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_owl_oneOf,X0,sK200_skl)|icext(X0,uri_ex_x))),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f5148,f2414])).
% 81.74/10.92 fof(f5262,plain,(
% 81.74/10.92 icext(sK201_skl,uri_ex_x)),
% 81.74/10.92 inference(resolution,[status(thm)],[f5261,f2409])).
% 81.74/10.92 fof(f5270,plain,(
% 81.74/10.92 ![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)),
% 81.74/10.92 inference(resolution,[status(thm)],[f5156,f2411])).
% 81.74/10.92 fof(f5272,plain,(
% 81.74/10.92 ![X0,X1]: (~iext(uri_owl_oneOf,X0,sK200_skl)|~icext(X0,X1)|X1=uri_ex_x|X1=uri_ex_y)),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f5270,f2412])).
% 81.74/10.92 fof(f5370,plain,(
% 81.74/10.92 ![X0]: (~icext(sK201_skl,X0)|X0=uri_ex_x|X0=uri_ex_y)),
% 81.74/10.92 inference(resolution,[status(thm)],[f5272,f2409])).
% 81.74/10.92 fof(f5400,plain,(
% 81.74/10.92 ic(uri_ex_e)),
% 81.74/10.92 inference(resolution,[status(thm)],[f933,f2410])).
% 81.74/10.92 fof(f9421,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~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)|~ic(X2)|icext(X2,sK11_skl(X2,uri_ex_y,X1,X0))|sK11_skl(X2,uri_ex_y,X1,X0)=X1|sK11_skl(X2,uri_ex_y,X1,X0)=uri_ex_y)),
% 81.74/10.92 inference(resolution,[status(thm)],[f1230,f2413])).
% 81.74/10.92 fof(f9423,plain,(
% 81.74/10.92 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK199_skl)|iext(uri_owl_oneOf,X2,X0)|~ic(X2)|icext(X2,sK11_skl(X2,uri_ex_y,X1,X0))|sK11_skl(X2,uri_ex_y,X1,X0)=X1|sK11_skl(X2,uri_ex_y,X1,X0)=uri_ex_y)),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f9421,f2414])).
% 81.74/10.92 fof(f9670,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK200_skl,sK199_skl)|iext(uri_owl_oneOf,X0,sK200_skl)|~ic(X0)|icext(X0,sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl))|sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y)),
% 81.74/10.92 inference(resolution,[status(thm)],[f9423,f2411])).
% 81.74/10.92 fof(f9672,plain,(
% 81.74/10.92 ![X0]: (iext(uri_owl_oneOf,X0,sK200_skl)|~ic(X0)|icext(X0,sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl))|sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(X0,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y)),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f9670,f2412])).
% 81.74/10.92 fof(f10880,plain,(
% 81.74/10.92 iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|icext(uri_ex_e,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl))|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y),
% 81.74/10.92 inference(resolution,[status(thm)],[f9672,f5400])).
% 81.74/10.92 fof(f10951,plain,(
% 81.74/10.92 icext(uri_ex_e,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl))|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f10880,f5245])).
% 81.74/10.92 fof(f18132,plain,(
% 81.74/10.92 ![X0]: (~icext(uri_ex_e,X0)|icext(sK201_skl,X0))),
% 81.74/10.92 inference(resolution,[status(thm)],[f1810,f2410])).
% 81.74/10.92 fof(f18136,plain,(
% 81.74/10.92 icext(sK201_skl,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl))|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y),
% 81.74/10.92 inference(resolution,[status(thm)],[f18132,f10951])).
% 81.74/10.92 fof(f18144,plain,(
% 81.74/10.92 sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_y),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f18136,f5370])).
% 81.74/10.92 fof(f18145,plain,(
% 81.74/10.92 ![X0]: (sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x|~iext(uri_rdf_first,sK200_skl,uri_ex_x)|~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~ic(uri_ex_e)|~icext(uri_ex_e,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)))),
% 81.74/10.92 inference(resolution,[status(thm)],[f18144,f1229])).
% 81.74/10.92 fof(f18149,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_first,sK200_skl,uri_ex_x)|~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~ic(uri_ex_e)|~icext(uri_ex_e,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)))),
% 81.74/10.92 inference(forward_subsumption_resolution,[status(thm)],[f18145,f1228])).
% 81.74/10.92 fof(f18195,plain,(
% 81.74/10.92 ![X0]: (icext(uri_ex_e,X0)|~icext(sK201_skl,X0))),
% 81.74/10.92 inference(resolution,[status(thm)],[f1811,f2410])).
% 81.74/10.92 fof(f18292,plain,(
% 81.74/10.92 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~ic(uri_ex_e)|~icext(uri_ex_e,sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)))),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18149,f2411])).
% 25.89/10.96 fof(f18293,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~ic(uri_ex_e)|~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x)),
% 25.89/10.96 inference(paramodulation,[status(thm)],[f18144,f18292])).
% 25.89/10.96 fof(f18294,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~ic(uri_ex_e)|~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x)),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18293,f5245])).
% 25.89/10.96 fof(f18295,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x)),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18294,f5400])).
% 25.89/10.96 fof(f18296,plain,(
% 25.89/10.96 ~iext(uri_rdf_rest,sK200_skl,sK199_skl)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x),
% 25.89/10.96 inference(resolution,[status(thm)],[f18295,f2413])).
% 25.89/10.96 fof(f18297,plain,(
% 25.89/10.96 ~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18296,f2412])).
% 25.89/10.96 fof(f18298,plain,(
% 25.89/10.96 ~icext(uri_ex_e,uri_ex_y)|sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18297,f2414])).
% 25.89/10.96 fof(f18308,plain,(
% 25.89/10.96 icext(uri_ex_e,uri_ex_x)),
% 25.89/10.96 inference(resolution,[status(thm)],[f18195,f5262])).
% 25.89/10.96 fof(f18309,plain,(
% 25.89/10.96 icext(uri_ex_e,uri_ex_y)),
% 25.89/10.96 inference(resolution,[status(thm)],[f18195,f5253])).
% 25.89/10.96 fof(f18317,plain,(
% 25.89/10.96 sK11_skl(uri_ex_e,uri_ex_y,uri_ex_x,sK200_skl)=uri_ex_x),
% 25.89/10.96 inference(backward_subsumption_resolution,[status(thm)],[f18298,f18309])).
% 25.89/10.96 fof(f18391,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_oneOf,uri_ex_e,sK200_skl)|~ic(uri_ex_e)|~icext(uri_ex_e,uri_ex_x))),
% 25.89/10.96 inference(backward_demodulation,[status(thm)],[f18317,f18292])).
% 25.89/10.96 fof(f18397,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~ic(uri_ex_e)|~icext(uri_ex_e,uri_ex_x))),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18391,f5245])).
% 25.89/10.96 fof(f18405,plain,(
% 25.89/10.96 ![X0]: (~iext(uri_rdf_rest,sK200_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_x))),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18397,f5400])).
% 25.89/10.96 fof(f18406,plain,(
% 25.89/10.96 ~iext(uri_rdf_rest,sK200_skl,sK199_skl)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_x)),
% 25.89/10.96 inference(resolution,[status(thm)],[f18405,f2413])).
% 25.89/10.96 fof(f18407,plain,(
% 25.89/10.96 ~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|~icext(uri_ex_e,uri_ex_x)),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18406,f2412])).
% 25.89/10.96 fof(f18409,plain,(
% 25.89/10.96 ~icext(uri_ex_e,uri_ex_x)),
% 25.89/10.96 inference(forward_subsumption_resolution,[status(thm)],[f18407,f2414])).
% 25.89/10.96 fof(f18410,plain,(
% 25.89/10.96 $false),
% 25.89/10.96 inference(backward_subsumption_resolution,[status(thm)],[f18308,f18409])).
% 25.89/10.96 % SZS output end CNFRefutation for theBenchmark.p
% 25.89/10.98 % Elapsed time: 10.524633 seconds
% 25.89/10.98 % CPU time: 82.579604 seconds
% 25.89/10.98 % Total memory used: 286.654 MB
% 25.89/10.98 % Net memory used: 264.210 MB
%------------------------------------------------------------------------------