%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP013+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:28:11 AM UTC 2026
% Result : Theorem 63.83s 22.29s
% Output : Refutation 141.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 38
% Syntax : Number of formulae : 174 ( 57 unt; 30 def)
% Number of atoms : 427 ( 76 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 461 ( 208 ~; 199 |; 12 &)
% ( 19 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 20 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 19 con; 0-2 aty)
% Number of variables : 93 ( 0 sgn 87 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_tp) ).
fof(f1221,axiom,
mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Earithmetic_2E_2D) ).
fof(f1325,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,X1),X0))
=> ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,X0),X1)),X1) = X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2ESUB__ADD) ).
fof(f10570,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Ewords_2En2w) ).
fof(f10875,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ! [X2] :
( mem(X2,ty_2Enum_2Enum)
=> ap(ap(c_2Ewords_2Eword__add(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2)) = ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2B,X1),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2Eword__add__n2w) ).
fof(f11094,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Efcp_2Ecart(bool,X0))
=> ! [X2] :
( mem(X2,ty_2Efcp_2Ecart(bool,X0))
=> ap(ap(c_2Ewords_2Eword__sub(X0),X1),ap(ap(c_2Ewords_2Eword__sub(X0),X1),X2)) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__SUB__SUB2) ).
fof(f11106,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Efcp_2Ecart(bool,X0))
=> ! [X2] :
( mem(X2,ty_2Efcp_2Ecart(bool,X0))
=> ap(ap(c_2Ewords_2Eword__sub(X0),ap(ap(c_2Ewords_2Eword__add(X0),X2),X1)),X2) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__ADD__SUB2) ).
fof(f11132,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ! [X2] :
( mem(X2,ty_2Enum_2Enum)
=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,X2),X1))
=> ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2D,X1),X2)) = ap(ap(c_2Ewords_2Eword__sub(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Ewords_2En2w__sub) ).
fof(f11133,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ! [X2] :
( mem(X2,ty_2Enum_2Enum)
=> ( p(ap(ap(c_2Earithmetic_2E_3C_3D,X2),X1))
=> ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2D,X1),X2)) = ap(ap(c_2Ewords_2Eword__sub(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f11132]) ).
fof(f11204,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2D,X1),X2)) != ap(ap(c_2Ewords_2Eword__sub(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2))
& p(ap(ap(c_2Earithmetic_2E_3C_3D,X2),X1))
& mem(X2,ty_2Enum_2Enum) )
& mem(X1,ty_2Enum_2Enum) )
& ne(X0) ),
inference(ennf_transformation,[],[f11133]) ).
fof(f11205,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2D,X1),X2)) != ap(ap(c_2Ewords_2Eword__sub(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2))
& p(ap(ap(c_2Earithmetic_2E_3C_3D,X2),X1))
& mem(X2,ty_2Enum_2Enum) )
& mem(X1,ty_2Enum_2Enum) )
& ne(X0) ),
inference(flattening,[],[f11204]) ).
fof(f11468,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f11529,plain,
! [X0] :
( ! [X1] :
( ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,X0),X1)),X1) = X0
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X1),X0))
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f1325]) ).
fof(f11530,plain,
! [X0] :
( ! [X1] :
( ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,X0),X1)),X1) = X0
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X1),X0))
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(flattening,[],[f11529]) ).
fof(f11605,plain,
! [X0] :
( mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0)))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f10570]) ).
fof(f11612,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ap(ap(c_2Ewords_2Eword__sub(X0),ap(ap(c_2Ewords_2Eword__add(X0),X2),X1)),X2) = X1
| ~ mem(X2,ty_2Efcp_2Ecart(bool,X0)) )
| ~ mem(X1,ty_2Efcp_2Ecart(bool,X0)) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f11106]) ).
fof(f11621,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ap(ap(c_2Ewords_2Eword__sub(X0),X1),ap(ap(c_2Ewords_2Eword__sub(X0),X1),X2)) = X2
| ~ mem(X2,ty_2Efcp_2Ecart(bool,X0)) )
| ~ mem(X1,ty_2Efcp_2Ecart(bool,X0)) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f11094]) ).
fof(f11987,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ap(ap(c_2Ewords_2Eword__add(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2)) = ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2B,X1),X2))
| ~ mem(X2,ty_2Enum_2Enum) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f10875]) ).
fof(f12709,plain,
( ap(c_2Ewords_2En2w(sK238),ap(ap(c_2Earithmetic_2E_2D,sK239),sK240)) != ap(ap(c_2Ewords_2Eword__sub(sK238),ap(c_2Ewords_2En2w(sK238),sK239)),ap(c_2Ewords_2En2w(sK238),sK240))
& p(ap(ap(c_2Earithmetic_2E_3C_3D,sK240),sK239))
& mem(sK240,ty_2Enum_2Enum)
& mem(sK239,ty_2Enum_2Enum)
& ne(sK238) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK238,sK239,sK240]),skolemize(X0,sK238),skolemize(X1,sK239),skolemize(X2,sK240)],[f11205]) ).
fof(f14152,plain,
ne(sK238),
inference(cnf_transformation,[],[f12709]) ).
fof(f14153,plain,
mem(sK239,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f12709]) ).
fof(f14154,plain,
mem(sK240,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f12709]) ).
fof(f14155,plain,
p(ap(ap(c_2Earithmetic_2E_3C_3D,sK240),sK239)),
inference(cnf_transformation,[],[f12709]) ).
fof(f14156,plain,
ap(c_2Ewords_2En2w(sK238),ap(ap(c_2Earithmetic_2E_2D,sK239),sK240)) != ap(ap(c_2Ewords_2Eword__sub(sK238),ap(c_2Ewords_2En2w(sK238),sK239)),ap(c_2Ewords_2En2w(sK238),sK240)),
inference(cnf_transformation,[],[f12709]) ).
fof(f15223,plain,
! [X2,X3,X0,X1] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f11468]) ).
fof(f15369,plain,
! [X0,X1] :
( ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,X0),X1)),X1) = X0
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X1),X0))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f11530]) ).
fof(f15378,plain,
mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
inference(cnf_transformation,[],[f1221]) ).
fof(f15501,plain,
! [X0] :
( mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f11605]) ).
fof(f15508,plain,
! [X2,X0,X1] :
( ap(ap(c_2Ewords_2Eword__sub(X0),ap(ap(c_2Ewords_2Eword__add(X0),X2),X1)),X2) = X1
| ~ mem(X2,ty_2Efcp_2Ecart(bool,X0))
| ~ mem(X1,ty_2Efcp_2Ecart(bool,X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f11612]) ).
fof(f15522,plain,
! [X2,X0,X1] :
( ap(ap(c_2Ewords_2Eword__sub(X0),X1),ap(ap(c_2Ewords_2Eword__sub(X0),X1),X2)) = X2
| ~ mem(X2,ty_2Efcp_2Ecart(bool,X0))
| ~ mem(X1,ty_2Efcp_2Ecart(bool,X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f11621]) ).
fof(f16963,plain,
! [X2,X0,X1] :
( ap(ap(c_2Ewords_2Eword__add(X0),ap(c_2Ewords_2En2w(X0),X1)),ap(c_2Ewords_2En2w(X0),X2)) = ap(c_2Ewords_2En2w(X0),ap(ap(c_2Earithmetic_2E_2B,X1),X2))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f11987]) ).
fof(f17959,definition,
sF958 = c_2Ewords_2En2w(sK238),
introduced(definition,[new_symbols(definition,[sF958])],[function_definition]) ).
fof(f17960,plain,
c_2Ewords_2En2w(sK238) = sF958,
inference(reorient_equations,[],[f17959]) ).
fof(f17961,definition,
sF959 = ap(c_2Earithmetic_2E_2D,sK239),
introduced(definition,[new_symbols(definition,[sF959])],[function_definition]) ).
fof(f17962,plain,
ap(c_2Earithmetic_2E_2D,sK239) = sF959,
inference(reorient_equations,[],[f17961]) ).
fof(f17963,definition,
sF960 = ap(sF959,sK240),
introduced(definition,[new_symbols(definition,[sF960])],[function_definition]) ).
fof(f17964,plain,
ap(sF959,sK240) = sF960,
inference(reorient_equations,[],[f17963]) ).
fof(f17965,definition,
sF961 = ap(sF958,sF960),
introduced(definition,[new_symbols(definition,[sF961])],[function_definition]) ).
fof(f17966,plain,
ap(sF958,sF960) = sF961,
inference(reorient_equations,[],[f17965]) ).
fof(f17967,definition,
sF962 = c_2Ewords_2Eword__sub(sK238),
introduced(definition,[new_symbols(definition,[sF962])],[function_definition]) ).
fof(f17968,plain,
c_2Ewords_2Eword__sub(sK238) = sF962,
inference(reorient_equations,[],[f17967]) ).
fof(f17969,definition,
sF963 = ap(sF958,sK239),
introduced(definition,[new_symbols(definition,[sF963])],[function_definition]) ).
fof(f17970,plain,
ap(sF958,sK239) = sF963,
inference(reorient_equations,[],[f17969]) ).
fof(f17971,definition,
sF964 = ap(sF962,sF963),
introduced(definition,[new_symbols(definition,[sF964])],[function_definition]) ).
fof(f17972,plain,
ap(sF962,sF963) = sF964,
inference(reorient_equations,[],[f17971]) ).
fof(f17973,definition,
sF965 = ap(sF958,sK240),
introduced(definition,[new_symbols(definition,[sF965])],[function_definition]) ).
fof(f17974,plain,
ap(sF958,sK240) = sF965,
inference(reorient_equations,[],[f17973]) ).
fof(f17975,definition,
sF966 = ap(sF964,sF965),
introduced(definition,[new_symbols(definition,[sF966])],[function_definition]) ).
fof(f17976,plain,
ap(sF964,sF965) = sF966,
inference(reorient_equations,[],[f17975]) ).
fof(f17977,plain,
sF961 != sF966,
inference(definition_folding,[],[f14156,f17976,f17974,f17960,f17972,f17970,f17960,f17968,f17966,f17964,f17962,f17960]) ).
fof(f17978,definition,
sF967 = ap(c_2Earithmetic_2E_3C_3D,sK240),
introduced(definition,[new_symbols(definition,[sF967])],[function_definition]) ).
fof(f17979,plain,
ap(c_2Earithmetic_2E_3C_3D,sK240) = sF967,
inference(reorient_equations,[],[f17978]) ).
fof(f17980,definition,
sF968 = ap(sF967,sK239),
introduced(definition,[new_symbols(definition,[sF968])],[function_definition]) ).
fof(f17981,plain,
ap(sF967,sK239) = sF968,
inference(reorient_equations,[],[f17980]) ).
fof(f17982,plain,
p(sF968),
inference(definition_folding,[],[f14155,f17981,f17979]) ).
fof(f18413,plain,
! [X0,X1] :
( ~ mem(c_2Earithmetic_2E_2D,arr(X1,X0))
| ~ mem(sK239,X1)
| mem(sF959,X0) ),
inference(superposition,[],[f15223,f17962]) ).
fof(f18415,plain,
! [X0,X1] :
( ~ mem(sF958,arr(X1,X0))
| ~ mem(sF960,X1)
| mem(sF961,X0) ),
inference(superposition,[],[f15223,f17966]) ).
fof(f18416,plain,
! [X0,X1] :
( ~ mem(sF958,arr(X1,X0))
| ~ mem(sK239,X1)
| mem(sF963,X0) ),
inference(superposition,[],[f15223,f17970]) ).
fof(f18417,plain,
! [X0,X1] :
( ~ mem(sF958,arr(X1,X0))
| ~ mem(sK240,X1)
| mem(sF965,X0) ),
inference(superposition,[],[f15223,f17974]) ).
fof(f18418,plain,
! [X0,X1] :
( ~ mem(sF959,arr(X1,X0))
| ~ mem(sK240,X1)
| mem(sF960,X0) ),
inference(superposition,[],[f15223,f17964]) ).
fof(f18425,definition,
( spl969_96
<=> ne(sK238) ),
introduced(definition,[new_symbols(definition,[spl969_96])],[avatar_definition]) ).
fof(f18434,plain,
spl969_96,
inference(avatar_split_clause,[],[f14152,f18425]) ).
fof(f18442,plain,
( mem(sF958,arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,sK238)))
| ~ ne(sK238) ),
inference(superposition,[],[f15501,f17960]) ).
fof(f18444,definition,
( spl969_99
<=> mem(sF958,arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,sK238))) ),
introduced(definition,[new_symbols(definition,[spl969_99])],[avatar_definition]) ).
fof(f18446,plain,
( mem(sF958,arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,sK238)))
| ~ spl969_99 ),
inference(avatar_component_clause,[],[f18444]) ).
fof(f18447,plain,
( ~ spl969_96
| spl969_99 ),
inference(avatar_split_clause,[],[f18442,f18444,f18425]) ).
fof(f18448,plain,
( ~ mem(sK239,ty_2Enum_2Enum)
| mem(sF963,ty_2Efcp_2Ecart(bool,sK238))
| ~ spl969_99 ),
inference(resolution,[],[f18446,f18416]) ).
fof(f18449,plain,
( ~ mem(sK240,ty_2Enum_2Enum)
| mem(sF965,ty_2Efcp_2Ecart(bool,sK238))
| ~ spl969_99 ),
inference(resolution,[],[f18446,f18417]) ).
fof(f18450,plain,
( ~ mem(sF960,ty_2Enum_2Enum)
| mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ spl969_99 ),
inference(resolution,[],[f18446,f18415]) ).
fof(f18452,definition,
( spl969_100
<=> mem(sF961,ty_2Efcp_2Ecart(bool,sK238)) ),
introduced(definition,[new_symbols(definition,[spl969_100])],[avatar_definition]) ).
fof(f18456,definition,
( spl969_101
<=> mem(sF960,ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl969_101])],[avatar_definition]) ).
fof(f18459,plain,
( spl969_100
| ~ spl969_101
| ~ spl969_99 ),
inference(avatar_split_clause,[],[f18450,f18444,f18456,f18452]) ).
fof(f18461,definition,
( spl969_102
<=> mem(sF965,ty_2Efcp_2Ecart(bool,sK238)) ),
introduced(definition,[new_symbols(definition,[spl969_102])],[avatar_definition]) ).
fof(f18465,definition,
( spl969_103
<=> mem(sK240,ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl969_103])],[avatar_definition]) ).
fof(f18468,plain,
( spl969_102
| ~ spl969_103
| ~ spl969_99 ),
inference(avatar_split_clause,[],[f18449,f18444,f18465,f18461]) ).
fof(f18470,definition,
( spl969_104
<=> mem(sF963,ty_2Efcp_2Ecart(bool,sK238)) ),
introduced(definition,[new_symbols(definition,[spl969_104])],[avatar_definition]) ).
fof(f18474,definition,
( spl969_105
<=> mem(sK239,ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl969_105])],[avatar_definition]) ).
fof(f18477,plain,
( spl969_104
| ~ spl969_105
| ~ spl969_99 ),
inference(avatar_split_clause,[],[f18448,f18444,f18474,f18470]) ).
fof(f18480,plain,
spl969_103,
inference(avatar_split_clause,[],[f14154,f18465]) ).
fof(f18483,plain,
spl969_105,
inference(avatar_split_clause,[],[f14153,f18474]) ).
fof(f18484,plain,
! [X0,X1] :
( ap(ap(sF962,X0),ap(ap(sF962,X0),X1)) = X1
| ~ mem(X1,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238))
| ~ ne(sK238) ),
inference(superposition,[],[f15522,f17968]) ).
fof(f18487,definition,
( spl969_106
<=> ! [X0,X1] :
( ap(ap(sF962,X0),ap(ap(sF962,X0),X1)) = X1
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(X1,ty_2Efcp_2Ecart(bool,sK238)) ) ),
introduced(definition,[new_symbols(definition,[spl969_106])],[avatar_definition]) ).
fof(f18488,plain,
( ! [X0,X1] :
( ap(ap(sF962,X0),ap(ap(sF962,X0),X1)) = X1
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(X1,ty_2Efcp_2Ecart(bool,sK238)) )
| ~ spl969_106 ),
inference(avatar_component_clause,[],[f18487]) ).
fof(f18489,plain,
( ~ spl969_96
| spl969_106 ),
inference(avatar_split_clause,[],[f18484,f18487,f18425]) ).
fof(f18499,plain,
! [X0,X1] :
( ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),ap(sF958,X1)) = ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),X1))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ ne(sK238) ),
inference(superposition,[],[f16963,f17960]) ).
fof(f18511,definition,
( spl969_108
<=> ! [X0,X1] :
( ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),ap(sF958,X1)) = ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),X1))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ) ),
introduced(definition,[new_symbols(definition,[spl969_108])],[avatar_definition]) ).
fof(f18512,plain,
( ! [X0,X1] :
( ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),ap(sF958,X1)) = ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),X1))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ spl969_108 ),
inference(avatar_component_clause,[],[f18511]) ).
fof(f18513,plain,
( ~ spl969_96
| spl969_108 ),
inference(avatar_split_clause,[],[f18499,f18511,f18425]) ).
fof(f18541,plain,
( ~ mem(sK239,ty_2Enum_2Enum)
| mem(sF959,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(resolution,[],[f15378,f18413]) ).
fof(f18543,definition,
( spl969_113
<=> mem(sF959,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
introduced(definition,[new_symbols(definition,[spl969_113])],[avatar_definition]) ).
fof(f18545,plain,
( mem(sF959,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))
| ~ spl969_113 ),
inference(avatar_component_clause,[],[f18543]) ).
fof(f18546,plain,
( spl969_113
| ~ spl969_105 ),
inference(avatar_split_clause,[],[f18541,f18474,f18543]) ).
fof(f18547,plain,
( ~ mem(sK240,ty_2Enum_2Enum)
| mem(sF960,ty_2Enum_2Enum)
| ~ spl969_113 ),
inference(resolution,[],[f18545,f18418]) ).
fof(f18548,plain,
( spl969_101
| ~ spl969_103
| ~ spl969_113 ),
inference(avatar_split_clause,[],[f18547,f18543,f18465,f18456]) ).
fof(f18551,plain,
( ! [X0] :
( ap(sF964,ap(sF964,X0)) = X0
| ~ mem(sF963,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238)) )
| ~ spl969_106 ),
inference(superposition,[],[f18488,f17972]) ).
fof(f18554,definition,
( spl969_114
<=> ! [X0] :
( ap(sF964,ap(sF964,X0)) = X0
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238)) ) ),
introduced(definition,[new_symbols(definition,[spl969_114])],[avatar_definition]) ).
fof(f18555,plain,
( ! [X0] :
( ap(sF964,ap(sF964,X0)) = X0
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK238)) )
| ~ spl969_114 ),
inference(avatar_component_clause,[],[f18554]) ).
fof(f18556,plain,
( ~ spl969_104
| spl969_114
| ~ spl969_106 ),
inference(avatar_split_clause,[],[f18551,f18487,f18554,f18470]) ).
fof(f18639,plain,
( ! [X0] :
( ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),sF965)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(sK240,ty_2Enum_2Enum) )
| ~ spl969_108 ),
inference(superposition,[],[f18512,f17974]) ).
fof(f18647,definition,
( spl969_125
<=> ! [X0] :
( ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),sF965)
| ~ mem(X0,ty_2Enum_2Enum) ) ),
introduced(definition,[new_symbols(definition,[spl969_125])],[avatar_definition]) ).
fof(f18648,plain,
( ! [X0] :
( ap(sF958,ap(ap(c_2Earithmetic_2E_2B,X0),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),ap(sF958,X0)),sF965)
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl969_125 ),
inference(avatar_component_clause,[],[f18647]) ).
fof(f18649,plain,
( ~ spl969_103
| spl969_125
| ~ spl969_108 ),
inference(avatar_split_clause,[],[f18639,f18511,f18647,f18465]) ).
fof(f18670,plain,
( ap(sF958,ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),sF961),sF965)
| ~ mem(sF960,ty_2Enum_2Enum)
| ~ spl969_125 ),
inference(superposition,[],[f18648,f17966]) ).
fof(f18673,definition,
( spl969_130
<=> ap(sF958,ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),sF961),sF965) ),
introduced(definition,[new_symbols(definition,[spl969_130])],[avatar_definition]) ).
fof(f18675,plain,
( ap(sF958,ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)) = ap(ap(c_2Ewords_2Eword__add(sK238),sF961),sF965)
| ~ spl969_130 ),
inference(avatar_component_clause,[],[f18673]) ).
fof(f18676,plain,
( ~ spl969_101
| spl969_130
| ~ spl969_125 ),
inference(avatar_split_clause,[],[f18670,f18647,f18673,f18456]) ).
fof(f18771,plain,
! [X0] :
( sK239 = ap(ap(c_2Earithmetic_2E_2B,ap(sF959,X0)),X0)
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X0),sK239))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(sK239,ty_2Enum_2Enum) ),
inference(superposition,[],[f15369,f17962]) ).
fof(f18776,definition,
( spl969_143
<=> ! [X0] :
( sK239 = ap(ap(c_2Earithmetic_2E_2B,ap(sF959,X0)),X0)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X0),sK239)) ) ),
introduced(definition,[new_symbols(definition,[spl969_143])],[avatar_definition]) ).
fof(f18777,plain,
( ! [X0] :
( sK239 = ap(ap(c_2Earithmetic_2E_2B,ap(sF959,X0)),X0)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,X0),sK239)) )
| ~ spl969_143 ),
inference(avatar_component_clause,[],[f18776]) ).
fof(f18778,plain,
( ~ spl969_105
| spl969_143 ),
inference(avatar_split_clause,[],[f18771,f18776,f18474]) ).
fof(f18779,plain,
( sK239 = ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)
| ~ mem(sK240,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Earithmetic_2E_3C_3D,sK240),sK239))
| ~ spl969_143 ),
inference(superposition,[],[f18777,f17964]) ).
fof(f18791,plain,
( ~ p(ap(sF967,sK239))
| sK239 = ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)
| ~ mem(sK240,ty_2Enum_2Enum)
| ~ spl969_143 ),
inference(forward_demodulation,[],[f18779,f17979]) ).
fof(f18792,plain,
( ~ p(sF968)
| sK239 = ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)
| ~ mem(sK240,ty_2Enum_2Enum)
| ~ spl969_143 ),
inference(forward_demodulation,[],[f18791,f17981]) ).
fof(f18794,definition,
( spl969_146
<=> sK239 = ap(ap(c_2Earithmetic_2E_2B,sF960),sK240) ),
introduced(definition,[new_symbols(definition,[spl969_146])],[avatar_definition]) ).
fof(f18796,plain,
( sK239 = ap(ap(c_2Earithmetic_2E_2B,sF960),sK240)
| ~ spl969_146 ),
inference(avatar_component_clause,[],[f18794]) ).
fof(f18798,definition,
( spl969_147
<=> p(sF968) ),
introduced(definition,[new_symbols(definition,[spl969_147])],[avatar_definition]) ).
fof(f18801,plain,
( ~ spl969_103
| spl969_146
| ~ spl969_147
| ~ spl969_143 ),
inference(avatar_split_clause,[],[f18792,f18776,f18798,f18794,f18465]) ).
fof(f18804,plain,
spl969_147,
inference(avatar_split_clause,[],[f17982,f18798]) ).
fof(f18899,plain,
( ap(sF958,sK239) = ap(ap(c_2Ewords_2Eword__add(sK238),sF961),sF965)
| ~ spl969_130
| ~ spl969_146 ),
inference(forward_demodulation,[],[f18675,f18796]) ).
fof(f18900,plain,
( sF963 = ap(ap(c_2Ewords_2Eword__add(sK238),sF961),sF965)
| ~ spl969_130
| ~ spl969_146 ),
inference(forward_demodulation,[],[f18899,f17970]) ).
fof(f18901,plain,
( sF965 = ap(ap(c_2Ewords_2Eword__sub(sK238),sF963),sF961)
| ~ mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(sF965,ty_2Efcp_2Ecart(bool,sK238))
| ~ ne(sK238)
| ~ spl969_130
| ~ spl969_146 ),
inference(superposition,[],[f15508,f18900]) ).
fof(f18903,plain,
( sF965 = ap(ap(sF962,sF963),sF961)
| ~ mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(sF965,ty_2Efcp_2Ecart(bool,sK238))
| ~ ne(sK238)
| ~ spl969_130
| ~ spl969_146 ),
inference(forward_demodulation,[],[f18901,f17968]) ).
fof(f18904,plain,
( sF965 = ap(sF964,sF961)
| ~ mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ mem(sF965,ty_2Efcp_2Ecart(bool,sK238))
| ~ ne(sK238)
| ~ spl969_130
| ~ spl969_146 ),
inference(forward_demodulation,[],[f18903,f17972]) ).
fof(f18906,definition,
( spl969_159
<=> sF965 = ap(sF964,sF961) ),
introduced(definition,[new_symbols(definition,[spl969_159])],[avatar_definition]) ).
fof(f18908,plain,
( sF965 = ap(sF964,sF961)
| ~ spl969_159 ),
inference(avatar_component_clause,[],[f18906]) ).
fof(f18909,plain,
( ~ spl969_96
| ~ spl969_102
| ~ spl969_100
| spl969_159
| ~ spl969_130
| ~ spl969_146 ),
inference(avatar_split_clause,[],[f18904,f18794,f18673,f18906,f18452,f18461,f18425]) ).
fof(f18910,plain,
( sF961 = ap(sF964,sF965)
| ~ mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ spl969_114
| ~ spl969_159 ),
inference(superposition,[],[f18555,f18908]) ).
fof(f18912,plain,
( sF961 = sF966
| ~ mem(sF961,ty_2Efcp_2Ecart(bool,sK238))
| ~ spl969_114
| ~ spl969_159 ),
inference(forward_demodulation,[],[f18910,f17976]) ).
fof(f18914,definition,
( spl969_160
<=> sF961 = sF966 ),
introduced(definition,[new_symbols(definition,[spl969_160])],[avatar_definition]) ).
fof(f18916,plain,
( sF961 = sF966
| ~ spl969_160 ),
inference(avatar_component_clause,[],[f18914]) ).
fof(f18917,plain,
( ~ spl969_100
| spl969_160
| ~ spl969_114
| ~ spl969_159 ),
inference(avatar_split_clause,[],[f18912,f18906,f18554,f18914,f18452]) ).
fof(f18918,plain,
( $false
| ~ spl969_160 ),
inference(backward_subsumption_resolution,[],[f17977,f18916]) ).
fof(f18921,plain,
~ spl969_160,
inference(avatar_contradiction_clause,[],[f18918]) ).
cnf(s107,plain,
spl969_96,
inference(sat_conversion,[],[f18434]) ).
cnf(s109,plain,
( ~ spl969_96
| spl969_99 ),
inference(sat_conversion,[],[f18447]) ).
cnf(s110,plain,
( ~ spl969_99
| spl969_100
| ~ spl969_101 ),
inference(sat_conversion,[],[f18459]) ).
cnf(s111,plain,
( ~ spl969_99
| spl969_102
| ~ spl969_103 ),
inference(sat_conversion,[],[f18468]) ).
cnf(s112,plain,
( ~ spl969_99
| spl969_104
| ~ spl969_105 ),
inference(sat_conversion,[],[f18477]) ).
cnf(s114,plain,
spl969_103,
inference(sat_conversion,[],[f18480]) ).
cnf(s116,plain,
spl969_105,
inference(sat_conversion,[],[f18483]) ).
cnf(s117,plain,
( ~ spl969_96
| spl969_106 ),
inference(sat_conversion,[],[f18489]) ).
cnf(s119,plain,
( ~ spl969_96
| spl969_108 ),
inference(sat_conversion,[],[f18513]) ).
cnf(s124,plain,
( ~ spl969_105
| spl969_113 ),
inference(sat_conversion,[],[f18546]) ).
cnf(s125,plain,
( spl969_101
| ~ spl969_103
| ~ spl969_113 ),
inference(sat_conversion,[],[f18548]) ).
cnf(s126,plain,
( ~ spl969_104
| ~ spl969_106
| spl969_114 ),
inference(sat_conversion,[],[f18556]) ).
cnf(s137,plain,
( ~ spl969_103
| ~ spl969_108
| spl969_125 ),
inference(sat_conversion,[],[f18649]) ).
cnf(s142,plain,
( ~ spl969_101
| ~ spl969_125
| spl969_130 ),
inference(sat_conversion,[],[f18676]) ).
cnf(s157,plain,
( ~ spl969_105
| spl969_143 ),
inference(sat_conversion,[],[f18778]) ).
cnf(s159,plain,
( ~ spl969_103
| ~ spl969_143
| spl969_146
| ~ spl969_147 ),
inference(sat_conversion,[],[f18801]) ).
cnf(s161,plain,
spl969_147,
inference(sat_conversion,[],[f18804]) ).
cnf(s172,plain,
( ~ spl969_96
| ~ spl969_100
| ~ spl969_102
| ~ spl969_130
| ~ spl969_146
| spl969_159 ),
inference(sat_conversion,[],[f18909]) ).
cnf(s173,plain,
( ~ spl969_100
| ~ spl969_114
| ~ spl969_159
| spl969_160 ),
inference(sat_conversion,[],[f18917]) ).
cnf(s174,plain,
~ spl969_160,
inference(sat_conversion,[],[f18921]) ).
cnf(s175,plain,
( ~ spl969_100
| ~ spl969_114
| ~ spl969_159 ),
inference(rat,[],[s173,s174]) ).
cnf(s176,plain,
( ~ spl969_103
| ~ spl969_143
| spl969_146 ),
inference(rat,[],[s159,s161]) ).
cnf(s177,plain,
spl969_143,
inference(rat,[],[s157,s116]) ).
cnf(s179,plain,
spl969_113,
inference(rat,[],[s124,s116]) ).
cnf(s180,plain,
spl969_146,
inference(rat,[],[s176,s177,s114]) ).
cnf(s183,plain,
spl969_101,
inference(rat,[],[s125,s179,s114]) ).
cnf(s185,plain,
( ~ spl969_99
| spl969_104 ),
inference(rat,[],[s112,s116]) ).
cnf(s186,plain,
( ~ spl969_99
| spl969_102 ),
inference(rat,[],[s111,s114]) ).
cnf(s187,plain,
( ~ spl969_99
| spl969_100 ),
inference(rat,[],[s110,s183]) ).
cnf(s196,plain,
spl969_108,
inference(rat,[],[s119,s107]) ).
cnf(s198,plain,
spl969_106,
inference(rat,[],[s117,s107]) ).
cnf(s199,plain,
spl969_99,
inference(rat,[],[s109,s107]) ).
cnf(s206,plain,
spl969_125,
inference(rat,[],[s137,s114,s196]) ).
cnf(s208,plain,
spl969_104,
inference(rat,[],[s185,s199]) ).
cnf(s209,plain,
spl969_102,
inference(rat,[],[s186,s199]) ).
cnf(s210,plain,
spl969_100,
inference(rat,[],[s187,s199]) ).
cnf(s216,plain,
spl969_130,
inference(rat,[],[s142,s183,s206]) ).
cnf(s223,plain,
spl969_114,
inference(rat,[],[s126,s198,s208]) ).
cnf(s226,plain,
spl969_159,
inference(rat,[],[s172,s209,s180,s216,s107,s210]) ).
cnf(s228,plain,
$false,
inference(rat,[],[s175,s210,s226,s223]) ).
fof(f18922,plain,
$false,
inference(avatar_sat_refutation,[],[s228]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP013+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n005.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 11:59:34 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.55/4.55 % (3868462)Detected formulas, will run a generic FOF schedule.
% 14.55/4.55 % (3868467)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=2058079948:i=141193_2982 on theBenchmark for (2982ds/141193Mi)
% 14.55/4.55 % (3868472)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=501942471:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi)
% 14.55/4.55 % (3868468)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=1624144566:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi)
% 14.55/4.55 % (3868470)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=771062277:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi)
% 14.55/4.55 % (3868469)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=264279744:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi)
% 14.55/4.55 % (3868471)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1820111734:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi)
% 14.55/4.55 % (3868473)dis-21_1_sil=8000:lcm=predicate:random_seed=263775516:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2982 on theBenchmark for (2982ds/129Mi)
% 14.55/4.55 % (3868472)Instruction limit reached!
% 14.55/4.55 % (3868472)------------------------------
% 14.55/4.55 % (3868472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/4.55 % (3868472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/4.55 % (3868472)CaDiCaL version: 2.1.3
% 14.55/4.55 % (3868472)Termination reason: Instruction limit
% 14.55/4.55 % (3868472)Termination phase: Property scanning
% 14.55/4.55 % (3868472)Time elapsed: 0.055 s
% 14.55/4.55 % (3868472)Peak memory usage: 111 MB
% 14.55/4.55 % (3868472)Instructions burned: 140 (million)
% 14.55/4.55 % (3868470)Instruction limit reached!
% 14.55/4.55 % (3868470)------------------------------
% 14.55/4.55 % (3868470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/4.55 % (3868470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/4.55 % (3868470)CaDiCaL version: 2.1.3
% 14.55/4.55 % (3868470)Termination reason: Instruction limit
% 14.55/4.55 % (3868470)Termination phase: SInE selection
% 14.55/4.55 % (3868470)Time elapsed: 0.074 s
% 14.55/4.55 % (3868470)Peak memory usage: 110 MB
% 14.55/4.55 % (3868470)Instructions burned: 109 (million)
% 14.55/4.55 % (3868471)Instruction limit reached!
% 14.55/4.55 % (3868471)------------------------------
% 14.55/4.55 % (3868471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/4.55 % (3868471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/4.55 % (3868471)CaDiCaL version: 2.1.3
% 14.55/4.55 % (3868471)Termination reason: Instruction limit
% 14.55/4.55 % (3868471)Termination phase: Preprocessing 1
% 14.55/4.55 % (3868471)Time elapsed: 0.085 s
% 14.55/4.55 % (3868471)Peak memory usage: 111 MB
% 14.55/4.55 % (3868471)Instructions burned: 119 (million)
% 14.55/4.55 % (3868473)Instruction limit reached!
% 14.55/4.55 % (3868473)------------------------------
% 14.55/4.55 % (3868473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.55/4.55 % (3868473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.55/4.55 % (3868473)CaDiCaL version: 2.1.3
% 14.55/4.55 % (3868473)Termination reason: Instruction limit
% 14.55/4.55 % (3868473)Termination phase: SInE selection
% 14.55/4.55 % (3868473)Time elapsed: 0.081 s
% 14.55/4.55 % (3868473)Peak memory usage: 110 MB
% 14.55/4.55 % (3868473)Instructions burned: 129 (million)
% 14.55/4.55 % (3868481)lrs+10_1_sil=8000:sp=occurrence:random_seed=462565434:i=285:sd=3:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/285Mi)
% 14.55/4.55 % (3868482)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1754104309:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/157Mi)
% 14.55/4.55 % (3868483)lrs+1011_1_sil=32000:sp=occurrence:random_seed=561681175:i=325:sd=1:ss=axioms:sgt=32_2979 on theBenchmark for (2979ds/325Mi)
% 14.55/4.55 % (3868484)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=1871690330:s2a=on:i=248:s2at=1.23:gtg=position_2979 on theBenchmark for (2979ds/248Mi)
% 14.55/4.55 % (3868482)Instruction limit reached!
% 21.46/5.43 % (3868482)------------------------------
% 21.46/5.43 % (3868482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868482)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868482)Termination reason: Instruction limit
% 21.46/5.43 % (3868482)Termination phase: Property scanning
% 21.46/5.43 % (3868482)Time elapsed: 0.061 s
% 21.46/5.43 % (3868482)Peak memory usage: 111 MB
% 21.46/5.43 % (3868482)Instructions burned: 159 (million)
% 21.46/5.43 % (3868484)Instruction limit reached!
% 21.46/5.43 % (3868484)------------------------------
% 21.46/5.43 % (3868484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868484)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868484)Termination reason: Instruction limit
% 21.46/5.43 % (3868484)Termination phase: Property scanning
% 21.46/5.43 % (3868484)Time elapsed: 0.095 s
% 21.46/5.43 % (3868484)Peak memory usage: 111 MB
% 21.46/5.43 % (3868484)Instructions burned: 249 (million)
% 21.46/5.43 % (3868481)Instruction limit reached!
% 21.46/5.43 % (3868481)------------------------------
% 21.46/5.43 % (3868481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868481)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868481)Termination reason: Instruction limit
% 21.46/5.43 % (3868481)Termination phase: Saturation
% 21.46/5.43 % (3868481)Time elapsed: 0.174 s
% 21.46/5.43 % (3868481)Peak memory usage: 117 MB
% 21.46/5.43 % (3868481)Instructions burned: 285 (million)
% 21.46/5.43 % (3868489)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2740751246:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2977 on theBenchmark for (2977ds/294Mi)
% 21.46/5.43 % (3868483)Instruction limit reached!
% 21.46/5.43 % (3868483)------------------------------
% 21.46/5.43 % (3868483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868483)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868483)Termination reason: Instruction limit
% 21.46/5.43 % (3868483)Termination phase: Saturation
% 21.46/5.43 % (3868483)Time elapsed: 0.215 s
% 21.46/5.43 % (3868483)Peak memory usage: 117 MB
% 21.46/5.43 % (3868483)Instructions burned: 325 (million)
% 21.46/5.43 % (3868490)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3554509121:i=2350_2977 on theBenchmark for (2977ds/2350Mi)
% 21.46/5.43 % (3868491)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2777314974:cts=off:i=113:fsr=off:ss=included:sgt=4_2977 on theBenchmark for (2977ds/113Mi)
% 21.46/5.43 % (3868491)Instruction limit reached!
% 21.46/5.43 % (3868491)------------------------------
% 21.46/5.43 % (3868491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868491)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868491)Termination reason: Instruction limit
% 21.46/5.43 % (3868491)Termination phase: SInE selection
% 21.46/5.43 % (3868491)Time elapsed: 0.082 s
% 21.46/5.43 % (3868491)Peak memory usage: 110 MB
% 21.46/5.43 % (3868491)Instructions burned: 114 (million)
% 21.46/5.43 % (3868493)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=60473951:i=127:av=off:fsr=off:sup=off_2976 on theBenchmark for (2976ds/127Mi)
% 21.46/5.43 % (3868489)Instruction limit reached!
% 21.46/5.43 % (3868489)------------------------------
% 21.46/5.43 % (3868489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868489)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868489)Termination reason: Instruction limit
% 21.46/5.43 % (3868489)Termination phase: Property scanning
% 21.46/5.43 % (3868489)Time elapsed: 0.196 s
% 21.46/5.43 % (3868489)Peak memory usage: 117 MB
% 21.46/5.43 % (3868489)Instructions burned: 294 (million)
% 21.46/5.43 % (3868493)Instruction limit reached!
% 21.46/5.43 % (3868493)------------------------------
% 21.46/5.43 % (3868493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/5.43 % (3868493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/5.43 % (3868493)CaDiCaL version: 2.1.3
% 21.46/5.43 % (3868493)Termination reason: Instruction limit
% 57.16/10.45 % (3868493)Termination phase: Preprocessing 1
% 57.16/10.45 % (3868493)Time elapsed: 0.092 s
% 57.16/10.45 % (3868493)Peak memory usage: 111 MB
% 57.16/10.45 % (3868493)Instructions burned: 128 (million)
% 57.16/10.45 % (3868496)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2073132033:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2974 on theBenchmark for (2974ds/114Mi)
% 57.16/10.45 % (3868498)lrs+10_1_sil=8000:sp=occurrence:random_seed=1185143299:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 57.16/10.45 % (3868496)Instruction limit reached!
% 57.16/10.45 % (3868496)------------------------------
% 57.16/10.45 % (3868496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.16/10.45 % (3868496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.16/10.45 % (3868496)CaDiCaL version: 2.1.3
% 57.16/10.45 % (3868496)Termination reason: Instruction limit
% 57.16/10.45 % (3868496)Termination phase: Property scanning
% 57.16/10.45 % (3868496)Time elapsed: 0.047 s
% 57.16/10.45 % (3868496)Peak memory usage: 111 MB
% 57.16/10.45 % (3868496)Instructions burned: 116 (million)
% 57.16/10.45 % (3868499)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=211881893:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi)
% 57.16/10.45 % (3868502)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3194252453:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi)
% 57.16/10.45 % (3868499)Instruction limit reached!
% 57.16/10.45 % (3868499)------------------------------
% 57.16/10.45 % (3868499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.16/10.45 % (3868499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.16/10.45 % (3868499)CaDiCaL version: 2.1.3
% 57.16/10.45 % (3868499)Termination reason: Instruction limit
% 57.16/10.45 % (3868499)Termination phase: Saturation
% 57.16/10.45 % (3868499)Time elapsed: 0.253 s
% 57.16/10.45 % (3868499)Peak memory usage: 120 MB
% 57.16/10.45 % (3868499)Instructions burned: 439 (million)
% 57.16/10.45 % (3868505)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=905136940:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2969 on theBenchmark for (2969ds/134Mi)
% 57.16/10.45 % (3868498)Instruction limit reached!
% 57.16/10.45 % (3868498)------------------------------
% 57.16/10.45 % (3868498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.16/10.45 % (3868498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.16/10.45 % (3868498)CaDiCaL version: 2.1.3
% 57.16/10.45 % (3868498)Termination reason: Instruction limit
% 57.16/10.45 % (3868498)Termination phase: Saturation
% 57.16/10.45 % (3868498)Time elapsed: 0.505 s
% 57.16/10.45 % (3868498)Peak memory usage: 126 MB
% 57.16/10.45 % (3868498)Instructions burned: 909 (million)
% 57.16/10.45 % (3868505)Instruction limit reached!
% 57.16/10.45 % (3868505)------------------------------
% 57.16/10.45 % (3868505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.16/10.45 % (3868505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.16/10.45 % (3868505)CaDiCaL version: 2.1.3
% 57.16/10.45 % (3868505)Termination reason: Instruction limit
% 57.16/10.45 % (3868505)Termination phase: Preprocessing 1
% 57.16/10.45 % (3868505)Time elapsed: 0.106 s
% 57.16/10.45 % (3868505)Peak memory usage: 111 MB
% 57.16/10.45 % (3868505)Instructions burned: 135 (million)
% 57.16/10.45 % (3868507)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=80769746:st=8:i=592:sd=3:ep=RST:ss=axioms_2968 on theBenchmark for (2968ds/592Mi)
% 57.16/10.45 % (3868508)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1189026256:st=3:i=13193:sd=3:ss=axioms_2967 on theBenchmark for (2967ds/13193Mi)
% 57.16/10.45 % (3868490)Instruction limit reached!
% 57.16/10.45 % (3868490)------------------------------
% 57.16/10.45 % (3868490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.16/10.45 % (3868490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.16/10.45 % (3868490)CaDiCaL version: 2.1.3
% 57.16/10.45 % (3868490)Termination reason: Instruction limit
% 57.16/10.45 % (3868490)Termination phase: Property scanning
% 57.16/10.45 % (3868490)Time elapsed: 1.204 s
% 57.16/10.45 % (3868490)Peak memory usage: 170 MB
% 57.16/10.45 % (3868490)Instructions burned: 2352 (million)
% 57.16/10.45 % (3868507)Instruction limit reached!
% 57.16/10.45 % (3868507)------------------------------
% 57.16/10.45 % (3868507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868507)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868507)Termination reason: Instruction limit
% 97.46/16.09 % (3868507)Termination phase: Preprocessing 3
% 97.46/16.09 % (3868507)Time elapsed: 0.364 s
% 97.46/16.09 % (3868507)Peak memory usage: 122 MB
% 97.46/16.09 % (3868507)Instructions burned: 593 (million)
% 97.46/16.09 % (3868511)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=2065023204:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/125Mi)
% 97.46/16.09 % (3868511)Instruction limit reached!
% 97.46/16.09 % (3868511)------------------------------
% 97.46/16.09 % (3868511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868511)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868511)Termination reason: Instruction limit
% 97.46/16.09 % (3868511)Termination phase: Property scanning
% 97.46/16.09 % (3868511)Time elapsed: 0.050 s
% 97.46/16.09 % (3868511)Peak memory usage: 111 MB
% 97.46/16.09 % (3868511)Instructions burned: 126 (million)
% 97.46/16.09 % (3868512)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3353049530:i=134:gtgl=5:slsql=off:gtg=exists_sym_2963 on theBenchmark for (2963ds/134Mi)
% 97.46/16.09 % (3868512)Instruction limit reached!
% 97.46/16.09 % (3868512)------------------------------
% 97.46/16.09 % (3868512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868512)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868512)Termination reason: Instruction limit
% 97.46/16.09 % (3868512)Termination phase: Property scanning
% 97.46/16.09 % (3868512)Time elapsed: 0.056 s
% 97.46/16.09 % (3868512)Peak memory usage: 111 MB
% 97.46/16.09 % (3868512)Instructions burned: 136 (million)
% 97.46/16.09 % (3868514)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2372583353:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi)
% 97.46/16.09 % (3868514)Instruction limit reached!
% 97.46/16.09 % (3868514)------------------------------
% 97.46/16.09 % (3868514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868514)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868514)Termination reason: Instruction limit
% 97.46/16.09 % (3868514)Termination phase: Property scanning
% 97.46/16.09 % (3868514)Time elapsed: 0.106 s
% 97.46/16.09 % (3868514)Peak memory usage: 113 MB
% 97.46/16.09 % (3868514)Instructions burned: 142 (million)
% 97.46/16.09 % (3868516)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1827344818:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2960 on theBenchmark for (2960ds/431Mi)
% 97.46/16.09 % (3868519)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=1920592819:i=6060:aac=none:ins=25_2959 on theBenchmark for (2959ds/6060Mi)
% 97.46/16.09 % (3868516)Instruction limit reached!
% 97.46/16.09 % (3868516)------------------------------
% 97.46/16.09 % (3868516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868516)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868516)Termination reason: Instruction limit
% 97.46/16.09 % (3868516)Termination phase: Saturation
% 97.46/16.09 % (3868516)Time elapsed: 0.267 s
% 97.46/16.09 % (3868516)Peak memory usage: 119 MB
% 97.46/16.09 % (3868516)Instructions burned: 431 (million)
% 97.46/16.09 % (3868521)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=304199103:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2956 on theBenchmark for (2956ds/150Mi)
% 97.46/16.09 % (3868521)Instruction limit reached!
% 97.46/16.09 % (3868521)------------------------------
% 97.46/16.09 % (3868521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.46/16.09 % (3868521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.46/16.09 % (3868521)CaDiCaL version: 2.1.3
% 97.46/16.09 % (3868521)Termination reason: Instruction limit
% 63.83/22.29 % (3868521)Termination phase: Preprocessing 1
% 63.83/22.29 % (3868521)Time elapsed: 0.106 s
% 63.83/22.29 % (3868521)Peak memory usage: 111 MB
% 63.83/22.29 % (3868521)Instructions burned: 150 (million)
% 63.83/22.29 % (3868523)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2167862616:i=14155:bd=all_2954 on theBenchmark for (2954ds/14155Mi)
% 63.83/22.29 % (3868502)Instruction limit reached!
% 63.83/22.29 % (3868502)------------------------------
% 63.83/22.29 % (3868502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868502)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868502)Termination reason: Instruction limit
% 63.83/22.29 % (3868502)Termination phase: Saturation
% 63.83/22.29 % (3868502)Time elapsed: 2.965 s
% 63.83/22.29 % (3868502)Peak memory usage: 207 MB
% 63.83/22.29 % (3868502)Instructions burned: 5202 (million)
% 63.83/22.29 % (3868525)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3555392861:i=667:av=off:fsr=off_2941 on theBenchmark for (2941ds/667Mi)
% 63.83/22.29 % (3868525)Instruction limit reached!
% 63.83/22.29 % (3868525)------------------------------
% 63.83/22.29 % (3868525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868525)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868525)Termination reason: Instruction limit
% 63.83/22.29 % (3868525)Termination phase: NewCNF
% 63.83/22.29 % (3868525)Time elapsed: 0.467 s
% 63.83/22.29 % (3868525)Peak memory usage: 136 MB
% 63.83/22.29 % (3868525)Instructions burned: 668 (million)
% 63.83/22.29 % (3868527)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=952446288:s2a=on:i=185:s2at=1.8:fdi=4_2935 on theBenchmark for (2935ds/185Mi)
% 63.83/22.29 % (3868527)Instruction limit reached!
% 63.83/22.29 % (3868527)------------------------------
% 63.83/22.29 % (3868527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868527)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868527)Termination reason: Instruction limit
% 63.83/22.29 % (3868527)Termination phase: SInE selection
% 63.83/22.29 % (3868527)Time elapsed: 0.124 s
% 63.83/22.29 % (3868527)Peak memory usage: 110 MB
% 63.83/22.29 % (3868527)Instructions burned: 186 (million)
% 63.83/22.29 % (3868529)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3825508127:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2932 on theBenchmark for (2932ds/193Mi)
% 63.83/22.29 % (3868529)Instruction limit reached!
% 63.83/22.29 % (3868529)------------------------------
% 63.83/22.29 % (3868529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868529)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868529)Termination reason: Instruction limit
% 63.83/22.29 % (3868529)Termination phase: SInE selection
% 63.83/22.29 % (3868529)Time elapsed: 0.129 s
% 63.83/22.29 % (3868529)Peak memory usage: 110 MB
% 63.83/22.29 % (3868529)Instructions burned: 194 (million)
% 63.83/22.29 % (3868531)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=366799208:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2930 on theBenchmark for (2930ds/4850Mi)
% 63.83/22.29 % (3868519)Instruction limit reached!
% 63.83/22.29 % (3868519)------------------------------
% 63.83/22.29 % (3868519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868519)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868519)Termination reason: Instruction limit
% 63.83/22.29 % (3868519)Termination phase: Saturation
% 63.83/22.29 % (3868519)Time elapsed: 3.733 s
% 63.83/22.29 % (3868519)Peak memory usage: 181 MB
% 63.83/22.29 % (3868519)Instructions burned: 6060 (million)
% 63.83/22.29 % (3868533)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=413144767:i=12111:sd=1:ss=included_2920 on theBenchmark for (2920ds/12111Mi)
% 63.83/22.29 % (3868531)Instruction limit reached!
% 63.83/22.29 % (3868531)------------------------------
% 63.83/22.29 % (3868531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868531)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868531)Termination reason: Instruction limit
% 63.83/22.29 % (3868531)Termination phase: Saturation
% 63.83/22.29 % (3868531)Time elapsed: 2.486 s
% 63.83/22.29 % (3868531)Peak memory usage: 217 MB
% 63.83/22.29 % (3868531)Instructions burned: 4850 (million)
% 63.83/22.29 % (3868535)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2203950916:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 63.83/22.29 % (3868535)Instruction limit reached!
% 63.83/22.29 % (3868535)------------------------------
% 63.83/22.29 % (3868535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868535)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868535)Termination reason: Instruction limit
% 63.83/22.29 % (3868535)Termination phase: Naming
% 63.83/22.29 % (3868535)Time elapsed: 0.216 s
% 63.83/22.29 % (3868535)Peak memory usage: 124 MB
% 63.83/22.29 % (3868535)Instructions burned: 321 (million)
% 63.83/22.29 % (3868537)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=285965834:i=2064:ep=RST_2900 on theBenchmark for (2900ds/2064Mi)
% 63.83/22.29 % (3868508)Instruction limit reached!
% 63.83/22.29 % (3868508)------------------------------
% 63.83/22.29 % (3868508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868508)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868508)Termination reason: Instruction limit
% 63.83/22.29 % (3868508)Termination phase: Saturation
% 63.83/22.29 % (3868508)Time elapsed: 7.706 s
% 63.83/22.29 % (3868508)Peak memory usage: 286 MB
% 63.83/22.29 % (3868508)Instructions burned: 13194 (million)
% 63.83/22.29 % (3868537)Instruction limit reached!
% 63.83/22.29 % (3868537)------------------------------
% 63.83/22.29 % (3868537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868537)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868537)Termination reason: Instruction limit
% 63.83/22.29 % (3868537)Termination phase: Property scanning
% 63.83/22.29 % (3868537)Time elapsed: 1.051 s
% 63.83/22.29 % (3868537)Peak memory usage: 170 MB
% 63.83/22.29 % (3868537)Instructions burned: 2067 (million)
% 63.83/22.29 % (3868685)dis-1011_128_sil=32000:random_seed=2304742556:i=3706:ep=RST:av=off_2888 on theBenchmark for (2888ds/3706Mi)
% 63.83/22.29 % (3868699)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2092515592:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2888 on theBenchmark for (2888ds/757Mi)
% 63.83/22.29 % (3868699)Instruction limit reached!
% 63.83/22.29 % (3868699)------------------------------
% 63.83/22.29 % (3868699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868699)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868699)Termination reason: Instruction limit
% 63.83/22.29 % (3868699)Termination phase: Saturation
% 63.83/22.29 % (3868699)Time elapsed: 0.508 s
% 63.83/22.29 % (3868699)Peak memory usage: 125 MB
% 63.83/22.29 % (3868699)Instructions burned: 757 (million)
% 63.83/22.29 % (3868798)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4012990326:i=13913:ss=axioms:sgt=8_2881 on theBenchmark for (2881ds/13913Mi)
% 63.83/22.29 % (3868685)Instruction limit reached!
% 63.83/22.29 % (3868685)------------------------------
% 63.83/22.29 % (3868685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868685)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868685)Termination reason: Instruction limit
% 63.83/22.29 % (3868685)Termination phase: Property scanning
% 63.83/22.29 % (3868685)Time elapsed: 2.654 s
% 63.83/22.29 % (3868685)Peak memory usage: 175 MB
% 63.83/22.29 % (3868685)Instructions burned: 3707 (million)
% 63.83/22.29 % (3868985)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=453424237:i=9925:aac=none_2860 on theBenchmark for (2860ds/9925Mi)
% 63.83/22.29 % (3868523)Instruction limit reached!
% 63.83/22.29 % (3868523)------------------------------
% 63.83/22.29 % (3868523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868523)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868523)Termination reason: Instruction limit
% 63.83/22.29 % (3868523)Termination phase: Saturation
% 63.83/22.29 % (3868523)Time elapsed: 10.517 s
% 63.83/22.29 % (3868523)Peak memory usage: 559 MB
% 63.83/22.29 % (3868523)Instructions burned: 14157 (million)
% 63.83/22.29 % (3869032)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2121380830:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2846 on theBenchmark for (2846ds/2479Mi)
% 63.83/22.29 % (3868533)Instruction limit reached!
% 63.83/22.29 % (3868533)------------------------------
% 63.83/22.29 % (3868533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3868533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3868533)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3868533)Termination reason: Instruction limit
% 63.83/22.29 % (3868533)Termination phase: Saturation
% 63.83/22.29 % (3868533)Time elapsed: 9.104 s
% 63.83/22.29 % (3868533)Peak memory usage: 291 MB
% 63.83/22.29 % (3868533)Instructions burned: 12111 (million)
% 63.83/22.29 % (3869093)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3670823466:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2827 on theBenchmark for (2827ds/440Mi)
% 63.83/22.29 % (3869032)Instruction limit reached!
% 63.83/22.29 % (3869032)------------------------------
% 63.83/22.29 % (3869032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3869032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3869032)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3869032)Termination reason: Instruction limit
% 63.83/22.29 % (3869032)Termination phase: Saturation
% 63.83/22.29 % (3869032)Time elapsed: 2.156 s
% 63.83/22.29 % (3869032)Peak memory usage: 131 MB
% 63.83/22.29 % (3869032)Instructions burned: 2479 (million)
% 63.83/22.29 % (3869093)Instruction limit reached!
% 63.83/22.29 % (3869093)------------------------------
% 63.83/22.29 % (3869093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3869093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3869093)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3869093)Termination reason: Instruction limit
% 63.83/22.29 % (3869093)Termination phase: Initialization
% 63.83/22.29 % (3869093)Time elapsed: 0.338 s
% 63.83/22.29 % (3869093)Peak memory usage: 111 MB
% 63.83/22.29 % (3869093)Instructions burned: 440 (million)
% 63.83/22.29 % (3869110)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4248131295:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2822 on theBenchmark for (2822ds/11145Mi)
% 63.83/22.29 % (3869112)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=2196783232:cts=off:i=3034:av=off:er=known:fsd=on_2822 on theBenchmark for (2822ds/3034Mi)
% 63.83/22.29 % (3869112)Instruction limit reached!
% 63.83/22.29 % (3869112)------------------------------
% 63.83/22.29 % (3869112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.83/22.29 % (3869112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.83/22.29 % (3869112)CaDiCaL version: 2.1.3
% 63.83/22.29 % (3869112)Termination reason: Instruction limit
% 63.83/22.29 % (3869112)Termination phase: Property scanning
% 63.83/22.29 % (3869112)Time elapsed: 2.633 s
% 63.83/22.29 % (3869112)Peak memory usage: 172 MB
% 63.83/22.29 % (3869112)Instructions burned: 3034 (million)
% 63.83/22.29 % (3869110)First to succeed.
% 63.83/22.29 % (3869110)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3868462"
% 63.83/22.29 % (3869180)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3391661150:st=2:s2a=on:i=524:s2at=2:ss=axioms_2793 on theBenchmark for (2793ds/524Mi)
% 63.83/22.29 % (3869110)Refutation found. Thanks to Tanya!
% 63.83/22.29 % SZS status Theorem for theBenchmark
% 63.83/22.29 % SZS output start Proof for theBenchmark
% See solution above
% 141.09/22.45 % (3869110)------------------------------
% 141.09/22.45 % (3869110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.09/22.45 % (3869110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.09/22.45 % (3869110)CaDiCaL version: 2.1.3
% 141.09/22.45 % (3869110)Termination reason: Refutation
% 141.09/22.45 % (3869110)Time elapsed: 2.848 s
% 141.09/22.45 % (3869110)Peak memory usage: 219 MB
% 141.09/22.45 % (3869110)Instructions burned: 3075 (million)
% 141.09/22.45 % (3869110)------------------------------
% 141.09/22.45 % (3869110)------------------------------
% 141.09/22.45 % (3868462)Success in time 21.42 s
% 141.09/22.45 % Vampire exiting
%------------------------------------------------------------------------------