%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+3 : 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 : n016.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 139.68s 21.88s
% Output : CNFRefutation 139.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_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(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]) ).
cnf(c_900,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26635]) ).
cnf(c_902,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]) ).
fof(kb_SUMO_59871,axiom,
s__subclass(s__Reptile,s__Animal),
file('theBenchmark.p',kb_SUMO_59871) ).
cnf(c_1092,plain,
s__subclass(s__Reptile,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_59871]) ).
fof(kb_SUMO_59877,axiom,
s__subclass(s__Reptile,s__Entity),
file('theBenchmark.p',kb_SUMO_59877) ).
cnf(c_1097,plain,
s__subclass(s__Reptile,s__Entity),
inference(clausify,[status(thm)],[kb_SUMO_59877]) ).
fof(nnf_29,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_29]) ).
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_1135,plain,
( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1136,plain,
s__instance(sK0,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1135]) ).
cnf(c_1137,plain,
( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1138,plain,
s__instance(sK1,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1137]) ).
cnf(c_1139,plain,
( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1140,plain,
s__instance(sK2,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1139]) ).
cnf(c_1141,plain,
( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1142,plain,
s__instance(sK3,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1141]) ).
cnf(c_1143,plain,
( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1144,plain,
s__instance(sK4,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1143]) ).
cnf(c_1145,plain,
( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1146,plain,
s__instance(sK5,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1145]) ).
cnf(c_1147,plain,
( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1148,plain,
s__instance(sK6,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1147]) ).
cnf(c_1149,plain,
( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1150,plain,
s__instance(sK7,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1149]) ).
cnf(c_1151,plain,
( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1152,plain,
s__instance(sK8,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1151]) ).
cnf(c_1153,plain,
( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1154,plain,
s__instance(sK9,s__SetOrClass),
inference(resolve,[status(thm)],[c_1092,c_1153]) ).
cnf(c_1155,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1156,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_1092,c_1155]) ).
cnf(c_1157,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1158,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_1092,c_1157]) ).
cnf(c_1159,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1160,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_1092,c_1159]) ).
cnf(c_1161,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1162,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_1092,c_1161]) ).
cnf(c_1163,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1164,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_1092,c_1163]) ).
cnf(c_1165,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1166,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_1092,c_1165]) ).
cnf(c_1167,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1168,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_1092,c_1167]) ).
cnf(c_1169,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1170,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_1092,c_1169]) ).
cnf(c_1171,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1172,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_1092,c_1171]) ).
cnf(c_1173,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1174,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_1092,c_1173]) ).
cnf(c_1175,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1176,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_1092,c_1175]) ).
cnf(c_1177,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_MILO_neg]) ).
cnf(c_3449,plain,
s__instance(s__Reptile,s__SetOrClass),
inference(resolve,[status(thm)],[c_900,c_1097]) ).
cnf(c_25438,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1172]) ).
cnf(c_25439,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1154,c_25438]) ).
cnf(c_4589,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8) ),
inference(resolve,[status(thm)],[c_1152,c_25439]) ).
cnf(c_25440,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1170]) ).
cnf(c_25441,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1152,c_25440]) ).
cnf(c_4590,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7) ),
inference(resolve,[status(thm)],[c_1150,c_25441]) ).
cnf(c_25442,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1168]) ).
cnf(c_25443,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1150,c_25442]) ).
cnf(c_4591,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6) ),
inference(resolve,[status(thm)],[c_1148,c_25443]) ).
cnf(c_25444,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1166]) ).
cnf(c_25445,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1148,c_25444]) ).
cnf(c_4592,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5) ),
inference(resolve,[status(thm)],[c_1146,c_25445]) ).
cnf(c_25446,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1164]) ).
cnf(c_25447,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1146,c_25446]) ).
cnf(c_4593,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4) ),
inference(resolve,[status(thm)],[c_1144,c_25447]) ).
cnf(c_25448,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1162]) ).
cnf(c_25449,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1144,c_25448]) ).
cnf(c_4594,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3) ),
inference(resolve,[status(thm)],[c_1142,c_25449]) ).
cnf(c_25450,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1160]) ).
cnf(c_25451,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1142,c_25450]) ).
cnf(c_4595,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2) ),
inference(resolve,[status(thm)],[c_1140,c_25451]) ).
cnf(c_25452,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1158]) ).
cnf(c_25453,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1140,c_25452]) ).
cnf(c_4596,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1) ),
inference(resolve,[status(thm)],[c_1138,c_25453]) ).
cnf(c_25454,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_902,c_1156]) ).
cnf(c_25455,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1138,c_25454]) ).
cnf(c_4597,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_1136,c_25455]) ).
cnf(c_25456,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_1174,c_902]) ).
cnf(c_25457,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_3449,c_25456]) ).
cnf(c_5105,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9) ),
inference(resolve,[status(thm)],[c_1154,c_25457]) ).
cnf(c_19296,plain,
s__instance(s__Creature50_1,sK1),
inference(resolve,[status(thm)],[c_4597,c_1176]) ).
cnf(c_19297,plain,
s__instance(s__Creature50_1,sK2),
inference(resolve,[status(thm)],[c_19296,c_4596]) ).
cnf(c_19307,plain,
s__instance(s__Creature50_1,sK3),
inference(resolve,[status(thm)],[c_19297,c_4595]) ).
cnf(c_19317,plain,
s__instance(s__Creature50_1,sK4),
inference(resolve,[status(thm)],[c_19307,c_4594]) ).
cnf(c_19341,plain,
s__instance(s__Creature50_1,sK5),
inference(resolve,[status(thm)],[c_19317,c_4593]) ).
cnf(c_19351,plain,
s__instance(s__Creature50_1,sK6),
inference(resolve,[status(thm)],[c_19341,c_4592]) ).
cnf(c_19361,plain,
s__instance(s__Creature50_1,sK7),
inference(resolve,[status(thm)],[c_19351,c_4591]) ).
cnf(c_19371,plain,
s__instance(s__Creature50_1,sK8),
inference(resolve,[status(thm)],[c_19361,c_4590]) ).
cnf(c_19397,plain,
s__instance(s__Creature50_1,sK9),
inference(resolve,[status(thm)],[c_19371,c_4589]) ).
cnf(c_25458,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_5105,c_19397]) ).
cnf(c_25437,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1177,c_25458]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR109+3 : 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.34 % Computer : n016.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Sun Sep 27 01:04:47 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.34 % Process 2093643 was started by sandbox2 on n016,
% 0.09/0.34 % Sun Sep 27 01:04:47 2026
% 0.09/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.45 WARNING: token truncated at 4095 chars (line 64008)
% 0.12/0.45 WARNING: token truncated at 4095 chars (line 64302)
% 0.12/0.45 WARNING: token truncated at 4095 chars (line 64389)
% 0.12/0.45 WARNING: token truncated at 4095 chars (line 65430)
% 0.12/0.46 WARNING: token truncated at 4095 chars (line 65625)
% 0.12/0.46 WARNING: token truncated at 4095 chars (line 65856)
% 139.68/21.88
% 139.68/21.88 % SInE (scan): 812 to sos (tol 1.5x), 94 to usable (tol 2.0x), 144197 zapped, of 145103 axioms (depth 3).
% 139.68/21.88
% 139.68/21.88 % From the command line: assign(max_seconds, 300).
% 139.68/21.88
% 139.68/21.88 % given #500 (A,wt=108): 1004 s__subclass(s__Rattlesnake,s__CorpuscularObject) # tptp_name(kb_SUMO_39993) # sine_depth(2) # clausal_fof(1). [assumption].
% 139.68/21.88
% 139.68/21.88 % given #1000 (F,wt=11): 16448 -s__disjoint(s__SetOrClass,s__Vertebrate) | -s__instance(s__SetOrClass,s__Vertebrate). [factor(16442,b,c),unit_del(b,3509)].
% 139.68/21.88
% 139.68/21.88 % given #1500 (W,wt=8): 20540 -s__instance(s__USMilitaryRankO4,s__FlagOfficerRank). [resolve(19114,b,399,a)].
% 139.68/21.88
% 139.68/21.88 % given #2000 (F,wt=11): 21854 -s__disjoint(c2,s__Abstract) | -s__instance(s__Collection,c2). [resolve(1647,d,21032,a),unit_del(b,4410)].
% 139.68/21.88
% 139.68/21.88 % given #2500 (W,wt=11): 5085 -s__subclass(s__SetOrClass,c9) | s__instance(s__SetOrClass,c9). [factor(4559,a,c),unit_del(a,3509)].
% 139.68/21.88
% 139.68/21.88 % SZS status Theorem for theBenchmark
% 139.68/21.88
% 139.68/21.88 % Proof 1 at 16.64 (+ 2.14) seconds.
% 139.68/21.88 % Length of proof is 72.
% 139.68/21.88 % Level of proof is 13.
% 139.68/21.88 % Maximum clause weight is 120.000.
% 139.68/21.88 % Given clauses 2522.
% 139.68/21.88
% 139.68/21.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------