%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB041+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 : n003.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:42 PM UTC 2026
% Result : Theorem 39.30s 5.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB041+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n003.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 07:45:01 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.55 % Drodi V4.1.1
% 39.30/5.63 % Refutation found
% 39.30/5.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.30/5.63 % SZS output start CNFRefutation for theBenchmark
% 39.30/5.63 fof(f202,axiom,(
% 39.30/5.63 (! [X,Y] :( iext(uri_owl_equivalentClass,X,Y)=> ( ic(X)& ic(Y) ) ) )),
% 39.30/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.30/5.63 fof(f289,axiom,(
% 39.30/5.63 (! [Z,S1,C1,S2,C2] :( ( iext(uri_rdf_first,S1,C1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,C2)& iext(uri_rdf_rest,S2,uri_rdf_nil) )=> ( iext(uri_owl_unionOf,Z,S1)<=> ( ic(Z)& ic(C1)& ic(C2)& (! [X] :( icext(Z,X)<=> ( icext(C1,X)| icext(C2,X) ) ) )) ) ) )),
% 39.30/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.30/5.63 fof(f351,axiom,(
% 39.30/5.63 (! [C1,C2] :( iext(uri_owl_equivalentClass,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)<=> icext(C2,X) ) )) ) )),
% 39.30/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.30/5.63 fof(f559,conjecture,(
% 39.30/5.63 (? [X0,X1] :( 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)& iext(uri_owl_unionOf,uri_ex_c,X0) ) )),
% 39.30/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.30/5.63 fof(f560,negated_conjecture,(
% 39.30/5.63 ~((? [X0,X1] :( 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)& iext(uri_owl_unionOf,uri_ex_c,X0) ) ))),
% 39.30/5.63 inference(negated_conjecture,[status(cth)],[f559])).
% 39.30/5.63 fof(f561,axiom,(
% 39.30/5.63 (? [X2,X1,X0] :( iext(uri_owl_unionOf,X0,X1)& 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)& iext(uri_owl_equivalentClass,uri_ex_c,X0) ) )),
% 39.30/5.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 39.30/5.63 fof(f932,plain,(
% 39.30/5.63 ![X,Y]: (~iext(uri_owl_equivalentClass,X,Y)|(ic(X)&ic(Y)))),
% 39.30/5.63 inference(pre_NNF_transformation,[status(thm)],[f202])).
% 39.30/5.63 fof(f933,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_owl_equivalentClass,X0,X1)|ic(X0))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f932])).
% 39.30/5.63 fof(f1169,plain,(
% 39.30/5.63 ![Z,S1,C1,S2,C2]: ((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|(iext(uri_owl_unionOf,Z,S1)<=>(((ic(Z)&ic(C1))&ic(C2))&(![X]: (icext(Z,X)<=>(icext(C1,X)|icext(C2,X)))))))),
% 39.30/5.63 inference(pre_NNF_transformation,[status(thm)],[f289])).
% 39.30/5.63 fof(f1170,plain,(
% 39.30/5.63 ![Z,S1,C1,S2,C2]: ((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_unionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&(![X]: ((~icext(Z,X)|(icext(C1,X)|icext(C2,X)))&(icext(Z,X)|(~icext(C1,X)&~icext(C2,X)))))))&(iext(uri_owl_unionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]: ((~icext(Z,X)|(~icext(C1,X)&~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)|icext(C2,X)))))))))),
% 39.30/5.63 inference(NNF_transformation,[status(thm)],[f1169])).
% 39.30/5.63 fof(f1171,plain,(
% 39.30/5.63 ![S1,C1,C2]: ((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_unionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]: (~icext(Z,X)|(icext(C1,X)|icext(C2,X))))&(![X]: (icext(Z,X)|(~icext(C1,X)&~icext(C2,X))))))))&(![Z]: (iext(uri_owl_unionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|(?[X]: ((~icext(Z,X)|(~icext(C1,X)&~icext(C2,X)))&(icext(Z,X)|(icext(C1,X)|icext(C2,X))))))))))),
% 39.30/5.63 inference(miniscoping,[status(thm)],[f1170])).
% 39.30/5.63 fof(f1172,plain,(
% 39.30/5.63 ![S1,C1,C2]: ((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_unionOf,Z,S1)|(((ic(Z)&ic(C1))&ic(C2))&((![X]: (~icext(Z,X)|(icext(C1,X)|icext(C2,X))))&(![X]: (icext(Z,X)|(~icext(C1,X)&~icext(C2,X))))))))&(![Z]: (iext(uri_owl_unionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|((~icext(Z,sK7_skl(Z,C2,C1,S1))|(~icext(C1,sK7_skl(Z,C2,C1,S1))&~icext(C2,sK7_skl(Z,C2,C1,S1))))&(icext(Z,sK7_skl(Z,C2,C1,S1))|(icext(C1,sK7_skl(Z,C2,C1,S1))|icext(C2,sK7_skl(Z,C2,C1,S1))))))))))),
% 39.30/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X,sK7_skl(Z,C2,C1,S1))],[f1171])).
% 39.30/5.63 fof(f1174,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|ic(X1))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1175,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|ic(X3))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1176,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|~icext(X4,X5)|icext(X1,X5)|icext(X3,X5))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1177,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|icext(X4,X5)|~icext(X1,X5))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1178,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|icext(X4,X5)|~icext(X3,X5))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1179,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|~icext(X4,sK7_skl(X4,X3,X1,X0))|~icext(X1,sK7_skl(X4,X3,X1,X0)))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1180,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|~icext(X4,sK7_skl(X4,X3,X1,X0))|~icext(X3,sK7_skl(X4,X3,X1,X0)))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1181,plain,(
% 39.30/5.63 ![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_unionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|icext(X4,sK7_skl(X4,X3,X1,X0))|icext(X1,sK7_skl(X4,X3,X1,X0))|icext(X3,sK7_skl(X4,X3,X1,X0)))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1172])).
% 39.30/5.63 fof(f1805,plain,(
% 39.30/5.63 ![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)))))))),
% 39.30/5.63 inference(NNF_transformation,[status(thm)],[f351])).
% 39.30/5.63 fof(f1806,plain,(
% 39.30/5.63 (![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)))))))),
% 39.30/5.63 inference(miniscoping,[status(thm)],[f1805])).
% 39.30/5.63 fof(f1807,plain,(
% 39.30/5.63 (![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)))))))),
% 39.30/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(X,sK123_skl(C2,C1))],[f1806])).
% 39.30/5.63 fof(f1810,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1807])).
% 39.30/5.63 fof(f1811,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|icext(X0,X2)|~icext(X1,X2))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f1807])).
% 39.30/5.63 fof(f2405,plain,(
% 39.30/5.63 (![X0,X1]: ((((~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))|~iext(uri_owl_unionOf,uri_ex_c,X0)))),
% 39.30/5.63 inference(pre_NNF_transformation,[status(thm)],[f560])).
% 39.30/5.63 fof(f2406,plain,(
% 39.30/5.63 ![X0]: ((![X1]: (((~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)))|~iext(uri_owl_unionOf,uri_ex_c,X0))),
% 39.30/5.63 inference(miniscoping,[status(thm)],[f2405])).
% 39.30/5.63 fof(f2407,plain,(
% 39.30/5.63 ![X0,X1]: (~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)|~iext(uri_owl_unionOf,uri_ex_c,X0))),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2406])).
% 39.30/5.63 fof(f2408,plain,(
% 39.30/5.63 ?[X0]: ((?[X2]: (((?[X1]: ((iext(uri_owl_unionOf,X0,X1)&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)))&iext(uri_owl_equivalentClass,uri_ex_c,X0))),
% 39.30/5.63 inference(miniscoping,[status(thm)],[f561])).
% 39.30/5.63 fof(f2409,plain,(
% 39.30/5.63 (((((iext(uri_owl_unionOf,sK199_skl,sK201_skl)&iext(uri_rdf_first,sK201_skl,uri_ex_x))&iext(uri_rdf_rest,sK201_skl,sK200_skl))&iext(uri_rdf_first,sK200_skl,uri_ex_y))&iext(uri_rdf_rest,sK200_skl,uri_rdf_nil))&iext(uri_owl_equivalentClass,uri_ex_c,sK199_skl))),
% 39.30/5.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl]),skolemize(X0,sK199_skl),skolemize(X2,sK200_skl),skolemize(X1,sK201_skl)],[f2408])).
% 39.30/5.63 fof(f2410,plain,(
% 39.30/5.63 iext(uri_owl_unionOf,sK199_skl,sK201_skl)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2411,plain,(
% 39.30/5.63 iext(uri_rdf_first,sK201_skl,uri_ex_x)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2412,plain,(
% 39.30/5.63 iext(uri_rdf_rest,sK201_skl,sK200_skl)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2413,plain,(
% 39.30/5.63 iext(uri_rdf_first,sK200_skl,uri_ex_y)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2414,plain,(
% 39.30/5.63 iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2415,plain,(
% 39.30/5.63 iext(uri_owl_equivalentClass,uri_ex_c,sK199_skl)),
% 39.30/5.63 inference(cnf_transformation,[status(thm)],[f2409])).
% 39.30/5.63 fof(f2556,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,X0,uri_ex_x)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~iext(uri_owl_unionOf,uri_ex_c,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2413,f2407])).
% 39.30/5.63 fof(f2557,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,X0,uri_ex_x)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_unionOf,uri_ex_c,X0))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2556,f2414])).
% 39.30/5.63 fof(f2558,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~iext(uri_owl_unionOf,X2,X0)|ic(X1))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1174,f2413])).
% 39.30/5.63 fof(f2561,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_unionOf,X2,X0)|ic(X1))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2558,f2414])).
% 39.30/5.63 fof(f2562,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~iext(uri_owl_unionOf,X2,X0)|ic(uri_ex_y))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1175,f2413])).
% 39.30/5.63 fof(f2565,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_unionOf,X2,X0)|ic(uri_ex_y))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2562,f2414])).
% 39.30/5.63 fof(f2566,plain,(
% 39.30/5.63 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~iext(uri_owl_unionOf,X2,X0)|~icext(X2,X3)|icext(X1,X3)|icext(uri_ex_y,X3))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1176,f2413])).
% 39.30/5.63 fof(f2569,plain,(
% 39.30/5.63 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_unionOf,X2,X0)|~icext(X2,X3)|icext(X1,X3)|icext(uri_ex_y,X3))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2566,f2414])).
% 39.30/5.63 fof(f2580,plain,(
% 39.30/5.63 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~iext(uri_owl_unionOf,X2,X0)|icext(X2,X3)|~icext(X1,X3))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1177,f2413])).
% 39.30/5.63 fof(f2583,plain,(
% 39.30/5.63 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_unionOf,X2,X0)|icext(X2,X3)|~icext(X1,X3))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2580,f2414])).
% 39.30/5.63 fof(f2805,plain,(
% 39.30/5.63 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(sK199_skl,X3)|~icext(X2,X3))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2410,f1178])).
% 39.30/5.63 fof(f2807,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,sK200_skl)|~icext(sK199_skl,X1)|icext(X0,X1)|icext(uri_ex_y,X1))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2410,f2569])).
% 39.30/5.63 fof(f2808,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,sK200_skl)|icext(sK199_skl,X1)|~icext(X0,X1))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2410,f2583])).
% 39.30/5.63 fof(f2810,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,sK200_skl)|ic(uri_ex_y))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2410,f2565])).
% 39.30/5.63 fof(f2811,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,sK200_skl)|ic(X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2410,f2561])).
% 39.30/5.63 fof(f2825,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~icext(sK199_skl,X1)|icext(X0,X1)|icext(uri_ex_y,X1))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2807,f2412])).
% 39.30/5.63 fof(f2826,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|icext(sK199_skl,X1)|~icext(X0,X1))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2808,f2412])).
% 39.30/5.63 fof(f2827,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,X0)|ic(uri_ex_y))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2810,f2412])).
% 39.30/5.63 fof(f2828,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,X0)|ic(X0))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2811,f2412])).
% 39.30/5.63 fof(f2845,plain,(
% 39.30/5.63 ~iext(uri_rdf_first,sK201_skl,uri_ex_x)|~iext(uri_owl_unionOf,uri_ex_c,sK201_skl)),
% 39.30/5.63 inference(resolution,[status(thm)],[f2412,f2557])).
% 39.30/5.63 fof(f2872,plain,(
% 39.30/5.63 ~iext(uri_owl_unionOf,uri_ex_c,sK201_skl)),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f2845,f2411])).
% 39.30/5.63 fof(f2949,plain,(
% 39.30/5.63 ic(uri_ex_x)),
% 39.30/5.63 inference(resolution,[status(thm)],[f2828,f2411])).
% 39.30/5.63 fof(f2960,plain,(
% 39.30/5.63 ic(uri_ex_y)),
% 39.30/5.63 inference(resolution,[status(thm)],[f2827,f2411])).
% 39.30/5.63 fof(f2964,plain,(
% 39.30/5.63 ![X0]: (icext(sK199_skl,X0)|~icext(uri_ex_x,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2826,f2411])).
% 39.30/5.63 fof(f2965,plain,(
% 39.30/5.63 ![X0]: (~icext(sK199_skl,X0)|icext(uri_ex_x,X0)|icext(uri_ex_y,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2825,f2411])).
% 39.30/5.63 fof(f3046,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|icext(sK199_skl,X2)|~icext(X1,X2))),
% 39.30/5.63 inference(resolution,[status(thm)],[f2805,f2412])).
% 39.30/5.63 fof(f3048,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|icext(sK199_skl,X2)|~icext(X1,X2))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f3046,f2414])).
% 39.30/5.63 fof(f3052,plain,(
% 39.30/5.63 ic(uri_ex_c)),
% 39.30/5.63 inference(resolution,[status(thm)],[f933,f2415])).
% 39.30/5.63 fof(f3077,plain,(
% 39.30/5.63 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|icext(sK199_skl,X1)|~icext(X0,X1))),
% 39.30/5.63 inference(resolution,[status(thm)],[f3048,f2411])).
% 39.30/5.63 fof(f3078,plain,(
% 39.30/5.63 ![X0]: (icext(sK199_skl,X0)|~icext(uri_ex_y,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f3077,f2413])).
% 39.30/5.63 fof(f3415,plain,(
% 39.30/5.63 ![X0]: (~icext(uri_ex_c,X0)|icext(sK199_skl,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1810,f2415])).
% 39.30/5.63 fof(f3416,plain,(
% 39.30/5.63 ![X0]: (icext(uri_ex_c,X0)|~icext(sK199_skl,X0))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1811,f2415])).
% 39.30/5.63 fof(f7664,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|iext(uri_owl_unionOf,X2,X0)|~ic(X2)|~ic(X1)|~ic(uri_ex_y)|icext(X2,sK7_skl(X2,uri_ex_y,X1,X0))|icext(X1,sK7_skl(X2,uri_ex_y,X1,X0))|icext(uri_ex_y,sK7_skl(X2,uri_ex_y,X1,X0)))),
% 39.30/5.63 inference(resolution,[status(thm)],[f1181,f2413])).
% 39.30/5.63 fof(f7670,plain,(
% 39.30/5.63 ![X0,X1,X2]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|iext(uri_owl_unionOf,X2,X0)|~ic(X2)|~ic(X1)|~ic(uri_ex_y)|icext(X2,sK7_skl(X2,uri_ex_y,X1,X0))|icext(X1,sK7_skl(X2,uri_ex_y,X1,X0))|icext(uri_ex_y,sK7_skl(X2,uri_ex_y,X1,X0)))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f7664,f2414])).
% 39.30/5.63 fof(f8813,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_rest,sK201_skl,sK200_skl)|iext(uri_owl_unionOf,X0,sK201_skl)|~ic(X0)|~ic(uri_ex_x)|~ic(uri_ex_y)|icext(X0,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.63 inference(resolution,[status(thm)],[f7670,f2411])).
% 39.30/5.63 fof(f8816,plain,(
% 39.30/5.63 ![X0]: (iext(uri_owl_unionOf,X0,sK201_skl)|~ic(X0)|~ic(uri_ex_x)|~ic(uri_ex_y)|icext(X0,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(X0,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f8813,f2412])).
% 39.30/5.63 fof(f17987,plain,(
% 39.30/5.63 iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_x)|~ic(uri_ex_y)|icext(uri_ex_c,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f8816,f3052])).
% 39.30/5.63 fof(f18061,plain,(
% 39.30/5.63 ~ic(uri_ex_x)|~ic(uri_ex_y)|icext(uri_ex_c,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f17987,f2872])).
% 39.30/5.63 fof(f18158,plain,(
% 39.30/5.63 ~ic(uri_ex_x)|icext(uri_ex_c,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18061,f2960])).
% 39.30/5.63 fof(f18159,plain,(
% 39.30/5.63 icext(uri_ex_c,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f18158,f2949])).
% 39.30/5.63 fof(f18160,plain,(
% 39.30/5.63 icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(sK199_skl,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18159,f3415])).
% 39.30/5.63 fof(f18171,plain,(
% 39.30/5.63 icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(sK199_skl,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f18160,f2964])).
% 39.30/5.63 fof(f18173,plain,(
% 39.30/5.63 icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18171,f2965])).
% 39.30/5.63 fof(f18182,plain,(
% 39.30/5.63 icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(duplicate_literals_removal,[status(thm)],[f18173])).
% 39.30/5.63 fof(f18195,plain,(
% 39.30/5.63 icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(sK199_skl,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18182,f3078])).
% 39.30/5.63 fof(f18204,plain,(
% 39.30/5.63 icext(sK199_skl,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(forward_subsumption_resolution,[status(thm)],[f18195,f2964])).
% 39.30/5.63 fof(f18205,plain,(
% 39.30/5.63 icext(uri_ex_c,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18204,f3416])).
% 39.30/5.63 fof(f18216,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,uri_ex_x)|~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|~icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.63 inference(resolution,[status(thm)],[f18205,f1180])).
% 39.30/5.63 fof(f18217,plain,(
% 39.30/5.63 ![X0]: (~iext(uri_rdf_first,sK201_skl,uri_ex_x)|~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|~icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.68 inference(resolution,[status(thm)],[f18205,f1179])).
% 39.30/5.68 fof(f18227,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|~icext(uri_ex_y,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f18216,f2411])).
% 39.30/5.68 fof(f18228,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|~icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f18217,f2411])).
% 39.30/5.68 fof(f19385,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.68 inference(resolution,[status(thm)],[f18227,f18182])).
% 39.30/5.68 fof(f19386,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|iext(uri_owl_unionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y))),
% 39.30/5.68 inference(backward_subsumption_resolution,[status(thm)],[f18228,f19387])).
% 39.30/5.68 fof(f19387,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)|icext(uri_ex_x,sK7_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl)))),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f19385,f2872])).
% 39.30/5.68 fof(f19388,plain,(
% 39.30/5.68 ![X0]: (~iext(uri_rdf_rest,sK201_skl,X0)|~iext(uri_rdf_first,X0,uri_ex_y)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y))),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f19386,f2872])).
% 39.30/5.68 fof(f19389,plain,(
% 39.30/5.68 ~iext(uri_rdf_first,sK200_skl,uri_ex_y)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)),
% 39.30/5.68 inference(resolution,[status(thm)],[f19388,f2412])).
% 39.30/5.68 fof(f19390,plain,(
% 39.30/5.68 ~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f19389,f2413])).
% 39.30/5.68 fof(f19395,plain,(
% 39.30/5.68 ~ic(uri_ex_c)|~ic(uri_ex_x)|~ic(uri_ex_y)),
% 39.30/5.68 inference(resolution,[status(thm)],[f19390,f2414])).
% 39.30/5.68 fof(f19396,plain,(
% 39.30/5.68 ~ic(uri_ex_x)|~ic(uri_ex_y)),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f19395,f3052])).
% 39.30/5.68 fof(f19397,plain,(
% 39.30/5.68 ~ic(uri_ex_x)),
% 39.30/5.68 inference(resolution,[status(thm)],[f19396,f2960])).
% 39.30/5.68 fof(f19398,plain,(
% 39.30/5.68 $false),
% 39.30/5.68 inference(forward_subsumption_resolution,[status(thm)],[f19397,f2949])).
% 39.30/5.68 % SZS output end CNFRefutation for theBenchmark.p
% 39.30/5.71 % Elapsed time: 5.254679 seconds
% 39.30/5.71 % CPU time: 40.350480 seconds
% 39.30/5.71 % Total memory used: 237.357 MB
% 39.30/5.71 % Net memory used: 228.046 MB
%------------------------------------------------------------------------------