%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR083+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 12:15:05 PM UTC 2026
% Result : Theorem 235.90s 30.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR083+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n001.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 14:57:00 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.21/0.48 % Drodi V4.1.1
% 235.90/30.24 % Refutation found
% 235.90/30.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 235.90/30.24 % SZS output start CNFRefutation for theBenchmark
% 235.90/30.24 fof(f26,axiom,(
% 235.90/30.24 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f27,axiom,(
% 235.90/30.24 (! [V__X,V__Y,V__Z] :( ( s__instance(V__Y,s__SetOrClass)& s__instance(V__X,s__SetOrClass) )=> ( ( s__subclass(V__X,V__Y)& s__instance(V__Z,V__X) )=> s__instance(V__Z,V__Y) ) ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f232,axiom,(
% 235.90/30.24 (! [V__VALUE,V__ROW1,V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__FUNCTION] :( ( s__instance(V__FUNCTION,s__Function)& s__instance(V__CLASS,s__SetOrClass) )=> ( ( s__range(V__FUNCTION,V__CLASS)& s__AssignmentFn_5(V__FUNCTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4) = V__VALUE )=> s__instance(V__VALUE,V__CLASS) ) ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f925,axiom,(
% 235.90/30.24 s__subclass(s__Set,s__SetOrClass) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f1291,axiom,(
% 235.90/30.24 (! [V__INST1,V__INST2,V__INST3] :( ( s__instance(V__INST3,s__SetOrClass)& s__instance(V__INST2,s__SetOrClass)& s__instance(V__INST1,s__SetOrClass) )=> ( ( s__subclass(V__INST1,V__INST2)& s__subclass(V__INST2,V__INST3) )=> s__subclass(V__INST1,V__INST3) ) ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f2375,axiom,(
% 235.90/30.24 s__subclass(s__UnaryFunction,s__Function) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f3094,axiom,(
% 235.90/30.24 s__instance(s__PropertyFn__m,s__UnaryFunction) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f3097,axiom,(
% 235.90/30.24 s__range(s__PropertyFn__m,s__Set) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f3477,axiom,(
% 235.90/30.24 (! [V__SET2,V__SET1] :( (! [V__ELEMENT] :( ( s__instance(V__SET1,s__Set)& s__instance(V__SET2,s__Set) )=> ( s__element(V__ELEMENT,V__SET1)<=> s__element(V__ELEMENT,V__SET2) ) ))=> V__SET1 = V__SET2 ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f5923,axiom,(
% 235.90/30.24 s__subclass(s__Vertebrate,s__Animal) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f5956,axiom,(
% 235.90/30.24 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f5972,axiom,(
% 235.90/30.24 s__subclass(s__Mammal,s__WarmBloodedVertebrate) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f5999,axiom,(
% 235.90/30.24 s__subclass(s__Primate,s__Mammal) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f6009,axiom,(
% 235.90/30.24 s__subclass(s__Hominid,s__Primate) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f6012,axiom,(
% 235.90/30.24 s__subclass(s__Human,s__Hominid) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f6013,axiom,(
% 235.90/30.24 s__subclass(s__Human,s__CognitiveAgent) ),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f7218,conjecture,(
% 235.90/30.24 (? [V_ENTITY] :( s__subclass(V_ENTITY,s__Animal)& s__subclass(V_ENTITY,s__CognitiveAgent)& V_ENTITY = s__Human ) )),
% 235.90/30.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 235.90/30.24 fof(f7219,negated_conjecture,(
% 235.90/30.24 ~((? [V_ENTITY] :( s__subclass(V_ENTITY,s__Animal)& s__subclass(V_ENTITY,s__CognitiveAgent)& V_ENTITY = s__Human ) ))),
% 235.90/30.24 inference(negated_conjecture,[status(cth)],[f7218])).
% 235.90/30.24 fof(f7259,plain,(
% 235.90/30.24 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 235.90/30.24 fof(f7260,plain,(
% 235.90/30.24 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f7259])).
% 235.90/30.24 fof(f7261,plain,(
% 235.90/30.24 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f7259])).
% 235.90/30.24 fof(f7262,plain,(
% 235.90/30.24 ![V__X,V__Y,V__Z]: ((~s__instance(V__Y,s__SetOrClass)|~s__instance(V__X,s__SetOrClass))|((~s__subclass(V__X,V__Y)|~s__instance(V__Z,V__X))|s__instance(V__Z,V__Y)))),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 235.90/30.24 fof(f7263,plain,(
% 235.90/30.24 ![V__X,V__Y]: ((~s__instance(V__Y,s__SetOrClass)|~s__instance(V__X,s__SetOrClass))|(![V__Z]: ((~s__subclass(V__X,V__Y)|~s__instance(V__Z,V__X))|s__instance(V__Z,V__Y))))),
% 235.90/30.24 inference(miniscoping,[status(thm)],[f7262])).
% 235.90/30.24 fof(f7264,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X0)|~s__instance(X2,X1)|s__instance(X2,X0))),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f7263])).
% 235.90/30.24 fof(f7720,plain,(
% 235.90/30.24 ![V__VALUE,V__ROW1,V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__FUNCTION]: ((~s__instance(V__FUNCTION,s__Function)|~s__instance(V__CLASS,s__SetOrClass))|((~s__range(V__FUNCTION,V__CLASS)|~s__AssignmentFn_5(V__FUNCTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)=V__VALUE)|s__instance(V__VALUE,V__CLASS)))),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f232])).
% 235.90/30.24 fof(f7721,plain,(
% 235.90/30.24 ![V__CLASS,V__FUNCTION]: ((~s__instance(V__FUNCTION,s__Function)|~s__instance(V__CLASS,s__SetOrClass))|(![V__VALUE]: ((~s__range(V__FUNCTION,V__CLASS)|(![V__ROW1,V__ROW2,V__ROW3,V__ROW4]: ~s__AssignmentFn_5(V__FUNCTION,V__ROW1,V__ROW2,V__ROW3,V__ROW4)=V__VALUE))|s__instance(V__VALUE,V__CLASS))))),
% 235.90/30.24 inference(miniscoping,[status(thm)],[f7720])).
% 235.90/30.24 fof(f7722,plain,(
% 235.90/30.24 ![X0,X1,X2,X3,X4,X5,X6]: (~s__instance(X0,s__Function)|~s__instance(X1,s__SetOrClass)|~s__range(X0,X1)|~s__AssignmentFn_5(X0,X2,X3,X4,X5)=X6|s__instance(X6,X1))),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f7721])).
% 235.90/30.24 fof(f8895,plain,(
% 235.90/30.24 s__subclass(s__Set,s__SetOrClass)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f925])).
% 235.90/30.24 fof(f9656,plain,(
% 235.90/30.24 ![V__INST1,V__INST2,V__INST3]: (((~s__instance(V__INST3,s__SetOrClass)|~s__instance(V__INST2,s__SetOrClass))|~s__instance(V__INST1,s__SetOrClass))|((~s__subclass(V__INST1,V__INST2)|~s__subclass(V__INST2,V__INST3))|s__subclass(V__INST1,V__INST3)))),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f1291])).
% 235.90/30.24 fof(f9657,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__instance(X2,s__SetOrClass)|~s__subclass(X2,X1)|~s__subclass(X1,X0)|s__subclass(X2,X0))),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f9656])).
% 235.90/30.24 fof(f11770,plain,(
% 235.90/30.24 s__subclass(s__UnaryFunction,s__Function)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f2375])).
% 235.90/30.24 fof(f13005,plain,(
% 235.90/30.24 s__instance(s__PropertyFn__m,s__UnaryFunction)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f3094])).
% 235.90/30.24 fof(f13008,plain,(
% 235.90/30.24 s__range(s__PropertyFn__m,s__Set)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f3097])).
% 235.90/30.24 fof(f13580,plain,(
% 235.90/30.24 ![V__SET2,V__SET1]: ((?[V__ELEMENT]: ((s__instance(V__SET1,s__Set)&s__instance(V__SET2,s__Set))&(s__element(V__ELEMENT,V__SET1)<~>s__element(V__ELEMENT,V__SET2))))|V__SET1=V__SET2)),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f3477])).
% 235.90/30.24 fof(f13581,plain,(
% 235.90/30.24 ![V__SET2,V__SET1]: ((?[V__ELEMENT]: ((s__instance(V__SET1,s__Set)&s__instance(V__SET2,s__Set))&((s__element(V__ELEMENT,V__SET1)|s__element(V__ELEMENT,V__SET2))&(~s__element(V__ELEMENT,V__SET1)|~s__element(V__ELEMENT,V__SET2)))))|V__SET1=V__SET2)),
% 235.90/30.24 inference(NNF_transformation,[status(thm)],[f13580])).
% 235.90/30.24 fof(f13582,plain,(
% 235.90/30.24 ![V__SET2,V__SET1]: (((s__instance(V__SET1,s__Set)&s__instance(V__SET2,s__Set))&(?[V__ELEMENT]: ((s__element(V__ELEMENT,V__SET1)|s__element(V__ELEMENT,V__SET2))&(~s__element(V__ELEMENT,V__SET1)|~s__element(V__ELEMENT,V__SET2)))))|V__SET1=V__SET2)),
% 235.90/30.24 inference(miniscoping,[status(thm)],[f13581])).
% 235.90/30.24 fof(f13583,plain,(
% 235.90/30.24 ![V__SET2,V__SET1]: (((s__instance(V__SET1,s__Set)&s__instance(V__SET2,s__Set))&((s__element(sK156_skl(V__SET1,V__SET2),V__SET1)|s__element(sK156_skl(V__SET1,V__SET2),V__SET2))&(~s__element(sK156_skl(V__SET1,V__SET2),V__SET1)|~s__element(sK156_skl(V__SET1,V__SET2),V__SET2))))|V__SET1=V__SET2)),
% 235.90/30.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK156_skl]),skolemize(V__ELEMENT,sK156_skl(V__SET1,V__SET2))],[f13582])).
% 235.90/30.24 fof(f13584,plain,(
% 235.90/30.24 ![X0,X1]: (s__instance(X0,s__Set)|X0=X1)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f13583])).
% 235.90/30.24 fof(f17408,plain,(
% 235.90/30.24 s__subclass(s__Vertebrate,s__Animal)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f5923])).
% 235.90/30.24 fof(f17441,plain,(
% 235.90/30.24 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f5956])).
% 235.90/30.24 fof(f17461,plain,(
% 235.90/30.24 s__subclass(s__Mammal,s__WarmBloodedVertebrate)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f5972])).
% 235.90/30.24 fof(f17490,plain,(
% 235.90/30.24 s__subclass(s__Primate,s__Mammal)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f5999])).
% 235.90/30.24 fof(f17500,plain,(
% 235.90/30.24 s__subclass(s__Hominid,s__Primate)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f6009])).
% 235.90/30.24 fof(f17503,plain,(
% 235.90/30.24 s__subclass(s__Human,s__Hominid)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f6012])).
% 235.90/30.24 fof(f17504,plain,(
% 235.90/30.24 s__subclass(s__Human,s__CognitiveAgent)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f6013])).
% 235.90/30.24 fof(f19219,plain,(
% 235.90/30.24 (![V_ENTITY]: ((~s__subclass(V_ENTITY,s__Animal)|~s__subclass(V_ENTITY,s__CognitiveAgent))|~V_ENTITY=s__Human))),
% 235.90/30.24 inference(pre_NNF_transformation,[status(thm)],[f7219])).
% 235.90/30.24 fof(f19220,plain,(
% 235.90/30.24 ![X0]: (~s__subclass(X0,s__Animal)|~s__subclass(X0,s__CognitiveAgent)|~X0=s__Human)),
% 235.90/30.24 inference(cnf_transformation,[status(thm)],[f19219])).
% 235.90/30.24 fof(f19428,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f7264,f7261])).
% 235.90/30.24 fof(f19437,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X2)|~s__subclass(X2,X0)|s__subclass(X1,X0))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f9657,f7261])).
% 235.90/30.24 fof(f21035,plain,(
% 235.90/30.24 ![X0]: (~s__instance(s__Set,s__SetOrClass)|~s__instance(X0,s__Set)|s__instance(X0,s__SetOrClass))),
% 235.90/30.24 inference(resolution,[status(thm)],[f8895,f19428])).
% 235.90/30.24 fof(f21038,plain,(
% 235.90/30.24 s__instance(s__Set,s__SetOrClass)),
% 235.90/30.24 inference(resolution,[status(thm)],[f8895,f7260])).
% 235.90/30.24 fof(f21991,plain,(
% 235.90/30.24 ![X0]: (~s__instance(s__UnaryFunction,s__SetOrClass)|~s__instance(X0,s__UnaryFunction)|s__instance(X0,s__Function))),
% 235.90/30.24 inference(resolution,[status(thm)],[f11770,f19428])).
% 235.90/30.24 fof(f21994,plain,(
% 235.90/30.24 s__instance(s__UnaryFunction,s__SetOrClass)),
% 235.90/30.24 inference(resolution,[status(thm)],[f11770,f7260])).
% 235.90/30.24 fof(f26571,plain,(
% 235.90/30.24 ![X0,X1,X2,X3,X4]: (~s__instance(s__PropertyFn__m,s__Function)|~s__instance(s__Set,s__SetOrClass)|~s__AssignmentFn_5(s__PropertyFn__m,X0,X1,X2,X3)=X4|s__instance(X4,s__Set))),
% 235.90/30.24 inference(resolution,[status(thm)],[f7722,f13008])).
% 235.90/30.24 fof(f26650,plain,(
% 235.90/30.24 ![X0,X1,X2,X3,X4]: (~s__instance(s__PropertyFn__m,s__Function)|~s__AssignmentFn_5(s__PropertyFn__m,X0,X1,X2,X3)=X4|s__instance(X4,s__Set))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f26571,f21038])).
% 235.90/30.24 fof(f31645,plain,(
% 235.90/30.24 ![X0]: (~s__instance(X0,s__Set)|s__instance(X0,s__SetOrClass))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f21035,f21038])).
% 235.90/30.24 fof(f39331,plain,(
% 235.90/30.24 ![X0]: (~s__instance(X0,s__UnaryFunction)|s__instance(X0,s__Function))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f21991,f21994])).
% 235.90/30.24 fof(f39378,plain,(
% 235.90/30.24 s__instance(s__PropertyFn__m,s__Function)),
% 235.90/30.24 inference(resolution,[status(thm)],[f39331,f13005])).
% 235.90/30.24 fof(f62975,plain,(
% 235.90/30.24 ![X0,X1,X2,X3,X4]: (~s__AssignmentFn_5(s__PropertyFn__m,X0,X1,X2,X3)=X4|s__instance(X4,s__Set))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f26650,f39378])).
% 235.90/30.24 fof(f64970,plain,(
% 235.90/30.24 ![X0]: (s__instance(X0,s__Set))),
% 235.90/30.24 inference(backward_subsumption_resolution,[status(thm)],[f62975,f13584])).
% 235.90/30.24 fof(f64979,plain,(
% 235.90/30.24 ![X0]: (s__instance(X0,s__SetOrClass))),
% 235.90/30.24 inference(backward_subsumption_resolution,[status(thm)],[f31645,f64970])).
% 235.90/30.24 fof(f65022,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X1,X2)|~s__subclass(X2,X0)|s__subclass(X1,X0))),
% 235.90/30.24 inference(backward_subsumption_resolution,[status(thm)],[f19437,f64979])).
% 235.90/30.24 fof(f65046,plain,(
% 235.90/30.24 ![X0,X1,X2]: (~s__subclass(X0,X1)|~s__subclass(X1,X2)|s__subclass(X0,X2))),
% 235.90/30.24 inference(forward_subsumption_resolution,[status(thm)],[f65022,f64979])).
% 235.90/30.24 fof(f70763,plain,(
% 235.90/30.24 ![X0]: (~s__subclass(s__Primate,X0)|s__subclass(s__Hominid,X0))),
% 235.90/30.24 inference(resolution,[status(thm)],[f65046,f17500])).
% 235.90/30.24 fof(f70766,plain,(
% 235.90/30.24 ![X0]: (~s__subclass(s__Mammal,X0)|s__subclass(s__Primate,X0))),
% 235.90/30.24 inference(resolution,[status(thm)],[f65046,f17490])).
% 214.65/30.36 fof(f70774,plain,(
% 214.65/30.36 ![X0]: (~s__subclass(s__WarmBloodedVertebrate,X0)|s__subclass(s__Mammal,X0))),
% 214.65/30.36 inference(resolution,[status(thm)],[f65046,f17461])).
% 214.65/30.36 fof(f70778,plain,(
% 214.65/30.36 ![X0]: (~s__subclass(s__Vertebrate,X0)|s__subclass(s__WarmBloodedVertebrate,X0))),
% 214.65/30.36 inference(resolution,[status(thm)],[f65046,f17441])).
% 214.65/30.36 fof(f72178,plain,(
% 214.65/30.36 ![X0]: (~s__subclass(s__Hominid,X0)|s__subclass(s__Human,X0))),
% 214.65/30.36 inference(resolution,[status(thm)],[f65046,f17503])).
% 214.65/30.36 fof(f99196,plain,(
% 214.65/30.36 s__subclass(s__WarmBloodedVertebrate,s__Animal)),
% 214.65/30.36 inference(resolution,[status(thm)],[f70778,f17408])).
% 214.65/30.36 fof(f99199,plain,(
% 214.65/30.36 s__subclass(s__Mammal,s__Animal)),
% 214.65/30.36 inference(resolution,[status(thm)],[f99196,f70774])).
% 214.65/30.36 fof(f99213,plain,(
% 214.65/30.36 s__subclass(s__Primate,s__Animal)),
% 214.65/30.36 inference(resolution,[status(thm)],[f99199,f70766])).
% 214.65/30.36 fof(f99242,plain,(
% 214.65/30.36 s__subclass(s__Hominid,s__Animal)),
% 214.65/30.36 inference(resolution,[status(thm)],[f99213,f70763])).
% 214.65/30.36 fof(f122325,plain,(
% 214.65/30.36 s__subclass(s__Human,s__Animal)),
% 214.65/30.36 inference(resolution,[status(thm)],[f72178,f99242])).
% 214.65/30.36 fof(f122358,plain,(
% 214.65/30.36 ~s__subclass(s__Human,s__CognitiveAgent)|~s__Human=s__Human),
% 214.65/30.36 inference(resolution,[status(thm)],[f122325,f19220])).
% 214.65/30.36 fof(f122362,plain,(
% 214.65/30.36 ~s__subclass(s__Human,s__CognitiveAgent)),
% 214.65/30.36 inference(trivial_equality_resolution,[status(thm)],[f122358])).
% 214.65/30.36 fof(f122363,plain,(
% 214.65/30.36 $false),
% 214.65/30.36 inference(forward_subsumption_resolution,[status(thm)],[f122362,f17504])).
% 214.65/30.36 % SZS output end CNFRefutation for theBenchmark.p
% 21.72/30.45 % Elapsed time: 30.058027 seconds
% 21.72/30.45 % CPU time: 237.142451 seconds
% 21.72/30.45 % Total memory used: 1.152 GB
% 21.72/30.45 % Net memory used: 1.110 GB
%------------------------------------------------------------------------------