%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP003+2 : 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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:27:41 AM UTC 2026
% Result : Theorem 18.14s 3.44s
% Output : Refutation 18.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 37
% Syntax : Number of formulae : 219 ( 46 unt; 10 def)
% Number of atoms : 719 ( 108 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 925 ( 425 ~; 430 |; 25 &)
% ( 19 <=>; 24 =>; 0 <=; 2 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 11 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 171 ( 0 sgn 161 !; 10 ?)
% 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/theBenchmark.p',ap_tp) ).
fof(f5,axiom,
! [X0] :
( mem(X0,bool)
=> ! [X1] :
( mem(X1,bool)
=> ( ( p(X0)
<=> p(X1) )
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',boolext) ).
fof(f9,axiom,
ne(ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Enum_2Enum) ).
fof(f10,axiom,
mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2EBIT1) ).
fof(f11,axiom,
mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2EEVEN) ).
fof(f12,axiom,
mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2EZERO) ).
fof(f13,axiom,
mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2EBIT2) ).
fof(f14,axiom,
mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2ENUMERAL) ).
fof(f17,axiom,
mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Earithmetic_2E_2A) ).
fof(f19,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
fof(f20,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
fof(f25,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
fof(f27,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(f28,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
fof(f41,axiom,
ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,c_2Enum_2E0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EONE) ).
fof(f42,axiom,
ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2ETWO) ).
fof(f43,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ap(ap(c_2Earithmetic_2E_2B,X0),c_2Enum_2E0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EADD__0) ).
fof(f44,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Enum_2ESUC,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2ELESS__MONO__EQ) ).
fof(f45,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ap(c_2Enum_2ESUC,X0) = ap(ap(c_2Earithmetic_2E_2B,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EADD1) ).
fof(f46,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ap(ap(c_2Earithmetic_2E_2A,X0),X1) = ap(ap(c_2Earithmetic_2E_2A,X1),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMULT__COMM) ).
fof(f47,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ( p(ap(c_2Earithmetic_2EEVEN,X0))
<=> ~ p(ap(c_2Earithmetic_2EODD,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EEVEN__ODD) ).
fof(f49,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ( p(ap(c_2Earithmetic_2EEVEN,X0))
<=> ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EEVEN__EXISTS) ).
fof(f50,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ( p(ap(c_2Earithmetic_2EODD,X0))
<=> ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EODD__EXISTS) ).
fof(f51,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ! [X2] :
( mem(X2,ty_2Enum_2Enum)
=> ( ? [X3] :
( mem(X3,ty_2Enum_2Enum)
& X1 = ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2)
& p(ap(ap(c_2Eprim__rec_2E_3C,X2),X0)) )
=> ap(ap(c_2Earithmetic_2EMOD,X1),X0) = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMOD__UNIQUE) ).
fof(f66,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(f82,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Enum_2ESUC,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eprim__rec_2ELESS__0) ).
fof(f98,conjecture,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,X0)),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMOD__2) ).
fof(f99,negated_conjecture,
~ ! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,X0)),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
fof(f123,plain,
? [X0] :
( ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,X0)),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))
& mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f99]) ).
fof(f128,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(ennf_transformation,[],[f5]) ).
fof(f129,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0] :
( ap(c_2Enum_2ESUC,X0) = ap(ap(c_2Earithmetic_2E_2B,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f45]) ).
fof(f131,plain,
! [X0] :
( ( p(ap(c_2Earithmetic_2EEVEN,X0))
<=> ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f49]) ).
fof(f133,plain,
! [X0] :
( ( p(ap(c_2Earithmetic_2EEVEN,X0))
<=> ~ p(ap(c_2Earithmetic_2EODD,X0)) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f47]) ).
fof(f134,plain,
! [X0] :
( ( p(ap(c_2Earithmetic_2EODD,X0))
<=> ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f50]) ).
fof(f135,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ap(ap(c_2Earithmetic_2EMOD,X1),X0) = X2
| ! [X3] :
( ~ mem(X3,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2) != X1
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X2),X0)) )
| ~ mem(X2,ty_2Enum_2Enum) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f51]) ).
fof(f136,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ap(ap(c_2Earithmetic_2EMOD,X1),X0) = X2
| ! [X3] :
( ~ mem(X3,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2) != X1
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X2),X0)) )
| ~ mem(X2,ty_2Enum_2Enum) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(flattening,[],[f135]) ).
fof(f140,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,[],[f66]) ).
fof(f142,plain,
! [X0] :
( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Enum_2ESUC,X0)))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f82]) ).
fof(f143,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2E_2B,X0),c_2Enum_2E0) = X0
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f43]) ).
fof(f155,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f196,plain,
! [X0] :
( ! [X1] :
( ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Enum_2ESUC,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f44]) ).
fof(f197,plain,
! [X0] :
( ! [X1] :
( ap(ap(c_2Earithmetic_2E_2A,X0),X1) = ap(ap(c_2Earithmetic_2E_2A,X1),X0)
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f46]) ).
fof(f222,plain,
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,sK18)),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))
& mem(sK18,ty_2Enum_2Enum) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X0,sK18)],[f123]) ).
fof(f225,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( ( ~ p(X1)
| ~ p(X0) )
& ( p(X1)
| p(X0) ) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(nnf_transformation,[],[f129]) ).
fof(f226,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EEVEN,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) != X0 ) )
& ( ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) )
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(nnf_transformation,[],[f131]) ).
fof(f227,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EEVEN,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) != X0 ) )
& ( ? [X2] :
( mem(X2,ty_2Enum_2Enum)
& ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X2) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(rectify,[],[f226]) ).
fof(f228,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EEVEN,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1) != X0 ) )
& ( ( mem(sK20(X0),ty_2Enum_2Enum)
& ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),sK20(X0)) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X2,sK20(X0))],[f227]) ).
fof(f230,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EEVEN,X0))
| p(ap(c_2Earithmetic_2EODD,X0)) )
& ( ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(nnf_transformation,[],[f133]) ).
fof(f231,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EODD,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) != X0 ) )
& ( ? [X1] :
( mem(X1,ty_2Enum_2Enum)
& X0 = ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) )
| ~ p(ap(c_2Earithmetic_2EODD,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(nnf_transformation,[],[f134]) ).
fof(f232,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EODD,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) != X0 ) )
& ( ? [X2] :
( mem(X2,ty_2Enum_2Enum)
& ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X2)) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(rectify,[],[f231]) ).
fof(f233,plain,
! [X0] :
( ( ( p(ap(c_2Earithmetic_2EODD,X0))
| ! [X1] :
( ~ mem(X1,ty_2Enum_2Enum)
| ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),X1)) != X0 ) )
& ( ( mem(sK21(X0),ty_2Enum_2Enum)
& ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),sK21(X0))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,X0)) ) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X2,sK21(X0))],[f232]) ).
fof(f334,plain,
! [X0] :
( ! [X1] :
( ( ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Enum_2ESUC,X1)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
& ( p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Enum_2ESUC,X1))) ) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(nnf_transformation,[],[f196]) ).
fof(f335,plain,
mem(sK18,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f222]) ).
fof(f336,plain,
ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,sK18)),c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),
inference(cnf_transformation,[],[f222]) ).
fof(f342,plain,
! [X0,X1] :
( ~ mem(X1,bool)
| p(X1)
| p(X0)
| X0 = X1
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f225]) ).
fof(f343,plain,
! [X0,X1] :
( ~ mem(X1,bool)
| ~ p(X1)
| ~ p(X0)
| X0 = X1
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f225]) ).
fof(f344,plain,
ne(ty_2Enum_2Enum),
inference(cnf_transformation,[],[f9]) ).
fof(f345,plain,
! [X0] :
( ap(c_2Enum_2ESUC,X0) = ap(ap(c_2Earithmetic_2E_2B,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f130]) ).
fof(f346,plain,
ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),
inference(cnf_transformation,[],[f42]) ).
fof(f347,plain,
ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,c_2Enum_2E0),
inference(cnf_transformation,[],[f41]) ).
fof(f348,plain,
mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f10]) ).
fof(f349,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),sK20(X0)) = X0
| ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f228]) ).
fof(f350,plain,
! [X0] :
( ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| mem(sK20(X0),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f228]) ).
fof(f355,plain,
! [X0] :
( p(ap(c_2Earithmetic_2EODD,X0))
| p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f230]) ).
fof(f356,plain,
mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool)),
inference(cnf_transformation,[],[f11]) ).
fof(f357,plain,
! [X0] :
( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),sK21(X0))) = X0
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f233]) ).
fof(f358,plain,
! [X0] :
( ~ p(ap(c_2Earithmetic_2EODD,X0))
| mem(sK21(X0),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f233]) ).
fof(f360,plain,
mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f12]) ).
fof(f361,plain,
mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f13]) ).
fof(f362,plain,
mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f14]) ).
fof(f363,plain,
! [X2,X3,X0,X1] :
( ap(ap(c_2Earithmetic_2EMOD,X1),X0) = X2
| ~ mem(X3,ty_2Enum_2Enum)
| ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2) != X1
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X2),X0))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f136]) ).
fof(f373,plain,
! [X2,X0,X1] :
( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X1),X2) = X2
| ~ mem(X2,X0)
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f374,plain,
! [X2,X0,X1] :
( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1
| ~ mem(X2,X0)
| ~ mem(X1,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f376,plain,
! [X0] :
( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Enum_2ESUC,X0)))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f142]) ).
fof(f377,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2E_2B,X0),c_2Enum_2E0) = X0
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f143]) ).
fof(f378,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f25]) ).
fof(f446,plain,
! [X2,X3,X0,X1] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f155]) ).
fof(f618,plain,
! [X0,X1] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Enum_2ESUC,X1)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f334]) ).
fof(f620,plain,
! [X0,X1] :
( ap(ap(c_2Earithmetic_2E_2A,X0),X1) = ap(ap(c_2Earithmetic_2E_2A,X1),X0)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f197]) ).
fof(f621,plain,
mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))),
inference(cnf_transformation,[],[f17]) ).
fof(f624,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f20]) ).
fof(f625,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f19]) ).
fof(f626,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f28]) ).
fof(f627,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f27]) ).
fof(f632,plain,
! [X2,X3,X0] :
( ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2)),X0) = X2
| ~ mem(X3,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X2),X0))
| ~ mem(X2,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,X3),X0)),X2),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(equality_resolution,[],[f363]) ).
fof(f705,plain,
ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) = ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,c_2Enum_2E0)),
inference(forward_demodulation,[],[f346,f347]) ).
fof(f706,plain,
! [X0] :
( ap(c_2Enum_2ESUC,X0) = ap(ap(c_2Earithmetic_2E_2B,X0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(forward_demodulation,[],[f345,f347]) ).
fof(f707,plain,
ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,sK18)),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0)),
inference(forward_demodulation,[],[f336,f347]) ).
fof(f711,plain,
! [X0,X1] :
( mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),X0)
| ~ mem(ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO),X1)
| ~ mem(c_2Earithmetic_2ENUMERAL,arr(X1,X0)) ),
inference(superposition,[],[f446,f347]) ).
fof(f712,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2E_2A,sK20(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = X0
| ~ mem(sK20(X0),ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(superposition,[],[f620,f349]) ).
fof(f721,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2E_2A,sK20(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = X0
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(forward_subsumption_resolution,[],[f712,f350]) ).
fof(f723,definition,
( spl43_15
<=> mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl43_15])],[avatar_definition]) ).
fof(f724,plain,
( mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ spl43_15 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f725,plain,
( ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| spl43_15 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f727,definition,
( spl43_16
<=> ! [X0] :
( ap(ap(c_2Earithmetic_2E_2A,sK20(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = X0
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl43_16])],[avatar_definition]) ).
fof(f728,plain,
( ! [X0] :
( ap(ap(c_2Earithmetic_2E_2A,sK20(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) = X0
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) )
| ~ spl43_16 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f732,plain,
( ~ spl43_15
| spl43_16 ),
inference(avatar_split_clause,[],[f721,f727,f723]) ).
fof(f733,plain,
( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum) ),
inference(superposition,[],[f376,f705]) ).
fof(f735,definition,
( spl43_17
<=> mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl43_17])],[avatar_definition]) ).
fof(f736,plain,
( mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ spl43_17 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f737,plain,
( ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| spl43_17 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f739,definition,
( spl43_18
<=> p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ),
introduced(definition,[new_symbols(definition,[spl43_18])],[avatar_definition]) ).
fof(f742,plain,
( ~ spl43_17
| spl43_18 ),
inference(avatar_split_clause,[],[f733,f739,f735]) ).
fof(f789,plain,
( ! [X0] :
( ~ mem(c_2Earithmetic_2ENUMERAL,arr(X0,ty_2Enum_2Enum))
| ~ mem(ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO),X0) )
| spl43_15 ),
inference(resolution,[],[f725,f446]) ).
fof(f851,plain,
! [X0] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X0),ap(c_2Enum_2ESUC,c_2Enum_2E0)))
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(superposition,[],[f618,f705]) ).
fof(f853,plain,
( ~ mem(ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO),ty_2Enum_2Enum)
| spl43_15 ),
inference(resolution,[],[f789,f362]) ).
fof(f854,plain,
( ! [X0] :
( ~ mem(c_2Earithmetic_2EBIT2,arr(X0,ty_2Enum_2Enum))
| ~ mem(c_2Earithmetic_2EZERO,X0) )
| spl43_15 ),
inference(resolution,[],[f853,f446]) ).
fof(f855,plain,
( ~ mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)
| spl43_15 ),
inference(resolution,[],[f854,f361]) ).
fof(f856,plain,
( $false
| spl43_15 ),
inference(forward_subsumption_resolution,[],[f855,f360]) ).
fof(f857,plain,
spl43_15,
inference(avatar_contradiction_clause,[],[f856]) ).
fof(f883,plain,
! [X0,X1] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,X0),X1))),X1)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),X1))
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,X0),X1)),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum) ),
inference(superposition,[],[f632,f706]) ).
fof(f884,plain,
! [X0,X1] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,X0),X1)),X1)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),X1))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum) ),
inference(superposition,[],[f632,f377]) ).
fof(f891,plain,
! [X0,X1] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,X0),X1)),X1)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),X1))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(duplicate_literal_removal,[],[f884]) ).
fof(f894,plain,
! [X0,X1] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,X0),X1)),X1)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),X1))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum) ),
inference(forward_subsumption_resolution,[],[f891,f378]) ).
fof(f902,plain,
( ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(sK20(X0),ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) )
| ~ spl43_16 ),
inference(superposition,[],[f894,f728]) ).
fof(f911,plain,
( ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(sK20(X0),ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) )
| ~ spl43_16 ),
inference(duplicate_literal_removal,[],[f902]) ).
fof(f915,plain,
( ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) )
| ~ spl43_16 ),
inference(forward_subsumption_resolution,[],[f911,f350]) ).
fof(f917,plain,
( ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X0)) )
| ~ spl43_15
| ~ spl43_16 ),
inference(forward_subsumption_resolution,[],[f915,f724]) ).
fof(f919,definition,
( spl43_19
<=> ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) ) ),
introduced(definition,[new_symbols(definition,[spl43_19])],[avatar_definition]) ).
fof(f920,plain,
( ! [X0] :
( c_2Enum_2E0 = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl43_19 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f921,plain,
( ~ spl43_18
| spl43_19
| ~ spl43_15
| ~ spl43_16 ),
inference(avatar_split_clause,[],[f917,f727,f723,f919,f739]) ).
fof(f966,plain,
! [X0] :
( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = X0
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(sK21(X0),ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum) ),
inference(superposition,[],[f357,f620]) ).
fof(f975,plain,
! [X0] :
( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = X0
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum) ),
inference(forward_subsumption_resolution,[],[f966,f358]) ).
fof(f977,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) = X0
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl43_15 ),
inference(forward_subsumption_resolution,[],[f975,f724]) ).
fof(f1034,plain,
( ! [X0] :
( ~ mem(c_2Earithmetic_2ENUMERAL,arr(X0,ty_2Enum_2Enum))
| ~ mem(ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO),X0) )
| spl43_17 ),
inference(resolution,[],[f711,f737]) ).
fof(f1035,plain,
( ~ mem(ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO),ty_2Enum_2Enum)
| spl43_17 ),
inference(resolution,[],[f1034,f362]) ).
fof(f1036,plain,
( ! [X0] :
( ~ mem(c_2Earithmetic_2EBIT1,arr(X0,ty_2Enum_2Enum))
| ~ mem(c_2Earithmetic_2EZERO,X0) )
| spl43_17 ),
inference(resolution,[],[f1035,f446]) ).
fof(f1037,plain,
( ~ mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)
| spl43_17 ),
inference(resolution,[],[f1036,f348]) ).
fof(f1038,plain,
( $false
| spl43_17 ),
inference(forward_subsumption_resolution,[],[f1037,f360]) ).
fof(f1039,plain,
spl43_17,
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1040,plain,
( ! [X0] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X0),ap(c_2Enum_2ESUC,c_2Enum_2E0)))
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl43_17 ),
inference(forward_subsumption_resolution,[],[f851,f736]) ).
fof(f1042,plain,
( ! [X0,X1] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,X0),X1))),X1)
| ~ mem(X0,ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),X1))
| ~ mem(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,X0),X1)),ty_2Enum_2Enum)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,X0),X1),ty_2Enum_2Enum) )
| ~ spl43_17 ),
inference(forward_subsumption_resolution,[],[f883,f736]) ).
fof(f1090,plain,
! [X2,X3,X0,X1] :
( ~ mem(X0,arr(X3,bool))
| ~ p(X2)
| ap(X0,X1) = X2
| ~ mem(X2,bool)
| ~ mem(X1,X3)
| ~ p(ap(X0,X1)) ),
inference(resolution,[],[f343,f446]) ).
fof(f1264,plain,
! [X0] :
( p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum)
| mem(sK21(X0),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(resolution,[],[f355,f358]) ).
fof(f1268,plain,
! [X0] :
( p(ap(c_2Earithmetic_2EEVEN,X0))
| ~ mem(X0,ty_2Enum_2Enum)
| mem(sK21(X0),ty_2Enum_2Enum) ),
inference(duplicate_literal_removal,[],[f1264]) ).
fof(f1847,definition,
( spl43_44
<=> p(ap(c_2Earithmetic_2EEVEN,sK18)) ),
introduced(definition,[new_symbols(definition,[spl43_44])],[avatar_definition]) ).
fof(f1848,plain,
( ~ p(ap(c_2Earithmetic_2EEVEN,sK18))
| spl43_44 ),
inference(avatar_component_clause,[],[f1847]) ).
fof(f1849,plain,
( p(ap(c_2Earithmetic_2EEVEN,sK18))
| ~ spl43_44 ),
inference(avatar_component_clause,[],[f1847]) ).
fof(f1964,plain,
! [X0] :
( p(c_2Ebool_2EF)
| p(X0)
| c_2Ebool_2EF = X0
| ~ mem(X0,bool) ),
inference(resolution,[],[f627,f342]) ).
fof(f1966,plain,
! [X0] :
( ~ mem(X0,bool)
| c_2Ebool_2EF = X0
| p(X0) ),
inference(forward_subsumption_resolution,[],[f1964,f626]) ).
fof(f1969,plain,
! [X2,X0,X1] :
( ~ mem(X0,arr(X2,bool))
| p(ap(X0,X1))
| ~ mem(X1,X2)
| c_2Ebool_2EF = ap(X0,X1) ),
inference(resolution,[],[f1966,f446]) ).
fof(f1997,plain,
! [X0] :
( c_2Ebool_2EF = ap(c_2Earithmetic_2EEVEN,X0)
| ~ mem(X0,ty_2Enum_2Enum)
| p(ap(c_2Earithmetic_2EEVEN,X0)) ),
inference(resolution,[],[f1969,f356]) ).
fof(f2010,plain,
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),c_2Ebool_2EF),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| ~ mem(sK18,ty_2Enum_2Enum)
| p(ap(c_2Earithmetic_2EEVEN,sK18)) ),
inference(superposition,[],[f707,f1997]) ).
fof(f2092,plain,
! [X0,X1] :
( ap(c_2Earithmetic_2EEVEN,X1) = X0
| ~ p(X0)
| ~ mem(X0,bool)
| ~ mem(X1,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,X1)) ),
inference(resolution,[],[f1090,f356]) ).
fof(f2110,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| ~ p(X0)
| ~ mem(X0,bool)
| ~ mem(sK18,ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EEVEN,sK18)) ),
inference(superposition,[],[f707,f2092]) ).
fof(f2154,plain,
! [X0] :
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| ~ p(X0)
| ~ mem(X0,bool)
| ~ p(ap(c_2Earithmetic_2EEVEN,sK18)) ),
inference(forward_subsumption_resolution,[],[f2110,f335]) ).
fof(f2155,plain,
( ! [X0] :
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| ~ p(X0)
| ~ mem(X0,bool) )
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2154,f1849]) ).
fof(f2157,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(c_2Ebool_2ET)
| ~ mem(c_2Ebool_2ET,bool)
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_44 ),
inference(superposition,[],[f2155,f374]) ).
fof(f2159,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(c_2Ebool_2ET,bool)
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2157,f624]) ).
fof(f2160,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2159,f625]) ).
fof(f2161,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_17
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2160,f736]) ).
fof(f2162,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_17
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2161,f378]) ).
fof(f2163,plain,
( c_2Enum_2E0 != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ spl43_17
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2162,f344]) ).
fof(f2164,plain,
( c_2Enum_2E0 != c_2Enum_2E0
| ~ p(ap(c_2Earithmetic_2EEVEN,sK18))
| ~ mem(sK18,ty_2Enum_2Enum)
| ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(superposition,[],[f2163,f920]) ).
fof(f2165,plain,
( ~ p(ap(c_2Earithmetic_2EEVEN,sK18))
| ~ mem(sK18,ty_2Enum_2Enum)
| ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(trivial_inequality_removal,[],[f2164]) ).
fof(f2166,plain,
( ~ mem(sK18,ty_2Enum_2Enum)
| ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2165,f1849]) ).
fof(f2167,plain,
( $false
| ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(forward_subsumption_resolution,[],[f2166,f335]) ).
fof(f2168,plain,
( ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(avatar_contradiction_clause,[],[f2167]) ).
fof(f2169,plain,
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),c_2Ebool_2EF),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| p(ap(c_2Earithmetic_2EEVEN,sK18)) ),
inference(forward_subsumption_resolution,[],[f2010,f335]) ).
fof(f2170,plain,
( ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))) != ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),c_2Ebool_2EF),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))
| spl43_44 ),
inference(forward_subsumption_resolution,[],[f2169,f1848]) ).
fof(f2171,plain,
( ap(c_2Enum_2ESUC,c_2Enum_2E0) != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| spl43_44 ),
inference(superposition,[],[f2170,f373]) ).
fof(f2172,plain,
( ap(c_2Enum_2ESUC,c_2Enum_2E0) != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_17
| spl43_44 ),
inference(forward_subsumption_resolution,[],[f2171,f736]) ).
fof(f2173,plain,
( ap(c_2Enum_2ESUC,c_2Enum_2E0) != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ ne(ty_2Enum_2Enum)
| ~ spl43_17
| spl43_44 ),
inference(forward_subsumption_resolution,[],[f2172,f378]) ).
fof(f2174,plain,
( ap(c_2Enum_2ESUC,c_2Enum_2E0) != ap(ap(c_2Earithmetic_2EMOD,sK18),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ spl43_17
| spl43_44 ),
inference(forward_subsumption_resolution,[],[f2173,f344]) ).
fof(f2175,plain,
( ~ mem(sK18,ty_2Enum_2Enum)
| mem(sK21(sK18),ty_2Enum_2Enum)
| spl43_44 ),
inference(resolution,[],[f1848,f1268]) ).
fof(f2180,plain,
( mem(sK21(sK18),ty_2Enum_2Enum)
| spl43_44 ),
inference(forward_subsumption_resolution,[],[f2175,f335]) ).
fof(f2797,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(sK21(X0),ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl43_15
| ~ spl43_17 ),
inference(superposition,[],[f1042,f977]) ).
fof(f2812,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ mem(sK21(X0),ty_2Enum_2Enum)
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EODD,X0)) )
| ~ spl43_15
| ~ spl43_17 ),
inference(duplicate_literal_removal,[],[f2797]) ).
fof(f2820,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EODD,X0)) )
| ~ spl43_15
| ~ spl43_17 ),
inference(forward_subsumption_resolution,[],[f2812,f358]) ).
fof(f2824,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| ~ mem(X0,ty_2Enum_2Enum)
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ p(ap(c_2Earithmetic_2EODD,X0)) )
| ~ spl43_15
| ~ spl43_17 ),
inference(forward_subsumption_resolution,[],[f2820,f724]) ).
fof(f2828,definition,
( spl43_52
<=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))) ),
introduced(definition,[new_symbols(definition,[spl43_52])],[avatar_definition]) ).
fof(f2830,plain,
( ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))))
| spl43_52 ),
inference(avatar_component_clause,[],[f2828]) ).
fof(f2832,definition,
( spl43_53
<=> ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ) ),
introduced(definition,[new_symbols(definition,[spl43_53])],[avatar_definition]) ).
fof(f2833,plain,
( ! [X0] :
( ap(c_2Enum_2ESUC,c_2Enum_2E0) = ap(ap(c_2Earithmetic_2EMOD,X0),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)))
| ~ p(ap(c_2Earithmetic_2EODD,X0))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) )
| ~ spl43_53 ),
inference(avatar_component_clause,[],[f2832]) ).
fof(f2834,plain,
( ~ spl43_52
| spl43_53
| ~ spl43_15
| ~ spl43_17 ),
inference(avatar_split_clause,[],[f2824,f735,f723,f2832,f2828]) ).
fof(f2839,plain,
( ~ p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0)))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl43_17
| spl43_52 ),
inference(resolution,[],[f2830,f1040]) ).
fof(f2840,plain,
( ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl43_17
| spl43_52 ),
inference(forward_subsumption_resolution,[],[f2839,f376]) ).
fof(f2841,plain,
( $false
| ~ spl43_17
| spl43_52 ),
inference(forward_subsumption_resolution,[],[f2840,f378]) ).
fof(f2842,plain,
( ~ spl43_17
| spl43_52 ),
inference(avatar_contradiction_clause,[],[f2841]) ).
fof(f2868,plain,
( ap(c_2Enum_2ESUC,c_2Enum_2E0) != ap(c_2Enum_2ESUC,c_2Enum_2E0)
| ~ p(ap(c_2Earithmetic_2EODD,sK18))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(sK18)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ mem(sK18,ty_2Enum_2Enum)
| ~ spl43_17
| spl43_44
| ~ spl43_53 ),
inference(superposition,[],[f2174,f2833]) ).
fof(f2884,plain,
( ~ p(ap(c_2Earithmetic_2EODD,sK18))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(sK18)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ mem(sK18,ty_2Enum_2Enum)
| ~ spl43_17
| spl43_44
| ~ spl43_53 ),
inference(trivial_inequality_removal,[],[f2868]) ).
fof(f2895,plain,
( ~ p(ap(c_2Earithmetic_2EODD,sK18))
| ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(sK18)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| ~ spl43_17
| spl43_44
| ~ spl43_53 ),
inference(forward_subsumption_resolution,[],[f2884,f335]) ).
fof(f2903,definition,
( spl43_55
<=> mem(ap(ap(c_2Earithmetic_2E_2A,sK21(sK18)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl43_55])],[avatar_definition]) ).
fof(f2905,plain,
( ~ mem(ap(ap(c_2Earithmetic_2E_2A,sK21(sK18)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO))),ty_2Enum_2Enum)
| spl43_55 ),
inference(avatar_component_clause,[],[f2903]) ).
fof(f2907,definition,
( spl43_56
<=> p(ap(c_2Earithmetic_2EODD,sK18)) ),
introduced(definition,[new_symbols(definition,[spl43_56])],[avatar_definition]) ).
fof(f2909,plain,
( ~ p(ap(c_2Earithmetic_2EODD,sK18))
| spl43_56 ),
inference(avatar_component_clause,[],[f2907]) ).
fof(f2910,plain,
( ~ spl43_55
| ~ spl43_56
| ~ spl43_17
| spl43_44
| ~ spl43_53 ),
inference(avatar_split_clause,[],[f2895,f2832,f1847,f735,f2907,f2903]) ).
fof(f3840,plain,
( p(ap(c_2Earithmetic_2EEVEN,sK18))
| ~ mem(sK18,ty_2Enum_2Enum)
| spl43_56 ),
inference(resolution,[],[f2909,f355]) ).
fof(f3850,plain,
( ~ mem(sK18,ty_2Enum_2Enum)
| spl43_44
| spl43_56 ),
inference(forward_subsumption_resolution,[],[f3840,f1848]) ).
fof(f3854,plain,
( $false
| spl43_44
| spl43_56 ),
inference(forward_subsumption_resolution,[],[f3850,f335]) ).
fof(f3855,plain,
( spl43_44
| spl43_56 ),
inference(avatar_contradiction_clause,[],[f3854]) ).
fof(f3857,plain,
( ! [X0] :
( ~ mem(ap(c_2Earithmetic_2E_2A,sK21(sK18)),arr(X0,ty_2Enum_2Enum))
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),X0) )
| spl43_55 ),
inference(resolution,[],[f2905,f446]) ).
fof(f3860,plain,
( ! [X0,X1] :
( ~ mem(c_2Earithmetic_2E_2A,arr(X1,arr(X0,ty_2Enum_2Enum)))
| ~ mem(sK21(sK18),X1)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),X0) )
| spl43_55 ),
inference(resolution,[],[f3857,f446]) ).
fof(f3954,plain,
( ~ mem(sK21(sK18),ty_2Enum_2Enum)
| ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| spl43_55 ),
inference(resolution,[],[f3860,f621]) ).
fof(f3955,plain,
( ~ mem(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)),ty_2Enum_2Enum)
| spl43_44
| spl43_55 ),
inference(forward_subsumption_resolution,[],[f3954,f2180]) ).
fof(f3956,plain,
( $false
| ~ spl43_15
| spl43_44
| spl43_55 ),
inference(forward_subsumption_resolution,[],[f3955,f724]) ).
fof(f3957,plain,
( ~ spl43_15
| spl43_44
| spl43_55 ),
inference(avatar_contradiction_clause,[],[f3956]) ).
cnf(s16,plain,
( ~ spl43_15
| spl43_16 ),
inference(sat_conversion,[],[f732]) ).
cnf(s17,plain,
( ~ spl43_17
| spl43_18 ),
inference(sat_conversion,[],[f742]) ).
cnf(s18,plain,
spl43_15,
inference(sat_conversion,[],[f857]) ).
cnf(s19,plain,
( ~ spl43_15
| ~ spl43_16
| ~ spl43_18
| spl43_19 ),
inference(sat_conversion,[],[f921]) ).
cnf(s20,plain,
spl43_17,
inference(sat_conversion,[],[f1039]) ).
cnf(s43,plain,
( ~ spl43_17
| ~ spl43_19
| ~ spl43_44 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s49,plain,
( ~ spl43_15
| ~ spl43_17
| ~ spl43_52
| spl43_53 ),
inference(sat_conversion,[],[f2834]) ).
cnf(s51,plain,
( ~ spl43_17
| spl43_52 ),
inference(sat_conversion,[],[f2842]) ).
cnf(s52,plain,
( ~ spl43_17
| spl43_44
| ~ spl43_53
| ~ spl43_55
| ~ spl43_56 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s62,plain,
( spl43_44
| spl43_56 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s63,plain,
( ~ spl43_15
| spl43_44
| spl43_55 ),
inference(sat_conversion,[],[f3957]) ).
cnf(s66,plain,
spl43_52,
inference(rat,[],[s51,s20]) ).
cnf(s69,plain,
spl43_53,
inference(rat,[],[s49,s20,s66,s18]) ).
cnf(s71,plain,
spl43_18,
inference(rat,[],[s17,s20]) ).
cnf(s72,plain,
spl43_16,
inference(rat,[],[s16,s18]) ).
cnf(s74,plain,
spl43_19,
inference(rat,[],[s19,s71,s18,s72]) ).
cnf(s75,plain,
~ spl43_44,
inference(rat,[],[s43,s20,s74]) ).
cnf(s76,plain,
spl43_55,
inference(rat,[],[s63,s18,s75]) ).
cnf(s77,plain,
spl43_56,
inference(rat,[],[s62,s75]) ).
cnf(s78,plain,
$false,
inference(rat,[],[s52,s77,s69,s20,s76,s75]) ).
fof(f3958,plain,
$false,
inference(avatar_sat_refutation,[],[s78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP003+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n026.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 11:51:26 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.45/2.35 % (2705593)Detected formulas, will run a generic FOF schedule.
% 10.45/2.35 % (2705601)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4286570169:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.45/2.35 % (2705601)Refutation not found, incomplete strategy
% 10.45/2.35 % (2705601)------------------------------
% 10.45/2.35 % (2705601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.35 % (2705601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.35 % (2705601)CaDiCaL version: 2.1.3
% 10.45/2.35 % (2705601)Termination reason: Refutation not found, incomplete strategy
% 10.45/2.35 % (2705601)Time elapsed: 0.002 s
% 10.45/2.35 % (2705601)Peak memory usage: 88 MB
% 10.45/2.35 % (2705601)Instructions burned: 4 (million)
% 10.45/2.35 % (2705599)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=2674872252:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.45/2.35 % (2705603)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2485371021:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.45/2.35 % (2705598)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=3649657395:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.45/2.35 % (2705602)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3751094426:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.45/2.35 % (2705604)dis-21_1_sil=8000:lcm=predicate:random_seed=2020286405:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.45/2.35 % (2705600)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=3063502878:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.45/2.35 % (2705604)Instruction limit reached!
% 10.45/2.35 % (2705604)------------------------------
% 10.45/2.35 % (2705604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.35 % (2705602)Instruction limit reached!
% 10.45/2.35 % (2705602)------------------------------
% 10.45/2.35 % (2705602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.35 % (2705602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.35 % (2705604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.35 % (2705602)CaDiCaL version: 2.1.3
% 10.45/2.35 % (2705604)CaDiCaL version: 2.1.3
% 10.45/2.35 % (2705602)Termination reason: Instruction limit
% 10.45/2.35 % (2705602)Termination phase: Saturation
% 10.45/2.35 % (2705602)Time elapsed: 0.069 s
% 10.45/2.35 % (2705604)Termination reason: Instruction limit
% 10.45/2.35 % (2705604)Termination phase: Saturation
% 10.45/2.35 % (2705602)Peak memory usage: 88 MB
% 10.45/2.35 % (2705604)Time elapsed: 0.069 s
% 10.45/2.35 % (2705602)Instructions burned: 121 (million)
% 10.45/2.35 % (2705604)Peak memory usage: 90 MB
% 10.45/2.35 % (2705604)Instructions burned: 131 (million)
% 10.45/2.35 % (2705603)Instruction limit reached!
% 10.45/2.35 % (2705603)------------------------------
% 10.45/2.35 % (2705603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.35 % (2705603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.35 % (2705603)CaDiCaL version: 2.1.3
% 10.45/2.35 % (2705603)Termination reason: Instruction limit
% 10.45/2.35 % (2705603)Termination phase: Saturation
% 10.45/2.35 % (2705603)Time elapsed: 0.097 s
% 10.45/2.35 % (2705603)Peak memory usage: 90 MB
% 10.45/2.35 % (2705603)Instructions burned: 140 (million)
% 10.45/2.35 % (2705601)------------------------------
% 10.45/2.35 % (2705601)------------------------------
% 10.45/2.35 % (2705612)lrs+10_1_sil=8000:sp=occurrence:random_seed=4038524466:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.45/2.35 % (2705615)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=998699085:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.45/2.35 % (2705613)lrs+10_1_sil=32000:urr=on:br=off:random_seed=985427982:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.45/2.35 % (2705614)lrs+1011_1_sil=32000:sp=occurrence:random_seed=636964122:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.14/3.44 % (2705613)Refutation not found, incomplete strategy
% 18.14/3.44 % (2705613)------------------------------
% 18.14/3.44 % (2705613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705613)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705613)Termination reason: Refutation not found, incomplete strategy
% 18.14/3.44 % (2705613)Time elapsed: 0.008 s
% 18.14/3.44 % (2705613)Peak memory usage: 89 MB
% 18.14/3.44 % (2705613)Instructions burned: 13 (million)
% 18.14/3.44 % (2705615)Instruction limit reached!
% 18.14/3.44 % (2705615)------------------------------
% 18.14/3.44 % (2705615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705615)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705615)Termination reason: Instruction limit
% 18.14/3.44 % (2705615)Termination phase: Saturation
% 18.14/3.44 % (2705615)Time elapsed: 0.064 s
% 18.14/3.44 % (2705615)Peak memory usage: 93 MB
% 18.14/3.44 % (2705615)Instructions burned: 252 (million)
% 18.14/3.44 % (2705620)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3138817210:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.14/3.44 % (2705612)Instruction limit reached!
% 18.14/3.44 % (2705612)------------------------------
% 18.14/3.44 % (2705612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705612)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705612)Termination reason: Instruction limit
% 18.14/3.44 % (2705612)Termination phase: Saturation
% 18.14/3.44 % (2705612)Time elapsed: 0.170 s
% 18.14/3.44 % (2705612)Peak memory usage: 92 MB
% 18.14/3.44 % (2705612)Instructions burned: 286 (million)
% 18.14/3.44 % (2705620)Refutation not found, incomplete strategy
% 18.14/3.44 % (2705620)------------------------------
% 18.14/3.44 % (2705620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705620)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705620)Termination reason: Refutation not found, incomplete strategy
% 18.14/3.44 % (2705620)Time elapsed: 0.004 s
% 18.14/3.44 % (2705620)Peak memory usage: 89 MB
% 18.14/3.44 % (2705620)Instructions burned: 12 (million)
% 18.14/3.44 % (2705614)Instruction limit reached!
% 18.14/3.44 % (2705614)------------------------------
% 18.14/3.44 % (2705614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705614)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705614)Termination reason: Instruction limit
% 18.14/3.44 % (2705614)Termination phase: Saturation
% 18.14/3.44 % (2705614)Time elapsed: 0.195 s
% 18.14/3.44 % (2705614)Peak memory usage: 92 MB
% 18.14/3.44 % (2705614)Instructions burned: 326 (million)
% 18.14/3.44 % (2705613)------------------------------
% 18.14/3.44 % (2705613)------------------------------
% 18.14/3.44 % (2705622)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3396943118:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.14/3.44 % (2705620)------------------------------
% 18.14/3.44 % (2705620)------------------------------
% 18.14/3.44 % (2705623)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4241722070:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.14/3.44 % (2705626)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4161751738:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 18.14/3.44 % (2705624)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4096839025:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 18.14/3.44 % (2705623)Instruction limit reached!
% 18.14/3.44 % (2705623)------------------------------
% 18.14/3.44 % (2705623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705623)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705623)Termination reason: Instruction limit
% 18.14/3.44 % (2705623)Termination phase: Saturation
% 18.14/3.44 % (2705623)Time elapsed: 0.069 s
% 18.14/3.44 % (2705623)Peak memory usage: 90 MB
% 18.14/3.44 % (2705623)Instructions burned: 113 (million)
% 18.14/3.44 % (2705626)Instruction limit reached!
% 18.14/3.44 % (2705626)------------------------------
% 18.14/3.44 % (2705626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705626)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705626)Termination reason: Instruction limit
% 18.14/3.44 % (2705626)Termination phase: Saturation
% 18.14/3.44 % (2705626)Time elapsed: 0.032 s
% 18.14/3.44 % (2705626)Peak memory usage: 89 MB
% 18.14/3.44 % (2705626)Instructions burned: 117 (million)
% 18.14/3.44 % (2705624)Instruction limit reached!
% 18.14/3.44 % (2705624)------------------------------
% 18.14/3.44 % (2705624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705624)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705624)Termination reason: Instruction limit
% 18.14/3.44 % (2705624)Termination phase: Saturation
% 18.14/3.44 % (2705624)Time elapsed: 0.060 s
% 18.14/3.44 % (2705624)Peak memory usage: 88 MB
% 18.14/3.44 % (2705624)Instructions burned: 127 (million)
% 18.14/3.44 % (2705631)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2860075659:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 18.14/3.44 % (2705631)Refutation not found, incomplete strategy
% 18.14/3.44 % (2705631)------------------------------
% 18.14/3.44 % (2705631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705631)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705631)Termination reason: Refutation not found, incomplete strategy
% 18.14/3.44 % (2705631)Time elapsed: 0.005 s
% 18.14/3.44 % (2705631)Peak memory usage: 89 MB
% 18.14/3.44 % (2705631)Instructions burned: 16 (million)
% 18.14/3.44 % (2705630)lrs+10_1_sil=8000:sp=occurrence:random_seed=1477752080:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 18.14/3.44 % (2705632)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2623947098:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 18.14/3.44 % (2705631)------------------------------
% 18.14/3.44 % (2705631)------------------------------
% 18.14/3.44 % (2705636)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=131527108:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 18.14/3.44 % (2705636)Instruction limit reached!
% 18.14/3.44 % (2705636)------------------------------
% 18.14/3.44 % (2705636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705636)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705636)Termination reason: Instruction limit
% 18.14/3.44 % (2705636)Termination phase: Saturation
% 18.14/3.44 % (2705636)Time elapsed: 0.035 s
% 18.14/3.44 % (2705636)Peak memory usage: 91 MB
% 18.14/3.44 % (2705636)Instructions burned: 137 (million)
% 18.14/3.44 % (2705638)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=80799273:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 18.14/3.44 % (2705638)Instruction limit reached!
% 18.14/3.44 % (2705638)------------------------------
% 18.14/3.44 % (2705638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705638)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705638)Termination reason: Instruction limit
% 18.14/3.44 % (2705638)Termination phase: Saturation
% 18.14/3.44 % (2705638)Time elapsed: 0.153 s
% 18.14/3.44 % (2705638)Peak memory usage: 91 MB
% 18.14/3.44 % (2705638)Instructions burned: 594 (million)
% 18.14/3.44 % (2705630)Instruction limit reached!
% 18.14/3.44 % (2705630)------------------------------
% 18.14/3.44 % (2705630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705630)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705630)Termination reason: Instruction limit
% 18.14/3.44 % (2705630)Termination phase: Saturation
% 18.14/3.44 % (2705630)Time elapsed: 0.508 s
% 18.14/3.44 % (2705630)Peak memory usage: 99 MB
% 18.14/3.44 % (2705630)Instructions burned: 908 (million)
% 18.14/3.44 % (2705640)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=647920458:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 18.14/3.44 % (2705641)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=975748808:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 18.14/3.44 % (2705641)Instruction limit reached!
% 18.14/3.44 % (2705641)------------------------------
% 18.14/3.44 % (2705641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705641)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705641)Termination reason: Instruction limit
% 18.14/3.44 % (2705641)Termination phase: Saturation
% 18.14/3.44 % (2705641)Time elapsed: 0.064 s
% 18.14/3.44 % (2705641)Peak memory usage: 91 MB
% 18.14/3.44 % (2705641)Instructions burned: 126 (million)
% 18.14/3.44 % (2705644)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2523965922:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 18.14/3.44 % (2705644)Instruction limit reached!
% 18.14/3.44 % (2705644)------------------------------
% 18.14/3.44 % (2705644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705644)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705644)Termination reason: Instruction limit
% 18.14/3.44 % (2705644)Termination phase: Saturation
% 18.14/3.44 % (2705644)Time elapsed: 0.079 s
% 18.14/3.44 % (2705644)Peak memory usage: 91 MB
% 18.14/3.44 % (2705644)Instructions burned: 135 (million)
% 18.14/3.44 % (2705646)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3161553725:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 18.14/3.44 % (2705646)Instruction limit reached!
% 18.14/3.44 % (2705646)------------------------------
% 18.14/3.44 % (2705646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705646)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705646)Termination reason: Instruction limit
% 18.14/3.44 % (2705646)Termination phase: Saturation
% 18.14/3.44 % (2705646)Time elapsed: 0.072 s
% 18.14/3.44 % (2705646)Peak memory usage: 89 MB
% 18.14/3.44 % (2705646)Instructions burned: 143 (million)
% 18.14/3.44 % (2705622)Instruction limit reached!
% 18.14/3.44 % (2705622)------------------------------
% 18.14/3.44 % (2705622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705622)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705622)Termination reason: Instruction limit
% 18.14/3.44 % (2705622)Termination phase: Saturation
% 18.14/3.44 % (2705622)Time elapsed: 1.441 s
% 18.14/3.44 % (2705622)Peak memory usage: 143 MB
% 18.14/3.44 % (2705622)Instructions burned: 2352 (million)
% 18.14/3.44 % (2705648)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=727192851:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 18.14/3.44 % (2705649)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=1820860564:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 18.14/3.44 % (2705632)First to succeed.
% 18.14/3.44 % (2705632)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2705593"
% 18.14/3.44 % (2705648)Instruction limit reached!
% 18.14/3.44 % (2705648)------------------------------
% 18.14/3.44 % (2705648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.44 % (2705648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.44 % (2705648)CaDiCaL version: 2.1.3
% 18.14/3.44 % (2705648)Termination reason: Instruction limit
% 18.14/3.44 % (2705648)Termination phase: Saturation
% 18.14/3.44 % (2705648)Time elapsed: 0.240 s
% 18.14/3.44 % (2705648)Peak memory usage: 95 MB
% 18.14/3.44 % (2705648)Instructions burned: 432 (million)
% 18.14/3.44 % (2705653)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=2836149042:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 18.14/3.44 % (2705632)Refutation found. Thanks to Tanya!
% 18.14/3.44 % SZS status Theorem for theBenchmark
% 18.14/3.44 % SZS output start Proof for theBenchmark
% See solution above
% 18.74/3.63 % (2705632)------------------------------
% 18.74/3.63 % (2705632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.63 % (2705632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.63 % (2705632)CaDiCaL version: 2.1.3
% 18.74/3.63 % (2705632)Termination reason: Refutation
% 18.74/3.63 % (2705632)Time elapsed: 1.341 s
% 18.74/3.63 % (2705632)Peak memory usage: 140 MB
% 18.74/3.63 % (2705632)Instructions burned: 2122 (million)
% 18.74/3.63 % (2705632)------------------------------
% 18.74/3.63 % (2705632)------------------------------
% 18.74/3.63 % (2705593)Success in time 2.568 s
% 18.74/3.63 % Vampire exiting
%------------------------------------------------------------------------------