%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT359+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 11:47:19 AM UTC 2026
% Result : Theorem 100.17s 22.91s
% Output : Refutation 147.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 40
% Syntax : Number of formulae : 180 ( 42 unt; 25 def)
% Number of atoms : 520 ( 77 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 606 ( 266 ~; 252 |; 39 &)
% ( 31 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 22 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 156 ( 0 sgn 148 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f68,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f431,axiom,
! [X0,X1,X2,X3] :
( r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))
<=> ( r2_hidden(X0,X2)
& r2_hidden(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t106_zfmisc_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f694,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_relat_1(k1_xboole_0)
& v3_relat_1(k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(f932,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] :
( ( r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) ) )
& ( ~ r2_hidden(X1,k1_relat_1(X0))
=> ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f2384,axiom,
! [X0] :
( ( v1_relat_1(X0)
& v1_funct_1(X0) )
=> ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_binop_1) ).
fof(f8084,axiom,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
=> ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pboole) ).
fof(f8263,axiom,
! [X0,X1] :
( m1_pboole(X1,X0)
=> ( v1_relat_1(X1)
& v1_funct_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_pboole) ).
fof(f36090,axiom,
! [X0] :
( l1_altcat_1(X0)
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_altcat_1(X0,X1,X2) = k1_binop_1(u1_altcat_1(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_altcat_1) ).
fof(f36134,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f36148,axiom,
! [X0] :
( l1_altcat_1(X0)
=> m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_altcat_1) ).
fof(f55706,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_altcat_1(X0) )
=> ! [X1,X2,X3] :
~ ( r2_hidden(X3,k1_binop_1(u1_altcat_1(X0),X1,X2))
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X0))
=> ~ ( X4 = X1
& X5 = X2
& r2_hidden(X3,k1_altcat_1(X0,X4,X5))
& m1_subset_1(X3,k1_altcat_1(X0,X4,X5)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_waybel34) ).
fof(f55707,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& l2_altcat_1(X0) )
=> ! [X1,X2,X3] :
~ ( r2_hidden(X3,k1_binop_1(u1_altcat_1(X0),X1,X2))
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X0))
=> ~ ( X4 = X1
& X5 = X2
& r2_hidden(X3,k1_altcat_1(X0,X4,X5))
& m1_subset_1(X3,k1_altcat_1(X0,X4,X5)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f55706]) ).
fof(f55743,plain,
? [X0] :
( ? [X1,X2,X3] :
( r2_hidden(X3,k1_binop_1(u1_altcat_1(X0),X1,X2))
& ! [X4] :
( ! [X5] :
( X1 != X4
| X2 != X5
| ~ r2_hidden(X3,k1_altcat_1(X0,X4,X5))
| ~ m1_subset_1(X3,k1_altcat_1(X0,X4,X5))
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
& ~ v3_struct_0(X0)
& l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f55707]) ).
fof(f55744,plain,
? [X0] :
( ? [X1,X2,X3] :
( r2_hidden(X3,k1_binop_1(u1_altcat_1(X0),X1,X2))
& ! [X4] :
( ! [X5] :
( X1 != X4
| X2 != X5
| ~ r2_hidden(X3,k1_altcat_1(X0,X4,X5))
| ~ m1_subset_1(X3,k1_altcat_1(X0,X4,X5))
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
& ~ v3_struct_0(X0)
& l2_altcat_1(X0) ),
inference(flattening,[],[f55743]) ).
fof(f55751,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f55753,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f68]) ).
fof(f55765,plain,
! [X0] :
( ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f2384]) ).
fof(f55766,plain,
! [X0] :
( ! [X1,X2] : k1_binop_1(X0,X1,X2) = k1_funct_1(X0,k4_tarski(X1,X2))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f55765]) ).
fof(f55772,plain,
! [X0] :
( m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f36148]) ).
fof(f55773,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_altcat_1(X0,X1,X2) = k1_binop_1(u1_altcat_1(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f36090]) ).
fof(f55813,plain,
! [X0,X1] :
( ( v1_relat_1(X1)
& v1_funct_1(X1) )
| ~ m1_pboole(X1,X0) ),
inference(ennf_transformation,[],[f8263]) ).
fof(f55817,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(ennf_transformation,[],[f8084]) ).
fof(f55818,plain,
! [X0,X1] :
( ( m1_pboole(X1,X0)
<=> k1_relat_1(X1) = X0 )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(flattening,[],[f55817]) ).
fof(f55870,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(ennf_transformation,[],[f932]) ).
fof(f55871,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = k1_funct_1(X0,X1)
<=> r2_hidden(k4_tarski(X1,X2),X0) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( X2 = k1_funct_1(X0,X1)
<=> X2 = k1_xboole_0 )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(flattening,[],[f55870]) ).
fof(f55936,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f36134]) ).
fof(f56543,plain,
( r2_hidden(sK16,k1_binop_1(u1_altcat_1(sK13),sK14,sK15))
& ! [X4] :
( ! [X5] :
( sK14 != X4
| sK15 != X5
| ~ r2_hidden(sK16,k1_altcat_1(sK13,X4,X5))
| ~ m1_subset_1(sK16,k1_altcat_1(sK13,X4,X5))
| ~ m1_subset_1(X5,u1_struct_0(sK13)) )
| ~ m1_subset_1(X4,u1_struct_0(sK13)) )
& ~ v3_struct_0(sK13)
& l2_altcat_1(sK13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15),skolemize(X3,sK16)],[f55744]) ).
fof(f56572,plain,
! [X0,X1] :
( ( ( m1_pboole(X1,X0)
| k1_relat_1(X1) != X0 )
& ( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0) ) )
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(nnf_transformation,[],[f55818]) ).
fof(f56607,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = k1_funct_1(X0,X1)
| ~ r2_hidden(k4_tarski(X1,X2),X0) )
& ( r2_hidden(k4_tarski(X1,X2),X0)
| k1_funct_1(X0,X1) != X2 ) )
| ~ r2_hidden(X1,k1_relat_1(X0)) )
& ( ( ( X2 = k1_funct_1(X0,X1)
| k1_xboole_0 != X2 )
& ( X2 = k1_xboole_0
| k1_funct_1(X0,X1) != X2 ) )
| r2_hidden(X1,k1_relat_1(X0)) ) )
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(nnf_transformation,[],[f55871]) ).
fof(f56640,plain,
! [X0,X1,X2,X3] :
( ( r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X1,X3) )
& ( ( r2_hidden(X0,X2)
& r2_hidden(X1,X3) )
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ) ),
inference(nnf_transformation,[],[f431]) ).
fof(f56641,plain,
! [X0,X1,X2,X3] :
( ( r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))
| ~ r2_hidden(X0,X2)
| ~ r2_hidden(X1,X3) )
& ( ( r2_hidden(X0,X2)
& r2_hidden(X1,X3) )
| ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3)) ) ),
inference(flattening,[],[f56640]) ).
fof(f56924,plain,
l2_altcat_1(sK13),
inference(cnf_transformation,[],[f56543]) ).
fof(f56926,plain,
! [X4,X5] :
( sK14 != X4
| sK15 != X5
| ~ r2_hidden(sK16,k1_altcat_1(sK13,X4,X5))
| ~ m1_subset_1(sK16,k1_altcat_1(sK13,X4,X5))
| ~ m1_subset_1(X5,u1_struct_0(sK13))
| ~ m1_subset_1(X4,u1_struct_0(sK13)) ),
inference(cnf_transformation,[],[f56543]) ).
fof(f56927,plain,
r2_hidden(sK16,k1_binop_1(u1_altcat_1(sK13),sK14,sK15)),
inference(cnf_transformation,[],[f56543]) ).
fof(f56933,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f55751]) ).
fof(f56938,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f55753]) ).
fof(f56954,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,k4_tarski(X1,X2)) = k1_binop_1(X0,X1,X2)
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f55766]) ).
fof(f56961,plain,
! [X0] :
( m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f55772]) ).
fof(f56962,plain,
! [X2,X0,X1] :
( k1_altcat_1(X0,X1,X2) = k1_binop_1(u1_altcat_1(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f55773]) ).
fof(f57050,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| v1_funct_1(X1) ),
inference(cnf_transformation,[],[f55813]) ).
fof(f57051,plain,
! [X0,X1] :
( ~ m1_pboole(X1,X0)
| v1_relat_1(X1) ),
inference(cnf_transformation,[],[f55813]) ).
fof(f57055,plain,
! [X0,X1] :
( k1_relat_1(X1) = X0
| ~ m1_pboole(X1,X0)
| ~ v1_relat_1(X1)
| ~ v1_funct_1(X1) ),
inference(cnf_transformation,[],[f56572]) ).
fof(f57161,plain,
! [X2,X0,X1] :
( k1_funct_1(X0,X1) = X2
| k1_xboole_0 != X2
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f56607]) ).
fof(f57217,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))
| r2_hidden(X1,X3) ),
inference(cnf_transformation,[],[f56641]) ).
fof(f57218,plain,
! [X2,X3,X0,X1] :
( ~ r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))
| r2_hidden(X0,X2) ),
inference(cnf_transformation,[],[f56641]) ).
fof(f57309,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f55936]) ).
fof(f57409,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f694]) ).
fof(f58253,plain,
! [X5] :
( sK15 != X5
| ~ r2_hidden(sK16,k1_altcat_1(sK13,sK14,X5))
| ~ m1_subset_1(sK16,k1_altcat_1(sK13,sK14,X5))
| ~ m1_subset_1(X5,u1_struct_0(sK13))
| ~ m1_subset_1(sK14,u1_struct_0(sK13)) ),
inference(equality_resolution,[],[f56926]) ).
fof(f58254,plain,
( ~ r2_hidden(sK16,k1_altcat_1(sK13,sK14,sK15))
| ~ m1_subset_1(sK16,k1_altcat_1(sK13,sK14,sK15))
| ~ m1_subset_1(sK15,u1_struct_0(sK13))
| ~ m1_subset_1(sK14,u1_struct_0(sK13)) ),
inference(equality_resolution,[],[f58253]) ).
fof(f58264,plain,
! [X0,X1] :
( k1_xboole_0 = k1_funct_1(X0,X1)
| r2_hidden(X1,k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(equality_resolution,[],[f57161]) ).
fof(f58353,definition,
sF288 = u1_altcat_1(sK13),
introduced(definition,[new_symbols(definition,[sF288])],[function_definition]) ).
fof(f58354,plain,
u1_altcat_1(sK13) = sF288,
inference(reorient_equations,[],[f58353]) ).
fof(f58355,definition,
sF289 = k1_binop_1(sF288,sK14,sK15),
introduced(definition,[new_symbols(definition,[sF289])],[function_definition]) ).
fof(f58356,plain,
k1_binop_1(sF288,sK14,sK15) = sF289,
inference(reorient_equations,[],[f58355]) ).
fof(f58357,plain,
r2_hidden(sK16,sF289),
inference(definition_folding,[],[f56927,f58356,f58354]) ).
fof(f58358,definition,
sF290 = k1_altcat_1(sK13,sK14,sK15),
introduced(definition,[new_symbols(definition,[sF290])],[function_definition]) ).
fof(f58359,plain,
k1_altcat_1(sK13,sK14,sK15) = sF290,
inference(reorient_equations,[],[f58358]) ).
fof(f58360,definition,
sF291 = u1_struct_0(sK13),
introduced(definition,[new_symbols(definition,[sF291])],[function_definition]) ).
fof(f58361,plain,
u1_struct_0(sK13) = sF291,
inference(reorient_equations,[],[f58360]) ).
fof(f58362,plain,
( ~ r2_hidden(sK16,sF290)
| ~ m1_subset_1(sK16,sF290)
| ~ m1_subset_1(sK15,sF291)
| ~ m1_subset_1(sK14,sF291) ),
inference(definition_folding,[],[f58254,f58361,f58361,f58359,f58359]) ).
fof(f58862,definition,
( spl292_100
<=> v1_xboole_0(k1_xboole_0) ),
introduced(definition,[new_symbols(definition,[spl292_100])],[avatar_definition]) ).
fof(f58865,plain,
spl292_100,
inference(avatar_split_clause,[],[f57409,f58862]) ).
fof(f59189,definition,
( spl292_165
<=> l2_altcat_1(sK13) ),
introduced(definition,[new_symbols(definition,[spl292_165])],[avatar_definition]) ).
fof(f59191,plain,
( l2_altcat_1(sK13)
| ~ spl292_165 ),
inference(avatar_component_clause,[],[f59189]) ).
fof(f59192,plain,
spl292_165,
inference(avatar_split_clause,[],[f56924,f59189]) ).
fof(f59199,definition,
( spl292_167
<=> m1_subset_1(sK14,sF291) ),
introduced(definition,[new_symbols(definition,[spl292_167])],[avatar_definition]) ).
fof(f59203,definition,
( spl292_168
<=> m1_subset_1(sK15,sF291) ),
introduced(definition,[new_symbols(definition,[spl292_168])],[avatar_definition]) ).
fof(f59205,plain,
( ~ m1_subset_1(sK15,sF291)
| spl292_168 ),
inference(avatar_component_clause,[],[f59203]) ).
fof(f59207,definition,
( spl292_169
<=> m1_subset_1(sK16,sF290) ),
introduced(definition,[new_symbols(definition,[spl292_169])],[avatar_definition]) ).
fof(f59211,definition,
( spl292_170
<=> r2_hidden(sK16,sF290) ),
introduced(definition,[new_symbols(definition,[spl292_170])],[avatar_definition]) ).
fof(f59214,plain,
( ~ spl292_167
| ~ spl292_168
| ~ spl292_169
| ~ spl292_170 ),
inference(avatar_split_clause,[],[f58362,f59211,f59207,f59203,f59199]) ).
fof(f59216,definition,
( spl292_171
<=> r2_hidden(sK16,sF289) ),
introduced(definition,[new_symbols(definition,[spl292_171])],[avatar_definition]) ).
fof(f59218,plain,
( r2_hidden(sK16,sF289)
| ~ spl292_171 ),
inference(avatar_component_clause,[],[f59216]) ).
fof(f59219,plain,
spl292_171,
inference(avatar_split_clause,[],[f58357,f59216]) ).
fof(f59226,definition,
( spl292_173
<=> u1_altcat_1(sK13) = sF288 ),
introduced(definition,[new_symbols(definition,[spl292_173])],[avatar_definition]) ).
fof(f59228,plain,
( u1_altcat_1(sK13) = sF288
| ~ spl292_173 ),
inference(avatar_component_clause,[],[f59226]) ).
fof(f59229,plain,
spl292_173,
inference(avatar_split_clause,[],[f58354,f59226]) ).
fof(f59231,definition,
( spl292_174
<=> k1_binop_1(sF288,sK14,sK15) = sF289 ),
introduced(definition,[new_symbols(definition,[spl292_174])],[avatar_definition]) ).
fof(f59233,plain,
( k1_binop_1(sF288,sK14,sK15) = sF289
| ~ spl292_174 ),
inference(avatar_component_clause,[],[f59231]) ).
fof(f59234,plain,
spl292_174,
inference(avatar_split_clause,[],[f58356,f59231]) ).
fof(f59236,definition,
( spl292_175
<=> k1_altcat_1(sK13,sK14,sK15) = sF290 ),
introduced(definition,[new_symbols(definition,[spl292_175])],[avatar_definition]) ).
fof(f59238,plain,
( k1_altcat_1(sK13,sK14,sK15) = sF290
| ~ spl292_175 ),
inference(avatar_component_clause,[],[f59236]) ).
fof(f59239,plain,
spl292_175,
inference(avatar_split_clause,[],[f58359,f59236]) ).
fof(f59241,definition,
( spl292_176
<=> u1_struct_0(sK13) = sF291 ),
introduced(definition,[new_symbols(definition,[spl292_176])],[avatar_definition]) ).
fof(f59243,plain,
( u1_struct_0(sK13) = sF291
| ~ spl292_176 ),
inference(avatar_component_clause,[],[f59241]) ).
fof(f59244,plain,
spl292_176,
inference(avatar_split_clause,[],[f58361,f59241]) ).
fof(f59245,plain,
( m1_subset_1(sK16,sF289)
| ~ spl292_171 ),
inference(resolution,[],[f56933,f59218]) ).
fof(f59247,definition,
( spl292_177
<=> m1_subset_1(sK16,sF289) ),
introduced(definition,[new_symbols(definition,[spl292_177])],[avatar_definition]) ).
fof(f59250,plain,
( spl292_177
| ~ spl292_171 ),
inference(avatar_split_clause,[],[f59245,f59216,f59247]) ).
fof(f59254,plain,
( l1_altcat_1(sK13)
| ~ spl292_165 ),
inference(resolution,[],[f57309,f59191]) ).
fof(f59256,definition,
( spl292_178
<=> l1_altcat_1(sK13) ),
introduced(definition,[new_symbols(definition,[spl292_178])],[avatar_definition]) ).
fof(f59258,plain,
( l1_altcat_1(sK13)
| ~ spl292_178 ),
inference(avatar_component_clause,[],[f59256]) ).
fof(f59259,plain,
( spl292_178
| ~ spl292_165 ),
inference(avatar_split_clause,[],[f59254,f59189,f59256]) ).
fof(f59262,plain,
( ! [X0,X1] :
( k1_altcat_1(sK13,X0,X1) = k1_binop_1(sF288,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK13))
| ~ m1_subset_1(X0,u1_struct_0(sK13))
| ~ l1_altcat_1(sK13) )
| ~ spl292_173 ),
inference(superposition,[],[f56962,f59228]) ).
fof(f59263,plain,
( ! [X0,X1] :
( k1_altcat_1(sK13,X0,X1) = k1_binop_1(sF288,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK13))
| ~ m1_subset_1(X0,u1_struct_0(sK13)) )
| ~ spl292_173
| ~ spl292_178 ),
inference(forward_subsumption_resolution,[],[f59262,f59258]) ).
fof(f59264,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF291)
| k1_altcat_1(sK13,X0,X1) = k1_binop_1(sF288,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK13)) )
| ~ spl292_173
| ~ spl292_176
| ~ spl292_178 ),
inference(forward_demodulation,[],[f59263,f59243]) ).
fof(f59265,plain,
( ! [X0,X1] :
( k1_altcat_1(sK13,X0,X1) = k1_binop_1(sF288,X0,X1)
| ~ m1_subset_1(X1,sF291)
| ~ m1_subset_1(X0,sF291) )
| ~ spl292_173
| ~ spl292_176
| ~ spl292_178 ),
inference(forward_demodulation,[],[f59264,f59243]) ).
fof(f59266,plain,
( ~ v1_xboole_0(sF289)
| ~ spl292_171 ),
inference(resolution,[],[f56938,f59218]) ).
fof(f59269,definition,
( spl292_179
<=> v1_xboole_0(sF289) ),
introduced(definition,[new_symbols(definition,[spl292_179])],[avatar_definition]) ).
fof(f59272,plain,
( ~ spl292_179
| ~ spl292_171 ),
inference(avatar_split_clause,[],[f59266,f59216,f59269]) ).
fof(f59274,plain,
( k1_altcat_1(sK13,sK14,sK15) = sF289
| ~ m1_subset_1(sK15,sF291)
| ~ m1_subset_1(sK14,sF291)
| ~ spl292_173
| ~ spl292_174
| ~ spl292_176
| ~ spl292_178 ),
inference(superposition,[],[f59265,f59233]) ).
fof(f59277,plain,
( sF289 = sF290
| ~ m1_subset_1(sK15,sF291)
| ~ m1_subset_1(sK14,sF291)
| ~ spl292_173
| ~ spl292_174
| ~ spl292_175
| ~ spl292_176
| ~ spl292_178 ),
inference(forward_demodulation,[],[f59274,f59238]) ).
fof(f59279,definition,
( spl292_180
<=> sF289 = sF290 ),
introduced(definition,[new_symbols(definition,[spl292_180])],[avatar_definition]) ).
fof(f59283,plain,
( ~ spl292_167
| ~ spl292_168
| spl292_180
| ~ spl292_173
| ~ spl292_174
| ~ spl292_175
| ~ spl292_176
| ~ spl292_178 ),
inference(avatar_split_clause,[],[f59277,f59256,f59241,f59236,f59231,f59226,f59279,f59203,f59199]) ).
fof(f59329,plain,
( m1_pboole(u1_altcat_1(sK13),k2_zfmisc_1(sF291,sF291))
| ~ l1_altcat_1(sK13)
| ~ spl292_176 ),
inference(superposition,[],[f56961,f59243]) ).
fof(f59330,plain,
( m1_pboole(u1_altcat_1(sK13),k2_zfmisc_1(sF291,sF291))
| ~ spl292_176
| ~ spl292_178 ),
inference(forward_subsumption_resolution,[],[f59329,f59258]) ).
fof(f59332,plain,
( m1_pboole(sF288,k2_zfmisc_1(sF291,sF291))
| ~ spl292_173
| ~ spl292_176
| ~ spl292_178 ),
inference(forward_demodulation,[],[f59330,f59228]) ).
fof(f59335,definition,
( spl292_185
<=> m1_pboole(sF288,k2_zfmisc_1(sF291,sF291)) ),
introduced(definition,[new_symbols(definition,[spl292_185])],[avatar_definition]) ).
fof(f59337,plain,
( m1_pboole(sF288,k2_zfmisc_1(sF291,sF291))
| ~ spl292_185 ),
inference(avatar_component_clause,[],[f59335]) ).
fof(f59338,plain,
( spl292_185
| ~ spl292_173
| ~ spl292_176
| ~ spl292_178 ),
inference(avatar_split_clause,[],[f59332,f59256,f59241,f59226,f59335]) ).
fof(f59361,definition,
( spl292_187
<=> v1_funct_1(sF288) ),
introduced(definition,[new_symbols(definition,[spl292_187])],[avatar_definition]) ).
fof(f59575,plain,
! [X2,X0,X1] :
( k1_xboole_0 = k1_binop_1(X0,X1,X2)
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| r2_hidden(k4_tarski(X1,X2),k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0) ),
inference(superposition,[],[f56954,f58264]) ).
fof(f59578,plain,
! [X2,X0,X1] :
( r2_hidden(k4_tarski(X1,X2),k1_relat_1(X0))
| ~ v1_relat_1(X0)
| ~ v1_funct_1(X0)
| k1_xboole_0 = k1_binop_1(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f59575]) ).
fof(f59787,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k4_tarski(X1,X2),X0)
| ~ v1_relat_1(X3)
| ~ v1_funct_1(X3)
| k1_xboole_0 = k1_binop_1(X3,X1,X2)
| ~ m1_pboole(X3,X0)
| ~ v1_relat_1(X3)
| ~ v1_funct_1(X3) ),
inference(superposition,[],[f59578,f57055]) ).
fof(f59788,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k4_tarski(X1,X2),X0)
| ~ v1_relat_1(X3)
| ~ v1_funct_1(X3)
| k1_xboole_0 = k1_binop_1(X3,X1,X2)
| ~ m1_pboole(X3,X0) ),
inference(duplicate_literal_removal,[],[f59787]) ).
fof(f59789,plain,
! [X2,X3,X0,X1] :
( k1_xboole_0 = k1_binop_1(X3,X1,X2)
| ~ v1_funct_1(X3)
| r2_hidden(k4_tarski(X1,X2),X0)
| ~ m1_pboole(X3,X0) ),
inference(forward_subsumption_resolution,[],[f59788,f57051]) ).
fof(f59790,plain,
( ! [X0] :
( k1_xboole_0 = sF289
| ~ v1_funct_1(sF288)
| r2_hidden(k4_tarski(sK14,sK15),X0)
| ~ m1_pboole(sF288,X0) )
| ~ spl292_174 ),
inference(superposition,[],[f59789,f59233]) ).
fof(f59809,definition,
( spl292_197
<=> ! [X0] :
( r2_hidden(k4_tarski(sK14,sK15),X0)
| ~ m1_pboole(sF288,X0) ) ),
introduced(definition,[new_symbols(definition,[spl292_197])],[avatar_definition]) ).
fof(f59810,plain,
( ! [X0] :
( r2_hidden(k4_tarski(sK14,sK15),X0)
| ~ m1_pboole(sF288,X0) )
| ~ spl292_197 ),
inference(avatar_component_clause,[],[f59809]) ).
fof(f59812,definition,
( spl292_198
<=> k1_xboole_0 = sF289 ),
introduced(definition,[new_symbols(definition,[spl292_198])],[avatar_definition]) ).
fof(f59817,plain,
( spl292_197
| ~ spl292_187
| spl292_198
| ~ spl292_174 ),
inference(avatar_split_clause,[],[f59790,f59231,f59812,f59361,f59809]) ).
fof(f59828,plain,
( v1_funct_1(sF288)
| ~ spl292_185 ),
inference(resolution,[],[f57050,f59337]) ).
fof(f59831,plain,
( spl292_187
| ~ spl292_185 ),
inference(avatar_split_clause,[],[f59828,f59335,f59361]) ).
fof(f59837,plain,
( ! [X0,X1] :
( ~ m1_pboole(sF288,k2_zfmisc_1(X0,X1))
| r2_hidden(sK15,X1) )
| ~ spl292_197 ),
inference(resolution,[],[f59810,f57217]) ).
fof(f59838,plain,
( ! [X0,X1] :
( ~ m1_pboole(sF288,k2_zfmisc_1(X0,X1))
| r2_hidden(sK14,X0) )
| ~ spl292_197 ),
inference(resolution,[],[f59810,f57218]) ).
fof(f59893,plain,
( k1_xboole_0 != sF289
| v1_xboole_0(sF289)
| ~ v1_xboole_0(k1_xboole_0) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f60231,definition,
( spl292_217
<=> r2_hidden(sK14,sF291) ),
introduced(definition,[new_symbols(definition,[spl292_217])],[avatar_definition]) ).
fof(f60232,plain,
( r2_hidden(sK14,sF291)
| ~ spl292_217 ),
inference(avatar_component_clause,[],[f60231]) ).
fof(f60434,plain,
( r2_hidden(sK14,sF291)
| ~ spl292_185
| ~ spl292_197 ),
inference(resolution,[],[f59838,f59337]) ).
fof(f60437,plain,
( spl292_217
| ~ spl292_185
| ~ spl292_197 ),
inference(avatar_split_clause,[],[f60434,f59809,f59335,f60231]) ).
fof(f60442,plain,
( m1_subset_1(sK14,sF291)
| ~ spl292_217 ),
inference(resolution,[],[f60232,f56933]) ).
fof(f60464,plain,
( spl292_167
| ~ spl292_217 ),
inference(avatar_split_clause,[],[f60442,f60231,f59199]) ).
fof(f60585,plain,
( r2_hidden(sK15,sF291)
| ~ spl292_185
| ~ spl292_197 ),
inference(resolution,[],[f59837,f59337]) ).
fof(f60587,definition,
( spl292_233
<=> r2_hidden(sK15,sF291) ),
introduced(definition,[new_symbols(definition,[spl292_233])],[avatar_definition]) ).
fof(f60589,plain,
( r2_hidden(sK15,sF291)
| ~ spl292_233 ),
inference(avatar_component_clause,[],[f60587]) ).
fof(f60590,plain,
( spl292_233
| ~ spl292_185
| ~ spl292_197 ),
inference(avatar_split_clause,[],[f60585,f59809,f59335,f60587]) ).
fof(f60595,plain,
( m1_subset_1(sK15,sF291)
| ~ spl292_233 ),
inference(resolution,[],[f60589,f56933]) ).
fof(f60603,plain,
( $false
| spl292_168
| ~ spl292_233 ),
inference(forward_subsumption_resolution,[],[f60595,f59205]) ).
fof(f60604,plain,
( spl292_168
| ~ spl292_233 ),
inference(avatar_contradiction_clause,[],[f60603]) ).
fof(f60605,plain,
( sF289 != sF290
| r2_hidden(sK16,sF290)
| ~ r2_hidden(sK16,sF289) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f60606,plain,
( sF289 != sF290
| m1_subset_1(sK16,sF290)
| ~ m1_subset_1(sK16,sF289) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s100,plain,
spl292_100,
inference(sat_conversion,[],[f58865]) ).
cnf(s196,plain,
spl292_165,
inference(sat_conversion,[],[f59192]) ).
cnf(s198,plain,
( ~ spl292_167
| ~ spl292_168
| ~ spl292_169
| ~ spl292_170 ),
inference(sat_conversion,[],[f59214]) ).
cnf(s199,plain,
spl292_171,
inference(sat_conversion,[],[f59219]) ).
cnf(s201,plain,
spl292_173,
inference(sat_conversion,[],[f59229]) ).
cnf(s202,plain,
spl292_174,
inference(sat_conversion,[],[f59234]) ).
cnf(s203,plain,
spl292_175,
inference(sat_conversion,[],[f59239]) ).
cnf(s204,plain,
spl292_176,
inference(sat_conversion,[],[f59244]) ).
cnf(s205,plain,
( ~ spl292_171
| spl292_177 ),
inference(sat_conversion,[],[f59250]) ).
cnf(s206,plain,
( ~ spl292_165
| spl292_178 ),
inference(sat_conversion,[],[f59259]) ).
cnf(s207,plain,
( ~ spl292_171
| ~ spl292_179 ),
inference(sat_conversion,[],[f59272]) ).
cnf(s209,plain,
( ~ spl292_167
| ~ spl292_168
| ~ spl292_173
| ~ spl292_174
| ~ spl292_175
| ~ spl292_176
| ~ spl292_178
| spl292_180 ),
inference(sat_conversion,[],[f59283]) ).
cnf(s212,plain,
( ~ spl292_173
| ~ spl292_176
| ~ spl292_178
| spl292_185 ),
inference(sat_conversion,[],[f59338]) ).
cnf(s228,plain,
( ~ spl292_174
| ~ spl292_187
| spl292_197
| spl292_198 ),
inference(sat_conversion,[],[f59817]) ).
cnf(s232,plain,
( ~ spl292_185
| spl292_187 ),
inference(sat_conversion,[],[f59831]) ).
cnf(s237,plain,
( ~ spl292_100
| spl292_179
| ~ spl292_198 ),
inference(sat_conversion,[],[f59893]) ).
cnf(s252,plain,
( ~ spl292_185
| ~ spl292_197
| spl292_217 ),
inference(sat_conversion,[],[f60437]) ).
cnf(s256,plain,
( spl292_167
| ~ spl292_217 ),
inference(sat_conversion,[],[f60464]) ).
cnf(s260,plain,
( ~ spl292_185
| ~ spl292_197
| spl292_233 ),
inference(sat_conversion,[],[f60590]) ).
cnf(s262,plain,
( spl292_168
| ~ spl292_233 ),
inference(sat_conversion,[],[f60604]) ).
cnf(s263,plain,
( spl292_170
| ~ spl292_171
| ~ spl292_180 ),
inference(sat_conversion,[],[f60605]) ).
cnf(s264,plain,
( spl292_169
| ~ spl292_177
| ~ spl292_180 ),
inference(sat_conversion,[],[f60606]) ).
cnf(s267,plain,
~ spl292_179,
inference(rat,[],[s207,s199]) ).
cnf(s268,plain,
spl292_177,
inference(rat,[],[s205,s199]) ).
cnf(s269,plain,
spl292_178,
inference(rat,[],[s206,s196]) ).
cnf(s271,plain,
spl292_185,
inference(rat,[],[s212,s201,s204,s269]) ).
cnf(s273,plain,
spl292_187,
inference(rat,[],[s232,s271]) ).
cnf(s276,plain,
~ spl292_198,
inference(rat,[],[s237,s267,s100]) ).
cnf(s277,plain,
spl292_197,
inference(rat,[],[s228,s273,s202,s276]) ).
cnf(s278,plain,
spl292_233,
inference(rat,[],[s260,s271,s277]) ).
cnf(s279,plain,
spl292_217,
inference(rat,[],[s252,s271,s277]) ).
cnf(s282,plain,
spl292_168,
inference(rat,[],[s262,s278]) ).
cnf(s285,plain,
spl292_167,
inference(rat,[],[s256,s279]) ).
cnf(s287,plain,
spl292_180,
inference(rat,[],[s209,s282,s269,s204,s203,s202,s201,s285]) ).
cnf(s288,plain,
spl292_170,
inference(rat,[],[s263,s199,s287]) ).
cnf(s289,plain,
spl292_169,
inference(rat,[],[s264,s268,s287]) ).
cnf(s290,plain,
$false,
inference(rat,[],[s198,s285,s282,s288,s289]) ).
fof(f60607,plain,
$false,
inference(avatar_sat_refutation,[],[s290]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT359+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n026.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 15:02:36 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
% 15.02/4.15 % (2954979)Detected formulas, will run a generic FOF schedule.
% 15.02/4.15 % (2954989)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2547919343:s2a=on:i=139:gtg=position_2983 on theBenchmark for (2983ds/139Mi)
% 15.02/4.15 % (2954984)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=4198337197:i=141193_2983 on theBenchmark for (2983ds/141193Mi)
% 15.02/4.15 % (2954988)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1097864648:i=119:av=off:ss=axioms_2983 on theBenchmark for (2983ds/119Mi)
% 15.02/4.15 % (2954986)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=237866300:i=141695:sd=1:nm=32:gsp=on:ss=included_2983 on theBenchmark for (2983ds/141695Mi)
% 15.02/4.15 % (2954990)dis-21_1_sil=8000:lcm=predicate:random_seed=1483909814:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2983 on theBenchmark for (2983ds/129Mi)
% 15.02/4.15 % (2954985)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=3214593297:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2983 on theBenchmark for (2983ds/134677Mi)
% 15.02/4.15 % (2954989)Instruction limit reached!
% 15.02/4.15 % (2954989)------------------------------
% 15.02/4.15 % (2954989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.15 % (2954989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.15 % (2954989)CaDiCaL version: 2.1.3
% 15.02/4.15 % (2954989)Termination reason: Instruction limit
% 15.02/4.15 % (2954989)Termination phase: Property scanning
% 15.02/4.15 % (2954989)Time elapsed: 0.036 s
% 15.02/4.15 % (2954989)Peak memory usage: 173 MB
% 15.02/4.15 % (2954989)Instructions burned: 140 (million)
% 15.02/4.15 % (2954987)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3751030691:i=109:sd=1:ins=1:gsp=on:ss=axioms_2983 on theBenchmark for (2983ds/109Mi)
% 15.02/4.15 % (2954987)Instruction limit reached!
% 15.02/4.15 % (2954987)------------------------------
% 15.02/4.15 % (2954987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.15 % (2954987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.15 % (2954987)CaDiCaL version: 2.1.3
% 15.02/4.15 % (2954987)Termination reason: Instruction limit
% 15.02/4.15 % (2954987)Termination phase: SInE selection
% 15.02/4.15 % (2954987)Time elapsed: 0.080 s
% 15.02/4.15 % (2954987)Peak memory usage: 173 MB
% 15.02/4.15 % (2954987)Instructions burned: 109 (million)
% 15.02/4.15 % (2954988)Instruction limit reached!
% 15.02/4.15 % (2954988)------------------------------
% 15.02/4.15 % (2954988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.15 % (2954988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.15 % (2954988)CaDiCaL version: 2.1.3
% 15.02/4.15 % (2954988)Termination reason: Instruction limit
% 15.02/4.15 % (2954988)Termination phase: SInE selection
% 15.02/4.15 % (2954988)Time elapsed: 0.088 s
% 15.02/4.15 % (2954988)Peak memory usage: 173 MB
% 15.02/4.15 % (2954988)Instructions burned: 119 (million)
% 15.02/4.15 % (2954990)Instruction limit reached!
% 15.02/4.15 % (2954990)------------------------------
% 15.02/4.15 % (2954990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.15 % (2954990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/4.15 % (2954990)CaDiCaL version: 2.1.3
% 15.02/4.15 % (2954990)Termination reason: Instruction limit
% 15.02/4.15 % (2954990)Termination phase: SInE selection
% 15.02/4.15 % (2954990)Time elapsed: 0.096 s
% 15.02/4.15 % (2954990)Peak memory usage: 173 MB
% 15.02/4.15 % (2954990)Instructions burned: 130 (million)
% 15.02/4.15 % (2954998)lrs+10_1_sil=8000:sp=occurrence:random_seed=590662648:i=285:sd=3:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/285Mi)
% 15.02/4.15 % (2955001)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4255038898:i=325:sd=1:ss=axioms:sgt=32_2981 on theBenchmark for (2981ds/325Mi)
% 15.02/4.15 % (2955000)lrs+10_1_sil=32000:urr=on:br=off:random_seed=360872406:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/157Mi)
% 15.02/4.15 % (2954998)Instruction limit reached!
% 15.02/4.15 % (2954998)------------------------------
% 15.02/4.15 % (2954998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/4.15 % (2954998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2954998)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2954998)Termination reason: Instruction limit
% 22.64/5.25 % (2954998)Termination phase: SInE selection
% 22.64/5.25 % (2954998)Time elapsed: 0.122 s
% 22.64/5.25 % (2954998)Peak memory usage: 174 MB
% 22.64/5.25 % (2954998)Instructions burned: 286 (million)
% 22.64/5.25 % (2955002)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=4058190508:s2a=on:i=248:s2at=1.23:gtg=position_2981 on theBenchmark for (2981ds/248Mi)
% 22.64/5.25 % (2955000)Instruction limit reached!
% 22.64/5.25 % (2955000)------------------------------
% 22.64/5.25 % (2955000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955000)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2955000)Termination reason: Instruction limit
% 22.64/5.25 % (2955000)Termination phase: Property scanning
% 22.64/5.25 % (2955000)Time elapsed: 0.073 s
% 22.64/5.25 % (2955000)Peak memory usage: 173 MB
% 22.64/5.25 % (2955000)Instructions burned: 159 (million)
% 22.64/5.25 % (2955005)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3974511468:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2979 on theBenchmark for (2979ds/294Mi)
% 22.64/5.25 % (2955002)Instruction limit reached!
% 22.64/5.25 % (2955002)------------------------------
% 22.64/5.25 % (2955002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955002)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2955002)Termination reason: Instruction limit
% 22.64/5.25 % (2955002)Termination phase: Property scanning
% 22.64/5.25 % (2955002)Time elapsed: 0.113 s
% 22.64/5.25 % (2955002)Peak memory usage: 173 MB
% 22.64/5.25 % (2955002)Instructions burned: 249 (million)
% 22.64/5.25 % (2955007)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=939894806:i=2350_2979 on theBenchmark for (2979ds/2350Mi)
% 22.64/5.25 % (2955005)Instruction limit reached!
% 22.64/5.25 % (2955005)------------------------------
% 22.64/5.25 % (2955005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955005)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2955005)Termination reason: Instruction limit
% 22.64/5.25 % (2955005)Termination phase: SInE selection
% 22.64/5.25 % (2955005)Time elapsed: 0.118 s
% 22.64/5.25 % (2955005)Peak memory usage: 174 MB
% 22.64/5.25 % (2955005)Instructions burned: 297 (million)
% 22.64/5.25 % (2955001)Instruction limit reached!
% 22.64/5.25 % (2955001)------------------------------
% 22.64/5.25 % (2955001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955001)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2955001)Termination reason: Instruction limit
% 22.64/5.25 % (2955001)Termination phase: SInE selection
% 22.64/5.25 % (2955001)Time elapsed: 0.237 s
% 22.64/5.25 % (2955001)Peak memory usage: 174 MB
% 22.64/5.25 % (2955001)Instructions burned: 325 (million)
% 22.64/5.25 % (2955009)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=217005969:cts=off:i=113:fsr=off:ss=included:sgt=4_2978 on theBenchmark for (2978ds/113Mi)
% 22.64/5.25 % (2955011)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=750767857:i=127:av=off:fsr=off:sup=off_2977 on theBenchmark for (2977ds/127Mi)
% 22.64/5.25 % (2955011)Instruction limit reached!
% 22.64/5.25 % (2955011)------------------------------
% 22.64/5.25 % (2955011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955011)CaDiCaL version: 2.1.3
% 22.64/5.25 % (2955011)Termination reason: Instruction limit
% 22.64/5.25 % (2955011)Termination phase: Preprocessing 1
% 22.64/5.25 % (2955011)Time elapsed: 0.058 s
% 22.64/5.25 % (2955011)Peak memory usage: 174 MB
% 22.64/5.25 % (2955011)Instructions burned: 129 (million)
% 22.64/5.25 % (2955009)Instruction limit reached!
% 22.64/5.25 % (2955009)------------------------------
% 22.64/5.25 % (2955009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.64/5.25 % (2955009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.64/5.25 % (2955009)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955009)Termination reason: Instruction limit
% 52.45/9.43 % (2955009)Termination phase: SInE selection
% 52.45/9.43 % (2955009)Time elapsed: 0.093 s
% 52.45/9.43 % (2955009)Peak memory usage: 173 MB
% 52.45/9.43 % (2955009)Instructions burned: 114 (million)
% 52.45/9.43 % (2955012)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2496160253:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2977 on theBenchmark for (2977ds/114Mi)
% 52.45/9.43 % (2955012)Instruction limit reached!
% 52.45/9.43 % (2955012)------------------------------
% 52.45/9.43 % (2955012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.45/9.43 % (2955012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.45/9.43 % (2955012)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955012)Termination reason: Instruction limit
% 52.45/9.43 % (2955012)Termination phase: Property scanning
% 52.45/9.43 % (2955012)Time elapsed: 0.057 s
% 52.45/9.43 % (2955012)Peak memory usage: 173 MB
% 52.45/9.43 % (2955012)Instructions burned: 115 (million)
% 52.45/9.43 % (2955015)lrs+10_1_sil=8000:sp=occurrence:random_seed=3329917847:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2976 on theBenchmark for (2976ds/907Mi)
% 52.45/9.43 % (2955017)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1214900959:i=437:sd=1:aac=none:ss=included_2976 on theBenchmark for (2976ds/437Mi)
% 52.45/9.43 % (2955018)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3699055721:i=5202:ss=axioms:sgt=16_2975 on theBenchmark for (2975ds/5202Mi)
% 52.45/9.43 % (2955015)Instruction limit reached!
% 52.45/9.43 % (2955015)------------------------------
% 52.45/9.43 % (2955015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.45/9.43 % (2955015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.45/9.43 % (2955015)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955015)Termination reason: Instruction limit
% 52.45/9.43 % (2955015)Termination phase: Property scanning
% 52.45/9.43 % (2955015)Time elapsed: 0.357 s
% 52.45/9.43 % (2955015)Peak memory usage: 183 MB
% 52.45/9.43 % (2955015)Instructions burned: 908 (million)
% 52.45/9.43 % (2955017)Instruction limit reached!
% 52.45/9.43 % (2955017)------------------------------
% 52.45/9.43 % (2955017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.45/9.43 % (2955017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.45/9.43 % (2955017)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955017)Termination reason: Instruction limit
% 52.45/9.43 % (2955017)Termination phase: Preprocessing 2
% 52.45/9.43 % (2955017)Time elapsed: 0.344 s
% 52.45/9.43 % (2955017)Peak memory usage: 176 MB
% 52.45/9.43 % (2955017)Instructions burned: 437 (million)
% 52.45/9.43 % (2955022)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1574843371:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2971 on theBenchmark for (2971ds/134Mi)
% 52.45/9.43 % (2955022)Instruction limit reached!
% 52.45/9.43 % (2955022)------------------------------
% 52.45/9.43 % (2955022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.45/9.43 % (2955022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.45/9.43 % (2955022)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955022)Termination reason: Instruction limit
% 52.45/9.43 % (2955022)Termination phase: SInE selection
% 52.45/9.43 % (2955022)Time elapsed: 0.060 s
% 52.45/9.43 % (2955022)Peak memory usage: 173 MB
% 52.45/9.43 % (2955022)Instructions burned: 135 (million)
% 52.45/9.43 % (2955023)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3930181742:st=8:i=592:sd=3:ep=RST:ss=axioms_2971 on theBenchmark for (2971ds/592Mi)
% 52.45/9.43 % (2955025)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4265180739:st=3:i=13193:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/13193Mi)
% 52.45/9.43 % (2955023)Instruction limit reached!
% 52.45/9.43 % (2955023)------------------------------
% 52.45/9.43 % (2955023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.45/9.43 % (2955023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.45/9.43 % (2955023)CaDiCaL version: 2.1.3
% 52.45/9.43 % (2955023)Termination reason: Instruction limit
% 52.45/9.43 % (2955023)Termination phase: SInE selection
% 52.45/9.43 % (2955023)Time elapsed: 0.386 s
% 52.45/9.43 % (2955023)Peak memory usage: 175 MB
% 52.45/9.43 % (2955023)Instructions burned: 592 (million)
% 52.45/9.43 % (2955028)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=1912948676:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/125Mi)
% 75.81/12.97 % (2955028)Instruction limit reached!
% 75.81/12.97 % (2955028)------------------------------
% 75.81/12.97 % (2955028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955028)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955028)Termination reason: Instruction limit
% 75.81/12.97 % (2955028)Termination phase: Property scanning
% 75.81/12.97 % (2955028)Time elapsed: 0.059 s
% 75.81/12.97 % (2955028)Peak memory usage: 173 MB
% 75.81/12.97 % (2955028)Instructions burned: 125 (million)
% 75.81/12.97 % (2955030)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1574151933:i=134:gtgl=5:slsql=off:gtg=exists_sym_2964 on theBenchmark for (2964ds/134Mi)
% 75.81/12.97 % (2955030)Instruction limit reached!
% 75.81/12.97 % (2955030)------------------------------
% 75.81/12.97 % (2955030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955030)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955030)Termination reason: Instruction limit
% 75.81/12.97 % (2955030)Termination phase: Property scanning
% 75.81/12.97 % (2955030)Time elapsed: 0.062 s
% 75.81/12.97 % (2955030)Peak memory usage: 173 MB
% 75.81/12.97 % (2955030)Instructions burned: 135 (million)
% 75.81/12.97 % (2955007)Instruction limit reached!
% 75.81/12.97 % (2955007)------------------------------
% 75.81/12.97 % (2955007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955007)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955007)Termination reason: Instruction limit
% 75.81/12.97 % (2955007)Termination phase: Preprocessing 3
% 75.81/12.97 % (2955007)Time elapsed: 1.641 s
% 75.81/12.97 % (2955007)Peak memory usage: 276 MB
% 75.81/12.97 % (2955007)Instructions burned: 2350 (million)
% 75.81/12.97 % (2955032)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1906453416:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/141Mi)
% 75.81/12.97 % (2955033)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3877763748:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi)
% 75.81/12.97 % (2955032)Instruction limit reached!
% 75.81/12.97 % (2955032)------------------------------
% 75.81/12.97 % (2955032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955032)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955032)Termination reason: Instruction limit
% 75.81/12.97 % (2955032)Termination phase: SInE selection
% 75.81/12.97 % (2955032)Time elapsed: 0.113 s
% 75.81/12.97 % (2955032)Peak memory usage: 173 MB
% 75.81/12.97 % (2955032)Instructions burned: 141 (million)
% 75.81/12.97 % (2955036)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=3695861929:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 75.81/12.97 % (2955033)Instruction limit reached!
% 75.81/12.97 % (2955033)------------------------------
% 75.81/12.97 % (2955033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955033)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955033)Termination reason: Instruction limit
% 75.81/12.97 % (2955033)Termination phase: Naming
% 75.81/12.97 % (2955033)Time elapsed: 0.346 s
% 75.81/12.97 % (2955033)Peak memory usage: 177 MB
% 75.81/12.97 % (2955033)Instructions burned: 432 (million)
% 75.81/12.97 % (2955038)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=2916712002:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2956 on theBenchmark for (2956ds/150Mi)
% 75.81/12.97 % (2955038)Instruction limit reached!
% 75.81/12.97 % (2955038)------------------------------
% 75.81/12.97 % (2955038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.81/12.97 % (2955038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.81/12.97 % (2955038)CaDiCaL version: 2.1.3
% 75.81/12.97 % (2955038)Termination reason: Instruction limit
% 107.36/17.19 % (2955038)Termination phase: SInE selection
% 107.36/17.19 % (2955038)Time elapsed: 0.123 s
% 107.36/17.19 % (2955038)Peak memory usage: 173 MB
% 107.36/17.19 % (2955038)Instructions burned: 151 (million)
% 107.36/17.19 % (2955040)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1150364895:i=14155:bd=all_2953 on theBenchmark for (2953ds/14155Mi)
% 107.36/17.19 % (2955018)Instruction limit reached!
% 107.36/17.19 % (2955018)------------------------------
% 107.36/17.19 % (2955018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.36/17.19 % (2955018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.36/17.19 % (2955018)CaDiCaL version: 2.1.3
% 107.36/17.19 % (2955018)Termination reason: Instruction limit
% 107.36/17.19 % (2955018)Termination phase: Saturation
% 107.36/17.19 % (2955018)Time elapsed: 3.446 s
% 107.36/17.19 % (2955018)Peak memory usage: 281 MB
% 107.36/17.19 % (2955018)Instructions burned: 5203 (million)
% 107.36/17.19 % (2955042)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=8035109:i=667:av=off:fsr=off_2939 on theBenchmark for (2939ds/667Mi)
% 107.36/17.19 % (2955042)Instruction limit reached!
% 107.36/17.19 % (2955042)------------------------------
% 107.36/17.19 % (2955042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.36/17.19 % (2955042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.36/17.19 % (2955042)CaDiCaL version: 2.1.3
% 107.36/17.19 % (2955042)Termination reason: Instruction limit
% 107.36/17.19 % (2955042)Termination phase: Preprocessing 2
% 107.36/17.19 % (2955042)Time elapsed: 0.597 s
% 107.36/17.19 % (2955042)Peak memory usage: 215 MB
% 107.36/17.19 % (2955042)Instructions burned: 667 (million)
% 107.36/17.19 % (2955036)Instruction limit reached!
% 107.36/17.19 % (2955036)------------------------------
% 107.36/17.19 % (2955036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.36/17.19 % (2955036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.36/17.19 % (2955036)CaDiCaL version: 2.1.3
% 107.36/17.19 % (2955036)Termination reason: Instruction limit
% 107.36/17.19 % (2955036)Termination phase: NewCNF
% 107.36/17.19 % (2955036)Time elapsed: 2.686 s
% 107.36/17.19 % (2955036)Peak memory usage: 331 MB
% 107.36/17.19 % (2955036)Instructions burned: 6061 (million)
% 107.36/17.19 % (2955044)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=3059368015:s2a=on:i=185:s2at=1.8:fdi=4_2931 on theBenchmark for (2931ds/185Mi)
% 107.36/17.19 % (2955045)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1041890195:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2931 on theBenchmark for (2931ds/193Mi)
% 107.36/17.19 % (2955045)Instruction limit reached!
% 107.36/17.19 % (2955045)------------------------------
% 107.36/17.19 % (2955045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.36/17.19 % (2955045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.36/17.19 % (2955045)CaDiCaL version: 2.1.3
% 107.36/17.19 % (2955045)Termination reason: Instruction limit
% 107.36/17.19 % (2955045)Termination phase: SInE selection
% 107.36/17.19 % (2955045)Time elapsed: 0.084 s
% 107.36/17.19 % (2955045)Peak memory usage: 173 MB
% 107.36/17.19 % (2955045)Instructions burned: 194 (million)
% 107.36/17.19 % (2955044)Instruction limit reached!
% 107.36/17.19 % (2955044)------------------------------
% 107.36/17.19 % (2955044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.36/17.19 % (2955044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.36/17.19 % (2955044)CaDiCaL version: 2.1.3
% 107.36/17.19 % (2955044)Termination reason: Instruction limit
% 107.36/17.19 % (2955044)Termination phase: SInE selection
% 107.36/17.19 % (2955044)Time elapsed: 0.140 s
% 107.36/17.19 % (2955044)Peak memory usage: 173 MB
% 107.36/17.19 % (2955044)Instructions burned: 185 (million)
% 107.36/17.19 % (2955048)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=545562388:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2929 on theBenchmark for (2929ds/4850Mi)
% 107.36/17.19 % (2955049)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3668353243:i=12111:sd=1:ss=included_2929 on theBenchmark for (2929ds/12111Mi)
% 107.36/17.19 % (2955048)Instruction limit reached!
% 107.36/17.19 % (2955048)------------------------------
% 107.36/17.19 % (2955048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955048)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955048)Termination reason: Instruction limit
% 130.41/20.49 % (2955048)Termination phase: Function definition elimination
% 130.41/20.49 % (2955048)Time elapsed: 1.679 s
% 130.41/20.49 % (2955048)Peak memory usage: 297 MB
% 130.41/20.49 % (2955048)Instructions burned: 4852 (million)
% 130.41/20.49 % (2955052)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=371380015:i=319:kws=precedence:fsr=off_2911 on theBenchmark for (2911ds/319Mi)
% 130.41/20.49 % (2955052)Instruction limit reached!
% 130.41/20.49 % (2955052)------------------------------
% 130.41/20.49 % (2955052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955052)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955052)Termination reason: Instruction limit
% 130.41/20.49 % (2955052)Termination phase: Preprocessing 1
% 130.41/20.49 % (2955052)Time elapsed: 0.134 s
% 130.41/20.49 % (2955052)Peak memory usage: 175 MB
% 130.41/20.49 % (2955052)Instructions burned: 321 (million)
% 130.41/20.49 % (2955054)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4178603663:i=2064:ep=RST_2909 on theBenchmark for (2909ds/2064Mi)
% 130.41/20.49 % (2955054)Instruction limit reached!
% 130.41/20.49 % (2955054)------------------------------
% 130.41/20.49 % (2955054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955054)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955054)Termination reason: Instruction limit
% 130.41/20.49 % (2955054)Termination phase: Preprocessing 3
% 130.41/20.49 % (2955054)Time elapsed: 0.838 s
% 130.41/20.49 % (2955054)Peak memory usage: 281 MB
% 130.41/20.49 % (2955054)Instructions burned: 2064 (million)
% 130.41/20.49 % (2955056)dis-1011_128_sil=32000:random_seed=812410989:i=3706:ep=RST:av=off_2900 on theBenchmark for (2900ds/3706Mi)
% 130.41/20.49 % (2955025)Instruction limit reached!
% 130.41/20.49 % (2955025)------------------------------
% 130.41/20.49 % (2955025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955025)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955025)Termination reason: Instruction limit
% 130.41/20.49 % (2955025)Termination phase: Saturation
% 130.41/20.49 % (2955025)Time elapsed: 7.676 s
% 130.41/20.49 % (2955025)Peak memory usage: 335 MB
% 130.41/20.49 % (2955025)Instructions burned: 13195 (million)
% 130.41/20.49 % (2955058)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=158604206:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2892 on theBenchmark for (2892ds/757Mi)
% 130.41/20.49 % (2955058)Refutation not found, incomplete strategy
% 130.41/20.49 % (2955058)------------------------------
% 130.41/20.49 % (2955058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955058)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955058)Termination reason: Refutation not found, incomplete strategy
% 130.41/20.49 % (2955058)Time elapsed: 0.387 s
% 130.41/20.49 % (2955058)Peak memory usage: 181 MB
% 130.41/20.49 % (2955058)Instructions burned: 462 (million)
% 130.41/20.49 % (2955056)Instruction limit reached!
% 130.41/20.49 % (2955056)------------------------------
% 130.41/20.49 % (2955056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.41/20.49 % (2955056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.41/20.49 % (2955056)CaDiCaL version: 2.1.3
% 130.41/20.49 % (2955056)Termination reason: Instruction limit
% 130.41/20.49 % (2955056)Termination phase: Property scanning
% 130.41/20.49 % (2955056)Time elapsed: 1.357 s
% 130.41/20.49 % (2955056)Peak memory usage: 338 MB
% 130.41/20.49 % (2955056)Instructions burned: 3707 (million)
% 130.41/20.49 % (2955058)------------------------------
% 130.41/20.49 % (2955058)------------------------------
% 130.41/20.49 % (2955060)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2807193600:i=13913:ss=axioms:sgt=8_2885 on theBenchmark for (2885ds/13913Mi)
% 130.41/20.49 % (2955062)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2614681837:i=9925:aac=none_2884 on theBenchmark for (2884ds/9925Mi)
% 130.41/20.49 % (2955040)Instruction limit reached!
% 100.17/22.91 % (2955040)------------------------------
% 100.17/22.91 % (2955040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955040)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955040)Termination reason: Instruction limit
% 100.17/22.91 % (2955040)Termination phase: Saturation
% 100.17/22.91 % (2955040)Time elapsed: 7.560 s
% 100.17/22.91 % (2955040)Peak memory usage: 775 MB
% 100.17/22.91 % (2955040)Instructions burned: 14155 (million)
% 100.17/22.91 % (2955064)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2348371538:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2875 on theBenchmark for (2875ds/2479Mi)
% 100.17/22.91 % (2955064)Refutation not found, incomplete strategy
% 100.17/22.91 % (2955064)------------------------------
% 100.17/22.91 % (2955064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955064)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955064)Termination reason: Refutation not found, incomplete strategy
% 100.17/22.91 % (2955064)Time elapsed: 0.699 s
% 100.17/22.91 % (2955064)Peak memory usage: 180 MB
% 100.17/22.91 % (2955064)Instructions burned: 946 (million)
% 100.17/22.91 % (2955064)------------------------------
% 100.17/22.91 % (2955064)------------------------------
% 100.17/22.91 % (2955066)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3184733804:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2864 on theBenchmark for (2864ds/440Mi)
% 100.17/22.91 % (2955066)Instruction limit reached!
% 100.17/22.91 % (2955066)------------------------------
% 100.17/22.91 % (2955066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955066)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955066)Termination reason: Instruction limit
% 100.17/22.91 % (2955066)Termination phase: Property scanning
% 100.17/22.91 % (2955066)Time elapsed: 0.189 s
% 100.17/22.91 % (2955066)Peak memory usage: 173 MB
% 100.17/22.91 % (2955066)Instructions burned: 440 (million)
% 100.17/22.91 % (2955068)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3687044030:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2861 on theBenchmark for (2861ds/11145Mi)
% 100.17/22.91 % (2955049)Instruction limit reached!
% 100.17/22.91 % (2955049)------------------------------
% 100.17/22.91 % (2955049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955049)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955049)Termination reason: Instruction limit
% 100.17/22.91 % (2955049)Termination phase: Saturation
% 100.17/22.91 % (2955049)Time elapsed: 7.178 s
% 100.17/22.91 % (2955049)Peak memory usage: 302 MB
% 100.17/22.91 % (2955049)Instructions burned: 12111 (million)
% 100.17/22.91 % (2955070)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1238607766:cts=off:i=3034:av=off:er=known:fsd=on_2855 on theBenchmark for (2855ds/3034Mi)
% 100.17/22.91 % (2955060)Instruction limit reached!
% 100.17/22.91 % (2955060)------------------------------
% 100.17/22.91 % (2955060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955060)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955060)Termination reason: Instruction limit
% 100.17/22.91 % (2955060)Termination phase: Saturation
% 100.17/22.91 % (2955060)Time elapsed: 4.894 s
% 100.17/22.91 % (2955060)Peak memory usage: 318 MB
% 100.17/22.91 % (2955060)Instructions burned: 13913 (million)
% 100.17/22.91 % (2955062)Instruction limit reached!
% 100.17/22.91 % (2955062)------------------------------
% 100.17/22.91 % (2955062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955062)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955062)Termination reason: Instruction limit
% 100.17/22.91 % (2955062)Termination phase: Property scanning
% 100.17/22.91 % (2955062)Time elapsed: 4.842 s
% 100.17/22.91 % (2955062)Peak memory usage: 361 MB
% 100.17/22.91 % (2955062)Instructions burned: 9926 (million)
% 100.17/22.91 % (2955072)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1964184379:st=2:s2a=on:i=524:s2at=2:ss=axioms_2835 on theBenchmark for (2835ds/524Mi)
% 100.17/22.91 % (2955070)Instruction limit reached!
% 100.17/22.91 % (2955070)------------------------------
% 100.17/22.91 % (2955070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955070)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955070)Termination reason: Instruction limit
% 100.17/22.91 % (2955070)Termination phase: Preprocessing 3
% 100.17/22.91 % (2955070)Time elapsed: 2.138 s
% 100.17/22.91 % (2955070)Peak memory usage: 307 MB
% 100.17/22.91 % (2955070)Instructions burned: 3035 (million)
% 100.17/22.91 % (2955074)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=973415475:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2833 on theBenchmark for (2833ds/1016Mi)
% 100.17/22.91 % (2955072)Instruction limit reached!
% 100.17/22.91 % (2955072)------------------------------
% 100.17/22.91 % (2955072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955072)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955072)Termination reason: Instruction limit
% 100.17/22.91 % (2955072)Termination phase: SInE selection
% 100.17/22.91 % (2955072)Time elapsed: 0.198 s
% 100.17/22.91 % (2955072)Peak memory usage: 174 MB
% 100.17/22.91 % (2955072)Instructions burned: 526 (million)
% 100.17/22.91 % (2955076)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=370634997:i=14123:bd=preordered:ins=4_2832 on theBenchmark for (2832ds/14123Mi)
% 100.17/22.91 % (2955077)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=870033967:i=5781:kws=precedence:bd=all:rawr=on_2832 on theBenchmark for (2832ds/5781Mi)
% 100.17/22.91 % (2955074)Instruction limit reached!
% 100.17/22.91 % (2955074)------------------------------
% 100.17/22.91 % (2955074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955074)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955074)Termination reason: Instruction limit
% 100.17/22.91 % (2955074)Termination phase: Saturation
% 100.17/22.91 % (2955074)Time elapsed: 0.694 s
% 100.17/22.91 % (2955074)Peak memory usage: 184 MB
% 100.17/22.91 % (2955074)Instructions burned: 1016 (million)
% 100.17/22.91 % (2955080)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2841467648:i=2448:gtgl=5:bd=preordered:gtg=all_2825 on theBenchmark for (2825ds/2448Mi)
% 100.17/22.91 % (2955080)Instruction limit reached!
% 100.17/22.91 % (2955080)------------------------------
% 100.17/22.91 % (2955080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955080)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955080)Termination reason: Instruction limit
% 100.17/22.91 % (2955080)Termination phase: Property scanning
% 100.17/22.91 % (2955080)Time elapsed: 1.028 s
% 100.17/22.91 % (2955080)Peak memory usage: 173 MB
% 100.17/22.91 % (2955080)Instructions burned: 2450 (million)
% 100.17/22.91 % (2955082)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=4209709620:i=3223:kws=precedence:fgj=on:av=off_2813 on theBenchmark for (2813ds/3223Mi)
% 100.17/22.91 % (2955077)Instruction limit reached!
% 100.17/22.91 % (2955077)------------------------------
% 100.17/22.91 % (2955077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955077)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955077)Termination reason: Instruction limit
% 100.17/22.91 % (2955077)Termination phase: Function definition elimination
% 100.17/22.91 % (2955077)Time elapsed: 1.949 s
% 100.17/22.91 % (2955077)Peak memory usage: 341 MB
% 100.17/22.91 % (2955077)Instructions burned: 5785 (million)
% 100.17/22.91 % (2955084)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=595037847:st=5.6:i=2033:sd=3:ss=axioms_2811 on theBenchmark for (2811ds/2033Mi)
% 100.17/22.91 % (2955084)Instruction limit reached!
% 100.17/22.91 % (2955084)------------------------------
% 100.17/22.91 % (2955084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955084)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955084)Termination reason: Instruction limit
% 100.17/22.91 % (2955084)Termination phase: Property scanning
% 100.17/22.91 % (2955084)Time elapsed: 0.810 s
% 100.17/22.91 % (2955084)Peak memory usage: 208 MB
% 100.17/22.91 % (2955084)Instructions burned: 2036 (million)
% 100.17/22.91 % (2955086)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3737816725:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2801 on theBenchmark for (2801ds/2055Mi)
% 100.17/22.91 % (2955086)Instruction limit reached!
% 100.17/22.91 % (2955086)------------------------------
% 100.17/22.91 % (2955086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955086)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955086)Termination reason: Instruction limit
% 100.17/22.91 % (2955086)Termination phase: Property scanning
% 100.17/22.91 % (2955086)Time elapsed: 0.662 s
% 100.17/22.91 % (2955086)Peak memory usage: 178 MB
% 100.17/22.91 % (2955086)Instructions burned: 2056 (million)
% 100.17/22.91 % (2955088)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1690460291:i=21611:sd=3:ss=axioms_2793 on theBenchmark for (2793ds/21611Mi)
% 100.17/22.91 % (2955082)Instruction limit reached!
% 100.17/22.91 % (2955082)------------------------------
% 100.17/22.91 % (2955082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955082)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955082)Termination reason: Instruction limit
% 100.17/22.91 % (2955082)Termination phase: Preprocessing 3
% 100.17/22.91 % (2955082)Time elapsed: 2.201 s
% 100.17/22.91 % (2955082)Peak memory usage: 312 MB
% 100.17/22.91 % (2955082)Instructions burned: 3225 (million)
% 100.17/22.91 % (2955090)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=826189147:i=4835:sd=13:ss=axioms:sgt=23_2789 on theBenchmark for (2789ds/4835Mi)
% 100.17/22.91 % (2955068)Instruction limit reached!
% 100.17/22.91 % (2955068)------------------------------
% 100.17/22.91 % (2955068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.17/22.91 % (2955068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.17/22.91 % (2955068)CaDiCaL version: 2.1.3
% 100.17/22.91 % (2955068)Termination reason: Instruction limit
% 100.17/22.91 % (2955068)Termination phase: Saturation
% 100.17/22.91 % (2955068)Time elapsed: 7.702 s
% 100.17/22.91 % (2955068)Peak memory usage: 299 MB
% 100.17/22.91 % (2955068)Instructions burned: 11145 (million)
% 100.17/22.91 % (2955092)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3513574989:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2782 on theBenchmark for (2782ds/797Mi)
% 100.17/22.91 % (2955088)First to succeed.
% 100.17/22.91 % (2955088)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2954979"
% 100.17/22.91 % (2955088)Refutation found. Thanks to Tanya!
% 100.17/22.91 % SZS status Theorem for theBenchmark
% 100.17/22.91 % SZS output start Proof for theBenchmark
% See solution above
% 147.38/23.13 % (2955088)------------------------------
% 147.38/23.13 % (2955088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 147.38/23.13 % (2955088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.38/23.13 % (2955088)CaDiCaL version: 2.1.3
% 147.38/23.13 % (2955088)Termination reason: Refutation
% 147.38/23.13 % (2955088)Time elapsed: 1.111 s
% 147.38/23.13 % (2955088)Peak memory usage: 259 MB
% 147.38/23.13 % (2955088)Instructions burned: 2913 (million)
% 147.38/23.13 % (2955088)------------------------------
% 147.38/23.13 % (2955088)------------------------------
% 147.38/23.13 % (2954979)Success in time 22.285 s
% 147.38/23.13 % Vampire exiting
%------------------------------------------------------------------------------