%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV025+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 01:20:01 PM UTC 2026
% Result : Theorem 0.18s 0.29s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 37
% Syntax : Number of formulae : 234 ( 51 unt; 36 def)
% Number of atoms : 1552 ( 324 equ)
% Maximal formula atoms : 66 ( 6 avg)
% Number of connectives : 2183 ( 865 ~; 977 |; 282 &)
% ( 33 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 37 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 29 con; 0-3 aty)
% Number of variables : 81 ( 0 sgn 57 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f53,conjecture,
( ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,minus(n3,n1)) )
=> a_select2(s_try7_init,X4) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,n2) )
=> ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select3(simplex7_init,X6,X5) = init ) )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n3) )
=> a_select2(s_values7_init,X7) = init )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,n2) )
=> a_select2(s_center7_init,X8) = init )
& ! [X9] :
( ( leq(n0,X9)
& leq(X9,minus(n3,n1)) )
=> a_select2(s_try7_init,X9) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0013) ).
fof(f54,negated_conjecture,
~ ( ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,minus(n3,n1)) )
=> a_select2(s_try7_init,X4) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X5] :
( ( leq(n0,X5)
& leq(X5,n2) )
=> ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select3(simplex7_init,X6,X5) = init ) )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n3) )
=> a_select2(s_values7_init,X7) = init )
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,n2) )
=> a_select2(s_center7_init,X8) = init )
& ! [X9] :
( ( leq(n0,X9)
& leq(X9,minus(n3,n1)) )
=> a_select2(s_try7_init,X9) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f151,plain,
( ( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f152,plain,
( ( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(flattening,[],[f151]) ).
fof(f172,definition,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f173,definition,
( ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f174,definition,
( ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f175,plain,
( ( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(definition_folding,[],[f152,f174,f173,f172]) ).
fof(f209,plain,
( ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP6 ),
inference(nnf_transformation,[],[f174]) ).
fof(f210,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP6 ),
inference(rectify,[],[f209]) ).
fof(f211,plain,
( ( init != a_select2(s_center7_init,sK34)
& leq(n0,sK34)
& leq(sK34,n2) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X0,sK34)],[f210]) ).
fof(f212,plain,
( ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ~ sP5 ),
inference(nnf_transformation,[],[f173]) ).
fof(f213,plain,
( ? [X0] :
( init != a_select2(s_try7_init,X0)
& leq(n0,X0)
& leq(X0,minus(n3,n1)) )
| ~ sP5 ),
inference(rectify,[],[f212]) ).
fof(f214,plain,
( ( init != a_select2(s_try7_init,sK35)
& leq(n0,sK35)
& leq(sK35,minus(n3,n1)) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X0,sK35)],[f213]) ).
fof(f215,plain,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP4 ),
inference(nnf_transformation,[],[f172]) ).
fof(f216,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP4 ),
inference(rectify,[],[f215]) ).
fof(f217,plain,
( ( init != a_select3(simplex7_init,sK37,sK36)
& leq(n0,sK37)
& leq(sK37,n3)
& leq(n0,sK36)
& leq(sK36,n2) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X0,sK36),skolemize(X1,sK37)],[f216]) ).
fof(f218,plain,
( ( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n3) )
& ! [X4] :
( init = a_select2(s_center7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,n2) )
& ! [X5] :
( init = a_select2(s_try7_init,X5)
| ~ leq(n0,X5)
| ~ leq(X5,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(rectify,[],[f175]) ).
fof(f219,plain,
( ( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| ( init != a_select2(s_values7_init,sK38)
& leq(n0,sK38)
& leq(sK38,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv7)
& leq(n0,pv19)
& leq(n0,pv20)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv7,minus(n410,n1))
& leq(pv19,minus(n410,n1))
& leq(pv20,minus(n330,n1))
& ! [X1] :
( ! [X2] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
| ~ leq(n0,X1)
| ~ leq(X1,n2) )
& ! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n3) )
& ! [X4] :
( init = a_select2(s_center7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,n2) )
& ! [X5] :
( init = a_select2(s_try7_init,X5)
| ~ leq(n0,X5)
| ~ leq(X5,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X0,sK38)],[f218]) ).
fof(f330,plain,
( leq(sK34,n2)
| ~ sP6 ),
inference(cnf_transformation,[],[f211]) ).
fof(f331,plain,
( leq(n0,sK34)
| ~ sP6 ),
inference(cnf_transformation,[],[f211]) ).
fof(f332,plain,
( init != a_select2(s_center7_init,sK34)
| ~ sP6 ),
inference(cnf_transformation,[],[f211]) ).
fof(f333,plain,
( leq(sK35,minus(n3,n1))
| ~ sP5 ),
inference(cnf_transformation,[],[f214]) ).
fof(f334,plain,
( leq(n0,sK35)
| ~ sP5 ),
inference(cnf_transformation,[],[f214]) ).
fof(f335,plain,
( init != a_select2(s_try7_init,sK35)
| ~ sP5 ),
inference(cnf_transformation,[],[f214]) ).
fof(f336,plain,
( leq(sK36,n2)
| ~ sP4 ),
inference(cnf_transformation,[],[f217]) ).
fof(f337,plain,
( leq(n0,sK36)
| ~ sP4 ),
inference(cnf_transformation,[],[f217]) ).
fof(f338,plain,
( leq(sK37,n3)
| ~ sP4 ),
inference(cnf_transformation,[],[f217]) ).
fof(f339,plain,
( leq(n0,sK37)
| ~ sP4 ),
inference(cnf_transformation,[],[f217]) ).
fof(f340,plain,
( init != a_select3(simplex7_init,sK37,sK36)
| ~ sP4 ),
inference(cnf_transformation,[],[f217]) ).
fof(f341,plain,
( init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f342,plain,
( init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f343,plain,
( init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f344,plain,
! [X5] :
( init = a_select2(s_try7_init,X5)
| ~ leq(n0,X5)
| ~ leq(X5,minus(n3,n1)) ),
inference(cnf_transformation,[],[f219]) ).
fof(f345,plain,
! [X4] :
( init = a_select2(s_center7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,n2) ),
inference(cnf_transformation,[],[f219]) ).
fof(f346,plain,
! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n3) ),
inference(cnf_transformation,[],[f219]) ).
fof(f347,plain,
! [X2,X1] :
( init = a_select3(simplex7_init,X2,X1)
| ~ leq(n0,X2)
| ~ leq(X2,n3)
| ~ leq(n0,X1)
| ~ leq(X1,n2) ),
inference(cnf_transformation,[],[f219]) ).
fof(f348,plain,
leq(pv20,minus(n330,n1)),
inference(cnf_transformation,[],[f219]) ).
fof(f349,plain,
leq(pv19,minus(n410,n1)),
inference(cnf_transformation,[],[f219]) ).
fof(f351,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f219]) ).
fof(f352,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f219]) ).
fof(f353,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f219]) ).
fof(f354,plain,
leq(n0,pv20),
inference(cnf_transformation,[],[f219]) ).
fof(f355,plain,
leq(n0,pv19),
inference(cnf_transformation,[],[f219]) ).
fof(f357,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f219]) ).
fof(f358,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f219]) ).
fof(f359,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f219]) ).
fof(f360,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f219]) ).
fof(f361,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f219]) ).
fof(f362,plain,
init = s_best7_init,
inference(cnf_transformation,[],[f219]) ).
fof(f364,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f365,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f219]) ).
fof(f366,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f367,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f219]) ).
fof(f368,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f219]) ).
fof(f369,plain,
( init != init
| init != s_best7_init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f219]) ).
fof(f438,plain,
( s_best7_init != a_select2(s_center7_init,sK34)
| ~ sP6 ),
inference(definition_unfolding,[],[f332,f362]) ).
fof(f439,plain,
( s_best7_init != a_select2(s_try7_init,sK35)
| ~ sP5 ),
inference(definition_unfolding,[],[f335,f362]) ).
fof(f440,plain,
( s_best7_init != a_select3(simplex7_init,sK37,sK36)
| ~ sP4 ),
inference(definition_unfolding,[],[f340,f362]) ).
fof(f441,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f369,f362,f362,f362,f362,f362,f362,f362,f362,f362]) ).
fof(f442,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f368,f362,f362,f362,f362,f362,f362]) ).
fof(f443,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f367,f362,f362,f362,f362,f362,f362,f362,f362]) ).
fof(f444,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f366,f362,f362,f362,f362,f362]) ).
fof(f445,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f365,f362,f362,f362,f362,f362,f362,f362,f362]) ).
fof(f446,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f364,f362,f362,f362,f362,f362]) ).
fof(f448,plain,
s_best7_init = s_sworst7_init,
inference(definition_unfolding,[],[f361,f362]) ).
fof(f449,plain,
s_best7_init = s_worst7_init,
inference(definition_unfolding,[],[f360,f362]) ).
fof(f450,plain,
! [X2,X1] :
( ~ leq(n0,X2)
| s_best7_init = a_select3(simplex7_init,X2,X1)
| ~ leq(X2,n3)
| ~ leq(n0,X1)
| ~ leq(X1,n2) ),
inference(definition_unfolding,[],[f347,f362]) ).
fof(f451,plain,
! [X3] :
( ~ leq(n0,X3)
| s_best7_init = a_select2(s_values7_init,X3)
| ~ leq(X3,n3) ),
inference(definition_unfolding,[],[f346,f362]) ).
fof(f452,plain,
! [X4] :
( ~ leq(n0,X4)
| s_best7_init = a_select2(s_center7_init,X4)
| ~ leq(X4,n2) ),
inference(definition_unfolding,[],[f345,f362]) ).
fof(f453,plain,
! [X5] :
( ~ leq(X5,minus(n3,n1))
| ~ leq(n0,X5)
| s_best7_init = a_select2(s_try7_init,X5) ),
inference(definition_unfolding,[],[f344,f362]) ).
fof(f454,plain,
( s_best7_init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f343,f362]) ).
fof(f455,plain,
( s_best7_init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f342,f362]) ).
fof(f456,plain,
( s_best7_init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f341,f362]) ).
fof(f465,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f446]) ).
fof(f466,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f465]) ).
fof(f467,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f445]) ).
fof(f468,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(sK38,n3)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f467]) ).
fof(f469,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f444]) ).
fof(f470,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f469]) ).
fof(f471,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f443]) ).
fof(f472,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| leq(n0,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f471]) ).
fof(f473,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f442]) ).
fof(f474,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f473]) ).
fof(f475,plain,
( s_best7_init != s_best7_init
| s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f441]) ).
fof(f476,plain,
( s_best7_init != s_sworst7_init
| s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv19)
| ~ leq(n0,pv20)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv20,minus(n330,n1))
| sP4
| s_best7_init != a_select2(s_values7_init,sK38)
| sP6
| sP5
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f475]) ).
fof(f478,definition,
( spl39_1
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[spl39_1])],[avatar_definition]) ).
fof(f482,definition,
( spl39_2
<=> s_best7_init = pvar1402_init ),
introduced(definition,[new_symbols(definition,[spl39_2])],[avatar_definition]) ).
fof(f485,plain,
( ~ spl39_1
| spl39_2 ),
inference(avatar_split_clause,[],[f456,f482,f478]) ).
fof(f487,definition,
( spl39_3
<=> s_best7_init = pvar1401_init ),
introduced(definition,[new_symbols(definition,[spl39_3])],[avatar_definition]) ).
fof(f490,plain,
( ~ spl39_1
| spl39_3 ),
inference(avatar_split_clause,[],[f455,f487,f478]) ).
fof(f492,definition,
( spl39_4
<=> s_best7_init = pvar1400_init ),
introduced(definition,[new_symbols(definition,[spl39_4])],[avatar_definition]) ).
fof(f495,plain,
( ~ spl39_1
| spl39_4 ),
inference(avatar_split_clause,[],[f454,f492,f478]) ).
fof(f497,definition,
( spl39_5
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl39_5])],[avatar_definition]) ).
fof(f501,definition,
( spl39_6
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl39_6])],[avatar_definition]) ).
fof(f505,definition,
( spl39_7
<=> leq(sK38,n3) ),
introduced(definition,[new_symbols(definition,[spl39_7])],[avatar_definition]) ).
fof(f507,plain,
( leq(sK38,n3)
| ~ spl39_7 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f509,definition,
( spl39_8
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl39_8])],[avatar_definition]) ).
fof(f513,definition,
( spl39_9
<=> leq(pv20,minus(n330,n1)) ),
introduced(definition,[new_symbols(definition,[spl39_9])],[avatar_definition]) ).
fof(f517,definition,
( spl39_10
<=> leq(pv19,minus(n410,n1)) ),
introduced(definition,[new_symbols(definition,[spl39_10])],[avatar_definition]) ).
fof(f521,definition,
( spl39_11
<=> leq(s_worst7,n3) ),
introduced(definition,[new_symbols(definition,[spl39_11])],[avatar_definition]) ).
fof(f525,definition,
( spl39_12
<=> leq(s_sworst7,n3) ),
introduced(definition,[new_symbols(definition,[spl39_12])],[avatar_definition]) ).
fof(f529,definition,
( spl39_13
<=> leq(s_best7,n3) ),
introduced(definition,[new_symbols(definition,[spl39_13])],[avatar_definition]) ).
fof(f533,definition,
( spl39_14
<=> leq(n0,pv20) ),
introduced(definition,[new_symbols(definition,[spl39_14])],[avatar_definition]) ).
fof(f537,definition,
( spl39_15
<=> leq(n0,pv19) ),
introduced(definition,[new_symbols(definition,[spl39_15])],[avatar_definition]) ).
fof(f541,definition,
( spl39_16
<=> leq(n0,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl39_16])],[avatar_definition]) ).
fof(f545,definition,
( spl39_17
<=> leq(n0,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl39_17])],[avatar_definition]) ).
fof(f549,definition,
( spl39_18
<=> leq(n0,s_best7) ),
introduced(definition,[new_symbols(definition,[spl39_18])],[avatar_definition]) ).
fof(f553,definition,
( spl39_19
<=> s_best7_init = s_worst7_init ),
introduced(definition,[new_symbols(definition,[spl39_19])],[avatar_definition]) ).
fof(f557,definition,
( spl39_20
<=> s_best7_init = s_sworst7_init ),
introduced(definition,[new_symbols(definition,[spl39_20])],[avatar_definition]) ).
fof(f560,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_7
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f466,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f505,f501,f497,f478]) ).
fof(f561,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_7
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f468,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f505,f501,f497,f492,f487,f482]) ).
fof(f563,definition,
( spl39_21
<=> leq(n0,sK38) ),
introduced(definition,[new_symbols(definition,[spl39_21])],[avatar_definition]) ).
fof(f565,plain,
( leq(n0,sK38)
| ~ spl39_21 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_21
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f470,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f563,f501,f497,f478]) ).
fof(f567,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_21
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f472,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f563,f501,f497,f492,f487,f482]) ).
fof(f569,definition,
( spl39_22
<=> s_best7_init = a_select2(s_values7_init,sK38) ),
introduced(definition,[new_symbols(definition,[spl39_22])],[avatar_definition]) ).
fof(f572,plain,
( spl39_1
| spl39_5
| spl39_6
| ~ spl39_22
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f474,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f569,f501,f497,f478]) ).
fof(f573,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| ~ spl39_22
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(avatar_split_clause,[],[f476,f557,f553,f549,f545,f541,f537,f533,f529,f525,f521,f517,f513,f509,f569,f501,f497,f492,f487,f482]) ).
fof(f575,definition,
( spl39_23
<=> leq(sK36,n2) ),
introduced(definition,[new_symbols(definition,[spl39_23])],[avatar_definition]) ).
fof(f577,plain,
( leq(sK36,n2)
| ~ spl39_23 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( ~ spl39_8
| spl39_23 ),
inference(avatar_split_clause,[],[f336,f575,f509]) ).
fof(f580,definition,
( spl39_24
<=> leq(n0,sK36) ),
introduced(definition,[new_symbols(definition,[spl39_24])],[avatar_definition]) ).
fof(f582,plain,
( leq(n0,sK36)
| ~ spl39_24 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f583,plain,
( ~ spl39_8
| spl39_24 ),
inference(avatar_split_clause,[],[f337,f580,f509]) ).
fof(f585,definition,
( spl39_25
<=> leq(sK37,n3) ),
introduced(definition,[new_symbols(definition,[spl39_25])],[avatar_definition]) ).
fof(f587,plain,
( leq(sK37,n3)
| ~ spl39_25 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
( ~ spl39_8
| spl39_25 ),
inference(avatar_split_clause,[],[f338,f585,f509]) ).
fof(f590,definition,
( spl39_26
<=> leq(n0,sK37) ),
introduced(definition,[new_symbols(definition,[spl39_26])],[avatar_definition]) ).
fof(f592,plain,
( leq(n0,sK37)
| ~ spl39_26 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f593,plain,
( ~ spl39_8
| spl39_26 ),
inference(avatar_split_clause,[],[f339,f590,f509]) ).
fof(f595,definition,
( spl39_27
<=> s_best7_init = a_select3(simplex7_init,sK37,sK36) ),
introduced(definition,[new_symbols(definition,[spl39_27])],[avatar_definition]) ).
fof(f597,plain,
( s_best7_init != a_select3(simplex7_init,sK37,sK36)
| spl39_27 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f598,plain,
( ~ spl39_8
| ~ spl39_27 ),
inference(avatar_split_clause,[],[f440,f595,f509]) ).
fof(f600,definition,
( spl39_28
<=> leq(sK35,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl39_28])],[avatar_definition]) ).
fof(f602,plain,
( leq(sK35,minus(n3,n1))
| ~ spl39_28 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( ~ spl39_5
| spl39_28 ),
inference(avatar_split_clause,[],[f333,f600,f497]) ).
fof(f605,definition,
( spl39_29
<=> leq(n0,sK35) ),
introduced(definition,[new_symbols(definition,[spl39_29])],[avatar_definition]) ).
fof(f607,plain,
( leq(n0,sK35)
| ~ spl39_29 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f608,plain,
( ~ spl39_5
| spl39_29 ),
inference(avatar_split_clause,[],[f334,f605,f497]) ).
fof(f610,definition,
( spl39_30
<=> s_best7_init = a_select2(s_try7_init,sK35) ),
introduced(definition,[new_symbols(definition,[spl39_30])],[avatar_definition]) ).
fof(f612,plain,
( s_best7_init != a_select2(s_try7_init,sK35)
| spl39_30 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
( ~ spl39_5
| ~ spl39_30 ),
inference(avatar_split_clause,[],[f439,f610,f497]) ).
fof(f615,definition,
( spl39_31
<=> leq(sK34,n2) ),
introduced(definition,[new_symbols(definition,[spl39_31])],[avatar_definition]) ).
fof(f617,plain,
( leq(sK34,n2)
| ~ spl39_31 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f618,plain,
( ~ spl39_6
| spl39_31 ),
inference(avatar_split_clause,[],[f330,f615,f501]) ).
fof(f620,definition,
( spl39_32
<=> leq(n0,sK34) ),
introduced(definition,[new_symbols(definition,[spl39_32])],[avatar_definition]) ).
fof(f622,plain,
( leq(n0,sK34)
| ~ spl39_32 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( ~ spl39_6
| spl39_32 ),
inference(avatar_split_clause,[],[f331,f620,f501]) ).
fof(f625,definition,
( spl39_33
<=> s_best7_init = a_select2(s_center7_init,sK34) ),
introduced(definition,[new_symbols(definition,[spl39_33])],[avatar_definition]) ).
fof(f628,plain,
( ~ spl39_6
| ~ spl39_33 ),
inference(avatar_split_clause,[],[f438,f625,f501]) ).
fof(f629,plain,
spl39_11,
inference(avatar_split_clause,[],[f351,f521]) ).
fof(f630,plain,
spl39_12,
inference(avatar_split_clause,[],[f352,f525]) ).
fof(f631,plain,
spl39_13,
inference(avatar_split_clause,[],[f353,f529]) ).
fof(f632,plain,
spl39_14,
inference(avatar_split_clause,[],[f354,f533]) ).
fof(f633,plain,
spl39_15,
inference(avatar_split_clause,[],[f355,f537]) ).
fof(f634,plain,
spl39_16,
inference(avatar_split_clause,[],[f357,f541]) ).
fof(f635,plain,
spl39_17,
inference(avatar_split_clause,[],[f358,f545]) ).
fof(f636,plain,
spl39_18,
inference(avatar_split_clause,[],[f359,f549]) ).
fof(f637,plain,
spl39_20,
inference(avatar_split_clause,[],[f448,f557]) ).
fof(f638,plain,
spl39_19,
inference(avatar_split_clause,[],[f449,f553]) ).
fof(f639,plain,
spl39_9,
inference(avatar_split_clause,[],[f348,f513]) ).
fof(f640,plain,
spl39_10,
inference(avatar_split_clause,[],[f349,f517]) ).
fof(f647,plain,
( s_best7_init = a_select2(s_values7_init,sK38)
| ~ leq(sK38,n3)
| ~ spl39_21 ),
inference(resolution,[],[f451,f565]) ).
fof(f681,plain,
( s_best7_init = a_select2(s_values7_init,sK38)
| ~ spl39_7
| ~ spl39_21 ),
inference(forward_subsumption_resolution,[],[f647,f507]) ).
fof(f682,plain,
( spl39_22
| ~ spl39_7
| ~ spl39_21 ),
inference(avatar_split_clause,[],[f681,f563,f505,f569]) ).
fof(f856,plain,
( ! [X0] :
( s_best7_init = a_select3(simplex7_init,sK37,X0)
| ~ leq(sK37,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
| ~ spl39_26 ),
inference(resolution,[],[f592,f450]) ).
fof(f893,plain,
( ! [X0] :
( ~ leq(n0,X0)
| s_best7_init = a_select3(simplex7_init,sK37,X0)
| ~ leq(X0,n2) )
| ~ spl39_25
| ~ spl39_26 ),
inference(forward_subsumption_resolution,[],[f856,f587]) ).
fof(f1117,plain,
( s_best7_init = a_select3(simplex7_init,sK37,sK36)
| ~ leq(sK36,n2)
| ~ spl39_24
| ~ spl39_25
| ~ spl39_26 ),
inference(resolution,[],[f893,f582]) ).
fof(f1122,plain,
( ~ leq(sK36,n2)
| ~ spl39_24
| ~ spl39_25
| ~ spl39_26
| spl39_27 ),
inference(forward_subsumption_resolution,[],[f1117,f597]) ).
fof(f1124,plain,
( $false
| ~ spl39_23
| ~ spl39_24
| ~ spl39_25
| ~ spl39_26
| spl39_27 ),
inference(forward_subsumption_resolution,[],[f1122,f577]) ).
fof(f1125,plain,
( ~ spl39_23
| ~ spl39_24
| ~ spl39_25
| ~ spl39_26
| spl39_27 ),
inference(avatar_contradiction_clause,[],[f1124]) ).
fof(f1148,plain,
( s_best7_init = a_select2(s_center7_init,sK34)
| ~ leq(sK34,n2)
| ~ spl39_32 ),
inference(resolution,[],[f622,f452]) ).
fof(f1177,plain,
( s_best7_init = a_select2(s_center7_init,sK34)
| ~ spl39_31
| ~ spl39_32 ),
inference(forward_subsumption_resolution,[],[f1148,f617]) ).
fof(f1178,plain,
( spl39_33
| ~ spl39_31
| ~ spl39_32 ),
inference(avatar_split_clause,[],[f1177,f620,f615,f625]) ).
fof(f1240,plain,
( ~ leq(n0,sK35)
| s_best7_init = a_select2(s_try7_init,sK35)
| ~ spl39_28 ),
inference(resolution,[],[f602,f453]) ).
fof(f1241,plain,
( s_best7_init = a_select2(s_try7_init,sK35)
| ~ spl39_28
| ~ spl39_29 ),
inference(forward_subsumption_resolution,[],[f1240,f607]) ).
fof(f1242,plain,
( $false
| ~ spl39_28
| ~ spl39_29
| spl39_30 ),
inference(forward_subsumption_resolution,[],[f1241,f612]) ).
fof(f1243,plain,
( ~ spl39_28
| ~ spl39_29
| spl39_30 ),
inference(avatar_contradiction_clause,[],[f1242]) ).
cnf(s1,plain,
( ~ spl39_1
| spl39_2 ),
inference(sat_conversion,[],[f485]) ).
cnf(s2,plain,
( ~ spl39_1
| spl39_3 ),
inference(sat_conversion,[],[f490]) ).
cnf(s3,plain,
( ~ spl39_1
| spl39_4 ),
inference(sat_conversion,[],[f495]) ).
cnf(s4,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_7
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(sat_conversion,[],[f560]) ).
cnf(s5,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_7
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20 ),
inference(sat_conversion,[],[f561]) ).
cnf(s6,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20
| spl39_21 ),
inference(sat_conversion,[],[f566]) ).
cnf(s7,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20
| spl39_21 ),
inference(sat_conversion,[],[f567]) ).
cnf(s8,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20
| ~ spl39_22 ),
inference(sat_conversion,[],[f572]) ).
cnf(s9,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_9
| ~ spl39_10
| ~ spl39_11
| ~ spl39_12
| ~ spl39_13
| ~ spl39_14
| ~ spl39_15
| ~ spl39_16
| ~ spl39_17
| ~ spl39_18
| ~ spl39_19
| ~ spl39_20
| ~ spl39_22 ),
inference(sat_conversion,[],[f573]) ).
cnf(s10,plain,
( ~ spl39_8
| spl39_23 ),
inference(sat_conversion,[],[f578]) ).
cnf(s11,plain,
( ~ spl39_8
| spl39_24 ),
inference(sat_conversion,[],[f583]) ).
cnf(s12,plain,
( ~ spl39_8
| spl39_25 ),
inference(sat_conversion,[],[f588]) ).
cnf(s13,plain,
( ~ spl39_8
| spl39_26 ),
inference(sat_conversion,[],[f593]) ).
cnf(s14,plain,
( ~ spl39_8
| ~ spl39_27 ),
inference(sat_conversion,[],[f598]) ).
cnf(s15,plain,
( ~ spl39_5
| spl39_28 ),
inference(sat_conversion,[],[f603]) ).
cnf(s16,plain,
( ~ spl39_5
| spl39_29 ),
inference(sat_conversion,[],[f608]) ).
cnf(s17,plain,
( ~ spl39_5
| ~ spl39_30 ),
inference(sat_conversion,[],[f613]) ).
cnf(s18,plain,
( ~ spl39_6
| spl39_31 ),
inference(sat_conversion,[],[f618]) ).
cnf(s19,plain,
( ~ spl39_6
| spl39_32 ),
inference(sat_conversion,[],[f623]) ).
cnf(s20,plain,
( ~ spl39_6
| ~ spl39_33 ),
inference(sat_conversion,[],[f628]) ).
cnf(s21,plain,
spl39_11,
inference(sat_conversion,[],[f629]) ).
cnf(s22,plain,
spl39_12,
inference(sat_conversion,[],[f630]) ).
cnf(s23,plain,
spl39_13,
inference(sat_conversion,[],[f631]) ).
cnf(s24,plain,
spl39_14,
inference(sat_conversion,[],[f632]) ).
cnf(s25,plain,
spl39_15,
inference(sat_conversion,[],[f633]) ).
cnf(s26,plain,
spl39_16,
inference(sat_conversion,[],[f634]) ).
cnf(s27,plain,
spl39_17,
inference(sat_conversion,[],[f635]) ).
cnf(s28,plain,
spl39_18,
inference(sat_conversion,[],[f636]) ).
cnf(s29,plain,
spl39_20,
inference(sat_conversion,[],[f637]) ).
cnf(s30,plain,
spl39_19,
inference(sat_conversion,[],[f638]) ).
cnf(s31,plain,
spl39_9,
inference(sat_conversion,[],[f639]) ).
cnf(s32,plain,
spl39_10,
inference(sat_conversion,[],[f640]) ).
cnf(s37,plain,
( ~ spl39_7
| ~ spl39_21
| spl39_22 ),
inference(sat_conversion,[],[f682]) ).
cnf(s71,plain,
( ~ spl39_23
| ~ spl39_24
| ~ spl39_25
| ~ spl39_26
| spl39_27 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s75,plain,
( ~ spl39_31
| ~ spl39_32
| spl39_33 ),
inference(sat_conversion,[],[f1178]) ).
cnf(s85,plain,
( ~ spl39_28
| ~ spl39_29
| spl39_30 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s96,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_22 ),
inference(rat,[],[s9,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s97,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_8
| ~ spl39_22 ),
inference(rat,[],[s8,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s98,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_8
| spl39_21 ),
inference(rat,[],[s7,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s99,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_8
| spl39_21 ),
inference(rat,[],[s6,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s100,plain,
( ~ spl39_2
| ~ spl39_3
| ~ spl39_4
| spl39_5
| spl39_6
| spl39_7
| spl39_8 ),
inference(rat,[],[s5,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s101,plain,
( spl39_1
| spl39_5
| spl39_6
| spl39_7
| spl39_8 ),
inference(rat,[],[s4,s29,s30,s28,s27,s26,s25,s24,s23,s22,s21,s32,s31]) ).
cnf(s102,plain,
~ spl39_8,
inference(rat,[],[s71,s10,s11,s12,s13,s14]) ).
cnf(s103,plain,
( spl39_6
| spl39_5
| spl39_1 ),
inference(rat,[],[s37,s99,s97,s101,s102]) ).
cnf(s104,plain,
~ spl39_6,
inference(rat,[],[s75,s18,s19,s20]) ).
cnf(s105,plain,
~ spl39_5,
inference(rat,[],[s85,s15,s16,s17]) ).
cnf(s106,plain,
spl39_1,
inference(rat,[],[s103,s104,s105]) ).
cnf(s107,plain,
spl39_4,
inference(rat,[],[s3,s106]) ).
cnf(s108,plain,
spl39_3,
inference(rat,[],[s2,s106]) ).
cnf(s109,plain,
spl39_2,
inference(rat,[],[s1,s106]) ).
cnf(s110,plain,
~ spl39_22,
inference(rat,[],[s96,s102,s105,s104,s108,s107,s109]) ).
cnf(s111,plain,
spl39_21,
inference(rat,[],[s98,s102,s105,s104,s108,s107,s109]) ).
cnf(s112,plain,
spl39_7,
inference(rat,[],[s100,s107,s105,s104,s108,s102,s109]) ).
cnf(s114,plain,
$false,
inference(rat,[],[s37,s110,s111,s112]) ).
fof(f1244,plain,
$false,
inference(avatar_sat_refutation,[],[s114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV025+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 09:43:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.29 % (246404)Will run a generic schedule for satisfiability detection.
% 0.18/0.29 % (246409)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2091032958_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.29 % (246410)% WARNING: option uhcvi not known.
% 0.18/0.29 % (246410)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2496948351:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.29 % (246411)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2275827387:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.29 % (246412)dis+10_1_sil=32000:sp=arity:random_seed=2325128734:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.29 % (246413)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3260461823:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.29 % (246415)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1203670748:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.29 % (246414)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4117781669:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.29 % TRYING [1]
% 0.18/0.29 % (246415) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-246404-246415"...
% 0.18/0.29 % (246412) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-246404-246412"...
% 0.18/0.29 % TRYING [2]
% 0.18/0.29 % (246413) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-246404-246413"...
% 0.18/0.29 % (246415)...printing done.
% 0.18/0.29 % (246412)...printing done.
% 0.18/0.29 % (246411) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-246404-246411"...
% 0.18/0.29 % (246412)Refutation found. Thanks to Tanya!
% 0.18/0.29 % SZS status Theorem for theBenchmark
% 0.18/0.29 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.29 % (246412)------------------------------
% 0.18/0.29 % (246412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.29 % (246412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.29 % (246412)CaDiCaL version: 2.1.3
% 0.18/0.29 % (246412)Termination reason: Refutation
% 0.18/0.29 % (246412)Time elapsed: 0.022 s
% 0.18/0.29 % (246412)Peak memory usage: 13 MB
% 0.18/0.29 % (246412)Instructions burned: 37 (million)
% 0.18/0.29 % (246404)Success in time 0.063 s
% 0.18/0.29 % Vampire exiting
%------------------------------------------------------------------------------