%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR109+2 : 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 : n002.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 47.92s 7.62s
% Output : CNFRefutation 47.92s
% 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_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_768,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_770,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_7294,axiom,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('theBenchmark.p',kb_SUMO_7294) ).
cnf(c_817,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
inference(clausify,[status(thm)],[kb_SUMO_7294]) ).
fof(kb_SUMO_9340,axiom,
s__subclass(s__Reptile,s__Animal),
file('theBenchmark.p',kb_SUMO_9340) ).
cnf(c_884,plain,
s__subclass(s__Reptile,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_9340]) ).
fof(nnf_19,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_19]) ).
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_990,plain,
( s__instance(sK0,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_991,plain,
s__instance(sK0,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_990]) ).
cnf(c_992,plain,
( s__instance(sK1,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_993,plain,
s__instance(sK1,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_992]) ).
cnf(c_994,plain,
( s__instance(sK2,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_995,plain,
s__instance(sK2,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_994]) ).
cnf(c_996,plain,
( s__instance(sK3,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_997,plain,
s__instance(sK3,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_996]) ).
cnf(c_998,plain,
( s__instance(sK4,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_999,plain,
s__instance(sK4,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_998]) ).
cnf(c_1000,plain,
( s__instance(sK5,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1001,plain,
s__instance(sK5,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_1000]) ).
cnf(c_1002,plain,
( s__instance(sK6,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1003,plain,
s__instance(sK6,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_1002]) ).
cnf(c_1004,plain,
( s__instance(sK7,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1005,plain,
s__instance(sK7,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_1004]) ).
cnf(c_1006,plain,
( s__instance(sK8,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1007,plain,
s__instance(sK8,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_1006]) ).
cnf(c_1008,plain,
( s__instance(sK9,s__SetOrClass)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1009,plain,
s__instance(sK9,s__SetOrClass),
inference(resolve,[status(thm)],[c_884,c_1008]) ).
cnf(c_1010,plain,
( s__subclass(sK0,sK1)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1011,plain,
s__subclass(sK0,sK1),
inference(resolve,[status(thm)],[c_884,c_1010]) ).
cnf(c_1012,plain,
( s__subclass(sK1,sK2)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1013,plain,
s__subclass(sK1,sK2),
inference(resolve,[status(thm)],[c_884,c_1012]) ).
cnf(c_1014,plain,
( s__subclass(sK2,sK3)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1015,plain,
s__subclass(sK2,sK3),
inference(resolve,[status(thm)],[c_884,c_1014]) ).
cnf(c_1016,plain,
( s__subclass(sK3,sK4)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1017,plain,
s__subclass(sK3,sK4),
inference(resolve,[status(thm)],[c_884,c_1016]) ).
cnf(c_1018,plain,
( s__subclass(sK4,sK5)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1019,plain,
s__subclass(sK4,sK5),
inference(resolve,[status(thm)],[c_884,c_1018]) ).
cnf(c_1020,plain,
( s__subclass(sK5,sK6)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1021,plain,
s__subclass(sK5,sK6),
inference(resolve,[status(thm)],[c_884,c_1020]) ).
cnf(c_1022,plain,
( s__subclass(sK6,sK7)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1023,plain,
s__subclass(sK6,sK7),
inference(resolve,[status(thm)],[c_884,c_1022]) ).
cnf(c_1024,plain,
( s__subclass(sK7,sK8)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1025,plain,
s__subclass(sK7,sK8),
inference(resolve,[status(thm)],[c_884,c_1024]) ).
cnf(c_1026,plain,
( s__subclass(sK8,sK9)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1027,plain,
s__subclass(sK8,sK9),
inference(resolve,[status(thm)],[c_884,c_1026]) ).
cnf(c_1028,plain,
( s__subclass(sK9,s__Reptile)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1029,plain,
s__subclass(sK9,s__Reptile),
inference(resolve,[status(thm)],[c_884,c_1028]) ).
cnf(c_1030,plain,
( s__instance(s__Creature50_1,sK0)
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(split_conjunct,[status(thm)],[sk_local_2]) ).
cnf(c_1031,plain,
s__instance(s__Creature50_1,sK0),
inference(resolve,[status(thm)],[c_884,c_1030]) ).
cnf(c_1032,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(clausify,[status(thm)],[prove_from_SUMO_MILO_neg]) ).
cnf(c_1141,plain,
s__instance(s__Reptile,s__SetOrClass),
inference(resolve,[status(thm)],[c_817,c_768]) ).
cnf(c_14744,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1011,c_770]) ).
cnf(c_14745,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0)
| ~ s__instance(sK0,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_993,c_14744]) ).
cnf(c_2066,plain,
( s__instance(A,sK1)
| ~ s__instance(A,sK0) ),
inference(resolve,[status(thm)],[c_991,c_14745]) ).
cnf(c_14746,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1013,c_770]) ).
cnf(c_14747,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1)
| ~ s__instance(sK1,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_995,c_14746]) ).
cnf(c_2069,plain,
( s__instance(A,sK2)
| ~ s__instance(A,sK1) ),
inference(resolve,[status(thm)],[c_993,c_14747]) ).
cnf(c_14748,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1015,c_770]) ).
cnf(c_14749,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2)
| ~ s__instance(sK2,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_997,c_14748]) ).
cnf(c_2072,plain,
( s__instance(A,sK3)
| ~ s__instance(A,sK2) ),
inference(resolve,[status(thm)],[c_995,c_14749]) ).
cnf(c_14750,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1017,c_770]) ).
cnf(c_14751,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3)
| ~ s__instance(sK3,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_999,c_14750]) ).
cnf(c_2133,plain,
( s__instance(A,sK4)
| ~ s__instance(A,sK3) ),
inference(resolve,[status(thm)],[c_997,c_14751]) ).
cnf(c_14752,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1019,c_770]) ).
cnf(c_14753,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4)
| ~ s__instance(sK4,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1001,c_14752]) ).
cnf(c_2136,plain,
( s__instance(A,sK5)
| ~ s__instance(A,sK4) ),
inference(resolve,[status(thm)],[c_999,c_14753]) ).
cnf(c_14754,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1021,c_770]) ).
cnf(c_14755,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5)
| ~ s__instance(sK5,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1003,c_14754]) ).
cnf(c_2139,plain,
( s__instance(A,sK6)
| ~ s__instance(A,sK5) ),
inference(resolve,[status(thm)],[c_1001,c_14755]) ).
cnf(c_14756,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1023,c_770]) ).
cnf(c_14757,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6)
| ~ s__instance(sK6,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1005,c_14756]) ).
cnf(c_2142,plain,
( s__instance(A,sK7)
| ~ s__instance(A,sK6) ),
inference(resolve,[status(thm)],[c_1003,c_14757]) ).
cnf(c_14758,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1025,c_770]) ).
cnf(c_14759,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7)
| ~ s__instance(sK7,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1007,c_14758]) ).
cnf(c_2145,plain,
( s__instance(A,sK8)
| ~ s__instance(A,sK7) ),
inference(resolve,[status(thm)],[c_1005,c_14759]) ).
cnf(c_14760,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1027,c_770]) ).
cnf(c_14761,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8)
| ~ s__instance(sK8,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1009,c_14760]) ).
cnf(c_2148,plain,
( s__instance(A,sK9)
| ~ s__instance(A,sK8) ),
inference(resolve,[status(thm)],[c_1007,c_14761]) ).
cnf(c_14762,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_1029,c_770]) ).
cnf(c_14763,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9)
| ~ s__instance(sK9,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1141,c_14762]) ).
cnf(c_2158,plain,
( s__instance(A,s__Reptile)
| ~ s__instance(A,sK9) ),
inference(resolve,[status(thm)],[c_1009,c_14763]) ).
cnf(c_14560,plain,
s__instance(s__Creature50_1,sK1),
inference(resolve,[status(thm)],[c_2066,c_1031]) ).
cnf(c_14582,plain,
s__instance(s__Creature50_1,sK2),
inference(resolve,[status(thm)],[c_2069,c_14560]) ).
cnf(c_14594,plain,
s__instance(s__Creature50_1,sK3),
inference(resolve,[status(thm)],[c_2072,c_14582]) ).
cnf(c_14641,plain,
s__instance(s__Creature50_1,sK4),
inference(resolve,[status(thm)],[c_2133,c_14594]) ).
cnf(c_14653,plain,
s__instance(s__Creature50_1,sK5),
inference(resolve,[status(thm)],[c_2136,c_14641]) ).
cnf(c_14675,plain,
s__instance(s__Creature50_1,sK6),
inference(resolve,[status(thm)],[c_2139,c_14653]) ).
cnf(c_14687,plain,
s__instance(s__Creature50_1,sK7),
inference(resolve,[status(thm)],[c_2142,c_14675]) ).
cnf(c_14709,plain,
s__instance(s__Creature50_1,sK8),
inference(resolve,[status(thm)],[c_2145,c_14687]) ).
cnf(c_14721,plain,
s__instance(s__Creature50_1,sK9),
inference(resolve,[status(thm)],[c_2148,c_14709]) ).
cnf(c_14764,plain,
s__instance(s__Creature50_1,s__Reptile),
inference(resolve,[status(thm)],[c_2158,c_14721]) ).
cnf(c_14743,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1032,c_14764]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+2 : 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.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 01:02:23 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3028434 was started by sandbox on n002,
% 0.09/0.36 % Sun Sep 27 01:02:23 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 47.92/7.62
% 47.92/7.62 % SInE (scan): 721 to sos (tol 1.5x), 72 to usable (tol 2.0x), 37190 zapped, of 37983 axioms (depth 3).
% 47.92/7.62
% 47.92/7.62 % From the command line: assign(max_seconds, 300).
% 47.92/7.62
% 47.92/7.62 % given #500 (F,wt=11): 3561 -s__disjoint(s__SetOrClass,s__PrepositionalPhrase) | -s__instance(s__SetOrClass,s__PrepositionalPhrase). [factor(3556,b,c),unit_del(b,1121)].
% 47.92/7.62
% 47.92/7.62 % given #1000 (T,wt=11): 1358 -s__instance(A,s__Toad) | s__instance(A,s__Agent). [resolve(770,c,606,a),unit_del(a,1167),unit_del(b,1077)].
% 47.92/7.62
% 47.92/7.62 % given #1500 (F,wt=11): 14210 -s__disjoint(s__Animal,s__CognitiveAgent) | -s__instance(s__Creature50_1,s__CognitiveAgent). [resolve(1640,b,1172,a)].
% 47.92/7.62
% 47.92/7.62 % SZS status Theorem for theBenchmark
% 47.92/7.62
% 47.92/7.62 % Proof 1 at 5.78 (+ 0.65) seconds.
% 47.92/7.62 % Length of proof is 72.
% 47.92/7.62 % Level of proof is 13.
% 47.92/7.62 % Maximum clause weight is 120.000.
% 47.92/7.62 % Given clauses 1757.
% 47.92/7.62
% 47.92/7.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------