%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWB079+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : 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:45 PM UTC 2026
% Result : Theorem 152.51s 19.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB079+1 : 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.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 07:45:34 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.42 % Drodi V4.1.1
% 152.51/19.74 % Refutation found
% 152.51/19.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 152.51/19.74 % SZS output start CNFRefutation for theBenchmark
% 152.51/19.74 fof(f241,axiom,(
% 152.51/19.74 (! [X,Y] :( iext(uri_owl_oneOf,X,Y)=> ( ic(X)& icext(uri_rdf_List,Y) ) ) )),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f295,axiom,(
% 152.51/19.74 (! [Z,S1,A1] :( ( iext(uri_rdf_first,S1,A1)& iext(uri_rdf_rest,S1,uri_rdf_nil) )=> ( iext(uri_owl_oneOf,Z,S1)<=> ( ic(Z)& (! [X] :( icext(Z,X)<=> X = A1 ) )) ) ) )),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f296,axiom,(
% 152.51/19.74 (! [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 ) ) )) ) ) )),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f343,axiom,(
% 152.51/19.74 (! [C1,C2] :( iext(uri_rdfs_subClassOf,C1,C2)<=> ( ic(C1)& ic(C2)& (! [X] :( icext(C1,X)=> icext(C2,X) ) )) ) )),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f559,conjecture,(
% 152.51/19.74 iext(uri_rdfs_subClassOf,uri_ex_c1,uri_ex_c2) ),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f560,negated_conjecture,(
% 152.51/19.74 ~(iext(uri_rdfs_subClassOf,uri_ex_c1,uri_ex_c2) )),
% 152.51/19.74 inference(negated_conjecture,[status(cth)],[f559])).
% 152.51/19.74 fof(f561,axiom,(
% 152.51/19.74 (? [X0,X1,X2] :( iext(uri_owl_oneOf,uri_ex_c2,X0)& iext(uri_rdf_first,X0,uri_ex_w)& iext(uri_rdf_rest,X0,X1)& iext(uri_owl_oneOf,uri_ex_c1,X2)& iext(uri_rdf_first,X2,uri_ex_w)& iext(uri_rdf_rest,X2,uri_rdf_nil)& iext(uri_rdf_first,X1,uri_ex_u)& iext(uri_rdf_rest,X1,uri_rdf_nil) ) )),
% 152.51/19.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 152.51/19.74 fof(f1009,plain,(
% 152.51/19.74 ![X,Y]: (~iext(uri_owl_oneOf,X,Y)|(ic(X)&icext(uri_rdf_List,Y)))),
% 152.51/19.74 inference(pre_NNF_transformation,[status(thm)],[f241])).
% 152.51/19.74 fof(f1010,plain,(
% 152.51/19.74 ![X0,X1]: (~iext(uri_owl_oneOf,X0,X1)|ic(X0))),
% 152.51/19.74 inference(cnf_transformation,[status(thm)],[f1009])).
% 152.51/19.74 fof(f1211,plain,(
% 152.51/19.74 ![Z,S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|(iext(uri_owl_oneOf,Z,S1)<=>(ic(Z)&(![X]: (icext(Z,X)<=>X=A1)))))),
% 152.51/19.74 inference(pre_NNF_transformation,[status(thm)],[f295])).
% 152.51/19.74 fof(f1212,plain,(
% 152.51/19.74 ![Z,S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&(![X]: ((~icext(Z,X)|X=A1)&(icext(Z,X)|~X=A1)))))&(iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~X=A1)&(icext(Z,X)|X=A1)))))))),
% 152.51/19.74 inference(NNF_transformation,[status(thm)],[f1211])).
% 152.51/19.74 fof(f1213,plain,(
% 152.51/19.74 ![S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|X=A1))&(![X]: (icext(Z,X)|~X=A1))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|(?[X]: ((~icext(Z,X)|~X=A1)&(icext(Z,X)|X=A1))))))))),
% 152.51/19.74 inference(miniscoping,[status(thm)],[f1212])).
% 152.51/19.74 fof(f1214,plain,(
% 152.51/19.74 ![S1,A1]: ((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,uri_rdf_nil))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|X=A1))&(![X]: (icext(Z,X)|~X=A1))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|((~icext(Z,sK10_skl(Z,A1,S1))|~sK10_skl(Z,A1,S1)=A1)&(icext(Z,sK10_skl(Z,A1,S1))|sK10_skl(Z,A1,S1)=A1)))))))),
% 152.51/19.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X,sK10_skl(Z,A1,S1))],[f1213])).
% 152.51/19.75 fof(f1216,plain,(
% 152.51/19.75 ![X0,X1,X2,X3]: (~iext(uri_rdf_first,X0,X1)|~iext(uri_rdf_rest,X0,uri_rdf_nil)|~iext(uri_owl_oneOf,X2,X0)|~icext(X2,X3)|X3=X1)),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f1214])).
% 152.51/19.75 fof(f1220,plain,(
% 152.51/19.75 ![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))))))),
% 152.51/19.75 inference(pre_NNF_transformation,[status(thm)],[f296])).
% 152.51/19.75 fof(f1221,plain,(
% 152.51/19.75 ![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))))))))),
% 152.51/19.75 inference(NNF_transformation,[status(thm)],[f1220])).
% 152.51/19.75 fof(f1222,plain,(
% 152.51/19.75 ![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)))))))))),
% 152.51/19.75 inference(miniscoping,[status(thm)],[f1221])).
% 152.51/19.75 fof(f1223,plain,(
% 152.51/19.75 ![S1,A1,A2]: ((![S2]: (((~iext(uri_rdf_first,S1,A1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,A2))|~iext(uri_rdf_rest,S2,uri_rdf_nil)))|((![Z]: (~iext(uri_owl_oneOf,Z,S1)|(ic(Z)&((![X]: (~icext(Z,X)|(X=A1|X=A2)))&(![X]: (icext(Z,X)|(~X=A1&~X=A2)))))))&(![Z]: (iext(uri_owl_oneOf,Z,S1)|(~ic(Z)|((~icext(Z,sK11_skl(Z,A2,A1,S1))|(~sK11_skl(Z,A2,A1,S1)=A1&~sK11_skl(Z,A2,A1,S1)=A2))&(icext(Z,sK11_skl(Z,A2,A1,S1))|(sK11_skl(Z,A2,A1,S1)=A1|sK11_skl(Z,A2,A1,S1)=A2))))))))),
% 152.51/19.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X,sK11_skl(Z,A2,A1,S1))],[f1222])).
% 152.51/19.75 fof(f1226,plain,(
% 152.51/19.75 ![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)),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f1223])).
% 152.51/19.75 fof(f1731,plain,(
% 152.51/19.75 ![C1,C2]: (iext(uri_rdfs_subClassOf,C1,C2)<=>((ic(C1)&ic(C2))&(![X]: (~icext(C1,X)|icext(C2,X)))))),
% 152.51/19.75 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 152.51/19.75 fof(f1732,plain,(
% 152.51/19.75 ![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))))))),
% 152.51/19.75 inference(NNF_transformation,[status(thm)],[f1731])).
% 152.51/19.75 fof(f1733,plain,(
% 152.51/19.75 (![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))))))),
% 152.51/19.75 inference(miniscoping,[status(thm)],[f1732])).
% 152.51/19.75 fof(f1734,plain,(
% 152.51/19.75 (![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,sK115_skl(C2,C1))&~icext(C2,sK115_skl(C2,C1))))))),
% 152.51/19.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK115_skl]),skolemize(X,sK115_skl(C2,C1))],[f1733])).
% 152.51/19.75 fof(f1738,plain,(
% 152.51/19.75 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|icext(X0,sK115_skl(X1,X0)))),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f1734])).
% 152.51/19.75 fof(f1739,plain,(
% 152.51/19.75 ![X0,X1]: (iext(uri_rdfs_subClassOf,X0,X1)|~ic(X0)|~ic(X1)|~icext(X1,sK115_skl(X1,X0)))),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f1734])).
% 152.51/19.75 fof(f2405,plain,(
% 152.51/19.75 ~iext(uri_rdfs_subClassOf,uri_ex_c1,uri_ex_c2)),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f560])).
% 152.51/19.75 fof(f2406,plain,(
% 152.51/19.75 ?[X1]: (((?[X2]: ((((?[X0]: ((iext(uri_owl_oneOf,uri_ex_c2,X0)&iext(uri_rdf_first,X0,uri_ex_w))&iext(uri_rdf_rest,X0,X1)))&iext(uri_owl_oneOf,uri_ex_c1,X2))&iext(uri_rdf_first,X2,uri_ex_w))&iext(uri_rdf_rest,X2,uri_rdf_nil)))&iext(uri_rdf_first,X1,uri_ex_u))&iext(uri_rdf_rest,X1,uri_rdf_nil))),
% 152.51/19.75 inference(miniscoping,[status(thm)],[f561])).
% 152.51/19.75 fof(f2407,plain,(
% 152.51/19.75 (((((((iext(uri_owl_oneOf,uri_ex_c2,sK201_skl)&iext(uri_rdf_first,sK201_skl,uri_ex_w))&iext(uri_rdf_rest,sK201_skl,sK199_skl))&iext(uri_owl_oneOf,uri_ex_c1,sK200_skl))&iext(uri_rdf_first,sK200_skl,uri_ex_w))&iext(uri_rdf_rest,sK200_skl,uri_rdf_nil))&iext(uri_rdf_first,sK199_skl,uri_ex_u))&iext(uri_rdf_rest,sK199_skl,uri_rdf_nil))),
% 152.51/19.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK199_skl,sK200_skl,sK201_skl]),skolemize(X1,sK199_skl),skolemize(X2,sK200_skl),skolemize(X0,sK201_skl)],[f2406])).
% 152.51/19.75 fof(f2408,plain,(
% 152.51/19.75 iext(uri_owl_oneOf,uri_ex_c2,sK201_skl)),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f2407])).
% 152.51/19.75 fof(f2409,plain,(
% 152.51/19.75 iext(uri_rdf_first,sK201_skl,uri_ex_w)),
% 152.51/19.75 inference(cnf_transformation,[status(thm)],[f2407])).
% 152.51/19.75 fof(f2410,plain,(
% 112.25/19.79 iext(uri_rdf_rest,sK201_skl,sK199_skl)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2411,plain,(
% 112.25/19.79 iext(uri_owl_oneOf,uri_ex_c1,sK200_skl)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2412,plain,(
% 112.25/19.79 iext(uri_rdf_first,sK200_skl,uri_ex_w)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2413,plain,(
% 112.25/19.79 iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2414,plain,(
% 112.25/19.79 iext(uri_rdf_first,sK199_skl,uri_ex_u)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2415,plain,(
% 112.25/19.79 iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)),
% 112.25/19.79 inference(cnf_transformation,[status(thm)],[f2407])).
% 112.25/19.79 fof(f2520,plain,(
% 112.25/19.79 ![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))),
% 112.25/19.79 inference(destructive_equality_resolution,[status(thm)],[f1226])).
% 112.25/19.79 fof(f2779,plain,(
% 112.25/19.79 ic(uri_ex_c1)),
% 112.25/19.79 inference(resolution,[status(thm)],[f1010,f2411])).
% 112.25/19.79 fof(f2780,plain,(
% 112.25/19.79 ic(uri_ex_c2)),
% 112.25/19.79 inference(resolution,[status(thm)],[f1010,f2408])).
% 112.25/19.79 fof(f9428,plain,(
% 112.25/19.79 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|~iext(uri_rdf_rest,sK200_skl,uri_rdf_nil)|~icext(uri_ex_c1,X1)|X1=X0)),
% 112.25/19.79 inference(resolution,[status(thm)],[f1216,f2411])).
% 112.25/19.79 fof(f9430,plain,(
% 112.25/19.79 ![X0,X1]: (~iext(uri_rdf_first,sK200_skl,X0)|~icext(uri_ex_c1,X1)|X1=X0)),
% 112.25/19.79 inference(forward_subsumption_resolution,[status(thm)],[f9428,f2413])).
% 112.25/19.79 fof(f9431,plain,(
% 112.25/19.79 ![X0]: (~icext(uri_ex_c1,X0)|X0=uri_ex_w)),
% 112.25/19.79 inference(resolution,[status(thm)],[f9430,f2412])).
% 112.25/19.79 fof(f9751,plain,(
% 112.25/19.79 ![X0,X1,X2]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_rest,sK201_skl,X1)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|icext(uri_ex_c2,X0))),
% 112.25/19.79 inference(resolution,[status(thm)],[f2520,f2408])).
% 112.25/19.79 fof(f9802,plain,(
% 112.25/19.79 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK199_skl,X1)|~iext(uri_rdf_rest,sK199_skl,uri_rdf_nil)|icext(uri_ex_c2,X0))),
% 112.25/19.79 inference(resolution,[status(thm)],[f9751,f2410])).
% 112.25/19.79 fof(f9805,plain,(
% 112.25/19.79 ![X0,X1]: (~iext(uri_rdf_first,sK201_skl,X0)|~iext(uri_rdf_first,sK199_skl,X1)|icext(uri_ex_c2,X0))),
% 112.25/19.79 inference(forward_subsumption_resolution,[status(thm)],[f9802,f2415])).
% 112.25/19.79 fof(f10657,plain,(
% 112.25/19.79 ![X0]: (~iext(uri_rdf_first,sK199_skl,X0)|icext(uri_ex_c2,uri_ex_w))),
% 112.25/19.79 inference(resolution,[status(thm)],[f9805,f2409])).
% 112.25/19.79 fof(f10752,plain,(
% 112.25/19.79 icext(uri_ex_c2,uri_ex_w)),
% 112.25/19.79 inference(resolution,[status(thm)],[f10657,f2414])).
% 112.25/19.79 fof(f18607,plain,(
% 112.25/19.79 ![X0]: (iext(uri_rdfs_subClassOf,uri_ex_c1,X0)|~ic(X0)|icext(uri_ex_c1,sK115_skl(X0,uri_ex_c1)))),
% 112.25/19.79 inference(resolution,[status(thm)],[f1738,f2779])).
% 112.25/19.79 fof(f18877,plain,(
% 112.25/19.79 iext(uri_rdfs_subClassOf,uri_ex_c1,uri_ex_c2)|icext(uri_ex_c1,sK115_skl(uri_ex_c2,uri_ex_c1))),
% 112.25/19.79 inference(resolution,[status(thm)],[f18607,f2780])).
% 112.25/19.79 fof(f18887,plain,(
% 112.25/19.79 icext(uri_ex_c1,sK115_skl(uri_ex_c2,uri_ex_c1))),
% 112.25/19.79 inference(forward_subsumption_resolution,[status(thm)],[f18877,f2405])).
% 112.25/19.79 fof(f19264,plain,(
% 112.25/19.79 sK115_skl(uri_ex_c2,uri_ex_c1)=uri_ex_w),
% 112.25/19.79 inference(resolution,[status(thm)],[f18887,f9431])).
% 112.25/19.79 fof(f19288,plain,(
% 112.25/19.79 iext(uri_rdfs_subClassOf,uri_ex_c1,uri_ex_c2)|~ic(uri_ex_c1)|~ic(uri_ex_c2)|~icext(uri_ex_c2,uri_ex_w)),
% 112.25/19.79 inference(paramodulation,[status(thm)],[f19264,f1739])).
% 112.25/19.79 fof(f19289,plain,(
% 112.25/19.79 ~ic(uri_ex_c1)|~ic(uri_ex_c2)|~icext(uri_ex_c2,uri_ex_w)),
% 112.25/19.79 inference(forward_subsumption_resolution,[status(thm)],[f19288,f2405])).
% 112.25/19.79 fof(f19290,plain,(
% 112.25/19.79 ~ic(uri_ex_c1)|~ic(uri_ex_c2)),
% 112.25/19.79 inference(resolution,[status(thm)],[f19289,f10752])).
% 112.25/19.79 fof(f19292,plain,(
% 112.25/19.79 ~ic(uri_ex_c2)),
% 112.25/19.79 inference(forward_subsumption_resolution,[status(thm)],[f19290,f2779])).
% 112.25/19.79 fof(f19293,plain,(
% 112.25/19.79 $false),
% 112.25/19.79 inference(backward_subsumption_resolution,[status(thm)],[f2780,f19292])).
% 112.25/19.79 % SZS output end CNFRefutation for theBenchmark.p
% 20.96/19.83 % Elapsed time: 19.431944 seconds
% 20.96/19.83 % CPU time: 153.728718 seconds
% 20.96/19.83 % Total memory used: 353.674 MB
% 20.96/19.83 % Net memory used: 328.247 MB
%------------------------------------------------------------------------------