%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB021+2 : 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 : n016.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:34 PM UTC 2026
% Result : Theorem 0.13s 10.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB021+2 : 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.08/10.37 % Computer : n016.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.37 % CPULimit : 300
% 0.08/10.37 % WCLimit : 300
% 0.08/10.37 % DateTime : Mon Sep 21 07:45:20 UTC 2026
% 0.08/10.37 % CPUTime :
% 0.08/10.38 % Drodi V4.1.1
% 0.13/10.57 % Refutation found
% 0.13/10.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/10.57 % SZS output start CNFRefutation for theBenchmark
% 0.13/10.57 fof(f1,axiom,(
% 0.13/10.57 (! [X,Y] :( iext(uri_owl_oneOf,X,Y)=> ( ic(X)& icext(uri_rdf_List,Y) ) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f2,axiom,(
% 0.13/10.57 (! [X,Y] :( iext(uri_owl_unionOf,X,Y)=> ( ic(X)& icext(uri_rdf_List,Y) ) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f3,axiom,(
% 0.13/10.57 (! [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) ) ) )) ) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f4,axiom,(
% 0.13/10.57 (! [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 ) ) )) ) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f5,axiom,(
% 0.13/10.57 (! [Z,S1,A1,S2,A2,S3,A3] :( ( iext(uri_rdf_first,S1,A1)& iext(uri_rdf_rest,S1,S2)& iext(uri_rdf_first,S2,A2)& iext(uri_rdf_rest,S2,S3)& iext(uri_rdf_first,S3,A3)& iext(uri_rdf_rest,S3,uri_rdf_nil) )=> ( iext(uri_owl_oneOf,Z,S1)<=> ( ic(Z)& (! [X] :( icext(Z,X)<=> ( X = A1| X = A2| X = A3 ) ) )) ) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f6,axiom,(
% 0.13/10.57 (! [C1,C2] :( iext(uri_owl_equivalentClass,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)<=> icext(C2,X) ) )) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f7,conjecture,(
% 0.13/10.57 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f8,negated_conjecture,(
% 0.13/10.57 ~(iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) )),
% 0.13/10.57 inference(negated_conjecture,[status(cth)],[f7])).
% 0.13/10.57 fof(f9,axiom,(
% 0.13/10.57 (? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33,BNODE_l41,BNODE_l42] :( iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11)& iext(uri_rdf_first,BNODE_l11,uri_ex_w1)& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)& iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21)& iext(uri_rdf_first,BNODE_l21,uri_ex_w2)& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)& iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31)& iext(uri_rdf_first,BNODE_l31,uri_ex_w1)& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)& iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)& iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41)& iext(uri_rdf_first,BNODE_l41,uri_ex_c1)& iext(uri_rdf_rest,BNODE_l41,BNODE_l42)& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)& iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil) ) )),
% 0.13/10.57 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/10.57 fof(f10,plain,(
% 0.13/10.57 ![X,Y]: (~iext(uri_owl_oneOf,X,Y)|(ic(X)&icext(uri_rdf_List,Y)))),
% 0.13/10.57 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.13/10.57 fof(f11,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_owl_oneOf,X0,X1)|ic(X0))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/10.57 fof(f13,plain,(
% 0.13/10.57 ![X,Y]: (~iext(uri_owl_unionOf,X,Y)|(ic(X)&icext(uri_rdf_List,Y)))),
% 0.13/10.57 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/10.57 fof(f14,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_owl_unionOf,X0,X1)|ic(X0))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/10.57 fof(f16,plain,(
% 0.13/10.57 ![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)))))))),
% 0.13/10.57 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.13/10.57 fof(f17,plain,(
% 0.13/10.57 ![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)))))))))),
% 0.13/10.57 inference(NNF_transformation,[status(thm)],[f16])).
% 0.13/10.57 fof(f18,plain,(
% 0.13/10.57 ![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))))))))))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f17])).
% 0.13/10.57 fof(f19,plain,(
% 0.13/10.57 ![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,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))))))))))),
% 0.13/10.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(Z,C2,C1,S1))],[f18])).
% 0.13/10.57 fof(f23,plain,(
% 0.13/10.57 ![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))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/10.57 fof(f24,plain,(
% 0.13/10.57 ![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))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/10.57 fof(f25,plain,(
% 0.13/10.57 ![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))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/10.57 fof(f29,plain,(
% 0.13/10.57 ![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))))))),
% 0.13/10.57 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.13/10.57 fof(f30,plain,(
% 0.13/10.57 ![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))))))))),
% 0.13/10.57 inference(NNF_transformation,[status(thm)],[f29])).
% 0.13/10.57 fof(f31,plain,(
% 0.13/10.57 ![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)))))))))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f30])).
% 0.13/10.57 fof(f32,plain,(
% 0.13/10.57 ![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,sK1_skl(Z,A2,A1,S1))|(~sK1_skl(Z,A2,A1,S1)=A1&~sK1_skl(Z,A2,A1,S1)=A2))&(icext(Z,sK1_skl(Z,A2,A1,S1))|(sK1_skl(Z,A2,A1,S1)=A1|sK1_skl(Z,A2,A1,S1)=A2))))))))),
% 0.13/10.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X,sK1_skl(Z,A2,A1,S1))],[f31])).
% 0.13/10.57 fof(f34,plain,(
% 0.13/10.57 ![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)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/10.57 fof(f35,plain,(
% 0.13/10.57 ![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)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/10.57 fof(f36,plain,(
% 0.13/10.57 ![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)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/10.57 fof(f40,plain,(
% 0.13/10.57 ![Z,S1,A1,S2,A2,S3,A3]: ((((((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,A3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]: (icext(Z,X)<=>((X=A1|X=A2)|X=A3))))))),
% 0.13/10.57 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/10.57 fof(f41,definition,(
% 0.13/10.57 ![A1,A2,A3,X]: (sP0_prd(X,A3,A2,A1)<=>((X=A1|X=A2)|X=A3))),
% 0.13/10.57 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.13/10.57 fof(f42,plain,(
% 0.13/10.57 ![Z,S1,A1,S2,A2,S3,A3]: ((((((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,A3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]: (icext(Z,X)<=>sP0_prd(X,A3,A2,A1))))))),
% 0.13/10.57 inference(formula_renaming,[status(thm)],[f40,f41])).
% 0.13/10.57 fof(f43,plain,(
% 0.13/10.57 ![Z,S1,A1,S2,A2,S3,A3]: ((((((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,A3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]: ((~icext(Z,X)|sP0_prd(X,A3,A2,A1))&(icext(Z,X)|~sP0_prd(X,A3,A2,A1))))))&(iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~sP0_prd(X,A3,A2,A1))&(icext(Z,X)|sP0_prd(X,A3,A2,A1))))))))),
% 0.13/10.57 inference(NNF_transformation,[status(thm)],[f42])).
% 0.13/10.57 fof(f44,plain,(
% 0.13/10.57 ![S1,A1,A2,A3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,A3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|sP0_prd(X,A3,A2,A1)))&(![X]: (icext(Z,X)|~sP0_prd(X,A3,A2,A1)))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~sP0_prd(X,A3,A2,A1))&(icext(Z,X)|sP0_prd(X,A3,A2,A1)))))))))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f43])).
% 0.13/10.57 fof(f45,plain,(
% 0.13/10.57 ![S1,A1,A2,A3]: ((![S3]: (((![S2]: (((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,S3)))|~iext(uri_rdf_first,S3,A3))|~iext(uri_rdf_rest,S3,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|sP0_prd(X,A3,A2,A1)))&(![X]: (icext(Z,X)|~sP0_prd(X,A3,A2,A1)))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|((~icext(Z,sK2_skl(Z,A3,A2,A1,S1))|~sP0_prd(sK2_skl(Z,A3,A2,A1,S1),A3,A2,A1))&(icext(Z,sK2_skl(Z,A3,A2,A1,S1))|sP0_prd(sK2_skl(Z,A3,A2,A1,S1),A3,A2,A1))))))))),
% 0.13/10.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl(Z,A3,A2,A1,S1))],[f44])).
% 0.13/10.57 fof(f47,plain,(
% 0.13/10.57 ![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_oneOf,X6,X0)|~icext(X6,X7)|sP0_prd(X7,X5,X3,X1))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/10.57 fof(f48,plain,(
% 0.13/10.57 ![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_oneOf,X6,X0)|icext(X6,X7)|~sP0_prd(X7,X5,X3,X1))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/10.57 fof(f51,plain,(
% 0.13/10.57 ![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)))))))),
% 0.13/10.57 inference(NNF_transformation,[status(thm)],[f6])).
% 0.13/10.57 fof(f52,plain,(
% 0.13/10.57 (![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)))))))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f51])).
% 0.13/10.57 fof(f53,plain,(
% 0.13/10.57 (![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,sK3_skl(C2,C1))|~icext(C2,sK3_skl(C2,C1)))&(icext(C1,sK3_skl(C2,C1))|icext(C2,sK3_skl(C2,C1)))))))),
% 0.13/10.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X,sK3_skl(C2,C1))],[f52])).
% 0.13/10.57 fof(f58,plain,(
% 0.13/10.57 ![X0,X1]: (iext(uri_owl_equivalentClass,X0,X1)|~ic(X0)|~ic(X1)|~icext(X0,sK3_skl(X1,X0))|~icext(X1,sK3_skl(X1,X0)))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f53])).
% 0.13/10.57 fof(f59,plain,(
% 0.13/10.57 ![X0,X1]: (iext(uri_owl_equivalentClass,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK3_skl(X1,X0))|icext(X1,sK3_skl(X1,X0)))),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f53])).
% 0.13/10.57 fof(f60,plain,(
% 0.13/10.57 ~iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/10.57 fof(f61,plain,(
% 0.13/10.57 ?[BNODE_l42]: (((?[BNODE_l41]: ((((?[BNODE_l33]: (((?[BNODE_l32]: (((?[BNODE_l31]: ((((?[BNODE_l22]: (((?[BNODE_l21]: ((((?[BNODE_l12]: (((?[BNODE_l11]: ((iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_w1))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12)))&iext(uri_rdf_first,BNODE_l12,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)))&iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22)))&iext(uri_rdf_first,BNODE_l22,uri_ex_w3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)))&iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31))&iext(uri_rdf_first,BNODE_l31,uri_ex_w1))&iext(uri_rdf_rest,BNODE_l31,BNODE_l32)))&iext(uri_rdf_first,BNODE_l32,uri_ex_w2))&iext(uri_rdf_rest,BNODE_l32,BNODE_l33)))&iext(uri_rdf_first,BNODE_l33,uri_ex_w3))&iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)))&iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41))&iext(uri_rdf_first,BNODE_l41,uri_ex_c1))&iext(uri_rdf_rest,BNODE_l41,BNODE_l42)))&iext(uri_rdf_first,BNODE_l42,uri_ex_c2))&iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f9])).
% 0.13/10.57 fof(f62,plain,(
% 0.13/10.57 (((((((((((((((((((((iext(uri_owl_oneOf,uri_ex_c1,sK12_skl)&iext(uri_rdf_first,sK12_skl,uri_ex_w1))&iext(uri_rdf_rest,sK12_skl,sK11_skl))&iext(uri_rdf_first,sK11_skl,uri_ex_w2))&iext(uri_rdf_rest,sK11_skl,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c2,sK10_skl))&iext(uri_rdf_first,sK10_skl,uri_ex_w2))&iext(uri_rdf_rest,sK10_skl,sK9_skl))&iext(uri_rdf_first,sK9_skl,uri_ex_w3))&iext(uri_rdf_rest,sK9_skl,uri_rdf_nil))&iext(uri_owl_oneOf,uri_ex_c3,sK8_skl))&iext(uri_rdf_first,sK8_skl,uri_ex_w1))&iext(uri_rdf_rest,sK8_skl,sK7_skl))&iext(uri_rdf_first,sK7_skl,uri_ex_w2))&iext(uri_rdf_rest,sK7_skl,sK6_skl))&iext(uri_rdf_first,sK6_skl,uri_ex_w3))&iext(uri_rdf_rest,sK6_skl,uri_rdf_nil))&iext(uri_owl_unionOf,uri_ex_c4,sK5_skl))&iext(uri_rdf_first,sK5_skl,uri_ex_c1))&iext(uri_rdf_rest,sK5_skl,sK4_skl))&iext(uri_rdf_first,sK4_skl,uri_ex_c2))&iext(uri_rdf_rest,sK4_skl,uri_rdf_nil))),
% 0.13/10.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(BNODE_l42,sK4_skl),skolemize(BNODE_l41,sK5_skl),skolemize(BNODE_l33,sK6_skl),skolemize(BNODE_l32,sK7_skl),skolemize(BNODE_l31,sK8_skl),skolemize(BNODE_l22,sK9_skl),skolemize(BNODE_l21,sK10_skl),skolemize(BNODE_l12,sK11_skl),skolemize(BNODE_l11,sK12_skl)],[f61])).
% 0.13/10.57 fof(f63,plain,(
% 0.13/10.57 iext(uri_owl_oneOf,uri_ex_c1,sK12_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f64,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK12_skl,uri_ex_w1)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f65,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK12_skl,sK11_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f66,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK11_skl,uri_ex_w2)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f67,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f68,plain,(
% 0.13/10.57 iext(uri_owl_oneOf,uri_ex_c2,sK10_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f69,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK10_skl,uri_ex_w2)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f70,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK10_skl,sK9_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f71,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK9_skl,uri_ex_w3)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f72,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f73,plain,(
% 0.13/10.57 iext(uri_owl_oneOf,uri_ex_c3,sK8_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f74,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK8_skl,uri_ex_w1)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f75,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK8_skl,sK7_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f76,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK7_skl,uri_ex_w2)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f77,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK7_skl,sK6_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f78,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK6_skl,uri_ex_w3)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f79,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f80,plain,(
% 0.13/10.57 iext(uri_owl_unionOf,uri_ex_c4,sK5_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f81,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK5_skl,uri_ex_c1)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f82,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK5_skl,sK4_skl)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f83,plain,(
% 0.13/10.57 iext(uri_rdf_first,sK4_skl,uri_ex_c2)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f84,plain,(
% 0.13/10.57 iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/10.57 fof(f85,plain,(
% 0.13/10.57 ![A1,A2,A3,X]: ((~sP0_prd(X,A3,A2,A1)|((X=A1|X=A2)|X=A3))&(sP0_prd(X,A3,A2,A1)|((~X=A1&~X=A2)&~X=A3)))),
% 0.13/10.57 inference(NNF_transformation,[status(thm)],[f41])).
% 0.13/10.57 fof(f86,plain,(
% 0.13/10.57 (![A1,A2,A3,X]: (~sP0_prd(X,A3,A2,A1)|((X=A1|X=A2)|X=A3)))&(![A1,A2,A3,X]: (sP0_prd(X,A3,A2,A1)|((~X=A1&~X=A2)&~X=A3)))),
% 0.13/10.57 inference(miniscoping,[status(thm)],[f85])).
% 0.13/10.57 fof(f87,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (~sP0_prd(X0,X1,X2,X3)|X0=X3|X0=X2|X0=X1)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/10.57 fof(f88,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X3)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/10.57 fof(f89,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X2)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/10.57 fof(f90,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (sP0_prd(X0,X1,X2,X3)|~X0=X1)),
% 0.13/10.57 inference(cnf_transformation,[status(thm)],[f86])).
% 0.13/10.57 fof(f91,plain,(
% 0.13/10.57 ![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))),
% 0.13/10.57 inference(destructive_equality_resolution,[status(thm)],[f35])).
% 0.13/10.57 fof(f92,plain,(
% 0.13/10.57 ![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))),
% 0.13/10.57 inference(destructive_equality_resolution,[status(thm)],[f36])).
% 0.13/10.57 fof(f93,plain,(
% 0.13/10.57 ![X0,X1,X2]: (sP0_prd(X0,X1,X2,X0))),
% 0.13/10.57 inference(destructive_equality_resolution,[status(thm)],[f88])).
% 0.13/10.57 fof(f94,plain,(
% 0.13/10.57 ![X0,X1,X2]: (sP0_prd(X0,X1,X0,X2))),
% 0.13/10.57 inference(destructive_equality_resolution,[status(thm)],[f89])).
% 0.13/10.57 fof(f95,plain,(
% 0.13/10.57 ![X0,X1,X2]: (sP0_prd(X0,X0,X1,X2))),
% 0.13/10.57 inference(destructive_equality_resolution,[status(thm)],[f90])).
% 0.13/10.57 fof(f97,plain,(
% 0.13/10.57 ic(uri_ex_c3)),
% 0.13/10.57 inference(resolution,[status(thm)],[f11,f73])).
% 0.13/10.57 fof(f102,plain,(
% 0.13/10.57 ic(uri_ex_c4)),
% 0.13/10.57 inference(resolution,[status(thm)],[f14,f80])).
% 0.13/10.57 fof(f114,plain,(
% 0.13/10.57 ![X0]: (iext(uri_owl_equivalentClass,X0,uri_ex_c4)|~ic(X0)|icext(X0,sK3_skl(uri_ex_c4,X0))|icext(uri_ex_c4,sK3_skl(uri_ex_c4,X0)))),
% 0.13/10.57 inference(resolution,[status(thm)],[f59,f102])).
% 0.13/10.57 fof(f121,plain,(
% 0.13/10.57 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|icext(uri_ex_c4,sK3_skl(uri_ex_c4,uri_ex_c3))),
% 0.13/10.57 inference(resolution,[status(thm)],[f114,f97])).
% 0.13/10.57 fof(f123,plain,(
% 0.13/10.57 icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|icext(uri_ex_c4,sK3_skl(uri_ex_c4,uri_ex_c3))),
% 0.13/10.57 inference(forward_subsumption_resolution,[status(thm)],[f121,f60])).
% 0.13/10.57 fof(f141,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK5_skl,X0)|~iext(uri_rdf_rest,sK5_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(uri_ex_c4,X3)|icext(X0,X3)|icext(X2,X3))),
% 0.13/10.57 inference(resolution,[status(thm)],[f23,f80])).
% 0.13/10.57 fof(f142,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK5_skl,X0)|~iext(uri_rdf_rest,sK5_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c4,X3)|~icext(X0,X3))),
% 0.13/10.57 inference(resolution,[status(thm)],[f24,f80])).
% 0.13/10.57 fof(f143,plain,(
% 0.13/10.57 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK5_skl,X0)|~iext(uri_rdf_rest,sK5_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c4,X3)|~icext(X2,X3))),
% 0.13/10.57 inference(resolution,[status(thm)],[f25,f80])).
% 0.13/10.57 fof(f158,plain,(
% 0.13/10.57 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK5_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_c4,X2)|icext(uri_ex_c1,X2)|icext(X1,X2))),
% 0.13/10.57 inference(resolution,[status(thm)],[f141,f81])).
% 0.13/10.57 fof(f163,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|~iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)|~icext(uri_ex_c4,X1)|icext(uri_ex_c1,X1)|icext(X0,X1))),
% 0.13/10.57 inference(resolution,[status(thm)],[f158,f82])).
% 0.13/10.57 fof(f164,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|~icext(uri_ex_c4,X1)|icext(uri_ex_c1,X1)|icext(X0,X1))),
% 0.13/10.57 inference(forward_subsumption_resolution,[status(thm)],[f163,f84])).
% 0.13/10.57 fof(f165,plain,(
% 0.13/10.57 ![X0]: (~icext(uri_ex_c4,X0)|icext(uri_ex_c1,X0)|icext(uri_ex_c2,X0))),
% 0.13/10.57 inference(resolution,[status(thm)],[f164,f83])).
% 0.13/10.57 fof(f166,plain,(
% 0.13/10.57 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK5_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c4,X2)|~icext(uri_ex_c1,X2))),
% 0.13/10.57 inference(resolution,[status(thm)],[f142,f81])).
% 0.13/10.57 fof(f167,plain,(
% 0.13/10.57 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK5_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c4,X2)|~icext(X1,X2))),
% 0.13/10.57 inference(resolution,[status(thm)],[f143,f81])).
% 0.13/10.57 fof(f202,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|~iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)|icext(uri_ex_c4,X1)|~icext(X0,X1))),
% 0.13/10.57 inference(resolution,[status(thm)],[f167,f82])).
% 0.13/10.57 fof(f203,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|icext(uri_ex_c4,X1)|~icext(X0,X1))),
% 0.13/10.57 inference(forward_subsumption_resolution,[status(thm)],[f202,f84])).
% 0.13/10.57 fof(f204,plain,(
% 0.13/10.57 ![X0]: (icext(uri_ex_c4,X0)|~icext(uri_ex_c2,X0))),
% 0.13/10.57 inference(resolution,[status(thm)],[f203,f83])).
% 0.13/10.57 fof(f213,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|~iext(uri_rdf_rest,sK4_skl,uri_rdf_nil)|icext(uri_ex_c4,X1)|~icext(uri_ex_c1,X1))),
% 0.13/10.57 inference(resolution,[status(thm)],[f166,f82])).
% 0.13/10.57 fof(f214,plain,(
% 0.13/10.57 ![X0,X1]: (~iext(uri_rdf_first,sK4_skl,X0)|icext(uri_ex_c4,X1)|~icext(uri_ex_c1,X1))),
% 0.13/10.57 inference(forward_subsumption_resolution,[status(thm)],[f213,f84])).
% 0.13/10.57 fof(f215,plain,(
% 0.13/10.57 ![X0]: (icext(uri_ex_c4,X0)|~icext(uri_ex_c1,X0))),
% 0.13/10.57 inference(resolution,[status(thm)],[f214,f83])).
% 0.13/10.57 fof(f223,plain,(
% 0.13/10.57 ![X0]: (~icext(uri_ex_c1,sK3_skl(uri_ex_c4,X0))|iext(uri_owl_equivalentClass,X0,uri_ex_c4)|~ic(X0)|~ic(uri_ex_c4)|~icext(X0,sK3_skl(uri_ex_c4,X0)))),
% 0.13/10.57 inference(resolution,[status(thm)],[f215,f58])).
% 0.13/10.57 fof(f226,plain,(
% 0.13/10.57 ![X0]: (~icext(uri_ex_c1,sK3_skl(uri_ex_c4,X0))|iext(uri_owl_equivalentClass,X0,uri_ex_c4)|~ic(X0)|~icext(X0,sK3_skl(uri_ex_c4,X0)))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f223,f102])).
% 0.13/10.58 fof(f241,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_first,sK12_skl,X0)|~iext(uri_rdf_rest,sK12_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c1,X0))),
% 0.13/10.58 inference(resolution,[status(thm)],[f91,f63])).
% 0.13/10.58 fof(f249,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_rest,sK12_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c1,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f241,f64])).
% 0.13/10.58 fof(f250,plain,(
% 0.13/10.58 ![X0,X1,X2,X3]: (~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,uri_rdf_nil)|~icext(uri_ex_c2,X3)|X3=X0|X3=X2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f34,f68])).
% 0.13/10.58 fof(f251,plain,(
% 0.13/10.58 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK12_skl,X0)|~iext(uri_rdf_rest,sK12_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(uri_ex_c1,X3)|X3=X0|X3=X2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f34,f63])).
% 0.13/10.58 fof(f253,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~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,uri_rdf_nil)|icext(uri_ex_c2,X2))),
% 0.13/10.58 inference(resolution,[status(thm)],[f92,f68])).
% 0.13/10.58 fof(f254,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_first,sK12_skl,X0)|~iext(uri_rdf_rest,sK12_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c1,X2))),
% 0.13/10.58 inference(resolution,[status(thm)],[f92,f63])).
% 0.13/10.58 fof(f276,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK11_skl,X0)|~iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)|icext(uri_ex_c1,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f249,f65])).
% 0.13/10.58 fof(f277,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK11_skl,X0)|icext(uri_ex_c1,uri_ex_w1))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f276,f67])).
% 0.13/10.58 fof(f278,plain,(
% 0.13/10.58 icext(uri_ex_c1,uri_ex_w1)),
% 0.13/10.58 inference(resolution,[status(thm)],[f277,f66])).
% 0.13/10.58 fof(f279,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_rest,sK10_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c2,X1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f253,f69])).
% 0.13/10.58 fof(f280,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK9_skl,X0)|~iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)|icext(uri_ex_c2,X0))),
% 0.13/10.58 inference(resolution,[status(thm)],[f279,f70])).
% 0.13/10.58 fof(f281,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK9_skl,X0)|icext(uri_ex_c2,X0))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f280,f72])).
% 0.13/10.58 fof(f282,plain,(
% 0.13/10.58 icext(uri_ex_c2,uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f281,f71])).
% 0.13/10.58 fof(f283,plain,(
% 0.13/10.58 icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f282,f204])).
% 0.13/10.58 fof(f285,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_rest,sK12_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c1,X1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f254,f64])).
% 0.13/10.58 fof(f286,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK11_skl,X0)|~iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)|icext(uri_ex_c1,X0))),
% 0.13/10.58 inference(resolution,[status(thm)],[f285,f65])).
% 0.13/10.58 fof(f287,plain,(
% 0.13/10.58 ![X0]: (~iext(uri_rdf_first,sK11_skl,X0)|icext(uri_ex_c1,X0))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f286,f67])).
% 0.13/10.58 fof(f288,plain,(
% 0.13/10.58 icext(uri_ex_c1,uri_ex_w2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f287,f66])).
% 0.13/10.58 fof(f295,plain,(
% 0.13/10.58 ![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_oneOf,X6,X0)|~icext(X6,X7)|X7=X1|X7=X3|X7=X5)),
% 0.13/10.58 inference(resolution,[status(thm)],[f47,f87])).
% 0.13/10.58 fof(f302,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK10_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_c2,X2)|X2=uri_ex_w2|X2=X1)),
% 0.13/10.58 inference(resolution,[status(thm)],[f250,f69])).
% 0.13/10.58 fof(f303,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK9_skl,X0)|~iext(uri_rdf_rest,sK9_skl,uri_rdf_nil)|~icext(uri_ex_c2,X1)|X1=uri_ex_w2|X1=X0)),
% 0.13/10.58 inference(resolution,[status(thm)],[f302,f70])).
% 0.13/10.58 fof(f304,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK9_skl,X0)|~icext(uri_ex_c2,X1)|X1=uri_ex_w2|X1=X0)),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f303,f72])).
% 0.13/10.58 fof(f305,plain,(
% 0.13/10.58 ![X0]: (~icext(uri_ex_c2,X0)|X0=uri_ex_w2|X0=uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f304,f71])).
% 0.13/10.58 fof(f349,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK12_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_c1,X2)|X2=uri_ex_w1|X2=X1)),
% 0.13/10.58 inference(resolution,[status(thm)],[f251,f64])).
% 0.13/10.58 fof(f350,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK11_skl,X0)|~iext(uri_rdf_rest,sK11_skl,uri_rdf_nil)|~icext(uri_ex_c1,X1)|X1=uri_ex_w1|X1=X0)),
% 0.13/10.58 inference(resolution,[status(thm)],[f349,f65])).
% 0.13/10.58 fof(f351,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK11_skl,X0)|~icext(uri_ex_c1,X1)|X1=uri_ex_w1|X1=X0)),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f350,f67])).
% 0.13/10.58 fof(f352,plain,(
% 0.13/10.58 ![X0]: (~icext(uri_ex_c1,X0)|X0=uri_ex_w1|X0=uri_ex_w2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f351,f66])).
% 0.13/10.58 fof(f355,plain,(
% 0.13/10.58 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,sK8_skl,X0)|~iext(uri_rdf_rest,sK8_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_c3,X5)|~sP0_prd(X5,X4,X2,X0))),
% 0.13/10.58 inference(resolution,[status(thm)],[f48,f73])).
% 0.13/10.58 fof(f368,plain,(
% 0.13/10.58 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_rest,sK8_skl,X0)|~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)|icext(uri_ex_c3,X4)|~sP0_prd(X4,X3,X1,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f355,f74])).
% 0.13/10.58 fof(f369,plain,(
% 0.13/10.58 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK7_skl,X0)|~iext(uri_rdf_rest,sK7_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c3,X3)|~sP0_prd(X3,X2,X0,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f368,f75])).
% 0.13/10.58 fof(f370,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK7_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|icext(uri_ex_c3,X2)|~sP0_prd(X2,X1,uri_ex_w2,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f369,f76])).
% 0.13/10.58 fof(f371,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)|icext(uri_ex_c3,X1)|~sP0_prd(X1,X0,uri_ex_w2,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f370,f77])).
% 0.13/10.58 fof(f372,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK6_skl,X0)|icext(uri_ex_c3,X1)|~sP0_prd(X1,X0,uri_ex_w2,uri_ex_w1))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f371,f79])).
% 0.13/10.58 fof(f373,plain,(
% 0.13/10.58 ![X0]: (icext(uri_ex_c3,X0)|~sP0_prd(X0,uri_ex_w3,uri_ex_w2,uri_ex_w1))),
% 0.13/10.58 inference(resolution,[status(thm)],[f372,f78])).
% 0.13/10.58 fof(f375,plain,(
% 0.13/10.58 icext(uri_ex_c3,uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f373,f95])).
% 0.13/10.58 fof(f376,plain,(
% 0.13/10.58 icext(uri_ex_c3,uri_ex_w2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f373,f94])).
% 0.13/10.58 fof(f377,plain,(
% 0.13/10.58 icext(uri_ex_c3,uri_ex_w1)),
% 0.13/10.58 inference(resolution,[status(thm)],[f373,f93])).
% 0.13/10.58 fof(f920,plain,(
% 0.13/10.58 ![X0,X1,X2,X3,X4,X5]: (~iext(uri_rdf_first,sK8_skl,X0)|~iext(uri_rdf_rest,sK8_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_c3,X5)|X5=X0|X5=X2|X5=X4)),
% 0.13/10.58 inference(resolution,[status(thm)],[f295,f73])).
% 0.13/10.58 fof(f955,plain,(
% 0.13/10.58 ![X0,X1,X2,X3,X4]: (~iext(uri_rdf_rest,sK8_skl,X0)|~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)|~icext(uri_ex_c3,X4)|X4=uri_ex_w1|X4=X1|X4=X3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f920,f74])).
% 0.13/10.58 fof(f987,plain,(
% 0.13/10.58 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,sK7_skl,X0)|~iext(uri_rdf_rest,sK7_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~icext(uri_ex_c3,X3)|X3=uri_ex_w1|X3=X0|X3=X2)),
% 0.13/10.58 inference(resolution,[status(thm)],[f955,f75])).
% 0.13/10.58 fof(f988,plain,(
% 0.13/10.58 ![X0,X1,X2]: (~iext(uri_rdf_rest,sK7_skl,X0)|~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~icext(uri_ex_c3,X2)|X2=uri_ex_w1|X2=uri_ex_w2|X2=X1)),
% 0.13/10.58 inference(resolution,[status(thm)],[f987,f76])).
% 0.13/10.58 fof(f989,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK6_skl,X0)|~iext(uri_rdf_rest,sK6_skl,uri_rdf_nil)|~icext(uri_ex_c3,X1)|X1=uri_ex_w1|X1=uri_ex_w2|X1=X0)),
% 0.13/10.58 inference(resolution,[status(thm)],[f988,f77])).
% 0.13/10.58 fof(f990,plain,(
% 0.13/10.58 ![X0,X1]: (~iext(uri_rdf_first,sK6_skl,X0)|~icext(uri_ex_c3,X1)|X1=uri_ex_w1|X1=uri_ex_w2|X1=X0)),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f989,f79])).
% 0.13/10.58 fof(f991,plain,(
% 0.13/10.58 ![X0]: (~icext(uri_ex_c3,X0)|X0=uri_ex_w1|X0=uri_ex_w2|X0=uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f990,f78])).
% 0.13/10.58 fof(f1001,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w1|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|icext(uri_ex_c4,sK3_skl(uri_ex_c4,uri_ex_c3))),
% 0.13/10.58 inference(resolution,[status(thm)],[f991,f123])).
% 0.13/10.58 fof(f1029,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w1|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|icext(uri_ex_c1,sK3_skl(uri_ex_c4,uri_ex_c3))|icext(uri_ex_c2,sK3_skl(uri_ex_c4,uri_ex_c3))),
% 0.13/10.58 inference(resolution,[status(thm)],[f1001,f165])).
% 0.13/10.58 fof(f1037,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w1|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|icext(uri_ex_c2,sK3_skl(uri_ex_c4,uri_ex_c3))),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1029,f352])).
% 0.13/10.58 fof(f1082,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w1|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(resolution,[status(thm)],[f1037,f305])).
% 0.13/10.58 fof(f1084,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w1|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(duplicate_literals_removal,[status(thm)],[f1082])).
% 0.13/10.58 fof(f1086,plain,(
% 0.13/10.58 ~icext(uri_ex_c1,uri_ex_w1)|iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(paramodulation,[status(thm)],[f1084,f226])).
% 0.13/10.58 fof(f1090,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1086,f278])).
% 0.13/10.58 fof(f1293,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(resolution,[status(thm)],[f1090,f97])).
% 0.13/10.58 fof(f1294,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1293,f60])).
% 0.13/10.58 fof(f1300,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w1)|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(paramodulation,[status(thm)],[f1084,f1294])).
% 0.13/10.58 fof(f1301,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w1)|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(duplicate_literals_removal,[status(thm)],[f1300])).
% 0.13/10.58 fof(f1302,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w2|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1301,f377])).
% 0.13/10.58 fof(f1309,plain,(
% 0.13/10.58 ~icext(uri_ex_c1,uri_ex_w2)|iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(paramodulation,[status(thm)],[f1302,f226])).
% 0.13/10.58 fof(f1312,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1309,f288])).
% 0.13/10.58 fof(f1322,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(resolution,[status(thm)],[f1312,f97])).
% 0.13/10.58 fof(f1323,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1322,f60])).
% 0.13/10.58 fof(f1329,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w2)|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(paramodulation,[status(thm)],[f1302,f1323])).
% 0.13/10.58 fof(f1330,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w2)|sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(duplicate_literals_removal,[status(thm)],[f1329])).
% 0.13/10.58 fof(f1379,plain,(
% 0.13/10.58 sK3_skl(uri_ex_c4,uri_ex_c3)=uri_ex_w3),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1330,f376])).
% 0.13/10.58 fof(f1392,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~ic(uri_ex_c4)|~icext(uri_ex_c3,sK3_skl(uri_ex_c4,uri_ex_c3))|~icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(paramodulation,[status(thm)],[f1379,f58])).
% 0.13/10.58 fof(f1395,plain,(
% 0.13/10.58 iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)|~ic(uri_ex_c3)|~ic(uri_ex_c4)|~icext(uri_ex_c3,uri_ex_w3)|~icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(forward_demodulation,[status(thm)],[f1379,f1392])).
% 0.13/10.58 fof(f1396,plain,(
% 0.13/10.58 ~ic(uri_ex_c3)|~ic(uri_ex_c4)|~icext(uri_ex_c3,uri_ex_w3)|~icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1395,f60])).
% 0.13/10.58 fof(f1479,plain,(
% 0.13/10.58 ~ic(uri_ex_c4)|~icext(uri_ex_c3,uri_ex_w3)|~icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f1396,f97])).
% 0.13/10.58 fof(f1480,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w3)|~icext(uri_ex_c4,uri_ex_w3)),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1479,f102])).
% 0.13/10.58 fof(f1481,plain,(
% 0.13/10.58 ~icext(uri_ex_c3,uri_ex_w3)),
% 0.13/10.58 inference(resolution,[status(thm)],[f1480,f283])).
% 0.13/10.58 fof(f1483,plain,(
% 0.13/10.58 $false),
% 0.13/10.58 inference(forward_subsumption_resolution,[status(thm)],[f1481,f375])).
% 0.13/10.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/10.60 % Elapsed time: 0.216582 seconds
% 0.13/10.60 % CPU time: 1.536693 seconds
% 0.13/10.60 % Total memory used: 103.531 MB
% 0.13/10.60 % Net memory used: 100.462 MB
%------------------------------------------------------------------------------