%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+4 : 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:31 AM UTC 2026
% Result : Theorem 5.99s 1.30s
% Output : CNFRefutation 5.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 8
% Syntax : Number of formulae : 117 ( 47 unt; 0 def)
% Number of atoms : 344 ( 0 equ)
% Maximal formula atoms : 42 ( 2 avg)
% Number of connectives : 364 ( 137 ~; 135 |; 86 &)
% ( 0 <=>; 6 =>; 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 : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 74 ( 2 sgn 8 !; 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(kb_SUMO_1294,axiom,
! [V__INST1,V__INST2,V__INST3] :
( ( s__instance(V__INST1,s__SetOrClass)
& s__instance(V__INST2,s__SetOrClass)
& s__instance(V__INST3,s__SetOrClass) )
=> ( ( s__subclass(V__INST2,V__INST3)
& s__subclass(V__INST1,V__INST2) )
=> s__subclass(V__INST1,V__INST3) ) ),
file('theBenchmark.p',kb_SUMO_1294) ).
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]) ).
fof(kb_SUMO_5997,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_5997) ).
cnf(c_121,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_5997]) ).
fof(nnf_61,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_61]) ).
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_128,plain,
( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_129,plain,
( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_130,plain,
( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_131,plain,
( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_132,plain,
( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_133,plain,
( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_134,plain,
( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_135,plain,
( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_136,plain,
( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_137,plain,
( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_138,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_139,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_140,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_141,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_142,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_143,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_144,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_145,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_146,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_147,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_148,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_149,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_150,plain,
( s__instance(B,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_151,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]) ).
cnf(c_159,plain,
( s__subclass(C,A)
| ~ s__subclass(B,A)
| ~ s__subclass(C,B)
| ~ s__instance(C,s__SetOrClass)
| ~ s__instance(B,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(clausify,[status(thm)],[kb_SUMO_1294]) ).
fof(kb_SUMO_6026,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('theBenchmark.p',kb_SUMO_6026) ).
cnf(c_168,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(clausify,[status(thm)],[kb_SUMO_6026]) ).
fof(kb_SUMO_6100,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('theBenchmark.p',kb_SUMO_6100) ).
cnf(c_176,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(clausify,[status(thm)],[kb_SUMO_6100]) ).
cnf(c_178,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_neg]) ).
cnf(c_201,plain,
s__instance(s__Vertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_149,c_121]) ).
cnf(c_205,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolve,[status(thm)],[c_150,c_121]) ).
cnf(c_214,plain,
s__instance(s__ColdBloodedVertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_176,c_150]) ).
cnf(c_215,plain,
s__instance(s__Reptile,s__SetOrClass),
inference(resolve,[status(thm)],[c_176,c_149]) ).
cnf(c_5632,plain,
( s__subclass(s__Reptile,A)
| ~ s__subclass(s__ColdBloodedVertebrate,A)
| ~ s__instance(s__Reptile,s__SetOrClass)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_159,c_176]) ).
cnf(c_5633,plain,
( s__subclass(s__Reptile,A)
| ~ s__subclass(s__ColdBloodedVertebrate,A)
| ~ s__instance(s__Reptile,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_214,c_5632]) ).
cnf(c_432,plain,
( s__subclass(s__Reptile,A)
| ~ s__subclass(s__ColdBloodedVertebrate,A)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_215,c_5633]) ).
cnf(c_5634,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate)
| ~ s__instance(A,s__SetOrClass)
| ~ s__instance(s__Vertebrate,s__SetOrClass)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_159,c_121]) ).
cnf(c_5635,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate)
| ~ s__instance(A,s__SetOrClass)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_205,c_5634]) ).
cnf(c_444,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_201,c_5635]) ).
cnf(c_5636,plain,
( s__subclass(s__Reptile,s__Vertebrate)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_432,c_168]) ).
cnf(c_2564,plain,
s__subclass(s__Reptile,s__Vertebrate),
inference(resolve,[status(thm)],[c_201,c_5636]) ).
cnf(c_5637,plain,
( s__subclass(s__Reptile,s__Animal)
| ~ s__instance(s__Reptile,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_444,c_2564]) ).
cnf(c_3109,plain,
s__subclass(s__Reptile,s__Animal),
inference(resolve,[status(thm)],[c_215,c_5637]) ).
cnf(c_3111,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_3109,c_148]) ).
cnf(c_3112,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_3109,c_147]) ).
cnf(c_3113,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_3109,c_146]) ).
cnf(c_3114,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_3109,c_145]) ).
cnf(c_3115,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_3109,c_144]) ).
cnf(c_3116,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_3109,c_143]) ).
cnf(c_3117,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_3109,c_142]) ).
cnf(c_3118,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_3109,c_141]) ).
cnf(c_3119,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_3109,c_140]) ).
cnf(c_3120,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_3109,c_139]) ).
cnf(c_3121,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_3109,c_138]) ).
cnf(c_3122,plain,
s__instance(sK9,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_137]) ).
cnf(c_3123,plain,
s__instance(sK8,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_136]) ).
cnf(c_3124,plain,
s__instance(sK7,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_135]) ).
cnf(c_3125,plain,
s__instance(sK6,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_134]) ).
cnf(c_3126,plain,
s__instance(sK5,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_133]) ).
cnf(c_3127,plain,
s__instance(sK4,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_132]) ).
cnf(c_3128,plain,
s__instance(sK3,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_131]) ).
cnf(c_3129,plain,
s__instance(sK2,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_130]) ).
cnf(c_3130,plain,
s__instance(sK1,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_129]) ).
cnf(c_3131,plain,
s__instance(sK0,s__SetOrClass),
inference(resolve,[status(thm)],[c_3109,c_128]) ).
cnf(c_5638,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_3112,c_151]) ).
cnf(c_5639,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_215,c_5638]) ).
cnf(c_3169,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9) ),
inference(resolve,[status(thm)],[c_3122,c_5639]) ).
cnf(c_5640,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3113,c_151]) ).
cnf(c_5641,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3122,c_5640]) ).
cnf(c_3175,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8) ),
inference(resolve,[status(thm)],[c_3123,c_5641]) ).
cnf(c_5642,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3114,c_151]) ).
cnf(c_5643,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3123,c_5642]) ).
cnf(c_3258,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7) ),
inference(resolve,[status(thm)],[c_3124,c_5643]) ).
cnf(c_5644,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3115,c_151]) ).
cnf(c_5645,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3124,c_5644]) ).
cnf(c_3264,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6) ),
inference(resolve,[status(thm)],[c_3125,c_5645]) ).
cnf(c_5646,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3116,c_151]) ).
cnf(c_5647,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3125,c_5646]) ).
cnf(c_3270,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5) ),
inference(resolve,[status(thm)],[c_3126,c_5647]) ).
cnf(c_5648,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3117,c_151]) ).
cnf(c_5649,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3126,c_5648]) ).
cnf(c_3276,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4) ),
inference(resolve,[status(thm)],[c_3127,c_5649]) ).
cnf(c_5650,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3118,c_151]) ).
cnf(c_5651,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3127,c_5650]) ).
cnf(c_3282,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3) ),
inference(resolve,[status(thm)],[c_3128,c_5651]) ).
cnf(c_5652,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3119,c_151]) ).
cnf(c_5653,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3128,c_5652]) ).
cnf(c_3288,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2) ),
inference(resolve,[status(thm)],[c_3129,c_5653]) ).
cnf(c_5654,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3120,c_151]) ).
cnf(c_5655,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3129,c_5654]) ).
cnf(c_3371,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1) ),
inference(resolve,[status(thm)],[c_3130,c_5655]) ).
cnf(c_5656,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3121,c_151]) ).
cnf(c_5657,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3130,c_5656]) ).
cnf(c_3377,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_3131,c_5657]) ).
cnf(c_5257,plain,
s__instance(s__Creature50_1,sK1),
inference(resolve,[status(thm)],[c_3377,c_3111]) ).
cnf(c_5260,plain,
s__instance(s__Creature50_1,sK2),
inference(resolve,[status(thm)],[c_5257,c_3371]) ).
cnf(c_5282,plain,
s__instance(s__Creature50_1,sK3),
inference(resolve,[status(thm)],[c_5260,c_3288]) ).
cnf(c_5304,plain,
s__instance(s__Creature50_1,sK4),
inference(resolve,[status(thm)],[c_5282,c_3282]) ).
cnf(c_5486,plain,
s__instance(s__Creature50_1,sK5),
inference(resolve,[status(thm)],[c_5304,c_3276]) ).
cnf(c_5508,plain,
s__instance(s__Creature50_1,sK6),
inference(resolve,[status(thm)],[c_5486,c_3270]) ).
cnf(c_5530,plain,
s__instance(s__Creature50_1,sK7),
inference(resolve,[status(thm)],[c_5508,c_3264]) ).
cnf(c_5552,plain,
s__instance(s__Creature50_1,sK8),
inference(resolve,[status(thm)],[c_5530,c_3258]) ).
cnf(c_5579,plain,
s__instance(s__Creature50_1,sK9),
inference(resolve,[status(thm)],[c_5552,c_3175]) ).
cnf(c_5658,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_5579,c_3169]) ).
cnf(c_5631,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_178,c_5658]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 01:00:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2914297 was started by sandbox on n020,
% 0.09/0.37 % Sun Sep 27 01:00:49 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 5.99/1.30
% 5.99/1.30 % SInE (scan): 61 to sos (tol 1.5x), 17 to usable (tol 2.0x), 7141 zapped, of 7219 axioms (depth 3).
% 5.99/1.30
% 5.99/1.30 % From the command line: assign(max_seconds, 300).
% 5.99/1.30
% 5.99/1.30 % given #500 (W,wt=11): 2720 -s__subclass(s__Vertebrate,s__Bird) | s__Bird = s__Vertebrate. [resolve(2717,a,158,d),flip(d),unit_del(a,199),unit_del(b,201)].
% 5.99/1.30
% 5.99/1.30 % SZS status Theorem for theBenchmark
% 5.99/1.30
% 5.99/1.30 % Proof 1 at 0.66 (+ 0.16) seconds.
% 5.99/1.30 % Length of proof is 83.
% 5.99/1.30 % Level of proof is 17.
% 5.99/1.30 % Maximum clause weight is 123.000.
% 5.99/1.30 % Given clauses 663.
% 5.99/1.30
% 5.99/1.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------