%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO490+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 09:52:47 AM UTC 2026
% Result : Theorem 83.59s 12.70s
% Output : Refutation 84.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 46
% Syntax : Number of formulae : 209 ( 42 unt; 23 def)
% Number of atoms : 504 ( 36 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 539 ( 244 ~; 262 |; 10 &)
% ( 23 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 24 prp; 0-8 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-6 aty)
% Number of variables : 290 ( 0 sgn 282 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : s_e(X0,X1,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA1) ).
fof(f2,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ~ s_e(X0,X1,X2,X3)
| ~ s_e(X0,X1,X4,X5)
| s_e(X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA2) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ~ s_e(X0,X1,X2,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA3) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( s_t(X0,X1,ext(X0,X1,X2,X3))
& s_e(X1,ext(X0,X1,X2,X3),X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA4) ).
fof(f5,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ s_e(X0,X1,X2,X3)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X6,X2,X7)
| ~ s_e(X1,X6,X3,X7)
| ~ s_t(X0,X1,X4)
| ~ s_t(X2,X3,X5)
| X0 = X1
| s_e(X4,X6,X5,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ s_t(X0,X1,X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aA6) ).
fof(f9,axiom,
! [X0,X1] : s_e(X0,X1,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_1) ).
fof(f10,axiom,
! [X0,X1,X2,X3] :
( ~ s_e(X0,X1,X2,X3)
| s_e(X2,X3,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_2) ).
fof(f11,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ~ s_e(X0,X1,X2,X3)
| ~ s_e(X2,X3,X4,X5)
| s_e(X0,X1,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_3) ).
fof(f14,axiom,
! [X0,X1] : s_e(X0,X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_8) ).
fof(f16,axiom,
! [X0,X1,X2,X3,X4] :
( X0 = X1
| ~ s_t(X0,X1,X2)
| ~ s_e(X1,X2,X3,X4)
| X2 = ext(X0,X1,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_12) ).
fof(f18,axiom,
! [X0,X1,X2,X3] :
( ~ s_e(X0,X1,X2,X3)
| s_e(X1,X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_14) ).
fof(f20,axiom,
! [X0,X1] : s_t(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_1) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ~ s_t(X0,X1,X2)
| s_t(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_2) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ~ s_t(X0,X1,X2)
| ~ s_t(X1,X0,X2)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_4) ).
fof(f24,axiom,
! [X0,X1,X2,X3] :
( ~ s_t(X0,X1,X2)
| ~ s_t(X1,X3,X2)
| s_t(X0,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_5a) ).
fof(f25,axiom,
! [X0,X1,X2,X3] :
( ~ s_t(X0,X1,X2)
| ~ s_t(X0,X2,X3)
| s_t(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_6a) ).
fof(f34,axiom,
! [X0,X1] : X0 != ext(X1,X0,alpha,gamma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_14b) ).
fof(f35,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ s_t(X0,X1,X2)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X5,X3)
| s_t(X5,crossbar(X0,X1,X2,X3,X4,X5),X2) )
& ( ~ s_t(X0,X1,X2)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X5,X3)
| s_t(X1,crossbar(X0,X1,X2,X3,X4,X5),X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_17) ).
fof(f36,conjecture,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X1,X3,X5,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz4_2) ).
fof(f37,negated_conjecture,
~ ! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X1,X3,X5,X7) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_t(X0,X1,X2) )
& ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_t(X4,X5,X6) )
& ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X0,X2,X4,X6) )
& ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X1,X2,X5,X6) )
& ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X0,X3,X4,X7) )
& ( ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
| s_e(X2,X3,X6,X7) )
& ( ~ s_t(X0,X1,X2)
| ~ s_t(X4,X5,X6)
| ~ s_e(X0,X2,X4,X6)
| ~ s_e(X1,X2,X5,X6)
| ~ s_e(X0,X3,X4,X7)
| ~ s_e(X2,X3,X6,X7)
| s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn4_1) ).
fof(f44,plain,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( s_ifs(X0,X1,X2,X3,X4,X5,X6,X7)
& ~ s_e(X1,X3,X5,X7) ),
inference(ennf_transformation,[],[f37]) ).
fof(f45,plain,
( s_ifs(sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7)
& ~ s_e(sK1,sK3,sK5,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6),skolemize(X7,sK7)],[f44]) ).
fof(f46,plain,
! [X0,X1] : s_e(X0,X1,X0,X1),
inference(cnf_transformation,[],[f9]) ).
fof(f47,plain,
! [X2,X3,X0,X1] :
( s_e(X2,X3,X0,X1)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f48,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X0,X1,X4,X5)
| ~ s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
! [X0,X1] : s_e(X0,X0,X1,X1),
inference(cnf_transformation,[],[f14]) ).
fof(f53,plain,
! [X2,X3,X0,X1,X4] :
( ~ s_t(X0,X1,X2)
| X0 = X1
| ~ s_e(X1,X2,X3,X4)
| ext(X0,X1,X3,X4) = X2 ),
inference(cnf_transformation,[],[f16]) ).
fof(f55,plain,
! [X2,X3,X0,X1] :
( s_e(X1,X0,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f18]) ).
fof(f57,plain,
! [X0,X1] : s_t(X0,X1,X1),
inference(cnf_transformation,[],[f20]) ).
fof(f58,plain,
! [X2,X0,X1] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f60,plain,
! [X2,X0,X1] :
( ~ s_t(X0,X1,X2)
| ~ s_t(X1,X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f23]) ).
fof(f61,plain,
! [X2,X3,X0,X1] :
( s_t(X0,X1,X3)
| ~ s_t(X1,X3,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f24]) ).
fof(f62,plain,
! [X2,X3,X0,X1] :
( s_t(X1,X2,X3)
| ~ s_t(X0,X2,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f25]) ).
fof(f71,plain,
! [X0,X1] : ext(X1,X0,alpha,gamma) != X0,
inference(cnf_transformation,[],[f34]) ).
fof(f72,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X1,crossbar(X0,X1,X2,X3,X4,X5),X4)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X5,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f73,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X5,crossbar(X0,X1,X2,X3,X4,X5),X2)
| ~ s_t(X3,X4,X2)
| ~ s_t(X0,X5,X3)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f35]) ).
fof(f74,plain,
~ s_e(sK1,sK3,sK5,sK7),
inference(cnf_transformation,[],[f45]) ).
fof(f75,plain,
s_ifs(sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7),
inference(cnf_transformation,[],[f45]) ).
fof(f85,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X2,X3,X6,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f86,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X0,X3,X4,X7)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f87,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X1,X2,X5,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f88,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X0,X2,X4,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f89,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_t(X4,X5,X6)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f90,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_t(X0,X1,X2)
| ~ s_ifs(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[],[f40]) ).
fof(f104,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_e(X2,X3,X4,X5)
| ~ s_e(X0,X1,X4,X5)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
! [X0,X1] : s_e(X0,X1,X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f106,plain,
! [X0,X1] :
( ~ s_t(X0,X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f6]) ).
fof(f107,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( s_e(X4,X6,X5,X7)
| ~ s_e(X1,X4,X3,X5)
| ~ s_e(X0,X6,X2,X7)
| ~ s_e(X1,X6,X3,X7)
| ~ s_t(X0,X1,X4)
| ~ s_t(X2,X3,X5)
| X0 = X1
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f108,plain,
! [X2,X0,X1] :
( ~ s_e(X0,X1,X2,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f109,plain,
! [X2,X3,X0,X1] : s_e(X1,ext(X0,X1,X2,X3),X2,X3),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
! [X2,X3,X0,X1] : s_t(X0,X1,ext(X0,X1,X2,X3)),
inference(cnf_transformation,[],[f4]) ).
fof(f130,definition,
( spl8_4
<=> s_e(sK1,sK3,sK5,sK7) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
fof(f132,plain,
( ~ s_e(sK1,sK3,sK5,sK7)
| spl8_4 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f133,plain,
~ spl8_4,
inference(avatar_split_clause,[],[f74,f130]) ).
fof(f135,definition,
( spl8_5
<=> s_ifs(sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f137,plain,
( s_ifs(sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7)
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f138,plain,
spl8_5,
inference(avatar_split_clause,[],[f75,f135]) ).
fof(f154,plain,
( s_e(sK0,sK3,sK4,sK7)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f86,f137]) ).
fof(f158,definition,
( spl8_9
<=> s_e(sK0,sK3,sK4,sK7) ),
introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition]) ).
fof(f160,plain,
( s_e(sK0,sK3,sK4,sK7)
| ~ spl8_9 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f161,plain,
( spl8_9
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f154,f135,f158]) ).
fof(f162,plain,
( s_e(sK1,sK2,sK5,sK6)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f87,f137]) ).
fof(f166,definition,
( spl8_10
<=> s_e(sK1,sK2,sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition]) ).
fof(f168,plain,
( s_e(sK1,sK2,sK5,sK6)
| ~ spl8_10 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
( spl8_10
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f162,f135,f166]) ).
fof(f170,plain,
( s_e(sK2,sK3,sK6,sK7)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f85,f137]) ).
fof(f174,definition,
( spl8_11
<=> s_e(sK2,sK3,sK6,sK7) ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f176,plain,
( s_e(sK2,sK3,sK6,sK7)
| ~ spl8_11 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f177,plain,
( spl8_11
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f170,f135,f174]) ).
fof(f178,plain,
( s_e(sK0,sK2,sK4,sK6)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f88,f137]) ).
fof(f182,definition,
( spl8_12
<=> s_e(sK0,sK2,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition]) ).
fof(f184,plain,
( s_e(sK0,sK2,sK4,sK6)
| ~ spl8_12 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
( spl8_12
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f178,f135,f182]) ).
fof(f186,plain,
( s_t(sK4,sK5,sK6)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f89,f137]) ).
fof(f188,definition,
( spl8_13
<=> s_t(sK4,sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl8_13])],[avatar_definition]) ).
fof(f190,plain,
( s_t(sK4,sK5,sK6)
| ~ spl8_13 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,plain,
( spl8_13
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f186,f135,f188]) ).
fof(f192,plain,
( s_t(sK0,sK1,sK2)
| ~ spl8_5 ),
inference(unit_resulting_resolution,[],[f90,f137]) ).
fof(f194,definition,
( spl8_14
<=> s_t(sK0,sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition]) ).
fof(f196,plain,
( s_t(sK0,sK1,sK2)
| ~ spl8_14 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f197,plain,
( spl8_14
| ~ spl8_5 ),
inference(avatar_split_clause,[],[f192,f135,f194]) ).
fof(f198,plain,
( s_t(sK6,sK5,sK4)
| ~ spl8_13 ),
inference(unit_resulting_resolution,[],[f58,f190]) ).
fof(f201,definition,
( spl8_15
<=> s_t(sK6,sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f203,plain,
( s_t(sK6,sK5,sK4)
| ~ spl8_15 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,plain,
( spl8_15
| ~ spl8_13 ),
inference(avatar_split_clause,[],[f198,f188,f201]) ).
fof(f235,plain,
! [X2,X3,X0,X1] : s_e(X0,X1,X2,ext(X3,X2,X0,X1)),
inference(unit_resulting_resolution,[],[f104,f109,f46]) ).
fof(f237,plain,
( s_e(sK4,sK6,sK0,sK2)
| ~ spl8_12 ),
inference(unit_resulting_resolution,[],[f104,f184,f46]) ).
fof(f238,plain,
( s_e(sK4,sK7,sK0,sK3)
| ~ spl8_9 ),
inference(unit_resulting_resolution,[],[f104,f160,f46]) ).
fof(f239,plain,
( s_e(sK6,sK7,sK2,sK3)
| ~ spl8_11 ),
inference(unit_resulting_resolution,[],[f104,f176,f46]) ).
fof(f240,plain,
( ~ s_e(sK5,sK7,sK1,sK3)
| spl8_4 ),
inference(unit_resulting_resolution,[],[f104,f132,f46]) ).
fof(f261,definition,
( spl8_18
<=> s_e(sK4,sK6,sK0,sK2) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
fof(f263,plain,
( s_e(sK4,sK6,sK0,sK2)
| ~ spl8_18 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,plain,
( spl8_18
| ~ spl8_12 ),
inference(avatar_split_clause,[],[f237,f182,f261]) ).
fof(f266,definition,
( spl8_19
<=> s_e(sK4,sK7,sK0,sK3) ),
introduced(definition,[new_symbols(definition,[spl8_19])],[avatar_definition]) ).
fof(f268,plain,
( s_e(sK4,sK7,sK0,sK3)
| ~ spl8_19 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f269,plain,
( spl8_19
| ~ spl8_9 ),
inference(avatar_split_clause,[],[f238,f158,f266]) ).
fof(f271,definition,
( spl8_20
<=> s_e(sK6,sK7,sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl8_20])],[avatar_definition]) ).
fof(f273,plain,
( s_e(sK6,sK7,sK2,sK3)
| ~ spl8_20 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( spl8_20
| ~ spl8_11 ),
inference(avatar_split_clause,[],[f239,f174,f271]) ).
fof(f276,definition,
( spl8_21
<=> s_e(sK5,sK7,sK1,sK3) ),
introduced(definition,[new_symbols(definition,[spl8_21])],[avatar_definition]) ).
fof(f278,plain,
( ~ s_e(sK5,sK7,sK1,sK3)
| spl8_21 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( ~ spl8_21
| spl8_4 ),
inference(avatar_split_clause,[],[f240,f130,f276]) ).
fof(f301,plain,
! [X2,X3,X0,X1] : s_e(X0,X1,ext(X2,X3,X0,X1),X3),
inference(unit_resulting_resolution,[],[f104,f109,f105]) ).
fof(f319,plain,
! [X2,X3,X0,X1] : s_e(X0,ext(X1,X0,X2,X3),X3,X2),
inference(unit_resulting_resolution,[],[f48,f109,f105]) ).
fof(f434,plain,
( s_e(sK2,sK1,sK6,sK5)
| ~ spl8_10 ),
inference(unit_resulting_resolution,[],[f55,f168]) ).
fof(f446,definition,
( spl8_38
<=> s_e(sK2,sK1,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl8_38])],[avatar_definition]) ).
fof(f448,plain,
( s_e(sK2,sK1,sK6,sK5)
| ~ spl8_38 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f449,plain,
( spl8_38
| ~ spl8_10 ),
inference(avatar_split_clause,[],[f434,f166,f446]) ).
fof(f482,plain,
! [X2,X3,X0,X1] : s_t(ext(X0,X1,X2,X3),X1,X0),
inference(unit_resulting_resolution,[],[f58,f110]) ).
fof(f941,plain,
! [X2,X0,X1] :
( ~ s_t(X0,X1,X2)
| X0 = X1
| ~ s_t(X2,X0,X1) ),
inference(resolution,[],[f60,f58]) ).
fof(f958,definition,
( spl8_67
<=> sK5 = sK6 ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f959,plain,
( sK5 != sK6
| spl8_67 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f960,plain,
( sK5 = sK6
| ~ spl8_67 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f976,definition,
( spl8_71
<=> sK1 = sK2 ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f977,plain,
( sK1 != sK2
| spl8_71 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f978,plain,
( sK1 = sK2
| ~ spl8_71 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f1006,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ s_ifs(X2,X0,X1,X3,X4,X5,X5,X6)
| X0 = X1 ),
inference(resolution,[],[f108,f87]) ).
fof(f1008,plain,
! [X2,X3,X0,X1,X4] :
( ~ s_e(X2,X3,X4,X4)
| X0 = X1
| ~ s_e(X2,X3,X0,X1) ),
inference(resolution,[],[f108,f104]) ).
fof(f1044,plain,
( s_e(sK6,sK5,sK2,sK1)
| ~ spl8_38 ),
inference(unit_resulting_resolution,[],[f47,f448]) ).
fof(f1068,definition,
( spl8_79
<=> s_e(sK6,sK5,sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f1070,plain,
( s_e(sK6,sK5,sK2,sK1)
| ~ spl8_79 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1071,plain,
( spl8_79
| ~ spl8_38 ),
inference(avatar_split_clause,[],[f1044,f446,f1068]) ).
fof(f1268,plain,
( s_t(sK5,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK5)
| ~ spl8_15 ),
inference(unit_resulting_resolution,[],[f72,f203,f57,f203]) ).
fof(f1327,definition,
( spl8_100
<=> s_t(sK5,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK5) ),
introduced(definition,[new_symbols(definition,[spl8_100])],[avatar_definition]) ).
fof(f1329,plain,
( s_t(sK5,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK5)
| ~ spl8_100 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1330,plain,
( spl8_100
| ~ spl8_15 ),
inference(avatar_split_clause,[],[f1268,f201,f1327]) ).
fof(f1534,plain,
( s_t(sK6,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK4)
| ~ spl8_15 ),
inference(unit_resulting_resolution,[],[f73,f203,f57,f203]) ).
fof(f1573,definition,
( spl8_110
<=> s_t(sK6,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK4) ),
introduced(definition,[new_symbols(definition,[spl8_110])],[avatar_definition]) ).
fof(f1576,plain,
( spl8_110
| ~ spl8_15 ),
inference(avatar_split_clause,[],[f1534,f201,f1573]) ).
fof(f3151,definition,
( spl8_166
<=> s_t(sK4,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f3153,plain,
( ~ s_t(sK4,sK6,sK5)
| spl8_166 ),
inference(avatar_component_clause,[],[f3151]) ).
fof(f3318,plain,
( ~ s_t(sK6,sK5,sK6)
| spl8_166 ),
inference(unit_resulting_resolution,[],[f61,f57,f3153]) ).
fof(f3351,definition,
( spl8_182
<=> s_t(sK6,sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl8_182])],[avatar_definition]) ).
fof(f3354,plain,
( ~ spl8_182
| spl8_166 ),
inference(avatar_split_clause,[],[f3318,f3151,f3351]) ).
fof(f3756,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ s_t(X5,X1,X2)
| ~ s_e(X1,X2,X3,X4)
| ext(X0,X1,X3,X4) = X2
| X0 = X1
| ~ s_t(X5,X0,X1) ),
inference(resolution,[],[f53,f62]) ).
fof(f4146,plain,
( ! [X2,X3,X0,X1,X4] : ~ s_ifs(X0,sK1,sK2,X1,X2,X3,X3,X4)
| spl8_71 ),
inference(unit_resulting_resolution,[],[f1006,f977]) ).
fof(f5238,plain,
( ~ s_t(sK4,sK6,sK5)
| ~ spl8_15
| spl8_67 ),
inference(unit_resulting_resolution,[],[f941,f203,f959]) ).
fof(f5323,plain,
( s_ifs(sK0,sK1,sK2,sK3,sK4,sK5,sK5,sK7)
| ~ spl8_5
| ~ spl8_67 ),
inference(superposition,[],[f137,f960]) ).
fof(f5361,plain,
( $false
| ~ spl8_5
| ~ spl8_67
| spl8_71 ),
inference(forward_subsumption_resolution,[],[f5323,f4146]) ).
fof(f5362,plain,
( ~ spl8_5
| ~ spl8_67
| spl8_71 ),
inference(avatar_contradiction_clause,[],[f5361]) ).
fof(f5367,plain,
( ~ spl8_166
| ~ spl8_15
| spl8_67 ),
inference(avatar_split_clause,[],[f5238,f958,f201,f3151]) ).
fof(f5513,plain,
( ! [X0] : ~ s_e(sK2,sK1,X0,X0)
| ~ spl8_38
| spl8_67 ),
inference(unit_resulting_resolution,[],[f1008,f448,f959]) ).
fof(f11110,plain,
( sK1 != sK2
| sK5 != sK6
| s_e(sK1,sK3,sK5,sK7)
| ~ s_e(sK2,sK3,sK6,sK7) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f11147,plain,
( ! [X0] : ~ s_e(sK1,sK1,X0,X0)
| ~ spl8_38
| spl8_67
| ~ spl8_71 ),
inference(forward_demodulation,[],[f5513,f978]) ).
fof(f11192,plain,
( $false
| ~ spl8_38
| spl8_67
| ~ spl8_71 ),
inference(forward_subsumption_resolution,[],[f11147,f51]) ).
fof(f11193,plain,
( ~ spl8_38
| spl8_67
| ~ spl8_71 ),
inference(avatar_contradiction_clause,[],[f11192]) ).
fof(f11210,plain,
( ! [X0,X1] : ext(sK1,sK2,X0,X1) = ext(sK1,sK2,X1,X0)
| spl8_71 ),
inference(unit_resulting_resolution,[],[f53,f319,f110,f977]) ).
fof(f44732,plain,
( ! [X0,X1] : ext(sK0,sK2,X0,X1) = ext(sK1,sK2,X0,X1)
| ~ spl8_14
| spl8_71 ),
inference(unit_resulting_resolution,[],[f3756,f196,f977,f110,f109]) ).
fof(f44737,plain,
( ! [X0,X1] : ext(sK4,sK6,X0,X1) = ext(sK5,sK6,X0,X1)
| ~ spl8_13
| spl8_67 ),
inference(unit_resulting_resolution,[],[f3756,f190,f959,f110,f109]) ).
fof(f58895,plain,
( sK5 = crossbar(sK6,sK5,sK4,sK6,sK5,sK6)
| ~ spl8_100 ),
inference(resolution,[],[f1329,f106]) ).
fof(f58918,definition,
( spl8_1115
<=> sK5 = crossbar(sK6,sK5,sK4,sK6,sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl8_1115])],[avatar_definition]) ).
fof(f58939,plain,
( spl8_1115
| ~ spl8_100 ),
inference(avatar_split_clause,[],[f58895,f1327,f58918]) ).
fof(f65883,definition,
( spl8_1368
<=> sK4 = sK6 ),
introduced(definition,[new_symbols(definition,[spl8_1368])],[avatar_definition]) ).
fof(f65884,plain,
( sK4 != sK6
| spl8_1368 ),
inference(avatar_component_clause,[],[f65883]) ).
fof(f65910,plain,
( sK5 != crossbar(sK6,sK5,sK4,sK6,sK5,sK6)
| sK4 != sK6
| s_t(sK6,sK5,sK6)
| ~ s_t(sK6,crossbar(sK6,sK5,sK4,sK6,sK5,sK6),sK4) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f66244,plain,
( ! [X0,X1] : s_e(ext(sK4,sK6,X0,X1),sK7,ext(sK0,sK2,sK6,ext(sK4,sK6,X0,X1)),sK3)
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_1368 ),
inference(unit_resulting_resolution,[],[f107,f268,f273,f263,f110,f235,f110,f65884]) ).
fof(f68107,plain,
( ! [X0,X1] : s_e(ext(sK4,sK6,X0,X1),sK7,ext(sK1,sK2,sK6,ext(sK4,sK6,X0,X1)),sK3)
| ~ spl8_14
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_71
| spl8_1368 ),
inference(forward_demodulation,[],[f66244,f44732]) ).
fof(f68993,plain,
( ! [X0,X1] : s_e(ext(sK5,sK6,X0,X1),sK7,ext(sK1,sK2,sK6,ext(sK5,sK6,X0,X1)),sK3)
| ~ spl8_13
| ~ spl8_14
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_67
| spl8_71
| spl8_1368 ),
inference(forward_demodulation,[],[f68107,f44737]) ).
fof(f84480,plain,
( ~ s_e(ext(sK5,sK6,alpha,gamma),sK7,ext(sK1,sK2,ext(sK5,sK6,alpha,gamma),sK6),sK3)
| ~ spl8_20
| spl8_21
| ~ spl8_79 ),
inference(unit_resulting_resolution,[],[f107,f71,f482,f301,f482,f273,f1070,f278]) ).
fof(f84509,plain,
( ~ s_e(ext(sK5,sK6,alpha,gamma),sK7,ext(sK1,sK2,sK6,ext(sK5,sK6,alpha,gamma)),sK3)
| ~ spl8_20
| spl8_21
| spl8_71
| ~ spl8_79 ),
inference(forward_demodulation,[],[f84480,f11210]) ).
fof(f84512,plain,
( $false
| ~ spl8_13
| ~ spl8_14
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_21
| spl8_67
| spl8_71
| ~ spl8_79
| spl8_1368 ),
inference(forward_subsumption_resolution,[],[f84509,f68993]) ).
fof(f84513,plain,
( ~ spl8_13
| ~ spl8_14
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_21
| spl8_67
| spl8_71
| ~ spl8_79
| spl8_1368 ),
inference(avatar_contradiction_clause,[],[f84512]) ).
cnf(s4,plain,
~ spl8_4,
inference(sat_conversion,[],[f133]) ).
cnf(s5,plain,
spl8_5,
inference(sat_conversion,[],[f138]) ).
cnf(s9,plain,
( ~ spl8_5
| spl8_9 ),
inference(sat_conversion,[],[f161]) ).
cnf(s10,plain,
( ~ spl8_5
| spl8_10 ),
inference(sat_conversion,[],[f169]) ).
cnf(s11,plain,
( ~ spl8_5
| spl8_11 ),
inference(sat_conversion,[],[f177]) ).
cnf(s12,plain,
( ~ spl8_5
| spl8_12 ),
inference(sat_conversion,[],[f185]) ).
cnf(s13,plain,
( ~ spl8_5
| spl8_13 ),
inference(sat_conversion,[],[f191]) ).
cnf(s14,plain,
( ~ spl8_5
| spl8_14 ),
inference(sat_conversion,[],[f197]) ).
cnf(s15,plain,
( ~ spl8_13
| spl8_15 ),
inference(sat_conversion,[],[f204]) ).
cnf(s18,plain,
( ~ spl8_12
| spl8_18 ),
inference(sat_conversion,[],[f264]) ).
cnf(s19,plain,
( ~ spl8_9
| spl8_19 ),
inference(sat_conversion,[],[f269]) ).
cnf(s20,plain,
( ~ spl8_11
| spl8_20 ),
inference(sat_conversion,[],[f274]) ).
cnf(s21,plain,
( spl8_4
| ~ spl8_21 ),
inference(sat_conversion,[],[f279]) ).
cnf(s43,plain,
( ~ spl8_10
| spl8_38 ),
inference(sat_conversion,[],[f449]) ).
cnf(s81,plain,
( ~ spl8_38
| spl8_79 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s113,plain,
( ~ spl8_15
| spl8_100 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s133,plain,
( ~ spl8_15
| spl8_110 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s209,plain,
( spl8_166
| ~ spl8_182 ),
inference(sat_conversion,[],[f3354]) ).
cnf(s275,plain,
( ~ spl8_5
| ~ spl8_67
| spl8_71 ),
inference(sat_conversion,[],[f5362]) ).
cnf(s281,plain,
( ~ spl8_15
| spl8_67
| ~ spl8_166 ),
inference(sat_conversion,[],[f5367]) ).
cnf(s314,plain,
( spl8_4
| ~ spl8_11
| ~ spl8_67
| ~ spl8_71 ),
inference(sat_conversion,[],[f11110]) ).
cnf(s348,plain,
( ~ spl8_38
| spl8_67
| ~ spl8_71 ),
inference(sat_conversion,[],[f11193]) ).
cnf(s2398,plain,
( ~ spl8_100
| spl8_1115 ),
inference(sat_conversion,[],[f58939]) ).
cnf(s3126,plain,
( ~ spl8_110
| spl8_182
| ~ spl8_1115
| ~ spl8_1368 ),
inference(sat_conversion,[],[f65910]) ).
cnf(s4020,plain,
( ~ spl8_13
| ~ spl8_14
| ~ spl8_18
| ~ spl8_19
| ~ spl8_20
| spl8_21
| spl8_67
| spl8_71
| ~ spl8_79
| spl8_1368 ),
inference(sat_conversion,[],[f84513]) ).
cnf(s4031,plain,
spl8_14,
inference(rat,[],[s14,s5]) ).
cnf(s4032,plain,
spl8_13,
inference(rat,[],[s13,s5]) ).
cnf(s4033,plain,
spl8_12,
inference(rat,[],[s12,s5]) ).
cnf(s4034,plain,
spl8_11,
inference(rat,[],[s11,s5]) ).
cnf(s4035,plain,
spl8_10,
inference(rat,[],[s10,s5]) ).
cnf(s4036,plain,
spl8_9,
inference(rat,[],[s9,s5]) ).
cnf(s4097,plain,
spl8_15,
inference(rat,[],[s15,s4032]) ).
cnf(s4110,plain,
spl8_18,
inference(rat,[],[s18,s4033]) ).
cnf(s4123,plain,
spl8_20,
inference(rat,[],[s20,s4034]) ).
cnf(s4139,plain,
spl8_38,
inference(rat,[],[s43,s4035]) ).
cnf(s4162,plain,
spl8_19,
inference(rat,[],[s19,s4036]) ).
cnf(s4256,plain,
spl8_110,
inference(rat,[],[s133,s4097]) ).
cnf(s4259,plain,
spl8_100,
inference(rat,[],[s113,s4097]) ).
cnf(s4385,plain,
spl8_79,
inference(rat,[],[s81,s4139]) ).
cnf(s4718,plain,
spl8_1115,
inference(rat,[],[s2398,s4259]) ).
cnf(s4830,plain,
~ spl8_21,
inference(rat,[],[s21,s4]) ).
cnf(s4837,plain,
spl8_67,
inference(rat,[],[s3126,s209,s4020,s281,s348,s4256,s4718,s4031,s4032,s4123,s4110,s4162,s4830,s4385,s4097,s4139]) ).
cnf(s4838,plain,
spl8_71,
inference(rat,[],[s275,s5,s4837]) ).
cnf(s4844,plain,
$false,
inference(rat,[],[s314,s4,s4034,s4838,s4837]) ).
fof(f84514,plain,
$false,
inference(avatar_sat_refutation,[],[s4844]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO490+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n015.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 08:24:30 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 11.38/2.59 % (1345813)Detected formulas, will run a generic FOF schedule.
% 11.38/2.59 % (1345818)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=310161904:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.38/2.59 % (1345822)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3639215486:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.38/2.59 % (1345820)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=434219331:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.38/2.59 % (1345819)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=1620598587:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.38/2.59 % (1345821)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2034057920:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.38/2.59 % (1345824)dis-21_1_sil=8000:lcm=predicate:random_seed=4251919172:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.38/2.59 % (1345823)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3534688217:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.38/2.59 % (1345821)Refutation not found, incomplete strategy
% 11.38/2.59 % (1345821)------------------------------
% 11.38/2.59 % (1345821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.38/2.59 % (1345821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.38/2.59 % (1345821)CaDiCaL version: 2.1.3
% 11.38/2.59 % (1345821)Termination reason: Refutation not found, incomplete strategy
% 11.38/2.59 % (1345821)Time elapsed: 0.014 s
% 11.38/2.59 % (1345821)Peak memory usage: 88 MB
% 11.38/2.59 % (1345821)Instructions burned: 23 (million)
% 11.38/2.59 % (1345822)Instruction limit reached!
% 11.38/2.59 % (1345822)------------------------------
% 11.38/2.59 % (1345822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.38/2.59 % (1345822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.38/2.59 % (1345822)CaDiCaL version: 2.1.3
% 11.38/2.59 % (1345822)Termination reason: Instruction limit
% 11.38/2.59 % (1345822)Termination phase: Saturation
% 11.38/2.59 % (1345822)Time elapsed: 0.062 s
% 11.38/2.59 % (1345822)Peak memory usage: 88 MB
% 11.38/2.59 % (1345822)Instructions burned: 119 (million)
% 11.38/2.59 % (1345824)Instruction limit reached!
% 11.38/2.59 % (1345824)------------------------------
% 11.38/2.59 % (1345824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.38/2.59 % (1345824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.38/2.59 % (1345824)CaDiCaL version: 2.1.3
% 11.38/2.59 % (1345824)Termination reason: Instruction limit
% 11.38/2.59 % (1345824)Termination phase: Saturation
% 11.38/2.59 % (1345824)Time elapsed: 0.073 s
% 11.38/2.59 % (1345824)Peak memory usage: 88 MB
% 11.38/2.59 % (1345824)Instructions burned: 129 (million)
% 11.38/2.59 % (1345823)Instruction limit reached!
% 11.38/2.59 % (1345823)------------------------------
% 11.38/2.59 % (1345823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.38/2.59 % (1345823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.38/2.59 % (1345823)CaDiCaL version: 2.1.3
% 11.38/2.59 % (1345823)Termination reason: Instruction limit
% 11.38/2.59 % (1345823)Termination phase: Saturation
% 11.38/2.59 % (1345823)Time elapsed: 0.089 s
% 11.38/2.59 % (1345823)Peak memory usage: 89 MB
% 11.38/2.59 % (1345823)Instructions burned: 140 (million)
% 11.38/2.59 % (1345832)lrs+10_1_sil=8000:sp=occurrence:random_seed=4206845336:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.38/2.59 % (1345833)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3705465506:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.38/2.59 % (1345832)Refutation not found, incomplete strategy
% 11.38/2.59 % (1345832)------------------------------
% 11.38/2.59 % (1345832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.38/2.59 % (1345832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.38/2.59 % (1345832)CaDiCaL version: 2.1.3
% 11.38/2.59 % (1345832)Termination reason: Refutation not found, incomplete strategy
% 19.42/3.70 % (1345832)Time elapsed: 0.018 s
% 19.42/3.70 % (1345832)Peak memory usage: 89 MB
% 19.42/3.70 % (1345832)Instructions burned: 30 (million)
% 19.42/3.70 % (1345833)Refutation not found, incomplete strategy
% 19.42/3.70 % (1345833)------------------------------
% 19.42/3.70 % (1345833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/3.70 % (1345833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/3.70 % (1345833)CaDiCaL version: 2.1.3
% 19.42/3.70 % (1345833)Termination reason: Refutation not found, incomplete strategy
% 19.42/3.70 % (1345833)Time elapsed: 0.026 s
% 19.42/3.70 % (1345833)Peak memory usage: 88 MB
% 19.42/3.70 % (1345833)Instructions burned: 47 (million)
% 19.42/3.70 % (1345834)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3292572760:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.42/3.70 % (1345821)------------------------------
% 19.42/3.70 % (1345821)------------------------------
% 19.42/3.70 % (1345838)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=562073508:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.42/3.70 % (1345834)Instruction limit reached!
% 19.42/3.70 % (1345834)------------------------------
% 19.42/3.70 % (1345834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/3.70 % (1345834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/3.70 % (1345834)CaDiCaL version: 2.1.3
% 19.42/3.70 % (1345834)Termination reason: Instruction limit
% 19.42/3.70 % (1345834)Termination phase: Saturation
% 19.42/3.70 % (1345834)Time elapsed: 0.196 s
% 19.42/3.70 % (1345834)Peak memory usage: 90 MB
% 19.42/3.70 % (1345834)Instructions burned: 325 (million)
% 19.42/3.70 % (1345832)------------------------------
% 19.42/3.70 % (1345832)------------------------------
% 19.42/3.70 % (1345833)------------------------------
% 19.42/3.70 % (1345833)------------------------------
% 19.42/3.70 % (1345838)Instruction limit reached!
% 19.42/3.70 % (1345838)------------------------------
% 19.42/3.70 % (1345838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/3.70 % (1345838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/3.70 % (1345838)CaDiCaL version: 2.1.3
% 19.42/3.70 % (1345838)Termination reason: Instruction limit
% 19.42/3.70 % (1345838)Termination phase: Saturation
% 19.42/3.70 % (1345838)Time elapsed: 0.123 s
% 19.42/3.70 % (1345838)Peak memory usage: 90 MB
% 19.42/3.70 % (1345838)Instructions burned: 250 (million)
% 19.42/3.70 % (1345840)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3530301901:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 19.42/3.70 % (1345841)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3715266346:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 19.42/3.70 % (1345842)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2361853262:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 19.42/3.70 % (1345843)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1718554461:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.42/3.70 % (1345842)Instruction limit reached!
% 19.42/3.70 % (1345842)------------------------------
% 19.42/3.70 % (1345842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/3.70 % (1345842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/3.70 % (1345842)CaDiCaL version: 2.1.3
% 19.42/3.70 % (1345842)Termination reason: Instruction limit
% 19.42/3.70 % (1345842)Termination phase: Saturation
% 19.42/3.70 % (1345842)Time elapsed: 0.062 s
% 19.42/3.70 % (1345842)Peak memory usage: 89 MB
% 19.42/3.70 % (1345842)Instructions burned: 114 (million)
% 19.42/3.70 % (1345840)Instruction limit reached!
% 19.42/3.70 % (1345840)------------------------------
% 19.42/3.70 % (1345840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.42/3.70 % (1345840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.42/3.70 % (1345840)CaDiCaL version: 2.1.3
% 19.42/3.70 % (1345840)Termination reason: Instruction limit
% 19.42/3.70 % (1345840)Termination phase: Saturation
% 19.42/3.70 % (1345840)Time elapsed: 0.159 s
% 19.42/3.70 % (1345840)Peak memory usage: 88 MB
% 19.42/3.70 % (1345840)Instructions burned: 295 (million)
% 19.42/3.70 % (1345843)Instruction limit reached!
% 19.42/3.70 % (1345843)------------------------------
% 19.42/3.70 % (1345843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345843)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345843)Termination reason: Instruction limit
% 44.11/7.13 % (1345843)Termination phase: Saturation
% 44.11/7.13 % (1345843)Time elapsed: 0.068 s
% 44.11/7.13 % (1345843)Peak memory usage: 89 MB
% 44.11/7.13 % (1345843)Instructions burned: 128 (million)
% 44.11/7.13 % (1345850)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2256783561:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 44.11/7.13 % (1345851)lrs+10_1_sil=8000:sp=occurrence:random_seed=317537765:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 44.11/7.13 % (1345852)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1524804436:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 44.11/7.13 % (1345851)Refutation not found, incomplete strategy
% 44.11/7.13 % (1345851)------------------------------
% 44.11/7.13 % (1345851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345851)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345851)Termination reason: Refutation not found, incomplete strategy
% 44.11/7.13 % (1345851)Time elapsed: 0.018 s
% 44.11/7.13 % (1345851)Peak memory usage: 89 MB
% 44.11/7.13 % (1345851)Instructions burned: 30 (million)
% 44.11/7.13 % (1345850)Instruction limit reached!
% 44.11/7.13 % (1345850)------------------------------
% 44.11/7.13 % (1345850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345850)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345850)Termination reason: Instruction limit
% 44.11/7.13 % (1345850)Termination phase: Saturation
% 44.11/7.13 % (1345850)Time elapsed: 0.062 s
% 44.11/7.13 % (1345850)Peak memory usage: 89 MB
% 44.11/7.13 % (1345850)Instructions burned: 114 (million)
% 44.11/7.13 % (1345856)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=948134677:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 44.11/7.13 % (1345851)------------------------------
% 44.11/7.13 % (1345851)------------------------------
% 44.11/7.13 % (1345852)Instruction limit reached!
% 44.11/7.13 % (1345852)------------------------------
% 44.11/7.13 % (1345852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345852)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345852)Termination reason: Instruction limit
% 44.11/7.13 % (1345852)Termination phase: Saturation
% 44.11/7.13 % (1345852)Time elapsed: 0.256 s
% 44.11/7.13 % (1345852)Peak memory usage: 91 MB
% 44.11/7.13 % (1345852)Instructions burned: 437 (million)
% 44.11/7.13 % (1345859)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2384224743:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 44.11/7.13 % (1345858)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2348295724:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 44.11/7.13 % (1345858)Instruction limit reached!
% 44.11/7.13 % (1345858)------------------------------
% 44.11/7.13 % (1345858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345858)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345858)Termination reason: Instruction limit
% 44.11/7.13 % (1345858)Termination phase: Saturation
% 44.11/7.13 % (1345858)Time elapsed: 0.069 s
% 44.11/7.13 % (1345858)Peak memory usage: 89 MB
% 44.11/7.13 % (1345858)Instructions burned: 135 (million)
% 44.11/7.13 % (1345862)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=867203746:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 44.11/7.13 % (1345859)Instruction limit reached!
% 44.11/7.13 % (1345859)------------------------------
% 44.11/7.13 % (1345859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.11/7.13 % (1345859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.11/7.13 % (1345859)CaDiCaL version: 2.1.3
% 44.11/7.13 % (1345859)Termination reason: Instruction limit
% 44.11/7.13 % (1345859)Termination phase: Saturation
% 44.11/7.13 % (1345859)Time elapsed: 0.346 s
% 76.56/11.74 % (1345859)Peak memory usage: 95 MB
% 76.56/11.74 % (1345859)Instructions burned: 592 (million)
% 76.56/11.74 % (1345864)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=3736074644:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 76.56/11.74 % (1345864)Instruction limit reached!
% 76.56/11.74 % (1345864)------------------------------
% 76.56/11.74 % (1345864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.56/11.74 % (1345864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.56/11.74 % (1345864)CaDiCaL version: 2.1.3
% 76.56/11.74 % (1345864)Termination reason: Instruction limit
% 76.56/11.74 % (1345864)Termination phase: Saturation
% 76.56/11.74 % (1345864)Time elapsed: 0.071 s
% 76.56/11.74 % (1345864)Peak memory usage: 89 MB
% 76.56/11.74 % (1345864)Instructions burned: 125 (million)
% 76.56/11.74 % (1345866)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3579617166:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 76.56/11.74 % (1345866)Instruction limit reached!
% 76.56/11.74 % (1345866)------------------------------
% 76.56/11.74 % (1345866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.56/11.74 % (1345866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.56/11.74 % (1345866)CaDiCaL version: 2.1.3
% 76.56/11.74 % (1345866)Termination reason: Instruction limit
% 76.56/11.74 % (1345866)Termination phase: Saturation
% 76.56/11.74 % (1345866)Time elapsed: 0.085 s
% 76.56/11.74 % (1345866)Peak memory usage: 90 MB
% 76.56/11.74 % (1345866)Instructions burned: 135 (million)
% 76.56/11.74 % (1345841)Instruction limit reached!
% 76.56/11.74 % (1345841)------------------------------
% 76.56/11.74 % (1345841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.56/11.74 % (1345841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.56/11.74 % (1345841)CaDiCaL version: 2.1.3
% 76.56/11.74 % (1345841)Termination reason: Instruction limit
% 76.56/11.74 % (1345841)Termination phase: Saturation
% 76.56/11.74 % (1345841)Time elapsed: 1.490 s
% 76.56/11.74 % (1345841)Peak memory usage: 141 MB
% 76.56/11.74 % (1345841)Instructions burned: 2351 (million)
% 76.56/11.74 % (1345868)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3805898036:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 76.56/11.74 % (1345868)Refutation not found, incomplete strategy
% 76.56/11.74 % (1345868)------------------------------
% 76.56/11.74 % (1345868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.56/11.74 % (1345868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.56/11.74 % (1345868)CaDiCaL version: 2.1.3
% 76.56/11.74 % (1345868)Termination reason: Refutation not found, incomplete strategy
% 76.56/11.74 % (1345868)Time elapsed: 0.014 s
% 76.56/11.74 % (1345868)Peak memory usage: 88 MB
% 76.56/11.74 % (1345868)Instructions burned: 23 (million)
% 76.56/11.74 % (1345869)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=486986485:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 76.56/11.74 % (1345868)------------------------------
% 76.56/11.74 % (1345868)------------------------------
% 76.56/11.74 % (1345869)Instruction limit reached!
% 76.56/11.74 % (1345869)------------------------------
% 76.56/11.74 % (1345869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.56/11.74 % (1345869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.56/11.74 % (1345869)CaDiCaL version: 2.1.3
% 76.56/11.74 % (1345869)Termination reason: Instruction limit
% 76.56/11.74 % (1345869)Termination phase: Saturation
% 76.56/11.74 % (1345869)Time elapsed: 0.252 s
% 76.56/11.74 % (1345869)Peak memory usage: 92 MB
% 76.56/11.74 % (1345869)Instructions burned: 431 (million)
% 76.56/11.74 % (1345872)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=1719215363:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 76.56/11.74 % (1345873)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=3564146242:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 76.56/11.74 % (1345873)Instruction limit reached!
% 76.56/11.74 % (1345873)------------------------------
% 83.59/12.69 % (1345873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345873)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345873)Termination reason: Instruction limit
% 83.59/12.69 % (1345873)Termination phase: Saturation
% 83.59/12.69 % (1345873)Time elapsed: 0.083 s
% 83.59/12.69 % (1345873)Peak memory usage: 90 MB
% 83.59/12.69 % (1345873)Instructions burned: 150 (million)
% 83.59/12.69 % (1345876)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1791719741:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 83.59/12.69 % (1345856)Instruction limit reached!
% 83.59/12.69 % (1345856)------------------------------
% 83.59/12.69 % (1345856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345856)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345856)Termination reason: Instruction limit
% 83.59/12.69 % (1345856)Termination phase: Saturation
% 83.59/12.69 % (1345856)Time elapsed: 3.450 s
% 83.59/12.69 % (1345856)Peak memory usage: 154 MB
% 83.59/12.69 % (1345856)Instructions burned: 5202 (million)
% 83.59/12.69 % (1345878)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2849490273:i=667:av=off:fsr=off_2954 on theBenchmark for (2954ds/667Mi)
% 83.59/12.69 % (1345878)Instruction limit reached!
% 83.59/12.69 % (1345878)------------------------------
% 83.59/12.69 % (1345878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345878)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345878)Termination reason: Instruction limit
% 83.59/12.69 % (1345878)Termination phase: Saturation
% 83.59/12.69 % (1345878)Time elapsed: 0.330 s
% 83.59/12.69 % (1345878)Peak memory usage: 90 MB
% 83.59/12.69 % (1345878)Instructions burned: 669 (million)
% 83.59/12.69 % (1345880)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1697120360:s2a=on:i=185:s2at=1.8:fdi=4_2949 on theBenchmark for (2949ds/185Mi)
% 83.59/12.69 % (1345880)Instruction limit reached!
% 83.59/12.69 % (1345880)------------------------------
% 83.59/12.69 % (1345880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345880)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345880)Termination reason: Instruction limit
% 83.59/12.69 % (1345880)Termination phase: Saturation
% 83.59/12.69 % (1345880)Time elapsed: 0.098 s
% 83.59/12.69 % (1345880)Peak memory usage: 90 MB
% 83.59/12.69 % (1345880)Instructions burned: 187 (million)
% 83.59/12.69 % (1345882)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=953106952:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2946 on theBenchmark for (2946ds/193Mi)
% 83.59/12.69 % (1345882)Refutation not found, incomplete strategy
% 83.59/12.69 % (1345882)------------------------------
% 83.59/12.69 % (1345882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345882)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345882)Termination reason: Refutation not found, incomplete strategy
% 83.59/12.69 % (1345882)Time elapsed: 0.021 s
% 83.59/12.69 % (1345882)Peak memory usage: 89 MB
% 83.59/12.69 % (1345882)Instructions burned: 35 (million)
% 83.59/12.69 % (1345882)------------------------------
% 83.59/12.69 % (1345882)------------------------------
% 83.59/12.69 % (1345884)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3178002382:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2943 on theBenchmark for (2943ds/4850Mi)
% 83.59/12.69 % (1345872)Instruction limit reached!
% 83.59/12.69 % (1345872)------------------------------
% 83.59/12.69 % (1345872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.69 % (1345872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.69 % (1345872)CaDiCaL version: 2.1.3
% 83.59/12.69 % (1345872)Termination reason: Instruction limit
% 83.59/12.69 % (1345872)Termination phase: Saturation
% 83.59/12.69 % (1345872)Time elapsed: 3.470 s
% 83.59/12.69 % (1345872)Peak memory usage: 157 MB
% 83.59/12.69 % (1345872)Instructions burned: 6060 (million)
% 83.59/12.69 % (1345886)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3470272079:i=12111:sd=1:ss=included_2938 on theBenchmark for (2938ds/12111Mi)
% 83.59/12.70 % (1345884)Instruction limit reached!
% 83.59/12.70 % (1345884)------------------------------
% 83.59/12.70 % (1345884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345884)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345884)Termination reason: Instruction limit
% 83.59/12.70 % (1345884)Termination phase: Saturation
% 83.59/12.70 % (1345884)Time elapsed: 2.811 s
% 83.59/12.70 % (1345884)Peak memory usage: 117 MB
% 83.59/12.70 % (1345884)Instructions burned: 4850 (million)
% 83.59/12.70 % (1345888)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=379471598:i=319:kws=precedence:fsr=off_2913 on theBenchmark for (2913ds/319Mi)
% 83.59/12.70 % (1345888)Instruction limit reached!
% 83.59/12.70 % (1345888)------------------------------
% 83.59/12.70 % (1345888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345888)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345888)Termination reason: Instruction limit
% 83.59/12.70 % (1345888)Termination phase: Saturation
% 83.59/12.70 % (1345888)Time elapsed: 0.179 s
% 83.59/12.70 % (1345888)Peak memory usage: 91 MB
% 83.59/12.70 % (1345888)Instructions burned: 320 (million)
% 83.59/12.70 % (1345890)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3644517224:i=2064:ep=RST_2910 on theBenchmark for (2910ds/2064Mi)
% 83.59/12.70 % (1345862)Instruction limit reached!
% 83.59/12.70 % (1345862)------------------------------
% 83.59/12.70 % (1345862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345862)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345862)Termination reason: Instruction limit
% 83.59/12.70 % (1345862)Termination phase: Saturation
% 83.59/12.70 % (1345862)Time elapsed: 8.168 s
% 83.59/12.70 % (1345862)Peak memory usage: 217 MB
% 83.59/12.70 % (1345862)Instructions burned: 13194 (million)
% 83.59/12.70 % (1345892)dis-1011_128_sil=32000:random_seed=526383423:i=3706:ep=RST:av=off_2902 on theBenchmark for (2902ds/3706Mi)
% 83.59/12.70 % (1345890)Instruction limit reached!
% 83.59/12.70 % (1345890)------------------------------
% 83.59/12.70 % (1345890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345890)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345890)Termination reason: Instruction limit
% 83.59/12.70 % (1345890)Termination phase: Saturation
% 83.59/12.70 % (1345890)Time elapsed: 1.118 s
% 83.59/12.70 % (1345890)Peak memory usage: 100 MB
% 83.59/12.70 % (1345890)Instructions burned: 2065 (million)
% 83.59/12.70 % (1345894)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=989054291:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2897 on theBenchmark for (2897ds/757Mi)
% 83.59/12.70 % (1345876)Instruction limit reached!
% 83.59/12.70 % (1345876)------------------------------
% 83.59/12.70 % (1345876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345876)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345876)Termination reason: Instruction limit
% 83.59/12.70 % (1345876)Termination phase: Saturation
% 83.59/12.70 % (1345876)Time elapsed: 7.767 s
% 83.59/12.70 % (1345876)Peak memory usage: 196 MB
% 83.59/12.70 % (1345876)Instructions burned: 14156 (million)
% 83.59/12.70 % (1345894)Instruction limit reached!
% 83.59/12.70 % (1345894)------------------------------
% 83.59/12.70 % (1345894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345894)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345894)Termination reason: Instruction limit
% 83.59/12.70 % (1345894)Termination phase: Saturation
% 83.59/12.70 % (1345894)Time elapsed: 0.518 s
% 83.59/12.70 % (1345894)Peak memory usage: 105 MB
% 83.59/12.70 % (1345894)Instructions burned: 758 (million)
% 83.59/12.70 % (1345896)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2531384116:i=13913:ss=axioms:sgt=8_2892 on theBenchmark for (2892ds/13913Mi)
% 83.59/12.70 % (1345897)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=50130752:i=9925:aac=none_2891 on theBenchmark for (2891ds/9925Mi)
% 83.59/12.70 % (1345886)First to succeed.
% 83.59/12.70 % (1345886)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1345813"
% 83.59/12.70 % (1345896)Refutation not found, incomplete strategy
% 83.59/12.70 % (1345896)------------------------------
% 83.59/12.70 % (1345896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345896)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345896)Termination reason: Refutation not found, incomplete strategy
% 83.59/12.70 % (1345896)Time elapsed: 0.669 s
% 83.59/12.70 % (1345896)Peak memory usage: 129 MB
% 83.59/12.70 % (1345896)Instructions burned: 1014 (million)
% 83.59/12.70 % (1345892)Instruction limit reached!
% 83.59/12.70 % (1345892)------------------------------
% 83.59/12.70 % (1345892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.59/12.70 % (1345892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.59/12.70 % (1345892)CaDiCaL version: 2.1.3
% 83.59/12.70 % (1345892)Termination reason: Instruction limit
% 83.59/12.70 % (1345892)Termination phase: Saturation
% 83.59/12.70 % (1345892)Time elapsed: 1.756 s
% 83.59/12.70 % (1345892)Peak memory usage: 103 MB
% 83.59/12.70 % (1345892)Instructions burned: 3707 (million)
% 83.59/12.70 % (1345900)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=678837498:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2883 on theBenchmark for (2883ds/2479Mi)
% 83.59/12.70 % (1345896)------------------------------
% 83.59/12.70 % (1345896)------------------------------
% 83.59/12.70 % (1345886)Refutation found. Thanks to Tanya!
% 83.59/12.70 % SZS status Theorem for theBenchmark
% 83.59/12.70 % SZS output start Proof for theBenchmark
% See solution above
% 84.40/12.90 % (1345886)------------------------------
% 84.40/12.90 % (1345886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.40/12.90 % (1345886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.40/12.90 % (1345886)CaDiCaL version: 2.1.3
% 84.40/12.90 % (1345886)Termination reason: Refutation
% 84.40/12.90 % (1345886)Time elapsed: 5.275 s
% 84.40/12.90 % (1345886)Peak memory usage: 187 MB
% 84.40/12.90 % (1345886)Instructions burned: 9643 (million)
% 84.40/12.90 % (1345886)------------------------------
% 84.40/12.90 % (1345886)------------------------------
% 84.40/12.90 % (1345813)Success in time 11.825 s
% 84.40/12.90 % Vampire exiting
%------------------------------------------------------------------------------