%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP020+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:35:52 AM UTC 2026
% Result : Theorem 13.26s 2.54s
% Output : Refutation 13.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 10
% Syntax : Number of formulae : 57 ( 11 unt; 2 def)
% Number of atoms : 164 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 203 ( 96 ~; 85 |; 7 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-4 aty)
% Number of variables : 63 ( 0 sgn 56 !; 7 ?)
% 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/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f25,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epred__set_2EUNIV) ).
fof(f26,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne(ty_2Epair_2Eprod(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Epair_2Eprod) ).
fof(f27,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> mem(c_2Epred__set_2ECROSS(X0,X1),arr(arr(X0,bool),arr(arr(X1,bool),arr(ty_2Epair_2Eprod(X0,X1),bool)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mem_c_2Epred__set_2ECROSS) ).
fof(f29,axiom,
ne(ty_2Enum_2Enum),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ne_ty_2Enum_2Enum) ).
fof(f51,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,bool))
=> ! [X3] :
( mem(X3,arr(X1,bool))
=> ( ? [X4] :
( mem(X4,arr(X0,X1))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3)) )
<=> ? [X5] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2)) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EBIJ__SYM) ).
fof(f62,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/sandbox/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ) ).
fof(f63,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/sandbox/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
fof(f64,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)],[f63]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f81,plain,
! [X0] :
( mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f82,plain,
! [X0] :
( ! [X1] :
( ne(ty_2Epair_2Eprod(X0,X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f83,plain,
! [X0] :
( ! [X1] :
( mem(c_2Epred__set_2ECROSS(X0,X1),arr(arr(X0,bool),arr(arr(X1,bool),arr(ty_2Epair_2Eprod(X0,X1),bool))))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f110,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ? [X4] :
( mem(X4,arr(X0,X1))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3)) )
<=> ? [X5] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2)) ) )
| ~ mem(X3,arr(X1,bool)) )
| ~ mem(X2,arr(X0,bool)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f125,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,[],[f64]) ).
fof(f129,plain,
! [X2,X3,X0,X1] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f162,plain,
! [X0] :
( mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f163,plain,
! [X0,X1] :
( ne(ty_2Epair_2Eprod(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f164,plain,
! [X0,X1] :
( mem(c_2Epred__set_2ECROSS(X0,X1),arr(arr(X0,bool),arr(arr(X1,bool),arr(ty_2Epair_2Eprod(X0,X1),bool))))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f166,plain,
ne(ty_2Enum_2Enum),
inference(cnf_transformation,[],[f29]) ).
fof(f219,plain,
! [X2,X3,X0,X1,X5] :
( mem(sK25(X0,X1,X2,X3),arr(X0,X1))
| ~ ne(X1)
| ~ mem(X2,arr(X0,bool))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X5] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),sK25(X0,X1,X2,X3)),X2),X3))
| ~ ne(X1)
| ~ mem(X2,arr(X0,bool))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f286,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK34),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,[],[f62]) ).
fof(f287,plain,
mem(sK34,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f62]) ).
fof(f288,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,[],[f125]) ).
fof(f2264,definition,
( spl35_19
<=> ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) ),
introduced(definition,[new_symbols(definition,[spl35_19])],[avatar_definition]) ).
fof(f2265,plain,
( ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))
| ~ spl35_19 ),
inference(avatar_component_clause,[],[f2264]) ).
fof(f2266,plain,
( ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))
| spl35_19 ),
inference(avatar_component_clause,[],[f2264]) ).
fof(f2272,definition,
( spl35_21
<=> mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) ),
introduced(definition,[new_symbols(definition,[spl35_21])],[avatar_definition]) ).
fof(f2273,plain,
( mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ spl35_21 ),
inference(avatar_component_clause,[],[f2272]) ).
fof(f2274,plain,
( ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| spl35_21 ),
inference(avatar_component_clause,[],[f2272]) ).
fof(f2284,plain,
( ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| spl35_19 ),
inference(resolution,[],[f2266,f163]) ).
fof(f2285,plain,
( ~ ne(ty_2Enum_2Enum)
| spl35_19 ),
inference(duplicate_literal_removal,[],[f2284]) ).
fof(f2286,plain,
( $false
| spl35_19 ),
inference(forward_subsumption_resolution,[],[f2285,f166]) ).
fof(f2287,plain,
spl35_19,
inference(avatar_contradiction_clause,[],[f2286]) ).
fof(f2365,plain,
( ! [X0] :
( ~ mem(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X0) )
| spl35_21 ),
inference(resolution,[],[f2274,f129]) ).
fof(f2371,plain,
( ! [X0,X1] :
( ~ mem(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(X1,arr(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X1)
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X0) )
| spl35_21 ),
inference(resolution,[],[f2365,f129]) ).
fof(f2372,plain,
! [X0] :
( ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum)
| ~ mem(sK25(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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))),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(resolution,[],[f220,f288]) ).
fof(f2373,plain,
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ ne(ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| spl35_21 ),
inference(resolution,[],[f2371,f164]) ).
fof(f2374,plain,
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ ne(ty_2Enum_2Enum)
| spl35_21 ),
inference(duplicate_literal_removal,[],[f2373]) ).
fof(f2375,plain,
( ~ ne(ty_2Enum_2Enum)
| spl35_21 ),
inference(forward_subsumption_resolution,[],[f2374,f162]) ).
fof(f2376,plain,
( $false
| spl35_21 ),
inference(forward_subsumption_resolution,[],[f2375,f166]) ).
fof(f2377,plain,
spl35_21,
inference(avatar_contradiction_clause,[],[f2376]) ).
fof(f2378,plain,
! [X0] :
( ~ ne(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum) ),
inference(forward_subsumption_resolution,[],[f2372,f219]) ).
fof(f2379,plain,
( ! [X0] :
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum) )
| ~ spl35_19 ),
inference(forward_subsumption_resolution,[],[f2378,f2265]) ).
fof(f2380,plain,
( ! [X0] :
( ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ ne(ty_2Enum_2Enum) )
| ~ spl35_19 ),
inference(forward_subsumption_resolution,[],[f2379,f162]) ).
fof(f2381,plain,
( ! [X0] :
( ~ mem(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)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )
| ~ spl35_19 ),
inference(forward_subsumption_resolution,[],[f2380,f166]) ).
fof(f2388,plain,
( ! [X0] :
( ~ 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)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )
| ~ spl35_19
| ~ spl35_21 ),
inference(forward_subsumption_resolution,[],[f2381,f2273]) ).
fof(f2411,plain,
( ~ mem(sK34,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ spl35_19
| ~ spl35_21 ),
inference(resolution,[],[f2388,f286]) ).
fof(f2467,plain,
( $false
| ~ spl35_19
| ~ spl35_21 ),
inference(forward_subsumption_resolution,[],[f2411,f287]) ).
fof(f2468,plain,
( ~ spl35_19
| ~ spl35_21 ),
inference(avatar_contradiction_clause,[],[f2467]) ).
cnf(s20,plain,
spl35_19,
inference(sat_conversion,[],[f2287]) ).
cnf(s22,plain,
spl35_21,
inference(sat_conversion,[],[f2377]) ).
cnf(s23,plain,
( ~ spl35_19
| ~ spl35_21 ),
inference(sat_conversion,[],[f2468]) ).
cnf(s24,plain,
~ spl35_19,
inference(rat,[],[s23,s22]) ).
cnf(s25,plain,
$false,
inference(rat,[],[s20,s24]) ).
fof(f2469,plain,
$false,
inference(avatar_sat_refutation,[],[s25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP020+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 27 12:08:08 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.21/0.49 Running first-order model finding
% 0.21/0.49 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.26/2.54 % (2230416)Will run a generic schedule for satisfiability detection.
% 13.26/2.54 % (2230422)% WARNING: option uhcvi not known.
% 13.26/2.54 % (2230425)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2366426515:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.26/2.54 % (2230422)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=414509486:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.26/2.54 % (2230423)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1570590276:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.26/2.54 % (2230421)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2531415771_2999 on theBenchmark for (2999ds/0Mi)
% 13.26/2.54 % (2230424)dis+10_1_sil=32000:sp=arity:random_seed=3704965463:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.26/2.54 % (2230426)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1529200918:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.54 % (2230427)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=175703753:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.26/2.54 % (2230425)Instruction limit reached!
% 13.26/2.54 % (2230425)------------------------------
% 13.26/2.54 % (2230425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230425)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230425)Termination reason: Instruction limit
% 13.26/2.54 % (2230425)Termination phase: Saturation
% 13.26/2.54 % (2230425)Time elapsed: 0.058 s
% 13.26/2.54 % (2230425)Peak memory usage: 12 MB
% 13.26/2.54 % (2230425)Instructions burned: 117 (million)
% 13.26/2.54 % TRYING [1]
% 13.26/2.54 % TRYING [2]
% 13.26/2.54 % (2230435)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=365393990:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.26/2.54 % TRYING [3]
% 13.26/2.54 % TRYING [1]
% 13.26/2.54 % TRYING [2]
% 13.26/2.54 % (2230424)Instruction limit reached!
% 13.26/2.54 % (2230424)------------------------------
% 13.26/2.54 % (2230424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230424)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230424)Termination reason: Instruction limit
% 13.26/2.54 % (2230424)Termination phase: Saturation
% 13.26/2.54 % (2230424)Time elapsed: 0.104 s
% 13.26/2.54 % (2230424)Peak memory usage: 13 MB
% 13.26/2.54 % (2230424)Instructions burned: 103 (million)
% 13.26/2.54 % TRYING [3]
% 13.26/2.54 % (2230426)Instruction limit reached!
% 13.26/2.54 % (2230426)------------------------------
% 13.26/2.54 % (2230426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230426)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230426)Termination reason: Instruction limit
% 13.26/2.54 % (2230426)Termination phase: Saturation
% 13.26/2.54 % (2230426)Time elapsed: 0.121 s
% 13.26/2.54 % (2230426)Peak memory usage: 13 MB
% 13.26/2.54 % (2230426)Instructions burned: 131 (million)
% 13.26/2.54 % (2230437)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3640916307:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.26/2.54 % TRYING [4]
% 13.26/2.54 % (2230438)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1260847835:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.26/2.54 % TRYING [4]
% 13.26/2.54 % (2230427)Instruction limit reached!
% 13.26/2.54 % (2230427)------------------------------
% 13.26/2.54 % (2230427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230427)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230427)Termination reason: Instruction limit
% 13.26/2.54 % (2230427)Termination phase: Saturation
% 13.26/2.54 % (2230427)Time elapsed: 0.165 s
% 13.26/2.54 % (2230427)Peak memory usage: 15 MB
% 13.26/2.54 % (2230427)Instructions burned: 159 (million)
% 13.26/2.54 % (2230441)ott-21_1_sil=16000:fs=off:random_seed=2151602890:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 13.26/2.54 % (2230437)Instruction limit reached!
% 13.26/2.54 % (2230437)------------------------------
% 13.26/2.54 % (2230437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230437)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230437)Termination reason: Instruction limit
% 13.26/2.54 % (2230437)Termination phase: Saturation
% 13.26/2.54 % (2230437)Time elapsed: 0.090 s
% 13.26/2.54 % (2230437)Peak memory usage: 14 MB
% 13.26/2.54 % (2230437)Instructions burned: 131 (million)
% 13.26/2.54 % (2230443)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=212932415:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.26/2.54 % (2230441)Instruction limit reached!
% 13.26/2.54 % (2230441)------------------------------
% 13.26/2.54 % (2230441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230441)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230441)Termination reason: Instruction limit
% 13.26/2.54 % (2230441)Termination phase: Saturation
% 13.26/2.54 % (2230441)Time elapsed: 0.167 s
% 13.26/2.54 % (2230441)Peak memory usage: 12 MB
% 13.26/2.54 % (2230441)Instructions burned: 180 (million)
% 13.26/2.54 % (2230435)Instruction limit reached!
% 13.26/2.54 % (2230435)------------------------------
% 13.26/2.54 % (2230435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230435)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230435)Termination reason: Instruction limit
% 13.26/2.54 % (2230435)Termination phase: Finite model building SAT solving
% 13.26/2.54 % (2230435)Time elapsed: 0.332 s
% 13.26/2.54 % (2230435)Peak memory usage: 35 MB
% 13.26/2.54 % (2230435)Instructions burned: 717 (million)
% 13.26/2.54 % (2230445)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3430681298:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 13.26/2.54 % (2230446)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3067563404:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 13.26/2.54 % TRYING [5]
% 13.26/2.54 % TRYING [1]
% 13.26/2.54 % TRYING [2]
% 13.26/2.54 % TRYING [3]
% 13.26/2.54 % (2230443)Instruction limit reached!
% 13.26/2.54 % (2230443)------------------------------
% 13.26/2.54 % (2230443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230443)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230443)Termination reason: Instruction limit
% 13.26/2.54 % (2230443)Termination phase: Saturation
% 13.26/2.54 % (2230443)Time elapsed: 0.488 s
% 13.26/2.54 % (2230443)Peak memory usage: 14 MB
% 13.26/2.54 % (2230443)Instructions burned: 478 (million)
% 13.26/2.54 % (2230449)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=186876177:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 13.26/2.54 % TRYING [4]
% 13.26/2.54 % (2230438)Instruction limit reached!
% 13.26/2.54 % (2230438)------------------------------
% 13.26/2.54 % (2230438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230438)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230438)Termination reason: Instruction limit
% 13.26/2.54 % (2230438)Termination phase: Saturation
% 13.26/2.54 % (2230438)Time elapsed: 0.643 s
% 13.26/2.54 % (2230438)Peak memory usage: 19 MB
% 13.26/2.54 % (2230438)Instructions burned: 684 (million)
% 13.26/2.54 % (2230451)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3450083594:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 13.26/2.54 % (2230446)Instruction limit reached!
% 13.26/2.54 % (2230446)------------------------------
% 13.26/2.54 % (2230446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230446)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230446)Termination reason: Instruction limit
% 13.26/2.54 % (2230446)Termination phase: Saturation
% 13.26/2.54 % (2230446)Time elapsed: 0.558 s
% 13.26/2.54 % (2230446)Peak memory usage: 22 MB
% 13.26/2.54 % (2230446)Instructions burned: 1180 (million)
% 13.26/2.54 % (2230453)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3262686729:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 13.26/2.54 % (2230445)Instruction limit reached!
% 13.26/2.54 % (2230445)------------------------------
% 13.26/2.54 % (2230445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230445)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230445)Termination reason: Instruction limit
% 13.26/2.54 % (2230445)Termination phase: Finite model building SAT solving
% 13.26/2.54 % (2230445)Time elapsed: 0.624 s
% 13.26/2.54 % (2230445)Peak memory usage: 30 MB
% 13.26/2.54 % (2230445)Instructions burned: 866 (million)
% 13.26/2.54 % (2230455)fmb+10_1_sil=64000:random_seed=3298466139:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 13.26/2.54 % TRYING [1]
% 13.26/2.54 % TRYING [2]
% 13.26/2.54 % TRYING [3]
% 13.26/2.54 % TRYING [4]
% 13.26/2.54 % TRYING [6]
% 13.26/2.54 % TRYING [5]
% 13.26/2.54 % (2230451)Instruction limit reached!
% 13.26/2.54 % (2230451)------------------------------
% 13.26/2.54 % (2230451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230451)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230451)Termination reason: Instruction limit
% 13.26/2.54 % (2230451)Termination phase: Saturation
% 13.26/2.54 % (2230451)Time elapsed: 0.674 s
% 13.26/2.54 % (2230451)Peak memory usage: 17 MB
% 13.26/2.54 % (2230451)Instructions burned: 692 (million)
% 13.26/2.54 % (2230459)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3729077935:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 13.26/2.54 % (2230449)Instruction limit reached!
% 13.26/2.54 % (2230449)------------------------------
% 13.26/2.54 % (2230449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230449)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230449)Termination reason: Instruction limit
% 13.26/2.54 % (2230449)Termination phase: Finite model building constraint generation
% 13.26/2.54 % (2230449)Time elapsed: 0.818 s
% 13.26/2.54 % (2230449)Peak memory usage: 108 MB
% 13.26/2.54 % (2230449)Instructions burned: 890 (million)
% 13.26/2.54 % TRYING [20]
% 13.26/2.54 % (2230461)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1819790059:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 13.26/2.54 % TRYING [8]
% 13.26/2.54 % (2230453)Instruction limit reached!
% 13.26/2.54 % (2230453)------------------------------
% 13.26/2.54 % (2230453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230453)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230453)Termination reason: Instruction limit
% 13.26/2.54 % (2230453)Termination phase: Saturation
% 13.26/2.54 % (2230453)Time elapsed: 0.718 s
% 13.26/2.54 % (2230453)Peak memory usage: 20 MB
% 13.26/2.54 % (2230453)Instructions burned: 881 (million)
% 13.26/2.54 % (2230465)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3206415745:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 13.26/2.54 % (2230465) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2230416-2230465"...
% 13.26/2.54 % (2230465)...printing done.
% 13.26/2.54 % (2230465)Refutation found. Thanks to Tanya!
% 13.26/2.54 % SZS status Theorem for theBenchmark
% 13.26/2.54 % SZS output start Proof for theBenchmark
% See solution above
% 13.26/2.54 % (2230465)------------------------------
% 13.26/2.54 % (2230465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.54 % (2230465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.54 % (2230465)CaDiCaL version: 2.1.3
% 13.26/2.54 % (2230465)Termination reason: Refutation
% 13.26/2.54 % (2230465)Time elapsed: 0.211 s
% 13.26/2.54 % (2230465)Peak memory usage: 14 MB
% 13.26/2.54 % (2230465)Instructions burned: 226 (million)
% 13.26/2.54 % (2230416)Success in time 2.036 s
% 13.26/2.54 % Vampire exiting
%------------------------------------------------------------------------------