%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB039+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 : n004.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 145.44s 24.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB039+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.18/5.64 % Computer : n004.cluster.edu
% 0.18/5.64 % Model : x86_64 x86_64
% 0.18/5.64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.64 % Memory : 8046.5625MB
% 0.18/5.64 % OS : Linux 6.8.0-71-generic
% 0.18/5.64 % CPULimit : 300
% 0.18/5.64 % WCLimit : 300
% 0.18/5.64 % DateTime : Mon Sep 21 07:43:10 UTC 2026
% 0.18/5.65 % CPUTime :
% 0.21/5.72 % Drodi V4.1.1
% 145.44/24.33 % Refutation found
% 145.44/24.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 145.44/24.33 % SZS output start CNFRefutation for theBenchmark
% 145.44/24.33 fof(f202,axiom,(
% 145.44/24.33 (! [X,Y] :( iext(uri_owl_equivalentClass,X,Y)=> ( ic(X)& ic(Y) ) ) )),
% 145.44/24.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 145.44/24.33 fof(f282,axiom,(
% 145.44/24.33 (! [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_intersectionOf,Z,S1)<=> ( ic(Z)& ic(C1)& ic(C2)& (! [X] :( icext(Z,X)<=> ( icext(C1,X)& icext(C2,X) ) ) )) ) ) )),
% 145.44/24.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 145.44/24.33 fof(f351,axiom,(
% 145.44/24.33 (! [C1,C2] :( iext(uri_owl_equivalentClass,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)<=> icext(C2,X) ) )) ) )),
% 145.44/24.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 145.44/24.33 fof(f559,conjecture,(
% 145.44/24.33 (? [X1,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)& iext(uri_owl_intersectionOf,uri_ex_c,X0) ) )),
% 145.44/24.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 145.44/24.33 fof(f560,negated_conjecture,(
% 145.44/24.33 ~((? [X1,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)& iext(uri_owl_intersectionOf,uri_ex_c,X0) ) ))),
% 145.44/24.33 inference(negated_conjecture,[status(cth)],[f559])).
% 145.44/24.33 fof(f561,axiom,(
% 145.44/24.33 (? [X0,X1,X2] :( iext(uri_rdf_first,X0,uri_ex_y)& iext(uri_rdf_rest,X0,uri_rdf_nil)& iext(uri_owl_intersectionOf,X1,X2)& iext(uri_rdf_first,X2,uri_ex_x)& iext(uri_rdf_rest,X2,X0)& iext(uri_owl_equivalentClass,uri_ex_c,X1) ) )),
% 145.44/24.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 145.44/24.33 fof(f932,plain,(
% 145.44/24.33 ![X,Y]: (~iext(uri_owl_equivalentClass,X,Y)|(ic(X)&ic(Y)))),
% 145.44/24.33 inference(pre_NNF_transformation,[status(thm)],[f202])).
% 145.44/24.33 fof(f933,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_owl_equivalentClass,X0,X1)|ic(X0))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f932])).
% 145.44/24.33 fof(f1117,plain,(
% 145.44/24.33 ![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_intersectionOf,Z,S1)<=>(((ic(Z)&ic(C1))&ic(C2))&(![X]: (icext(Z,X)<=>(icext(C1,X)&icext(C2,X)))))))),
% 145.44/24.33 inference(pre_NNF_transformation,[status(thm)],[f282])).
% 145.44/24.33 fof(f1118,plain,(
% 145.44/24.33 ![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_intersectionOf,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_intersectionOf,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)))))))))),
% 145.44/24.33 inference(NNF_transformation,[status(thm)],[f1117])).
% 145.44/24.33 fof(f1119,plain,(
% 145.44/24.33 ![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_intersectionOf,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_intersectionOf,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))))))))))),
% 145.44/24.33 inference(miniscoping,[status(thm)],[f1118])).
% 145.44/24.33 fof(f1120,plain,(
% 145.44/24.33 ![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_intersectionOf,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_intersectionOf,Z,S1)|(((~ic(Z)|~ic(C1))|~ic(C2))|((~icext(Z,sK3_skl(Z,C2,C1,S1))|(~icext(C1,sK3_skl(Z,C2,C1,S1))|~icext(C2,sK3_skl(Z,C2,C1,S1))))&(icext(Z,sK3_skl(Z,C2,C1,S1))|(icext(C1,sK3_skl(Z,C2,C1,S1))&icext(C2,sK3_skl(Z,C2,C1,S1))))))))))),
% 145.44/24.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(Z,C2,C1,S1))],[f1119])).
% 145.44/24.33 fof(f1122,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|ic(X1))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1123,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|ic(X3))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1124,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|~icext(X4,X5)|icext(X1,X5))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1125,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|~icext(X4,X5)|icext(X3,X5))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1126,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|icext(X4,X5)|~icext(X1,X5)|~icext(X3,X5))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1127,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|~icext(X4,sK3_skl(X4,X3,X1,X0))|~icext(X1,sK3_skl(X4,X3,X1,X0))|~icext(X3,sK3_skl(X4,X3,X1,X0)))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1128,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|icext(X4,sK3_skl(X4,X3,X1,X0))|icext(X1,sK3_skl(X4,X3,X1,X0)))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1129,plain,(
% 145.44/24.33 ![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_intersectionOf,X4,X0)|~ic(X4)|~ic(X1)|~ic(X3)|icext(X4,sK3_skl(X4,X3,X1,X0))|icext(X3,sK3_skl(X4,X3,X1,X0)))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1120])).
% 145.44/24.33 fof(f1805,plain,(
% 145.44/24.33 ![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)))))))),
% 145.44/24.33 inference(NNF_transformation,[status(thm)],[f351])).
% 145.44/24.33 fof(f1806,plain,(
% 145.44/24.33 (![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)))))))),
% 145.44/24.33 inference(miniscoping,[status(thm)],[f1805])).
% 145.44/24.33 fof(f1807,plain,(
% 145.44/24.33 (![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)))))))),
% 145.44/24.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(X,sK123_skl(C2,C1))],[f1806])).
% 145.44/24.33 fof(f1810,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1807])).
% 145.44/24.33 fof(f1811,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_owl_equivalentClass,X0,X1)|icext(X0,X2)|~icext(X1,X2))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f1807])).
% 145.44/24.33 fof(f2405,plain,(
% 145.44/24.33 (![X1,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))|~iext(uri_owl_intersectionOf,uri_ex_c,X0)))),
% 145.44/24.33 inference(pre_NNF_transformation,[status(thm)],[f560])).
% 145.44/24.33 fof(f2406,plain,(
% 145.44/24.33 ![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_intersectionOf,uri_ex_c,X0))),
% 145.44/24.33 inference(miniscoping,[status(thm)],[f2405])).
% 145.44/24.33 fof(f2407,plain,(
% 145.44/24.33 ![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_intersectionOf,uri_ex_c,X0))),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2406])).
% 145.44/24.33 fof(f2408,plain,(
% 145.44/24.33 ?[X1]: ((?[X0,X2]: ((((iext(uri_rdf_first,X0,uri_ex_y)&iext(uri_rdf_rest,X0,uri_rdf_nil))&iext(uri_owl_intersectionOf,X1,X2))&iext(uri_rdf_first,X2,uri_ex_x))&iext(uri_rdf_rest,X2,X0)))&iext(uri_owl_equivalentClass,uri_ex_c,X1))),
% 145.44/24.33 inference(miniscoping,[status(thm)],[f561])).
% 145.44/24.33 fof(f2409,plain,(
% 145.44/24.33 (((((iext(uri_rdf_first,sK200_skl,uri_ex_y)&iext(uri_rdf_rest,sK200_skl,uri_rdf_nil))&iext(uri_owl_intersectionOf,sK199_skl,sK201_skl))&iext(uri_rdf_first,sK201_skl,uri_ex_x))&iext(uri_rdf_rest,sK201_skl,sK200_skl))&iext(uri_owl_equivalentClass,uri_ex_c,sK199_skl))),
% 145.44/24.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl]),skolemize(X1,sK199_skl),skolemize(X0,sK200_skl),skolemize(X2,sK201_skl)],[f2408])).
% 145.44/24.33 fof(f2410,plain,(
% 145.44/24.33 iext(uri_rdf_first,sK200_skl,uri_ex_y)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2411,plain,(
% 145.44/24.33 iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2412,plain,(
% 145.44/24.33 iext(uri_owl_intersectionOf,sK199_skl,sK201_skl)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2413,plain,(
% 145.44/24.33 iext(uri_rdf_first,sK201_skl,uri_ex_x)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2414,plain,(
% 145.44/24.33 iext(uri_rdf_rest,sK201_skl,sK200_skl)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2415,plain,(
% 145.44/24.33 iext(uri_owl_equivalentClass,uri_ex_c,sK199_skl)),
% 145.44/24.33 inference(cnf_transformation,[status(thm)],[f2409])).
% 145.44/24.33 fof(f2555,plain,(
% 145.44/24.33 ![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_intersectionOf,uri_ex_c,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2410,f2407])).
% 145.44/24.33 fof(f2556,plain,(
% 145.44/24.33 ![X0]: (~iext(uri_rdf_first,X0,uri_ex_x)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_owl_intersectionOf,uri_ex_c,X0))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f2555,f2411])).
% 145.44/24.33 fof(f3744,plain,(
% 145.44/24.33 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|icext(X3,X4)|~icext(X1,X4)|~icext(X2,X4))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2411,f1126])).
% 145.44/24.33 fof(f3745,plain,(
% 145.44/24.33 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|~icext(X3,X4)|icext(X2,X4))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2411,f1125])).
% 145.44/24.33 fof(f3746,plain,(
% 145.44/24.33 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|~icext(X3,X4)|icext(X1,X4))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2411,f1124])).
% 145.44/24.33 fof(f3747,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|ic(X2))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2411,f1123])).
% 145.44/24.33 fof(f3748,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|~iext(uri_owl_intersectionOf,X3,X0)|ic(X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f2411,f1122])).
% 145.44/24.33 fof(f3758,plain,(
% 145.44/24.33 ~iext(uri_rdf_first,sK201_skl,uri_ex_x)|~iext(uri_owl_intersectionOf,uri_ex_c,sK201_skl)),
% 145.44/24.33 inference(resolution,[status(thm)],[f2414,f2556])).
% 145.44/24.33 fof(f3760,plain,(
% 145.44/24.33 ~iext(uri_owl_intersectionOf,uri_ex_c,sK201_skl)),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f3758,f2413])).
% 145.44/24.33 fof(f3793,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK201_skl)|icext(X2,X3)|~icext(X0,X3)|~icext(X1,X3))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3744,f2414])).
% 145.44/24.33 fof(f3794,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK201_skl)|~icext(X2,X3)|icext(X1,X3))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3745,f2414])).
% 145.44/24.33 fof(f3795,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK201_skl)|~icext(X2,X3)|icext(X0,X3))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3746,f2414])).
% 145.44/24.33 fof(f3796,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK201_skl)|ic(X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3747,f2414])).
% 145.44/24.33 fof(f3797,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~iext(uri_owl_intersectionOf,X2,sK201_skl)|ic(X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3748,f2414])).
% 145.44/24.33 fof(f3798,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|ic(X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3796,f2412])).
% 145.44/24.33 fof(f3799,plain,(
% 145.44/24.33 ![X0]: (~iext(uri_rdf_first,sK200_skl,X0)|ic(X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3798,f2413])).
% 145.44/24.33 fof(f3800,plain,(
% 145.44/24.33 ic(uri_ex_c)),
% 145.44/24.33 inference(resolution,[status(thm)],[f933,f2415])).
% 145.44/24.33 fof(f3803,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|ic(X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3797,f2412])).
% 145.44/24.33 fof(f3806,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~icext(sK199_skl,X2)|icext(X1,X2))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3794,f2412])).
% 145.44/24.33 fof(f3807,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|~icext(sK199_skl,X1)|icext(X0,X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3806,f2413])).
% 145.44/24.33 fof(f3808,plain,(
% 145.44/24.33 ![X0]: (~icext(sK199_skl,X0)|icext(uri_ex_y,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3807,f2410])).
% 145.44/24.33 fof(f3813,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|~icext(sK199_skl,X2)|icext(X0,X2))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3795,f2412])).
% 145.44/24.33 fof(f3814,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|~icext(sK199_skl,X1)|icext(uri_ex_x,X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3813,f2413])).
% 145.44/24.33 fof(f3815,plain,(
% 145.44/24.33 ![X0]: (~icext(sK199_skl,X0)|icext(uri_ex_x,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3814,f2410])).
% 145.44/24.33 fof(f4022,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|icext(sK199_skl,X2)|~icext(X0,X2)|~icext(X1,X2))),
% 145.44/24.33 inference(resolution,[status(thm)],[f3793,f2412])).
% 145.44/24.33 fof(f4023,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|icext(sK199_skl,X1)|~icext(uri_ex_x,X1)|~icext(X0,X1))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4022,f2413])).
% 145.44/24.33 fof(f4024,plain,(
% 145.44/24.33 ![X0]: (icext(sK199_skl,X0)|~icext(uri_ex_x,X0)|~icext(uri_ex_y,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4023,f2410])).
% 145.44/24.33 fof(f4223,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|~ic(X2)|~icext(X3,sK3_skl(X3,X2,X1,X0))|~icext(X1,sK3_skl(X3,X2,X1,X0))|~icext(X2,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f1127,f2411])).
% 145.44/24.33 fof(f4224,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|~icext(X3,sK3_skl(X3,X2,X1,X0))|~icext(X1,sK3_skl(X3,X2,X1,X0))|~icext(X2,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4223,f3799])).
% 145.44/24.33 fof(f4225,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|~ic(X2)|icext(X3,sK3_skl(X3,X2,X1,X0))|icext(X1,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f1128,f2411])).
% 145.44/24.33 fof(f4226,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|icext(X3,sK3_skl(X3,X2,X1,X0))|icext(X1,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4225,f3799])).
% 145.44/24.33 fof(f4227,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|~ic(X2)|icext(X3,sK3_skl(X3,X2,X1,X0))|icext(X2,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f1129,f2411])).
% 145.44/24.33 fof(f4228,plain,(
% 145.44/24.33 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,sK200_skl)|~iext(uri_rdf_first,sK200_skl,X2)|iext(uri_owl_intersectionOf,X3,X0)|~ic(X3)|~ic(X1)|icext(X3,sK3_skl(X3,X2,X1,X0))|icext(X2,sK3_skl(X3,X2,X1,X0)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4227,f3799])).
% 145.44/24.33 fof(f4238,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|~ic(X0)|~icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|~icext(X0,sK3_skl(X2,X1,X0,sK201_skl))|~icext(X1,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4224,f2414])).
% 145.44/24.33 fof(f4239,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|~icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|~icext(X0,sK3_skl(X2,X1,X0,sK201_skl))|~icext(X1,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4238,f3803])).
% 145.44/24.33 fof(f4248,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|~ic(X0)|icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|icext(X0,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4226,f2414])).
% 145.44/24.33 fof(f4249,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|icext(X0,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4248,f3803])).
% 145.44/24.33 fof(f4250,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|~ic(X0)|icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|icext(X1,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4228,f2414])).
% 145.44/24.33 fof(f4251,plain,(
% 145.44/24.33 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK200_skl,X1)|iext(uri_owl_intersectionOf,X2,sK201_skl)|~ic(X2)|icext(X2,sK3_skl(X2,X1,X0,sK201_skl))|icext(X1,sK3_skl(X2,X1,X0,sK201_skl)))),
% 145.44/24.33 inference(forward_subsumption_resolution,[status(thm)],[f4250,f3803])).
% 145.44/24.33 fof(f4443,plain,(
% 145.44/24.33 ![X0]: (~icext(uri_ex_c,X0)|icext(sK199_skl,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f1810,f2415])).
% 145.44/24.33 fof(f4449,plain,(
% 145.44/24.33 ![X0]: (icext(uri_ex_c,X0)|~icext(sK199_skl,X0))),
% 145.44/24.33 inference(resolution,[status(thm)],[f1811,f2415])).
% 145.44/24.33 fof(f5821,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|iext(uri_owl_intersectionOf,X1,sK201_skl)|~ic(X1)|~icext(X1,sK3_skl(X1,X0,uri_ex_x,sK201_skl))|~icext(uri_ex_x,sK3_skl(X1,X0,uri_ex_x,sK201_skl))|~icext(X0,sK3_skl(X1,X0,uri_ex_x,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4239,f2413])).
% 145.44/24.33 fof(f5831,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|iext(uri_owl_intersectionOf,X1,sK201_skl)|~ic(X1)|icext(X1,sK3_skl(X1,X0,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK3_skl(X1,X0,uri_ex_x,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4249,f2413])).
% 145.44/24.33 fof(f5832,plain,(
% 145.44/24.33 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|iext(uri_owl_intersectionOf,X1,sK201_skl)|~ic(X1)|icext(X1,sK3_skl(X1,X0,uri_ex_x,sK201_skl))|icext(X0,sK3_skl(X1,X0,uri_ex_x,sK201_skl)))),
% 145.44/24.33 inference(resolution,[status(thm)],[f4251,f2413])).
% 145.44/24.33 fof(f6756,plain,(
% 145.44/24.33 ![X0]: (iext(uri_owl_intersectionOf,X0,sK201_skl)|~ic(X0)|~icext(X0,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|~icext(uri_ex_x,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|~icext(uri_ex_y,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl)))),
% 145.44/24.40 inference(resolution,[status(thm)],[f5821,f2410])).
% 145.44/24.40 fof(f6757,plain,(
% 145.44/24.40 ![X0]: (iext(uri_owl_intersectionOf,X0,sK201_skl)|~ic(X0)|icext(X0,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl)))),
% 145.44/24.40 inference(resolution,[status(thm)],[f5831,f2410])).
% 145.44/24.40 fof(f6813,plain,(
% 145.44/24.40 ![X0]: (iext(uri_owl_intersectionOf,X0,sK201_skl)|~ic(X0)|icext(X0,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK3_skl(X0,uri_ex_y,uri_ex_x,sK201_skl)))),
% 145.44/24.40 inference(resolution,[status(thm)],[f5832,f2410])).
% 145.44/24.40 fof(f7932,plain,(
% 145.44/24.40 iext(uri_owl_intersectionOf,uri_ex_c,sK201_skl)|icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f6757,f3800])).
% 145.44/24.40 fof(f8004,plain,(
% 145.44/24.40 icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f7932,f3760])).
% 145.44/24.40 fof(f8006,plain,(
% 145.44/24.40 icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(sK199_skl,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f8004,f4443])).
% 145.44/24.40 fof(f8009,plain,(
% 145.44/24.40 icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8006,f3815])).
% 145.44/24.40 fof(f8035,plain,(
% 145.44/24.40 iext(uri_owl_intersectionOf,uri_ex_c,sK201_skl)|icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f6813,f3800])).
% 145.44/24.40 fof(f8107,plain,(
% 145.44/24.40 icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(uri_ex_y,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8035,f3760])).
% 145.44/24.40 fof(f8173,plain,(
% 145.44/24.40 icext(uri_ex_y,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|icext(sK199_skl,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f8107,f4443])).
% 145.44/24.40 fof(f8176,plain,(
% 145.44/24.40 icext(uri_ex_y,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8173,f3808])).
% 145.44/24.40 fof(f8177,plain,(
% 145.44/24.40 iext(uri_owl_intersectionOf,uri_ex_c,sK201_skl)|~ic(uri_ex_c)|~icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|~icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f8176,f6756])).
% 145.44/24.40 fof(f8178,plain,(
% 145.44/24.40 icext(sK199_skl,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|~icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f8176,f4024])).
% 145.44/24.40 fof(f8181,plain,(
% 145.44/24.40 ~ic(uri_ex_c)|~icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))|~icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8177,f3760])).
% 145.44/24.40 fof(f8182,plain,(
% 145.44/24.40 icext(sK199_skl,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8178,f8009])).
% 145.44/24.40 fof(f8183,plain,(
% 145.44/24.40 icext(uri_ex_c,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(resolution,[status(thm)],[f8182,f4449])).
% 145.44/24.40 fof(f8188,plain,(
% 145.44/24.40 ~ic(uri_ex_c)|~icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(backward_subsumption_resolution,[status(thm)],[f8181,f8183])).
% 145.44/24.40 fof(f8190,plain,(
% 145.44/24.40 ~icext(uri_ex_x,sK3_skl(uri_ex_c,uri_ex_y,uri_ex_x,sK201_skl))),
% 145.44/24.40 inference(forward_subsumption_resolution,[status(thm)],[f8188,f3800])).
% 145.44/24.40 fof(f8191,plain,(
% 145.44/24.40 $false),
% 145.44/24.40 inference(backward_subsumption_resolution,[status(thm)],[f8009,f8190])).
% 145.44/24.40 % SZS output end CNFRefutation for theBenchmark.p
% 104.16/24.46 % Elapsed time: 18.783393 seconds
% 104.16/24.46 % CPU time: 147.588099 seconds
% 104.16/24.46 % Total memory used: 344.709 MB
% 104.16/24.46 % Net memory used: 324.681 MB
%------------------------------------------------------------------------------