%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP021+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:53 AM UTC 2026
% Result : Theorem 37.28s 5.88s
% Output : Refutation 37.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 22
% Syntax : Number of formulae : 227 ( 57 unt; 8 def)
% Number of atoms : 616 ( 182 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 622 ( 233 ~; 336 |; 25 &)
% ( 3 <=>; 22 =>; 0 <=; 3 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 17 con; 0-2 aty)
% Number of variables : 125 ( 116 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f5,axiom,
! [X0] :
( mem(X0,bool)
=> ! [X1] :
( mem(X1,bool)
=> ( ( p(X0)
<=> p(X1) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001+2.ax',boolext) ).
fof(f9,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(f10,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
fof(f11,axiom,
ne(ty_2Eextreal_2Eextreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Eextreal_2Eextreal) ).
fof(f12,axiom,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eextreal_2Eextreal__le) ).
fof(f14,axiom,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eextreal_2Eextreal__max) ).
fof(f15,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(f16,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
fof(f39,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,X0)
=> ! [X2] :
( mem(X2,X0)
=> ( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1
& ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X1),X2) = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2ECOND__CLAUSES) ).
fof(f43,axiom,
! [X0] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ! [X1] :
( mem(X1,ty_2Eextreal_2Eextreal)
=> ! [X2] :
( mem(X2,ty_2Eextreal_2Eextreal)
=> ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X2)) )
=> p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Ele__trans) ).
fof(f44,axiom,
! [X0] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ! [X1] :
( mem(X1,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Ele__total) ).
fof(f45,axiom,
! [X0] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ! [X1] :
( mem(X1,ty_2Eextreal_2Eextreal)
=> ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,X0),X1)),X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Eextreal_2Eextreal__max__def) ).
fof(f56,conjecture,
! [X0] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ! [X1] :
( mem(X1,ty_2Eextreal_2Eextreal)
=> ! [X2] :
( mem(X2,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Emax__le) ).
fof(f57,negated_conjecture,
~ ! [X0] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ! [X1] :
( mem(X1,ty_2Eextreal_2Eextreal)
=> ! [X2] :
( mem(X2,ty_2Eextreal_2Eextreal)
=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f78,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(ennf_transformation,[],[f5]) ).
fof(f79,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(flattening,[],[f78]) ).
fof(f105,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1
& ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X1),X2) = X2 )
| ~ mem(X2,X0) )
| ~ mem(X1,X0) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f109,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X2))
| ~ mem(X2,ty_2Eextreal_2Eextreal) )
| ~ mem(X1,ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(ennf_transformation,[],[f43]) ).
fof(f110,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X2))
| ~ mem(X2,ty_2Eextreal_2Eextreal) )
| ~ mem(X1,ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0] :
( ! [X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(ennf_transformation,[],[f44]) ).
fof(f112,plain,
! [X0] :
( ! [X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,X0),X1)),X1),X0)
| ~ mem(X1,ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(ennf_transformation,[],[f45]) ).
fof(f126,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0))
<~> ( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0)) ) )
& mem(X2,ty_2Eextreal_2Eextreal) )
& mem(X1,ty_2Eextreal_2Eextreal) )
& mem(X0,ty_2Eextreal_2Eextreal) ),
inference(ennf_transformation,[],[f57]) ).
fof(f148,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( ( ~ p(X1)
| ~ p(X0) )
& ( p(X1)
| p(X0) ) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(nnf_transformation,[],[f79]) ).
fof(f219,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0)) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0)) )
& mem(X2,ty_2Eextreal_2Eextreal) )
& mem(X1,ty_2Eextreal_2Eextreal) )
& mem(X0,ty_2Eextreal_2Eextreal) ),
inference(nnf_transformation,[],[f126]) ).
fof(f220,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0)) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
& p(ap(ap(c_2Eextreal_2Eextreal__le,X2),X0)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,X1),X2)),X0)) )
& mem(X2,ty_2Eextreal_2Eextreal) )
& mem(X1,ty_2Eextreal_2Eextreal) )
& mem(X0,ty_2Eextreal_2Eextreal) ),
inference(flattening,[],[f219]) ).
fof(f221,plain,
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK19),sK18))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK20),sK18))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20)),sK18)) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,sK19),sK18))
& p(ap(ap(c_2Eextreal_2Eextreal__le,sK20),sK18)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20)),sK18)) )
& mem(sK20,ty_2Eextreal_2Eextreal)
& mem(sK19,ty_2Eextreal_2Eextreal)
& mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X2,sK20)],[f220]) ).
fof(f225,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f226,plain,
! [X0,X1] :
( ~ mem(X1,bool)
| p(X1)
| p(X0)
| X0 = X1
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f148]) ).
fof(f227,plain,
! [X0,X1] :
( ~ mem(X1,bool)
| ~ p(X1)
| ~ p(X0)
| X0 = X1
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f148]) ).
fof(f232,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f9]) ).
fof(f233,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f10]) ).
fof(f234,plain,
ne(ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f11]) ).
fof(f235,plain,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
inference(cnf_transformation,[],[f12]) ).
fof(f237,plain,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
inference(cnf_transformation,[],[f14]) ).
fof(f238,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f15]) ).
fof(f239,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f16]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ mem(X2,X0)
| ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X1),X2) = X2
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f291,plain,
! [X2,X0,X1] :
( ~ mem(X2,X0)
| ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f310,plain,
! [X2,X0,X1] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X2))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X2))
| ~ mem(X2,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[],[f110]) ).
fof(f311,plain,
! [X0,X1] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[],[f112]) ).
fof(f312,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,X0),X1)),X1),X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[],[f113]) ).
fof(f418,plain,
mem(sK18,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f221]) ).
fof(f419,plain,
mem(sK19,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f221]) ).
fof(f420,plain,
mem(sK20,ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f221]) ).
fof(f421,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK20),sK18))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20)),sK18)) ),
inference(cnf_transformation,[],[f221]) ).
fof(f422,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,sK19),sK18))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20)),sK18)) ),
inference(cnf_transformation,[],[f221]) ).
fof(f423,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK19),sK18))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sK20),sK18))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20)),sK18)) ),
inference(cnf_transformation,[],[f221]) ).
fof(f427,definition,
sF21 = ap(c_2Eextreal_2Eextreal__le,sK19),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f428,plain,
ap(c_2Eextreal_2Eextreal__le,sK19) = sF21,
inference(reorient_equations,[],[f427]) ).
fof(f429,definition,
sF22 = ap(sF21,sK18),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f430,plain,
ap(sF21,sK18) = sF22,
inference(reorient_equations,[],[f429]) ).
fof(f431,definition,
sF23 = ap(c_2Eextreal_2Eextreal__le,sK20),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f432,plain,
ap(c_2Eextreal_2Eextreal__le,sK20) = sF23,
inference(reorient_equations,[],[f431]) ).
fof(f433,definition,
sF24 = ap(sF23,sK18),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f434,plain,
ap(sF23,sK18) = sF24,
inference(reorient_equations,[],[f433]) ).
fof(f435,definition,
sF25 = ap(c_2Eextreal_2Eextreal__max,sK19),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f436,plain,
ap(c_2Eextreal_2Eextreal__max,sK19) = sF25,
inference(reorient_equations,[],[f435]) ).
fof(f437,definition,
sF26 = ap(sF25,sK20),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f438,plain,
ap(sF25,sK20) = sF26,
inference(reorient_equations,[],[f437]) ).
fof(f439,definition,
sF27 = ap(c_2Eextreal_2Eextreal__le,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f440,plain,
ap(c_2Eextreal_2Eextreal__le,sF26) = sF27,
inference(reorient_equations,[],[f439]) ).
fof(f441,definition,
sF28 = ap(sF27,sK18),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f442,plain,
ap(sF27,sK18) = sF28,
inference(reorient_equations,[],[f441]) ).
fof(f443,plain,
( ~ p(sF28)
| ~ p(sF24)
| ~ p(sF22) ),
inference(definition_folding,[],[f423,f442,f440,f438,f436,f434,f432,f430,f428]) ).
fof(f444,plain,
( p(sF22)
| p(sF28) ),
inference(definition_folding,[],[f422,f442,f440,f438,f436,f430,f428]) ).
fof(f445,plain,
( p(sF24)
| p(sF28) ),
inference(definition_folding,[],[f421,f442,f440,f438,f436,f434,f432]) ).
fof(f625,plain,
! [X0] :
( mem(ap(c_2Eextreal_2Eextreal__le,X0),arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f225,f235]) ).
fof(f627,plain,
! [X0] :
( mem(ap(c_2Eextreal_2Eextreal__max,X0),arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f225,f237]) ).
fof(f635,plain,
! [X0] :
( p(c_2Ebool_2EF)
| p(X0)
| c_2Ebool_2EF = X0
| ~ mem(X0,bool) ),
inference(resolution,[],[f226,f238]) ).
fof(f636,plain,
! [X0] :
( ~ mem(X0,bool)
| c_2Ebool_2EF = X0
| p(X0) ),
inference(forward_subsumption_resolution,[],[f635,f239]) ).
fof(f643,plain,
! [X0] :
( ~ p(c_2Ebool_2ET)
| ~ p(X0)
| c_2Ebool_2ET = X0
| ~ mem(X0,bool) ),
inference(resolution,[],[f227,f232]) ).
fof(f646,plain,
! [X0] :
( ~ mem(X0,bool)
| c_2Ebool_2ET = X0
| ~ p(X0) ),
inference(forward_subsumption_resolution,[],[f643,f233]) ).
fof(f665,plain,
( mem(sF21,arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f625,f428]) ).
fof(f666,plain,
( mem(sF23,arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f625,f432]) ).
fof(f667,plain,
( mem(sF27,arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(sF26,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f625,f440]) ).
fof(f668,plain,
mem(sF23,arr(ty_2Eextreal_2Eextreal,bool)),
inference(forward_subsumption_resolution,[],[f666,f420]) ).
fof(f669,plain,
mem(sF21,arr(ty_2Eextreal_2Eextreal,bool)),
inference(forward_subsumption_resolution,[],[f665,f419]) ).
fof(f670,plain,
! [X0] :
( mem(ap(sF23,X0),bool)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f668,f225]) ).
fof(f673,plain,
! [X0] :
( mem(ap(sF21,X0),bool)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f669,f225]) ).
fof(f681,plain,
! [X0] :
( p(ap(sF23,X0))
| c_2Ebool_2EF = ap(sF23,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f670,f636]) ).
fof(f682,plain,
! [X0] :
( ~ p(ap(sF23,X0))
| c_2Ebool_2ET = ap(sF23,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f670,f646]) ).
fof(f685,plain,
( mem(sF24,bool)
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f670,f434]) ).
fof(f686,plain,
mem(sF24,bool),
inference(forward_subsumption_resolution,[],[f685,f418]) ).
fof(f687,plain,
! [X0] :
( ~ mem(X0,bool)
| p(X0)
| sF24 = X0
| p(sF24) ),
inference(resolution,[],[f686,f226]) ).
fof(f692,plain,
( p(sF24)
| c_2Ebool_2EF = sF24 ),
inference(resolution,[],[f686,f636]) ).
fof(f693,plain,
( ~ p(sF24)
| c_2Ebool_2ET = sF24 ),
inference(resolution,[],[f686,f646]) ).
fof(f698,plain,
( c_2Ebool_2EF = sF24
| c_2Ebool_2ET = sF24 ),
inference(resolution,[],[f693,f692]) ).
fof(f731,plain,
( c_2Ebool_2ET != c_2Ebool_2EF
| c_2Ebool_2ET = sF24 ),
inference(equality_factoring,[],[f698]) ).
fof(f751,plain,
! [X0] :
( sK19 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),X0),sK19)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ ne(ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f290,f419]) ).
fof(f776,plain,
! [X0] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| sK19 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),X0),sK19) ),
inference(forward_subsumption_resolution,[],[f751,f234]) ).
fof(f783,plain,
! [X0] :
( p(ap(sF21,X0))
| c_2Ebool_2EF = ap(sF21,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f673,f636]) ).
fof(f784,plain,
! [X0] :
( ~ p(ap(sF21,X0))
| c_2Ebool_2ET = ap(sF21,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f673,f646]) ).
fof(f789,plain,
( mem(sF22,bool)
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f673,f430]) ).
fof(f790,plain,
mem(sF22,bool),
inference(forward_subsumption_resolution,[],[f789,f418]) ).
fof(f793,plain,
! [X0] :
( ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),X0),sK19) = X0
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ ne(ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f291,f419]) ).
fof(f820,plain,
! [X0] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),X0),sK19) = X0 ),
inference(forward_subsumption_resolution,[],[f793,f234]) ).
fof(f828,plain,
( ~ p(sF22)
| c_2Ebool_2ET = sF22 ),
inference(resolution,[],[f790,f646]) ).
fof(f840,plain,
! [X0] :
( p(ap(sF21,X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK19))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f311,f428]) ).
fof(f841,plain,
! [X0] :
( p(ap(sF23,X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK20))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f311,f432]) ).
fof(f844,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK20))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f841,f420]) ).
fof(f845,plain,
! [X0] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),sK19))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f840,f419]) ).
fof(f869,plain,
! [X0] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ap(ap(c_2Eextreal_2Eextreal__max,X0),sK20) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,X0),sK20)),sK20),X0) ),
inference(resolution,[],[f312,f420]) ).
fof(f881,plain,
! [X0,X1] :
( ~ p(ap(sF21,X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),sK19))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK19,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f310,f428]) ).
fof(f882,plain,
! [X0,X1] :
( ~ p(ap(sF23,X0))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),sK20))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f310,f432]) ).
fof(f883,plain,
! [X0,X1] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),sF26))
| ~ p(ap(sF27,X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sF26,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f310,f440]) ).
fof(f886,plain,
! [X0,X1] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),sK20))
| ~ p(ap(sF23,X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f882,f420]) ).
fof(f887,plain,
! [X0,X1] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),sK19))
| ~ p(ap(sF21,X0))
| p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f881,f419]) ).
fof(f893,plain,
sK19 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),sK20),sK19),
inference(resolution,[],[f776,f420]) ).
fof(f915,plain,
sK20 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),sK20),sK19),
inference(resolution,[],[f820,f420]) ).
fof(f921,plain,
( p(ap(sF21,sK20))
| p(ap(sF23,sK19))
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f844,f428]) ).
fof(f922,plain,
( p(ap(sF23,sK20))
| p(ap(sF23,sK20))
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f844,f432]) ).
fof(f924,plain,
( p(ap(sF23,sK20))
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literal_removal,[],[f922]) ).
fof(f926,plain,
p(ap(sF23,sK20)),
inference(forward_subsumption_resolution,[],[f924,f420]) ).
fof(f927,plain,
( p(ap(sF23,sK19))
| p(ap(sF21,sK20)) ),
inference(forward_subsumption_resolution,[],[f921,f419]) ).
fof(f930,plain,
( p(ap(sF21,sK19))
| p(ap(sF21,sK19))
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f845,f428]) ).
fof(f933,plain,
( p(ap(sF21,sK19))
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(duplicate_literal_removal,[],[f930]) ).
fof(f935,plain,
p(ap(sF21,sK19)),
inference(forward_subsumption_resolution,[],[f933,f419]) ).
fof(f952,plain,
ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,sK19),sK20)),sK20),sK19),
inference(resolution,[],[f869,f419]) ).
fof(f955,plain,
ap(ap(c_2Eextreal_2Eextreal__max,sK19),sK20) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(sF21,sK20)),sK20),sK19),
inference(forward_demodulation,[],[f952,f428]) ).
fof(f956,plain,
ap(sF25,sK20) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(sF21,sK20)),sK20),sK19),
inference(forward_demodulation,[],[f955,f436]) ).
fof(f957,plain,
sF26 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(sF21,sK20)),sK20),sK19),
inference(forward_demodulation,[],[f956,f438]) ).
fof(f962,plain,
! [X0] :
( ~ p(ap(sF21,sK20))
| ~ p(ap(sF23,X0))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f886,f428]) ).
fof(f968,plain,
! [X0] :
( ~ p(ap(sF23,X0))
| ~ p(ap(sF21,sK20))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f962,f419]) ).
fof(f978,plain,
! [X0] :
( ~ p(ap(sF23,sK19))
| ~ p(ap(sF21,X0))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f887,f432]) ).
fof(f983,plain,
! [X0] :
( ~ p(ap(sF23,sK19))
| ~ p(ap(sF21,X0))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f978,f420]) ).
fof(f1009,plain,
( mem(sF25,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f627,f436]) ).
fof(f1010,plain,
mem(sF25,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)),
inference(forward_subsumption_resolution,[],[f1009,f419]) ).
fof(f1012,plain,
! [X0] :
( mem(ap(sF25,X0),ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f1010,f225]) ).
fof(f1039,plain,
( mem(sF26,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f1012,f438]) ).
fof(f1040,plain,
mem(sF26,ty_2Eextreal_2Eextreal),
inference(forward_subsumption_resolution,[],[f1039,f420]) ).
fof(f1350,plain,
( p(sF24)
| sF22 = sF24
| p(sF22) ),
inference(resolution,[],[f687,f790]) ).
fof(f1356,plain,
( p(sF22)
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(resolution,[],[f1350,f693]) ).
fof(f1437,plain,
! [X0] :
( ~ p(ap(sF21,sF26))
| ~ p(ap(sF27,X0))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sF26,ty_2Eextreal_2Eextreal)
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f883,f428]) ).
fof(f1438,plain,
! [X0] :
( ~ p(ap(sF23,sF26))
| ~ p(ap(sF27,X0))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sF26,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f883,f432]) ).
fof(f1445,plain,
! [X0] :
( ~ p(ap(sF23,sF26))
| ~ p(ap(sF27,X0))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f1438,f1040]) ).
fof(f1446,plain,
! [X0] :
( ~ p(ap(sF21,sF26))
| ~ p(ap(sF27,X0))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f1437,f1040]) ).
fof(f1451,plain,
! [X0] :
( ~ p(ap(sF27,X0))
| ~ p(ap(sF23,sF26))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f1445,f420]) ).
fof(f1452,plain,
! [X0] :
( ~ p(ap(sF27,X0))
| ~ p(ap(sF21,sF26))
| p(ap(sF21,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f1446,f419]) ).
fof(f1651,plain,
( ~ p(sF24)
| ~ p(ap(sF21,sK20))
| p(ap(sF21,sK18))
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f968,f434]) ).
fof(f1652,plain,
( ~ p(sF24)
| ~ p(ap(sF21,sK20))
| p(ap(sF21,sK18)) ),
inference(forward_subsumption_resolution,[],[f1651,f418]) ).
fof(f1653,plain,
( ~ p(ap(sF21,sK20))
| ~ p(sF24)
| p(sF22) ),
inference(forward_demodulation,[],[f1652,f430]) ).
fof(f1654,plain,
! [X0] :
( ~ p(ap(sF21,X0))
| p(ap(sF23,X0))
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| p(ap(sF21,sK20)) ),
inference(resolution,[],[f983,f927]) ).
fof(f1663,plain,
( ~ p(sF28)
| ~ p(ap(sF23,sF26))
| p(ap(sF23,sK18))
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f1451,f442]) ).
fof(f1664,plain,
( ~ p(sF28)
| ~ p(ap(sF23,sF26))
| p(ap(sF23,sK18)) ),
inference(forward_subsumption_resolution,[],[f1663,f418]) ).
fof(f1666,plain,
( p(sF24)
| ~ p(sF28)
| ~ p(ap(sF23,sF26)) ),
inference(forward_demodulation,[],[f1664,f434]) ).
fof(f1668,plain,
( ~ p(ap(sF23,sF26))
| p(sF24) ),
inference(forward_subsumption_resolution,[],[f1666,f445]) ).
fof(f1669,plain,
( p(sF24)
| c_2Ebool_2EF = ap(sF23,sF26)
| ~ mem(sF26,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f1668,f681]) ).
fof(f1670,plain,
( p(sF24)
| c_2Ebool_2EF = ap(sF23,sF26) ),
inference(forward_subsumption_resolution,[],[f1669,f1040]) ).
fof(f1673,plain,
( ~ p(sF28)
| ~ p(ap(sF21,sF26))
| p(ap(sF21,sK18))
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f1452,f442]) ).
fof(f1674,plain,
( ~ p(sF28)
| ~ p(ap(sF21,sF26))
| p(ap(sF21,sK18)) ),
inference(forward_subsumption_resolution,[],[f1673,f418]) ).
fof(f1675,plain,
( p(sF22)
| ~ p(sF28)
| ~ p(ap(sF21,sF26)) ),
inference(forward_demodulation,[],[f1674,f430]) ).
fof(f1676,plain,
( ~ p(ap(sF21,sF26))
| p(sF22) ),
inference(forward_subsumption_resolution,[],[f1675,f444]) ).
fof(f1678,plain,
( c_2Ebool_2EF = ap(sF23,sF26)
| c_2Ebool_2ET = sF24 ),
inference(resolution,[],[f1670,f693]) ).
fof(f1712,plain,
( c_2Ebool_2ET = ap(sF23,sK20)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f682,f926]) ).
fof(f1720,plain,
c_2Ebool_2ET = ap(sF23,sK20),
inference(forward_subsumption_resolution,[],[f1712,f420]) ).
fof(f2067,plain,
! [X0] :
( ~ mem(sF26,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| mem(ap(sF27,X0),bool) ),
inference(resolution,[],[f667,f225]) ).
fof(f2076,plain,
! [X0] :
( mem(ap(sF27,X0),bool)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(forward_subsumption_resolution,[],[f2067,f1040]) ).
fof(f2124,plain,
( mem(sF28,bool)
| ~ mem(sK18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f2076,f442]) ).
fof(f2125,plain,
mem(sF28,bool),
inference(forward_subsumption_resolution,[],[f2124,f418]) ).
fof(f2156,plain,
( p(sF28)
| c_2Ebool_2EF = sF28 ),
inference(resolution,[],[f2125,f636]) ).
fof(f2273,plain,
( ~ p(sF24)
| c_2Ebool_2EF = sF28
| ~ p(sF22) ),
inference(resolution,[],[f2156,f443]) ).
fof(f5872,plain,
( c_2Ebool_2EF = ap(sF21,sK20)
| ~ mem(sK20,ty_2Eextreal_2Eextreal)
| ~ p(sF24)
| p(sF22) ),
inference(resolution,[],[f783,f1653]) ).
fof(f5873,plain,
( c_2Ebool_2EF = ap(sF21,sF26)
| ~ mem(sF26,ty_2Eextreal_2Eextreal)
| p(sF22) ),
inference(resolution,[],[f783,f1676]) ).
fof(f5876,plain,
( p(sF22)
| c_2Ebool_2EF = ap(sF21,sF26) ),
inference(forward_subsumption_resolution,[],[f5873,f1040]) ).
fof(f5877,plain,
( ~ p(sF24)
| c_2Ebool_2EF = ap(sF21,sK20)
| p(sF22) ),
inference(forward_subsumption_resolution,[],[f5872,f420]) ).
fof(f5881,plain,
( c_2Ebool_2EF = ap(sF21,sF26)
| c_2Ebool_2ET = sF22 ),
inference(resolution,[],[f5876,f828]) ).
fof(f5909,plain,
( c_2Ebool_2EF = ap(sF21,sK20)
| p(sF22)
| sF22 = sF24
| p(sF22) ),
inference(resolution,[],[f5877,f1350]) ).
fof(f5926,plain,
( p(sF22)
| c_2Ebool_2EF = ap(sF21,sK20)
| sF22 = sF24 ),
inference(duplicate_literal_removal,[],[f5909]) ).
fof(f5949,plain,
( c_2Ebool_2EF = ap(sF21,sK20)
| sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(resolution,[],[f5926,f828]) ).
fof(f6782,plain,
( sF26 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),sK20),sK19)
| sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(superposition,[],[f957,f5949]) ).
fof(f6792,plain,
( sK19 = sF26
| sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(forward_demodulation,[],[f6782,f893]) ).
fof(f6812,plain,
( ~ p(ap(sF21,sK19))
| p(sF22)
| sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(superposition,[],[f1676,f6792]) ).
fof(f6835,plain,
( p(sF22)
| sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(forward_subsumption_resolution,[],[f6812,f935]) ).
fof(f6840,plain,
( sF22 = sF24
| c_2Ebool_2ET = sF22 ),
inference(forward_subsumption_resolution,[],[f6835,f828]) ).
fof(f7558,plain,
( c_2Ebool_2ET = ap(sF21,sK19)
| ~ mem(sK19,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f784,f935]) ).
fof(f7560,plain,
! [X0] :
( c_2Ebool_2ET = ap(sF21,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| c_2Ebool_2EF = ap(sF21,X0)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f784,f783]) ).
fof(f7578,plain,
! [X0] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| c_2Ebool_2ET = ap(sF21,X0)
| c_2Ebool_2EF = ap(sF21,X0) ),
inference(duplicate_literal_removal,[],[f7560]) ).
fof(f7580,plain,
c_2Ebool_2ET = ap(sF21,sK19),
inference(forward_subsumption_resolution,[],[f7558,f419]) ).
fof(f10418,plain,
( ~ p(sF22)
| p(ap(sF23,sK18))
| ~ mem(sK18,ty_2Eextreal_2Eextreal)
| p(ap(sF21,sK20)) ),
inference(superposition,[],[f1654,f430]) ).
fof(f10437,plain,
( ~ p(sF22)
| p(ap(sF23,sK18))
| p(ap(sF21,sK20)) ),
inference(forward_subsumption_resolution,[],[f10418,f418]) ).
fof(f10438,plain,
( p(ap(sF21,sK20))
| ~ p(sF22)
| p(sF24) ),
inference(forward_demodulation,[],[f10437,f434]) ).
fof(f10441,plain,
( ~ p(sF22)
| p(sF24)
| c_2Ebool_2ET = ap(sF21,sK20)
| ~ mem(sK20,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f10438,f784]) ).
fof(f10448,plain,
( ~ p(sF22)
| p(sF24)
| c_2Ebool_2ET = ap(sF21,sK20) ),
inference(forward_subsumption_resolution,[],[f10441,f420]) ).
fof(f11223,plain,
( p(sF24)
| c_2Ebool_2ET = ap(sF21,sK20)
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(resolution,[],[f10448,f1356]) ).
fof(f11248,plain,
( c_2Ebool_2ET = ap(sF21,sK20)
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(forward_subsumption_resolution,[],[f11223,f693]) ).
fof(f13927,plain,
( sF26 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),sK20),sK19)
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(superposition,[],[f957,f11248]) ).
fof(f13960,plain,
( sK20 = sF26
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(forward_demodulation,[],[f13927,f915]) ).
fof(f14008,plain,
( c_2Ebool_2EF = ap(sF23,sK20)
| c_2Ebool_2ET = sF24
| sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(superposition,[],[f1678,f13960]) ).
fof(f14065,plain,
( c_2Ebool_2EF = ap(sF23,sK20)
| c_2Ebool_2ET = sF24
| sF22 = sF24 ),
inference(duplicate_literal_removal,[],[f14008]) ).
fof(f14074,plain,
( c_2Ebool_2ET = c_2Ebool_2EF
| c_2Ebool_2ET = sF24
| sF22 = sF24 ),
inference(forward_demodulation,[],[f14065,f1720]) ).
fof(f14082,plain,
( sF22 = sF24
| c_2Ebool_2ET = sF24 ),
inference(forward_subsumption_resolution,[],[f14074,f731]) ).
fof(f14184,plain,
( c_2Ebool_2ET != sF22
| c_2Ebool_2ET = sF24 ),
inference(equality_factoring,[],[f14082]) ).
fof(f23270,plain,
( c_2Ebool_2EF = ap(sF21,sK20)
| c_2Ebool_2ET = ap(sF21,sK20) ),
inference(resolution,[],[f7578,f420]) ).
fof(f23297,plain,
( sF26 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),sK20),sK19)
| c_2Ebool_2ET = ap(sF21,sK20) ),
inference(superposition,[],[f957,f23270]) ).
fof(f23334,plain,
( c_2Ebool_2ET = ap(sF21,sK20)
| sK19 = sF26 ),
inference(forward_demodulation,[],[f23297,f893]) ).
fof(f23360,plain,
( sF26 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),sK20),sK19)
| sK19 = sF26 ),
inference(superposition,[],[f957,f23334]) ).
fof(f23402,plain,
( sK20 = sF26
| sK19 = sF26 ),
inference(forward_demodulation,[],[f23360,f915]) ).
fof(f23414,plain,
( ap(c_2Eextreal_2Eextreal__le,sK20) = sF27
| sK19 = sF26 ),
inference(superposition,[],[f440,f23402]) ).
fof(f23431,plain,
( c_2Ebool_2EF = ap(sF23,sK20)
| c_2Ebool_2ET = sF24
| sK19 = sF26 ),
inference(superposition,[],[f1678,f23402]) ).
fof(f23523,plain,
( c_2Ebool_2ET = c_2Ebool_2EF
| c_2Ebool_2ET = sF24
| sK19 = sF26 ),
inference(forward_demodulation,[],[f23431,f1720]) ).
fof(f23527,plain,
( sF23 = sF27
| sK19 = sF26 ),
inference(forward_demodulation,[],[f23414,f432]) ).
fof(f23530,plain,
( sK19 = sF26
| c_2Ebool_2ET = sF24 ),
inference(forward_subsumption_resolution,[],[f23523,f731]) ).
fof(f23627,plain,
( ap(sF23,sK18) = sF28
| sK19 = sF26 ),
inference(superposition,[],[f442,f23527]) ).
fof(f23709,plain,
( sK19 = sF26
| sF24 = sF28 ),
inference(forward_demodulation,[],[f23627,f434]) ).
fof(f23775,plain,
( c_2Ebool_2EF = ap(sF21,sK19)
| c_2Ebool_2ET = sF22
| c_2Ebool_2ET = sF24 ),
inference(superposition,[],[f5881,f23530]) ).
fof(f23853,plain,
( c_2Ebool_2EF = ap(sF21,sK19)
| c_2Ebool_2ET = sF24 ),
inference(forward_subsumption_resolution,[],[f23775,f14184]) ).
fof(f23867,plain,
( c_2Ebool_2ET = c_2Ebool_2EF
| c_2Ebool_2ET = sF24 ),
inference(forward_demodulation,[],[f23853,f7580]) ).
fof(f23868,plain,
c_2Ebool_2ET = sF24,
inference(forward_subsumption_resolution,[],[f23867,f731]) ).
fof(f23958,plain,
( ~ p(c_2Ebool_2ET)
| c_2Ebool_2EF = sF28
| ~ p(sF22) ),
inference(superposition,[],[f2273,f23868]) ).
fof(f23992,plain,
( c_2Ebool_2ET = sF22
| c_2Ebool_2ET = sF22 ),
inference(superposition,[],[f6840,f23868]) ).
fof(f24027,plain,
c_2Ebool_2ET = sF22,
inference(duplicate_literal_removal,[],[f23992]) ).
fof(f24036,plain,
( c_2Ebool_2EF = sF28
| ~ p(sF22) ),
inference(forward_subsumption_resolution,[],[f23958,f233]) ).
fof(f24042,plain,
( ~ p(c_2Ebool_2ET)
| c_2Ebool_2EF = sF28 ),
inference(forward_demodulation,[],[f24036,f24027]) ).
fof(f24046,plain,
c_2Ebool_2EF = sF28,
inference(forward_subsumption_resolution,[],[f24042,f233]) ).
fof(f24216,plain,
~ p(sF28),
inference(superposition,[],[f239,f24046]) ).
fof(f24547,plain,
( ap(c_2Eextreal_2Eextreal__le,sK19) = sF27
| sF24 = sF28 ),
inference(superposition,[],[f440,f23709]) ).
fof(f24680,plain,
( sF21 = sF27
| sF24 = sF28 ),
inference(forward_demodulation,[],[f24547,f428]) ).
fof(f24694,plain,
( sF21 = sF27
| c_2Ebool_2ET = sF28 ),
inference(forward_demodulation,[],[f24680,f23868]) ).
fof(f25332,plain,
( ap(sF21,sK18) = sF28
| c_2Ebool_2ET = sF28 ),
inference(superposition,[],[f442,f24694]) ).
fof(f25419,plain,
( sF22 = sF28
| c_2Ebool_2ET = sF28 ),
inference(forward_demodulation,[],[f25332,f430]) ).
fof(f25421,plain,
( c_2Ebool_2ET = sF28
| c_2Ebool_2ET = sF28 ),
inference(forward_demodulation,[],[f25419,f24027]) ).
fof(f25422,plain,
c_2Ebool_2ET = sF28,
inference(duplicate_literal_removal,[],[f25421]) ).
fof(f25424,plain,
p(sF28),
inference(superposition,[],[f233,f25422]) ).
fof(f25566,plain,
$false,
inference(forward_subsumption_resolution,[],[f25424,f24216]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.40 % Computer : n019.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 12:07:03 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.46 Running first-order model finding
% 0.14/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.37/4.28 % (2974645)Will run a generic schedule for satisfiability detection.
% 26.37/4.28 % (2974656)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1476987299:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.37/4.28 % (2974651)% WARNING: option uhcvi not known.
% 26.37/4.28 % (2974650)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1018828970_2999 on theBenchmark for (2999ds/0Mi)
% 26.37/4.28 % (2974652)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3449512689:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.37/4.28 % (2974653)dis+10_1_sil=32000:sp=arity:random_seed=2089748056:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.37/4.28 % (2974654)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1358606063:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.37/4.28 % (2974655)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3868760755:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.37/4.28 % (2974651)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2021714696:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.37/4.28 % TRYING [1]
% 26.37/4.28 % TRYING [2]
% 26.37/4.28 % TRYING [3]
% 26.37/4.28 % TRYING [4]
% 26.37/4.28 % (2974656)Instruction limit reached!
% 26.37/4.28 % (2974656)------------------------------
% 26.37/4.28 % (2974656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.37/4.28 % (2974656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.28 % (2974656)CaDiCaL version: 2.1.3
% 26.37/4.28 % (2974656)Termination reason: Instruction limit
% 26.37/4.28 % (2974656)Termination phase: Saturation
% 26.37/4.28 % (2974656)Time elapsed: 0.082 s
% 26.37/4.28 % (2974656)Peak memory usage: 14 MB
% 26.37/4.28 % (2974656)Instructions burned: 159 (million)
% 26.37/4.28 % (2974664)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1799404007:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 26.37/4.28 % (2974653)Instruction limit reached!
% 26.37/4.28 % (2974653)------------------------------
% 26.37/4.28 % (2974653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.37/4.28 % (2974653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.28 % (2974653)CaDiCaL version: 2.1.3
% 26.37/4.28 % (2974653)Termination reason: Instruction limit
% 26.37/4.28 % (2974653)Termination phase: Saturation
% 26.37/4.28 % (2974653)Time elapsed: 0.100 s
% 26.37/4.28 % (2974653)Peak memory usage: 12 MB
% 26.37/4.28 % (2974653)Instructions burned: 103 (million)
% 26.37/4.28 % TRYING [1]
% 26.37/4.28 % TRYING [2]
% 26.37/4.28 % TRYING [5]
% 26.37/4.28 % TRYING [3]
% 26.37/4.28 % (2974655)Instruction limit reached!
% 26.37/4.28 % (2974655)------------------------------
% 26.37/4.28 % (2974655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.37/4.28 % (2974655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.28 % (2974655)CaDiCaL version: 2.1.3
% 26.37/4.28 % (2974655)Termination reason: Instruction limit
% 26.37/4.28 % (2974655)Termination phase: Saturation
% 26.37/4.28 % (2974655)Time elapsed: 0.119 s
% 26.37/4.28 % (2974655)Peak memory usage: 13 MB
% 26.37/4.28 % (2974655)Instructions burned: 131 (million)
% 26.37/4.28 % (2974654)Instruction limit reached!
% 26.37/4.28 % (2974654)------------------------------
% 26.37/4.28 % (2974654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.37/4.28 % (2974654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.28 % (2974654)CaDiCaL version: 2.1.3
% 26.37/4.28 % (2974654)Termination reason: Instruction limit
% 26.37/4.28 % (2974654)Termination phase: Saturation
% 26.37/4.28 % (2974654)Time elapsed: 0.121 s
% 26.37/4.28 % (2974654)Peak memory usage: 13 MB
% 26.37/4.28 % (2974654)Instructions burned: 116 (million)
% 26.37/4.28 % TRYING [4]
% 26.37/4.28 % (2974666)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1630128724:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.37/4.28 % (2974667)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=197199886:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.37/4.28 % (2974668)ott-21_1_sil=16000:fs=off:random_seed=1629478020:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 26.37/4.28 % TRYING [5]
% 26.37/4.28 % (2974666)Instruction limit reached!
% 26.37/4.28 % (2974666)------------------------------
% 26.37/4.28 % (2974666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974666)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974666)Termination reason: Instruction limit
% 37.28/5.88 % (2974666)Termination phase: Saturation
% 37.28/5.88 % (2974666)Time elapsed: 0.133 s
% 37.28/5.88 % (2974666)Peak memory usage: 13 MB
% 37.28/5.88 % (2974666)Instructions burned: 131 (million)
% 37.28/5.88 % (2974674)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1594731406:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 37.28/5.88 % (2974668)Instruction limit reached!
% 37.28/5.88 % (2974668)------------------------------
% 37.28/5.88 % (2974668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974668)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974668)Termination reason: Instruction limit
% 37.28/5.88 % (2974668)Termination phase: Saturation
% 37.28/5.88 % (2974668)Time elapsed: 0.172 s
% 37.28/5.88 % (2974668)Peak memory usage: 13 MB
% 37.28/5.88 % (2974668)Instructions burned: 181 (million)
% 37.28/5.88 % (2974676)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3215857885:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 37.28/5.88 % TRYING [1]
% 37.28/5.88 % TRYING [2]
% 37.28/5.88 % TRYING [3]
% 37.28/5.88 % TRYING [6]
% 37.28/5.88 % (2974664)Instruction limit reached!
% 37.28/5.88 % (2974664)------------------------------
% 37.28/5.88 % (2974664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974664)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974664)Termination reason: Instruction limit
% 37.28/5.88 % (2974664)Termination phase: Finite model building SAT solving
% 37.28/5.88 % (2974664)Time elapsed: 0.318 s
% 37.28/5.88 % (2974664)Peak memory usage: 22 MB
% 37.28/5.88 % (2974664)Instructions burned: 715 (million)
% 37.28/5.88 % TRYING [4]
% 37.28/5.88 % (2974678)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2998034835:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 37.28/5.88 % TRYING [5]
% 37.28/5.88 % TRYING [6]
% 37.28/5.88 % (2974676)Instruction limit reached!
% 37.28/5.88 % (2974676)------------------------------
% 37.28/5.88 % (2974676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974676)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974676)Termination reason: Instruction limit
% 37.28/5.88 % (2974676)Termination phase: Finite model building SAT solving
% 37.28/5.88 % (2974676)Time elapsed: 0.365 s
% 37.28/5.88 % (2974676)Peak memory usage: 25 MB
% 37.28/5.88 % (2974676)Instructions burned: 867 (million)
% 37.28/5.88 % (2974667)Instruction limit reached!
% 37.28/5.88 % (2974667)------------------------------
% 37.28/5.88 % (2974667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974667)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974667)Termination reason: Instruction limit
% 37.28/5.88 % (2974667)Termination phase: Saturation
% 37.28/5.88 % (2974667)Time elapsed: 0.591 s
% 37.28/5.88 % (2974667)Peak memory usage: 18 MB
% 37.28/5.88 % (2974667)Instructions burned: 685 (million)
% 37.28/5.88 % (2974682)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3655523624:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 37.28/5.88 % (2974684)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=317041450:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 37.28/5.88 % (2974674)Instruction limit reached!
% 37.28/5.88 % (2974674)------------------------------
% 37.28/5.88 % (2974674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974674)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974674)Termination reason: Instruction limit
% 37.28/5.88 % (2974674)Termination phase: Saturation
% 37.28/5.88 % (2974674)Time elapsed: 0.479 s
% 37.28/5.88 % (2974674)Peak memory usage: 14 MB
% 37.28/5.88 % (2974674)Instructions burned: 477 (million)
% 37.28/5.88 % (2974686)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3605800919:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 37.28/5.88 % TRYING [14]
% 37.28/5.88 % TRYING [7]
% 37.28/5.88 % (2974684)Instruction limit reached!
% 37.28/5.88 % (2974684)------------------------------
% 37.28/5.88 % (2974684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974684)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974684)Termination reason: Instruction limit
% 37.28/5.88 % (2974684)Termination phase: Saturation
% 37.28/5.88 % (2974684)Time elapsed: 0.334 s
% 37.28/5.88 % (2974684)Peak memory usage: 17 MB
% 37.28/5.88 % (2974684)Instructions burned: 694 (million)
% 37.28/5.88 % (2974688)fmb+10_1_sil=64000:random_seed=569932568:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 37.28/5.88 % TRYING [1]
% 37.28/5.88 % TRYING [2]
% 37.28/5.88 % TRYING [3]
% 37.28/5.88 % TRYING [4]
% 37.28/5.88 % TRYING [5]
% 37.28/5.88 % (2974682)Instruction limit reached!
% 37.28/5.88 % (2974682)------------------------------
% 37.28/5.88 % (2974682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974682)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974682)Termination reason: Instruction limit
% 37.28/5.88 % (2974682)Termination phase: Finite model building constraint generation
% 37.28/5.88 % (2974682)Time elapsed: 0.619 s
% 37.28/5.88 % (2974682)Peak memory usage: 75 MB
% 37.28/5.88 % (2974682)Instructions burned: 890 (million)
% 37.28/5.88 % (2974690)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2081579201:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 37.28/5.88 % TRYING [6]
% 37.28/5.88 % TRYING [20]
% 37.28/5.88 % (2974678)Instruction limit reached!
% 37.28/5.88 % (2974678)------------------------------
% 37.28/5.88 % (2974678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974678)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974678)Termination reason: Instruction limit
% 37.28/5.88 % (2974678)Termination phase: Saturation
% 37.28/5.88 % (2974678)Time elapsed: 1.012 s
% 37.28/5.88 % (2974678)Peak memory usage: 19 MB
% 37.28/5.88 % (2974678)Instructions burned: 1180 (million)
% 37.28/5.88 % (2974692)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2461621849:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 37.28/5.88 % TRYING [8]
% 37.28/5.88 % (2974686)Instruction limit reached!
% 37.28/5.88 % (2974686)------------------------------
% 37.28/5.88 % (2974686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974686)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974686)Termination reason: Instruction limit
% 37.28/5.88 % (2974686)Termination phase: Saturation
% 37.28/5.88 % (2974686)Time elapsed: 0.788 s
% 37.28/5.88 % (2974686)Peak memory usage: 20 MB
% 37.28/5.88 % (2974686)Instructions burned: 879 (million)
% 37.28/5.88 % (2974694)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3949002231:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 37.28/5.88 % TRYING [7]
% 37.28/5.88 % (2974692)Instruction limit reached!
% 37.28/5.88 % (2974692)------------------------------
% 37.28/5.88 % (2974692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974692)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974692)Termination reason: Instruction limit
% 37.28/5.88 % (2974692)Termination phase: Finite model building SAT solving
% 37.28/5.88 % (2974692)Time elapsed: 0.761 s
% 37.28/5.88 % (2974692)Peak memory usage: 60 MB
% 37.28/5.88 % (2974692)Instructions burned: 920 (million)
% 37.28/5.88 % (2974696)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1079138289:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 37.28/5.88 % TRYING [8]
% 37.28/5.88 % (2974696)Instruction limit reached!
% 37.28/5.88 % (2974696)------------------------------
% 37.28/5.88 % (2974696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974696)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974696)Termination reason: Instruction limit
% 37.28/5.88 % (2974696)Termination phase: Saturation
% 37.28/5.88 % (2974696)Time elapsed: 1.448 s
% 37.28/5.88 % (2974696)Peak memory usage: 31 MB
% 37.28/5.88 % (2974696)Instructions burned: 1472 (million)
% 37.28/5.88 % (2974702)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1156939818:i=6324_2962 on theBenchmark for (2962ds/6324Mi)
% 37.28/5.88 % TRYING [77]
% 37.28/5.88 % (2974694)Instruction limit reached!
% 37.28/5.88 % (2974694)------------------------------
% 37.28/5.88 % (2974694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974694)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974694)Termination reason: Instruction limit
% 37.28/5.88 % (2974694)Termination phase: Saturation
% 37.28/5.88 % (2974694)Time elapsed: 2.292 s
% 37.28/5.88 % (2974694)Peak memory usage: 28 MB
% 37.28/5.88 % (2974694)Instructions burned: 5133 (million)
% 37.28/5.88 % (2974706)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1773179393:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 37.28/5.88 % TRYING [16]
% 37.28/5.88 % TRYING [8]
% 37.28/5.88 % (2974706)Instruction limit reached!
% 37.28/5.88 % (2974706)------------------------------
% 37.28/5.88 % (2974706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974706)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974706)Termination reason: Instruction limit
% 37.28/5.88 % (2974706)Termination phase: Finite model building constraint generation
% 37.28/5.88 % (2974706)Time elapsed: 0.594 s
% 37.28/5.88 % (2974706)Peak memory usage: 137 MB
% 37.28/5.88 % (2974706)Instructions burned: 2178 (million)
% 37.28/5.88 % (2974721)ott-2_1_sil=16000:newcnf=on:random_seed=3792700572:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 37.28/5.88 % (2974721)Instruction limit reached!
% 37.28/5.88 % (2974721)------------------------------
% 37.28/5.88 % (2974721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974721)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974721)Termination reason: Instruction limit
% 37.28/5.88 % (2974721)Termination phase: Saturation
% 37.28/5.88 % (2974721)Time elapsed: 0.264 s
% 37.28/5.88 % (2974721)Peak memory usage: 18 MB
% 37.28/5.88 % (2974721)Instructions burned: 871 (million)
% 37.28/5.88 % (2974817)ott+10_1_sil=32000:tgt=ground:random_seed=313260081:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 37.28/5.88 % (2974817) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2974645-2974817"...
% 37.28/5.88 % (2974817)...printing done.
% 37.28/5.88 % (2974817)Refutation found. Thanks to Tanya!
% 37.28/5.88 % SZS status Theorem for theBenchmark
% 37.28/5.88 % SZS output start Proof for theBenchmark
% See solution above
% 37.28/5.88 % (2974817)------------------------------
% 37.28/5.88 % (2974817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.28/5.88 % (2974817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.28/5.88 % (2974817)CaDiCaL version: 2.1.3
% 37.28/5.88 % (2974817)Termination reason: Refutation
% 37.28/5.88 % (2974817)Time elapsed: 0.445 s
% 37.28/5.88 % (2974817)Peak memory usage: 22 MB
% 37.28/5.88 % (2974817)Instructions burned: 1456 (million)
% 37.28/5.88 % (2974645)Success in time 5.409 s
% 37.28/5.88 % Vampire exiting
%------------------------------------------------------------------------------