%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:13:45 PM UTC 2026
% Result : Theorem 65.40s 9.22s
% Output : CNFRefutation 59.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 5
% Syntax : Number of formulae : 90 ( 37 unt; 0 def)
% Number of atoms : 249 ( 0 equ)
% Maximal formula atoms : 22 ( 2 avg)
% Number of connectives : 232 ( 73 ~; 71 |; 84 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 71 ( 41 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [V__X,V__Y,V__Z] :
( ( s__instance(V__X,s__SetOrClass)
& s__instance(V__Y,s__SetOrClass) )
=> ( ( s__instance(V__Z,V__X)
& s__subclass(V__X,V__Y) )
=> s__instance(V__Z,V__Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14492,axiom,
s__subclass(s__Reptile,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14789,axiom,
( 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(s__Creature50_1,V_C1)
& s__subclass(V_C10,s__Reptile)
& s__subclass(V_C9,V_C10)
& s__subclass(V_C8,V_C9)
& s__subclass(V_C7,V_C8)
& s__subclass(V_C6,V_C7)
& s__subclass(V_C5,V_C6)
& s__subclass(V_C4,V_C5)
& s__subclass(V_C3,V_C4)
& s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14790,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14791,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f14790]) ).
fof(f14831,plain,
! [V__X,V__Y] :
( ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) )
| ~ s__subclass(V__X,V__Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f14833,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f14831]) ).
fof(f14834,plain,
! [V__X,V__Y,V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y)
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f14835,plain,
! [V__X,V__Y] :
( ! [V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y) )
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(miniscoping,[status(thm)],[f14834]) ).
fof(f14836,plain,
! [X0,X1,X2] :
( s__instance(X2,X0)
| ~ s__instance(X2,X1)
| ~ s__subclass(X1,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f14835]) ).
fof(f34065,plain,
s__subclass(s__Reptile,s__Animal),
inference(cnf_transformation,[status(thm)],[f14492]) ).
fof(f34362,plain,
( ? [V_C1,V_C2,V_C3,V_C4,V_C5,V_C6,V_C7,V_C8,V_C9,V_C10] :
( s__instance(s__Creature50_1,V_C1)
& s__subclass(V_C10,s__Reptile)
& s__subclass(V_C9,V_C10)
& s__subclass(V_C8,V_C9)
& s__subclass(V_C7,V_C8)
& s__subclass(V_C6,V_C7)
& s__subclass(V_C5,V_C6)
& s__subclass(V_C4,V_C5)
& s__subclass(V_C3,V_C4)
& s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(pre_NNF_transformation,[status(thm)],[f14789]) ).
fof(f34363,plain,
( ? [V_C1] :
( s__instance(s__Creature50_1,V_C1)
& ? [V_C10] :
( s__subclass(V_C10,s__Reptile)
& ? [V_C9] :
( s__subclass(V_C9,V_C10)
& ? [V_C8] :
( s__subclass(V_C8,V_C9)
& ? [V_C7] :
( s__subclass(V_C7,V_C8)
& ? [V_C6] :
( s__subclass(V_C6,V_C7)
& ? [V_C5] :
( s__subclass(V_C5,V_C6)
& ? [V_C4] :
( s__subclass(V_C4,V_C5)
& ? [V_C3] :
( s__subclass(V_C3,V_C4)
& ? [V_C2] :
( s__subclass(V_C2,V_C3)
& s__subclass(V_C1,V_C2)
& s__instance(V_C10,s__SetOrClass)
& s__instance(V_C9,s__SetOrClass)
& s__instance(V_C8,s__SetOrClass)
& s__instance(V_C7,s__SetOrClass)
& s__instance(V_C6,s__SetOrClass)
& s__instance(V_C5,s__SetOrClass)
& s__instance(V_C4,s__SetOrClass)
& s__instance(V_C3,s__SetOrClass)
& s__instance(V_C2,s__SetOrClass)
& s__instance(V_C1,s__SetOrClass) ) ) ) ) ) ) ) ) ) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(miniscoping,[status(thm)],[f34362]) ).
fof(f34364,plain,
( ( s__instance(s__Creature50_1,sK508_skl)
& s__subclass(sK509_skl,s__Reptile)
& s__subclass(sK510_skl,sK509_skl)
& s__subclass(sK511_skl,sK510_skl)
& s__subclass(sK512_skl,sK511_skl)
& s__subclass(sK513_skl,sK512_skl)
& s__subclass(sK514_skl,sK513_skl)
& s__subclass(sK515_skl,sK514_skl)
& s__subclass(sK516_skl,sK515_skl)
& s__subclass(sK517_skl,sK516_skl)
& s__subclass(sK508_skl,sK517_skl)
& s__instance(sK509_skl,s__SetOrClass)
& s__instance(sK510_skl,s__SetOrClass)
& s__instance(sK511_skl,s__SetOrClass)
& s__instance(sK512_skl,s__SetOrClass)
& s__instance(sK513_skl,s__SetOrClass)
& s__instance(sK514_skl,s__SetOrClass)
& s__instance(sK515_skl,s__SetOrClass)
& s__instance(sK516_skl,s__SetOrClass)
& s__instance(sK517_skl,s__SetOrClass)
& s__instance(sK508_skl,s__SetOrClass) )
| ~ s__subclass(s__Reptile,s__Animal) ),
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]) ).
fof(f34365,plain,
( s__instance(sK508_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34366,plain,
( s__instance(sK517_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34367,plain,
( s__instance(sK516_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34368,plain,
( s__instance(sK515_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34369,plain,
( s__instance(sK514_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34370,plain,
( s__instance(sK513_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34371,plain,
( s__instance(sK512_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34372,plain,
( s__instance(sK511_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34373,plain,
( s__instance(sK510_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34374,plain,
( s__instance(sK509_skl,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34375,plain,
( s__subclass(sK508_skl,sK517_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34376,plain,
( s__subclass(sK517_skl,sK516_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34377,plain,
( s__subclass(sK516_skl,sK515_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34378,plain,
( s__subclass(sK515_skl,sK514_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34379,plain,
( s__subclass(sK514_skl,sK513_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34380,plain,
( s__subclass(sK513_skl,sK512_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34381,plain,
( s__subclass(sK512_skl,sK511_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34382,plain,
( s__subclass(sK511_skl,sK510_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34383,plain,
( s__subclass(sK510_skl,sK509_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34384,plain,
( s__subclass(sK509_skl,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34385,plain,
( s__instance(s__Creature50_1,sK508_skl)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(cnf_transformation,[status(thm)],[f34364]) ).
fof(f34386,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[status(thm)],[f14791]) ).
fof(f34493,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f14836,f14833]) ).
fof(f35356,plain,
s__instance(sK508_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34365,f34065]) ).
fof(f35357,plain,
s__instance(sK517_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34366,f34065]) ).
fof(f35358,plain,
s__instance(sK516_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34367,f34065]) ).
fof(f35359,plain,
s__instance(sK515_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34368,f34065]) ).
fof(f35360,plain,
s__instance(sK514_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34369,f34065]) ).
fof(f35361,plain,
s__instance(sK513_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34370,f34065]) ).
fof(f35362,plain,
s__instance(sK512_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34371,f34065]) ).
fof(f35363,plain,
s__instance(sK511_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34372,f34065]) ).
fof(f35364,plain,
s__instance(sK510_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34373,f34065]) ).
fof(f35365,plain,
s__instance(sK509_skl,s__SetOrClass),
inference(forward_subsumption_resolution,[status(thm)],[f34374,f34065]) ).
fof(f35366,plain,
s__subclass(sK508_skl,sK517_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34375,f34065]) ).
fof(f35367,plain,
s__subclass(sK517_skl,sK516_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34376,f34065]) ).
fof(f35368,plain,
s__subclass(sK516_skl,sK515_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34377,f34065]) ).
fof(f35369,plain,
s__subclass(sK515_skl,sK514_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34378,f34065]) ).
fof(f35370,plain,
s__subclass(sK514_skl,sK513_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34379,f34065]) ).
fof(f35371,plain,
s__subclass(sK513_skl,sK512_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34380,f34065]) ).
fof(f35372,plain,
s__subclass(sK512_skl,sK511_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34381,f34065]) ).
fof(f35373,plain,
s__subclass(sK511_skl,sK510_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34382,f34065]) ).
fof(f35374,plain,
s__subclass(sK510_skl,sK509_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34383,f34065]) ).
fof(f35375,plain,
s__subclass(sK509_skl,s__Reptile),
inference(forward_subsumption_resolution,[status(thm)],[f34384,f34065]) ).
fof(f35376,plain,
s__instance(s__Creature50_1,sK508_skl),
inference(forward_subsumption_resolution,[status(thm)],[f34385,f34065]) ).
fof(f35440,plain,
! [X0] :
( s__instance(X0,s__Reptile)
| ~ s__instance(X0,sK509_skl)
| ~ s__instance(sK509_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35375]) ).
fof(f35441,plain,
! [X0] :
( s__instance(X0,sK509_skl)
| ~ s__instance(X0,sK510_skl)
| ~ s__instance(sK510_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35374]) ).
fof(f35442,plain,
! [X0] :
( s__instance(X0,sK510_skl)
| ~ s__instance(X0,sK511_skl)
| ~ s__instance(sK511_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35373]) ).
fof(f35443,plain,
! [X0] :
( s__instance(X0,sK511_skl)
| ~ s__instance(X0,sK512_skl)
| ~ s__instance(sK512_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35372]) ).
fof(f35444,plain,
! [X0] :
( s__instance(X0,sK512_skl)
| ~ s__instance(X0,sK513_skl)
| ~ s__instance(sK513_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35371]) ).
fof(f35445,plain,
! [X0] :
( s__instance(X0,sK513_skl)
| ~ s__instance(X0,sK514_skl)
| ~ s__instance(sK514_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35370]) ).
fof(f35446,plain,
! [X0] :
( s__instance(X0,sK514_skl)
| ~ s__instance(X0,sK515_skl)
| ~ s__instance(sK515_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35369]) ).
fof(f35447,plain,
! [X0] :
( s__instance(X0,sK515_skl)
| ~ s__instance(X0,sK516_skl)
| ~ s__instance(sK516_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35368]) ).
fof(f35448,plain,
! [X0] :
( s__instance(X0,sK516_skl)
| ~ s__instance(X0,sK517_skl)
| ~ s__instance(sK517_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35367]) ).
fof(f35449,plain,
! [X0] :
( s__instance(X0,sK517_skl)
| ~ s__instance(X0,sK508_skl)
| ~ s__instance(sK508_skl,s__SetOrClass) ),
inference(resolution,[status(thm)],[f34493,f35366]) ).
fof(f35460,plain,
! [X0] :
( s__instance(X0,s__Reptile)
| ~ s__instance(X0,sK509_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35440,f35365]) ).
fof(f35461,plain,
! [X0] :
( s__instance(X0,sK509_skl)
| ~ s__instance(X0,sK510_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35441,f35364]) ).
fof(f35462,plain,
! [X0] :
( s__instance(X0,sK510_skl)
| ~ s__instance(X0,sK511_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35442,f35363]) ).
fof(f35463,plain,
! [X0] :
( s__instance(X0,sK511_skl)
| ~ s__instance(X0,sK512_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35443,f35362]) ).
fof(f35464,plain,
! [X0] :
( s__instance(X0,sK512_skl)
| ~ s__instance(X0,sK513_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35444,f35361]) ).
fof(f35465,plain,
! [X0] :
( s__instance(X0,sK513_skl)
| ~ s__instance(X0,sK514_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35445,f35360]) ).
fof(f35466,plain,
! [X0] :
( s__instance(X0,sK514_skl)
| ~ s__instance(X0,sK515_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35446,f35359]) ).
fof(f35467,plain,
! [X0] :
( s__instance(X0,sK515_skl)
| ~ s__instance(X0,sK516_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35447,f35358]) ).
fof(f35468,plain,
! [X0] :
( s__instance(X0,sK516_skl)
| ~ s__instance(X0,sK517_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35448,f35357]) ).
fof(f35469,plain,
! [X0] :
( s__instance(X0,sK517_skl)
| ~ s__instance(X0,sK508_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f35449,f35356]) ).
fof(f35483,plain,
s__instance(s__Creature50_1,sK517_skl),
inference(resolution,[status(thm)],[f35469,f35376]) ).
fof(f35484,plain,
s__instance(s__Creature50_1,sK516_skl),
inference(resolution,[status(thm)],[f35483,f35468]) ).
fof(f35485,plain,
s__instance(s__Creature50_1,sK515_skl),
inference(resolution,[status(thm)],[f35484,f35467]) ).
fof(f35486,plain,
s__instance(s__Creature50_1,sK514_skl),
inference(resolution,[status(thm)],[f35485,f35466]) ).
fof(f35487,plain,
s__instance(s__Creature50_1,sK513_skl),
inference(resolution,[status(thm)],[f35486,f35465]) ).
fof(f35492,plain,
s__instance(s__Creature50_1,sK512_skl),
inference(resolution,[status(thm)],[f35487,f35464]) ).
fof(f35493,plain,
s__instance(s__Creature50_1,sK511_skl),
inference(resolution,[status(thm)],[f35492,f35463]) ).
fof(f35494,plain,
s__instance(s__Creature50_1,sK510_skl),
inference(resolution,[status(thm)],[f35493,f35462]) ).
fof(f35495,plain,
s__instance(s__Creature50_1,sK509_skl),
inference(resolution,[status(thm)],[f35494,f35461]) ).
fof(f35496,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolution,[status(thm)],[f35495,f35460]) ).
fof(f35497,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f35496,f34386]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n018.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 15:03:45 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.63/1.00 % Drodi V4.1.1
% 65.40/9.22 % Refutation found
% 65.40/9.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 65.40/9.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.22/9.43 % Elapsed time: 8.978651 seconds
% 8.22/9.43 % CPU time: 66.285736 seconds
% 8.22/9.43 % Total memory used: 941.867 MB
% 8.22/9.43 % Net memory used: 916.630 MB
%------------------------------------------------------------------------------