%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM862+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 12:17:19 PM UTC 2026
% Result : Theorem 54.34s 16.31s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 38
% Syntax : Number of formulae : 308 ( 16 unt; 24 def)
% Number of atoms : 882 ( 28 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1005 ( 431 ~; 487 |; 47 &)
% ( 35 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 25 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 222 ( 0 sgn 207 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : lesseq(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lesseq_ref) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( lesseq(X0,X1)
& lesseq(X1,X2) )
=> lesseq(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lesseq_trans) ).
fof(f3,axiom,
! [X0,X1] :
( ( lesseq(X0,X1)
& lesseq(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lesseq_antisymmetric) ).
fof(f4,axiom,
! [X0,X1] :
( lesseq(X0,X1)
| lesseq(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lesseq_total) ).
fof(f5,axiom,
! [X0,X1,X2] :
( lesseq(X0,X1)
<=> lesseq(sum(X2,X0),sum(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_monotone_1) ).
fof(f6,axiom,
! [X0,X1] :
( lesseq(X0,X1)
<=> lesseq(summation(X0),summation(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',summation_monotone) ).
fof(f7,axiom,
! [X0,X1] :
( max(X0,X1) = X0
| ~ lesseq(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_1) ).
fof(f8,axiom,
! [X0,X1] :
( max(X0,X1) = X1
| ~ lesseq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_2) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ub(X0,X1,X2)
<=> ( lesseq(X0,X2)
& lesseq(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ub) ).
fof(f10,axiom,
! [X0,X1,X2] :
( model_max(X0,X1,X2)
<=> lesseq(sum(c,summation(max(X0,X1))),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_max_5) ).
fof(f11,axiom,
! [X0,X1,X2] :
( model_ub(X0,X1,X2)
<=> ? [X3] :
( ub(X0,X1,X3)
& lesseq(sum(c,summation(X3)),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',model_ub_5) ).
fof(f12,axiom,
! [X0,X1,X2] :
( minsol_model_max(X0,X1,X2)
<=> ( model_max(X0,X1,X2)
& ! [X3] :
( model_max(X0,X1,X3)
=> lesseq(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minsol_model_max) ).
fof(f13,axiom,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> ( model_ub(X0,X1,X2)
& ! [X3] :
( model_ub(X0,X1,X3)
=> lesseq(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minsol_model_ub) ).
fof(f14,conjecture,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',max_is_ub_1) ).
fof(f15,negated_conjecture,
~ ! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> minsol_model_max(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f16,plain,
! [X0,X1,X2] :
( lesseq(X0,X2)
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f17,plain,
! [X0,X1,X2] :
( lesseq(X0,X2)
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X2) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
! [X0,X1] :
( X0 = X1
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f19,plain,
! [X0,X1] :
( X0 = X1
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X0) ),
inference(flattening,[],[f18]) ).
fof(f20,plain,
! [X0,X1,X2] :
( minsol_model_max(X0,X1,X2)
<=> ( model_max(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3) ) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f21,plain,
! [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<=> ( model_ub(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3) ) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f22,plain,
? [X0,X1,X2] :
( minsol_model_ub(X0,X1,X2)
<~> minsol_model_max(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f23,plain,
! [X0,X1,X2] :
( ( lesseq(X0,X1)
| ~ lesseq(sum(X2,X0),sum(X2,X1)) )
& ( lesseq(sum(X2,X0),sum(X2,X1))
| ~ lesseq(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f24,plain,
! [X0,X1] :
( ( lesseq(X0,X1)
| ~ lesseq(summation(X0),summation(X1)) )
& ( lesseq(summation(X0),summation(X1))
| ~ lesseq(X0,X1) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ( ub(X0,X1,X2)
| ~ lesseq(X0,X2)
| ~ lesseq(X1,X2) )
& ( ( lesseq(X0,X2)
& lesseq(X1,X2) )
| ~ ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f26,plain,
! [X0,X1,X2] :
( ( ub(X0,X1,X2)
| ~ lesseq(X0,X2)
| ~ lesseq(X1,X2) )
& ( ( lesseq(X0,X2)
& lesseq(X1,X2) )
| ~ ub(X0,X1,X2) ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0,X1,X2] :
( ( model_max(X0,X1,X2)
| ~ lesseq(sum(c,summation(max(X0,X1))),X2) )
& ( lesseq(sum(c,summation(max(X0,X1))),X2)
| ~ model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f28,plain,
! [X0,X1,X2] :
( ( model_ub(X0,X1,X2)
| ! [X3] :
( ~ ub(X0,X1,X3)
| ~ lesseq(sum(c,summation(X3)),X2) ) )
& ( ? [X3] :
( ub(X0,X1,X3)
& lesseq(sum(c,summation(X3)),X2) )
| ~ model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ( model_ub(X0,X1,X2)
| ! [X3] :
( ~ ub(X0,X1,X3)
| ~ lesseq(sum(c,summation(X3)),X2) ) )
& ( ? [X4] :
( ub(X0,X1,X4)
& lesseq(sum(c,summation(X4)),X2) )
| ~ model_ub(X0,X1,X2) ) ),
inference(rectify,[],[f28]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ( model_ub(X0,X1,X2)
| ! [X3] :
( ~ ub(X0,X1,X3)
| ~ lesseq(sum(c,summation(X3)),X2) ) )
& ( ( ub(X0,X1,sK0(X0,X1,X2))
& lesseq(sum(c,summation(sK0(X0,X1,X2))),X2) )
| ~ model_ub(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X4,sK0(X0,X1,X2))],[f29]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_max(X0,X1,X3) ) )
& ( ( model_max(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3) ) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_max(X0,X1,X3) ) )
& ( ( model_max(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_max(X0,X1,X3) ) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_max(X0,X1,X3) ) )
& ( ( model_max(X0,X1,X2)
& ! [X4] :
( lesseq(X2,X4)
| ~ model_max(X0,X1,X4) ) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(rectify,[],[f32]) ).
fof(f34,plain,
! [X0,X1,X2] :
( ( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| ( ~ lesseq(X2,sK1(X0,X1,X2))
& model_max(X0,X1,sK1(X0,X1,X2)) ) )
& ( ( model_max(X0,X1,X2)
& ! [X4] :
( lesseq(X2,X4)
| ~ model_max(X0,X1,X4) ) )
| ~ minsol_model_max(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f33]) ).
fof(f35,plain,
! [X0,X1,X2] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_ub(X0,X1,X3) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_ub(X0,X1,X3) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X3] :
( lesseq(X2,X3)
| ~ model_ub(X0,X1,X3) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ? [X3] :
( ~ lesseq(X2,X3)
& model_ub(X0,X1,X3) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X4] :
( lesseq(X2,X4)
| ~ model_ub(X0,X1,X4) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(rectify,[],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( ( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ( ~ lesseq(X2,sK2(X0,X1,X2))
& model_ub(X0,X1,sK2(X0,X1,X2)) ) )
& ( ( model_ub(X0,X1,X2)
& ! [X4] :
( lesseq(X2,X4)
| ~ model_ub(X0,X1,X4) ) )
| ~ minsol_model_ub(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f37]) ).
fof(f39,plain,
? [X0,X1,X2] :
( ( ~ minsol_model_max(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) )
& ( minsol_model_max(X0,X1,X2)
| minsol_model_ub(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f40,plain,
( ( ~ minsol_model_max(sK3,sK4,sK5)
| ~ minsol_model_ub(sK3,sK4,sK5) )
& ( minsol_model_max(sK3,sK4,sK5)
| minsol_model_ub(sK3,sK4,sK5) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f39]) ).
fof(f41,plain,
! [X0] : lesseq(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f42,plain,
! [X2,X0,X1] :
( lesseq(X0,X2)
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X2) ),
inference(cnf_transformation,[],[f17]) ).
fof(f43,plain,
! [X0,X1] :
( X0 = X1
| ~ lesseq(X0,X1)
| ~ lesseq(X1,X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f44,plain,
! [X0,X1] :
( lesseq(X0,X1)
| lesseq(X1,X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f45,plain,
! [X2,X0,X1] :
( lesseq(sum(X2,X0),sum(X2,X1))
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f47,plain,
! [X0,X1] :
( lesseq(summation(X0),summation(X1))
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f24]) ).
fof(f49,plain,
! [X0,X1] :
( max(X0,X1) = X0
| ~ lesseq(X1,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f50,plain,
! [X0,X1] :
( max(X0,X1) = X1
| ~ lesseq(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
fof(f51,plain,
! [X2,X0,X1] :
( lesseq(X1,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f52,plain,
! [X2,X0,X1] :
( lesseq(X0,X2)
| ~ ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f53,plain,
! [X2,X0,X1] :
( ub(X0,X1,X2)
| ~ lesseq(X0,X2)
| ~ lesseq(X1,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f54,plain,
! [X2,X0,X1] :
( lesseq(sum(c,summation(max(X0,X1))),X2)
| ~ model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f55,plain,
! [X2,X0,X1] :
( model_max(X0,X1,X2)
| ~ lesseq(sum(c,summation(max(X0,X1))),X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f56,plain,
! [X2,X0,X1] :
( lesseq(sum(c,summation(sK0(X0,X1,X2))),X2)
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ub(X0,X1,sK0(X0,X1,X2))
| ~ model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f58,plain,
! [X2,X3,X0,X1] :
( model_ub(X0,X1,X2)
| ~ ub(X0,X1,X3)
| ~ lesseq(sum(c,summation(X3)),X2) ),
inference(cnf_transformation,[],[f30]) ).
fof(f59,plain,
! [X2,X0,X1,X4] :
( lesseq(X2,X4)
| ~ model_max(X0,X1,X4)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f60,plain,
! [X2,X0,X1] :
( model_max(X0,X1,X2)
| ~ minsol_model_max(X0,X1,X2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f61,plain,
! [X2,X0,X1] :
( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| model_max(X0,X1,sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f34]) ).
fof(f62,plain,
! [X2,X0,X1] :
( minsol_model_max(X0,X1,X2)
| ~ model_max(X0,X1,X2)
| ~ lesseq(X2,sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f34]) ).
fof(f63,plain,
! [X2,X0,X1,X4] :
( lesseq(X2,X4)
| ~ model_ub(X0,X1,X4)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f64,plain,
! [X2,X0,X1] :
( model_ub(X0,X1,X2)
| ~ minsol_model_ub(X0,X1,X2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f65,plain,
! [X2,X0,X1] :
( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| model_ub(X0,X1,sK2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f66,plain,
! [X2,X0,X1] :
( minsol_model_ub(X0,X1,X2)
| ~ model_ub(X0,X1,X2)
| ~ lesseq(X2,sK2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f67,plain,
( minsol_model_max(sK3,sK4,sK5)
| minsol_model_ub(sK3,sK4,sK5) ),
inference(cnf_transformation,[],[f40]) ).
fof(f68,plain,
( ~ minsol_model_max(sK3,sK4,sK5)
| ~ minsol_model_ub(sK3,sK4,sK5) ),
inference(cnf_transformation,[],[f40]) ).
fof(f70,definition,
( spl6_1
<=> minsol_model_ub(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition]) ).
fof(f71,plain,
( minsol_model_ub(sK3,sK4,sK5)
| ~ spl6_1 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f73,definition,
( spl6_2
<=> minsol_model_max(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f74,plain,
( minsol_model_max(sK3,sK4,sK5)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f73]) ).
fof(f75,plain,
( spl6_1
| spl6_2 ),
inference(avatar_split_clause,[],[f67,f73,f70]) ).
fof(f76,plain,
( ~ minsol_model_ub(sK3,sK4,sK5)
| spl6_1 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f77,plain,
( ~ minsol_model_max(sK3,sK4,sK5)
| spl6_2 ),
inference(avatar_component_clause,[],[f73]) ).
fof(f78,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f68,f73,f70]) ).
fof(f80,plain,
( model_max(sK3,sK4,sK5)
| ~ spl6_2 ),
inference(resolution,[],[f74,f60]) ).
fof(f84,plain,
( lesseq(sum(c,summation(max(sK3,sK4))),sK5)
| ~ spl6_2 ),
inference(resolution,[],[f80,f54]) ).
fof(f89,plain,
( sK5 = sum(c,summation(max(sK3,sK4)))
| ~ lesseq(sK5,sum(c,summation(max(sK3,sK4))))
| ~ spl6_2 ),
inference(resolution,[],[f84,f43]) ).
fof(f97,plain,
( lesseq(sum(c,summation(sK4)),sK5)
| ~ lesseq(sK3,sK4)
| ~ spl6_2 ),
inference(superposition,[],[f84,f50]) ).
fof(f98,plain,
( lesseq(sum(c,summation(sK3)),sK5)
| ~ lesseq(sK4,sK3)
| ~ spl6_2 ),
inference(superposition,[],[f84,f49]) ).
fof(f100,definition,
( spl6_3
<=> lesseq(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
fof(f101,plain,
( ~ lesseq(sK4,sK3)
| spl6_3 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,definition,
( spl6_4
<=> lesseq(sum(c,summation(sK3)),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f104,plain,
( lesseq(sum(c,summation(sK3)),sK5)
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f105,plain,
( ~ spl6_3
| spl6_4
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f98,f73,f103,f100]) ).
fof(f107,definition,
( spl6_5
<=> lesseq(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition]) ).
fof(f108,plain,
( ~ lesseq(sK3,sK4)
| spl6_5 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,definition,
( spl6_6
<=> lesseq(sum(c,summation(sK4)),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f111,plain,
( lesseq(sum(c,summation(sK4)),sK5)
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f112,plain,
( ~ spl6_5
| spl6_6
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f97,f73,f110,f107]) ).
fof(f114,definition,
( spl6_7
<=> lesseq(sK5,sum(c,summation(max(sK3,sK4)))) ),
introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition]) ).
fof(f115,plain,
( ~ lesseq(sK5,sum(c,summation(max(sK3,sK4))))
| spl6_7 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f117,definition,
( spl6_8
<=> sK5 = sum(c,summation(max(sK3,sK4))) ),
introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition]) ).
fof(f118,plain,
( sK5 = sum(c,summation(max(sK3,sK4)))
| ~ spl6_8 ),
inference(avatar_component_clause,[],[f117]) ).
fof(f120,plain,
( ~ spl6_7
| spl6_8
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f89,f73,f117,f114]) ).
fof(f121,plain,
( ~ model_ub(sK3,sK4,sK5)
| model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| spl6_1 ),
inference(resolution,[],[f76,f65]) ).
fof(f122,plain,
( ~ model_ub(sK3,sK4,sK5)
| ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_1 ),
inference(resolution,[],[f76,f66]) ).
fof(f124,definition,
( spl6_9
<=> lesseq(sK5,sK2(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
fof(f125,plain,
( ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_9 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f127,definition,
( spl6_10
<=> model_ub(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
fof(f128,plain,
( ~ model_ub(sK3,sK4,sK5)
| spl6_10 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f129,plain,
( ~ spl6_9
| ~ spl6_10
| spl6_1 ),
inference(avatar_split_clause,[],[f122,f70,f127,f124]) ).
fof(f131,definition,
( spl6_11
<=> model_ub(sK3,sK4,sK2(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_11])],[avatar_definition]) ).
fof(f132,plain,
( model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| ~ spl6_11 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f133,plain,
( spl6_11
| ~ spl6_10
| spl6_1 ),
inference(avatar_split_clause,[],[f121,f70,f127,f131]) ).
fof(f177,plain,
( lesseq(sK4,sK3)
| spl6_5 ),
inference(resolution,[],[f108,f44]) ).
fof(f178,plain,
( lesseq(sK4,sK3)
| spl6_5 ),
inference(resolution,[],[f108,f44]) ).
fof(f187,plain,
( $false
| spl6_3
| spl6_5 ),
inference(forward_subsumption_resolution,[],[f177,f101]) ).
fof(f188,plain,
( spl6_3
| spl6_5 ),
inference(avatar_contradiction_clause,[],[f187]) ).
fof(f192,plain,
( model_ub(sK3,sK4,sK5)
| ~ spl6_1 ),
inference(resolution,[],[f71,f64]) ).
fof(f196,plain,
( lesseq(sum(c,summation(sK0(sK3,sK4,sK5))),sK5)
| ~ spl6_1 ),
inference(resolution,[],[f192,f56]) ).
fof(f197,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ spl6_1 ),
inference(resolution,[],[f192,f57]) ).
fof(f200,plain,
( lesseq(sK3,sK0(sK3,sK4,sK5))
| ~ spl6_1 ),
inference(resolution,[],[f197,f52]) ).
fof(f204,plain,
( sK5 = sum(c,summation(sK0(sK3,sK4,sK5)))
| ~ lesseq(sK5,sum(c,summation(sK0(sK3,sK4,sK5))))
| ~ spl6_1 ),
inference(resolution,[],[f196,f43]) ).
fof(f213,definition,
( spl6_14
<=> lesseq(sK5,sum(c,summation(sK0(sK3,sK4,sK5)))) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
fof(f214,plain,
( ~ lesseq(sK5,sum(c,summation(sK0(sK3,sK4,sK5))))
| spl6_14 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,definition,
( spl6_15
<=> sK5 = sum(c,summation(sK0(sK3,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl6_15])],[avatar_definition]) ).
fof(f217,plain,
( sK5 = sum(c,summation(sK0(sK3,sK4,sK5)))
| ~ spl6_15 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
( ~ spl6_14
| spl6_15
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f204,f70,f216,f213]) ).
fof(f221,plain,
( ~ model_max(sK3,sK4,sK5)
| ~ lesseq(sK5,sK1(sK3,sK4,sK5))
| spl6_2 ),
inference(resolution,[],[f77,f62]) ).
fof(f223,definition,
( spl6_16
<=> lesseq(sK5,sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_16])],[avatar_definition]) ).
fof(f224,plain,
( ~ lesseq(sK5,sK1(sK3,sK4,sK5))
| spl6_16 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,definition,
( spl6_17
<=> model_max(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_17])],[avatar_definition]) ).
fof(f227,plain,
( ~ model_max(sK3,sK4,sK5)
| spl6_17 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( ~ spl6_16
| ~ spl6_17
| spl6_2 ),
inference(avatar_split_clause,[],[f221,f73,f226,f223]) ).
fof(f230,definition,
( spl6_18
<=> model_max(sK3,sK4,sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition]) ).
fof(f231,plain,
( model_max(sK3,sK4,sK1(sK3,sK4,sK5))
| ~ spl6_18 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f253,plain,
( sK3 = sK0(sK3,sK4,sK5)
| ~ lesseq(sK0(sK3,sK4,sK5),sK3)
| ~ spl6_1 ),
inference(resolution,[],[f200,f43]) ).
fof(f262,definition,
( spl6_21
<=> lesseq(sK0(sK3,sK4,sK5),sK3) ),
introduced(definition,[new_symbols(definition,[spl6_21])],[avatar_definition]) ).
fof(f263,plain,
( ~ lesseq(sK0(sK3,sK4,sK5),sK3)
| spl6_21 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f265,definition,
( spl6_22
<=> sK3 = sK0(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_22])],[avatar_definition]) ).
fof(f266,plain,
( sK3 = sK0(sK3,sK4,sK5)
| ~ spl6_22 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
( ~ spl6_21
| spl6_22
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f253,f70,f265,f262]) ).
fof(f278,plain,
( ! [X0] :
( lesseq(sK4,X0)
| ~ lesseq(sK3,X0) )
| spl6_5 ),
inference(resolution,[],[f178,f42]) ).
fof(f284,plain,
( sK3 = max(sK3,sK4)
| spl6_5 ),
inference(resolution,[],[f178,f49]) ).
fof(f376,plain,
( lesseq(sK3,sK0(sK3,sK4,sK5))
| spl6_21 ),
inference(resolution,[],[f263,f44]) ).
fof(f670,plain,
( ! [X0] :
( ~ lesseq(sum(c,summation(X0)),sK5)
| ~ ub(sK3,sK4,X0) )
| spl6_10 ),
inference(resolution,[],[f128,f58]) ).
fof(f682,plain,
( sK5 = sum(c,summation(sK3))
| ~ lesseq(sK5,sum(c,summation(sK3)))
| ~ spl6_4 ),
inference(resolution,[],[f104,f43]) ).
fof(f703,plain,
( ~ ub(sK3,sK4,sK3)
| ~ spl6_4
| spl6_10 ),
inference(resolution,[],[f670,f104]) ).
fof(f715,plain,
( ~ lesseq(sK3,sK3)
| ~ lesseq(sK4,sK3)
| ~ spl6_4
| spl6_10 ),
inference(resolution,[],[f703,f53]) ).
fof(f758,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ spl6_1 ),
inference(resolution,[],[f192,f57]) ).
fof(f775,plain,
( ! [X0] :
( ~ lesseq(sum(c,summation(sK0(sK3,sK4,sK5))),X0)
| model_ub(sK3,sK4,X0) )
| ~ spl6_1 ),
inference(resolution,[],[f758,f58]) ).
fof(f787,plain,
( ! [X0] :
( ~ model_ub(sK3,sK4,X0)
| lesseq(sK5,X0) )
| ~ spl6_1 ),
inference(resolution,[],[f71,f63]) ).
fof(f1138,definition,
( spl6_57
<=> lesseq(sK5,sum(c,summation(sK3))) ),
introduced(definition,[new_symbols(definition,[spl6_57])],[avatar_definition]) ).
fof(f1139,plain,
( ~ lesseq(sK5,sum(c,summation(sK3)))
| spl6_57 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1141,definition,
( spl6_58
<=> sK5 = sum(c,summation(sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_58])],[avatar_definition]) ).
fof(f1142,plain,
( sK5 = sum(c,summation(sK3))
| ~ spl6_58 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1144,plain,
( ~ spl6_57
| spl6_58
| ~ spl6_4 ),
inference(avatar_split_clause,[],[f682,f103,f1141,f1138]) ).
fof(f1146,plain,
( ~ lesseq(sum(c,summation(max(sK3,sK4))),sK5)
| spl6_17 ),
inference(resolution,[],[f227,f55]) ).
fof(f1147,plain,
( ~ lesseq(sum(c,summation(sK3)),sK5)
| spl6_5
| spl6_17 ),
inference(forward_demodulation,[],[f1146,f284]) ).
fof(f1184,plain,
( model_ub(sK3,sK4,sum(c,summation(sK0(sK3,sK4,sK5))))
| ~ spl6_1 ),
inference(resolution,[],[f775,f41]) ).
fof(f1385,definition,
( spl6_70
<=> ub(sK3,sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_70])],[avatar_definition]) ).
fof(f1386,plain,
( ~ ub(sK3,sK4,sK3)
| spl6_70 ),
inference(avatar_component_clause,[],[f1385]) ).
fof(f1408,plain,
( ~ lesseq(sK3,sK3)
| ~ lesseq(sK4,sK3)
| spl6_70 ),
inference(resolution,[],[f1386,f53]) ).
fof(f1409,plain,
( ~ lesseq(sK3,sK3)
| spl6_5
| spl6_70 ),
inference(forward_subsumption_resolution,[],[f1408,f278]) ).
fof(f1410,plain,
( $false
| spl6_5
| spl6_70 ),
inference(forward_subsumption_resolution,[],[f1409,f41]) ).
fof(f1411,plain,
( spl6_5
| spl6_70 ),
inference(avatar_contradiction_clause,[],[f1410]) ).
fof(f1592,plain,
( lesseq(sK5,sum(c,summation(sK0(sK3,sK4,sK5))))
| ~ spl6_1 ),
inference(resolution,[],[f1184,f787]) ).
fof(f1609,plain,
( $false
| ~ spl6_1
| spl6_14 ),
inference(forward_subsumption_resolution,[],[f1592,f214]) ).
fof(f1610,plain,
( ~ spl6_1
| spl6_14 ),
inference(avatar_contradiction_clause,[],[f1609]) ).
fof(f1623,plain,
( ! [X0] :
( ~ lesseq(X0,summation(sK0(sK3,sK4,sK5)))
| lesseq(sum(c,X0),sK5) )
| ~ spl6_15 ),
inference(superposition,[],[f45,f217]) ).
fof(f1706,plain,
( ! [X0] :
( ~ lesseq(X0,sK0(sK3,sK4,sK5))
| lesseq(sum(c,summation(X0)),sK5) )
| ~ spl6_15 ),
inference(resolution,[],[f1623,f47]) ).
fof(f1724,plain,
( lesseq(sum(c,summation(sK3)),sK5)
| ~ spl6_15
| spl6_21 ),
inference(resolution,[],[f1706,f376]) ).
fof(f1728,plain,
( $false
| spl6_5
| ~ spl6_15
| spl6_17
| spl6_21 ),
inference(forward_subsumption_resolution,[],[f1724,f1147]) ).
fof(f1729,plain,
( spl6_5
| ~ spl6_15
| spl6_17
| spl6_21 ),
inference(avatar_contradiction_clause,[],[f1728]) ).
fof(f1740,plain,
( ! [X0,X1] :
( ~ ub(X0,X1,sK4)
| model_ub(X0,X1,sK5) )
| ~ spl6_6 ),
inference(resolution,[],[f111,f58]) ).
fof(f1755,definition,
( spl6_90
<=> sK5 = sum(c,summation(sK4)) ),
introduced(definition,[new_symbols(definition,[spl6_90])],[avatar_definition]) ).
fof(f1756,plain,
( sK5 = sum(c,summation(sK4))
| ~ spl6_90 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1773,plain,
( lesseq(sum(c,summation(sK3)),sK5)
| ~ model_ub(sK3,sK4,sK5)
| ~ spl6_22 ),
inference(superposition,[],[f56,f266]) ).
fof(f1776,plain,
( ~ model_ub(sK3,sK4,sK5)
| spl6_5
| spl6_17
| ~ spl6_22 ),
inference(forward_subsumption_resolution,[],[f1773,f1147]) ).
fof(f1780,plain,
( $false
| ~ spl6_1
| spl6_5
| spl6_17
| ~ spl6_22 ),
inference(forward_subsumption_resolution,[],[f1776,f192]) ).
fof(f1781,plain,
( ~ spl6_1
| spl6_5
| spl6_17
| ~ spl6_22 ),
inference(avatar_contradiction_clause,[],[f1780]) ).
fof(f1794,plain,
( lesseq(sum(c,summation(sK0(sK3,sK4,sK2(sK3,sK4,sK5)))),sK2(sK3,sK4,sK5))
| ~ spl6_11 ),
inference(resolution,[],[f132,f56]) ).
fof(f1795,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_11 ),
inference(resolution,[],[f132,f57]) ).
fof(f1804,plain,
( ! [X0] :
( ~ lesseq(X0,sum(c,summation(sK0(sK3,sK4,sK2(sK3,sK4,sK5)))))
| lesseq(X0,sK2(sK3,sK4,sK5)) )
| ~ spl6_11 ),
inference(resolution,[],[f1794,f42]) ).
fof(f1838,plain,
( lesseq(sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_11 ),
inference(resolution,[],[f1795,f51]) ).
fof(f1839,plain,
( lesseq(sK3,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_11 ),
inference(resolution,[],[f1795,f52]) ).
fof(f1840,plain,
( ! [X0] :
( ~ model_max(sK3,sK4,X0)
| lesseq(sK5,X0) )
| ~ spl6_2 ),
inference(resolution,[],[f74,f59]) ).
fof(f1861,plain,
( ! [X0] :
( ~ lesseq(sum(c,summation(max(sK3,sK4))),X0)
| lesseq(sK5,X0) )
| ~ spl6_2 ),
inference(resolution,[],[f1840,f55]) ).
fof(f1863,plain,
( ! [X0] :
( ~ lesseq(sum(c,summation(sK3)),X0)
| lesseq(sK5,X0) )
| ~ spl6_2
| spl6_5 ),
inference(forward_demodulation,[],[f1861,f284]) ).
fof(f1888,plain,
( lesseq(summation(sK4),summation(sK0(sK3,sK4,sK2(sK3,sK4,sK5))))
| ~ spl6_11 ),
inference(resolution,[],[f1838,f47]) ).
fof(f1916,plain,
( lesseq(summation(sK3),summation(sK0(sK3,sK4,sK2(sK3,sK4,sK5))))
| ~ spl6_11 ),
inference(resolution,[],[f1839,f47]) ).
fof(f1939,plain,
( ! [X0] :
( ~ lesseq(X0,summation(sK0(sK3,sK4,sK2(sK3,sK4,sK5))))
| lesseq(sum(c,X0),sK2(sK3,sK4,sK5)) )
| ~ spl6_11 ),
inference(resolution,[],[f1804,f45]) ).
fof(f1965,plain,
( ! [X0,X1] :
( ~ ub(X0,X1,sK3)
| model_ub(X0,X1,sK5) )
| ~ spl6_4 ),
inference(resolution,[],[f104,f58]) ).
fof(f2285,plain,
( ub(sK3,sK4,sK3)
| ~ spl6_70 ),
inference(avatar_component_clause,[],[f1385]) ).
fof(f2288,plain,
( lesseq(sK4,sK3)
| ~ spl6_70 ),
inference(resolution,[],[f2285,f51]) ).
fof(f2447,plain,
( ! [X0,X1] :
( model_ub(X0,X1,sK5)
| ~ lesseq(X0,sK4)
| ~ lesseq(X1,sK4) )
| ~ spl6_6 ),
inference(resolution,[],[f1740,f53]) ).
fof(f2449,plain,
( model_ub(sK3,sK4,sK5)
| ~ spl6_4
| ~ spl6_70 ),
inference(resolution,[],[f1965,f2285]) ).
fof(f2452,plain,
( minsol_model_ub(sK3,sK4,sK5)
| ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| ~ spl6_4
| ~ spl6_70 ),
inference(resolution,[],[f2449,f66]) ).
fof(f3728,plain,
( lesseq(sum(c,summation(sK3)),sK2(sK3,sK4,sK5))
| ~ spl6_11 ),
inference(resolution,[],[f1939,f1916]) ).
fof(f3729,plain,
( lesseq(sum(c,summation(sK4)),sK2(sK3,sK4,sK5))
| ~ spl6_11 ),
inference(resolution,[],[f1939,f1888]) ).
fof(f5933,plain,
( lesseq(sK5,sum(c,summation(sK3)))
| ~ spl6_2
| spl6_5 ),
inference(resolution,[],[f1863,f41]) ).
fof(f5957,plain,
( $false
| ~ spl6_2
| spl6_5
| spl6_57 ),
inference(forward_subsumption_resolution,[],[f5933,f1139]) ).
fof(f5958,plain,
( ~ spl6_2
| spl6_5
| spl6_57 ),
inference(avatar_contradiction_clause,[],[f5957]) ).
fof(f6020,plain,
( lesseq(sK5,sK2(sK3,sK4,sK5))
| ~ spl6_11
| ~ spl6_58 ),
inference(forward_demodulation,[],[f3728,f1142]) ).
fof(f6427,plain,
( ~ lesseq(sK4,sK3)
| ~ spl6_4
| spl6_10 ),
inference(forward_subsumption_resolution,[],[f715,f41]) ).
fof(f6432,plain,
( ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_1
| ~ spl6_4
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f2452,f76]) ).
fof(f6509,plain,
( $false
| spl6_1
| ~ spl6_4
| ~ spl6_11
| ~ spl6_58
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f6432,f6020]) ).
fof(f6510,plain,
( spl6_1
| ~ spl6_4
| ~ spl6_11
| ~ spl6_58
| ~ spl6_70 ),
inference(avatar_contradiction_clause,[],[f6509]) ).
fof(f6526,plain,
( ~ spl6_3
| ~ spl6_4
| spl6_10 ),
inference(avatar_split_clause,[],[f6427,f127,f103,f100]) ).
fof(f6554,plain,
( ~ lesseq(sK3,sK4)
| ~ lesseq(sK4,sK4)
| ~ spl6_6
| spl6_10 ),
inference(resolution,[],[f128,f2447]) ).
fof(f6558,plain,
( ~ lesseq(sK3,sK4)
| ~ spl6_6
| spl6_10 ),
inference(forward_subsumption_resolution,[],[f6554,f41]) ).
fof(f6559,plain,
( ~ spl6_5
| ~ spl6_6
| spl6_10 ),
inference(avatar_split_clause,[],[f6558,f127,f110,f107]) ).
fof(f6592,plain,
( ! [X0] :
( ~ lesseq(X0,sK2(sK3,sK4,sK5))
| ~ lesseq(sK5,X0) )
| spl6_9 ),
inference(resolution,[],[f125,f42]) ).
fof(f6646,plain,
( sK5 = sum(c,summation(sK4))
| ~ lesseq(sK3,sK4)
| ~ spl6_8 ),
inference(superposition,[],[f118,f50]) ).
fof(f6671,plain,
( ~ spl6_5
| spl6_90
| ~ spl6_8 ),
inference(avatar_split_clause,[],[f6646,f117,f1755,f107]) ).
fof(f6702,plain,
( lesseq(sK3,sK4)
| spl6_3 ),
inference(resolution,[],[f101,f44]) ).
fof(f7112,plain,
( ~ lesseq(sK3,sK3)
| ~ lesseq(sK4,sK3)
| spl6_70 ),
inference(resolution,[],[f1386,f53]) ).
fof(f8108,plain,
( ~ lesseq(sK5,sum(c,summation(sK4)))
| spl6_9
| ~ spl6_11 ),
inference(resolution,[],[f3729,f6592]) ).
fof(f9419,plain,
( lesseq(sK5,sum(c,summation(max(sK3,sK4))))
| ~ spl6_2 ),
inference(resolution,[],[f1861,f41]) ).
fof(f9606,plain,
( ~ lesseq(sK5,sK5)
| spl6_9
| ~ spl6_11
| ~ spl6_90 ),
inference(forward_demodulation,[],[f8108,f1756]) ).
fof(f9610,plain,
( $false
| spl6_9
| ~ spl6_11
| ~ spl6_90 ),
inference(forward_subsumption_resolution,[],[f9606,f41]) ).
fof(f9611,plain,
( spl6_9
| ~ spl6_11
| ~ spl6_90 ),
inference(avatar_contradiction_clause,[],[f9610]) ).
fof(f9621,plain,
( ~ lesseq(sK4,sK3)
| spl6_70 ),
inference(forward_subsumption_resolution,[],[f7112,f41]) ).
fof(f9624,definition,
( spl6_517
<=> sK3 = sK4 ),
introduced(definition,[new_symbols(definition,[spl6_517])],[avatar_definition]) ).
fof(f9625,plain,
( sK3 = sK4
| ~ spl6_517 ),
inference(avatar_component_clause,[],[f9624]) ).
fof(f9669,plain,
( $false
| ~ spl6_2
| spl6_7 ),
inference(forward_subsumption_resolution,[],[f9419,f115]) ).
fof(f9670,plain,
( ~ spl6_2
| spl6_7 ),
inference(avatar_contradiction_clause,[],[f9669]) ).
fof(f9683,plain,
( ~ spl6_3
| spl6_70 ),
inference(avatar_split_clause,[],[f9621,f1385,f100]) ).
fof(f9707,plain,
( lesseq(sum(c,summation(max(sK3,sK4))),sK1(sK3,sK4,sK5))
| ~ spl6_18 ),
inference(resolution,[],[f231,f54]) ).
fof(f9722,plain,
( lesseq(sum(c,summation(sK4)),sK1(sK3,sK4,sK5))
| ~ lesseq(sK3,sK4)
| ~ spl6_18 ),
inference(superposition,[],[f9707,f50]) ).
fof(f9723,plain,
( lesseq(sum(c,summation(sK3)),sK1(sK3,sK4,sK5))
| ~ lesseq(sK4,sK3)
| ~ spl6_18 ),
inference(superposition,[],[f9707,f49]) ).
fof(f9724,plain,
( lesseq(sum(c,summation(sK3)),sK1(sK3,sK4,sK5))
| ~ spl6_18
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f9723,f2288]) ).
fof(f9726,definition,
( spl6_526
<=> lesseq(sum(c,summation(sK4)),sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_526])],[avatar_definition]) ).
fof(f9727,plain,
( lesseq(sum(c,summation(sK4)),sK1(sK3,sK4,sK5))
| ~ spl6_526 ),
inference(avatar_component_clause,[],[f9726]) ).
fof(f9728,plain,
( ~ spl6_5
| spl6_526
| ~ spl6_18 ),
inference(avatar_split_clause,[],[f9722,f230,f9726,f107]) ).
fof(f9738,plain,
( ! [X0] :
( ~ model_ub(sK3,sK4,X0)
| lesseq(sK5,X0) )
| ~ spl6_1 ),
inference(resolution,[],[f71,f63]) ).
fof(f9740,plain,
( ~ model_max(sK3,sK4,sK5)
| model_max(sK3,sK4,sK1(sK3,sK4,sK5))
| spl6_2 ),
inference(resolution,[],[f77,f61]) ).
fof(f9935,plain,
( ! [X0,X1] :
( ~ lesseq(sum(c,summation(X1)),X0)
| ~ ub(sK3,sK4,X1)
| lesseq(sK5,X0) )
| ~ spl6_1 ),
inference(resolution,[],[f9738,f58]) ).
fof(f10034,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ spl6_1 ),
inference(resolution,[],[f192,f57]) ).
fof(f10051,plain,
( lesseq(sK4,sK0(sK3,sK4,sK5))
| ~ spl6_1 ),
inference(resolution,[],[f10034,f51]) ).
fof(f10068,plain,
( ! [X0] :
( ~ lesseq(X0,summation(sK0(sK3,sK4,sK5)))
| lesseq(sum(c,X0),sK5) )
| ~ spl6_15 ),
inference(superposition,[],[f45,f217]) ).
fof(f11196,plain,
( ! [X0] :
( ~ lesseq(X0,sK0(sK3,sK4,sK5))
| lesseq(sum(c,summation(X0)),sK5) )
| ~ spl6_15 ),
inference(resolution,[],[f10068,f47]) ).
fof(f11719,plain,
( sK3 = sK4
| ~ lesseq(sK3,sK4)
| ~ spl6_70 ),
inference(resolution,[],[f2288,f43]) ).
fof(f11728,plain,
( ~ spl6_5
| spl6_517
| ~ spl6_70 ),
inference(avatar_split_clause,[],[f11719,f1385,f9624,f107]) ).
fof(f11731,plain,
( lesseq(sum(c,summation(sK3)),sK5)
| ~ spl6_6
| ~ spl6_517 ),
inference(superposition,[],[f111,f9625]) ).
fof(f13079,plain,
( ~ ub(sK3,sK4,sK3)
| lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_1
| ~ spl6_18
| ~ spl6_70 ),
inference(resolution,[],[f9935,f9724]) ).
fof(f13080,plain,
( ~ ub(sK3,sK4,sK4)
| lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_1
| ~ spl6_526 ),
inference(resolution,[],[f9935,f9727]) ).
fof(f13147,plain,
( ~ ub(sK3,sK4,sK4)
| ~ spl6_1
| spl6_16
| ~ spl6_526 ),
inference(forward_subsumption_resolution,[],[f13080,f224]) ).
fof(f13148,plain,
( lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_1
| ~ spl6_18
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f13079,f2285]) ).
fof(f13167,plain,
( $false
| ~ spl6_1
| spl6_16
| ~ spl6_18
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f13148,f224]) ).
fof(f13168,plain,
( ~ spl6_1
| spl6_16
| ~ spl6_18
| ~ spl6_70 ),
inference(avatar_contradiction_clause,[],[f13167]) ).
fof(f13212,plain,
( ~ model_max(sK3,sK3,sK5)
| spl6_17
| ~ spl6_517 ),
inference(forward_demodulation,[],[f227,f9625]) ).
fof(f13243,plain,
( ~ lesseq(sum(c,summation(max(sK3,sK3))),sK5)
| spl6_17
| ~ spl6_517 ),
inference(resolution,[],[f13212,f55]) ).
fof(f13933,plain,
( ~ lesseq(sum(c,summation(sK3)),sK5)
| ~ lesseq(sK3,sK3)
| spl6_17
| ~ spl6_517 ),
inference(superposition,[],[f13243,f50]) ).
fof(f13936,plain,
( ~ lesseq(sK3,sK3)
| ~ spl6_4
| spl6_17
| ~ spl6_517 ),
inference(forward_subsumption_resolution,[],[f13933,f104]) ).
fof(f13939,plain,
( $false
| ~ spl6_4
| spl6_17
| ~ spl6_517 ),
inference(forward_subsumption_resolution,[],[f13936,f41]) ).
fof(f13940,plain,
( ~ spl6_4
| spl6_17
| ~ spl6_517 ),
inference(avatar_contradiction_clause,[],[f13939]) ).
fof(f13944,plain,
( spl6_4
| ~ spl6_6
| ~ spl6_517 ),
inference(avatar_split_clause,[],[f11731,f9624,f110,f103]) ).
fof(f21011,plain,
( spl6_18
| ~ spl6_17
| spl6_2 ),
inference(avatar_split_clause,[],[f9740,f73,f226,f230]) ).
fof(f21604,plain,
( lesseq(sum(c,summation(sK4)),sK5)
| ~ spl6_1
| ~ spl6_15 ),
inference(resolution,[],[f10051,f11196]) ).
fof(f21774,plain,
( sK4 = max(sK3,sK4)
| spl6_3 ),
inference(resolution,[],[f6702,f50]) ).
fof(f21848,plain,
( ~ lesseq(sK3,sK4)
| ~ lesseq(sK4,sK4)
| ~ spl6_1
| spl6_16
| ~ spl6_526 ),
inference(resolution,[],[f13147,f53]) ).
fof(f21849,plain,
( ~ lesseq(sK4,sK4)
| ~ spl6_1
| spl6_3
| spl6_16
| ~ spl6_526 ),
inference(forward_subsumption_resolution,[],[f21848,f6702]) ).
fof(f21850,plain,
( $false
| ~ spl6_1
| spl6_3
| spl6_16
| ~ spl6_526 ),
inference(forward_subsumption_resolution,[],[f21849,f41]) ).
fof(f21851,plain,
( ~ spl6_1
| spl6_3
| spl6_16
| ~ spl6_526 ),
inference(avatar_contradiction_clause,[],[f21850]) ).
fof(f21853,plain,
( ~ lesseq(sum(c,summation(max(sK3,sK4))),sK5)
| spl6_17 ),
inference(resolution,[],[f227,f55]) ).
fof(f21854,plain,
( ~ lesseq(sum(c,summation(sK4)),sK5)
| spl6_3
| spl6_17 ),
inference(forward_demodulation,[],[f21853,f21774]) ).
fof(f21855,plain,
( $false
| spl6_3
| ~ spl6_6
| spl6_17 ),
inference(forward_subsumption_resolution,[],[f21854,f111]) ).
fof(f21856,plain,
( spl6_3
| ~ spl6_6
| spl6_17 ),
inference(avatar_contradiction_clause,[],[f21855]) ).
fof(f21861,plain,
( spl6_6
| ~ spl6_1
| ~ spl6_15 ),
inference(avatar_split_clause,[],[f21604,f216,f70,f110]) ).
cnf(s1,plain,
( spl6_1
| spl6_2 ),
inference(sat_conversion,[],[f75]) ).
cnf(s2,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(sat_conversion,[],[f78]) ).
cnf(s3,plain,
( ~ spl6_2
| ~ spl6_3
| spl6_4 ),
inference(sat_conversion,[],[f105]) ).
cnf(s4,plain,
( ~ spl6_2
| ~ spl6_5
| spl6_6 ),
inference(sat_conversion,[],[f112]) ).
cnf(s6,plain,
( ~ spl6_2
| ~ spl6_7
| spl6_8 ),
inference(sat_conversion,[],[f120]) ).
cnf(s7,plain,
( spl6_1
| ~ spl6_9
| ~ spl6_10 ),
inference(sat_conversion,[],[f129]) ).
cnf(s8,plain,
( spl6_1
| ~ spl6_10
| spl6_11 ),
inference(sat_conversion,[],[f133]) ).
cnf(s12,plain,
( spl6_3
| spl6_5 ),
inference(sat_conversion,[],[f188]) ).
cnf(s15,plain,
( ~ spl6_1
| ~ spl6_14
| spl6_15 ),
inference(sat_conversion,[],[f219]) ).
cnf(s16,plain,
( spl6_2
| ~ spl6_16
| ~ spl6_17 ),
inference(sat_conversion,[],[f228]) ).
cnf(s21,plain,
( ~ spl6_1
| ~ spl6_21
| spl6_22 ),
inference(sat_conversion,[],[f268]) ).
cnf(s53,plain,
( ~ spl6_4
| ~ spl6_57
| spl6_58 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s74,plain,
( spl6_5
| spl6_70 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s81,plain,
( ~ spl6_1
| spl6_14 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s90,plain,
( spl6_5
| ~ spl6_15
| spl6_17
| spl6_21 ),
inference(sat_conversion,[],[f1729]) ).
cnf(s96,plain,
( ~ spl6_1
| spl6_5
| spl6_17
| ~ spl6_22 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s255,plain,
( ~ spl6_2
| spl6_5
| spl6_57 ),
inference(sat_conversion,[],[f5958]) ).
cnf(s351,plain,
( spl6_1
| ~ spl6_4
| ~ spl6_11
| ~ spl6_58
| ~ spl6_70 ),
inference(sat_conversion,[],[f6510]) ).
cnf(s359,plain,
( ~ spl6_3
| ~ spl6_4
| spl6_10 ),
inference(sat_conversion,[],[f6526]) ).
cnf(s360,plain,
( ~ spl6_5
| ~ spl6_6
| spl6_10 ),
inference(sat_conversion,[],[f6559]) ).
cnf(s372,plain,
( ~ spl6_5
| ~ spl6_8
| spl6_90 ),
inference(sat_conversion,[],[f6671]) ).
cnf(s551,plain,
( spl6_9
| ~ spl6_11
| ~ spl6_90 ),
inference(sat_conversion,[],[f9611]) ).
cnf(s565,plain,
( ~ spl6_2
| spl6_7 ),
inference(sat_conversion,[],[f9670]) ).
cnf(s566,plain,
( ~ spl6_3
| spl6_70 ),
inference(sat_conversion,[],[f9683]) ).
cnf(s575,plain,
( ~ spl6_5
| ~ spl6_18
| spl6_526 ),
inference(sat_conversion,[],[f9728]) ).
cnf(s704,plain,
( ~ spl6_5
| ~ spl6_70
| spl6_517 ),
inference(sat_conversion,[],[f11728]) ).
cnf(s729,plain,
( ~ spl6_1
| spl6_16
| ~ spl6_18
| ~ spl6_70 ),
inference(sat_conversion,[],[f13168]) ).
cnf(s749,plain,
( ~ spl6_4
| spl6_17
| ~ spl6_517 ),
inference(sat_conversion,[],[f13940]) ).
cnf(s756,plain,
( spl6_4
| ~ spl6_6
| ~ spl6_517 ),
inference(sat_conversion,[],[f13944]) ).
cnf(s1058,plain,
( spl6_2
| ~ spl6_17
| spl6_18 ),
inference(sat_conversion,[],[f21011]) ).
cnf(s1172,plain,
( ~ spl6_1
| spl6_3
| spl6_16
| ~ spl6_526 ),
inference(sat_conversion,[],[f21851]) ).
cnf(s1173,plain,
( spl6_3
| ~ spl6_6
| spl6_17 ),
inference(sat_conversion,[],[f21856]) ).
cnf(s1178,plain,
( ~ spl6_1
| spl6_6
| ~ spl6_15 ),
inference(sat_conversion,[],[f21861]) ).
cnf(s1179,plain,
( ~ spl6_5
| spl6_1 ),
inference(rat,[],[s551,s7,s8,s360,s4,s372,s6,s565,s1]) ).
cnf(s1180,plain,
spl6_1,
inference(rat,[],[s351,s8,s53,s359,s3,s12,s74,s255,s1179,s1]) ).
cnf(s1181,plain,
spl6_14,
inference(rat,[],[s81,s1180]) ).
cnf(s1183,plain,
~ spl6_2,
inference(rat,[],[s2,s1180]) ).
cnf(s1184,plain,
spl6_15,
inference(rat,[],[s15,s1180,s1181]) ).
cnf(s1186,plain,
spl6_6,
inference(rat,[],[s1178,s1180,s1184]) ).
cnf(s1188,plain,
spl6_3,
inference(rat,[],[s1172,s575,s16,s1058,s1173,s12,s1180,s1183,s1186]) ).
cnf(s1189,plain,
spl6_70,
inference(rat,[],[s566,s1188]) ).
cnf(s1191,plain,
~ spl6_17,
inference(rat,[],[s729,s16,s1058,s1180,s1189,s1183]) ).
cnf(s1193,plain,
~ spl6_517,
inference(rat,[],[s749,s756,s1191,s1186]) ).
cnf(s1194,plain,
~ spl6_5,
inference(rat,[],[s704,s1189,s1193]) ).
cnf(s1195,plain,
~ spl6_22,
inference(rat,[],[s96,s1191,s1180,s1194]) ).
cnf(s1198,plain,
spl6_21,
inference(rat,[],[s90,s1191,s1184,s1194]) ).
cnf(s1201,plain,
$false,
inference(rat,[],[s21,s1180,s1195,s1198]) ).
fof(f21862,plain,
$false,
inference(avatar_sat_refutation,[],[s1201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM862+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 21:36:44 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 17.66/3.50 % (3336195)Detected formulas, will run a generic FOF schedule.
% 17.66/3.50 % (3336222)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=3723341817:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 17.66/3.50 % (3336223)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=1360444405:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 17.66/3.50 % (3336228)dis-21_1_sil=8000:lcm=predicate:random_seed=3624302864:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 17.66/3.50 % (3336226)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1233058302:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 17.66/3.50 % (3336225)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4024697133:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 17.66/3.50 % (3336227)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4242407268:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 17.66/3.50 % (3336224)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=4016656932:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 17.66/3.50 % (3336225)Refutation not found, incomplete strategy
% 17.66/3.50 % (3336225)------------------------------
% 17.66/3.50 % (3336225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.66/3.50 % (3336225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.66/3.50 % (3336225)CaDiCaL version: 2.1.3
% 17.66/3.50 % (3336225)Termination reason: Refutation not found, incomplete strategy
% 17.66/3.50 % (3336225)Time elapsed: 0.002 s
% 17.66/3.50 % (3336225)Peak memory usage: 87 MB
% 17.66/3.50 % (3336228)Instruction limit reached!
% 17.66/3.50 % (3336228)------------------------------
% 17.66/3.50 % (3336228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.66/3.50 % (3336228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.66/3.50 % (3336228)CaDiCaL version: 2.1.3
% 17.66/3.50 % (3336228)Termination reason: Instruction limit
% 17.66/3.50 % (3336228)Termination phase: Saturation
% 17.66/3.50 % (3336228)Time elapsed: 0.122 s
% 17.66/3.50 % (3336228)Peak memory usage: 89 MB
% 17.66/3.50 % (3336228)Instructions burned: 129 (million)
% 17.66/3.50 % (3336226)Instruction limit reached!
% 17.66/3.50 % (3336226)------------------------------
% 17.66/3.50 % (3336226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.66/3.50 % (3336226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.66/3.50 % (3336226)CaDiCaL version: 2.1.3
% 17.66/3.50 % (3336226)Termination reason: Instruction limit
% 17.66/3.50 % (3336226)Termination phase: Saturation
% 17.66/3.50 % (3336226)Time elapsed: 0.109 s
% 17.66/3.50 % (3336226)Peak memory usage: 88 MB
% 17.66/3.50 % (3336226)Instructions burned: 120 (million)
% 17.66/3.50 % (3336227)Instruction limit reached!
% 17.66/3.50 % (3336227)------------------------------
% 17.66/3.50 % (3336227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.66/3.50 % (3336227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.66/3.50 % (3336227)CaDiCaL version: 2.1.3
% 17.66/3.50 % (3336227)Termination reason: Instruction limit
% 17.66/3.50 % (3336227)Termination phase: Saturation
% 17.66/3.50 % (3336227)Time elapsed: 0.145 s
% 17.66/3.50 % (3336227)Peak memory usage: 89 MB
% 17.66/3.50 % (3336227)Instructions burned: 139 (million)
% 17.66/3.50 % (3336239)lrs+10_1_sil=8000:sp=occurrence:random_seed=1822536466:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 17.66/3.50 % (3336242)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4161853710:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 17.66/3.50 % (3336242)Refutation not found, incomplete strategy
% 17.66/3.50 % (3336242)------------------------------
% 17.66/3.50 % (3336242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.66/3.50 % (3336242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.66/3.50 % (3336242)CaDiCaL version: 2.1.3
% 17.66/3.50 % (3336242)Termination reason: Refutation not found, incomplete strategy
% 17.66/3.50 % (3336242)Time elapsed: 0.002 s
% 31.23/5.35 % (3336242)Peak memory usage: 88 MB
% 31.23/5.35 % (3336240)lrs+10_1_sil=32000:urr=on:br=off:random_seed=618556528:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 31.23/5.35 % (3336240)Refutation not found, incomplete strategy
% 31.23/5.35 % (3336240)------------------------------
% 31.23/5.35 % (3336240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.35 % (3336240)CaDiCaL version: 2.1.3
% 31.23/5.35 % (3336240)Termination reason: Refutation not found, incomplete strategy
% 31.23/5.35 % (3336240)Time elapsed: 0.002 s
% 31.23/5.35 % (3336240)Peak memory usage: 88 MB
% 31.23/5.35 % (3336240)Instructions burned: 1 (million)
% 31.23/5.35 % (3336225)------------------------------
% 31.23/5.35 % (3336225)------------------------------
% 31.23/5.35 % (3336249)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=4020095648:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 31.23/5.35 % (3336239)Instruction limit reached!
% 31.23/5.35 % (3336239)------------------------------
% 31.23/5.35 % (3336239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.35 % (3336239)CaDiCaL version: 2.1.3
% 31.23/5.35 % (3336239)Termination reason: Instruction limit
% 31.23/5.35 % (3336239)Termination phase: Saturation
% 31.23/5.35 % (3336239)Time elapsed: 0.267 s
% 31.23/5.35 % (3336239)Peak memory usage: 91 MB
% 31.23/5.35 % (3336239)Instructions burned: 286 (million)
% 31.23/5.35 % (3336240)------------------------------
% 31.23/5.35 % (3336240)------------------------------
% 31.23/5.35 % (3336242)------------------------------
% 31.23/5.35 % (3336242)------------------------------
% 31.23/5.35 % (3336249)Instruction limit reached!
% 31.23/5.35 % (3336249)------------------------------
% 31.23/5.35 % (3336249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.35 % (3336249)CaDiCaL version: 2.1.3
% 31.23/5.35 % (3336249)Termination reason: Instruction limit
% 31.23/5.35 % (3336249)Termination phase: Saturation
% 31.23/5.35 % (3336249)Time elapsed: 0.204 s
% 31.23/5.35 % (3336249)Peak memory usage: 91 MB
% 31.23/5.35 % (3336249)Instructions burned: 249 (million)
% 31.23/5.35 % (3336255)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4131796390:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 31.23/5.35 % (3336255)Refutation not found, incomplete strategy
% 31.23/5.35 % (3336255)------------------------------
% 31.23/5.35 % (3336255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.35 % (3336255)CaDiCaL version: 2.1.3
% 31.23/5.35 % (3336255)Termination reason: Refutation not found, incomplete strategy
% 31.23/5.35 % (3336255)Time elapsed: 0.002 s
% 31.23/5.35 % (3336255)Peak memory usage: 88 MB
% 31.23/5.35 % (3336255)Instructions burned: 1 (million)
% 31.23/5.35 % (3336258)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2095010711:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 31.23/5.35 % (3336259)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1282667446:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 31.23/5.35 % (3336257)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4031647851:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 31.23/5.35 % (3336258)Instruction limit reached!
% 31.23/5.35 % (3336258)------------------------------
% 31.23/5.35 % (3336258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.23/5.35 % (3336258)CaDiCaL version: 2.1.3
% 31.23/5.35 % (3336258)Termination reason: Instruction limit
% 31.23/5.35 % (3336258)Termination phase: Saturation
% 31.23/5.35 % (3336258)Time elapsed: 0.079 s
% 31.23/5.35 % (3336258)Peak memory usage: 89 MB
% 31.23/5.35 % (3336258)Instructions burned: 114 (million)
% 31.23/5.35 % (3336259)Instruction limit reached!
% 31.23/5.35 % (3336259)------------------------------
% 31.23/5.35 % (3336259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.23/5.35 % (3336259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336259)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336259)Termination reason: Instruction limit
% 49.58/8.01 % (3336259)Termination phase: Saturation
% 49.58/8.01 % (3336259)Time elapsed: 0.112 s
% 49.58/8.01 % (3336259)Peak memory usage: 88 MB
% 49.58/8.01 % (3336259)Instructions burned: 127 (million)
% 49.58/8.01 % (3336255)------------------------------
% 49.58/8.01 % (3336255)------------------------------
% 49.58/8.01 % (3336268)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2697712023:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 49.58/8.01 % (3336269)lrs+10_1_sil=8000:sp=occurrence:random_seed=825227380:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 49.58/8.01 % (3336268)Instruction limit reached!
% 49.58/8.01 % (3336268)------------------------------
% 49.58/8.01 % (3336268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.58/8.01 % (3336268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336268)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336268)Termination reason: Instruction limit
% 49.58/8.01 % (3336268)Termination phase: Saturation
% 49.58/8.01 % (3336268)Time elapsed: 0.101 s
% 49.58/8.01 % (3336268)Peak memory usage: 88 MB
% 49.58/8.01 % (3336268)Instructions burned: 114 (million)
% 49.58/8.01 % (3336272)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3655420371:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 49.58/8.01 % (3336274)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4046950503:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 49.58/8.01 % (3336272)Instruction limit reached!
% 49.58/8.01 % (3336272)------------------------------
% 49.58/8.01 % (3336272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.58/8.01 % (3336272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336272)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336272)Termination reason: Instruction limit
% 49.58/8.01 % (3336272)Termination phase: Saturation
% 49.58/8.01 % (3336272)Time elapsed: 0.354 s
% 49.58/8.01 % (3336272)Peak memory usage: 89 MB
% 49.58/8.01 % (3336272)Instructions burned: 437 (million)
% 49.58/8.01 % (3336281)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=349170583:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 49.58/8.01 % (3336281)Instruction limit reached!
% 49.58/8.01 % (3336281)------------------------------
% 49.58/8.01 % (3336281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.58/8.01 % (3336281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336281)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336281)Termination reason: Instruction limit
% 49.58/8.01 % (3336281)Termination phase: Saturation
% 49.58/8.01 % (3336281)Time elapsed: 0.134 s
% 49.58/8.01 % (3336281)Peak memory usage: 90 MB
% 49.58/8.01 % (3336281)Instructions burned: 134 (million)
% 49.58/8.01 % (3336269)Instruction limit reached!
% 49.58/8.01 % (3336269)------------------------------
% 49.58/8.01 % (3336269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.58/8.01 % (3336269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336269)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336269)Termination reason: Instruction limit
% 49.58/8.01 % (3336269)Termination phase: Saturation
% 49.58/8.01 % (3336269)Time elapsed: 0.901 s
% 49.58/8.01 % (3336269)Peak memory usage: 96 MB
% 49.58/8.01 % (3336269)Instructions burned: 907 (million)
% 49.58/8.01 % (3336285)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4128489465:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 49.58/8.01 % (3336285)Refutation not found, incomplete strategy
% 49.58/8.01 % (3336285)------------------------------
% 49.58/8.01 % (3336285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.58/8.01 % (3336285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.58/8.01 % (3336285)CaDiCaL version: 2.1.3
% 49.58/8.01 % (3336285)Termination reason: Refutation not found, incomplete strategy
% 49.58/8.01 % (3336285)Time elapsed: 0.003 s
% 49.58/8.01 % (3336285)Peak memory usage: 88 MB
% 49.58/8.01 % (3336285)Instructions burned: 1 (million)
% 49.58/8.01 % (3336286)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=341080269:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 88.88/13.49 % (3336285)------------------------------
% 88.88/13.49 % (3336285)------------------------------
% 88.88/13.49 % (3336291)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=216898434:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 88.88/13.49 % (3336291)Instruction limit reached!
% 88.88/13.49 % (3336291)------------------------------
% 88.88/13.49 % (3336291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.88/13.49 % (3336291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.88/13.49 % (3336291)CaDiCaL version: 2.1.3
% 88.88/13.49 % (3336291)Termination reason: Instruction limit
% 88.88/13.49 % (3336291)Termination phase: Saturation
% 88.88/13.49 % (3336291)Time elapsed: 0.123 s
% 88.88/13.49 % (3336291)Peak memory usage: 90 MB
% 88.88/13.49 % (3336291)Instructions burned: 126 (million)
% 88.88/13.49 % (3336294)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1879091977:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 88.88/13.49 % (3336294)Instruction limit reached!
% 88.88/13.49 % (3336294)------------------------------
% 88.88/13.49 % (3336294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.88/13.49 % (3336294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.88/13.49 % (3336294)CaDiCaL version: 2.1.3
% 88.88/13.49 % (3336294)Termination reason: Instruction limit
% 88.88/13.49 % (3336294)Termination phase: Saturation
% 88.88/13.49 % (3336294)Time elapsed: 0.068 s
% 88.88/13.49 % (3336294)Peak memory usage: 88 MB
% 88.88/13.49 % (3336294)Instructions burned: 135 (million)
% 88.88/13.49 % (3336300)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2640440105:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 88.88/13.49 % (3336300)Refutation not found, incomplete strategy
% 88.88/13.49 % (3336300)------------------------------
% 88.88/13.49 % (3336300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.88/13.49 % (3336300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.88/13.49 % (3336300)CaDiCaL version: 2.1.3
% 88.88/13.49 % (3336300)Termination reason: Refutation not found, incomplete strategy
% 88.88/13.49 % (3336300)Time elapsed: 0.002 s
% 88.88/13.49 % (3336300)Peak memory usage: 88 MB
% 88.88/13.49 % (3336257)Instruction limit reached!
% 88.88/13.49 % (3336257)------------------------------
% 88.88/13.49 % (3336257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.88/13.49 % (3336257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.88/13.49 % (3336257)CaDiCaL version: 2.1.3
% 88.88/13.49 % (3336257)Termination reason: Instruction limit
% 88.88/13.49 % (3336257)Termination phase: Saturation
% 88.88/13.49 % (3336257)Time elapsed: 2.578 s
% 88.88/13.49 % (3336257)Peak memory usage: 141 MB
% 88.88/13.49 % (3336257)Instructions burned: 2350 (million)
% 88.88/13.49 % (3336300)------------------------------
% 88.88/13.49 % (3336300)------------------------------
% 88.88/13.49 % (3336303)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1404408309:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2962 on theBenchmark for (2962ds/431Mi)
% 88.88/13.49 % (3336303)Refutation not found, incomplete strategy
% 88.88/13.49 % (3336303)------------------------------
% 88.88/13.49 % (3336303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.88/13.49 % (3336303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.88/13.49 % (3336303)CaDiCaL version: 2.1.3
% 88.88/13.49 % (3336303)Termination reason: Refutation not found, incomplete strategy
% 88.88/13.49 % (3336303)Time elapsed: 0.001 s
% 88.88/13.49 % (3336303)Peak memory usage: 88 MB
% 88.88/13.49 % (3336304)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=2235147662:i=6060:aac=none:ins=25_2961 on theBenchmark for (2961ds/6060Mi)
% 88.88/13.49 % (3336303)------------------------------
% 88.88/13.49 % (3336303)------------------------------
% 88.88/13.49 % (3336314)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=2675401573:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2958 on theBenchmark for (2958ds/150Mi)
% 88.88/13.49 % (3336314)Instruction limit reached!
% 88.88/13.49 % (3336314)------------------------------
% 54.34/16.31 % (3336314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336314)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336314)Termination reason: Instruction limit
% 54.34/16.31 % (3336314)Termination phase: Saturation
% 54.34/16.31 % (3336314)Time elapsed: 0.102 s
% 54.34/16.31 % (3336314)Peak memory usage: 90 MB
% 54.34/16.31 % (3336314)Instructions burned: 150 (million)
% 54.34/16.31 % (3336394)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=670578667:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi)
% 54.34/16.31 % (3336274)Instruction limit reached!
% 54.34/16.31 % (3336274)------------------------------
% 54.34/16.31 % (3336274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336274)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336274)Termination reason: Instruction limit
% 54.34/16.31 % (3336274)Termination phase: Saturation
% 54.34/16.31 % (3336274)Time elapsed: 4.153 s
% 54.34/16.31 % (3336274)Peak memory usage: 159 MB
% 54.34/16.31 % (3336274)Instructions burned: 5203 (million)
% 54.34/16.31 % (3336464)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2063135831:i=667:av=off:fsr=off_2941 on theBenchmark for (2941ds/667Mi)
% 54.34/16.31 % (3336464)Instruction limit reached!
% 54.34/16.31 % (3336464)------------------------------
% 54.34/16.31 % (3336464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336464)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336464)Termination reason: Instruction limit
% 54.34/16.31 % (3336464)Termination phase: Saturation
% 54.34/16.31 % (3336464)Time elapsed: 0.297 s
% 54.34/16.31 % (3336464)Peak memory usage: 93 MB
% 54.34/16.31 % (3336464)Instructions burned: 668 (million)
% 54.34/16.31 % (3336466)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=2628902137:s2a=on:i=185:s2at=1.8:fdi=4_2937 on theBenchmark for (2937ds/185Mi)
% 54.34/16.31 % (3336466)Instruction limit reached!
% 54.34/16.31 % (3336466)------------------------------
% 54.34/16.31 % (3336466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336466)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336466)Termination reason: Instruction limit
% 54.34/16.31 % (3336466)Termination phase: Saturation
% 54.34/16.31 % (3336466)Time elapsed: 0.113 s
% 54.34/16.31 % (3336466)Peak memory usage: 91 MB
% 54.34/16.31 % (3336466)Instructions burned: 186 (million)
% 54.34/16.31 % (3336468)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=807846270:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2935 on theBenchmark for (2935ds/193Mi)
% 54.34/16.31 % (3336468)Instruction limit reached!
% 54.34/16.31 % (3336468)------------------------------
% 54.34/16.31 % (3336468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336468)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336468)Termination reason: Instruction limit
% 54.34/16.31 % (3336468)Termination phase: Saturation
% 54.34/16.31 % (3336468)Time elapsed: 0.120 s
% 54.34/16.31 % (3336468)Peak memory usage: 90 MB
% 54.34/16.31 % (3336468)Instructions burned: 194 (million)
% 54.34/16.31 % (3336470)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4244544906:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2932 on theBenchmark for (2932ds/4850Mi)
% 54.34/16.31 % (3336304)Instruction limit reached!
% 54.34/16.31 % (3336304)------------------------------
% 54.34/16.31 % (3336304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336304)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336304)Termination reason: Instruction limit
% 54.34/16.31 % (3336304)Termination phase: Saturation
% 54.34/16.31 % (3336304)Time elapsed: 2.960 s
% 54.34/16.31 % (3336304)Peak memory usage: 141 MB
% 54.34/16.31 % (3336304)Instructions burned: 6061 (million)
% 54.34/16.31 % (3336472)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=102754503:i=12111:sd=1:ss=included_2930 on theBenchmark for (2930ds/12111Mi)
% 54.34/16.31 % (3336470)Instruction limit reached!
% 54.34/16.31 % (3336470)------------------------------
% 54.34/16.31 % (3336470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336470)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336470)Termination reason: Instruction limit
% 54.34/16.31 % (3336470)Termination phase: Saturation
% 54.34/16.31 % (3336470)Time elapsed: 2.787 s
% 54.34/16.31 % (3336470)Peak memory usage: 99 MB
% 54.34/16.31 % (3336470)Instructions burned: 4851 (million)
% 54.34/16.31 % (3336681)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2586766788:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 54.34/16.31 % (3336681)Instruction limit reached!
% 54.34/16.31 % (3336681)------------------------------
% 54.34/16.31 % (3336681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336681)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336681)Termination reason: Instruction limit
% 54.34/16.31 % (3336681)Termination phase: Saturation
% 54.34/16.31 % (3336681)Time elapsed: 0.184 s
% 54.34/16.31 % (3336681)Peak memory usage: 92 MB
% 54.34/16.31 % (3336681)Instructions burned: 321 (million)
% 54.34/16.31 % (3336776)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3504331050:i=2064:ep=RST_2900 on theBenchmark for (2900ds/2064Mi)
% 54.34/16.31 % (3336776)Refutation not found, incomplete strategy
% 54.34/16.31 % (3336776)------------------------------
% 54.34/16.31 % (3336776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336776)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336776)Termination reason: Refutation not found, incomplete strategy
% 54.34/16.31 % (3336776)Time elapsed: 0.002 s
% 54.34/16.31 % (3336776)Peak memory usage: 88 MB
% 54.34/16.31 % (3336776)Instructions burned: 1 (million)
% 54.34/16.31 % (3336776)------------------------------
% 54.34/16.31 % (3336776)------------------------------
% 54.34/16.31 % (3336837)dis-1011_128_sil=32000:random_seed=2331628224:i=3706:ep=RST:av=off_2897 on theBenchmark for (2897ds/3706Mi)
% 54.34/16.31 % (3336286)Instruction limit reached!
% 54.34/16.31 % (3336286)------------------------------
% 54.34/16.31 % (3336286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336286)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336286)Termination reason: Instruction limit
% 54.34/16.31 % (3336286)Termination phase: Saturation
% 54.34/16.31 % (3336286)Time elapsed: 8.190 s
% 54.34/16.31 % (3336286)Peak memory usage: 159 MB
% 54.34/16.31 % (3336286)Instructions burned: 13194 (million)
% 54.34/16.31 % (3336839)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2758678754:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2892 on theBenchmark for (2892ds/757Mi)
% 54.34/16.31 % (3336839)Instruction limit reached!
% 54.34/16.31 % (3336839)------------------------------
% 54.34/16.31 % (3336839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336839)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336839)Termination reason: Instruction limit
% 54.34/16.31 % (3336839)Termination phase: Saturation
% 54.34/16.31 % (3336839)Time elapsed: 0.519 s
% 54.34/16.31 % (3336839)Peak memory usage: 92 MB
% 54.34/16.31 % (3336839)Instructions burned: 758 (million)
% 54.34/16.31 % (3336841)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1890231606:i=13913:ss=axioms:sgt=8_2885 on theBenchmark for (2885ds/13913Mi)
% 54.34/16.31 % (3336837)Instruction limit reached!
% 54.34/16.31 % (3336837)------------------------------
% 54.34/16.31 % (3336837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336837)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336837)Termination reason: Instruction limit
% 54.34/16.31 % (3336837)Termination phase: Saturation
% 54.34/16.31 % (3336837)Time elapsed: 1.996 s
% 54.34/16.31 % (3336837)Peak memory usage: 99 MB
% 54.34/16.31 % (3336837)Instructions burned: 3707 (million)
% 54.34/16.31 % (3336843)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=91830649:i=9925:aac=none_2875 on theBenchmark for (2875ds/9925Mi)
% 54.34/16.31 % (3336394)Instruction limit reached!
% 54.34/16.31 % (3336394)------------------------------
% 54.34/16.31 % (3336394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336394)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336394)Termination reason: Instruction limit
% 54.34/16.31 % (3336394)Termination phase: Saturation
% 54.34/16.31 % (3336394)Time elapsed: 8.458 s
% 54.34/16.31 % (3336394)Peak memory usage: 226 MB
% 54.34/16.31 % (3336394)Instructions burned: 14156 (million)
% 54.34/16.31 % (3336845)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1750028941:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2869 on theBenchmark for (2869ds/2479Mi)
% 54.34/16.31 % (3336845)Refutation not found, incomplete strategy
% 54.34/16.31 % (3336845)------------------------------
% 54.34/16.31 % (3336845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336845)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336845)Termination reason: Refutation not found, incomplete strategy
% 54.34/16.31 % (3336845)Time elapsed: 0.002 s
% 54.34/16.31 % (3336845)Peak memory usage: 88 MB
% 54.34/16.31 % (3336845)Instructions burned: 1 (million)
% 54.34/16.31 % (3336845)------------------------------
% 54.34/16.31 % (3336845)------------------------------
% 54.34/16.31 % (3336847)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=592071558:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2865 on theBenchmark for (2865ds/440Mi)
% 54.34/16.31 % (3336847)Instruction limit reached!
% 54.34/16.31 % (3336847)------------------------------
% 54.34/16.31 % (3336847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.34/16.31 % (3336847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.34/16.31 % (3336847)CaDiCaL version: 2.1.3
% 54.34/16.31 % (3336847)Termination reason: Instruction limit
% 54.34/16.31 % (3336847)Termination phase: Saturation
% 54.34/16.31 % (3336847)Time elapsed: 0.251 s
% 54.34/16.31 % (3336847)Peak memory usage: 93 MB
% 54.34/16.31 % (3336847)Instructions burned: 442 (million)
% 54.34/16.31 % (3336849)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=554196423:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2862 on theBenchmark for (2862ds/11145Mi)
% 54.34/16.31 % (3336843)First to succeed.
% 54.34/16.31 % (3336843)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3336195"
% 54.34/16.31 % (3336843)Refutation found. Thanks to Tanya!
% 54.34/16.31 % SZS status Theorem for theBenchmark
% 54.34/16.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/16.50 % (3336843)------------------------------
% 0.17/16.50 % (3336843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/16.50 % (3336843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/16.50 % (3336843)CaDiCaL version: 2.1.3
% 0.17/16.50 % (3336843)Termination reason: Refutation
% 0.17/16.50 % (3336843)Time elapsed: 2.528 s
% 0.17/16.50 % (3336843)Peak memory usage: 154 MB
% 0.17/16.50 % (3336843)Instructions burned: 3732 (million)
% 0.17/16.50 % (3336843)------------------------------
% 0.17/16.50 % (3336843)------------------------------
% 0.17/16.50 % (3336195)Success in time 15.376 s
% 0.17/16.50 % Vampire exiting
%------------------------------------------------------------------------------