%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 07:07:30 AM UTC 2026
% Result : Theorem 39.68s 6.29s
% Output : CNFRefutation 39.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 6
% Syntax : Number of formulae : 99 ( 40 unt; 0 def)
% Number of atoms : 295 ( 0 equ)
% Maximal formula atoms : 42 ( 2 avg)
% Number of connectives : 307 ( 111 ~; 109 |; 83 &)
% ( 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 : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 60 ( 1 sgn 5 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(kb_SUMO_26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('theBenchmark.p',kb_SUMO_26) ).
fof(kb_SUMO_27,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('theBenchmark.p',kb_SUMO_27) ).
fof(local_2,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('theBenchmark.p',local_2) ).
fof(prove_from_SUMO,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('theBenchmark.p',prove_from_SUMO) ).
fof(prove_from_SUMO_neg,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(assume_negation,[status(cth)],[prove_from_SUMO]) ).
cnf(c_626,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_628,plain,
( s__instance(C,A)
| ~ s__instance(C,B)
| ~ s__subclass(B,A)
| ~ s__instance(B,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(clausify,[status(thm)],[kb_SUMO_27]) ).
fof(kb_SUMO_6100,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('theBenchmark.p',kb_SUMO_6100) ).
cnf(c_670,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(clausify,[status(thm)],[kb_SUMO_6100]) ).
fof(kb_SUMOcache_7275,axiom,
s__subclass(s__Reptile,s__Animal),
file('theBenchmark.p',kb_SUMOcache_7275) ).
cnf(c_759,plain,
s__subclass(s__Reptile,s__Animal),
inference(clausify,[status(thm)],[kb_SUMOcache_7275]) ).
fof(nnf_16,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(fof_nnf,[status(thm)],[local_2]) ).
fof(sk_local_2_sk,plain,
( ( s__instance(s__Creature50_1,sK0)
& s__subclass(sK9,s__Reptile)
& s__subclass(sK8,sK9)
& s__subclass(sK7,sK8)
& s__subclass(sK6,sK7)
& s__subclass(sK5,sK6)
& s__subclass(sK4,sK5)
& s__subclass(sK3,sK4)
& s__subclass(sK2,sK3)
& s__subclass(sK1,sK2)
& s__subclass(sK0,sK1)
& s__instance(sK9,s__SetOrClass)
& s__instance(sK8,s__SetOrClass)
& s__instance(sK7,s__SetOrClass)
& s__instance(sK6,s__SetOrClass)
& s__instance(sK5,s__SetOrClass)
& s__instance(sK4,s__SetOrClass)
& s__instance(sK3,s__SetOrClass)
& s__instance(sK2,s__SetOrClass)
& s__instance(sK1,s__SetOrClass)
& s__instance(sK0,s__SetOrClass) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9]),skolemize(V_C1,sK0),skolemize(V_C2,sK1),skolemize(V_C3,sK2),skolemize(V_C4,sK3),skolemize(V_C5,sK4),skolemize(V_C6,sK5),skolemize(V_C7,sK6),skolemize(V_C8,sK7),skolemize(V_C9,sK8),skolemize(V_C10,sK9)],[nnf_16]) ).
fof(sk_local_2,plain,
( ( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) )
& ( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ) ),
inference(cnf_transformation,[status(thm)],[sk_local_2_sk]) ).
cnf(c_766,plain,
( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_767,plain,
s__instance(sK0,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_766]) ).
cnf(c_768,plain,
( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_769,plain,
s__instance(sK1,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_768]) ).
cnf(c_770,plain,
( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_771,plain,
s__instance(sK2,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_770]) ).
cnf(c_772,plain,
( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_773,plain,
s__instance(sK3,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_772]) ).
cnf(c_774,plain,
( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_775,plain,
s__instance(sK4,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_774]) ).
cnf(c_776,plain,
( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_777,plain,
s__instance(sK5,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_776]) ).
cnf(c_778,plain,
( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_779,plain,
s__instance(sK6,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_778]) ).
cnf(c_780,plain,
( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_781,plain,
s__instance(sK7,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_780]) ).
cnf(c_782,plain,
( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_783,plain,
s__instance(sK8,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_782]) ).
cnf(c_784,plain,
( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_785,plain,
s__instance(sK9,s__SetOrClass),
inference(resolve,[status(thm)],[c_759,c_784]) ).
cnf(c_786,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_787,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_759,c_786]) ).
cnf(c_788,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_789,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_759,c_788]) ).
cnf(c_790,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_791,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_759,c_790]) ).
cnf(c_792,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_793,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_759,c_792]) ).
cnf(c_794,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_795,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_759,c_794]) ).
cnf(c_796,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_797,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_759,c_796]) ).
cnf(c_798,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_799,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_759,c_798]) ).
cnf(c_800,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_801,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_759,c_800]) ).
cnf(c_802,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_803,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_759,c_802]) ).
cnf(c_804,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_805,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_759,c_804]) ).
cnf(c_806,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_807,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_759,c_806]) ).
cnf(c_808,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_neg]) ).
cnf(c_1248,plain,
s__instance(s__Reptile,s__SetOrClass),
inference(resolve,[status(thm)],[c_670,c_626]) ).
cnf(c_29891,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_787,c_628]) ).
cnf(c_29892,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_769,c_29891]) ).
cnf(c_1772,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_767,c_29892]) ).
cnf(c_29893,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_789,c_628]) ).
cnf(c_29894,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_771,c_29893]) ).
cnf(c_1790,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1) ),
inference(resolve,[status(thm)],[c_769,c_29894]) ).
cnf(c_29895,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_791,c_628]) ).
cnf(c_29896,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_773,c_29895]) ).
cnf(c_1793,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2) ),
inference(resolve,[status(thm)],[c_771,c_29896]) ).
cnf(c_29897,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_793,c_628]) ).
cnf(c_29898,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_775,c_29897]) ).
cnf(c_1796,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3) ),
inference(resolve,[status(thm)],[c_773,c_29898]) ).
cnf(c_29899,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_795,c_628]) ).
cnf(c_29900,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_777,c_29899]) ).
cnf(c_1799,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4) ),
inference(resolve,[status(thm)],[c_775,c_29900]) ).
cnf(c_29901,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_797,c_628]) ).
cnf(c_29902,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_779,c_29901]) ).
cnf(c_1802,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5) ),
inference(resolve,[status(thm)],[c_777,c_29902]) ).
cnf(c_29903,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_799,c_628]) ).
cnf(c_29904,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_781,c_29903]) ).
cnf(c_1805,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6) ),
inference(resolve,[status(thm)],[c_779,c_29904]) ).
cnf(c_29905,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_801,c_628]) ).
cnf(c_29906,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_783,c_29905]) ).
cnf(c_2239,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7) ),
inference(resolve,[status(thm)],[c_781,c_29906]) ).
cnf(c_29907,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_803,c_628]) ).
cnf(c_29908,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_785,c_29907]) ).
cnf(c_2243,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8) ),
inference(resolve,[status(thm)],[c_783,c_29908]) ).
cnf(c_29909,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass)
| ~ s__instance(s__Reptile,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_805,c_628]) ).
cnf(c_29910,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1248,c_29909]) ).
cnf(c_2247,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9) ),
inference(resolve,[status(thm)],[c_785,c_29910]) ).
cnf(c_14259,plain,
s__instance(s__Creature50_1,sK1),
inference(resolve,[status(thm)],[c_1772,c_807]) ).
cnf(c_14382,plain,
s__instance(s__Creature50_1,sK2),
inference(resolve,[status(thm)],[c_1790,c_14259]) ).
cnf(c_15363,plain,
s__instance(s__Creature50_1,sK3),
inference(resolve,[status(thm)],[c_1793,c_14382]) ).
cnf(c_15482,plain,
s__instance(s__Creature50_1,sK4),
inference(resolve,[status(thm)],[c_1796,c_15363]) ).
cnf(c_15500,plain,
s__instance(s__Creature50_1,sK5),
inference(resolve,[status(thm)],[c_1799,c_15482]) ).
cnf(c_16036,plain,
s__instance(s__Creature50_1,sK6),
inference(resolve,[status(thm)],[c_1802,c_15500]) ).
cnf(c_16053,plain,
s__instance(s__Creature50_1,sK7),
inference(resolve,[status(thm)],[c_1805,c_16036]) ).
cnf(c_29834,plain,
s__instance(s__Creature50_1,sK8),
inference(resolve,[status(thm)],[c_2239,c_16053]) ).
cnf(c_29862,plain,
s__instance(s__Creature50_1,sK9),
inference(resolve,[status(thm)],[c_2243,c_29834]) ).
cnf(c_29911,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_2247,c_29862]) ).
cnf(c_29890,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_808,c_29911]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 01:00:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2913918 was started by sandbox on n020,
% 0.10/0.37 % Sun Sep 27 01:00:35 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 39.68/6.29
% 39.68/6.29 % SInE (scan): 557 to sos (tol 1.5x), 55 to usable (tol 2.0x), 14177 zapped, of 14789 axioms (depth 3).
% 39.68/6.29
% 39.68/6.29 % From the command line: assign(max_seconds, 300).
% 39.68/6.29
% 39.68/6.29 % given #500 (W,wt=8): 7290 s__instance(s__CognitiveAgent,s__Class). [resolve(876,a,122,a),unit_del(b,341)].
% 39.68/6.29
% 39.68/6.29 % given #1000 (F,wt=11): 8367 -s__disjoint(s__Vertebrate,s__Vertebrate) | -s__instance(A,s__Vertebrate). [factor(8353,c,d),unit_del(b,896)].
% 39.68/6.29
% 39.68/6.29 % given #1500 (W,wt=8): 14400 s__instance(s__Creature50_1,s__Physical). [resolve(1324,a,897,a),unit_del(a,745)].
% 39.68/6.29
% 39.68/6.29 % given #2000 (F,wt=11): 14168 -s__disjoint(s__Entity,s__Protein) | -s__instance(A,s__Protein). [resolve(1312,b,881,a)].
% 39.68/6.29
% 39.68/6.29 % given #2500 (T,wt=11): 2200 -s__subclass(s__Carnivore,s__Feline) | s__Feline = s__Carnivore. [resolve(643,c,226,a),unit_del(a,837),unit_del(b,853)].
% 39.68/6.29
% 39.68/6.29 % SZS status Theorem for theBenchmark
% 39.68/6.29
% 39.68/6.29 % Proof 1 at 4.70 (+ 0.99) seconds.
% 39.68/6.29 % Length of proof is 72.
% 39.68/6.29 % Level of proof is 13.
% 39.68/6.29 % Maximum clause weight is 120.000.
% 39.68/6.29 % Given clauses 2591.
% 39.68/6.29
% 39.68/6.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------