%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR092+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:09 PM UTC 2026
% Result : Theorem 124.64s 26.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR092+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/10.38 % Computer : n003.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Mon Sep 21 14:57:12 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.14/10.97 % Drodi V4.1.1
% 124.64/26.81 % Refutation found
% 124.64/26.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 124.64/26.81 % SZS output start CNFRefutation for theBenchmark
% 124.64/26.81 fof(f26,axiom,(
% 124.64/26.81 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f27,axiom,(
% 124.64/26.81 (! [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) ) ) )),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f93,axiom,(
% 124.64/26.81 (! [V__ROW1,V__ROW2] :( ( s__instance(V__ROW2,s__Organism)& s__instance(V__ROW1,s__Organism) )=> ( s__parent(V__ROW1,V__ROW2)=> s__ancestor(V__ROW1,V__ROW2) ) ) )),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f226,axiom,(
% 124.64/26.81 (! [V__ROW1,V__ROW2] :( ( s__instance(V__ROW2,s__Organism)& s__instance(V__ROW1,s__Organism) )=> ( s__son(V__ROW1,V__ROW2)=> s__parent(V__ROW1,V__ROW2) ) ) )),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7100,axiom,(
% 124.64/26.81 s__subclass(s__Animal,s__Organism) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7117,axiom,(
% 124.64/26.81 s__subclass(s__Vertebrate,s__Animal) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7150,axiom,(
% 124.64/26.81 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7166,axiom,(
% 124.64/26.81 s__subclass(s__Mammal,s__WarmBloodedVertebrate) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7193,axiom,(
% 124.64/26.81 s__subclass(s__Primate,s__Mammal) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7203,axiom,(
% 124.64/26.81 s__subclass(s__Hominid,s__Primate) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7206,axiom,(
% 124.64/26.81 s__subclass(s__Human,s__Hominid) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f7211,axiom,(
% 124.64/26.81 s__subclass(s__Man,s__Human) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f16749,axiom,(
% 124.64/26.81 s__instance(s__Man22_1,s__Man) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f16750,axiom,(
% 124.64/26.81 s__instance(s__Ancestor22_1,s__Human) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f16751,axiom,(
% 124.64/26.81 s__son(s__Man22_1,s__Ancestor22_1) ),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f16752,conjecture,(
% 124.64/26.81 (? [V_X] :( s__ancestor(s__Man22_1,V_X)& V_X = s__Ancestor22_1 ) )),
% 124.64/26.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.64/26.81 fof(f16753,negated_conjecture,(
% 124.64/26.81 ~((? [V_X] :( s__ancestor(s__Man22_1,V_X)& V_X = s__Ancestor22_1 ) ))),
% 124.64/26.81 inference(negated_conjecture,[status(cth)],[f16752])).
% 124.64/26.81 fof(f16793,plain,(
% 124.64/26.81 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 124.64/26.81 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 124.64/26.81 fof(f16794,plain,(
% 124.64/26.81 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 124.64/26.81 inference(cnf_transformation,[status(thm)],[f16793])).
% 124.64/26.81 fof(f16795,plain,(
% 124.64/26.81 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 124.64/26.81 inference(cnf_transformation,[status(thm)],[f16793])).
% 124.64/26.81 fof(f16796,plain,(
% 124.64/26.81 ![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)))),
% 124.64/26.81 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 124.64/26.81 fof(f16797,plain,(
% 124.64/26.81 ![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))))),
% 124.64/26.81 inference(miniscoping,[status(thm)],[f16796])).
% 124.64/26.81 fof(f16798,plain,(
% 124.64/26.81 ![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))),
% 124.64/26.81 inference(cnf_transformation,[status(thm)],[f16797])).
% 124.64/26.81 fof(f16921,plain,(
% 124.64/26.81 ![V__ROW1,V__ROW2]: ((~s__instance(V__ROW2,s__Organism)|~s__instance(V__ROW1,s__Organism))|(~s__parent(V__ROW1,V__ROW2)|s__ancestor(V__ROW1,V__ROW2)))),
% 124.64/26.82 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 124.64/26.82 fof(f16922,plain,(
% 124.64/26.82 ![X0,X1]: (~s__instance(X0,s__Organism)|~s__instance(X1,s__Organism)|~s__parent(X1,X0)|s__ancestor(X1,X0))),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f16921])).
% 124.64/26.82 fof(f17196,plain,(
% 124.64/26.82 ![V__ROW1,V__ROW2]: ((~s__instance(V__ROW2,s__Organism)|~s__instance(V__ROW1,s__Organism))|(~s__son(V__ROW1,V__ROW2)|s__parent(V__ROW1,V__ROW2)))),
% 124.64/26.82 inference(pre_NNF_transformation,[status(thm)],[f226])).
% 124.64/26.82 fof(f17197,plain,(
% 124.64/26.82 ![X0,X1]: (~s__instance(X0,s__Organism)|~s__instance(X1,s__Organism)|~s__son(X1,X0)|s__parent(X1,X0))),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f17196])).
% 124.64/26.82 fof(f29376,plain,(
% 124.64/26.82 s__subclass(s__Animal,s__Organism)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7100])).
% 124.64/26.82 fof(f29404,plain,(
% 124.64/26.82 s__subclass(s__Vertebrate,s__Animal)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7117])).
% 124.64/26.82 fof(f29437,plain,(
% 124.64/26.82 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7150])).
% 124.64/26.82 fof(f29457,plain,(
% 124.64/26.82 s__subclass(s__Mammal,s__WarmBloodedVertebrate)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7166])).
% 124.64/26.82 fof(f29486,plain,(
% 124.64/26.82 s__subclass(s__Primate,s__Mammal)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7193])).
% 124.64/26.82 fof(f29496,plain,(
% 124.64/26.82 s__subclass(s__Hominid,s__Primate)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7203])).
% 124.64/26.82 fof(f29499,plain,(
% 124.64/26.82 s__subclass(s__Human,s__Hominid)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7206])).
% 124.64/26.82 fof(f29504,plain,(
% 124.64/26.82 s__subclass(s__Man,s__Human)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f7211])).
% 124.64/26.82 fof(f44206,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__Man)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f16749])).
% 124.64/26.82 fof(f44207,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Human)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f16750])).
% 124.64/26.82 fof(f44208,plain,(
% 124.64/26.82 s__son(s__Man22_1,s__Ancestor22_1)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f16751])).
% 124.64/26.82 fof(f44209,plain,(
% 124.64/26.82 (![V_X]: (~s__ancestor(s__Man22_1,V_X)|~V_X=s__Ancestor22_1))),
% 124.64/26.82 inference(pre_NNF_transformation,[status(thm)],[f16753])).
% 124.64/26.82 fof(f44210,plain,(
% 124.64/26.82 ![X0]: (~s__ancestor(s__Man22_1,X0)|~X0=s__Ancestor22_1)),
% 124.64/26.82 inference(cnf_transformation,[status(thm)],[f44209])).
% 124.64/26.82 fof(f44558,plain,(
% 124.64/26.82 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f16798,f16795])).
% 124.64/26.82 fof(f44624,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Human,s__SetOrClass)|~s__subclass(s__Human,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f44558,f44207])).
% 124.64/26.82 fof(f44625,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Man,s__SetOrClass)|~s__subclass(s__Man,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f44558,f44206])).
% 124.64/26.82 fof(f44687,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Human,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f44624,f16794])).
% 124.64/26.82 fof(f44688,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Man,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f44625,f16794])).
% 124.64/26.82 fof(f48564,plain,(
% 124.64/26.82 ~s__instance(s__Ancestor22_1,s__Organism)|~s__instance(s__Man22_1,s__Organism)|s__parent(s__Man22_1,s__Ancestor22_1)),
% 124.64/26.82 inference(resolution,[status(thm)],[f17197,f44208])).
% 124.64/26.82 fof(f125393,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Hominid)),
% 124.64/26.82 inference(resolution,[status(thm)],[f29499,f44687])).
% 124.64/26.82 fof(f125500,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__Human)),
% 124.64/26.82 inference(resolution,[status(thm)],[f29504,f44688])).
% 124.64/26.82 fof(f125837,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Hominid,s__SetOrClass)|~s__subclass(s__Hominid,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f125393,f44558])).
% 124.64/26.82 fof(f125840,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Hominid,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f125837,f16794])).
% 124.64/26.82 fof(f126068,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Human,s__SetOrClass)|~s__subclass(s__Human,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f125500,f44558])).
% 124.64/26.82 fof(f126071,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Human,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f126068,f16794])).
% 124.64/26.82 fof(f126072,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Primate)),
% 124.64/26.82 inference(resolution,[status(thm)],[f125840,f29496])).
% 124.64/26.82 fof(f126115,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Primate,s__SetOrClass)|~s__subclass(s__Primate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f126072,f44558])).
% 124.64/26.82 fof(f126118,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Primate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f126115,f16794])).
% 124.64/26.82 fof(f126167,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__Hominid)),
% 124.64/26.82 inference(resolution,[status(thm)],[f126071,f29499])).
% 124.64/26.82 fof(f126281,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Hominid,s__SetOrClass)|~s__subclass(s__Hominid,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f126167,f44558])).
% 124.64/26.82 fof(f126284,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Hominid,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f126281,f16794])).
% 124.64/26.82 fof(f126285,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Mammal)),
% 124.64/26.82 inference(resolution,[status(thm)],[f126118,f29486])).
% 124.64/26.82 fof(f126328,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Mammal,s__SetOrClass)|~s__subclass(s__Mammal,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f126285,f44558])).
% 124.64/26.82 fof(f126331,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Mammal,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f126328,f16794])).
% 124.64/26.82 fof(f127029,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__Primate)),
% 124.64/26.82 inference(resolution,[status(thm)],[f126284,f29496])).
% 124.64/26.82 fof(f127072,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Primate,s__SetOrClass)|~s__subclass(s__Primate,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f127029,f44558])).
% 124.64/26.82 fof(f127075,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Primate,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f127072,f16794])).
% 124.64/26.82 fof(f127076,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__WarmBloodedVertebrate)),
% 124.64/26.82 inference(resolution,[status(thm)],[f126331,f29457])).
% 124.64/26.82 fof(f127119,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__WarmBloodedVertebrate,s__SetOrClass)|~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f127076,f44558])).
% 124.64/26.82 fof(f127122,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f127119,f16794])).
% 124.64/26.82 fof(f127956,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__Mammal)),
% 124.64/26.82 inference(resolution,[status(thm)],[f127075,f29486])).
% 124.64/26.82 fof(f127999,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Mammal,s__SetOrClass)|~s__subclass(s__Mammal,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f127956,f44558])).
% 124.64/26.82 fof(f128002,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Mammal,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f127999,f16794])).
% 124.64/26.82 fof(f128003,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Vertebrate)),
% 124.64/26.82 inference(resolution,[status(thm)],[f127122,f29437])).
% 124.64/26.82 fof(f128046,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__Vertebrate,s__SetOrClass)|~s__subclass(s__Vertebrate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f128003,f44558])).
% 124.64/26.82 fof(f128049,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__Vertebrate,X0)|s__instance(s__Ancestor22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f128046,f16794])).
% 124.64/26.82 fof(f128264,plain,(
% 124.64/26.82 s__instance(s__Man22_1,s__WarmBloodedVertebrate)),
% 124.64/26.82 inference(resolution,[status(thm)],[f128002,f29457])).
% 124.64/26.82 fof(f128307,plain,(
% 124.64/26.82 ![X0]: (~s__instance(s__WarmBloodedVertebrate,s__SetOrClass)|~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(resolution,[status(thm)],[f128264,f44558])).
% 124.64/26.82 fof(f128310,plain,(
% 124.64/26.82 ![X0]: (~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Man22_1,X0))),
% 124.64/26.82 inference(forward_subsumption_resolution,[status(thm)],[f128307,f16794])).
% 124.64/26.82 fof(f128311,plain,(
% 124.64/26.82 s__instance(s__Ancestor22_1,s__Animal)),
% 32.93/27.04 inference(resolution,[status(thm)],[f128049,f29404])).
% 32.93/27.04 fof(f128356,plain,(
% 32.93/27.04 ![X0]: (~s__instance(s__Animal,s__SetOrClass)|~s__subclass(s__Animal,X0)|s__instance(s__Ancestor22_1,X0))),
% 32.93/27.04 inference(resolution,[status(thm)],[f128311,f44558])).
% 32.93/27.04 fof(f128359,plain,(
% 32.93/27.04 ![X0]: (~s__subclass(s__Animal,X0)|s__instance(s__Ancestor22_1,X0))),
% 32.93/27.04 inference(forward_subsumption_resolution,[status(thm)],[f128356,f16794])).
% 32.93/27.04 fof(f129031,plain,(
% 32.93/27.04 s__instance(s__Man22_1,s__Vertebrate)),
% 32.93/27.04 inference(resolution,[status(thm)],[f128310,f29437])).
% 32.93/27.04 fof(f129074,plain,(
% 32.93/27.04 ![X0]: (~s__instance(s__Vertebrate,s__SetOrClass)|~s__subclass(s__Vertebrate,X0)|s__instance(s__Man22_1,X0))),
% 32.93/27.04 inference(resolution,[status(thm)],[f129031,f44558])).
% 32.93/27.04 fof(f129077,plain,(
% 32.93/27.04 ![X0]: (~s__subclass(s__Vertebrate,X0)|s__instance(s__Man22_1,X0))),
% 32.93/27.04 inference(forward_subsumption_resolution,[status(thm)],[f129074,f16794])).
% 32.93/27.04 fof(f129078,plain,(
% 32.93/27.04 s__instance(s__Ancestor22_1,s__Organism)),
% 32.93/27.04 inference(resolution,[status(thm)],[f128359,f29376])).
% 32.93/27.04 fof(f129079,plain,(
% 32.93/27.04 ~s__instance(s__Man22_1,s__Organism)|s__parent(s__Man22_1,s__Ancestor22_1)),
% 32.93/27.04 inference(backward_subsumption_resolution,[status(thm)],[f48564,f129078])).
% 32.93/27.04 fof(f129187,plain,(
% 32.93/27.04 s__instance(s__Man22_1,s__Animal)),
% 32.93/27.04 inference(resolution,[status(thm)],[f129077,f29404])).
% 32.93/27.04 fof(f129232,plain,(
% 32.93/27.04 ![X0]: (~s__instance(s__Animal,s__SetOrClass)|~s__subclass(s__Animal,X0)|s__instance(s__Man22_1,X0))),
% 32.93/27.04 inference(resolution,[status(thm)],[f129187,f44558])).
% 32.93/27.04 fof(f129235,plain,(
% 32.93/27.04 ![X0]: (~s__subclass(s__Animal,X0)|s__instance(s__Man22_1,X0))),
% 32.93/27.04 inference(forward_subsumption_resolution,[status(thm)],[f129232,f16794])).
% 32.93/27.04 fof(f129775,plain,(
% 32.93/27.04 s__instance(s__Man22_1,s__Organism)),
% 32.93/27.04 inference(resolution,[status(thm)],[f129235,f29376])).
% 32.93/27.04 fof(f129776,plain,(
% 32.93/27.04 s__parent(s__Man22_1,s__Ancestor22_1)),
% 32.93/27.04 inference(backward_subsumption_resolution,[status(thm)],[f129079,f129775])).
% 32.93/27.04 fof(f129883,plain,(
% 32.93/27.04 ~s__instance(s__Ancestor22_1,s__Organism)|~s__instance(s__Man22_1,s__Organism)|s__ancestor(s__Man22_1,s__Ancestor22_1)),
% 32.93/27.04 inference(resolution,[status(thm)],[f129776,f16922])).
% 32.93/27.04 fof(f129885,plain,(
% 32.93/27.04 ~s__instance(s__Man22_1,s__Organism)|s__ancestor(s__Man22_1,s__Ancestor22_1)),
% 32.93/27.04 inference(forward_subsumption_resolution,[status(thm)],[f129883,f129078])).
% 32.93/27.04 fof(f148265,plain,(
% 32.93/27.04 s__ancestor(s__Man22_1,s__Ancestor22_1)),
% 32.93/27.04 inference(forward_subsumption_resolution,[status(thm)],[f129885,f129775])).
% 32.93/27.04 fof(f148266,plain,(
% 32.93/27.04 ~s__Ancestor22_1=s__Ancestor22_1),
% 32.93/27.04 inference(resolution,[status(thm)],[f148265,f44210])).
% 32.93/27.04 fof(f148277,plain,(
% 32.93/27.04 $false),
% 32.93/27.04 inference(trivial_equality_resolution,[status(thm)],[f148266])).
% 32.93/27.04 % SZS output end CNFRefutation for theBenchmark.p
% 4.34/27.11 % Elapsed time: 16.704169 seconds
% 4.34/27.11 % CPU time: 127.165516 seconds
% 4.34/27.11 % Total memory used: 1.569 GB
% 4.34/27.11 % Net memory used: 1.541 GB
%------------------------------------------------------------------------------