%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR084+2 : 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 : n005.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 51.62s 8.17s
% Output : CNFRefutation 51.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 21
% Syntax : Number of formulae : 95 ( 48 unt; 0 def)
% Number of atoms : 222 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 226 ( 99 ~; 96 |; 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 : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 54 ( 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_608,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_608) ).
fof(prove_from_SUMO_MILO,conjecture,
s__instance(s__BananaSlug10_1,s__Invertebrate),
file('theBenchmark.p',prove_from_SUMO_MILO) ).
fof(prove_from_SUMO_MILO_neg,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(assume_negation,[status(cth)],[prove_from_SUMO_MILO]) ).
cnf(c_138,plain,
( s__instance(A,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_139,plain,
( s__instance(B,s__SetOrClass)
| ~ s__subclass(A,B) ),
inference(clausify,[status(thm)],[kb_SUMO_26]) ).
cnf(c_140,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_160,plain,
( ~ s__subclass(A,s__Entity)
| s__instance(A,s__Class)
| ~ s__instance(A,s__SetOrClass) ),
inference(clausify,[status(thm)],[kb_SUMO_608]) ).
fof(kb_SUMO_827,axiom,
s__subclass(s__Agent,s__Object),
file('theBenchmark.p',kb_SUMO_827) ).
cnf(c_782,plain,
s__subclass(s__Agent,s__Object),
inference(clausify,[status(thm)],[kb_SUMO_827]) ).
fof(kb_SUMO_7129,axiom,
s__subclass(s__Organism,s__Agent),
file('theBenchmark.p',kb_SUMO_7129) ).
cnf(c_792,plain,
s__subclass(s__Organism,s__Agent),
inference(clausify,[status(thm)],[kb_SUMO_7129]) ).
fof(kb_SUMO_7174,axiom,
s__subclass(s__Animal,s__Organism),
file('theBenchmark.p',kb_SUMO_7174) ).
cnf(c_793,plain,
s__subclass(s__Animal,s__Organism),
inference(clausify,[status(thm)],[kb_SUMO_7174]) ).
fof(kb_SUMO_7175,axiom,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
file('theBenchmark.p',kb_SUMO_7175) ).
cnf(c_794,plain,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
inference(clausify,[status(thm)],[kb_SUMO_7175]) ).
fof(kb_SUMO_7191,axiom,
s__subclass(s__Vertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_7191) ).
cnf(c_795,plain,
s__subclass(s__Vertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_7191]) ).
fof(kb_SUMO_7193,axiom,
s__subclass(s__Invertebrate,s__Animal),
file('theBenchmark.p',kb_SUMO_7193) ).
cnf(c_796,plain,
s__subclass(s__Invertebrate,s__Animal),
inference(clausify,[status(thm)],[kb_SUMO_7193]) ).
fof(kb_SUMO_8537,axiom,
s__subclass(s__Vertebrate,s__Entity),
file('theBenchmark.p',kb_SUMO_8537) ).
cnf(c_836,plain,
s__subclass(s__Vertebrate,s__Entity),
inference(clausify,[status(thm)],[kb_SUMO_8537]) ).
fof(kb_SUMO_12505,axiom,
s__subclass(s__Animal,s__Entity),
file('theBenchmark.p',kb_SUMO_12505) ).
cnf(c_875,plain,
s__subclass(s__Animal,s__Entity),
inference(clausify,[status(thm)],[kb_SUMO_12505]) ).
fof(kb_SUMO_19052,axiom,
s__subclass(s__Invertebrate,s__Agent),
file('theBenchmark.p',kb_SUMO_19052) ).
cnf(c_922,plain,
s__subclass(s__Invertebrate,s__Agent),
inference(clausify,[status(thm)],[kb_SUMO_19052]) ).
fof(kb_SUMO_19054,axiom,
s__subclass(s__Invertebrate,s__Organism),
file('theBenchmark.p',kb_SUMO_19054) ).
cnf(c_924,plain,
s__subclass(s__Invertebrate,s__Organism),
inference(clausify,[status(thm)],[kb_SUMO_19054]) ).
fof(kb_SUMO_19055,axiom,
s__subclass(s__Invertebrate,s__Object),
file('theBenchmark.p',kb_SUMO_19055) ).
cnf(c_925,plain,
s__subclass(s__Invertebrate,s__Object),
inference(clausify,[status(thm)],[kb_SUMO_19055]) ).
fof(kb_SUMO_19057,axiom,
s__subclass(s__Invertebrate,s__Entity),
file('theBenchmark.p',kb_SUMO_19057) ).
cnf(c_927,plain,
s__subclass(s__Invertebrate,s__Entity),
inference(clausify,[status(thm)],[kb_SUMO_19057]) ).
fof(nnf_10,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_10]) ).
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_931,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_932,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_933,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_934,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_935,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_936,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_937,plain,
s__instance(s__BananaSlug10_1,s__Animal),
inference(clausify,[status(thm)],[local_6]) ).
cnf(c_938,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
inference(clausify,[status(thm)],[prove_from_SUMO_MILO_neg]) ).
cnf(c_955,plain,
s__instance(s__Animal,s__SetOrClass),
inference(resolve,[status(thm)],[c_796,c_139]) ).
cnf(c_956,plain,
s__instance(s__Invertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_796,c_138]) ).
cnf(c_1043,plain,
s__instance(s__Agent,s__SetOrClass),
inference(resolve,[status(thm)],[c_922,c_139]) ).
cnf(c_1071,plain,
s__instance(s__Organism,s__SetOrClass),
inference(resolve,[status(thm)],[c_924,c_139]) ).
cnf(c_1085,plain,
s__instance(s__Object,s__SetOrClass),
inference(resolve,[status(thm)],[c_925,c_139]) ).
cnf(c_21616,plain,
( s__instance(s__Invertebrate,s__Class)
| ~ s__instance(s__Invertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_927,c_160]) ).
cnf(c_1111,plain,
s__instance(s__Invertebrate,s__Class),
inference(resolve,[status(thm)],[c_956,c_21616]) ).
cnf(c_21617,plain,
( s__instance(A,s__Object)
| ~ s__instance(A,s__Agent)
| ~ s__instance(s__Agent,s__SetOrClass)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_782,c_140]) ).
cnf(c_21618,plain,
( s__instance(A,s__Object)
| ~ s__instance(A,s__Agent)
| ~ s__instance(s__Agent,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1085,c_21617]) ).
cnf(c_1317,plain,
( s__instance(A,s__Object)
| ~ s__instance(A,s__Agent) ),
inference(resolve,[status(thm)],[c_1043,c_21618]) ).
cnf(c_21619,plain,
( s__instance(A,s__Agent)
| ~ s__instance(A,s__Organism)
| ~ s__instance(s__Organism,s__SetOrClass)
| ~ s__instance(s__Agent,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_792,c_140]) ).
cnf(c_21620,plain,
( s__instance(A,s__Agent)
| ~ s__instance(A,s__Organism)
| ~ s__instance(s__Organism,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1043,c_21619]) ).
cnf(c_1819,plain,
( s__instance(A,s__Agent)
| ~ s__instance(A,s__Organism) ),
inference(resolve,[status(thm)],[c_1071,c_21620]) ).
cnf(c_21621,plain,
( s__instance(A,s__Organism)
| ~ s__instance(A,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass)
| ~ s__instance(s__Organism,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_793,c_140]) ).
cnf(c_21622,plain,
( s__instance(A,s__Organism)
| ~ s__instance(A,s__Animal)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_1071,c_21621]) ).
cnf(c_1865,plain,
( s__instance(A,s__Organism)
| ~ s__instance(A,s__Animal) ),
inference(resolve,[status(thm)],[c_955,c_21622]) ).
cnf(c_1866,plain,
s__instance(s__BananaSlug10_1,s__Organism),
inference(resolve,[status(thm)],[c_1865,c_937]) ).
cnf(c_1867,plain,
s__instance(s__BananaSlug10_1,s__Agent),
inference(resolve,[status(thm)],[c_1866,c_1819]) ).
cnf(c_1872,plain,
s__instance(s__BananaSlug10_1,s__Object),
inference(resolve,[status(thm)],[c_1867,c_1317]) ).
cnf(c_1893,plain,
s__instance(s__Vertebrate,s__SetOrClass),
inference(resolve,[status(thm)],[c_795,c_138]) ).
cnf(c_21623,plain,
( s__instance(s__Vertebrate,s__Class)
| ~ s__instance(s__Vertebrate,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_836,c_160]) ).
cnf(c_3698,plain,
s__instance(s__Vertebrate,s__Class),
inference(resolve,[status(thm)],[c_1893,c_21623]) ).
cnf(c_21624,plain,
( s__instance(s__Animal,s__Class)
| ~ s__instance(s__Animal,s__SetOrClass) ),
inference(resolve,[status(thm)],[c_875,c_160]) ).
cnf(c_5274,plain,
s__instance(s__Animal,s__Class),
inference(resolve,[status(thm)],[c_955,c_21624]) ).
cnf(c_21625,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_935,c_794]) ).
cnf(c_21626,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_5274,c_21625]) ).
cnf(c_21627,plain,
( s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate)
| ~ s__instance(s__Invertebrate,s__Class) ),
inference(resolve,[status(thm)],[c_3698,c_21626]) ).
cnf(c_7315,plain,
s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate),
inference(resolve,[status(thm)],[c_1111,c_21627]) ).
cnf(c_21628,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_936,c_7315]) ).
cnf(c_21629,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_5274,c_21628]) ).
cnf(c_21630,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_1111,c_21629]) ).
cnf(c_7332,plain,
( s__instance(A,s__Vertebrate)
| s__instance(A,s__Invertebrate)
| ~ s__instance(A,s__Animal) ),
inference(resolve,[status(thm)],[c_3698,c_21630]) ).
cnf(c_21631,plain,
( s__instance(s__BananaSlug10_1,s__Vertebrate)
| s__instance(s__BananaSlug10_1,s__Invertebrate) ),
inference(resolve,[status(thm)],[c_7332,c_937]) ).
cnf(c_21601,negated_conjecture,
s__instance(s__BananaSlug10_1,s__Vertebrate),
inference(resolve,[status(thm)],[c_938,c_21631]) ).
cnf(c_21632,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_21601,c_933]) ).
cnf(c_21633,plain,
( s__part(sK0(s__BananaSlug10_1),s__BananaSlug10_1)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1872,c_21632]) ).
cnf(c_21607,plain,
s__part(sK0(s__BananaSlug10_1),s__BananaSlug10_1),
inference(resolve,[status(thm)],[c_937,c_21633]) ).
cnf(c_21634,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_21601,c_932]) ).
cnf(c_21635,plain,
( s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1872,c_21634]) ).
cnf(c_21608,plain,
s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn),
inference(resolve,[status(thm)],[c_937,c_21635]) ).
cnf(c_21636,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_21601,c_931]) ).
cnf(c_21637,plain,
( s__instance(sK0(s__BananaSlug10_1),s__Object)
| ~ s__instance(s__BananaSlug10_1,s__Animal) ),
inference(resolve,[status(thm)],[c_1872,c_21636]) ).
cnf(c_21609,plain,
s__instance(sK0(s__BananaSlug10_1),s__Object),
inference(resolve,[status(thm)],[c_937,c_21637]) ).
cnf(c_21638,plain,
( ~ s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(sK0(s__BananaSlug10_1),s__Object) ),
inference(resolve,[status(thm)],[c_21607,c_934]) ).
cnf(c_21639,plain,
~ s__instance(sK0(s__BananaSlug10_1),s__SpinalColumn),
inference(resolve,[status(thm)],[c_21609,c_21638]) ).
cnf(c_21615,plain,
$false,
inference(resolve,[status(thm)],[c_21608,c_21639]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR084+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 00:45:32 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.39 % Process 3460944 was started by sandbox2 on n005,
% 0.09/0.39 % Sun Sep 27 00:45:32 2026
% 0.09/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 51.62/8.17
% 51.62/8.17 % SInE (scan): 646 to sos (tol 1.5x), 77 to usable (tol 2.0x), 37265 zapped, of 37988 axioms (depth 3).
% 51.62/8.17
% 51.62/8.17 % From the command line: assign(max_seconds, 300).
% 51.62/8.17
% 51.62/8.17 % given #500 (W,wt=7): 3564 s__instance(s__ListOrderFn(s__ListFn_2(s__Vertebrate,s__Agent),do_2),s__SetOrClass). [resolve(831,a,227,c),unit_del(a,1043),unit_del(b,1893)].
% 51.62/8.17
% 51.62/8.17 % given #1000 (A,wt=103): 917 s__subclass(s__QueenInsect,s__Entity) # tptp_name(kb_SUMO_18429) # sine_depth(2) # clausal_fof(1). [assumption].
% 51.62/8.17
% 51.62/8.17 % given #1500 (A,wt=17): 1352 A != B | -s__instance(B,s__ListOrderFn(s__ListFn_2(s__Invertebrate,s__Animal),do_2)) | s__instance(A,s__ListOrderFn(s__ListFn_2(s__Invertebrate,s__Animal),do_2)). [resolve(963,a,146,b)].
% 51.62/8.17
% 51.62/8.17 % given #2000 (T,wt=6): 20938 s__QueenInsect != s__SetOrClass | s__instance(s__Entity,s__QueenInsect). [resolve(3396,b,2542,a),flip(a)].
% 51.62/8.17
% 51.62/8.17 % given #2500 (W,wt=9): 5658 -s__instance(A,s__SetOrClass) | -s__subclass(s__OrganicThing,A) | s__subclass(s__Human,A). [resolve(882,a,215,d),unit_del(b,1057),unit_del(c,5622)].
% 51.62/8.17
% 51.62/8.17 % SZS status Theorem for theBenchmark
% 51.62/8.17
% 51.62/8.17 % Proof 1 at 5.79 (+ 1.48) seconds.
% 51.62/8.17 % Length of proof is 54.
% 51.62/8.17 % Level of proof is 8.
% 51.62/8.17 % Maximum clause weight is 122.000.
% 51.62/8.17 % Given clauses 2638.
% 51.62/8.17
% 51.62/8.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------