%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV029+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:07:57 PM UTC 2026
% Result : Theorem 5.59s 1.73s
% Output : Refutation 0.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 27
% Syntax : Number of formulae : 244 ( 25 unt; 24 def)
% Number of atoms : 1640 ( 430 equ)
% Maximal formula atoms : 58 ( 6 avg)
% Number of connectives : 2244 ( 848 ~;1101 |; 247 &)
% ( 21 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 25 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 25 con; 0-3 aty)
% Number of variables : 109 ( 0 sgn 85 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f48,axiom,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel2_update_1) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( X0 != X1
& a_select2(X2,X1) = X3 )
=> a_select2(tptp_update2(X2,X0,X4),X1) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sel2_update_2) ).
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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [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(tptp_update2(s_values7_init,pv1376,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/sandbox2/benchmark/theBenchmark.p',gauss_init_0029) ).
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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [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(tptp_update2(s_values7_init,pv1376,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(f87,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [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(tptp_update2(s_values7_init,pv1376,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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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(f88,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [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(tptp_update2(s_values7_init,pv1376,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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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,[],[f87]) ).
fof(f100,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(ennf_transformation,[],[f49]) ).
fof(f101,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(flattening,[],[f100]) ).
fof(f111,definition,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f112,definition,
( ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f113,definition,
( ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f114,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| ? [X7] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X7)
& leq(n0,X7)
& leq(X7,n3) )
| sP2
| sP1
| ( ( 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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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,[],[f88,f113,f112,f111]) ).
fof(f115,plain,
( ? [X8] :
( init != a_select2(s_center7_init,X8)
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP2 ),
inference(nnf_transformation,[],[f113]) ).
fof(f116,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP2 ),
inference(rectify,[],[f115]) ).
fof(f117,plain,
( ( init != a_select2(s_center7_init,sK3)
& leq(n0,sK3)
& leq(sK3,n2) )
| ~ sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f116]) ).
fof(f118,plain,
( ? [X9] :
( init != a_select2(s_try7_init,X9)
& leq(n0,X9)
& leq(X9,minus(n3,n1)) )
| ~ sP1 ),
inference(nnf_transformation,[],[f112]) ).
fof(f119,plain,
( ? [X0] :
( init != a_select2(s_try7_init,X0)
& leq(n0,X0)
& leq(X0,minus(n3,n1)) )
| ~ sP1 ),
inference(rectify,[],[f118]) ).
fof(f120,plain,
( ( init != a_select2(s_try7_init,sK4)
& leq(n0,sK4)
& leq(sK4,minus(n3,n1)) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X0,sK4)],[f119]) ).
fof(f121,plain,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP0 ),
inference(nnf_transformation,[],[f111]) ).
fof(f122,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP0 ),
inference(rectify,[],[f121]) ).
fof(f123,plain,
( ( init != a_select3(simplex7_init,sK6,sK5)
& leq(n0,sK6)
& leq(sK6,n3)
& leq(n0,sK5)
& leq(sK5,n2) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X0,sK5),skolemize(X1,sK6)],[f122]) ).
fof(f124,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| ? [X0] :
( init != a_select2(tptp_update2(s_values7_init,pv1376,init),X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP2
| sP1
| ( ( 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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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,[],[f114]) ).
fof(f125,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| ( init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK7)
& leq(n0,sK7)
& leq(sK7,n3) )
| sP2
| sP1
| ( ( 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,pv1376)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1376,n3)
& ! [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,[sK7]),skolemize(X0,sK7)],[f124]) ).
fof(f127,plain,
( leq(sK3,n2)
| ~ sP2 ),
inference(cnf_transformation,[],[f117]) ).
fof(f128,plain,
( leq(n0,sK3)
| ~ sP2 ),
inference(cnf_transformation,[],[f117]) ).
fof(f129,plain,
( init != a_select2(s_center7_init,sK3)
| ~ sP2 ),
inference(cnf_transformation,[],[f117]) ).
fof(f130,plain,
( leq(sK4,minus(n3,n1))
| ~ sP1 ),
inference(cnf_transformation,[],[f120]) ).
fof(f131,plain,
( leq(n0,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f120]) ).
fof(f132,plain,
( init != a_select2(s_try7_init,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f120]) ).
fof(f133,plain,
( leq(sK5,n2)
| ~ sP0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f134,plain,
( leq(n0,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f135,plain,
( leq(sK6,n3)
| ~ sP0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f136,plain,
( leq(n0,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f137,plain,
( init != a_select3(simplex7_init,sK6,sK5)
| ~ sP0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f138,plain,
( init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f139,plain,
( init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f140,plain,
( init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f141,plain,
! [X5] :
( init = a_select2(s_try7_init,X5)
| ~ leq(n0,X5)
| ~ leq(X5,minus(n3,n1)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f142,plain,
! [X4] :
( init = a_select2(s_center7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,n2) ),
inference(cnf_transformation,[],[f125]) ).
fof(f143,plain,
! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n3) ),
inference(cnf_transformation,[],[f125]) ).
fof(f144,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,[],[f125]) ).
fof(f146,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f125]) ).
fof(f147,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f125]) ).
fof(f148,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f125]) ).
fof(f150,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f125]) ).
fof(f151,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f125]) ).
fof(f152,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f125]) ).
fof(f153,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f125]) ).
fof(f154,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f125]) ).
fof(f155,plain,
init = s_best7_init,
inference(cnf_transformation,[],[f125]) ).
fof(f157,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f158,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f125]) ).
fof(f159,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f160,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f125]) ).
fof(f161,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f162,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| init != a_select2(tptp_update2(s_values7_init,pv1376,init),sK7)
| sP2
| sP1
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f125]) ).
fof(f174,plain,
! [X2,X3,X0,X1,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(cnf_transformation,[],[f101]) ).
fof(f175,plain,
! [X2,X0,X1] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f48]) ).
fof(f191,plain,
( s_best7_init != a_select2(s_center7_init,sK3)
| ~ sP2 ),
inference(definition_unfolding,[],[f129,f155]) ).
fof(f192,plain,
( s_best7_init != a_select2(s_try7_init,sK4)
| ~ sP1 ),
inference(definition_unfolding,[],[f132,f155]) ).
fof(f193,plain,
( s_best7_init != a_select3(simplex7_init,sK6,sK5)
| ~ sP0 ),
inference(definition_unfolding,[],[f137,f155]) ).
fof(f194,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f162,f155,f155,f155,f155,f155,f155,f155,f155,f155,f155]) ).
fof(f195,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f161,f155,f155,f155,f155,f155,f155,f155]) ).
fof(f196,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f160,f155,f155,f155,f155,f155,f155,f155,f155]) ).
fof(f197,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f159,f155,f155,f155,f155,f155]) ).
fof(f198,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(definition_unfolding,[],[f158,f155,f155,f155,f155,f155,f155,f155,f155]) ).
fof(f199,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f157,f155,f155,f155,f155,f155]) ).
fof(f201,plain,
s_best7_init = s_sworst7_init,
inference(definition_unfolding,[],[f154,f155]) ).
fof(f202,plain,
s_best7_init = s_worst7_init,
inference(definition_unfolding,[],[f153,f155]) ).
fof(f203,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,[],[f144,f155]) ).
fof(f204,plain,
! [X3] :
( ~ leq(n0,X3)
| s_best7_init = a_select2(s_values7_init,X3)
| ~ leq(X3,n3) ),
inference(definition_unfolding,[],[f143,f155]) ).
fof(f205,plain,
! [X4] :
( ~ leq(n0,X4)
| s_best7_init = a_select2(s_center7_init,X4)
| ~ leq(X4,n2) ),
inference(definition_unfolding,[],[f142,f155]) ).
fof(f206,plain,
! [X5] :
( ~ leq(X5,minus(n3,n1))
| ~ leq(n0,X5)
| s_best7_init = a_select2(s_try7_init,X5) ),
inference(definition_unfolding,[],[f141,f155]) ).
fof(f207,plain,
( s_best7_init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f140,f155]) ).
fof(f208,plain,
( s_best7_init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f139,f155]) ).
fof(f209,plain,
( s_best7_init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f138,f155]) ).
fof(f210,plain,
! [X2,X0,X1,X4] :
( a_select2(X2,X1) = a_select2(tptp_update2(X2,X0,X4),X1)
| X0 = X1 ),
inference(equality_resolution,[],[f174]) ).
fof(f211,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f199]) ).
fof(f212,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f211]) ).
fof(f213,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f198]) ).
fof(f214,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f213]) ).
fof(f215,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f197]) ).
fof(f216,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f215]) ).
fof(f217,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f196]) ).
fof(f218,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f217]) ).
fof(f219,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f195]) ).
fof(f220,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f219]) ).
fof(f221,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f194]) ).
fof(f222,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(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f221]) ).
fof(f224,definition,
( spl9_1
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f228,definition,
( spl9_2
<=> s_best7_init = pvar1402_init ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f231,plain,
( ~ spl9_1
| spl9_2 ),
inference(avatar_split_clause,[],[f209,f228,f224]) ).
fof(f233,definition,
( spl9_3
<=> s_best7_init = pvar1401_init ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f236,plain,
( ~ spl9_1
| spl9_3 ),
inference(avatar_split_clause,[],[f208,f233,f224]) ).
fof(f238,definition,
( spl9_4
<=> s_best7_init = pvar1400_init ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f241,plain,
( ~ spl9_1
| spl9_4 ),
inference(avatar_split_clause,[],[f207,f238,f224]) ).
fof(f242,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f212,f201]) ).
fof(f243,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f214,f201]) ).
fof(f244,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f216,f201]) ).
fof(f245,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f218,f201]) ).
fof(f246,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f220,f201]) ).
fof(f247,plain,
( s_best7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f222,f201]) ).
fof(f249,definition,
( spl9_5
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
fof(f253,definition,
( spl9_6
<=> leq(sK5,n2) ),
introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition]) ).
fof(f255,plain,
( leq(sK5,n2)
| ~ spl9_6 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,plain,
( ~ spl9_5
| spl9_6 ),
inference(avatar_split_clause,[],[f133,f253,f249]) ).
fof(f258,definition,
( spl9_7
<=> leq(n0,sK5) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
fof(f260,plain,
( leq(n0,sK5)
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f261,plain,
( ~ spl9_5
| spl9_7 ),
inference(avatar_split_clause,[],[f134,f258,f249]) ).
fof(f263,definition,
( spl9_8
<=> leq(sK6,n3) ),
introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition]) ).
fof(f265,plain,
( leq(sK6,n3)
| ~ spl9_8 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( ~ spl9_5
| spl9_8 ),
inference(avatar_split_clause,[],[f135,f263,f249]) ).
fof(f268,definition,
( spl9_9
<=> leq(n0,sK6) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
fof(f270,plain,
( leq(n0,sK6)
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f271,plain,
( ~ spl9_5
| spl9_9 ),
inference(avatar_split_clause,[],[f136,f268,f249]) ).
fof(f273,definition,
( spl9_10
<=> s_best7_init = a_select3(simplex7_init,sK6,sK5) ),
introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition]) ).
fof(f275,plain,
( s_best7_init != a_select3(simplex7_init,sK6,sK5)
| spl9_10 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f276,plain,
( ~ spl9_5
| ~ spl9_10 ),
inference(avatar_split_clause,[],[f193,f273,f249]) ).
fof(f278,definition,
( spl9_11
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f282,definition,
( spl9_12
<=> leq(sK4,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl9_12])],[avatar_definition]) ).
fof(f284,plain,
( leq(sK4,minus(n3,n1))
| ~ spl9_12 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,plain,
( ~ spl9_11
| spl9_12 ),
inference(avatar_split_clause,[],[f130,f282,f278]) ).
fof(f287,definition,
( spl9_13
<=> leq(n0,sK4) ),
introduced(definition,[new_symbols(definition,[spl9_13])],[avatar_definition]) ).
fof(f289,plain,
( leq(n0,sK4)
| ~ spl9_13 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,plain,
( ~ spl9_11
| spl9_13 ),
inference(avatar_split_clause,[],[f131,f287,f278]) ).
fof(f292,definition,
( spl9_14
<=> s_best7_init = a_select2(s_try7_init,sK4) ),
introduced(definition,[new_symbols(definition,[spl9_14])],[avatar_definition]) ).
fof(f294,plain,
( s_best7_init != a_select2(s_try7_init,sK4)
| spl9_14 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
( ~ spl9_11
| ~ spl9_14 ),
inference(avatar_split_clause,[],[f192,f292,f278]) ).
fof(f297,definition,
( spl9_15
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl9_15])],[avatar_definition]) ).
fof(f301,definition,
( spl9_16
<=> leq(sK3,n2) ),
introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition]) ).
fof(f303,plain,
( leq(sK3,n2)
| ~ spl9_16 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( ~ spl9_15
| spl9_16 ),
inference(avatar_split_clause,[],[f127,f301,f297]) ).
fof(f306,definition,
( spl9_17
<=> leq(n0,sK3) ),
introduced(definition,[new_symbols(definition,[spl9_17])],[avatar_definition]) ).
fof(f308,plain,
( leq(n0,sK3)
| ~ spl9_17 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( ~ spl9_15
| spl9_17 ),
inference(avatar_split_clause,[],[f128,f306,f297]) ).
fof(f311,definition,
( spl9_18
<=> s_best7_init = a_select2(s_center7_init,sK3) ),
introduced(definition,[new_symbols(definition,[spl9_18])],[avatar_definition]) ).
fof(f313,plain,
( s_best7_init != a_select2(s_center7_init,sK3)
| spl9_18 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,plain,
( ~ spl9_15
| ~ spl9_18 ),
inference(avatar_split_clause,[],[f191,f311,f297]) ).
fof(f315,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f242,f202]) ).
fof(f316,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f243,f202]) ).
fof(f317,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f244,f202]) ).
fof(f318,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f245,f202]) ).
fof(f319,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f246,f202]) ).
fof(f320,plain,
( ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f247,f202]) ).
fof(f321,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f315,f152]) ).
fof(f322,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f316,f152]) ).
fof(f323,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f317,f152]) ).
fof(f324,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f318,f152]) ).
fof(f325,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f319,f152]) ).
fof(f326,plain,
( ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f320,f152]) ).
fof(f327,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f321,f151]) ).
fof(f328,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f322,f151]) ).
fof(f329,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f323,f151]) ).
fof(f330,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f324,f151]) ).
fof(f331,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f325,f151]) ).
fof(f332,plain,
( ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f326,f151]) ).
fof(f333,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f327,f150]) ).
fof(f334,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f328,f150]) ).
fof(f335,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f329,f150]) ).
fof(f336,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f330,f150]) ).
fof(f337,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f331,f150]) ).
fof(f338,plain,
( ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f332,f150]) ).
fof(f339,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f333,f148]) ).
fof(f340,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f334,f148]) ).
fof(f341,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f335,f148]) ).
fof(f342,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f336,f148]) ).
fof(f343,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f337,f148]) ).
fof(f344,plain,
( ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f338,f148]) ).
fof(f345,plain,
( ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f339,f147]) ).
fof(f346,plain,
( ~ leq(s_worst7,n3)
| sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f340,f147]) ).
fof(f347,plain,
( ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f341,f147]) ).
fof(f348,plain,
( ~ leq(s_worst7,n3)
| sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f342,f147]) ).
fof(f349,plain,
( ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f343,f147]) ).
fof(f350,plain,
( ~ leq(s_worst7,n3)
| sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f344,f147]) ).
fof(f351,plain,
( sP0
| leq(sK7,n3)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f345,f146]) ).
fof(f352,plain,
( sP0
| leq(sK7,n3)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f346,f146]) ).
fof(f353,plain,
( sP0
| leq(n0,sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f347,f146]) ).
fof(f354,plain,
( sP0
| leq(n0,sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f348,f146]) ).
fof(f355,plain,
( sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| gt(loopcounter,n1) ),
inference(forward_subsumption_resolution,[],[f349,f146]) ).
fof(f356,plain,
( sP0
| s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| sP2
| sP1
| s_best7_init != pvar1400_init
| s_best7_init != pvar1401_init
| s_best7_init != pvar1402_init ),
inference(forward_subsumption_resolution,[],[f350,f146]) ).
fof(f358,definition,
( spl9_19
<=> leq(sK7,n3) ),
introduced(definition,[new_symbols(definition,[spl9_19])],[avatar_definition]) ).
fof(f360,plain,
( leq(sK7,n3)
| ~ spl9_19 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f361,plain,
( spl9_1
| spl9_11
| spl9_15
| spl9_19
| spl9_5 ),
inference(avatar_split_clause,[],[f351,f249,f358,f297,f278,f224]) ).
fof(f362,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_11
| spl9_15
| spl9_19
| spl9_5 ),
inference(avatar_split_clause,[],[f352,f249,f358,f297,f278,f238,f233,f228]) ).
fof(f364,definition,
( spl9_20
<=> leq(n0,sK7) ),
introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition]) ).
fof(f366,plain,
( leq(n0,sK7)
| ~ spl9_20 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f367,plain,
( spl9_1
| spl9_11
| spl9_15
| spl9_20
| spl9_5 ),
inference(avatar_split_clause,[],[f353,f249,f364,f297,f278,f224]) ).
fof(f368,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_11
| spl9_15
| spl9_20
| spl9_5 ),
inference(avatar_split_clause,[],[f354,f249,f364,f297,f278,f238,f233,f228]) ).
fof(f370,definition,
( spl9_21
<=> s_best7_init = a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7) ),
introduced(definition,[new_symbols(definition,[spl9_21])],[avatar_definition]) ).
fof(f372,plain,
( s_best7_init != a_select2(tptp_update2(s_values7_init,pv1376,s_best7_init),sK7)
| spl9_21 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( spl9_1
| spl9_11
| spl9_15
| ~ spl9_21
| spl9_5 ),
inference(avatar_split_clause,[],[f355,f249,f370,f297,f278,f224]) ).
fof(f374,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_11
| spl9_15
| ~ spl9_21
| spl9_5 ),
inference(avatar_split_clause,[],[f356,f249,f370,f297,f278,f238,f233,f228]) ).
fof(f384,plain,
( ~ leq(n0,sK6)
| ~ spl9_6
| ~ spl9_7
| ~ spl9_8
| spl9_10 ),
inference(unit_resulting_resolution,[],[f203,f255,f260,f275,f265]) ).
fof(f385,plain,
( $false
| ~ spl9_6
| ~ spl9_7
| ~ spl9_8
| ~ spl9_9
| spl9_10 ),
inference(forward_subsumption_resolution,[],[f384,f270]) ).
fof(f386,plain,
( ~ spl9_6
| ~ spl9_7
| ~ spl9_8
| ~ spl9_9
| spl9_10 ),
inference(avatar_contradiction_clause,[],[f385]) ).
fof(f388,plain,
( s_best7_init = a_select2(s_values7_init,sK7)
| ~ spl9_19
| ~ spl9_20 ),
inference(unit_resulting_resolution,[],[f204,f360,f366]) ).
fof(f494,plain,
( s_best7_init != a_select2(s_values7_init,sK7)
| pv1376 = sK7
| spl9_21 ),
inference(superposition,[],[f372,f210]) ).
fof(f495,plain,
( pv1376 = sK7
| ~ spl9_19
| ~ spl9_20
| spl9_21 ),
inference(forward_subsumption_resolution,[],[f494,f388]) ).
fof(f554,plain,
( s_best7_init != a_select2(tptp_update2(s_values7_init,sK7,s_best7_init),sK7)
| ~ spl9_19
| ~ spl9_20
| spl9_21 ),
inference(superposition,[],[f372,f495]) ).
fof(f558,plain,
( $false
| ~ spl9_19
| ~ spl9_20
| spl9_21 ),
inference(forward_subsumption_resolution,[],[f554,f175]) ).
fof(f559,plain,
( ~ spl9_19
| ~ spl9_20
| spl9_21 ),
inference(avatar_contradiction_clause,[],[f558]) ).
fof(f591,plain,
( ~ leq(sK4,minus(n3,n1))
| ~ spl9_13
| spl9_14 ),
inference(unit_resulting_resolution,[],[f206,f294,f289]) ).
fof(f597,plain,
( $false
| ~ spl9_12
| ~ spl9_13
| spl9_14 ),
inference(forward_subsumption_resolution,[],[f591,f284]) ).
fof(f598,plain,
( ~ spl9_12
| ~ spl9_13
| spl9_14 ),
inference(avatar_contradiction_clause,[],[f597]) ).
fof(f611,plain,
( ~ leq(n0,sK3)
| ~ spl9_16
| spl9_18 ),
inference(unit_resulting_resolution,[],[f205,f313,f303]) ).
fof(f616,plain,
( $false
| ~ spl9_16
| ~ spl9_17
| spl9_18 ),
inference(forward_subsumption_resolution,[],[f611,f308]) ).
fof(f617,plain,
( ~ spl9_16
| ~ spl9_17
| spl9_18 ),
inference(avatar_contradiction_clause,[],[f616]) ).
cnf(s1,plain,
( ~ spl9_1
| spl9_2 ),
inference(sat_conversion,[],[f231]) ).
cnf(s2,plain,
( ~ spl9_1
| spl9_3 ),
inference(sat_conversion,[],[f236]) ).
cnf(s3,plain,
( ~ spl9_1
| spl9_4 ),
inference(sat_conversion,[],[f241]) ).
cnf(s4,plain,
( ~ spl9_5
| spl9_6 ),
inference(sat_conversion,[],[f256]) ).
cnf(s5,plain,
( ~ spl9_5
| spl9_7 ),
inference(sat_conversion,[],[f261]) ).
cnf(s6,plain,
( ~ spl9_5
| spl9_8 ),
inference(sat_conversion,[],[f266]) ).
cnf(s7,plain,
( ~ spl9_5
| spl9_9 ),
inference(sat_conversion,[],[f271]) ).
cnf(s8,plain,
( ~ spl9_5
| ~ spl9_10 ),
inference(sat_conversion,[],[f276]) ).
cnf(s9,plain,
( ~ spl9_11
| spl9_12 ),
inference(sat_conversion,[],[f285]) ).
cnf(s10,plain,
( ~ spl9_11
| spl9_13 ),
inference(sat_conversion,[],[f290]) ).
cnf(s11,plain,
( ~ spl9_11
| ~ spl9_14 ),
inference(sat_conversion,[],[f295]) ).
cnf(s12,plain,
( ~ spl9_15
| spl9_16 ),
inference(sat_conversion,[],[f304]) ).
cnf(s13,plain,
( ~ spl9_15
| spl9_17 ),
inference(sat_conversion,[],[f309]) ).
cnf(s14,plain,
( ~ spl9_15
| ~ spl9_18 ),
inference(sat_conversion,[],[f314]) ).
cnf(s15,plain,
( spl9_1
| spl9_5
| spl9_11
| spl9_15
| spl9_19 ),
inference(sat_conversion,[],[f361]) ).
cnf(s16,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_5
| spl9_11
| spl9_15
| spl9_19 ),
inference(sat_conversion,[],[f362]) ).
cnf(s17,plain,
( spl9_1
| spl9_5
| spl9_11
| spl9_15
| spl9_20 ),
inference(sat_conversion,[],[f367]) ).
cnf(s18,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_5
| spl9_11
| spl9_15
| spl9_20 ),
inference(sat_conversion,[],[f368]) ).
cnf(s19,plain,
( spl9_1
| spl9_5
| spl9_11
| spl9_15
| ~ spl9_21 ),
inference(sat_conversion,[],[f373]) ).
cnf(s20,plain,
( ~ spl9_2
| ~ spl9_3
| ~ spl9_4
| spl9_5
| spl9_11
| spl9_15
| ~ spl9_21 ),
inference(sat_conversion,[],[f374]) ).
cnf(s21,plain,
( ~ spl9_6
| ~ spl9_7
| ~ spl9_8
| ~ spl9_9
| spl9_10 ),
inference(sat_conversion,[],[f386]) ).
cnf(s22,plain,
( ~ spl9_19
| ~ spl9_20
| spl9_21 ),
inference(sat_conversion,[],[f559]) ).
cnf(s24,plain,
( ~ spl9_12
| ~ spl9_13
| spl9_14 ),
inference(sat_conversion,[],[f598]) ).
cnf(s25,plain,
( ~ spl9_16
| ~ spl9_17
| spl9_18 ),
inference(sat_conversion,[],[f617]) ).
cnf(s26,plain,
( spl9_15
| spl9_11
| spl9_5
| spl9_1 ),
inference(rat,[],[s22,s19,s17,s15]) ).
cnf(s27,plain,
~ spl9_15,
inference(rat,[],[s25,s12,s13,s14]) ).
cnf(s28,plain,
~ spl9_11,
inference(rat,[],[s24,s9,s10,s11]) ).
cnf(s29,plain,
~ spl9_5,
inference(rat,[],[s21,s4,s5,s6,s7,s8]) ).
cnf(s30,plain,
spl9_1,
inference(rat,[],[s26,s28,s27,s29]) ).
cnf(s31,plain,
spl9_4,
inference(rat,[],[s3,s30]) ).
cnf(s32,plain,
spl9_3,
inference(rat,[],[s2,s30]) ).
cnf(s33,plain,
spl9_2,
inference(rat,[],[s1,s30]) ).
cnf(s34,plain,
~ spl9_21,
inference(rat,[],[s20,s31,s27,s28,s32,s29,s33]) ).
cnf(s35,plain,
spl9_20,
inference(rat,[],[s18,s31,s27,s28,s32,s29,s33]) ).
cnf(s36,plain,
spl9_19,
inference(rat,[],[s16,s31,s27,s28,s32,s29,s33]) ).
cnf(s37,plain,
$false,
inference(rat,[],[s22,s34,s35,s36]) ).
fof(f618,plain,
$false,
inference(avatar_sat_refutation,[],[s37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV029+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.30 % Computer : n026.cluster.edu
% 0.27/0.30 % Model : x86_64 x86_64
% 0.27/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.30 % Memory : 8046.5625MB
% 0.27/0.30 % OS : Linux 6.8.0-71-generic
% 0.27/0.30 % CPULimit : 300
% 0.27/0.30 % WCLimit : 300
% 0.27/0.30 % DateTime : Mon Sep 28 09:45:41 UTC 2026
% 0.27/0.30 % CPUTime :
% 0.27/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.36 Running first-order theorem proving
% 0.27/0.36 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
% 5.59/1.73 % (3735302)Detected formulas, will run a generic FOF schedule.
% 5.59/1.73 % (3735309)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=3910059637:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.59/1.73 % (3735307)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=1248550766:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.59/1.73 % (3735308)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=2945017632:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.59/1.73 % (3735311)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2806041388:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.59/1.73 % (3735313)dis-21_1_sil=8000:lcm=predicate:random_seed=2918471717: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)
% 5.59/1.73 % (3735310)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3916483403:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.59/1.73 % (3735312)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3401733051:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.59/1.73 % (3735311)Instruction limit reached!
% 5.59/1.73 % (3735311)------------------------------
% 5.59/1.73 % (3735311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.73 % (3735311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.73 % (3735311)CaDiCaL version: 2.1.3
% 5.59/1.73 % (3735311)Termination reason: Instruction limit
% 5.59/1.73 % (3735311)Termination phase: Saturation
% 5.59/1.73 % (3735311)Time elapsed: 0.104 s
% 5.59/1.73 % (3735311)Peak memory usage: 88 MB
% 5.59/1.73 % (3735311)Instructions burned: 120 (million)
% 5.59/1.73 % (3735310)Instruction limit reached!
% 5.59/1.73 % (3735310)------------------------------
% 5.59/1.73 % (3735310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.73 % (3735310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.73 % (3735310)CaDiCaL version: 2.1.3
% 5.59/1.73 % (3735310)Termination reason: Instruction limit
% 5.59/1.73 % (3735310)Termination phase: Saturation
% 5.59/1.73 % (3735310)Time elapsed: 0.108 s
% 5.59/1.73 % (3735310)Peak memory usage: 89 MB
% 5.59/1.73 % (3735310)Instructions burned: 109 (million)
% 5.59/1.73 % (3735313)Instruction limit reached!
% 5.59/1.73 % (3735313)------------------------------
% 5.59/1.73 % (3735313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.73 % (3735313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.73 % (3735313)CaDiCaL version: 2.1.3
% 5.59/1.73 % (3735313)Termination reason: Instruction limit
% 5.59/1.73 % (3735313)Termination phase: Saturation
% 5.59/1.73 % (3735313)Time elapsed: 0.111 s
% 5.59/1.73 % (3735313)Peak memory usage: 89 MB
% 5.59/1.73 % (3735313)Instructions burned: 130 (million)
% 5.59/1.73 % (3735312)Instruction limit reached!
% 5.59/1.73 % (3735312)------------------------------
% 5.59/1.73 % (3735312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.73 % (3735312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.73 % (3735312)CaDiCaL version: 2.1.3
% 5.59/1.73 % (3735312)Termination reason: Instruction limit
% 5.59/1.73 % (3735312)Termination phase: Saturation
% 5.59/1.73 % (3735312)Time elapsed: 0.089 s
% 5.59/1.73 % (3735312)Peak memory usage: 90 MB
% 5.59/1.73 % (3735312)Instructions burned: 140 (million)
% 5.59/1.73 % (3735324)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=3037721855:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 5.59/1.73 % (3735322)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2194595385:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 5.59/1.73 % (3735323)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2443534482:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 5.59/1.73 % (3735321)lrs+10_1_sil=8000:sp=occurrence:random_seed=806030790:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 5.59/1.73 % (3735322)First to succeed.
% 5.59/1.73 % (3735322)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3735302"
% 5.59/1.73 % (3735323)Also succeeded, but the first one will report.
% 5.59/1.73 % (3735324)Instruction limit reached!
% 5.59/1.73 % (3735324)------------------------------
% 5.59/1.73 % (3735324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.73 % (3735324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.73 % (3735324)CaDiCaL version: 2.1.3
% 5.59/1.73 % (3735324)Termination reason: Instruction limit
% 5.59/1.73 % (3735324)Termination phase: Saturation
% 5.59/1.73 % (3735324)Time elapsed: 0.108 s
% 5.59/1.73 % (3735324)Peak memory usage: 94 MB
% 5.59/1.73 % (3735324)Instructions burned: 249 (million)
% 5.59/1.73 % (3735321)Also succeeded, but the first one will report.
% 5.59/1.73 % (3735329)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4116515735:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 5.59/1.73 % (3735322)Refutation found. Thanks to Tanya!
% 5.59/1.73 % SZS status Theorem for theBenchmark
% 5.59/1.73 % SZS output start Proof for theBenchmark
% See solution above
% 0.34/2.05 % (3735322)------------------------------
% 0.34/2.05 % (3735322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.34/2.05 % (3735322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.34/2.05 % (3735322)CaDiCaL version: 2.1.3
% 0.34/2.05 % (3735322)Termination reason: Refutation
% 0.34/2.05 % (3735322)Time elapsed: 0.029 s
% 0.34/2.05 % (3735322)Peak memory usage: 90 MB
% 0.34/2.05 % (3735322)Instructions burned: 28 (million)
% 0.34/2.05 % (3735322)------------------------------
% 0.34/2.05 % (3735322)------------------------------
% 0.34/2.05 % (3735302)Success in time 0.989 s
% 0.34/2.05 % Vampire exiting
%------------------------------------------------------------------------------