%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+6 : 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 : n014.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 222.13s 33.06s
% Output : CNFRefutation 222.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 9
% Syntax : Number of formulae : 88 ( 37 unt; 0 def)
% Number of atoms : 285 ( 2 equ)
% Maximal formula atoms : 42 ( 3 avg)
% Number of connectives : 288 ( 91 ~; 96 |; 92 &)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 16 con; 0-2 aty)
% Number of variables : 89 ( 11 sgn 14 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(kb_SUMO_26635,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_26635) ).
fof(kb_SUMO_26636,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_26636) ).
fof(kb_SUMO_28461,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_28461) ).
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(kb_SUMO_32603,axiom,
! [V__C2,V__U,V__C1] :
( V__U = s__UnionFn(V__C1,V__C2)
<=> ! [V__I1,V__I2,V__I3] :
( ( s__instance(V__C2,s__SetOrClass)
& s__instance(V__U,s__SetOrClass)
& s__instance(V__C1,s__SetOrClass) )
=> ( ( s__instance(V__I3,V__U)
& s__instance(V__I2,V__C2)
& s__instance(V__I1,V__C1) )
=> ( ( s__instance(V__I3,V__C2)
| s__instance(V__I3,V__C1) )
& s__instance(V__I2,V__U)
& s__instance(V__I1,V__U) ) ) ) ),
file('theBenchmark.p',kb_SUMO_32603) ).
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]) ).
cnf(c_197,plain,
( s__instance(A,s__SetOrClass)
| s__UnionFn(A,B) = C ),
inference(clausify,[status(thm)],[kb_SUMO_32603]) ).
fof(kb_SUMO_35116,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_35116) ).
cnf(c_213,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_35116]) ).
cnf(c_292,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26635]) ).
cnf(c_293,plain,
( s__instance(B,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26635]) ).
cnf(c_294,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_26636]) ).
cnf(c_303,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_28461]) ).
fof(kb_SUMO_35145,axiom,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('theBenchmark.p',kb_SUMO_35145) ).
cnf(c_315,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
inference(clausify,[status(thm)],[kb_SUMO_35145]) ).
fof(kb_SUMO_35219,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('theBenchmark.p',kb_SUMO_35219) ).
cnf(c_322,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(clausify,[status(thm)],[kb_SUMO_35219]) ).
fof(nnf_21,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_21]) ).
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_339,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_340,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_341,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_342,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_343,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_344,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_345,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_346,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_347,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_348,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_349,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_350,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_MILO_neg]) ).
cnf(c_528,plain,
( s__subclass(s__UnionFn(A,B),s__ColdBloodedVertebrate)
| s__instance(A,s__SetOrClass) ),
inference(paramod,[status(thm)],[c_197,c_322]) ).
cnf(c_1719,plain,
s__instance(s__Vertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_292,c_213]) ).
cnf(c_2460,plain,
s__instance(s__ColdBloodedVertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_293,c_322]) ).
cnf(c_2467,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolve,[status(thm)],[c_293,c_213]) ).
cnf(c_51396,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_303,c_213]) ).
cnf(c_51397,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_2467,c_51396]) ).
cnf(c_7866,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1719,c_51397]) ).
cnf(c_51398,plain,
( s__subclass(A,s__Vertebrate)
| ~ s__subclass(A,s__ColdBloodedVertebrate)
| ~ s__instance(A,s__SetOrClass)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_315,c_303]) ).
cnf(c_51399,plain,
( s__subclass(A,s__Vertebrate)
| ~ s__subclass(A,s__ColdBloodedVertebrate)
| ~ s__instance(A,s__SetOrClass)
| ~ s__instance(s__ColdBloodedVertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1719,c_51398]) ).
cnf(c_11536,plain,
( s__subclass(A,s__Vertebrate)
| ~ s__subclass(A,s__ColdBloodedVertebrate)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_2460,c_51399]) ).
cnf(c_51400,plain,
( s__subclass(B,s__ColdBloodedVertebrate)
| s__instance(A,s__SetOrClass)
| s__instance(A,s__SetOrClass) ),
inference(paramod,[status(thm)],[c_197,c_528]) ).
cnf(c_16760,plain,
( s__subclass(B,s__ColdBloodedVertebrate)
| s__instance(A,s__SetOrClass) ),
inference(copy,[status(thm)],[c_51400]) ).
cnf(c_17828,plain,
( s__instance(B,s__SetOrClass)
| s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_16760,c_292]) ).
cnf(c_17834,plain,
s__instance(A,s__SetOrClass),
inference(factor,[status(thm)],[c_17828]) ).
cnf(c_18117,plain,
( s__subclass(A,s__Vertebrate)
| ~ s__subclass(A,s__ColdBloodedVertebrate) ),
inference(resolve,[status(thm)],[c_17834,c_11536]) ).
cnf(c_19116,plain,
( s__subclass(A,s__Animal)
| ~ s__subclass(A,s__Vertebrate) ),
inference(resolve,[status(thm)],[c_17834,c_7866]) ).
cnf(c_51401,plain,
( s__subclass(B,C)
| ~ s__subclass(A,C)
| ~ s__subclass(B,A)
| ~ s__instance(B,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_17834,c_303]) ).
cnf(c_51402,plain,
( s__subclass(A,C)
| ~ s__subclass(B,C)
| ~ s__subclass(A,B)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_17834,c_51401]) ).
cnf(c_21634,plain,
( s__subclass(A,C)
| ~ s__subclass(B,C)
| ~ s__subclass(A,B) ),
inference(resolve,[status(thm)],[c_17834,c_51402]) ).
cnf(c_51403,plain,
( s__instance(C,B)
| ~ s__instance(C,A)
| ~ s__subclass(A,B)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_17834,c_294]) ).
cnf(c_21641,plain,
( s__instance(C,B)
| ~ s__instance(C,A)
| ~ s__subclass(A,B) ),
inference(resolve,[status(thm)],[c_17834,c_51403]) ).
cnf(c_23241,plain,
s__subclass(s__Reptile,s__Vertebrate),
inference(resolve,[status(thm)],[c_18117,c_322]) ).
cnf(c_25760,plain,
s__subclass(s__Reptile,s__Animal),
inference(resolve,[status(thm)],[c_19116,c_23241]) ).
cnf(c_25766,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_25760,c_349]) ).
cnf(c_25767,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_25760,c_348]) ).
cnf(c_25768,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_25760,c_347]) ).
cnf(c_25769,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_25760,c_346]) ).
cnf(c_25770,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_25760,c_345]) ).
cnf(c_25771,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_25760,c_344]) ).
cnf(c_25772,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_25760,c_343]) ).
cnf(c_25773,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_25760,c_342]) ).
cnf(c_25774,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_25760,c_341]) ).
cnf(c_25775,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_25760,c_340]) ).
cnf(c_25776,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_25760,c_339]) ).
cnf(c_41281,plain,
( s__subclass(sK0,A)
| ~ s__subclass(sK1,A) ),
inference(resolve,[status(thm)],[c_21634,c_25776]) ).
cnf(c_41282,plain,
( s__subclass(sK1,A)
| ~ s__subclass(sK2,A) ),
inference(resolve,[status(thm)],[c_21634,c_25775]) ).
cnf(c_41283,plain,
( s__subclass(sK2,A)
| ~ s__subclass(sK3,A) ),
inference(resolve,[status(thm)],[c_21634,c_25774]) ).
cnf(c_41284,plain,
( s__subclass(sK3,A)
| ~ s__subclass(sK4,A) ),
inference(resolve,[status(thm)],[c_21634,c_25773]) ).
cnf(c_41285,plain,
( s__subclass(sK4,A)
| ~ s__subclass(sK5,A) ),
inference(resolve,[status(thm)],[c_21634,c_25772]) ).
cnf(c_41286,plain,
( s__subclass(sK5,A)
| ~ s__subclass(sK6,A) ),
inference(resolve,[status(thm)],[c_21634,c_25771]) ).
cnf(c_41287,plain,
( s__subclass(sK6,A)
| ~ s__subclass(sK7,A) ),
inference(resolve,[status(thm)],[c_21634,c_25770]) ).
cnf(c_41288,plain,
( s__subclass(sK7,A)
| ~ s__subclass(sK8,A) ),
inference(resolve,[status(thm)],[c_21634,c_25769]) ).
cnf(c_41289,plain,
( s__subclass(sK8,A)
| ~ s__subclass(sK9,A) ),
inference(resolve,[status(thm)],[c_21634,c_25768]) ).
cnf(c_42186,plain,
s__subclass(sK8,s__Reptile),
inference(resolve,[status(thm)],[c_41289,c_25767]) ).
cnf(c_42247,plain,
s__subclass(sK7,s__Reptile),
inference(resolve,[status(thm)],[c_42186,c_41288]) ).
cnf(c_42318,plain,
s__subclass(sK6,s__Reptile),
inference(resolve,[status(thm)],[c_42247,c_41287]) ).
cnf(c_42388,plain,
s__subclass(sK5,s__Reptile),
inference(resolve,[status(thm)],[c_42318,c_41286]) ).
cnf(c_42457,plain,
s__subclass(sK4,s__Reptile),
inference(resolve,[status(thm)],[c_42388,c_41285]) ).
cnf(c_42526,plain,
s__subclass(sK3,s__Reptile),
inference(resolve,[status(thm)],[c_42457,c_41284]) ).
cnf(c_42595,plain,
s__subclass(sK2,s__Reptile),
inference(resolve,[status(thm)],[c_42526,c_41283]) ).
cnf(c_42664,plain,
s__subclass(sK1,s__Reptile),
inference(resolve,[status(thm)],[c_42595,c_41282]) ).
cnf(c_42733,plain,
s__subclass(sK0,s__Reptile),
inference(resolve,[status(thm)],[c_42664,c_41281]) ).
cnf(c_50997,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_21641,c_42733]) ).
cnf(c_51404,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_50997,c_25766]) ).
cnf(c_51395,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_350,c_51404]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR109+6 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n014.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 00:59:32 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.43 % Process 271317 was started by sandbox2 on n014,
% 0.17/0.43 % Sun Sep 27 00:59:32 2026
% 0.17/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.26/0.59 WARNING: token truncated at 4095 chars (line 64008)
% 0.26/0.59 WARNING: token truncated at 4095 chars (line 64302)
% 0.26/0.59 WARNING: token truncated at 4095 chars (line 64389)
% 0.26/0.60 WARNING: token truncated at 4095 chars (line 65430)
% 0.36/0.60 WARNING: token truncated at 4095 chars (line 65625)
% 0.36/0.60 WARNING: token truncated at 4095 chars (line 65856)
% 222.13/33.06
% 222.13/33.06 % SInE (scan): 126 to sos (tol 1.5x), 23 to usable (tol 2.0x), 55439 zapped, of 55588 axioms (depth 3).
% 222.13/33.06
% 222.13/33.06 % From the command line: assign(max_seconds, 300).
% 222.13/33.06
% 222.13/33.06 % given #500 (A,wt=30): 424 -s__instance(A,s__Object) | -s__subclass(B,s__Organism) | -s__instance(B,s__SetOrClass) | s__instance(f1(f22(C,D,s__Seafood),B,A),s__DeadFn(B)) | s__UnionFn(s__Seafood,C) = D. [resolve(276,d,200,b)].
% 222.13/33.06
% 222.13/33.06 % given #1000 (F,wt=5): 22832 -s__instance(s__Creature50_1,s__Artifact). [resolve(17862,a,211,a)].
% 222.13/33.06
% 222.13/33.06 % given #1500 (F,wt=12): 28555 -s__disjoint(A,s__Animal) | -s__instance(f20(s__Object,s__Animal),A). [resolve(16223,a,21661,c)].
% 222.13/33.06
% 222.13/33.06 % given #2000 (T,wt=8): 33859 s__disjoint(A,s__Seafood) | -s__disjoint(s__ColdBloodedVertebrate,s__Vertebrate). [factor(33857,a,b)].
% 222.13/33.06
% 222.13/33.06 % given #2500 (A,wt=18): 6883 s__instance(f24(A,s__Leg,B),s__Leg) | -s__disjoint(s__SetOrClass,s__Leg) | -s__instance(s__SetOrClass,s__UnionFn(B,A)). [para(202(a,2),2765(b,2))].
% 222.13/33.06
% 222.13/33.06 % given #3000 (T,wt=8): 41304 -s__subclass(s__Agent,A) | s__subclass(s__Amphibian,A). [resolve(21634,a,25440,a)].
% 222.13/33.06
% 222.13/33.06 % given #3500 (A,wt=15): 10760 s__instance(f24(A,s__GeopoliticalArea,B),s__GeopoliticalArea) | s__subclass(s__UnionFn(B,A),s__GeopoliticalArea). [para(202(a,2),6716(a,1))].
% 222.13/33.06
% 222.13/33.06 % given #4000 (F,wt=21): 39717 -s__instance(f20(s__Object,s__SetOrClass),s__Snake) | -s__instance(f20(s__Organism,s__Agent),s__Limb) | -s__part(f20(s__Organism,s__Agent),f20(s__Object,s__SetOrClass)). [resolve(28877,b,29539,a)].
% 222.13/33.06
% 222.13/33.06 % SZS status Theorem for theBenchmark
% 222.13/33.06
% 222.13/33.06 % Proof 1 at 26.51 (+ 4.96) seconds.
% 222.13/33.06 % Length of proof is 72.
% 222.13/33.06 % Level of proof is 21.
% 222.13/33.06 % Maximum clause weight is 120.000.
% 222.13/33.06 % Given clauses 4387.
% 222.13/33.06
% 222.13/33.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------