%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP020+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:40 AM UTC 2026
% Result : Theorem 15.10s 8.09s
% Output : Refutation 33.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 53 ( 11 unt; 2 def)
% Number of atoms : 181 ( 11 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 238 ( 110 ~; 95 |; 16 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-5 aty)
% Number of variables : 71 ( 0 sgn 65 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f475,axiom,
ne(ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Enum_2Enum) ).
fof(f973,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne(ty_2Epair_2Eprod(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Epair_2Eprod) ).
fof(f2264,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2EUNIV) ).
fof(f2518,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,arr(X0,bool))
=> ! [X4] :
( mem(X4,arr(X1,bool))
=> ( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
=> ? [X5] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X4),X3))
& ! [X6] :
( mem(X6,X0)
=> ( p(ap(ap(c_2Ebool_2EIN(X0),X6),X3))
=> ap(ap(ap(c_2Ecombin_2Eo(X0,X0,X1),X5),X2),X6) = X6 ) )
& ! [X7] :
( mem(X7,X1)
=> ( p(ap(ap(c_2Ebool_2EIN(X1),X7),X4))
=> ap(ap(ap(c_2Ecombin_2Eo(X1,X1,X0),X2),X5),X7) = X7 ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EBIJ__INV) ).
fof(f2698,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(X0,X1)) = ap(ap(c_2Epred__set_2ECROSS(X0,X1),c_2Epred__set_2EUNIV(X0)),c_2Epred__set_2EUNIV(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Epred__set_2ECROSS__UNIV) ).
fof(f18000,axiom,
? [X0] :
( mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ) ).
fof(f18001,conjecture,
? [X0] :
( mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
fof(f18002,negated_conjecture,
~ ? [X0] :
( mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
inference(negated_conjecture,[status(cth)],[f18001]) ).
fof(f18111,plain,
! [X0] :
( ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
inference(ennf_transformation,[],[f18002]) ).
fof(f18461,plain,
! [X0] :
( ! [X1] :
( ne(ty_2Epair_2Eprod(X0,X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f973]) ).
fof(f18488,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ? [X5] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X4),X3))
& ! [X6] :
( ap(ap(ap(c_2Ecombin_2Eo(X0,X0,X1),X5),X2),X6) = X6
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X6),X3))
| ~ mem(X6,X0) )
& ! [X7] :
( ap(ap(ap(c_2Ecombin_2Eo(X1,X1,X0),X2),X5),X7) = X7
| ~ p(ap(ap(c_2Ebool_2EIN(X1),X7),X4))
| ~ mem(X7,X1) ) )
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,bool)) )
| ~ mem(X3,arr(X0,bool)) )
| ~ mem(X2,arr(X0,X1)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2518]) ).
fof(f18489,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ? [X5] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X4),X3))
& ! [X6] :
( ap(ap(ap(c_2Ecombin_2Eo(X0,X0,X1),X5),X2),X6) = X6
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X6),X3))
| ~ mem(X6,X0) )
& ! [X7] :
( ap(ap(ap(c_2Ecombin_2Eo(X1,X1,X0),X2),X5),X7) = X7
| ~ p(ap(ap(c_2Ebool_2EIN(X1),X7),X4))
| ~ mem(X7,X1) ) )
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,bool)) )
| ~ mem(X3,arr(X0,bool)) )
| ~ mem(X2,arr(X0,X1)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f18488]) ).
fof(f18542,plain,
! [X0] :
( ! [X1] :
( c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(X0,X1)) = ap(ap(c_2Epred__set_2ECROSS(X0,X1),c_2Epred__set_2EUNIV(X0)),c_2Epred__set_2EUNIV(X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2698]) ).
fof(f18586,plain,
! [X0] :
( mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f2264]) ).
fof(f21158,plain,
( mem(sK425,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK425),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK425]),skolemize(X0,sK425)],[f18000]) ).
fof(f21184,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( mem(sK437(X0,X1,X2,X3,X4),arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),sK437(X0,X1,X2,X3,X4)),X4),X3))
& ! [X6] :
( ap(ap(ap(c_2Ecombin_2Eo(X0,X0,X1),sK437(X0,X1,X2,X3,X4)),X2),X6) = X6
| ~ p(ap(ap(c_2Ebool_2EIN(X0),X6),X3))
| ~ mem(X6,X0) )
& ! [X7] :
( ap(ap(ap(c_2Ecombin_2Eo(X1,X1,X0),X2),sK437(X0,X1,X2,X3,X4)),X7) = X7
| ~ p(ap(ap(c_2Ebool_2EIN(X1),X7),X4))
| ~ mem(X7,X1) ) )
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,bool)) )
| ~ mem(X3,arr(X0,bool)) )
| ~ mem(X2,arr(X0,X1)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK437]),skolemize(X5,sK437(X0,X1,X2,X3,X4))],[f18489]) ).
fof(f22782,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))
| ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(cnf_transformation,[],[f18111]) ).
fof(f24022,plain,
ne(ty_2Enum_2Enum),
inference(cnf_transformation,[],[f475]) ).
fof(f24023,plain,
! [X0,X1] :
( ne(ty_2Epair_2Eprod(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f18461]) ).
fof(f24024,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK425),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),
inference(cnf_transformation,[],[f21158]) ).
fof(f24025,plain,
mem(sK425,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f21158]) ).
fof(f24079,plain,
! [X2,X3,X0,X1,X4] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),sK437(X0,X1,X2,X3,X4)),X4),X3))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
| ~ mem(X4,arr(X1,bool))
| ~ mem(X3,arr(X0,bool))
| ~ mem(X2,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f21184]) ).
fof(f24080,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X2),X3),X4))
| mem(sK437(X0,X1,X2,X3,X4),arr(X1,X0))
| ~ mem(X4,arr(X1,bool))
| ~ mem(X3,arr(X0,bool))
| ~ mem(X2,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f21184]) ).
fof(f24128,plain,
! [X0,X1] :
( c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(X0,X1)) = ap(ap(c_2Epred__set_2ECROSS(X0,X1),c_2Epred__set_2EUNIV(X0)),c_2Epred__set_2EUNIV(X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f18542]) ).
fof(f24239,plain,
! [X0] :
( mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f18586]) ).
fof(f30236,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))
| ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum) ),
inference(superposition,[],[f22782,f24128]) ).
fof(f30238,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))
| ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ ne(ty_2Enum_2Enum) ),
inference(duplicate_literal_removal,[],[f30236]) ).
fof(f30239,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))
| ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(forward_subsumption_resolution,[],[f30238,f24022]) ).
fof(f30240,plain,
! [X0] :
( ~ mem(sK437(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum,X0,c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(resolution,[],[f30239,f24079]) ).
fof(f30282,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(forward_subsumption_resolution,[],[f30240,f24080]) ).
fof(f30294,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(forward_subsumption_resolution,[],[f30282,f24239]) ).
fof(f30299,definition,
( spl1260_118
<=> ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
introduced(definition,[new_symbols(definition,[spl1260_118])],[avatar_definition]) ).
fof(f30301,plain,
( ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))
| spl1260_118 ),
inference(avatar_component_clause,[],[f30299]) ).
fof(f30313,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(forward_subsumption_resolution,[],[f30294,f24239]) ).
fof(f30317,plain,
! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
inference(forward_subsumption_resolution,[],[f30313,f24022]) ).
fof(f30319,definition,
( spl1260_121
<=> ! [X0] :
( ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ) ),
introduced(definition,[new_symbols(definition,[spl1260_121])],[avatar_definition]) ).
fof(f30320,plain,
( ! [X0] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )
| ~ spl1260_121 ),
inference(avatar_component_clause,[],[f30319]) ).
fof(f30324,plain,
( ~ spl1260_118
| spl1260_121 ),
inference(avatar_split_clause,[],[f30317,f30319,f30299]) ).
fof(f30423,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK425),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum) ),
inference(superposition,[],[f24024,f24128]) ).
fof(f30424,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK425),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ ne(ty_2Enum_2Enum) ),
inference(duplicate_literal_removal,[],[f30423]) ).
fof(f30425,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK425),c_2Epred__set_2EUNIV(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),
inference(forward_subsumption_resolution,[],[f30424,f24022]) ).
fof(f31211,plain,
( ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| spl1260_118 ),
inference(resolution,[],[f24023,f30301]) ).
fof(f31212,plain,
( ~ ne(ty_2Enum_2Enum)
| spl1260_118 ),
inference(duplicate_literal_removal,[],[f31211]) ).
fof(f31213,plain,
( $false
| spl1260_118 ),
inference(forward_subsumption_resolution,[],[f31212,f24022]) ).
fof(f31214,plain,
spl1260_118,
inference(avatar_contradiction_clause,[],[f31213]) ).
fof(f31298,plain,
( ~ mem(sK425,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ spl1260_121 ),
inference(resolution,[],[f30320,f30425]) ).
fof(f31307,plain,
( $false
| ~ spl1260_121 ),
inference(forward_subsumption_resolution,[],[f31298,f24025]) ).
fof(f31308,plain,
~ spl1260_121,
inference(avatar_contradiction_clause,[],[f31307]) ).
cnf(s156,plain,
( ~ spl1260_118
| spl1260_121 ),
inference(sat_conversion,[],[f30324]) ).
cnf(s184,plain,
spl1260_118,
inference(sat_conversion,[],[f31214]) ).
cnf(s185,plain,
~ spl1260_121,
inference(sat_conversion,[],[f31308]) ).
cnf(s189,plain,
$false,
inference(rat,[],[s156,s185,s184]) ).
fof(f31309,plain,
$false,
inference(avatar_sat_refutation,[],[s189]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020+5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 12:02:07 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 17.65/5.94 % (2432325)Detected formulas, will run a generic FOF schedule.
% 17.65/5.94 % (2432332)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=2912041126:i=141695:sd=1:nm=32:gsp=on:ss=included_2970 on theBenchmark for (2970ds/141695Mi)
% 17.65/5.94 % (2432331)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=1110799782:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2970 on theBenchmark for (2970ds/134677Mi)
% 17.65/5.94 % (2432330)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=286599908:i=141193_2970 on theBenchmark for (2970ds/141193Mi)
% 17.65/5.94 % (2432335)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2860756304:s2a=on:i=139:gtg=position_2970 on theBenchmark for (2970ds/139Mi)
% 17.65/5.94 % (2432333)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2519441015:i=109:sd=1:ins=1:gsp=on:ss=axioms_2970 on theBenchmark for (2970ds/109Mi)
% 17.65/5.94 % (2432334)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1203544274:i=119:av=off:ss=axioms_2970 on theBenchmark for (2970ds/119Mi)
% 17.65/5.94 % (2432336)dis-21_1_sil=8000:lcm=predicate:random_seed=3412967198:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2970 on theBenchmark for (2970ds/129Mi)
% 17.65/5.94 % (2432335)Instruction limit reached!
% 17.65/5.94 % (2432335)------------------------------
% 17.65/5.94 % (2432335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/5.94 % (2432335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/5.94 % (2432335)CaDiCaL version: 2.1.3
% 17.65/5.94 % (2432335)Termination reason: Instruction limit
% 17.65/5.94 % (2432335)Termination phase: Property scanning
% 17.65/5.94 % (2432335)Time elapsed: 0.060 s
% 17.65/5.94 % (2432335)Peak memory usage: 122 MB
% 17.65/5.94 % (2432335)Instructions burned: 142 (million)
% 17.65/5.94 % (2432333)Instruction limit reached!
% 17.65/5.94 % (2432333)------------------------------
% 17.65/5.94 % (2432333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/5.94 % (2432333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/5.94 % (2432333)CaDiCaL version: 2.1.3
% 17.65/5.94 % (2432333)Termination reason: Instruction limit
% 17.65/5.94 % (2432333)Termination phase: SInE selection
% 17.65/5.94 % (2432333)Time elapsed: 0.073 s
% 17.65/5.94 % (2432333)Peak memory usage: 121 MB
% 17.65/5.94 % (2432333)Instructions burned: 110 (million)
% 17.65/5.94 % (2432334)Instruction limit reached!
% 17.65/5.94 % (2432334)------------------------------
% 17.65/5.94 % (2432334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/5.94 % (2432334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/5.94 % (2432334)CaDiCaL version: 2.1.3
% 17.65/5.94 % (2432334)Termination reason: Instruction limit
% 17.65/5.94 % (2432334)Termination phase: SInE selection
% 17.65/5.94 % (2432334)Time elapsed: 0.078 s
% 17.65/5.94 % (2432334)Peak memory usage: 121 MB
% 17.65/5.94 % (2432334)Instructions burned: 120 (million)
% 17.65/5.94 % (2432336)Instruction limit reached!
% 17.65/5.94 % (2432336)------------------------------
% 17.65/5.94 % (2432336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.65/5.94 % (2432336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.65/5.94 % (2432336)CaDiCaL version: 2.1.3
% 17.65/5.94 % (2432336)Termination reason: Instruction limit
% 17.65/5.94 % (2432336)Termination phase: SInE selection
% 17.65/5.94 % (2432336)Time elapsed: 0.085 s
% 17.65/5.94 % (2432336)Peak memory usage: 121 MB
% 17.65/5.94 % (2432336)Instructions burned: 129 (million)
% 17.65/5.94 % (2432344)lrs+10_1_sil=8000:sp=occurrence:random_seed=3973074431:i=285:sd=3:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/285Mi)
% 17.65/5.94 % (2432345)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1088912724:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/157Mi)
% 17.65/5.94 % (2432346)lrs+1011_1_sil=32000:sp=occurrence:random_seed=122641219:i=325:sd=1:ss=axioms:sgt=32_2967 on theBenchmark for (2967ds/325Mi)
% 17.65/5.94 % (2432347)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=597023876:s2a=on:i=248:s2at=1.23:gtg=position_2967 on theBenchmark for (2967ds/248Mi)
% 17.65/5.94 % (2432345)Instruction limit reached!
% 23.93/6.90 % (2432345)------------------------------
% 23.93/6.90 % (2432345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432345)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432345)Termination reason: Instruction limit
% 23.93/6.90 % (2432345)Termination phase: Property scanning
% 23.93/6.90 % (2432345)Time elapsed: 0.062 s
% 23.93/6.90 % (2432345)Peak memory usage: 122 MB
% 23.93/6.90 % (2432345)Instructions burned: 159 (million)
% 23.93/6.90 % (2432347)Instruction limit reached!
% 23.93/6.90 % (2432347)------------------------------
% 23.93/6.90 % (2432347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432347)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432347)Termination reason: Instruction limit
% 23.93/6.90 % (2432347)Termination phase: Property scanning
% 23.93/6.90 % (2432347)Time elapsed: 0.097 s
% 23.93/6.90 % (2432347)Peak memory usage: 122 MB
% 23.93/6.90 % (2432347)Instructions burned: 250 (million)
% 23.93/6.90 % (2432344)Instruction limit reached!
% 23.93/6.90 % (2432344)------------------------------
% 23.93/6.90 % (2432344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432344)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432344)Termination reason: Instruction limit
% 23.93/6.90 % (2432344)Termination phase: Preprocessing 3
% 23.93/6.90 % (2432344)Time elapsed: 0.211 s
% 23.93/6.90 % (2432344)Peak memory usage: 127 MB
% 23.93/6.90 % (2432344)Instructions burned: 286 (million)
% 23.93/6.90 % (2432352)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1112012736:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2965 on theBenchmark for (2965ds/294Mi)
% 23.93/6.90 % (2432346)Instruction limit reached!
% 23.93/6.90 % (2432346)------------------------------
% 23.93/6.90 % (2432346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432346)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432346)Termination reason: Instruction limit
% 23.93/6.90 % (2432346)Termination phase: Saturation
% 23.93/6.90 % (2432346)Time elapsed: 0.221 s
% 23.93/6.90 % (2432346)Peak memory usage: 128 MB
% 23.93/6.90 % (2432346)Instructions burned: 325 (million)
% 23.93/6.90 % (2432353)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3179461305:i=2350_2964 on theBenchmark for (2964ds/2350Mi)
% 23.93/6.90 % (2432354)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4138834144:cts=off:i=113:fsr=off:ss=included:sgt=4_2964 on theBenchmark for (2964ds/113Mi)
% 23.93/6.90 % (2432352)Instruction limit reached!
% 23.93/6.90 % (2432352)------------------------------
% 23.93/6.90 % (2432352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432352)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432352)Termination reason: Instruction limit
% 23.93/6.90 % (2432352)Termination phase: Preprocessing 1
% 23.93/6.90 % (2432352)Time elapsed: 0.185 s
% 23.93/6.90 % (2432352)Peak memory usage: 122 MB
% 23.93/6.90 % (2432352)Instructions burned: 295 (million)
% 23.93/6.90 % (2432356)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1291843876:i=127:av=off:fsr=off:sup=off_2963 on theBenchmark for (2963ds/127Mi)
% 23.93/6.90 % (2432354)Instruction limit reached!
% 23.93/6.90 % (2432354)------------------------------
% 23.93/6.90 % (2432354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432354)CaDiCaL version: 2.1.3
% 23.93/6.90 % (2432354)Termination reason: Instruction limit
% 23.93/6.90 % (2432354)Termination phase: SInE selection
% 23.93/6.90 % (2432354)Time elapsed: 0.083 s
% 23.93/6.90 % (2432354)Peak memory usage: 121 MB
% 23.93/6.90 % (2432354)Instructions burned: 115 (million)
% 23.93/6.90 % (2432356)Instruction limit reached!
% 23.93/6.90 % (2432356)------------------------------
% 23.93/6.90 % (2432356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.93/6.90 % (2432356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/6.90 % (2432356)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432356)Termination reason: Instruction limit
% 15.10/8.09 % (2432356)Termination phase: Preprocessing 1
% 15.10/8.09 % (2432356)Time elapsed: 0.090 s
% 15.10/8.09 % (2432356)Peak memory usage: 122 MB
% 15.10/8.09 % (2432356)Instructions burned: 127 (million)
% 15.10/8.09 % (2432359)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4244881614:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2962 on theBenchmark for (2962ds/114Mi)
% 15.10/8.09 % (2432361)lrs+10_1_sil=8000:sp=occurrence:random_seed=3876229552:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2961 on theBenchmark for (2961ds/907Mi)
% 15.10/8.09 % (2432359)Instruction limit reached!
% 15.10/8.09 % (2432359)------------------------------
% 15.10/8.09 % (2432359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432359)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432359)Termination reason: Instruction limit
% 15.10/8.09 % (2432359)Termination phase: Property scanning
% 15.10/8.09 % (2432359)Time elapsed: 0.047 s
% 15.10/8.09 % (2432359)Peak memory usage: 122 MB
% 15.10/8.09 % (2432359)Instructions burned: 114 (million)
% 15.10/8.09 % (2432362)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3307725543:i=437:sd=1:aac=none:ss=included_2961 on theBenchmark for (2961ds/437Mi)
% 15.10/8.09 % (2432365)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3658484720:i=5202:ss=axioms:sgt=16_2960 on theBenchmark for (2960ds/5202Mi)
% 15.10/8.09 % (2432362)Instruction limit reached!
% 15.10/8.09 % (2432362)------------------------------
% 15.10/8.09 % (2432362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432362)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432362)Termination reason: Instruction limit
% 15.10/8.09 % (2432362)Termination phase: Saturation
% 15.10/8.09 % (2432362)Time elapsed: 0.265 s
% 15.10/8.09 % (2432362)Peak memory usage: 130 MB
% 15.10/8.09 % (2432362)Instructions burned: 438 (million)
% 15.10/8.09 % (2432368)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1984186900:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2956 on theBenchmark for (2956ds/134Mi)
% 15.10/8.09 % (2432361)Instruction limit reached!
% 15.10/8.09 % (2432361)------------------------------
% 15.10/8.09 % (2432361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432361)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432361)Termination reason: Instruction limit
% 15.10/8.09 % (2432361)Termination phase: Saturation
% 15.10/8.09 % (2432361)Time elapsed: 0.492 s
% 15.10/8.09 % (2432361)Peak memory usage: 139 MB
% 15.10/8.09 % (2432361)Instructions burned: 907 (million)
% 15.10/8.09 % (2432368)Instruction limit reached!
% 15.10/8.09 % (2432368)------------------------------
% 15.10/8.09 % (2432368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432368)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432368)Termination reason: Instruction limit
% 15.10/8.09 % (2432368)Termination phase: SInE selection
% 15.10/8.09 % (2432368)Time elapsed: 0.094 s
% 15.10/8.09 % (2432368)Peak memory usage: 121 MB
% 15.10/8.09 % (2432368)Instructions burned: 135 (million)
% 15.10/8.09 % (2432370)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2784349145:st=8:i=592:sd=3:ep=RST:ss=axioms_2955 on theBenchmark for (2955ds/592Mi)
% 15.10/8.09 % (2432371)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3244398539:st=3:i=13193:sd=3:ss=axioms_2954 on theBenchmark for (2954ds/13193Mi)
% 15.10/8.09 % (2432370)Instruction limit reached!
% 15.10/8.09 % (2432370)------------------------------
% 15.10/8.09 % (2432370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432370)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432370)Termination reason: Instruction limit
% 15.10/8.09 % (2432370)Termination phase: Naming
% 15.10/8.09 % (2432370)Time elapsed: 0.386 s
% 15.10/8.09 % (2432370)Peak memory usage: 133 MB
% 15.10/8.09 % (2432370)Instructions burned: 594 (million)
% 15.10/8.09 % (2432353)Instruction limit reached!
% 15.10/8.09 % (2432353)------------------------------
% 15.10/8.09 % (2432353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432353)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432353)Termination reason: Instruction limit
% 15.10/8.09 % (2432353)Termination phase: Property scanning
% 15.10/8.09 % (2432353)Time elapsed: 1.410 s
% 15.10/8.09 % (2432353)Peak memory usage: 197 MB
% 15.10/8.09 % (2432353)Instructions burned: 2351 (million)
% 15.10/8.09 % (2432374)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=3025471278:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/125Mi)
% 15.10/8.09 % (2432374)Instruction limit reached!
% 15.10/8.09 % (2432374)------------------------------
% 15.10/8.09 % (2432374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432374)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432374)Termination reason: Instruction limit
% 15.10/8.09 % (2432374)Termination phase: Property scanning
% 15.10/8.09 % (2432374)Time elapsed: 0.051 s
% 15.10/8.09 % (2432374)Peak memory usage: 122 MB
% 15.10/8.09 % (2432374)Instructions burned: 126 (million)
% 15.10/8.09 % (2432375)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2063409897:i=134:gtgl=5:slsql=off:gtg=exists_sym_2948 on theBenchmark for (2948ds/134Mi)
% 15.10/8.09 % (2432375)Instruction limit reached!
% 15.10/8.09 % (2432375)------------------------------
% 15.10/8.09 % (2432375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432375)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432375)Termination reason: Instruction limit
% 15.10/8.09 % (2432375)Termination phase: Property scanning
% 15.10/8.09 % (2432375)Time elapsed: 0.056 s
% 15.10/8.09 % (2432375)Peak memory usage: 122 MB
% 15.10/8.09 % (2432375)Instructions burned: 137 (million)
% 15.10/8.09 % (2432377)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3719959443:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2947 on theBenchmark for (2947ds/141Mi)
% 15.10/8.09 % (2432379)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=318086454:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2946 on theBenchmark for (2946ds/431Mi)
% 15.10/8.09 % (2432377)Instruction limit reached!
% 15.10/8.09 % (2432377)------------------------------
% 15.10/8.09 % (2432377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432377)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432377)Termination reason: Instruction limit
% 15.10/8.09 % (2432377)Termination phase: SInE selection
% 15.10/8.09 % (2432377)Time elapsed: 0.096 s
% 15.10/8.09 % (2432377)Peak memory usage: 121 MB
% 15.10/8.09 % (2432377)Instructions burned: 142 (million)
% 15.10/8.09 % (2432382)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=1733179350:i=6060:aac=none:ins=25_2944 on theBenchmark for (2944ds/6060Mi)
% 15.10/8.09 % (2432379)Instruction limit reached!
% 15.10/8.09 % (2432379)------------------------------
% 15.10/8.09 % (2432379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432379)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432379)Termination reason: Instruction limit
% 15.10/8.09 % (2432379)Termination phase: Saturation
% 15.10/8.09 % (2432379)Time elapsed: 0.282 s
% 15.10/8.09 % (2432379)Peak memory usage: 129 MB
% 15.10/8.09 % (2432379)Instructions burned: 432 (million)
% 15.10/8.09 % (2432384)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=77258531:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2942 on theBenchmark for (2942ds/150Mi)
% 15.10/8.09 % (2432384)Instruction limit reached!
% 15.10/8.09 % (2432384)------------------------------
% 15.10/8.09 % (2432384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.10/8.09 % (2432384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.10/8.09 % (2432384)CaDiCaL version: 2.1.3
% 15.10/8.09 % (2432384)Termination reason: Instruction limit
% 15.10/8.09 % (2432384)Termination phase: SInE selection
% 15.10/8.09 % (2432384)Time elapsed: 0.102 s
% 15.10/8.09 % (2432384)Peak memory usage: 121 MB
% 15.10/8.09 % (2432384)Instructions burned: 150 (million)
% 15.10/8.09 % (2432386)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2849734545:i=14155:bd=all_2939 on theBenchmark for (2939ds/14155Mi)
% 15.10/8.09 % (2432365)First to succeed.
% 15.10/8.09 % (2432365)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2432325"
% 15.10/8.09 % (2432365)Refutation found. Thanks to Tanya!
% 15.10/8.09 % SZS status Theorem for theBenchmark
% 15.10/8.09 % SZS output start Proof for theBenchmark
% See solution above
% 33.60/8.34 % (2432365)------------------------------
% 33.60/8.34 % (2432365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.60/8.34 % (2432365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.60/8.34 % (2432365)CaDiCaL version: 2.1.3
% 33.60/8.34 % (2432365)Termination reason: Refutation
% 33.60/8.34 % (2432365)Time elapsed: 2.684 s
% 33.60/8.34 % (2432365)Peak memory usage: 261 MB
% 33.60/8.34 % (2432365)Instructions burned: 4329 (million)
% 33.60/8.34 % (2432365)------------------------------
% 33.60/8.34 % (2432365)------------------------------
% 33.60/8.34 % (2432325)Success in time 7.238 s
% 33.60/8.34 % Vampire exiting
%------------------------------------------------------------------------------