%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM861+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:18 PM UTC 2026
% Result : Theorem 28.14s 5.01s
% Output : Refutation 29.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 53
% Syntax : Number of formulae : 363 ( 21 unt; 40 def)
% Number of atoms : 986 ( 18 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1130 ( 507 ~; 522 |; 46 &)
% ( 50 <=>; 4 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 41 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 237 ( 0 sgn 222 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : lesseq(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_ref) ).
fof(f2,axiom,
! [X0,X1,X2] :
( ( lesseq(X0,X1)
& lesseq(X1,X2) )
=> lesseq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_trans) ).
fof(f3,axiom,
! [X0,X1] :
( ( lesseq(X0,X1)
& lesseq(X1,X0) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_antisymmetric) ).
fof(f4,axiom,
! [X0,X1] :
( lesseq(X0,X1)
| lesseq(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lesseq_total) ).
fof(f5,axiom,
! [X0,X1,X2] :
( lesseq(X0,X1)
<=> lesseq(sum(X2,X0),sum(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_monotone_1) ).
fof(f7,axiom,
! [X0,X1] :
( max(X0,X1) = X0
| ~ lesseq(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_1) ).
fof(f8,axiom,
! [X0,X1] :
( max(X0,X1) = X1
| ~ lesseq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_2) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ub(X0,X1,X2)
<=> ( lesseq(X0,X2)
& lesseq(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ub) ).
fof(f10,axiom,
! [X0,X1,X2] :
( model_max(X0,X1,X2)
<=> lesseq(sum(c,max(X0,X1)),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_max_4) ).
fof(f11,axiom,
! [X0,X1,X2] :
( model_ub(X0,X1,X2)
<=> ? [X3] :
( ub(X0,X1,X3)
& lesseq(sum(c,X3),X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_ub_4) ).
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/sandbox2/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/sandbox2/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/sandbox2/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(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,max(X0,X1)),X2) )
& ( lesseq(sum(c,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,X3),X2) ) )
& ( ? [X3] :
( ub(X0,X1,X3)
& lesseq(sum(c,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,X3),X2) ) )
& ( ? [X4] :
( ub(X0,X1,X4)
& lesseq(sum(c,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,X3),X2) ) )
& ( ( ub(X0,X1,sK0(X0,X1,X2))
& lesseq(sum(c,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(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,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,max(X0,X1)),X2) ),
inference(cnf_transformation,[],[f27]) ).
fof(f56,plain,
! [X2,X0,X1] :
( lesseq(sum(c,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,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(f72,plain,
( ~ minsol_model_ub(sK3,sK4,sK5)
| spl6_1 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f74,definition,
( spl6_2
<=> minsol_model_max(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition]) ).
fof(f75,plain,
( minsol_model_max(sK3,sK4,sK5)
| ~ spl6_2 ),
inference(avatar_component_clause,[],[f74]) ).
fof(f76,plain,
( ~ minsol_model_max(sK3,sK4,sK5)
| spl6_2 ),
inference(avatar_component_clause,[],[f74]) ).
fof(f77,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f68,f74,f70]) ).
fof(f78,plain,
( minsol_model_max(sK3,sK4,sK5)
| spl6_1 ),
inference(backward_subsumption_resolution,[],[f67,f72]) ).
fof(f81,plain,
( spl6_2
| spl6_1 ),
inference(avatar_split_clause,[],[f78,f70,f74]) ).
fof(f82,plain,
( ~ model_max(sK3,sK4,sK5)
| model_max(sK3,sK4,sK1(sK3,sK4,sK5))
| spl6_2 ),
inference(resolution,[],[f76,f61]) ).
fof(f83,plain,
( ~ model_max(sK3,sK4,sK5)
| ~ lesseq(sK5,sK1(sK3,sK4,sK5))
| spl6_2 ),
inference(resolution,[],[f76,f62]) ).
fof(f85,plain,
( model_ub(sK3,sK4,sK5)
| ~ spl6_1 ),
inference(resolution,[],[f71,f64]) ).
fof(f87,definition,
( spl6_3
<=> model_ub(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition]) ).
fof(f88,plain,
( ~ model_ub(sK3,sK4,sK5)
| spl6_3 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f89,plain,
( model_ub(sK3,sK4,sK5)
| ~ spl6_3 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
( spl6_3
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f85,f70,f87]) ).
fof(f94,plain,
( lesseq(sum(c,sK0(sK3,sK4,sK5)),sK5)
| ~ spl6_3 ),
inference(resolution,[],[f89,f56]) ).
fof(f95,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ spl6_3 ),
inference(resolution,[],[f89,f57]) ).
fof(f97,definition,
( spl6_4
<=> lesseq(sum(c,sK0(sK3,sK4,sK5)),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f99,plain,
( lesseq(sum(c,sK0(sK3,sK4,sK5)),sK5)
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,plain,
( spl6_4
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f94,f87,f97]) ).
fof(f103,plain,
( ! [X0] :
( lesseq(X0,sK5)
| ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK5))) )
| ~ spl6_4 ),
inference(resolution,[],[f99,f42]) ).
fof(f113,definition,
( spl6_5
<=> ub(sK3,sK4,sK0(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition]) ).
fof(f115,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK5))
| ~ spl6_5 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f116,plain,
( spl6_5
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f95,f87,f113]) ).
fof(f118,plain,
( lesseq(sK4,sK0(sK3,sK4,sK5))
| ~ spl6_5 ),
inference(resolution,[],[f115,f51]) ).
fof(f119,plain,
( lesseq(sK3,sK0(sK3,sK4,sK5))
| ~ spl6_5 ),
inference(resolution,[],[f115,f52]) ).
fof(f121,definition,
( spl6_6
<=> lesseq(sK4,sK0(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f123,plain,
( lesseq(sK4,sK0(sK3,sK4,sK5))
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
( spl6_6
| ~ spl6_5 ),
inference(avatar_split_clause,[],[f118,f113,f121]) ).
fof(f136,definition,
( spl6_7
<=> lesseq(sK5,sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition]) ).
fof(f138,plain,
( ~ lesseq(sK5,sK1(sK3,sK4,sK5))
| spl6_7 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f140,definition,
( spl6_8
<=> model_max(sK3,sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition]) ).
fof(f141,plain,
( model_max(sK3,sK4,sK5)
| ~ spl6_8 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f142,plain,
( ~ model_max(sK3,sK4,sK5)
| spl6_8 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,plain,
( ~ spl6_7
| ~ spl6_8
| spl6_2 ),
inference(avatar_split_clause,[],[f83,f74,f140,f136]) ).
fof(f154,definition,
( spl6_9
<=> lesseq(sK3,sK0(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
fof(f156,plain,
( lesseq(sK3,sK0(sK3,sK4,sK5))
| ~ spl6_9 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f157,plain,
( spl6_9
| ~ spl6_5 ),
inference(avatar_split_clause,[],[f119,f113,f154]) ).
fof(f169,definition,
( spl6_10
<=> model_max(sK3,sK4,sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
fof(f171,plain,
( model_max(sK3,sK4,sK1(sK3,sK4,sK5))
| ~ spl6_10 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f172,plain,
( spl6_10
| ~ spl6_8
| spl6_2 ),
inference(avatar_split_clause,[],[f82,f74,f140,f169]) ).
fof(f173,plain,
( ~ minsol_model_max(sK3,sK4,sK5)
| spl6_8 ),
inference(resolution,[],[f142,f60]) ).
fof(f179,plain,
( $false
| spl6_1
| spl6_8 ),
inference(forward_subsumption_resolution,[],[f173,f78]) ).
fof(f180,plain,
( spl6_1
| spl6_8 ),
inference(avatar_contradiction_clause,[],[f179]) ).
fof(f202,plain,
( lesseq(sum(c,max(sK3,sK4)),sK5)
| ~ spl6_8 ),
inference(resolution,[],[f141,f54]) ).
fof(f204,definition,
( spl6_13
<=> lesseq(sum(c,max(sK3,sK4)),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition]) ).
fof(f205,plain,
( ~ lesseq(sum(c,max(sK3,sK4)),sK5)
| spl6_13 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f206,plain,
( lesseq(sum(c,max(sK3,sK4)),sK5)
| ~ spl6_13 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f207,plain,
( spl6_13
| ~ spl6_8 ),
inference(avatar_split_clause,[],[f202,f140,f204]) ).
fof(f214,plain,
( minsol_model_ub(sK3,sK4,sK5)
| model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| ~ spl6_3 ),
inference(resolution,[],[f89,f65]) ).
fof(f219,plain,
( ~ lesseq(sum(c,max(sK3,sK4)),sK5)
| spl6_8 ),
inference(resolution,[],[f142,f55]) ).
fof(f221,plain,
( ! [X0] :
( lesseq(sK5,X0)
| ~ model_ub(sK3,sK4,X0) )
| ~ spl6_1 ),
inference(resolution,[],[f71,f63]) ).
fof(f333,plain,
( ~ spl6_13
| spl6_8 ),
inference(avatar_split_clause,[],[f219,f140,f204]) ).
fof(f347,definition,
( spl6_17
<=> ! [X0] :
( lesseq(sK5,X0)
| ~ model_ub(sK3,sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_17])],[avatar_definition]) ).
fof(f348,plain,
( ! [X0] :
( ~ model_ub(sK3,sK4,X0)
| lesseq(sK5,X0) )
| ~ spl6_17 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f349,plain,
( spl6_17
| ~ spl6_1 ),
inference(avatar_split_clause,[],[f221,f70,f347]) ).
fof(f351,plain,
( model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| spl6_1
| ~ spl6_3 ),
inference(forward_subsumption_resolution,[],[f214,f72]) ).
fof(f353,definition,
( spl6_18
<=> model_ub(sK3,sK4,sK2(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_18])],[avatar_definition]) ).
fof(f355,plain,
( model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| ~ spl6_18 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f356,plain,
( spl6_18
| spl6_1
| ~ spl6_3 ),
inference(avatar_split_clause,[],[f351,f87,f70,f353]) ).
fof(f368,plain,
( lesseq(sum(c,max(sK3,sK4)),sK1(sK3,sK4,sK5))
| ~ spl6_10 ),
inference(resolution,[],[f171,f54]) ).
fof(f370,definition,
( spl6_19
<=> lesseq(sum(c,max(sK3,sK4)),sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_19])],[avatar_definition]) ).
fof(f372,plain,
( lesseq(sum(c,max(sK3,sK4)),sK1(sK3,sK4,sK5))
| ~ spl6_19 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( spl6_19
| ~ spl6_10 ),
inference(avatar_split_clause,[],[f368,f169,f370]) ).
fof(f539,plain,
( ! [X0] :
( lesseq(sK5,X0)
| ~ model_max(sK3,sK4,X0) )
| ~ spl6_2 ),
inference(resolution,[],[f75,f59]) ).
fof(f568,definition,
( spl6_22
<=> ! [X0] :
( lesseq(sK5,X0)
| ~ model_max(sK3,sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_22])],[avatar_definition]) ).
fof(f569,plain,
( ! [X0] :
( ~ model_max(sK3,sK4,X0)
| lesseq(sK5,X0) )
| ~ spl6_22 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f570,plain,
( spl6_22
| ~ spl6_2 ),
inference(avatar_split_clause,[],[f539,f74,f568]) ).
fof(f631,plain,
( ~ lesseq(sum(c,sK4),sK5)
| ~ lesseq(sK3,sK4)
| spl6_13 ),
inference(superposition,[],[f205,f50]) ).
fof(f632,plain,
( ~ lesseq(sum(c,sK3),sK5)
| ~ lesseq(sK4,sK3)
| spl6_13 ),
inference(superposition,[],[f205,f49]) ).
fof(f676,plain,
( ! [X0,X1] :
( lesseq(sK5,X0)
| ~ ub(sK3,sK4,X1)
| ~ lesseq(sum(c,X1),X0) )
| ~ spl6_17 ),
inference(resolution,[],[f348,f58]) ).
fof(f818,plain,
( lesseq(sum(c,sK3),sK1(sK3,sK4,sK5))
| ~ lesseq(sK4,sK3)
| ~ spl6_19 ),
inference(superposition,[],[f372,f49]) ).
fof(f857,definition,
( spl6_31
<=> lesseq(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_31])],[avatar_definition]) ).
fof(f858,plain,
( lesseq(sK3,sK4)
| ~ spl6_31 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f859,plain,
( ~ lesseq(sK3,sK4)
| spl6_31 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f866,definition,
( spl6_33
<=> lesseq(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_33])],[avatar_definition]) ).
fof(f867,plain,
( lesseq(sK4,sK3)
| ~ spl6_33 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( ~ lesseq(sK4,sK3)
| spl6_33 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f870,definition,
( spl6_34
<=> lesseq(sum(c,sK3),sK1(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_34])],[avatar_definition]) ).
fof(f872,plain,
( lesseq(sum(c,sK3),sK1(sK3,sK4,sK5))
| ~ spl6_34 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,plain,
( ~ spl6_33
| spl6_34
| ~ spl6_19 ),
inference(avatar_split_clause,[],[f818,f370,f870,f866]) ).
fof(f1183,plain,
( lesseq(sK4,sK3)
| spl6_31 ),
inference(resolution,[],[f859,f44]) ).
fof(f1184,plain,
( lesseq(sK4,sK3)
| spl6_31 ),
inference(resolution,[],[f859,f44]) ).
fof(f1191,plain,
( $false
| spl6_31
| spl6_33 ),
inference(forward_subsumption_resolution,[],[f1184,f868]) ).
fof(f1192,plain,
( spl6_31
| spl6_33 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1195,plain,
( ~ lesseq(sum(c,sK3),sK5)
| spl6_13
| ~ spl6_33 ),
inference(backward_subsumption_resolution,[],[f632,f867]) ).
fof(f1204,plain,
( sK3 = max(sK3,sK4)
| ~ spl6_33 ),
inference(resolution,[],[f867,f49]) ).
fof(f1289,definition,
( spl6_47
<=> ! [X0] :
( lesseq(X0,sK5)
| ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK5))) ) ),
introduced(definition,[new_symbols(definition,[spl6_47])],[avatar_definition]) ).
fof(f1290,plain,
( ! [X0] :
( ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK5)))
| lesseq(X0,sK5) )
| ~ spl6_47 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1291,plain,
( spl6_47
| ~ spl6_4 ),
inference(avatar_split_clause,[],[f103,f97,f1289]) ).
fof(f1302,plain,
( ! [X0] :
( lesseq(sum(c,X0),sK5)
| ~ lesseq(X0,sK0(sK3,sK4,sK5)) )
| ~ spl6_47 ),
inference(resolution,[],[f1290,f45]) ).
fof(f1311,definition,
( spl6_49
<=> sK3 = max(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_49])],[avatar_definition]) ).
fof(f1313,plain,
( sK3 = max(sK3,sK4)
| ~ spl6_49 ),
inference(avatar_component_clause,[],[f1311]) ).
fof(f1314,plain,
( spl6_49
| ~ spl6_33 ),
inference(avatar_split_clause,[],[f1204,f866,f1311]) ).
fof(f1315,plain,
( ~ lesseq(sum(c,sK4),sK5)
| spl6_13
| ~ spl6_31 ),
inference(backward_subsumption_resolution,[],[f631,f858]) ).
fof(f1323,plain,
( spl6_33
| spl6_31 ),
inference(avatar_split_clause,[],[f1183,f857,f866]) ).
fof(f1365,definition,
( spl6_50
<=> lesseq(sum(c,sK3),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_50])],[avatar_definition]) ).
fof(f1366,plain,
( lesseq(sum(c,sK3),sK5)
| ~ spl6_50 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1367,plain,
( ~ lesseq(sum(c,sK3),sK5)
| spl6_50 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1368,plain,
( ~ spl6_50
| spl6_13
| ~ spl6_33 ),
inference(avatar_split_clause,[],[f1195,f866,f204,f1365]) ).
fof(f1693,definition,
( spl6_79
<=> lesseq(sK5,sum(c,max(sK3,sK4))) ),
introduced(definition,[new_symbols(definition,[spl6_79])],[avatar_definition]) ).
fof(f1694,plain,
( ~ lesseq(sK5,sum(c,max(sK3,sK4)))
| spl6_79 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1695,plain,
( lesseq(sK5,sum(c,max(sK3,sK4)))
| ~ spl6_79 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1697,plain,
( lesseq(sK5,sum(c,sK3))
| ~ spl6_49
| ~ spl6_79 ),
inference(forward_demodulation,[],[f1695,f1313]) ).
fof(f1791,plain,
( ! [X0] :
( lesseq(sK3,X0)
| ~ lesseq(sK4,X0) )
| ~ spl6_31 ),
inference(resolution,[],[f858,f42]) ).
fof(f1798,plain,
( sK4 = max(sK3,sK4)
| ~ spl6_31 ),
inference(resolution,[],[f858,f50]) ).
fof(f1899,definition,
( spl6_85
<=> sK4 = max(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_85])],[avatar_definition]) ).
fof(f1901,plain,
( sK4 = max(sK3,sK4)
| ~ spl6_85 ),
inference(avatar_component_clause,[],[f1899]) ).
fof(f1902,plain,
( spl6_85
| ~ spl6_31 ),
inference(avatar_split_clause,[],[f1798,f857,f1899]) ).
fof(f1909,definition,
( spl6_87
<=> lesseq(sum(c,sK4),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_87])],[avatar_definition]) ).
fof(f1910,plain,
( lesseq(sum(c,sK4),sK5)
| ~ spl6_87 ),
inference(avatar_component_clause,[],[f1909]) ).
fof(f1911,plain,
( ~ lesseq(sum(c,sK4),sK5)
| spl6_87 ),
inference(avatar_component_clause,[],[f1909]) ).
fof(f1912,plain,
( ~ spl6_87
| spl6_13
| ~ spl6_31 ),
inference(avatar_split_clause,[],[f1315,f857,f204,f1909]) ).
fof(f2336,definition,
( spl6_112
<=> ! [X0,X1] :
( lesseq(sK5,X0)
| ~ ub(sK3,sK4,X1)
| ~ lesseq(sum(c,X1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_112])],[avatar_definition]) ).
fof(f2337,plain,
( ! [X0,X1] :
( ~ lesseq(sum(c,X1),X0)
| ~ ub(sK3,sK4,X1)
| lesseq(sK5,X0) )
| ~ spl6_112 ),
inference(avatar_component_clause,[],[f2336]) ).
fof(f2338,plain,
( spl6_112
| ~ spl6_17 ),
inference(avatar_split_clause,[],[f676,f347,f2336]) ).
fof(f2374,definition,
( spl6_114
<=> ! [X0] :
( lesseq(sK3,X0)
| ~ lesseq(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_114])],[avatar_definition]) ).
fof(f2375,plain,
( ! [X0] :
( lesseq(sK3,X0)
| ~ lesseq(sK4,X0) )
| ~ spl6_114 ),
inference(avatar_component_clause,[],[f2374]) ).
fof(f2376,plain,
( spl6_114
| ~ spl6_31 ),
inference(avatar_split_clause,[],[f1791,f857,f2374]) ).
fof(f2475,definition,
( spl6_125
<=> ! [X0] :
( lesseq(sum(c,X0),sK5)
| ~ lesseq(X0,sK0(sK3,sK4,sK5)) ) ),
introduced(definition,[new_symbols(definition,[spl6_125])],[avatar_definition]) ).
fof(f2476,plain,
( ! [X0] :
( ~ lesseq(X0,sK0(sK3,sK4,sK5))
| lesseq(sum(c,X0),sK5) )
| ~ spl6_125 ),
inference(avatar_component_clause,[],[f2475]) ).
fof(f2477,plain,
( spl6_125
| ~ spl6_47 ),
inference(avatar_split_clause,[],[f1302,f1289,f2475]) ).
fof(f2493,plain,
( lesseq(sum(c,sK3),sK5)
| ~ spl6_9
| ~ spl6_125 ),
inference(resolution,[],[f2476,f156]) ).
fof(f2494,plain,
( lesseq(sum(c,sK4),sK5)
| ~ spl6_6
| ~ spl6_125 ),
inference(resolution,[],[f2476,f123]) ).
fof(f2495,plain,
( $false
| ~ spl6_6
| spl6_87
| ~ spl6_125 ),
inference(forward_subsumption_resolution,[],[f2494,f1911]) ).
fof(f2496,plain,
( ~ spl6_6
| spl6_87
| ~ spl6_125 ),
inference(avatar_contradiction_clause,[],[f2495]) ).
fof(f2501,plain,
( lesseq(sum(c,sK4),sK5)
| ~ spl6_13
| ~ spl6_85 ),
inference(forward_demodulation,[],[f206,f1901]) ).
fof(f3156,plain,
( $false
| ~ spl6_9
| spl6_50
| ~ spl6_125 ),
inference(forward_subsumption_resolution,[],[f2493,f1367]) ).
fof(f3157,plain,
( ~ spl6_9
| spl6_50
| ~ spl6_125 ),
inference(avatar_contradiction_clause,[],[f3156]) ).
fof(f3582,plain,
( ~ ub(sK3,sK4,max(sK3,sK4))
| lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_19
| ~ spl6_112 ),
inference(resolution,[],[f372,f2337]) ).
fof(f3607,plain,
( ~ ub(sK3,sK4,max(sK3,sK4))
| spl6_7
| ~ spl6_19
| ~ spl6_112 ),
inference(forward_subsumption_resolution,[],[f3582,f138]) ).
fof(f3611,plain,
( ~ ub(sK3,sK4,sK4)
| spl6_7
| ~ spl6_19
| ~ spl6_85
| ~ spl6_112 ),
inference(forward_demodulation,[],[f3607,f1901]) ).
fof(f3909,plain,
( lesseq(sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5))),sK2(sK3,sK4,sK5))
| ~ spl6_18 ),
inference(resolution,[],[f355,f56]) ).
fof(f3921,definition,
( spl6_126
<=> lesseq(sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5))),sK2(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_126])],[avatar_definition]) ).
fof(f3923,plain,
( lesseq(sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5))),sK2(sK3,sK4,sK5))
| ~ spl6_126 ),
inference(avatar_component_clause,[],[f3921]) ).
fof(f3924,plain,
( spl6_126
| ~ spl6_18 ),
inference(avatar_split_clause,[],[f3909,f353,f3921]) ).
fof(f3928,plain,
( ! [X0] :
( lesseq(X0,sK2(sK3,sK4,sK5))
| ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))) )
| ~ spl6_126 ),
inference(resolution,[],[f3923,f42]) ).
fof(f3939,definition,
( spl6_127
<=> lesseq(sK5,sK2(sK3,sK4,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_127])],[avatar_definition]) ).
fof(f3940,plain,
( ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_127 ),
inference(avatar_component_clause,[],[f3939]) ).
fof(f3941,plain,
( lesseq(sK5,sK2(sK3,sK4,sK5))
| ~ spl6_127 ),
inference(avatar_component_clause,[],[f3939]) ).
fof(f4036,definition,
( spl6_128
<=> ub(sK3,sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl6_128])],[avatar_definition]) ).
fof(f4037,plain,
( ub(sK3,sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_128 ),
inference(avatar_component_clause,[],[f4036]) ).
fof(f4038,plain,
( ~ ub(sK3,sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| spl6_128 ),
inference(avatar_component_clause,[],[f4036]) ).
fof(f4270,plain,
( sK5 = sum(c,sK3)
| ~ lesseq(sK5,sum(c,sK3))
| ~ spl6_50 ),
inference(resolution,[],[f1366,f43]) ).
fof(f4277,plain,
( spl6_87
| ~ spl6_13
| ~ spl6_85 ),
inference(avatar_split_clause,[],[f2501,f1899,f204,f1909]) ).
fof(f4283,plain,
( sK5 = sum(c,sK4)
| ~ lesseq(sK5,sum(c,sK4))
| ~ spl6_87 ),
inference(resolution,[],[f1910,f43]) ).
fof(f4291,definition,
( spl6_133
<=> ! [X0] :
( lesseq(X0,sK2(sK3,sK4,sK5))
| ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))) ) ),
introduced(definition,[new_symbols(definition,[spl6_133])],[avatar_definition]) ).
fof(f4292,plain,
( ! [X0] :
( ~ lesseq(X0,sum(c,sK0(sK3,sK4,sK2(sK3,sK4,sK5))))
| lesseq(X0,sK2(sK3,sK4,sK5)) )
| ~ spl6_133 ),
inference(avatar_component_clause,[],[f4291]) ).
fof(f4293,plain,
( spl6_133
| ~ spl6_126 ),
inference(avatar_split_clause,[],[f3928,f3921,f4291]) ).
fof(f4304,plain,
( ! [X0] :
( lesseq(sum(c,X0),sK2(sK3,sK4,sK5))
| ~ lesseq(X0,sK0(sK3,sK4,sK2(sK3,sK4,sK5))) )
| ~ spl6_133 ),
inference(resolution,[],[f4292,f45]) ).
fof(f4317,definition,
( spl6_134
<=> ub(sK3,sK4,sK4) ),
introduced(definition,[new_symbols(definition,[spl6_134])],[avatar_definition]) ).
fof(f4318,plain,
( ub(sK3,sK4,sK4)
| ~ spl6_134 ),
inference(avatar_component_clause,[],[f4317]) ).
fof(f4319,plain,
( ~ ub(sK3,sK4,sK4)
| spl6_134 ),
inference(avatar_component_clause,[],[f4317]) ).
fof(f4320,plain,
( ~ spl6_134
| spl6_7
| ~ spl6_19
| ~ spl6_85
| ~ spl6_112 ),
inference(avatar_split_clause,[],[f3611,f2336,f1899,f370,f136,f4317]) ).
fof(f4331,plain,
( ~ lesseq(sK3,sK4)
| ~ lesseq(sK4,sK4)
| spl6_134 ),
inference(resolution,[],[f4319,f53]) ).
fof(f4332,plain,
( ~ lesseq(sK4,sK4)
| ~ spl6_114
| spl6_134 ),
inference(forward_subsumption_resolution,[],[f4331,f2375]) ).
fof(f4333,plain,
( $false
| ~ spl6_114
| spl6_134 ),
inference(forward_subsumption_resolution,[],[f4332,f41]) ).
fof(f4334,plain,
( ~ spl6_114
| spl6_134 ),
inference(avatar_contradiction_clause,[],[f4333]) ).
fof(f5427,plain,
( ! [X0] :
( lesseq(sK5,X0)
| ~ lesseq(sum(c,max(sK3,sK4)),X0) )
| ~ spl6_22 ),
inference(resolution,[],[f569,f55]) ).
fof(f5592,plain,
( ~ ub(sK3,sK4,sK3)
| lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_34
| ~ spl6_112 ),
inference(resolution,[],[f872,f2337]) ).
fof(f6144,plain,
( ~ model_ub(sK3,sK4,sK2(sK3,sK4,sK5))
| spl6_128 ),
inference(resolution,[],[f4038,f57]) ).
fof(f6181,plain,
( ! [X0] :
( ~ ub(sK3,sK4,X0)
| ~ lesseq(sum(c,X0),sK5) )
| spl6_3 ),
inference(resolution,[],[f88,f58]) ).
fof(f6183,definition,
( spl6_153
<=> ! [X0] :
( ~ ub(sK3,sK4,X0)
| ~ lesseq(sum(c,X0),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl6_153])],[avatar_definition]) ).
fof(f6184,plain,
( ! [X0] :
( ~ lesseq(sum(c,X0),sK5)
| ~ ub(sK3,sK4,X0) )
| ~ spl6_153 ),
inference(avatar_component_clause,[],[f6183]) ).
fof(f6185,plain,
( spl6_153
| spl6_3 ),
inference(avatar_split_clause,[],[f6181,f87,f6183]) ).
fof(f6186,plain,
( ~ ub(sK3,sK4,sK4)
| ~ spl6_87
| ~ spl6_153 ),
inference(resolution,[],[f6184,f1910]) ).
fof(f6191,plain,
( ! [X0,X1] :
( ~ ub(sK3,sK4,max(X0,X1))
| ~ model_max(X0,X1,sK5) )
| ~ spl6_153 ),
inference(resolution,[],[f6184,f54]) ).
fof(f6202,plain,
( $false
| ~ spl6_87
| ~ spl6_134
| ~ spl6_153 ),
inference(forward_subsumption_resolution,[],[f6186,f4318]) ).
fof(f6203,plain,
( ~ spl6_87
| ~ spl6_134
| ~ spl6_153 ),
inference(avatar_contradiction_clause,[],[f6202]) ).
fof(f6307,plain,
( ~ lesseq(sK5,sum(c,sK3))
| ~ spl6_49
| spl6_79 ),
inference(forward_demodulation,[],[f1694,f1313]) ).
fof(f6330,plain,
( ! [X0] :
( ~ lesseq(sum(c,sK3),X0)
| lesseq(sK5,X0) )
| ~ spl6_22
| ~ spl6_49 ),
inference(forward_demodulation,[],[f5427,f1313]) ).
fof(f6405,definition,
( spl6_158
<=> ub(sK3,sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl6_158])],[avatar_definition]) ).
fof(f6406,plain,
( ub(sK3,sK4,sK3)
| ~ spl6_158 ),
inference(avatar_component_clause,[],[f6405]) ).
fof(f6407,plain,
( ~ ub(sK3,sK4,sK3)
| spl6_158 ),
inference(avatar_component_clause,[],[f6405]) ).
fof(f6409,plain,
( ~ lesseq(sK3,sK3)
| ~ lesseq(sK4,sK3)
| spl6_158 ),
inference(resolution,[],[f6407,f53]) ).
fof(f7119,definition,
( spl6_196
<=> ! [X0,X1] :
( ~ ub(sK3,sK4,max(X0,X1))
| ~ model_max(X0,X1,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl6_196])],[avatar_definition]) ).
fof(f7120,plain,
( ! [X0,X1] :
( ~ ub(sK3,sK4,max(X0,X1))
| ~ model_max(X0,X1,sK5) )
| ~ spl6_196 ),
inference(avatar_component_clause,[],[f7119]) ).
fof(f7121,plain,
( spl6_196
| ~ spl6_153 ),
inference(avatar_split_clause,[],[f6191,f6183,f7119]) ).
fof(f7132,plain,
( ~ ub(sK3,sK4,sK3)
| ~ model_max(sK3,sK4,sK5)
| ~ spl6_49
| ~ spl6_196 ),
inference(superposition,[],[f7120,f1313]) ).
fof(f7189,definition,
( spl6_202
<=> ! [X0] :
( ~ lesseq(sum(c,sK3),X0)
| lesseq(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_202])],[avatar_definition]) ).
fof(f7190,plain,
( ! [X0] :
( ~ lesseq(sum(c,sK3),X0)
| lesseq(sK5,X0) )
| ~ spl6_202 ),
inference(avatar_component_clause,[],[f7189]) ).
fof(f7191,plain,
( spl6_202
| ~ spl6_22
| ~ spl6_49 ),
inference(avatar_split_clause,[],[f6330,f1311,f568,f7189]) ).
fof(f7198,plain,
( lesseq(sK5,sum(c,sK3))
| ~ spl6_202 ),
inference(resolution,[],[f7190,f41]) ).
fof(f7221,plain,
( $false
| ~ spl6_49
| spl6_79
| ~ spl6_202 ),
inference(forward_subsumption_resolution,[],[f7198,f6307]) ).
fof(f7222,plain,
( ~ spl6_49
| spl6_79
| ~ spl6_202 ),
inference(avatar_contradiction_clause,[],[f7221]) ).
fof(f7224,plain,
( sK5 = sum(c,sK3)
| ~ spl6_49
| ~ spl6_50
| ~ spl6_79 ),
inference(backward_subsumption_resolution,[],[f4270,f1697]) ).
fof(f8967,plain,
( ~ lesseq(sK4,sK3)
| spl6_158 ),
inference(forward_subsumption_resolution,[],[f6409,f41]) ).
fof(f8968,plain,
( $false
| ~ spl6_33
| spl6_158 ),
inference(forward_subsumption_resolution,[],[f8967,f867]) ).
fof(f8969,plain,
( ~ spl6_33
| spl6_158 ),
inference(avatar_contradiction_clause,[],[f8968]) ).
fof(f8994,plain,
( ~ model_max(sK3,sK4,sK5)
| ~ spl6_49
| ~ spl6_158
| ~ spl6_196 ),
inference(forward_subsumption_resolution,[],[f7132,f6406]) ).
fof(f9024,plain,
( lesseq(sK5,sK1(sK3,sK4,sK5))
| ~ spl6_34
| ~ spl6_112
| ~ spl6_158 ),
inference(forward_subsumption_resolution,[],[f5592,f6406]) ).
fof(f9353,plain,
( $false
| ~ spl6_8
| ~ spl6_49
| ~ spl6_158
| ~ spl6_196 ),
inference(forward_subsumption_resolution,[],[f8994,f141]) ).
fof(f9354,plain,
( ~ spl6_8
| ~ spl6_49
| ~ spl6_158
| ~ spl6_196 ),
inference(avatar_contradiction_clause,[],[f9353]) ).
fof(f9361,plain,
( $false
| spl6_7
| ~ spl6_34
| ~ spl6_112
| ~ spl6_158 ),
inference(forward_subsumption_resolution,[],[f9024,f138]) ).
fof(f9362,plain,
( spl6_7
| ~ spl6_34
| ~ spl6_112
| ~ spl6_158 ),
inference(avatar_contradiction_clause,[],[f9361]) ).
fof(f10252,plain,
( $false
| ~ spl6_18
| spl6_128 ),
inference(forward_subsumption_resolution,[],[f6144,f355]) ).
fof(f10253,plain,
( ~ spl6_18
| spl6_128 ),
inference(avatar_contradiction_clause,[],[f10252]) ).
fof(f11286,plain,
( ~ model_ub(sK3,sK4,sK5)
| ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_1 ),
inference(resolution,[],[f72,f66]) ).
fof(f11441,plain,
( ! [X0] :
( lesseq(sK5,X0)
| ~ lesseq(sum(c,max(sK3,sK4)),X0) )
| ~ spl6_22 ),
inference(resolution,[],[f569,f55]) ).
fof(f11481,plain,
( lesseq(sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_128 ),
inference(resolution,[],[f4037,f51]) ).
fof(f11482,plain,
( lesseq(sK3,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_128 ),
inference(resolution,[],[f4037,f52]) ).
fof(f11745,definition,
( spl6_319
<=> lesseq(sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl6_319])],[avatar_definition]) ).
fof(f11747,plain,
( lesseq(sK4,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_319 ),
inference(avatar_component_clause,[],[f11745]) ).
fof(f11748,plain,
( spl6_319
| ~ spl6_128 ),
inference(avatar_split_clause,[],[f11481,f4036,f11745]) ).
fof(f11930,definition,
( spl6_323
<=> lesseq(sK3,sK0(sK3,sK4,sK2(sK3,sK4,sK5))) ),
introduced(definition,[new_symbols(definition,[spl6_323])],[avatar_definition]) ).
fof(f11932,plain,
( lesseq(sK3,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| ~ spl6_323 ),
inference(avatar_component_clause,[],[f11930]) ).
fof(f11933,plain,
( spl6_323
| ~ spl6_128 ),
inference(avatar_split_clause,[],[f11482,f4036,f11930]) ).
fof(f17789,definition,
( spl6_395
<=> ! [X0] :
( lesseq(sum(c,X0),sK2(sK3,sK4,sK5))
| ~ lesseq(X0,sK0(sK3,sK4,sK2(sK3,sK4,sK5))) ) ),
introduced(definition,[new_symbols(definition,[spl6_395])],[avatar_definition]) ).
fof(f17790,plain,
( ! [X0] :
( ~ lesseq(X0,sK0(sK3,sK4,sK2(sK3,sK4,sK5)))
| lesseq(sum(c,X0),sK2(sK3,sK4,sK5)) )
| ~ spl6_395 ),
inference(avatar_component_clause,[],[f17789]) ).
fof(f17791,plain,
( spl6_395
| ~ spl6_133 ),
inference(avatar_split_clause,[],[f4304,f4291,f17789]) ).
fof(f17816,plain,
( lesseq(sum(c,sK3),sK2(sK3,sK4,sK5))
| ~ spl6_323
| ~ spl6_395 ),
inference(resolution,[],[f17790,f11932]) ).
fof(f17817,plain,
( lesseq(sum(c,sK4),sK2(sK3,sK4,sK5))
| ~ spl6_319
| ~ spl6_395 ),
inference(resolution,[],[f17790,f11747]) ).
fof(f17818,plain,
( lesseq(sK5,sK2(sK3,sK4,sK5))
| ~ spl6_49
| ~ spl6_50
| ~ spl6_79
| ~ spl6_323
| ~ spl6_395 ),
inference(forward_demodulation,[],[f17816,f7224]) ).
fof(f17823,plain,
( $false
| ~ spl6_49
| ~ spl6_50
| ~ spl6_79
| spl6_127
| ~ spl6_323
| ~ spl6_395 ),
inference(forward_subsumption_resolution,[],[f17818,f3940]) ).
fof(f17824,plain,
( ~ spl6_49
| ~ spl6_50
| ~ spl6_79
| spl6_127
| ~ spl6_323
| ~ spl6_395 ),
inference(avatar_contradiction_clause,[],[f17823]) ).
fof(f17850,plain,
( ~ lesseq(sK5,sK2(sK3,sK4,sK5))
| spl6_1
| ~ spl6_3 ),
inference(forward_subsumption_resolution,[],[f11286,f89]) ).
fof(f19539,plain,
( $false
| spl6_1
| ~ spl6_3
| ~ spl6_127 ),
inference(forward_subsumption_resolution,[],[f17850,f3941]) ).
fof(f19540,plain,
( spl6_1
| ~ spl6_3
| ~ spl6_127 ),
inference(avatar_contradiction_clause,[],[f19539]) ).
fof(f19586,plain,
( ! [X0] :
( ~ lesseq(sum(c,sK4),X0)
| lesseq(sK5,X0) )
| ~ spl6_22
| ~ spl6_85 ),
inference(forward_demodulation,[],[f11441,f1901]) ).
fof(f21398,definition,
( spl6_400
<=> ! [X0] :
( ~ lesseq(sum(c,sK4),X0)
| lesseq(sK5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl6_400])],[avatar_definition]) ).
fof(f21399,plain,
( ! [X0] :
( ~ lesseq(sum(c,sK4),X0)
| lesseq(sK5,X0) )
| ~ spl6_400 ),
inference(avatar_component_clause,[],[f21398]) ).
fof(f21400,plain,
( spl6_400
| ~ spl6_22
| ~ spl6_85 ),
inference(avatar_split_clause,[],[f19586,f1899,f568,f21398]) ).
fof(f21409,plain,
( lesseq(sK5,sum(c,sK4))
| ~ spl6_400 ),
inference(resolution,[],[f21399,f41]) ).
fof(f21442,plain,
( sK5 = sum(c,sK4)
| ~ spl6_87
| ~ spl6_400 ),
inference(backward_subsumption_resolution,[],[f4283,f21409]) ).
fof(f23769,plain,
( lesseq(sK5,sK2(sK3,sK4,sK5))
| ~ spl6_87
| ~ spl6_319
| ~ spl6_395
| ~ spl6_400 ),
inference(forward_demodulation,[],[f17817,f21442]) ).
fof(f24150,plain,
( $false
| ~ spl6_87
| spl6_127
| ~ spl6_319
| ~ spl6_395
| ~ spl6_400 ),
inference(forward_subsumption_resolution,[],[f23769,f3940]) ).
fof(f24151,plain,
( ~ spl6_87
| spl6_127
| ~ spl6_319
| ~ spl6_395
| ~ spl6_400 ),
inference(avatar_contradiction_clause,[],[f24150]) ).
cnf(s1,plain,
( ~ spl6_1
| ~ spl6_2 ),
inference(sat_conversion,[],[f77]) ).
cnf(s2,plain,
( spl6_1
| spl6_2 ),
inference(sat_conversion,[],[f81]) ).
cnf(s3,plain,
( ~ spl6_1
| spl6_3 ),
inference(sat_conversion,[],[f90]) ).
cnf(s4,plain,
( ~ spl6_3
| spl6_4 ),
inference(sat_conversion,[],[f100]) ).
cnf(s5,plain,
( ~ spl6_3
| spl6_5 ),
inference(sat_conversion,[],[f116]) ).
cnf(s6,plain,
( ~ spl6_5
| spl6_6 ),
inference(sat_conversion,[],[f124]) ).
cnf(s7,plain,
( spl6_2
| ~ spl6_7
| ~ spl6_8 ),
inference(sat_conversion,[],[f143]) ).
cnf(s8,plain,
( ~ spl6_5
| spl6_9 ),
inference(sat_conversion,[],[f157]) ).
cnf(s9,plain,
( spl6_2
| ~ spl6_8
| spl6_10 ),
inference(sat_conversion,[],[f172]) ).
cnf(s11,plain,
( spl6_1
| spl6_8 ),
inference(sat_conversion,[],[f180]) ).
cnf(s14,plain,
( ~ spl6_8
| spl6_13 ),
inference(sat_conversion,[],[f207]) ).
cnf(s20,plain,
( spl6_8
| ~ spl6_13 ),
inference(sat_conversion,[],[f333]) ).
cnf(s21,plain,
( ~ spl6_1
| spl6_17 ),
inference(sat_conversion,[],[f349]) ).
cnf(s22,plain,
( spl6_1
| ~ spl6_3
| spl6_18 ),
inference(sat_conversion,[],[f356]) ).
cnf(s26,plain,
( ~ spl6_10
| spl6_19 ),
inference(sat_conversion,[],[f373]) ).
cnf(s38,plain,
( ~ spl6_2
| spl6_22 ),
inference(sat_conversion,[],[f570]) ).
cnf(s52,plain,
( ~ spl6_19
| ~ spl6_33
| spl6_34 ),
inference(sat_conversion,[],[f873]) ).
cnf(s67,plain,
( spl6_31
| spl6_33 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s76,plain,
( ~ spl6_4
| spl6_47 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s78,plain,
( ~ spl6_33
| spl6_49 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s81,plain,
( spl6_31
| spl6_33 ),
inference(sat_conversion,[],[f1323]) ).
cnf(s82,plain,
( spl6_13
| ~ spl6_33
| ~ spl6_50 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s125,plain,
( ~ spl6_31
| spl6_85 ),
inference(sat_conversion,[],[f1902]) ).
cnf(s127,plain,
( spl6_13
| ~ spl6_31
| ~ spl6_87 ),
inference(sat_conversion,[],[f1912]) ).
cnf(s153,plain,
( ~ spl6_17
| spl6_112 ),
inference(sat_conversion,[],[f2338]) ).
cnf(s155,plain,
( ~ spl6_31
| spl6_114 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s166,plain,
( ~ spl6_47
| spl6_125 ),
inference(sat_conversion,[],[f2477]) ).
cnf(s167,plain,
( ~ spl6_6
| spl6_87
| ~ spl6_125 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s225,plain,
( ~ spl6_9
| spl6_50
| ~ spl6_125 ),
inference(sat_conversion,[],[f3157]) ).
cnf(s291,plain,
( ~ spl6_18
| spl6_126 ),
inference(sat_conversion,[],[f3924]) ).
cnf(s304,plain,
( ~ spl6_13
| ~ spl6_85
| spl6_87 ),
inference(sat_conversion,[],[f4277]) ).
cnf(s305,plain,
( ~ spl6_126
| spl6_133 ),
inference(sat_conversion,[],[f4293]) ).
cnf(s306,plain,
( spl6_7
| ~ spl6_19
| ~ spl6_85
| ~ spl6_112
| ~ spl6_134 ),
inference(sat_conversion,[],[f4320]) ).
cnf(s307,plain,
( ~ spl6_114
| spl6_134 ),
inference(sat_conversion,[],[f4334]) ).
cnf(s445,plain,
( spl6_3
| spl6_153 ),
inference(sat_conversion,[],[f6185]) ).
cnf(s446,plain,
( ~ spl6_87
| ~ spl6_134
| ~ spl6_153 ),
inference(sat_conversion,[],[f6203]) ).
cnf(s499,plain,
( ~ spl6_153
| spl6_196 ),
inference(sat_conversion,[],[f7121]) ).
cnf(s505,plain,
( ~ spl6_22
| ~ spl6_49
| spl6_202 ),
inference(sat_conversion,[],[f7191]) ).
cnf(s506,plain,
( ~ spl6_49
| spl6_79
| ~ spl6_202 ),
inference(sat_conversion,[],[f7222]) ).
cnf(s630,plain,
( ~ spl6_33
| spl6_158 ),
inference(sat_conversion,[],[f8969]) ).
cnf(s668,plain,
( ~ spl6_8
| ~ spl6_49
| ~ spl6_158
| ~ spl6_196 ),
inference(sat_conversion,[],[f9354]) ).
cnf(s670,plain,
( spl6_7
| ~ spl6_34
| ~ spl6_112
| ~ spl6_158 ),
inference(sat_conversion,[],[f9362]) ).
cnf(s752,plain,
( ~ spl6_18
| spl6_128 ),
inference(sat_conversion,[],[f10253]) ).
cnf(s841,plain,
( ~ spl6_128
| spl6_319 ),
inference(sat_conversion,[],[f11748]) ).
cnf(s847,plain,
( ~ spl6_128
| spl6_323 ),
inference(sat_conversion,[],[f11933]) ).
cnf(s1126,plain,
( ~ spl6_133
| spl6_395 ),
inference(sat_conversion,[],[f17791]) ).
cnf(s1127,plain,
( ~ spl6_49
| ~ spl6_50
| ~ spl6_79
| spl6_127
| ~ spl6_323
| ~ spl6_395 ),
inference(sat_conversion,[],[f17824]) ).
cnf(s1284,plain,
( spl6_1
| ~ spl6_3
| ~ spl6_127 ),
inference(sat_conversion,[],[f19540]) ).
cnf(s1308,plain,
( ~ spl6_22
| ~ spl6_85
| spl6_400 ),
inference(sat_conversion,[],[f21400]) ).
cnf(s1548,plain,
( ~ spl6_87
| spl6_127
| ~ spl6_319
| ~ spl6_395
| ~ spl6_400 ),
inference(sat_conversion,[],[f24151]) ).
cnf(s1642,plain,
( ~ spl6_33
| ~ spl6_196
| ~ spl6_8 ),
inference(rat,[],[s668,s78,s630]) ).
cnf(s1643,plain,
( ~ spl6_153
| ~ spl6_8 ),
inference(rat,[],[s446,s304,s307,s125,s155,s81,s1642,s499,s14]) ).
cnf(s1644,plain,
spl6_1,
inference(rat,[],[s506,s1127,s505,s78,s81,s125,s1308,s1548,s167,s225,s1126,s166,s305,s841,s847,s76,s6,s8,s291,s752,s4,s5,s22,s1284,s445,s1643,s38,s2,s11]) ).
cnf(s1646,plain,
spl6_17,
inference(rat,[],[s21,s1644]) ).
cnf(s1647,plain,
spl6_3,
inference(rat,[],[s3,s1644]) ).
cnf(s1648,plain,
~ spl6_2,
inference(rat,[],[s1,s1644]) ).
cnf(s1651,plain,
spl6_112,
inference(rat,[],[s153,s1646]) ).
cnf(s1655,plain,
spl6_5,
inference(rat,[],[s5,s1647]) ).
cnf(s1656,plain,
spl6_4,
inference(rat,[],[s4,s1647]) ).
cnf(s1663,plain,
spl6_9,
inference(rat,[],[s8,s1655]) ).
cnf(s1664,plain,
spl6_6,
inference(rat,[],[s6,s1655]) ).
cnf(s1672,plain,
spl6_47,
inference(rat,[],[s76,s1656]) ).
cnf(s1694,plain,
spl6_125,
inference(rat,[],[s166,s1672]) ).
cnf(s1712,plain,
spl6_50,
inference(rat,[],[s225,s1663,s1694]) ).
cnf(s1713,plain,
spl6_87,
inference(rat,[],[s167,s1664,s1694]) ).
cnf(s1734,plain,
( ~ spl6_33
| ~ spl6_8 ),
inference(rat,[],[s670,s52,s630,s7,s26,s9,s1651,s1648]) ).
cnf(s1735,plain,
~ spl6_8,
inference(rat,[],[s306,s307,s125,s155,s81,s1734,s26,s7,s9,s1651,s1648]) ).
cnf(s1736,plain,
~ spl6_13,
inference(rat,[],[s20,s1735]) ).
cnf(s1739,plain,
~ spl6_31,
inference(rat,[],[s127,s1713,s1736]) ).
cnf(s1743,plain,
~ spl6_33,
inference(rat,[],[s82,s1712,s1736]) ).
cnf(s1752,plain,
$false,
inference(rat,[],[s67,s1743,s1739]) ).
fof(f25300,plain,
$false,
inference(avatar_sat_refutation,[],[s1752]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM861+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n006.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 21:36:44 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.42/3.56 % (3336150)Detected formulas, will run a generic FOF schedule.
% 18.42/3.56 % (3336200)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=196175457:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 18.42/3.56 % (3336205)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4014930120:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 18.42/3.56 % (3336201)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=3863862208:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 18.42/3.56 % (3336203)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4245482459:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 18.42/3.56 % (3336202)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=2208634784:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 18.42/3.56 % (3336203)Refutation not found, incomplete strategy
% 18.42/3.56 % (3336203)------------------------------
% 18.42/3.56 % (3336203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.56 % (3336203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.56 % (3336203)CaDiCaL version: 2.1.3
% 18.42/3.56 % (3336203)Termination reason: Refutation not found, incomplete strategy
% 18.42/3.56 % (3336203)Time elapsed: 0.001 s
% 18.42/3.56 % (3336203)Peak memory usage: 87 MB
% 18.42/3.56 % (3336206)dis-21_1_sil=8000:lcm=predicate:random_seed=2278544862: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)
% 18.42/3.56 % (3336204)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3021864373:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 18.42/3.56 % (3336206)Instruction limit reached!
% 18.42/3.56 % (3336206)------------------------------
% 18.42/3.56 % (3336206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.56 % (3336206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.56 % (3336206)CaDiCaL version: 2.1.3
% 18.42/3.56 % (3336206)Termination reason: Instruction limit
% 18.42/3.56 % (3336206)Termination phase: Saturation
% 18.42/3.56 % (3336206)Time elapsed: 0.083 s
% 18.42/3.56 % (3336206)Peak memory usage: 90 MB
% 18.42/3.56 % (3336206)Instructions burned: 131 (million)
% 18.42/3.56 % (3336205)Instruction limit reached!
% 18.42/3.56 % (3336205)------------------------------
% 18.42/3.56 % (3336205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.56 % (3336205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.56 % (3336205)CaDiCaL version: 2.1.3
% 18.42/3.56 % (3336205)Termination reason: Instruction limit
% 18.42/3.56 % (3336205)Termination phase: Saturation
% 18.42/3.56 % (3336205)Time elapsed: 0.094 s
% 18.42/3.56 % (3336205)Peak memory usage: 89 MB
% 18.42/3.56 % (3336205)Instructions burned: 140 (million)
% 18.42/3.56 % (3336204)Instruction limit reached!
% 18.42/3.56 % (3336204)------------------------------
% 18.42/3.56 % (3336204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.56 % (3336204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.56 % (3336204)CaDiCaL version: 2.1.3
% 18.42/3.56 % (3336204)Termination reason: Instruction limit
% 18.42/3.56 % (3336204)Termination phase: Saturation
% 18.42/3.56 % (3336204)Time elapsed: 0.085 s
% 18.42/3.56 % (3336204)Peak memory usage: 88 MB
% 18.42/3.56 % (3336204)Instructions burned: 120 (million)
% 18.42/3.56 % (3336203)------------------------------
% 18.42/3.56 % (3336203)------------------------------
% 18.42/3.56 % (3336215)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3630381418:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.42/3.56 % (3336214)lrs+10_1_sil=8000:sp=occurrence:random_seed=3664274190:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 18.42/3.56 % (3336215)Refutation not found, incomplete strategy
% 18.42/3.56 % (3336215)------------------------------
% 18.42/3.56 % (3336215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.42/3.56 % (3336215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.42/3.56 % (3336215)CaDiCaL version: 2.1.3
% 18.42/3.56 % (3336215)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336215)Time elapsed: 0.002 s
% 28.14/5.01 % (3336215)Peak memory usage: 88 MB
% 28.14/5.01 % (3336215)Instructions burned: 1 (million)
% 28.14/5.01 % (3336216)lrs+1011_1_sil=32000:sp=occurrence:random_seed=17036163:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 28.14/5.01 % (3336216)Refutation not found, incomplete strategy
% 28.14/5.01 % (3336216)------------------------------
% 28.14/5.01 % (3336216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336216)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336216)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336216)Time elapsed: 0.002 s
% 28.14/5.01 % (3336216)Peak memory usage: 88 MB
% 28.14/5.01 % (3336214)Instruction limit reached!
% 28.14/5.01 % (3336214)------------------------------
% 28.14/5.01 % (3336214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336214)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336214)Termination reason: Instruction limit
% 28.14/5.01 % (3336214)Termination phase: Saturation
% 28.14/5.01 % (3336214)Time elapsed: 0.240 s
% 28.14/5.01 % (3336214)Peak memory usage: 90 MB
% 28.14/5.01 % (3336214)Instructions burned: 286 (million)
% 28.14/5.01 % (3336219)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=3784235730:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 28.14/5.01 % (3336215)------------------------------
% 28.14/5.01 % (3336215)------------------------------
% 28.14/5.01 % (3336216)------------------------------
% 28.14/5.01 % (3336216)------------------------------
% 28.14/5.01 % (3336219)Instruction limit reached!
% 28.14/5.01 % (3336219)------------------------------
% 28.14/5.01 % (3336219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336219)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336219)Termination reason: Instruction limit
% 28.14/5.01 % (3336219)Termination phase: Saturation
% 28.14/5.01 % (3336219)Time elapsed: 0.257 s
% 28.14/5.01 % (3336219)Peak memory usage: 91 MB
% 28.14/5.01 % (3336219)Instructions burned: 248 (million)
% 28.14/5.01 % (3336233)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3061331104:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 28.14/5.01 % (3336233)Refutation not found, incomplete strategy
% 28.14/5.01 % (3336233)------------------------------
% 28.14/5.01 % (3336233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336233)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336233)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336233)Time elapsed: 0.002 s
% 28.14/5.01 % (3336233)Peak memory usage: 88 MB
% 28.14/5.01 % (3336233)Instructions burned: 1 (million)
% 28.14/5.01 % (3336238)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3811729807:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 28.14/5.01 % (3336241)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4214282418:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 28.14/5.01 % (3336243)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1201925999:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 28.14/5.01 % (3336233)------------------------------
% 28.14/5.01 % (3336233)------------------------------
% 28.14/5.01 % (3336241)Instruction limit reached!
% 28.14/5.01 % (3336241)------------------------------
% 28.14/5.01 % (3336241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336241)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336241)Termination reason: Instruction limit
% 28.14/5.01 % (3336241)Termination phase: Saturation
% 28.14/5.01 % (3336241)Time elapsed: 0.131 s
% 28.14/5.01 % (3336241)Peak memory usage: 90 MB
% 28.14/5.01 % (3336241)Instructions burned: 113 (million)
% 28.14/5.01 % (3336243)Instruction limit reached!
% 28.14/5.01 % (3336243)------------------------------
% 28.14/5.01 % (3336243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336243)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336243)Termination reason: Instruction limit
% 28.14/5.01 % (3336243)Termination phase: Saturation
% 28.14/5.01 % (3336243)Time elapsed: 0.111 s
% 28.14/5.01 % (3336243)Peak memory usage: 88 MB
% 28.14/5.01 % (3336243)Instructions burned: 128 (million)
% 28.14/5.01 % (3336253)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2861814485:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 28.14/5.01 % (3336254)lrs+10_1_sil=8000:sp=occurrence:random_seed=3615106707:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 28.14/5.01 % (3336253)Instruction limit reached!
% 28.14/5.01 % (3336253)------------------------------
% 28.14/5.01 % (3336253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336253)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336253)Termination reason: Instruction limit
% 28.14/5.01 % (3336253)Termination phase: Saturation
% 28.14/5.01 % (3336253)Time elapsed: 0.092 s
% 28.14/5.01 % (3336253)Peak memory usage: 88 MB
% 28.14/5.01 % (3336253)Instructions burned: 115 (million)
% 28.14/5.01 % (3336256)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4274979429:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 28.14/5.01 % (3336263)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3220680831:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 28.14/5.01 % (3336256)Instruction limit reached!
% 28.14/5.01 % (3336256)------------------------------
% 28.14/5.01 % (3336256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336256)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336256)Termination reason: Instruction limit
% 28.14/5.01 % (3336256)Termination phase: Saturation
% 28.14/5.01 % (3336256)Time elapsed: 0.331 s
% 28.14/5.01 % (3336256)Peak memory usage: 89 MB
% 28.14/5.01 % (3336256)Instructions burned: 438 (million)
% 28.14/5.01 % (3336275)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3933068412:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 28.14/5.01 % (3336254)Instruction limit reached!
% 28.14/5.01 % (3336254)------------------------------
% 28.14/5.01 % (3336254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336254)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336254)Termination reason: Instruction limit
% 28.14/5.01 % (3336254)Termination phase: Saturation
% 28.14/5.01 % (3336254)Time elapsed: 0.808 s
% 28.14/5.01 % (3336254)Peak memory usage: 93 MB
% 28.14/5.01 % (3336254)Instructions burned: 907 (million)
% 28.14/5.01 % (3336275)Instruction limit reached!
% 28.14/5.01 % (3336275)------------------------------
% 28.14/5.01 % (3336275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336275)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336275)Termination reason: Instruction limit
% 28.14/5.01 % (3336275)Termination phase: Saturation
% 28.14/5.01 % (3336275)Time elapsed: 0.145 s
% 28.14/5.01 % (3336275)Peak memory usage: 90 MB
% 28.14/5.01 % (3336275)Instructions burned: 134 (million)
% 28.14/5.01 % (3336279)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1455760121:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 28.14/5.01 % (3336279)Refutation not found, incomplete strategy
% 28.14/5.01 % (3336279)------------------------------
% 28.14/5.01 % (3336279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336279)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336279)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336279)Time elapsed: 0.003 s
% 28.14/5.01 % (3336279)Peak memory usage: 88 MB
% 28.14/5.01 % (3336279)Instructions burned: 1 (million)
% 28.14/5.01 % (3336280)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1134989839:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 28.14/5.01 % (3336279)------------------------------
% 28.14/5.01 % (3336279)------------------------------
% 28.14/5.01 % (3336288)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=1706202629:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 28.14/5.01 % (3336288)Instruction limit reached!
% 28.14/5.01 % (3336288)------------------------------
% 28.14/5.01 % (3336288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336288)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336288)Termination reason: Instruction limit
% 28.14/5.01 % (3336288)Termination phase: Saturation
% 28.14/5.01 % (3336288)Time elapsed: 0.107 s
% 28.14/5.01 % (3336288)Peak memory usage: 91 MB
% 28.14/5.01 % (3336288)Instructions burned: 125 (million)
% 28.14/5.01 % (3336238)Instruction limit reached!
% 28.14/5.01 % (3336238)------------------------------
% 28.14/5.01 % (3336238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336238)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336238)Termination reason: Instruction limit
% 28.14/5.01 % (3336238)Termination phase: Saturation
% 28.14/5.01 % (3336238)Time elapsed: 2.555 s
% 28.14/5.01 % (3336238)Peak memory usage: 140 MB
% 28.14/5.01 % (3336238)Instructions burned: 2350 (million)
% 28.14/5.01 % (3336292)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3869072526:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 28.14/5.01 % (3336202)First to succeed.
% 28.14/5.01 % (3336202)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3336150"
% 28.14/5.01 % (3336292)Instruction limit reached!
% 28.14/5.01 % (3336292)------------------------------
% 28.14/5.01 % (3336292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336292)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336292)Termination reason: Instruction limit
% 28.14/5.01 % (3336292)Termination phase: Saturation
% 28.14/5.01 % (3336292)Time elapsed: 0.094 s
% 28.14/5.01 % (3336292)Peak memory usage: 88 MB
% 28.14/5.01 % (3336292)Instructions burned: 134 (million)
% 28.14/5.01 % (3336295)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2603293472:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/141Mi)
% 28.14/5.01 % (3336295)Refutation not found, incomplete strategy
% 28.14/5.01 % (3336295)------------------------------
% 28.14/5.01 % (3336295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336295)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336295)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336295)Time elapsed: 0.002 s
% 28.14/5.01 % (3336295)Peak memory usage: 88 MB
% 28.14/5.01 % (3336297)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3885972984:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2962 on theBenchmark for (2962ds/431Mi)
% 28.14/5.01 % (3336297)Refutation not found, incomplete strategy
% 28.14/5.01 % (3336297)------------------------------
% 28.14/5.01 % (3336297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.14/5.01 % (3336297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.14/5.01 % (3336297)CaDiCaL version: 2.1.3
% 28.14/5.01 % (3336297)Termination reason: Refutation not found, incomplete strategy
% 28.14/5.01 % (3336297)Time elapsed: 0.002 s
% 28.14/5.01 % (3336297)Peak memory usage: 88 MB
% 28.14/5.01 % (3336202)Refutation found. Thanks to Tanya!
% 28.14/5.01 % SZS status Theorem for theBenchmark
% 28.14/5.01 % SZS output start Proof for theBenchmark
% See solution above
% 29.79/5.30 % (3336202)------------------------------
% 29.79/5.30 % (3336202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.79/5.30 % (3336202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.79/5.30 % (3336202)CaDiCaL version: 2.1.3
% 29.79/5.30 % (3336202)Termination reason: Refutation
% 29.79/5.30 % (3336202)Time elapsed: 3.519 s
% 29.79/5.30 % (3336202)Peak memory usage: 147 MB
% 29.79/5.30 % (3336202)Instructions burned: 3291 (million)
% 29.79/5.30 % (3336202)------------------------------
% 29.79/5.30 % (3336202)------------------------------
% 29.79/5.30 % (3336150)Success in time 4.13 s
% 29.79/5.30 % Vampire exiting
%------------------------------------------------------------------------------