TPTP Problem File: SWX147_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX147_1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Neural network verification problem B_025
% Version : Especial.
% English :
% Refs : [PT12] Pulina & Tacchella (2012), Challenging SMT Solvers to
% : [GPP23] Guidotti et al. (2023), Leveraging Satisfiability Modu
% : [Pul25] Pulina (2025), Email to Geoff Sutcliffe
% Source : [Pul25]
% Names : B_025_cvc.smt2 [Pul25]
% Status : Unsatisfiable
% Rating : 0.80 v9.3.0
% Syntax : Number of formulae : 36 ( 21 unt; 13 typ; 1 def)
% Number of atoms : 31 ( 5 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 9 ( 1 ~; 5 |; 1 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 77 ( 4 avg)
% Number arithmetic : 7271 ( 26 atm;4888 fun;2355 num; 2 var)
% Number of types : 1 ( 0 usr; 1 ari)
% Number of type conns : 2 ( 1 >; 1 *; 0 +; 0 <<)
% Number of predicates : 3 ( 0 usr; 0 prp; 2-2 aty)
% Number of functors : 876 ( 13 usr; 872 con; 0-2 aty)
% Number of variables : 2 ( 2 !; 0 ?; 2 :)
% SPC : TF0_THM_EQU_ARI
% Comments :
%------------------------------------------------------------------------------
%---Declarations:
tff('X_7',type,
'X_7': $real ).
tff('X_8',type,
'X_8': $real ).
tff('X_3',type,
'X_3': $real ).
tff('Y_0',type,
'Y_0': $real ).
tff('Y_2',type,
'Y_2': $real ).
tff('X_0',type,
'X_0': $real ).
tff('X_4',type,
'X_4': $real ).
tff(max,type,
max: ( $real * $real ) > $real ).
tff('X_1',type,
'X_1': $real ).
tff('Y_1',type,
'Y_1': $real ).
tff('X_2',type,
'X_2': $real ).
tff('X_6',type,
'X_6': $real ).
tff('X_5',type,
'X_5': $real ).
%---Assertions:
%---((-1.0 * X_0) ≤ -0.155896813422542)
tff(formula_1,axiom,
$lesseq($product($uminus(1.0),'X_0'),$uminus(0.155896813422542)) ).
%---((1.0 * X_0) ≤ 0.157896813422542)
tff(formula_2,axiom,
$lesseq($product(1.0,'X_0'),0.157896813422542) ).
%---((-1.0 * X_1) ≤ -0.056416492942258)
tff(formula_3,axiom,
$lesseq($product($uminus(1.0),'X_1'),$uminus(0.056416492942258)) ).
%---((1.0 * X_1) ≤ 0.058416492942258)
tff(formula_4,axiom,
$lesseq($product(1.0,'X_1'),0.058416492942258) ).
%---((-1.0 * X_2) ≤ -0.0030793814015310002)
tff(formula_5,axiom,
$lesseq($product($uminus(1.0),'X_2'),$uminus(0.0030793814015310002)) ).
%---((1.0 * X_2) ≤ 0.005079381401531)
tff(formula_6,axiom,
$lesseq($product(1.0,'X_2'),0.005079381401531) ).
%---((-1.0 * X_3) ≤ -0.497784248037036)
tff(formula_7,axiom,
$lesseq($product($uminus(1.0),'X_3'),$uminus(0.497784248037036)) ).
%---((1.0 * X_3) ≤ 0.499784248037036)
tff(formula_8,axiom,
$lesseq($product(1.0,'X_3'),0.499784248037036) ).
%---((-1.0 * X_4) ≤ -0.345103843238191)
tff(formula_9,axiom,
$lesseq($product($uminus(1.0),'X_4'),$uminus(0.345103843238191)) ).
%---((1.0 * X_4) ≤ 0.347103843238191)
tff(formula_10,axiom,
$lesseq($product(1.0,'X_4'),0.347103843238191) ).
%---((-1.0 * X_5) ≤ -0.042908722363159)
tff(formula_11,axiom,
$lesseq($product($uminus(1.0),'X_5'),$uminus(0.042908722363159)) ).
%---((1.0 * X_5) ≤ 0.044908722363159)
tff(formula_12,axiom,
$lesseq($product(1.0,'X_5'),0.044908722363159) ).
%---((-1.0 * X_6) ≤ -0.998829251495207)
tff(formula_13,axiom,
$lesseq($product($uminus(1.0),'X_6'),$uminus(0.998829251495207)) ).
%---((1.0 * X_6) ≤ 1.0)
tff(formula_14,axiom,
$lesseq($product(1.0,'X_6'),1.0) ).
%---((-1.0 * X_7) ≤ -0.492043249872778)
tff(formula_15,axiom,
$lesseq($product($uminus(1.0),'X_7'),$uminus(0.492043249872778)) ).
%---((1.0 * X_7) ≤ 0.494043249872778)
tff(formula_16,axiom,
$lesseq($product(1.0,'X_7'),0.494043249872778) ).
%---((-1.0 * X_8) ≤ -0.038862760896398)
tff(formula_17,axiom,
$lesseq($product($uminus(1.0),'X_8'),$uminus(0.038862760896398)) ).
%---((1.0 * X_8) ≤ 0.040862760896398)
tff(formula_18,axiom,
$lesseq($product(1.0,'X_8'),0.040862760896398) ).
%---(((1.0 * Y_0) ≤ -0.9940313744198672) ∨ ((-1.0 * Y_0) ≤ -1.0059686255801328) ∨ ((1.0 * Y_1) ≤ -0.9938034386370552) ∨ ((-1.0 * Y_1) ≤ -1.0061965613629447) ∨ ((1.0 * Y_2) ≤ -0.5166291220164629) ∨ ((-1.0 * Y_2) ≤ -1.483370877983537))
tff(formula_19,axiom,
( $lesseq($product(1.0,'Y_0'),$uminus(0.9940313744198672))
| $lesseq($product($uminus(1.0),'Y_0'),$uminus(1.0059686255801328))
| $lesseq($product(1.0,'Y_1'),$uminus(0.9938034386370552))
| $lesseq($product($uminus(1.0),'Y_1'),$uminus(1.0061965613629447))
| $lesseq($product(1.0,'Y_2'),$uminus(0.5166291220164629))
| $lesseq($product($uminus(1.0),'Y_2'),$uminus(1.483370877983537)) ) ).
%---(Y_0 = ((max(((X_0 * -0.034143127336152712) + (X_1 * 0.322824668200060227) + (X_2 * 0.091291052421442809) + (X_3 * -0.012612789817531833) + (X_4 * 0.273541493916837075) + (X_5 * -0.150105792320639253) + (X_6 * -0.049406931293640266) + (X_7 * -0.21107752838875965) + (X_8 * 0.277909149915428422) + -0.019189099155314304), 0.0) * -0.002546245018821197) + (max(((X_0 * 0.135860462188255371) + (X_1 * 0.187969393886196101) + (X_2 * 0.174517671834989951) + (X_3 * 0.127635942676799008) + (X_4 * -0.136994285692501105) + (X_5 * 0.012365905796069943) + (X_6 * -0.027014764654490264) + (X_7 * -0.305544519265200321) + (X_8 * -0.206852248891131074) + -0.314645004469935208), 0.0) * 0.081027244089196759) + (max(((X_0 * -0.081020401392122687) + (X_1 * 0.062490409237779099) + (X_2 * 0.111520586127630439) + (X_3 * -0.213447096651937063) + (X_4 * 0.132706362488796692) + (X_5 * -0.261185283187217065) + (X_6 * 0.00474527583528711) + (X_7 * -0.06688270460651552) + (X_8 * -0.320470498630223033) + -0.190989000847826468), 0.0) * 0.120795879453134219) + (max(((X_0 * 0.138290117678506908) + (X_1 * 0.005330501640528451) + (X_2 * -0.13333471971657565) + (X_3 * 0.153277069170855151) + (X_4 * 0.193097250496935435) + (X_5 * 0.124353050256880426) + (X_6 * -0.312998335768394587) + (X_7 * 0.14582588668244395) + (X_8 * 0.017849845577707468) + -0.207803467395465624), 0.0) * -0.10301681682459779) + (max(((X_0 * 0.25616055553271605) + (X_1 * -0.03627032974016875) + (X_2 * -0.194452918074013159) + (X_3 * 0.10008950100824493) + (X_4 * 0.321933544906211566) + (X_5 * 0.302676823386164806) + (X_6 * 0.282644938195837081) + (X_7 * 0.218166819191055239) + (X_8 * 0.061315114611943666) + 0.294909295927187565), 0.0) * 0.119309649478056334) + (max(((X_0 * -0.203907213010214777) + (X_1 * -0.329328844050836067) + (X_2 * -0.282209682521432303) + (X_3 * 0.194481051286681639) + (X_4 * 0.223447381199474771) + (X_5 * -0.130047140060396471) + (X_6 * 0.258072855214746821) + (X_7 * 0.236670528410227232) + (X_8 * 0.219327984313435753) + 0.307309013280585186), 0.0) * -0.000471133946861574) + (max(((X_0 * -0.025392492262058697) + (X_1 * -0.260814592583792804) + (X_2 * -0.060464105023337156) + (X_3 * 0.235580850968075406) + (X_4 * 0.013069063238517142) + (X_5 * -0.196757326475462957) + (X_6 * 0.028155879508867165) + (X_7 * -0.181432604418310606) + (X_8 * 0.089552351207647263) + 0.233953211619548462), 0.0) * -0.012643206083268216) + (max(((X_0 * -0.316000969071793147) + (X_1 * 0.025263023662981166) + (X_2 * 0.177171946751012388) + (X_3 * -0.035122639314649318) + (X_4 * -0.23096764293788713) + (X_5 * 0.017100988871234346) + (X_6 * -0.209560107747809532) + (X_7 * -0.026921531592388137) + (X_8 * -0.032723387475881827) + 0.168724722506589486), 0.0) * 0.112900602789428761) + (max(((X_0 * 0.001306859463930443) + (X_1 * -0.32178678467757027) + (X_2 * -0.073177542048799837) + (X_3 * 0.002394918508160371) + (X_4 * 0.093730698889344044) + (X_5 * 0.008752806231017984) + (X_6 * -0.084064570826615143) + (X_7 * 0.250900209655107453) + (X_8 * 0.022976222292577286) + 0.077232081109878559), 0.0) * 0.082335754692696106) + (max(((X_0 * 0.194049225184143082) + (X_1 * -0.022183735625062984) + (X_2 * -0.196724399739592354) + (X_3 * 0.07635785513446619) + (X_4 * -0.196322916482755933) + (X_5 * -0.288926766400791291) + (X_6 * 0.213700339341032219) + (X_7 * -0.253512613136544884) + (X_8 * 0.231484855576049309) + 0.280058863303405625), 0.0) * -0.074458908043544547) + (max(((X_0 * 0.317728685554186929) + (X_1 * 0.332150001647927684) + (X_2 * -0.001259591758584755) + (X_3 * -0.207453820552864571) + (X_4 * 0.005723595304183482) + (X_5 * 0.185428526068087629) + (X_6 * 0.054353623505082105) + (X_7 * 0.132946612680298504) + (X_8 * 0.011140036900155748) + -0.209314307847249387), 0.0) * -0.110400328569695477) + (max(((X_0 * -0.269304224359853461) + (X_1 * -0.310904419113500918) + (X_2 * 0.32027709592926229) + (X_3 * -0.200037762633937188) + (X_4 * -0.026191122665172317) + (X_5 * -0.042660660377485116) + (X_6 * -0.146275965076368142) + (X_7 * -0.305670262866760689) + (X_8 * 0.322576996064118438) + -0.183572002247813032), 0.0) * 0.066133019473005733) + (max(((X_0 * 0.136084741586379454) + (X_1 * 0.26228771638376186) + (X_2 * -0.284171295665994417) + (X_3 * 0.211831054834103749) + (X_4 * 0.285004999381932744) + (X_5 * -0.007441424708356792) + (X_6 * -0.140284600003246995) + (X_7 * -0.207592415895373833) + (X_8 * 0.27321519909354347) + -0.207526152104757111), 0.0) * 0.038353156981341702) + (max(((X_0 * -0.22841409680804925) + (X_1 * 0.240551489683236974) + (X_2 * 0.312484269972083728) + (X_3 * -0.181755643345508588) + (X_4 * 0.030657116136170337) + (X_5 * -0.055299675827487349) + (X_6 * -0.062998580523338621) + (X_7 * 0.098231667492682917) + (X_8 * -0.015349265026970815) + 0.174413712522803299), 0.0) * -0.121499176770419159) + (max(((X_0 * 0.326514337483990558) + (X_1 * -0.139206653914812462) + (X_2 * -0.301944004088363971) + (X_3 * 0.007220186513743954) + (X_4 * -0.082554028749347141) + (X_5 * -0.040344607481459793) + (X_6 * -0.215478397144116013) + (X_7 * 0.145783348414039393) + (X_8 * -0.142290498498560514) + -0.21557124240865938), 0.0) * -0.013954590494720587) + (max(((X_0 * -0.001976599008208513) + (X_1 * -0.057764032526161302) + (X_2 * 0.159396263708995178) + (X_3 * -0.183991541476796888) + (X_4 * 0.142504183402018647) + (X_5 * -0.238937927812336026) + (X_6 * -0.30402575884910954) + (X_7 * 0.29491808364114086) + (X_8 * 0.054445412143243832) + -0.170312927346704335), 0.0) * -0.040915377252787377) + (max(((X_0 * -0.069437022416364014) + (X_1 * -0.00060254546898092) + (X_2 * 0.247675182881536504) + (X_3 * 0.234314025579507035) + (X_4 * -0.177673295141312471) + (X_5 * -0.332483963357472823) + (X_6 * -0.218038989896279178) + (X_7 * 0.127363049893037317) + (X_8 * -0.2086790536248469) + -0.187722099200903436), 0.0) * -0.05295491168066957) + (max(((X_0 * 0.324876735423139718) + (X_1 * 0.075982824387152592) + (X_2 * -0.313261926183435957) + (X_3 * -0.209064108357157524) + (X_4 * -0.261535938731004891) + (X_5 * -0.234787129658768606) + (X_6 * 0.112031404664260759) + (X_7 * 0.225008006173745667) + (X_8 * 0.140199347195911539) + 0.139447447171109518), 0.0) * -0.086948235574972305) + (max(((X_0 * 0.202182439886614829) + (X_1 * 0.228470631117320078) + (X_2 * 0.074549186229916131) + (X_3 * 0.233422713721841812) + (X_4 * 0.131135712704656016) + (X_5 * -0.326710062287342951) + (X_6 * 0.012038286823084332) + (X_7 * 0.231618192292777969) + (X_8 * 0.000719113164345198) + 0.213277245603735233), 0.0) * -0.008697914681319946) + (max(((X_0 * 0.28449527898218091) + (X_1 * -0.081527175695953635) + (X_2 * -0.153930222701464642) + (X_3 * -0.186077449214199719) + (X_4 * -0.05936612416981174) + (X_5 * -0.154628465341259957) + (X_6 * -0.166498063888305931) + (X_7 * 0.055266800565439478) + (X_8 * -0.213197545634780383) + 0.010205194890945457), 0.0) * -0.104668729123890775) + (max(((X_0 * -0.180816367347528484) + (X_1 * 0.043531190359145266) + (X_2 * -0.047619638831746636) + (X_3 * -0.058934638109038928) + (X_4 * -0.124666639609441937) + (X_5 * -0.318308163331019744) + (X_6 * 0.193062520783280067) + (X_7 * 0.020418055017284109) + (X_8 * 0.060922472827523722) + 0.223360539691101423), 0.0) * -0.054775070975789514) + (max(((X_0 * 0.134746472119233907) + (X_1 * -0.217554078381223898) + (X_2 * -0.085730993819177093) + (X_3 * 0.297521692708929308) + (X_4 * 0.063860554017248994) + (X_5 * 0.217082184168041759) + (X_6 * -0.021045092732637605) + (X_7 * 0.259811010052565072) + (X_8 * 0.200338555724555889) + 0.247229328571023033), 0.0) * -0.095070995295625293) + (max(((X_0 * 0.203487277967640046) + (X_1 * 0.324424625686173973) + (X_2 * -0.024662687002090788) + (X_3 * 0.216277755365953894) + (X_4 * 0.163509105125114296) + (X_5 * -0.034687792438270026) + (X_6 * 0.206452845548049824) + (X_7 * 0.154282897842712208) + (X_8 * -0.017555615896969023) + 0.272302961557755852), 0.0) * 0.10157507612563263) + (max(((X_0 * -0.244290676854412331) + (X_1 * -0.204088781911439338) + (X_2 * -0.03882746711711399) + (X_3 * -0.097232792095546527) + (X_4 * -0.303174897657345899) + (X_5 * -0.051070311788715628) + (X_6 * 0.149992479035335302) + (X_7 * -0.102185614965710991) + (X_8 * -0.106519170243570216) + 0.058597670613885988), 0.0) * 0.089954845675315365) + (max(((X_0 * 0.012864262113814806) + (X_1 * 0.109069631915820031) + (X_2 * 0.101543371952154571) + (X_3 * 0.06799496124837745) + (X_4 * -0.26445983492561137) + (X_5 * 0.215833875445791301) + (X_6 * 0.272580780248200039) + (X_7 * -0.039747643760278006) + (X_8 * -0.243825769939117892) + -0.123945865842741254), 0.0) * 0.057172696196788608) + (max(((X_0 * -0.154837365313728936) + (X_1 * 0.085840778969112019) + (X_2 * 0.165077967938471126) + (X_3 * 0.111848736690037587) + (X_4 * -0.240612563426037041) + (X_5 * 0.140637468751368289) + (X_6 * -0.149768050036042905) + (X_7 * -0.283477350113733539) + (X_8 * 0.073570979765799127) + 0.079922247453340256), 0.0) * 0.013857350493885673) + (max(((X_0 * -0.100199971469390775) + (X_1 * 0.186120110641400827) + (X_2 * 0.049038095207454113) + (X_3 * -0.196087530498076618) + (X_4 * 0.08711796538252381) + (X_5 * -0.101227855157801916) + (X_6 * 0.158620075819161321) + (X_7 * -0.146913672899774472) + (X_8 * -0.119082579355500373) + 0.138895725711660534), 0.0) * -0.005384789761385123) + (max(((X_0 * 0.180027772073166392) + (X_1 * -0.103336431479241098) + (X_2 * -0.267316901673856466) + (X_3 * 0.263656543687109834) + (X_4 * 0.332642570227415224) + (X_5 * 0.277967948182220759) + (X_6 * 0.30343956010141554) + (X_7 * 0.03447325941087459) + (X_8 * 0.125197865386826701) + 0.192506796333139885), 0.0) * -0.057310478208179444) + (max(((X_0 * -0.229596022939276084) + (X_1 * 0.306162374571047058) + (X_2 * -0.214349113239148403) + (X_3 * 0.05827258272512098) + (X_4 * 0.131302065849309368) + (X_5 * -0.271631521510831919) + (X_6 * -0.270260881180521384) + (X_7 * -0.202970959783648347) + (X_8 * 0.179428170698139933) + 0.115665614154320362), 0.0) * -0.092476757020151706) + (max(((X_0 * 0.194962600903016259) + (X_1 * -0.17835559373673493) + (X_2 * -0.228962538545053329) + (X_3 * 0.306214141164736053) + (X_4 * 0.257337107072608651) + (X_5 * -0.299595911463449771) + (X_6 * 0.089666024789417487) + (X_7 * 0.326462876291198911) + (X_8 * -0.062301378541843311) + 0.172234015205460611), 0.0) * -0.08196635417351622) + (max(((X_0 * 0.255845191590086396) + (X_1 * 0.215495725762357482) + (X_2 * -0.302097504773537306) + (X_3 * 0.095845709494328524) + (X_4 * -0.075426811348071776) + (X_5 * 0.218624900118963683) + (X_6 * 0.26160805655982583) + (X_7 * -0.212202541273525114) + (X_8 * -0.041523081831996933) + 0.102324186276997908), 0.0) * -0.092317073009903355) + (max(((X_0 * 0.30493330995168616) + (X_1 * -0.122490486481055483) + (X_2 * 0.174817256741448934) + (X_3 * -0.202369269426108028) + (X_4 * -0.323621969121451081) + (X_5 * 0.303508866087579043) + (X_6 * -0.223769302030546458) + (X_7 * -0.27502503528423522) + (X_8 * 0.129622404600985675) + -0.253776462014690563), 0.0) * 0.033984477497181892) + (max(((X_0 * 0.269059547412644651) + (X_1 * -0.005882567254681115) + (X_2 * -0.171353970135741607) + (X_3 * 0.294037626949683328) + (X_4 * -0.255251802687420648) + (X_5 * -0.009759698938691885) + (X_6 * 0.180149176039681114) + (X_7 * 0.045388866190233079) + (X_8 * -0.179760143010707252) + 0.269823604538700745), 0.0) * 0.08550415622620669) + (max(((X_0 * -0.138558699684565634) + (X_1 * 0.003660311035716235) + (X_2 * -0.328144076991653155) + (X_3 * 0.17711252434090502) + (X_4 * 0.086745978461675144) + (X_5 * 0.052468260508699016) + (X_6 * 0.051635532764924497) + (X_7 * 0.032455574507212981) + (X_8 * -0.079164165185457769) + 0.068544128415001238), 0.0) * -0.101034255172639253) + (max(((X_0 * -0.188430209592040626) + (X_1 * 0.180982936820061113) + (X_2 * 0.124800571217657474) + (X_3 * -0.054881926059530961) + (X_4 * -0.026456773114379717) + (X_5 * 0.162595317059087197) + (X_6 * 0.049021975497793691) + (X_7 * -0.246830321591287927) + (X_8 * 0.232013828123107502) + -0.062546264757998127), 0.0) * -0.113667293596708435) + (max(((X_0 * 0.040962088339393521) + (X_1 * -0.254386604085368229) + (X_2 * -0.112672966314846829) + (X_3 * -0.159902546439000759) + (X_4 * -0.207701480823660051) + (X_5 * 0.133165675227524982) + (X_6 * 0.193618244226427871) + (X_7 * 0.082613724983702452) + (X_8 * 0.322632448399385929) + 0.224209517678037373), 0.0) * 0.114938780024844672) + (max(((X_0 * -0.134886517018193708) + (X_1 * 0.144899616770255646) + (X_2 * -0.17980112071828272) + (X_3 * -0.267509492307719976) + (X_4 * -0.157528799514788709) + (X_5 * -0.079420419232439199) + (X_6 * -0.299465230679228367) + (X_7 * -0.125820656916256324) + (X_8 * 0.019239984001792998) + 0.142229458135585185), 0.0) * -0.035320785296854867) + (max(((X_0 * -0.172346696671293709) + (X_1 * 0.090451716164184959) + (X_2 * -0.228793228787715741) + (X_3 * 0.180997116632383548) + (X_4 * 0.290344111330939902) + (X_5 * -0.234970994376170916) + (X_6 * 0.005159751606115537) + (X_7 * -0.155461525393435412) + (X_8 * -0.288046325238939249) + -0.070296844355285437), 0.0) * -0.000302411809356834) + (max(((X_0 * -0.234997276198458949) + (X_1 * -0.172512713965825709) + (X_2 * 0.114308047040828642) + (X_3 * -0.063627448790975871) + (X_4 * -0.205794049922004174) + (X_5 * 0.19287844644458868) + (X_6 * -0.257664032924889597) + (X_7 * -0.233509914142561753) + (X_8 * 0.267404797826638896) + 0.248418369896963032), 0.0) * -0.041750357136473404) + (max(((X_0 * 0.296841143323539114) + (X_1 * -0.012110575240900978) + (X_2 * -0.122779558396503508) + (X_3 * 0.145965415302344859) + (X_4 * 0.115669853903047126) + (X_5 * 0.181260046623958171) + (X_6 * 0.176356841716120927) + (X_7 * 0.054758245250969895) + (X_8 * 0.066387541776141479) + 0.033378311133483385), 0.0) * 0.097285514236117476) + (max(((X_0 * -0.068127119880877884) + (X_1 * -0.193888759810902311) + (X_2 * -0.075010565817496266) + (X_3 * 0.116013395273452391) + (X_4 * 0.197890889155673377) + (X_5 * 0.321385853477913319) + (X_6 * 0.050015661552153368) + (X_7 * -0.054890782359229284) + (X_8 * 0.258758291380532579) + -0.143355802615697941), 0.0) * -0.004404402516794192) + (max(((X_0 * -0.071997512442384004) + (X_1 * 0.017303820158426297) + (X_2 * 0.091534845651731311) + (X_3 * 0.311279068800356329) + (X_4 * -0.00312157907909616) + (X_5 * -0.188277000904065517) + (X_6 * -0.183479587316280945) + (X_7 * 0.212372245445371421) + (X_8 * -0.077162998727941579) + -0.223645418757847825), 0.0) * 0.015491725814317153) + (max(((X_0 * -0.32243249625430126) + (X_1 * 0.182253848897861837) + (X_2 * -0.099368623456786598) + (X_3 * -0.156602428474534483) + (X_4 * 0.030765939328599223) + (X_5 * -0.026342715055112154) + (X_6 * 0.000532788149621544) + (X_7 * 0.303861041761946782) + (X_8 * 0.265755190798946772) + 0.100146050819974963), 0.0) * 0.001192439002770218) + (max(((X_0 * -0.112545642928356893) + (X_1 * 0.265866650798053328) + (X_2 * 0.015101151225212606) + (X_3 * -0.317799591526125247) + (X_4 * -0.168903714240354275) + (X_5 * 0.030188500593428369) + (X_6 * 0.061277558788815967) + (X_7 * 0.200866407017562254) + (X_8 * -0.112371008406928929) + -0.079493482734081355), 0.0) * -0.015260232367988874) + (max(((X_0 * -0.192154828636623531) + (X_1 * 0.083979791049164365) + (X_2 * 0.159973530860791413) + (X_3 * -0.265406610551946254) + (X_4 * 0.287198912407206131) + (X_5 * 0.095627746140380554) + (X_6 * -0.00994146969909776) + (X_7 * -0.219422562050552161) + (X_8 * -0.081085067577720604) + 0.104747771083528063), 0.0) * -0.09459565655845989) + (max(((X_0 * -0.057039132055541286) + (X_1 * 0.038985751754933406) + (X_2 * -0.004944442157409357) + (X_3 * -0.15462525839770902) + (X_4 * -0.1398935031159593) + (X_5 * -0.061959641528152032) + (X_6 * 0.098679300771940037) + (X_7 * -0.201235020697894035) + (X_8 * -0.237594859082526227) + -0.158841501426246007), 0.0) * -0.108315821817297875) + (max(((X_0 * 0.331353170527205643) + (X_1 * -0.288645365007353272) + (X_2 * 0.223956278926402741) + (X_3 * 0.279170663263683283) + (X_4 * 0.017978724577996319) + (X_5 * -0.250013034963560865) + (X_6 * 0.098807821234157156) + (X_7 * 0.258776815881270383) + (X_8 * 0.152988470579232594) + 0.28246081276552143), 0.0) * 0.003632176971928025) + (max(((X_0 * -0.100883845060276311) + (X_1 * 0.046212140463826712) + (X_2 * -0.026600669905651519) + (X_3 * 0.142320732212770695) + (X_4 * 0.072733698806154878) + (X_5 * 0.197196887480299343) + (X_6 * 0.237120144257248089) + (X_7 * -0.166327692927533299) + (X_8 * -0.078131387240757411) + -0.293417736964490861), 0.0) * 0.11352795843340871) + (max(((X_0 * 0.294400522037719437) + (X_1 * 0.082094261162431514) + (X_2 * 0.101918067411788049) + (X_3 * 0.17357922076579041) + (X_4 * 0.114082861901367405) + (X_5 * -0.311032034544396929) + (X_6 * 0.258029579372313467) + (X_7 * 0.145657792087877658) + (X_8 * -0.033975658190385893) + 0.194899911587433305), 0.0) * -0.049073925423291309) + (max(((X_0 * 0.034313476891573602) + (X_1 * -0.189736665978239627) + (X_2 * 0.098474573164286039) + (X_3 * 0.220418718662632351) + (X_4 * 0.03836653204063839) + (X_5 * 0.279710695915403817) + (X_6 * 0.14410430753399317) + (X_7 * 0.204156618335651407) + (X_8 * 0.176473915501038803) + -0.03827183418778396), 0.0) * -0.100382386321973965) + (max(((X_0 * 0.00869382371014682) + (X_1 * -0.310492767426873872) + (X_2 * 0.117116910196331914) + (X_3 * 0.169087657846020811) + (X_4 * -0.273335058913078577) + (X_5 * -0.000683592328365401) + (X_6 * 0.139512227022986102) + (X_7 * -0.313799159812941153) + (X_8 * -0.196166996347198946) + 0.236750714424111497), 0.0) * -0.00867737418549025) + (max(((X_0 * 0.137861025679069715) + (X_1 * -0.024667890831123473) + (X_2 * -0.315714844767212732) + (X_3 * 0.237047096266294222) + (X_4 * 0.202101116810822823) + (X_5 * -0.020405610795288631) + (X_6 * 0.223248306677427399) + (X_7 * 0.166427221032260431) + (X_8 * 0.322898701032060254) + 0.085041015223344729), 0.0) * -0.071289808274688116) + (max(((X_0 * 0.063704153901590399) + (X_1 * 0.084893455136697493) + (X_2 * 0.162022423603656263) + (X_3 * -0.026069359722939833) + (X_4 * -0.103610576532342291) + (X_5 * 0.247462072588003845) + (X_6 * 0.235604458158232999) + (X_7 * 0.094778590268327412) + (X_8 * 0.317884709780666685) + -0.259110365198896853), 0.0) * 0.086383813374095925) + (max(((X_0 * 0.157051962420222013) + (X_1 * 0.02119912918435074) + (X_2 * -0.144567654546317315) + (X_3 * -0.120485782181390416) + (X_4 * 0.245385692300038649) + (X_5 * -0.12013008718360596) + (X_6 * -0.264054168644354381) + (X_7 * 0.113466930567937607) + (X_8 * 0.018847290606381961) + -0.306458405399606004), 0.0) * -0.059685017745032737) + (max(((X_0 * 0.287194094745330031) + (X_1 * -0.279329006877257702) + (X_2 * -0.27381666760090273) + (X_3 * -0.241196338354026901) + (X_4 * 0.166076860453970354) + (X_5 * 0.003947070874237735) + (X_6 * -0.079391976830132827) + (X_7 * -0.311101692329606716) + (X_8 * 0.028656916570530377) + -0.242226407222209617), 0.0) * -0.046964598953949693) + (max(((X_0 * 0.04404093390102809) + (X_1 * 0.223856941183437852) + (X_2 * 0.030174154656356367) + (X_3 * -0.093021470933494721) + (X_4 * -0.040972965799927652) + (X_5 * 0.134584475865453967) + (X_6 * 0.312199328391165765) + (X_7 * 0.040627871296072593) + (X_8 * -0.123070819674687693) + 0.158068620935378545), 0.0) * -0.00949230176884347) + (max(((X_0 * 0.309415963276349515) + (X_1 * 0.039481469238021816) + (X_2 * 0.15094441592481006) + (X_3 * 0.30522360340783411) + (X_4 * -0.229798563734669559) + (X_5 * -0.192960605209967856) + (X_6 * -0.20370062757883689) + (X_7 * -0.047763191941385397) + (X_8 * -0.266019895781817062) + -0.3239652657122854), 0.0) * 0.086203635808430462) + (max(((X_0 * 0.291655730227005694) + (X_1 * -0.211448651190053294) + (X_2 * 0.262759471678295109) + (X_3 * 0.250069844719772838) + (X_4 * -0.0381186790917451) + (X_5 * -0.146083546836047795) + (X_6 * -0.151529498387592332) + (X_7 * 0.201164755659322625) + (X_8 * 0.146160292641425327) + -0.046301663710338892), 0.0) * 0.095552962647780709) + (max(((X_0 * -0.184467825491839488) + (X_1 * -0.268161247711679374) + (X_2 * -0.153535151736396536) + (X_3 * -0.065596192568929845) + (X_4 * 0.21729520120637863) + (X_5 * -0.092332864688549343) + (X_6 * 0.018066462919213766) + (X_7 * -0.287370290741390033) + (X_8 * -0.222457450236703963) + -0.231100948340147661), 0.0) * 0.021596476162055234) + (max(((X_0 * 0.112387308333164793) + (X_1 * -0.164516529633275843) + (X_2 * 0.303715756573457785) + (X_3 * -0.115559064636028858) + (X_4 * -0.101279569170582118) + (X_5 * -0.312584846980395903) + (X_6 * -0.073897332022657303) + (X_7 * -0.187107831241006384) + (X_8 * 0.191742606049471742) + 0.219833682999539703), 0.0) * 0.096870702408133114) + (max(((X_0 * 0.272843083546418008) + (X_1 * -0.26331667301370465) + (X_2 * 0.228746460665943896) + (X_3 * 0.083017409074116422) + (X_4 * 0.2906669151723143) + (X_5 * 0.035447691086564703) + (X_6 * 0.312581653146865424) + (X_7 * -0.052006990099353001) + (X_8 * -0.238709163668962665) + 0.28076114529116375), 0.0) * 0.05751082454825035) + (max(((X_0 * 0.074020874970563255) + (X_1 * -0.022502229774748639) + (X_2 * 0.183897093057601213) + (X_3 * -0.287464703406070055) + (X_4 * -0.079254407166150287) + (X_5 * -0.330123738440344594) + (X_6 * 0.302019322984987182) + (X_7 * 0.060629658317428392) + (X_8 * -0.066123676240795071) + -0.168318244851325016), 0.0) * 0.057710761405758232) + (max(((X_0 * 0.117161478668860342) + (X_1 * -0.309380508435266599) + (X_2 * 0.166150746972853758) + (X_3 * 0.013701434090766906) + (X_4 * 0.141685721053067371) + (X_5 * -0.028880166693844356) + (X_6 * 0.260745424659842906) + (X_7 * -0.158065618750375059) + (X_8 * 0.095877003914591752) + 0.118188048960575609), 0.0) * -0.03306695210110433) + (max(((X_0 * -0.242158813559863934) + (X_1 * 0.121440841134675681) + (X_2 * 0.244934559694501341) + (X_3 * -0.317637615301534615) + (X_4 * -0.25005972927599035) + (X_5 * -0.215710382695643604) + (X_6 * 0.124190735382829098) + (X_7 * -0.059589490133065748) + (X_8 * 0.251407265038740835) + 0.08916513259423331), 0.0) * -0.014603565459802764) + 0.047833667018511383))
tff(formula_20,axiom,
'Y_0' = $sum($product(max($sum($product('X_0',$uminus(0.034143127336152712)),$sum($product('X_1',0.322824668200060227),$sum($product('X_2',0.091291052421442809),$sum($product('X_3',$uminus(0.012612789817531833)),$sum($product('X_4',0.273541493916837075),$sum($product('X_5',$uminus(0.150105792320639253)),$sum($product('X_6',$uminus(0.049406931293640266)),$sum($product('X_7',$uminus(0.21107752838875965)),$sum($product('X_8',0.277909149915428422),$uminus(0.019189099155314304)))))))))),0.0),$uminus(0.002546245018821197)),$sum($product(max($sum($product('X_0',0.135860462188255371),$sum($product('X_1',0.187969393886196101),$sum($product('X_2',0.174517671834989951),$sum($product('X_3',0.127635942676799008),$sum($product('X_4',$uminus(0.136994285692501105)),$sum($product('X_5',0.012365905796069943),$sum($product('X_6',$uminus(0.027014764654490264)),$sum($product('X_7',$uminus(0.305544519265200321)),$sum($product('X_8',$uminus(0.206852248891131074)),$uminus(0.314645004469935208)))))))))),0.0),0.081027244089196759),$sum($product(max($sum($product('X_0',$uminus(0.081020401392122687)),$sum($product('X_1',0.062490409237779099),$sum($product('X_2',0.111520586127630439),$sum($product('X_3',$uminus(0.213447096651937063)),$sum($product('X_4',0.132706362488796692),$sum($product('X_5',$uminus(0.261185283187217065)),$sum($product('X_6',0.00474527583528711),$sum($product('X_7',$uminus(0.06688270460651552)),$sum($product('X_8',$uminus(0.320470498630223033)),$uminus(0.190989000847826468)))))))))),0.0),0.120795879453134219),$sum($product(max($sum($product('X_0',0.138290117678506908),$sum($product('X_1',0.005330501640528451),$sum($product('X_2',$uminus(0.13333471971657565)),$sum($product('X_3',0.153277069170855151),$sum($product('X_4',0.193097250496935435),$sum($product('X_5',0.124353050256880426),$sum($product('X_6',$uminus(0.312998335768394587)),$sum($product('X_7',0.14582588668244395),$sum($product('X_8',0.017849845577707468),$uminus(0.207803467395465624)))))))))),0.0),$uminus(0.10301681682459779)),$sum($product(max($sum($product('X_0',0.25616055553271605),$sum($product('X_1',$uminus(0.03627032974016875)),$sum($product('X_2',$uminus(0.194452918074013159)),$sum($product('X_3',0.10008950100824493),$sum($product('X_4',0.321933544906211566),$sum($product('X_5',0.302676823386164806),$sum($product('X_6',0.282644938195837081),$sum($product('X_7',0.218166819191055239),$sum($product('X_8',0.061315114611943666),0.294909295927187565))))))))),0.0),0.119309649478056334),$sum($product(max($sum($product('X_0',$uminus(0.203907213010214777)),$sum($product('X_1',$uminus(0.329328844050836067)),$sum($product('X_2',$uminus(0.282209682521432303)),$sum($product('X_3',0.194481051286681639),$sum($product('X_4',0.223447381199474771),$sum($product('X_5',$uminus(0.130047140060396471)),$sum($product('X_6',0.258072855214746821),$sum($product('X_7',0.236670528410227232),$sum($product('X_8',0.219327984313435753),0.307309013280585186))))))))),0.0),$uminus(0.000471133946861574)),$sum($product(max($sum($product('X_0',$uminus(0.025392492262058697)),$sum($product('X_1',$uminus(0.260814592583792804)),$sum($product('X_2',$uminus(0.060464105023337156)),$sum($product('X_3',0.235580850968075406),$sum($product('X_4',0.013069063238517142),$sum($product('X_5',$uminus(0.196757326475462957)),$sum($product('X_6',0.028155879508867165),$sum($product('X_7',$uminus(0.181432604418310606)),$sum($product('X_8',0.089552351207647263),0.233953211619548462))))))))),0.0),$uminus(0.012643206083268216)),$sum($product(max($sum($product('X_0',$uminus(0.316000969071793147)),$sum($product('X_1',0.025263023662981166),$sum($product('X_2',0.177171946751012388),$sum($product('X_3',$uminus(0.035122639314649318)),$sum($product('X_4',$uminus(0.23096764293788713)),$sum($product('X_5',0.017100988871234346),$sum($product('X_6',$uminus(0.209560107747809532)),$sum($product('X_7',$uminus(0.026921531592388137)),$sum($product('X_8',$uminus(0.032723387475881827)),0.168724722506589486))))))))),0.0),0.112900602789428761),$sum($product(max($sum($product('X_0',0.001306859463930443),$sum($product('X_1',$uminus(0.32178678467757027)),$sum($product('X_2',$uminus(0.073177542048799837)),$sum($product('X_3',0.002394918508160371),$sum($product('X_4',0.093730698889344044),$sum($product('X_5',0.008752806231017984),$sum($product('X_6',$uminus(0.084064570826615143)),$sum($product('X_7',0.250900209655107453),$sum($product('X_8',0.022976222292577286),0.077232081109878559))))))))),0.0),0.082335754692696106),$sum($product(max($sum($product('X_0',0.194049225184143082),$sum($product('X_1',$uminus(0.022183735625062984)),$sum($product('X_2',$uminus(0.196724399739592354)),$sum($product('X_3',0.07635785513446619),$sum($product('X_4',$uminus(0.196322916482755933)),$sum($product('X_5',$uminus(0.288926766400791291)),$sum($product('X_6',0.213700339341032219),$sum($product('X_7',$uminus(0.253512613136544884)),$sum($product('X_8',0.231484855576049309),0.280058863303405625))))))))),0.0),$uminus(0.074458908043544547)),$sum($product(max($sum($product('X_0',0.317728685554186929),$sum($product('X_1',0.332150001647927684),$sum($product('X_2',$uminus(0.001259591758584755)),$sum($product('X_3',$uminus(0.207453820552864571)),$sum($product('X_4',0.005723595304183482),$sum($product('X_5',0.185428526068087629),$sum($product('X_6',0.054353623505082105),$sum($product('X_7',0.132946612680298504),$sum($product('X_8',0.011140036900155748),$uminus(0.209314307847249387)))))))))),0.0),$uminus(0.110400328569695477)),$sum($product(max($sum($product('X_0',$uminus(0.269304224359853461)),$sum($product('X_1',$uminus(0.310904419113500918)),$sum($product('X_2',0.32027709592926229),$sum($product('X_3',$uminus(0.200037762633937188)),$sum($product('X_4',$uminus(0.026191122665172317)),$sum($product('X_5',$uminus(0.042660660377485116)),$sum($product('X_6',$uminus(0.146275965076368142)),$sum($product('X_7',$uminus(0.305670262866760689)),$sum($product('X_8',0.322576996064118438),$uminus(0.183572002247813032)))))))))),0.0),0.066133019473005733),$sum($product(max($sum($product('X_0',0.136084741586379454),$sum($product('X_1',0.26228771638376186),$sum($product('X_2',$uminus(0.284171295665994417)),$sum($product('X_3',0.211831054834103749),$sum($product('X_4',0.285004999381932744),$sum($product('X_5',$uminus(0.007441424708356792)),$sum($product('X_6',$uminus(0.140284600003246995)),$sum($product('X_7',$uminus(0.207592415895373833)),$sum($product('X_8',0.27321519909354347),$uminus(0.207526152104757111)))))))))),0.0),0.038353156981341702),$sum($product(max($sum($product('X_0',$uminus(0.22841409680804925)),$sum($product('X_1',0.240551489683236974),$sum($product('X_2',0.312484269972083728),$sum($product('X_3',$uminus(0.181755643345508588)),$sum($product('X_4',0.030657116136170337),$sum($product('X_5',$uminus(0.055299675827487349)),$sum($product('X_6',$uminus(0.062998580523338621)),$sum($product('X_7',0.098231667492682917),$sum($product('X_8',$uminus(0.015349265026970815)),0.174413712522803299))))))))),0.0),$uminus(0.121499176770419159)),$sum($product(max($sum($product('X_0',0.326514337483990558),$sum($product('X_1',$uminus(0.139206653914812462)),$sum($product('X_2',$uminus(0.301944004088363971)),$sum($product('X_3',0.007220186513743954),$sum($product('X_4',$uminus(0.082554028749347141)),$sum($product('X_5',$uminus(0.040344607481459793)),$sum($product('X_6',$uminus(0.215478397144116013)),$sum($product('X_7',0.145783348414039393),$sum($product('X_8',$uminus(0.142290498498560514)),$uminus(0.21557124240865938)))))))))),0.0),$uminus(0.013954590494720587)),$sum($product(max($sum($product('X_0',$uminus(0.001976599008208513)),$sum($product('X_1',$uminus(0.057764032526161302)),$sum($product('X_2',0.159396263708995178),$sum($product('X_3',$uminus(0.183991541476796888)),$sum($product('X_4',0.142504183402018647),$sum($product('X_5',$uminus(0.238937927812336026)),$sum($product('X_6',$uminus(0.30402575884910954)),$sum($product('X_7',0.29491808364114086),$sum($product('X_8',0.054445412143243832),$uminus(0.170312927346704335)))))))))),0.0),$uminus(0.040915377252787377)),$sum($product(max($sum($product('X_0',$uminus(0.069437022416364014)),$sum($product('X_1',$uminus(0.00060254546898092)),$sum($product('X_2',0.247675182881536504),$sum($product('X_3',0.234314025579507035),$sum($product('X_4',$uminus(0.177673295141312471)),$sum($product('X_5',$uminus(0.332483963357472823)),$sum($product('X_6',$uminus(0.218038989896279178)),$sum($product('X_7',0.127363049893037317),$sum($product('X_8',$uminus(0.2086790536248469)),$uminus(0.187722099200903436)))))))))),0.0),$uminus(0.05295491168066957)),$sum($product(max($sum($product('X_0',0.324876735423139718),$sum($product('X_1',0.075982824387152592),$sum($product('X_2',$uminus(0.313261926183435957)),$sum($product('X_3',$uminus(0.209064108357157524)),$sum($product('X_4',$uminus(0.261535938731004891)),$sum($product('X_5',$uminus(0.234787129658768606)),$sum($product('X_6',0.112031404664260759),$sum($product('X_7',0.225008006173745667),$sum($product('X_8',0.140199347195911539),0.139447447171109518))))))))),0.0),$uminus(0.086948235574972305)),$sum($product(max($sum($product('X_0',0.202182439886614829),$sum($product('X_1',0.228470631117320078),$sum($product('X_2',0.074549186229916131),$sum($product('X_3',0.233422713721841812),$sum($product('X_4',0.131135712704656016),$sum($product('X_5',$uminus(0.326710062287342951)),$sum($product('X_6',0.012038286823084332),$sum($product('X_7',0.231618192292777969),$sum($product('X_8',0.000719113164345198),0.213277245603735233))))))))),0.0),$uminus(0.008697914681319946)),$sum($product(max($sum($product('X_0',0.28449527898218091),$sum($product('X_1',$uminus(0.081527175695953635)),$sum($product('X_2',$uminus(0.153930222701464642)),$sum($product('X_3',$uminus(0.186077449214199719)),$sum($product('X_4',$uminus(0.05936612416981174)),$sum($product('X_5',$uminus(0.154628465341259957)),$sum($product('X_6',$uminus(0.166498063888305931)),$sum($product('X_7',0.055266800565439478),$sum($product('X_8',$uminus(0.213197545634780383)),0.010205194890945457))))))))),0.0),$uminus(0.104668729123890775)),$sum($product(max($sum($product('X_0',$uminus(0.180816367347528484)),$sum($product('X_1',0.043531190359145266),$sum($product('X_2',$uminus(0.047619638831746636)),$sum($product('X_3',$uminus(0.058934638109038928)),$sum($product('X_4',$uminus(0.124666639609441937)),$sum($product('X_5',$uminus(0.318308163331019744)),$sum($product('X_6',0.193062520783280067),$sum($product('X_7',0.020418055017284109),$sum($product('X_8',0.060922472827523722),0.223360539691101423))))))))),0.0),$uminus(0.054775070975789514)),$sum($product(max($sum($product('X_0',0.134746472119233907),$sum($product('X_1',$uminus(0.217554078381223898)),$sum($product('X_2',$uminus(0.085730993819177093)),$sum($product('X_3',0.297521692708929308),$sum($product('X_4',0.063860554017248994),$sum($product('X_5',0.217082184168041759),$sum($product('X_6',$uminus(0.021045092732637605)),$sum($product('X_7',0.259811010052565072),$sum($product('X_8',0.200338555724555889),0.247229328571023033))))))))),0.0),$uminus(0.095070995295625293)),$sum($product(max($sum($product('X_0',0.203487277967640046),$sum($product('X_1',0.324424625686173973),$sum($product('X_2',$uminus(0.024662687002090788)),$sum($product('X_3',0.216277755365953894),$sum($product('X_4',0.163509105125114296),$sum($product('X_5',$uminus(0.034687792438270026)),$sum($product('X_6',0.206452845548049824),$sum($product('X_7',0.154282897842712208),$sum($product('X_8',$uminus(0.017555615896969023)),0.272302961557755852))))))))),0.0),0.10157507612563263),$sum($product(max($sum($product('X_0',$uminus(0.244290676854412331)),$sum($product('X_1',$uminus(0.204088781911439338)),$sum($product('X_2',$uminus(0.03882746711711399)),$sum($product('X_3',$uminus(0.097232792095546527)),$sum($product('X_4',$uminus(0.303174897657345899)),$sum($product('X_5',$uminus(0.051070311788715628)),$sum($product('X_6',0.149992479035335302),$sum($product('X_7',$uminus(0.102185614965710991)),$sum($product('X_8',$uminus(0.106519170243570216)),0.058597670613885988))))))))),0.0),0.089954845675315365),$sum($product(max($sum($product('X_0',0.012864262113814806),$sum($product('X_1',0.109069631915820031),$sum($product('X_2',0.101543371952154571),$sum($product('X_3',0.06799496124837745),$sum($product('X_4',$uminus(0.26445983492561137)),$sum($product('X_5',0.215833875445791301),$sum($product('X_6',0.272580780248200039),$sum($product('X_7',$uminus(0.039747643760278006)),$sum($product('X_8',$uminus(0.243825769939117892)),$uminus(0.123945865842741254)))))))))),0.0),0.057172696196788608),$sum($product(max($sum($product('X_0',$uminus(0.154837365313728936)),$sum($product('X_1',0.085840778969112019),$sum($product('X_2',0.165077967938471126),$sum($product('X_3',0.111848736690037587),$sum($product('X_4',$uminus(0.240612563426037041)),$sum($product('X_5',0.140637468751368289),$sum($product('X_6',$uminus(0.149768050036042905)),$sum($product('X_7',$uminus(0.283477350113733539)),$sum($product('X_8',0.073570979765799127),0.079922247453340256))))))))),0.0),0.013857350493885673),$sum($product(max($sum($product('X_0',$uminus(0.100199971469390775)),$sum($product('X_1',0.186120110641400827),$sum($product('X_2',0.049038095207454113),$sum($product('X_3',$uminus(0.196087530498076618)),$sum($product('X_4',0.08711796538252381),$sum($product('X_5',$uminus(0.101227855157801916)),$sum($product('X_6',0.158620075819161321),$sum($product('X_7',$uminus(0.146913672899774472)),$sum($product('X_8',$uminus(0.119082579355500373)),0.138895725711660534))))))))),0.0),$uminus(0.005384789761385123)),$sum($product(max($sum($product('X_0',0.180027772073166392),$sum($product('X_1',$uminus(0.103336431479241098)),$sum($product('X_2',$uminus(0.267316901673856466)),$sum($product('X_3',0.263656543687109834),$sum($product('X_4',0.332642570227415224),$sum($product('X_5',0.277967948182220759),$sum($product('X_6',0.30343956010141554),$sum($product('X_7',0.03447325941087459),$sum($product('X_8',0.125197865386826701),0.192506796333139885))))))))),0.0),$uminus(0.057310478208179444)),$sum($product(max($sum($product('X_0',$uminus(0.229596022939276084)),$sum($product('X_1',0.306162374571047058),$sum($product('X_2',$uminus(0.214349113239148403)),$sum($product('X_3',0.05827258272512098),$sum($product('X_4',0.131302065849309368),$sum($product('X_5',$uminus(0.271631521510831919)),$sum($product('X_6',$uminus(0.270260881180521384)),$sum($product('X_7',$uminus(0.202970959783648347)),$sum($product('X_8',0.179428170698139933),0.115665614154320362))))))))),0.0),$uminus(0.092476757020151706)),$sum($product(max($sum($product('X_0',0.194962600903016259),$sum($product('X_1',$uminus(0.17835559373673493)),$sum($product('X_2',$uminus(0.228962538545053329)),$sum($product('X_3',0.306214141164736053),$sum($product('X_4',0.257337107072608651),$sum($product('X_5',$uminus(0.299595911463449771)),$sum($product('X_6',0.089666024789417487),$sum($product('X_7',0.326462876291198911),$sum($product('X_8',$uminus(0.062301378541843311)),0.172234015205460611))))))))),0.0),$uminus(0.08196635417351622)),$sum($product(max($sum($product('X_0',0.255845191590086396),$sum($product('X_1',0.215495725762357482),$sum($product('X_2',$uminus(0.302097504773537306)),$sum($product('X_3',0.095845709494328524),$sum($product('X_4',$uminus(0.075426811348071776)),$sum($product('X_5',0.218624900118963683),$sum($product('X_6',0.26160805655982583),$sum($product('X_7',$uminus(0.212202541273525114)),$sum($product('X_8',$uminus(0.041523081831996933)),0.102324186276997908))))))))),0.0),$uminus(0.092317073009903355)),$sum($product(max($sum($product('X_0',0.30493330995168616),$sum($product('X_1',$uminus(0.122490486481055483)),$sum($product('X_2',0.174817256741448934),$sum($product('X_3',$uminus(0.202369269426108028)),$sum($product('X_4',$uminus(0.323621969121451081)),$sum($product('X_5',0.303508866087579043),$sum($product('X_6',$uminus(0.223769302030546458)),$sum($product('X_7',$uminus(0.27502503528423522)),$sum($product('X_8',0.129622404600985675),$uminus(0.253776462014690563)))))))))),0.0),0.033984477497181892),$sum($product(max($sum($product('X_0',0.269059547412644651),$sum($product('X_1',$uminus(0.005882567254681115)),$sum($product('X_2',$uminus(0.171353970135741607)),$sum($product('X_3',0.294037626949683328),$sum($product('X_4',$uminus(0.255251802687420648)),$sum($product('X_5',$uminus(0.009759698938691885)),$sum($product('X_6',0.180149176039681114),$sum($product('X_7',0.045388866190233079),$sum($product('X_8',$uminus(0.179760143010707252)),0.269823604538700745))))))))),0.0),0.08550415622620669),$sum($product(max($sum($product('X_0',$uminus(0.138558699684565634)),$sum($product('X_1',0.003660311035716235),$sum($product('X_2',$uminus(0.328144076991653155)),$sum($product('X_3',0.17711252434090502),$sum($product('X_4',0.086745978461675144),$sum($product('X_5',0.052468260508699016),$sum($product('X_6',0.051635532764924497),$sum($product('X_7',0.032455574507212981),$sum($product('X_8',$uminus(0.079164165185457769)),0.068544128415001238))))))))),0.0),$uminus(0.101034255172639253)),$sum($product(max($sum($product('X_0',$uminus(0.188430209592040626)),$sum($product('X_1',0.180982936820061113),$sum($product('X_2',0.124800571217657474),$sum($product('X_3',$uminus(0.054881926059530961)),$sum($product('X_4',$uminus(0.026456773114379717)),$sum($product('X_5',0.162595317059087197),$sum($product('X_6',0.049021975497793691),$sum($product('X_7',$uminus(0.246830321591287927)),$sum($product('X_8',0.232013828123107502),$uminus(0.062546264757998127)))))))))),0.0),$uminus(0.113667293596708435)),$sum($product(max($sum($product('X_0',0.040962088339393521),$sum($product('X_1',$uminus(0.254386604085368229)),$sum($product('X_2',$uminus(0.112672966314846829)),$sum($product('X_3',$uminus(0.159902546439000759)),$sum($product('X_4',$uminus(0.207701480823660051)),$sum($product('X_5',0.133165675227524982),$sum($product('X_6',0.193618244226427871),$sum($product('X_7',0.082613724983702452),$sum($product('X_8',0.322632448399385929),0.224209517678037373))))))))),0.0),0.114938780024844672),$sum($product(max($sum($product('X_0',$uminus(0.134886517018193708)),$sum($product('X_1',0.144899616770255646),$sum($product('X_2',$uminus(0.17980112071828272)),$sum($product('X_3',$uminus(0.267509492307719976)),$sum($product('X_4',$uminus(0.157528799514788709)),$sum($product('X_5',$uminus(0.079420419232439199)),$sum($product('X_6',$uminus(0.299465230679228367)),$sum($product('X_7',$uminus(0.125820656916256324)),$sum($product('X_8',0.019239984001792998),0.142229458135585185))))))))),0.0),$uminus(0.035320785296854867)),$sum($product(max($sum($product('X_0',$uminus(0.172346696671293709)),$sum($product('X_1',0.090451716164184959),$sum($product('X_2',$uminus(0.228793228787715741)),$sum($product('X_3',0.180997116632383548),$sum($product('X_4',0.290344111330939902),$sum($product('X_5',$uminus(0.234970994376170916)),$sum($product('X_6',0.005159751606115537),$sum($product('X_7',$uminus(0.155461525393435412)),$sum($product('X_8',$uminus(0.288046325238939249)),$uminus(0.070296844355285437)))))))))),0.0),$uminus(0.000302411809356834)),$sum($product(max($sum($product('X_0',$uminus(0.234997276198458949)),$sum($product('X_1',$uminus(0.172512713965825709)),$sum($product('X_2',0.114308047040828642),$sum($product('X_3',$uminus(0.063627448790975871)),$sum($product('X_4',$uminus(0.205794049922004174)),$sum($product('X_5',0.19287844644458868),$sum($product('X_6',$uminus(0.257664032924889597)),$sum($product('X_7',$uminus(0.233509914142561753)),$sum($product('X_8',0.267404797826638896),0.248418369896963032))))))))),0.0),$uminus(0.041750357136473404)),$sum($product(max($sum($product('X_0',0.296841143323539114),$sum($product('X_1',$uminus(0.012110575240900978)),$sum($product('X_2',$uminus(0.122779558396503508)),$sum($product('X_3',0.145965415302344859),$sum($product('X_4',0.115669853903047126),$sum($product('X_5',0.181260046623958171),$sum($product('X_6',0.176356841716120927),$sum($product('X_7',0.054758245250969895),$sum($product('X_8',0.066387541776141479),0.033378311133483385))))))))),0.0),0.097285514236117476),$sum($product(max($sum($product('X_0',$uminus(0.068127119880877884)),$sum($product('X_1',$uminus(0.193888759810902311)),$sum($product('X_2',$uminus(0.075010565817496266)),$sum($product('X_3',0.116013395273452391),$sum($product('X_4',0.197890889155673377),$sum($product('X_5',0.321385853477913319),$sum($product('X_6',0.050015661552153368),$sum($product('X_7',$uminus(0.054890782359229284)),$sum($product('X_8',0.258758291380532579),$uminus(0.143355802615697941)))))))))),0.0),$uminus(0.004404402516794192)),$sum($product(max($sum($product('X_0',$uminus(0.071997512442384004)),$sum($product('X_1',0.017303820158426297),$sum($product('X_2',0.091534845651731311),$sum($product('X_3',0.311279068800356329),$sum($product('X_4',$uminus(0.00312157907909616)),$sum($product('X_5',$uminus(0.188277000904065517)),$sum($product('X_6',$uminus(0.183479587316280945)),$sum($product('X_7',0.212372245445371421),$sum($product('X_8',$uminus(0.077162998727941579)),$uminus(0.223645418757847825)))))))))),0.0),0.015491725814317153),$sum($product(max($sum($product('X_0',$uminus(0.32243249625430126)),$sum($product('X_1',0.182253848897861837),$sum($product('X_2',$uminus(0.099368623456786598)),$sum($product('X_3',$uminus(0.156602428474534483)),$sum($product('X_4',0.030765939328599223),$sum($product('X_5',$uminus(0.026342715055112154)),$sum($product('X_6',0.000532788149621544),$sum($product('X_7',0.303861041761946782),$sum($product('X_8',0.265755190798946772),0.100146050819974963))))))))),0.0),0.001192439002770218),$sum($product(max($sum($product('X_0',$uminus(0.112545642928356893)),$sum($product('X_1',0.265866650798053328),$sum($product('X_2',0.015101151225212606),$sum($product('X_3',$uminus(0.317799591526125247)),$sum($product('X_4',$uminus(0.168903714240354275)),$sum($product('X_5',0.030188500593428369),$sum($product('X_6',0.061277558788815967),$sum($product('X_7',0.200866407017562254),$sum($product('X_8',$uminus(0.112371008406928929)),$uminus(0.079493482734081355)))))))))),0.0),$uminus(0.015260232367988874)),$sum($product(max($sum($product('X_0',$uminus(0.192154828636623531)),$sum($product('X_1',0.083979791049164365),$sum($product('X_2',0.159973530860791413),$sum($product('X_3',$uminus(0.265406610551946254)),$sum($product('X_4',0.287198912407206131),$sum($product('X_5',0.095627746140380554),$sum($product('X_6',$uminus(0.00994146969909776)),$sum($product('X_7',$uminus(0.219422562050552161)),$sum($product('X_8',$uminus(0.081085067577720604)),0.104747771083528063))))))))),0.0),$uminus(0.09459565655845989)),$sum($product(max($sum($product('X_0',$uminus(0.057039132055541286)),$sum($product('X_1',0.038985751754933406),$sum($product('X_2',$uminus(0.004944442157409357)),$sum($product('X_3',$uminus(0.15462525839770902)),$sum($product('X_4',$uminus(0.1398935031159593)),$sum($product('X_5',$uminus(0.061959641528152032)),$sum($product('X_6',0.098679300771940037),$sum($product('X_7',$uminus(0.201235020697894035)),$sum($product('X_8',$uminus(0.237594859082526227)),$uminus(0.158841501426246007)))))))))),0.0),$uminus(0.108315821817297875)),$sum($product(max($sum($product('X_0',0.331353170527205643),$sum($product('X_1',$uminus(0.288645365007353272)),$sum($product('X_2',0.223956278926402741),$sum($product('X_3',0.279170663263683283),$sum($product('X_4',0.017978724577996319),$sum($product('X_5',$uminus(0.250013034963560865)),$sum($product('X_6',0.098807821234157156),$sum($product('X_7',0.258776815881270383),$sum($product('X_8',0.152988470579232594),0.28246081276552143))))))))),0.0),0.003632176971928025),$sum($product(max($sum($product('X_0',$uminus(0.100883845060276311)),$sum($product('X_1',0.046212140463826712),$sum($product('X_2',$uminus(0.026600669905651519)),$sum($product('X_3',0.142320732212770695),$sum($product('X_4',0.072733698806154878),$sum($product('X_5',0.197196887480299343),$sum($product('X_6',0.237120144257248089),$sum($product('X_7',$uminus(0.166327692927533299)),$sum($product('X_8',$uminus(0.078131387240757411)),$uminus(0.293417736964490861)))))))))),0.0),0.11352795843340871),$sum($product(max($sum($product('X_0',0.294400522037719437),$sum($product('X_1',0.082094261162431514),$sum($product('X_2',0.101918067411788049),$sum($product('X_3',0.17357922076579041),$sum($product('X_4',0.114082861901367405),$sum($product('X_5',$uminus(0.311032034544396929)),$sum($product('X_6',0.258029579372313467),$sum($product('X_7',0.145657792087877658),$sum($product('X_8',$uminus(0.033975658190385893)),0.194899911587433305))))))))),0.0),$uminus(0.049073925423291309)),$sum($product(max($sum($product('X_0',0.034313476891573602),$sum($product('X_1',$uminus(0.189736665978239627)),$sum($product('X_2',0.098474573164286039),$sum($product('X_3',0.220418718662632351),$sum($product('X_4',0.03836653204063839),$sum($product('X_5',0.279710695915403817),$sum($product('X_6',0.14410430753399317),$sum($product('X_7',0.204156618335651407),$sum($product('X_8',0.176473915501038803),$uminus(0.03827183418778396)))))))))),0.0),$uminus(0.100382386321973965)),$sum($product(max($sum($product('X_0',0.00869382371014682),$sum($product('X_1',$uminus(0.310492767426873872)),$sum($product('X_2',0.117116910196331914),$sum($product('X_3',0.169087657846020811),$sum($product('X_4',$uminus(0.273335058913078577)),$sum($product('X_5',$uminus(0.000683592328365401)),$sum($product('X_6',0.139512227022986102),$sum($product('X_7',$uminus(0.313799159812941153)),$sum($product('X_8',$uminus(0.196166996347198946)),0.236750714424111497))))))))),0.0),$uminus(0.00867737418549025)),$sum($product(max($sum($product('X_0',0.137861025679069715),$sum($product('X_1',$uminus(0.024667890831123473)),$sum($product('X_2',$uminus(0.315714844767212732)),$sum($product('X_3',0.237047096266294222),$sum($product('X_4',0.202101116810822823),$sum($product('X_5',$uminus(0.020405610795288631)),$sum($product('X_6',0.223248306677427399),$sum($product('X_7',0.166427221032260431),$sum($product('X_8',0.322898701032060254),0.085041015223344729))))))))),0.0),$uminus(0.071289808274688116)),$sum($product(max($sum($product('X_0',0.063704153901590399),$sum($product('X_1',0.084893455136697493),$sum($product('X_2',0.162022423603656263),$sum($product('X_3',$uminus(0.026069359722939833)),$sum($product('X_4',$uminus(0.103610576532342291)),$sum($product('X_5',0.247462072588003845),$sum($product('X_6',0.235604458158232999),$sum($product('X_7',0.094778590268327412),$sum($product('X_8',0.317884709780666685),$uminus(0.259110365198896853)))))))))),0.0),0.086383813374095925),$sum($product(max($sum($product('X_0',0.157051962420222013),$sum($product('X_1',0.02119912918435074),$sum($product('X_2',$uminus(0.144567654546317315)),$sum($product('X_3',$uminus(0.120485782181390416)),$sum($product('X_4',0.245385692300038649),$sum($product('X_5',$uminus(0.12013008718360596)),$sum($product('X_6',$uminus(0.264054168644354381)),$sum($product('X_7',0.113466930567937607),$sum($product('X_8',0.018847290606381961),$uminus(0.306458405399606004)))))))))),0.0),$uminus(0.059685017745032737)),$sum($product(max($sum($product('X_0',0.287194094745330031),$sum($product('X_1',$uminus(0.279329006877257702)),$sum($product('X_2',$uminus(0.27381666760090273)),$sum($product('X_3',$uminus(0.241196338354026901)),$sum($product('X_4',0.166076860453970354),$sum($product('X_5',0.003947070874237735),$sum($product('X_6',$uminus(0.079391976830132827)),$sum($product('X_7',$uminus(0.311101692329606716)),$sum($product('X_8',0.028656916570530377),$uminus(0.242226407222209617)))))))))),0.0),$uminus(0.046964598953949693)),$sum($product(max($sum($product('X_0',0.04404093390102809),$sum($product('X_1',0.223856941183437852),$sum($product('X_2',0.030174154656356367),$sum($product('X_3',$uminus(0.093021470933494721)),$sum($product('X_4',$uminus(0.040972965799927652)),$sum($product('X_5',0.134584475865453967),$sum($product('X_6',0.312199328391165765),$sum($product('X_7',0.040627871296072593),$sum($product('X_8',$uminus(0.123070819674687693)),0.158068620935378545))))))))),0.0),$uminus(0.00949230176884347)),$sum($product(max($sum($product('X_0',0.309415963276349515),$sum($product('X_1',0.039481469238021816),$sum($product('X_2',0.15094441592481006),$sum($product('X_3',0.30522360340783411),$sum($product('X_4',$uminus(0.229798563734669559)),$sum($product('X_5',$uminus(0.192960605209967856)),$sum($product('X_6',$uminus(0.20370062757883689)),$sum($product('X_7',$uminus(0.047763191941385397)),$sum($product('X_8',$uminus(0.266019895781817062)),$uminus(0.3239652657122854)))))))))),0.0),0.086203635808430462),$sum($product(max($sum($product('X_0',0.291655730227005694),$sum($product('X_1',$uminus(0.211448651190053294)),$sum($product('X_2',0.262759471678295109),$sum($product('X_3',0.250069844719772838),$sum($product('X_4',$uminus(0.0381186790917451)),$sum($product('X_5',$uminus(0.146083546836047795)),$sum($product('X_6',$uminus(0.151529498387592332)),$sum($product('X_7',0.201164755659322625),$sum($product('X_8',0.146160292641425327),$uminus(0.046301663710338892)))))))))),0.0),0.095552962647780709),$sum($product(max($sum($product('X_0',$uminus(0.184467825491839488)),$sum($product('X_1',$uminus(0.268161247711679374)),$sum($product('X_2',$uminus(0.153535151736396536)),$sum($product('X_3',$uminus(0.065596192568929845)),$sum($product('X_4',0.21729520120637863),$sum($product('X_5',$uminus(0.092332864688549343)),$sum($product('X_6',0.018066462919213766),$sum($product('X_7',$uminus(0.287370290741390033)),$sum($product('X_8',$uminus(0.222457450236703963)),$uminus(0.231100948340147661)))))))))),0.0),0.021596476162055234),$sum($product(max($sum($product('X_0',0.112387308333164793),$sum($product('X_1',$uminus(0.164516529633275843)),$sum($product('X_2',0.303715756573457785),$sum($product('X_3',$uminus(0.115559064636028858)),$sum($product('X_4',$uminus(0.101279569170582118)),$sum($product('X_5',$uminus(0.312584846980395903)),$sum($product('X_6',$uminus(0.073897332022657303)),$sum($product('X_7',$uminus(0.187107831241006384)),$sum($product('X_8',0.191742606049471742),0.219833682999539703))))))))),0.0),0.096870702408133114),$sum($product(max($sum($product('X_0',0.272843083546418008),$sum($product('X_1',$uminus(0.26331667301370465)),$sum($product('X_2',0.228746460665943896),$sum($product('X_3',0.083017409074116422),$sum($product('X_4',0.2906669151723143),$sum($product('X_5',0.035447691086564703),$sum($product('X_6',0.312581653146865424),$sum($product('X_7',$uminus(0.052006990099353001)),$sum($product('X_8',$uminus(0.238709163668962665)),0.28076114529116375))))))))),0.0),0.05751082454825035),$sum($product(max($sum($product('X_0',0.074020874970563255),$sum($product('X_1',$uminus(0.022502229774748639)),$sum($product('X_2',0.183897093057601213),$sum($product('X_3',$uminus(0.287464703406070055)),$sum($product('X_4',$uminus(0.079254407166150287)),$sum($product('X_5',$uminus(0.330123738440344594)),$sum($product('X_6',0.302019322984987182),$sum($product('X_7',0.060629658317428392),$sum($product('X_8',$uminus(0.066123676240795071)),$uminus(0.168318244851325016)))))))))),0.0),0.057710761405758232),$sum($product(max($sum($product('X_0',0.117161478668860342),$sum($product('X_1',$uminus(0.309380508435266599)),$sum($product('X_2',0.166150746972853758),$sum($product('X_3',0.013701434090766906),$sum($product('X_4',0.141685721053067371),$sum($product('X_5',$uminus(0.028880166693844356)),$sum($product('X_6',0.260745424659842906),$sum($product('X_7',$uminus(0.158065618750375059)),$sum($product('X_8',0.095877003914591752),0.118188048960575609))))))))),0.0),$uminus(0.03306695210110433)),$sum($product(max($sum($product('X_0',$uminus(0.242158813559863934)),$sum($product('X_1',0.121440841134675681),$sum($product('X_2',0.244934559694501341),$sum($product('X_3',$uminus(0.317637615301534615)),$sum($product('X_4',$uminus(0.25005972927599035)),$sum($product('X_5',$uminus(0.215710382695643604)),$sum($product('X_6',0.124190735382829098),$sum($product('X_7',$uminus(0.059589490133065748)),$sum($product('X_8',0.251407265038740835),0.08916513259423331))))))))),0.0),$uminus(0.014603565459802764)),0.047833667018511383)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ).
%---(Y_1 = ((max(((X_0 * -0.034143127336152712) + (X_1 * 0.322824668200060227) + (X_2 * 0.091291052421442809) + (X_3 * -0.012612789817531833) + (X_4 * 0.273541493916837075) + (X_5 * -0.150105792320639253) + (X_6 * -0.049406931293640266) + (X_7 * -0.21107752838875965) + (X_8 * 0.277909149915428422) + -0.019189099155314304), 0.0) * -0.073998450024932688) + (max(((X_0 * 0.135860462188255371) + (X_1 * 0.187969393886196101) + (X_2 * 0.174517671834989951) + (X_3 * 0.127635942676799008) + (X_4 * -0.136994285692501105) + (X_5 * 0.012365905796069943) + (X_6 * -0.027014764654490264) + (X_7 * -0.305544519265200321) + (X_8 * -0.206852248891131074) + -0.314645004469935208), 0.0) * -0.064513743407656948) + (max(((X_0 * -0.081020401392122687) + (X_1 * 0.062490409237779099) + (X_2 * 0.111520586127630439) + (X_3 * -0.213447096651937063) + (X_4 * 0.132706362488796692) + (X_5 * -0.261185283187217065) + (X_6 * 0.00474527583528711) + (X_7 * -0.06688270460651552) + (X_8 * -0.320470498630223033) + -0.190989000847826468), 0.0) * -0.026160320859166641) + (max(((X_0 * 0.138290117678506908) + (X_1 * 0.005330501640528451) + (X_2 * -0.13333471971657565) + (X_3 * 0.153277069170855151) + (X_4 * 0.193097250496935435) + (X_5 * 0.124353050256880426) + (X_6 * -0.312998335768394587) + (X_7 * 0.14582588668244395) + (X_8 * 0.017849845577707468) + -0.207803467395465624), 0.0) * 0.081871644668587457) + (max(((X_0 * 0.25616055553271605) + (X_1 * -0.03627032974016875) + (X_2 * -0.194452918074013159) + (X_3 * 0.10008950100824493) + (X_4 * 0.321933544906211566) + (X_5 * 0.302676823386164806) + (X_6 * 0.282644938195837081) + (X_7 * 0.218166819191055239) + (X_8 * 0.061315114611943666) + 0.294909295927187565), 0.0) * -0.001332491252833162) + (max(((X_0 * -0.203907213010214777) + (X_1 * -0.329328844050836067) + (X_2 * -0.282209682521432303) + (X_3 * 0.194481051286681639) + (X_4 * 0.223447381199474771) + (X_5 * -0.130047140060396471) + (X_6 * 0.258072855214746821) + (X_7 * 0.236670528410227232) + (X_8 * 0.219327984313435753) + 0.307309013280585186), 0.0) * 0.044857164486815815) + (max(((X_0 * -0.025392492262058697) + (X_1 * -0.260814592583792804) + (X_2 * -0.060464105023337156) + (X_3 * 0.235580850968075406) + (X_4 * 0.013069063238517142) + (X_5 * -0.196757326475462957) + (X_6 * 0.028155879508867165) + (X_7 * -0.181432604418310606) + (X_8 * 0.089552351207647263) + 0.233953211619548462), 0.0) * -0.028382197281112381) + (max(((X_0 * -0.316000969071793147) + (X_1 * 0.025263023662981166) + (X_2 * 0.177171946751012388) + (X_3 * -0.035122639314649318) + (X_4 * -0.23096764293788713) + (X_5 * 0.017100988871234346) + (X_6 * -0.209560107747809532) + (X_7 * -0.026921531592388137) + (X_8 * -0.032723387475881827) + 0.168724722506589486), 0.0) * -0.052279107638462302) + (max(((X_0 * 0.001306859463930443) + (X_1 * -0.32178678467757027) + (X_2 * -0.073177542048799837) + (X_3 * 0.002394918508160371) + (X_4 * 0.093730698889344044) + (X_5 * 0.008752806231017984) + (X_6 * -0.084064570826615143) + (X_7 * 0.250900209655107453) + (X_8 * 0.022976222292577286) + 0.077232081109878559), 0.0) * 0.050512184504869773) + (max(((X_0 * 0.194049225184143082) + (X_1 * -0.022183735625062984) + (X_2 * -0.196724399739592354) + (X_3 * 0.07635785513446619) + (X_4 * -0.196322916482755933) + (X_5 * -0.288926766400791291) + (X_6 * 0.213700339341032219) + (X_7 * -0.253512613136544884) + (X_8 * 0.231484855576049309) + 0.280058863303405625), 0.0) * -0.066188932067793194) + (max(((X_0 * 0.317728685554186929) + (X_1 * 0.332150001647927684) + (X_2 * -0.001259591758584755) + (X_3 * -0.207453820552864571) + (X_4 * 0.005723595304183482) + (X_5 * 0.185428526068087629) + (X_6 * 0.054353623505082105) + (X_7 * 0.132946612680298504) + (X_8 * 0.011140036900155748) + -0.209314307847249387), 0.0) * -0.018565609615204703) + (max(((X_0 * -0.269304224359853461) + (X_1 * -0.310904419113500918) + (X_2 * 0.32027709592926229) + (X_3 * -0.200037762633937188) + (X_4 * -0.026191122665172317) + (X_5 * -0.042660660377485116) + (X_6 * -0.146275965076368142) + (X_7 * -0.305670262866760689) + (X_8 * 0.322576996064118438) + -0.183572002247813032), 0.0) * -0.114746509627626225) + (max(((X_0 * 0.136084741586379454) + (X_1 * 0.26228771638376186) + (X_2 * -0.284171295665994417) + (X_3 * 0.211831054834103749) + (X_4 * 0.285004999381932744) + (X_5 * -0.007441424708356792) + (X_6 * -0.140284600003246995) + (X_7 * -0.207592415895373833) + (X_8 * 0.27321519909354347) + -0.207526152104757111), 0.0) * 0.068807719524015376) + (max(((X_0 * -0.22841409680804925) + (X_1 * 0.240551489683236974) + (X_2 * 0.312484269972083728) + (X_3 * -0.181755643345508588) + (X_4 * 0.030657116136170337) + (X_5 * -0.055299675827487349) + (X_6 * -0.062998580523338621) + (X_7 * 0.098231667492682917) + (X_8 * -0.015349265026970815) + 0.174413712522803299), 0.0) * 0.040671257241023412) + (max(((X_0 * 0.326514337483990558) + (X_1 * -0.139206653914812462) + (X_2 * -0.301944004088363971) + (X_3 * 0.007220186513743954) + (X_4 * -0.082554028749347141) + (X_5 * -0.040344607481459793) + (X_6 * -0.215478397144116013) + (X_7 * 0.145783348414039393) + (X_8 * -0.142290498498560514) + -0.21557124240865938), 0.0) * -0.040973937252329506) + (max(((X_0 * -0.001976599008208513) + (X_1 * -0.057764032526161302) + (X_2 * 0.159396263708995178) + (X_3 * -0.183991541476796888) + (X_4 * 0.142504183402018647) + (X_5 * -0.238937927812336026) + (X_6 * -0.30402575884910954) + (X_7 * 0.29491808364114086) + (X_8 * 0.054445412143243832) + -0.170312927346704335), 0.0) * 0.054472072806984684) + (max(((X_0 * -0.069437022416364014) + (X_1 * -0.00060254546898092) + (X_2 * 0.247675182881536504) + (X_3 * 0.234314025579507035) + (X_4 * -0.177673295141312471) + (X_5 * -0.332483963357472823) + (X_6 * -0.218038989896279178) + (X_7 * 0.127363049893037317) + (X_8 * -0.2086790536248469) + -0.187722099200903436), 0.0) * 0.024969370219846659) + (max(((X_0 * 0.324876735423139718) + (X_1 * 0.075982824387152592) + (X_2 * -0.313261926183435957) + (X_3 * -0.209064108357157524) + (X_4 * -0.261535938731004891) + (X_5 * -0.234787129658768606) + (X_6 * 0.112031404664260759) + (X_7 * 0.225008006173745667) + (X_8 * 0.140199347195911539) + 0.139447447171109518), 0.0) * -0.080517183573391909) + (max(((X_0 * 0.202182439886614829) + (X_1 * 0.228470631117320078) + (X_2 * 0.074549186229916131) + (X_3 * 0.233422713721841812) + (X_4 * 0.131135712704656016) + (X_5 * -0.326710062287342951) + (X_6 * 0.012038286823084332) + (X_7 * 0.231618192292777969) + (X_8 * 0.000719113164345198) + 0.213277245603735233), 0.0) * -0.110508536016433095) + (max(((X_0 * 0.28449527898218091) + (X_1 * -0.081527175695953635) + (X_2 * -0.153930222701464642) + (X_3 * -0.186077449214199719) + (X_4 * -0.05936612416981174) + (X_5 * -0.154628465341259957) + (X_6 * -0.166498063888305931) + (X_7 * 0.055266800565439478) + (X_8 * -0.213197545634780383) + 0.010205194890945457), 0.0) * 0.079700459465058576) + (max(((X_0 * -0.180816367347528484) + (X_1 * 0.043531190359145266) + (X_2 * -0.047619638831746636) + (X_3 * -0.058934638109038928) + (X_4 * -0.124666639609441937) + (X_5 * -0.318308163331019744) + (X_6 * 0.193062520783280067) + (X_7 * 0.020418055017284109) + (X_8 * 0.060922472827523722) + 0.223360539691101423), 0.0) * -0.117348884884679872) + (max(((X_0 * 0.134746472119233907) + (X_1 * -0.217554078381223898) + (X_2 * -0.085730993819177093) + (X_3 * 0.297521692708929308) + (X_4 * 0.063860554017248994) + (X_5 * 0.217082184168041759) + (X_6 * -0.021045092732637605) + (X_7 * 0.259811010052565072) + (X_8 * 0.200338555724555889) + 0.247229328571023033), 0.0) * -0.072948417866398663) + (max(((X_0 * 0.203487277967640046) + (X_1 * 0.324424625686173973) + (X_2 * -0.024662687002090788) + (X_3 * 0.216277755365953894) + (X_4 * 0.163509105125114296) + (X_5 * -0.034687792438270026) + (X_6 * 0.206452845548049824) + (X_7 * 0.154282897842712208) + (X_8 * -0.017555615896969023) + 0.272302961557755852), 0.0) * -0.07655439511301329) + (max(((X_0 * -0.244290676854412331) + (X_1 * -0.204088781911439338) + (X_2 * -0.03882746711711399) + (X_3 * -0.097232792095546527) + (X_4 * -0.303174897657345899) + (X_5 * -0.051070311788715628) + (X_6 * 0.149992479035335302) + (X_7 * -0.102185614965710991) + (X_8 * -0.106519170243570216) + 0.058597670613885988), 0.0) * -0.040583535831473089) + (max(((X_0 * 0.012864262113814806) + (X_1 * 0.109069631915820031) + (X_2 * 0.101543371952154571) + (X_3 * 0.06799496124837745) + (X_4 * -0.26445983492561137) + (X_5 * 0.215833875445791301) + (X_6 * 0.272580780248200039) + (X_7 * -0.039747643760278006) + (X_8 * -0.243825769939117892) + -0.123945865842741254), 0.0) * 0.040847410791384653) + (max(((X_0 * -0.154837365313728936) + (X_1 * 0.085840778969112019) + (X_2 * 0.165077967938471126) + (X_3 * 0.111848736690037587) + (X_4 * -0.240612563426037041) + (X_5 * 0.140637468751368289) + (X_6 * -0.149768050036042905) + (X_7 * -0.283477350113733539) + (X_8 * 0.073570979765799127) + 0.079922247453340256), 0.0) * 0.107608377126927612) + (max(((X_0 * -0.100199971469390775) + (X_1 * 0.186120110641400827) + (X_2 * 0.049038095207454113) + (X_3 * -0.196087530498076618) + (X_4 * 0.08711796538252381) + (X_5 * -0.101227855157801916) + (X_6 * 0.158620075819161321) + (X_7 * -0.146913672899774472) + (X_8 * -0.119082579355500373) + 0.138895725711660534), 0.0) * 0.111136415946718747) + (max(((X_0 * 0.180027772073166392) + (X_1 * -0.103336431479241098) + (X_2 * -0.267316901673856466) + (X_3 * 0.263656543687109834) + (X_4 * 0.332642570227415224) + (X_5 * 0.277967948182220759) + (X_6 * 0.30343956010141554) + (X_7 * 0.03447325941087459) + (X_8 * 0.125197865386826701) + 0.192506796333139885), 0.0) * 0.099246897649233917) + (max(((X_0 * -0.229596022939276084) + (X_1 * 0.306162374571047058) + (X_2 * -0.214349113239148403) + (X_3 * 0.05827258272512098) + (X_4 * 0.131302065849309368) + (X_5 * -0.271631521510831919) + (X_6 * -0.270260881180521384) + (X_7 * -0.202970959783648347) + (X_8 * 0.179428170698139933) + 0.115665614154320362), 0.0) * 0.040522696972192768) + (max(((X_0 * 0.194962600903016259) + (X_1 * -0.17835559373673493) + (X_2 * -0.228962538545053329) + (X_3 * 0.306214141164736053) + (X_4 * 0.257337107072608651) + (X_5 * -0.299595911463449771) + (X_6 * 0.089666024789417487) + (X_7 * 0.326462876291198911) + (X_8 * -0.062301378541843311) + 0.172234015205460611), 0.0) * 0.074811979072499146) + (max(((X_0 * 0.255845191590086396) + (X_1 * 0.215495725762357482) + (X_2 * -0.302097504773537306) + (X_3 * 0.095845709494328524) + (X_4 * -0.075426811348071776) + (X_5 * 0.218624900118963683) + (X_6 * 0.26160805655982583) + (X_7 * -0.212202541273525114) + (X_8 * -0.041523081831996933) + 0.102324186276997908), 0.0) * -0.083572412646659655) + (max(((X_0 * 0.30493330995168616) + (X_1 * -0.122490486481055483) + (X_2 * 0.174817256741448934) + (X_3 * -0.202369269426108028) + (X_4 * -0.323621969121451081) + (X_5 * 0.303508866087579043) + (X_6 * -0.223769302030546458) + (X_7 * -0.27502503528423522) + (X_8 * 0.129622404600985675) + -0.253776462014690563), 0.0) * -0.035980293323670226) + (max(((X_0 * 0.269059547412644651) + (X_1 * -0.005882567254681115) + (X_2 * -0.171353970135741607) + (X_3 * 0.294037626949683328) + (X_4 * -0.255251802687420648) + (X_5 * -0.009759698938691885) + (X_6 * 0.180149176039681114) + (X_7 * 0.045388866190233079) + (X_8 * -0.179760143010707252) + 0.269823604538700745), 0.0) * -0.093401995853832742) + (max(((X_0 * -0.138558699684565634) + (X_1 * 0.003660311035716235) + (X_2 * -0.328144076991653155) + (X_3 * 0.17711252434090502) + (X_4 * 0.086745978461675144) + (X_5 * 0.052468260508699016) + (X_6 * 0.051635532764924497) + (X_7 * 0.032455574507212981) + (X_8 * -0.079164165185457769) + 0.068544128415001238), 0.0) * 0.014988998746798182) + (max(((X_0 * -0.188430209592040626) + (X_1 * 0.180982936820061113) + (X_2 * 0.124800571217657474) + (X_3 * -0.054881926059530961) + (X_4 * -0.026456773114379717) + (X_5 * 0.162595317059087197) + (X_6 * 0.049021975497793691) + (X_7 * -0.246830321591287927) + (X_8 * 0.232013828123107502) + -0.062546264757998127), 0.0) * 0.09899955044625447) + (max(((X_0 * 0.040962088339393521) + (X_1 * -0.254386604085368229) + (X_2 * -0.112672966314846829) + (X_3 * -0.159902546439000759) + (X_4 * -0.207701480823660051) + (X_5 * 0.133165675227524982) + (X_6 * 0.193618244226427871) + (X_7 * 0.082613724983702452) + (X_8 * 0.322632448399385929) + 0.224209517678037373), 0.0) * 0.117837399943200416) + (max(((X_0 * -0.134886517018193708) + (X_1 * 0.144899616770255646) + (X_2 * -0.17980112071828272) + (X_3 * -0.267509492307719976) + (X_4 * -0.157528799514788709) + (X_5 * -0.079420419232439199) + (X_6 * -0.299465230679228367) + (X_7 * -0.125820656916256324) + (X_8 * 0.019239984001792998) + 0.142229458135585185), 0.0) * 0.019122155497841964) + (max(((X_0 * -0.172346696671293709) + (X_1 * 0.090451716164184959) + (X_2 * -0.228793228787715741) + (X_3 * 0.180997116632383548) + (X_4 * 0.290344111330939902) + (X_5 * -0.234970994376170916) + (X_6 * 0.005159751606115537) + (X_7 * -0.155461525393435412) + (X_8 * -0.288046325238939249) + -0.070296844355285437), 0.0) * -0.11907840381428797) + (max(((X_0 * -0.234997276198458949) + (X_1 * -0.172512713965825709) + (X_2 * 0.114308047040828642) + (X_3 * -0.063627448790975871) + (X_4 * -0.205794049922004174) + (X_5 * 0.19287844644458868) + (X_6 * -0.257664032924889597) + (X_7 * -0.233509914142561753) + (X_8 * 0.267404797826638896) + 0.248418369896963032), 0.0) * -0.057272059559953431) + (max(((X_0 * 0.296841143323539114) + (X_1 * -0.012110575240900978) + (X_2 * -0.122779558396503508) + (X_3 * 0.145965415302344859) + (X_4 * 0.115669853903047126) + (X_5 * 0.181260046623958171) + (X_6 * 0.176356841716120927) + (X_7 * 0.054758245250969895) + (X_8 * 0.066387541776141479) + 0.033378311133483385), 0.0) * -0.088314638651521005) + (max(((X_0 * -0.068127119880877884) + (X_1 * -0.193888759810902311) + (X_2 * -0.075010565817496266) + (X_3 * 0.116013395273452391) + (X_4 * 0.197890889155673377) + (X_5 * 0.321385853477913319) + (X_6 * 0.050015661552153368) + (X_7 * -0.054890782359229284) + (X_8 * 0.258758291380532579) + -0.143355802615697941), 0.0) * 0.042882380581039575) + (max(((X_0 * -0.071997512442384004) + (X_1 * 0.017303820158426297) + (X_2 * 0.091534845651731311) + (X_3 * 0.311279068800356329) + (X_4 * -0.00312157907909616) + (X_5 * -0.188277000904065517) + (X_6 * -0.183479587316280945) + (X_7 * 0.212372245445371421) + (X_8 * -0.077162998727941579) + -0.223645418757847825), 0.0) * 0.00608997096424313) + (max(((X_0 * -0.32243249625430126) + (X_1 * 0.182253848897861837) + (X_2 * -0.099368623456786598) + (X_3 * -0.156602428474534483) + (X_4 * 0.030765939328599223) + (X_5 * -0.026342715055112154) + (X_6 * 0.000532788149621544) + (X_7 * 0.303861041761946782) + (X_8 * 0.265755190798946772) + 0.100146050819974963), 0.0) * -0.09913956730640347) + (max(((X_0 * -0.112545642928356893) + (X_1 * 0.265866650798053328) + (X_2 * 0.015101151225212606) + (X_3 * -0.317799591526125247) + (X_4 * -0.168903714240354275) + (X_5 * 0.030188500593428369) + (X_6 * 0.061277558788815967) + (X_7 * 0.200866407017562254) + (X_8 * -0.112371008406928929) + -0.079493482734081355), 0.0) * -0.062563463103772948) + (max(((X_0 * -0.192154828636623531) + (X_1 * 0.083979791049164365) + (X_2 * 0.159973530860791413) + (X_3 * -0.265406610551946254) + (X_4 * 0.287198912407206131) + (X_5 * 0.095627746140380554) + (X_6 * -0.00994146969909776) + (X_7 * -0.219422562050552161) + (X_8 * -0.081085067577720604) + 0.104747771083528063), 0.0) * 0.028402193751599886) + (max(((X_0 * -0.057039132055541286) + (X_1 * 0.038985751754933406) + (X_2 * -0.004944442157409357) + (X_3 * -0.15462525839770902) + (X_4 * -0.1398935031159593) + (X_5 * -0.061959641528152032) + (X_6 * 0.098679300771940037) + (X_7 * -0.201235020697894035) + (X_8 * -0.237594859082526227) + -0.158841501426246007), 0.0) * -0.114140016983423964) + (max(((X_0 * 0.331353170527205643) + (X_1 * -0.288645365007353272) + (X_2 * 0.223956278926402741) + (X_3 * 0.279170663263683283) + (X_4 * 0.017978724577996319) + (X_5 * -0.250013034963560865) + (X_6 * 0.098807821234157156) + (X_7 * 0.258776815881270383) + (X_8 * 0.152988470579232594) + 0.28246081276552143), 0.0) * -0.079083806413413033) + (max(((X_0 * -0.100883845060276311) + (X_1 * 0.046212140463826712) + (X_2 * -0.026600669905651519) + (X_3 * 0.142320732212770695) + (X_4 * 0.072733698806154878) + (X_5 * 0.197196887480299343) + (X_6 * 0.237120144257248089) + (X_7 * -0.166327692927533299) + (X_8 * -0.078131387240757411) + -0.293417736964490861), 0.0) * 0.069237546080712919) + (max(((X_0 * 0.294400522037719437) + (X_1 * 0.082094261162431514) + (X_2 * 0.101918067411788049) + (X_3 * 0.17357922076579041) + (X_4 * 0.114082861901367405) + (X_5 * -0.311032034544396929) + (X_6 * 0.258029579372313467) + (X_7 * 0.145657792087877658) + (X_8 * -0.033975658190385893) + 0.194899911587433305), 0.0) * -0.092256427149248615) + (max(((X_0 * 0.034313476891573602) + (X_1 * -0.189736665978239627) + (X_2 * 0.098474573164286039) + (X_3 * 0.220418718662632351) + (X_4 * 0.03836653204063839) + (X_5 * 0.279710695915403817) + (X_6 * 0.14410430753399317) + (X_7 * 0.204156618335651407) + (X_8 * 0.176473915501038803) + -0.03827183418778396), 0.0) * -0.103757965589408141) + (max(((X_0 * 0.00869382371014682) + (X_1 * -0.310492767426873872) + (X_2 * 0.117116910196331914) + (X_3 * 0.169087657846020811) + (X_4 * -0.273335058913078577) + (X_5 * -0.000683592328365401) + (X_6 * 0.139512227022986102) + (X_7 * -0.313799159812941153) + (X_8 * -0.196166996347198946) + 0.236750714424111497), 0.0) * -0.02251099020301281) + (max(((X_0 * 0.137861025679069715) + (X_1 * -0.024667890831123473) + (X_2 * -0.315714844767212732) + (X_3 * 0.237047096266294222) + (X_4 * 0.202101116810822823) + (X_5 * -0.020405610795288631) + (X_6 * 0.223248306677427399) + (X_7 * 0.166427221032260431) + (X_8 * 0.322898701032060254) + 0.085041015223344729), 0.0) * -0.050331754476605595) + (max(((X_0 * 0.063704153901590399) + (X_1 * 0.084893455136697493) + (X_2 * 0.162022423603656263) + (X_3 * -0.026069359722939833) + (X_4 * -0.103610576532342291) + (X_5 * 0.247462072588003845) + (X_6 * 0.235604458158232999) + (X_7 * 0.094778590268327412) + (X_8 * 0.317884709780666685) + -0.259110365198896853), 0.0) * 0.062023155901275023) + (max(((X_0 * 0.157051962420222013) + (X_1 * 0.02119912918435074) + (X_2 * -0.144567654546317315) + (X_3 * -0.120485782181390416) + (X_4 * 0.245385692300038649) + (X_5 * -0.12013008718360596) + (X_6 * -0.264054168644354381) + (X_7 * 0.113466930567937607) + (X_8 * 0.018847290606381961) + -0.306458405399606004), 0.0) * 0.050539905176572114) + (max(((X_0 * 0.287194094745330031) + (X_1 * -0.279329006877257702) + (X_2 * -0.27381666760090273) + (X_3 * -0.241196338354026901) + (X_4 * 0.166076860453970354) + (X_5 * 0.003947070874237735) + (X_6 * -0.079391976830132827) + (X_7 * -0.311101692329606716) + (X_8 * 0.028656916570530377) + -0.242226407222209617), 0.0) * -0.113341220129465542) + (max(((X_0 * 0.04404093390102809) + (X_1 * 0.223856941183437852) + (X_2 * 0.030174154656356367) + (X_3 * -0.093021470933494721) + (X_4 * -0.040972965799927652) + (X_5 * 0.134584475865453967) + (X_6 * 0.312199328391165765) + (X_7 * 0.040627871296072593) + (X_8 * -0.123070819674687693) + 0.158068620935378545), 0.0) * -0.091388057110437182) + (max(((X_0 * 0.309415963276349515) + (X_1 * 0.039481469238021816) + (X_2 * 0.15094441592481006) + (X_3 * 0.30522360340783411) + (X_4 * -0.229798563734669559) + (X_5 * -0.192960605209967856) + (X_6 * -0.20370062757883689) + (X_7 * -0.047763191941385397) + (X_8 * -0.266019895781817062) + -0.3239652657122854), 0.0) * 0.01226672300108253) + (max(((X_0 * 0.291655730227005694) + (X_1 * -0.211448651190053294) + (X_2 * 0.262759471678295109) + (X_3 * 0.250069844719772838) + (X_4 * -0.0381186790917451) + (X_5 * -0.146083546836047795) + (X_6 * -0.151529498387592332) + (X_7 * 0.201164755659322625) + (X_8 * 0.146160292641425327) + -0.046301663710338892), 0.0) * -0.011881258815351903) + (max(((X_0 * -0.184467825491839488) + (X_1 * -0.268161247711679374) + (X_2 * -0.153535151736396536) + (X_3 * -0.065596192568929845) + (X_4 * 0.21729520120637863) + (X_5 * -0.092332864688549343) + (X_6 * 0.018066462919213766) + (X_7 * -0.287370290741390033) + (X_8 * -0.222457450236703963) + -0.231100948340147661), 0.0) * 0.058279261437098495) + (max(((X_0 * 0.112387308333164793) + (X_1 * -0.164516529633275843) + (X_2 * 0.303715756573457785) + (X_3 * -0.115559064636028858) + (X_4 * -0.101279569170582118) + (X_5 * -0.312584846980395903) + (X_6 * -0.073897332022657303) + (X_7 * -0.187107831241006384) + (X_8 * 0.191742606049471742) + 0.219833682999539703), 0.0) * 0.123000304336519151) + (max(((X_0 * 0.272843083546418008) + (X_1 * -0.26331667301370465) + (X_2 * 0.228746460665943896) + (X_3 * 0.083017409074116422) + (X_4 * 0.2906669151723143) + (X_5 * 0.035447691086564703) + (X_6 * 0.312581653146865424) + (X_7 * -0.052006990099353001) + (X_8 * -0.238709163668962665) + 0.28076114529116375), 0.0) * -0.108282925757814397) + (max(((X_0 * 0.074020874970563255) + (X_1 * -0.022502229774748639) + (X_2 * 0.183897093057601213) + (X_3 * -0.287464703406070055) + (X_4 * -0.079254407166150287) + (X_5 * -0.330123738440344594) + (X_6 * 0.302019322984987182) + (X_7 * 0.060629658317428392) + (X_8 * -0.066123676240795071) + -0.168318244851325016), 0.0) * 0.095025211690298095) + (max(((X_0 * 0.117161478668860342) + (X_1 * -0.309380508435266599) + (X_2 * 0.166150746972853758) + (X_3 * 0.013701434090766906) + (X_4 * 0.141685721053067371) + (X_5 * -0.028880166693844356) + (X_6 * 0.260745424659842906) + (X_7 * -0.158065618750375059) + (X_8 * 0.095877003914591752) + 0.118188048960575609), 0.0) * 0.097016468103824222) + (max(((X_0 * -0.242158813559863934) + (X_1 * 0.121440841134675681) + (X_2 * 0.244934559694501341) + (X_3 * -0.317637615301534615) + (X_4 * -0.25005972927599035) + (X_5 * -0.215710382695643604) + (X_6 * 0.124190735382829098) + (X_7 * -0.059589490133065748) + (X_8 * 0.251407265038740835) + 0.08916513259423331), 0.0) * 0.042911582712372859) + -0.083772180253624123))
tff(formula_21,axiom,
'Y_1' = $sum($product(max($sum($product('X_0',$uminus(0.034143127336152712)),$sum($product('X_1',0.322824668200060227),$sum($product('X_2',0.091291052421442809),$sum($product('X_3',$uminus(0.012612789817531833)),$sum($product('X_4',0.273541493916837075),$sum($product('X_5',$uminus(0.150105792320639253)),$sum($product('X_6',$uminus(0.049406931293640266)),$sum($product('X_7',$uminus(0.21107752838875965)),$sum($product('X_8',0.277909149915428422),$uminus(0.019189099155314304)))))))))),0.0),$uminus(0.073998450024932688)),$sum($product(max($sum($product('X_0',0.135860462188255371),$sum($product('X_1',0.187969393886196101),$sum($product('X_2',0.174517671834989951),$sum($product('X_3',0.127635942676799008),$sum($product('X_4',$uminus(0.136994285692501105)),$sum($product('X_5',0.012365905796069943),$sum($product('X_6',$uminus(0.027014764654490264)),$sum($product('X_7',$uminus(0.305544519265200321)),$sum($product('X_8',$uminus(0.206852248891131074)),$uminus(0.314645004469935208)))))))))),0.0),$uminus(0.064513743407656948)),$sum($product(max($sum($product('X_0',$uminus(0.081020401392122687)),$sum($product('X_1',0.062490409237779099),$sum($product('X_2',0.111520586127630439),$sum($product('X_3',$uminus(0.213447096651937063)),$sum($product('X_4',0.132706362488796692),$sum($product('X_5',$uminus(0.261185283187217065)),$sum($product('X_6',0.00474527583528711),$sum($product('X_7',$uminus(0.06688270460651552)),$sum($product('X_8',$uminus(0.320470498630223033)),$uminus(0.190989000847826468)))))))))),0.0),$uminus(0.026160320859166641)),$sum($product(max($sum($product('X_0',0.138290117678506908),$sum($product('X_1',0.005330501640528451),$sum($product('X_2',$uminus(0.13333471971657565)),$sum($product('X_3',0.153277069170855151),$sum($product('X_4',0.193097250496935435),$sum($product('X_5',0.124353050256880426),$sum($product('X_6',$uminus(0.312998335768394587)),$sum($product('X_7',0.14582588668244395),$sum($product('X_8',0.017849845577707468),$uminus(0.207803467395465624)))))))))),0.0),0.081871644668587457),$sum($product(max($sum($product('X_0',0.25616055553271605),$sum($product('X_1',$uminus(0.03627032974016875)),$sum($product('X_2',$uminus(0.194452918074013159)),$sum($product('X_3',0.10008950100824493),$sum($product('X_4',0.321933544906211566),$sum($product('X_5',0.302676823386164806),$sum($product('X_6',0.282644938195837081),$sum($product('X_7',0.218166819191055239),$sum($product('X_8',0.061315114611943666),0.294909295927187565))))))))),0.0),$uminus(0.001332491252833162)),$sum($product(max($sum($product('X_0',$uminus(0.203907213010214777)),$sum($product('X_1',$uminus(0.329328844050836067)),$sum($product('X_2',$uminus(0.282209682521432303)),$sum($product('X_3',0.194481051286681639),$sum($product('X_4',0.223447381199474771),$sum($product('X_5',$uminus(0.130047140060396471)),$sum($product('X_6',0.258072855214746821),$sum($product('X_7',0.236670528410227232),$sum($product('X_8',0.219327984313435753),0.307309013280585186))))))))),0.0),0.044857164486815815),$sum($product(max($sum($product('X_0',$uminus(0.025392492262058697)),$sum($product('X_1',$uminus(0.260814592583792804)),$sum($product('X_2',$uminus(0.060464105023337156)),$sum($product('X_3',0.235580850968075406),$sum($product('X_4',0.013069063238517142),$sum($product('X_5',$uminus(0.196757326475462957)),$sum($product('X_6',0.028155879508867165),$sum($product('X_7',$uminus(0.181432604418310606)),$sum($product('X_8',0.089552351207647263),0.233953211619548462))))))))),0.0),$uminus(0.028382197281112381)),$sum($product(max($sum($product('X_0',$uminus(0.316000969071793147)),$sum($product('X_1',0.025263023662981166),$sum($product('X_2',0.177171946751012388),$sum($product('X_3',$uminus(0.035122639314649318)),$sum($product('X_4',$uminus(0.23096764293788713)),$sum($product('X_5',0.017100988871234346),$sum($product('X_6',$uminus(0.209560107747809532)),$sum($product('X_7',$uminus(0.026921531592388137)),$sum($product('X_8',$uminus(0.032723387475881827)),0.168724722506589486))))))))),0.0),$uminus(0.052279107638462302)),$sum($product(max($sum($product('X_0',0.001306859463930443),$sum($product('X_1',$uminus(0.32178678467757027)),$sum($product('X_2',$uminus(0.073177542048799837)),$sum($product('X_3',0.002394918508160371),$sum($product('X_4',0.093730698889344044),$sum($product('X_5',0.008752806231017984),$sum($product('X_6',$uminus(0.084064570826615143)),$sum($product('X_7',0.250900209655107453),$sum($product('X_8',0.022976222292577286),0.077232081109878559))))))))),0.0),0.050512184504869773),$sum($product(max($sum($product('X_0',0.194049225184143082),$sum($product('X_1',$uminus(0.022183735625062984)),$sum($product('X_2',$uminus(0.196724399739592354)),$sum($product('X_3',0.07635785513446619),$sum($product('X_4',$uminus(0.196322916482755933)),$sum($product('X_5',$uminus(0.288926766400791291)),$sum($product('X_6',0.213700339341032219),$sum($product('X_7',$uminus(0.253512613136544884)),$sum($product('X_8',0.231484855576049309),0.280058863303405625))))))))),0.0),$uminus(0.066188932067793194)),$sum($product(max($sum($product('X_0',0.317728685554186929),$sum($product('X_1',0.332150001647927684),$sum($product('X_2',$uminus(0.001259591758584755)),$sum($product('X_3',$uminus(0.207453820552864571)),$sum($product('X_4',0.005723595304183482),$sum($product('X_5',0.185428526068087629),$sum($product('X_6',0.054353623505082105),$sum($product('X_7',0.132946612680298504),$sum($product('X_8',0.011140036900155748),$uminus(0.209314307847249387)))))))))),0.0),$uminus(0.018565609615204703)),$sum($product(max($sum($product('X_0',$uminus(0.269304224359853461)),$sum($product('X_1',$uminus(0.310904419113500918)),$sum($product('X_2',0.32027709592926229),$sum($product('X_3',$uminus(0.200037762633937188)),$sum($product('X_4',$uminus(0.026191122665172317)),$sum($product('X_5',$uminus(0.042660660377485116)),$sum($product('X_6',$uminus(0.146275965076368142)),$sum($product('X_7',$uminus(0.305670262866760689)),$sum($product('X_8',0.322576996064118438),$uminus(0.183572002247813032)))))))))),0.0),$uminus(0.114746509627626225)),$sum($product(max($sum($product('X_0',0.136084741586379454),$sum($product('X_1',0.26228771638376186),$sum($product('X_2',$uminus(0.284171295665994417)),$sum($product('X_3',0.211831054834103749),$sum($product('X_4',0.285004999381932744),$sum($product('X_5',$uminus(0.007441424708356792)),$sum($product('X_6',$uminus(0.140284600003246995)),$sum($product('X_7',$uminus(0.207592415895373833)),$sum($product('X_8',0.27321519909354347),$uminus(0.207526152104757111)))))))))),0.0),0.068807719524015376),$sum($product(max($sum($product('X_0',$uminus(0.22841409680804925)),$sum($product('X_1',0.240551489683236974),$sum($product('X_2',0.312484269972083728),$sum($product('X_3',$uminus(0.181755643345508588)),$sum($product('X_4',0.030657116136170337),$sum($product('X_5',$uminus(0.055299675827487349)),$sum($product('X_6',$uminus(0.062998580523338621)),$sum($product('X_7',0.098231667492682917),$sum($product('X_8',$uminus(0.015349265026970815)),0.174413712522803299))))))))),0.0),0.040671257241023412),$sum($product(max($sum($product('X_0',0.326514337483990558),$sum($product('X_1',$uminus(0.139206653914812462)),$sum($product('X_2',$uminus(0.301944004088363971)),$sum($product('X_3',0.007220186513743954),$sum($product('X_4',$uminus(0.082554028749347141)),$sum($product('X_5',$uminus(0.040344607481459793)),$sum($product('X_6',$uminus(0.215478397144116013)),$sum($product('X_7',0.145783348414039393),$sum($product('X_8',$uminus(0.142290498498560514)),$uminus(0.21557124240865938)))))))))),0.0),$uminus(0.040973937252329506)),$sum($product(max($sum($product('X_0',$uminus(0.001976599008208513)),$sum($product('X_1',$uminus(0.057764032526161302)),$sum($product('X_2',0.159396263708995178),$sum($product('X_3',$uminus(0.183991541476796888)),$sum($product('X_4',0.142504183402018647),$sum($product('X_5',$uminus(0.238937927812336026)),$sum($product('X_6',$uminus(0.30402575884910954)),$sum($product('X_7',0.29491808364114086),$sum($product('X_8',0.054445412143243832),$uminus(0.170312927346704335)))))))))),0.0),0.054472072806984684),$sum($product(max($sum($product('X_0',$uminus(0.069437022416364014)),$sum($product('X_1',$uminus(0.00060254546898092)),$sum($product('X_2',0.247675182881536504),$sum($product('X_3',0.234314025579507035),$sum($product('X_4',$uminus(0.177673295141312471)),$sum($product('X_5',$uminus(0.332483963357472823)),$sum($product('X_6',$uminus(0.218038989896279178)),$sum($product('X_7',0.127363049893037317),$sum($product('X_8',$uminus(0.2086790536248469)),$uminus(0.187722099200903436)))))))))),0.0),0.024969370219846659),$sum($product(max($sum($product('X_0',0.324876735423139718),$sum($product('X_1',0.075982824387152592),$sum($product('X_2',$uminus(0.313261926183435957)),$sum($product('X_3',$uminus(0.209064108357157524)),$sum($product('X_4',$uminus(0.261535938731004891)),$sum($product('X_5',$uminus(0.234787129658768606)),$sum($product('X_6',0.112031404664260759),$sum($product('X_7',0.225008006173745667),$sum($product('X_8',0.140199347195911539),0.139447447171109518))))))))),0.0),$uminus(0.080517183573391909)),$sum($product(max($sum($product('X_0',0.202182439886614829),$sum($product('X_1',0.228470631117320078),$sum($product('X_2',0.074549186229916131),$sum($product('X_3',0.233422713721841812),$sum($product('X_4',0.131135712704656016),$sum($product('X_5',$uminus(0.326710062287342951)),$sum($product('X_6',0.012038286823084332),$sum($product('X_7',0.231618192292777969),$sum($product('X_8',0.000719113164345198),0.213277245603735233))))))))),0.0),$uminus(0.110508536016433095)),$sum($product(max($sum($product('X_0',0.28449527898218091),$sum($product('X_1',$uminus(0.081527175695953635)),$sum($product('X_2',$uminus(0.153930222701464642)),$sum($product('X_3',$uminus(0.186077449214199719)),$sum($product('X_4',$uminus(0.05936612416981174)),$sum($product('X_5',$uminus(0.154628465341259957)),$sum($product('X_6',$uminus(0.166498063888305931)),$sum($product('X_7',0.055266800565439478),$sum($product('X_8',$uminus(0.213197545634780383)),0.010205194890945457))))))))),0.0),0.079700459465058576),$sum($product(max($sum($product('X_0',$uminus(0.180816367347528484)),$sum($product('X_1',0.043531190359145266),$sum($product('X_2',$uminus(0.047619638831746636)),$sum($product('X_3',$uminus(0.058934638109038928)),$sum($product('X_4',$uminus(0.124666639609441937)),$sum($product('X_5',$uminus(0.318308163331019744)),$sum($product('X_6',0.193062520783280067),$sum($product('X_7',0.020418055017284109),$sum($product('X_8',0.060922472827523722),0.223360539691101423))))))))),0.0),$uminus(0.117348884884679872)),$sum($product(max($sum($product('X_0',0.134746472119233907),$sum($product('X_1',$uminus(0.217554078381223898)),$sum($product('X_2',$uminus(0.085730993819177093)),$sum($product('X_3',0.297521692708929308),$sum($product('X_4',0.063860554017248994),$sum($product('X_5',0.217082184168041759),$sum($product('X_6',$uminus(0.021045092732637605)),$sum($product('X_7',0.259811010052565072),$sum($product('X_8',0.200338555724555889),0.247229328571023033))))))))),0.0),$uminus(0.072948417866398663)),$sum($product(max($sum($product('X_0',0.203487277967640046),$sum($product('X_1',0.324424625686173973),$sum($product('X_2',$uminus(0.024662687002090788)),$sum($product('X_3',0.216277755365953894),$sum($product('X_4',0.163509105125114296),$sum($product('X_5',$uminus(0.034687792438270026)),$sum($product('X_6',0.206452845548049824),$sum($product('X_7',0.154282897842712208),$sum($product('X_8',$uminus(0.017555615896969023)),0.272302961557755852))))))))),0.0),$uminus(0.07655439511301329)),$sum($product(max($sum($product('X_0',$uminus(0.244290676854412331)),$sum($product('X_1',$uminus(0.204088781911439338)),$sum($product('X_2',$uminus(0.03882746711711399)),$sum($product('X_3',$uminus(0.097232792095546527)),$sum($product('X_4',$uminus(0.303174897657345899)),$sum($product('X_5',$uminus(0.051070311788715628)),$sum($product('X_6',0.149992479035335302),$sum($product('X_7',$uminus(0.102185614965710991)),$sum($product('X_8',$uminus(0.106519170243570216)),0.058597670613885988))))))))),0.0),$uminus(0.040583535831473089)),$sum($product(max($sum($product('X_0',0.012864262113814806),$sum($product('X_1',0.109069631915820031),$sum($product('X_2',0.101543371952154571),$sum($product('X_3',0.06799496124837745),$sum($product('X_4',$uminus(0.26445983492561137)),$sum($product('X_5',0.215833875445791301),$sum($product('X_6',0.272580780248200039),$sum($product('X_7',$uminus(0.039747643760278006)),$sum($product('X_8',$uminus(0.243825769939117892)),$uminus(0.123945865842741254)))))))))),0.0),0.040847410791384653),$sum($product(max($sum($product('X_0',$uminus(0.154837365313728936)),$sum($product('X_1',0.085840778969112019),$sum($product('X_2',0.165077967938471126),$sum($product('X_3',0.111848736690037587),$sum($product('X_4',$uminus(0.240612563426037041)),$sum($product('X_5',0.140637468751368289),$sum($product('X_6',$uminus(0.149768050036042905)),$sum($product('X_7',$uminus(0.283477350113733539)),$sum($product('X_8',0.073570979765799127),0.079922247453340256))))))))),0.0),0.107608377126927612),$sum($product(max($sum($product('X_0',$uminus(0.100199971469390775)),$sum($product('X_1',0.186120110641400827),$sum($product('X_2',0.049038095207454113),$sum($product('X_3',$uminus(0.196087530498076618)),$sum($product('X_4',0.08711796538252381),$sum($product('X_5',$uminus(0.101227855157801916)),$sum($product('X_6',0.158620075819161321),$sum($product('X_7',$uminus(0.146913672899774472)),$sum($product('X_8',$uminus(0.119082579355500373)),0.138895725711660534))))))))),0.0),0.111136415946718747),$sum($product(max($sum($product('X_0',0.180027772073166392),$sum($product('X_1',$uminus(0.103336431479241098)),$sum($product('X_2',$uminus(0.267316901673856466)),$sum($product('X_3',0.263656543687109834),$sum($product('X_4',0.332642570227415224),$sum($product('X_5',0.277967948182220759),$sum($product('X_6',0.30343956010141554),$sum($product('X_7',0.03447325941087459),$sum($product('X_8',0.125197865386826701),0.192506796333139885))))))))),0.0),0.099246897649233917),$sum($product(max($sum($product('X_0',$uminus(0.229596022939276084)),$sum($product('X_1',0.306162374571047058),$sum($product('X_2',$uminus(0.214349113239148403)),$sum($product('X_3',0.05827258272512098),$sum($product('X_4',0.131302065849309368),$sum($product('X_5',$uminus(0.271631521510831919)),$sum($product('X_6',$uminus(0.270260881180521384)),$sum($product('X_7',$uminus(0.202970959783648347)),$sum($product('X_8',0.179428170698139933),0.115665614154320362))))))))),0.0),0.040522696972192768),$sum($product(max($sum($product('X_0',0.194962600903016259),$sum($product('X_1',$uminus(0.17835559373673493)),$sum($product('X_2',$uminus(0.228962538545053329)),$sum($product('X_3',0.306214141164736053),$sum($product('X_4',0.257337107072608651),$sum($product('X_5',$uminus(0.299595911463449771)),$sum($product('X_6',0.089666024789417487),$sum($product('X_7',0.326462876291198911),$sum($product('X_8',$uminus(0.062301378541843311)),0.172234015205460611))))))))),0.0),0.074811979072499146),$sum($product(max($sum($product('X_0',0.255845191590086396),$sum($product('X_1',0.215495725762357482),$sum($product('X_2',$uminus(0.302097504773537306)),$sum($product('X_3',0.095845709494328524),$sum($product('X_4',$uminus(0.075426811348071776)),$sum($product('X_5',0.218624900118963683),$sum($product('X_6',0.26160805655982583),$sum($product('X_7',$uminus(0.212202541273525114)),$sum($product('X_8',$uminus(0.041523081831996933)),0.102324186276997908))))))))),0.0),$uminus(0.083572412646659655)),$sum($product(max($sum($product('X_0',0.30493330995168616),$sum($product('X_1',$uminus(0.122490486481055483)),$sum($product('X_2',0.174817256741448934),$sum($product('X_3',$uminus(0.202369269426108028)),$sum($product('X_4',$uminus(0.323621969121451081)),$sum($product('X_5',0.303508866087579043),$sum($product('X_6',$uminus(0.223769302030546458)),$sum($product('X_7',$uminus(0.27502503528423522)),$sum($product('X_8',0.129622404600985675),$uminus(0.253776462014690563)))))))))),0.0),$uminus(0.035980293323670226)),$sum($product(max($sum($product('X_0',0.269059547412644651),$sum($product('X_1',$uminus(0.005882567254681115)),$sum($product('X_2',$uminus(0.171353970135741607)),$sum($product('X_3',0.294037626949683328),$sum($product('X_4',$uminus(0.255251802687420648)),$sum($product('X_5',$uminus(0.009759698938691885)),$sum($product('X_6',0.180149176039681114),$sum($product('X_7',0.045388866190233079),$sum($product('X_8',$uminus(0.179760143010707252)),0.269823604538700745))))))))),0.0),$uminus(0.093401995853832742)),$sum($product(max($sum($product('X_0',$uminus(0.138558699684565634)),$sum($product('X_1',0.003660311035716235),$sum($product('X_2',$uminus(0.328144076991653155)),$sum($product('X_3',0.17711252434090502),$sum($product('X_4',0.086745978461675144),$sum($product('X_5',0.052468260508699016),$sum($product('X_6',0.051635532764924497),$sum($product('X_7',0.032455574507212981),$sum($product('X_8',$uminus(0.079164165185457769)),0.068544128415001238))))))))),0.0),0.014988998746798182),$sum($product(max($sum($product('X_0',$uminus(0.188430209592040626)),$sum($product('X_1',0.180982936820061113),$sum($product('X_2',0.124800571217657474),$sum($product('X_3',$uminus(0.054881926059530961)),$sum($product('X_4',$uminus(0.026456773114379717)),$sum($product('X_5',0.162595317059087197),$sum($product('X_6',0.049021975497793691),$sum($product('X_7',$uminus(0.246830321591287927)),$sum($product('X_8',0.232013828123107502),$uminus(0.062546264757998127)))))))))),0.0),0.09899955044625447),$sum($product(max($sum($product('X_0',0.040962088339393521),$sum($product('X_1',$uminus(0.254386604085368229)),$sum($product('X_2',$uminus(0.112672966314846829)),$sum($product('X_3',$uminus(0.159902546439000759)),$sum($product('X_4',$uminus(0.207701480823660051)),$sum($product('X_5',0.133165675227524982),$sum($product('X_6',0.193618244226427871),$sum($product('X_7',0.082613724983702452),$sum($product('X_8',0.322632448399385929),0.224209517678037373))))))))),0.0),0.117837399943200416),$sum($product(max($sum($product('X_0',$uminus(0.134886517018193708)),$sum($product('X_1',0.144899616770255646),$sum($product('X_2',$uminus(0.17980112071828272)),$sum($product('X_3',$uminus(0.267509492307719976)),$sum($product('X_4',$uminus(0.157528799514788709)),$sum($product('X_5',$uminus(0.079420419232439199)),$sum($product('X_6',$uminus(0.299465230679228367)),$sum($product('X_7',$uminus(0.125820656916256324)),$sum($product('X_8',0.019239984001792998),0.142229458135585185))))))))),0.0),0.019122155497841964),$sum($product(max($sum($product('X_0',$uminus(0.172346696671293709)),$sum($product('X_1',0.090451716164184959),$sum($product('X_2',$uminus(0.228793228787715741)),$sum($product('X_3',0.180997116632383548),$sum($product('X_4',0.290344111330939902),$sum($product('X_5',$uminus(0.234970994376170916)),$sum($product('X_6',0.005159751606115537),$sum($product('X_7',$uminus(0.155461525393435412)),$sum($product('X_8',$uminus(0.288046325238939249)),$uminus(0.070296844355285437)))))))))),0.0),$uminus(0.11907840381428797)),$sum($product(max($sum($product('X_0',$uminus(0.234997276198458949)),$sum($product('X_1',$uminus(0.172512713965825709)),$sum($product('X_2',0.114308047040828642),$sum($product('X_3',$uminus(0.063627448790975871)),$sum($product('X_4',$uminus(0.205794049922004174)),$sum($product('X_5',0.19287844644458868),$sum($product('X_6',$uminus(0.257664032924889597)),$sum($product('X_7',$uminus(0.233509914142561753)),$sum($product('X_8',0.267404797826638896),0.248418369896963032))))))))),0.0),$uminus(0.057272059559953431)),$sum($product(max($sum($product('X_0',0.296841143323539114),$sum($product('X_1',$uminus(0.012110575240900978)),$sum($product('X_2',$uminus(0.122779558396503508)),$sum($product('X_3',0.145965415302344859),$sum($product('X_4',0.115669853903047126),$sum($product('X_5',0.181260046623958171),$sum($product('X_6',0.176356841716120927),$sum($product('X_7',0.054758245250969895),$sum($product('X_8',0.066387541776141479),0.033378311133483385))))))))),0.0),$uminus(0.088314638651521005)),$sum($product(max($sum($product('X_0',$uminus(0.068127119880877884)),$sum($product('X_1',$uminus(0.193888759810902311)),$sum($product('X_2',$uminus(0.075010565817496266)),$sum($product('X_3',0.116013395273452391),$sum($product('X_4',0.197890889155673377),$sum($product('X_5',0.321385853477913319),$sum($product('X_6',0.050015661552153368),$sum($product('X_7',$uminus(0.054890782359229284)),$sum($product('X_8',0.258758291380532579),$uminus(0.143355802615697941)))))))))),0.0),0.042882380581039575),$sum($product(max($sum($product('X_0',$uminus(0.071997512442384004)),$sum($product('X_1',0.017303820158426297),$sum($product('X_2',0.091534845651731311),$sum($product('X_3',0.311279068800356329),$sum($product('X_4',$uminus(0.00312157907909616)),$sum($product('X_5',$uminus(0.188277000904065517)),$sum($product('X_6',$uminus(0.183479587316280945)),$sum($product('X_7',0.212372245445371421),$sum($product('X_8',$uminus(0.077162998727941579)),$uminus(0.223645418757847825)))))))))),0.0),0.00608997096424313),$sum($product(max($sum($product('X_0',$uminus(0.32243249625430126)),$sum($product('X_1',0.182253848897861837),$sum($product('X_2',$uminus(0.099368623456786598)),$sum($product('X_3',$uminus(0.156602428474534483)),$sum($product('X_4',0.030765939328599223),$sum($product('X_5',$uminus(0.026342715055112154)),$sum($product('X_6',0.000532788149621544),$sum($product('X_7',0.303861041761946782),$sum($product('X_8',0.265755190798946772),0.100146050819974963))))))))),0.0),$uminus(0.09913956730640347)),$sum($product(max($sum($product('X_0',$uminus(0.112545642928356893)),$sum($product('X_1',0.265866650798053328),$sum($product('X_2',0.015101151225212606),$sum($product('X_3',$uminus(0.317799591526125247)),$sum($product('X_4',$uminus(0.168903714240354275)),$sum($product('X_5',0.030188500593428369),$sum($product('X_6',0.061277558788815967),$sum($product('X_7',0.200866407017562254),$sum($product('X_8',$uminus(0.112371008406928929)),$uminus(0.079493482734081355)))))))))),0.0),$uminus(0.062563463103772948)),$sum($product(max($sum($product('X_0',$uminus(0.192154828636623531)),$sum($product('X_1',0.083979791049164365),$sum($product('X_2',0.159973530860791413),$sum($product('X_3',$uminus(0.265406610551946254)),$sum($product('X_4',0.287198912407206131),$sum($product('X_5',0.095627746140380554),$sum($product('X_6',$uminus(0.00994146969909776)),$sum($product('X_7',$uminus(0.219422562050552161)),$sum($product('X_8',$uminus(0.081085067577720604)),0.104747771083528063))))))))),0.0),0.028402193751599886),$sum($product(max($sum($product('X_0',$uminus(0.057039132055541286)),$sum($product('X_1',0.038985751754933406),$sum($product('X_2',$uminus(0.004944442157409357)),$sum($product('X_3',$uminus(0.15462525839770902)),$sum($product('X_4',$uminus(0.1398935031159593)),$sum($product('X_5',$uminus(0.061959641528152032)),$sum($product('X_6',0.098679300771940037),$sum($product('X_7',$uminus(0.201235020697894035)),$sum($product('X_8',$uminus(0.237594859082526227)),$uminus(0.158841501426246007)))))))))),0.0),$uminus(0.114140016983423964)),$sum($product(max($sum($product('X_0',0.331353170527205643),$sum($product('X_1',$uminus(0.288645365007353272)),$sum($product('X_2',0.223956278926402741),$sum($product('X_3',0.279170663263683283),$sum($product('X_4',0.017978724577996319),$sum($product('X_5',$uminus(0.250013034963560865)),$sum($product('X_6',0.098807821234157156),$sum($product('X_7',0.258776815881270383),$sum($product('X_8',0.152988470579232594),0.28246081276552143))))))))),0.0),$uminus(0.079083806413413033)),$sum($product(max($sum($product('X_0',$uminus(0.100883845060276311)),$sum($product('X_1',0.046212140463826712),$sum($product('X_2',$uminus(0.026600669905651519)),$sum($product('X_3',0.142320732212770695),$sum($product('X_4',0.072733698806154878),$sum($product('X_5',0.197196887480299343),$sum($product('X_6',0.237120144257248089),$sum($product('X_7',$uminus(0.166327692927533299)),$sum($product('X_8',$uminus(0.078131387240757411)),$uminus(0.293417736964490861)))))))))),0.0),0.069237546080712919),$sum($product(max($sum($product('X_0',0.294400522037719437),$sum($product('X_1',0.082094261162431514),$sum($product('X_2',0.101918067411788049),$sum($product('X_3',0.17357922076579041),$sum($product('X_4',0.114082861901367405),$sum($product('X_5',$uminus(0.311032034544396929)),$sum($product('X_6',0.258029579372313467),$sum($product('X_7',0.145657792087877658),$sum($product('X_8',$uminus(0.033975658190385893)),0.194899911587433305))))))))),0.0),$uminus(0.092256427149248615)),$sum($product(max($sum($product('X_0',0.034313476891573602),$sum($product('X_1',$uminus(0.189736665978239627)),$sum($product('X_2',0.098474573164286039),$sum($product('X_3',0.220418718662632351),$sum($product('X_4',0.03836653204063839),$sum($product('X_5',0.279710695915403817),$sum($product('X_6',0.14410430753399317),$sum($product('X_7',0.204156618335651407),$sum($product('X_8',0.176473915501038803),$uminus(0.03827183418778396)))))))))),0.0),$uminus(0.103757965589408141)),$sum($product(max($sum($product('X_0',0.00869382371014682),$sum($product('X_1',$uminus(0.310492767426873872)),$sum($product('X_2',0.117116910196331914),$sum($product('X_3',0.169087657846020811),$sum($product('X_4',$uminus(0.273335058913078577)),$sum($product('X_5',$uminus(0.000683592328365401)),$sum($product('X_6',0.139512227022986102),$sum($product('X_7',$uminus(0.313799159812941153)),$sum($product('X_8',$uminus(0.196166996347198946)),0.236750714424111497))))))))),0.0),$uminus(0.02251099020301281)),$sum($product(max($sum($product('X_0',0.137861025679069715),$sum($product('X_1',$uminus(0.024667890831123473)),$sum($product('X_2',$uminus(0.315714844767212732)),$sum($product('X_3',0.237047096266294222),$sum($product('X_4',0.202101116810822823),$sum($product('X_5',$uminus(0.020405610795288631)),$sum($product('X_6',0.223248306677427399),$sum($product('X_7',0.166427221032260431),$sum($product('X_8',0.322898701032060254),0.085041015223344729))))))))),0.0),$uminus(0.050331754476605595)),$sum($product(max($sum($product('X_0',0.063704153901590399),$sum($product('X_1',0.084893455136697493),$sum($product('X_2',0.162022423603656263),$sum($product('X_3',$uminus(0.026069359722939833)),$sum($product('X_4',$uminus(0.103610576532342291)),$sum($product('X_5',0.247462072588003845),$sum($product('X_6',0.235604458158232999),$sum($product('X_7',0.094778590268327412),$sum($product('X_8',0.317884709780666685),$uminus(0.259110365198896853)))))))))),0.0),0.062023155901275023),$sum($product(max($sum($product('X_0',0.157051962420222013),$sum($product('X_1',0.02119912918435074),$sum($product('X_2',$uminus(0.144567654546317315)),$sum($product('X_3',$uminus(0.120485782181390416)),$sum($product('X_4',0.245385692300038649),$sum($product('X_5',$uminus(0.12013008718360596)),$sum($product('X_6',$uminus(0.264054168644354381)),$sum($product('X_7',0.113466930567937607),$sum($product('X_8',0.018847290606381961),$uminus(0.306458405399606004)))))))))),0.0),0.050539905176572114),$sum($product(max($sum($product('X_0',0.287194094745330031),$sum($product('X_1',$uminus(0.279329006877257702)),$sum($product('X_2',$uminus(0.27381666760090273)),$sum($product('X_3',$uminus(0.241196338354026901)),$sum($product('X_4',0.166076860453970354),$sum($product('X_5',0.003947070874237735),$sum($product('X_6',$uminus(0.079391976830132827)),$sum($product('X_7',$uminus(0.311101692329606716)),$sum($product('X_8',0.028656916570530377),$uminus(0.242226407222209617)))))))))),0.0),$uminus(0.113341220129465542)),$sum($product(max($sum($product('X_0',0.04404093390102809),$sum($product('X_1',0.223856941183437852),$sum($product('X_2',0.030174154656356367),$sum($product('X_3',$uminus(0.093021470933494721)),$sum($product('X_4',$uminus(0.040972965799927652)),$sum($product('X_5',0.134584475865453967),$sum($product('X_6',0.312199328391165765),$sum($product('X_7',0.040627871296072593),$sum($product('X_8',$uminus(0.123070819674687693)),0.158068620935378545))))))))),0.0),$uminus(0.091388057110437182)),$sum($product(max($sum($product('X_0',0.309415963276349515),$sum($product('X_1',0.039481469238021816),$sum($product('X_2',0.15094441592481006),$sum($product('X_3',0.30522360340783411),$sum($product('X_4',$uminus(0.229798563734669559)),$sum($product('X_5',$uminus(0.192960605209967856)),$sum($product('X_6',$uminus(0.20370062757883689)),$sum($product('X_7',$uminus(0.047763191941385397)),$sum($product('X_8',$uminus(0.266019895781817062)),$uminus(0.3239652657122854)))))))))),0.0),0.01226672300108253),$sum($product(max($sum($product('X_0',0.291655730227005694),$sum($product('X_1',$uminus(0.211448651190053294)),$sum($product('X_2',0.262759471678295109),$sum($product('X_3',0.250069844719772838),$sum($product('X_4',$uminus(0.0381186790917451)),$sum($product('X_5',$uminus(0.146083546836047795)),$sum($product('X_6',$uminus(0.151529498387592332)),$sum($product('X_7',0.201164755659322625),$sum($product('X_8',0.146160292641425327),$uminus(0.046301663710338892)))))))))),0.0),$uminus(0.011881258815351903)),$sum($product(max($sum($product('X_0',$uminus(0.184467825491839488)),$sum($product('X_1',$uminus(0.268161247711679374)),$sum($product('X_2',$uminus(0.153535151736396536)),$sum($product('X_3',$uminus(0.065596192568929845)),$sum($product('X_4',0.21729520120637863),$sum($product('X_5',$uminus(0.092332864688549343)),$sum($product('X_6',0.018066462919213766),$sum($product('X_7',$uminus(0.287370290741390033)),$sum($product('X_8',$uminus(0.222457450236703963)),$uminus(0.231100948340147661)))))))))),0.0),0.058279261437098495),$sum($product(max($sum($product('X_0',0.112387308333164793),$sum($product('X_1',$uminus(0.164516529633275843)),$sum($product('X_2',0.303715756573457785),$sum($product('X_3',$uminus(0.115559064636028858)),$sum($product('X_4',$uminus(0.101279569170582118)),$sum($product('X_5',$uminus(0.312584846980395903)),$sum($product('X_6',$uminus(0.073897332022657303)),$sum($product('X_7',$uminus(0.187107831241006384)),$sum($product('X_8',0.191742606049471742),0.219833682999539703))))))))),0.0),0.123000304336519151),$sum($product(max($sum($product('X_0',0.272843083546418008),$sum($product('X_1',$uminus(0.26331667301370465)),$sum($product('X_2',0.228746460665943896),$sum($product('X_3',0.083017409074116422),$sum($product('X_4',0.2906669151723143),$sum($product('X_5',0.035447691086564703),$sum($product('X_6',0.312581653146865424),$sum($product('X_7',$uminus(0.052006990099353001)),$sum($product('X_8',$uminus(0.238709163668962665)),0.28076114529116375))))))))),0.0),$uminus(0.108282925757814397)),$sum($product(max($sum($product('X_0',0.074020874970563255),$sum($product('X_1',$uminus(0.022502229774748639)),$sum($product('X_2',0.183897093057601213),$sum($product('X_3',$uminus(0.287464703406070055)),$sum($product('X_4',$uminus(0.079254407166150287)),$sum($product('X_5',$uminus(0.330123738440344594)),$sum($product('X_6',0.302019322984987182),$sum($product('X_7',0.060629658317428392),$sum($product('X_8',$uminus(0.066123676240795071)),$uminus(0.168318244851325016)))))))))),0.0),0.095025211690298095),$sum($product(max($sum($product('X_0',0.117161478668860342),$sum($product('X_1',$uminus(0.309380508435266599)),$sum($product('X_2',0.166150746972853758),$sum($product('X_3',0.013701434090766906),$sum($product('X_4',0.141685721053067371),$sum($product('X_5',$uminus(0.028880166693844356)),$sum($product('X_6',0.260745424659842906),$sum($product('X_7',$uminus(0.158065618750375059)),$sum($product('X_8',0.095877003914591752),0.118188048960575609))))))))),0.0),0.097016468103824222),$sum($product(max($sum($product('X_0',$uminus(0.242158813559863934)),$sum($product('X_1',0.121440841134675681),$sum($product('X_2',0.244934559694501341),$sum($product('X_3',$uminus(0.317637615301534615)),$sum($product('X_4',$uminus(0.25005972927599035)),$sum($product('X_5',$uminus(0.215710382695643604)),$sum($product('X_6',0.124190735382829098),$sum($product('X_7',$uminus(0.059589490133065748)),$sum($product('X_8',0.251407265038740835),0.08916513259423331))))))))),0.0),0.042911582712372859),$uminus(0.083772180253624123))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ).
%---(Y_2 = ((max(((X_0 * -0.034143127336152712) + (X_1 * 0.322824668200060227) + (X_2 * 0.091291052421442809) + (X_3 * -0.012612789817531833) + (X_4 * 0.273541493916837075) + (X_5 * -0.150105792320639253) + (X_6 * -0.049406931293640266) + (X_7 * -0.21107752838875965) + (X_8 * 0.277909149915428422) + -0.019189099155314304), 0.0) * -0.10749292408716854) + (max(((X_0 * 0.135860462188255371) + (X_1 * 0.187969393886196101) + (X_2 * 0.174517671834989951) + (X_3 * 0.127635942676799008) + (X_4 * -0.136994285692501105) + (X_5 * 0.012365905796069943) + (X_6 * -0.027014764654490264) + (X_7 * -0.305544519265200321) + (X_8 * -0.206852248891131074) + -0.314645004469935208), 0.0) * -0.025444934006065789) + (max(((X_0 * -0.081020401392122687) + (X_1 * 0.062490409237779099) + (X_2 * 0.111520586127630439) + (X_3 * -0.213447096651937063) + (X_4 * 0.132706362488796692) + (X_5 * -0.261185283187217065) + (X_6 * 0.00474527583528711) + (X_7 * -0.06688270460651552) + (X_8 * -0.320470498630223033) + -0.190989000847826468), 0.0) * 0.048331775028051804) + (max(((X_0 * 0.138290117678506908) + (X_1 * 0.005330501640528451) + (X_2 * -0.13333471971657565) + (X_3 * 0.153277069170855151) + (X_4 * 0.193097250496935435) + (X_5 * 0.124353050256880426) + (X_6 * -0.312998335768394587) + (X_7 * 0.14582588668244395) + (X_8 * 0.017849845577707468) + -0.207803467395465624), 0.0) * 0.06298034823490356) + (max(((X_0 * 0.25616055553271605) + (X_1 * -0.03627032974016875) + (X_2 * -0.194452918074013159) + (X_3 * 0.10008950100824493) + (X_4 * 0.321933544906211566) + (X_5 * 0.302676823386164806) + (X_6 * 0.282644938195837081) + (X_7 * 0.218166819191055239) + (X_8 * 0.061315114611943666) + 0.294909295927187565), 0.0) * 0.021852100858195472) + (max(((X_0 * -0.203907213010214777) + (X_1 * -0.329328844050836067) + (X_2 * -0.282209682521432303) + (X_3 * 0.194481051286681639) + (X_4 * 0.223447381199474771) + (X_5 * -0.130047140060396471) + (X_6 * 0.258072855214746821) + (X_7 * 0.236670528410227232) + (X_8 * 0.219327984313435753) + 0.307309013280585186), 0.0) * 0.073203845426866615) + (max(((X_0 * -0.025392492262058697) + (X_1 * -0.260814592583792804) + (X_2 * -0.060464105023337156) + (X_3 * 0.235580850968075406) + (X_4 * 0.013069063238517142) + (X_5 * -0.196757326475462957) + (X_6 * 0.028155879508867165) + (X_7 * -0.181432604418310606) + (X_8 * 0.089552351207647263) + 0.233953211619548462), 0.0) * 0.056217054024664731) + (max(((X_0 * -0.316000969071793147) + (X_1 * 0.025263023662981166) + (X_2 * 0.177171946751012388) + (X_3 * -0.035122639314649318) + (X_4 * -0.23096764293788713) + (X_5 * 0.017100988871234346) + (X_6 * -0.209560107747809532) + (X_7 * -0.026921531592388137) + (X_8 * -0.032723387475881827) + 0.168724722506589486), 0.0) * 0.052260645821233631) + (max(((X_0 * 0.001306859463930443) + (X_1 * -0.32178678467757027) + (X_2 * -0.073177542048799837) + (X_3 * 0.002394918508160371) + (X_4 * 0.093730698889344044) + (X_5 * 0.008752806231017984) + (X_6 * -0.084064570826615143) + (X_7 * 0.250900209655107453) + (X_8 * 0.022976222292577286) + 0.077232081109878559), 0.0) * 0.084353338138808603) + (max(((X_0 * 0.194049225184143082) + (X_1 * -0.022183735625062984) + (X_2 * -0.196724399739592354) + (X_3 * 0.07635785513446619) + (X_4 * -0.196322916482755933) + (X_5 * -0.288926766400791291) + (X_6 * 0.213700339341032219) + (X_7 * -0.253512613136544884) + (X_8 * 0.231484855576049309) + 0.280058863303405625), 0.0) * 0.094324221587388124) + (max(((X_0 * 0.317728685554186929) + (X_1 * 0.332150001647927684) + (X_2 * -0.001259591758584755) + (X_3 * -0.207453820552864571) + (X_4 * 0.005723595304183482) + (X_5 * 0.185428526068087629) + (X_6 * 0.054353623505082105) + (X_7 * 0.132946612680298504) + (X_8 * 0.011140036900155748) + -0.209314307847249387), 0.0) * 0.028953936906730815) + (max(((X_0 * -0.269304224359853461) + (X_1 * -0.310904419113500918) + (X_2 * 0.32027709592926229) + (X_3 * -0.200037762633937188) + (X_4 * -0.026191122665172317) + (X_5 * -0.042660660377485116) + (X_6 * -0.146275965076368142) + (X_7 * -0.305670262866760689) + (X_8 * 0.322576996064118438) + -0.183572002247813032), 0.0) * 0.031108681214278511) + (max(((X_0 * 0.136084741586379454) + (X_1 * 0.26228771638376186) + (X_2 * -0.284171295665994417) + (X_3 * 0.211831054834103749) + (X_4 * 0.285004999381932744) + (X_5 * -0.007441424708356792) + (X_6 * -0.140284600003246995) + (X_7 * -0.207592415895373833) + (X_8 * 0.27321519909354347) + -0.207526152104757111), 0.0) * -0.099556705813419605) + (max(((X_0 * -0.22841409680804925) + (X_1 * 0.240551489683236974) + (X_2 * 0.312484269972083728) + (X_3 * -0.181755643345508588) + (X_4 * 0.030657116136170337) + (X_5 * -0.055299675827487349) + (X_6 * -0.062998580523338621) + (X_7 * 0.098231667492682917) + (X_8 * -0.015349265026970815) + 0.174413712522803299), 0.0) * 0.00625946211122691) + (max(((X_0 * 0.326514337483990558) + (X_1 * -0.139206653914812462) + (X_2 * -0.301944004088363971) + (X_3 * 0.007220186513743954) + (X_4 * -0.082554028749347141) + (X_5 * -0.040344607481459793) + (X_6 * -0.215478397144116013) + (X_7 * 0.145783348414039393) + (X_8 * -0.142290498498560514) + -0.21557124240865938), 0.0) * 0.118747540091114462) + (max(((X_0 * -0.001976599008208513) + (X_1 * -0.057764032526161302) + (X_2 * 0.159396263708995178) + (X_3 * -0.183991541476796888) + (X_4 * 0.142504183402018647) + (X_5 * -0.238937927812336026) + (X_6 * -0.30402575884910954) + (X_7 * 0.29491808364114086) + (X_8 * 0.054445412143243832) + -0.170312927346704335), 0.0) * 0.104189793663520019) + (max(((X_0 * -0.069437022416364014) + (X_1 * -0.00060254546898092) + (X_2 * 0.247675182881536504) + (X_3 * 0.234314025579507035) + (X_4 * -0.177673295141312471) + (X_5 * -0.332483963357472823) + (X_6 * -0.218038989896279178) + (X_7 * 0.127363049893037317) + (X_8 * -0.2086790536248469) + -0.187722099200903436), 0.0) * -0.093691513654441894) + (max(((X_0 * 0.324876735423139718) + (X_1 * 0.075982824387152592) + (X_2 * -0.313261926183435957) + (X_3 * -0.209064108357157524) + (X_4 * -0.261535938731004891) + (X_5 * -0.234787129658768606) + (X_6 * 0.112031404664260759) + (X_7 * 0.225008006173745667) + (X_8 * 0.140199347195911539) + 0.139447447171109518), 0.0) * 0.033226748160356534) + (max(((X_0 * 0.202182439886614829) + (X_1 * 0.228470631117320078) + (X_2 * 0.074549186229916131) + (X_3 * 0.233422713721841812) + (X_4 * 0.131135712704656016) + (X_5 * -0.326710062287342951) + (X_6 * 0.012038286823084332) + (X_7 * 0.231618192292777969) + (X_8 * 0.000719113164345198) + 0.213277245603735233), 0.0) * 0.005058129077434026) + (max(((X_0 * 0.28449527898218091) + (X_1 * -0.081527175695953635) + (X_2 * -0.153930222701464642) + (X_3 * -0.186077449214199719) + (X_4 * -0.05936612416981174) + (X_5 * -0.154628465341259957) + (X_6 * -0.166498063888305931) + (X_7 * 0.055266800565439478) + (X_8 * -0.213197545634780383) + 0.010205194890945457), 0.0) * 0.057406717591976186) + (max(((X_0 * -0.180816367347528484) + (X_1 * 0.043531190359145266) + (X_2 * -0.047619638831746636) + (X_3 * -0.058934638109038928) + (X_4 * -0.124666639609441937) + (X_5 * -0.318308163331019744) + (X_6 * 0.193062520783280067) + (X_7 * 0.020418055017284109) + (X_8 * 0.060922472827523722) + 0.223360539691101423), 0.0) * -0.11499567096929042) + (max(((X_0 * 0.134746472119233907) + (X_1 * -0.217554078381223898) + (X_2 * -0.085730993819177093) + (X_3 * 0.297521692708929308) + (X_4 * 0.063860554017248994) + (X_5 * 0.217082184168041759) + (X_6 * -0.021045092732637605) + (X_7 * 0.259811010052565072) + (X_8 * 0.200338555724555889) + 0.247229328571023033), 0.0) * -0.097156778957540602) + (max(((X_0 * 0.203487277967640046) + (X_1 * 0.324424625686173973) + (X_2 * -0.024662687002090788) + (X_3 * 0.216277755365953894) + (X_4 * 0.163509105125114296) + (X_5 * -0.034687792438270026) + (X_6 * 0.206452845548049824) + (X_7 * 0.154282897842712208) + (X_8 * -0.017555615896969023) + 0.272302961557755852), 0.0) * 0.050213208089163019) + (max(((X_0 * -0.244290676854412331) + (X_1 * -0.204088781911439338) + (X_2 * -0.03882746711711399) + (X_3 * -0.097232792095546527) + (X_4 * -0.303174897657345899) + (X_5 * -0.051070311788715628) + (X_6 * 0.149992479035335302) + (X_7 * -0.102185614965710991) + (X_8 * -0.106519170243570216) + 0.058597670613885988), 0.0) * 0.075903362329694385) + (max(((X_0 * 0.012864262113814806) + (X_1 * 0.109069631915820031) + (X_2 * 0.101543371952154571) + (X_3 * 0.06799496124837745) + (X_4 * -0.26445983492561137) + (X_5 * 0.215833875445791301) + (X_6 * 0.272580780248200039) + (X_7 * -0.039747643760278006) + (X_8 * -0.243825769939117892) + -0.123945865842741254), 0.0) * 0.117071543259732069) + (max(((X_0 * -0.154837365313728936) + (X_1 * 0.085840778969112019) + (X_2 * 0.165077967938471126) + (X_3 * 0.111848736690037587) + (X_4 * -0.240612563426037041) + (X_5 * 0.140637468751368289) + (X_6 * -0.149768050036042905) + (X_7 * -0.283477350113733539) + (X_8 * 0.073570979765799127) + 0.079922247453340256), 0.0) * -0.117127414463641222) + (max(((X_0 * -0.100199971469390775) + (X_1 * 0.186120110641400827) + (X_2 * 0.049038095207454113) + (X_3 * -0.196087530498076618) + (X_4 * 0.08711796538252381) + (X_5 * -0.101227855157801916) + (X_6 * 0.158620075819161321) + (X_7 * -0.146913672899774472) + (X_8 * -0.119082579355500373) + 0.138895725711660534), 0.0) * 0.073012917986197551) + (max(((X_0 * 0.180027772073166392) + (X_1 * -0.103336431479241098) + (X_2 * -0.267316901673856466) + (X_3 * 0.263656543687109834) + (X_4 * 0.332642570227415224) + (X_5 * 0.277967948182220759) + (X_6 * 0.30343956010141554) + (X_7 * 0.03447325941087459) + (X_8 * 0.125197865386826701) + 0.192506796333139885), 0.0) * 0.036191857489016793) + (max(((X_0 * -0.229596022939276084) + (X_1 * 0.306162374571047058) + (X_2 * -0.214349113239148403) + (X_3 * 0.05827258272512098) + (X_4 * 0.131302065849309368) + (X_5 * -0.271631521510831919) + (X_6 * -0.270260881180521384) + (X_7 * -0.202970959783648347) + (X_8 * 0.179428170698139933) + 0.115665614154320362), 0.0) * 0.012001299526650439) + (max(((X_0 * 0.194962600903016259) + (X_1 * -0.17835559373673493) + (X_2 * -0.228962538545053329) + (X_3 * 0.306214141164736053) + (X_4 * 0.257337107072608651) + (X_5 * -0.299595911463449771) + (X_6 * 0.089666024789417487) + (X_7 * 0.326462876291198911) + (X_8 * -0.062301378541843311) + 0.172234015205460611), 0.0) * -0.047718020776529202) + (max(((X_0 * 0.255845191590086396) + (X_1 * 0.215495725762357482) + (X_2 * -0.302097504773537306) + (X_3 * 0.095845709494328524) + (X_4 * -0.075426811348071776) + (X_5 * 0.218624900118963683) + (X_6 * 0.26160805655982583) + (X_7 * -0.212202541273525114) + (X_8 * -0.041523081831996933) + 0.102324186276997908), 0.0) * 0.073891041809129809) + (max(((X_0 * 0.30493330995168616) + (X_1 * -0.122490486481055483) + (X_2 * 0.174817256741448934) + (X_3 * -0.202369269426108028) + (X_4 * -0.323621969121451081) + (X_5 * 0.303508866087579043) + (X_6 * -0.223769302030546458) + (X_7 * -0.27502503528423522) + (X_8 * 0.129622404600985675) + -0.253776462014690563), 0.0) * -0.011131151861281635) + (max(((X_0 * 0.269059547412644651) + (X_1 * -0.005882567254681115) + (X_2 * -0.171353970135741607) + (X_3 * 0.294037626949683328) + (X_4 * -0.255251802687420648) + (X_5 * -0.009759698938691885) + (X_6 * 0.180149176039681114) + (X_7 * 0.045388866190233079) + (X_8 * -0.179760143010707252) + 0.269823604538700745), 0.0) * 0.064944743830792212) + (max(((X_0 * -0.138558699684565634) + (X_1 * 0.003660311035716235) + (X_2 * -0.328144076991653155) + (X_3 * 0.17711252434090502) + (X_4 * 0.086745978461675144) + (X_5 * 0.052468260508699016) + (X_6 * 0.051635532764924497) + (X_7 * 0.032455574507212981) + (X_8 * -0.079164165185457769) + 0.068544128415001238), 0.0) * 0.090318943668232093) + (max(((X_0 * -0.188430209592040626) + (X_1 * 0.180982936820061113) + (X_2 * 0.124800571217657474) + (X_3 * -0.054881926059530961) + (X_4 * -0.026456773114379717) + (X_5 * 0.162595317059087197) + (X_6 * 0.049021975497793691) + (X_7 * -0.246830321591287927) + (X_8 * 0.232013828123107502) + -0.062546264757998127), 0.0) * -0.059004652372120825) + (max(((X_0 * 0.040962088339393521) + (X_1 * -0.254386604085368229) + (X_2 * -0.112672966314846829) + (X_3 * -0.159902546439000759) + (X_4 * -0.207701480823660051) + (X_5 * 0.133165675227524982) + (X_6 * 0.193618244226427871) + (X_7 * 0.082613724983702452) + (X_8 * 0.322632448399385929) + 0.224209517678037373), 0.0) * 0.059029698850776358) + (max(((X_0 * -0.134886517018193708) + (X_1 * 0.144899616770255646) + (X_2 * -0.17980112071828272) + (X_3 * -0.267509492307719976) + (X_4 * -0.157528799514788709) + (X_5 * -0.079420419232439199) + (X_6 * -0.299465230679228367) + (X_7 * -0.125820656916256324) + (X_8 * 0.019239984001792998) + 0.142229458135585185), 0.0) * 0.078095912707851267) + (max(((X_0 * -0.172346696671293709) + (X_1 * 0.090451716164184959) + (X_2 * -0.228793228787715741) + (X_3 * 0.180997116632383548) + (X_4 * 0.290344111330939902) + (X_5 * -0.234970994376170916) + (X_6 * 0.005159751606115537) + (X_7 * -0.155461525393435412) + (X_8 * -0.288046325238939249) + -0.070296844355285437), 0.0) * -0.102576319270196892) + (max(((X_0 * -0.234997276198458949) + (X_1 * -0.172512713965825709) + (X_2 * 0.114308047040828642) + (X_3 * -0.063627448790975871) + (X_4 * -0.205794049922004174) + (X_5 * 0.19287844644458868) + (X_6 * -0.257664032924889597) + (X_7 * -0.233509914142561753) + (X_8 * 0.267404797826638896) + 0.248418369896963032), 0.0) * 0.082530845893993066) + (max(((X_0 * 0.296841143323539114) + (X_1 * -0.012110575240900978) + (X_2 * -0.122779558396503508) + (X_3 * 0.145965415302344859) + (X_4 * 0.115669853903047126) + (X_5 * 0.181260046623958171) + (X_6 * 0.176356841716120927) + (X_7 * 0.054758245250969895) + (X_8 * 0.066387541776141479) + 0.033378311133483385), 0.0) * -0.004491445329617622) + (max(((X_0 * -0.068127119880877884) + (X_1 * -0.193888759810902311) + (X_2 * -0.075010565817496266) + (X_3 * 0.116013395273452391) + (X_4 * 0.197890889155673377) + (X_5 * 0.321385853477913319) + (X_6 * 0.050015661552153368) + (X_7 * -0.054890782359229284) + (X_8 * 0.258758291380532579) + -0.143355802615697941), 0.0) * 0.085842128835569187) + (max(((X_0 * -0.071997512442384004) + (X_1 * 0.017303820158426297) + (X_2 * 0.091534845651731311) + (X_3 * 0.311279068800356329) + (X_4 * -0.00312157907909616) + (X_5 * -0.188277000904065517) + (X_6 * -0.183479587316280945) + (X_7 * 0.212372245445371421) + (X_8 * -0.077162998727941579) + -0.223645418757847825), 0.0) * -0.097576865502374766) + (max(((X_0 * -0.32243249625430126) + (X_1 * 0.182253848897861837) + (X_2 * -0.099368623456786598) + (X_3 * -0.156602428474534483) + (X_4 * 0.030765939328599223) + (X_5 * -0.026342715055112154) + (X_6 * 0.000532788149621544) + (X_7 * 0.303861041761946782) + (X_8 * 0.265755190798946772) + 0.100146050819974963), 0.0) * -0.084025778703360643) + (max(((X_0 * -0.112545642928356893) + (X_1 * 0.265866650798053328) + (X_2 * 0.015101151225212606) + (X_3 * -0.317799591526125247) + (X_4 * -0.168903714240354275) + (X_5 * 0.030188500593428369) + (X_6 * 0.061277558788815967) + (X_7 * 0.200866407017562254) + (X_8 * -0.112371008406928929) + -0.079493482734081355), 0.0) * -0.034735156589022237) + (max(((X_0 * -0.192154828636623531) + (X_1 * 0.083979791049164365) + (X_2 * 0.159973530860791413) + (X_3 * -0.265406610551946254) + (X_4 * 0.287198912407206131) + (X_5 * 0.095627746140380554) + (X_6 * -0.00994146969909776) + (X_7 * -0.219422562050552161) + (X_8 * -0.081085067577720604) + 0.104747771083528063), 0.0) * -0.118270746034032648) + (max(((X_0 * -0.057039132055541286) + (X_1 * 0.038985751754933406) + (X_2 * -0.004944442157409357) + (X_3 * -0.15462525839770902) + (X_4 * -0.1398935031159593) + (X_5 * -0.061959641528152032) + (X_6 * 0.098679300771940037) + (X_7 * -0.201235020697894035) + (X_8 * -0.237594859082526227) + -0.158841501426246007), 0.0) * 0.051373552185939142) + (max(((X_0 * 0.331353170527205643) + (X_1 * -0.288645365007353272) + (X_2 * 0.223956278926402741) + (X_3 * 0.279170663263683283) + (X_4 * 0.017978724577996319) + (X_5 * -0.250013034963560865) + (X_6 * 0.098807821234157156) + (X_7 * 0.258776815881270383) + (X_8 * 0.152988470579232594) + 0.28246081276552143), 0.0) * 0.100331652345120453) + (max(((X_0 * -0.100883845060276311) + (X_1 * 0.046212140463826712) + (X_2 * -0.026600669905651519) + (X_3 * 0.142320732212770695) + (X_4 * 0.072733698806154878) + (X_5 * 0.197196887480299343) + (X_6 * 0.237120144257248089) + (X_7 * -0.166327692927533299) + (X_8 * -0.078131387240757411) + -0.293417736964490861), 0.0) * -0.091927630668716565) + (max(((X_0 * 0.294400522037719437) + (X_1 * 0.082094261162431514) + (X_2 * 0.101918067411788049) + (X_3 * 0.17357922076579041) + (X_4 * 0.114082861901367405) + (X_5 * -0.311032034544396929) + (X_6 * 0.258029579372313467) + (X_7 * 0.145657792087877658) + (X_8 * -0.033975658190385893) + 0.194899911587433305), 0.0) * 0.010671274760385541) + (max(((X_0 * 0.034313476891573602) + (X_1 * -0.189736665978239627) + (X_2 * 0.098474573164286039) + (X_3 * 0.220418718662632351) + (X_4 * 0.03836653204063839) + (X_5 * 0.279710695915403817) + (X_6 * 0.14410430753399317) + (X_7 * 0.204156618335651407) + (X_8 * 0.176473915501038803) + -0.03827183418778396), 0.0) * -0.092607909899420082) + (max(((X_0 * 0.00869382371014682) + (X_1 * -0.310492767426873872) + (X_2 * 0.117116910196331914) + (X_3 * 0.169087657846020811) + (X_4 * -0.273335058913078577) + (X_5 * -0.000683592328365401) + (X_6 * 0.139512227022986102) + (X_7 * -0.313799159812941153) + (X_8 * -0.196166996347198946) + 0.236750714424111497), 0.0) * -0.042263748114422739) + (max(((X_0 * 0.137861025679069715) + (X_1 * -0.024667890831123473) + (X_2 * -0.315714844767212732) + (X_3 * 0.237047096266294222) + (X_4 * 0.202101116810822823) + (X_5 * -0.020405610795288631) + (X_6 * 0.223248306677427399) + (X_7 * 0.166427221032260431) + (X_8 * 0.322898701032060254) + 0.085041015223344729), 0.0) * -0.089157291219461171) + (max(((X_0 * 0.063704153901590399) + (X_1 * 0.084893455136697493) + (X_2 * 0.162022423603656263) + (X_3 * -0.026069359722939833) + (X_4 * -0.103610576532342291) + (X_5 * 0.247462072588003845) + (X_6 * 0.235604458158232999) + (X_7 * 0.094778590268327412) + (X_8 * 0.317884709780666685) + -0.259110365198896853), 0.0) * -0.06510923211031816) + (max(((X_0 * 0.157051962420222013) + (X_1 * 0.02119912918435074) + (X_2 * -0.144567654546317315) + (X_3 * -0.120485782181390416) + (X_4 * 0.245385692300038649) + (X_5 * -0.12013008718360596) + (X_6 * -0.264054168644354381) + (X_7 * 0.113466930567937607) + (X_8 * 0.018847290606381961) + -0.306458405399606004), 0.0) * 0.08954218524327956) + (max(((X_0 * 0.287194094745330031) + (X_1 * -0.279329006877257702) + (X_2 * -0.27381666760090273) + (X_3 * -0.241196338354026901) + (X_4 * 0.166076860453970354) + (X_5 * 0.003947070874237735) + (X_6 * -0.079391976830132827) + (X_7 * -0.311101692329606716) + (X_8 * 0.028656916570530377) + -0.242226407222209617), 0.0) * 0.072530356741432905) + (max(((X_0 * 0.04404093390102809) + (X_1 * 0.223856941183437852) + (X_2 * 0.030174154656356367) + (X_3 * -0.093021470933494721) + (X_4 * -0.040972965799927652) + (X_5 * 0.134584475865453967) + (X_6 * 0.312199328391165765) + (X_7 * 0.040627871296072593) + (X_8 * -0.123070819674687693) + 0.158068620935378545), 0.0) * 0.031019648051496651) + (max(((X_0 * 0.309415963276349515) + (X_1 * 0.039481469238021816) + (X_2 * 0.15094441592481006) + (X_3 * 0.30522360340783411) + (X_4 * -0.229798563734669559) + (X_5 * -0.192960605209967856) + (X_6 * -0.20370062757883689) + (X_7 * -0.047763191941385397) + (X_8 * -0.266019895781817062) + -0.3239652657122854), 0.0) * 0.014296021586679558) + (max(((X_0 * 0.291655730227005694) + (X_1 * -0.211448651190053294) + (X_2 * 0.262759471678295109) + (X_3 * 0.250069844719772838) + (X_4 * -0.0381186790917451) + (X_5 * -0.146083546836047795) + (X_6 * -0.151529498387592332) + (X_7 * 0.201164755659322625) + (X_8 * 0.146160292641425327) + -0.046301663710338892), 0.0) * 0.121361832369365152) + (max(((X_0 * -0.184467825491839488) + (X_1 * -0.268161247711679374) + (X_2 * -0.153535151736396536) + (X_3 * -0.065596192568929845) + (X_4 * 0.21729520120637863) + (X_5 * -0.092332864688549343) + (X_6 * 0.018066462919213766) + (X_7 * -0.287370290741390033) + (X_8 * -0.222457450236703963) + -0.231100948340147661), 0.0) * 0.065772794248384892) + (max(((X_0 * 0.112387308333164793) + (X_1 * -0.164516529633275843) + (X_2 * 0.303715756573457785) + (X_3 * -0.115559064636028858) + (X_4 * -0.101279569170582118) + (X_5 * -0.312584846980395903) + (X_6 * -0.073897332022657303) + (X_7 * -0.187107831241006384) + (X_8 * 0.191742606049471742) + 0.219833682999539703), 0.0) * 0.104689867766233291) + (max(((X_0 * 0.272843083546418008) + (X_1 * -0.26331667301370465) + (X_2 * 0.228746460665943896) + (X_3 * 0.083017409074116422) + (X_4 * 0.2906669151723143) + (X_5 * 0.035447691086564703) + (X_6 * 0.312581653146865424) + (X_7 * -0.052006990099353001) + (X_8 * -0.238709163668962665) + 0.28076114529116375), 0.0) * 0.103569185790112789) + (max(((X_0 * 0.074020874970563255) + (X_1 * -0.022502229774748639) + (X_2 * 0.183897093057601213) + (X_3 * -0.287464703406070055) + (X_4 * -0.079254407166150287) + (X_5 * -0.330123738440344594) + (X_6 * 0.302019322984987182) + (X_7 * 0.060629658317428392) + (X_8 * -0.066123676240795071) + -0.168318244851325016), 0.0) * -0.096451090569280251) + (max(((X_0 * 0.117161478668860342) + (X_1 * -0.309380508435266599) + (X_2 * 0.166150746972853758) + (X_3 * 0.013701434090766906) + (X_4 * 0.141685721053067371) + (X_5 * -0.028880166693844356) + (X_6 * 0.260745424659842906) + (X_7 * -0.158065618750375059) + (X_8 * 0.095877003914591752) + 0.118188048960575609), 0.0) * -0.050297575744101902) + (max(((X_0 * -0.242158813559863934) + (X_1 * 0.121440841134675681) + (X_2 * 0.244934559694501341) + (X_3 * -0.317637615301534615) + (X_4 * -0.25005972927599035) + (X_5 * -0.215710382695643604) + (X_6 * 0.124190735382829098) + (X_7 * -0.059589490133065748) + (X_8 * 0.251407265038740835) + 0.08916513259423331), 0.0) * -0.01178624591574956) + 0.014290126991849089))
tff(formula_22,axiom,
'Y_2' = $sum($product(max($sum($product('X_0',$uminus(0.034143127336152712)),$sum($product('X_1',0.322824668200060227),$sum($product('X_2',0.091291052421442809),$sum($product('X_3',$uminus(0.012612789817531833)),$sum($product('X_4',0.273541493916837075),$sum($product('X_5',$uminus(0.150105792320639253)),$sum($product('X_6',$uminus(0.049406931293640266)),$sum($product('X_7',$uminus(0.21107752838875965)),$sum($product('X_8',0.277909149915428422),$uminus(0.019189099155314304)))))))))),0.0),$uminus(0.10749292408716854)),$sum($product(max($sum($product('X_0',0.135860462188255371),$sum($product('X_1',0.187969393886196101),$sum($product('X_2',0.174517671834989951),$sum($product('X_3',0.127635942676799008),$sum($product('X_4',$uminus(0.136994285692501105)),$sum($product('X_5',0.012365905796069943),$sum($product('X_6',$uminus(0.027014764654490264)),$sum($product('X_7',$uminus(0.305544519265200321)),$sum($product('X_8',$uminus(0.206852248891131074)),$uminus(0.314645004469935208)))))))))),0.0),$uminus(0.025444934006065789)),$sum($product(max($sum($product('X_0',$uminus(0.081020401392122687)),$sum($product('X_1',0.062490409237779099),$sum($product('X_2',0.111520586127630439),$sum($product('X_3',$uminus(0.213447096651937063)),$sum($product('X_4',0.132706362488796692),$sum($product('X_5',$uminus(0.261185283187217065)),$sum($product('X_6',0.00474527583528711),$sum($product('X_7',$uminus(0.06688270460651552)),$sum($product('X_8',$uminus(0.320470498630223033)),$uminus(0.190989000847826468)))))))))),0.0),0.048331775028051804),$sum($product(max($sum($product('X_0',0.138290117678506908),$sum($product('X_1',0.005330501640528451),$sum($product('X_2',$uminus(0.13333471971657565)),$sum($product('X_3',0.153277069170855151),$sum($product('X_4',0.193097250496935435),$sum($product('X_5',0.124353050256880426),$sum($product('X_6',$uminus(0.312998335768394587)),$sum($product('X_7',0.14582588668244395),$sum($product('X_8',0.017849845577707468),$uminus(0.207803467395465624)))))))))),0.0),0.06298034823490356),$sum($product(max($sum($product('X_0',0.25616055553271605),$sum($product('X_1',$uminus(0.03627032974016875)),$sum($product('X_2',$uminus(0.194452918074013159)),$sum($product('X_3',0.10008950100824493),$sum($product('X_4',0.321933544906211566),$sum($product('X_5',0.302676823386164806),$sum($product('X_6',0.282644938195837081),$sum($product('X_7',0.218166819191055239),$sum($product('X_8',0.061315114611943666),0.294909295927187565))))))))),0.0),0.021852100858195472),$sum($product(max($sum($product('X_0',$uminus(0.203907213010214777)),$sum($product('X_1',$uminus(0.329328844050836067)),$sum($product('X_2',$uminus(0.282209682521432303)),$sum($product('X_3',0.194481051286681639),$sum($product('X_4',0.223447381199474771),$sum($product('X_5',$uminus(0.130047140060396471)),$sum($product('X_6',0.258072855214746821),$sum($product('X_7',0.236670528410227232),$sum($product('X_8',0.219327984313435753),0.307309013280585186))))))))),0.0),0.073203845426866615),$sum($product(max($sum($product('X_0',$uminus(0.025392492262058697)),$sum($product('X_1',$uminus(0.260814592583792804)),$sum($product('X_2',$uminus(0.060464105023337156)),$sum($product('X_3',0.235580850968075406),$sum($product('X_4',0.013069063238517142),$sum($product('X_5',$uminus(0.196757326475462957)),$sum($product('X_6',0.028155879508867165),$sum($product('X_7',$uminus(0.181432604418310606)),$sum($product('X_8',0.089552351207647263),0.233953211619548462))))))))),0.0),0.056217054024664731),$sum($product(max($sum($product('X_0',$uminus(0.316000969071793147)),$sum($product('X_1',0.025263023662981166),$sum($product('X_2',0.177171946751012388),$sum($product('X_3',$uminus(0.035122639314649318)),$sum($product('X_4',$uminus(0.23096764293788713)),$sum($product('X_5',0.017100988871234346),$sum($product('X_6',$uminus(0.209560107747809532)),$sum($product('X_7',$uminus(0.026921531592388137)),$sum($product('X_8',$uminus(0.032723387475881827)),0.168724722506589486))))))))),0.0),0.052260645821233631),$sum($product(max($sum($product('X_0',0.001306859463930443),$sum($product('X_1',$uminus(0.32178678467757027)),$sum($product('X_2',$uminus(0.073177542048799837)),$sum($product('X_3',0.002394918508160371),$sum($product('X_4',0.093730698889344044),$sum($product('X_5',0.008752806231017984),$sum($product('X_6',$uminus(0.084064570826615143)),$sum($product('X_7',0.250900209655107453),$sum($product('X_8',0.022976222292577286),0.077232081109878559))))))))),0.0),0.084353338138808603),$sum($product(max($sum($product('X_0',0.194049225184143082),$sum($product('X_1',$uminus(0.022183735625062984)),$sum($product('X_2',$uminus(0.196724399739592354)),$sum($product('X_3',0.07635785513446619),$sum($product('X_4',$uminus(0.196322916482755933)),$sum($product('X_5',$uminus(0.288926766400791291)),$sum($product('X_6',0.213700339341032219),$sum($product('X_7',$uminus(0.253512613136544884)),$sum($product('X_8',0.231484855576049309),0.280058863303405625))))))))),0.0),0.094324221587388124),$sum($product(max($sum($product('X_0',0.317728685554186929),$sum($product('X_1',0.332150001647927684),$sum($product('X_2',$uminus(0.001259591758584755)),$sum($product('X_3',$uminus(0.207453820552864571)),$sum($product('X_4',0.005723595304183482),$sum($product('X_5',0.185428526068087629),$sum($product('X_6',0.054353623505082105),$sum($product('X_7',0.132946612680298504),$sum($product('X_8',0.011140036900155748),$uminus(0.209314307847249387)))))))))),0.0),0.028953936906730815),$sum($product(max($sum($product('X_0',$uminus(0.269304224359853461)),$sum($product('X_1',$uminus(0.310904419113500918)),$sum($product('X_2',0.32027709592926229),$sum($product('X_3',$uminus(0.200037762633937188)),$sum($product('X_4',$uminus(0.026191122665172317)),$sum($product('X_5',$uminus(0.042660660377485116)),$sum($product('X_6',$uminus(0.146275965076368142)),$sum($product('X_7',$uminus(0.305670262866760689)),$sum($product('X_8',0.322576996064118438),$uminus(0.183572002247813032)))))))))),0.0),0.031108681214278511),$sum($product(max($sum($product('X_0',0.136084741586379454),$sum($product('X_1',0.26228771638376186),$sum($product('X_2',$uminus(0.284171295665994417)),$sum($product('X_3',0.211831054834103749),$sum($product('X_4',0.285004999381932744),$sum($product('X_5',$uminus(0.007441424708356792)),$sum($product('X_6',$uminus(0.140284600003246995)),$sum($product('X_7',$uminus(0.207592415895373833)),$sum($product('X_8',0.27321519909354347),$uminus(0.207526152104757111)))))))))),0.0),$uminus(0.099556705813419605)),$sum($product(max($sum($product('X_0',$uminus(0.22841409680804925)),$sum($product('X_1',0.240551489683236974),$sum($product('X_2',0.312484269972083728),$sum($product('X_3',$uminus(0.181755643345508588)),$sum($product('X_4',0.030657116136170337),$sum($product('X_5',$uminus(0.055299675827487349)),$sum($product('X_6',$uminus(0.062998580523338621)),$sum($product('X_7',0.098231667492682917),$sum($product('X_8',$uminus(0.015349265026970815)),0.174413712522803299))))))))),0.0),0.00625946211122691),$sum($product(max($sum($product('X_0',0.326514337483990558),$sum($product('X_1',$uminus(0.139206653914812462)),$sum($product('X_2',$uminus(0.301944004088363971)),$sum($product('X_3',0.007220186513743954),$sum($product('X_4',$uminus(0.082554028749347141)),$sum($product('X_5',$uminus(0.040344607481459793)),$sum($product('X_6',$uminus(0.215478397144116013)),$sum($product('X_7',0.145783348414039393),$sum($product('X_8',$uminus(0.142290498498560514)),$uminus(0.21557124240865938)))))))))),0.0),0.118747540091114462),$sum($product(max($sum($product('X_0',$uminus(0.001976599008208513)),$sum($product('X_1',$uminus(0.057764032526161302)),$sum($product('X_2',0.159396263708995178),$sum($product('X_3',$uminus(0.183991541476796888)),$sum($product('X_4',0.142504183402018647),$sum($product('X_5',$uminus(0.238937927812336026)),$sum($product('X_6',$uminus(0.30402575884910954)),$sum($product('X_7',0.29491808364114086),$sum($product('X_8',0.054445412143243832),$uminus(0.170312927346704335)))))))))),0.0),0.104189793663520019),$sum($product(max($sum($product('X_0',$uminus(0.069437022416364014)),$sum($product('X_1',$uminus(0.00060254546898092)),$sum($product('X_2',0.247675182881536504),$sum($product('X_3',0.234314025579507035),$sum($product('X_4',$uminus(0.177673295141312471)),$sum($product('X_5',$uminus(0.332483963357472823)),$sum($product('X_6',$uminus(0.218038989896279178)),$sum($product('X_7',0.127363049893037317),$sum($product('X_8',$uminus(0.2086790536248469)),$uminus(0.187722099200903436)))))))))),0.0),$uminus(0.093691513654441894)),$sum($product(max($sum($product('X_0',0.324876735423139718),$sum($product('X_1',0.075982824387152592),$sum($product('X_2',$uminus(0.313261926183435957)),$sum($product('X_3',$uminus(0.209064108357157524)),$sum($product('X_4',$uminus(0.261535938731004891)),$sum($product('X_5',$uminus(0.234787129658768606)),$sum($product('X_6',0.112031404664260759),$sum($product('X_7',0.225008006173745667),$sum($product('X_8',0.140199347195911539),0.139447447171109518))))))))),0.0),0.033226748160356534),$sum($product(max($sum($product('X_0',0.202182439886614829),$sum($product('X_1',0.228470631117320078),$sum($product('X_2',0.074549186229916131),$sum($product('X_3',0.233422713721841812),$sum($product('X_4',0.131135712704656016),$sum($product('X_5',$uminus(0.326710062287342951)),$sum($product('X_6',0.012038286823084332),$sum($product('X_7',0.231618192292777969),$sum($product('X_8',0.000719113164345198),0.213277245603735233))))))))),0.0),0.005058129077434026),$sum($product(max($sum($product('X_0',0.28449527898218091),$sum($product('X_1',$uminus(0.081527175695953635)),$sum($product('X_2',$uminus(0.153930222701464642)),$sum($product('X_3',$uminus(0.186077449214199719)),$sum($product('X_4',$uminus(0.05936612416981174)),$sum($product('X_5',$uminus(0.154628465341259957)),$sum($product('X_6',$uminus(0.166498063888305931)),$sum($product('X_7',0.055266800565439478),$sum($product('X_8',$uminus(0.213197545634780383)),0.010205194890945457))))))))),0.0),0.057406717591976186),$sum($product(max($sum($product('X_0',$uminus(0.180816367347528484)),$sum($product('X_1',0.043531190359145266),$sum($product('X_2',$uminus(0.047619638831746636)),$sum($product('X_3',$uminus(0.058934638109038928)),$sum($product('X_4',$uminus(0.124666639609441937)),$sum($product('X_5',$uminus(0.318308163331019744)),$sum($product('X_6',0.193062520783280067),$sum($product('X_7',0.020418055017284109),$sum($product('X_8',0.060922472827523722),0.223360539691101423))))))))),0.0),$uminus(0.11499567096929042)),$sum($product(max($sum($product('X_0',0.134746472119233907),$sum($product('X_1',$uminus(0.217554078381223898)),$sum($product('X_2',$uminus(0.085730993819177093)),$sum($product('X_3',0.297521692708929308),$sum($product('X_4',0.063860554017248994),$sum($product('X_5',0.217082184168041759),$sum($product('X_6',$uminus(0.021045092732637605)),$sum($product('X_7',0.259811010052565072),$sum($product('X_8',0.200338555724555889),0.247229328571023033))))))))),0.0),$uminus(0.097156778957540602)),$sum($product(max($sum($product('X_0',0.203487277967640046),$sum($product('X_1',0.324424625686173973),$sum($product('X_2',$uminus(0.024662687002090788)),$sum($product('X_3',0.216277755365953894),$sum($product('X_4',0.163509105125114296),$sum($product('X_5',$uminus(0.034687792438270026)),$sum($product('X_6',0.206452845548049824),$sum($product('X_7',0.154282897842712208),$sum($product('X_8',$uminus(0.017555615896969023)),0.272302961557755852))))))))),0.0),0.050213208089163019),$sum($product(max($sum($product('X_0',$uminus(0.244290676854412331)),$sum($product('X_1',$uminus(0.204088781911439338)),$sum($product('X_2',$uminus(0.03882746711711399)),$sum($product('X_3',$uminus(0.097232792095546527)),$sum($product('X_4',$uminus(0.303174897657345899)),$sum($product('X_5',$uminus(0.051070311788715628)),$sum($product('X_6',0.149992479035335302),$sum($product('X_7',$uminus(0.102185614965710991)),$sum($product('X_8',$uminus(0.106519170243570216)),0.058597670613885988))))))))),0.0),0.075903362329694385),$sum($product(max($sum($product('X_0',0.012864262113814806),$sum($product('X_1',0.109069631915820031),$sum($product('X_2',0.101543371952154571),$sum($product('X_3',0.06799496124837745),$sum($product('X_4',$uminus(0.26445983492561137)),$sum($product('X_5',0.215833875445791301),$sum($product('X_6',0.272580780248200039),$sum($product('X_7',$uminus(0.039747643760278006)),$sum($product('X_8',$uminus(0.243825769939117892)),$uminus(0.123945865842741254)))))))))),0.0),0.117071543259732069),$sum($product(max($sum($product('X_0',$uminus(0.154837365313728936)),$sum($product('X_1',0.085840778969112019),$sum($product('X_2',0.165077967938471126),$sum($product('X_3',0.111848736690037587),$sum($product('X_4',$uminus(0.240612563426037041)),$sum($product('X_5',0.140637468751368289),$sum($product('X_6',$uminus(0.149768050036042905)),$sum($product('X_7',$uminus(0.283477350113733539)),$sum($product('X_8',0.073570979765799127),0.079922247453340256))))))))),0.0),$uminus(0.117127414463641222)),$sum($product(max($sum($product('X_0',$uminus(0.100199971469390775)),$sum($product('X_1',0.186120110641400827),$sum($product('X_2',0.049038095207454113),$sum($product('X_3',$uminus(0.196087530498076618)),$sum($product('X_4',0.08711796538252381),$sum($product('X_5',$uminus(0.101227855157801916)),$sum($product('X_6',0.158620075819161321),$sum($product('X_7',$uminus(0.146913672899774472)),$sum($product('X_8',$uminus(0.119082579355500373)),0.138895725711660534))))))))),0.0),0.073012917986197551),$sum($product(max($sum($product('X_0',0.180027772073166392),$sum($product('X_1',$uminus(0.103336431479241098)),$sum($product('X_2',$uminus(0.267316901673856466)),$sum($product('X_3',0.263656543687109834),$sum($product('X_4',0.332642570227415224),$sum($product('X_5',0.277967948182220759),$sum($product('X_6',0.30343956010141554),$sum($product('X_7',0.03447325941087459),$sum($product('X_8',0.125197865386826701),0.192506796333139885))))))))),0.0),0.036191857489016793),$sum($product(max($sum($product('X_0',$uminus(0.229596022939276084)),$sum($product('X_1',0.306162374571047058),$sum($product('X_2',$uminus(0.214349113239148403)),$sum($product('X_3',0.05827258272512098),$sum($product('X_4',0.131302065849309368),$sum($product('X_5',$uminus(0.271631521510831919)),$sum($product('X_6',$uminus(0.270260881180521384)),$sum($product('X_7',$uminus(0.202970959783648347)),$sum($product('X_8',0.179428170698139933),0.115665614154320362))))))))),0.0),0.012001299526650439),$sum($product(max($sum($product('X_0',0.194962600903016259),$sum($product('X_1',$uminus(0.17835559373673493)),$sum($product('X_2',$uminus(0.228962538545053329)),$sum($product('X_3',0.306214141164736053),$sum($product('X_4',0.257337107072608651),$sum($product('X_5',$uminus(0.299595911463449771)),$sum($product('X_6',0.089666024789417487),$sum($product('X_7',0.326462876291198911),$sum($product('X_8',$uminus(0.062301378541843311)),0.172234015205460611))))))))),0.0),$uminus(0.047718020776529202)),$sum($product(max($sum($product('X_0',0.255845191590086396),$sum($product('X_1',0.215495725762357482),$sum($product('X_2',$uminus(0.302097504773537306)),$sum($product('X_3',0.095845709494328524),$sum($product('X_4',$uminus(0.075426811348071776)),$sum($product('X_5',0.218624900118963683),$sum($product('X_6',0.26160805655982583),$sum($product('X_7',$uminus(0.212202541273525114)),$sum($product('X_8',$uminus(0.041523081831996933)),0.102324186276997908))))))))),0.0),0.073891041809129809),$sum($product(max($sum($product('X_0',0.30493330995168616),$sum($product('X_1',$uminus(0.122490486481055483)),$sum($product('X_2',0.174817256741448934),$sum($product('X_3',$uminus(0.202369269426108028)),$sum($product('X_4',$uminus(0.323621969121451081)),$sum($product('X_5',0.303508866087579043),$sum($product('X_6',$uminus(0.223769302030546458)),$sum($product('X_7',$uminus(0.27502503528423522)),$sum($product('X_8',0.129622404600985675),$uminus(0.253776462014690563)))))))))),0.0),$uminus(0.011131151861281635)),$sum($product(max($sum($product('X_0',0.269059547412644651),$sum($product('X_1',$uminus(0.005882567254681115)),$sum($product('X_2',$uminus(0.171353970135741607)),$sum($product('X_3',0.294037626949683328),$sum($product('X_4',$uminus(0.255251802687420648)),$sum($product('X_5',$uminus(0.009759698938691885)),$sum($product('X_6',0.180149176039681114),$sum($product('X_7',0.045388866190233079),$sum($product('X_8',$uminus(0.179760143010707252)),0.269823604538700745))))))))),0.0),0.064944743830792212),$sum($product(max($sum($product('X_0',$uminus(0.138558699684565634)),$sum($product('X_1',0.003660311035716235),$sum($product('X_2',$uminus(0.328144076991653155)),$sum($product('X_3',0.17711252434090502),$sum($product('X_4',0.086745978461675144),$sum($product('X_5',0.052468260508699016),$sum($product('X_6',0.051635532764924497),$sum($product('X_7',0.032455574507212981),$sum($product('X_8',$uminus(0.079164165185457769)),0.068544128415001238))))))))),0.0),0.090318943668232093),$sum($product(max($sum($product('X_0',$uminus(0.188430209592040626)),$sum($product('X_1',0.180982936820061113),$sum($product('X_2',0.124800571217657474),$sum($product('X_3',$uminus(0.054881926059530961)),$sum($product('X_4',$uminus(0.026456773114379717)),$sum($product('X_5',0.162595317059087197),$sum($product('X_6',0.049021975497793691),$sum($product('X_7',$uminus(0.246830321591287927)),$sum($product('X_8',0.232013828123107502),$uminus(0.062546264757998127)))))))))),0.0),$uminus(0.059004652372120825)),$sum($product(max($sum($product('X_0',0.040962088339393521),$sum($product('X_1',$uminus(0.254386604085368229)),$sum($product('X_2',$uminus(0.112672966314846829)),$sum($product('X_3',$uminus(0.159902546439000759)),$sum($product('X_4',$uminus(0.207701480823660051)),$sum($product('X_5',0.133165675227524982),$sum($product('X_6',0.193618244226427871),$sum($product('X_7',0.082613724983702452),$sum($product('X_8',0.322632448399385929),0.224209517678037373))))))))),0.0),0.059029698850776358),$sum($product(max($sum($product('X_0',$uminus(0.134886517018193708)),$sum($product('X_1',0.144899616770255646),$sum($product('X_2',$uminus(0.17980112071828272)),$sum($product('X_3',$uminus(0.267509492307719976)),$sum($product('X_4',$uminus(0.157528799514788709)),$sum($product('X_5',$uminus(0.079420419232439199)),$sum($product('X_6',$uminus(0.299465230679228367)),$sum($product('X_7',$uminus(0.125820656916256324)),$sum($product('X_8',0.019239984001792998),0.142229458135585185))))))))),0.0),0.078095912707851267),$sum($product(max($sum($product('X_0',$uminus(0.172346696671293709)),$sum($product('X_1',0.090451716164184959),$sum($product('X_2',$uminus(0.228793228787715741)),$sum($product('X_3',0.180997116632383548),$sum($product('X_4',0.290344111330939902),$sum($product('X_5',$uminus(0.234970994376170916)),$sum($product('X_6',0.005159751606115537),$sum($product('X_7',$uminus(0.155461525393435412)),$sum($product('X_8',$uminus(0.288046325238939249)),$uminus(0.070296844355285437)))))))))),0.0),$uminus(0.102576319270196892)),$sum($product(max($sum($product('X_0',$uminus(0.234997276198458949)),$sum($product('X_1',$uminus(0.172512713965825709)),$sum($product('X_2',0.114308047040828642),$sum($product('X_3',$uminus(0.063627448790975871)),$sum($product('X_4',$uminus(0.205794049922004174)),$sum($product('X_5',0.19287844644458868),$sum($product('X_6',$uminus(0.257664032924889597)),$sum($product('X_7',$uminus(0.233509914142561753)),$sum($product('X_8',0.267404797826638896),0.248418369896963032))))))))),0.0),0.082530845893993066),$sum($product(max($sum($product('X_0',0.296841143323539114),$sum($product('X_1',$uminus(0.012110575240900978)),$sum($product('X_2',$uminus(0.122779558396503508)),$sum($product('X_3',0.145965415302344859),$sum($product('X_4',0.115669853903047126),$sum($product('X_5',0.181260046623958171),$sum($product('X_6',0.176356841716120927),$sum($product('X_7',0.054758245250969895),$sum($product('X_8',0.066387541776141479),0.033378311133483385))))))))),0.0),$uminus(0.004491445329617622)),$sum($product(max($sum($product('X_0',$uminus(0.068127119880877884)),$sum($product('X_1',$uminus(0.193888759810902311)),$sum($product('X_2',$uminus(0.075010565817496266)),$sum($product('X_3',0.116013395273452391),$sum($product('X_4',0.197890889155673377),$sum($product('X_5',0.321385853477913319),$sum($product('X_6',0.050015661552153368),$sum($product('X_7',$uminus(0.054890782359229284)),$sum($product('X_8',0.258758291380532579),$uminus(0.143355802615697941)))))))))),0.0),0.085842128835569187),$sum($product(max($sum($product('X_0',$uminus(0.071997512442384004)),$sum($product('X_1',0.017303820158426297),$sum($product('X_2',0.091534845651731311),$sum($product('X_3',0.311279068800356329),$sum($product('X_4',$uminus(0.00312157907909616)),$sum($product('X_5',$uminus(0.188277000904065517)),$sum($product('X_6',$uminus(0.183479587316280945)),$sum($product('X_7',0.212372245445371421),$sum($product('X_8',$uminus(0.077162998727941579)),$uminus(0.223645418757847825)))))))))),0.0),$uminus(0.097576865502374766)),$sum($product(max($sum($product('X_0',$uminus(0.32243249625430126)),$sum($product('X_1',0.182253848897861837),$sum($product('X_2',$uminus(0.099368623456786598)),$sum($product('X_3',$uminus(0.156602428474534483)),$sum($product('X_4',0.030765939328599223),$sum($product('X_5',$uminus(0.026342715055112154)),$sum($product('X_6',0.000532788149621544),$sum($product('X_7',0.303861041761946782),$sum($product('X_8',0.265755190798946772),0.100146050819974963))))))))),0.0),$uminus(0.084025778703360643)),$sum($product(max($sum($product('X_0',$uminus(0.112545642928356893)),$sum($product('X_1',0.265866650798053328),$sum($product('X_2',0.015101151225212606),$sum($product('X_3',$uminus(0.317799591526125247)),$sum($product('X_4',$uminus(0.168903714240354275)),$sum($product('X_5',0.030188500593428369),$sum($product('X_6',0.061277558788815967),$sum($product('X_7',0.200866407017562254),$sum($product('X_8',$uminus(0.112371008406928929)),$uminus(0.079493482734081355)))))))))),0.0),$uminus(0.034735156589022237)),$sum($product(max($sum($product('X_0',$uminus(0.192154828636623531)),$sum($product('X_1',0.083979791049164365),$sum($product('X_2',0.159973530860791413),$sum($product('X_3',$uminus(0.265406610551946254)),$sum($product('X_4',0.287198912407206131),$sum($product('X_5',0.095627746140380554),$sum($product('X_6',$uminus(0.00994146969909776)),$sum($product('X_7',$uminus(0.219422562050552161)),$sum($product('X_8',$uminus(0.081085067577720604)),0.104747771083528063))))))))),0.0),$uminus(0.118270746034032648)),$sum($product(max($sum($product('X_0',$uminus(0.057039132055541286)),$sum($product('X_1',0.038985751754933406),$sum($product('X_2',$uminus(0.004944442157409357)),$sum($product('X_3',$uminus(0.15462525839770902)),$sum($product('X_4',$uminus(0.1398935031159593)),$sum($product('X_5',$uminus(0.061959641528152032)),$sum($product('X_6',0.098679300771940037),$sum($product('X_7',$uminus(0.201235020697894035)),$sum($product('X_8',$uminus(0.237594859082526227)),$uminus(0.158841501426246007)))))))))),0.0),0.051373552185939142),$sum($product(max($sum($product('X_0',0.331353170527205643),$sum($product('X_1',$uminus(0.288645365007353272)),$sum($product('X_2',0.223956278926402741),$sum($product('X_3',0.279170663263683283),$sum($product('X_4',0.017978724577996319),$sum($product('X_5',$uminus(0.250013034963560865)),$sum($product('X_6',0.098807821234157156),$sum($product('X_7',0.258776815881270383),$sum($product('X_8',0.152988470579232594),0.28246081276552143))))))))),0.0),0.100331652345120453),$sum($product(max($sum($product('X_0',$uminus(0.100883845060276311)),$sum($product('X_1',0.046212140463826712),$sum($product('X_2',$uminus(0.026600669905651519)),$sum($product('X_3',0.142320732212770695),$sum($product('X_4',0.072733698806154878),$sum($product('X_5',0.197196887480299343),$sum($product('X_6',0.237120144257248089),$sum($product('X_7',$uminus(0.166327692927533299)),$sum($product('X_8',$uminus(0.078131387240757411)),$uminus(0.293417736964490861)))))))))),0.0),$uminus(0.091927630668716565)),$sum($product(max($sum($product('X_0',0.294400522037719437),$sum($product('X_1',0.082094261162431514),$sum($product('X_2',0.101918067411788049),$sum($product('X_3',0.17357922076579041),$sum($product('X_4',0.114082861901367405),$sum($product('X_5',$uminus(0.311032034544396929)),$sum($product('X_6',0.258029579372313467),$sum($product('X_7',0.145657792087877658),$sum($product('X_8',$uminus(0.033975658190385893)),0.194899911587433305))))))))),0.0),0.010671274760385541),$sum($product(max($sum($product('X_0',0.034313476891573602),$sum($product('X_1',$uminus(0.189736665978239627)),$sum($product('X_2',0.098474573164286039),$sum($product('X_3',0.220418718662632351),$sum($product('X_4',0.03836653204063839),$sum($product('X_5',0.279710695915403817),$sum($product('X_6',0.14410430753399317),$sum($product('X_7',0.204156618335651407),$sum($product('X_8',0.176473915501038803),$uminus(0.03827183418778396)))))))))),0.0),$uminus(0.092607909899420082)),$sum($product(max($sum($product('X_0',0.00869382371014682),$sum($product('X_1',$uminus(0.310492767426873872)),$sum($product('X_2',0.117116910196331914),$sum($product('X_3',0.169087657846020811),$sum($product('X_4',$uminus(0.273335058913078577)),$sum($product('X_5',$uminus(0.000683592328365401)),$sum($product('X_6',0.139512227022986102),$sum($product('X_7',$uminus(0.313799159812941153)),$sum($product('X_8',$uminus(0.196166996347198946)),0.236750714424111497))))))))),0.0),$uminus(0.042263748114422739)),$sum($product(max($sum($product('X_0',0.137861025679069715),$sum($product('X_1',$uminus(0.024667890831123473)),$sum($product('X_2',$uminus(0.315714844767212732)),$sum($product('X_3',0.237047096266294222),$sum($product('X_4',0.202101116810822823),$sum($product('X_5',$uminus(0.020405610795288631)),$sum($product('X_6',0.223248306677427399),$sum($product('X_7',0.166427221032260431),$sum($product('X_8',0.322898701032060254),0.085041015223344729))))))))),0.0),$uminus(0.089157291219461171)),$sum($product(max($sum($product('X_0',0.063704153901590399),$sum($product('X_1',0.084893455136697493),$sum($product('X_2',0.162022423603656263),$sum($product('X_3',$uminus(0.026069359722939833)),$sum($product('X_4',$uminus(0.103610576532342291)),$sum($product('X_5',0.247462072588003845),$sum($product('X_6',0.235604458158232999),$sum($product('X_7',0.094778590268327412),$sum($product('X_8',0.317884709780666685),$uminus(0.259110365198896853)))))))))),0.0),$uminus(0.06510923211031816)),$sum($product(max($sum($product('X_0',0.157051962420222013),$sum($product('X_1',0.02119912918435074),$sum($product('X_2',$uminus(0.144567654546317315)),$sum($product('X_3',$uminus(0.120485782181390416)),$sum($product('X_4',0.245385692300038649),$sum($product('X_5',$uminus(0.12013008718360596)),$sum($product('X_6',$uminus(0.264054168644354381)),$sum($product('X_7',0.113466930567937607),$sum($product('X_8',0.018847290606381961),$uminus(0.306458405399606004)))))))))),0.0),0.08954218524327956),$sum($product(max($sum($product('X_0',0.287194094745330031),$sum($product('X_1',$uminus(0.279329006877257702)),$sum($product('X_2',$uminus(0.27381666760090273)),$sum($product('X_3',$uminus(0.241196338354026901)),$sum($product('X_4',0.166076860453970354),$sum($product('X_5',0.003947070874237735),$sum($product('X_6',$uminus(0.079391976830132827)),$sum($product('X_7',$uminus(0.311101692329606716)),$sum($product('X_8',0.028656916570530377),$uminus(0.242226407222209617)))))))))),0.0),0.072530356741432905),$sum($product(max($sum($product('X_0',0.04404093390102809),$sum($product('X_1',0.223856941183437852),$sum($product('X_2',0.030174154656356367),$sum($product('X_3',$uminus(0.093021470933494721)),$sum($product('X_4',$uminus(0.040972965799927652)),$sum($product('X_5',0.134584475865453967),$sum($product('X_6',0.312199328391165765),$sum($product('X_7',0.040627871296072593),$sum($product('X_8',$uminus(0.123070819674687693)),0.158068620935378545))))))))),0.0),0.031019648051496651),$sum($product(max($sum($product('X_0',0.309415963276349515),$sum($product('X_1',0.039481469238021816),$sum($product('X_2',0.15094441592481006),$sum($product('X_3',0.30522360340783411),$sum($product('X_4',$uminus(0.229798563734669559)),$sum($product('X_5',$uminus(0.192960605209967856)),$sum($product('X_6',$uminus(0.20370062757883689)),$sum($product('X_7',$uminus(0.047763191941385397)),$sum($product('X_8',$uminus(0.266019895781817062)),$uminus(0.3239652657122854)))))))))),0.0),0.014296021586679558),$sum($product(max($sum($product('X_0',0.291655730227005694),$sum($product('X_1',$uminus(0.211448651190053294)),$sum($product('X_2',0.262759471678295109),$sum($product('X_3',0.250069844719772838),$sum($product('X_4',$uminus(0.0381186790917451)),$sum($product('X_5',$uminus(0.146083546836047795)),$sum($product('X_6',$uminus(0.151529498387592332)),$sum($product('X_7',0.201164755659322625),$sum($product('X_8',0.146160292641425327),$uminus(0.046301663710338892)))))))))),0.0),0.121361832369365152),$sum($product(max($sum($product('X_0',$uminus(0.184467825491839488)),$sum($product('X_1',$uminus(0.268161247711679374)),$sum($product('X_2',$uminus(0.153535151736396536)),$sum($product('X_3',$uminus(0.065596192568929845)),$sum($product('X_4',0.21729520120637863),$sum($product('X_5',$uminus(0.092332864688549343)),$sum($product('X_6',0.018066462919213766),$sum($product('X_7',$uminus(0.287370290741390033)),$sum($product('X_8',$uminus(0.222457450236703963)),$uminus(0.231100948340147661)))))))))),0.0),0.065772794248384892),$sum($product(max($sum($product('X_0',0.112387308333164793),$sum($product('X_1',$uminus(0.164516529633275843)),$sum($product('X_2',0.303715756573457785),$sum($product('X_3',$uminus(0.115559064636028858)),$sum($product('X_4',$uminus(0.101279569170582118)),$sum($product('X_5',$uminus(0.312584846980395903)),$sum($product('X_6',$uminus(0.073897332022657303)),$sum($product('X_7',$uminus(0.187107831241006384)),$sum($product('X_8',0.191742606049471742),0.219833682999539703))))))))),0.0),0.104689867766233291),$sum($product(max($sum($product('X_0',0.272843083546418008),$sum($product('X_1',$uminus(0.26331667301370465)),$sum($product('X_2',0.228746460665943896),$sum($product('X_3',0.083017409074116422),$sum($product('X_4',0.2906669151723143),$sum($product('X_5',0.035447691086564703),$sum($product('X_6',0.312581653146865424),$sum($product('X_7',$uminus(0.052006990099353001)),$sum($product('X_8',$uminus(0.238709163668962665)),0.28076114529116375))))))))),0.0),0.103569185790112789),$sum($product(max($sum($product('X_0',0.074020874970563255),$sum($product('X_1',$uminus(0.022502229774748639)),$sum($product('X_2',0.183897093057601213),$sum($product('X_3',$uminus(0.287464703406070055)),$sum($product('X_4',$uminus(0.079254407166150287)),$sum($product('X_5',$uminus(0.330123738440344594)),$sum($product('X_6',0.302019322984987182),$sum($product('X_7',0.060629658317428392),$sum($product('X_8',$uminus(0.066123676240795071)),$uminus(0.168318244851325016)))))))))),0.0),$uminus(0.096451090569280251)),$sum($product(max($sum($product('X_0',0.117161478668860342),$sum($product('X_1',$uminus(0.309380508435266599)),$sum($product('X_2',0.166150746972853758),$sum($product('X_3',0.013701434090766906),$sum($product('X_4',0.141685721053067371),$sum($product('X_5',$uminus(0.028880166693844356)),$sum($product('X_6',0.260745424659842906),$sum($product('X_7',$uminus(0.158065618750375059)),$sum($product('X_8',0.095877003914591752),0.118188048960575609))))))))),0.0),$uminus(0.050297575744101902)),$sum($product(max($sum($product('X_0',$uminus(0.242158813559863934)),$sum($product('X_1',0.121440841134675681),$sum($product('X_2',0.244934559694501341),$sum($product('X_3',$uminus(0.317637615301534615)),$sum($product('X_4',$uminus(0.25005972927599035)),$sum($product('X_5',$uminus(0.215710382695643604)),$sum($product('X_6',0.124190735382829098),$sum($product('X_7',$uminus(0.059589490133065748)),$sum($product('X_8',0.251407265038740835),0.08916513259423331))))))))),0.0),$uminus(0.01178624591574956)),0.014290126991849089)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ).
%---∀ x:Real y:Real (max(x, y) = (if (x < y) y else x))
tff(formula_23,definition,
! [X: $real,Y: $real] :
( ( $less(X,Y)
=> ( max(X,Y) = Y ) )
& ( ~ $less(X,Y)
=> ( max(X,Y) = X ) ) ) ).
%------------------------------------------------------------------------------