%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO480+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 09:52:46 AM UTC 2026
% Result : Theorem 73.31s 14.29s
% Output : Refutation 86.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 51
% Syntax : Number of formulae : 276 ( 96 unt; 47 def)
% Number of atoms : 557 ( 215 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 512 ( 231 ~; 249 |; 16 &)
% ( 10 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 10 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 47 con; 0-5 aty)
% Number of variables : 273 ( 0 sgn 260 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f43,axiom,
~ p(s(bool,f0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSsrboolo_notu_falseu_isu_true) ).
fof(f97,axiom,
! [X0] :
( s(bool,X0) = s(bool,t)
| s(bool,X0) = s(bool,f0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aBOOLu_CASESu_AX) ).
fof(f721,axiom,
! [X0,X1,X2,X3,X4] :
( p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
<=> ? [X5] :
( p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
& s(X0,X3) = s(X0,i(s(fun(X1,X0),X2),s(X1,X5))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aMEMu_MAP) ).
fof(f3635,conjecture,
! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(fun(cart(real,X1),cart(real,X0)),bool),linear),s(fun(cart(real,X1),cart(real,X0)),X2))))
& ! [X3,X5] :
( s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))) = s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X5)))
=> s(cart(real,X1),X3) = s(cart(real,X1),X5) ) )
=> s(bool,i(s(fun(list(cart(real,X0)),bool),i(s(fun(cart(real,X0),fun(list(cart(real,X0)),bool)),mem),s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))))),s(list(cart(real,X0)),i(s(fun(list(cart(real,X1)),list(cart(real,X0))),i(s(fun(fun(cart(real,X1),cart(real,X0)),fun(list(cart(real,X1)),list(cart(real,X0)))),map0),s(fun(cart(real,X1),cart(real,X0)),X2))),s(list(cart(real,X1)),X4))))) = s(bool,i(s(fun(list(cart(real,X1)),bool),i(s(fun(cart(real,X1),fun(list(cart(real,X1)),bool)),mem),s(cart(real,X1),X3))),s(list(cart(real,X1)),X4))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aMEMu_LINEARu_IMAGE) ).
fof(f3636,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(fun(cart(real,X1),cart(real,X0)),bool),linear),s(fun(cart(real,X1),cart(real,X0)),X2))))
& ! [X3,X5] :
( s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))) = s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X5)))
=> s(cart(real,X1),X3) = s(cart(real,X1),X5) ) )
=> s(bool,i(s(fun(list(cart(real,X0)),bool),i(s(fun(cart(real,X0),fun(list(cart(real,X0)),bool)),mem),s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))))),s(list(cart(real,X0)),i(s(fun(list(cart(real,X1)),list(cart(real,X0))),i(s(fun(fun(cart(real,X1),cart(real,X0)),fun(list(cart(real,X1)),list(cart(real,X0)))),map0),s(fun(cart(real,X1),cart(real,X0)),X2))),s(list(cart(real,X1)),X4))))) = s(bool,i(s(fun(list(cart(real,X1)),bool),i(s(fun(cart(real,X1),fun(list(cart(real,X1)),bool)),mem),s(cart(real,X1),X3))),s(list(cart(real,X1)),X4))) ),
inference(negated_conjecture,[status(cth)],[f3635]) ).
fof(f4333,plain,
~ ! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(fun(cart(real,X1),cart(real,X0)),bool),linear),s(fun(cart(real,X1),cart(real,X0)),X2))))
& ! [X5,X6] :
( s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X5))) = s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X6)))
=> s(cart(real,X1),X5) = s(cart(real,X1),X6) ) )
=> s(bool,i(s(fun(list(cart(real,X0)),bool),i(s(fun(cart(real,X0),fun(list(cart(real,X0)),bool)),mem),s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))))),s(list(cart(real,X0)),i(s(fun(list(cart(real,X1)),list(cart(real,X0))),i(s(fun(fun(cart(real,X1),cart(real,X0)),fun(list(cart(real,X1)),list(cart(real,X0)))),map0),s(fun(cart(real,X1),cart(real,X0)),X2))),s(list(cart(real,X1)),X4))))) = s(bool,i(s(fun(list(cart(real,X1)),bool),i(s(fun(cart(real,X1),fun(list(cart(real,X1)),bool)),mem),s(cart(real,X1),X3))),s(list(cart(real,X1)),X4))) ),
inference(rectify,[],[f3636]) ).
fof(f6827,plain,
? [X0,X1,X2,X3,X4] :
( s(bool,i(s(fun(list(cart(real,X0)),bool),i(s(fun(cart(real,X0),fun(list(cart(real,X0)),bool)),mem),s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))))),s(list(cart(real,X0)),i(s(fun(list(cart(real,X1)),list(cart(real,X0))),i(s(fun(fun(cart(real,X1),cart(real,X0)),fun(list(cart(real,X1)),list(cart(real,X0)))),map0),s(fun(cart(real,X1),cart(real,X0)),X2))),s(list(cart(real,X1)),X4))))) != s(bool,i(s(fun(list(cart(real,X1)),bool),i(s(fun(cart(real,X1),fun(list(cart(real,X1)),bool)),mem),s(cart(real,X1),X3))),s(list(cart(real,X1)),X4)))
& p(s(bool,i(s(fun(fun(cart(real,X1),cart(real,X0)),bool),linear),s(fun(cart(real,X1),cart(real,X0)),X2))))
& ! [X5,X6] :
( s(cart(real,X1),X5) = s(cart(real,X1),X6)
| s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X5))) != s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X6))) ) ),
inference(ennf_transformation,[],[f4333]) ).
fof(f6828,plain,
? [X0,X1,X2,X3,X4] :
( s(bool,i(s(fun(list(cart(real,X0)),bool),i(s(fun(cart(real,X0),fun(list(cart(real,X0)),bool)),mem),s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X3))))),s(list(cart(real,X0)),i(s(fun(list(cart(real,X1)),list(cart(real,X0))),i(s(fun(fun(cart(real,X1),cart(real,X0)),fun(list(cart(real,X1)),list(cart(real,X0)))),map0),s(fun(cart(real,X1),cart(real,X0)),X2))),s(list(cart(real,X1)),X4))))) != s(bool,i(s(fun(list(cart(real,X1)),bool),i(s(fun(cart(real,X1),fun(list(cart(real,X1)),bool)),mem),s(cart(real,X1),X3))),s(list(cart(real,X1)),X4)))
& p(s(bool,i(s(fun(fun(cart(real,X1),cart(real,X0)),bool),linear),s(fun(cart(real,X1),cart(real,X0)),X2))))
& ! [X5,X6] :
( s(cart(real,X1),X5) = s(cart(real,X1),X6)
| s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X5))) != s(cart(real,X0),i(s(fun(cart(real,X1),cart(real,X0)),X2),s(cart(real,X1),X6))) ) ),
inference(flattening,[],[f6827]) ).
fof(f7950,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
| ! [X5] :
( ~ p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
| s(X0,X3) != s(X0,i(s(fun(X1,X0),X2),s(X1,X5))) ) )
& ( ? [X5] :
( p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
& s(X0,X3) = s(X0,i(s(fun(X1,X0),X2),s(X1,X5))) )
| ~ p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4)))))) ) ),
inference(nnf_transformation,[],[f721]) ).
fof(f7951,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
| ! [X5] :
( ~ p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
| s(X0,X3) != s(X0,i(s(fun(X1,X0),X2),s(X1,X5))) ) )
& ( ? [X6] :
( p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X6))),s(list(X1),X4))))
& s(X0,X3) = s(X0,i(s(fun(X1,X0),X2),s(X1,X6))) )
| ~ p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4)))))) ) ),
inference(rectify,[],[f7950]) ).
fof(f7952,plain,
! [X0,X1,X2,X3,X4] :
( ( p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
| ! [X5] :
( ~ p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
| s(X0,X3) != s(X0,i(s(fun(X1,X0),X2),s(X1,X5))) ) )
& ( ( p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,sK721(X0,X1,X2,X3,X4)))),s(list(X1),X4))))
& s(X0,X3) = s(X0,i(s(fun(X1,X0),X2),s(X1,sK721(X0,X1,X2,X3,X4)))) )
| ~ p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4)))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK721]),skolemize(X6,sK721(X0,X1,X2,X3,X4))],[f7951]) ).
fof(f11278,plain,
( s(bool,i(s(fun(list(cart(real,sK4556)),bool),i(s(fun(cart(real,sK4556),fun(list(cart(real,sK4556)),bool)),mem),s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),sK4559))))),s(list(cart(real,sK4556)),i(s(fun(list(cart(real,sK4557)),list(cart(real,sK4556))),i(s(fun(fun(cart(real,sK4557),cart(real,sK4556)),fun(list(cart(real,sK4557)),list(cart(real,sK4556)))),map0),s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558))),s(list(cart(real,sK4557)),sK4560))))) != s(bool,i(s(fun(list(cart(real,sK4557)),bool),i(s(fun(cart(real,sK4557),fun(list(cart(real,sK4557)),bool)),mem),s(cart(real,sK4557),sK4559))),s(list(cart(real,sK4557)),sK4560)))
& p(s(bool,i(s(fun(fun(cart(real,sK4557),cart(real,sK4556)),bool),linear),s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558))))
& ! [X5,X6] :
( s(cart(real,sK4557),X5) = s(cart(real,sK4557),X6)
| s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),X5))) != s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),X6))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4556,sK4557,sK4558,sK4559,sK4560]),skolemize(X0,sK4556),skolemize(X1,sK4557),skolemize(X2,sK4558),skolemize(X3,sK4559),skolemize(X4,sK4560)],[f6828]) ).
fof(f11445,plain,
~ p(s(bool,f0)),
inference(cnf_transformation,[],[f43]) ).
fof(f11677,plain,
! [X0] :
( s(bool,X0) = s(bool,f0)
| s(bool,t) = s(bool,X0) ),
inference(cnf_transformation,[],[f97]) ).
fof(f12870,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
| s(X0,X3) = s(X0,i(s(fun(X1,X0),X2),s(X1,sK721(X0,X1,X2,X3,X4)))) ),
inference(cnf_transformation,[],[f7952]) ).
fof(f12871,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4))))))
| p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,sK721(X0,X1,X2,X3,X4)))),s(list(X1),X4)))) ),
inference(cnf_transformation,[],[f7952]) ).
fof(f12872,plain,
! [X2,X3,X0,X1,X4,X5] :
( s(X0,X3) != s(X0,i(s(fun(X1,X0),X2),s(X1,X5)))
| ~ p(s(bool,i(s(fun(list(X1),bool),i(s(fun(X1,fun(list(X1),bool)),mem),s(X1,X5))),s(list(X1),X4))))
| p(s(bool,i(s(fun(list(X0),bool),i(s(fun(X0,fun(list(X0),bool)),mem),s(X0,X3))),s(list(X0),i(s(fun(list(X1),list(X0)),i(s(fun(fun(X1,X0),fun(list(X1),list(X0))),map0),s(fun(X1,X0),X2))),s(list(X1),X4)))))) ),
inference(cnf_transformation,[],[f7952]) ).
fof(f19398,plain,
! [X6,X5] :
( s(cart(real,sK4557),X5) = s(cart(real,sK4557),X6)
| s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),X5))) != s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),X6))) ),
inference(cnf_transformation,[],[f11278]) ).
fof(f19399,plain,
p(s(bool,i(s(fun(fun(cart(real,sK4557),cart(real,sK4556)),bool),linear),s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558)))),
inference(cnf_transformation,[],[f11278]) ).
fof(f19400,plain,
s(bool,i(s(fun(list(cart(real,sK4556)),bool),i(s(fun(cart(real,sK4556),fun(list(cart(real,sK4556)),bool)),mem),s(cart(real,sK4556),i(s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558),s(cart(real,sK4557),sK4559))))),s(list(cart(real,sK4556)),i(s(fun(list(cart(real,sK4557)),list(cart(real,sK4556))),i(s(fun(fun(cart(real,sK4557),cart(real,sK4556)),fun(list(cart(real,sK4557)),list(cart(real,sK4556)))),map0),s(fun(cart(real,sK4557),cart(real,sK4556)),sK4558))),s(list(cart(real,sK4557)),sK4560))))) != s(bool,i(s(fun(list(cart(real,sK4557)),bool),i(s(fun(cart(real,sK4557),fun(list(cart(real,sK4557)),bool)),mem),s(cart(real,sK4557),sK4559))),s(list(cart(real,sK4557)),sK4560))),
inference(cnf_transformation,[],[f11278]) ).
fof(f19401,definition,
sF4561 = cart(real,sK4556),
introduced(definition,[new_symbols(definition,[sF4561])],[function_definition]) ).
fof(f19402,plain,
cart(real,sK4556) = sF4561,
inference(reorient_equations,[],[f19401]) ).
fof(f19403,definition,
sF4562 = list(sF4561),
introduced(definition,[new_symbols(definition,[sF4562])],[function_definition]) ).
fof(f19404,plain,
list(sF4561) = sF4562,
inference(reorient_equations,[],[f19403]) ).
fof(f19405,definition,
sF4563 = fun(sF4562,bool),
introduced(definition,[new_symbols(definition,[sF4563])],[function_definition]) ).
fof(f19406,plain,
fun(sF4562,bool) = sF4563,
inference(reorient_equations,[],[f19405]) ).
fof(f19407,definition,
sF4564 = fun(sF4561,sF4563),
introduced(definition,[new_symbols(definition,[sF4564])],[function_definition]) ).
fof(f19408,plain,
fun(sF4561,sF4563) = sF4564,
inference(reorient_equations,[],[f19407]) ).
fof(f19409,definition,
sF4565 = s(sF4564,mem),
introduced(definition,[new_symbols(definition,[sF4565])],[function_definition]) ).
fof(f19410,plain,
s(sF4564,mem) = sF4565,
inference(reorient_equations,[],[f19409]) ).
fof(f19411,definition,
sF4566 = cart(real,sK4557),
introduced(definition,[new_symbols(definition,[sF4566])],[function_definition]) ).
fof(f19412,plain,
cart(real,sK4557) = sF4566,
inference(reorient_equations,[],[f19411]) ).
fof(f19413,definition,
sF4567 = fun(sF4566,sF4561),
introduced(definition,[new_symbols(definition,[sF4567])],[function_definition]) ).
fof(f19414,plain,
fun(sF4566,sF4561) = sF4567,
inference(reorient_equations,[],[f19413]) ).
fof(f19415,definition,
sF4568 = s(sF4567,sK4558),
introduced(definition,[new_symbols(definition,[sF4568])],[function_definition]) ).
fof(f19416,plain,
s(sF4567,sK4558) = sF4568,
inference(reorient_equations,[],[f19415]) ).
fof(f19417,definition,
sF4569 = s(sF4566,sK4559),
introduced(definition,[new_symbols(definition,[sF4569])],[function_definition]) ).
fof(f19418,plain,
s(sF4566,sK4559) = sF4569,
inference(reorient_equations,[],[f19417]) ).
fof(f19419,definition,
sF4570 = i(sF4568,sF4569),
introduced(definition,[new_symbols(definition,[sF4570])],[function_definition]) ).
fof(f19420,plain,
i(sF4568,sF4569) = sF4570,
inference(reorient_equations,[],[f19419]) ).
fof(f19421,definition,
sF4571 = s(sF4561,sF4570),
introduced(definition,[new_symbols(definition,[sF4571])],[function_definition]) ).
fof(f19422,plain,
s(sF4561,sF4570) = sF4571,
inference(reorient_equations,[],[f19421]) ).
fof(f19423,definition,
sF4572 = i(sF4565,sF4571),
introduced(definition,[new_symbols(definition,[sF4572])],[function_definition]) ).
fof(f19424,plain,
i(sF4565,sF4571) = sF4572,
inference(reorient_equations,[],[f19423]) ).
fof(f19425,definition,
sF4573 = s(sF4563,sF4572),
introduced(definition,[new_symbols(definition,[sF4573])],[function_definition]) ).
fof(f19426,plain,
s(sF4563,sF4572) = sF4573,
inference(reorient_equations,[],[f19425]) ).
fof(f19427,definition,
sF4574 = list(sF4566),
introduced(definition,[new_symbols(definition,[sF4574])],[function_definition]) ).
fof(f19428,plain,
list(sF4566) = sF4574,
inference(reorient_equations,[],[f19427]) ).
fof(f19429,definition,
sF4575 = fun(sF4574,sF4562),
introduced(definition,[new_symbols(definition,[sF4575])],[function_definition]) ).
fof(f19430,plain,
fun(sF4574,sF4562) = sF4575,
inference(reorient_equations,[],[f19429]) ).
fof(f19431,definition,
sF4576 = fun(sF4567,sF4575),
introduced(definition,[new_symbols(definition,[sF4576])],[function_definition]) ).
fof(f19432,plain,
fun(sF4567,sF4575) = sF4576,
inference(reorient_equations,[],[f19431]) ).
fof(f19433,definition,
sF4577 = s(sF4576,map0),
introduced(definition,[new_symbols(definition,[sF4577])],[function_definition]) ).
fof(f19434,plain,
s(sF4576,map0) = sF4577,
inference(reorient_equations,[],[f19433]) ).
fof(f19435,definition,
sF4578 = i(sF4577,sF4568),
introduced(definition,[new_symbols(definition,[sF4578])],[function_definition]) ).
fof(f19436,plain,
i(sF4577,sF4568) = sF4578,
inference(reorient_equations,[],[f19435]) ).
fof(f19437,definition,
sF4579 = s(sF4575,sF4578),
introduced(definition,[new_symbols(definition,[sF4579])],[function_definition]) ).
fof(f19438,plain,
s(sF4575,sF4578) = sF4579,
inference(reorient_equations,[],[f19437]) ).
fof(f19439,definition,
sF4580 = s(sF4574,sK4560),
introduced(definition,[new_symbols(definition,[sF4580])],[function_definition]) ).
fof(f19440,plain,
s(sF4574,sK4560) = sF4580,
inference(reorient_equations,[],[f19439]) ).
fof(f19441,definition,
sF4581 = i(sF4579,sF4580),
introduced(definition,[new_symbols(definition,[sF4581])],[function_definition]) ).
fof(f19442,plain,
i(sF4579,sF4580) = sF4581,
inference(reorient_equations,[],[f19441]) ).
fof(f19443,definition,
sF4582 = s(sF4562,sF4581),
introduced(definition,[new_symbols(definition,[sF4582])],[function_definition]) ).
fof(f19444,plain,
s(sF4562,sF4581) = sF4582,
inference(reorient_equations,[],[f19443]) ).
fof(f19445,definition,
sF4583 = i(sF4573,sF4582),
introduced(definition,[new_symbols(definition,[sF4583])],[function_definition]) ).
fof(f19446,plain,
i(sF4573,sF4582) = sF4583,
inference(reorient_equations,[],[f19445]) ).
fof(f19447,definition,
sF4584 = s(bool,sF4583),
introduced(definition,[new_symbols(definition,[sF4584])],[function_definition]) ).
fof(f19448,plain,
s(bool,sF4583) = sF4584,
inference(reorient_equations,[],[f19447]) ).
fof(f19449,definition,
sF4585 = fun(sF4574,bool),
introduced(definition,[new_symbols(definition,[sF4585])],[function_definition]) ).
fof(f19450,plain,
fun(sF4574,bool) = sF4585,
inference(reorient_equations,[],[f19449]) ).
fof(f19451,definition,
sF4586 = fun(sF4566,sF4585),
introduced(definition,[new_symbols(definition,[sF4586])],[function_definition]) ).
fof(f19452,plain,
fun(sF4566,sF4585) = sF4586,
inference(reorient_equations,[],[f19451]) ).
fof(f19453,definition,
sF4587 = s(sF4586,mem),
introduced(definition,[new_symbols(definition,[sF4587])],[function_definition]) ).
fof(f19454,plain,
s(sF4586,mem) = sF4587,
inference(reorient_equations,[],[f19453]) ).
fof(f19455,definition,
sF4588 = i(sF4587,sF4569),
introduced(definition,[new_symbols(definition,[sF4588])],[function_definition]) ).
fof(f19456,plain,
i(sF4587,sF4569) = sF4588,
inference(reorient_equations,[],[f19455]) ).
fof(f19457,definition,
sF4589 = s(sF4585,sF4588),
introduced(definition,[new_symbols(definition,[sF4589])],[function_definition]) ).
fof(f19458,plain,
s(sF4585,sF4588) = sF4589,
inference(reorient_equations,[],[f19457]) ).
fof(f19459,definition,
sF4590 = i(sF4589,sF4580),
introduced(definition,[new_symbols(definition,[sF4590])],[function_definition]) ).
fof(f19460,plain,
i(sF4589,sF4580) = sF4590,
inference(reorient_equations,[],[f19459]) ).
fof(f19461,definition,
sF4591 = s(bool,sF4590),
introduced(definition,[new_symbols(definition,[sF4591])],[function_definition]) ).
fof(f19462,plain,
s(bool,sF4590) = sF4591,
inference(reorient_equations,[],[f19461]) ).
fof(f19463,plain,
sF4584 != sF4591,
inference(definition_folding,[],[f19400,f19462,f19460,f19440,f19428,f19412,f19458,f19456,f19418,f19412,f19454,f19452,f19450,f19428,f19412,f19412,f19450,f19428,f19412,f19448,f19446,f19444,f19442,f19440,f19428,f19412,f19438,f19436,f19416,f19414,f19402,f19412,f19434,f19432,f19430,f19404,f19402,f19428,f19412,f19414,f19402,f19412,f19430,f19404,f19402,f19428,f19412,f19404,f19402,f19426,f19424,f19422,f19420,f19418,f19412,f19416,f19414,f19402,f19412,f19402,f19410,f19408,f19406,f19404,f19402,f19402,f19406,f19404,f19402]) ).
fof(f19464,definition,
sF4592 = fun(sF4567,bool),
introduced(definition,[new_symbols(definition,[sF4592])],[function_definition]) ).
fof(f19465,plain,
fun(sF4567,bool) = sF4592,
inference(reorient_equations,[],[f19464]) ).
fof(f19466,definition,
sF4593 = s(sF4592,linear),
introduced(definition,[new_symbols(definition,[sF4593])],[function_definition]) ).
fof(f19467,plain,
s(sF4592,linear) = sF4593,
inference(reorient_equations,[],[f19466]) ).
fof(f19468,definition,
sF4594 = i(sF4593,sF4568),
introduced(definition,[new_symbols(definition,[sF4594])],[function_definition]) ).
fof(f19469,plain,
i(sF4593,sF4568) = sF4594,
inference(reorient_equations,[],[f19468]) ).
fof(f19470,definition,
sF4595 = s(bool,sF4594),
introduced(definition,[new_symbols(definition,[sF4595])],[function_definition]) ).
fof(f19471,plain,
s(bool,sF4594) = sF4595,
inference(reorient_equations,[],[f19470]) ).
fof(f19472,plain,
p(sF4595),
inference(definition_folding,[],[f19399,f19471,f19469,f19416,f19414,f19402,f19412,f19467,f19465,f19414,f19402,f19412]) ).
fof(f19473,definition,
! [X5] : sF4596(X5) = s(sF4566,X5),
introduced(definition,[new_symbols(definition,[sF4596])],[function_definition]) ).
fof(f19474,plain,
! [X5] : s(sF4566,X5) = sF4596(X5),
inference(reorient_equations,[],[f19473]) ).
fof(f19475,definition,
! [X5] : sF4597(X5) = i(sF4568,sF4596(X5)),
introduced(definition,[new_symbols(definition,[sF4597])],[function_definition]) ).
fof(f19476,plain,
! [X5] : i(sF4568,sF4596(X5)) = sF4597(X5),
inference(reorient_equations,[],[f19475]) ).
fof(f19477,definition,
! [X5] : sF4598(X5) = s(sF4561,sF4597(X5)),
introduced(definition,[new_symbols(definition,[sF4598])],[function_definition]) ).
fof(f19478,plain,
! [X5] : s(sF4561,sF4597(X5)) = sF4598(X5),
inference(reorient_equations,[],[f19477]) ).
fof(f19479,plain,
! [X6,X5] :
( sF4598(X5) != sF4598(X6)
| sF4596(X5) = sF4596(X6) ),
inference(definition_folding,[],[f19398,f19478,f19476,f19474,f19412,f19416,f19414,f19402,f19412,f19402,f19478,f19476,f19474,f19412,f19416,f19414,f19402,f19412,f19402,f19474,f19412,f19474,f19412]) ).
fof(f19845,definition,
( spl4599_61
<=> p(s(bool,f0)) ),
introduced(definition,[new_symbols(definition,[spl4599_61])],[avatar_definition]) ).
fof(f19846,plain,
( ~ p(s(bool,f0))
| spl4599_61 ),
inference(avatar_component_clause,[],[f19845]) ).
fof(f20808,plain,
~ spl4599_61,
inference(avatar_split_clause,[],[f11445,f19845]) ).
fof(f21408,plain,
sF4569 = sF4596(sK4559),
inference(superposition,[],[f19474,f19418]) ).
fof(f21413,plain,
! [X2,X3,X0,X1] :
( s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),s(sF4566,X2)))
| ~ p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,X2))),s(list(sF4566),X3))))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(superposition,[],[f12872,f19414]) ).
fof(f21438,plain,
! [X2,X3,X0,X1] :
( s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| ~ p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,X2))),s(list(sF4566),X3))))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21413,f19474]) ).
fof(f21446,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4574,bool),i(s(fun(sF4566,fun(sF4574,bool)),mem),s(sF4566,X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21438,f19428]) ).
fof(f21454,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4574,bool),i(s(fun(sF4566,fun(sF4574,bool)),mem),sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21446,f19474]) ).
fof(f21462,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(sF4585,i(s(fun(sF4566,sF4585),mem),sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21454,f19450]) ).
fof(f21470,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(sF4585,i(s(sF4586,mem),sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21462,f19452]) ).
fof(f21477,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X3)))))) ),
inference(forward_demodulation,[],[f21470,f19454]) ).
fof(f21481,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(sF4574,list(sF4561)),i(s(fun(sF4567,fun(sF4574,list(sF4561))),map0),s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21477,f19428]) ).
fof(f21483,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(fun(sF4574,sF4562),i(s(fun(sF4567,fun(sF4574,sF4562)),map0),s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21481,f19404]) ).
fof(f21484,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(fun(sF4567,sF4575),map0),s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21483,f19430]) ).
fof(f21485,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(sF4576,map0),s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21484,f19432]) ).
fof(f21486,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21485,f19434]) ).
fof(f21487,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(sF4563,i(s(fun(sF4561,sF4563),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21486,f19406]) ).
fof(f21488,plain,
! [X2,X3,X0,X1] :
( p(s(bool,i(s(sF4563,i(s(sF4564,mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X3))))))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2))) ),
inference(forward_demodulation,[],[f21487,f19408]) ).
fof(f21489,plain,
! [X2,X3,X0,X1] :
( s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4596(X2)))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4596(X2))),s(sF4574,X3))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X3)))))) ),
inference(forward_demodulation,[],[f21488,f19410]) ).
fof(f21637,definition,
( spl4599_220
<=> p(sF4591) ),
introduced(definition,[new_symbols(definition,[spl4599_220])],[avatar_definition]) ).
fof(f21638,plain,
( p(sF4591)
| ~ spl4599_220 ),
inference(avatar_component_clause,[],[f21637]) ).
fof(f21639,plain,
( ~ p(sF4591)
| spl4599_220 ),
inference(avatar_component_clause,[],[f21637]) ).
fof(f21672,definition,
( spl4599_222
<=> p(sF4584) ),
introduced(definition,[new_symbols(definition,[spl4599_222])],[avatar_definition]) ).
fof(f21673,plain,
( p(sF4584)
| ~ spl4599_222 ),
inference(avatar_component_clause,[],[f21672]) ).
fof(f21674,plain,
( ~ p(sF4584)
| spl4599_222 ),
inference(avatar_component_clause,[],[f21672]) ).
fof(f21681,plain,
! [X2,X0,X1] :
( s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4569))
| ~ p(s(bool,i(s(sF4585,i(sF4587,sF4569)),s(sF4574,X2))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(superposition,[],[f21489,f21408]) ).
fof(f21682,plain,
i(sF4568,sF4569) = sF4597(sK4559),
inference(superposition,[],[f19476,f21408]) ).
fof(f21683,plain,
sF4570 = sF4597(sK4559),
inference(forward_demodulation,[],[f21682,f19420]) ).
fof(f21684,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4585,sF4588),s(sF4574,X2))))
| s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4569))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21681,f19456]) ).
fof(f21685,plain,
! [X2,X0,X1] :
( s(sF4561,X0) != s(sF4561,i(s(sF4567,X1),sF4569))
| ~ p(s(bool,i(sF4589,s(sF4574,X2))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21684,f19458]) ).
fof(f21686,plain,
s(sF4561,sF4570) = sF4598(sK4559),
inference(superposition,[],[f19478,f21683]) ).
fof(f21687,plain,
sF4571 = sF4598(sK4559),
inference(forward_demodulation,[],[f21686,f19422]) ).
fof(f21689,plain,
! [X0,X1] :
( s(sF4561,X0) != s(sF4561,i(sF4568,sF4569))
| ~ p(s(bool,i(sF4589,s(sF4574,X1))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,sF4568)),s(sF4574,X1)))))) ),
inference(superposition,[],[f21685,f19416]) ).
fof(f21691,plain,
! [X0,X1] :
( s(sF4561,sF4570) != s(sF4561,X0)
| ~ p(s(bool,i(sF4589,s(sF4574,X1))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,sF4568)),s(sF4574,X1)))))) ),
inference(forward_demodulation,[],[f21689,f19420]) ).
fof(f21692,plain,
! [X0,X1] :
( sF4571 != s(sF4561,X0)
| ~ p(s(bool,i(sF4589,s(sF4574,X1))))
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,sF4568)),s(sF4574,X1)))))) ),
inference(forward_demodulation,[],[f21691,f19422]) ).
fof(f21693,plain,
! [X0,X1] :
( p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,sF4578),s(sF4574,X1))))))
| sF4571 != s(sF4561,X0)
| ~ p(s(bool,i(sF4589,s(sF4574,X1)))) ),
inference(forward_demodulation,[],[f21692,f19436]) ).
fof(f21694,plain,
! [X0,X1] :
( sF4571 != s(sF4561,X0)
| p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(sF4579,s(sF4574,X1))))))
| ~ p(s(bool,i(sF4589,s(sF4574,X1)))) ),
inference(forward_demodulation,[],[f21693,f19438]) ).
fof(f21747,plain,
! [X0] :
( sF4571 != sF4571
| p(s(bool,i(s(sF4563,i(sF4565,sF4571)),s(sF4562,i(sF4579,s(sF4574,X0))))))
| ~ p(s(bool,i(sF4589,s(sF4574,X0)))) ),
inference(superposition,[],[f21694,f19422]) ).
fof(f21749,plain,
! [X0] :
( p(s(bool,i(s(sF4563,i(sF4565,sF4571)),s(sF4562,i(sF4579,s(sF4574,X0))))))
| ~ p(s(bool,i(sF4589,s(sF4574,X0)))) ),
inference(trivial_inequality_removal,[],[f21747]) ).
fof(f21750,plain,
! [X0] :
( p(s(bool,i(s(sF4563,sF4572),s(sF4562,i(sF4579,s(sF4574,X0))))))
| ~ p(s(bool,i(sF4589,s(sF4574,X0)))) ),
inference(forward_demodulation,[],[f21749,f19424]) ).
fof(f21751,plain,
! [X0] :
( p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,X0))))))
| ~ p(s(bool,i(sF4589,s(sF4574,X0)))) ),
inference(forward_demodulation,[],[f21750,f19426]) ).
fof(f21791,plain,
! [X0] :
( sF4571 != sF4598(X0)
| sF4596(X0) = sF4596(sK4559) ),
inference(superposition,[],[f19479,f21687]) ).
fof(f21793,plain,
! [X0] :
( sF4571 != sF4598(X0)
| sF4569 = sF4596(X0) ),
inference(forward_demodulation,[],[f21791,f21408]) ).
fof(f21843,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(superposition,[],[f12871,f19414]) ).
fof(f21852,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(sF4574,list(sF4561)),i(s(fun(sF4567,fun(sF4574,list(sF4561))),map0),s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21843,f19428]) ).
fof(f21863,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(fun(sF4574,sF4562),i(s(fun(sF4567,fun(sF4574,sF4562)),map0),s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21852,f19404]) ).
fof(f21874,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(fun(sF4567,sF4575),map0),s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21863,f19430]) ).
fof(f21884,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(sF4576,map0),s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21874,f19432]) ).
fof(f21892,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21884,f19434]) ).
fof(f21897,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(s(fun(sF4561,sF4563),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21892,f19406]) ).
fof(f21901,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(s(sF4564,mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21897,f19408]) ).
fof(f21902,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(fun(list(sF4566),bool),i(s(fun(sF4566,fun(list(sF4566),bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(list(sF4566),X2)))) ),
inference(forward_demodulation,[],[f21901,f19410]) ).
fof(f21903,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(fun(sF4574,bool),i(s(fun(sF4566,fun(sF4574,bool)),mem),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))),s(sF4574,X2))))
| ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21902,f19428]) ).
fof(f21904,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(fun(sF4574,bool),i(s(fun(sF4566,fun(sF4574,bool)),mem),sF4596(sK721(sF4561,sF4566,X1,X0,X2)))),s(sF4574,X2))))
| ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21903,f19474]) ).
fof(f21905,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(sF4585,i(s(fun(sF4566,sF4585),mem),sF4596(sK721(sF4561,sF4566,X1,X0,X2)))),s(sF4574,X2))))
| ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21904,f19450]) ).
fof(f21906,plain,
! [X2,X0,X1] :
( p(s(bool,i(s(sF4585,i(s(sF4586,mem),sF4596(sK721(sF4561,sF4566,X1,X0,X2)))),s(sF4574,X2))))
| ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2)))))) ),
inference(forward_demodulation,[],[f21905,f19452]) ).
fof(f21907,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,X1,X0,X2)))),s(sF4574,X2)))) ),
inference(forward_demodulation,[],[f21906,f19454]) ).
fof(f21908,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,sF4571)),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X0))),s(sF4574,X1))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,X0,sF4570,X1)))),s(sF4574,X1)))) ),
inference(superposition,[],[f21907,f19422]) ).
fof(f21913,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,sF4572),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X0))),s(sF4574,X1))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,X0,sF4570,X1)))),s(sF4574,X1)))) ),
inference(forward_demodulation,[],[f21908,f19424]) ).
fof(f21915,plain,
! [X0,X1] :
( ~ p(s(bool,i(sF4573,s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X0))),s(sF4574,X1))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,X0,sF4570,X1)))),s(sF4574,X1)))) ),
inference(forward_demodulation,[],[f21913,f19426]) ).
fof(f22137,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(list(sF4566),list(sF4561)),i(s(fun(sF4567,fun(list(sF4566),list(sF4561))),map0),s(sF4567,X1))),s(list(sF4566),X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(superposition,[],[f12870,f19414]) ).
fof(f22145,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(list(sF4561),bool),i(s(fun(sF4561,fun(list(sF4561),bool)),mem),s(sF4561,X0))),s(list(sF4561),i(s(fun(sF4574,list(sF4561)),i(s(fun(sF4567,fun(sF4574,list(sF4561))),map0),s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22137,f19428]) ).
fof(f22154,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(fun(sF4574,sF4562),i(s(fun(sF4567,fun(sF4574,sF4562)),map0),s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22145,f19404]) ).
fof(f22162,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(fun(sF4567,sF4575),map0),s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22154,f19430]) ).
fof(f22169,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(s(sF4576,map0),s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22162,f19432]) ).
fof(f22175,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(fun(sF4562,bool),i(s(fun(sF4561,fun(sF4562,bool)),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22169,f19434]) ).
fof(f22180,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(s(fun(sF4561,sF4563),mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22175,f19406]) ).
fof(f22184,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(s(sF4564,mem),s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22180,f19408]) ).
fof(f22186,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),s(sF4566,sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22184,f19410]) ).
fof(f22187,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,s(sF4567,X1))),s(sF4574,X2))))))
| s(sF4561,X0) = s(sF4561,i(s(sF4567,X1),sF4596(sK721(sF4561,sF4566,X1,X0,X2)))) ),
inference(forward_demodulation,[],[f22186,f19474]) ).
fof(f22190,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,i(sF4577,sF4568)),s(sF4574,X1))))))
| s(sF4561,X0) = s(sF4561,i(sF4568,sF4596(sK721(sF4561,sF4566,sK4558,X0,X1)))) ),
inference(superposition,[],[f22187,f19416]) ).
fof(f22192,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(s(sF4575,sF4578),s(sF4574,X1))))))
| s(sF4561,X0) = s(sF4561,i(sF4568,sF4596(sK721(sF4561,sF4566,sK4558,X0,X1)))) ),
inference(forward_demodulation,[],[f22190,f19436]) ).
fof(f22194,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(sF4579,s(sF4574,X1))))))
| s(sF4561,X0) = s(sF4561,i(sF4568,sF4596(sK721(sF4561,sF4566,sK4558,X0,X1)))) ),
inference(forward_demodulation,[],[f22192,f19438]) ).
fof(f22196,plain,
! [X0,X1] :
( s(sF4561,X0) = s(sF4561,sF4597(sK721(sF4561,sF4566,sK4558,X0,X1)))
| ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(sF4579,s(sF4574,X1)))))) ),
inference(forward_demodulation,[],[f22194,f19476]) ).
fof(f22197,plain,
! [X0,X1] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(sF4579,s(sF4574,X1))))))
| s(sF4561,X0) = sF4598(sK721(sF4561,sF4566,sK4558,X0,X1)) ),
inference(forward_demodulation,[],[f22196,f19478]) ).
fof(f22206,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,i(sF4579,sF4580)))))
| s(sF4561,X0) = sF4598(sK721(sF4561,sF4566,sK4558,X0,sK4560)) ),
inference(superposition,[],[f22197,f19440]) ).
fof(f22207,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),s(sF4562,sF4581))))
| s(sF4561,X0) = sF4598(sK721(sF4561,sF4566,sK4558,X0,sK4560)) ),
inference(forward_demodulation,[],[f22206,f19442]) ).
fof(f22209,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,s(sF4561,X0))),sF4582)))
| s(sF4561,X0) = sF4598(sK721(sF4561,sF4566,sK4558,X0,sK4560)) ),
inference(forward_demodulation,[],[f22207,f19444]) ).
fof(f22212,plain,
! [X0] :
( ~ p(s(bool,i(s(sF4563,i(sF4565,sF4598(X0))),sF4582)))
| sF4598(X0) = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(X0),sK4560)) ),
inference(superposition,[],[f22209,f19478]) ).
fof(f22261,plain,
( ~ p(s(bool,i(s(sF4563,i(sF4565,sF4571)),sF4582)))
| sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560)) ),
inference(superposition,[],[f22212,f21687]) ).
fof(f22262,plain,
( ~ p(s(bool,i(s(sF4563,sF4572),sF4582)))
| sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560)) ),
inference(forward_demodulation,[],[f22261,f19424]) ).
fof(f22263,plain,
( ~ p(s(bool,i(sF4573,sF4582)))
| sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560)) ),
inference(forward_demodulation,[],[f22262,f19426]) ).
fof(f22264,plain,
( ~ p(s(bool,sF4583))
| sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560)) ),
inference(forward_demodulation,[],[f22263,f19446]) ).
fof(f22265,plain,
( ~ p(sF4584)
| sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560)) ),
inference(forward_demodulation,[],[f22264,f19448]) ).
fof(f22305,plain,
! [X0] :
( ~ p(s(bool,i(sF4573,s(sF4562,i(s(sF4575,i(sF4577,sF4568)),s(sF4574,X0))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,sK4558,sF4570,X0)))),s(sF4574,X0)))) ),
inference(superposition,[],[f21915,f19416]) ).
fof(f22307,plain,
! [X0] :
( ~ p(s(bool,i(sF4573,s(sF4562,i(s(sF4575,sF4578),s(sF4574,X0))))))
| p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,sK4558,sF4570,X0)))),s(sF4574,X0)))) ),
inference(forward_demodulation,[],[f22305,f19436]) ).
fof(f22308,plain,
! [X0] :
( p(s(bool,i(s(sF4585,i(sF4587,sF4596(sK721(sF4561,sF4566,sK4558,sF4570,X0)))),s(sF4574,X0))))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,X0)))))) ),
inference(forward_demodulation,[],[f22307,f19438]) ).
fof(f24250,plain,
( s(bool,f0) = sF4591
| s(bool,t) = sF4591 ),
inference(superposition,[],[f11677,f19462]) ).
fof(f24383,plain,
! [X0] :
( p(s(bool,f0))
| ~ p(s(bool,i(sF4589,s(sF4574,X0))))
| s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,X0))))) ),
inference(superposition,[],[f21751,f11677]) ).
fof(f24428,plain,
( s(bool,f0) = sF4584
| s(bool,t) = s(bool,sF4583) ),
inference(superposition,[],[f19448,f11677]) ).
fof(f24429,plain,
( s(bool,f0) = sF4591
| s(bool,t) = s(bool,sF4590) ),
inference(superposition,[],[f19462,f11677]) ).
fof(f24430,plain,
( s(bool,f0) = sF4595
| s(bool,t) = s(bool,sF4594) ),
inference(superposition,[],[f19471,f11677]) ).
fof(f24489,plain,
( s(bool,t) = sF4595
| s(bool,f0) = sF4595 ),
inference(forward_demodulation,[],[f24430,f19471]) ).
fof(f24490,plain,
( s(bool,t) = sF4591
| s(bool,f0) = sF4591 ),
inference(forward_demodulation,[],[f24429,f19462]) ).
fof(f24491,plain,
( s(bool,t) = sF4584
| s(bool,f0) = sF4584 ),
inference(forward_demodulation,[],[f24428,f19448]) ).
fof(f24499,plain,
( ! [X0] :
( ~ p(s(bool,i(sF4589,s(sF4574,X0))))
| s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,X0))))) )
| spl4599_61 ),
inference(forward_subsumption_resolution,[],[f24383,f19846]) ).
fof(f24557,definition,
( spl4599_241
<=> s(bool,t) = sF4595 ),
introduced(definition,[new_symbols(definition,[spl4599_241])],[avatar_definition]) ).
fof(f24559,plain,
( s(bool,t) = sF4595
| ~ spl4599_241 ),
inference(avatar_component_clause,[],[f24557]) ).
fof(f24561,definition,
( spl4599_242
<=> s(bool,f0) = sF4595 ),
introduced(definition,[new_symbols(definition,[spl4599_242])],[avatar_definition]) ).
fof(f24563,plain,
( s(bool,f0) = sF4595
| ~ spl4599_242 ),
inference(avatar_component_clause,[],[f24561]) ).
fof(f24566,definition,
( spl4599_243
<=> s(bool,t) = sF4591 ),
introduced(definition,[new_symbols(definition,[spl4599_243])],[avatar_definition]) ).
fof(f24568,plain,
( s(bool,t) = sF4591
| ~ spl4599_243 ),
inference(avatar_component_clause,[],[f24566]) ).
fof(f24570,definition,
( spl4599_244
<=> s(bool,f0) = sF4591 ),
introduced(definition,[new_symbols(definition,[spl4599_244])],[avatar_definition]) ).
fof(f24572,plain,
( s(bool,f0) = sF4591
| ~ spl4599_244 ),
inference(avatar_component_clause,[],[f24570]) ).
fof(f24573,plain,
( spl4599_243
| spl4599_244 ),
inference(avatar_split_clause,[],[f24250,f24570,f24566]) ).
fof(f24575,definition,
( spl4599_245
<=> s(bool,t) = sF4584 ),
introduced(definition,[new_symbols(definition,[spl4599_245])],[avatar_definition]) ).
fof(f24577,plain,
( s(bool,t) = sF4584
| ~ spl4599_245 ),
inference(avatar_component_clause,[],[f24575]) ).
fof(f24579,definition,
( spl4599_246
<=> s(bool,f0) = sF4584 ),
introduced(definition,[new_symbols(definition,[spl4599_246])],[avatar_definition]) ).
fof(f24581,plain,
( s(bool,f0) = sF4584
| ~ spl4599_246 ),
inference(avatar_component_clause,[],[f24579]) ).
fof(f24583,plain,
( spl4599_242
| spl4599_241 ),
inference(avatar_split_clause,[],[f24489,f24557,f24561]) ).
fof(f24584,plain,
( spl4599_244
| spl4599_243 ),
inference(avatar_split_clause,[],[f24490,f24566,f24570]) ).
fof(f24585,plain,
( spl4599_246
| spl4599_245 ),
inference(avatar_split_clause,[],[f24491,f24575,f24579]) ).
fof(f24588,plain,
( sF4591 = sF4595
| ~ spl4599_241
| ~ spl4599_243 ),
inference(forward_demodulation,[],[f24568,f24559]) ).
fof(f24589,plain,
( p(sF4591)
| ~ spl4599_241
| ~ spl4599_243 ),
inference(superposition,[],[f19472,f24588]) ).
fof(f24595,plain,
( $false
| spl4599_220
| ~ spl4599_241
| ~ spl4599_243 ),
inference(forward_subsumption_resolution,[],[f24589,f21639]) ).
fof(f24596,plain,
( spl4599_220
| ~ spl4599_241
| ~ spl4599_243 ),
inference(avatar_contradiction_clause,[],[f24595]) ).
fof(f24631,plain,
( sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4597(sK4559),sK4560))
| ~ spl4599_222 ),
inference(forward_subsumption_resolution,[],[f22265,f21673]) ).
fof(f24639,plain,
( sF4571 = sF4598(sK721(sF4561,sF4566,sK4558,sF4570,sK4560))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f24631,f21683]) ).
fof(f30718,plain,
( ~ p(s(bool,i(sF4589,sF4580)))
| s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,sF4580))))
| spl4599_61 ),
inference(superposition,[],[f24499,f19440]) ).
fof(f30720,plain,
( ~ p(s(bool,sF4590))
| s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,sF4580))))
| spl4599_61 ),
inference(forward_demodulation,[],[f30718,f19460]) ).
fof(f30725,plain,
( ~ p(sF4591)
| s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,sF4580))))
| spl4599_61 ),
inference(forward_demodulation,[],[f30720,f19462]) ).
fof(f30730,plain,
( s(bool,t) = s(bool,i(sF4573,s(sF4562,i(sF4579,sF4580))))
| spl4599_61
| ~ spl4599_220 ),
inference(forward_subsumption_resolution,[],[f30725,f21638]) ).
fof(f30731,plain,
( s(bool,t) = s(bool,i(sF4573,s(sF4562,sF4581)))
| spl4599_61
| ~ spl4599_220 ),
inference(forward_demodulation,[],[f30730,f19442]) ).
fof(f30732,plain,
( s(bool,t) = s(bool,i(sF4573,sF4582))
| spl4599_61
| ~ spl4599_220 ),
inference(forward_demodulation,[],[f30731,f19444]) ).
fof(f30733,plain,
( s(bool,t) = s(bool,sF4583)
| spl4599_61
| ~ spl4599_220 ),
inference(forward_demodulation,[],[f30732,f19446]) ).
fof(f30734,plain,
( s(bool,t) = sF4584
| spl4599_61
| ~ spl4599_220 ),
inference(forward_demodulation,[],[f30733,f19448]) ).
fof(f30892,plain,
( sF4584 = sF4591
| spl4599_61
| ~ spl4599_220
| ~ spl4599_243 ),
inference(forward_demodulation,[],[f30734,f24568]) ).
fof(f30913,plain,
( $false
| spl4599_61
| ~ spl4599_220
| ~ spl4599_243 ),
inference(forward_subsumption_resolution,[],[f30892,f19463]) ).
fof(f30914,plain,
( spl4599_61
| ~ spl4599_220
| ~ spl4599_243 ),
inference(avatar_contradiction_clause,[],[f30913]) ).
fof(f30954,plain,
( sF4584 = sF4591
| ~ spl4599_244
| ~ spl4599_246 ),
inference(forward_demodulation,[],[f24572,f24581]) ).
fof(f30957,plain,
( $false
| ~ spl4599_244
| ~ spl4599_246 ),
inference(forward_subsumption_resolution,[],[f30954,f19463]) ).
fof(f30958,plain,
( ~ spl4599_244
| ~ spl4599_246 ),
inference(avatar_contradiction_clause,[],[f30957]) ).
fof(f49364,plain,
( ~ p(sF4595)
| spl4599_61
| ~ spl4599_242 ),
inference(superposition,[],[f19846,f24563]) ).
fof(f49368,plain,
( $false
| spl4599_61
| ~ spl4599_242 ),
inference(forward_subsumption_resolution,[],[f49364,f19472]) ).
fof(f49369,plain,
( spl4599_61
| ~ spl4599_242 ),
inference(avatar_contradiction_clause,[],[f49368]) ).
fof(f49372,plain,
( sF4584 = sF4595
| ~ spl4599_241
| ~ spl4599_245 ),
inference(forward_demodulation,[],[f24559,f24577]) ).
fof(f49499,plain,
( ~ p(sF4591)
| spl4599_61
| ~ spl4599_244 ),
inference(superposition,[],[f19846,f24572]) ).
fof(f49516,plain,
( $false
| spl4599_61
| ~ spl4599_220
| ~ spl4599_244 ),
inference(forward_subsumption_resolution,[],[f49499,f21638]) ).
fof(f49517,plain,
( spl4599_61
| ~ spl4599_220
| ~ spl4599_244 ),
inference(avatar_contradiction_clause,[],[f49516]) ).
fof(f49552,plain,
( p(sF4584)
| ~ spl4599_241
| ~ spl4599_245 ),
inference(superposition,[],[f19472,f49372]) ).
fof(f50747,plain,
( sF4571 != sF4571
| sF4569 = sF4596(sK721(sF4561,sF4566,sK4558,sF4570,sK4560))
| ~ spl4599_222 ),
inference(superposition,[],[f21793,f24639]) ).
fof(f50765,plain,
( sF4569 = sF4596(sK721(sF4561,sF4566,sK4558,sF4570,sK4560))
| ~ spl4599_222 ),
inference(trivial_inequality_removal,[],[f50747]) ).
fof(f50803,plain,
( p(s(bool,i(s(sF4585,i(sF4587,sF4569)),s(sF4574,sK4560))))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(superposition,[],[f22308,f50765]) ).
fof(f50838,plain,
( p(s(bool,i(s(sF4585,i(sF4587,sF4569)),sF4580)))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50803,f19440]) ).
fof(f50853,plain,
( p(s(bool,i(s(sF4585,sF4588),sF4580)))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50838,f19456]) ).
fof(f50856,plain,
( p(s(bool,i(sF4589,sF4580)))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50853,f19458]) ).
fof(f50859,plain,
( p(s(bool,sF4590))
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50856,f19460]) ).
fof(f50860,plain,
( p(sF4591)
| ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50859,f19462]) ).
fof(f50861,plain,
( ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,s(sF4574,sK4560))))))
| spl4599_220
| ~ spl4599_222 ),
inference(forward_subsumption_resolution,[],[f50860,f21639]) ).
fof(f50862,plain,
( ~ p(s(bool,i(sF4573,s(sF4562,i(sF4579,sF4580)))))
| spl4599_220
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50861,f19440]) ).
fof(f50863,plain,
( ~ p(s(bool,i(sF4573,s(sF4562,sF4581))))
| spl4599_220
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50862,f19442]) ).
fof(f50864,plain,
( ~ p(s(bool,i(sF4573,sF4582)))
| spl4599_220
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50863,f19444]) ).
fof(f50865,plain,
( ~ p(s(bool,sF4583))
| spl4599_220
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50864,f19446]) ).
fof(f50866,plain,
( ~ p(sF4584)
| spl4599_220
| ~ spl4599_222 ),
inference(forward_demodulation,[],[f50865,f19448]) ).
fof(f50867,plain,
( $false
| spl4599_220
| ~ spl4599_222 ),
inference(forward_subsumption_resolution,[],[f50866,f21673]) ).
fof(f50868,plain,
( spl4599_220
| ~ spl4599_222 ),
inference(avatar_contradiction_clause,[],[f50867]) ).
fof(f50875,plain,
( $false
| spl4599_222
| ~ spl4599_241
| ~ spl4599_245 ),
inference(forward_subsumption_resolution,[],[f49552,f21674]) ).
fof(f50876,plain,
( spl4599_222
| ~ spl4599_241
| ~ spl4599_245 ),
inference(avatar_contradiction_clause,[],[f50875]) ).
cnf(s198,plain,
~ spl4599_61,
inference(sat_conversion,[],[f20808]) ).
cnf(s240,plain,
( spl4599_243
| spl4599_244 ),
inference(sat_conversion,[],[f24573]) ).
cnf(s242,plain,
( spl4599_241
| spl4599_242 ),
inference(sat_conversion,[],[f24583]) ).
cnf(s243,plain,
( spl4599_243
| spl4599_244 ),
inference(sat_conversion,[],[f24584]) ).
cnf(s244,plain,
( spl4599_245
| spl4599_246 ),
inference(sat_conversion,[],[f24585]) ).
cnf(s245,plain,
( spl4599_220
| ~ spl4599_241
| ~ spl4599_243 ),
inference(sat_conversion,[],[f24596]) ).
cnf(s248,plain,
( spl4599_61
| ~ spl4599_220
| ~ spl4599_243 ),
inference(sat_conversion,[],[f30914]) ).
cnf(s250,plain,
( ~ spl4599_244
| ~ spl4599_246 ),
inference(sat_conversion,[],[f30958]) ).
cnf(s279,plain,
( spl4599_61
| ~ spl4599_242 ),
inference(sat_conversion,[],[f49369]) ).
cnf(s281,plain,
( spl4599_61
| ~ spl4599_220
| ~ spl4599_244 ),
inference(sat_conversion,[],[f49517]) ).
cnf(s291,plain,
( spl4599_220
| ~ spl4599_222 ),
inference(sat_conversion,[],[f50868]) ).
cnf(s292,plain,
( spl4599_222
| ~ spl4599_241
| ~ spl4599_245 ),
inference(sat_conversion,[],[f50876]) ).
cnf(s302,plain,
~ spl4599_242,
inference(rat,[],[s279,s198]) ).
cnf(s304,plain,
spl4599_241,
inference(rat,[],[s242,s302]) ).
cnf(s311,plain,
spl4599_220,
inference(rat,[],[s250,s244,s243,s292,s245,s291,s304]) ).
cnf(s312,plain,
~ spl4599_244,
inference(rat,[],[s281,s198,s311]) ).
cnf(s314,plain,
~ spl4599_243,
inference(rat,[],[s248,s198,s311]) ).
cnf(s317,plain,
$false,
inference(rat,[],[s240,s312,s314]) ).
fof(f50889,plain,
$false,
inference(avatar_sat_refutation,[],[s317]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO480+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n016.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 08:22:59 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.33/3.54 % (2315495)Detected formulas, will run a generic FOF schedule.
% 11.33/3.54 % (2315504)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2794244111:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 11.33/3.54 % (2315504)Instruction limit reached!
% 11.33/3.54 % (2315504)------------------------------
% 11.33/3.54 % (2315504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/3.54 % (2315504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/3.54 % (2315504)CaDiCaL version: 2.1.3
% 11.33/3.54 % (2315504)Termination reason: Instruction limit
% 11.33/3.54 % (2315504)Termination phase: Preprocessing 1
% 11.33/3.54 % (2315504)Time elapsed: 0.038 s
% 11.33/3.54 % (2315504)Peak memory usage: 91 MB
% 11.33/3.54 % (2315504)Instructions burned: 119 (million)
% 11.33/3.54 % (2315502)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=3406057316:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 11.33/3.54 % (2315501)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=1070248574:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 11.33/3.54 % (2315503)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=645758182:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 11.33/3.54 % (2315500)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=2043211877:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 11.33/3.54 % (2315505)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=961829620:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 11.33/3.54 % (2315506)dis-21_1_sil=8000:lcm=predicate:random_seed=2969983085:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 11.33/3.54 % (2315505)Instruction limit reached!
% 11.33/3.54 % (2315505)------------------------------
% 11.33/3.54 % (2315505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/3.54 % (2315505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/3.54 % (2315505)CaDiCaL version: 2.1.3
% 11.33/3.54 % (2315505)Termination reason: Instruction limit
% 11.33/3.54 % (2315505)Termination phase: Property scanning
% 11.33/3.54 % (2315505)Time elapsed: 0.049 s
% 11.33/3.54 % (2315505)Peak memory usage: 91 MB
% 11.33/3.54 % (2315505)Instructions burned: 141 (million)
% 11.33/3.54 % (2315503)Instruction limit reached!
% 11.33/3.54 % (2315503)------------------------------
% 11.33/3.54 % (2315503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/3.54 % (2315503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/3.54 % (2315503)CaDiCaL version: 2.1.3
% 11.33/3.54 % (2315503)Termination reason: Instruction limit
% 11.33/3.54 % (2315503)Termination phase: Property scanning
% 11.33/3.54 % (2315503)Time elapsed: 0.059 s
% 11.33/3.54 % (2315503)Peak memory usage: 93 MB
% 11.33/3.54 % (2315503)Instructions burned: 110 (million)
% 11.33/3.54 % (2315506)Instruction limit reached!
% 11.33/3.54 % (2315506)------------------------------
% 11.33/3.54 % (2315506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/3.54 % (2315506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/3.54 % (2315506)CaDiCaL version: 2.1.3
% 11.33/3.54 % (2315506)Termination reason: Instruction limit
% 11.33/3.54 % (2315506)Termination phase: SInE selection
% 11.33/3.54 % (2315506)Time elapsed: 0.061 s
% 11.33/3.54 % (2315506)Peak memory usage: 91 MB
% 11.33/3.54 % (2315506)Instructions burned: 129 (million)
% 11.33/3.54 % (2315508)lrs+10_1_sil=8000:sp=occurrence:random_seed=42582860:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 11.33/3.54 % (2315508)Instruction limit reached!
% 11.33/3.54 % (2315508)------------------------------
% 11.33/3.54 % (2315508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.33/3.54 % (2315508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.33/3.54 % (2315508)CaDiCaL version: 2.1.3
% 11.33/3.54 % (2315508)Termination reason: Instruction limit
% 11.33/3.54 % (2315508)Termination phase: Preprocessing 3
% 11.33/3.54 % (2315508)Time elapsed: 0.083 s
% 11.33/3.54 % (2315508)Peak memory usage: 98 MB
% 11.33/3.54 % (2315508)Instructions burned: 286 (million)
% 18.11/4.40 % (2315515)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2094023804:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 18.11/4.40 % (2315516)lrs+1011_1_sil=32000:sp=occurrence:random_seed=997426797:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 18.11/4.40 % (2315517)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=3224930512:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 18.11/4.40 % (2315515)Instruction limit reached!
% 18.11/4.40 % (2315515)------------------------------
% 18.11/4.40 % (2315515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/4.40 % (2315515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/4.40 % (2315515)CaDiCaL version: 2.1.3
% 18.11/4.40 % (2315515)Termination reason: Instruction limit
% 18.11/4.40 % (2315515)Termination phase: Property scanning
% 18.11/4.40 % (2315515)Time elapsed: 0.055 s
% 18.11/4.40 % (2315515)Peak memory usage: 90 MB
% 18.11/4.40 % (2315515)Instructions burned: 159 (million)
% 18.11/4.40 % (2315519)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=325018983:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 18.11/4.40 % (2315517)Instruction limit reached!
% 18.11/4.40 % (2315517)------------------------------
% 18.11/4.40 % (2315517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/4.40 % (2315517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/4.40 % (2315517)CaDiCaL version: 2.1.3
% 18.11/4.40 % (2315517)Termination reason: Instruction limit
% 18.11/4.40 % (2315517)Termination phase: Property scanning
% 18.11/4.40 % (2315517)Time elapsed: 0.086 s
% 18.11/4.40 % (2315517)Peak memory usage: 91 MB
% 18.11/4.40 % (2315517)Instructions burned: 250 (million)
% 18.11/4.40 % (2315516)Instruction limit reached!
% 18.11/4.40 % (2315516)------------------------------
% 18.11/4.40 % (2315516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/4.40 % (2315516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/4.40 % (2315516)CaDiCaL version: 2.1.3
% 18.11/4.40 % (2315516)Termination reason: Instruction limit
% 18.11/4.40 % (2315516)Termination phase: Saturation
% 18.11/4.40 % (2315516)Time elapsed: 0.163 s
% 18.11/4.40 % (2315516)Peak memory usage: 97 MB
% 18.11/4.40 % (2315516)Instructions burned: 325 (million)
% 18.11/4.40 % (2315519)Instruction limit reached!
% 18.11/4.40 % (2315519)------------------------------
% 18.11/4.40 % (2315519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/4.40 % (2315519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/4.40 % (2315519)CaDiCaL version: 2.1.3
% 18.11/4.40 % (2315519)Termination reason: Instruction limit
% 18.11/4.40 % (2315519)Termination phase: Preprocessing 3
% 18.11/4.40 % (2315519)Time elapsed: 0.083 s
% 18.11/4.40 % (2315519)Peak memory usage: 95 MB
% 18.11/4.40 % (2315519)Instructions burned: 297 (million)
% 18.11/4.40 % (2315523)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3357604901:i=2350_2984 on theBenchmark for (2984ds/2350Mi)
% 18.11/4.40 % (2315525)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3151415526:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 18.11/4.40 % (2315527)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1251242164:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 18.11/4.40 % (2315526)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3309498672:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 18.11/4.40 % (2315527)Instruction limit reached!
% 18.11/4.40 % (2315527)------------------------------
% 18.11/4.40 % (2315527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.11/4.40 % (2315527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.11/4.40 % (2315527)CaDiCaL version: 2.1.3
% 18.11/4.40 % (2315527)Termination reason: Instruction limit
% 18.11/4.40 % (2315527)Termination phase: Property scanning
% 18.11/4.40 % (2315527)Time elapsed: 0.022 s
% 18.11/4.40 % (2315527)Peak memory usage: 91 MB
% 18.11/4.40 % (2315527)Instructions burned: 120 (million)
% 18.11/4.40 % (2315525)Instruction limit reached!
% 18.11/4.40 % (2315525)------------------------------
% 18.11/4.40 % (2315525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315525)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315525)Termination reason: Instruction limit
% 41.07/7.63 % (2315525)Termination phase: Preprocessing 1
% 41.07/7.63 % (2315525)Time elapsed: 0.061 s
% 41.07/7.63 % (2315525)Peak memory usage: 91 MB
% 41.07/7.63 % (2315525)Instructions burned: 113 (million)
% 41.07/7.63 % (2315526)Instruction limit reached!
% 41.07/7.63 % (2315526)------------------------------
% 41.07/7.63 % (2315526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315526)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315526)Termination reason: Instruction limit
% 41.07/7.63 % (2315526)Termination phase: Naming
% 41.07/7.63 % (2315526)Time elapsed: 0.072 s
% 41.07/7.63 % (2315526)Peak memory usage: 94 MB
% 41.07/7.63 % (2315526)Instructions burned: 129 (million)
% 41.07/7.63 % (2315532)lrs+10_1_sil=8000:sp=occurrence:random_seed=1749691779:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 41.07/7.63 % (2315533)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1540410701:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 41.07/7.63 % (2315534)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3745455169:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 41.07/7.63 % (2315532)Instruction limit reached!
% 41.07/7.63 % (2315532)------------------------------
% 41.07/7.63 % (2315532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315532)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315532)Termination reason: Instruction limit
% 41.07/7.63 % (2315532)Termination phase: Property scanning
% 41.07/7.63 % (2315532)Time elapsed: 0.208 s
% 41.07/7.63 % (2315532)Peak memory usage: 100 MB
% 41.07/7.63 % (2315532)Instructions burned: 913 (million)
% 41.07/7.63 % (2315533)Instruction limit reached!
% 41.07/7.63 % (2315533)------------------------------
% 41.07/7.63 % (2315533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315533)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315533)Termination reason: Instruction limit
% 41.07/7.63 % (2315533)Termination phase: Preprocessing 3
% 41.07/7.63 % (2315533)Time elapsed: 0.215 s
% 41.07/7.63 % (2315533)Peak memory usage: 100 MB
% 41.07/7.63 % (2315533)Instructions burned: 439 (million)
% 41.07/7.63 % (2315538)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1432905230:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 41.07/7.63 % (2315538)Instruction limit reached!
% 41.07/7.63 % (2315538)------------------------------
% 41.07/7.63 % (2315538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315538)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315538)Termination reason: Instruction limit
% 41.07/7.63 % (2315538)Termination phase: Preprocessing 1
% 41.07/7.63 % (2315538)Time elapsed: 0.039 s
% 41.07/7.63 % (2315538)Peak memory usage: 91 MB
% 41.07/7.63 % (2315538)Instructions burned: 135 (million)
% 41.07/7.63 % (2315539)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=782378919:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 41.07/7.63 % (2315541)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=431238028:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 41.07/7.63 % (2315523)Instruction limit reached!
% 41.07/7.63 % (2315523)------------------------------
% 41.07/7.63 % (2315523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.07/7.63 % (2315523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.07/7.63 % (2315523)CaDiCaL version: 2.1.3
% 41.07/7.63 % (2315523)Termination reason: Instruction limit
% 41.07/7.63 % (2315523)Termination phase: Twee Goal Transformation
% 41.07/7.63 % (2315523)Time elapsed: 0.890 s
% 41.07/7.63 % (2315523)Peak memory usage: 106 MB
% 41.07/7.63 % (2315523)Instructions burned: 2352 (million)
% 41.07/7.63 % (2315539)Instruction limit reached!
% 41.07/7.63 % (2315539)------------------------------
% 41.07/7.63 % (2315539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315539)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315539)Termination reason: Instruction limit
% 65.83/11.15 % (2315539)Termination phase: Preprocessing 3
% 65.83/11.15 % (2315539)Time elapsed: 0.288 s
% 65.83/11.15 % (2315539)Peak memory usage: 102 MB
% 65.83/11.15 % (2315539)Instructions burned: 592 (million)
% 65.83/11.15 % (2315544)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=3335172585:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 65.83/11.15 % (2315545)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3545301529:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 65.83/11.15 % (2315544)Instruction limit reached!
% 65.83/11.15 % (2315544)------------------------------
% 65.83/11.15 % (2315544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315544)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315544)Termination reason: Instruction limit
% 65.83/11.15 % (2315544)Termination phase: Property scanning
% 65.83/11.15 % (2315544)Time elapsed: 0.044 s
% 65.83/11.15 % (2315544)Peak memory usage: 91 MB
% 65.83/11.15 % (2315544)Instructions burned: 126 (million)
% 65.83/11.15 % (2315545)Instruction limit reached!
% 65.83/11.15 % (2315545)------------------------------
% 65.83/11.15 % (2315545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315545)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315545)Termination reason: Instruction limit
% 65.83/11.15 % (2315545)Termination phase: Property scanning
% 65.83/11.15 % (2315545)Time elapsed: 0.048 s
% 65.83/11.15 % (2315545)Peak memory usage: 91 MB
% 65.83/11.15 % (2315545)Instructions burned: 137 (million)
% 65.83/11.15 % (2315548)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=351280659:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 65.83/11.15 % (2315549)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1514078837:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2971 on theBenchmark for (2971ds/431Mi)
% 65.83/11.15 % (2315548)Instruction limit reached!
% 65.83/11.15 % (2315548)------------------------------
% 65.83/11.15 % (2315548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315548)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315548)Termination reason: Instruction limit
% 65.83/11.15 % (2315548)Termination phase: General splitting
% 65.83/11.15 % (2315548)Time elapsed: 0.072 s
% 65.83/11.15 % (2315548)Peak memory usage: 93 MB
% 65.83/11.15 % (2315548)Instructions burned: 142 (million)
% 65.83/11.15 % (2315552)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=509122452:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 65.83/11.15 % (2315549)Instruction limit reached!
% 65.83/11.15 % (2315549)------------------------------
% 65.83/11.15 % (2315549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315549)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315549)Termination reason: Instruction limit
% 65.83/11.15 % (2315549)Termination phase: Saturation
% 65.83/11.15 % (2315549)Time elapsed: 0.207 s
% 65.83/11.15 % (2315549)Peak memory usage: 96 MB
% 65.83/11.15 % (2315549)Instructions burned: 433 (million)
% 65.83/11.15 % (2315554)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=3037009994:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 65.83/11.15 % (2315554)Instruction limit reached!
% 65.83/11.15 % (2315554)------------------------------
% 65.83/11.15 % (2315554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.83/11.15 % (2315554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.83/11.15 % (2315554)CaDiCaL version: 2.1.3
% 65.83/11.15 % (2315554)Termination reason: Instruction limit
% 73.31/14.29 % (2315554)Termination phase: Preprocessing 1
% 73.31/14.29 % (2315554)Time elapsed: 0.084 s
% 73.31/14.29 % (2315554)Peak memory usage: 92 MB
% 73.31/14.29 % (2315554)Instructions burned: 150 (million)
% 73.31/14.29 % (2315556)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1863009957:i=14155:bd=all_2964 on theBenchmark for (2964ds/14155Mi)
% 73.31/14.29 % (2315534)Instruction limit reached!
% 73.31/14.29 % (2315534)------------------------------
% 73.31/14.29 % (2315534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315534)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315534)Termination reason: Instruction limit
% 73.31/14.29 % (2315534)Termination phase: Saturation
% 73.31/14.29 % (2315534)Time elapsed: 2.990 s
% 73.31/14.29 % (2315534)Peak memory usage: 260 MB
% 73.31/14.29 % (2315534)Instructions burned: 5202 (million)
% 73.31/14.29 % (2315558)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2534068324:i=667:av=off:fsr=off_2949 on theBenchmark for (2949ds/667Mi)
% 73.31/14.29 % (2315558)Instruction limit reached!
% 73.31/14.29 % (2315558)------------------------------
% 73.31/14.29 % (2315558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315558)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315558)Termination reason: Instruction limit
% 73.31/14.29 % (2315558)Termination phase: Property scanning
% 73.31/14.29 % (2315558)Time elapsed: 0.340 s
% 73.31/14.29 % (2315558)Peak memory usage: 103 MB
% 73.31/14.29 % (2315558)Instructions burned: 670 (million)
% 73.31/14.29 % (2315560)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2411441320:s2a=on:i=185:s2at=1.8:fdi=4_2944 on theBenchmark for (2944ds/185Mi)
% 73.31/14.29 % (2315560)Instruction limit reached!
% 73.31/14.29 % (2315560)------------------------------
% 73.31/14.29 % (2315560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315560)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315560)Termination reason: Instruction limit
% 73.31/14.29 % (2315560)Termination phase: Preprocessing 1
% 73.31/14.29 % (2315560)Time elapsed: 0.096 s
% 73.31/14.29 % (2315560)Peak memory usage: 91 MB
% 73.31/14.29 % (2315560)Instructions burned: 187 (million)
% 73.31/14.29 % (2315562)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3745039840:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2941 on theBenchmark for (2941ds/193Mi)
% 73.31/14.29 % (2315562)Instruction limit reached!
% 73.31/14.29 % (2315562)------------------------------
% 73.31/14.29 % (2315562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315562)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315562)Termination reason: Instruction limit
% 73.31/14.29 % (2315562)Termination phase: SInE selection
% 73.31/14.29 % (2315562)Time elapsed: 0.100 s
% 73.31/14.29 % (2315562)Peak memory usage: 90 MB
% 73.31/14.29 % (2315562)Instructions burned: 194 (million)
% 73.31/14.29 % (2315564)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=820035883:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2938 on theBenchmark for (2938ds/4850Mi)
% 73.31/14.29 % (2315541)Instruction limit reached!
% 73.31/14.29 % (2315541)------------------------------
% 73.31/14.29 % (2315541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315541)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315541)Termination reason: Instruction limit
% 73.31/14.29 % (2315541)Termination phase: Saturation
% 73.31/14.29 % (2315541)Time elapsed: 4.254 s
% 73.31/14.29 % (2315541)Peak memory usage: 278 MB
% 73.31/14.29 % (2315541)Instructions burned: 13195 (million)
% 73.31/14.29 % (2315552)Instruction limit reached!
% 73.31/14.29 % (2315552)------------------------------
% 73.31/14.29 % (2315552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315552)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315552)Termination reason: Instruction limit
% 73.31/14.29 % (2315552)Termination phase: Saturation
% 73.31/14.29 % (2315552)Time elapsed: 3.507 s
% 73.31/14.29 % (2315552)Peak memory usage: 338 MB
% 73.31/14.29 % (2315552)Instructions burned: 6060 (million)
% 73.31/14.29 % (2315566)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2297280217:i=12111:sd=1:ss=included_2932 on theBenchmark for (2932ds/12111Mi)
% 73.31/14.29 % (2315567)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3262342774:i=319:kws=precedence:fsr=off_2932 on theBenchmark for (2932ds/319Mi)
% 73.31/14.29 % (2315567)Instruction limit reached!
% 73.31/14.29 % (2315567)------------------------------
% 73.31/14.29 % (2315567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315567)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315567)Termination reason: Instruction limit
% 73.31/14.29 % (2315567)Termination phase: Preprocessing 3
% 73.31/14.29 % (2315567)Time elapsed: 0.171 s
% 73.31/14.29 % (2315567)Peak memory usage: 100 MB
% 73.31/14.29 % (2315567)Instructions burned: 326 (million)
% 73.31/14.29 % (2315570)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3218909704:i=2064:ep=RST_2928 on theBenchmark for (2928ds/2064Mi)
% 73.31/14.29 % (2315570)Instruction limit reached!
% 73.31/14.29 % (2315570)------------------------------
% 73.31/14.29 % (2315570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315570)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315570)Termination reason: Instruction limit
% 73.31/14.29 % (2315570)Termination phase: Property scanning
% 73.31/14.29 % (2315570)Time elapsed: 0.800 s
% 73.31/14.29 % (2315570)Peak memory usage: 108 MB
% 73.31/14.29 % (2315570)Instructions burned: 2065 (million)
% 73.31/14.29 % (2315572)dis-1011_128_sil=32000:random_seed=3121718931:i=3706:ep=RST:av=off_2918 on theBenchmark for (2918ds/3706Mi)
% 73.31/14.29 % (2315564)Instruction limit reached!
% 73.31/14.29 % (2315564)------------------------------
% 73.31/14.29 % (2315564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315564)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315564)Termination reason: Instruction limit
% 73.31/14.29 % (2315564)Termination phase: Saturation
% 73.31/14.29 % (2315564)Time elapsed: 2.511 s
% 73.31/14.29 % (2315564)Peak memory usage: 135 MB
% 73.31/14.29 % (2315564)Instructions burned: 4850 (million)
% 73.31/14.29 % (2315574)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1183677896:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2911 on theBenchmark for (2911ds/757Mi)
% 73.31/14.29 % (2315574)Instruction limit reached!
% 73.31/14.29 % (2315574)------------------------------
% 73.31/14.29 % (2315574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315574)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315574)Termination reason: Instruction limit
% 73.31/14.29 % (2315574)Termination phase: Property scanning
% 73.31/14.29 % (2315574)Time elapsed: 0.297 s
% 73.31/14.29 % (2315574)Peak memory usage: 96 MB
% 73.31/14.29 % (2315574)Instructions burned: 757 (million)
% 73.31/14.29 % (2315576)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2806292460:i=13913:ss=axioms:sgt=8_2907 on theBenchmark for (2907ds/13913Mi)
% 73.31/14.29 % (2315572)Instruction limit reached!
% 73.31/14.29 % (2315572)------------------------------
% 73.31/14.29 % (2315572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315572)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315572)Termination reason: Instruction limit
% 73.31/14.29 % (2315572)Termination phase: Saturation
% 73.31/14.29 % (2315572)Time elapsed: 1.549 s
% 73.31/14.29 % (2315572)Peak memory usage: 115 MB
% 73.31/14.29 % (2315572)Instructions burned: 3707 (million)
% 73.31/14.29 % (2315578)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3576080848:i=9925:aac=none_2901 on theBenchmark for (2901ds/9925Mi)
% 73.31/14.29 % (2315566)Instruction limit reached!
% 73.31/14.29 % (2315566)------------------------------
% 73.31/14.29 % (2315566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315566)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315566)Termination reason: Instruction limit
% 73.31/14.29 % (2315566)Termination phase: Saturation
% 73.31/14.29 % (2315566)Time elapsed: 3.439 s
% 73.31/14.29 % (2315566)Peak memory usage: 240 MB
% 73.31/14.29 % (2315566)Instructions burned: 12115 (million)
% 73.31/14.29 % (2315580)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2033406453:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2897 on theBenchmark for (2897ds/2479Mi)
% 73.31/14.29 % (2315580)Instruction limit reached!
% 73.31/14.29 % (2315580)------------------------------
% 73.31/14.29 % (2315580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315580)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315580)Termination reason: Instruction limit
% 73.31/14.29 % (2315580)Termination phase: Saturation
% 73.31/14.29 % (2315580)Time elapsed: 0.673 s
% 73.31/14.29 % (2315580)Peak memory usage: 106 MB
% 73.31/14.29 % (2315580)Instructions burned: 2482 (million)
% 73.31/14.29 % (2315582)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1263362777:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2889 on theBenchmark for (2889ds/440Mi)
% 73.31/14.29 % (2315582)Instruction limit reached!
% 73.31/14.29 % (2315582)------------------------------
% 73.31/14.29 % (2315582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315582)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315582)Termination reason: Instruction limit
% 73.31/14.29 % (2315582)Termination phase: Property scanning
% 73.31/14.29 % (2315582)Time elapsed: 0.080 s
% 73.31/14.29 % (2315582)Peak memory usage: 91 MB
% 73.31/14.29 % (2315582)Instructions burned: 441 (million)
% 73.31/14.29 % (2315556)Instruction limit reached!
% 73.31/14.29 % (2315556)------------------------------
% 73.31/14.29 % (2315556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.31/14.29 % (2315556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.31/14.29 % (2315556)CaDiCaL version: 2.1.3
% 73.31/14.29 % (2315556)Termination reason: Instruction limit
% 73.31/14.29 % (2315556)Termination phase: Saturation
% 73.31/14.29 % (2315556)Time elapsed: 7.698 s
% 73.31/14.29 % (2315556)Peak memory usage: 370 MB
% 73.31/14.29 % (2315556)Instructions burned: 14155 (million)
% 73.31/14.29 % (2315584)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2162253639:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2886 on theBenchmark for (2886ds/11145Mi)
% 73.31/14.29 % (2315585)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1553334375:cts=off:i=3034:av=off:er=known:fsd=on_2885 on theBenchmark for (2885ds/3034Mi)
% 73.31/14.29 % (2315500)First to succeed.
% 73.31/14.29 % (2315500)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2315495"
% 73.31/14.29 % (2315500)Refutation found. Thanks to Tanya!
% 73.31/14.29 % SZS status Theorem for theBenchmark
% 73.31/14.29 % SZS output start Proof for theBenchmark
% See solution above
% 86.03/14.49 % (2315500)------------------------------
% 86.03/14.49 % (2315500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.03/14.49 % (2315500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.03/14.49 % (2315500)CaDiCaL version: 2.1.3
% 86.03/14.49 % (2315500)Termination reason: Refutation
% 86.03/14.49 % (2315500)Time elapsed: 11.482 s
% 86.03/14.49 % (2315500)Peak memory usage: 448 MB
% 86.03/14.49 % (2315500)Instructions burned: 20884 (million)
% 86.03/14.49 % (2315500)------------------------------
% 86.03/14.49 % (2315500)------------------------------
% 86.03/14.49 % (2315495)Success in time 13.415 s
% 86.03/14.49 % Vampire exiting
%------------------------------------------------------------------------------