%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV036+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:02 PM UTC 2026
% Result : Theorem 66.85s 13.54s
% Output : Refutation 66.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 90
% Syntax : Number of formulae : 593 ( 59 unt; 86 def)
% Number of atoms : 4494 (1133 equ)
% Maximal formula atoms : 140 ( 7 avg)
% Number of connectives : 6685 (2784 ~;3212 |; 548 &)
% ( 75 <=>; 66 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 90 ( 88 usr; 87 prp; 0-2 aty)
% Number of functors : 38 ( 38 usr; 36 con; 0-3 aty)
% Number of variables : 176 ( 0 sgn 97 !; 79 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( ( leq(X0,X1)
& leq(X1,X2) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f53,conjecture,
( ( 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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 )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_best7_init = init
& a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_worst7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( init = init
& s_sworst7_init = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( 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)
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,n2) )
=> ! [X5] :
( ( leq(n0,X5)
& leq(X5,n3) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select2(s_values7_init,X6) = init )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n2) )
=> a_select2(s_center7_init,X7) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) )
& ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( init = init
& s_best7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_best7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,n2) )
=> ! [X9] :
( ( leq(n0,X9)
& leq(X9,n3) )
=> a_select3(simplex7_init,X9,X8) = init ) )
& ! [X10] :
( ( leq(n0,X10)
& leq(X10,n3) )
=> a_select2(s_values7_init,X10) = init )
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> a_select2(s_center7_init,X11) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_best7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X12] :
( ( leq(n0,X12)
& leq(X12,n2) )
=> ! [X13] :
( ( leq(n0,X13)
& leq(X13,n3) )
=> a_select3(simplex7_init,X13,X12) = init ) )
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n3) )
=> a_select2(s_values7_init,X14) = init )
& ! [X15] :
( ( leq(n0,X15)
& leq(X15,n2) )
=> a_select2(s_center7_init,X15) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X16] :
( ( leq(n0,X16)
& leq(X16,n2) )
=> ! [X17] :
( ( leq(n0,X17)
& leq(X17,n3) )
=> a_select3(simplex7_init,X17,X16) = init ) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,n3) )
=> a_select2(s_values7_init,X18) = init )
& ! [X19] :
( ( leq(n0,X19)
& leq(X19,n2) )
=> a_select2(s_center7_init,X19) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gauss_init_0057) ).
fof(f54,negated_conjecture,
~ ( ( 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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 )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_best7_init = init
& a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_worst7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( init = init
& s_sworst7_init = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,pv1388) = init
& ( ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( 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)
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,n2) )
=> ! [X5] :
( ( leq(n0,X5)
& leq(X5,n3) )
=> a_select3(simplex7_init,X5,X4) = init ) )
& ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select2(s_values7_init,X6) = init )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n2) )
=> a_select2(s_center7_init,X7) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) )
& ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7))
=> ( init = init
& s_best7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_best7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X8] :
( ( leq(n0,X8)
& leq(X8,n2) )
=> ! [X9] :
( ( leq(n0,X9)
& leq(X9,n3) )
=> a_select3(simplex7_init,X9,X8) = init ) )
& ! [X10] :
( ( leq(n0,X10)
& leq(X10,n3) )
=> a_select2(s_values7_init,X10) = init )
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> a_select2(s_center7_init,X11) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_best7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X12] :
( ( leq(n0,X12)
& leq(X12,n2) )
=> ! [X13] :
( ( leq(n0,X13)
& leq(X13,n3) )
=> a_select3(simplex7_init,X13,X12) = init ) )
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n3) )
=> a_select2(s_values7_init,X14) = init )
& ! [X15] :
( ( leq(n0,X15)
& leq(X15,n2) )
=> a_select2(s_center7_init,X15) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7))
=> ( init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(n0,pv1388)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,n3)
& ! [X16] :
( ( leq(n0,X16)
& leq(X16,n2) )
=> ! [X17] :
( ( leq(n0,X17)
& leq(X17,n3) )
=> a_select3(simplex7_init,X17,X16) = init ) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,n3) )
=> a_select2(s_values7_init,X18) = init )
& ! [X19] :
( ( leq(n0,X19)
& leq(X19,n2) )
=> a_select2(s_center7_init,X19) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f65,axiom,
gt(n2,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gt_2_0) ).
fof(f98,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f99,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f136,plain,
( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| ? [X11] :
( init != a_select2(s_center7_init,X11)
& leq(n0,X11)
& leq(X11,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X12] :
( ? [X13] :
( init != a_select3(simplex7_init,X13,X12)
& leq(n0,X13)
& leq(X13,n3) )
& leq(n0,X12)
& leq(X12,n2) )
| ? [X14] :
( init != a_select2(s_values7_init,X14)
& leq(n0,X14)
& leq(X14,n3) )
| ? [X15] :
( init != a_select2(s_center7_init,X15)
& leq(n0,X15)
& leq(X15,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ( ( init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ? [X18] :
( init != a_select2(s_values7_init,X18)
& leq(n0,X18)
& leq(X18,n3) )
| ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) ) )
& 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f137,plain,
( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| ? [X11] :
( init != a_select2(s_center7_init,X11)
& leq(n0,X11)
& leq(X11,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X12] :
( ? [X13] :
( init != a_select3(simplex7_init,X13,X12)
& leq(n0,X13)
& leq(X13,n3) )
& leq(n0,X12)
& leq(X12,n2) )
| ? [X14] :
( init != a_select2(s_values7_init,X14)
& leq(n0,X14)
& leq(X14,n3) )
| ? [X15] :
( init != a_select2(s_center7_init,X15)
& leq(n0,X15)
& leq(X15,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ( ( init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ? [X18] :
( init != a_select2(s_values7_init,X18)
& leq(n0,X18)
& leq(X18,n3) )
| ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) ) )
& 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(flattening,[],[f136]) ).
fof(f157,definition,
( ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f158,definition,
( ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f159,definition,
( ? [X12] :
( ? [X13] :
( init != a_select3(simplex7_init,X13,X12)
& leq(n0,X13)
& leq(X13,n3) )
& leq(n0,X12)
& leq(X12,n2) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f160,definition,
( ? [X15] :
( init != a_select2(s_center7_init,X15)
& leq(n0,X15)
& leq(X15,n2) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f161,definition,
( ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f162,definition,
( ? [X11] :
( init != a_select2(s_center7_init,X11)
& leq(n0,X11)
& leq(X11,n2) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f163,definition,
( ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f164,definition,
( ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f165,definition,
( ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| sP9
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f166,definition,
( ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| sP10
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| sP12 )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f167,definition,
( ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| ? [X14] :
( init != a_select2(s_values7_init,X14)
& leq(n0,X14)
& leq(X14,n3) )
| sP7
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f168,plain,
( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| ( ( init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| ? [X18] :
( init != a_select2(s_values7_init,X18)
& leq(n0,X18)
& leq(X18,n3) )
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) ) )
& 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(definition_folding,[],[f137,f167,f166,f165,f164,f163,f162,f161,f160,f159,f158,f157]) ).
fof(f202,plain,
( ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| ? [X14] :
( init != a_select2(s_values7_init,X14)
& leq(n0,X14)
& leq(X14,n3) )
| sP7
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ~ sP14 ),
inference(nnf_transformation,[],[f167]) ).
fof(f203,plain,
( ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP7
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ~ sP14 ),
inference(rectify,[],[f202]) ).
fof(f204,plain,
( ( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| ( init != a_select2(s_values7_init,sK42)
& leq(n0,sK42)
& leq(sK42,n3) )
| sP7
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) ) )
& ~ gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) )
| ~ sP14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X0,sK42)],[f203]) ).
fof(f205,plain,
( ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| sP10
| ? [X6] :
( init != a_select2(s_values7_init,X6)
& leq(n0,X6)
& leq(X6,n3) )
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| sP12 )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ~ sP13 ),
inference(nnf_transformation,[],[f166]) ).
fof(f206,plain,
( ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| sP10
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| sP12 )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ~ sP13 ),
inference(rectify,[],[f205]) ).
fof(f207,plain,
( ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| ( ( s_best7_init != 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)
| sP10
| ( init != a_select2(s_values7_init,sK43)
& leq(n0,sK43)
& leq(sK43,n3) )
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| sP12 )
& ~ leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_worst7)) )
| ~ sP13 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X0,sK43)],[f206]) ).
fof(f208,plain,
( ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| sP9
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ~ sP12 ),
inference(nnf_transformation,[],[f165]) ).
fof(f209,plain,
( ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP9
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ~ sP12 ),
inference(rectify,[],[f208]) ).
fof(f210,plain,
( ( ( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| ( init != a_select2(s_values7_init,sK44)
& leq(n0,sK44)
& leq(sK44,n3) )
| sP9
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(a_select2(s_values7,pv1388),a_select2(s_values7,s_sworst7)) )
| ~ sP12 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X0,sK44)],[f209]) ).
fof(f211,plain,
( ? [X7] :
( init != a_select2(s_center7_init,X7)
& leq(n0,X7)
& leq(X7,n2) )
| ~ sP11 ),
inference(nnf_transformation,[],[f164]) ).
fof(f212,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP11 ),
inference(rectify,[],[f211]) ).
fof(f213,plain,
( ( init != a_select2(s_center7_init,sK45)
& leq(n0,sK45)
& leq(sK45,n2) )
| ~ sP11 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X0,sK45)],[f212]) ).
fof(f214,plain,
( ? [X4] :
( ? [X5] :
( init != a_select3(simplex7_init,X5,X4)
& leq(n0,X5)
& leq(X5,n3) )
& leq(n0,X4)
& leq(X4,n2) )
| ~ sP10 ),
inference(nnf_transformation,[],[f163]) ).
fof(f215,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP10 ),
inference(rectify,[],[f214]) ).
fof(f216,plain,
( ( init != a_select3(simplex7_init,sK47,sK46)
& leq(n0,sK47)
& leq(sK47,n3)
& leq(n0,sK46)
& leq(sK46,n2) )
| ~ sP10 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47]),skolemize(X0,sK46),skolemize(X1,sK47)],[f215]) ).
fof(f217,plain,
( ? [X11] :
( init != a_select2(s_center7_init,X11)
& leq(n0,X11)
& leq(X11,n2) )
| ~ sP9 ),
inference(nnf_transformation,[],[f162]) ).
fof(f218,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP9 ),
inference(rectify,[],[f217]) ).
fof(f219,plain,
( ( init != a_select2(s_center7_init,sK48)
& leq(n0,sK48)
& leq(sK48,n2) )
| ~ sP9 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(X0,sK48)],[f218]) ).
fof(f220,plain,
( ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP8 ),
inference(nnf_transformation,[],[f161]) ).
fof(f221,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP8 ),
inference(rectify,[],[f220]) ).
fof(f222,plain,
( ( init != a_select3(simplex7_init,sK50,sK49)
& leq(n0,sK50)
& leq(sK50,n3)
& leq(n0,sK49)
& leq(sK49,n2) )
| ~ sP8 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49,sK50]),skolemize(X0,sK49),skolemize(X1,sK50)],[f221]) ).
fof(f223,plain,
( ? [X15] :
( init != a_select2(s_center7_init,X15)
& leq(n0,X15)
& leq(X15,n2) )
| ~ sP7 ),
inference(nnf_transformation,[],[f160]) ).
fof(f224,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP7 ),
inference(rectify,[],[f223]) ).
fof(f225,plain,
( ( init != a_select2(s_center7_init,sK51)
& leq(n0,sK51)
& leq(sK51,n2) )
| ~ sP7 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X0,sK51)],[f224]) ).
fof(f226,plain,
( ? [X12] :
( ? [X13] :
( init != a_select3(simplex7_init,X13,X12)
& leq(n0,X13)
& leq(X13,n3) )
& leq(n0,X12)
& leq(X12,n2) )
| ~ sP6 ),
inference(nnf_transformation,[],[f159]) ).
fof(f227,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP6 ),
inference(rectify,[],[f226]) ).
fof(f228,plain,
( ( init != a_select3(simplex7_init,sK53,sK52)
& leq(n0,sK53)
& leq(sK53,n3)
& leq(n0,sK52)
& leq(sK52,n2) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52,sK53]),skolemize(X0,sK52),skolemize(X1,sK53)],[f227]) ).
fof(f229,plain,
( ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ~ sP5 ),
inference(nnf_transformation,[],[f158]) ).
fof(f230,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP5 ),
inference(rectify,[],[f229]) ).
fof(f231,plain,
( ( init != a_select2(s_center7_init,sK54)
& leq(n0,sK54)
& leq(sK54,n2) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X0,sK54)],[f230]) ).
fof(f232,plain,
( ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ~ sP4 ),
inference(nnf_transformation,[],[f157]) ).
fof(f233,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,[],[f232]) ).
fof(f234,plain,
( ( init != a_select3(simplex7_init,sK56,sK55)
& leq(n0,sK56)
& leq(sK56,n3)
& leq(n0,sK55)
& leq(sK55,n2) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56]),skolemize(X0,sK55),skolemize(X1,sK56)],[f233]) ).
fof(f235,plain,
( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| ( ( init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) ) )
& 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(rectify,[],[f168]) ).
fof(f236,plain,
( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| ( ( init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| ( init != a_select2(s_values7_init,sK57)
& leq(n0,sK57)
& leq(sK57,n3) )
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(a_select2(s_values7,pv1388),a_select2(s_values7,s_best7)) ) )
& 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(n2,pv1388)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& leq(pv1388,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) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(X0,sK57)],[f235]) ).
fof(f241,plain,
! [X2,X0,X1] :
( ~ leq(X1,X2)
| ~ leq(X0,X1)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f242,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f349,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f350,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f351,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f352,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f353,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| init != a_select2(s_values7_init,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f354,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != a_select2(s_values7_init,pv1388)
| sP13
| init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| init != a_select2(s_values7_init,sK42)
| sP7
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP14 ),
inference(cnf_transformation,[],[f204]) ).
fof(f357,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| leq(sK43,n3)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f358,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| leq(sK43,n3)
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f359,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| leq(n0,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f360,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| leq(n0,sK43)
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f361,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| init != a_select2(s_values7_init,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f362,plain,
( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,pv1388)
| s_best7_init != 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)
| sP10
| init != a_select2(s_values7_init,sK43)
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f207]) ).
fof(f364,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f365,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f366,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f367,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f368,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| init != a_select2(s_values7_init,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f369,plain,
( init != init
| s_best7_init != init
| init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| init != a_select2(s_values7_init,sK44)
| sP9
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP12 ),
inference(cnf_transformation,[],[f210]) ).
fof(f370,plain,
( leq(sK45,n2)
| ~ sP11 ),
inference(cnf_transformation,[],[f213]) ).
fof(f371,plain,
( leq(n0,sK45)
| ~ sP11 ),
inference(cnf_transformation,[],[f213]) ).
fof(f372,plain,
( init != a_select2(s_center7_init,sK45)
| ~ sP11 ),
inference(cnf_transformation,[],[f213]) ).
fof(f373,plain,
( leq(sK46,n2)
| ~ sP10 ),
inference(cnf_transformation,[],[f216]) ).
fof(f374,plain,
( leq(n0,sK46)
| ~ sP10 ),
inference(cnf_transformation,[],[f216]) ).
fof(f375,plain,
( leq(sK47,n3)
| ~ sP10 ),
inference(cnf_transformation,[],[f216]) ).
fof(f376,plain,
( leq(n0,sK47)
| ~ sP10 ),
inference(cnf_transformation,[],[f216]) ).
fof(f377,plain,
( init != a_select3(simplex7_init,sK47,sK46)
| ~ sP10 ),
inference(cnf_transformation,[],[f216]) ).
fof(f378,plain,
( leq(sK48,n2)
| ~ sP9 ),
inference(cnf_transformation,[],[f219]) ).
fof(f379,plain,
( leq(n0,sK48)
| ~ sP9 ),
inference(cnf_transformation,[],[f219]) ).
fof(f380,plain,
( init != a_select2(s_center7_init,sK48)
| ~ sP9 ),
inference(cnf_transformation,[],[f219]) ).
fof(f381,plain,
( leq(sK49,n2)
| ~ sP8 ),
inference(cnf_transformation,[],[f222]) ).
fof(f382,plain,
( leq(n0,sK49)
| ~ sP8 ),
inference(cnf_transformation,[],[f222]) ).
fof(f383,plain,
( leq(sK50,n3)
| ~ sP8 ),
inference(cnf_transformation,[],[f222]) ).
fof(f384,plain,
( leq(n0,sK50)
| ~ sP8 ),
inference(cnf_transformation,[],[f222]) ).
fof(f385,plain,
( init != a_select3(simplex7_init,sK50,sK49)
| ~ sP8 ),
inference(cnf_transformation,[],[f222]) ).
fof(f386,plain,
( leq(sK51,n2)
| ~ sP7 ),
inference(cnf_transformation,[],[f225]) ).
fof(f387,plain,
( leq(n0,sK51)
| ~ sP7 ),
inference(cnf_transformation,[],[f225]) ).
fof(f388,plain,
( init != a_select2(s_center7_init,sK51)
| ~ sP7 ),
inference(cnf_transformation,[],[f225]) ).
fof(f389,plain,
( leq(sK52,n2)
| ~ sP6 ),
inference(cnf_transformation,[],[f228]) ).
fof(f390,plain,
( leq(n0,sK52)
| ~ sP6 ),
inference(cnf_transformation,[],[f228]) ).
fof(f391,plain,
( leq(sK53,n3)
| ~ sP6 ),
inference(cnf_transformation,[],[f228]) ).
fof(f392,plain,
( leq(n0,sK53)
| ~ sP6 ),
inference(cnf_transformation,[],[f228]) ).
fof(f393,plain,
( init != a_select3(simplex7_init,sK53,sK52)
| ~ sP6 ),
inference(cnf_transformation,[],[f228]) ).
fof(f394,plain,
( leq(sK54,n2)
| ~ sP5 ),
inference(cnf_transformation,[],[f231]) ).
fof(f395,plain,
( leq(n0,sK54)
| ~ sP5 ),
inference(cnf_transformation,[],[f231]) ).
fof(f396,plain,
( init != a_select2(s_center7_init,sK54)
| ~ sP5 ),
inference(cnf_transformation,[],[f231]) ).
fof(f397,plain,
( leq(sK55,n2)
| ~ sP4 ),
inference(cnf_transformation,[],[f234]) ).
fof(f398,plain,
( leq(n0,sK55)
| ~ sP4 ),
inference(cnf_transformation,[],[f234]) ).
fof(f399,plain,
( leq(sK56,n3)
| ~ sP4 ),
inference(cnf_transformation,[],[f234]) ).
fof(f400,plain,
( leq(n0,sK56)
| ~ sP4 ),
inference(cnf_transformation,[],[f234]) ).
fof(f401,plain,
( init != a_select3(simplex7_init,sK56,sK55)
| ~ sP4 ),
inference(cnf_transformation,[],[f234]) ).
fof(f402,plain,
( init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f403,plain,
( init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f404,plain,
( init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f405,plain,
! [X4] :
( init = a_select2(s_center7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,n2) ),
inference(cnf_transformation,[],[f236]) ).
fof(f406,plain,
! [X3] :
( init = a_select2(s_values7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f407,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,[],[f236]) ).
fof(f408,plain,
leq(pv1388,n3),
inference(cnf_transformation,[],[f236]) ).
fof(f409,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f236]) ).
fof(f410,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f236]) ).
fof(f411,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f236]) ).
fof(f412,plain,
leq(n2,pv1388),
inference(cnf_transformation,[],[f236]) ).
fof(f413,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f236]) ).
fof(f414,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f236]) ).
fof(f415,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f236]) ).
fof(f416,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f236]) ).
fof(f417,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f236]) ).
fof(f418,plain,
s_best7_init = init,
inference(cnf_transformation,[],[f236]) ).
fof(f420,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f421,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f236]) ).
fof(f422,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f423,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f236]) ).
fof(f424,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| init != a_select2(s_values7_init,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f236]) ).
fof(f425,plain,
( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,pv1388)
| sP14
| init != init
| init != s_sworst7_init
| init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| init != a_select2(s_values7_init,sK57)
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init ),
inference(cnf_transformation,[],[f236]) ).
fof(f436,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f65]) ).
fof(f458,plain,
s_best7_init = s_sworst7_init,
inference(definition_unfolding,[],[f418,f417]) ).
fof(f480,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(definition_unfolding,[],[f354,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417,f417]) ).
fof(f481,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(definition_unfolding,[],[f353,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417,f417]) ).
fof(f482,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(definition_unfolding,[],[f352,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417]) ).
fof(f483,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(definition_unfolding,[],[f351,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417]) ).
fof(f484,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(definition_unfolding,[],[f350,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417]) ).
fof(f485,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(definition_unfolding,[],[f349,f417,f417,f417,f417,f417,f417,f417,f458,f417,f417]) ).
fof(f487,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f362,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f488,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f361,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417]) ).
fof(f489,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f360,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417,f417]) ).
fof(f490,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f359,f417,f417,f417,f417,f417,f458,f417,f417,f417]) ).
fof(f491,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f358,f417,f417,f417,f417,f417,f458,f417,f417,f417,f417,f417,f417]) ).
fof(f492,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(definition_unfolding,[],[f357,f417,f417,f417,f417,f417,f458,f417,f417,f417]) ).
fof(f494,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(definition_unfolding,[],[f369,f417,f417,f458,f417,f417,f417,f417,f417,f417]) ).
fof(f495,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(definition_unfolding,[],[f368,f417,f417,f458,f417,f417,f417]) ).
fof(f496,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(definition_unfolding,[],[f367,f417,f417,f458,f417,f417,f417,f417,f417]) ).
fof(f497,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(definition_unfolding,[],[f366,f417,f417,f458,f417,f417]) ).
fof(f498,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(definition_unfolding,[],[f365,f417,f417,f458,f417,f417,f417,f417,f417]) ).
fof(f499,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(definition_unfolding,[],[f364,f417,f417,f458,f417,f417]) ).
fof(f500,plain,
( s_sworst7_init != a_select2(s_center7_init,sK45)
| ~ sP11 ),
inference(definition_unfolding,[],[f372,f417]) ).
fof(f501,plain,
( s_sworst7_init != a_select3(simplex7_init,sK47,sK46)
| ~ sP10 ),
inference(definition_unfolding,[],[f377,f417]) ).
fof(f502,plain,
( s_sworst7_init != a_select2(s_center7_init,sK48)
| ~ sP9 ),
inference(definition_unfolding,[],[f380,f417]) ).
fof(f503,plain,
( s_sworst7_init != a_select3(simplex7_init,sK50,sK49)
| ~ sP8 ),
inference(definition_unfolding,[],[f385,f417]) ).
fof(f504,plain,
( s_sworst7_init != a_select2(s_center7_init,sK51)
| ~ sP7 ),
inference(definition_unfolding,[],[f388,f417]) ).
fof(f505,plain,
( s_sworst7_init != a_select3(simplex7_init,sK53,sK52)
| ~ sP6 ),
inference(definition_unfolding,[],[f393,f417]) ).
fof(f506,plain,
( s_sworst7_init != a_select2(s_center7_init,sK54)
| ~ sP5 ),
inference(definition_unfolding,[],[f396,f417]) ).
fof(f507,plain,
( s_sworst7_init != a_select3(simplex7_init,sK56,sK55)
| ~ sP4 ),
inference(definition_unfolding,[],[f401,f417]) ).
fof(f508,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(definition_unfolding,[],[f425,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f509,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f424,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f510,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(definition_unfolding,[],[f423,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f511,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f422,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f512,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(definition_unfolding,[],[f421,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f513,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f420,f417,f417,f458,f417,f417,f417,f417,f417,f417,f417]) ).
fof(f515,plain,
s_sworst7_init = s_worst7_init,
inference(definition_unfolding,[],[f416,f417]) ).
fof(f516,plain,
! [X2,X1] :
( ~ leq(X1,n2)
| ~ leq(n0,X2)
| ~ leq(X2,n3)
| ~ leq(n0,X1)
| s_sworst7_init = a_select3(simplex7_init,X2,X1) ),
inference(definition_unfolding,[],[f407,f417]) ).
fof(f517,plain,
! [X3] :
( ~ leq(X3,n3)
| ~ leq(n0,X3)
| s_sworst7_init = a_select2(s_values7_init,X3) ),
inference(definition_unfolding,[],[f406,f417]) ).
fof(f518,plain,
! [X4] :
( ~ leq(X4,n2)
| ~ leq(n0,X4)
| s_sworst7_init = a_select2(s_center7_init,X4) ),
inference(definition_unfolding,[],[f405,f417]) ).
fof(f519,plain,
( s_sworst7_init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f404,f417]) ).
fof(f520,plain,
( s_sworst7_init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f403,f417]) ).
fof(f521,plain,
( s_sworst7_init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f402,f417]) ).
fof(f532,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f513]) ).
fof(f533,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f532]) ).
fof(f534,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f512]) ).
fof(f535,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(sK57,n3)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f534]) ).
fof(f536,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f511]) ).
fof(f537,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f536]) ).
fof(f538,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f510]) ).
fof(f539,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| leq(n0,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f538]) ).
fof(f540,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(duplicate_literal_removal,[],[f509]) ).
fof(f541,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| gt(loopcounter,n1) ),
inference(trivial_inequality_removal,[],[f540]) ).
fof(f542,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(duplicate_literal_removal,[],[f508]) ).
fof(f543,plain,
( s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP14
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP4
| s_sworst7_init != a_select2(s_values7_init,sK57)
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init ),
inference(trivial_inequality_removal,[],[f542]) ).
fof(f544,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f499]) ).
fof(f545,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f544]) ).
fof(f546,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f498]) ).
fof(f547,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(sK44,n3)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f546]) ).
fof(f548,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f497]) ).
fof(f549,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f548]) ).
fof(f550,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f496]) ).
fof(f551,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| leq(n0,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f550]) ).
fof(f552,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f495]) ).
fof(f553,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| gt(loopcounter,n1)
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f552]) ).
fof(f554,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(duplicate_literal_removal,[],[f494]) ).
fof(f555,plain,
( s_sworst7_init != s_worst7_init
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP8
| s_sworst7_init != a_select2(s_values7_init,sK44)
| sP9
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP12 ),
inference(trivial_inequality_removal,[],[f554]) ).
fof(f558,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f492]) ).
fof(f559,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f558]) ).
fof(f560,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f491]) ).
fof(f561,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(sK43,n3)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f560]) ).
fof(f562,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f490]) ).
fof(f563,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f562]) ).
fof(f564,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f489]) ).
fof(f565,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| leq(n0,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f564]) ).
fof(f566,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f488]) ).
fof(f567,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| gt(loopcounter,n1)
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f566]) ).
fof(f568,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(duplicate_literal_removal,[],[f487]) ).
fof(f569,plain,
( s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| s_sworst7_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)
| sP10
| s_sworst7_init != a_select2(s_values7_init,sK43)
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| sP12
| ~ sP13 ),
inference(trivial_inequality_removal,[],[f568]) ).
fof(f571,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f485]) ).
fof(f572,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f571]) ).
fof(f573,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f484]) ).
fof(f574,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(sK42,n3)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f573]) ).
fof(f575,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f483]) ).
fof(f576,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f575]) ).
fof(f577,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f482]) ).
fof(f578,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| leq(n0,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f577]) ).
fof(f579,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f481]) ).
fof(f580,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| gt(loopcounter,n1)
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f579]) ).
fof(f581,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(duplicate_literal_removal,[],[f480]) ).
fof(f582,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| s_sworst7_init != a_select2(s_values7_init,pv1388)
| sP13
| ~ leq(n0,s_best7)
| ~ leq(n0,s_worst7)
| ~ leq(n0,pv1388)
| ~ leq(s_best7,n3)
| ~ leq(s_worst7,n3)
| ~ leq(pv1388,n3)
| sP6
| s_sworst7_init != a_select2(s_values7_init,sK42)
| sP7
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP14 ),
inference(trivial_inequality_removal,[],[f581]) ).
fof(f584,definition,
( spl58_1
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[spl58_1])],[avatar_definition]) ).
fof(f588,definition,
( spl58_2
<=> s_sworst7_init = pvar1402_init ),
introduced(definition,[new_symbols(definition,[spl58_2])],[avatar_definition]) ).
fof(f591,plain,
( ~ spl58_1
| spl58_2 ),
inference(avatar_split_clause,[],[f521,f588,f584]) ).
fof(f593,definition,
( spl58_3
<=> s_sworst7_init = pvar1401_init ),
introduced(definition,[new_symbols(definition,[spl58_3])],[avatar_definition]) ).
fof(f596,plain,
( ~ spl58_1
| spl58_3 ),
inference(avatar_split_clause,[],[f520,f593,f584]) ).
fof(f598,definition,
( spl58_4
<=> s_sworst7_init = pvar1400_init ),
introduced(definition,[new_symbols(definition,[spl58_4])],[avatar_definition]) ).
fof(f601,plain,
( ~ spl58_1
| spl58_4 ),
inference(avatar_split_clause,[],[f519,f598,f584]) ).
fof(f607,definition,
( spl58_6
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl58_6])],[avatar_definition]) ).
fof(f611,definition,
( spl58_7
<=> s_sworst7_init = a_select2(s_values7_init,pv1388) ),
introduced(definition,[new_symbols(definition,[spl58_7])],[avatar_definition]) ).
fof(f615,definition,
( spl58_8
<=> s_sworst7_init = a_select2(s_values7_init,s_best7) ),
introduced(definition,[new_symbols(definition,[spl58_8])],[avatar_definition]) ).
fof(f620,definition,
( spl58_9
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl58_9])],[avatar_definition]) ).
fof(f624,definition,
( spl58_10
<=> leq(sK57,n3) ),
introduced(definition,[new_symbols(definition,[spl58_10])],[avatar_definition]) ).
fof(f626,plain,
( leq(sK57,n3)
| ~ spl58_10 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f628,definition,
( spl58_11
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl58_11])],[avatar_definition]) ).
fof(f632,definition,
( spl58_12
<=> leq(pv1388,n3) ),
introduced(definition,[new_symbols(definition,[spl58_12])],[avatar_definition]) ).
fof(f633,plain,
( leq(pv1388,n3)
| ~ spl58_12 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f636,definition,
( spl58_13
<=> leq(s_worst7,n3) ),
introduced(definition,[new_symbols(definition,[spl58_13])],[avatar_definition]) ).
fof(f637,plain,
( leq(s_worst7,n3)
| ~ spl58_13 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f640,definition,
( spl58_14
<=> leq(s_sworst7,n3) ),
introduced(definition,[new_symbols(definition,[spl58_14])],[avatar_definition]) ).
fof(f641,plain,
( leq(s_sworst7,n3)
| ~ spl58_14 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f644,definition,
( spl58_15
<=> leq(n0,pv1388) ),
introduced(definition,[new_symbols(definition,[spl58_15])],[avatar_definition]) ).
fof(f648,definition,
( spl58_16
<=> leq(n0,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl58_16])],[avatar_definition]) ).
fof(f649,plain,
( leq(n0,s_worst7)
| ~ spl58_16 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f652,definition,
( spl58_17
<=> leq(n0,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl58_17])],[avatar_definition]) ).
fof(f653,plain,
( leq(n0,s_sworst7)
| ~ spl58_17 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f656,definition,
( spl58_18
<=> s_sworst7_init = s_worst7_init ),
introduced(definition,[new_symbols(definition,[spl58_18])],[avatar_definition]) ).
fof(f659,plain,
( spl58_1
| spl58_9
| spl58_10
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f533,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f624,f620,f584]) ).
fof(f660,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_9
| spl58_10
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f535,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f624,f620,f598,f593,f588]) ).
fof(f662,definition,
( spl58_19
<=> leq(n0,sK57) ),
introduced(definition,[new_symbols(definition,[spl58_19])],[avatar_definition]) ).
fof(f665,plain,
( spl58_1
| spl58_9
| spl58_19
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f537,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f662,f620,f584]) ).
fof(f666,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_9
| spl58_19
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f539,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f662,f620,f598,f593,f588]) ).
fof(f668,definition,
( spl58_20
<=> s_sworst7_init = a_select2(s_values7_init,sK57) ),
introduced(definition,[new_symbols(definition,[spl58_20])],[avatar_definition]) ).
fof(f671,plain,
( spl58_1
| spl58_9
| ~ spl58_20
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f541,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f668,f620,f584]) ).
fof(f672,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_9
| ~ spl58_20
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_6
| ~ spl58_7
| ~ spl58_8 ),
inference(avatar_split_clause,[],[f543,f615,f611,f607,f656,f652,f648,f644,f640,f636,f632,f628,f668,f620,f598,f593,f588]) ).
fof(f674,definition,
( spl58_21
<=> leq(sK55,n2) ),
introduced(definition,[new_symbols(definition,[spl58_21])],[avatar_definition]) ).
fof(f676,plain,
( leq(sK55,n2)
| ~ spl58_21 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f677,plain,
( ~ spl58_11
| spl58_21 ),
inference(avatar_split_clause,[],[f397,f674,f628]) ).
fof(f679,definition,
( spl58_22
<=> leq(n0,sK55) ),
introduced(definition,[new_symbols(definition,[spl58_22])],[avatar_definition]) ).
fof(f682,plain,
( ~ spl58_11
| spl58_22 ),
inference(avatar_split_clause,[],[f398,f679,f628]) ).
fof(f684,definition,
( spl58_23
<=> leq(sK56,n3) ),
introduced(definition,[new_symbols(definition,[spl58_23])],[avatar_definition]) ).
fof(f686,plain,
( leq(sK56,n3)
| ~ spl58_23 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f687,plain,
( ~ spl58_11
| spl58_23 ),
inference(avatar_split_clause,[],[f399,f684,f628]) ).
fof(f689,definition,
( spl58_24
<=> leq(n0,sK56) ),
introduced(definition,[new_symbols(definition,[spl58_24])],[avatar_definition]) ).
fof(f692,plain,
( ~ spl58_11
| spl58_24 ),
inference(avatar_split_clause,[],[f400,f689,f628]) ).
fof(f694,definition,
( spl58_25
<=> s_sworst7_init = a_select3(simplex7_init,sK56,sK55) ),
introduced(definition,[new_symbols(definition,[spl58_25])],[avatar_definition]) ).
fof(f697,plain,
( ~ spl58_11
| ~ spl58_25 ),
inference(avatar_split_clause,[],[f507,f694,f628]) ).
fof(f699,definition,
( spl58_26
<=> leq(sK54,n2) ),
introduced(definition,[new_symbols(definition,[spl58_26])],[avatar_definition]) ).
fof(f701,plain,
( leq(sK54,n2)
| ~ spl58_26 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,plain,
( ~ spl58_9
| spl58_26 ),
inference(avatar_split_clause,[],[f394,f699,f620]) ).
fof(f704,definition,
( spl58_27
<=> leq(n0,sK54) ),
introduced(definition,[new_symbols(definition,[spl58_27])],[avatar_definition]) ).
fof(f707,plain,
( ~ spl58_9
| spl58_27 ),
inference(avatar_split_clause,[],[f395,f704,f620]) ).
fof(f709,definition,
( spl58_28
<=> s_sworst7_init = a_select2(s_center7_init,sK54) ),
introduced(definition,[new_symbols(definition,[spl58_28])],[avatar_definition]) ).
fof(f711,plain,
( s_sworst7_init != a_select2(s_center7_init,sK54)
| spl58_28 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f712,plain,
( ~ spl58_9
| ~ spl58_28 ),
inference(avatar_split_clause,[],[f506,f709,f620]) ).
fof(f714,definition,
( spl58_29
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl58_29])],[avatar_definition]) ).
fof(f718,definition,
( spl58_30
<=> leq(sK52,n2) ),
introduced(definition,[new_symbols(definition,[spl58_30])],[avatar_definition]) ).
fof(f720,plain,
( leq(sK52,n2)
| ~ spl58_30 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f721,plain,
( ~ spl58_29
| spl58_30 ),
inference(avatar_split_clause,[],[f389,f718,f714]) ).
fof(f723,definition,
( spl58_31
<=> leq(n0,sK52) ),
introduced(definition,[new_symbols(definition,[spl58_31])],[avatar_definition]) ).
fof(f725,plain,
( leq(n0,sK52)
| ~ spl58_31 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( ~ spl58_29
| spl58_31 ),
inference(avatar_split_clause,[],[f390,f723,f714]) ).
fof(f728,definition,
( spl58_32
<=> leq(sK53,n3) ),
introduced(definition,[new_symbols(definition,[spl58_32])],[avatar_definition]) ).
fof(f730,plain,
( leq(sK53,n3)
| ~ spl58_32 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f731,plain,
( ~ spl58_29
| spl58_32 ),
inference(avatar_split_clause,[],[f391,f728,f714]) ).
fof(f733,definition,
( spl58_33
<=> leq(n0,sK53) ),
introduced(definition,[new_symbols(definition,[spl58_33])],[avatar_definition]) ).
fof(f735,plain,
( leq(n0,sK53)
| ~ spl58_33 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f736,plain,
( ~ spl58_29
| spl58_33 ),
inference(avatar_split_clause,[],[f392,f733,f714]) ).
fof(f738,definition,
( spl58_34
<=> s_sworst7_init = a_select3(simplex7_init,sK53,sK52) ),
introduced(definition,[new_symbols(definition,[spl58_34])],[avatar_definition]) ).
fof(f740,plain,
( s_sworst7_init != a_select3(simplex7_init,sK53,sK52)
| spl58_34 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f741,plain,
( ~ spl58_29
| ~ spl58_34 ),
inference(avatar_split_clause,[],[f505,f738,f714]) ).
fof(f743,definition,
( spl58_35
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl58_35])],[avatar_definition]) ).
fof(f747,definition,
( spl58_36
<=> leq(sK51,n2) ),
introduced(definition,[new_symbols(definition,[spl58_36])],[avatar_definition]) ).
fof(f749,plain,
( leq(sK51,n2)
| ~ spl58_36 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f750,plain,
( ~ spl58_35
| spl58_36 ),
inference(avatar_split_clause,[],[f386,f747,f743]) ).
fof(f752,definition,
( spl58_37
<=> leq(n0,sK51) ),
introduced(definition,[new_symbols(definition,[spl58_37])],[avatar_definition]) ).
fof(f754,plain,
( leq(n0,sK51)
| ~ spl58_37 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f755,plain,
( ~ spl58_35
| spl58_37 ),
inference(avatar_split_clause,[],[f387,f752,f743]) ).
fof(f757,definition,
( spl58_38
<=> s_sworst7_init = a_select2(s_center7_init,sK51) ),
introduced(definition,[new_symbols(definition,[spl58_38])],[avatar_definition]) ).
fof(f760,plain,
( ~ spl58_35
| ~ spl58_38 ),
inference(avatar_split_clause,[],[f504,f757,f743]) ).
fof(f762,definition,
( spl58_39
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl58_39])],[avatar_definition]) ).
fof(f766,definition,
( spl58_40
<=> leq(sK49,n2) ),
introduced(definition,[new_symbols(definition,[spl58_40])],[avatar_definition]) ).
fof(f768,plain,
( leq(sK49,n2)
| ~ spl58_40 ),
inference(avatar_component_clause,[],[f766]) ).
fof(f769,plain,
( ~ spl58_39
| spl58_40 ),
inference(avatar_split_clause,[],[f381,f766,f762]) ).
fof(f771,definition,
( spl58_41
<=> leq(n0,sK49) ),
introduced(definition,[new_symbols(definition,[spl58_41])],[avatar_definition]) ).
fof(f773,plain,
( leq(n0,sK49)
| ~ spl58_41 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f774,plain,
( ~ spl58_39
| spl58_41 ),
inference(avatar_split_clause,[],[f382,f771,f762]) ).
fof(f776,definition,
( spl58_42
<=> leq(sK50,n3) ),
introduced(definition,[new_symbols(definition,[spl58_42])],[avatar_definition]) ).
fof(f778,plain,
( leq(sK50,n3)
| ~ spl58_42 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( ~ spl58_39
| spl58_42 ),
inference(avatar_split_clause,[],[f383,f776,f762]) ).
fof(f781,definition,
( spl58_43
<=> leq(n0,sK50) ),
introduced(definition,[new_symbols(definition,[spl58_43])],[avatar_definition]) ).
fof(f783,plain,
( leq(n0,sK50)
| ~ spl58_43 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f784,plain,
( ~ spl58_39
| spl58_43 ),
inference(avatar_split_clause,[],[f384,f781,f762]) ).
fof(f786,definition,
( spl58_44
<=> s_sworst7_init = a_select3(simplex7_init,sK50,sK49) ),
introduced(definition,[new_symbols(definition,[spl58_44])],[avatar_definition]) ).
fof(f788,plain,
( s_sworst7_init != a_select3(simplex7_init,sK50,sK49)
| spl58_44 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f789,plain,
( ~ spl58_39
| ~ spl58_44 ),
inference(avatar_split_clause,[],[f503,f786,f762]) ).
fof(f791,definition,
( spl58_45
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl58_45])],[avatar_definition]) ).
fof(f795,definition,
( spl58_46
<=> leq(sK48,n2) ),
introduced(definition,[new_symbols(definition,[spl58_46])],[avatar_definition]) ).
fof(f797,plain,
( leq(sK48,n2)
| ~ spl58_46 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f798,plain,
( ~ spl58_45
| spl58_46 ),
inference(avatar_split_clause,[],[f378,f795,f791]) ).
fof(f800,definition,
( spl58_47
<=> leq(n0,sK48) ),
introduced(definition,[new_symbols(definition,[spl58_47])],[avatar_definition]) ).
fof(f802,plain,
( leq(n0,sK48)
| ~ spl58_47 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,plain,
( ~ spl58_45
| spl58_47 ),
inference(avatar_split_clause,[],[f379,f800,f791]) ).
fof(f805,definition,
( spl58_48
<=> s_sworst7_init = a_select2(s_center7_init,sK48) ),
introduced(definition,[new_symbols(definition,[spl58_48])],[avatar_definition]) ).
fof(f808,plain,
( ~ spl58_45
| ~ spl58_48 ),
inference(avatar_split_clause,[],[f502,f805,f791]) ).
fof(f810,definition,
( spl58_49
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl58_49])],[avatar_definition]) ).
fof(f814,definition,
( spl58_50
<=> leq(sK46,n2) ),
introduced(definition,[new_symbols(definition,[spl58_50])],[avatar_definition]) ).
fof(f816,plain,
( leq(sK46,n2)
| ~ spl58_50 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f817,plain,
( ~ spl58_49
| spl58_50 ),
inference(avatar_split_clause,[],[f373,f814,f810]) ).
fof(f819,definition,
( spl58_51
<=> leq(n0,sK46) ),
introduced(definition,[new_symbols(definition,[spl58_51])],[avatar_definition]) ).
fof(f822,plain,
( ~ spl58_49
| spl58_51 ),
inference(avatar_split_clause,[],[f374,f819,f810]) ).
fof(f824,definition,
( spl58_52
<=> leq(sK47,n3) ),
introduced(definition,[new_symbols(definition,[spl58_52])],[avatar_definition]) ).
fof(f826,plain,
( leq(sK47,n3)
| ~ spl58_52 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f827,plain,
( ~ spl58_49
| spl58_52 ),
inference(avatar_split_clause,[],[f375,f824,f810]) ).
fof(f829,definition,
( spl58_53
<=> leq(n0,sK47) ),
introduced(definition,[new_symbols(definition,[spl58_53])],[avatar_definition]) ).
fof(f832,plain,
( ~ spl58_49
| spl58_53 ),
inference(avatar_split_clause,[],[f376,f829,f810]) ).
fof(f834,definition,
( spl58_54
<=> s_sworst7_init = a_select3(simplex7_init,sK47,sK46) ),
introduced(definition,[new_symbols(definition,[spl58_54])],[avatar_definition]) ).
fof(f837,plain,
( ~ spl58_49
| ~ spl58_54 ),
inference(avatar_split_clause,[],[f501,f834,f810]) ).
fof(f839,definition,
( spl58_55
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl58_55])],[avatar_definition]) ).
fof(f843,definition,
( spl58_56
<=> leq(sK45,n2) ),
introduced(definition,[new_symbols(definition,[spl58_56])],[avatar_definition]) ).
fof(f845,plain,
( leq(sK45,n2)
| ~ spl58_56 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f846,plain,
( ~ spl58_55
| spl58_56 ),
inference(avatar_split_clause,[],[f370,f843,f839]) ).
fof(f848,definition,
( spl58_57
<=> leq(n0,sK45) ),
introduced(definition,[new_symbols(definition,[spl58_57])],[avatar_definition]) ).
fof(f851,plain,
( ~ spl58_55
| spl58_57 ),
inference(avatar_split_clause,[],[f371,f848,f839]) ).
fof(f853,definition,
( spl58_58
<=> s_sworst7_init = a_select2(s_center7_init,sK45) ),
introduced(definition,[new_symbols(definition,[spl58_58])],[avatar_definition]) ).
fof(f856,plain,
( ~ spl58_55
| ~ spl58_58 ),
inference(avatar_split_clause,[],[f500,f853,f839]) ).
fof(f858,definition,
( spl58_59
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl58_59])],[avatar_definition]) ).
fof(f867,definition,
( spl58_61
<=> leq(sK44,n3) ),
introduced(definition,[new_symbols(definition,[spl58_61])],[avatar_definition]) ).
fof(f869,plain,
( leq(sK44,n3)
| ~ spl58_61 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f871,definition,
( spl58_62
<=> leq(s_best7,n3) ),
introduced(definition,[new_symbols(definition,[spl58_62])],[avatar_definition]) ).
fof(f872,plain,
( leq(s_best7,n3)
| ~ spl58_62 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f875,definition,
( spl58_63
<=> leq(n0,s_best7) ),
introduced(definition,[new_symbols(definition,[spl58_63])],[avatar_definition]) ).
fof(f876,plain,
( leq(n0,s_best7)
| ~ spl58_63 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f878,plain,
( ~ spl58_59
| spl58_1
| spl58_45
| spl58_61
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f545,f656,f875,f648,f644,f871,f636,f632,f762,f867,f791,f584,f858]) ).
fof(f879,plain,
( ~ spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_45
| spl58_61
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f547,f656,f875,f648,f644,f871,f636,f632,f762,f867,f791,f598,f593,f588,f858]) ).
fof(f881,definition,
( spl58_64
<=> leq(n0,sK44) ),
introduced(definition,[new_symbols(definition,[spl58_64])],[avatar_definition]) ).
fof(f884,plain,
( ~ spl58_59
| spl58_1
| spl58_45
| spl58_64
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f549,f656,f875,f648,f644,f871,f636,f632,f762,f881,f791,f584,f858]) ).
fof(f885,plain,
( ~ spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_45
| spl58_64
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f551,f656,f875,f648,f644,f871,f636,f632,f762,f881,f791,f598,f593,f588,f858]) ).
fof(f887,definition,
( spl58_65
<=> s_sworst7_init = a_select2(s_values7_init,sK44) ),
introduced(definition,[new_symbols(definition,[spl58_65])],[avatar_definition]) ).
fof(f890,plain,
( ~ spl58_59
| spl58_1
| spl58_45
| ~ spl58_65
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f553,f656,f875,f648,f644,f871,f636,f632,f762,f887,f791,f584,f858]) ).
fof(f891,plain,
( ~ spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_45
| ~ spl58_65
| spl58_39
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f555,f656,f875,f648,f644,f871,f636,f632,f762,f887,f791,f598,f593,f588,f858]) ).
fof(f893,definition,
( spl58_66
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl58_66])],[avatar_definition]) ).
fof(f902,definition,
( spl58_68
<=> s_sworst7_init = a_select2(s_values7_init,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl58_68])],[avatar_definition]) ).
fof(f907,definition,
( spl58_69
<=> leq(sK43,n3) ),
introduced(definition,[new_symbols(definition,[spl58_69])],[avatar_definition]) ).
fof(f909,plain,
( leq(sK43,n3)
| ~ spl58_69 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f910,plain,
( ~ spl58_66
| spl58_59
| spl58_1
| spl58_55
| spl58_69
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f559,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f907,f839,f584,f858,f893]) ).
fof(f911,plain,
( ~ spl58_66
| spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_55
| spl58_69
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f561,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f907,f839,f598,f593,f588,f858,f893]) ).
fof(f913,definition,
( spl58_70
<=> leq(n0,sK43) ),
introduced(definition,[new_symbols(definition,[spl58_70])],[avatar_definition]) ).
fof(f916,plain,
( ~ spl58_66
| spl58_59
| spl58_1
| spl58_55
| spl58_70
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f563,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f913,f839,f584,f858,f893]) ).
fof(f917,plain,
( ~ spl58_66
| spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_55
| spl58_70
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f565,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f913,f839,f598,f593,f588,f858,f893]) ).
fof(f919,definition,
( spl58_71
<=> s_sworst7_init = a_select2(s_values7_init,sK43) ),
introduced(definition,[new_symbols(definition,[spl58_71])],[avatar_definition]) ).
fof(f922,plain,
( ~ spl58_66
| spl58_59
| spl58_1
| spl58_55
| ~ spl58_71
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f567,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f919,f839,f584,f858,f893]) ).
fof(f923,plain,
( ~ spl58_66
| spl58_59
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_55
| ~ spl58_71
| spl58_49
| ~ spl58_13
| ~ spl58_14
| ~ spl58_62
| ~ spl58_16
| ~ spl58_17
| ~ spl58_63
| ~ spl58_18
| ~ spl58_7
| ~ spl58_68 ),
inference(avatar_split_clause,[],[f569,f902,f611,f656,f875,f652,f648,f871,f640,f636,f810,f919,f839,f598,f593,f588,f858,f893]) ).
fof(f926,definition,
( spl58_72
<=> s_sworst7_init = a_select2(s_values7_init,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl58_72])],[avatar_definition]) ).
fof(f931,definition,
( spl58_73
<=> leq(sK42,n3) ),
introduced(definition,[new_symbols(definition,[spl58_73])],[avatar_definition]) ).
fof(f933,plain,
( leq(sK42,n3)
| ~ spl58_73 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f934,plain,
( ~ spl58_6
| spl58_1
| spl58_35
| spl58_73
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f572,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f931,f743,f584,f607]) ).
fof(f935,plain,
( ~ spl58_6
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_35
| spl58_73
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f574,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f931,f743,f598,f593,f588,f607]) ).
fof(f937,definition,
( spl58_74
<=> leq(n0,sK42) ),
introduced(definition,[new_symbols(definition,[spl58_74])],[avatar_definition]) ).
fof(f940,plain,
( ~ spl58_6
| spl58_1
| spl58_35
| spl58_74
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f576,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f937,f743,f584,f607]) ).
fof(f941,plain,
( ~ spl58_6
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_35
| spl58_74
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f578,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f937,f743,f598,f593,f588,f607]) ).
fof(f943,definition,
( spl58_75
<=> s_sworst7_init = a_select2(s_values7_init,sK42) ),
introduced(definition,[new_symbols(definition,[spl58_75])],[avatar_definition]) ).
fof(f946,plain,
( ~ spl58_6
| spl58_1
| spl58_35
| ~ spl58_75
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f580,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f943,f743,f584,f607]) ).
fof(f947,plain,
( ~ spl58_6
| ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_35
| ~ spl58_75
| spl58_29
| ~ spl58_12
| ~ spl58_13
| ~ spl58_62
| ~ spl58_15
| ~ spl58_16
| ~ spl58_63
| spl58_66
| ~ spl58_7
| ~ spl58_72
| ~ spl58_18 ),
inference(avatar_split_clause,[],[f582,f656,f926,f611,f893,f875,f648,f644,f871,f636,f632,f714,f943,f743,f598,f593,f588,f607]) ).
fof(f948,plain,
spl58_12,
inference(avatar_split_clause,[],[f408,f632]) ).
fof(f949,plain,
spl58_13,
inference(avatar_split_clause,[],[f409,f636]) ).
fof(f950,plain,
spl58_14,
inference(avatar_split_clause,[],[f410,f640]) ).
fof(f951,plain,
spl58_62,
inference(avatar_split_clause,[],[f411,f871]) ).
fof(f952,plain,
spl58_16,
inference(avatar_split_clause,[],[f413,f648]) ).
fof(f953,plain,
spl58_17,
inference(avatar_split_clause,[],[f414,f652]) ).
fof(f954,plain,
spl58_63,
inference(avatar_split_clause,[],[f415,f875]) ).
fof(f955,plain,
spl58_18,
inference(avatar_split_clause,[],[f515,f656]) ).
fof(f956,plain,
( ~ leq(n0,s_best7)
| s_sworst7_init = a_select2(s_values7_init,s_best7)
| ~ spl58_62 ),
inference(resolution,[],[f517,f872]) ).
fof(f957,plain,
( ~ leq(n0,s_sworst7)
| s_sworst7_init = a_select2(s_values7_init,s_sworst7)
| ~ spl58_14 ),
inference(resolution,[],[f517,f641]) ).
fof(f958,plain,
( ~ leq(n0,s_worst7)
| s_sworst7_init = a_select2(s_values7_init,s_worst7)
| ~ spl58_13 ),
inference(resolution,[],[f517,f637]) ).
fof(f959,plain,
( ~ leq(n0,pv1388)
| s_sworst7_init = a_select2(s_values7_init,pv1388)
| ~ spl58_12 ),
inference(resolution,[],[f517,f633]) ).
fof(f960,plain,
( s_sworst7_init = a_select2(s_values7_init,s_worst7)
| ~ spl58_13
| ~ spl58_16 ),
inference(forward_subsumption_resolution,[],[f958,f649]) ).
fof(f961,plain,
( s_sworst7_init = a_select2(s_values7_init,s_sworst7)
| ~ spl58_14
| ~ spl58_17 ),
inference(forward_subsumption_resolution,[],[f957,f653]) ).
fof(f962,plain,
( s_sworst7_init = a_select2(s_values7_init,s_best7)
| ~ spl58_62
| ~ spl58_63 ),
inference(forward_subsumption_resolution,[],[f956,f876]) ).
fof(f969,plain,
( spl58_72
| ~ spl58_13
| ~ spl58_16 ),
inference(avatar_split_clause,[],[f960,f648,f636,f926]) ).
fof(f970,plain,
( spl58_68
| ~ spl58_14
| ~ spl58_17 ),
inference(avatar_split_clause,[],[f961,f652,f640,f902]) ).
fof(f971,plain,
( spl58_8
| ~ spl58_62
| ~ spl58_63 ),
inference(avatar_split_clause,[],[f962,f875,f871,f615]) ).
fof(f980,definition,
( spl58_77
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl58_77])],[avatar_definition]) ).
fof(f981,plain,
( leq(n0,n2)
| ~ spl58_77 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f1004,plain,
leq(n0,n2),
inference(resolution,[],[f242,f436]) ).
fof(f1026,plain,
spl58_77,
inference(avatar_split_clause,[],[f1004,f980]) ).
fof(f1137,plain,
( spl58_7
| ~ spl58_15
| ~ spl58_12 ),
inference(avatar_split_clause,[],[f959,f632,f644,f611]) ).
fof(f1151,plain,
( ~ leq(n0,sK57)
| s_sworst7_init = a_select2(s_values7_init,sK57)
| ~ spl58_10 ),
inference(resolution,[],[f626,f517]) ).
fof(f1152,plain,
( spl58_20
| ~ spl58_19
| ~ spl58_10 ),
inference(avatar_split_clause,[],[f1151,f624,f662,f668]) ).
fof(f1165,plain,
( ~ leq(n0,sK44)
| s_sworst7_init = a_select2(s_values7_init,sK44)
| ~ spl58_61 ),
inference(resolution,[],[f869,f517]) ).
fof(f1166,plain,
( spl58_65
| ~ spl58_64
| ~ spl58_61 ),
inference(avatar_split_clause,[],[f1165,f867,f881,f887]) ).
fof(f1179,plain,
( ~ leq(n0,sK43)
| s_sworst7_init = a_select2(s_values7_init,sK43)
| ~ spl58_69 ),
inference(resolution,[],[f909,f517]) ).
fof(f1180,plain,
( spl58_71
| ~ spl58_70
| ~ spl58_69 ),
inference(avatar_split_clause,[],[f1179,f907,f913,f919]) ).
fof(f1214,definition,
( spl58_94
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK55)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl58_94])],[avatar_definition]) ).
fof(f1215,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK55)
| ~ leq(n0,X0) )
| ~ spl58_94 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1236,plain,
( ~ leq(n0,sK54)
| s_sworst7_init = a_select2(s_center7_init,sK54)
| ~ spl58_26 ),
inference(resolution,[],[f701,f518]) ).
fof(f1237,plain,
( ~ leq(n0,sK54)
| ~ spl58_26
| spl58_28 ),
inference(forward_subsumption_resolution,[],[f1236,f711]) ).
fof(f1242,plain,
( ~ spl58_27
| ~ spl58_26
| spl58_28 ),
inference(avatar_split_clause,[],[f1237,f709,f699,f704]) ).
fof(f1357,plain,
! [X0] :
( ~ leq(X0,n2)
| leq(X0,pv1388) ),
inference(resolution,[],[f241,f412]) ).
fof(f1423,plain,
( leq(n0,pv1388)
| ~ spl58_77 ),
inference(resolution,[],[f1357,f981]) ).
fof(f1437,plain,
( spl58_15
| ~ spl58_77 ),
inference(avatar_split_clause,[],[f1423,f980,f644]) ).
fof(f1455,plain,
( ~ leq(n0,sK45)
| s_sworst7_init = a_select2(s_center7_init,sK45)
| ~ spl58_56 ),
inference(resolution,[],[f845,f518]) ).
fof(f1464,plain,
( spl58_58
| ~ spl58_57
| ~ spl58_56 ),
inference(avatar_split_clause,[],[f1455,f843,f848,f853]) ).
fof(f1496,definition,
( spl58_105
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK46)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl58_105])],[avatar_definition]) ).
fof(f1497,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK46)
| ~ leq(n0,X0) )
| ~ spl58_105 ),
inference(avatar_component_clause,[],[f1496]) ).
fof(f13405,plain,
( ~ leq(n0,sK51)
| s_sworst7_init = a_select2(s_center7_init,sK51)
| ~ spl58_36 ),
inference(resolution,[],[f749,f518]) ).
fof(f13485,plain,
( s_sworst7_init = a_select2(s_center7_init,sK51)
| ~ spl58_36
| ~ spl58_37 ),
inference(forward_subsumption_resolution,[],[f13405,f754]) ).
fof(f13495,plain,
( spl58_38
| ~ spl58_36
| ~ spl58_37 ),
inference(avatar_split_clause,[],[f13485,f752,f747,f757]) ).
fof(f19948,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK52)
| s_sworst7_init = a_select3(simplex7_init,X0,sK52) )
| ~ spl58_30 ),
inference(resolution,[],[f720,f516]) ).
fof(f20030,plain,
( ! [X0] :
( ~ leq(X0,n3)
| ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK52) )
| ~ spl58_30
| ~ spl58_31 ),
inference(forward_subsumption_resolution,[],[f19948,f725]) ).
fof(f20901,plain,
( ~ leq(n0,sK53)
| s_sworst7_init = a_select3(simplex7_init,sK53,sK52)
| ~ spl58_30
| ~ spl58_31
| ~ spl58_32 ),
inference(resolution,[],[f20030,f730]) ).
fof(f20902,plain,
( s_sworst7_init = a_select3(simplex7_init,sK53,sK52)
| ~ spl58_30
| ~ spl58_31
| ~ spl58_32
| ~ spl58_33 ),
inference(forward_subsumption_resolution,[],[f20901,f735]) ).
fof(f20933,plain,
( $false
| ~ spl58_30
| ~ spl58_31
| ~ spl58_32
| ~ spl58_33
| spl58_34 ),
inference(forward_subsumption_resolution,[],[f20902,f740]) ).
fof(f20934,plain,
( ~ spl58_30
| ~ spl58_31
| ~ spl58_32
| ~ spl58_33
| spl58_34 ),
inference(avatar_contradiction_clause,[],[f20933]) ).
fof(f22185,plain,
( s_sworst7_init = a_select3(simplex7_init,sK56,sK55)
| ~ leq(n0,sK56)
| ~ spl58_23
| ~ spl58_94 ),
inference(resolution,[],[f1215,f686]) ).
fof(f24310,plain,
( ~ leq(n0,sK48)
| s_sworst7_init = a_select2(s_center7_init,sK48)
| ~ spl58_46 ),
inference(resolution,[],[f797,f518]) ).
fof(f24390,plain,
( s_sworst7_init = a_select2(s_center7_init,sK48)
| ~ spl58_46
| ~ spl58_47 ),
inference(forward_subsumption_resolution,[],[f24310,f802]) ).
fof(f24398,plain,
( spl58_48
| ~ spl58_46
| ~ spl58_47 ),
inference(avatar_split_clause,[],[f24390,f800,f795,f805]) ).
fof(f29035,plain,
( ~ leq(n0,sK42)
| s_sworst7_init = a_select2(s_values7_init,sK42)
| ~ spl58_73 ),
inference(resolution,[],[f933,f517]) ).
fof(f29172,plain,
( spl58_75
| ~ spl58_74
| ~ spl58_73 ),
inference(avatar_split_clause,[],[f29035,f931,f937,f943]) ).
fof(f29349,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK55)
| s_sworst7_init = a_select3(simplex7_init,X0,sK55) )
| ~ spl58_21 ),
inference(resolution,[],[f676,f516]) ).
fof(f29545,plain,
( ~ spl58_22
| spl58_94
| ~ spl58_21 ),
inference(avatar_split_clause,[],[f29349,f674,f1214,f679]) ).
fof(f30232,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK49)
| s_sworst7_init = a_select3(simplex7_init,X0,sK49) )
| ~ spl58_40 ),
inference(resolution,[],[f768,f516]) ).
fof(f30314,plain,
( ! [X0] :
( ~ leq(X0,n3)
| ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK49) )
| ~ spl58_40
| ~ spl58_41 ),
inference(forward_subsumption_resolution,[],[f30232,f773]) ).
fof(f30423,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK46)
| s_sworst7_init = a_select3(simplex7_init,X0,sK46) )
| ~ spl58_50 ),
inference(resolution,[],[f816,f516]) ).
fof(f30619,plain,
( ~ spl58_51
| spl58_105
| ~ spl58_50 ),
inference(avatar_split_clause,[],[f30423,f814,f1496,f819]) ).
fof(f31968,plain,
( s_sworst7_init = a_select3(simplex7_init,sK47,sK46)
| ~ leq(n0,sK47)
| ~ spl58_52
| ~ spl58_105 ),
inference(resolution,[],[f1497,f826]) ).
fof(f32206,plain,
( ~ spl58_24
| spl58_25
| ~ spl58_23
| ~ spl58_94 ),
inference(avatar_split_clause,[],[f22185,f1214,f684,f694,f689]) ).
fof(f32302,plain,
( ~ spl58_53
| spl58_54
| ~ spl58_52
| ~ spl58_105 ),
inference(avatar_split_clause,[],[f31968,f1496,f824,f834,f829]) ).
fof(f33574,plain,
( ~ leq(n0,sK50)
| s_sworst7_init = a_select3(simplex7_init,sK50,sK49)
| ~ spl58_40
| ~ spl58_41
| ~ spl58_42 ),
inference(resolution,[],[f30314,f778]) ).
fof(f33575,plain,
( s_sworst7_init = a_select3(simplex7_init,sK50,sK49)
| ~ spl58_40
| ~ spl58_41
| ~ spl58_42
| ~ spl58_43 ),
inference(forward_subsumption_resolution,[],[f33574,f783]) ).
fof(f33599,plain,
( $false
| ~ spl58_40
| ~ spl58_41
| ~ spl58_42
| ~ spl58_43
| spl58_44 ),
inference(forward_subsumption_resolution,[],[f33575,f788]) ).
fof(f33600,plain,
( ~ spl58_40
| ~ spl58_41
| ~ spl58_42
| ~ spl58_43
| spl58_44 ),
inference(avatar_contradiction_clause,[],[f33599]) ).
cnf(s1,plain,
( ~ spl58_1
| spl58_2 ),
inference(sat_conversion,[],[f591]) ).
cnf(s2,plain,
( ~ spl58_1
| spl58_3 ),
inference(sat_conversion,[],[f596]) ).
cnf(s3,plain,
( ~ spl58_1
| spl58_4 ),
inference(sat_conversion,[],[f601]) ).
cnf(s5,plain,
( spl58_1
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_10
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18 ),
inference(sat_conversion,[],[f659]) ).
cnf(s6,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_10
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18 ),
inference(sat_conversion,[],[f660]) ).
cnf(s7,plain,
( spl58_1
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_19 ),
inference(sat_conversion,[],[f665]) ).
cnf(s8,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_19 ),
inference(sat_conversion,[],[f666]) ).
cnf(s9,plain,
( spl58_1
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| ~ spl58_20 ),
inference(sat_conversion,[],[f671]) ).
cnf(s10,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| ~ spl58_7
| ~ spl58_8
| spl58_9
| spl58_11
| ~ spl58_12
| ~ spl58_13
| ~ spl58_14
| ~ spl58_15
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| ~ spl58_20 ),
inference(sat_conversion,[],[f672]) ).
cnf(s11,plain,
( ~ spl58_11
| spl58_21 ),
inference(sat_conversion,[],[f677]) ).
cnf(s12,plain,
( ~ spl58_11
| spl58_22 ),
inference(sat_conversion,[],[f682]) ).
cnf(s13,plain,
( ~ spl58_11
| spl58_23 ),
inference(sat_conversion,[],[f687]) ).
cnf(s14,plain,
( ~ spl58_11
| spl58_24 ),
inference(sat_conversion,[],[f692]) ).
cnf(s15,plain,
( ~ spl58_11
| ~ spl58_25 ),
inference(sat_conversion,[],[f697]) ).
cnf(s16,plain,
( ~ spl58_9
| spl58_26 ),
inference(sat_conversion,[],[f702]) ).
cnf(s17,plain,
( ~ spl58_9
| spl58_27 ),
inference(sat_conversion,[],[f707]) ).
cnf(s18,plain,
( ~ spl58_9
| ~ spl58_28 ),
inference(sat_conversion,[],[f712]) ).
cnf(s19,plain,
( ~ spl58_29
| spl58_30 ),
inference(sat_conversion,[],[f721]) ).
cnf(s20,plain,
( ~ spl58_29
| spl58_31 ),
inference(sat_conversion,[],[f726]) ).
cnf(s21,plain,
( ~ spl58_29
| spl58_32 ),
inference(sat_conversion,[],[f731]) ).
cnf(s22,plain,
( ~ spl58_29
| spl58_33 ),
inference(sat_conversion,[],[f736]) ).
cnf(s23,plain,
( ~ spl58_29
| ~ spl58_34 ),
inference(sat_conversion,[],[f741]) ).
cnf(s24,plain,
( ~ spl58_35
| spl58_36 ),
inference(sat_conversion,[],[f750]) ).
cnf(s25,plain,
( ~ spl58_35
| spl58_37 ),
inference(sat_conversion,[],[f755]) ).
cnf(s26,plain,
( ~ spl58_35
| ~ spl58_38 ),
inference(sat_conversion,[],[f760]) ).
cnf(s27,plain,
( ~ spl58_39
| spl58_40 ),
inference(sat_conversion,[],[f769]) ).
cnf(s28,plain,
( ~ spl58_39
| spl58_41 ),
inference(sat_conversion,[],[f774]) ).
cnf(s29,plain,
( ~ spl58_39
| spl58_42 ),
inference(sat_conversion,[],[f779]) ).
cnf(s30,plain,
( ~ spl58_39
| spl58_43 ),
inference(sat_conversion,[],[f784]) ).
cnf(s31,plain,
( ~ spl58_39
| ~ spl58_44 ),
inference(sat_conversion,[],[f789]) ).
cnf(s32,plain,
( ~ spl58_45
| spl58_46 ),
inference(sat_conversion,[],[f798]) ).
cnf(s33,plain,
( ~ spl58_45
| spl58_47 ),
inference(sat_conversion,[],[f803]) ).
cnf(s34,plain,
( ~ spl58_45
| ~ spl58_48 ),
inference(sat_conversion,[],[f808]) ).
cnf(s35,plain,
( ~ spl58_49
| spl58_50 ),
inference(sat_conversion,[],[f817]) ).
cnf(s36,plain,
( ~ spl58_49
| spl58_51 ),
inference(sat_conversion,[],[f822]) ).
cnf(s37,plain,
( ~ spl58_49
| spl58_52 ),
inference(sat_conversion,[],[f827]) ).
cnf(s38,plain,
( ~ spl58_49
| spl58_53 ),
inference(sat_conversion,[],[f832]) ).
cnf(s39,plain,
( ~ spl58_49
| ~ spl58_54 ),
inference(sat_conversion,[],[f837]) ).
cnf(s40,plain,
( ~ spl58_55
| spl58_56 ),
inference(sat_conversion,[],[f846]) ).
cnf(s41,plain,
( ~ spl58_55
| spl58_57 ),
inference(sat_conversion,[],[f851]) ).
cnf(s42,plain,
( ~ spl58_55
| ~ spl58_58 ),
inference(sat_conversion,[],[f856]) ).
cnf(s44,plain,
( spl58_1
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_61
| ~ spl58_62
| ~ spl58_63 ),
inference(sat_conversion,[],[f878]) ).
cnf(s45,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_61
| ~ spl58_62
| ~ spl58_63 ),
inference(sat_conversion,[],[f879]) ).
cnf(s46,plain,
( spl58_1
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_62
| ~ spl58_63
| spl58_64 ),
inference(sat_conversion,[],[f884]) ).
cnf(s47,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_62
| ~ spl58_63
| spl58_64 ),
inference(sat_conversion,[],[f885]) ).
cnf(s48,plain,
( spl58_1
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_65 ),
inference(sat_conversion,[],[f890]) ).
cnf(s49,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_65 ),
inference(sat_conversion,[],[f891]) ).
cnf(s52,plain,
( spl58_1
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| spl58_69 ),
inference(sat_conversion,[],[f910]) ).
cnf(s53,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| spl58_69 ),
inference(sat_conversion,[],[f911]) ).
cnf(s54,plain,
( spl58_1
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| spl58_70 ),
inference(sat_conversion,[],[f916]) ).
cnf(s55,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| spl58_70 ),
inference(sat_conversion,[],[f917]) ).
cnf(s56,plain,
( spl58_1
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| ~ spl58_71 ),
inference(sat_conversion,[],[f922]) ).
cnf(s57,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_7
| ~ spl58_13
| ~ spl58_14
| ~ spl58_16
| ~ spl58_17
| ~ spl58_18
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_62
| ~ spl58_63
| ~ spl58_66
| ~ spl58_68
| ~ spl58_71 ),
inference(sat_conversion,[],[f923]) ).
cnf(s60,plain,
( spl58_1
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| spl58_73 ),
inference(sat_conversion,[],[f934]) ).
cnf(s61,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| spl58_73 ),
inference(sat_conversion,[],[f935]) ).
cnf(s62,plain,
( spl58_1
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| spl58_74 ),
inference(sat_conversion,[],[f940]) ).
cnf(s63,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| spl58_74 ),
inference(sat_conversion,[],[f941]) ).
cnf(s64,plain,
( spl58_1
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| ~ spl58_75 ),
inference(sat_conversion,[],[f946]) ).
cnf(s65,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| ~ spl58_7
| ~ spl58_12
| ~ spl58_13
| ~ spl58_15
| ~ spl58_16
| ~ spl58_18
| spl58_29
| spl58_35
| ~ spl58_62
| ~ spl58_63
| spl58_66
| ~ spl58_72
| ~ spl58_75 ),
inference(sat_conversion,[],[f947]) ).
cnf(s66,plain,
spl58_12,
inference(sat_conversion,[],[f948]) ).
cnf(s67,plain,
spl58_13,
inference(sat_conversion,[],[f949]) ).
cnf(s68,plain,
spl58_14,
inference(sat_conversion,[],[f950]) ).
cnf(s69,plain,
spl58_62,
inference(sat_conversion,[],[f951]) ).
cnf(s70,plain,
spl58_16,
inference(sat_conversion,[],[f952]) ).
cnf(s71,plain,
spl58_17,
inference(sat_conversion,[],[f953]) ).
cnf(s72,plain,
spl58_63,
inference(sat_conversion,[],[f954]) ).
cnf(s73,plain,
spl58_18,
inference(sat_conversion,[],[f955]) ).
cnf(s77,plain,
( ~ spl58_13
| ~ spl58_16
| spl58_72 ),
inference(sat_conversion,[],[f969]) ).
cnf(s78,plain,
( ~ spl58_14
| ~ spl58_17
| spl58_68 ),
inference(sat_conversion,[],[f970]) ).
cnf(s79,plain,
( spl58_8
| ~ spl58_62
| ~ spl58_63 ),
inference(sat_conversion,[],[f971]) ).
cnf(s86,plain,
spl58_77,
inference(sat_conversion,[],[f1026]) ).
cnf(s88,plain,
( spl58_7
| ~ spl58_12
| ~ spl58_15 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s91,plain,
( ~ spl58_10
| ~ spl58_19
| spl58_20 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s94,plain,
( ~ spl58_61
| ~ spl58_64
| spl58_65 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s97,plain,
( ~ spl58_69
| ~ spl58_70
| spl58_71 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s109,plain,
( ~ spl58_26
| ~ spl58_27
| spl58_28 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s115,plain,
( spl58_15
| ~ spl58_77 ),
inference(sat_conversion,[],[f1437]) ).
cnf(s119,plain,
( ~ spl58_56
| ~ spl58_57
| spl58_58 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s665,plain,
( ~ spl58_36
| ~ spl58_37
| spl58_38 ),
inference(sat_conversion,[],[f13495]) ).
cnf(s972,plain,
( ~ spl58_30
| ~ spl58_31
| ~ spl58_32
| ~ spl58_33
| spl58_34 ),
inference(sat_conversion,[],[f20934]) ).
cnf(s1234,plain,
( ~ spl58_46
| ~ spl58_47
| spl58_48 ),
inference(sat_conversion,[],[f24398]) ).
cnf(s1685,plain,
( ~ spl58_73
| ~ spl58_74
| spl58_75 ),
inference(sat_conversion,[],[f29172]) ).
cnf(s1736,plain,
( ~ spl58_21
| ~ spl58_22
| spl58_94 ),
inference(sat_conversion,[],[f29545]) ).
cnf(s1860,plain,
( ~ spl58_50
| ~ spl58_51
| spl58_105 ),
inference(sat_conversion,[],[f30619]) ).
cnf(s2032,plain,
( ~ spl58_23
| ~ spl58_24
| spl58_25
| ~ spl58_94 ),
inference(sat_conversion,[],[f32206]) ).
cnf(s2073,plain,
( ~ spl58_52
| ~ spl58_53
| spl58_54
| ~ spl58_105 ),
inference(sat_conversion,[],[f32302]) ).
cnf(s2179,plain,
( ~ spl58_40
| ~ spl58_41
| ~ spl58_42
| ~ spl58_43
| spl58_44 ),
inference(sat_conversion,[],[f33600]) ).
cnf(s2180,plain,
spl58_15,
inference(rat,[],[s115,s86]) ).
cnf(s2184,plain,
spl58_8,
inference(rat,[],[s79,s72,s69]) ).
cnf(s2185,plain,
spl58_68,
inference(rat,[],[s78,s71,s68]) ).
cnf(s2186,plain,
spl58_72,
inference(rat,[],[s77,s70,s67]) ).
cnf(s2189,plain,
spl58_7,
inference(rat,[],[s88,s2180,s66]) ).
cnf(s2190,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| ~ spl58_75 ),
inference(rat,[],[s65,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2191,plain,
( spl58_1
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| ~ spl58_75 ),
inference(rat,[],[s64,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2192,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| spl58_74 ),
inference(rat,[],[s63,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2193,plain,
( spl58_1
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| spl58_74 ),
inference(rat,[],[s62,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2194,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| spl58_73 ),
inference(rat,[],[s61,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2195,plain,
( spl58_1
| ~ spl58_6
| spl58_29
| spl58_35
| spl58_66
| spl58_73 ),
inference(rat,[],[s60,s2186,s72,s69,s73,s70,s2180,s67,s66,s2189]) ).
cnf(s2197,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| ~ spl58_71 ),
inference(rat,[],[s57,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2198,plain,
( spl58_1
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| ~ spl58_71 ),
inference(rat,[],[s56,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2199,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| spl58_70 ),
inference(rat,[],[s55,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2200,plain,
( spl58_1
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| spl58_70 ),
inference(rat,[],[s54,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2201,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| spl58_69 ),
inference(rat,[],[s53,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2202,plain,
( spl58_1
| spl58_49
| spl58_55
| spl58_59
| ~ spl58_66
| spl58_69 ),
inference(rat,[],[s52,s2185,s72,s69,s73,s71,s70,s68,s67,s2189]) ).
cnf(s2204,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_65 ),
inference(rat,[],[s49,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2205,plain,
( spl58_1
| spl58_39
| spl58_45
| ~ spl58_59
| ~ spl58_65 ),
inference(rat,[],[s48,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2206,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_64 ),
inference(rat,[],[s47,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2207,plain,
( spl58_1
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_64 ),
inference(rat,[],[s46,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2208,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_61 ),
inference(rat,[],[s45,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2209,plain,
( spl58_1
| spl58_39
| spl58_45
| ~ spl58_59
| spl58_61 ),
inference(rat,[],[s44,s72,s69,s73,s70,s2180,s67,s66]) ).
cnf(s2210,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| spl58_9
| spl58_11
| ~ spl58_20 ),
inference(rat,[],[s10,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2211,plain,
( spl58_1
| spl58_6
| spl58_9
| spl58_11
| ~ spl58_20 ),
inference(rat,[],[s9,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2212,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| spl58_9
| spl58_11
| spl58_19 ),
inference(rat,[],[s8,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2213,plain,
( spl58_1
| spl58_6
| spl58_9
| spl58_11
| spl58_19 ),
inference(rat,[],[s7,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2214,plain,
( ~ spl58_2
| ~ spl58_3
| ~ spl58_4
| spl58_6
| spl58_9
| spl58_10
| spl58_11 ),
inference(rat,[],[s6,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2215,plain,
( spl58_1
| spl58_6
| spl58_9
| spl58_10
| spl58_11 ),
inference(rat,[],[s5,s73,s71,s70,s2180,s68,s67,s66,s2184,s2189]) ).
cnf(s2217,plain,
( spl58_66
| spl58_35
| spl58_29
| spl58_1
| ~ spl58_6 ),
inference(rat,[],[s1685,s2195,s2193,s2191]) ).
cnf(s2218,plain,
( ~ spl58_66
| spl58_59
| spl58_1
| spl58_49
| spl58_55 ),
inference(rat,[],[s97,s2202,s2200,s2198]) ).
cnf(s2219,plain,
( ~ spl58_59
| spl58_45
| spl58_1
| spl58_39 ),
inference(rat,[],[s94,s2209,s2207,s2205]) ).
cnf(s2220,plain,
~ spl58_55,
inference(rat,[],[s119,s40,s41,s42]) ).
cnf(s2221,plain,
~ spl58_49,
inference(rat,[],[s1860,s2073,s35,s36,s37,s38,s39]) ).
cnf(s2222,plain,
~ spl58_35,
inference(rat,[],[s665,s24,s25,s26]) ).
cnf(s2223,plain,
~ spl58_29,
inference(rat,[],[s972,s19,s20,s21,s22,s23]) ).
cnf(s2224,plain,
~ spl58_11,
inference(rat,[],[s1736,s2032,s11,s12,s13,s14,s15]) ).
cnf(s2225,plain,
( spl58_9
| spl58_6
| spl58_1 ),
inference(rat,[],[s91,s2215,s2213,s2211,s2224]) ).
cnf(s2226,plain,
~ spl58_9,
inference(rat,[],[s109,s16,s17,s18]) ).
cnf(s2227,plain,
~ spl58_45,
inference(rat,[],[s1234,s32,s33,s34]) ).
cnf(s2228,plain,
~ spl58_39,
inference(rat,[],[s2179,s27,s28,s29,s30,s31]) ).
cnf(s2229,plain,
spl58_1,
inference(rat,[],[s2218,s2217,s2219,s2225,s2221,s2220,s2222,s2223,s2228,s2227,s2226]) ).
cnf(s2230,plain,
spl58_4,
inference(rat,[],[s3,s2229]) ).
cnf(s2231,plain,
spl58_3,
inference(rat,[],[s2,s2229]) ).
cnf(s2232,plain,
spl58_2,
inference(rat,[],[s1,s2229]) ).
cnf(s2233,plain,
spl58_6,
inference(rat,[],[s91,s2212,s2214,s2210,s2224,s2230,s2232,s2231,s2226]) ).
cnf(s2235,plain,
spl58_66,
inference(rat,[],[s1685,s2190,s2194,s2192,s2230,s2231,s2232,s2223,s2222,s2233]) ).
cnf(s2237,plain,
spl58_59,
inference(rat,[],[s97,s2201,s2199,s2197,s2235,s2230,s2231,s2232,s2220,s2221]) ).
cnf(s2239,plain,
~ spl58_65,
inference(rat,[],[s2204,s2227,s2228,s2232,s2230,s2231,s2237]) ).
cnf(s2240,plain,
spl58_64,
inference(rat,[],[s2206,s2230,s2228,s2232,s2231,s2227,s2237]) ).
cnf(s2241,plain,
spl58_61,
inference(rat,[],[s2208,s2230,s2228,s2232,s2231,s2227,s2237]) ).
cnf(s2242,plain,
$false,
inference(rat,[],[s94,s2239,s2240,s2241]) ).
fof(f33612,plain,
$false,
inference(avatar_sat_refutation,[],[s2242]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV036+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 % Computer : n018.cluster.edu
% 0.11/0.22 % Model : x86_64 x86_64
% 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.22 % Memory : 8046.5625MB
% 0.11/0.22 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Mon Sep 28 09:45:55 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 Running first-order model finding
% 0.11/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.84/4.29 % (3267963)Will run a generic schedule for satisfiability detection.
% 27.84/4.29 % (3267969)% WARNING: option uhcvi not known.
% 27.84/4.29 % (3267970)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2202955073:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.84/4.29 % (3267973)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2947514677:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.84/4.29 % (3267974)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2106859809:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.84/4.29 % (3267969)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=54953571:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.84/4.29 % (3267971)dis+10_1_sil=32000:sp=arity:random_seed=1752429400:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.84/4.29 % (3267968)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4078949645_2999 on theBenchmark for (2999ds/0Mi)
% 27.84/4.29 % (3267972)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=477039548:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.84/4.29 % TRYING [1]
% 27.84/4.29 % TRYING [2]
% 27.84/4.29 % (3267973)Instruction limit reached!
% 27.84/4.29 % (3267973)------------------------------
% 27.84/4.29 % (3267973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.84/4.29 % (3267973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.29 % (3267973)CaDiCaL version: 2.1.3
% 27.84/4.29 % (3267973)Termination reason: Instruction limit
% 27.84/4.29 % (3267973)Termination phase: Saturation
% 27.84/4.29 % (3267973)Time elapsed: 0.100 s
% 27.84/4.29 % (3267973)Peak memory usage: 13 MB
% 27.84/4.29 % (3267973)Instructions burned: 132 (million)
% 27.84/4.29 % TRYING [3]
% 27.84/4.29 % (3267971)Instruction limit reached!
% 27.84/4.29 % (3267971)------------------------------
% 27.84/4.29 % (3267971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.84/4.29 % (3267971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.29 % (3267971)CaDiCaL version: 2.1.3
% 27.84/4.29 % (3267971)Termination reason: Instruction limit
% 27.84/4.29 % (3267971)Termination phase: Saturation
% 27.84/4.29 % (3267971)Time elapsed: 0.102 s
% 27.84/4.29 % (3267971)Peak memory usage: 13 MB
% 27.84/4.29 % (3267971)Instructions burned: 103 (million)
% 27.84/4.29 % (3267972)Instruction limit reached!
% 27.84/4.29 % (3267972)------------------------------
% 27.84/4.29 % (3267972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.84/4.29 % (3267972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.29 % (3267972)CaDiCaL version: 2.1.3
% 27.84/4.29 % (3267972)Termination reason: Instruction limit
% 27.84/4.29 % (3267972)Termination phase: Saturation
% 27.84/4.29 % (3267972)Time elapsed: 0.109 s
% 27.84/4.29 % (3267972)Peak memory usage: 13 MB
% 27.84/4.29 % (3267972)Instructions burned: 117 (million)
% 27.84/4.29 % (3267982)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=51202439:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.84/4.29 % (3267974)Instruction limit reached!
% 27.84/4.29 % (3267974)------------------------------
% 27.84/4.29 % (3267974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.84/4.29 % (3267974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.84/4.29 % (3267974)CaDiCaL version: 2.1.3
% 27.84/4.29 % (3267974)Termination reason: Instruction limit
% 27.84/4.29 % (3267974)Termination phase: Saturation
% 27.84/4.29 % (3267974)Time elapsed: 0.145 s
% 27.84/4.29 % (3267974)Peak memory usage: 15 MB
% 27.84/4.29 % (3267974)Instructions burned: 160 (million)
% 27.84/4.29 % (3267986)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3036275057:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.84/4.29 % (3267983)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1937828002:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.84/4.29 % TRYING [4]
% 27.84/4.29 % TRYING [1]
% 27.84/4.29 % TRYING [2]
% 27.84/4.29 % (3267989)ott-21_1_sil=16000:fs=off:random_seed=3855256915:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.84/4.29 % TRYING [3]
% 27.84/4.29 % TRYING [4]
% 27.84/4.29 % (3267983)Instruction limit reached!
% 27.84/4.29 % (3267983)------------------------------
% 27.84/4.29 % (3267983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.84/4.29 % (3267983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267983)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267983)Termination reason: Instruction limit
% 79.14/11.48 % (3267983)Termination phase: Saturation
% 79.14/11.48 % (3267983)Time elapsed: 0.138 s
% 79.14/11.48 % (3267983)Peak memory usage: 13 MB
% 79.14/11.48 % (3267983)Instructions burned: 131 (million)
% 79.14/11.48 % (3267995)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2504344801:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 79.14/11.48 % (3267989)Instruction limit reached!
% 79.14/11.48 % (3267989)------------------------------
% 79.14/11.48 % (3267989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.14/11.48 % (3267989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267989)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267989)Termination reason: Instruction limit
% 79.14/11.48 % (3267989)Termination phase: Saturation
% 79.14/11.48 % (3267989)Time elapsed: 0.180 s
% 79.14/11.48 % (3267989)Peak memory usage: 13 MB
% 79.14/11.48 % (3267989)Instructions burned: 180 (million)
% 79.14/11.48 % (3267997)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=439108842:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 79.14/11.48 % TRYING [5]
% 79.14/11.48 % TRYING [1]
% 79.14/11.48 % TRYING [2]
% 79.14/11.48 % TRYING [5]
% 79.14/11.48 % TRYING [3]
% 79.14/11.48 % (3267982)Instruction limit reached!
% 79.14/11.48 % (3267982)------------------------------
% 79.14/11.48 % (3267982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.14/11.48 % (3267982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267982)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267982)Termination reason: Instruction limit
% 79.14/11.48 % (3267982)Termination phase: Finite model building constraint generation
% 79.14/11.48 % (3267982)Time elapsed: 0.475 s
% 79.14/11.48 % (3267982)Peak memory usage: 36 MB
% 79.14/11.48 % (3267982)Instructions burned: 715 (million)
% 79.14/11.48 % (3268003)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3960935793:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 79.14/11.48 % (3267995)Instruction limit reached!
% 79.14/11.48 % (3267995)------------------------------
% 79.14/11.48 % (3267995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.14/11.48 % (3267995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267995)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267995)Termination reason: Instruction limit
% 79.14/11.48 % (3267995)Termination phase: Saturation
% 79.14/11.48 % (3267995)Time elapsed: 0.428 s
% 79.14/11.48 % (3267995)Peak memory usage: 15 MB
% 79.14/11.48 % (3267995)Instructions burned: 477 (million)
% 79.14/11.48 % (3267986)Instruction limit reached!
% 79.14/11.48 % (3267986)------------------------------
% 79.14/11.48 % (3267986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.14/11.48 % (3267986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267986)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267986)Termination reason: Instruction limit
% 79.14/11.48 % (3267986)Termination phase: Saturation
% 79.14/11.48 % (3267986)Time elapsed: 0.623 s
% 79.14/11.48 % (3267986)Peak memory usage: 19 MB
% 79.14/11.48 % (3267986)Instructions burned: 684 (million)
% 79.14/11.48 % (3268008)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2672939551:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 79.14/11.48 % (3268011)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=423785372:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 79.14/11.48 % TRYING [4]
% 79.14/11.48 % (3267997)Instruction limit reached!
% 79.14/11.48 % (3267997)------------------------------
% 79.14/11.48 % (3267997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.14/11.48 % (3267997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.14/11.48 % (3267997)CaDiCaL version: 2.1.3
% 79.14/11.48 % (3267997)Termination reason: Instruction limit
% 79.14/11.48 % (3267997)Termination phase: Finite model building constraint generation
% 79.14/11.48 % (3267997)Time elapsed: 0.659 s
% 79.14/11.48 % (3267997)Peak memory usage: 33 MB
% 79.14/11.48 % (3267997)Instructions burned: 866 (million)
% 79.14/11.48 % (3268018)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2289351503:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 79.14/11.48 % (3268011)Instruction limit reached!
% 79.14/11.48 % (3268011)------------------------------
% 66.85/13.54 % (3268011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268011)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268011)Termination reason: Instruction limit
% 66.85/13.54 % (3268011)Termination phase: Saturation
% 66.85/13.54 % (3268011)Time elapsed: 0.625 s
% 66.85/13.54 % (3268011)Peak memory usage: 19 MB
% 66.85/13.54 % (3268011)Instructions burned: 693 (million)
% 66.85/13.54 % (3268022)fmb+10_1_sil=64000:random_seed=939725931:i=22061:nm=2:gsp=on_2985 on theBenchmark for (2985ds/22061Mi)
% 66.85/13.54 % TRYING [1]
% 66.85/13.54 % TRYING [2]
% 66.85/13.54 % (3268008)Instruction limit reached!
% 66.85/13.54 % (3268008)------------------------------
% 66.85/13.54 % (3268008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268008)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268008)Termination reason: Instruction limit
% 66.85/13.54 % (3268008)Termination phase: Finite model building constraint generation
% 66.85/13.54 % (3268008)Time elapsed: 0.765 s
% 66.85/13.54 % (3268008)Peak memory usage: 100 MB
% 66.85/13.54 % (3268008)Instructions burned: 890 (million)
% 66.85/13.54 % TRYING [3]
% 66.85/13.54 % (3268025)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=500065651:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 66.85/13.54 % TRYING [20]
% 66.85/13.54 % TRYING [4]
% 66.85/13.54 % TRYING [6]
% 66.85/13.54 % (3268003)Instruction limit reached!
% 66.85/13.54 % (3268003)------------------------------
% 66.85/13.54 % (3268003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268003)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268003)Termination reason: Instruction limit
% 66.85/13.54 % (3268003)Termination phase: Saturation
% 66.85/13.54 % (3268003)Time elapsed: 1.115 s
% 66.85/13.54 % (3268003)Peak memory usage: 20 MB
% 66.85/13.54 % (3268003)Instructions burned: 1179 (million)
% 66.85/13.54 % (3268028)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3375993964:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 66.85/13.54 % TRYING [8]
% 66.85/13.54 % (3268018)Instruction limit reached!
% 66.85/13.54 % (3268018)------------------------------
% 66.85/13.54 % (3268018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268018)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268018)Termination reason: Instruction limit
% 66.85/13.54 % (3268018)Termination phase: Saturation
% 66.85/13.54 % (3268018)Time elapsed: 0.801 s
% 66.85/13.54 % (3268018)Peak memory usage: 19 MB
% 66.85/13.54 % (3268018)Instructions burned: 879 (million)
% 66.85/13.54 % (3268031)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=135265397:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 66.85/13.54 % (3268028)Instruction limit reached!
% 66.85/13.54 % (3268028)------------------------------
% 66.85/13.54 % (3268028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268028)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268028)Termination reason: Instruction limit
% 66.85/13.54 % (3268028)Termination phase: Finite model building constraint generation
% 66.85/13.54 % (3268028)Time elapsed: 0.648 s
% 66.85/13.54 % (3268028)Peak memory usage: 61 MB
% 66.85/13.54 % (3268028)Instructions burned: 921 (million)
% 66.85/13.54 % (3268036)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1183417924:i=1472:ins=7:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/1472Mi)
% 66.85/13.54 % TRYING [5]
% 66.85/13.54 % (3268036)Instruction limit reached!
% 66.85/13.54 % (3268036)------------------------------
% 66.85/13.54 % (3268036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268036)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268036)Termination reason: Instruction limit
% 66.85/13.54 % (3268036)Termination phase: Saturation
% 66.85/13.54 % (3268036)Time elapsed: 1.333 s
% 66.85/13.54 % (3268036)Peak memory usage: 24 MB
% 66.85/13.54 % (3268036)Instructions burned: 1472 (million)
% 66.85/13.54 % (3268046)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3791610119:i=6324_2961 on theBenchmark for (2961ds/6324Mi)
% 66.85/13.54 % (3268046)Cannot represent all propositional literals internally
% 66.85/13.54 % (3268046)Refutation not found, incomplete strategy
% 66.85/13.54 % (3268046)------------------------------
% 66.85/13.54 % (3268046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268046)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268046)Termination reason: Refutation not found, incomplete strategy
% 66.85/13.54 % (3268046)Time elapsed: 0.132 s
% 66.85/13.54 % (3268046)Peak memory usage: 13 MB
% 66.85/13.54 % (3268046)Instructions burned: 139 (million)
% 66.85/13.54 % (3268046)------------------------------
% 66.85/13.54 % (3268046)------------------------------
% 66.85/13.54 % (3268050)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=465373837:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 66.85/13.54 % TRYING [16]
% 66.85/13.54 % TRYING [7]
% 66.85/13.54 % (3268050)Instruction limit reached!
% 66.85/13.54 % (3268050)------------------------------
% 66.85/13.54 % (3268050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268050)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268050)Termination reason: Instruction limit
% 66.85/13.54 % (3268050)Termination phase: Finite model building constraint generation
% 66.85/13.54 % (3268050)Time elapsed: 1.656 s
% 66.85/13.54 % (3268050)Peak memory usage: 119 MB
% 66.85/13.54 % (3268050)Instructions burned: 2175 (million)
% 66.85/13.54 % (3268056)ott-2_1_sil=16000:newcnf=on:random_seed=2893787667:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2942 on theBenchmark for (2942ds/869Mi)
% 66.85/13.54 % (3268031)Instruction limit reached!
% 66.85/13.54 % (3268031)------------------------------
% 66.85/13.54 % (3268031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268031)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268031)Termination reason: Instruction limit
% 66.85/13.54 % (3268031)Termination phase: Saturation
% 66.85/13.54 % (3268031)Time elapsed: 4.201 s
% 66.85/13.54 % (3268031)Peak memory usage: 28 MB
% 66.85/13.54 % (3268031)Instructions burned: 5132 (million)
% 66.85/13.54 % (3268058)ott+10_1_sil=32000:tgt=ground:random_seed=1689568088:i=5114:av=off_2938 on theBenchmark for (2938ds/5114Mi)
% 66.85/13.54 % TRYING [6]
% 66.85/13.54 % (3268056)Instruction limit reached!
% 66.85/13.54 % (3268056)------------------------------
% 66.85/13.54 % (3268056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268056)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268056)Termination reason: Instruction limit
% 66.85/13.54 % (3268056)Termination phase: Saturation
% 66.85/13.54 % (3268056)Time elapsed: 0.814 s
% 66.85/13.54 % (3268056)Peak memory usage: 18 MB
% 66.85/13.54 % (3268056)Instructions burned: 869 (million)
% 66.85/13.54 % (3268061)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=404026621:i=54282_2934 on theBenchmark for (2934ds/54282Mi)
% 66.85/13.54 % TRYING [1]
% 66.85/13.54 % TRYING [2]
% 66.85/13.54 % TRYING [3]
% 66.85/13.54 % TRYING [4]
% 66.85/13.54 % TRYING [5]
% 66.85/13.54 % (3268025)Instruction limit reached!
% 66.85/13.54 % (3268025)------------------------------
% 66.85/13.54 % (3268025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268025)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268025)Termination reason: Instruction limit
% 66.85/13.54 % (3268025)Termination phase: Finite model building constraint generation
% 66.85/13.54 % (3268025)Time elapsed: 6.596 s
% 66.85/13.54 % (3268025)Peak memory usage: 594 MB
% 66.85/13.54 % (3268025)Instructions burned: 9516 (million)
% 66.85/13.54 % (3268069)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2275616888:i=3512:aac=none_2916 on theBenchmark for (2916ds/3512Mi)
% 66.85/13.54 % TRYING [6]
% 66.85/13.54 % (3268058)Instruction limit reached!
% 66.85/13.54 % (3268058)------------------------------
% 66.85/13.54 % (3268058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268058)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268058)Termination reason: Instruction limit
% 66.85/13.54 % (3268058)Termination phase: Saturation
% 66.85/13.54 % (3268058)Time elapsed: 4.946 s
% 66.85/13.54 % (3268058)Peak memory usage: 55 MB
% 66.85/13.54 % (3268058)Instructions burned: 5114 (million)
% 66.85/13.54 % (3268074)dis+21_1_sil=32000:sas=cadical:random_seed=1980191738:i=3773:amm=off_2888 on theBenchmark for (2888ds/3773Mi)
% 66.85/13.54 % (3268069)Instruction limit reached!
% 66.85/13.54 % (3268069)------------------------------
% 66.85/13.54 % (3268069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.54 % (3268069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.54 % (3268069)CaDiCaL version: 2.1.3
% 66.85/13.54 % (3268069)Termination reason: Instruction limit
% 66.85/13.54 % (3268069)Termination phase: Saturation
% 66.85/13.54 % (3268069)Time elapsed: 3.232 s
% 66.85/13.54 % (3268069)Peak memory usage: 33 MB
% 66.85/13.54 % (3268069)Instructions burned: 3512 (million)
% 66.85/13.54 % (3268076)ott+11_1_sil=16000:gs=on:random_seed=3995233973:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2883 on theBenchmark for (2883ds/2251Mi)
% 66.85/13.54 % (3268074) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3267963-3268074"...
% 66.85/13.54 % (3268074)...printing done.
% 66.85/13.54 % (3268074)Refutation found. Thanks to Tanya!
% 66.85/13.54 % SZS status Theorem for theBenchmark
% 66.85/13.54 % SZS output start Proof for theBenchmark
% See solution above
% 66.85/13.55 % (3268074)------------------------------
% 66.85/13.55 % (3268074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.85/13.55 % (3268074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/13.55 % (3268074)CaDiCaL version: 2.1.3
% 66.85/13.55 % (3268074)Termination reason: Refutation
% 66.85/13.55 % (3268074)Time elapsed: 1.893 s
% 66.85/13.55 % (3268074)Peak memory usage: 24 MB
% 66.85/13.55 % (3268074)Instructions burned: 2185 (million)
% 66.85/13.55 % (3267963)Success in time 13.263 s
% 66.85/13.55 % Vampire exiting
%------------------------------------------------------------------------------