%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP015+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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:28:14 AM UTC 2026
% Result : Theorem 7.04s 2.00s
% Output : Refutation 8.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 27
% Syntax : Number of formulae : 138 ( 42 unt; 9 def)
% Number of atoms : 379 ( 84 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 407 ( 166 ~; 165 |; 31 &)
% ( 18 <=>; 25 =>; 0 <=; 2 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 17 con; 0-2 aty)
% Number of variables : 89 ( 0 sgn 88 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
ne(bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bool_ne) ).
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(f13,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
fof(f14,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
fof(f20,axiom,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__neg) ).
fof(f23,axiom,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__of__num) ).
fof(f24,axiom,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Einteger_2Eint__lt) ).
fof(f26,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ne(ty_2Efcp_2Ecart(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ne_ty_2Efcp_2Ecart) ).
fof(f37,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
fof(f38,axiom,
! [X0] :
( ne(X0)
=> mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ewords_2En2w) ).
fof(f49,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 ) )
& ! [X3] :
( mem(X3,X0)
=> ! [X4] :
( mem(X4,X0)
=> ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X3),X4) = X4 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2Ebool__case__thm) ).
fof(f50,axiom,
ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__NEG__0) ).
fof(f51,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
<=> ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0 ) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
<=> $false ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2EINT__LT__CALCULATE) ).
fof(f52,axiom,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger_2ENUM__OF__INT) ).
fof(f53,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( mem(X1,ty_2Einteger_2Eint)
=> ap(c_2Einteger__word_2Ei2w(X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X1))))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Einteger__word_2Ei2w__def) ).
fof(f56,axiom,
! [X0] :
( ne(X0)
=> ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X0),c_2Enum_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ewords_2EWORD__NEG__0) ).
fof(f57,conjecture,
! [X0] :
( ne(X0)
=> ap(c_2Einteger__word_2Ei2w(X0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X0),c_2Enum_2E0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Einteger__word_2Ei2w__0) ).
fof(f58,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ap(c_2Einteger__word_2Ei2w(X0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X0),c_2Enum_2E0) ),
inference(negated_conjecture,[status(cth)],[f57]) ).
fof(f61,plain,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
<=> ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0 ) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) ) ) ),
inference(true_and_false_elimination,[],[f51]) ).
fof(f62,plain,
! [X0] :
( mem(X0,ty_2Enum_2Enum)
=> ! [X1] :
( mem(X1,ty_2Enum_2Enum)
=> ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
<=> ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0 ) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) ) ) ),
inference(flattening,[],[f61]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f65,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(ennf_transformation,[],[f5]) ).
fof(f66,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(flattening,[],[f65]) ).
fof(f75,plain,
! [X0] :
( ! [X1] :
( ne(ty_2Efcp_2Ecart(X0,X1))
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f83,plain,
! [X0] :
( mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0)))
| ~ ne(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f95,plain,
! [X0] :
( ( ! [X1] :
( ! [X2] :
( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1
| ~ mem(X2,X0) )
| ~ mem(X1,X0) )
& ! [X3] :
( ! [X4] :
( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X3),X4) = X4
| ~ mem(X4,X0) )
| ~ mem(X3,X0) ) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1)))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X0),X1)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
<=> ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0 ) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f62]) ).
fof(f97,plain,
! [X0] :
( ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X0)) = X0
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f52]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ap(c_2Einteger__word_2Ei2w(X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X1))))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,X1)))
| ~ mem(X1,ty_2Einteger_2Eint) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f101,plain,
! [X0] :
( ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),c_2Enum_2E0)) = ap(c_2Ewords_2En2w(X0),c_2Enum_2E0)
| ~ ne(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f102,plain,
? [X0] :
( ap(c_2Ewords_2En2w(X0),c_2Enum_2E0) != ap(c_2Einteger__word_2Ei2w(X0),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
& ne(X0) ),
inference(ennf_transformation,[],[f58]) ).
fof(f103,plain,
! [X0] :
( ! [X1] :
( X0 = X1
| ( ( ~ p(X1)
| ~ p(X0) )
& ( p(X1)
| p(X0) ) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(nnf_transformation,[],[f66]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,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_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1))) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
| ( c_2Enum_2E0 = X0
& c_2Enum_2E0 = X1 ) )
& ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1))) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(nnf_transformation,[],[f96]) ).
fof(f122,plain,
! [X0] :
( ! [X1] :
( ( ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,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_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__of__num,X1))) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0)) )
& ( p(ap(ap(c_2Eprim__rec_2E_3C,X1),X0))
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) )
& ( p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
| ( c_2Enum_2E0 = X0
& c_2Enum_2E0 = X1 ) )
& ( X0 != c_2Enum_2E0
| X1 != c_2Enum_2E0
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1))) )
& ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,X0)),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X1)))) )
| ~ mem(X1,ty_2Enum_2Enum) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(flattening,[],[f121]) ).
fof(f124,plain,
( ap(c_2Ewords_2En2w(sK2),c_2Enum_2E0) != ap(c_2Einteger__word_2Ei2w(sK2),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
& ne(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f102]) ).
fof(f125,plain,
ne(bool),
inference(cnf_transformation,[],[f1]) ).
fof(f128,plain,
! [X2,X3,X0,X1] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f129,plain,
! [X0,X1] :
( ~ mem(X1,bool)
| p(X1)
| p(X0)
| X0 = X1
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f103]) ).
fof(f141,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f13]) ).
fof(f142,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f14]) ).
fof(f152,plain,
mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)),
inference(cnf_transformation,[],[f20]) ).
fof(f155,plain,
mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)),
inference(cnf_transformation,[],[f23]) ).
fof(f156,plain,
mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool))),
inference(cnf_transformation,[],[f24]) ).
fof(f158,plain,
! [X0,X1] :
( ne(ty_2Efcp_2Ecart(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f172,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f37]) ).
fof(f173,plain,
! [X0] :
( mem(c_2Ewords_2En2w(X0),arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,X0)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f203,plain,
! [X3,X0,X4] :
( ~ mem(X4,X0)
| ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X3),X4) = X4
| ~ mem(X3,X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f205,plain,
ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) = ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),
inference(cnf_transformation,[],[f50]) ).
fof(f207,plain,
! [X0,X1] :
( c_2Enum_2E0 != X0
| c_2Enum_2E0 != X1
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,X0))),ap(c_2Einteger_2Eint__of__num,X1)))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f122]) ).
fof(f214,plain,
! [X0] :
( ~ mem(X0,ty_2Enum_2Enum)
| ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,X0)) = X0 ),
inference(cnf_transformation,[],[f97]) ).
fof(f215,plain,
! [X0,X1] :
( ~ mem(X1,ty_2Einteger_2Eint)
| ap(c_2Einteger__word_2Ei2w(X0),X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,X1),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,X1))))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,X1)))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f219,plain,
! [X0] :
( ~ ne(X0)
| ap(c_2Ewords_2En2w(X0),c_2Enum_2E0) = ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),c_2Enum_2E0)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f220,plain,
ne(sK2),
inference(cnf_transformation,[],[f124]) ).
fof(f221,plain,
ap(c_2Ewords_2En2w(sK2),c_2Enum_2E0) != ap(c_2Einteger__word_2Ei2w(sK2),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)),
inference(cnf_transformation,[],[f124]) ).
fof(f233,plain,
! [X1] :
( c_2Enum_2E0 != X1
| ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,X1)))
| ~ mem(X1,ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
inference(equality_resolution,[],[f207]) ).
fof(f234,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
inference(equality_resolution,[],[f233]) ).
fof(f235,definition,
sF3 = c_2Ewords_2En2w(sK2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f236,plain,
c_2Ewords_2En2w(sK2) = sF3,
inference(reorient_equations,[],[f235]) ).
fof(f237,definition,
sF4 = ap(sF3,c_2Enum_2E0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f238,plain,
ap(sF3,c_2Enum_2E0) = sF4,
inference(reorient_equations,[],[f237]) ).
fof(f239,definition,
sF5 = c_2Einteger__word_2Ei2w(sK2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f240,plain,
c_2Einteger__word_2Ei2w(sK2) = sF5,
inference(reorient_equations,[],[f239]) ).
fof(f241,definition,
sF6 = ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f242,plain,
ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0) = sF6,
inference(reorient_equations,[],[f241]) ).
fof(f243,definition,
sF7 = ap(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f244,plain,
ap(sF5,sF6) = sF7,
inference(reorient_equations,[],[f243]) ).
fof(f245,plain,
sF4 != sF7,
inference(definition_folding,[],[f221,f244,f242,f240,f238,f236]) ).
fof(f246,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
inference(duplicate_literal_removal,[],[f234]) ).
fof(f267,definition,
( spl8_1
<=> mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f268,plain,
( mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl8_1 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl8_2
<=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f273,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0)))
| spl8_2 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f246,f271,f267]) ).
fof(f275,plain,
spl8_1,
inference(avatar_split_clause,[],[f172,f267]) ).
fof(f276,plain,
( ~ p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,sF6)),sF6))
| spl8_2 ),
inference(forward_demodulation,[],[f273,f242]) ).
fof(f277,plain,
ap(c_2Ewords_2En2w(sK2),c_2Enum_2E0) = ap(c_2Ewords_2Eword__2comp(sK2),ap(c_2Ewords_2En2w(sK2),c_2Enum_2E0)),
inference(resolution,[],[f219,f220]) ).
fof(f278,plain,
ap(sF3,c_2Enum_2E0) = ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,c_2Enum_2E0)),
inference(forward_demodulation,[],[f277,f236]) ).
fof(f279,plain,
sF4 = ap(c_2Ewords_2Eword__2comp(sK2),sF4),
inference(forward_demodulation,[],[f278,f238]) ).
fof(f283,plain,
sF6 = ap(c_2Einteger_2Eint__neg,sF6),
inference(superposition,[],[f205,f242]) ).
fof(f285,plain,
! [X0] :
( mem(ap(c_2Einteger_2Eint__of__num,X0),ty_2Einteger_2Eint)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(resolution,[],[f155,f128]) ).
fof(f287,plain,
( mem(sF3,arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,sK2)))
| ~ ne(sK2) ),
inference(superposition,[],[f173,f236]) ).
fof(f288,plain,
mem(sF3,arr(ty_2Enum_2Enum,ty_2Efcp_2Ecart(bool,sK2))),
inference(forward_subsumption_resolution,[],[f287,f220]) ).
fof(f289,plain,
! [X0] :
( mem(ap(sF3,X0),ty_2Efcp_2Ecart(bool,sK2))
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(resolution,[],[f288,f128]) ).
fof(f290,plain,
( mem(sF4,ty_2Efcp_2Ecart(bool,sK2))
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
inference(superposition,[],[f289,f238]) ).
fof(f291,plain,
( mem(sF4,ty_2Efcp_2Ecart(bool,sK2))
| ~ spl8_1 ),
inference(forward_subsumption_resolution,[],[f290,f268]) ).
fof(f300,definition,
( spl8_3
<=> mem(sF6,ty_2Einteger_2Eint) ),
introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition]) ).
fof(f301,plain,
( mem(sF6,ty_2Einteger_2Eint)
| ~ spl8_3 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f302,plain,
( ~ mem(sF6,ty_2Einteger_2Eint)
| spl8_3 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f309,plain,
( mem(sF6,ty_2Einteger_2Eint)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum) ),
inference(superposition,[],[f285,f242]) ).
fof(f310,plain,
( ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f309,f302]) ).
fof(f312,plain,
( $false
| ~ spl8_1
| spl8_3 ),
inference(forward_subsumption_resolution,[],[f310,f268]) ).
fof(f313,plain,
( ~ spl8_1
| spl8_3 ),
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f314,plain,
( ! [X0] :
( ap(c_2Einteger__word_2Ei2w(X0),sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,sF6),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__neg,sF6))))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,sF6)))
| ~ ne(X0) )
| ~ spl8_3 ),
inference(resolution,[],[f301,f215]) ).
fof(f315,plain,
( ! [X0] :
( ap(c_2Einteger__word_2Ei2w(X0),sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,sF6),ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,sF6)))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,sF6)))
| ~ ne(X0) )
| ~ spl8_3 ),
inference(forward_demodulation,[],[f314,f283]) ).
fof(f316,plain,
( ! [X0] :
( ~ ne(X0)
| ap(c_2Einteger__word_2Ei2w(X0),sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,X0)),ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)),ap(c_2Ewords_2Eword__2comp(X0),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,sF6)))),ap(c_2Ewords_2En2w(X0),ap(c_2Einteger_2ENum,sF6))) )
| ~ spl8_3 ),
inference(forward_demodulation,[],[f315,f242]) ).
fof(f322,plain,
( ap(c_2Einteger__word_2Ei2w(sK2),sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)),ap(c_2Ewords_2Eword__2comp(sK2),ap(c_2Ewords_2En2w(sK2),ap(c_2Einteger_2ENum,sF6)))),ap(c_2Ewords_2En2w(sK2),ap(c_2Einteger_2ENum,sF6)))
| ~ spl8_3 ),
inference(resolution,[],[f316,f220]) ).
fof(f323,plain,
( ap(c_2Einteger__word_2Ei2w(sK2),sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)),ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,ap(c_2Einteger_2ENum,sF6)))),ap(sF3,ap(c_2Einteger_2ENum,sF6)))
| ~ spl8_3 ),
inference(forward_demodulation,[],[f322,f236]) ).
fof(f324,plain,
( ap(sF5,sF6) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)),ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,ap(c_2Einteger_2ENum,sF6)))),ap(sF3,ap(c_2Einteger_2ENum,sF6)))
| ~ spl8_3 ),
inference(forward_demodulation,[],[f323,f240]) ).
fof(f325,plain,
( sF7 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)),ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,ap(c_2Einteger_2ENum,sF6)))),ap(sF3,ap(c_2Einteger_2ENum,sF6)))
| ~ spl8_3 ),
inference(forward_demodulation,[],[f324,f244]) ).
fof(f327,plain,
( c_2Enum_2E0 = ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,c_2Enum_2E0))
| ~ spl8_1 ),
inference(resolution,[],[f268,f214]) ).
fof(f328,plain,
( c_2Enum_2E0 = ap(c_2Einteger_2ENum,sF6)
| ~ spl8_1 ),
inference(forward_demodulation,[],[f327,f242]) ).
fof(f333,plain,
! [X0] :
( p(c_2Ebool_2EF)
| p(X0)
| c_2Ebool_2EF = X0
| ~ mem(X0,bool) ),
inference(resolution,[],[f141,f129]) ).
fof(f334,plain,
! [X0] :
( ~ mem(X0,bool)
| c_2Ebool_2EF = X0
| p(X0) ),
inference(forward_subsumption_resolution,[],[f333,f142]) ).
fof(f380,definition,
( spl8_5
<=> ne(ty_2Efcp_2Ecart(bool,sK2)) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f381,plain,
( ne(ty_2Efcp_2Ecart(bool,sK2))
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f382,plain,
( ~ ne(ty_2Efcp_2Ecart(bool,sK2))
| spl8_5 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f428,plain,
( ~ ne(sK2)
| ~ ne(bool)
| spl8_5 ),
inference(resolution,[],[f382,f158]) ).
fof(f429,plain,
( ~ ne(bool)
| spl8_5 ),
inference(forward_subsumption_resolution,[],[f428,f220]) ).
fof(f430,plain,
( $false
| spl8_5 ),
inference(forward_subsumption_resolution,[],[f429,f125]) ).
fof(f431,plain,
spl8_5,
inference(avatar_contradiction_clause,[],[f430]) ).
fof(f461,plain,
! [X0] :
( mem(ap(c_2Einteger_2Eint__neg,X0),ty_2Einteger_2Eint)
| ~ mem(X0,ty_2Einteger_2Eint) ),
inference(resolution,[],[f152,f128]) ).
fof(f494,plain,
( ! [X0] :
( sF4 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),X0),sF4)
| ~ mem(X0,ty_2Efcp_2Ecart(bool,sK2))
| ~ ne(ty_2Efcp_2Ecart(bool,sK2)) )
| ~ spl8_1 ),
inference(resolution,[],[f203,f291]) ).
fof(f501,plain,
( ! [X0] :
( ~ mem(X0,ty_2Efcp_2Ecart(bool,sK2))
| sF4 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),X0),sF4) )
| ~ spl8_1
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f494,f381]) ).
fof(f523,plain,
( sF4 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),sF4),sF4)
| ~ spl8_1
| ~ spl8_5 ),
inference(resolution,[],[f501,f291]) ).
fof(f598,plain,
! [X0] :
( mem(ap(c_2Einteger_2Eint__lt,X0),arr(ty_2Einteger_2Eint,bool))
| ~ mem(X0,ty_2Einteger_2Eint) ),
inference(resolution,[],[f156,f128]) ).
fof(f614,plain,
! [X0,X1] :
( mem(ap(ap(c_2Einteger_2Eint__lt,X0),X1),bool)
| ~ mem(X1,ty_2Einteger_2Eint)
| ~ mem(X0,ty_2Einteger_2Eint) ),
inference(resolution,[],[f598,f128]) ).
fof(f677,plain,
! [X0,X1] :
( p(ap(ap(c_2Einteger_2Eint__lt,X1),X0))
| ~ mem(X1,ty_2Einteger_2Eint)
| c_2Ebool_2EF = ap(ap(c_2Einteger_2Eint__lt,X1),X0)
| ~ mem(X0,ty_2Einteger_2Eint) ),
inference(resolution,[],[f614,f334]) ).
fof(f683,plain,
( ~ mem(ap(c_2Einteger_2Eint__neg,sF6),ty_2Einteger_2Eint)
| c_2Ebool_2EF = ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,sF6)),sF6)
| ~ mem(sF6,ty_2Einteger_2Eint)
| spl8_2 ),
inference(resolution,[],[f677,f276]) ).
fof(f684,plain,
( c_2Ebool_2EF = ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,sF6)),sF6)
| ~ mem(sF6,ty_2Einteger_2Eint)
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f683,f461]) ).
fof(f685,plain,
( c_2Ebool_2EF = ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,sF6)),sF6)
| spl8_2
| ~ spl8_3 ),
inference(forward_subsumption_resolution,[],[f684,f301]) ).
fof(f686,plain,
( c_2Ebool_2EF = ap(ap(c_2Einteger_2Eint__lt,sF6),sF6)
| spl8_2
| ~ spl8_3 ),
inference(forward_demodulation,[],[f685,f283]) ).
fof(f688,plain,
( sF7 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,ap(c_2Einteger_2ENum,sF6)))),ap(sF3,ap(c_2Einteger_2ENum,sF6)))
| spl8_2
| ~ spl8_3 ),
inference(superposition,[],[f325,f686]) ).
fof(f691,plain,
( sF7 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(sK2),ap(sF3,c_2Enum_2E0))),ap(sF3,c_2Enum_2E0))
| ~ spl8_1
| spl8_2
| ~ spl8_3 ),
inference(forward_demodulation,[],[f688,f328]) ).
fof(f693,plain,
( sF7 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),ap(c_2Ewords_2Eword__2comp(sK2),sF4)),sF4)
| ~ spl8_1
| spl8_2
| ~ spl8_3 ),
inference(forward_demodulation,[],[f691,f238]) ).
fof(f696,plain,
( sF7 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Efcp_2Ecart(bool,sK2)),c_2Ebool_2EF),sF4),sF4)
| ~ spl8_1
| spl8_2
| ~ spl8_3 ),
inference(forward_demodulation,[],[f693,f279]) ).
fof(f697,plain,
( sF4 = sF7
| ~ spl8_1
| spl8_2
| ~ spl8_3
| ~ spl8_5 ),
inference(forward_demodulation,[],[f696,f523]) ).
fof(f698,plain,
( $false
| ~ spl8_1
| spl8_2
| ~ spl8_3
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f697,f245]) ).
fof(f699,plain,
( ~ spl8_1
| spl8_2
| ~ spl8_3
| ~ spl8_5 ),
inference(avatar_contradiction_clause,[],[f698]) ).
cnf(s1,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f274]) ).
cnf(s2,plain,
spl8_1,
inference(sat_conversion,[],[f275]) ).
cnf(s4,plain,
( ~ spl8_1
| spl8_3 ),
inference(sat_conversion,[],[f313]) ).
cnf(s12,plain,
spl8_5,
inference(sat_conversion,[],[f431]) ).
cnf(s29,plain,
( ~ spl8_1
| spl8_2
| ~ spl8_3
| ~ spl8_5 ),
inference(sat_conversion,[],[f699]) ).
cnf(s42,plain,
spl8_3,
inference(rat,[],[s4,s2]) ).
cnf(s44,plain,
spl8_2,
inference(rat,[],[s29,s12,s2,s42]) ).
cnf(s46,plain,
$false,
inference(rat,[],[s1,s44,s2]) ).
fof(f700,plain,
$false,
inference(avatar_sat_refutation,[],[s46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP015+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 12:06:32 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 7.04/2.00 % (2512629)Detected formulas, will run a generic FOF schedule.
% 7.04/2.00 % (2512635)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=4139080442:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.04/2.00 % (2512636)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=3407874424:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.04/2.00 % (2512640)dis-21_1_sil=8000:lcm=predicate:random_seed=2403297272: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)
% 7.04/2.00 % (2512634)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=3530007747:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.04/2.00 % (2512638)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=966725006:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.04/2.00 % (2512639)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3069390354:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.04/2.00 % (2512637)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=688266547:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.04/2.00 % (2512637)Refutation not found, incomplete strategy
% 7.04/2.00 % (2512637)------------------------------
% 7.04/2.00 % (2512637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512637)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512637)Termination reason: Refutation not found, incomplete strategy
% 7.04/2.00 % (2512637)Time elapsed: 0.002 s
% 7.04/2.00 % (2512637)Peak memory usage: 88 MB
% 7.04/2.00 % (2512637)Instructions burned: 1 (million)
% 7.04/2.00 % (2512638)Instruction limit reached!
% 7.04/2.00 % (2512638)------------------------------
% 7.04/2.00 % (2512638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512638)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512638)Termination reason: Instruction limit
% 7.04/2.00 % (2512638)Termination phase: Saturation
% 7.04/2.00 % (2512638)Time elapsed: 0.064 s
% 7.04/2.00 % (2512638)Peak memory usage: 88 MB
% 7.04/2.00 % (2512638)Instructions burned: 119 (million)
% 7.04/2.00 % (2512640)Instruction limit reached!
% 7.04/2.00 % (2512640)------------------------------
% 7.04/2.00 % (2512640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512640)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512640)Termination reason: Instruction limit
% 7.04/2.00 % (2512640)Termination phase: Saturation
% 7.04/2.00 % (2512640)Time elapsed: 0.079 s
% 7.04/2.00 % (2512640)Peak memory usage: 89 MB
% 7.04/2.00 % (2512640)Instructions burned: 130 (million)
% 7.04/2.00 % (2512639)Instruction limit reached!
% 7.04/2.00 % (2512639)------------------------------
% 7.04/2.00 % (2512639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512639)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512639)Termination reason: Instruction limit
% 7.04/2.00 % (2512639)Termination phase: Saturation
% 7.04/2.00 % (2512639)Time elapsed: 0.093 s
% 7.04/2.00 % (2512639)Peak memory usage: 89 MB
% 7.04/2.00 % (2512639)Instructions burned: 139 (million)
% 7.04/2.00 % (2512648)lrs+10_1_sil=8000:sp=occurrence:random_seed=2556764409:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.04/2.00 % (2512649)lrs+10_1_sil=32000:urr=on:br=off:random_seed=907365149:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.04/2.00 % (2512637)------------------------------
% 7.04/2.00 % (2512637)------------------------------
% 7.04/2.00 % (2512650)lrs+1011_1_sil=32000:sp=occurrence:random_seed=374543805:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.04/2.00 % (2512649)Refutation not found, incomplete strategy
% 7.04/2.00 % (2512649)------------------------------
% 7.04/2.00 % (2512649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512649)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512649)Termination reason: Refutation not found, incomplete strategy
% 7.04/2.00 % (2512649)Time elapsed: 0.007 s
% 7.04/2.00 % (2512649)Peak memory usage: 89 MB
% 7.04/2.00 % (2512649)Instructions burned: 8 (million)
% 7.04/2.00 % (2512648)Instruction limit reached!
% 7.04/2.00 % (2512648)------------------------------
% 7.04/2.00 % (2512648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512648)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512648)Termination reason: Instruction limit
% 7.04/2.00 % (2512648)Termination phase: Saturation
% 7.04/2.00 % (2512648)Time elapsed: 0.165 s
% 7.04/2.00 % (2512648)Peak memory usage: 92 MB
% 7.04/2.00 % (2512648)Instructions burned: 285 (million)
% 7.04/2.00 % (2512654)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=665873747:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 7.04/2.00 % (2512650)Instruction limit reached!
% 7.04/2.00 % (2512650)------------------------------
% 7.04/2.00 % (2512650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512650)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512650)Termination reason: Instruction limit
% 7.04/2.00 % (2512650)Termination phase: Saturation
% 7.04/2.00 % (2512650)Time elapsed: 0.216 s
% 7.04/2.00 % (2512650)Peak memory usage: 91 MB
% 7.04/2.00 % (2512650)Instructions burned: 326 (million)
% 7.04/2.00 % (2512649)------------------------------
% 7.04/2.00 % (2512649)------------------------------
% 7.04/2.00 % (2512654)Instruction limit reached!
% 7.04/2.00 % (2512654)------------------------------
% 7.04/2.00 % (2512654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512654)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512654)Termination reason: Instruction limit
% 7.04/2.00 % (2512654)Termination phase: Saturation
% 7.04/2.00 % (2512654)Time elapsed: 0.135 s
% 7.04/2.00 % (2512654)Peak memory usage: 95 MB
% 7.04/2.00 % (2512654)Instructions burned: 249 (million)
% 7.04/2.00 % (2512655)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1954087189:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 7.04/2.00 % (2512655)Refutation not found, incomplete strategy
% 7.04/2.00 % (2512655)------------------------------
% 7.04/2.00 % (2512655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512655)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512655)Termination reason: Refutation not found, incomplete strategy
% 7.04/2.00 % (2512655)Time elapsed: 0.003 s
% 7.04/2.00 % (2512655)Peak memory usage: 88 MB
% 7.04/2.00 % (2512655)Instructions burned: 4 (million)
% 7.04/2.00 % (2512657)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1167035152:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 7.04/2.00 % (2512658)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3828407710:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 7.04/2.00 % (2512634)First to succeed.
% 7.04/2.00 % (2512660)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1827836858:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 7.04/2.00 % (2512634)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2512629"
% 7.04/2.00 % (2512658)Instruction limit reached!
% 7.04/2.00 % (2512658)------------------------------
% 7.04/2.00 % (2512658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512658)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512658)Termination reason: Instruction limit
% 7.04/2.00 % (2512658)Termination phase: Saturation
% 7.04/2.00 % (2512658)Time elapsed: 0.073 s
% 7.04/2.00 % (2512658)Peak memory usage: 92 MB
% 7.04/2.00 % (2512658)Instructions burned: 114 (million)
% 7.04/2.00 % (2512660)Instruction limit reached!
% 7.04/2.00 % (2512660)------------------------------
% 7.04/2.00 % (2512660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512660)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512660)Termination reason: Instruction limit
% 7.04/2.00 % (2512660)Termination phase: Saturation
% 7.04/2.00 % (2512660)Time elapsed: 0.064 s
% 7.04/2.00 % (2512660)Peak memory usage: 89 MB
% 7.04/2.00 % (2512660)Instructions burned: 128 (million)
% 7.04/2.00 % (2512655)------------------------------
% 7.04/2.00 % (2512655)------------------------------
% 7.04/2.00 % (2512664)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=412134852:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 7.04/2.00 % (2512665)lrs+10_1_sil=8000:sp=occurrence:random_seed=1749440666:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 7.04/2.00 % (2512664)Instruction limit reached!
% 7.04/2.00 % (2512664)------------------------------
% 7.04/2.00 % (2512664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512664)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512664)Termination reason: Instruction limit
% 7.04/2.00 % (2512664)Termination phase: Saturation
% 7.04/2.00 % (2512664)Time elapsed: 0.062 s
% 7.04/2.00 % (2512664)Peak memory usage: 89 MB
% 7.04/2.00 % (2512664)Instructions burned: 116 (million)
% 7.04/2.00 % (2512666)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4268562541:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 7.04/2.00 % (2512666)Refutation not found, incomplete strategy
% 7.04/2.00 % (2512666)------------------------------
% 7.04/2.00 % (2512666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.04/2.00 % (2512666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.04/2.00 % (2512666)CaDiCaL version: 2.1.3
% 7.04/2.00 % (2512666)Termination reason: Refutation not found, incomplete strategy
% 7.04/2.00 % (2512666)Time elapsed: 0.004 s
% 7.04/2.00 % (2512666)Peak memory usage: 88 MB
% 7.04/2.00 % (2512666)Instructions burned: 6 (million)
% 7.04/2.00 % (2512634)Refutation found. Thanks to Tanya!
% 7.04/2.00 % SZS status Theorem for theBenchmark
% 7.04/2.00 % SZS output start Proof for theBenchmark
% See solution above
% 8.60/2.20 % (2512634)------------------------------
% 8.60/2.20 % (2512634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.20 % (2512634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.20 % (2512634)CaDiCaL version: 2.1.3
% 8.60/2.20 % (2512634)Termination reason: Refutation
% 8.60/2.20 % (2512634)Time elapsed: 0.710 s
% 8.60/2.20 % (2512634)Peak memory usage: 130 MB
% 8.60/2.20 % (2512634)Instructions burned: 1068 (million)
% 8.60/2.20 % (2512634)------------------------------
% 8.60/2.20 % (2512634)------------------------------
% 8.60/2.20 % (2512629)Success in time 1.138 s
% 8.60/2.20 % Vampire exiting
%------------------------------------------------------------------------------