%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR109+1 : 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 : n017.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:16 PM UTC 2026
% Result : Theorem 59.69s 13.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n017.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Mon Sep 21 14:57:02 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.21/6.02 % Drodi V4.1.1
% 59.69/13.61 % Refutation found
% 59.69/13.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 59.69/13.61 % SZS output start CNFRefutation for theBenchmark
% 59.69/13.61 fof(f26,axiom,(
% 59.69/13.61 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 59.69/13.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.69/13.61 fof(f27,axiom,(
% 59.69/13.61 (! [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) ) ) )),
% 59.69/13.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.69/13.61 fof(f14492,axiom,(
% 59.69/13.61 s__subclass(s__Reptile,s__Animal) ),
% 59.69/13.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.69/13.61 fof(f14789,axiom,(
% 59.69/13.61 ( s__subclass(s__Reptile,s__Animal)=> (? [V_C1,V_C2,V_C3,V_C4,V_C5,V_C6,V_C7,V_C8,V_C9,V_C10] :( s__instance(V_C1,s__SetOrClass)& s__instance(V_C2,s__SetOrClass)& s__instance(V_C3,s__SetOrClass)& s__instance(V_C4,s__SetOrClass)& s__instance(V_C5,s__SetOrClass)& s__instance(V_C6,s__SetOrClass)& s__instance(V_C7,s__SetOrClass)& s__instance(V_C8,s__SetOrClass)& s__instance(V_C9,s__SetOrClass)& s__instance(V_C10,s__SetOrClass)& s__subclass(V_C1,V_C2)& s__subclass(V_C2,V_C3)& s__subclass(V_C3,V_C4)& s__subclass(V_C4,V_C5)& s__subclass(V_C5,V_C6)& s__subclass(V_C6,V_C7)& s__subclass(V_C7,V_C8)& s__subclass(V_C8,V_C9)& s__subclass(V_C9,V_C10)& s__subclass(V_C10,s__Reptile)& s__instance(s__Creature50_1,V_C1) ) )) ),
% 59.69/13.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.69/13.61 fof(f14790,conjecture,(
% 59.69/13.61 s__instance(s__Creature50_1,s__Reptile) ),
% 59.69/13.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.69/13.61 fof(f14791,negated_conjecture,(
% 59.69/13.61 ~(s__instance(s__Creature50_1,s__Reptile) )),
% 59.69/13.61 inference(negated_conjecture,[status(cth)],[f14790])).
% 59.69/13.61 fof(f14831,plain,(
% 59.69/13.61 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 59.69/13.61 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 59.69/13.61 fof(f14832,plain,(
% 59.69/13.61 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f14831])).
% 59.69/13.61 fof(f14833,plain,(
% 59.69/13.61 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f14831])).
% 59.69/13.61 fof(f14834,plain,(
% 59.69/13.61 ![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)))),
% 59.69/13.61 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 59.69/13.61 fof(f14835,plain,(
% 59.69/13.61 ![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))))),
% 59.69/13.61 inference(miniscoping,[status(thm)],[f14834])).
% 59.69/13.61 fof(f14836,plain,(
% 59.69/13.61 ![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))),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f14835])).
% 59.69/13.61 fof(f34065,plain,(
% 59.69/13.61 s__subclass(s__Reptile,s__Animal)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f14492])).
% 59.69/13.61 fof(f34362,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|(?[V_C1,V_C2,V_C3,V_C4,V_C5,V_C6,V_C7,V_C8,V_C9,V_C10]: ((((((((((((((((((((s__instance(V_C1,s__SetOrClass)&s__instance(V_C2,s__SetOrClass))&s__instance(V_C3,s__SetOrClass))&s__instance(V_C4,s__SetOrClass))&s__instance(V_C5,s__SetOrClass))&s__instance(V_C6,s__SetOrClass))&s__instance(V_C7,s__SetOrClass))&s__instance(V_C8,s__SetOrClass))&s__instance(V_C9,s__SetOrClass))&s__instance(V_C10,s__SetOrClass))&s__subclass(V_C1,V_C2))&s__subclass(V_C2,V_C3))&s__subclass(V_C3,V_C4))&s__subclass(V_C4,V_C5))&s__subclass(V_C5,V_C6))&s__subclass(V_C6,V_C7))&s__subclass(V_C7,V_C8))&s__subclass(V_C8,V_C9))&s__subclass(V_C9,V_C10))&s__subclass(V_C10,s__Reptile))&s__instance(s__Creature50_1,V_C1)))),
% 59.69/13.61 inference(pre_NNF_transformation,[status(thm)],[f14789])).
% 59.69/13.61 fof(f34363,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|(?[V_C1]: ((?[V_C10]: ((?[V_C9]: ((?[V_C8]: ((?[V_C7]: ((?[V_C6]: ((?[V_C5]: ((?[V_C4]: ((?[V_C3]: ((?[V_C2]: (((((((((((s__instance(V_C1,s__SetOrClass)&s__instance(V_C2,s__SetOrClass))&s__instance(V_C3,s__SetOrClass))&s__instance(V_C4,s__SetOrClass))&s__instance(V_C5,s__SetOrClass))&s__instance(V_C6,s__SetOrClass))&s__instance(V_C7,s__SetOrClass))&s__instance(V_C8,s__SetOrClass))&s__instance(V_C9,s__SetOrClass))&s__instance(V_C10,s__SetOrClass))&s__subclass(V_C1,V_C2))&s__subclass(V_C2,V_C3)))&s__subclass(V_C3,V_C4)))&s__subclass(V_C4,V_C5)))&s__subclass(V_C5,V_C6)))&s__subclass(V_C6,V_C7)))&s__subclass(V_C7,V_C8)))&s__subclass(V_C8,V_C9)))&s__subclass(V_C9,V_C10)))&s__subclass(V_C10,s__Reptile)))&s__instance(s__Creature50_1,V_C1)))),
% 59.69/13.61 inference(miniscoping,[status(thm)],[f34362])).
% 59.69/13.61 fof(f34364,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|((((((((((((((((((((s__instance(sK508_skl,s__SetOrClass)&s__instance(sK517_skl,s__SetOrClass))&s__instance(sK516_skl,s__SetOrClass))&s__instance(sK515_skl,s__SetOrClass))&s__instance(sK514_skl,s__SetOrClass))&s__instance(sK513_skl,s__SetOrClass))&s__instance(sK512_skl,s__SetOrClass))&s__instance(sK511_skl,s__SetOrClass))&s__instance(sK510_skl,s__SetOrClass))&s__instance(sK509_skl,s__SetOrClass))&s__subclass(sK508_skl,sK517_skl))&s__subclass(sK517_skl,sK516_skl))&s__subclass(sK516_skl,sK515_skl))&s__subclass(sK515_skl,sK514_skl))&s__subclass(sK514_skl,sK513_skl))&s__subclass(sK513_skl,sK512_skl))&s__subclass(sK512_skl,sK511_skl))&s__subclass(sK511_skl,sK510_skl))&s__subclass(sK510_skl,sK509_skl))&s__subclass(sK509_skl,s__Reptile))&s__instance(s__Creature50_1,sK508_skl))),
% 59.69/13.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK508_skl,sK509_skl,sK510_skl,sK511_skl,sK512_skl,sK513_skl,sK514_skl,sK515_skl,sK516_skl,sK517_skl]),skolemize(V_C1,sK508_skl),skolemize(V_C10,sK509_skl),skolemize(V_C9,sK510_skl),skolemize(V_C8,sK511_skl),skolemize(V_C7,sK512_skl),skolemize(V_C6,sK513_skl),skolemize(V_C5,sK514_skl),skolemize(V_C4,sK515_skl),skolemize(V_C3,sK516_skl),skolemize(V_C2,sK517_skl)],[f34363])).
% 59.69/13.61 fof(f34375,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK508_skl,sK517_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34376,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK517_skl,sK516_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34377,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK516_skl,sK515_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34378,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK515_skl,sK514_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34379,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK514_skl,sK513_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34380,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK513_skl,sK512_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34381,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK512_skl,sK511_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34382,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK511_skl,sK510_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34383,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK510_skl,sK509_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34384,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__subclass(sK509_skl,s__Reptile)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34385,plain,(
% 59.69/13.61 ~s__subclass(s__Reptile,s__Animal)|s__instance(s__Creature50_1,sK508_skl)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f34364])).
% 59.69/13.61 fof(f34386,plain,(
% 59.69/13.61 ~s__instance(s__Creature50_1,s__Reptile)),
% 59.69/13.61 inference(cnf_transformation,[status(thm)],[f14791])).
% 59.69/13.61 fof(f34493,plain,(
% 59.69/13.61 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f14836,f14833])).
% 59.69/13.61 fof(f35366,plain,(
% 59.69/13.61 s__subclass(sK508_skl,sK517_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34375,f34065])).
% 59.69/13.61 fof(f35367,plain,(
% 59.69/13.61 s__subclass(sK517_skl,sK516_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34376,f34065])).
% 59.69/13.61 fof(f35368,plain,(
% 59.69/13.61 s__subclass(sK516_skl,sK515_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34377,f34065])).
% 59.69/13.61 fof(f35369,plain,(
% 59.69/13.61 s__subclass(sK515_skl,sK514_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34378,f34065])).
% 59.69/13.61 fof(f35370,plain,(
% 59.69/13.61 s__subclass(sK514_skl,sK513_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34379,f34065])).
% 59.69/13.61 fof(f35371,plain,(
% 59.69/13.61 s__subclass(sK513_skl,sK512_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34380,f34065])).
% 59.69/13.61 fof(f35372,plain,(
% 59.69/13.61 s__subclass(sK512_skl,sK511_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34381,f34065])).
% 59.69/13.61 fof(f35373,plain,(
% 59.69/13.61 s__subclass(sK511_skl,sK510_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34382,f34065])).
% 59.69/13.61 fof(f35374,plain,(
% 59.69/13.61 s__subclass(sK510_skl,sK509_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34383,f34065])).
% 59.69/13.61 fof(f35375,plain,(
% 59.69/13.61 s__subclass(sK509_skl,s__Reptile)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34384,f34065])).
% 59.69/13.61 fof(f35376,plain,(
% 59.69/13.61 s__instance(s__Creature50_1,sK508_skl)),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f34385,f34065])).
% 59.69/13.61 fof(f35440,plain,(
% 59.69/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,s__Reptile)|~s__instance(s__Creature50_1,X0))),
% 59.69/13.61 inference(resolution,[status(thm)],[f34493,f34386])).
% 59.69/13.61 fof(f35448,plain,(
% 59.69/13.61 ![X0]: (~s__subclass(X0,s__Reptile)|~s__instance(s__Creature50_1,X0))),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35440,f14832])).
% 59.69/13.61 fof(f35456,plain,(
% 59.69/13.61 ~s__instance(s__Creature50_1,sK509_skl)),
% 59.69/13.61 inference(resolution,[status(thm)],[f35448,f35375])).
% 59.69/13.61 fof(f35457,plain,(
% 59.69/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK509_skl)|~s__instance(s__Creature50_1,X0))),
% 59.69/13.61 inference(resolution,[status(thm)],[f35456,f34493])).
% 59.69/13.61 fof(f35458,plain,(
% 59.69/13.61 ![X0]: (~s__subclass(X0,sK509_skl)|~s__instance(s__Creature50_1,X0))),
% 59.69/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35457,f14832])).
% 59.69/13.61 fof(f35459,plain,(
% 60.45/13.61 ~s__instance(s__Creature50_1,sK510_skl)),
% 60.45/13.61 inference(resolution,[status(thm)],[f35458,f35374])).
% 60.45/13.61 fof(f35460,plain,(
% 60.45/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK510_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(resolution,[status(thm)],[f35459,f34493])).
% 60.45/13.61 fof(f35461,plain,(
% 60.45/13.61 ![X0]: (~s__subclass(X0,sK510_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35460,f14832])).
% 60.45/13.61 fof(f35462,plain,(
% 60.45/13.61 ~s__instance(s__Creature50_1,sK511_skl)),
% 60.45/13.61 inference(resolution,[status(thm)],[f35461,f35373])).
% 60.45/13.61 fof(f35463,plain,(
% 60.45/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK511_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(resolution,[status(thm)],[f35462,f34493])).
% 60.45/13.61 fof(f35464,plain,(
% 60.45/13.61 ![X0]: (~s__subclass(X0,sK511_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35463,f14832])).
% 60.45/13.61 fof(f35465,plain,(
% 60.45/13.61 ~s__instance(s__Creature50_1,sK512_skl)),
% 60.45/13.61 inference(resolution,[status(thm)],[f35464,f35372])).
% 60.45/13.61 fof(f35466,plain,(
% 60.45/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK512_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(resolution,[status(thm)],[f35465,f34493])).
% 60.45/13.61 fof(f35467,plain,(
% 60.45/13.61 ![X0]: (~s__subclass(X0,sK512_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35466,f14832])).
% 60.45/13.61 fof(f35468,plain,(
% 60.45/13.61 ~s__instance(s__Creature50_1,sK513_skl)),
% 60.45/13.61 inference(resolution,[status(thm)],[f35467,f35371])).
% 60.45/13.61 fof(f35469,plain,(
% 60.45/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK513_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(resolution,[status(thm)],[f35468,f34493])).
% 60.45/13.61 fof(f35470,plain,(
% 60.45/13.61 ![X0]: (~s__subclass(X0,sK513_skl)|~s__instance(s__Creature50_1,X0))),
% 60.45/13.61 inference(forward_subsumption_resolution,[status(thm)],[f35469,f14832])).
% 60.45/13.61 fof(f35471,plain,(
% 60.45/13.61 ~s__instance(s__Creature50_1,sK514_skl)),
% 60.45/13.61 inference(resolution,[status(thm)],[f35470,f35370])).
% 60.45/13.61 fof(f35472,plain,(
% 60.45/13.61 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK514_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(resolution,[status(thm)],[f35471,f34493])).
% 43.08/13.74 fof(f35473,plain,(
% 43.08/13.74 ![X0]: (~s__subclass(X0,sK514_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(forward_subsumption_resolution,[status(thm)],[f35472,f14832])).
% 43.08/13.74 fof(f35474,plain,(
% 43.08/13.74 ~s__instance(s__Creature50_1,sK515_skl)),
% 43.08/13.74 inference(resolution,[status(thm)],[f35473,f35369])).
% 43.08/13.74 fof(f35475,plain,(
% 43.08/13.74 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK515_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(resolution,[status(thm)],[f35474,f34493])).
% 43.08/13.74 fof(f35476,plain,(
% 43.08/13.74 ![X0]: (~s__subclass(X0,sK515_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(forward_subsumption_resolution,[status(thm)],[f35475,f14832])).
% 43.08/13.74 fof(f35477,plain,(
% 43.08/13.74 ~s__instance(s__Creature50_1,sK516_skl)),
% 43.08/13.74 inference(resolution,[status(thm)],[f35476,f35368])).
% 43.08/13.74 fof(f35478,plain,(
% 43.08/13.74 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK516_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(resolution,[status(thm)],[f35477,f34493])).
% 43.08/13.74 fof(f35479,plain,(
% 43.08/13.74 ![X0]: (~s__subclass(X0,sK516_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(forward_subsumption_resolution,[status(thm)],[f35478,f14832])).
% 43.08/13.74 fof(f35480,plain,(
% 43.08/13.74 ~s__instance(s__Creature50_1,sK517_skl)),
% 43.08/13.74 inference(resolution,[status(thm)],[f35479,f35367])).
% 43.08/13.74 fof(f35481,plain,(
% 43.08/13.74 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,sK517_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(resolution,[status(thm)],[f35480,f34493])).
% 43.08/13.74 fof(f35482,plain,(
% 43.08/13.74 ![X0]: (~s__subclass(X0,sK517_skl)|~s__instance(s__Creature50_1,X0))),
% 43.08/13.74 inference(forward_subsumption_resolution,[status(thm)],[f35481,f14832])).
% 43.08/13.74 fof(f35483,plain,(
% 43.08/13.74 ~s__instance(s__Creature50_1,sK508_skl)),
% 43.08/13.74 inference(resolution,[status(thm)],[f35482,f35366])).
% 43.08/13.74 fof(f35484,plain,(
% 43.08/13.74 $false),
% 43.08/13.74 inference(forward_subsumption_resolution,[status(thm)],[f35483,f35376])).
% 43.08/13.74 % SZS output end CNFRefutation for theBenchmark.p
% 43.08/13.76 % Elapsed time: 8.294945 seconds
% 43.08/13.76 % CPU time: 60.960119 seconds
% 43.08/13.76 % Total memory used: 987.797 MB
% 43.08/13.76 % Net memory used: 975.808 MB
%------------------------------------------------------------------------------