%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV037+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 : n015.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 40.11s 6.00s
% Output : Refutation 40.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 117
% Syntax : Number of formulae : 696 ( 58 unt; 114 def)
% Number of atoms : 4684 (1149 equ)
% Maximal formula atoms : 201 ( 6 avg)
% Number of connectives : 6744 (2756 ~;3115 |; 686 &)
% ( 96 <=>; 91 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 6 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 119 ( 117 usr; 115 prp; 0-2 aty)
% Number of functors : 58 ( 58 usr; 50 con; 0-3 aty)
% Number of variables : 227 ( 0 sgn 122 !; 105 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f48,axiom,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
fof(f49,axiom,
! [X0,X1,X2,X3,X4] :
( ( X0 != X1
& a_select2(X2,X1) = X3 )
=> a_select2(tptp_update2(X2,X0,X4),X1) = X3 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,minus(n3,n1)) )
=> a_select2(s_try7_init,X4) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_worst7) = init
& ( ~ gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& a_select2(s_values7_init,s_best7) = init
& ( ~ geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7))
=> ( init = init
& s_sworst7_init = init
& a_select2(s_values7_init,s_sworst7) = init
& ( ~ leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7))
=> ( init = init
& ( ~ gt(loopcounter,n1)
=> ( ! [X5] :
( ( leq(n0,X5)
& leq(X5,n2) )
=> ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select3(simplex7_init,X6,X5) = init ) )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n3) )
=> a_select2(s_values7_init,X7) = init )
& ( ~ geq(pv1403,tptp_float_0_001)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init ) ) ) )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init
& ! [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 )
& ( ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init ) ) ) ) ) )
& ( leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7))
=> ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& a_select2(s_values7_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)
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> ! [X12] :
( ( leq(n0,X12)
& leq(X12,n3) )
=> a_select3(simplex7_init,X12,X11) = init ) )
& ! [X13] :
( ( leq(n0,X13)
& leq(X13,n3) )
=> a_select2(s_values7_init,X13) = init )
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n2) )
=> a_select2(s_center7_init,X14) = init )
& ! [X15] :
( ( leq(n0,X15)
& leq(X15,minus(n3,n1)) )
=> a_select2(s_try7_init,X15) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,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 )
& ! [X20] :
( ( leq(n0,X20)
& leq(X20,minus(n3,n1)) )
=> a_select2(s_try7_init,X20) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X21] :
( ( leq(n0,X21)
& leq(X21,n2) )
=> ! [X22] :
( ( leq(n0,X22)
& leq(X22,n3) )
=> a_select3(simplex7_init,X22,X21) = init ) )
& ! [X23] :
( ( leq(n0,X23)
& leq(X23,n3) )
=> a_select2(tptp_update2(s_values7_init,s_worst7,init),X23) = init )
& ! [X24] :
( ( leq(n0,X24)
& leq(X24,n2) )
=> a_select2(s_center7_init,X24) = init )
& ! [X25] :
( ( leq(n0,X25)
& leq(X25,minus(n3,n1)) )
=> a_select2(s_try7_init,X25) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gauss_init_0061) ).
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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X0] :
( ( leq(n0,X0)
& leq(X0,n2) )
=> ! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> a_select3(simplex7_init,X1,X0) = init ) )
& ! [X2] :
( ( leq(n0,X2)
& leq(X2,n3) )
=> a_select2(s_values7_init,X2) = init )
& ! [X3] :
( ( leq(n0,X3)
& leq(X3,n2) )
=> a_select2(s_center7_init,X3) = init )
& ! [X4] :
( ( leq(n0,X4)
& leq(X4,minus(n3,n1)) )
=> a_select2(s_try7_init,X4) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) )
=> ( init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_worst7) = init
& ( ~ gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& a_select2(s_values7_init,s_best7) = init
& ( ~ geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7))
=> ( init = init
& s_sworst7_init = init
& a_select2(s_values7_init,s_sworst7) = init
& ( ~ leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7))
=> ( init = init
& ( ~ gt(loopcounter,n1)
=> ( ! [X5] :
( ( leq(n0,X5)
& leq(X5,n2) )
=> ! [X6] :
( ( leq(n0,X6)
& leq(X6,n3) )
=> a_select3(simplex7_init,X6,X5) = init ) )
& ! [X7] :
( ( leq(n0,X7)
& leq(X7,n3) )
=> a_select2(s_values7_init,X7) = init )
& ( ~ geq(pv1403,tptp_float_0_001)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init ) ) ) )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init
& ! [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 )
& ( ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( 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) ) )
& ( gt(loopcounter,n0)
=> ( a_select2(s_values7_init,s_best7) = init
& a_select2(s_values7_init,s_sworst7) = init
& a_select2(s_values7_init,s_worst7) = init ) ) ) ) ) )
& ( leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7))
=> ( s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& a_select2(s_values7_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)
& ! [X11] :
( ( leq(n0,X11)
& leq(X11,n2) )
=> ! [X12] :
( ( leq(n0,X12)
& leq(X12,n3) )
=> a_select3(simplex7_init,X12,X11) = init ) )
& ! [X13] :
( ( leq(n0,X13)
& leq(X13,n3) )
=> a_select2(s_values7_init,X13) = init )
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,n2) )
=> a_select2(s_center7_init,X14) = init )
& ! [X15] :
( ( leq(n0,X15)
& leq(X15,minus(n3,n1)) )
=> a_select2(s_try7_init,X15) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),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(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,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 )
& ! [X20] :
( ( leq(n0,X20)
& leq(X20,minus(n3,n1)) )
=> a_select2(s_try7_init,X20) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) )
& ( gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7))
=> ( init = init
& s_best7_init = init
& s_sworst7_init = init
& s_worst7_init = init
& leq(n0,s_best7)
& leq(n0,s_sworst7)
& leq(n0,s_worst7)
& leq(s_best7,n3)
& leq(s_sworst7,n3)
& leq(s_worst7,n3)
& ! [X21] :
( ( leq(n0,X21)
& leq(X21,n2) )
=> ! [X22] :
( ( leq(n0,X22)
& leq(X22,n3) )
=> a_select3(simplex7_init,X22,X21) = init ) )
& ! [X23] :
( ( leq(n0,X23)
& leq(X23,n3) )
=> a_select2(tptp_update2(s_values7_init,s_worst7,init),X23) = init )
& ! [X24] :
( ( leq(n0,X24)
& leq(X24,n2) )
=> a_select2(s_center7_init,X24) = init )
& ! [X25] :
( ( leq(n0,X25)
& leq(X25,minus(n3,n1)) )
=> a_select2(s_try7_init,X25) = init )
& ( gt(loopcounter,n1)
=> ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(ennf_transformation,[],[f49]) ).
fof(f148,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(flattening,[],[f147]) ).
fof(f151,plain,
( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| ( ( init != init
| ( ( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ( ( 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) )
& ~ geq(pv1403,tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) ) )
& ~ gt(loopcounter,n1) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| ? [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) )
| ( ( 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) )
& ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) ) )
& gt(loopcounter,n1) ) )
& ~ leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [X11] :
( ? [X12] :
( init != a_select3(simplex7_init,X12,X11)
& leq(n0,X12)
& leq(X12,n3) )
& leq(n0,X11)
& leq(X11,n2) )
| ? [X13] :
( init != a_select2(s_values7_init,X13)
& leq(n0,X13)
& leq(X13,n3) )
| ? [X14] :
( init != a_select2(s_center7_init,X14)
& leq(n0,X14)
& leq(X14,n2) )
| ? [X15] :
( init != a_select2(s_try7_init,X15)
& leq(n0,X15)
& leq(X15,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) ) )
& ~ geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ( ( 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)
| ? [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) )
| ? [X20] :
( init != a_select2(s_try7_init,X20)
& leq(n0,X20)
& leq(X20,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) ) )
& ~ gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ( ( init != init
| 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)
| ? [X21] :
( ? [X22] :
( init != a_select3(simplex7_init,X22,X21)
& leq(n0,X22)
& leq(X22,n3) )
& leq(n0,X21)
& leq(X21,n2) )
| ? [X23] :
( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),X23)
& leq(n0,X23)
& leq(X23,n3) )
| ? [X24] :
( init != a_select2(s_center7_init,X24)
& leq(n0,X24)
& leq(X24,n2) )
| ? [X25] :
( init != a_select2(s_try7_init,X25)
& leq(n0,X25)
& leq(X25,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) ) )
& 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)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f152,plain,
( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| ( ( init != init
| ( ( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ( ( 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) )
& ~ geq(pv1403,tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) ) )
& ~ gt(loopcounter,n1) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| ? [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) )
| ( ( 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) )
& ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) ) )
& gt(loopcounter,n1) ) )
& ~ leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ? [X11] :
( ? [X12] :
( init != a_select3(simplex7_init,X12,X11)
& leq(n0,X12)
& leq(X12,n3) )
& leq(n0,X11)
& leq(X11,n2) )
| ? [X13] :
( init != a_select2(s_values7_init,X13)
& leq(n0,X13)
& leq(X13,n3) )
| ? [X14] :
( init != a_select2(s_center7_init,X14)
& leq(n0,X14)
& leq(X14,n2) )
| ? [X15] :
( init != a_select2(s_try7_init,X15)
& leq(n0,X15)
& leq(X15,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) ) )
& ~ geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ( ( 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)
| ? [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) )
| ? [X20] :
( init != a_select2(s_try7_init,X20)
& leq(n0,X20)
& leq(X20,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) ) )
& ~ gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ( ( init != init
| 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)
| ? [X21] :
( ? [X22] :
( init != a_select3(simplex7_init,X22,X21)
& leq(n0,X22)
& leq(X22,n3) )
& leq(n0,X21)
& leq(X21,n2) )
| ? [X23] :
( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),X23)
& leq(n0,X23)
& leq(X23,n3) )
| ? [X24] :
( init != a_select2(s_center7_init,X24)
& leq(n0,X24)
& leq(X24,n2) )
| ? [X25] :
( init != a_select2(s_try7_init,X25)
& leq(n0,X25)
& leq(X25,minus(n3,n1)) )
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) ) )
& 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)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(flattening,[],[f151]) ).
fof(f172,definition,
( ? [X21] :
( ? [X22] :
( init != a_select3(simplex7_init,X22,X21)
& leq(n0,X22)
& leq(X22,n3) )
& leq(n0,X21)
& leq(X21,n2) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f173,definition,
( ? [X25] :
( init != a_select2(s_try7_init,X25)
& leq(n0,X25)
& leq(X25,minus(n3,n1)) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f174,definition,
( ? [X24] :
( init != a_select2(s_center7_init,X24)
& leq(n0,X24)
& leq(X24,n2) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f175,definition,
( ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f176,definition,
( ? [X20] :
( init != a_select2(s_try7_init,X20)
& leq(n0,X20)
& leq(X20,minus(n3,n1)) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f177,definition,
( ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f178,definition,
( ? [X11] :
( ? [X12] :
( init != a_select3(simplex7_init,X12,X11)
& leq(n0,X12)
& leq(X12,n3) )
& leq(n0,X11)
& leq(X11,n2) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f179,definition,
( ? [X15] :
( init != a_select2(s_try7_init,X15)
& leq(n0,X15)
& leq(X15,minus(n3,n1)) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f180,definition,
( ? [X14] :
( init != a_select2(s_center7_init,X14)
& leq(n0,X14)
& leq(X14,n2) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f181,definition,
( ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f182,definition,
( ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f183,definition,
( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| ( ( 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) )
& ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f184,definition,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f185,definition,
( ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f186,definition,
( sP16
| sP17
| ( ( 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) )
& ~ geq(pv1403,tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f187,definition,
( ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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
| ? [X13] :
( init != a_select2(s_values7_init,X13)
& leq(n0,X13)
& leq(X13,n3) )
| sP12
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f188,definition,
( ( ( 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)
| sP7
| ? [X18] :
( init != a_select2(s_values7_init,X18)
& leq(n0,X18)
& leq(X18,n3) )
| sP9
| sP8
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f189,definition,
( ( ( init != init
| 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)
| sP4
| ? [X23] :
( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),X23)
& leq(n0,X23)
& leq(X23,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f190,plain,
( ( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ( ( init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| ( ( init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| ( ( init != init
| ( sP18
& ~ gt(loopcounter,n1) )
| ( sP15
& gt(loopcounter,n1) ) )
& ~ leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| sP19 )
& ~ geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| sP20 )
& ~ gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| sP21 )
& 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)
& ! [X0] :
( ! [X1] :
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(n0,X1)
| ~ leq(X1,n3) )
| ~ leq(n0,X0)
| ~ leq(X0,n2) )
& ! [X2] :
( a_select2(s_values7_init,X2) = init
| ~ leq(n0,X2)
| ~ leq(X2,n3) )
& ! [X3] :
( a_select2(s_center7_init,X3) = init
| ~ leq(n0,X3)
| ~ leq(X3,n2) )
& ! [X4] :
( a_select2(s_try7_init,X4) = init
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) )
& ( ( pvar1400_init = init
& pvar1401_init = init
& pvar1402_init = init )
| ~ gt(loopcounter,n1) ) ),
inference(definition_folding,[],[f152,f189,f188,f187,f186,f185,f184,f183,f182,f181,f180,f179,f178,f177,f176,f175,f174,f173,f172]) ).
fof(f225,plain,
( ( ( init != init
| 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)
| sP4
| ? [X23] :
( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),X23)
& leq(n0,X23)
& leq(X23,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ~ sP21 ),
inference(nnf_transformation,[],[f189]) ).
fof(f226,plain,
( ( ( init != init
| 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)
| sP4
| ? [X0] :
( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ~ sP21 ),
inference(rectify,[],[f225]) ).
fof(f227,plain,
( ( ( init != init
| 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)
| sP4
| ( init != a_select2(tptp_update2(s_values7_init,s_worst7,init),sK49)
& leq(n0,sK49)
& leq(sK49,n3) )
| sP6
| sP5
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& gt(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_worst7)) )
| ~ sP21 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(X0,sK49)],[f226]) ).
fof(f228,plain,
( ( ( 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)
| sP7
| ? [X18] :
( init != a_select2(s_values7_init,X18)
& leq(n0,X18)
& leq(X18,n3) )
| sP9
| sP8
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ~ sP20 ),
inference(nnf_transformation,[],[f188]) ).
fof(f229,plain,
( ( ( 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)
| sP7
| ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| sP9
| sP8
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ~ sP20 ),
inference(rectify,[],[f228]) ).
fof(f230,plain,
( ( ( 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)
| sP7
| ( init != a_select2(s_values7_init,sK50)
& leq(n0,sK50)
& leq(sK50,n3) )
| sP9
| sP8
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& geq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_best7)) )
| ~ sP20 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(X0,sK50)],[f229]) ).
fof(f231,plain,
( ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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
| ? [X13] :
( init != a_select2(s_values7_init,X13)
& leq(n0,X13)
& leq(X13,n3) )
| sP12
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ~ sP19 ),
inference(nnf_transformation,[],[f187]) ).
fof(f232,plain,
( ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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) )
| sP12
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ~ sP19 ),
inference(rectify,[],[f231]) ).
fof(f233,plain,
( ( ( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
& leq(n0,sK51)
& leq(sK51,n3) )
| sP12
| sP11
| ( ( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init )
& gt(loopcounter,n1) ) )
& leq(plus(log(n2),divide(minus(minus(minus(plus(log(n330),log(n410)),log(pv1410)),n1),log(n4)),n2)),a_select2(s_values7,s_sworst7)) )
| ~ sP19 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X0,sK51)],[f232]) ).
fof(f234,plain,
( sP16
| sP17
| ( ( 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) )
& ~ geq(pv1403,tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) )
| ~ sP18 ),
inference(nnf_transformation,[],[f186]) ).
fof(f235,plain,
( ? [X7] :
( init != a_select2(s_values7_init,X7)
& leq(n0,X7)
& leq(X7,n3) )
| ~ sP17 ),
inference(nnf_transformation,[],[f185]) ).
fof(f236,plain,
( ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| ~ sP17 ),
inference(rectify,[],[f235]) ).
fof(f237,plain,
( ( init != a_select2(s_values7_init,sK52)
& leq(n0,sK52)
& leq(sK52,n3) )
| ~ sP17 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(X0,sK52)],[f236]) ).
fof(f238,plain,
( ? [X5] :
( ? [X6] :
( init != a_select3(simplex7_init,X6,X5)
& leq(n0,X6)
& leq(X6,n3) )
& leq(n0,X5)
& leq(X5,n2) )
| ~ sP16 ),
inference(nnf_transformation,[],[f184]) ).
fof(f239,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP16 ),
inference(rectify,[],[f238]) ).
fof(f240,plain,
( ( init != a_select3(simplex7_init,sK54,sK53)
& leq(n0,sK54)
& leq(sK54,n3)
& leq(n0,sK53)
& leq(sK53,n2) )
| ~ sP16 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53,sK54]),skolemize(X0,sK53),skolemize(X1,sK54)],[f239]) ).
fof(f241,plain,
( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| ( ( 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) )
& ~ geq(plus(abs(minus(a_select2(s_values7,s_best7),pv1400)),plus(abs(minus(a_select2(s_values7,s_sworst7),pv1401)),abs(minus(a_select2(s_values7,s_worst7),pv1402)))),tptp_float_0_001) )
| ( ( 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) )
& gt(loopcounter,n0) )
| ( ( init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7) )
& gt(loopcounter,n0) )
| ~ sP15 ),
inference(nnf_transformation,[],[f183]) ).
fof(f242,plain,
( ? [X10] :
( init != a_select2(s_values7_init,X10)
& leq(n0,X10)
& leq(X10,n3) )
| ~ sP14 ),
inference(nnf_transformation,[],[f182]) ).
fof(f243,plain,
( ? [X0] :
( init != a_select2(s_values7_init,X0)
& leq(n0,X0)
& leq(X0,n3) )
| ~ sP14 ),
inference(rectify,[],[f242]) ).
fof(f244,plain,
( ( init != a_select2(s_values7_init,sK55)
& leq(n0,sK55)
& leq(sK55,n3) )
| ~ sP14 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(X0,sK55)],[f243]) ).
fof(f245,plain,
( ? [X8] :
( ? [X9] :
( init != a_select3(simplex7_init,X9,X8)
& leq(n0,X9)
& leq(X9,n3) )
& leq(n0,X8)
& leq(X8,n2) )
| ~ sP13 ),
inference(nnf_transformation,[],[f181]) ).
fof(f246,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP13 ),
inference(rectify,[],[f245]) ).
fof(f247,plain,
( ( init != a_select3(simplex7_init,sK57,sK56)
& leq(n0,sK57)
& leq(sK57,n3)
& leq(n0,sK56)
& leq(sK56,n2) )
| ~ sP13 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56,sK57]),skolemize(X0,sK56),skolemize(X1,sK57)],[f246]) ).
fof(f248,plain,
( ? [X14] :
( init != a_select2(s_center7_init,X14)
& leq(n0,X14)
& leq(X14,n2) )
| ~ sP12 ),
inference(nnf_transformation,[],[f180]) ).
fof(f249,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP12 ),
inference(rectify,[],[f248]) ).
fof(f250,plain,
( ( init != a_select2(s_center7_init,sK58)
& leq(n0,sK58)
& leq(sK58,n2) )
| ~ sP12 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X0,sK58)],[f249]) ).
fof(f251,plain,
( ? [X15] :
( init != a_select2(s_try7_init,X15)
& leq(n0,X15)
& leq(X15,minus(n3,n1)) )
| ~ sP11 ),
inference(nnf_transformation,[],[f179]) ).
fof(f252,plain,
( ? [X0] :
( init != a_select2(s_try7_init,X0)
& leq(n0,X0)
& leq(X0,minus(n3,n1)) )
| ~ sP11 ),
inference(rectify,[],[f251]) ).
fof(f253,plain,
( ( init != a_select2(s_try7_init,sK59)
& leq(n0,sK59)
& leq(sK59,minus(n3,n1)) )
| ~ sP11 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X0,sK59)],[f252]) ).
fof(f254,plain,
( ? [X11] :
( ? [X12] :
( init != a_select3(simplex7_init,X12,X11)
& leq(n0,X12)
& leq(X12,n3) )
& leq(n0,X11)
& leq(X11,n2) )
| ~ sP10 ),
inference(nnf_transformation,[],[f178]) ).
fof(f255,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,[],[f254]) ).
fof(f256,plain,
( ( init != a_select3(simplex7_init,sK61,sK60)
& leq(n0,sK61)
& leq(sK61,n3)
& leq(n0,sK60)
& leq(sK60,n2) )
| ~ sP10 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60,sK61]),skolemize(X0,sK60),skolemize(X1,sK61)],[f255]) ).
fof(f257,plain,
( ? [X19] :
( init != a_select2(s_center7_init,X19)
& leq(n0,X19)
& leq(X19,n2) )
| ~ sP9 ),
inference(nnf_transformation,[],[f177]) ).
fof(f258,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP9 ),
inference(rectify,[],[f257]) ).
fof(f259,plain,
( ( init != a_select2(s_center7_init,sK62)
& leq(n0,sK62)
& leq(sK62,n2) )
| ~ sP9 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X0,sK62)],[f258]) ).
fof(f260,plain,
( ? [X20] :
( init != a_select2(s_try7_init,X20)
& leq(n0,X20)
& leq(X20,minus(n3,n1)) )
| ~ sP8 ),
inference(nnf_transformation,[],[f176]) ).
fof(f261,plain,
( ? [X0] :
( init != a_select2(s_try7_init,X0)
& leq(n0,X0)
& leq(X0,minus(n3,n1)) )
| ~ sP8 ),
inference(rectify,[],[f260]) ).
fof(f262,plain,
( ( init != a_select2(s_try7_init,sK63)
& leq(n0,sK63)
& leq(sK63,minus(n3,n1)) )
| ~ sP8 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X0,sK63)],[f261]) ).
fof(f263,plain,
( ? [X16] :
( ? [X17] :
( init != a_select3(simplex7_init,X17,X16)
& leq(n0,X17)
& leq(X17,n3) )
& leq(n0,X16)
& leq(X16,n2) )
| ~ sP7 ),
inference(nnf_transformation,[],[f175]) ).
fof(f264,plain,
( ? [X0] :
( ? [X1] :
( init != a_select3(simplex7_init,X1,X0)
& leq(n0,X1)
& leq(X1,n3) )
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP7 ),
inference(rectify,[],[f263]) ).
fof(f265,plain,
( ( init != a_select3(simplex7_init,sK65,sK64)
& leq(n0,sK65)
& leq(sK65,n3)
& leq(n0,sK64)
& leq(sK64,n2) )
| ~ sP7 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65]),skolemize(X0,sK64),skolemize(X1,sK65)],[f264]) ).
fof(f266,plain,
( ? [X24] :
( init != a_select2(s_center7_init,X24)
& leq(n0,X24)
& leq(X24,n2) )
| ~ sP6 ),
inference(nnf_transformation,[],[f174]) ).
fof(f267,plain,
( ? [X0] :
( init != a_select2(s_center7_init,X0)
& leq(n0,X0)
& leq(X0,n2) )
| ~ sP6 ),
inference(rectify,[],[f266]) ).
fof(f268,plain,
( ( init != a_select2(s_center7_init,sK66)
& leq(n0,sK66)
& leq(sK66,n2) )
| ~ sP6 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(X0,sK66)],[f267]) ).
fof(f269,plain,
( ? [X25] :
( init != a_select2(s_try7_init,X25)
& leq(n0,X25)
& leq(X25,minus(n3,n1)) )
| ~ sP5 ),
inference(nnf_transformation,[],[f173]) ).
fof(f270,plain,
( ? [X0] :
( init != a_select2(s_try7_init,X0)
& leq(n0,X0)
& leq(X0,minus(n3,n1)) )
| ~ sP5 ),
inference(rectify,[],[f269]) ).
fof(f271,plain,
( ( init != a_select2(s_try7_init,sK67)
& leq(n0,sK67)
& leq(sK67,minus(n3,n1)) )
| ~ sP5 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(X0,sK67)],[f270]) ).
fof(f272,plain,
( ? [X21] :
( ? [X22] :
( init != a_select3(simplex7_init,X22,X21)
& leq(n0,X22)
& leq(X22,n3) )
& leq(n0,X21)
& leq(X21,n2) )
| ~ sP4 ),
inference(nnf_transformation,[],[f172]) ).
fof(f273,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,[],[f272]) ).
fof(f274,plain,
( ( init != a_select3(simplex7_init,sK69,sK68)
& leq(n0,sK69)
& leq(sK69,n3)
& leq(n0,sK68)
& leq(sK68,n2) )
| ~ sP4 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68,sK69]),skolemize(X0,sK68),skolemize(X1,sK69)],[f273]) ).
fof(f381,plain,
! [X2,X0,X1] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f48]) ).
fof(f382,plain,
! [X2,X3,X0,X1,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| X0 = X1
| a_select2(X2,X1) != X3 ),
inference(cnf_transformation,[],[f148]) ).
fof(f388,plain,
( init != init
| 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f389,plain,
( init != init
| 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f390,plain,
( init != init
| 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f391,plain,
( init != init
| 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f392,plain,
( init != init
| 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)
| sP4
| init != a_select2(tptp_update2(s_values7_init,s_worst7,init),sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f393,plain,
( init != init
| 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)
| sP4
| init != a_select2(tptp_update2(s_values7_init,s_worst7,init),sK49)
| sP6
| sP5
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP21 ),
inference(cnf_transformation,[],[f227]) ).
fof(f395,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f396,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f397,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f398,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f399,plain,
( 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)
| sP7
| init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f400,plain,
( 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)
| sP7
| init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP20 ),
inference(cnf_transformation,[],[f230]) ).
fof(f402,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f403,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f404,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f405,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f406,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f407,plain,
( s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| ~ sP19 ),
inference(cnf_transformation,[],[f233]) ).
fof(f415,plain,
( sP16
| sP17
| 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)
| 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)
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| ~ sP18 ),
inference(cnf_transformation,[],[f234]) ).
fof(f416,plain,
( leq(sK52,n3)
| ~ sP17 ),
inference(cnf_transformation,[],[f237]) ).
fof(f417,plain,
( leq(n0,sK52)
| ~ sP17 ),
inference(cnf_transformation,[],[f237]) ).
fof(f418,plain,
( init != a_select2(s_values7_init,sK52)
| ~ sP17 ),
inference(cnf_transformation,[],[f237]) ).
fof(f419,plain,
( leq(sK53,n2)
| ~ sP16 ),
inference(cnf_transformation,[],[f240]) ).
fof(f420,plain,
( leq(n0,sK53)
| ~ sP16 ),
inference(cnf_transformation,[],[f240]) ).
fof(f421,plain,
( leq(sK54,n3)
| ~ sP16 ),
inference(cnf_transformation,[],[f240]) ).
fof(f422,plain,
( leq(n0,sK54)
| ~ sP16 ),
inference(cnf_transformation,[],[f240]) ).
fof(f423,plain,
( init != a_select3(simplex7_init,sK54,sK53)
| ~ sP16 ),
inference(cnf_transformation,[],[f240]) ).
fof(f431,plain,
( init != pvar1400_init
| init != pvar1401_init
| init != pvar1402_init
| s_best7_init != init
| init != s_sworst7_init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| 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)
| 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)
| init != a_select2(s_values7_init,s_best7)
| init != a_select2(s_values7_init,s_sworst7)
| init != a_select2(s_values7_init,s_worst7)
| ~ sP15 ),
inference(cnf_transformation,[],[f241]) ).
fof(f432,plain,
( leq(sK55,n3)
| ~ sP14 ),
inference(cnf_transformation,[],[f244]) ).
fof(f433,plain,
( leq(n0,sK55)
| ~ sP14 ),
inference(cnf_transformation,[],[f244]) ).
fof(f434,plain,
( init != a_select2(s_values7_init,sK55)
| ~ sP14 ),
inference(cnf_transformation,[],[f244]) ).
fof(f435,plain,
( leq(sK56,n2)
| ~ sP13 ),
inference(cnf_transformation,[],[f247]) ).
fof(f436,plain,
( leq(n0,sK56)
| ~ sP13 ),
inference(cnf_transformation,[],[f247]) ).
fof(f437,plain,
( leq(sK57,n3)
| ~ sP13 ),
inference(cnf_transformation,[],[f247]) ).
fof(f438,plain,
( leq(n0,sK57)
| ~ sP13 ),
inference(cnf_transformation,[],[f247]) ).
fof(f439,plain,
( init != a_select3(simplex7_init,sK57,sK56)
| ~ sP13 ),
inference(cnf_transformation,[],[f247]) ).
fof(f440,plain,
( leq(sK58,n2)
| ~ sP12 ),
inference(cnf_transformation,[],[f250]) ).
fof(f441,plain,
( leq(n0,sK58)
| ~ sP12 ),
inference(cnf_transformation,[],[f250]) ).
fof(f442,plain,
( init != a_select2(s_center7_init,sK58)
| ~ sP12 ),
inference(cnf_transformation,[],[f250]) ).
fof(f443,plain,
( leq(sK59,minus(n3,n1))
| ~ sP11 ),
inference(cnf_transformation,[],[f253]) ).
fof(f444,plain,
( leq(n0,sK59)
| ~ sP11 ),
inference(cnf_transformation,[],[f253]) ).
fof(f445,plain,
( init != a_select2(s_try7_init,sK59)
| ~ sP11 ),
inference(cnf_transformation,[],[f253]) ).
fof(f446,plain,
( leq(sK60,n2)
| ~ sP10 ),
inference(cnf_transformation,[],[f256]) ).
fof(f447,plain,
( leq(n0,sK60)
| ~ sP10 ),
inference(cnf_transformation,[],[f256]) ).
fof(f448,plain,
( leq(sK61,n3)
| ~ sP10 ),
inference(cnf_transformation,[],[f256]) ).
fof(f449,plain,
( leq(n0,sK61)
| ~ sP10 ),
inference(cnf_transformation,[],[f256]) ).
fof(f450,plain,
( init != a_select3(simplex7_init,sK61,sK60)
| ~ sP10 ),
inference(cnf_transformation,[],[f256]) ).
fof(f451,plain,
( leq(sK62,n2)
| ~ sP9 ),
inference(cnf_transformation,[],[f259]) ).
fof(f452,plain,
( leq(n0,sK62)
| ~ sP9 ),
inference(cnf_transformation,[],[f259]) ).
fof(f453,plain,
( init != a_select2(s_center7_init,sK62)
| ~ sP9 ),
inference(cnf_transformation,[],[f259]) ).
fof(f454,plain,
( leq(sK63,minus(n3,n1))
| ~ sP8 ),
inference(cnf_transformation,[],[f262]) ).
fof(f455,plain,
( leq(n0,sK63)
| ~ sP8 ),
inference(cnf_transformation,[],[f262]) ).
fof(f456,plain,
( init != a_select2(s_try7_init,sK63)
| ~ sP8 ),
inference(cnf_transformation,[],[f262]) ).
fof(f457,plain,
( leq(sK64,n2)
| ~ sP7 ),
inference(cnf_transformation,[],[f265]) ).
fof(f458,plain,
( leq(n0,sK64)
| ~ sP7 ),
inference(cnf_transformation,[],[f265]) ).
fof(f459,plain,
( leq(sK65,n3)
| ~ sP7 ),
inference(cnf_transformation,[],[f265]) ).
fof(f460,plain,
( leq(n0,sK65)
| ~ sP7 ),
inference(cnf_transformation,[],[f265]) ).
fof(f461,plain,
( init != a_select3(simplex7_init,sK65,sK64)
| ~ sP7 ),
inference(cnf_transformation,[],[f265]) ).
fof(f462,plain,
( leq(sK66,n2)
| ~ sP6 ),
inference(cnf_transformation,[],[f268]) ).
fof(f463,plain,
( leq(n0,sK66)
| ~ sP6 ),
inference(cnf_transformation,[],[f268]) ).
fof(f464,plain,
( init != a_select2(s_center7_init,sK66)
| ~ sP6 ),
inference(cnf_transformation,[],[f268]) ).
fof(f465,plain,
( leq(sK67,minus(n3,n1))
| ~ sP5 ),
inference(cnf_transformation,[],[f271]) ).
fof(f466,plain,
( leq(n0,sK67)
| ~ sP5 ),
inference(cnf_transformation,[],[f271]) ).
fof(f467,plain,
( init != a_select2(s_try7_init,sK67)
| ~ sP5 ),
inference(cnf_transformation,[],[f271]) ).
fof(f468,plain,
( leq(sK68,n2)
| ~ sP4 ),
inference(cnf_transformation,[],[f274]) ).
fof(f469,plain,
( leq(n0,sK68)
| ~ sP4 ),
inference(cnf_transformation,[],[f274]) ).
fof(f470,plain,
( leq(sK69,n3)
| ~ sP4 ),
inference(cnf_transformation,[],[f274]) ).
fof(f471,plain,
( leq(n0,sK69)
| ~ sP4 ),
inference(cnf_transformation,[],[f274]) ).
fof(f472,plain,
( init != a_select3(simplex7_init,sK69,sK68)
| ~ sP4 ),
inference(cnf_transformation,[],[f274]) ).
fof(f473,plain,
( init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f474,plain,
( init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f475,plain,
( init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f476,plain,
! [X4] :
( init = a_select2(s_try7_init,X4)
| ~ leq(n0,X4)
| ~ leq(X4,minus(n3,n1)) ),
inference(cnf_transformation,[],[f190]) ).
fof(f477,plain,
! [X3] :
( init = a_select2(s_center7_init,X3)
| ~ leq(n0,X3)
| ~ leq(X3,n2) ),
inference(cnf_transformation,[],[f190]) ).
fof(f478,plain,
! [X2] :
( init = a_select2(s_values7_init,X2)
| ~ leq(n0,X2)
| ~ leq(X2,n3) ),
inference(cnf_transformation,[],[f190]) ).
fof(f479,plain,
! [X0,X1] :
( init = a_select3(simplex7_init,X1,X0)
| ~ leq(n0,X1)
| ~ leq(X1,n3)
| ~ leq(n0,X0)
| ~ leq(X0,n2) ),
inference(cnf_transformation,[],[f190]) ).
fof(f480,plain,
leq(s_worst7,n3),
inference(cnf_transformation,[],[f190]) ).
fof(f481,plain,
leq(s_sworst7,n3),
inference(cnf_transformation,[],[f190]) ).
fof(f482,plain,
leq(s_best7,n3),
inference(cnf_transformation,[],[f190]) ).
fof(f483,plain,
leq(n0,s_worst7),
inference(cnf_transformation,[],[f190]) ).
fof(f484,plain,
leq(n0,s_sworst7),
inference(cnf_transformation,[],[f190]) ).
fof(f485,plain,
leq(n0,s_best7),
inference(cnf_transformation,[],[f190]) ).
fof(f486,plain,
init = s_worst7_init,
inference(cnf_transformation,[],[f190]) ).
fof(f487,plain,
init = s_sworst7_init,
inference(cnf_transformation,[],[f190]) ).
fof(f488,plain,
s_best7_init = init,
inference(cnf_transformation,[],[f190]) ).
fof(f494,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != init
| sP18
| gt(loopcounter,n1)
| sP19
| sP20
| sP21 ),
inference(cnf_transformation,[],[f190]) ).
fof(f495,plain,
( init != init
| init != s_worst7_init
| init != a_select2(s_values7_init,s_worst7)
| init != init
| s_best7_init != init
| init != a_select2(s_values7_init,s_best7)
| init != init
| init != s_sworst7_init
| init != a_select2(s_values7_init,s_sworst7)
| init != init
| sP18
| sP15
| sP19
| sP20
| sP21 ),
inference(cnf_transformation,[],[f190]) ).
fof(f543,plain,
s_best7_init = s_sworst7_init,
inference(definition_unfolding,[],[f488,f487]) ).
fof(f565,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(definition_unfolding,[],[f393,f487,f487,f543,f487,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f566,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(definition_unfolding,[],[f392,f487,f487,f543,f487,f487,f487,f487,f487]) ).
fof(f567,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(definition_unfolding,[],[f391,f487,f487,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f568,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(definition_unfolding,[],[f390,f487,f487,f543,f487,f487,f487]) ).
fof(f569,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(definition_unfolding,[],[f389,f487,f487,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f570,plain,
( s_sworst7_init != s_sworst7_init
| 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(definition_unfolding,[],[f388,f487,f487,f543,f487,f487,f487]) ).
fof(f571,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(definition_unfolding,[],[f400,f543,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f572,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(definition_unfolding,[],[f399,f543,f487,f487,f487,f487]) ).
fof(f573,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(definition_unfolding,[],[f398,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f574,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(definition_unfolding,[],[f397,f543,f487,f487,f487]) ).
fof(f575,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(definition_unfolding,[],[f396,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f576,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_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(definition_unfolding,[],[f395,f543,f487,f487,f487]) ).
fof(f577,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(definition_unfolding,[],[f407,f543,f487,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f578,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(definition_unfolding,[],[f406,f543,f487,f487,f487,f487,f487]) ).
fof(f579,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(definition_unfolding,[],[f405,f543,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f580,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(definition_unfolding,[],[f404,f543,f487,f487,f487,f487]) ).
fof(f581,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(definition_unfolding,[],[f403,f543,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f582,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(definition_unfolding,[],[f402,f543,f487,f487,f487,f487]) ).
fof(f583,plain,
( sP16
| sP17
| 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)
| 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)
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ sP18 ),
inference(definition_unfolding,[],[f415,f543,f487,f487,f487,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f590,plain,
( s_sworst7_init != a_select2(s_values7_init,sK52)
| ~ sP17 ),
inference(definition_unfolding,[],[f418,f487]) ).
fof(f591,plain,
( s_sworst7_init != a_select3(simplex7_init,sK54,sK53)
| ~ sP16 ),
inference(definition_unfolding,[],[f423,f487]) ).
fof(f592,plain,
( s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| 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)
| 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)
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ sP15 ),
inference(definition_unfolding,[],[f431,f487,f487,f487,f543,f487,f487,f487,f487,f487,f487,f543,f487,f487,f487,f543,f487,f487,f487,f487,f487,f487]) ).
fof(f600,plain,
( s_sworst7_init != a_select2(s_values7_init,sK55)
| ~ sP14 ),
inference(definition_unfolding,[],[f434,f487]) ).
fof(f601,plain,
( s_sworst7_init != a_select3(simplex7_init,sK57,sK56)
| ~ sP13 ),
inference(definition_unfolding,[],[f439,f487]) ).
fof(f602,plain,
( s_sworst7_init != a_select2(s_center7_init,sK58)
| ~ sP12 ),
inference(definition_unfolding,[],[f442,f487]) ).
fof(f603,plain,
( s_sworst7_init != a_select2(s_try7_init,sK59)
| ~ sP11 ),
inference(definition_unfolding,[],[f445,f487]) ).
fof(f604,plain,
( s_sworst7_init != a_select3(simplex7_init,sK61,sK60)
| ~ sP10 ),
inference(definition_unfolding,[],[f450,f487]) ).
fof(f605,plain,
( s_sworst7_init != a_select2(s_center7_init,sK62)
| ~ sP9 ),
inference(definition_unfolding,[],[f453,f487]) ).
fof(f606,plain,
( s_sworst7_init != a_select2(s_try7_init,sK63)
| ~ sP8 ),
inference(definition_unfolding,[],[f456,f487]) ).
fof(f607,plain,
( s_sworst7_init != a_select3(simplex7_init,sK65,sK64)
| ~ sP7 ),
inference(definition_unfolding,[],[f461,f487]) ).
fof(f608,plain,
( s_sworst7_init != a_select2(s_center7_init,sK66)
| ~ sP6 ),
inference(definition_unfolding,[],[f464,f487]) ).
fof(f609,plain,
( s_sworst7_init != a_select2(s_try7_init,sK67)
| ~ sP5 ),
inference(definition_unfolding,[],[f467,f487]) ).
fof(f610,plain,
( s_sworst7_init != a_select3(simplex7_init,sK69,sK68)
| ~ sP4 ),
inference(definition_unfolding,[],[f472,f487]) ).
fof(f611,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 != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| 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 != s_sworst7_init
| sP18
| sP15
| sP19
| sP20
| sP21 ),
inference(definition_unfolding,[],[f495,f487,f487,f487,f487,f487,f487,f543,f487,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f612,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 != s_sworst7_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| 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 != s_sworst7_init
| sP18
| gt(loopcounter,n1)
| sP19
| sP20
| sP21 ),
inference(definition_unfolding,[],[f494,f487,f487,f487,f487,f487,f487,f543,f487,f487,f487,f487,f487,f487,f487,f487]) ).
fof(f618,plain,
s_sworst7_init = s_worst7_init,
inference(definition_unfolding,[],[f486,f487]) ).
fof(f619,plain,
! [X0,X1] :
( ~ leq(X0,n2)
| ~ leq(n0,X1)
| ~ leq(X1,n3)
| ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X1,X0) ),
inference(definition_unfolding,[],[f479,f487]) ).
fof(f620,plain,
! [X2] :
( ~ leq(X2,n3)
| ~ leq(n0,X2)
| s_sworst7_init = a_select2(s_values7_init,X2) ),
inference(definition_unfolding,[],[f478,f487]) ).
fof(f621,plain,
! [X3] :
( ~ leq(X3,n2)
| ~ leq(n0,X3)
| s_sworst7_init = a_select2(s_center7_init,X3) ),
inference(definition_unfolding,[],[f477,f487]) ).
fof(f622,plain,
! [X4] :
( ~ leq(X4,minus(n3,n1))
| ~ leq(n0,X4)
| s_sworst7_init = a_select2(s_try7_init,X4) ),
inference(definition_unfolding,[],[f476,f487]) ).
fof(f623,plain,
( s_sworst7_init = pvar1400_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f475,f487]) ).
fof(f624,plain,
( s_sworst7_init = pvar1401_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f474,f487]) ).
fof(f625,plain,
( s_sworst7_init = pvar1402_init
| ~ gt(loopcounter,n1) ),
inference(definition_unfolding,[],[f473,f487]) ).
fof(f633,plain,
! [X2,X0,X1,X4] :
( a_select2(X2,X1) = a_select2(tptp_update2(X2,X0,X4),X1)
| X0 = X1 ),
inference(equality_resolution,[],[f382]) ).
fof(f642,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,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| sP18
| gt(loopcounter,n1)
| sP19
| sP20
| sP21 ),
inference(duplicate_literal_removal,[],[f612]) ).
fof(f643,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,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| sP18
| gt(loopcounter,n1)
| sP19
| sP20
| sP21 ),
inference(trivial_inequality_removal,[],[f642]) ).
fof(f644,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,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| sP18
| sP15
| sP19
| sP20
| sP21 ),
inference(duplicate_literal_removal,[],[f611]) ).
fof(f645,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,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| sP18
| sP15
| sP19
| sP20
| sP21 ),
inference(trivial_inequality_removal,[],[f644]) ).
fof(f660,plain,
( s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ sP15 ),
inference(duplicate_literal_removal,[],[f592]) ).
fof(f661,plain,
( s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| sP13
| sP14
| ~ leq(n0,s_best7)
| ~ leq(n0,s_sworst7)
| ~ leq(n0,s_worst7)
| ~ leq(s_best7,n3)
| ~ leq(s_sworst7,n3)
| ~ leq(s_worst7,n3)
| ~ sP15 ),
inference(trivial_inequality_removal,[],[f660]) ).
fof(f673,plain,
( sP16
| sP17
| 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)
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ sP18 ),
inference(duplicate_literal_removal,[],[f583]) ).
fof(f674,plain,
( sP16
| sP17
| 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)
| s_sworst7_init != a_select2(s_values7_init,s_best7)
| s_sworst7_init != a_select2(s_values7_init,s_sworst7)
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ sP18 ),
inference(trivial_inequality_removal,[],[f673]) ).
fof(f675,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f582]) ).
fof(f676,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f675]) ).
fof(f677,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f581]) ).
fof(f678,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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(sK51,n3)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f677]) ).
fof(f679,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f580]) ).
fof(f680,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f679]) ).
fof(f681,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f579]) ).
fof(f682,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f681]) ).
fof(f683,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f578]) ).
fof(f684,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| gt(loopcounter,n1)
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f683]) ).
fof(f685,plain,
( s_sworst7_init != s_sworst7_init
| s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(duplicate_literal_removal,[],[f577]) ).
fof(f686,plain,
( s_sworst7_init != s_worst7_init
| s_sworst7_init != a_select2(s_values7_init,s_worst7)
| ~ 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,sK51)
| sP12
| sP11
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP19 ),
inference(trivial_inequality_removal,[],[f685]) ).
fof(f687,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f576]) ).
fof(f688,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f687]) ).
fof(f689,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f575]) ).
fof(f690,plain,
( 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)
| sP7
| leq(sK50,n3)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f689]) ).
fof(f691,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f574]) ).
fof(f692,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f691]) ).
fof(f693,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f573]) ).
fof(f694,plain,
( 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)
| sP7
| leq(n0,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f693]) ).
fof(f695,plain,
( 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)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f572]) ).
fof(f696,plain,
( 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)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| gt(loopcounter,n1)
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f695]) ).
fof(f697,plain,
( 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)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(duplicate_literal_removal,[],[f571]) ).
fof(f698,plain,
( 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)
| sP7
| s_sworst7_init != a_select2(s_values7_init,sK50)
| sP9
| sP8
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP20 ),
inference(trivial_inequality_removal,[],[f697]) ).
fof(f699,plain,
( 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f570]) ).
fof(f700,plain,
( 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f699]) ).
fof(f701,plain,
( 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f569]) ).
fof(f702,plain,
( 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)
| sP4
| leq(sK49,n3)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f701]) ).
fof(f703,plain,
( 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f568]) ).
fof(f704,plain,
( 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f703]) ).
fof(f705,plain,
( 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f567]) ).
fof(f706,plain,
( 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)
| sP4
| leq(n0,sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f705]) ).
fof(f707,plain,
( 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f566]) ).
fof(f708,plain,
( 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| gt(loopcounter,n1)
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f707]) ).
fof(f709,plain,
( 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(duplicate_literal_removal,[],[f565]) ).
fof(f710,plain,
( 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)
| sP4
| s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| sP6
| sP5
| s_sworst7_init != pvar1400_init
| s_sworst7_init != pvar1401_init
| s_sworst7_init != pvar1402_init
| ~ sP21 ),
inference(trivial_inequality_removal,[],[f709]) ).
fof(f712,definition,
( spl70_1
<=> gt(loopcounter,n1) ),
introduced(definition,[new_symbols(definition,[spl70_1])],[avatar_definition]) ).
fof(f716,definition,
( spl70_2
<=> s_sworst7_init = pvar1402_init ),
introduced(definition,[new_symbols(definition,[spl70_2])],[avatar_definition]) ).
fof(f719,plain,
( ~ spl70_1
| spl70_2 ),
inference(avatar_split_clause,[],[f625,f716,f712]) ).
fof(f721,definition,
( spl70_3
<=> s_sworst7_init = pvar1401_init ),
introduced(definition,[new_symbols(definition,[spl70_3])],[avatar_definition]) ).
fof(f724,plain,
( ~ spl70_1
| spl70_3 ),
inference(avatar_split_clause,[],[f624,f721,f712]) ).
fof(f726,definition,
( spl70_4
<=> s_sworst7_init = pvar1400_init ),
introduced(definition,[new_symbols(definition,[spl70_4])],[avatar_definition]) ).
fof(f729,plain,
( ~ spl70_1
| spl70_4 ),
inference(avatar_split_clause,[],[f623,f726,f712]) ).
fof(f731,definition,
( spl70_5
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl70_5])],[avatar_definition]) ).
fof(f739,definition,
( spl70_7
<=> s_sworst7_init = a_select2(s_values7_init,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl70_7])],[avatar_definition]) ).
fof(f743,definition,
( spl70_8
<=> s_sworst7_init = s_worst7_init ),
introduced(definition,[new_symbols(definition,[spl70_8])],[avatar_definition]) ).
fof(f748,definition,
( spl70_9
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl70_9])],[avatar_definition]) ).
fof(f756,definition,
( spl70_11
<=> s_sworst7_init = a_select2(s_values7_init,s_best7) ),
introduced(definition,[new_symbols(definition,[spl70_11])],[avatar_definition]) ).
fof(f761,definition,
( spl70_12
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl70_12])],[avatar_definition]) ).
fof(f769,definition,
( spl70_14
<=> s_sworst7_init = a_select2(s_values7_init,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl70_14])],[avatar_definition]) ).
fof(f774,definition,
( spl70_15
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl70_15])],[avatar_definition]) ).
fof(f779,definition,
( spl70_16
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl70_16])],[avatar_definition]) ).
fof(f782,plain,
( spl70_5
| spl70_9
| spl70_12
| spl70_1
| spl70_16
| ~ spl70_14
| ~ spl70_11
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f643,f743,f739,f756,f769,f779,f712,f761,f748,f731]) ).
fof(f783,plain,
( spl70_5
| spl70_9
| spl70_12
| spl70_15
| spl70_16
| ~ spl70_14
| ~ spl70_11
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f645,f743,f739,f756,f769,f779,f774,f761,f748,f731]) ).
fof(f785,definition,
( spl70_17
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl70_17])],[avatar_definition]) ).
fof(f789,definition,
( spl70_18
<=> leq(sK68,n2) ),
introduced(definition,[new_symbols(definition,[spl70_18])],[avatar_definition]) ).
fof(f791,plain,
( leq(sK68,n2)
| ~ spl70_18 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f792,plain,
( ~ spl70_17
| spl70_18 ),
inference(avatar_split_clause,[],[f468,f789,f785]) ).
fof(f794,definition,
( spl70_19
<=> leq(n0,sK68) ),
introduced(definition,[new_symbols(definition,[spl70_19])],[avatar_definition]) ).
fof(f797,plain,
( ~ spl70_17
| spl70_19 ),
inference(avatar_split_clause,[],[f469,f794,f785]) ).
fof(f799,definition,
( spl70_20
<=> leq(sK69,n3) ),
introduced(definition,[new_symbols(definition,[spl70_20])],[avatar_definition]) ).
fof(f801,plain,
( leq(sK69,n3)
| ~ spl70_20 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f802,plain,
( ~ spl70_17
| spl70_20 ),
inference(avatar_split_clause,[],[f470,f799,f785]) ).
fof(f804,definition,
( spl70_21
<=> leq(n0,sK69) ),
introduced(definition,[new_symbols(definition,[spl70_21])],[avatar_definition]) ).
fof(f807,plain,
( ~ spl70_17
| spl70_21 ),
inference(avatar_split_clause,[],[f471,f804,f785]) ).
fof(f809,definition,
( spl70_22
<=> s_sworst7_init = a_select3(simplex7_init,sK69,sK68) ),
introduced(definition,[new_symbols(definition,[spl70_22])],[avatar_definition]) ).
fof(f812,plain,
( ~ spl70_17
| ~ spl70_22 ),
inference(avatar_split_clause,[],[f610,f809,f785]) ).
fof(f814,definition,
( spl70_23
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl70_23])],[avatar_definition]) ).
fof(f818,definition,
( spl70_24
<=> leq(sK67,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl70_24])],[avatar_definition]) ).
fof(f820,plain,
( leq(sK67,minus(n3,n1))
| ~ spl70_24 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f821,plain,
( ~ spl70_23
| spl70_24 ),
inference(avatar_split_clause,[],[f465,f818,f814]) ).
fof(f823,definition,
( spl70_25
<=> leq(n0,sK67) ),
introduced(definition,[new_symbols(definition,[spl70_25])],[avatar_definition]) ).
fof(f825,plain,
( leq(n0,sK67)
| ~ spl70_25 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f826,plain,
( ~ spl70_23
| spl70_25 ),
inference(avatar_split_clause,[],[f466,f823,f814]) ).
fof(f828,definition,
( spl70_26
<=> s_sworst7_init = a_select2(s_try7_init,sK67) ),
introduced(definition,[new_symbols(definition,[spl70_26])],[avatar_definition]) ).
fof(f831,plain,
( ~ spl70_23
| ~ spl70_26 ),
inference(avatar_split_clause,[],[f609,f828,f814]) ).
fof(f833,definition,
( spl70_27
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl70_27])],[avatar_definition]) ).
fof(f837,definition,
( spl70_28
<=> leq(sK66,n2) ),
introduced(definition,[new_symbols(definition,[spl70_28])],[avatar_definition]) ).
fof(f839,plain,
( leq(sK66,n2)
| ~ spl70_28 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f840,plain,
( ~ spl70_27
| spl70_28 ),
inference(avatar_split_clause,[],[f462,f837,f833]) ).
fof(f842,definition,
( spl70_29
<=> leq(n0,sK66) ),
introduced(definition,[new_symbols(definition,[spl70_29])],[avatar_definition]) ).
fof(f845,plain,
( ~ spl70_27
| spl70_29 ),
inference(avatar_split_clause,[],[f463,f842,f833]) ).
fof(f847,definition,
( spl70_30
<=> s_sworst7_init = a_select2(s_center7_init,sK66) ),
introduced(definition,[new_symbols(definition,[spl70_30])],[avatar_definition]) ).
fof(f849,plain,
( s_sworst7_init != a_select2(s_center7_init,sK66)
| spl70_30 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f850,plain,
( ~ spl70_27
| ~ spl70_30 ),
inference(avatar_split_clause,[],[f608,f847,f833]) ).
fof(f852,definition,
( spl70_31
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl70_31])],[avatar_definition]) ).
fof(f856,definition,
( spl70_32
<=> leq(sK64,n2) ),
introduced(definition,[new_symbols(definition,[spl70_32])],[avatar_definition]) ).
fof(f858,plain,
( leq(sK64,n2)
| ~ spl70_32 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f859,plain,
( ~ spl70_31
| spl70_32 ),
inference(avatar_split_clause,[],[f457,f856,f852]) ).
fof(f861,definition,
( spl70_33
<=> leq(n0,sK64) ),
introduced(definition,[new_symbols(definition,[spl70_33])],[avatar_definition]) ).
fof(f864,plain,
( ~ spl70_31
| spl70_33 ),
inference(avatar_split_clause,[],[f458,f861,f852]) ).
fof(f866,definition,
( spl70_34
<=> leq(sK65,n3) ),
introduced(definition,[new_symbols(definition,[spl70_34])],[avatar_definition]) ).
fof(f868,plain,
( leq(sK65,n3)
| ~ spl70_34 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f869,plain,
( ~ spl70_31
| spl70_34 ),
inference(avatar_split_clause,[],[f459,f866,f852]) ).
fof(f871,definition,
( spl70_35
<=> leq(n0,sK65) ),
introduced(definition,[new_symbols(definition,[spl70_35])],[avatar_definition]) ).
fof(f874,plain,
( ~ spl70_31
| spl70_35 ),
inference(avatar_split_clause,[],[f460,f871,f852]) ).
fof(f876,definition,
( spl70_36
<=> s_sworst7_init = a_select3(simplex7_init,sK65,sK64) ),
introduced(definition,[new_symbols(definition,[spl70_36])],[avatar_definition]) ).
fof(f879,plain,
( ~ spl70_31
| ~ spl70_36 ),
inference(avatar_split_clause,[],[f607,f876,f852]) ).
fof(f881,definition,
( spl70_37
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl70_37])],[avatar_definition]) ).
fof(f885,definition,
( spl70_38
<=> leq(sK63,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl70_38])],[avatar_definition]) ).
fof(f887,plain,
( leq(sK63,minus(n3,n1))
| ~ spl70_38 ),
inference(avatar_component_clause,[],[f885]) ).
fof(f888,plain,
( ~ spl70_37
| spl70_38 ),
inference(avatar_split_clause,[],[f454,f885,f881]) ).
fof(f890,definition,
( spl70_39
<=> leq(n0,sK63) ),
introduced(definition,[new_symbols(definition,[spl70_39])],[avatar_definition]) ).
fof(f892,plain,
( leq(n0,sK63)
| ~ spl70_39 ),
inference(avatar_component_clause,[],[f890]) ).
fof(f893,plain,
( ~ spl70_37
| spl70_39 ),
inference(avatar_split_clause,[],[f455,f890,f881]) ).
fof(f895,definition,
( spl70_40
<=> s_sworst7_init = a_select2(s_try7_init,sK63) ),
introduced(definition,[new_symbols(definition,[spl70_40])],[avatar_definition]) ).
fof(f898,plain,
( ~ spl70_37
| ~ spl70_40 ),
inference(avatar_split_clause,[],[f606,f895,f881]) ).
fof(f900,definition,
( spl70_41
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl70_41])],[avatar_definition]) ).
fof(f904,definition,
( spl70_42
<=> leq(sK62,n2) ),
introduced(definition,[new_symbols(definition,[spl70_42])],[avatar_definition]) ).
fof(f906,plain,
( leq(sK62,n2)
| ~ spl70_42 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f907,plain,
( ~ spl70_41
| spl70_42 ),
inference(avatar_split_clause,[],[f451,f904,f900]) ).
fof(f909,definition,
( spl70_43
<=> leq(n0,sK62) ),
introduced(definition,[new_symbols(definition,[spl70_43])],[avatar_definition]) ).
fof(f912,plain,
( ~ spl70_41
| spl70_43 ),
inference(avatar_split_clause,[],[f452,f909,f900]) ).
fof(f914,definition,
( spl70_44
<=> s_sworst7_init = a_select2(s_center7_init,sK62) ),
introduced(definition,[new_symbols(definition,[spl70_44])],[avatar_definition]) ).
fof(f917,plain,
( ~ spl70_41
| ~ spl70_44 ),
inference(avatar_split_clause,[],[f605,f914,f900]) ).
fof(f919,definition,
( spl70_45
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl70_45])],[avatar_definition]) ).
fof(f923,definition,
( spl70_46
<=> leq(sK60,n2) ),
introduced(definition,[new_symbols(definition,[spl70_46])],[avatar_definition]) ).
fof(f925,plain,
( leq(sK60,n2)
| ~ spl70_46 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( ~ spl70_45
| spl70_46 ),
inference(avatar_split_clause,[],[f446,f923,f919]) ).
fof(f928,definition,
( spl70_47
<=> leq(n0,sK60) ),
introduced(definition,[new_symbols(definition,[spl70_47])],[avatar_definition]) ).
fof(f931,plain,
( ~ spl70_45
| spl70_47 ),
inference(avatar_split_clause,[],[f447,f928,f919]) ).
fof(f933,definition,
( spl70_48
<=> leq(sK61,n3) ),
introduced(definition,[new_symbols(definition,[spl70_48])],[avatar_definition]) ).
fof(f935,plain,
( leq(sK61,n3)
| ~ spl70_48 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f936,plain,
( ~ spl70_45
| spl70_48 ),
inference(avatar_split_clause,[],[f448,f933,f919]) ).
fof(f938,definition,
( spl70_49
<=> leq(n0,sK61) ),
introduced(definition,[new_symbols(definition,[spl70_49])],[avatar_definition]) ).
fof(f941,plain,
( ~ spl70_45
| spl70_49 ),
inference(avatar_split_clause,[],[f449,f938,f919]) ).
fof(f943,definition,
( spl70_50
<=> s_sworst7_init = a_select3(simplex7_init,sK61,sK60) ),
introduced(definition,[new_symbols(definition,[spl70_50])],[avatar_definition]) ).
fof(f946,plain,
( ~ spl70_45
| ~ spl70_50 ),
inference(avatar_split_clause,[],[f604,f943,f919]) ).
fof(f948,definition,
( spl70_51
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl70_51])],[avatar_definition]) ).
fof(f952,definition,
( spl70_52
<=> leq(sK59,minus(n3,n1)) ),
introduced(definition,[new_symbols(definition,[spl70_52])],[avatar_definition]) ).
fof(f954,plain,
( leq(sK59,minus(n3,n1))
| ~ spl70_52 ),
inference(avatar_component_clause,[],[f952]) ).
fof(f955,plain,
( ~ spl70_51
| spl70_52 ),
inference(avatar_split_clause,[],[f443,f952,f948]) ).
fof(f957,definition,
( spl70_53
<=> leq(n0,sK59) ),
introduced(definition,[new_symbols(definition,[spl70_53])],[avatar_definition]) ).
fof(f959,plain,
( leq(n0,sK59)
| ~ spl70_53 ),
inference(avatar_component_clause,[],[f957]) ).
fof(f960,plain,
( ~ spl70_51
| spl70_53 ),
inference(avatar_split_clause,[],[f444,f957,f948]) ).
fof(f962,definition,
( spl70_54
<=> s_sworst7_init = a_select2(s_try7_init,sK59) ),
introduced(definition,[new_symbols(definition,[spl70_54])],[avatar_definition]) ).
fof(f965,plain,
( ~ spl70_51
| ~ spl70_54 ),
inference(avatar_split_clause,[],[f603,f962,f948]) ).
fof(f967,definition,
( spl70_55
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl70_55])],[avatar_definition]) ).
fof(f971,definition,
( spl70_56
<=> leq(sK58,n2) ),
introduced(definition,[new_symbols(definition,[spl70_56])],[avatar_definition]) ).
fof(f973,plain,
( leq(sK58,n2)
| ~ spl70_56 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f974,plain,
( ~ spl70_55
| spl70_56 ),
inference(avatar_split_clause,[],[f440,f971,f967]) ).
fof(f976,definition,
( spl70_57
<=> leq(n0,sK58) ),
introduced(definition,[new_symbols(definition,[spl70_57])],[avatar_definition]) ).
fof(f979,plain,
( ~ spl70_55
| spl70_57 ),
inference(avatar_split_clause,[],[f441,f976,f967]) ).
fof(f981,definition,
( spl70_58
<=> s_sworst7_init = a_select2(s_center7_init,sK58) ),
introduced(definition,[new_symbols(definition,[spl70_58])],[avatar_definition]) ).
fof(f984,plain,
( ~ spl70_55
| ~ spl70_58 ),
inference(avatar_split_clause,[],[f602,f981,f967]) ).
fof(f986,definition,
( spl70_59
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl70_59])],[avatar_definition]) ).
fof(f990,definition,
( spl70_60
<=> leq(sK56,n2) ),
introduced(definition,[new_symbols(definition,[spl70_60])],[avatar_definition]) ).
fof(f992,plain,
( leq(sK56,n2)
| ~ spl70_60 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f993,plain,
( ~ spl70_59
| spl70_60 ),
inference(avatar_split_clause,[],[f435,f990,f986]) ).
fof(f995,definition,
( spl70_61
<=> leq(n0,sK56) ),
introduced(definition,[new_symbols(definition,[spl70_61])],[avatar_definition]) ).
fof(f998,plain,
( ~ spl70_59
| spl70_61 ),
inference(avatar_split_clause,[],[f436,f995,f986]) ).
fof(f1000,definition,
( spl70_62
<=> leq(sK57,n3) ),
introduced(definition,[new_symbols(definition,[spl70_62])],[avatar_definition]) ).
fof(f1002,plain,
( leq(sK57,n3)
| ~ spl70_62 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1003,plain,
( ~ spl70_59
| spl70_62 ),
inference(avatar_split_clause,[],[f437,f1000,f986]) ).
fof(f1005,definition,
( spl70_63
<=> leq(n0,sK57) ),
introduced(definition,[new_symbols(definition,[spl70_63])],[avatar_definition]) ).
fof(f1007,plain,
( leq(n0,sK57)
| ~ spl70_63 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1008,plain,
( ~ spl70_59
| spl70_63 ),
inference(avatar_split_clause,[],[f438,f1005,f986]) ).
fof(f1010,definition,
( spl70_64
<=> s_sworst7_init = a_select3(simplex7_init,sK57,sK56) ),
introduced(definition,[new_symbols(definition,[spl70_64])],[avatar_definition]) ).
fof(f1012,plain,
( s_sworst7_init != a_select3(simplex7_init,sK57,sK56)
| spl70_64 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1013,plain,
( ~ spl70_59
| ~ spl70_64 ),
inference(avatar_split_clause,[],[f601,f1010,f986]) ).
fof(f1015,definition,
( spl70_65
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl70_65])],[avatar_definition]) ).
fof(f1019,definition,
( spl70_66
<=> leq(sK55,n3) ),
introduced(definition,[new_symbols(definition,[spl70_66])],[avatar_definition]) ).
fof(f1021,plain,
( leq(sK55,n3)
| ~ spl70_66 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1022,plain,
( ~ spl70_65
| spl70_66 ),
inference(avatar_split_clause,[],[f432,f1019,f1015]) ).
fof(f1024,definition,
( spl70_67
<=> leq(n0,sK55) ),
introduced(definition,[new_symbols(definition,[spl70_67])],[avatar_definition]) ).
fof(f1027,plain,
( ~ spl70_65
| spl70_67 ),
inference(avatar_split_clause,[],[f433,f1024,f1015]) ).
fof(f1029,definition,
( spl70_68
<=> s_sworst7_init = a_select2(s_values7_init,sK55) ),
introduced(definition,[new_symbols(definition,[spl70_68])],[avatar_definition]) ).
fof(f1032,plain,
( ~ spl70_65
| ~ spl70_68 ),
inference(avatar_split_clause,[],[f600,f1029,f1015]) ).
fof(f1044,definition,
( spl70_71
<=> leq(s_worst7,n3) ),
introduced(definition,[new_symbols(definition,[spl70_71])],[avatar_definition]) ).
fof(f1045,plain,
( leq(s_worst7,n3)
| ~ spl70_71 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1048,definition,
( spl70_72
<=> leq(s_sworst7,n3) ),
introduced(definition,[new_symbols(definition,[spl70_72])],[avatar_definition]) ).
fof(f1049,plain,
( leq(s_sworst7,n3)
| ~ spl70_72 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1052,definition,
( spl70_73
<=> leq(s_best7,n3) ),
introduced(definition,[new_symbols(definition,[spl70_73])],[avatar_definition]) ).
fof(f1053,plain,
( leq(s_best7,n3)
| ~ spl70_73 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1056,definition,
( spl70_74
<=> leq(n0,s_worst7) ),
introduced(definition,[new_symbols(definition,[spl70_74])],[avatar_definition]) ).
fof(f1057,plain,
( leq(n0,s_worst7)
| ~ spl70_74 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1060,definition,
( spl70_75
<=> leq(n0,s_sworst7) ),
introduced(definition,[new_symbols(definition,[spl70_75])],[avatar_definition]) ).
fof(f1061,plain,
( leq(n0,s_sworst7)
| ~ spl70_75 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1064,definition,
( spl70_76
<=> leq(n0,s_best7) ),
introduced(definition,[new_symbols(definition,[spl70_76])],[avatar_definition]) ).
fof(f1065,plain,
( leq(n0,s_best7)
| ~ spl70_76 ),
inference(avatar_component_clause,[],[f1064]) ).
fof(f1072,plain,
( ~ spl70_15
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_65
| spl70_59
| ~ spl70_7
| ~ spl70_14
| ~ spl70_11
| ~ spl70_8
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4 ),
inference(avatar_split_clause,[],[f661,f726,f721,f716,f743,f756,f769,f739,f986,f1015,f1064,f1060,f1056,f1052,f1048,f1044,f774]) ).
fof(f1074,definition,
( spl70_77
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl70_77])],[avatar_definition]) ).
fof(f1078,definition,
( spl70_78
<=> leq(sK53,n2) ),
introduced(definition,[new_symbols(definition,[spl70_78])],[avatar_definition]) ).
fof(f1080,plain,
( leq(sK53,n2)
| ~ spl70_78 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1081,plain,
( ~ spl70_77
| spl70_78 ),
inference(avatar_split_clause,[],[f419,f1078,f1074]) ).
fof(f1083,definition,
( spl70_79
<=> leq(n0,sK53) ),
introduced(definition,[new_symbols(definition,[spl70_79])],[avatar_definition]) ).
fof(f1086,plain,
( ~ spl70_77
| spl70_79 ),
inference(avatar_split_clause,[],[f420,f1083,f1074]) ).
fof(f1088,definition,
( spl70_80
<=> leq(sK54,n3) ),
introduced(definition,[new_symbols(definition,[spl70_80])],[avatar_definition]) ).
fof(f1090,plain,
( leq(sK54,n3)
| ~ spl70_80 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1091,plain,
( ~ spl70_77
| spl70_80 ),
inference(avatar_split_clause,[],[f421,f1088,f1074]) ).
fof(f1093,definition,
( spl70_81
<=> leq(n0,sK54) ),
introduced(definition,[new_symbols(definition,[spl70_81])],[avatar_definition]) ).
fof(f1096,plain,
( ~ spl70_77
| spl70_81 ),
inference(avatar_split_clause,[],[f422,f1093,f1074]) ).
fof(f1098,definition,
( spl70_82
<=> s_sworst7_init = a_select3(simplex7_init,sK54,sK53) ),
introduced(definition,[new_symbols(definition,[spl70_82])],[avatar_definition]) ).
fof(f1101,plain,
( ~ spl70_77
| ~ spl70_82 ),
inference(avatar_split_clause,[],[f591,f1098,f1074]) ).
fof(f1103,definition,
( spl70_83
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl70_83])],[avatar_definition]) ).
fof(f1107,definition,
( spl70_84
<=> leq(sK52,n3) ),
introduced(definition,[new_symbols(definition,[spl70_84])],[avatar_definition]) ).
fof(f1109,plain,
( leq(sK52,n3)
| ~ spl70_84 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1110,plain,
( ~ spl70_83
| spl70_84 ),
inference(avatar_split_clause,[],[f416,f1107,f1103]) ).
fof(f1112,definition,
( spl70_85
<=> leq(n0,sK52) ),
introduced(definition,[new_symbols(definition,[spl70_85])],[avatar_definition]) ).
fof(f1115,plain,
( ~ spl70_83
| spl70_85 ),
inference(avatar_split_clause,[],[f417,f1112,f1103]) ).
fof(f1117,definition,
( spl70_86
<=> s_sworst7_init = a_select2(s_values7_init,sK52) ),
introduced(definition,[new_symbols(definition,[spl70_86])],[avatar_definition]) ).
fof(f1120,plain,
( ~ spl70_83
| ~ spl70_86 ),
inference(avatar_split_clause,[],[f590,f1117,f1103]) ).
fof(f1132,plain,
( ~ spl70_16
| ~ spl70_7
| ~ spl70_14
| ~ spl70_11
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8
| spl70_83
| spl70_77 ),
inference(avatar_split_clause,[],[f674,f1074,f1103,f743,f1064,f1060,f1056,f1052,f1048,f1044,f756,f769,f739,f779]) ).
fof(f1135,definition,
( spl70_88
<=> leq(sK51,n3) ),
introduced(definition,[new_symbols(definition,[spl70_88])],[avatar_definition]) ).
fof(f1137,plain,
( leq(sK51,n3)
| ~ spl70_88 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1138,plain,
( ~ spl70_12
| spl70_1
| spl70_51
| spl70_55
| spl70_88
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f676,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1135,f967,f948,f712,f761]) ).
fof(f1139,plain,
( ~ spl70_12
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_51
| spl70_55
| spl70_88
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f678,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1135,f967,f948,f726,f721,f716,f761]) ).
fof(f1141,definition,
( spl70_89
<=> leq(n0,sK51) ),
introduced(definition,[new_symbols(definition,[spl70_89])],[avatar_definition]) ).
fof(f1144,plain,
( ~ spl70_12
| spl70_1
| spl70_51
| spl70_55
| spl70_89
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f680,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1141,f967,f948,f712,f761]) ).
fof(f1145,plain,
( ~ spl70_12
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_51
| spl70_55
| spl70_89
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f682,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1141,f967,f948,f726,f721,f716,f761]) ).
fof(f1147,definition,
( spl70_90
<=> s_sworst7_init = a_select2(s_values7_init,sK51) ),
introduced(definition,[new_symbols(definition,[spl70_90])],[avatar_definition]) ).
fof(f1150,plain,
( ~ spl70_12
| spl70_1
| spl70_51
| spl70_55
| ~ spl70_90
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f684,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1147,f967,f948,f712,f761]) ).
fof(f1151,plain,
( ~ spl70_12
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_51
| spl70_55
| ~ spl70_90
| spl70_45
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_7
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f686,f743,f739,f1064,f1060,f1056,f1052,f1048,f1044,f919,f1147,f967,f948,f726,f721,f716,f761]) ).
fof(f1154,definition,
( spl70_91
<=> leq(sK50,n3) ),
introduced(definition,[new_symbols(definition,[spl70_91])],[avatar_definition]) ).
fof(f1156,plain,
( leq(sK50,n3)
| ~ spl70_91 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1157,plain,
( ~ spl70_9
| spl70_1
| spl70_37
| spl70_41
| spl70_91
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f688,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1154,f900,f881,f712,f748]) ).
fof(f1158,plain,
( ~ spl70_9
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_37
| spl70_41
| spl70_91
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f690,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1154,f900,f881,f726,f721,f716,f748]) ).
fof(f1160,definition,
( spl70_92
<=> leq(n0,sK50) ),
introduced(definition,[new_symbols(definition,[spl70_92])],[avatar_definition]) ).
fof(f1163,plain,
( ~ spl70_9
| spl70_1
| spl70_37
| spl70_41
| spl70_92
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f692,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1160,f900,f881,f712,f748]) ).
fof(f1164,plain,
( ~ spl70_9
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_37
| spl70_41
| spl70_92
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f694,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1160,f900,f881,f726,f721,f716,f748]) ).
fof(f1166,definition,
( spl70_93
<=> s_sworst7_init = a_select2(s_values7_init,sK50) ),
introduced(definition,[new_symbols(definition,[spl70_93])],[avatar_definition]) ).
fof(f1169,plain,
( ~ spl70_9
| spl70_1
| spl70_37
| spl70_41
| ~ spl70_93
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f696,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1166,f900,f881,f712,f748]) ).
fof(f1170,plain,
( ~ spl70_9
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_37
| spl70_41
| ~ spl70_93
| spl70_31
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f698,f743,f1064,f1060,f1056,f1052,f1048,f1044,f852,f1166,f900,f881,f726,f721,f716,f748]) ).
fof(f1173,definition,
( spl70_94
<=> leq(sK49,n3) ),
introduced(definition,[new_symbols(definition,[spl70_94])],[avatar_definition]) ).
fof(f1175,plain,
( leq(sK49,n3)
| ~ spl70_94 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1176,plain,
( ~ spl70_5
| spl70_1
| spl70_23
| spl70_27
| spl70_94
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f700,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1173,f833,f814,f712,f731]) ).
fof(f1177,plain,
( ~ spl70_5
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_23
| spl70_27
| spl70_94
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f702,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1173,f833,f814,f726,f721,f716,f731]) ).
fof(f1179,definition,
( spl70_95
<=> leq(n0,sK49) ),
introduced(definition,[new_symbols(definition,[spl70_95])],[avatar_definition]) ).
fof(f1182,plain,
( ~ spl70_5
| spl70_1
| spl70_23
| spl70_27
| spl70_95
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f704,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1179,f833,f814,f712,f731]) ).
fof(f1183,plain,
( ~ spl70_5
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_23
| spl70_27
| spl70_95
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f706,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1179,f833,f814,f726,f721,f716,f731]) ).
fof(f1185,definition,
( spl70_96
<=> s_sworst7_init = a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49) ),
introduced(definition,[new_symbols(definition,[spl70_96])],[avatar_definition]) ).
fof(f1187,plain,
( s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),sK49)
| spl70_96 ),
inference(avatar_component_clause,[],[f1185]) ).
fof(f1188,plain,
( ~ spl70_5
| spl70_1
| spl70_23
| spl70_27
| ~ spl70_96
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f708,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1185,f833,f814,f712,f731]) ).
fof(f1189,plain,
( ~ spl70_5
| ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| spl70_23
| spl70_27
| ~ spl70_96
| spl70_17
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_8 ),
inference(avatar_split_clause,[],[f710,f743,f1064,f1060,f1056,f1052,f1048,f1044,f785,f1185,f833,f814,f726,f721,f716,f731]) ).
fof(f1190,plain,
spl70_71,
inference(avatar_split_clause,[],[f480,f1044]) ).
fof(f1191,plain,
spl70_72,
inference(avatar_split_clause,[],[f481,f1048]) ).
fof(f1192,plain,
spl70_73,
inference(avatar_split_clause,[],[f482,f1052]) ).
fof(f1193,plain,
spl70_74,
inference(avatar_split_clause,[],[f483,f1056]) ).
fof(f1194,plain,
spl70_75,
inference(avatar_split_clause,[],[f484,f1060]) ).
fof(f1195,plain,
spl70_76,
inference(avatar_split_clause,[],[f485,f1064]) ).
fof(f1196,plain,
spl70_8,
inference(avatar_split_clause,[],[f618,f743]) ).
fof(f1197,plain,
( ~ leq(n0,s_worst7)
| s_sworst7_init = a_select2(s_values7_init,s_worst7)
| ~ spl70_71 ),
inference(resolution,[],[f620,f1045]) ).
fof(f1198,plain,
( ~ leq(n0,s_sworst7)
| s_sworst7_init = a_select2(s_values7_init,s_sworst7)
| ~ spl70_72 ),
inference(resolution,[],[f620,f1049]) ).
fof(f1199,plain,
( ~ leq(n0,s_best7)
| s_sworst7_init = a_select2(s_values7_init,s_best7)
| ~ spl70_73 ),
inference(resolution,[],[f620,f1053]) ).
fof(f1200,plain,
( s_sworst7_init = a_select2(s_values7_init,s_best7)
| ~ spl70_73
| ~ spl70_76 ),
inference(forward_subsumption_resolution,[],[f1199,f1065]) ).
fof(f1201,plain,
( s_sworst7_init = a_select2(s_values7_init,s_sworst7)
| ~ spl70_72
| ~ spl70_75 ),
inference(forward_subsumption_resolution,[],[f1198,f1061]) ).
fof(f1202,plain,
( s_sworst7_init = a_select2(s_values7_init,s_worst7)
| ~ spl70_71
| ~ spl70_74 ),
inference(forward_subsumption_resolution,[],[f1197,f1057]) ).
fof(f1209,plain,
( spl70_14
| ~ spl70_72
| ~ spl70_75 ),
inference(avatar_split_clause,[],[f1201,f1060,f1048,f769]) ).
fof(f1210,plain,
( spl70_11
| ~ spl70_73
| ~ spl70_76 ),
inference(avatar_split_clause,[],[f1200,f1064,f1052,f756]) ).
fof(f1211,plain,
( spl70_7
| ~ spl70_71
| ~ spl70_74 ),
inference(avatar_split_clause,[],[f1202,f1056,f1044,f739]) ).
fof(f1218,definition,
( spl70_97
<=> s_sworst7_init = a_select2(s_values7_init,sK49) ),
introduced(definition,[new_symbols(definition,[spl70_97])],[avatar_definition]) ).
fof(f1220,plain,
( s_sworst7_init = a_select2(s_values7_init,sK49)
| ~ spl70_97 ),
inference(avatar_component_clause,[],[f1218]) ).
fof(f1305,definition,
( spl70_106
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK68)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl70_106])],[avatar_definition]) ).
fof(f1306,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK68)
| ~ leq(n0,X0) )
| ~ spl70_106 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1327,plain,
( ~ leq(n0,sK66)
| s_sworst7_init = a_select2(s_center7_init,sK66)
| ~ spl70_28 ),
inference(resolution,[],[f839,f621]) ).
fof(f1328,plain,
( ~ leq(n0,sK66)
| ~ spl70_28
| spl70_30 ),
inference(forward_subsumption_resolution,[],[f1327,f849]) ).
fof(f1333,plain,
( ~ spl70_29
| ~ spl70_28
| spl70_30 ),
inference(avatar_split_clause,[],[f1328,f847,f837,f842]) ).
fof(f1334,plain,
( ~ leq(n0,sK52)
| s_sworst7_init = a_select2(s_values7_init,sK52)
| ~ spl70_84 ),
inference(resolution,[],[f1109,f620]) ).
fof(f1337,plain,
( spl70_86
| ~ spl70_85
| ~ spl70_84 ),
inference(avatar_split_clause,[],[f1334,f1107,f1112,f1117]) ).
fof(f1338,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK53)
| s_sworst7_init = a_select3(simplex7_init,X0,sK53) )
| ~ spl70_78 ),
inference(resolution,[],[f1080,f619]) ).
fof(f1346,definition,
( spl70_112
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK53)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl70_112])],[avatar_definition]) ).
fof(f1347,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK53)
| ~ leq(n0,X0) )
| ~ spl70_112 ),
inference(avatar_component_clause,[],[f1346]) ).
fof(f1348,plain,
( ~ spl70_79
| spl70_112
| ~ spl70_78 ),
inference(avatar_split_clause,[],[f1338,f1078,f1346,f1083]) ).
fof(f1358,plain,
( s_sworst7_init = a_select3(simplex7_init,sK54,sK53)
| ~ leq(n0,sK54)
| ~ spl70_80
| ~ spl70_112 ),
inference(resolution,[],[f1347,f1090]) ).
fof(f1369,plain,
( ~ leq(n0,sK58)
| s_sworst7_init = a_select2(s_center7_init,sK58)
| ~ spl70_56 ),
inference(resolution,[],[f973,f621]) ).
fof(f1380,plain,
( spl70_58
| ~ spl70_57
| ~ spl70_56 ),
inference(avatar_split_clause,[],[f1369,f971,f976,f981]) ).
fof(f1383,plain,
( ~ leq(n0,sK59)
| s_sworst7_init = a_select2(s_try7_init,sK59)
| ~ spl70_52 ),
inference(resolution,[],[f954,f622]) ).
fof(f1384,plain,
( s_sworst7_init = a_select2(s_try7_init,sK59)
| ~ spl70_52
| ~ spl70_53 ),
inference(forward_subsumption_resolution,[],[f1383,f959]) ).
fof(f1391,plain,
( spl70_54
| ~ spl70_52
| ~ spl70_53 ),
inference(avatar_split_clause,[],[f1384,f957,f952,f962]) ).
fof(f1392,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK60)
| s_sworst7_init = a_select3(simplex7_init,X0,sK60) )
| ~ spl70_46 ),
inference(resolution,[],[f925,f619]) ).
fof(f1400,definition,
( spl70_116
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK60)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl70_116])],[avatar_definition]) ).
fof(f1401,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK60)
| ~ leq(n0,X0) )
| ~ spl70_116 ),
inference(avatar_component_clause,[],[f1400]) ).
fof(f1402,plain,
( ~ spl70_47
| spl70_116
| ~ spl70_46 ),
inference(avatar_split_clause,[],[f1392,f923,f1400,f928]) ).
fof(f1412,plain,
( s_sworst7_init = a_select3(simplex7_init,sK61,sK60)
| ~ leq(n0,sK61)
| ~ spl70_48
| ~ spl70_116 ),
inference(resolution,[],[f1401,f935]) ).
fof(f1425,plain,
( ~ leq(n0,sK62)
| s_sworst7_init = a_select2(s_center7_init,sK62)
| ~ spl70_42 ),
inference(resolution,[],[f906,f621]) ).
fof(f1439,plain,
( spl70_44
| ~ spl70_43
| ~ spl70_42 ),
inference(avatar_split_clause,[],[f1425,f904,f909,f914]) ).
fof(f1440,plain,
( ~ leq(n0,sK63)
| s_sworst7_init = a_select2(s_try7_init,sK63)
| ~ spl70_38 ),
inference(resolution,[],[f887,f622]) ).
fof(f1441,plain,
( s_sworst7_init = a_select2(s_try7_init,sK63)
| ~ spl70_38
| ~ spl70_39 ),
inference(forward_subsumption_resolution,[],[f1440,f892]) ).
fof(f1451,plain,
( spl70_40
| ~ spl70_38
| ~ spl70_39 ),
inference(avatar_split_clause,[],[f1441,f890,f885,f895]) ).
fof(f1452,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK64)
| s_sworst7_init = a_select3(simplex7_init,X0,sK64) )
| ~ spl70_32 ),
inference(resolution,[],[f858,f619]) ).
fof(f1460,definition,
( spl70_120
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK64)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl70_120])],[avatar_definition]) ).
fof(f1461,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK64)
| ~ leq(n0,X0) )
| ~ spl70_120 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1462,plain,
( ~ spl70_33
| spl70_120
| ~ spl70_32 ),
inference(avatar_split_clause,[],[f1452,f856,f1460,f861]) ).
fof(f1472,plain,
( s_sworst7_init = a_select3(simplex7_init,sK65,sK64)
| ~ leq(n0,sK65)
| ~ spl70_34
| ~ spl70_120 ),
inference(resolution,[],[f1461,f868]) ).
fof(f2082,plain,
( s_sworst7_init != a_select2(s_values7_init,sK49)
| s_worst7 = sK49
| spl70_96 ),
inference(superposition,[],[f1187,f633]) ).
fof(f2083,plain,
( s_worst7 = sK49
| spl70_96
| ~ spl70_97 ),
inference(forward_subsumption_resolution,[],[f2082,f1220]) ).
fof(f2086,plain,
( s_sworst7_init != a_select2(tptp_update2(s_values7_init,s_worst7,s_sworst7_init),s_worst7)
| spl70_96
| ~ spl70_97 ),
inference(superposition,[],[f1187,f2083]) ).
fof(f2093,plain,
( $false
| spl70_96
| ~ spl70_97 ),
inference(forward_subsumption_resolution,[],[f2086,f381]) ).
fof(f2094,plain,
( spl70_96
| ~ spl70_97 ),
inference(avatar_contradiction_clause,[],[f2093]) ).
fof(f2137,plain,
( ~ leq(n0,sK67)
| s_sworst7_init = a_select2(s_try7_init,sK67)
| ~ spl70_24 ),
inference(resolution,[],[f820,f622]) ).
fof(f2140,plain,
( s_sworst7_init = a_select2(s_try7_init,sK67)
| ~ spl70_24
| ~ spl70_25 ),
inference(forward_subsumption_resolution,[],[f2137,f825]) ).
fof(f2163,plain,
( spl70_26
| ~ spl70_24
| ~ spl70_25 ),
inference(avatar_split_clause,[],[f2140,f823,f818,f828]) ).
fof(f2169,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK68)
| s_sworst7_init = a_select3(simplex7_init,X0,sK68) )
| ~ spl70_18 ),
inference(resolution,[],[f791,f619]) ).
fof(f2172,plain,
( ~ spl70_19
| spl70_106
| ~ spl70_18 ),
inference(avatar_split_clause,[],[f2169,f789,f1305,f794]) ).
fof(f8258,plain,
( s_sworst7_init = a_select3(simplex7_init,sK69,sK68)
| ~ leq(n0,sK69)
| ~ spl70_20
| ~ spl70_106 ),
inference(resolution,[],[f1306,f801]) ).
fof(f8733,plain,
( ! [X0] :
( ~ leq(n0,X0)
| ~ leq(X0,n3)
| ~ leq(n0,sK56)
| s_sworst7_init = a_select3(simplex7_init,X0,sK56) )
| ~ spl70_60 ),
inference(resolution,[],[f992,f619]) ).
fof(f8934,definition,
( spl70_308
<=> ! [X0] :
( ~ leq(n0,X0)
| s_sworst7_init = a_select3(simplex7_init,X0,sK56)
| ~ leq(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl70_308])],[avatar_definition]) ).
fof(f8935,plain,
( ! [X0] :
( ~ leq(X0,n3)
| s_sworst7_init = a_select3(simplex7_init,X0,sK56)
| ~ leq(n0,X0) )
| ~ spl70_308 ),
inference(avatar_component_clause,[],[f8934]) ).
fof(f8936,plain,
( ~ spl70_61
| spl70_308
| ~ spl70_60 ),
inference(avatar_split_clause,[],[f8733,f990,f8934,f995]) ).
fof(f8954,plain,
( ~ spl70_35
| spl70_36
| ~ spl70_34
| ~ spl70_120 ),
inference(avatar_split_clause,[],[f1472,f1460,f866,f876,f871]) ).
fof(f8956,plain,
( ~ spl70_49
| spl70_50
| ~ spl70_48
| ~ spl70_116 ),
inference(avatar_split_clause,[],[f1412,f1400,f933,f943,f938]) ).
fof(f9286,plain,
( ~ leq(n0,sK51)
| s_sworst7_init = a_select2(s_values7_init,sK51)
| ~ spl70_88 ),
inference(resolution,[],[f1137,f620]) ).
fof(f9480,plain,
( spl70_90
| ~ spl70_89
| ~ spl70_88 ),
inference(avatar_split_clause,[],[f9286,f1135,f1141,f1147]) ).
fof(f9586,plain,
( ~ leq(n0,sK50)
| s_sworst7_init = a_select2(s_values7_init,sK50)
| ~ spl70_91 ),
inference(resolution,[],[f1156,f620]) ).
fof(f9780,plain,
( spl70_93
| ~ spl70_92
| ~ spl70_91 ),
inference(avatar_split_clause,[],[f9586,f1154,f1160,f1166]) ).
fof(f9886,plain,
( ~ leq(n0,sK49)
| s_sworst7_init = a_select2(s_values7_init,sK49)
| ~ spl70_94 ),
inference(resolution,[],[f1175,f620]) ).
fof(f10080,plain,
( spl70_97
| ~ spl70_95
| ~ spl70_94 ),
inference(avatar_split_clause,[],[f9886,f1173,f1179,f1218]) ).
fof(f10322,plain,
( ~ leq(n0,sK55)
| s_sworst7_init = a_select2(s_values7_init,sK55)
| ~ spl70_66 ),
inference(resolution,[],[f1021,f620]) ).
fof(f10550,plain,
( ~ spl70_21
| spl70_22
| ~ spl70_20
| ~ spl70_106 ),
inference(avatar_split_clause,[],[f8258,f1305,f799,f809,f804]) ).
fof(f10555,plain,
( ~ spl70_81
| spl70_82
| ~ spl70_80
| ~ spl70_112 ),
inference(avatar_split_clause,[],[f1358,f1346,f1088,f1098,f1093]) ).
fof(f10670,plain,
( spl70_68
| ~ spl70_67
| ~ spl70_66 ),
inference(avatar_split_clause,[],[f10322,f1019,f1024,f1029]) ).
fof(f11779,plain,
( s_sworst7_init = a_select3(simplex7_init,sK57,sK56)
| ~ leq(n0,sK57)
| ~ spl70_62
| ~ spl70_308 ),
inference(resolution,[],[f8935,f1002]) ).
fof(f11800,plain,
( ~ leq(n0,sK57)
| ~ spl70_62
| spl70_64
| ~ spl70_308 ),
inference(forward_subsumption_resolution,[],[f11779,f1012]) ).
fof(f11809,plain,
( $false
| ~ spl70_62
| ~ spl70_63
| spl70_64
| ~ spl70_308 ),
inference(forward_subsumption_resolution,[],[f11800,f1007]) ).
fof(f11810,plain,
( ~ spl70_62
| ~ spl70_63
| spl70_64
| ~ spl70_308 ),
inference(avatar_contradiction_clause,[],[f11809]) ).
cnf(s1,plain,
( ~ spl70_1
| spl70_2 ),
inference(sat_conversion,[],[f719]) ).
cnf(s2,plain,
( ~ spl70_1
| spl70_3 ),
inference(sat_conversion,[],[f724]) ).
cnf(s3,plain,
( ~ spl70_1
| spl70_4 ),
inference(sat_conversion,[],[f729]) ).
cnf(s8,plain,
( spl70_1
| spl70_5
| ~ spl70_7
| ~ spl70_8
| spl70_9
| ~ spl70_11
| spl70_12
| ~ spl70_14
| spl70_16 ),
inference(sat_conversion,[],[f782]) ).
cnf(s9,plain,
( spl70_5
| ~ spl70_7
| ~ spl70_8
| spl70_9
| ~ spl70_11
| spl70_12
| ~ spl70_14
| spl70_15
| spl70_16 ),
inference(sat_conversion,[],[f783]) ).
cnf(s10,plain,
( ~ spl70_17
| spl70_18 ),
inference(sat_conversion,[],[f792]) ).
cnf(s11,plain,
( ~ spl70_17
| spl70_19 ),
inference(sat_conversion,[],[f797]) ).
cnf(s12,plain,
( ~ spl70_17
| spl70_20 ),
inference(sat_conversion,[],[f802]) ).
cnf(s13,plain,
( ~ spl70_17
| spl70_21 ),
inference(sat_conversion,[],[f807]) ).
cnf(s14,plain,
( ~ spl70_17
| ~ spl70_22 ),
inference(sat_conversion,[],[f812]) ).
cnf(s15,plain,
( ~ spl70_23
| spl70_24 ),
inference(sat_conversion,[],[f821]) ).
cnf(s16,plain,
( ~ spl70_23
| spl70_25 ),
inference(sat_conversion,[],[f826]) ).
cnf(s17,plain,
( ~ spl70_23
| ~ spl70_26 ),
inference(sat_conversion,[],[f831]) ).
cnf(s18,plain,
( ~ spl70_27
| spl70_28 ),
inference(sat_conversion,[],[f840]) ).
cnf(s19,plain,
( ~ spl70_27
| spl70_29 ),
inference(sat_conversion,[],[f845]) ).
cnf(s20,plain,
( ~ spl70_27
| ~ spl70_30 ),
inference(sat_conversion,[],[f850]) ).
cnf(s21,plain,
( ~ spl70_31
| spl70_32 ),
inference(sat_conversion,[],[f859]) ).
cnf(s22,plain,
( ~ spl70_31
| spl70_33 ),
inference(sat_conversion,[],[f864]) ).
cnf(s23,plain,
( ~ spl70_31
| spl70_34 ),
inference(sat_conversion,[],[f869]) ).
cnf(s24,plain,
( ~ spl70_31
| spl70_35 ),
inference(sat_conversion,[],[f874]) ).
cnf(s25,plain,
( ~ spl70_31
| ~ spl70_36 ),
inference(sat_conversion,[],[f879]) ).
cnf(s26,plain,
( ~ spl70_37
| spl70_38 ),
inference(sat_conversion,[],[f888]) ).
cnf(s27,plain,
( ~ spl70_37
| spl70_39 ),
inference(sat_conversion,[],[f893]) ).
cnf(s28,plain,
( ~ spl70_37
| ~ spl70_40 ),
inference(sat_conversion,[],[f898]) ).
cnf(s29,plain,
( ~ spl70_41
| spl70_42 ),
inference(sat_conversion,[],[f907]) ).
cnf(s30,plain,
( ~ spl70_41
| spl70_43 ),
inference(sat_conversion,[],[f912]) ).
cnf(s31,plain,
( ~ spl70_41
| ~ spl70_44 ),
inference(sat_conversion,[],[f917]) ).
cnf(s32,plain,
( ~ spl70_45
| spl70_46 ),
inference(sat_conversion,[],[f926]) ).
cnf(s33,plain,
( ~ spl70_45
| spl70_47 ),
inference(sat_conversion,[],[f931]) ).
cnf(s34,plain,
( ~ spl70_45
| spl70_48 ),
inference(sat_conversion,[],[f936]) ).
cnf(s35,plain,
( ~ spl70_45
| spl70_49 ),
inference(sat_conversion,[],[f941]) ).
cnf(s36,plain,
( ~ spl70_45
| ~ spl70_50 ),
inference(sat_conversion,[],[f946]) ).
cnf(s37,plain,
( ~ spl70_51
| spl70_52 ),
inference(sat_conversion,[],[f955]) ).
cnf(s38,plain,
( ~ spl70_51
| spl70_53 ),
inference(sat_conversion,[],[f960]) ).
cnf(s39,plain,
( ~ spl70_51
| ~ spl70_54 ),
inference(sat_conversion,[],[f965]) ).
cnf(s40,plain,
( ~ spl70_55
| spl70_56 ),
inference(sat_conversion,[],[f974]) ).
cnf(s41,plain,
( ~ spl70_55
| spl70_57 ),
inference(sat_conversion,[],[f979]) ).
cnf(s42,plain,
( ~ spl70_55
| ~ spl70_58 ),
inference(sat_conversion,[],[f984]) ).
cnf(s43,plain,
( ~ spl70_59
| spl70_60 ),
inference(sat_conversion,[],[f993]) ).
cnf(s44,plain,
( ~ spl70_59
| spl70_61 ),
inference(sat_conversion,[],[f998]) ).
cnf(s45,plain,
( ~ spl70_59
| spl70_62 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s46,plain,
( ~ spl70_59
| spl70_63 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s47,plain,
( ~ spl70_59
| ~ spl70_64 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s48,plain,
( ~ spl70_65
| spl70_66 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s49,plain,
( ~ spl70_65
| spl70_67 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s50,plain,
( ~ spl70_65
| ~ spl70_68 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s58,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_7
| ~ spl70_8
| ~ spl70_11
| ~ spl70_14
| ~ spl70_15
| spl70_59
| spl70_65
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s59,plain,
( ~ spl70_77
| spl70_78 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s60,plain,
( ~ spl70_77
| spl70_79 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s61,plain,
( ~ spl70_77
| spl70_80 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s62,plain,
( ~ spl70_77
| spl70_81 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s63,plain,
( ~ spl70_77
| ~ spl70_82 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s64,plain,
( ~ spl70_83
| spl70_84 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s65,plain,
( ~ spl70_83
| spl70_85 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s66,plain,
( ~ spl70_83
| ~ spl70_86 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s74,plain,
( ~ spl70_7
| ~ spl70_8
| ~ spl70_11
| ~ spl70_14
| ~ spl70_16
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_77
| spl70_83 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s76,plain,
( spl70_1
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_88 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s77,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_88 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s78,plain,
( spl70_1
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_89 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s79,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_89 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s80,plain,
( spl70_1
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_90 ),
inference(sat_conversion,[],[f1150]) ).
cnf(s81,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_7
| ~ spl70_8
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_90 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s83,plain,
( spl70_1
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_91 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s84,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_91 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s85,plain,
( spl70_1
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_92 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s86,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_92 ),
inference(sat_conversion,[],[f1164]) ).
cnf(s87,plain,
( spl70_1
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_93 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s88,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_8
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_93 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s90,plain,
( spl70_1
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_94 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s91,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_94 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s92,plain,
( spl70_1
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_95 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s93,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| spl70_95 ),
inference(sat_conversion,[],[f1183]) ).
cnf(s94,plain,
( spl70_1
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_96 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s95,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| ~ spl70_8
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_71
| ~ spl70_72
| ~ spl70_73
| ~ spl70_74
| ~ spl70_75
| ~ spl70_76
| ~ spl70_96 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s96,plain,
spl70_71,
inference(sat_conversion,[],[f1190]) ).
cnf(s97,plain,
spl70_72,
inference(sat_conversion,[],[f1191]) ).
cnf(s98,plain,
spl70_73,
inference(sat_conversion,[],[f1192]) ).
cnf(s99,plain,
spl70_74,
inference(sat_conversion,[],[f1193]) ).
cnf(s100,plain,
spl70_75,
inference(sat_conversion,[],[f1194]) ).
cnf(s101,plain,
spl70_76,
inference(sat_conversion,[],[f1195]) ).
cnf(s102,plain,
spl70_8,
inference(sat_conversion,[],[f1196]) ).
cnf(s106,plain,
( spl70_14
| ~ spl70_72
| ~ spl70_75 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s107,plain,
( spl70_11
| ~ spl70_73
| ~ spl70_76 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s108,plain,
( spl70_7
| ~ spl70_71
| ~ spl70_74 ),
inference(sat_conversion,[],[f1211]) ).
cnf(s122,plain,
( ~ spl70_28
| ~ spl70_29
| spl70_30 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s124,plain,
( ~ spl70_84
| ~ spl70_85
| spl70_86 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s126,plain,
( ~ spl70_78
| ~ spl70_79
| spl70_112 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s134,plain,
( ~ spl70_56
| ~ spl70_57
| spl70_58 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s138,plain,
( ~ spl70_52
| ~ spl70_53
| spl70_54 ),
inference(sat_conversion,[],[f1391]) ).
cnf(s140,plain,
( ~ spl70_46
| ~ spl70_47
| spl70_116 ),
inference(sat_conversion,[],[f1402]) ).
cnf(s151,plain,
( ~ spl70_42
| ~ spl70_43
| spl70_44 ),
inference(sat_conversion,[],[f1439]) ).
cnf(s156,plain,
( ~ spl70_38
| ~ spl70_39
| spl70_40 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s158,plain,
( ~ spl70_32
| ~ spl70_33
| spl70_120 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s180,plain,
( spl70_96
| ~ spl70_97 ),
inference(sat_conversion,[],[f2094]) ).
cnf(s195,plain,
( ~ spl70_24
| ~ spl70_25
| spl70_26 ),
inference(sat_conversion,[],[f2163]) ).
cnf(s199,plain,
( ~ spl70_18
| ~ spl70_19
| spl70_106 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s379,plain,
( ~ spl70_60
| ~ spl70_61
| spl70_308 ),
inference(sat_conversion,[],[f8936]) ).
cnf(s386,plain,
( ~ spl70_34
| ~ spl70_35
| spl70_36
| ~ spl70_120 ),
inference(sat_conversion,[],[f8954]) ).
cnf(s388,plain,
( ~ spl70_48
| ~ spl70_49
| spl70_50
| ~ spl70_116 ),
inference(sat_conversion,[],[f8956]) ).
cnf(s455,plain,
( ~ spl70_88
| ~ spl70_89
| spl70_90 ),
inference(sat_conversion,[],[f9480]) ).
cnf(s497,plain,
( ~ spl70_91
| ~ spl70_92
| spl70_93 ),
inference(sat_conversion,[],[f9780]) ).
cnf(s539,plain,
( ~ spl70_94
| ~ spl70_95
| spl70_97 ),
inference(sat_conversion,[],[f10080]) ).
cnf(s604,plain,
( ~ spl70_20
| ~ spl70_21
| spl70_22
| ~ spl70_106 ),
inference(sat_conversion,[],[f10550]) ).
cnf(s609,plain,
( ~ spl70_80
| ~ spl70_81
| spl70_82
| ~ spl70_112 ),
inference(sat_conversion,[],[f10555]) ).
cnf(s611,plain,
( ~ spl70_66
| ~ spl70_67
| spl70_68 ),
inference(sat_conversion,[],[f10670]) ).
cnf(s755,plain,
( ~ spl70_62
| ~ spl70_63
| spl70_64
| ~ spl70_308 ),
inference(sat_conversion,[],[f11810]) ).
cnf(s765,plain,
spl70_11,
inference(rat,[],[s107,s101,s98]) ).
cnf(s766,plain,
spl70_14,
inference(rat,[],[s106,s100,s97]) ).
cnf(s767,plain,
spl70_7,
inference(rat,[],[s108,s99,s96]) ).
cnf(s768,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_96 ),
inference(rat,[],[s95,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s769,plain,
( spl70_1
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| ~ spl70_96 ),
inference(rat,[],[s94,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s770,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| spl70_95 ),
inference(rat,[],[s93,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s771,plain,
( spl70_1
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| spl70_95 ),
inference(rat,[],[s92,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s772,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| spl70_94 ),
inference(rat,[],[s91,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s773,plain,
( spl70_1
| ~ spl70_5
| spl70_17
| spl70_23
| spl70_27
| spl70_94 ),
inference(rat,[],[s90,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s774,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_93 ),
inference(rat,[],[s88,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s775,plain,
( spl70_1
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| ~ spl70_93 ),
inference(rat,[],[s87,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s776,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| spl70_92 ),
inference(rat,[],[s86,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s777,plain,
( spl70_1
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| spl70_92 ),
inference(rat,[],[s85,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s778,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| spl70_91 ),
inference(rat,[],[s84,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s779,plain,
( spl70_1
| ~ spl70_9
| spl70_31
| spl70_37
| spl70_41
| spl70_91 ),
inference(rat,[],[s83,s101,s100,s99,s98,s97,s96,s102]) ).
cnf(s780,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_90 ),
inference(rat,[],[s81,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s781,plain,
( spl70_1
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| ~ spl70_90 ),
inference(rat,[],[s80,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s782,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| spl70_89 ),
inference(rat,[],[s79,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s783,plain,
( spl70_1
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| spl70_89 ),
inference(rat,[],[s78,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s784,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| spl70_88 ),
inference(rat,[],[s77,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s785,plain,
( spl70_1
| ~ spl70_12
| spl70_45
| spl70_51
| spl70_55
| spl70_88 ),
inference(rat,[],[s76,s101,s100,s99,s98,s97,s96,s102,s767]) ).
cnf(s786,plain,
( ~ spl70_16
| spl70_77
| spl70_83 ),
inference(rat,[],[s74,s101,s100,s99,s98,s97,s96,s766,s765,s102,s767]) ).
cnf(s793,plain,
( ~ spl70_2
| ~ spl70_3
| ~ spl70_4
| ~ spl70_15
| spl70_59
| spl70_65 ),
inference(rat,[],[s58,s101,s100,s99,s98,s97,s96,s766,s765,s102,s767]) ).
cnf(s801,plain,
( spl70_5
| spl70_9
| spl70_12
| spl70_15
| spl70_16 ),
inference(rat,[],[s9,s766,s765,s102,s767]) ).
cnf(s802,plain,
( spl70_1
| spl70_5
| spl70_9
| spl70_12
| spl70_16 ),
inference(rat,[],[s8,s766,s765,s102,s767]) ).
cnf(s807,plain,
~ spl70_83,
inference(rat,[],[s124,s64,s65,s66]) ).
cnf(s808,plain,
~ spl70_77,
inference(rat,[],[s126,s609,s59,s60,s61,s62,s63]) ).
cnf(s809,plain,
~ spl70_16,
inference(rat,[],[s786,s807,s808]) ).
cnf(s810,plain,
( spl70_55
| spl70_51
| spl70_1
| ~ spl70_12
| spl70_45 ),
inference(rat,[],[s455,s785,s783,s781]) ).
cnf(s811,plain,
~ spl70_55,
inference(rat,[],[s134,s40,s41,s42]) ).
cnf(s812,plain,
~ spl70_51,
inference(rat,[],[s138,s37,s38,s39]) ).
cnf(s813,plain,
~ spl70_45,
inference(rat,[],[s140,s388,s32,s33,s34,s35,s36]) ).
cnf(s814,plain,
( spl70_41
| spl70_37
| spl70_1
| ~ spl70_9
| spl70_31 ),
inference(rat,[],[s497,s779,s777,s775]) ).
cnf(s815,plain,
~ spl70_41,
inference(rat,[],[s151,s29,s30,s31]) ).
cnf(s816,plain,
~ spl70_37,
inference(rat,[],[s156,s26,s27,s28]) ).
cnf(s817,plain,
~ spl70_31,
inference(rat,[],[s158,s386,s21,s22,s23,s24,s25]) ).
cnf(s818,plain,
( spl70_27
| spl70_23
| spl70_17
| spl70_1
| ~ spl70_5 ),
inference(rat,[],[s539,s180,s773,s771,s769]) ).
cnf(s819,plain,
~ spl70_27,
inference(rat,[],[s122,s18,s19,s20]) ).
cnf(s820,plain,
~ spl70_23,
inference(rat,[],[s195,s15,s16,s17]) ).
cnf(s821,plain,
~ spl70_17,
inference(rat,[],[s199,s604,s10,s11,s12,s13,s14]) ).
cnf(s822,plain,
spl70_1,
inference(rat,[],[s802,s818,s814,s810,s809,s819,s820,s821,s817,s815,s816,s813,s811,s812]) ).
cnf(s824,plain,
spl70_4,
inference(rat,[],[s3,s822]) ).
cnf(s825,plain,
spl70_3,
inference(rat,[],[s2,s822]) ).
cnf(s826,plain,
spl70_2,
inference(rat,[],[s1,s822]) ).
cnf(s827,plain,
~ spl70_65,
inference(rat,[],[s611,s48,s49,s50]) ).
cnf(s828,plain,
~ spl70_59,
inference(rat,[],[s379,s755,s43,s44,s45,s46,s47]) ).
cnf(s829,plain,
~ spl70_15,
inference(rat,[],[s793,s827,s826,s825,s824,s828]) ).
cnf(s830,plain,
~ spl70_12,
inference(rat,[],[s455,s782,s784,s780,s812,s824,s826,s825,s813,s811]) ).
cnf(s831,plain,
~ spl70_9,
inference(rat,[],[s497,s776,s778,s774,s816,s824,s826,s825,s817,s815]) ).
cnf(s832,plain,
spl70_5,
inference(rat,[],[s801,s809,s830,s829,s831]) ).
cnf(s834,plain,
~ spl70_96,
inference(rat,[],[s768,s821,s819,s824,s826,s825,s820,s832]) ).
cnf(s835,plain,
spl70_95,
inference(rat,[],[s770,s819,s821,s824,s826,s825,s820,s832]) ).
cnf(s836,plain,
spl70_94,
inference(rat,[],[s772,s819,s821,s824,s826,s825,s820,s832]) ).
cnf(s837,plain,
~ spl70_97,
inference(rat,[],[s180,s834]) ).
cnf(s838,plain,
$false,
inference(rat,[],[s539,s837,s835,s836]) ).
fof(f11815,plain,
$false,
inference(avatar_sat_refutation,[],[s838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV037+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 09:46:47 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 14.68/2.36 % (2513265)Will run a generic schedule for satisfiability detection.
% 14.68/2.36 % (2513274)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=137676939:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.68/2.36 % (2513271)% WARNING: option uhcvi not known.
% 14.68/2.36 % (2513270)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3893483067_2999 on theBenchmark for (2999ds/0Mi)
% 14.68/2.36 % (2513271)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1872248463:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.68/2.36 % (2513272)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1064587178:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.68/2.36 % (2513273)dis+10_1_sil=32000:sp=arity:random_seed=2656183290:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.68/2.36 % (2513275)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1518882484:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.68/2.36 % (2513276)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1164744556:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.68/2.36 % (2513274)Instruction limit reached!
% 14.68/2.36 % (2513274)------------------------------
% 14.68/2.36 % (2513274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.36 % (2513274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.36 % (2513274)CaDiCaL version: 2.1.3
% 14.68/2.36 % (2513274)Termination reason: Instruction limit
% 14.68/2.36 % (2513274)Termination phase: Saturation
% 14.68/2.36 % (2513274)Time elapsed: 0.032 s
% 14.68/2.36 % (2513274)Peak memory usage: 13 MB
% 14.68/2.36 % (2513274)Instructions burned: 118 (million)
% 14.68/2.36 % (2513284)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1361553279:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.68/2.36 % TRYING [1]
% 14.68/2.36 % TRYING [2]
% 14.68/2.36 % TRYING [3]
% 14.68/2.36 % (2513273)Instruction limit reached!
% 14.68/2.36 % (2513273)------------------------------
% 14.68/2.36 % (2513273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.36 % (2513273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.37 % (2513273)CaDiCaL version: 2.1.3
% 14.68/2.37 % (2513273)Termination reason: Instruction limit
% 14.68/2.37 % (2513273)Termination phase: Saturation
% 14.68/2.37 % (2513273)Time elapsed: 0.059 s
% 14.68/2.37 % (2513273)Peak memory usage: 13 MB
% 14.68/2.37 % (2513273)Instructions burned: 105 (million)
% 14.68/2.37 % (2513275)Instruction limit reached!
% 14.68/2.37 % (2513275)------------------------------
% 14.68/2.37 % (2513275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.37 % (2513275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.37 % (2513275)CaDiCaL version: 2.1.3
% 14.68/2.37 % (2513275)Termination reason: Instruction limit
% 14.68/2.37 % (2513275)Termination phase: Saturation
% 14.68/2.37 % (2513275)Time elapsed: 0.066 s
% 14.68/2.37 % (2513275)Peak memory usage: 13 MB
% 14.68/2.37 % (2513275)Instructions burned: 131 (million)
% 14.68/2.37 % TRYING [1]
% 14.68/2.37 % (2513286)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4035596327:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.68/2.37 % TRYING [2]
% 14.68/2.37 % TRYING [4]
% 14.68/2.37 % (2513287)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=202314176:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.68/2.37 % (2513276)Instruction limit reached!
% 14.68/2.37 % (2513276)------------------------------
% 14.68/2.37 % (2513276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.37 % (2513276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.68/2.37 % (2513276)CaDiCaL version: 2.1.3
% 14.68/2.37 % (2513276)Termination reason: Instruction limit
% 14.68/2.37 % (2513276)Termination phase: Saturation
% 14.68/2.37 % (2513276)Time elapsed: 0.095 s
% 14.68/2.37 % (2513276)Peak memory usage: 15 MB
% 14.68/2.37 % (2513276)Instructions burned: 160 (million)
% 14.68/2.37 % TRYING [3]
% 14.68/2.37 % (2513290)ott-21_1_sil=16000:fs=off:random_seed=63553662:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.68/2.37 % (2513286)Instruction limit reached!
% 14.68/2.37 % (2513286)------------------------------
% 14.68/2.37 % (2513286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.68/2.37 % (2513286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513286)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513286)Termination reason: Instruction limit
% 38.85/5.74 % (2513286)Termination phase: Saturation
% 38.85/5.74 % (2513286)Time elapsed: 0.074 s
% 38.85/5.74 % (2513286)Peak memory usage: 13 MB
% 38.85/5.74 % (2513286)Instructions burned: 131 (million)
% 38.85/5.74 % (2513292)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4194210325:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 38.85/5.74 % TRYING [5]
% 38.85/5.74 % (2513284)Instruction limit reached!
% 38.85/5.74 % (2513284)------------------------------
% 38.85/5.74 % (2513284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.85/5.74 % (2513284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513284)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513284)Termination reason: Instruction limit
% 38.85/5.74 % (2513284)Termination phase: Finite model building constraint generation
% 38.85/5.74 % (2513284)Time elapsed: 0.146 s
% 38.85/5.74 % (2513284)Peak memory usage: 37 MB
% 38.85/5.74 % (2513284)Instructions burned: 715 (million)
% 38.85/5.74 % (2513294)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2141757717:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.85/5.74 % (2513290)Instruction limit reached!
% 38.85/5.74 % (2513290)------------------------------
% 38.85/5.74 % (2513290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.85/5.74 % (2513290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513290)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513290)Termination reason: Instruction limit
% 38.85/5.74 % (2513290)Termination phase: Saturation
% 38.85/5.74 % (2513290)Time elapsed: 0.090 s
% 38.85/5.74 % (2513290)Peak memory usage: 13 MB
% 38.85/5.74 % (2513290)Instructions burned: 181 (million)
% 38.85/5.74 % TRYING [4]
% 38.85/5.74 % (2513296)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3739057782:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 38.85/5.74 % TRYING [1]
% 38.85/5.74 % TRYING [2]
% 38.85/5.74 % TRYING [3]
% 38.85/5.74 % (2513294)Instruction limit reached!
% 38.85/5.74 % (2513294)------------------------------
% 38.85/5.74 % (2513294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.85/5.74 % (2513294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513294)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513294)Termination reason: Instruction limit
% 38.85/5.74 % (2513294)Termination phase: Finite model building SAT solving
% 38.85/5.74 % (2513294)Time elapsed: 0.195 s
% 38.85/5.74 % (2513294)Peak memory usage: 31 MB
% 38.85/5.74 % (2513294)Instructions burned: 870 (million)
% 38.85/5.74 % (2513298)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1621501381:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.85/5.74 % (2513287)Instruction limit reached!
% 38.85/5.74 % (2513287)------------------------------
% 38.85/5.74 % (2513287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.85/5.74 % (2513287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513287)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513287)Termination reason: Instruction limit
% 38.85/5.74 % (2513287)Termination phase: Saturation
% 38.85/5.74 % (2513287)Time elapsed: 0.359 s
% 38.85/5.74 % (2513287)Peak memory usage: 16 MB
% 38.85/5.74 % (2513287)Instructions burned: 685 (million)
% 38.85/5.74 % (2513292)Instruction limit reached!
% 38.85/5.74 % (2513292)------------------------------
% 38.85/5.74 % (2513292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.85/5.74 % (2513292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.85/5.74 % (2513292)CaDiCaL version: 2.1.3
% 38.85/5.74 % (2513292)Termination reason: Instruction limit
% 38.85/5.74 % (2513292)Termination phase: Saturation
% 38.85/5.74 % (2513292)Time elapsed: 0.285 s
% 38.85/5.74 % (2513292)Peak memory usage: 15 MB
% 38.85/5.74 % (2513292)Instructions burned: 478 (million)
% 38.85/5.74 % (2513300)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=3360856296:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 38.85/5.74 % (2513301)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3368401234:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 38.85/5.74 % (2513298)Instruction limit reached!
% 38.85/5.74 % (2513298)------------------------------
% 38.85/5.74 % (2513298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513298)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513298)Termination reason: Instruction limit
% 40.11/6.00 % (2513298)Termination phase: Finite model building constraint generation
% 40.11/6.00 % (2513298)Time elapsed: 0.241 s
% 40.11/6.00 % (2513298)Peak memory usage: 98 MB
% 40.11/6.00 % (2513298)Instructions burned: 889 (million)
% 40.11/6.00 % TRYING [5]
% 40.11/6.00 % (2513304)fmb+10_1_sil=64000:random_seed=2660321435:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 40.11/6.00 % TRYING [1]
% 40.11/6.00 % TRYING [2]
% 40.11/6.00 % TRYING [3]
% 40.11/6.00 % TRYING [4]
% 40.11/6.00 % (2513296)Instruction limit reached!
% 40.11/6.00 % (2513296)------------------------------
% 40.11/6.00 % (2513296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513296)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513296)Termination reason: Instruction limit
% 40.11/6.00 % (2513296)Termination phase: Saturation
% 40.11/6.00 % (2513296)Time elapsed: 0.682 s
% 40.11/6.00 % (2513296)Peak memory usage: 22 MB
% 40.11/6.00 % (2513296)Instructions burned: 1179 (million)
% 40.11/6.00 % (2513300)Instruction limit reached!
% 40.11/6.00 % (2513300)------------------------------
% 40.11/6.00 % (2513300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513300)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513300)Termination reason: Instruction limit
% 40.11/6.00 % (2513300)Termination phase: Saturation
% 40.11/6.00 % (2513300)Time elapsed: 0.443 s
% 40.11/6.00 % (2513300)Peak memory usage: 19 MB
% 40.11/6.00 % (2513300)Instructions burned: 692 (million)
% 40.11/6.00 % (2513301)Instruction limit reached!
% 40.11/6.00 % (2513301)------------------------------
% 40.11/6.00 % (2513301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513301)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513301)Termination reason: Instruction limit
% 40.11/6.00 % (2513301)Termination phase: Saturation
% 40.11/6.00 % (2513301)Time elapsed: 0.441 s
% 40.11/6.00 % (2513301)Peak memory usage: 21 MB
% 40.11/6.00 % (2513301)Instructions burned: 879 (million)
% 40.11/6.00 % (2513306)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3039236861:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 40.11/6.00 % (2513307)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3255649852:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 40.11/6.00 % (2513308)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1172446780:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 40.11/6.00 % TRYING [20]
% 40.11/6.00 % TRYING [8]
% 40.11/6.00 % TRYING [5]
% 40.11/6.00 % (2513307)Instruction limit reached!
% 40.11/6.00 % (2513307)------------------------------
% 40.11/6.00 % (2513307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513307)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513307)Termination reason: Instruction limit
% 40.11/6.00 % (2513307)Termination phase: Finite model building constraint generation
% 40.11/6.00 % (2513307)Time elapsed: 0.325 s
% 40.11/6.00 % (2513307)Peak memory usage: 60 MB
% 40.11/6.00 % (2513307)Instructions burned: 920 (million)
% 40.11/6.00 % (2513312)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3895183511:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 40.11/6.00 % TRYING [6]
% 40.11/6.00 % (2513312)Instruction limit reached!
% 40.11/6.00 % (2513312)------------------------------
% 40.11/6.00 % (2513312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513312)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513312)Termination reason: Instruction limit
% 40.11/6.00 % (2513312)Termination phase: Saturation
% 40.11/6.00 % (2513312)Time elapsed: 0.728 s
% 40.11/6.00 % (2513312)Peak memory usage: 26 MB
% 40.11/6.00 % (2513312)Instructions burned: 1473 (million)
% 40.11/6.00 % (2513314)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=270462339:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 40.11/6.00 % (2513314)Cannot represent all propositional literals internally
% 40.11/6.00 % (2513314)Refutation not found, incomplete strategy
% 40.11/6.00 % (2513314)------------------------------
% 40.11/6.00 % (2513314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513314)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513314)Termination reason: Refutation not found, incomplete strategy
% 40.11/6.00 % (2513314)Time elapsed: 0.076 s
% 40.11/6.00 % (2513314)Peak memory usage: 13 MB
% 40.11/6.00 % (2513314)Instructions burned: 172 (million)
% 40.11/6.00 % (2513314)------------------------------
% 40.11/6.00 % (2513314)------------------------------
% 40.11/6.00 % (2513316)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3117310295:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 40.11/6.00 % TRYING [6]
% 40.11/6.00 % TRYING [16]
% 40.11/6.00 % (2513316)Instruction limit reached!
% 40.11/6.00 % (2513316)------------------------------
% 40.11/6.00 % (2513316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513316)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513316)Termination reason: Instruction limit
% 40.11/6.00 % (2513316)Termination phase: Finite model building constraint generation
% 40.11/6.00 % (2513316)Time elapsed: 0.806 s
% 40.11/6.00 % (2513316)Peak memory usage: 123 MB
% 40.11/6.00 % (2513316)Instructions burned: 2175 (million)
% 40.11/6.00 % (2513318)ott-2_1_sil=16000:newcnf=on:random_seed=2691251992:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 40.11/6.00 % (2513318)Instruction limit reached!
% 40.11/6.00 % (2513318)------------------------------
% 40.11/6.00 % (2513318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513318)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513318)Termination reason: Instruction limit
% 40.11/6.00 % (2513318)Termination phase: Saturation
% 40.11/6.00 % (2513318)Time elapsed: 0.482 s
% 40.11/6.00 % (2513318)Peak memory usage: 19 MB
% 40.11/6.00 % (2513318)Instructions burned: 869 (million)
% 40.11/6.00 % (2513320)ott+10_1_sil=32000:tgt=ground:random_seed=893785359:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 40.11/6.00 % (2513308)Instruction limit reached!
% 40.11/6.00 % (2513308)------------------------------
% 40.11/6.00 % (2513308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513308)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513308)Termination reason: Instruction limit
% 40.11/6.00 % (2513308)Termination phase: Saturation
% 40.11/6.00 % (2513308)Time elapsed: 2.556 s
% 40.11/6.00 % (2513308)Peak memory usage: 29 MB
% 40.11/6.00 % (2513308)Instructions burned: 5132 (million)
% 40.11/6.00 % (2513322)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=489071148:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 40.11/6.00 % TRYING [1]
% 40.11/6.00 % TRYING [2]
% 40.11/6.00 % TRYING [3]
% 40.11/6.00 % TRYING [4]
% 40.11/6.00 % TRYING [5]
% 40.11/6.00 % (2513306)Instruction limit reached!
% 40.11/6.00 % (2513306)------------------------------
% 40.11/6.00 % (2513306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513306)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513306)Termination reason: Instruction limit
% 40.11/6.00 % (2513306)Termination phase: Finite model building constraint generation
% 40.11/6.00 % (2513306)Time elapsed: 3.359 s
% 40.11/6.00 % (2513306)Peak memory usage: 592 MB
% 40.11/6.00 % (2513306)Instructions burned: 9515 (million)
% 40.11/6.00 % (2513324)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3381249031:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 40.11/6.00 % TRYING [7]
% 40.11/6.00 % TRYING [6]
% 40.11/6.00 % (2513304)Instruction limit reached!
% 40.11/6.00 % (2513304)------------------------------
% 40.11/6.00 % (2513304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.00 % (2513304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.00 % (2513304)CaDiCaL version: 2.1.3
% 40.11/6.00 % (2513304)Termination reason: Instruction limit
% 40.11/6.00 % (2513304)Termination phase: Finite model building SAT solving
% 40.11/6.00 % (2513304)Time elapsed: 4.794 s
% 40.11/6.00 % (2513304)Peak memory usage: 213 MB
% 40.11/6.00 % (2513304)Instructions burned: 22064 (million)
% 40.11/6.00 % (2513326)dis+21_1_sil=32000:sas=cadical:random_seed=3558641816:i=3773:amm=off_2944 on theBenchmark for (2944ds/3773Mi)
% 40.11/6.00 % (2513326) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2513265-2513326"...
% 40.11/6.00 % (2513326)...printing done.
% 40.11/6.00 % (2513326)Refutation found. Thanks to Tanya!
% 40.11/6.00 % SZS status Theorem for theBenchmark
% 40.11/6.00 % SZS output start Proof for theBenchmark
% See solution above
% 40.11/6.01 % (2513326)------------------------------
% 40.11/6.01 % (2513326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.11/6.01 % (2513326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.11/6.01 % (2513326)CaDiCaL version: 2.1.3
% 40.11/6.01 % (2513326)Termination reason: Refutation
% 40.11/6.01 % (2513326)Time elapsed: 0.199 s
% 40.11/6.01 % (2513326)Peak memory usage: 17 MB
% 40.11/6.01 % (2513326)Instructions burned: 717 (million)
% 40.11/6.01 % (2513265)Success in time 5.778 s
% 40.11/6.01 % Vampire exiting
%------------------------------------------------------------------------------