%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR093+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 : Tue Sep 29 09:42:54 AM UTC 2026
% Result : Theorem 18.39s 6.05s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 38
% Syntax : Number of formulae : 162 ( 98 unt; 2 def)
% Number of atoms : 298 ( 0 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 259 ( 123 ~; 120 |; 9 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 65 ( 0 sgn 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26635) ).
fof(f26457,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_26636) ).
fof(f28242,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__Organism)
& s__instance(X1,s__Organism)
& s__instance(X0,s__Organism) )
=> ( ( s__ancestor(X0,X1)
& s__ancestor(X1,X2) )
=> s__ancestor(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_28424) ).
fof(f124477,axiom,
s__subclass(s__Human,s__Organism),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',kb_SUMO_68891) ).
fof(f145102,axiom,
s__instance(s__Human23_1,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(f145103,axiom,
s__instance(s__Human23_2,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(f145104,axiom,
s__instance(s__Human23_3,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(f145105,axiom,
s__instance(s__Human23_4,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(f145106,axiom,
s__instance(s__Human23_5,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(f145107,axiom,
s__instance(s__Human23_6,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_6) ).
fof(f145108,axiom,
s__instance(s__Human23_7,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_7) ).
fof(f145109,axiom,
s__instance(s__Human23_8,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_8) ).
fof(f145110,axiom,
s__instance(s__Human23_9,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_9) ).
fof(f145111,axiom,
s__instance(s__Human23_10,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_10) ).
fof(f145112,axiom,
s__instance(s__Human23_11,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_11) ).
fof(f145113,axiom,
s__instance(s__Human23_12,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_12) ).
fof(f145114,axiom,
s__instance(s__Human23_13,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_13) ).
fof(f145115,axiom,
s__instance(s__Human23_14,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_14) ).
fof(f145116,axiom,
s__instance(s__Human23_15,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_15) ).
fof(f145117,axiom,
s__instance(s__Human23_16,s__Human),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_16) ).
fof(f145118,axiom,
s__ancestor(s__Human23_1,s__Human23_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_17) ).
fof(f145119,axiom,
s__ancestor(s__Human23_2,s__Human23_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_18) ).
fof(f145120,axiom,
s__ancestor(s__Human23_3,s__Human23_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_19) ).
fof(f145121,axiom,
s__ancestor(s__Human23_4,s__Human23_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_20) ).
fof(f145122,axiom,
s__ancestor(s__Human23_5,s__Human23_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_21) ).
fof(f145123,axiom,
s__ancestor(s__Human23_6,s__Human23_7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_22) ).
fof(f145124,axiom,
s__ancestor(s__Human23_7,s__Human23_8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_23) ).
fof(f145125,axiom,
s__ancestor(s__Human23_8,s__Human23_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_24) ).
fof(f145126,axiom,
s__ancestor(s__Human23_9,s__Human23_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_25) ).
fof(f145127,axiom,
s__ancestor(s__Human23_10,s__Human23_11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_26) ).
fof(f145128,axiom,
s__ancestor(s__Human23_11,s__Human23_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_27) ).
fof(f145129,axiom,
s__ancestor(s__Human23_12,s__Human23_13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_28) ).
fof(f145130,axiom,
s__ancestor(s__Human23_13,s__Human23_14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_29) ).
fof(f145131,axiom,
s__ancestor(s__Human23_14,s__Human23_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_30) ).
fof(f145132,axiom,
s__ancestor(s__Human23_14,s__Human23_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_31) ).
fof(f145133,conjecture,
( s__ancestor(s__Human23_1,s__Human23_15)
& s__ancestor(s__Human23_1,s__Human23_16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145134,negated_conjecture,
~ ( s__ancestor(s__Human23_1,s__Human23_15)
& s__ancestor(s__Human23_1,s__Human23_16) ),
inference(negated_conjecture,[status(cth)],[f145133]) ).
fof(f145135,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(ennf_transformation,[],[f145134]) ).
fof(f145140,plain,
! [X0,X1,X2] :
( s__ancestor(X0,X2)
| ~ s__ancestor(X0,X1)
| ~ s__ancestor(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(ennf_transformation,[],[f28242]) ).
fof(f145141,plain,
! [X0,X1,X2] :
( s__ancestor(X0,X2)
| ~ s__ancestor(X0,X1)
| ~ s__ancestor(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism) ),
inference(flattening,[],[f145140]) ).
fof(f145208,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f26457]) ).
fof(f145209,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f145208]) ).
fof(f145210,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f145306,plain,
s__instance(s__Human23_1,s__Human),
inference(cnf_transformation,[],[f145102]) ).
fof(f145307,plain,
s__instance(s__Human23_2,s__Human),
inference(cnf_transformation,[],[f145103]) ).
fof(f145308,plain,
s__instance(s__Human23_3,s__Human),
inference(cnf_transformation,[],[f145104]) ).
fof(f145309,plain,
s__instance(s__Human23_4,s__Human),
inference(cnf_transformation,[],[f145105]) ).
fof(f145310,plain,
s__instance(s__Human23_5,s__Human),
inference(cnf_transformation,[],[f145106]) ).
fof(f145311,plain,
s__instance(s__Human23_6,s__Human),
inference(cnf_transformation,[],[f145107]) ).
fof(f145312,plain,
s__instance(s__Human23_7,s__Human),
inference(cnf_transformation,[],[f145108]) ).
fof(f145313,plain,
s__instance(s__Human23_8,s__Human),
inference(cnf_transformation,[],[f145109]) ).
fof(f145314,plain,
s__instance(s__Human23_9,s__Human),
inference(cnf_transformation,[],[f145110]) ).
fof(f145315,plain,
s__instance(s__Human23_10,s__Human),
inference(cnf_transformation,[],[f145111]) ).
fof(f145316,plain,
s__instance(s__Human23_11,s__Human),
inference(cnf_transformation,[],[f145112]) ).
fof(f145317,plain,
s__instance(s__Human23_12,s__Human),
inference(cnf_transformation,[],[f145113]) ).
fof(f145318,plain,
s__instance(s__Human23_13,s__Human),
inference(cnf_transformation,[],[f145114]) ).
fof(f145319,plain,
s__instance(s__Human23_14,s__Human),
inference(cnf_transformation,[],[f145115]) ).
fof(f145320,plain,
s__instance(s__Human23_15,s__Human),
inference(cnf_transformation,[],[f145116]) ).
fof(f145321,plain,
s__instance(s__Human23_16,s__Human),
inference(cnf_transformation,[],[f145117]) ).
fof(f145322,plain,
s__ancestor(s__Human23_1,s__Human23_2),
inference(cnf_transformation,[],[f145118]) ).
fof(f145323,plain,
s__ancestor(s__Human23_2,s__Human23_3),
inference(cnf_transformation,[],[f145119]) ).
fof(f145324,plain,
s__ancestor(s__Human23_3,s__Human23_4),
inference(cnf_transformation,[],[f145120]) ).
fof(f145325,plain,
s__ancestor(s__Human23_4,s__Human23_5),
inference(cnf_transformation,[],[f145121]) ).
fof(f145326,plain,
s__ancestor(s__Human23_5,s__Human23_6),
inference(cnf_transformation,[],[f145122]) ).
fof(f145327,plain,
s__ancestor(s__Human23_6,s__Human23_7),
inference(cnf_transformation,[],[f145123]) ).
fof(f145328,plain,
s__ancestor(s__Human23_7,s__Human23_8),
inference(cnf_transformation,[],[f145124]) ).
fof(f145329,plain,
s__ancestor(s__Human23_8,s__Human23_9),
inference(cnf_transformation,[],[f145125]) ).
fof(f145330,plain,
s__ancestor(s__Human23_9,s__Human23_10),
inference(cnf_transformation,[],[f145126]) ).
fof(f145331,plain,
s__ancestor(s__Human23_10,s__Human23_11),
inference(cnf_transformation,[],[f145127]) ).
fof(f145332,plain,
s__ancestor(s__Human23_11,s__Human23_12),
inference(cnf_transformation,[],[f145128]) ).
fof(f145333,plain,
s__ancestor(s__Human23_12,s__Human23_13),
inference(cnf_transformation,[],[f145129]) ).
fof(f145334,plain,
s__ancestor(s__Human23_13,s__Human23_14),
inference(cnf_transformation,[],[f145130]) ).
fof(f145335,plain,
s__ancestor(s__Human23_14,s__Human23_15),
inference(cnf_transformation,[],[f145131]) ).
fof(f145336,plain,
s__ancestor(s__Human23_14,s__Human23_16),
inference(cnf_transformation,[],[f145132]) ).
fof(f145337,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| ~ s__ancestor(s__Human23_1,s__Human23_16) ),
inference(cnf_transformation,[],[f145135]) ).
fof(f145348,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__Organism)
| ~ s__ancestor(X0,X1)
| ~ s__ancestor(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__ancestor(X0,X2) ),
inference(cnf_transformation,[],[f145141]) ).
fof(f145370,plain,
s__subclass(s__Human,s__Organism),
inference(cnf_transformation,[],[f124477]) ).
fof(f145426,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145209]) ).
fof(f145427,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f145210]) ).
fof(f145428,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145210]) ).
fof(f145641,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f145426,f145427]) ).
fof(f145647,definition,
( spl9_1
<=> s__ancestor(s__Human23_1,s__Human23_16) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f145648,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_16)
| spl9_1 ),
inference(avatar_component_clause,[],[f145647]) ).
fof(f145650,definition,
( spl9_2
<=> s__ancestor(s__Human23_1,s__Human23_15) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f145651,plain,
( ~ s__ancestor(s__Human23_1,s__Human23_15)
| spl9_2 ),
inference(avatar_component_clause,[],[f145650]) ).
fof(f145652,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(avatar_split_clause,[],[f145337,f145650,f145647]) ).
fof(f145653,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f145641,f145428]) ).
fof(f145658,plain,
! [X0] :
( ~ s__instance(X0,s__Human)
| s__instance(X0,s__Organism) ),
inference(resolution,[],[f145370,f145653]) ).
fof(f145659,plain,
s__instance(s__Human23_1,s__Organism),
inference(resolution,[],[f145658,f145306]) ).
fof(f145660,plain,
s__instance(s__Human23_2,s__Organism),
inference(resolution,[],[f145658,f145307]) ).
fof(f145661,plain,
s__instance(s__Human23_14,s__Organism),
inference(resolution,[],[f145658,f145319]) ).
fof(f145662,plain,
s__instance(s__Human23_15,s__Organism),
inference(resolution,[],[f145658,f145320]) ).
fof(f145663,plain,
s__instance(s__Human23_16,s__Organism),
inference(resolution,[],[f145658,f145321]) ).
fof(f145664,plain,
! [X0,X1] :
( ~ s__ancestor(s__Human23_1,X0)
| ~ s__ancestor(X0,X1)
| ~ s__instance(X1,s__Organism)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X1) ),
inference(resolution,[],[f145348,f145659]) ).
fof(f145671,plain,
s__instance(s__Human23_13,s__Organism),
inference(resolution,[],[f145318,f145658]) ).
fof(f145672,plain,
s__instance(s__Human23_11,s__Organism),
inference(resolution,[],[f145316,f145658]) ).
fof(f145673,plain,
s__instance(s__Human23_7,s__Organism),
inference(resolution,[],[f145312,f145658]) ).
fof(f145674,plain,
s__instance(s__Human23_12,s__Organism),
inference(resolution,[],[f145317,f145658]) ).
fof(f145675,plain,
s__instance(s__Human23_6,s__Organism),
inference(resolution,[],[f145311,f145658]) ).
fof(f145676,plain,
s__instance(s__Human23_8,s__Organism),
inference(resolution,[],[f145313,f145658]) ).
fof(f145677,plain,
s__instance(s__Human23_9,s__Organism),
inference(resolution,[],[f145314,f145658]) ).
fof(f145678,plain,
s__instance(s__Human23_5,s__Organism),
inference(resolution,[],[f145310,f145658]) ).
fof(f145679,plain,
s__instance(s__Human23_10,s__Organism),
inference(resolution,[],[f145315,f145658]) ).
fof(f145680,plain,
s__instance(s__Human23_4,s__Organism),
inference(resolution,[],[f145309,f145658]) ).
fof(f145681,plain,
s__instance(s__Human23_3,s__Organism),
inference(resolution,[],[f145308,f145658]) ).
fof(f145682,plain,
! [X0] :
( ~ s__ancestor(s__Human23_2,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_2,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145664,f145322]) ).
fof(f145683,plain,
! [X0] :
( ~ s__ancestor(s__Human23_2,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145682,f145660]) ).
fof(f145684,plain,
( ~ s__instance(s__Human23_3,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_3) ),
inference(resolution,[],[f145683,f145323]) ).
fof(f145685,plain,
s__ancestor(s__Human23_1,s__Human23_3),
inference(forward_subsumption_resolution,[],[f145684,f145681]) ).
fof(f145686,plain,
! [X0] :
( ~ s__ancestor(s__Human23_3,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_3,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145685,f145664]) ).
fof(f145687,plain,
! [X0] :
( ~ s__ancestor(s__Human23_3,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145686,f145681]) ).
fof(f145688,plain,
( ~ s__instance(s__Human23_4,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_4) ),
inference(resolution,[],[f145324,f145687]) ).
fof(f145689,plain,
s__ancestor(s__Human23_1,s__Human23_4),
inference(forward_subsumption_resolution,[],[f145688,f145680]) ).
fof(f145690,plain,
! [X0] :
( ~ s__ancestor(s__Human23_4,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_4,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145689,f145664]) ).
fof(f145691,plain,
! [X0] :
( ~ s__ancestor(s__Human23_4,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145690,f145680]) ).
fof(f145692,plain,
( ~ s__instance(s__Human23_5,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_5) ),
inference(resolution,[],[f145691,f145325]) ).
fof(f145693,plain,
s__ancestor(s__Human23_1,s__Human23_5),
inference(forward_subsumption_resolution,[],[f145692,f145678]) ).
fof(f145694,plain,
! [X0] :
( ~ s__ancestor(s__Human23_5,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_5,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145693,f145664]) ).
fof(f145695,plain,
! [X0] :
( ~ s__ancestor(s__Human23_5,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145694,f145678]) ).
fof(f145696,plain,
( ~ s__instance(s__Human23_6,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_6) ),
inference(resolution,[],[f145695,f145326]) ).
fof(f145697,plain,
s__ancestor(s__Human23_1,s__Human23_6),
inference(forward_subsumption_resolution,[],[f145696,f145675]) ).
fof(f145698,plain,
! [X0] :
( ~ s__ancestor(s__Human23_6,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_6,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145697,f145664]) ).
fof(f145699,plain,
! [X0] :
( ~ s__ancestor(s__Human23_6,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145698,f145675]) ).
fof(f145700,plain,
( ~ s__instance(s__Human23_7,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_7) ),
inference(resolution,[],[f145699,f145327]) ).
fof(f145701,plain,
s__ancestor(s__Human23_1,s__Human23_7),
inference(forward_subsumption_resolution,[],[f145700,f145673]) ).
fof(f145702,plain,
! [X0] :
( ~ s__ancestor(s__Human23_7,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_7,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145701,f145664]) ).
fof(f145703,plain,
! [X0] :
( ~ s__ancestor(s__Human23_7,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145702,f145673]) ).
fof(f145704,plain,
( ~ s__instance(s__Human23_8,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_8) ),
inference(resolution,[],[f145703,f145328]) ).
fof(f145705,plain,
s__ancestor(s__Human23_1,s__Human23_8),
inference(forward_subsumption_resolution,[],[f145704,f145676]) ).
fof(f145706,plain,
! [X0] :
( ~ s__ancestor(s__Human23_8,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_8,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145705,f145664]) ).
fof(f145707,plain,
! [X0] :
( ~ s__ancestor(s__Human23_8,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145706,f145676]) ).
fof(f145708,plain,
( ~ s__instance(s__Human23_9,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_9) ),
inference(resolution,[],[f145707,f145329]) ).
fof(f145709,plain,
s__ancestor(s__Human23_1,s__Human23_9),
inference(forward_subsumption_resolution,[],[f145708,f145677]) ).
fof(f145710,plain,
! [X0] :
( ~ s__ancestor(s__Human23_9,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_9,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145709,f145664]) ).
fof(f145711,plain,
! [X0] :
( ~ s__ancestor(s__Human23_9,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145710,f145677]) ).
fof(f145712,plain,
( ~ s__instance(s__Human23_10,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_10) ),
inference(resolution,[],[f145711,f145330]) ).
fof(f145713,plain,
s__ancestor(s__Human23_1,s__Human23_10),
inference(forward_subsumption_resolution,[],[f145712,f145679]) ).
fof(f145714,plain,
! [X0] :
( ~ s__ancestor(s__Human23_10,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_10,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145713,f145664]) ).
fof(f145715,plain,
! [X0] :
( ~ s__ancestor(s__Human23_10,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145714,f145679]) ).
fof(f145716,plain,
( ~ s__instance(s__Human23_11,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_11) ),
inference(resolution,[],[f145715,f145331]) ).
fof(f145717,plain,
s__ancestor(s__Human23_1,s__Human23_11),
inference(forward_subsumption_resolution,[],[f145716,f145672]) ).
fof(f145718,plain,
! [X0] :
( ~ s__ancestor(s__Human23_11,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_11,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145717,f145664]) ).
fof(f145719,plain,
! [X0] :
( ~ s__ancestor(s__Human23_11,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145718,f145672]) ).
fof(f145720,plain,
( ~ s__instance(s__Human23_12,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_12) ),
inference(resolution,[],[f145719,f145332]) ).
fof(f145721,plain,
s__ancestor(s__Human23_1,s__Human23_12),
inference(forward_subsumption_resolution,[],[f145720,f145674]) ).
fof(f145722,plain,
! [X0] :
( ~ s__ancestor(s__Human23_12,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_12,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145721,f145664]) ).
fof(f145723,plain,
! [X0] :
( ~ s__ancestor(s__Human23_12,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145722,f145674]) ).
fof(f145724,plain,
( ~ s__instance(s__Human23_13,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_13) ),
inference(resolution,[],[f145723,f145333]) ).
fof(f145725,plain,
s__ancestor(s__Human23_1,s__Human23_13),
inference(forward_subsumption_resolution,[],[f145724,f145671]) ).
fof(f145726,plain,
! [X0] :
( ~ s__ancestor(s__Human23_13,X0)
| ~ s__instance(X0,s__Organism)
| ~ s__instance(s__Human23_13,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(resolution,[],[f145725,f145664]) ).
fof(f145727,plain,
! [X0] :
( ~ s__ancestor(s__Human23_13,X0)
| ~ s__instance(X0,s__Organism)
| s__ancestor(s__Human23_1,X0) ),
inference(forward_subsumption_resolution,[],[f145726,f145671]) ).
fof(f145728,plain,
( ~ s__instance(s__Human23_14,s__Organism)
| s__ancestor(s__Human23_1,s__Human23_14) ),
inference(resolution,[],[f145727,f145334]) ).
fof(f145729,plain,
s__ancestor(s__Human23_1,s__Human23_14),
inference(forward_subsumption_resolution,[],[f145728,f145661]) ).
fof(f145731,plain,
( $false
| spl9_1 ),
inference(unit_resulting_resolution,[],[f145348,f145648,f145336,f145663,f145661,f145659,f145729]) ).
fof(f145734,plain,
spl9_1,
inference(avatar_contradiction_clause,[],[f145731]) ).
fof(f145737,plain,
( $false
| spl9_2 ),
inference(unit_resulting_resolution,[],[f145348,f145335,f145661,f145729,f145659,f145662,f145651]) ).
fof(f145739,plain,
spl9_2,
inference(avatar_contradiction_clause,[],[f145737]) ).
cnf(s1,plain,
( ~ spl9_1
| ~ spl9_2 ),
inference(sat_conversion,[],[f145652]) ).
cnf(s3,plain,
spl9_1,
inference(sat_conversion,[],[f145734]) ).
cnf(s5,plain,
spl9_2,
inference(sat_conversion,[],[f145739]) ).
cnf(s6,plain,
$false,
inference(rat,[],[s1,s5,s3]) ).
fof(f145740,plain,
$false,
inference(avatar_sat_refutation,[],[s6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR093+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n004.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 22:42:37 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running first-order theorem proving
% 0.07/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.64/5.23 % (867632)Detected formulas, will run a generic FOF schedule.
% 14.64/5.23 % (867640)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=660512735:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 14.64/5.23 % (867637)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=304278098:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 14.64/5.23 % (867639)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3483514793:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 14.64/5.23 % (867638)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=197141540:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 14.64/5.23 % (867640)Instruction limit reached!
% 14.64/5.23 % (867640)------------------------------
% 14.64/5.23 % (867640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.64/5.23 % (867640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/5.23 % (867640)CaDiCaL version: 2.1.3
% 14.64/5.23 % (867640)Termination reason: Instruction limit
% 14.64/5.23 % (867640)Termination phase: SInE selection
% 14.64/5.23 % (867640)Time elapsed: 0.039 s
% 14.64/5.23 % (867640)Peak memory usage: 165 MB
% 14.64/5.23 % (867640)Instructions burned: 112 (million)
% 14.64/5.23 % (867642)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1491585128:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 14.64/5.23 % (867641)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3898402209:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 14.64/5.23 % (867643)dis-21_1_sil=8000:lcm=predicate:random_seed=874296645:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 14.64/5.23 % (867641)Instruction limit reached!
% 14.64/5.23 % (867641)------------------------------
% 14.64/5.23 % (867641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.64/5.23 % (867641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/5.23 % (867641)CaDiCaL version: 2.1.3
% 14.64/5.23 % (867641)Termination reason: Instruction limit
% 14.64/5.23 % (867641)Termination phase: SInE selection
% 14.64/5.23 % (867641)Time elapsed: 0.068 s
% 14.64/5.23 % (867641)Peak memory usage: 164 MB
% 14.64/5.23 % (867641)Instructions burned: 120 (million)
% 14.64/5.23 % (867642)Instruction limit reached!
% 14.64/5.23 % (867642)------------------------------
% 14.64/5.23 % (867642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.64/5.23 % (867642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/5.23 % (867642)CaDiCaL version: 2.1.3
% 14.64/5.23 % (867642)Termination reason: Instruction limit
% 14.64/5.23 % (867642)Termination phase: Property scanning
% 14.64/5.23 % (867642)Time elapsed: 0.075 s
% 14.64/5.23 % (867642)Peak memory usage: 165 MB
% 14.64/5.23 % (867642)Instructions burned: 139 (million)
% 14.64/5.23 % (867643)Instruction limit reached!
% 14.64/5.23 % (867643)------------------------------
% 14.64/5.23 % (867643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.64/5.23 % (867643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.64/5.23 % (867643)CaDiCaL version: 2.1.3
% 14.64/5.23 % (867643)Termination reason: Instruction limit
% 14.64/5.23 % (867643)Termination phase: SInE selection
% 14.64/5.23 % (867643)Time elapsed: 0.076 s
% 14.64/5.23 % (867643)Peak memory usage: 165 MB
% 14.64/5.23 % (867643)Instructions burned: 130 (million)
% 14.64/5.23 % (867648)lrs+10_1_sil=8000:sp=occurrence:random_seed=2255561699:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 14.64/5.23 % (867653)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1331313539:i=325:sd=1:ss=axioms:sgt=32_2968 on theBenchmark for (2968ds/325Mi)
% 14.64/5.23 % (867652)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4281201112:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/157Mi)
% 14.64/5.23 % (867654)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=518666197:s2a=on:i=248:s2at=1.23:gtg=position_2968 on theBenchmark for (2968ds/248Mi)
% 14.64/5.23 % (867648)Instruction limit reached!
% 14.64/5.23 % (867648)------------------------------
% 18.04/5.90 % (867648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867648)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867648)Termination reason: Instruction limit
% 18.04/5.90 % (867648)Termination phase: SInE selection
% 18.04/5.90 % (867648)Time elapsed: 0.155 s
% 18.04/5.90 % (867648)Peak memory usage: 164 MB
% 18.04/5.90 % (867648)Instructions burned: 285 (million)
% 18.04/5.90 % (867652)Instruction limit reached!
% 18.04/5.90 % (867652)------------------------------
% 18.04/5.90 % (867652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867652)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867652)Termination reason: Instruction limit
% 18.04/5.90 % (867652)Termination phase: Property scanning
% 18.04/5.90 % (867652)Time elapsed: 0.083 s
% 18.04/5.90 % (867652)Peak memory usage: 165 MB
% 18.04/5.90 % (867652)Instructions burned: 158 (million)
% 18.04/5.90 % (867654)Instruction limit reached!
% 18.04/5.90 % (867654)------------------------------
% 18.04/5.90 % (867654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867654)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867654)Termination reason: Instruction limit
% 18.04/5.90 % (867654)Termination phase: Property scanning
% 18.04/5.90 % (867654)Time elapsed: 0.119 s
% 18.04/5.90 % (867654)Peak memory usage: 165 MB
% 18.04/5.90 % (867654)Instructions burned: 249 (million)
% 18.04/5.90 % (867653)Instruction limit reached!
% 18.04/5.90 % (867653)------------------------------
% 18.04/5.90 % (867653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867653)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867653)Termination reason: Instruction limit
% 18.04/5.90 % (867653)Termination phase: SInE selection
% 18.04/5.90 % (867653)Time elapsed: 0.162 s
% 18.04/5.90 % (867653)Peak memory usage: 164 MB
% 18.04/5.90 % (867653)Instructions burned: 327 (million)
% 18.04/5.90 % (867660)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1784437604:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 18.04/5.90 % (867659)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3267917377:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2966 on theBenchmark for (2966ds/294Mi)
% 18.04/5.90 % (867661)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1719700558:cts=off:i=113:fsr=off:ss=included:sgt=4_2965 on theBenchmark for (2965ds/113Mi)
% 18.04/5.90 % (867662)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2010714200:i=127:av=off:fsr=off:sup=off_2965 on theBenchmark for (2965ds/127Mi)
% 18.04/5.90 % (867661)Instruction limit reached!
% 18.04/5.90 % (867661)------------------------------
% 18.04/5.90 % (867661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867661)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867661)Termination reason: Instruction limit
% 18.04/5.90 % (867661)Termination phase: SInE selection
% 18.04/5.90 % (867661)Time elapsed: 0.067 s
% 18.04/5.90 % (867661)Peak memory usage: 165 MB
% 18.04/5.90 % (867661)Instructions burned: 114 (million)
% 18.04/5.90 % (867659)Instruction limit reached!
% 18.04/5.90 % (867659)------------------------------
% 18.04/5.90 % (867659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867659)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867659)Termination reason: Instruction limit
% 18.04/5.90 % (867659)Termination phase: SInE selection
% 18.04/5.90 % (867659)Time elapsed: 0.163 s
% 18.04/5.90 % (867659)Peak memory usage: 165 MB
% 18.04/5.90 % (867659)Instructions burned: 294 (million)
% 18.04/5.90 % (867662)Instruction limit reached!
% 18.04/5.90 % (867662)------------------------------
% 18.04/5.90 % (867662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.04/5.90 % (867662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.04/5.90 % (867662)CaDiCaL version: 2.1.3
% 18.04/5.90 % (867662)Termination reason: Instruction limit
% 18.04/5.90 % (867662)Termination phase: Preprocessing 1
% 18.04/5.90 % (867662)Time elapsed: 0.084 s
% 18.39/6.05 % (867662)Peak memory usage: 165 MB
% 18.39/6.05 % (867662)Instructions burned: 127 (million)
% 18.39/6.05 % (867667)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3016924547:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2963 on theBenchmark for (2963ds/114Mi)
% 18.39/6.05 % (867668)lrs+10_1_sil=8000:sp=occurrence:random_seed=2528772442:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 18.39/6.05 % (867669)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2770853236:i=437:sd=1:aac=none:ss=included_2963 on theBenchmark for (2963ds/437Mi)
% 18.39/6.05 % (867667)Instruction limit reached!
% 18.39/6.05 % (867667)------------------------------
% 18.39/6.05 % (867667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867667)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867667)Termination reason: Instruction limit
% 18.39/6.05 % (867667)Termination phase: Property scanning
% 18.39/6.05 % (867667)Time elapsed: 0.065 s
% 18.39/6.05 % (867667)Peak memory usage: 165 MB
% 18.39/6.05 % (867667)Instructions burned: 116 (million)
% 18.39/6.05 % (867673)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1725621684:i=5202:ss=axioms:sgt=16_2961 on theBenchmark for (2961ds/5202Mi)
% 18.39/6.05 % (867669)Refutation not found, incomplete strategy
% 18.39/6.05 % (867669)------------------------------
% 18.39/6.05 % (867669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867669)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867669)Termination reason: Refutation not found, incomplete strategy
% 18.39/6.05 % (867669)Time elapsed: 0.240 s
% 18.39/6.05 % (867669)Peak memory usage: 169 MB
% 18.39/6.05 % (867669)Instructions burned: 397 (million)
% 18.39/6.05 % (867660)Instruction limit reached!
% 18.39/6.05 % (867660)------------------------------
% 18.39/6.05 % (867660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867660)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867660)Termination reason: Instruction limit
% 18.39/6.05 % (867660)Termination phase: Property scanning
% 18.39/6.05 % (867660)Time elapsed: 0.684 s
% 18.39/6.05 % (867660)Peak memory usage: 194 MB
% 18.39/6.05 % (867660)Instructions burned: 2353 (million)
% 18.39/6.05 % (867675)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=196179444:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2958 on theBenchmark for (2958ds/134Mi)
% 18.39/6.05 % (867675)Instruction limit reached!
% 18.39/6.05 % (867675)------------------------------
% 18.39/6.05 % (867675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867675)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867675)Termination reason: Instruction limit
% 18.39/6.05 % (867675)Termination phase: SInE selection
% 18.39/6.05 % (867675)Time elapsed: 0.044 s
% 18.39/6.05 % (867675)Peak memory usage: 165 MB
% 18.39/6.05 % (867675)Instructions burned: 135 (million)
% 18.39/6.05 % (867669)------------------------------
% 18.39/6.05 % (867669)------------------------------
% 18.39/6.05 % (867668)Instruction limit reached!
% 18.39/6.05 % (867668)------------------------------
% 18.39/6.05 % (867668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867668)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867668)Termination reason: Instruction limit
% 18.39/6.05 % (867668)Termination phase: Saturation
% 18.39/6.05 % (867668)Time elapsed: 0.546 s
% 18.39/6.05 % (867668)Peak memory usage: 175 MB
% 18.39/6.05 % (867668)Instructions burned: 908 (million)
% 18.39/6.05 % (867677)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=444135338:st=8:i=592:sd=3:ep=RST:ss=axioms_2956 on theBenchmark for (2956ds/592Mi)
% 18.39/6.05 % (867678)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=714636538:st=3:i=13193:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/13193Mi)
% 18.39/6.05 % (867679)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=794227484:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/125Mi)
% 18.39/6.05 % (867679)Instruction limit reached!
% 18.39/6.05 % (867679)------------------------------
% 18.39/6.05 % (867679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867679)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867679)Termination reason: Instruction limit
% 18.39/6.05 % (867679)Termination phase: Property scanning
% 18.39/6.05 % (867679)Time elapsed: 0.070 s
% 18.39/6.05 % (867679)Peak memory usage: 165 MB
% 18.39/6.05 % (867679)Instructions burned: 125 (million)
% 18.39/6.05 % (867677)Instruction limit reached!
% 18.39/6.05 % (867677)------------------------------
% 18.39/6.05 % (867677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867677)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867677)Termination reason: Instruction limit
% 18.39/6.05 % (867677)Termination phase: Preprocessing 2
% 18.39/6.05 % (867677)Time elapsed: 0.195 s
% 18.39/6.05 % (867677)Peak memory usage: 167 MB
% 18.39/6.05 % (867677)Instructions burned: 592 (million)
% 18.39/6.05 % (867639)Refutation not found, incomplete strategy
% 18.39/6.05 % (867639)------------------------------
% 18.39/6.05 % (867639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867639)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867639)Termination reason: Refutation not found, incomplete strategy
% 18.39/6.05 % (867639)Time elapsed: 1.712 s
% 18.39/6.05 % (867639)Peak memory usage: 236 MB
% 18.39/6.05 % (867639)Instructions burned: 2526 (million)
% 18.39/6.05 % (867684)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3648636055:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/141Mi)
% 18.39/6.05 % (867683)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2943118523:i=134:gtgl=5:slsql=off:gtg=exists_sym_2953 on theBenchmark for (2953ds/134Mi)
% 18.39/6.05 % (867684)Instruction limit reached!
% 18.39/6.05 % (867684)------------------------------
% 18.39/6.05 % (867684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867684)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867684)Termination reason: Instruction limit
% 18.39/6.05 % (867684)Termination phase: SInE selection
% 18.39/6.05 % (867684)Time elapsed: 0.047 s
% 18.39/6.05 % (867684)Peak memory usage: 165 MB
% 18.39/6.05 % (867684)Instructions burned: 145 (million)
% 18.39/6.05 % (867683)Instruction limit reached!
% 18.39/6.05 % (867683)------------------------------
% 18.39/6.05 % (867683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867683)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867683)Termination reason: Instruction limit
% 18.39/6.05 % (867683)Termination phase: Property scanning
% 18.39/6.05 % (867683)Time elapsed: 0.075 s
% 18.39/6.05 % (867683)Peak memory usage: 165 MB
% 18.39/6.05 % (867683)Instructions burned: 134 (million)
% 18.39/6.05 % (867687)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2735190277:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2951 on theBenchmark for (2951ds/431Mi)
% 18.39/6.05 % (867638)First to succeed.
% 18.39/6.05 % (867638)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-867632"
% 18.39/6.05 % (867639)------------------------------
% 18.39/6.05 % (867639)------------------------------
% 18.39/6.05 % (867688)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2142512485:i=6060:aac=none:ins=25_2951 on theBenchmark for (2951ds/6060Mi)
% 18.39/6.05 % (867687)Refutation not found, incomplete strategy
% 18.39/6.05 % (867687)------------------------------
% 18.39/6.05 % (867687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867687)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867687)Termination reason: Refutation not found, incomplete strategy
% 18.39/6.05 % (867687)Time elapsed: 0.147 s
% 18.39/6.05 % (867687)Peak memory usage: 170 MB
% 18.39/6.05 % (867687)Instructions burned: 398 (million)
% 18.39/6.05 % (867690)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3114489427:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2949 on theBenchmark for (2949ds/150Mi)
% 18.39/6.05 % (867687)------------------------------
% 18.39/6.05 % (867687)------------------------------
% 18.39/6.05 % (867690)Instruction limit reached!
% 18.39/6.05 % (867690)------------------------------
% 18.39/6.05 % (867690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.39/6.05 % (867690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.39/6.05 % (867690)CaDiCaL version: 2.1.3
% 18.39/6.05 % (867690)Termination reason: Instruction limit
% 18.39/6.05 % (867690)Termination phase: SInE selection
% 18.39/6.05 % (867690)Time elapsed: 0.091 s
% 18.39/6.05 % (867690)Peak memory usage: 165 MB
% 18.39/6.05 % (867690)Instructions burned: 151 (million)
% 18.39/6.05 % (867638)Refutation found. Thanks to Tanya!
% 18.39/6.05 % SZS status Theorem for theBenchmark
% 18.39/6.05 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/6.32 % (867638)------------------------------
% 0.19/6.32 % (867638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/6.32 % (867638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/6.32 % (867638)CaDiCaL version: 2.1.3
% 0.19/6.32 % (867638)Termination reason: Refutation
% 0.19/6.32 % (867638)Time elapsed: 1.980 s
% 0.19/6.32 % (867638)Peak memory usage: 321 MB
% 0.19/6.32 % (867638)Instructions burned: 2813 (million)
% 0.19/6.32 % (867638)------------------------------
% 0.19/6.32 % (867638)------------------------------
% 0.19/6.32 % (867632)Success in time 5.37 s
% 0.19/6.32 % Vampire exiting
%------------------------------------------------------------------------------