%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB020+2 : 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 : n019.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:33 PM UTC 2026
% Result : Theorem 3.08s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB020+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:40:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 3.08/0.84 % Refutation found
% 3.08/0.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.08/0.84 % SZS output start CNFRefutation for theBenchmark
% 3.08/0.84 fof(f2,axiom,(
% 3.08/0.84 (! [Z,C] :( iext(uri_owl_complementOf,Z,C)=> ( ic(Z)& ic(C)& (! [X] :( icext(Z,X)<=> ~ icext(C,X) ) )) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f3,axiom,(
% 3.08/0.84 (! [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) ) ) )) ) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f4,axiom,(
% 3.08/0.84 (! [Z,S1,C1,S2,C2,S3,C3] :( ( iext(uri_rdf_first,S1,C1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,C2)& iext(uri_rdf_rest,S2,S3)& iext(uri_rdf_first,S3,C3)& iext(uri_rdf_rest,S3,uri_rdf_nil) )=> ( iext(uri_owl_unionOf,Z,S1)<=> ( ic(Z)& ic(C1)& ic(C2)& ic(C3)& (! [X] :( icext(Z,X)<=> ( icext(C1,X)| icext(C2,X)| icext(C3,X) ) ) )) ) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f5,axiom,(
% 3.08/0.84 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f6,axiom,(
% 3.08/0.84 (! [C1,C2] :( iext(uri_owl_disjointWith,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :~ ( icext(C1,X)& icext(C2,X) ) )) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f7,conjecture,(
% 3.08/0.84 iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3) ),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f8,negated_conjecture,(
% 3.08/0.84 ~(iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3) )),
% 3.08/0.84 inference(negated_conjecture,[status(cth)],[f7])).
% 3.08/0.84 fof(f9,axiom,(
% 3.08/0.84 (? [BNODE_xs,BNODE_xc,BNODE_lu1,BNODE_lu2,BNODE_lu3,BNODE_li1,BNODE_li2] :( iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1)& iext(uri_rdf_first,BNODE_lu1,uri_ex_c1)& iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2)& iext(uri_rdf_first,BNODE_lu2,uri_ex_c2)& iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3)& iext(uri_rdf_first,BNODE_lu3,uri_ex_c3)& iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil)& iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1)& iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs)& iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1)& iext(uri_rdf_first,BNODE_li1,uri_ex_c)& iext(uri_rdf_rest,BNODE_li1,BNODE_li2)& iext(uri_rdf_first,BNODE_li2,BNODE_xc)& iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil)& iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2) ) )),
% 3.08/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.08/0.84 fof(f13,plain,(
% 3.08/0.84 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&(![X]: (icext(Z,X)<=>~icext(C,X)))))),
% 3.08/0.84 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 3.08/0.84 fof(f14,plain,(
% 3.08/0.84 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&(![X]: ((~icext(Z,X)|~icext(C,X))&(icext(Z,X)|icext(C,X))))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f13])).
% 3.08/0.84 fof(f15,plain,(
% 3.08/0.84 ![Z,C]: (~iext(uri_owl_complementOf,Z,C)|((ic(Z)&ic(C))&((![X]: (~icext(Z,X)|~icext(C,X)))&(![X]: (icext(Z,X)|icext(C,X))))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f14])).
% 3.08/0.84 fof(f17,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_owl_complementOf,X0,X1)|ic(X1))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f15])).
% 3.08/0.84 fof(f18,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_owl_complementOf,X0,X1)|~icext(X0,X2)|~icext(X1,X2))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f15])).
% 3.08/0.84 fof(f20,plain,(
% 3.08/0.84 ![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)))))))),
% 3.08/0.84 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 3.08/0.84 fof(f21,plain,(
% 3.08/0.84 ![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)))))))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f20])).
% 3.08/0.84 fof(f22,plain,(
% 3.08/0.84 ![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))))))))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f21])).
% 3.08/0.84 fof(f23,plain,(
% 3.08/0.84 ![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,sK0_skl(Z,C2,C1,S1))|(~icext(C1,sK0_skl(Z,C2,C1,S1))|~icext(C2,sK0_skl(Z,C2,C1,S1))))&(icext(Z,sK0_skl(Z,C2,C1,S1))|(icext(C1,sK0_skl(Z,C2,C1,S1))&icext(C2,sK0_skl(Z,C2,C1,S1))))))))))),
% 3.08/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(Z,C2,C1,S1))],[f22])).
% 3.08/0.84 fof(f27,plain,(
% 3.08/0.84 ![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))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f23])).
% 3.08/0.84 fof(f28,plain,(
% 3.08/0.84 ![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))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f23])).
% 3.08/0.84 fof(f33,plain,(
% 3.08/0.84 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_unionOf,Z,S1)<=>((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: (icext(Z,X)<=>((icext(C1,X)|icext(C2,X))|icext(C3,X)))))))),
% 3.08/0.84 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 3.08/0.84 fof(f34,definition,(
% 3.08/0.84 ![C1,C2,C3,X]: (sP0_prd(X,C3,C2,C1)<=>((icext(C1,X)|icext(C2,X))|icext(C3,X)))),
% 3.08/0.84 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 3.08/0.84 fof(f35,plain,(
% 3.08/0.84 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_unionOf,Z,S1)<=>((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: (icext(Z,X)<=>sP0_prd(X,C3,C2,C1))))))),
% 3.08/0.84 inference(formula_renaming,[status(thm)],[f33,f34])).
% 3.08/0.84 fof(f36,plain,(
% 3.08/0.84 ![Z,S1,C1,S2,C2,S3,C3]: ((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|((~iext(uri_owl_unionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]: ((~icext(Z,X)|sP0_prd(X,C3,C2,C1))&(icext(Z,X)|~sP0_prd(X,C3,C2,C1))))))&(iext(uri_owl_unionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]: ((~icext(Z,X)|~sP0_prd(X,C3,C2,C1))&(icext(Z,X)|sP0_prd(X,C3,C2,C1))))))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f35])).
% 3.08/0.84 fof(f37,plain,(
% 3.08/0.84 ![S1,C1,C2,C3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_unionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&((![X]: (~icext(Z,X)|sP0_prd(X,C3,C2,C1)))&(![X]: (icext(Z,X)|~sP0_prd(X,C3,C2,C1)))))))&(![Z]: (iext(uri_owl_unionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]: ((~icext(Z,X)|~sP0_prd(X,C3,C2,C1))&(icext(Z,X)|sP0_prd(X,C3,C2,C1)))))))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f36])).
% 3.08/0.84 fof(f38,plain,(
% 3.08/0.84 ![S1,C1,C2,C3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_unionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&((![X]: (~icext(Z,X)|sP0_prd(X,C3,C2,C1)))&(![X]: (icext(Z,X)|~sP0_prd(X,C3,C2,C1)))))))&(![Z]: (iext(uri_owl_unionOf,Z,S1)|((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|((~icext(Z,sK1_skl(Z,C3,C2,C1,S1))|~sP0_prd(sK1_skl(Z,C3,C2,C1,S1),C3,C2,C1))&(icext(Z,sK1_skl(Z,C3,C2,C1,S1))|sP0_prd(sK1_skl(Z,C3,C2,C1,S1),C3,C2,C1))))))))),
% 3.08/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(Z,C3,C2,C1,S1))],[f37])).
% 3.08/0.84 fof(f42,plain,(
% 3.08/0.84 ![X0,X1,X2,X3,X4,X5,X6]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,X4)|~iext(uri_rdf_first,X4,X5)|~iext(uri_rdf_rest,X4,uri_rdf_nil)|~iext(uri_owl_unionOf,X6,X0)|ic(X5))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f38])).
% 3.08/0.84 fof(f43,plain,(
% 3.08/0.84 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,X4)|~iext(uri_rdf_first,X4,X5)|~iext(uri_rdf_rest,X4,uri_rdf_nil)|~iext(uri_owl_unionOf,X6,X0)|~icext(X6,X7)|sP0_prd(X7,X5,X3,X1))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f38])).
% 3.08/0.84 fof(f47,plain,(
% 3.08/0.84 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 3.08/0.84 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 3.08/0.84 fof(f48,plain,(
% 3.08/0.84 ![C1,C2]: ((~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))&(iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f47])).
% 3.08/0.84 fof(f49,plain,(
% 3.08/0.84 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(?[X]: (icext(C1,X)&~icext(C2,X))))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f48])).
% 3.08/0.84 fof(f50,plain,(
% 3.08/0.84 (![C1,C2]: (~iext(uri_rdfs_subClassOf,C1,C2)|((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X))))))&(![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)|((~ic(C1)|~ic(C2))|(icext(C1,sK2_skl(C2,C1))&~icext(C2,sK2_skl(C2,C1))))))),
% 3.08/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl(C2,C1))],[f49])).
% 3.08/0.84 fof(f51,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdfs_subClassOf,X0,X1)|ic(X0))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f50])).
% 3.08/0.84 fof(f52,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdfs_subClassOf,X0,X1)|ic(X1))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f50])).
% 3.08/0.84 fof(f53,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdfs_subClassOf,X0,X1)|~icext(X0,X2)|icext(X1,X2))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f50])).
% 3.08/0.84 fof(f54,plain,(
% 3.08/0.84 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK2_skl(X1,X0)))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f50])).
% 3.08/0.84 fof(f55,plain,(
% 3.08/0.84 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK2_skl(X1,X0)))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f50])).
% 3.08/0.84 fof(f56,plain,(
% 3.08/0.84 ![C1,C2]: (iext(uri_owl_disjointWith,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|~icext(C2,X)))))),
% 3.08/0.84 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 3.08/0.84 fof(f57,plain,(
% 3.08/0.84 ![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))))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f56])).
% 3.08/0.84 fof(f58,plain,(
% 3.08/0.84 (![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))))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f57])).
% 3.08/0.84 fof(f59,plain,(
% 3.08/0.84 (![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,sK3_skl(C2,C1))&icext(C2,sK3_skl(C2,C1))))))),
% 3.08/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(C2,C1))],[f58])).
% 3.08/0.84 fof(f62,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_owl_disjointWith,X0,X1)|~icext(X0,X2)|~icext(X1,X2))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f59])).
% 3.08/0.84 fof(f63,plain,(
% 3.08/0.84 ![X0,X1]: (iext(uri_owl_disjointWith,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK3_skl(X1,X0)))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f59])).
% 3.08/0.84 fof(f64,plain,(
% 3.08/0.84 ![X0,X1]: (iext(uri_owl_disjointWith,X0,X1)|~ic(X0)|~ic(X1)|icext(X1,sK3_skl(X1,X0)))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f59])).
% 3.08/0.84 fof(f65,plain,(
% 3.08/0.84 ~iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f8])).
% 3.08/0.84 fof(f66,plain,(
% 3.08/0.84 ?[BNODE_xc]: ((?[BNODE_li2]: (((?[BNODE_li1]: (((?[BNODE_xs]: ((((?[BNODE_lu3]: (((?[BNODE_lu2]: (((?[BNODE_lu1]: ((iext(uri_owl_unionOf,uri_ex_c,BNODE_lu1)&iext(uri_rdf_first,BNODE_lu1,uri_ex_c1))&iext(uri_rdf_rest,BNODE_lu1,BNODE_lu2)))&iext(uri_rdf_first,BNODE_lu2,uri_ex_c2))&iext(uri_rdf_rest,BNODE_lu2,BNODE_lu3)))&iext(uri_rdf_first,BNODE_lu3,uri_ex_c3))&iext(uri_rdf_rest,BNODE_lu3,uri_rdf_nil)))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,BNODE_xs))&iext(uri_owl_intersectionOf,BNODE_xs,BNODE_li1)))&iext(uri_rdf_first,BNODE_li1,uri_ex_c))&iext(uri_rdf_rest,BNODE_li1,BNODE_li2)))&iext(uri_rdf_first,BNODE_li2,BNODE_xc))&iext(uri_rdf_rest,BNODE_li2,uri_rdf_nil)))&iext(uri_owl_complementOf,BNODE_xc,uri_ex_c2))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f9])).
% 3.08/0.84 fof(f67,plain,(
% 3.08/0.84 ((((((((((((((iext(uri_owl_unionOf,uri_ex_c,sK10_skl)&iext(uri_rdf_first,sK10_skl,uri_ex_c1))&iext(uri_rdf_rest,sK10_skl,sK9_skl))&iext(uri_rdf_first,sK9_skl,uri_ex_c2))&iext(uri_rdf_rest,sK9_skl,sK8_skl))&iext(uri_rdf_first,sK8_skl,uri_ex_c3))&iext(uri_rdf_rest,sK8_skl,uri_rdf_nil))&iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1))&iext(uri_rdfs_subClassOf,uri_ex_d,sK7_skl))&iext(uri_owl_intersectionOf,sK7_skl,sK6_skl))&iext(uri_rdf_first,sK6_skl,uri_ex_c))&iext(uri_rdf_rest,sK6_skl,sK5_skl))&iext(uri_rdf_first,sK5_skl,sK4_skl))&iext(uri_rdf_rest,sK5_skl,uri_rdf_nil))&iext(uri_owl_complementOf,sK4_skl,uri_ex_c2))),
% 3.08/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(BNODE_xc,sK4_skl),skolemize(BNODE_li2,sK5_skl),skolemize(BNODE_li1,sK6_skl),skolemize(BNODE_xs,sK7_skl),skolemize(BNODE_lu3,sK8_skl),skolemize(BNODE_lu2,sK9_skl),skolemize(BNODE_lu1,sK10_skl)],[f66])).
% 3.08/0.84 fof(f68,plain,(
% 3.08/0.84 iext(uri_owl_unionOf,uri_ex_c,sK10_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f69,plain,(
% 3.08/0.84 iext(uri_rdf_first,sK10_skl,uri_ex_c1)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f70,plain,(
% 3.08/0.84 iext(uri_rdf_rest,sK10_skl,sK9_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f71,plain,(
% 3.08/0.84 iext(uri_rdf_first,sK9_skl,uri_ex_c2)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f72,plain,(
% 3.08/0.84 iext(uri_rdf_rest,sK9_skl,sK8_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f73,plain,(
% 3.08/0.84 iext(uri_rdf_first,sK8_skl,uri_ex_c3)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f74,plain,(
% 3.08/0.84 iext(uri_rdf_rest,sK8_skl,uri_rdf_nil)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f75,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_d,uri_ex_c1)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f76,plain,(
% 3.08/0.84 iext(uri_rdfs_subClassOf,uri_ex_d,sK7_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f77,plain,(
% 3.08/0.84 iext(uri_owl_intersectionOf,sK7_skl,sK6_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f78,plain,(
% 3.08/0.84 iext(uri_rdf_first,sK6_skl,uri_ex_c)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f79,plain,(
% 3.08/0.84 iext(uri_rdf_rest,sK6_skl,sK5_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f80,plain,(
% 3.08/0.84 iext(uri_rdf_first,sK5_skl,sK4_skl)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f81,plain,(
% 3.08/0.84 iext(uri_rdf_rest,sK5_skl,uri_rdf_nil)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f82,plain,(
% 3.08/0.84 iext(uri_owl_complementOf,sK4_skl,uri_ex_c2)),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f67])).
% 3.08/0.84 fof(f83,plain,(
% 3.08/0.84 ![C1,C2,C3,X]: ((~sP0_prd(X,C3,C2,C1)|((icext(C1,X)|icext(C2,X))|icext(C3,X)))&(sP0_prd(X,C3,C2,C1)|((~icext(C1,X)&~icext(C2,X))&~icext(C3,X))))),
% 3.08/0.84 inference(NNF_transformation,[status(thm)],[f34])).
% 3.08/0.84 fof(f84,plain,(
% 3.08/0.84 (![C1,C2,C3,X]: (~sP0_prd(X,C3,C2,C1)|((icext(C1,X)|icext(C2,X))|icext(C3,X))))&(![C1,C2,C3,X]: (sP0_prd(X,C3,C2,C1)|((~icext(C1,X)&~icext(C2,X))&~icext(C3,X))))),
% 3.08/0.84 inference(miniscoping,[status(thm)],[f83])).
% 3.08/0.84 fof(f85,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|icext(X3,X0)|icext(X2,X0)|icext(X1,X0))),
% 3.08/0.84 inference(cnf_transformation,[status(thm)],[f84])).
% 3.08/0.84 fof(f89,plain,(
% 3.08/0.84 ![X0]: (~icext(uri_ex_d,X0)|icext(sK7_skl,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f76,f53])).
% 3.08/0.84 fof(f90,plain,(
% 3.08/0.84 ic(sK7_skl)),
% 3.08/0.84 inference(resolution,[status(thm)],[f76,f52])).
% 3.08/0.84 fof(f91,plain,(
% 3.08/0.84 ic(uri_ex_d)),
% 3.08/0.84 inference(resolution,[status(thm)],[f76,f51])).
% 3.08/0.84 fof(f95,plain,(
% 3.08/0.84 ic(uri_ex_c2)),
% 3.08/0.84 inference(resolution,[status(thm)],[f17,f82])).
% 3.08/0.84 fof(f102,plain,(
% 3.08/0.84 ![X0]: (~icext(uri_ex_d,X0)|~icext(uri_ex_c1,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f62,f75])).
% 3.08/0.84 fof(f157,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_rest,sK6_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(sK7_skl,X3)|icext(X0,X3))),
% 3.08/0.84 inference(resolution,[status(thm)],[f27,f77])).
% 3.08/0.84 fof(f158,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_rest,sK6_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(sK7_skl,X3)|icext(X2,X3))),
% 3.08/0.84 inference(resolution,[status(thm)],[f28,f77])).
% 3.08/0.84 fof(f290,plain,(
% 3.08/0.84 ![X0]: (iext(uri_owl_disjointWith,X0,sK7_skl)|~ic(X0)|icext(X0,sK3_skl(sK7_skl,X0)))),
% 3.08/0.84 inference(resolution,[status(thm)],[f63,f90])).
% 3.08/0.84 fof(f311,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)|icext(uri_ex_c2,sK3_skl(sK7_skl,uri_ex_c2))),
% 3.08/0.84 inference(resolution,[status(thm)],[f290,f95])).
% 3.08/0.84 fof(f385,plain,(
% 3.08/0.84 ![X0]: (iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)|~iext(uri_owl_complementOf,X0,uri_ex_c2)|~icext(X0,sK3_skl(sK7_skl,uri_ex_c2)))),
% 3.08/0.84 inference(resolution,[status(thm)],[f311,f18])).
% 3.08/0.84 fof(f440,plain,(
% 3.08/0.84 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_rest,sK10_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,X3)|~iext(uri_rdf_first,X3,X4)|~iext(uri_rdf_rest,X3,uri_rdf_nil)|ic(X4))),
% 3.08/0.84 inference(resolution,[status(thm)],[f42,f68])).
% 3.08/0.84 fof(f441,plain,(
% 3.08/0.84 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_rest,sK10_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,X3)|~iext(uri_rdf_first,X3,X4)|~iext(uri_rdf_rest,X3,uri_rdf_nil)|~icext(uri_ex_c,X5)|sP0_prd(X5,X4,X2,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f43,f68])).
% 3.08/0.84 fof(f466,plain,(
% 3.08/0.84 ![X0]: (iext(uri_owl_disjointWith,X0,sK7_skl)|~ic(X0)|icext(sK7_skl,sK3_skl(sK7_skl,X0)))),
% 3.08/0.84 inference(resolution,[status(thm)],[f64,f90])).
% 3.08/0.84 fof(f609,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_first,sK5_skl,X1)|~iext(uri_rdf_rest,sK5_skl,uri_rdf_nil)|~icext(sK7_skl,X2)|icext(X0,X2))),
% 3.08/0.84 inference(resolution,[status(thm)],[f157,f79])).
% 3.08/0.84 fof(f610,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_first,sK5_skl,X1)|~icext(sK7_skl,X2)|icext(X0,X2))),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f609,f81])).
% 3.08/0.84 fof(f611,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_first,sK5_skl,X1)|~iext(uri_rdf_rest,sK5_skl,uri_rdf_nil)|~icext(sK7_skl,X2)|icext(X1,X2))),
% 3.08/0.84 inference(resolution,[status(thm)],[f158,f79])).
% 3.08/0.84 fof(f612,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_first,sK5_skl,X1)|~icext(sK7_skl,X2)|icext(X1,X2))),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f611,f81])).
% 3.08/0.84 fof(f716,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_rest,sK9_skl,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|ic(X3))),
% 3.08/0.84 inference(resolution,[status(thm)],[f440,f70])).
% 3.08/0.84 fof(f738,plain,(
% 3.08/0.84 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_rest,sK9_skl,X2)|~iext(uri_rdf_first,X2,X3)|~iext(uri_rdf_rest,X2,uri_rdf_nil)|~icext(uri_ex_c,X4)|sP0_prd(X4,X3,X1,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f441,f70])).
% 3.08/0.84 fof(f795,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdf_first,sK5_skl,X0)|~icext(sK7_skl,X1)|icext(uri_ex_c,X1))),
% 3.08/0.84 inference(resolution,[status(thm)],[f610,f78])).
% 3.08/0.84 fof(f796,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdf_first,sK5_skl,X0)|~icext(sK7_skl,X1)|icext(X0,X1))),
% 3.08/0.84 inference(resolution,[status(thm)],[f612,f78])).
% 3.08/0.84 fof(f810,plain,(
% 3.08/0.84 ![X0]: (~icext(sK7_skl,X0)|icext(sK4_skl,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f796,f80])).
% 3.08/0.84 fof(f814,plain,(
% 3.08/0.84 ![X0]: (icext(sK4_skl,sK3_skl(sK7_skl,X0))|iext(uri_owl_disjointWith,X0,sK7_skl)|~ic(X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f810,f466])).
% 3.08/0.84 fof(f869,plain,(
% 3.08/0.84 ![X0]: (~icext(sK7_skl,X0)|icext(uri_ex_c,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f795,f80])).
% 3.08/0.84 fof(f907,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)|~icext(sK4_skl,sK3_skl(sK7_skl,uri_ex_c2))),
% 3.08/0.84 inference(resolution,[status(thm)],[f385,f82])).
% 3.08/0.84 fof(f990,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)|~ic(uri_ex_c2)|iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)),
% 3.08/0.84 inference(resolution,[status(thm)],[f814,f907])).
% 3.08/0.84 fof(f995,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)|~ic(uri_ex_c2)),
% 3.08/0.84 inference(duplicate_literals_removal,[status(thm)],[f990])).
% 3.08/0.84 fof(f996,plain,(
% 3.08/0.84 iext(uri_owl_disjointWith,uri_ex_c2,sK7_skl)),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f995,f95])).
% 3.08/0.84 fof(f997,plain,(
% 3.08/0.84 ![X0]: (~icext(uri_ex_c2,X0)|~icext(sK7_skl,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f996,f62])).
% 3.08/0.84 fof(f1013,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_first,sK8_skl,X2)|~iext(uri_rdf_rest,sK8_skl,uri_rdf_nil)|ic(X2))),
% 3.08/0.84 inference(resolution,[status(thm)],[f716,f72])).
% 3.08/0.84 fof(f1014,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_first,sK8_skl,X2)|ic(X2))),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1013,f74])).
% 3.08/0.84 fof(f1015,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_first,sK8_skl,X2)|~iext(uri_rdf_rest,sK8_skl,uri_rdf_nil)|~icext(uri_ex_c,X3)|sP0_prd(X3,X2,X1,X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f738,f72])).
% 3.08/0.84 fof(f1016,plain,(
% 3.08/0.84 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK10_skl,X0)|~iext(uri_rdf_first,sK9_skl,X1)|~iext(uri_rdf_first,sK8_skl,X2)|~icext(uri_ex_c,X3)|sP0_prd(X3,X2,X1,X0))),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1015,f74])).
% 3.08/0.84 fof(f1252,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdf_first,sK9_skl,X0)|~iext(uri_rdf_first,sK8_skl,X1)|ic(X1))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1014,f69])).
% 3.08/0.84 fof(f1256,plain,(
% 3.08/0.84 ![X0]: (~iext(uri_rdf_first,sK8_skl,X0)|ic(X0))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1252,f71])).
% 3.08/0.84 fof(f1263,plain,(
% 3.08/0.84 ic(uri_ex_c3)),
% 3.08/0.84 inference(resolution,[status(thm)],[f1256,f73])).
% 3.08/0.84 fof(f1274,plain,(
% 3.08/0.84 ![X0]: (iext(uri_rdfs_subClassOf,X0,uri_ex_c3)|~ic(X0)|~icext(uri_ex_c3,sK2_skl(uri_ex_c3,X0)))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1263,f55])).
% 3.08/0.84 fof(f1280,plain,(
% 3.08/0.84 ![X0]: (iext(uri_rdfs_subClassOf,X0,uri_ex_c3)|~ic(X0)|icext(X0,sK2_skl(uri_ex_c3,X0)))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1263,f54])).
% 3.08/0.84 fof(f1355,plain,(
% 3.08/0.84 iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3)|icext(uri_ex_d,sK2_skl(uri_ex_c3,uri_ex_d))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1280,f91])).
% 3.08/0.84 fof(f1357,plain,(
% 3.08/0.84 icext(uri_ex_d,sK2_skl(uri_ex_c3,uri_ex_d))),
% 3.08/0.84 inference(forward_subsumption_resolution,[status(thm)],[f1355,f65])).
% 3.08/0.84 fof(f1575,plain,(
% 3.08/0.84 ![X0,X1,X2]: (~iext(uri_rdf_first,sK9_skl,X0)|~iext(uri_rdf_first,sK8_skl,X1)|~icext(uri_ex_c,X2)|sP0_prd(X2,X1,X0,uri_ex_c1))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1016,f69])).
% 3.08/0.84 fof(f1722,plain,(
% 3.08/0.84 ![X0,X1]: (~iext(uri_rdf_first,sK8_skl,X0)|~icext(uri_ex_c,X1)|sP0_prd(X1,X0,uri_ex_c2,uri_ex_c1))),
% 3.08/0.84 inference(resolution,[status(thm)],[f1575,f71])).
% 3.08/0.84 fof(f1723,plain,(
% 3.08/0.84 ![X0]: (~icext(uri_ex_c,X0)|sP0_prd(X0,uri_ex_c3,uri_ex_c2,uri_ex_c1))),
% 3.08/0.85 inference(resolution,[status(thm)],[f1722,f73])).
% 3.08/0.85 fof(f1724,plain,(
% 3.08/0.85 ![X0]: (~icext(uri_ex_c,X0)|icext(uri_ex_c1,X0)|icext(uri_ex_c2,X0)|icext(uri_ex_c3,X0))),
% 3.08/0.85 inference(resolution,[status(thm)],[f1723,f85])).
% 3.08/0.85 fof(f1727,plain,(
% 3.08/0.85 ![X0]: (~icext(uri_ex_c,X0)|icext(uri_ex_c1,X0)|icext(uri_ex_c3,X0)|~icext(sK7_skl,X0))),
% 3.08/0.85 inference(resolution,[status(thm)],[f1724,f997])).
% 3.08/0.85 fof(f1736,plain,(
% 3.08/0.85 ![X0]: (icext(uri_ex_c1,X0)|icext(uri_ex_c3,X0)|~icext(sK7_skl,X0))),
% 3.08/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1727,f869])).
% 3.08/0.85 fof(f1753,plain,(
% 3.08/0.85 ![X0]: (icext(uri_ex_c3,X0)|~icext(sK7_skl,X0)|~icext(uri_ex_d,X0))),
% 3.08/0.85 inference(resolution,[status(thm)],[f1736,f102])).
% 3.08/0.85 fof(f1761,plain,(
% 3.08/0.85 ![X0]: (icext(uri_ex_c3,X0)|~icext(uri_ex_d,X0))),
% 3.08/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1753,f89])).
% 3.08/0.85 fof(f1765,plain,(
% 3.08/0.85 ![X0]: (~icext(uri_ex_d,sK2_skl(uri_ex_c3,X0))|iext(uri_rdfs_subClassOf,X0,uri_ex_c3)|~ic(X0))),
% 3.08/0.85 inference(resolution,[status(thm)],[f1761,f1274])).
% 3.08/0.85 fof(f1785,plain,(
% 3.08/0.85 iext(uri_rdfs_subClassOf,uri_ex_d,uri_ex_c3)|~ic(uri_ex_d)),
% 3.08/0.85 inference(resolution,[status(thm)],[f1765,f1357])).
% 3.08/0.85 fof(f1786,plain,(
% 3.08/0.85 ~ic(uri_ex_d)),
% 3.08/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1785,f65])).
% 3.08/0.85 fof(f1787,plain,(
% 3.08/0.85 $false),
% 3.08/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1786,f91])).
% 3.08/0.85 % SZS output end CNFRefutation for theBenchmark.p
% 3.08/0.86 % Elapsed time: 0.487471 seconds
% 3.08/0.86 % CPU time: 3.600328 seconds
% 3.08/0.86 % Total memory used: 61.045 MB
% 3.08/0.86 % Net memory used: 56.736 MB
%------------------------------------------------------------------------------