%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR084+1 : 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 : n015.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:15 AM UTC 2026
% Result : Theorem 183.02s 27.18s
% Output : CNFRefutation 183.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 17
% Syntax : Number of formulae : 77 ( 36 unt; 0 def)
% Number of atoms : 192 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 202 ( 87 ~; 84 |; 20 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-1 aty)
% Number of variables : 47 ( 2 sgn 19 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(local_1,axiom,
! [V_A] :
( s__instance(V_A,s__Object)
=> ( ( ~ ? [V_PART] :
( s__part(V_PART,V_A)
& s__instance(V_PART,s__SpinalColumn)
& s__instance(V_PART,s__Object) )
& s__instance(V_A,s__Animal) )
=> ~ s__instance(V_A,s__Vertebrate) ) ),
file('theBenchmark.p',local_1) ).
fof(local_2,axiom,
~ ? [V_SPINE] :
( s__part(V_SPINE,s__BananaSlug10_1)
& s__instance(V_SPINE,s__SpinalColumn)
& s__instance(V_SPINE,s__Object) ),
file('theBenchmark.p',local_2) ).
fof(local_4,axiom,
! [V_SUPER,V_SUB1,V_SUB2] :
( ( s__instance(V_SUB2,s__Class)
& s__instance(V_SUB1,s__Class)
& s__instance(V_SUPER,s__Class) )
=> ( s__partition_3(V_SUPER,V_SUB1,V_SUB2)
=> s__partition_3(V_SUPER,V_SUB2,V_SUB1) ) ),
file('theBenchmark.p',local_4) ).
fof(local_5,axiom,
! [V_SUPER,V_SUB1,V_SUB2,V_INST] :
( ( s__instance(V_SUB2,s__Class)
& s__instance(V_SUB1,s__Class)
& s__instance(V_SUPER,s__Class) )
=> ( ( ~ s__instance(V_INST,V_SUB1)
& s__instance(V_INST,V_SUPER)
& s__partition_3(V_SUPER,V_SUB1,V_SUB2) )
=> s__instance(V_INST,V_SUB2) ) ),
file('theBenchmark.p',local_5) ).
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_504,axiom,
! [V__CLASS] :
( s__instance(V__CLASS,s__SetOrClass)
=> ( s__instance(V__CLASS,s__Class)
<=> s__subclass(V__CLASS,s__Entity) ) ),
file('theBenchmark.p',kb_SUMO_504) ).
fof(prove_from_SUMO,conjecture,
s__instance(s__BananaSlug10_1,s__Invertebrate),
file('theBenchmark.p',prove_from_SUMO) ).
fof(prove_from_SUMO_neg,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(assume_negation,[status(cth)],[prove_from_SUMO]) ).
cnf(c_97,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_98,plain,
( s__instance(B,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_99,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_127,plain,
( ~ s__subclass(A,s__Entity)
| s__instance(A,s__Class)
| ~ s__instance(A,s__SetOrClass) ),
inference(clausify,[status(thm)],[kb_SUMO_504]) ).
fof(kb_SUMO_5981,axiom,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
file('theBenchmark.p',kb_SUMO_5981) ).
cnf(c_696,plain,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
inference(clausify,[status(thm)],[kb_SUMO_5981]) ).
fof(kb_SUMO_5997,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_5997) ).
cnf(c_697,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_5997]) ).
fof(kb_SUMO_5999,axiom,
s__subclass(s__Invertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_5999) ).
cnf(c_698,plain,
s__subclass(s__Invertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_5999]) ).
fof(kb_SUMOcache_5297,axiom,
s__subclass(s__Invertebrate,s__Object),
file('theBenchmark.p',kb_SUMOcache_5297) ).
cnf(c_763,plain,
s__subclass(s__Invertebrate,s__Object),
inference(clausify,[status(thm)],[kb_SUMOcache_5297]) ).
fof(kb_SUMOcache_5298,axiom,
s__subclass(s__Invertebrate,s__Entity),
file('theBenchmark.p',kb_SUMOcache_5298) ).
cnf(c_764,plain,
s__subclass(s__Invertebrate,s__Entity),
inference(clausify,[status(thm)],[kb_SUMOcache_5298]) ).
fof(kb_SUMOcache_6275,axiom,
s__subclass(s__Vertebrate,s__Entity),
file('theBenchmark.p',kb_SUMOcache_6275) ).
cnf(c_807,plain,
s__subclass(s__Vertebrate,s__Entity),
inference(clausify,[status(thm)],[kb_SUMOcache_6275]) ).
fof(kb_SUMOcache_6550,axiom,
s__subclass(s__Animal,s__Object),
file('theBenchmark.p',kb_SUMOcache_6550) ).
cnf(c_818,plain,
s__subclass(s__Animal,s__Object),
inference(clausify,[status(thm)],[kb_SUMOcache_6550]) ).
fof(kb_SUMOcache_6552,axiom,
s__subclass(s__Animal,s__Entity),
file('theBenchmark.p',kb_SUMOcache_6552) ).
cnf(c_820,plain,
s__subclass(s__Animal,s__Entity),
inference(clausify,[status(thm)],[kb_SUMOcache_6552]) ).
fof(nnf_12,plain,
! [V_A] :
( ~ s__instance(V_A,s__Vertebrate)
| ? [V_PART] :
( s__part(V_PART,V_A)
& s__instance(V_PART,s__SpinalColumn)
& s__instance(V_PART,s__Object) )
| ~ s__instance(V_A,s__Animal)
| ~ s__instance(V_A,s__Object) ),
inference(fof_nnf,[status(thm)],[local_1]) ).
fof(sk_local_1_sk,plain,
! [V_A] :
( ~ s__instance(V_A,s__Vertebrate)
| ( s__part(sK0(V_A),V_A)
& s__instance(sK0(V_A),s__SpinalColumn)
& s__instance(sK0(V_A),s__Object) )
| ~ s__instance(V_A,s__Animal)
| ~ s__instance(V_A,s__Object) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(V_PART,sK0(V_A))],[nnf_12]) ).
fof(sk_local_1,plain,
( ! [VAR_0] :
( ~ s__instance(VAR_0,s__Vertebrate)
| s__part(sK0(VAR_0),VAR_0)
| ~ s__instance(VAR_0,s__Animal)
| ~ s__instance(VAR_0,s__Object) )
& ! [VAR_0] :
( ~ s__instance(VAR_0,s__Vertebrate)
| s__instance(sK0(VAR_0),s__SpinalColumn)
| ~ s__instance(VAR_0,s__Animal)
| ~ s__instance(VAR_0,s__Object) )
& ! [VAR_0] :
( ~ s__instance(VAR_0,s__Vertebrate)
| s__instance(sK0(VAR_0),s__Object)
| ~ s__instance(VAR_0,s__Animal)
| ~ s__instance(VAR_0,s__Object) ) ),
inference(cnf_transformation,[status(thm)],[sk_local_1_sk]) ).
cnf(c_844,plain,
( ~ s__instance(A,s__Vertebrate)
| s__instance(sK0(A),s__Object)
| ~ s__instance(A,s__Animal)
| ~ s__instance(A,s__Object) ),
inference(split_conjunct,[status(thm)],[sk_local_1]) ).
cnf(c_845,plain,
( ~ s__instance(A,s__Vertebrate)
| s__instance(sK0(A),s__SpinalColumn)
| ~ s__instance(A,s__Animal)
| ~ s__instance(A,s__Object) ),
inference(split_conjunct,[status(thm)],[sk_local_1]) ).
cnf(c_846,plain,
( ~ s__instance(A,s__Vertebrate)
| s__part(sK0(A),A)
| ~ s__instance(A,s__Animal)
| ~ s__instance(A,s__Object) ),
inference(split_conjunct,[status(thm)],[sk_local_1]) ).
cnf(c_847,plain,
( ~ s__part(A,s__BananaSlug10_1)
| ~ s__instance(A,s__SpinalColumn)
| ~ s__instance(A,s__Object) ),
inference(clausify,[status(thm)],[local_2]) ).
cnf(c_848,plain,
( s__partition_3(A,C,B)
| ~ s__partition_3(A,B,C)
| ~ s__instance(C,s__Class)
| ~ s__instance(B,s__Class)
| ~ s__instance(A,s__Class) ),
inference(clausify,[status(thm)],[local_4]) ).
cnf(c_849,plain,
( s__instance(D,C)
| s__instance(D,B)
| ~ s__instance(D,A)
| ~ s__partition_3(A,B,C)
| ~ s__instance(C,s__Class)
| ~ s__instance(B,s__Class)
| ~ s__instance(A,s__Class) ),
inference(clausify,[status(thm)],[local_5]) ).
fof(local_6,axiom,
s__instance(s__BananaSlug10_1,s__Animal),
file('theBenchmark.p',local_6) ).
cnf(c_850,plain,
s__instance(s__BananaSlug10_1,s__Animal),
inference(clausify,[status(thm)],[local_6]) ).
cnf(c_851,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(clausify,[status(thm)],[prove_from_SUMO_neg]) ).
cnf(c_880,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolve,[status(thm)],[c_698,c_98]) ).
cnf(c_881,plain,
s__instance(s__Invertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_698,c_97]) ).
cnf(c_890,plain,
s__instance(s__Object,s__SetOrClass),
inference(resolve,[status(thm)],[c_763,c_98]) ).
cnf(c_68683,plain,
( s__instance(s__BananaSlug10_1,A)
| ~ s__subclass(s__Animal,A)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_850,c_99]) ).
cnf(c_902,plain,
( s__instance(s__BananaSlug10_1,A)
| ~ s__subclass(s__Animal,A)
| ~ s__instance(A,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_880,c_68683]) ).
cnf(c_68684,plain,
( ~ s__subclass(s__Animal,s__Entity)
| s__instance(s__Animal,s__Class) ),
inference(resolve,[status(thm)],[c_880,c_127]) ).
cnf(c_914,plain,
s__instance(s__Animal,s__Class),
inference(resolve,[status(thm)],[c_820,c_68684]) ).
cnf(c_68685,plain,
( ~ s__subclass(s__Invertebrate,s__Entity)
| s__instance(s__Invertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_881,c_127]) ).
cnf(c_937,plain,
s__instance(s__Invertebrate,s__Class),
inference(resolve,[status(thm)],[c_764,c_68685]) ).
cnf(c_68686,plain,
( s__instance(s__BananaSlug10_1,s__Object)
| ~ s__subclass(s__Animal,s__Object) ),
inference(resolve,[status(thm)],[c_902,c_890]) ).
cnf(c_1487,plain,
s__instance(s__BananaSlug10_1,s__Object),
inference(resolve,[status(thm)],[c_818,c_68686]) ).
cnf(c_1868,plain,
s__instance(s__Vertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_697,c_97]) ).
cnf(c_68687,plain,
( ~ s__subclass(s__Vertebrate,s__Entity)
| s__instance(s__Vertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_1868,c_127]) ).
cnf(c_1884,plain,
s__instance(s__Vertebrate,s__Class),
inference(resolve,[status(thm)],[c_807,c_68687]) ).
cnf(c_68688,plain,
( s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate)
| ~ s__instance(s__Invertebrate,s__Class)
| ~ s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Animal,s__Class) ),
inference(resolve,[status(thm)],[c_848,c_696]) ).
cnf(c_68689,plain,
( s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate)
| ~ s__instance(s__Invertebrate,s__Class)
| ~ s__instance(s__Vertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_914,c_68688]) ).
cnf(c_68690,plain,
( s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_1884,c_68689]) ).
cnf(c_5449,plain,
s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate),
inference(resolve,[status(thm)],[c_937,c_68690]) ).
cnf(c_68691,plain,
( s__instance(A,s__Vertebrate)
| s__instance(A,s__Invertebrate)
| ~ s__instance(A,s__Animal)
| ~ s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Invertebrate,s__Class)
| ~ s__instance(s__Animal,s__Class) ),
inference(resolve,[status(thm)],[c_849,c_5449]) ).
cnf(c_68692,plain,
( s__instance(A,s__Vertebrate)
| s__instance(A,s__Invertebrate)
| ~ s__instance(A,s__Animal)
| ~ s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_914,c_68691]) ).
cnf(c_68693,plain,
( s__instance(A,s__Vertebrate)
| s__instance(A,s__Invertebrate)
| ~ s__instance(A,s__Animal)
| ~ s__instance(s__Vertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_937,c_68692]) ).
cnf(c_5462,plain,
( s__instance(A,s__Vertebrate)
| s__instance(A,s__Invertebrate)
| ~ s__instance(A,s__Animal) ),
inference(resolve,[status(thm)],[c_1884,c_68693]) ).
cnf(c_68694,plain,
( s__instance(s__BananaSlug10_1,s__Vertebrate)
| s__instance(s__BananaSlug10_1,s__Invertebrate) ),
inference(resolve,[status(thm)],[c_5462,c_850]) ).
cnf(c_68661,negated_conjecture,
s__instance(s__BananaSlug10_1,s__Vertebrate),
inference(resolve,[status(thm)],[c_851,c_68694]) ).
cnf(c_68695,plain,
( s__part(sK0(s__BananaSlug10_1),s__BananaSlug10_1)
| ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Object) ),
inference(resolve,[status(thm)],[c_68661,c_846]) ).
cnf(c_68696,plain,
( s__part(sK0(s__BananaSlug10_1),s__BananaSlug10_1)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1487,c_68695]) ).
cnf(c_68675,plain,
s__part(sK0(s__BananaSlug10_1),s__BananaSlug10_1),
inference(resolve,[status(thm)],[c_850,c_68696]) ).
cnf(c_68697,plain,
( s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Object) ),
inference(resolve,[status(thm)],[c_68661,c_845]) ).
cnf(c_68698,plain,
( s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1487,c_68697]) ).
cnf(c_68676,plain,
s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn),
inference(resolve,[status(thm)],[c_850,c_68698]) ).
cnf(c_68699,plain,
( s__instance(sK0(s__BananaSlug10_1),s__Object)
| ~ s__instance(s__BananaSlug10_1,s__Animal)
| ~ s__instance(s__BananaSlug10_1,s__Object) ),
inference(resolve,[status(thm)],[c_68661,c_844]) ).
cnf(c_68700,plain,
( s__instance(sK0(s__BananaSlug10_1),s__Object)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1487,c_68699]) ).
cnf(c_68677,plain,
s__instance(sK0(s__BananaSlug10_1),s__Object),
inference(resolve,[status(thm)],[c_850,c_68700]) ).
cnf(c_68701,plain,
( ~ s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(sK0(s__BananaSlug10_1),s__Object) ),
inference(resolve,[status(thm)],[c_68675,c_847]) ).
cnf(c_68702,plain,
~ s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn),
inference(resolve,[status(thm)],[c_68677,c_68701]) ).
cnf(c_68682,plain,
$false,
inference(resolve,[status(thm)],[c_68676,c_68702]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR084+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.56 % Computer : n015.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Sun Sep 27 00:48:45 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.57 % Process 1120917 was started by sandbox on n015,
% 0.10/0.57 % Sun Sep 27 00:48:45 2026
% 0.10/0.57 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 183.02/27.18
% 183.02/27.18 % SInE (scan): 634 to sos (tol 1.5x), 73 to usable (tol 2.0x), 14087 zapped, of 14794 axioms (depth 3).
% 183.02/27.18
% 183.02/27.18 % From the command line: assign(max_seconds, 300).
% 183.02/27.18
% 183.02/27.18 % given #500 (W,wt=6): 3059 s__Arachnid != s__Organism | s__instance(s__BananaSlug10_1,s__Arachnid). [resolve(1506,b,896,a),flip(a)].
% 183.02/27.18
% 183.02/27.18 % given #1000 (W,wt=6): 4938 s__Human != s__SetOrClass | s__instance(s__Vertebrate,s__Human). [resolve(2006,b,4470,a),flip(a)].
% 183.02/27.18
% 183.02/27.18 % given #1500 (T,wt=6): 9307 s__Animal != s__SetOrClass | s__instance(s__Organism,s__Animal). [resolve(916,d,888,a),unit_del(b,1989)].
% 183.02/27.18
% 183.02/27.18 % given #2000 (W,wt=6): 16278 -s__subclass(s__SetOrClass,s__Physical) | s__instance(s__Physical,s__Physical). [resolve(993,c,883,a),unit_del(a,1989)].
% 183.02/27.18
% 183.02/27.18 % given #2500 (F,wt=9): 19984 -s__instance(A,s__SetOrClass) | -s__subclass(s__Agent,A) | -s__subclass(A,s__Mollusk). [resolve(1048,a,3189,a),unit_del(d,9078)].
% 183.02/27.18
% 183.02/27.18 % given #3000 (W,wt=7): 14229 s__instance(s__ListOrderFn(s__ListFn_2(s__Myriapod,s__Physical),do_2),s__SetOrClass). [resolve(978,a,892,a),unit_del(a,765)].
% 183.02/27.18
% 183.02/27.18 % given #3500 (F,wt=14): 9001 -s__subclass(s__Animal,s__ListOrderFn(s__ListFn_2(s__Mammal,s__Animal),do_1)) | -s__subclass(s__ListOrderFn(s__ListFn_2(s__Mammal,s__Animal),do_1),s__Mollusk). [resolve(7605,a,6047,a)].
% 183.02/27.18
% 183.02/27.18 % given #4000 (T,wt=9): 2140 -s__instance(A,s__SetOrClass) | -s__subclass(s__SetOrClass,A) | s__instance(s__OrganicObject,A). [back_unit_del(1014),unit_del(b,1989)].
% 183.02/27.18
% 183.02/27.18 % SZS status Theorem for theBenchmark
% 183.02/27.18
% 183.02/27.18 % Proof 1 at 19.87 (+ 6.20) seconds.
% 183.02/27.18 % Length of proof is 44.
% 183.02/27.18 % Level of proof is 8.
% 183.02/27.18 % Maximum clause weight is 122.000.
% 183.02/27.18 % Given clauses 4461.
% 183.02/27.18
% 183.02/27.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------