%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 11.01s 2.52s
% Output : CNFRefutation 11.01s
% 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_1539,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_1539) ).
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_MILO,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('theBenchmark.p',prove_from_SUMO_MILO) ).
fof(prove_from_SUMO_MILO_neg,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(assume_negation,[status(cth)],[prove_from_SUMO_MILO]) ).
fof(kb_SUMO_7191,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_7191) ).
cnf(c_131,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_7191]) ).
cnf(c_174,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_175,plain,
( s__instance(B,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_176,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_184,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_1539]) ).
fof(kb_SUMO_7220,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('theBenchmark.p',kb_SUMO_7220) ).
cnf(c_196,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(clausify,[status(thm)],[kb_SUMO_7220]) ).
fof(kb_SUMO_7294,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('theBenchmark.p',kb_SUMO_7294) ).
cnf(c_204,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(clausify,[status(thm)],[kb_SUMO_7294]) ).
fof(nnf_17,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_17]) ).
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_213,plain,
( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_214,plain,
( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_215,plain,
( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_216,plain,
( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_217,plain,
( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_218,plain,
( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_219,plain,
( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_220,plain,
( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_221,plain,
( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_222,plain,
( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_223,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_224,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_225,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_226,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_227,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_228,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_229,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_230,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_231,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_232,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_233,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_234,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_MILO_neg]) ).
cnf(c_268,plain,
s__instance(s__Vertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_174,c_131]) ).
cnf(c_276,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolve,[status(thm)],[c_175,c_131]) ).
cnf(c_285,plain,
s__instance(s__ColdBloodedVertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_204,c_175]) ).
cnf(c_286,plain,
s__instance(s__Reptile,s__SetOrClass),
inference(resolve,[status(thm)],[c_204,c_174]) ).
cnf(c_15801,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_184,c_204]) ).
cnf(c_15802,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_285,c_15801]) ).
cnf(c_624,plain,
( s__subclass(s__Reptile,A)
| ~ s__subclass(s__ColdBloodedVertebrate,A)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_286,c_15802]) ).
cnf(c_15803,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_184,c_131]) ).
cnf(c_15804,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_276,c_15803]) ).
cnf(c_657,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_268,c_15804]) ).
cnf(c_15805,plain,
( s__subclass(s__Reptile,s__Vertebrate)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_624,c_196]) ).
cnf(c_7855,plain,
s__subclass(s__Reptile,s__Vertebrate),
inference(resolve,[status(thm)],[c_268,c_15805]) ).
cnf(c_15806,plain,
( s__subclass(s__Reptile,s__Animal)
| ~ s__instance(s__Reptile,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_657,c_7855]) ).
cnf(c_8019,plain,
s__subclass(s__Reptile,s__Animal),
inference(resolve,[status(thm)],[c_286,c_15806]) ).
cnf(c_8021,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_8019,c_233]) ).
cnf(c_8022,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_8019,c_232]) ).
cnf(c_8023,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_8019,c_231]) ).
cnf(c_8024,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_8019,c_230]) ).
cnf(c_8025,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_8019,c_229]) ).
cnf(c_8026,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_8019,c_228]) ).
cnf(c_8027,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_8019,c_227]) ).
cnf(c_8028,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_8019,c_226]) ).
cnf(c_8029,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_8019,c_225]) ).
cnf(c_8030,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_8019,c_224]) ).
cnf(c_8031,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_8019,c_223]) ).
cnf(c_8032,plain,
s__instance(sK9,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_222]) ).
cnf(c_8033,plain,
s__instance(sK8,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_221]) ).
cnf(c_8034,plain,
s__instance(sK7,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_220]) ).
cnf(c_8035,plain,
s__instance(sK6,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_219]) ).
cnf(c_8036,plain,
s__instance(sK5,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_218]) ).
cnf(c_8037,plain,
s__instance(sK4,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_217]) ).
cnf(c_8038,plain,
s__instance(sK3,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_216]) ).
cnf(c_8039,plain,
s__instance(sK2,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_215]) ).
cnf(c_8040,plain,
s__instance(sK1,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_214]) ).
cnf(c_8041,plain,
s__instance(sK0,s__SetOrClass),
inference(resolve,[status(thm)],[c_8019,c_213]) ).
cnf(c_15807,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_8022,c_176]) ).
cnf(c_15808,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_286,c_15807]) ).
cnf(c_8114,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9) ),
inference(resolve,[status(thm)],[c_8032,c_15808]) ).
cnf(c_15809,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8023,c_176]) ).
cnf(c_15810,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8032,c_15809]) ).
cnf(c_8120,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8) ),
inference(resolve,[status(thm)],[c_8033,c_15810]) ).
cnf(c_15811,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8024,c_176]) ).
cnf(c_15812,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8033,c_15811]) ).
cnf(c_8126,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7) ),
inference(resolve,[status(thm)],[c_8034,c_15812]) ).
cnf(c_15813,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8025,c_176]) ).
cnf(c_15814,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8034,c_15813]) ).
cnf(c_8132,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6) ),
inference(resolve,[status(thm)],[c_8035,c_15814]) ).
cnf(c_15815,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8026,c_176]) ).
cnf(c_15816,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8035,c_15815]) ).
cnf(c_8138,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5) ),
inference(resolve,[status(thm)],[c_8036,c_15816]) ).
cnf(c_15817,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8027,c_176]) ).
cnf(c_15818,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8036,c_15817]) ).
cnf(c_8144,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4) ),
inference(resolve,[status(thm)],[c_8037,c_15818]) ).
cnf(c_15819,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8028,c_176]) ).
cnf(c_15820,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8037,c_15819]) ).
cnf(c_8276,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3) ),
inference(resolve,[status(thm)],[c_8038,c_15820]) ).
cnf(c_15821,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8029,c_176]) ).
cnf(c_15822,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8038,c_15821]) ).
cnf(c_8282,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2) ),
inference(resolve,[status(thm)],[c_8039,c_15822]) ).
cnf(c_15823,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8030,c_176]) ).
cnf(c_15824,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8039,c_15823]) ).
cnf(c_8288,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1) ),
inference(resolve,[status(thm)],[c_8040,c_15824]) ).
cnf(c_15825,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8031,c_176]) ).
cnf(c_15826,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_8040,c_15825]) ).
cnf(c_8294,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_8041,c_15826]) ).
cnf(c_15481,plain,
s__instance(s__Creature50_1,sK1),
inference(resolve,[status(thm)],[c_8294,c_8021]) ).
cnf(c_15484,plain,
s__instance(s__Creature50_1,sK2),
inference(resolve,[status(thm)],[c_15481,c_8288]) ).
cnf(c_15520,plain,
s__instance(s__Creature50_1,sK3),
inference(resolve,[status(thm)],[c_15484,c_8282]) ).
cnf(c_15556,plain,
s__instance(s__Creature50_1,sK4),
inference(resolve,[status(thm)],[c_15520,c_8276]) ).
cnf(c_15592,plain,
s__instance(s__Creature50_1,sK5),
inference(resolve,[status(thm)],[c_15556,c_8144]) ).
cnf(c_15628,plain,
s__instance(s__Creature50_1,sK6),
inference(resolve,[status(thm)],[c_15592,c_8138]) ).
cnf(c_15664,plain,
s__instance(s__Creature50_1,sK7),
inference(resolve,[status(thm)],[c_15628,c_8132]) ).
cnf(c_15700,plain,
s__instance(s__Creature50_1,sK8),
inference(resolve,[status(thm)],[c_15664,c_8126]) ).
cnf(c_15764,plain,
s__instance(s__Creature50_1,sK9),
inference(resolve,[status(thm)],[c_15700,c_8120]) ).
cnf(c_15827,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_15764,c_8114]) ).
cnf(c_15800,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_234,c_15827]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.79 % Computer : n013.cluster.edu
% 0.09/0.79 % Model : x86_64 x86_64
% 0.09/0.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.79 % Memory : 8046.5625MB
% 0.09/0.79 % OS : Linux 6.8.0-71-generic
% 0.09/0.79 % CPULimit : 300
% 0.09/0.79 % WCLimit : 300
% 0.09/0.79 % DateTime : Sun Sep 27 00:59:25 UTC 2026
% 0.09/0.79 % CPUTime :
% 0.09/0.79 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.79 % Process 3913590 was started by sandbox2 on n013,
% 0.09/0.79 % Sun Sep 27 00:59:25 2026
% 0.09/0.79 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 11.01/2.52
% 11.01/2.52 % SInE (scan): 94 to sos (tol 1.5x), 17 to usable (tol 2.0x), 16639 zapped, of 16750 axioms (depth 3).
% 11.01/2.52
% 11.01/2.52 % From the command line: assign(max_seconds, 300).
% 11.01/2.52
% 11.01/2.52 % given #500 (W,wt=11): 1643 s__Organ != s__SetOrClass | s__instance(s__Anaconda,s__Organ). [resolve(373,c,258,a),unit_del(b,279)].
% 11.01/2.52
% 11.01/2.52 % given #1000 (A,wt=17): 612 s__Reptile != A | -s__instance(A,s__SetOrClass) | s__instance(B,A) | -s__instance(B,s__Reptile). [resolve(286,a,180,b)].
% 11.01/2.52
% 11.01/2.52 % given #1500 (T,wt=11): 5901 s__Animal != s__SetOrClass | s__instance(s__Fish,s__Animal). [resolve(521,d,836,a),unit_del(b,279)].
% 11.01/2.52
% 11.01/2.52 % SZS status Theorem for theBenchmark
% 11.01/2.52
% 11.01/2.52 % Proof 1 at 1.22 (+ 0.28) seconds.
% 11.01/2.52 % Length of proof is 83.
% 11.01/2.52 % Level of proof is 17.
% 11.01/2.52 % Maximum clause weight is 123.000.
% 11.01/2.52 % Given clauses 1786.
% 11.01/2.52
% 11.01/2.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------