TPTP Problem File: SWX129_1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX129_1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Neural network verification problem B_007
% 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_007_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 : 45 ( 4 avg)
% Number arithmetic : 3718 ( 26 atm;2487 fun;1203 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 : 460 ( 13 usr; 456 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.9929137836358598) ∨ ((-1.0 * Y_0) ≤ -1.00708621636414) ∨ ((1.0 * Y_1) ≤ -0.9882619152687477) ∨ ((-1.0 * Y_1) ≤ -1.0117380847312523) ∨ ((1.0 * Y_2) ≤ -0.5146207957568867) ∨ ((-1.0 * Y_2) ≤ -1.4853792042431133))
tff(formula_19,axiom,
( $lesseq($product(1.0,'Y_0'),$uminus(0.9929137836358598))
| $lesseq($product($uminus(1.0),'Y_0'),$uminus(1.00708621636414))
| $lesseq($product(1.0,'Y_1'),$uminus(0.9882619152687477))
| $lesseq($product($uminus(1.0),'Y_1'),$uminus(1.0117380847312523))
| $lesseq($product(1.0,'Y_2'),$uminus(0.5146207957568867))
| $lesseq($product($uminus(1.0),'Y_2'),$uminus(1.4853792042431133)) ) ).
%---(Y_0 = ((max(((X_0 * -0.085084204329484825) + (X_1 * 0.227277475280493524) + (X_2 * -0.146610404330747374) + (X_3 * -0.025088421047380127) + (X_4 * -0.236920078172610987) + (X_5 * 0.23556591236427632) + (X_6 * 0.045722886609951274) + (X_7 * -0.02105634790933264) + (X_8 * 0.299466624300461504) + 0.329253528971797216), 0.0) * 0.010732777043649416) + (max(((X_0 * 0.131301485190524703) + (X_1 * 0.209271326399700974) + (X_2 * -0.003838650175968794) + (X_3 * 0.216285547045041937) + (X_4 * -0.078518216784271455) + (X_5 * -0.101796191230834998) + (X_6 * -0.11810206645944557) + (X_7 * 0.073250343005372975) + (X_8 * 0.081758464201247938) + -0.139974431335130989), 0.0) * 0.167274653008469137) + (max(((X_0 * 0.151966319200479649) + (X_1 * -0.110606617906597343) + (X_2 * -0.060634341256404101) + (X_3 * 0.064220146693632352) + (X_4 * 0.022958266738014321) + (X_5 * -0.019995998724101849) + (X_6 * -0.050459445689319427) + (X_7 * 0.239386637748791598) + (X_8 * 0.193895523780232837) + -0.025201949827679204), 0.0) * -0.142184808252202699) + (max(((X_0 * 0.201918035720349331) + (X_1 * 0.071474693145737511) + (X_2 * -0.23470773195197539) + (X_3 * -0.233331659063250207) + (X_4 * 0.208583110235902314) + (X_5 * 0.291057185061493195) + (X_6 * -0.225458440742216049) + (X_7 * 0.30067966240644789) + (X_8 * -0.089917230539459242) + 0.021089287317174688), 0.0) * -0.02382037872995374) + (max(((X_0 * -0.133815944346616478) + (X_1 * -0.141304679292629271) + (X_2 * -0.219916577214829184) + (X_3 * -0.139758046639439831) + (X_4 * 0.023704997592138122) + (X_5 * 0.027489860415485401) + (X_6 * 0.28621826738765116) + (X_7 * 0.17028321810148489) + (X_8 * 0.155422226139109998) + -0.115193574595601644), 0.0) * 0.043165332199750189) + (max(((X_0 * -0.253268830840590653) + (X_1 * -0.063029704424822863) + (X_2 * 0.108342209516613941) + (X_3 * 0.011393961409695397) + (X_4 * -0.247224555255746742) + (X_5 * -0.245467779204527226) + (X_6 * 0.255234081909341326) + (X_7 * 0.147853392187311028) + (X_8 * 0.289447914966787068) + 0.203088066262591405), 0.0) * 0.012537760103520673) + (max(((X_0 * -0.119348940666866188) + (X_1 * -0.015475394094090544) + (X_2 * -0.257618085520195383) + (X_3 * 0.266883445685118181) + (X_4 * 0.154463982908279673) + (X_5 * 0.049303003478437801) + (X_6 * 0.170243650563203286) + (X_7 * 0.269376706562944379) + (X_8 * -0.046691059958949621) + 0.141036994079377198), 0.0) * 0.029226445907193227) + (max(((X_0 * 0.181914050129224181) + (X_1 * 0.069066291091121113) + (X_2 * 0.078554846238518217) + (X_3 * 0.123390095445965298) + (X_4 * -0.031434673366901533) + (X_5 * 0.120282490489638627) + (X_6 * 0.031318603965440728) + (X_7 * 0.245581722149856574) + (X_8 * -0.021362740664095992) + 0.197320938824874503), 0.0) * -0.101556012654238387) + (max(((X_0 * -0.098483582586146978) + (X_1 * 0.243394546376257848) + (X_2 * 0.115025912113307038) + (X_3 * 0.059118247029516235) + (X_4 * -0.044447188855861575) + (X_5 * -0.173647353012183814) + (X_6 * 0.176566057771695817) + (X_7 * 0.264381326549107676) + (X_8 * 0.078060224645663701) + 0.038845687539709906), 0.0) * -0.013920940990784864) + (max(((X_0 * -0.323129810216333357) + (X_1 * 0.203658385409960896) + (X_2 * 0.113291471700892099) + (X_3 * -0.100124959660652074) + (X_4 * -0.28985347600821415) + (X_5 * 0.296479167320807202) + (X_6 * 0.199063337816699659) + (X_7 * -0.06805784076294108) + (X_8 * -0.28999374577009368) + -0.064859166636634213), 0.0) * 0.079012933904652) + (max(((X_0 * -0.101138320969167639) + (X_1 * 0.320103369940945515) + (X_2 * 0.229092709080107315) + (X_3 * 0.100355428234711164) + (X_4 * 0.17256061748191559) + (X_5 * 0.172824269742782366) + (X_6 * -0.00821012582886177) + (X_7 * 0.159414582738557076) + (X_8 * -0.198533216177367772) + -0.318412682581384776), 0.0) * 0.063126247279672365) + (max(((X_0 * 0.175819166464083299) + (X_1 * -0.14776993571183028) + (X_2 * -0.068844059775948763) + (X_3 * -0.188063081708857771) + (X_4 * -0.311504716200073695) + (X_5 * 0.088351922204317035) + (X_6 * -0.16596908518028744) + (X_7 * -0.139144677747215173) + (X_8 * 0.243917224520820819) + -0.047620091562705691), 0.0) * -0.038234297711364024) + (max(((X_0 * -0.315331204850205105) + (X_1 * -0.094618536390520314) + (X_2 * -0.156319919457583195) + (X_3 * 0.314122227139165766) + (X_4 * 0.181343578932227689) + (X_5 * 0.287763417098287844) + (X_6 * 0.019804317916209957) + (X_7 * 0.102935985091808402) + (X_8 * -0.170962160039119043) + -0.19759119588505758), 0.0) * 0.039864266384938729) + (max(((X_0 * 0.076796260324881238) + (X_1 * -0.07336050052662707) + (X_2 * 0.312311337905172348) + (X_3 * -0.317577596340329005) + (X_4 * 0.302325881276476804) + (X_5 * -0.128005488866581196) + (X_6 * -0.096981057694019324) + (X_7 * -0.133248611155060148) + (X_8 * 0.226658256292756988) + 0.124205739234839296), 0.0) * 0.163985334342465067) + (max(((X_0 * 0.265775077062823717) + (X_1 * 0.247512118108101642) + (X_2 * 0.052452192142516785) + (X_3 * 0.002814471274279473) + (X_4 * 0.054493435203783414) + (X_5 * -0.277167547039640971) + (X_6 * 0.149280534429790446) + (X_7 * 0.300917351504644548) + (X_8 * 0.201867708618147346) + -0.02249745933799302), 0.0) * 0.144406036938515975) + (max(((X_0 * 0.06116423178510666) + (X_1 * 0.204715007928164938) + (X_2 * -0.099435113324590901) + (X_3 * -0.075076646106589484) + (X_4 * -0.147611930043982709) + (X_5 * 0.329771718125498159) + (X_6 * -0.077929763794931661) + (X_7 * 0.158305623398400153) + (X_8 * 0.106605366167060955) + 0.227482560218186969), 0.0) * 0.133743485380546451) + (max(((X_0 * -0.092366462711563596) + (X_1 * 0.052646937452845266) + (X_2 * 0.015413236401603803) + (X_3 * 0.113228661403501463) + (X_4 * -0.121216575464961451) + (X_5 * -0.215702653361375507) + (X_6 * 0.226017336583560879) + (X_7 * -0.220132361394591358) + (X_8 * -0.307768566023152002) + 0.320006108957572477), 0.0) * -0.066401586557737285) + (max(((X_0 * -0.226766580533465462) + (X_1 * 0.00391162568521225) + (X_2 * 0.019473623430183329) + (X_3 * 0.216386614008901634) + (X_4 * -0.078297955556637266) + (X_5 * 0.255109588258111974) + (X_6 * -0.083549070923979812) + (X_7 * -0.227547325045974136) + (X_8 * -0.243613693974603474) + -0.293731755902412184), 0.0) * -0.164130337839928003) + (max(((X_0 * 0.067140788316724598) + (X_1 * -0.03548741081174861) + (X_2 * 0.172652969653422972) + (X_3 * -0.0931690048650268) + (X_4 * -0.028500025351721081) + (X_5 * 0.14805861924911623) + (X_6 * -0.269308449436302999) + (X_7 * -0.224045703414196051) + (X_8 * -0.031612092375694345) + -0.190489098222868414), 0.0) * 0.168596695989742668) + (max(((X_0 * -0.283171155800769958) + (X_1 * -0.018460033900721984) + (X_2 * 0.218690372500649099) + (X_3 * 0.284174999537985584) + (X_4 * 0.127309836240449004) + (X_5 * 0.163578447613004718) + (X_6 * -0.19874294302317802) + (X_7 * -0.317257731536686072) + (X_8 * -0.267960016746490171) + 0.290800639964543028), 0.0) * 0.032600747798382873) + (max(((X_0 * -0.0725795111797361) + (X_1 * -0.120319623004474657) + (X_2 * -0.114421945285064997) + (X_3 * 0.215714109924082409) + (X_4 * -0.008755817146637979) + (X_5 * -0.219790524805509563) + (X_6 * -0.302111967118618541) + (X_7 * -0.222922230078116679) + (X_8 * -0.251709505974506254) + -0.326284828368465285), 0.0) * 0.122956455521180091) + (max(((X_0 * 0.223511809452060006) + (X_1 * 0.105431646849439176) + (X_2 * 0.017074992645697451) + (X_3 * -0.068702701737561434) + (X_4 * -0.042933026550501019) + (X_5 * -0.05012084091704655) + (X_6 * -0.267050073103187069) + (X_7 * -0.305230848586137749) + (X_8 * 0.169917993562293479) + 0.242389984971433103), 0.0) * 0.062501369306116467) + (max(((X_0 * 0.143380167173043749) + (X_1 * -0.261902473627182053) + (X_2 * -0.069372572421227796) + (X_3 * -0.09762913086169403) + (X_4 * -0.279467825999905162) + (X_5 * -0.074563064956958358) + (X_6 * 0.242162004287260368) + (X_7 * 0.064739396957266548) + (X_8 * -0.24585648625546358) + -0.120744054176062848), 0.0) * -0.118489976256117985) + (max(((X_0 * -0.271806868921937173) + (X_1 * 0.192786148129760748) + (X_2 * -0.265789744937258876) + (X_3 * 0.305951947524789991) + (X_4 * 0.23169263946176194) + (X_5 * -0.058046107628971055) + (X_6 * -0.260905027316403082) + (X_7 * 0.140278727566981731) + (X_8 * -0.119580601626665756) + -0.25399765408133701), 0.0) * 0.157608946257712407) + (max(((X_0 * -0.180535942580106135) + (X_1 * -0.078816567104432078) + (X_2 * 0.270339928183404965) + (X_3 * 0.167454511534455508) + (X_4 * -0.331345024402933341) + (X_5 * -0.134734984988303996) + (X_6 * 0.11646087972096425) + (X_7 * -0.288940128920388006) + (X_8 * 0.023771975478321161) + 0.119256284613703689), 0.0) * -0.16656626582306075) + (max(((X_0 * 0.229344671986353832) + (X_1 * 0.077751196189045302) + (X_2 * -0.299189374278061193) + (X_3 * -0.063015801812984884) + (X_4 * 0.328319748032158965) + (X_5 * 0.157088214412941352) + (X_6 * 0.029268535381060168) + (X_7 * 0.274656616745850568) + (X_8 * 0.144313026206903172) + -0.076488406458863623), 0.0) * -0.040581563938859755) + (max(((X_0 * -0.295229121002945238) + (X_1 * 0.250267751274626249) + (X_2 * 0.05458341403079503) + (X_3 * -0.316841801114587041) + (X_4 * -0.010146514051700473) + (X_5 * 0.028656171184171575) + (X_6 * 0.096331746773274329) + (X_7 * -0.010367995907403615) + (X_8 * 0.099029964077058219) + 0.23009073028369359), 0.0) * -0.106538241437495115) + (max(((X_0 * -0.024154254689310706) + (X_1 * -0.318461633220060603) + (X_2 * -0.099539216620869064) + (X_3 * -0.269059058694451791) + (X_4 * 0.315147523984193823) + (X_5 * 0.040530443292059626) + (X_6 * 0.076347447009154579) + (X_7 * -0.147734037206016217) + (X_8 * 0.291049624306576049) + 0.08619313628106634), 0.0) * 0.094850147204340401) + (max(((X_0 * -0.112409864464090792) + (X_1 * 0.01353162096107452) + (X_2 * -0.02548901498770223) + (X_3 * 0.032351808775658186) + (X_4 * -0.162908946127287457) + (X_5 * -0.13855301706381265) + (X_6 * -0.123810348662606678) + (X_7 * -0.212094939047360098) + (X_8 * -0.216677291236464425) + -0.095959155784354933), 0.0) * -0.035709609041463808) + (max(((X_0 * 0.175651345260155523) + (X_1 * 0.188605425088383905) + (X_2 * 0.023435288099971918) + (X_3 * 0.248480660255076702) + (X_4 * 0.273942775226820479) + (X_5 * -0.135710397401424709) + (X_6 * -0.30755508160556011) + (X_7 * 0.144725408519543242) + (X_8 * 0.011562496541478506) + 0.079719747766130833), 0.0) * -0.088201596438197694) + (max(((X_0 * 0.091009525495494847) + (X_1 * -0.292547844235659493) + (X_2 * 0.197565541562245206) + (X_3 * -0.095680712033663573) + (X_4 * 0.325005835691322853) + (X_5 * 0.196008450170439052) + (X_6 * -0.291515907551800346) + (X_7 * 0.194995070875606913) + (X_8 * -0.164718689523304068) + 0.163495981361108544), 0.0) * -0.011218478566687562) + (max(((X_0 * -0.05565613137069686) + (X_1 * 0.059211661997694842) + (X_2 * -0.209390279526032064) + (X_3 * -0.083248962597532949) + (X_4 * -0.108617811253452518) + (X_5 * -0.094488758575356713) + (X_6 * -0.284226770453594624) + (X_7 * 0.23114465798782774) + (X_8 * 0.232274809206353294) + -0.232150653009682018), 0.0) * 0.010742052005284886) + 0.11769837313980594))
tff(formula_20,axiom,
'Y_0' = $sum($product(max($sum($product('X_0',$uminus(0.085084204329484825)),$sum($product('X_1',0.227277475280493524),$sum($product('X_2',$uminus(0.146610404330747374)),$sum($product('X_3',$uminus(0.025088421047380127)),$sum($product('X_4',$uminus(0.236920078172610987)),$sum($product('X_5',0.23556591236427632),$sum($product('X_6',0.045722886609951274),$sum($product('X_7',$uminus(0.02105634790933264)),$sum($product('X_8',0.299466624300461504),0.329253528971797216))))))))),0.0),0.010732777043649416),$sum($product(max($sum($product('X_0',0.131301485190524703),$sum($product('X_1',0.209271326399700974),$sum($product('X_2',$uminus(0.003838650175968794)),$sum($product('X_3',0.216285547045041937),$sum($product('X_4',$uminus(0.078518216784271455)),$sum($product('X_5',$uminus(0.101796191230834998)),$sum($product('X_6',$uminus(0.11810206645944557)),$sum($product('X_7',0.073250343005372975),$sum($product('X_8',0.081758464201247938),$uminus(0.139974431335130989)))))))))),0.0),0.167274653008469137),$sum($product(max($sum($product('X_0',0.151966319200479649),$sum($product('X_1',$uminus(0.110606617906597343)),$sum($product('X_2',$uminus(0.060634341256404101)),$sum($product('X_3',0.064220146693632352),$sum($product('X_4',0.022958266738014321),$sum($product('X_5',$uminus(0.019995998724101849)),$sum($product('X_6',$uminus(0.050459445689319427)),$sum($product('X_7',0.239386637748791598),$sum($product('X_8',0.193895523780232837),$uminus(0.025201949827679204)))))))))),0.0),$uminus(0.142184808252202699)),$sum($product(max($sum($product('X_0',0.201918035720349331),$sum($product('X_1',0.071474693145737511),$sum($product('X_2',$uminus(0.23470773195197539)),$sum($product('X_3',$uminus(0.233331659063250207)),$sum($product('X_4',0.208583110235902314),$sum($product('X_5',0.291057185061493195),$sum($product('X_6',$uminus(0.225458440742216049)),$sum($product('X_7',0.30067966240644789),$sum($product('X_8',$uminus(0.089917230539459242)),0.021089287317174688))))))))),0.0),$uminus(0.02382037872995374)),$sum($product(max($sum($product('X_0',$uminus(0.133815944346616478)),$sum($product('X_1',$uminus(0.141304679292629271)),$sum($product('X_2',$uminus(0.219916577214829184)),$sum($product('X_3',$uminus(0.139758046639439831)),$sum($product('X_4',0.023704997592138122),$sum($product('X_5',0.027489860415485401),$sum($product('X_6',0.28621826738765116),$sum($product('X_7',0.17028321810148489),$sum($product('X_8',0.155422226139109998),$uminus(0.115193574595601644)))))))))),0.0),0.043165332199750189),$sum($product(max($sum($product('X_0',$uminus(0.253268830840590653)),$sum($product('X_1',$uminus(0.063029704424822863)),$sum($product('X_2',0.108342209516613941),$sum($product('X_3',0.011393961409695397),$sum($product('X_4',$uminus(0.247224555255746742)),$sum($product('X_5',$uminus(0.245467779204527226)),$sum($product('X_6',0.255234081909341326),$sum($product('X_7',0.147853392187311028),$sum($product('X_8',0.289447914966787068),0.203088066262591405))))))))),0.0),0.012537760103520673),$sum($product(max($sum($product('X_0',$uminus(0.119348940666866188)),$sum($product('X_1',$uminus(0.015475394094090544)),$sum($product('X_2',$uminus(0.257618085520195383)),$sum($product('X_3',0.266883445685118181),$sum($product('X_4',0.154463982908279673),$sum($product('X_5',0.049303003478437801),$sum($product('X_6',0.170243650563203286),$sum($product('X_7',0.269376706562944379),$sum($product('X_8',$uminus(0.046691059958949621)),0.141036994079377198))))))))),0.0),0.029226445907193227),$sum($product(max($sum($product('X_0',0.181914050129224181),$sum($product('X_1',0.069066291091121113),$sum($product('X_2',0.078554846238518217),$sum($product('X_3',0.123390095445965298),$sum($product('X_4',$uminus(0.031434673366901533)),$sum($product('X_5',0.120282490489638627),$sum($product('X_6',0.031318603965440728),$sum($product('X_7',0.245581722149856574),$sum($product('X_8',$uminus(0.021362740664095992)),0.197320938824874503))))))))),0.0),$uminus(0.101556012654238387)),$sum($product(max($sum($product('X_0',$uminus(0.098483582586146978)),$sum($product('X_1',0.243394546376257848),$sum($product('X_2',0.115025912113307038),$sum($product('X_3',0.059118247029516235),$sum($product('X_4',$uminus(0.044447188855861575)),$sum($product('X_5',$uminus(0.173647353012183814)),$sum($product('X_6',0.176566057771695817),$sum($product('X_7',0.264381326549107676),$sum($product('X_8',0.078060224645663701),0.038845687539709906))))))))),0.0),$uminus(0.013920940990784864)),$sum($product(max($sum($product('X_0',$uminus(0.323129810216333357)),$sum($product('X_1',0.203658385409960896),$sum($product('X_2',0.113291471700892099),$sum($product('X_3',$uminus(0.100124959660652074)),$sum($product('X_4',$uminus(0.28985347600821415)),$sum($product('X_5',0.296479167320807202),$sum($product('X_6',0.199063337816699659),$sum($product('X_7',$uminus(0.06805784076294108)),$sum($product('X_8',$uminus(0.28999374577009368)),$uminus(0.064859166636634213)))))))))),0.0),0.079012933904652),$sum($product(max($sum($product('X_0',$uminus(0.101138320969167639)),$sum($product('X_1',0.320103369940945515),$sum($product('X_2',0.229092709080107315),$sum($product('X_3',0.100355428234711164),$sum($product('X_4',0.17256061748191559),$sum($product('X_5',0.172824269742782366),$sum($product('X_6',$uminus(0.00821012582886177)),$sum($product('X_7',0.159414582738557076),$sum($product('X_8',$uminus(0.198533216177367772)),$uminus(0.318412682581384776)))))))))),0.0),0.063126247279672365),$sum($product(max($sum($product('X_0',0.175819166464083299),$sum($product('X_1',$uminus(0.14776993571183028)),$sum($product('X_2',$uminus(0.068844059775948763)),$sum($product('X_3',$uminus(0.188063081708857771)),$sum($product('X_4',$uminus(0.311504716200073695)),$sum($product('X_5',0.088351922204317035),$sum($product('X_6',$uminus(0.16596908518028744)),$sum($product('X_7',$uminus(0.139144677747215173)),$sum($product('X_8',0.243917224520820819),$uminus(0.047620091562705691)))))))))),0.0),$uminus(0.038234297711364024)),$sum($product(max($sum($product('X_0',$uminus(0.315331204850205105)),$sum($product('X_1',$uminus(0.094618536390520314)),$sum($product('X_2',$uminus(0.156319919457583195)),$sum($product('X_3',0.314122227139165766),$sum($product('X_4',0.181343578932227689),$sum($product('X_5',0.287763417098287844),$sum($product('X_6',0.019804317916209957),$sum($product('X_7',0.102935985091808402),$sum($product('X_8',$uminus(0.170962160039119043)),$uminus(0.19759119588505758)))))))))),0.0),0.039864266384938729),$sum($product(max($sum($product('X_0',0.076796260324881238),$sum($product('X_1',$uminus(0.07336050052662707)),$sum($product('X_2',0.312311337905172348),$sum($product('X_3',$uminus(0.317577596340329005)),$sum($product('X_4',0.302325881276476804),$sum($product('X_5',$uminus(0.128005488866581196)),$sum($product('X_6',$uminus(0.096981057694019324)),$sum($product('X_7',$uminus(0.133248611155060148)),$sum($product('X_8',0.226658256292756988),0.124205739234839296))))))))),0.0),0.163985334342465067),$sum($product(max($sum($product('X_0',0.265775077062823717),$sum($product('X_1',0.247512118108101642),$sum($product('X_2',0.052452192142516785),$sum($product('X_3',0.002814471274279473),$sum($product('X_4',0.054493435203783414),$sum($product('X_5',$uminus(0.277167547039640971)),$sum($product('X_6',0.149280534429790446),$sum($product('X_7',0.300917351504644548),$sum($product('X_8',0.201867708618147346),$uminus(0.02249745933799302)))))))))),0.0),0.144406036938515975),$sum($product(max($sum($product('X_0',0.06116423178510666),$sum($product('X_1',0.204715007928164938),$sum($product('X_2',$uminus(0.099435113324590901)),$sum($product('X_3',$uminus(0.075076646106589484)),$sum($product('X_4',$uminus(0.147611930043982709)),$sum($product('X_5',0.329771718125498159),$sum($product('X_6',$uminus(0.077929763794931661)),$sum($product('X_7',0.158305623398400153),$sum($product('X_8',0.106605366167060955),0.227482560218186969))))))))),0.0),0.133743485380546451),$sum($product(max($sum($product('X_0',$uminus(0.092366462711563596)),$sum($product('X_1',0.052646937452845266),$sum($product('X_2',0.015413236401603803),$sum($product('X_3',0.113228661403501463),$sum($product('X_4',$uminus(0.121216575464961451)),$sum($product('X_5',$uminus(0.215702653361375507)),$sum($product('X_6',0.226017336583560879),$sum($product('X_7',$uminus(0.220132361394591358)),$sum($product('X_8',$uminus(0.307768566023152002)),0.320006108957572477))))))))),0.0),$uminus(0.066401586557737285)),$sum($product(max($sum($product('X_0',$uminus(0.226766580533465462)),$sum($product('X_1',0.00391162568521225),$sum($product('X_2',0.019473623430183329),$sum($product('X_3',0.216386614008901634),$sum($product('X_4',$uminus(0.078297955556637266)),$sum($product('X_5',0.255109588258111974),$sum($product('X_6',$uminus(0.083549070923979812)),$sum($product('X_7',$uminus(0.227547325045974136)),$sum($product('X_8',$uminus(0.243613693974603474)),$uminus(0.293731755902412184)))))))))),0.0),$uminus(0.164130337839928003)),$sum($product(max($sum($product('X_0',0.067140788316724598),$sum($product('X_1',$uminus(0.03548741081174861)),$sum($product('X_2',0.172652969653422972),$sum($product('X_3',$uminus(0.0931690048650268)),$sum($product('X_4',$uminus(0.028500025351721081)),$sum($product('X_5',0.14805861924911623),$sum($product('X_6',$uminus(0.269308449436302999)),$sum($product('X_7',$uminus(0.224045703414196051)),$sum($product('X_8',$uminus(0.031612092375694345)),$uminus(0.190489098222868414)))))))))),0.0),0.168596695989742668),$sum($product(max($sum($product('X_0',$uminus(0.283171155800769958)),$sum($product('X_1',$uminus(0.018460033900721984)),$sum($product('X_2',0.218690372500649099),$sum($product('X_3',0.284174999537985584),$sum($product('X_4',0.127309836240449004),$sum($product('X_5',0.163578447613004718),$sum($product('X_6',$uminus(0.19874294302317802)),$sum($product('X_7',$uminus(0.317257731536686072)),$sum($product('X_8',$uminus(0.267960016746490171)),0.290800639964543028))))))))),0.0),0.032600747798382873),$sum($product(max($sum($product('X_0',$uminus(0.0725795111797361)),$sum($product('X_1',$uminus(0.120319623004474657)),$sum($product('X_2',$uminus(0.114421945285064997)),$sum($product('X_3',0.215714109924082409),$sum($product('X_4',$uminus(0.008755817146637979)),$sum($product('X_5',$uminus(0.219790524805509563)),$sum($product('X_6',$uminus(0.302111967118618541)),$sum($product('X_7',$uminus(0.222922230078116679)),$sum($product('X_8',$uminus(0.251709505974506254)),$uminus(0.326284828368465285)))))))))),0.0),0.122956455521180091),$sum($product(max($sum($product('X_0',0.223511809452060006),$sum($product('X_1',0.105431646849439176),$sum($product('X_2',0.017074992645697451),$sum($product('X_3',$uminus(0.068702701737561434)),$sum($product('X_4',$uminus(0.042933026550501019)),$sum($product('X_5',$uminus(0.05012084091704655)),$sum($product('X_6',$uminus(0.267050073103187069)),$sum($product('X_7',$uminus(0.305230848586137749)),$sum($product('X_8',0.169917993562293479),0.242389984971433103))))))))),0.0),0.062501369306116467),$sum($product(max($sum($product('X_0',0.143380167173043749),$sum($product('X_1',$uminus(0.261902473627182053)),$sum($product('X_2',$uminus(0.069372572421227796)),$sum($product('X_3',$uminus(0.09762913086169403)),$sum($product('X_4',$uminus(0.279467825999905162)),$sum($product('X_5',$uminus(0.074563064956958358)),$sum($product('X_6',0.242162004287260368),$sum($product('X_7',0.064739396957266548),$sum($product('X_8',$uminus(0.24585648625546358)),$uminus(0.120744054176062848)))))))))),0.0),$uminus(0.118489976256117985)),$sum($product(max($sum($product('X_0',$uminus(0.271806868921937173)),$sum($product('X_1',0.192786148129760748),$sum($product('X_2',$uminus(0.265789744937258876)),$sum($product('X_3',0.305951947524789991),$sum($product('X_4',0.23169263946176194),$sum($product('X_5',$uminus(0.058046107628971055)),$sum($product('X_6',$uminus(0.260905027316403082)),$sum($product('X_7',0.140278727566981731),$sum($product('X_8',$uminus(0.119580601626665756)),$uminus(0.25399765408133701)))))))))),0.0),0.157608946257712407),$sum($product(max($sum($product('X_0',$uminus(0.180535942580106135)),$sum($product('X_1',$uminus(0.078816567104432078)),$sum($product('X_2',0.270339928183404965),$sum($product('X_3',0.167454511534455508),$sum($product('X_4',$uminus(0.331345024402933341)),$sum($product('X_5',$uminus(0.134734984988303996)),$sum($product('X_6',0.11646087972096425),$sum($product('X_7',$uminus(0.288940128920388006)),$sum($product('X_8',0.023771975478321161),0.119256284613703689))))))))),0.0),$uminus(0.16656626582306075)),$sum($product(max($sum($product('X_0',0.229344671986353832),$sum($product('X_1',0.077751196189045302),$sum($product('X_2',$uminus(0.299189374278061193)),$sum($product('X_3',$uminus(0.063015801812984884)),$sum($product('X_4',0.328319748032158965),$sum($product('X_5',0.157088214412941352),$sum($product('X_6',0.029268535381060168),$sum($product('X_7',0.274656616745850568),$sum($product('X_8',0.144313026206903172),$uminus(0.076488406458863623)))))))))),0.0),$uminus(0.040581563938859755)),$sum($product(max($sum($product('X_0',$uminus(0.295229121002945238)),$sum($product('X_1',0.250267751274626249),$sum($product('X_2',0.05458341403079503),$sum($product('X_3',$uminus(0.316841801114587041)),$sum($product('X_4',$uminus(0.010146514051700473)),$sum($product('X_5',0.028656171184171575),$sum($product('X_6',0.096331746773274329),$sum($product('X_7',$uminus(0.010367995907403615)),$sum($product('X_8',0.099029964077058219),0.23009073028369359))))))))),0.0),$uminus(0.106538241437495115)),$sum($product(max($sum($product('X_0',$uminus(0.024154254689310706)),$sum($product('X_1',$uminus(0.318461633220060603)),$sum($product('X_2',$uminus(0.099539216620869064)),$sum($product('X_3',$uminus(0.269059058694451791)),$sum($product('X_4',0.315147523984193823),$sum($product('X_5',0.040530443292059626),$sum($product('X_6',0.076347447009154579),$sum($product('X_7',$uminus(0.147734037206016217)),$sum($product('X_8',0.291049624306576049),0.08619313628106634))))))))),0.0),0.094850147204340401),$sum($product(max($sum($product('X_0',$uminus(0.112409864464090792)),$sum($product('X_1',0.01353162096107452),$sum($product('X_2',$uminus(0.02548901498770223)),$sum($product('X_3',0.032351808775658186),$sum($product('X_4',$uminus(0.162908946127287457)),$sum($product('X_5',$uminus(0.13855301706381265)),$sum($product('X_6',$uminus(0.123810348662606678)),$sum($product('X_7',$uminus(0.212094939047360098)),$sum($product('X_8',$uminus(0.216677291236464425)),$uminus(0.095959155784354933)))))))))),0.0),$uminus(0.035709609041463808)),$sum($product(max($sum($product('X_0',0.175651345260155523),$sum($product('X_1',0.188605425088383905),$sum($product('X_2',0.023435288099971918),$sum($product('X_3',0.248480660255076702),$sum($product('X_4',0.273942775226820479),$sum($product('X_5',$uminus(0.135710397401424709)),$sum($product('X_6',$uminus(0.30755508160556011)),$sum($product('X_7',0.144725408519543242),$sum($product('X_8',0.011562496541478506),0.079719747766130833))))))))),0.0),$uminus(0.088201596438197694)),$sum($product(max($sum($product('X_0',0.091009525495494847),$sum($product('X_1',$uminus(0.292547844235659493)),$sum($product('X_2',0.197565541562245206),$sum($product('X_3',$uminus(0.095680712033663573)),$sum($product('X_4',0.325005835691322853),$sum($product('X_5',0.196008450170439052),$sum($product('X_6',$uminus(0.291515907551800346)),$sum($product('X_7',0.194995070875606913),$sum($product('X_8',$uminus(0.164718689523304068)),0.163495981361108544))))))))),0.0),$uminus(0.011218478566687562)),$sum($product(max($sum($product('X_0',$uminus(0.05565613137069686)),$sum($product('X_1',0.059211661997694842),$sum($product('X_2',$uminus(0.209390279526032064)),$sum($product('X_3',$uminus(0.083248962597532949)),$sum($product('X_4',$uminus(0.108617811253452518)),$sum($product('X_5',$uminus(0.094488758575356713)),$sum($product('X_6',$uminus(0.284226770453594624)),$sum($product('X_7',0.23114465798782774),$sum($product('X_8',0.232274809206353294),$uminus(0.232150653009682018)))))))))),0.0),0.010742052005284886),0.11769837313980594)))))))))))))))))))))))))))))))) ).
%---(Y_1 = ((max(((X_0 * -0.085084204329484825) + (X_1 * 0.227277475280493524) + (X_2 * -0.146610404330747374) + (X_3 * -0.025088421047380127) + (X_4 * -0.236920078172610987) + (X_5 * 0.23556591236427632) + (X_6 * 0.045722886609951274) + (X_7 * -0.02105634790933264) + (X_8 * 0.299466624300461504) + 0.329253528971797216), 0.0) * -0.094110066454354796) + (max(((X_0 * 0.131301485190524703) + (X_1 * 0.209271326399700974) + (X_2 * -0.003838650175968794) + (X_3 * 0.216285547045041937) + (X_4 * -0.078518216784271455) + (X_5 * -0.101796191230834998) + (X_6 * -0.11810206645944557) + (X_7 * 0.073250343005372975) + (X_8 * 0.081758464201247938) + -0.139974431335130989), 0.0) * -0.01947810299144398) + (max(((X_0 * 0.151966319200479649) + (X_1 * -0.110606617906597343) + (X_2 * -0.060634341256404101) + (X_3 * 0.064220146693632352) + (X_4 * 0.022958266738014321) + (X_5 * -0.019995998724101849) + (X_6 * -0.050459445689319427) + (X_7 * 0.239386637748791598) + (X_8 * 0.193895523780232837) + -0.025201949827679204), 0.0) * -0.156513262655119695) + (max(((X_0 * 0.201918035720349331) + (X_1 * 0.071474693145737511) + (X_2 * -0.23470773195197539) + (X_3 * -0.233331659063250207) + (X_4 * 0.208583110235902314) + (X_5 * 0.291057185061493195) + (X_6 * -0.225458440742216049) + (X_7 * 0.30067966240644789) + (X_8 * -0.089917230539459242) + 0.021089287317174688), 0.0) * 0.047701233745661459) + (max(((X_0 * -0.133815944346616478) + (X_1 * -0.141304679292629271) + (X_2 * -0.219916577214829184) + (X_3 * -0.139758046639439831) + (X_4 * 0.023704997592138122) + (X_5 * 0.027489860415485401) + (X_6 * 0.28621826738765116) + (X_7 * 0.17028321810148489) + (X_8 * 0.155422226139109998) + -0.115193574595601644), 0.0) * 0.032595205404072375) + (max(((X_0 * -0.253268830840590653) + (X_1 * -0.063029704424822863) + (X_2 * 0.108342209516613941) + (X_3 * 0.011393961409695397) + (X_4 * -0.247224555255746742) + (X_5 * -0.245467779204527226) + (X_6 * 0.255234081909341326) + (X_7 * 0.147853392187311028) + (X_8 * 0.289447914966787068) + 0.203088066262591405), 0.0) * 0.062041920553589897) + (max(((X_0 * -0.119348940666866188) + (X_1 * -0.015475394094090544) + (X_2 * -0.257618085520195383) + (X_3 * 0.266883445685118181) + (X_4 * 0.154463982908279673) + (X_5 * 0.049303003478437801) + (X_6 * 0.170243650563203286) + (X_7 * 0.269376706562944379) + (X_8 * -0.046691059958949621) + 0.141036994079377198), 0.0) * -0.076308797292992378) + (max(((X_0 * 0.181914050129224181) + (X_1 * 0.069066291091121113) + (X_2 * 0.078554846238518217) + (X_3 * 0.123390095445965298) + (X_4 * -0.031434673366901533) + (X_5 * 0.120282490489638627) + (X_6 * 0.031318603965440728) + (X_7 * 0.245581722149856574) + (X_8 * -0.021362740664095992) + 0.197320938824874503), 0.0) * -0.041180941315936609) + (max(((X_0 * -0.098483582586146978) + (X_1 * 0.243394546376257848) + (X_2 * 0.115025912113307038) + (X_3 * 0.059118247029516235) + (X_4 * -0.044447188855861575) + (X_5 * -0.173647353012183814) + (X_6 * 0.176566057771695817) + (X_7 * 0.264381326549107676) + (X_8 * 0.078060224645663701) + 0.038845687539709906), 0.0) * 0.082016785298440781) + (max(((X_0 * -0.323129810216333357) + (X_1 * 0.203658385409960896) + (X_2 * 0.113291471700892099) + (X_3 * -0.100124959660652074) + (X_4 * -0.28985347600821415) + (X_5 * 0.296479167320807202) + (X_6 * 0.199063337816699659) + (X_7 * -0.06805784076294108) + (X_8 * -0.28999374577009368) + -0.064859166636634213), 0.0) * -0.167978421384639531) + (max(((X_0 * -0.101138320969167639) + (X_1 * 0.320103369940945515) + (X_2 * 0.229092709080107315) + (X_3 * 0.100355428234711164) + (X_4 * 0.17256061748191559) + (X_5 * 0.172824269742782366) + (X_6 * -0.00821012582886177) + (X_7 * 0.159414582738557076) + (X_8 * -0.198533216177367772) + -0.318412682581384776), 0.0) * 0.137274148471937169) + (max(((X_0 * 0.175819166464083299) + (X_1 * -0.14776993571183028) + (X_2 * -0.068844059775948763) + (X_3 * -0.188063081708857771) + (X_4 * -0.311504716200073695) + (X_5 * 0.088351922204317035) + (X_6 * -0.16596908518028744) + (X_7 * -0.139144677747215173) + (X_8 * 0.243917224520820819) + -0.047620091562705691), 0.0) * 0.103233629505499164) + (max(((X_0 * -0.315331204850205105) + (X_1 * -0.094618536390520314) + (X_2 * -0.156319919457583195) + (X_3 * 0.314122227139165766) + (X_4 * 0.181343578932227689) + (X_5 * 0.287763417098287844) + (X_6 * 0.019804317916209957) + (X_7 * 0.102935985091808402) + (X_8 * -0.170962160039119043) + -0.19759119588505758), 0.0) * 0.063074710402062195) + (max(((X_0 * 0.076796260324881238) + (X_1 * -0.07336050052662707) + (X_2 * 0.312311337905172348) + (X_3 * -0.317577596340329005) + (X_4 * 0.302325881276476804) + (X_5 * -0.128005488866581196) + (X_6 * -0.096981057694019324) + (X_7 * -0.133248611155060148) + (X_8 * 0.226658256292756988) + 0.124205739234839296), 0.0) * -0.022518788252598232) + (max(((X_0 * 0.265775077062823717) + (X_1 * 0.247512118108101642) + (X_2 * 0.052452192142516785) + (X_3 * 0.002814471274279473) + (X_4 * 0.054493435203783414) + (X_5 * -0.277167547039640971) + (X_6 * 0.149280534429790446) + (X_7 * 0.300917351504644548) + (X_8 * 0.201867708618147346) + -0.02249745933799302), 0.0) * 0.136425962361040792) + (max(((X_0 * 0.06116423178510666) + (X_1 * 0.204715007928164938) + (X_2 * -0.099435113324590901) + (X_3 * -0.075076646106589484) + (X_4 * -0.147611930043982709) + (X_5 * 0.329771718125498159) + (X_6 * -0.077929763794931661) + (X_7 * 0.158305623398400153) + (X_8 * 0.106605366167060955) + 0.227482560218186969), 0.0) * 0.056848109871719316) + (max(((X_0 * -0.092366462711563596) + (X_1 * 0.052646937452845266) + (X_2 * 0.015413236401603803) + (X_3 * 0.113228661403501463) + (X_4 * -0.121216575464961451) + (X_5 * -0.215702653361375507) + (X_6 * 0.226017336583560879) + (X_7 * -0.220132361394591358) + (X_8 * -0.307768566023152002) + 0.320006108957572477), 0.0) * -0.151135334635830232) + (max(((X_0 * -0.226766580533465462) + (X_1 * 0.00391162568521225) + (X_2 * 0.019473623430183329) + (X_3 * 0.216386614008901634) + (X_4 * -0.078297955556637266) + (X_5 * 0.255109588258111974) + (X_6 * -0.083549070923979812) + (X_7 * -0.227547325045974136) + (X_8 * -0.243613693974603474) + -0.293731755902412184), 0.0) * 0.064636879471871189) + (max(((X_0 * 0.067140788316724598) + (X_1 * -0.03548741081174861) + (X_2 * 0.172652969653422972) + (X_3 * -0.0931690048650268) + (X_4 * -0.028500025351721081) + (X_5 * 0.14805861924911623) + (X_6 * -0.269308449436302999) + (X_7 * -0.224045703414196051) + (X_8 * -0.031612092375694345) + -0.190489098222868414), 0.0) * 0.008393055112702774) + (max(((X_0 * -0.283171155800769958) + (X_1 * -0.018460033900721984) + (X_2 * 0.218690372500649099) + (X_3 * 0.284174999537985584) + (X_4 * 0.127309836240449004) + (X_5 * 0.163578447613004718) + (X_6 * -0.19874294302317802) + (X_7 * -0.317257731536686072) + (X_8 * -0.267960016746490171) + 0.290800639964543028), 0.0) * -0.086590064435252648) + (max(((X_0 * -0.0725795111797361) + (X_1 * -0.120319623004474657) + (X_2 * -0.114421945285064997) + (X_3 * 0.215714109924082409) + (X_4 * -0.008755817146637979) + (X_5 * -0.219790524805509563) + (X_6 * -0.302111967118618541) + (X_7 * -0.222922230078116679) + (X_8 * -0.251709505974506254) + -0.326284828368465285), 0.0) * 0.027061152757942769) + (max(((X_0 * 0.223511809452060006) + (X_1 * 0.105431646849439176) + (X_2 * 0.017074992645697451) + (X_3 * -0.068702701737561434) + (X_4 * -0.042933026550501019) + (X_5 * -0.05012084091704655) + (X_6 * -0.267050073103187069) + (X_7 * -0.305230848586137749) + (X_8 * 0.169917993562293479) + 0.242389984971433103), 0.0) * -0.116050913247573606) + (max(((X_0 * 0.143380167173043749) + (X_1 * -0.261902473627182053) + (X_2 * -0.069372572421227796) + (X_3 * -0.09762913086169403) + (X_4 * -0.279467825999905162) + (X_5 * -0.074563064956958358) + (X_6 * 0.242162004287260368) + (X_7 * 0.064739396957266548) + (X_8 * -0.24585648625546358) + -0.120744054176062848), 0.0) * 0.120861687905538667) + (max(((X_0 * -0.271806868921937173) + (X_1 * 0.192786148129760748) + (X_2 * -0.265789744937258876) + (X_3 * 0.305951947524789991) + (X_4 * 0.23169263946176194) + (X_5 * -0.058046107628971055) + (X_6 * -0.260905027316403082) + (X_7 * 0.140278727566981731) + (X_8 * -0.119580601626665756) + -0.25399765408133701), 0.0) * -0.141158103785410327) + (max(((X_0 * -0.180535942580106135) + (X_1 * -0.078816567104432078) + (X_2 * 0.270339928183404965) + (X_3 * 0.167454511534455508) + (X_4 * -0.331345024402933341) + (X_5 * -0.134734984988303996) + (X_6 * 0.11646087972096425) + (X_7 * -0.288940128920388006) + (X_8 * 0.023771975478321161) + 0.119256284613703689), 0.0) * 0.004501265651469327) + (max(((X_0 * 0.229344671986353832) + (X_1 * 0.077751196189045302) + (X_2 * -0.299189374278061193) + (X_3 * -0.063015801812984884) + (X_4 * 0.328319748032158965) + (X_5 * 0.157088214412941352) + (X_6 * 0.029268535381060168) + (X_7 * 0.274656616745850568) + (X_8 * 0.144313026206903172) + -0.076488406458863623), 0.0) * -0.148575278274818645) + (max(((X_0 * -0.295229121002945238) + (X_1 * 0.250267751274626249) + (X_2 * 0.05458341403079503) + (X_3 * -0.316841801114587041) + (X_4 * -0.010146514051700473) + (X_5 * 0.028656171184171575) + (X_6 * 0.096331746773274329) + (X_7 * -0.010367995907403615) + (X_8 * 0.099029964077058219) + 0.23009073028369359), 0.0) * 0.107636773564289218) + (max(((X_0 * -0.024154254689310706) + (X_1 * -0.318461633220060603) + (X_2 * -0.099539216620869064) + (X_3 * -0.269059058694451791) + (X_4 * 0.315147523984193823) + (X_5 * 0.040530443292059626) + (X_6 * 0.076347447009154579) + (X_7 * -0.147734037206016217) + (X_8 * 0.291049624306576049) + 0.08619313628106634), 0.0) * 0.173317570857946995) + (max(((X_0 * -0.112409864464090792) + (X_1 * 0.01353162096107452) + (X_2 * -0.02548901498770223) + (X_3 * 0.032351808775658186) + (X_4 * -0.162908946127287457) + (X_5 * -0.13855301706381265) + (X_6 * -0.123810348662606678) + (X_7 * -0.212094939047360098) + (X_8 * -0.216677291236464425) + -0.095959155784354933), 0.0) * -0.105501284321076805) + (max(((X_0 * 0.175651345260155523) + (X_1 * 0.188605425088383905) + (X_2 * 0.023435288099971918) + (X_3 * 0.248480660255076702) + (X_4 * 0.273942775226820479) + (X_5 * -0.135710397401424709) + (X_6 * -0.30755508160556011) + (X_7 * 0.144725408519543242) + (X_8 * 0.011562496541478506) + 0.079719747766130833), 0.0) * -0.07057415354783815) + (max(((X_0 * 0.091009525495494847) + (X_1 * -0.292547844235659493) + (X_2 * 0.197565541562245206) + (X_3 * -0.095680712033663573) + (X_4 * 0.325005835691322853) + (X_5 * 0.196008450170439052) + (X_6 * -0.291515907551800346) + (X_7 * 0.194995070875606913) + (X_8 * -0.164718689523304068) + 0.163495981361108544), 0.0) * 0.114115570696125684) + (max(((X_0 * -0.05565613137069686) + (X_1 * 0.059211661997694842) + (X_2 * -0.209390279526032064) + (X_3 * -0.083248962597532949) + (X_4 * -0.108617811253452518) + (X_5 * -0.094488758575356713) + (X_6 * -0.284226770453594624) + (X_7 * 0.23114465798782774) + (X_8 * 0.232274809206353294) + -0.232150653009682018), 0.0) * 0.059991453404205669) + 0.002318902408805029))
tff(formula_21,axiom,
'Y_1' = $sum($product(max($sum($product('X_0',$uminus(0.085084204329484825)),$sum($product('X_1',0.227277475280493524),$sum($product('X_2',$uminus(0.146610404330747374)),$sum($product('X_3',$uminus(0.025088421047380127)),$sum($product('X_4',$uminus(0.236920078172610987)),$sum($product('X_5',0.23556591236427632),$sum($product('X_6',0.045722886609951274),$sum($product('X_7',$uminus(0.02105634790933264)),$sum($product('X_8',0.299466624300461504),0.329253528971797216))))))))),0.0),$uminus(0.094110066454354796)),$sum($product(max($sum($product('X_0',0.131301485190524703),$sum($product('X_1',0.209271326399700974),$sum($product('X_2',$uminus(0.003838650175968794)),$sum($product('X_3',0.216285547045041937),$sum($product('X_4',$uminus(0.078518216784271455)),$sum($product('X_5',$uminus(0.101796191230834998)),$sum($product('X_6',$uminus(0.11810206645944557)),$sum($product('X_7',0.073250343005372975),$sum($product('X_8',0.081758464201247938),$uminus(0.139974431335130989)))))))))),0.0),$uminus(0.01947810299144398)),$sum($product(max($sum($product('X_0',0.151966319200479649),$sum($product('X_1',$uminus(0.110606617906597343)),$sum($product('X_2',$uminus(0.060634341256404101)),$sum($product('X_3',0.064220146693632352),$sum($product('X_4',0.022958266738014321),$sum($product('X_5',$uminus(0.019995998724101849)),$sum($product('X_6',$uminus(0.050459445689319427)),$sum($product('X_7',0.239386637748791598),$sum($product('X_8',0.193895523780232837),$uminus(0.025201949827679204)))))))))),0.0),$uminus(0.156513262655119695)),$sum($product(max($sum($product('X_0',0.201918035720349331),$sum($product('X_1',0.071474693145737511),$sum($product('X_2',$uminus(0.23470773195197539)),$sum($product('X_3',$uminus(0.233331659063250207)),$sum($product('X_4',0.208583110235902314),$sum($product('X_5',0.291057185061493195),$sum($product('X_6',$uminus(0.225458440742216049)),$sum($product('X_7',0.30067966240644789),$sum($product('X_8',$uminus(0.089917230539459242)),0.021089287317174688))))))))),0.0),0.047701233745661459),$sum($product(max($sum($product('X_0',$uminus(0.133815944346616478)),$sum($product('X_1',$uminus(0.141304679292629271)),$sum($product('X_2',$uminus(0.219916577214829184)),$sum($product('X_3',$uminus(0.139758046639439831)),$sum($product('X_4',0.023704997592138122),$sum($product('X_5',0.027489860415485401),$sum($product('X_6',0.28621826738765116),$sum($product('X_7',0.17028321810148489),$sum($product('X_8',0.155422226139109998),$uminus(0.115193574595601644)))))))))),0.0),0.032595205404072375),$sum($product(max($sum($product('X_0',$uminus(0.253268830840590653)),$sum($product('X_1',$uminus(0.063029704424822863)),$sum($product('X_2',0.108342209516613941),$sum($product('X_3',0.011393961409695397),$sum($product('X_4',$uminus(0.247224555255746742)),$sum($product('X_5',$uminus(0.245467779204527226)),$sum($product('X_6',0.255234081909341326),$sum($product('X_7',0.147853392187311028),$sum($product('X_8',0.289447914966787068),0.203088066262591405))))))))),0.0),0.062041920553589897),$sum($product(max($sum($product('X_0',$uminus(0.119348940666866188)),$sum($product('X_1',$uminus(0.015475394094090544)),$sum($product('X_2',$uminus(0.257618085520195383)),$sum($product('X_3',0.266883445685118181),$sum($product('X_4',0.154463982908279673),$sum($product('X_5',0.049303003478437801),$sum($product('X_6',0.170243650563203286),$sum($product('X_7',0.269376706562944379),$sum($product('X_8',$uminus(0.046691059958949621)),0.141036994079377198))))))))),0.0),$uminus(0.076308797292992378)),$sum($product(max($sum($product('X_0',0.181914050129224181),$sum($product('X_1',0.069066291091121113),$sum($product('X_2',0.078554846238518217),$sum($product('X_3',0.123390095445965298),$sum($product('X_4',$uminus(0.031434673366901533)),$sum($product('X_5',0.120282490489638627),$sum($product('X_6',0.031318603965440728),$sum($product('X_7',0.245581722149856574),$sum($product('X_8',$uminus(0.021362740664095992)),0.197320938824874503))))))))),0.0),$uminus(0.041180941315936609)),$sum($product(max($sum($product('X_0',$uminus(0.098483582586146978)),$sum($product('X_1',0.243394546376257848),$sum($product('X_2',0.115025912113307038),$sum($product('X_3',0.059118247029516235),$sum($product('X_4',$uminus(0.044447188855861575)),$sum($product('X_5',$uminus(0.173647353012183814)),$sum($product('X_6',0.176566057771695817),$sum($product('X_7',0.264381326549107676),$sum($product('X_8',0.078060224645663701),0.038845687539709906))))))))),0.0),0.082016785298440781),$sum($product(max($sum($product('X_0',$uminus(0.323129810216333357)),$sum($product('X_1',0.203658385409960896),$sum($product('X_2',0.113291471700892099),$sum($product('X_3',$uminus(0.100124959660652074)),$sum($product('X_4',$uminus(0.28985347600821415)),$sum($product('X_5',0.296479167320807202),$sum($product('X_6',0.199063337816699659),$sum($product('X_7',$uminus(0.06805784076294108)),$sum($product('X_8',$uminus(0.28999374577009368)),$uminus(0.064859166636634213)))))))))),0.0),$uminus(0.167978421384639531)),$sum($product(max($sum($product('X_0',$uminus(0.101138320969167639)),$sum($product('X_1',0.320103369940945515),$sum($product('X_2',0.229092709080107315),$sum($product('X_3',0.100355428234711164),$sum($product('X_4',0.17256061748191559),$sum($product('X_5',0.172824269742782366),$sum($product('X_6',$uminus(0.00821012582886177)),$sum($product('X_7',0.159414582738557076),$sum($product('X_8',$uminus(0.198533216177367772)),$uminus(0.318412682581384776)))))))))),0.0),0.137274148471937169),$sum($product(max($sum($product('X_0',0.175819166464083299),$sum($product('X_1',$uminus(0.14776993571183028)),$sum($product('X_2',$uminus(0.068844059775948763)),$sum($product('X_3',$uminus(0.188063081708857771)),$sum($product('X_4',$uminus(0.311504716200073695)),$sum($product('X_5',0.088351922204317035),$sum($product('X_6',$uminus(0.16596908518028744)),$sum($product('X_7',$uminus(0.139144677747215173)),$sum($product('X_8',0.243917224520820819),$uminus(0.047620091562705691)))))))))),0.0),0.103233629505499164),$sum($product(max($sum($product('X_0',$uminus(0.315331204850205105)),$sum($product('X_1',$uminus(0.094618536390520314)),$sum($product('X_2',$uminus(0.156319919457583195)),$sum($product('X_3',0.314122227139165766),$sum($product('X_4',0.181343578932227689),$sum($product('X_5',0.287763417098287844),$sum($product('X_6',0.019804317916209957),$sum($product('X_7',0.102935985091808402),$sum($product('X_8',$uminus(0.170962160039119043)),$uminus(0.19759119588505758)))))))))),0.0),0.063074710402062195),$sum($product(max($sum($product('X_0',0.076796260324881238),$sum($product('X_1',$uminus(0.07336050052662707)),$sum($product('X_2',0.312311337905172348),$sum($product('X_3',$uminus(0.317577596340329005)),$sum($product('X_4',0.302325881276476804),$sum($product('X_5',$uminus(0.128005488866581196)),$sum($product('X_6',$uminus(0.096981057694019324)),$sum($product('X_7',$uminus(0.133248611155060148)),$sum($product('X_8',0.226658256292756988),0.124205739234839296))))))))),0.0),$uminus(0.022518788252598232)),$sum($product(max($sum($product('X_0',0.265775077062823717),$sum($product('X_1',0.247512118108101642),$sum($product('X_2',0.052452192142516785),$sum($product('X_3',0.002814471274279473),$sum($product('X_4',0.054493435203783414),$sum($product('X_5',$uminus(0.277167547039640971)),$sum($product('X_6',0.149280534429790446),$sum($product('X_7',0.300917351504644548),$sum($product('X_8',0.201867708618147346),$uminus(0.02249745933799302)))))))))),0.0),0.136425962361040792),$sum($product(max($sum($product('X_0',0.06116423178510666),$sum($product('X_1',0.204715007928164938),$sum($product('X_2',$uminus(0.099435113324590901)),$sum($product('X_3',$uminus(0.075076646106589484)),$sum($product('X_4',$uminus(0.147611930043982709)),$sum($product('X_5',0.329771718125498159),$sum($product('X_6',$uminus(0.077929763794931661)),$sum($product('X_7',0.158305623398400153),$sum($product('X_8',0.106605366167060955),0.227482560218186969))))))))),0.0),0.056848109871719316),$sum($product(max($sum($product('X_0',$uminus(0.092366462711563596)),$sum($product('X_1',0.052646937452845266),$sum($product('X_2',0.015413236401603803),$sum($product('X_3',0.113228661403501463),$sum($product('X_4',$uminus(0.121216575464961451)),$sum($product('X_5',$uminus(0.215702653361375507)),$sum($product('X_6',0.226017336583560879),$sum($product('X_7',$uminus(0.220132361394591358)),$sum($product('X_8',$uminus(0.307768566023152002)),0.320006108957572477))))))))),0.0),$uminus(0.151135334635830232)),$sum($product(max($sum($product('X_0',$uminus(0.226766580533465462)),$sum($product('X_1',0.00391162568521225),$sum($product('X_2',0.019473623430183329),$sum($product('X_3',0.216386614008901634),$sum($product('X_4',$uminus(0.078297955556637266)),$sum($product('X_5',0.255109588258111974),$sum($product('X_6',$uminus(0.083549070923979812)),$sum($product('X_7',$uminus(0.227547325045974136)),$sum($product('X_8',$uminus(0.243613693974603474)),$uminus(0.293731755902412184)))))))))),0.0),0.064636879471871189),$sum($product(max($sum($product('X_0',0.067140788316724598),$sum($product('X_1',$uminus(0.03548741081174861)),$sum($product('X_2',0.172652969653422972),$sum($product('X_3',$uminus(0.0931690048650268)),$sum($product('X_4',$uminus(0.028500025351721081)),$sum($product('X_5',0.14805861924911623),$sum($product('X_6',$uminus(0.269308449436302999)),$sum($product('X_7',$uminus(0.224045703414196051)),$sum($product('X_8',$uminus(0.031612092375694345)),$uminus(0.190489098222868414)))))))))),0.0),0.008393055112702774),$sum($product(max($sum($product('X_0',$uminus(0.283171155800769958)),$sum($product('X_1',$uminus(0.018460033900721984)),$sum($product('X_2',0.218690372500649099),$sum($product('X_3',0.284174999537985584),$sum($product('X_4',0.127309836240449004),$sum($product('X_5',0.163578447613004718),$sum($product('X_6',$uminus(0.19874294302317802)),$sum($product('X_7',$uminus(0.317257731536686072)),$sum($product('X_8',$uminus(0.267960016746490171)),0.290800639964543028))))))))),0.0),$uminus(0.086590064435252648)),$sum($product(max($sum($product('X_0',$uminus(0.0725795111797361)),$sum($product('X_1',$uminus(0.120319623004474657)),$sum($product('X_2',$uminus(0.114421945285064997)),$sum($product('X_3',0.215714109924082409),$sum($product('X_4',$uminus(0.008755817146637979)),$sum($product('X_5',$uminus(0.219790524805509563)),$sum($product('X_6',$uminus(0.302111967118618541)),$sum($product('X_7',$uminus(0.222922230078116679)),$sum($product('X_8',$uminus(0.251709505974506254)),$uminus(0.326284828368465285)))))))))),0.0),0.027061152757942769),$sum($product(max($sum($product('X_0',0.223511809452060006),$sum($product('X_1',0.105431646849439176),$sum($product('X_2',0.017074992645697451),$sum($product('X_3',$uminus(0.068702701737561434)),$sum($product('X_4',$uminus(0.042933026550501019)),$sum($product('X_5',$uminus(0.05012084091704655)),$sum($product('X_6',$uminus(0.267050073103187069)),$sum($product('X_7',$uminus(0.305230848586137749)),$sum($product('X_8',0.169917993562293479),0.242389984971433103))))))))),0.0),$uminus(0.116050913247573606)),$sum($product(max($sum($product('X_0',0.143380167173043749),$sum($product('X_1',$uminus(0.261902473627182053)),$sum($product('X_2',$uminus(0.069372572421227796)),$sum($product('X_3',$uminus(0.09762913086169403)),$sum($product('X_4',$uminus(0.279467825999905162)),$sum($product('X_5',$uminus(0.074563064956958358)),$sum($product('X_6',0.242162004287260368),$sum($product('X_7',0.064739396957266548),$sum($product('X_8',$uminus(0.24585648625546358)),$uminus(0.120744054176062848)))))))))),0.0),0.120861687905538667),$sum($product(max($sum($product('X_0',$uminus(0.271806868921937173)),$sum($product('X_1',0.192786148129760748),$sum($product('X_2',$uminus(0.265789744937258876)),$sum($product('X_3',0.305951947524789991),$sum($product('X_4',0.23169263946176194),$sum($product('X_5',$uminus(0.058046107628971055)),$sum($product('X_6',$uminus(0.260905027316403082)),$sum($product('X_7',0.140278727566981731),$sum($product('X_8',$uminus(0.119580601626665756)),$uminus(0.25399765408133701)))))))))),0.0),$uminus(0.141158103785410327)),$sum($product(max($sum($product('X_0',$uminus(0.180535942580106135)),$sum($product('X_1',$uminus(0.078816567104432078)),$sum($product('X_2',0.270339928183404965),$sum($product('X_3',0.167454511534455508),$sum($product('X_4',$uminus(0.331345024402933341)),$sum($product('X_5',$uminus(0.134734984988303996)),$sum($product('X_6',0.11646087972096425),$sum($product('X_7',$uminus(0.288940128920388006)),$sum($product('X_8',0.023771975478321161),0.119256284613703689))))))))),0.0),0.004501265651469327),$sum($product(max($sum($product('X_0',0.229344671986353832),$sum($product('X_1',0.077751196189045302),$sum($product('X_2',$uminus(0.299189374278061193)),$sum($product('X_3',$uminus(0.063015801812984884)),$sum($product('X_4',0.328319748032158965),$sum($product('X_5',0.157088214412941352),$sum($product('X_6',0.029268535381060168),$sum($product('X_7',0.274656616745850568),$sum($product('X_8',0.144313026206903172),$uminus(0.076488406458863623)))))))))),0.0),$uminus(0.148575278274818645)),$sum($product(max($sum($product('X_0',$uminus(0.295229121002945238)),$sum($product('X_1',0.250267751274626249),$sum($product('X_2',0.05458341403079503),$sum($product('X_3',$uminus(0.316841801114587041)),$sum($product('X_4',$uminus(0.010146514051700473)),$sum($product('X_5',0.028656171184171575),$sum($product('X_6',0.096331746773274329),$sum($product('X_7',$uminus(0.010367995907403615)),$sum($product('X_8',0.099029964077058219),0.23009073028369359))))))))),0.0),0.107636773564289218),$sum($product(max($sum($product('X_0',$uminus(0.024154254689310706)),$sum($product('X_1',$uminus(0.318461633220060603)),$sum($product('X_2',$uminus(0.099539216620869064)),$sum($product('X_3',$uminus(0.269059058694451791)),$sum($product('X_4',0.315147523984193823),$sum($product('X_5',0.040530443292059626),$sum($product('X_6',0.076347447009154579),$sum($product('X_7',$uminus(0.147734037206016217)),$sum($product('X_8',0.291049624306576049),0.08619313628106634))))))))),0.0),0.173317570857946995),$sum($product(max($sum($product('X_0',$uminus(0.112409864464090792)),$sum($product('X_1',0.01353162096107452),$sum($product('X_2',$uminus(0.02548901498770223)),$sum($product('X_3',0.032351808775658186),$sum($product('X_4',$uminus(0.162908946127287457)),$sum($product('X_5',$uminus(0.13855301706381265)),$sum($product('X_6',$uminus(0.123810348662606678)),$sum($product('X_7',$uminus(0.212094939047360098)),$sum($product('X_8',$uminus(0.216677291236464425)),$uminus(0.095959155784354933)))))))))),0.0),$uminus(0.105501284321076805)),$sum($product(max($sum($product('X_0',0.175651345260155523),$sum($product('X_1',0.188605425088383905),$sum($product('X_2',0.023435288099971918),$sum($product('X_3',0.248480660255076702),$sum($product('X_4',0.273942775226820479),$sum($product('X_5',$uminus(0.135710397401424709)),$sum($product('X_6',$uminus(0.30755508160556011)),$sum($product('X_7',0.144725408519543242),$sum($product('X_8',0.011562496541478506),0.079719747766130833))))))))),0.0),$uminus(0.07057415354783815)),$sum($product(max($sum($product('X_0',0.091009525495494847),$sum($product('X_1',$uminus(0.292547844235659493)),$sum($product('X_2',0.197565541562245206),$sum($product('X_3',$uminus(0.095680712033663573)),$sum($product('X_4',0.325005835691322853),$sum($product('X_5',0.196008450170439052),$sum($product('X_6',$uminus(0.291515907551800346)),$sum($product('X_7',0.194995070875606913),$sum($product('X_8',$uminus(0.164718689523304068)),0.163495981361108544))))))))),0.0),0.114115570696125684),$sum($product(max($sum($product('X_0',$uminus(0.05565613137069686)),$sum($product('X_1',0.059211661997694842),$sum($product('X_2',$uminus(0.209390279526032064)),$sum($product('X_3',$uminus(0.083248962597532949)),$sum($product('X_4',$uminus(0.108617811253452518)),$sum($product('X_5',$uminus(0.094488758575356713)),$sum($product('X_6',$uminus(0.284226770453594624)),$sum($product('X_7',0.23114465798782774),$sum($product('X_8',0.232274809206353294),$uminus(0.232150653009682018)))))))))),0.0),0.059991453404205669),0.002318902408805029)))))))))))))))))))))))))))))))) ).
%---(Y_2 = ((max(((X_0 * -0.085084204329484825) + (X_1 * 0.227277475280493524) + (X_2 * -0.146610404330747374) + (X_3 * -0.025088421047380127) + (X_4 * -0.236920078172610987) + (X_5 * 0.23556591236427632) + (X_6 * 0.045722886609951274) + (X_7 * -0.02105634790933264) + (X_8 * 0.299466624300461504) + 0.329253528971797216), 0.0) * 0.028186373852603058) + (max(((X_0 * 0.131301485190524703) + (X_1 * 0.209271326399700974) + (X_2 * -0.003838650175968794) + (X_3 * 0.216285547045041937) + (X_4 * -0.078518216784271455) + (X_5 * -0.101796191230834998) + (X_6 * -0.11810206645944557) + (X_7 * 0.073250343005372975) + (X_8 * 0.081758464201247938) + -0.139974431335130989), 0.0) * 0.048165901753140727) + (max(((X_0 * 0.151966319200479649) + (X_1 * -0.110606617906597343) + (X_2 * -0.060634341256404101) + (X_3 * 0.064220146693632352) + (X_4 * 0.022958266738014321) + (X_5 * -0.019995998724101849) + (X_6 * -0.050459445689319427) + (X_7 * 0.239386637748791598) + (X_8 * 0.193895523780232837) + -0.025201949827679204), 0.0) * 0.144120854085439648) + (max(((X_0 * 0.201918035720349331) + (X_1 * 0.071474693145737511) + (X_2 * -0.23470773195197539) + (X_3 * -0.233331659063250207) + (X_4 * 0.208583110235902314) + (X_5 * 0.291057185061493195) + (X_6 * -0.225458440742216049) + (X_7 * 0.30067966240644789) + (X_8 * -0.089917230539459242) + 0.021089287317174688), 0.0) * 0.009241838848862954) + (max(((X_0 * -0.133815944346616478) + (X_1 * -0.141304679292629271) + (X_2 * -0.219916577214829184) + (X_3 * -0.139758046639439831) + (X_4 * 0.023704997592138122) + (X_5 * 0.027489860415485401) + (X_6 * 0.28621826738765116) + (X_7 * 0.17028321810148489) + (X_8 * 0.155422226139109998) + -0.115193574595601644), 0.0) * -0.070659865038523909) + (max(((X_0 * -0.253268830840590653) + (X_1 * -0.063029704424822863) + (X_2 * 0.108342209516613941) + (X_3 * 0.011393961409695397) + (X_4 * -0.247224555255746742) + (X_5 * -0.245467779204527226) + (X_6 * 0.255234081909341326) + (X_7 * 0.147853392187311028) + (X_8 * 0.289447914966787068) + 0.203088066262591405), 0.0) * -0.008366350840023101) + (max(((X_0 * -0.119348940666866188) + (X_1 * -0.015475394094090544) + (X_2 * -0.257618085520195383) + (X_3 * 0.266883445685118181) + (X_4 * 0.154463982908279673) + (X_5 * 0.049303003478437801) + (X_6 * 0.170243650563203286) + (X_7 * 0.269376706562944379) + (X_8 * -0.046691059958949621) + 0.141036994079377198), 0.0) * 0.10830601332381648) + (max(((X_0 * 0.181914050129224181) + (X_1 * 0.069066291091121113) + (X_2 * 0.078554846238518217) + (X_3 * 0.123390095445965298) + (X_4 * -0.031434673366901533) + (X_5 * 0.120282490489638627) + (X_6 * 0.031318603965440728) + (X_7 * 0.245581722149856574) + (X_8 * -0.021362740664095992) + 0.197320938824874503), 0.0) * -0.144237909177295065) + (max(((X_0 * -0.098483582586146978) + (X_1 * 0.243394546376257848) + (X_2 * 0.115025912113307038) + (X_3 * 0.059118247029516235) + (X_4 * -0.044447188855861575) + (X_5 * -0.173647353012183814) + (X_6 * 0.176566057771695817) + (X_7 * 0.264381326549107676) + (X_8 * 0.078060224645663701) + 0.038845687539709906), 0.0) * -0.001756068565124336) + (max(((X_0 * -0.323129810216333357) + (X_1 * 0.203658385409960896) + (X_2 * 0.113291471700892099) + (X_3 * -0.100124959660652074) + (X_4 * -0.28985347600821415) + (X_5 * 0.296479167320807202) + (X_6 * 0.199063337816699659) + (X_7 * -0.06805784076294108) + (X_8 * -0.28999374577009368) + -0.064859166636634213), 0.0) * 0.060670637467299948) + (max(((X_0 * -0.101138320969167639) + (X_1 * 0.320103369940945515) + (X_2 * 0.229092709080107315) + (X_3 * 0.100355428234711164) + (X_4 * 0.17256061748191559) + (X_5 * 0.172824269742782366) + (X_6 * -0.00821012582886177) + (X_7 * 0.159414582738557076) + (X_8 * -0.198533216177367772) + -0.318412682581384776), 0.0) * -0.171905335021565575) + (max(((X_0 * 0.175819166464083299) + (X_1 * -0.14776993571183028) + (X_2 * -0.068844059775948763) + (X_3 * -0.188063081708857771) + (X_4 * -0.311504716200073695) + (X_5 * 0.088351922204317035) + (X_6 * -0.16596908518028744) + (X_7 * -0.139144677747215173) + (X_8 * 0.243917224520820819) + -0.047620091562705691), 0.0) * -0.166703466294858271) + (max(((X_0 * -0.315331204850205105) + (X_1 * -0.094618536390520314) + (X_2 * -0.156319919457583195) + (X_3 * 0.314122227139165766) + (X_4 * 0.181343578932227689) + (X_5 * 0.287763417098287844) + (X_6 * 0.019804317916209957) + (X_7 * 0.102935985091808402) + (X_8 * -0.170962160039119043) + -0.19759119588505758), 0.0) * -0.15235942333208416) + (max(((X_0 * 0.076796260324881238) + (X_1 * -0.07336050052662707) + (X_2 * 0.312311337905172348) + (X_3 * -0.317577596340329005) + (X_4 * 0.302325881276476804) + (X_5 * -0.128005488866581196) + (X_6 * -0.096981057694019324) + (X_7 * -0.133248611155060148) + (X_8 * 0.226658256292756988) + 0.124205739234839296), 0.0) * -0.090176877137669503) + (max(((X_0 * 0.265775077062823717) + (X_1 * 0.247512118108101642) + (X_2 * 0.052452192142516785) + (X_3 * 0.002814471274279473) + (X_4 * 0.054493435203783414) + (X_5 * -0.277167547039640971) + (X_6 * 0.149280534429790446) + (X_7 * 0.300917351504644548) + (X_8 * 0.201867708618147346) + -0.02249745933799302), 0.0) * -0.021033488455386162) + (max(((X_0 * 0.06116423178510666) + (X_1 * 0.204715007928164938) + (X_2 * -0.099435113324590901) + (X_3 * -0.075076646106589484) + (X_4 * -0.147611930043982709) + (X_5 * 0.329771718125498159) + (X_6 * -0.077929763794931661) + (X_7 * 0.158305623398400153) + (X_8 * 0.106605366167060955) + 0.227482560218186969), 0.0) * -0.176679172968433801) + (max(((X_0 * -0.092366462711563596) + (X_1 * 0.052646937452845266) + (X_2 * 0.015413236401603803) + (X_3 * 0.113228661403501463) + (X_4 * -0.121216575464961451) + (X_5 * -0.215702653361375507) + (X_6 * 0.226017336583560879) + (X_7 * -0.220132361394591358) + (X_8 * -0.307768566023152002) + 0.320006108957572477), 0.0) * 0.052727973594992344) + (max(((X_0 * -0.226766580533465462) + (X_1 * 0.00391162568521225) + (X_2 * 0.019473623430183329) + (X_3 * 0.216386614008901634) + (X_4 * -0.078297955556637266) + (X_5 * 0.255109588258111974) + (X_6 * -0.083549070923979812) + (X_7 * -0.227547325045974136) + (X_8 * -0.243613693974603474) + -0.293731755902412184), 0.0) * 0.13557251843815385) + (max(((X_0 * 0.067140788316724598) + (X_1 * -0.03548741081174861) + (X_2 * 0.172652969653422972) + (X_3 * -0.0931690048650268) + (X_4 * -0.028500025351721081) + (X_5 * 0.14805861924911623) + (X_6 * -0.269308449436302999) + (X_7 * -0.224045703414196051) + (X_8 * -0.031612092375694345) + -0.190489098222868414), 0.0) * 0.105705324742397938) + (max(((X_0 * -0.283171155800769958) + (X_1 * -0.018460033900721984) + (X_2 * 0.218690372500649099) + (X_3 * 0.284174999537985584) + (X_4 * 0.127309836240449004) + (X_5 * 0.163578447613004718) + (X_6 * -0.19874294302317802) + (X_7 * -0.317257731536686072) + (X_8 * -0.267960016746490171) + 0.290800639964543028), 0.0) * 0.051486515265045107) + (max(((X_0 * -0.0725795111797361) + (X_1 * -0.120319623004474657) + (X_2 * -0.114421945285064997) + (X_3 * 0.215714109924082409) + (X_4 * -0.008755817146637979) + (X_5 * -0.219790524805509563) + (X_6 * -0.302111967118618541) + (X_7 * -0.222922230078116679) + (X_8 * -0.251709505974506254) + -0.326284828368465285), 0.0) * -0.031404566017481289) + (max(((X_0 * 0.223511809452060006) + (X_1 * 0.105431646849439176) + (X_2 * 0.017074992645697451) + (X_3 * -0.068702701737561434) + (X_4 * -0.042933026550501019) + (X_5 * -0.05012084091704655) + (X_6 * -0.267050073103187069) + (X_7 * -0.305230848586137749) + (X_8 * 0.169917993562293479) + 0.242389984971433103), 0.0) * 0.042609344002828536) + (max(((X_0 * 0.143380167173043749) + (X_1 * -0.261902473627182053) + (X_2 * -0.069372572421227796) + (X_3 * -0.09762913086169403) + (X_4 * -0.279467825999905162) + (X_5 * -0.074563064956958358) + (X_6 * 0.242162004287260368) + (X_7 * 0.064739396957266548) + (X_8 * -0.24585648625546358) + -0.120744054176062848), 0.0) * 0.045186478342727487) + (max(((X_0 * -0.271806868921937173) + (X_1 * 0.192786148129760748) + (X_2 * -0.265789744937258876) + (X_3 * 0.305951947524789991) + (X_4 * 0.23169263946176194) + (X_5 * -0.058046107628971055) + (X_6 * -0.260905027316403082) + (X_7 * 0.140278727566981731) + (X_8 * -0.119580601626665756) + -0.25399765408133701), 0.0) * 0.023098752982494614) + (max(((X_0 * -0.180535942580106135) + (X_1 * -0.078816567104432078) + (X_2 * 0.270339928183404965) + (X_3 * 0.167454511534455508) + (X_4 * -0.331345024402933341) + (X_5 * -0.134734984988303996) + (X_6 * 0.11646087972096425) + (X_7 * -0.288940128920388006) + (X_8 * 0.023771975478321161) + 0.119256284613703689), 0.0) * -0.042633078628132176) + (max(((X_0 * 0.229344671986353832) + (X_1 * 0.077751196189045302) + (X_2 * -0.299189374278061193) + (X_3 * -0.063015801812984884) + (X_4 * 0.328319748032158965) + (X_5 * 0.157088214412941352) + (X_6 * 0.029268535381060168) + (X_7 * 0.274656616745850568) + (X_8 * 0.144313026206903172) + -0.076488406458863623), 0.0) * 0.028755904445657815) + (max(((X_0 * -0.295229121002945238) + (X_1 * 0.250267751274626249) + (X_2 * 0.05458341403079503) + (X_3 * -0.316841801114587041) + (X_4 * -0.010146514051700473) + (X_5 * 0.028656171184171575) + (X_6 * 0.096331746773274329) + (X_7 * -0.010367995907403615) + (X_8 * 0.099029964077058219) + 0.23009073028369359), 0.0) * -0.119335312267801155) + (max(((X_0 * -0.024154254689310706) + (X_1 * -0.318461633220060603) + (X_2 * -0.099539216620869064) + (X_3 * -0.269059058694451791) + (X_4 * 0.315147523984193823) + (X_5 * 0.040530443292059626) + (X_6 * 0.076347447009154579) + (X_7 * -0.147734037206016217) + (X_8 * 0.291049624306576049) + 0.08619313628106634), 0.0) * 0.066694870286236413) + (max(((X_0 * -0.112409864464090792) + (X_1 * 0.01353162096107452) + (X_2 * -0.02548901498770223) + (X_3 * 0.032351808775658186) + (X_4 * -0.162908946127287457) + (X_5 * -0.13855301706381265) + (X_6 * -0.123810348662606678) + (X_7 * -0.212094939047360098) + (X_8 * -0.216677291236464425) + -0.095959155784354933), 0.0) * 0.014763255248747831) + (max(((X_0 * 0.175651345260155523) + (X_1 * 0.188605425088383905) + (X_2 * 0.023435288099971918) + (X_3 * 0.248480660255076702) + (X_4 * 0.273942775226820479) + (X_5 * -0.135710397401424709) + (X_6 * -0.30755508160556011) + (X_7 * 0.144725408519543242) + (X_8 * 0.011562496541478506) + 0.079719747766130833), 0.0) * 0.087028504640350196) + (max(((X_0 * 0.091009525495494847) + (X_1 * -0.292547844235659493) + (X_2 * 0.197565541562245206) + (X_3 * -0.095680712033663573) + (X_4 * 0.325005835691322853) + (X_5 * 0.196008450170439052) + (X_6 * -0.291515907551800346) + (X_7 * 0.194995070875606913) + (X_8 * -0.164718689523304068) + 0.163495981361108544), 0.0) * -0.072092186879369802) + (max(((X_0 * -0.05565613137069686) + (X_1 * 0.059211661997694842) + (X_2 * -0.209390279526032064) + (X_3 * -0.083248962597532949) + (X_4 * -0.108617811253452518) + (X_5 * -0.094488758575356713) + (X_6 * -0.284226770453594624) + (X_7 * 0.23114465798782774) + (X_8 * 0.232274809206353294) + -0.232150653009682018), 0.0) * 0.02097734458237227) + 0.118035789508800421))
tff(formula_22,axiom,
'Y_2' = $sum($product(max($sum($product('X_0',$uminus(0.085084204329484825)),$sum($product('X_1',0.227277475280493524),$sum($product('X_2',$uminus(0.146610404330747374)),$sum($product('X_3',$uminus(0.025088421047380127)),$sum($product('X_4',$uminus(0.236920078172610987)),$sum($product('X_5',0.23556591236427632),$sum($product('X_6',0.045722886609951274),$sum($product('X_7',$uminus(0.02105634790933264)),$sum($product('X_8',0.299466624300461504),0.329253528971797216))))))))),0.0),0.028186373852603058),$sum($product(max($sum($product('X_0',0.131301485190524703),$sum($product('X_1',0.209271326399700974),$sum($product('X_2',$uminus(0.003838650175968794)),$sum($product('X_3',0.216285547045041937),$sum($product('X_4',$uminus(0.078518216784271455)),$sum($product('X_5',$uminus(0.101796191230834998)),$sum($product('X_6',$uminus(0.11810206645944557)),$sum($product('X_7',0.073250343005372975),$sum($product('X_8',0.081758464201247938),$uminus(0.139974431335130989)))))))))),0.0),0.048165901753140727),$sum($product(max($sum($product('X_0',0.151966319200479649),$sum($product('X_1',$uminus(0.110606617906597343)),$sum($product('X_2',$uminus(0.060634341256404101)),$sum($product('X_3',0.064220146693632352),$sum($product('X_4',0.022958266738014321),$sum($product('X_5',$uminus(0.019995998724101849)),$sum($product('X_6',$uminus(0.050459445689319427)),$sum($product('X_7',0.239386637748791598),$sum($product('X_8',0.193895523780232837),$uminus(0.025201949827679204)))))))))),0.0),0.144120854085439648),$sum($product(max($sum($product('X_0',0.201918035720349331),$sum($product('X_1',0.071474693145737511),$sum($product('X_2',$uminus(0.23470773195197539)),$sum($product('X_3',$uminus(0.233331659063250207)),$sum($product('X_4',0.208583110235902314),$sum($product('X_5',0.291057185061493195),$sum($product('X_6',$uminus(0.225458440742216049)),$sum($product('X_7',0.30067966240644789),$sum($product('X_8',$uminus(0.089917230539459242)),0.021089287317174688))))))))),0.0),0.009241838848862954),$sum($product(max($sum($product('X_0',$uminus(0.133815944346616478)),$sum($product('X_1',$uminus(0.141304679292629271)),$sum($product('X_2',$uminus(0.219916577214829184)),$sum($product('X_3',$uminus(0.139758046639439831)),$sum($product('X_4',0.023704997592138122),$sum($product('X_5',0.027489860415485401),$sum($product('X_6',0.28621826738765116),$sum($product('X_7',0.17028321810148489),$sum($product('X_8',0.155422226139109998),$uminus(0.115193574595601644)))))))))),0.0),$uminus(0.070659865038523909)),$sum($product(max($sum($product('X_0',$uminus(0.253268830840590653)),$sum($product('X_1',$uminus(0.063029704424822863)),$sum($product('X_2',0.108342209516613941),$sum($product('X_3',0.011393961409695397),$sum($product('X_4',$uminus(0.247224555255746742)),$sum($product('X_5',$uminus(0.245467779204527226)),$sum($product('X_6',0.255234081909341326),$sum($product('X_7',0.147853392187311028),$sum($product('X_8',0.289447914966787068),0.203088066262591405))))))))),0.0),$uminus(0.008366350840023101)),$sum($product(max($sum($product('X_0',$uminus(0.119348940666866188)),$sum($product('X_1',$uminus(0.015475394094090544)),$sum($product('X_2',$uminus(0.257618085520195383)),$sum($product('X_3',0.266883445685118181),$sum($product('X_4',0.154463982908279673),$sum($product('X_5',0.049303003478437801),$sum($product('X_6',0.170243650563203286),$sum($product('X_7',0.269376706562944379),$sum($product('X_8',$uminus(0.046691059958949621)),0.141036994079377198))))))))),0.0),0.10830601332381648),$sum($product(max($sum($product('X_0',0.181914050129224181),$sum($product('X_1',0.069066291091121113),$sum($product('X_2',0.078554846238518217),$sum($product('X_3',0.123390095445965298),$sum($product('X_4',$uminus(0.031434673366901533)),$sum($product('X_5',0.120282490489638627),$sum($product('X_6',0.031318603965440728),$sum($product('X_7',0.245581722149856574),$sum($product('X_8',$uminus(0.021362740664095992)),0.197320938824874503))))))))),0.0),$uminus(0.144237909177295065)),$sum($product(max($sum($product('X_0',$uminus(0.098483582586146978)),$sum($product('X_1',0.243394546376257848),$sum($product('X_2',0.115025912113307038),$sum($product('X_3',0.059118247029516235),$sum($product('X_4',$uminus(0.044447188855861575)),$sum($product('X_5',$uminus(0.173647353012183814)),$sum($product('X_6',0.176566057771695817),$sum($product('X_7',0.264381326549107676),$sum($product('X_8',0.078060224645663701),0.038845687539709906))))))))),0.0),$uminus(0.001756068565124336)),$sum($product(max($sum($product('X_0',$uminus(0.323129810216333357)),$sum($product('X_1',0.203658385409960896),$sum($product('X_2',0.113291471700892099),$sum($product('X_3',$uminus(0.100124959660652074)),$sum($product('X_4',$uminus(0.28985347600821415)),$sum($product('X_5',0.296479167320807202),$sum($product('X_6',0.199063337816699659),$sum($product('X_7',$uminus(0.06805784076294108)),$sum($product('X_8',$uminus(0.28999374577009368)),$uminus(0.064859166636634213)))))))))),0.0),0.060670637467299948),$sum($product(max($sum($product('X_0',$uminus(0.101138320969167639)),$sum($product('X_1',0.320103369940945515),$sum($product('X_2',0.229092709080107315),$sum($product('X_3',0.100355428234711164),$sum($product('X_4',0.17256061748191559),$sum($product('X_5',0.172824269742782366),$sum($product('X_6',$uminus(0.00821012582886177)),$sum($product('X_7',0.159414582738557076),$sum($product('X_8',$uminus(0.198533216177367772)),$uminus(0.318412682581384776)))))))))),0.0),$uminus(0.171905335021565575)),$sum($product(max($sum($product('X_0',0.175819166464083299),$sum($product('X_1',$uminus(0.14776993571183028)),$sum($product('X_2',$uminus(0.068844059775948763)),$sum($product('X_3',$uminus(0.188063081708857771)),$sum($product('X_4',$uminus(0.311504716200073695)),$sum($product('X_5',0.088351922204317035),$sum($product('X_6',$uminus(0.16596908518028744)),$sum($product('X_7',$uminus(0.139144677747215173)),$sum($product('X_8',0.243917224520820819),$uminus(0.047620091562705691)))))))))),0.0),$uminus(0.166703466294858271)),$sum($product(max($sum($product('X_0',$uminus(0.315331204850205105)),$sum($product('X_1',$uminus(0.094618536390520314)),$sum($product('X_2',$uminus(0.156319919457583195)),$sum($product('X_3',0.314122227139165766),$sum($product('X_4',0.181343578932227689),$sum($product('X_5',0.287763417098287844),$sum($product('X_6',0.019804317916209957),$sum($product('X_7',0.102935985091808402),$sum($product('X_8',$uminus(0.170962160039119043)),$uminus(0.19759119588505758)))))))))),0.0),$uminus(0.15235942333208416)),$sum($product(max($sum($product('X_0',0.076796260324881238),$sum($product('X_1',$uminus(0.07336050052662707)),$sum($product('X_2',0.312311337905172348),$sum($product('X_3',$uminus(0.317577596340329005)),$sum($product('X_4',0.302325881276476804),$sum($product('X_5',$uminus(0.128005488866581196)),$sum($product('X_6',$uminus(0.096981057694019324)),$sum($product('X_7',$uminus(0.133248611155060148)),$sum($product('X_8',0.226658256292756988),0.124205739234839296))))))))),0.0),$uminus(0.090176877137669503)),$sum($product(max($sum($product('X_0',0.265775077062823717),$sum($product('X_1',0.247512118108101642),$sum($product('X_2',0.052452192142516785),$sum($product('X_3',0.002814471274279473),$sum($product('X_4',0.054493435203783414),$sum($product('X_5',$uminus(0.277167547039640971)),$sum($product('X_6',0.149280534429790446),$sum($product('X_7',0.300917351504644548),$sum($product('X_8',0.201867708618147346),$uminus(0.02249745933799302)))))))))),0.0),$uminus(0.021033488455386162)),$sum($product(max($sum($product('X_0',0.06116423178510666),$sum($product('X_1',0.204715007928164938),$sum($product('X_2',$uminus(0.099435113324590901)),$sum($product('X_3',$uminus(0.075076646106589484)),$sum($product('X_4',$uminus(0.147611930043982709)),$sum($product('X_5',0.329771718125498159),$sum($product('X_6',$uminus(0.077929763794931661)),$sum($product('X_7',0.158305623398400153),$sum($product('X_8',0.106605366167060955),0.227482560218186969))))))))),0.0),$uminus(0.176679172968433801)),$sum($product(max($sum($product('X_0',$uminus(0.092366462711563596)),$sum($product('X_1',0.052646937452845266),$sum($product('X_2',0.015413236401603803),$sum($product('X_3',0.113228661403501463),$sum($product('X_4',$uminus(0.121216575464961451)),$sum($product('X_5',$uminus(0.215702653361375507)),$sum($product('X_6',0.226017336583560879),$sum($product('X_7',$uminus(0.220132361394591358)),$sum($product('X_8',$uminus(0.307768566023152002)),0.320006108957572477))))))))),0.0),0.052727973594992344),$sum($product(max($sum($product('X_0',$uminus(0.226766580533465462)),$sum($product('X_1',0.00391162568521225),$sum($product('X_2',0.019473623430183329),$sum($product('X_3',0.216386614008901634),$sum($product('X_4',$uminus(0.078297955556637266)),$sum($product('X_5',0.255109588258111974),$sum($product('X_6',$uminus(0.083549070923979812)),$sum($product('X_7',$uminus(0.227547325045974136)),$sum($product('X_8',$uminus(0.243613693974603474)),$uminus(0.293731755902412184)))))))))),0.0),0.13557251843815385),$sum($product(max($sum($product('X_0',0.067140788316724598),$sum($product('X_1',$uminus(0.03548741081174861)),$sum($product('X_2',0.172652969653422972),$sum($product('X_3',$uminus(0.0931690048650268)),$sum($product('X_4',$uminus(0.028500025351721081)),$sum($product('X_5',0.14805861924911623),$sum($product('X_6',$uminus(0.269308449436302999)),$sum($product('X_7',$uminus(0.224045703414196051)),$sum($product('X_8',$uminus(0.031612092375694345)),$uminus(0.190489098222868414)))))))))),0.0),0.105705324742397938),$sum($product(max($sum($product('X_0',$uminus(0.283171155800769958)),$sum($product('X_1',$uminus(0.018460033900721984)),$sum($product('X_2',0.218690372500649099),$sum($product('X_3',0.284174999537985584),$sum($product('X_4',0.127309836240449004),$sum($product('X_5',0.163578447613004718),$sum($product('X_6',$uminus(0.19874294302317802)),$sum($product('X_7',$uminus(0.317257731536686072)),$sum($product('X_8',$uminus(0.267960016746490171)),0.290800639964543028))))))))),0.0),0.051486515265045107),$sum($product(max($sum($product('X_0',$uminus(0.0725795111797361)),$sum($product('X_1',$uminus(0.120319623004474657)),$sum($product('X_2',$uminus(0.114421945285064997)),$sum($product('X_3',0.215714109924082409),$sum($product('X_4',$uminus(0.008755817146637979)),$sum($product('X_5',$uminus(0.219790524805509563)),$sum($product('X_6',$uminus(0.302111967118618541)),$sum($product('X_7',$uminus(0.222922230078116679)),$sum($product('X_8',$uminus(0.251709505974506254)),$uminus(0.326284828368465285)))))))))),0.0),$uminus(0.031404566017481289)),$sum($product(max($sum($product('X_0',0.223511809452060006),$sum($product('X_1',0.105431646849439176),$sum($product('X_2',0.017074992645697451),$sum($product('X_3',$uminus(0.068702701737561434)),$sum($product('X_4',$uminus(0.042933026550501019)),$sum($product('X_5',$uminus(0.05012084091704655)),$sum($product('X_6',$uminus(0.267050073103187069)),$sum($product('X_7',$uminus(0.305230848586137749)),$sum($product('X_8',0.169917993562293479),0.242389984971433103))))))))),0.0),0.042609344002828536),$sum($product(max($sum($product('X_0',0.143380167173043749),$sum($product('X_1',$uminus(0.261902473627182053)),$sum($product('X_2',$uminus(0.069372572421227796)),$sum($product('X_3',$uminus(0.09762913086169403)),$sum($product('X_4',$uminus(0.279467825999905162)),$sum($product('X_5',$uminus(0.074563064956958358)),$sum($product('X_6',0.242162004287260368),$sum($product('X_7',0.064739396957266548),$sum($product('X_8',$uminus(0.24585648625546358)),$uminus(0.120744054176062848)))))))))),0.0),0.045186478342727487),$sum($product(max($sum($product('X_0',$uminus(0.271806868921937173)),$sum($product('X_1',0.192786148129760748),$sum($product('X_2',$uminus(0.265789744937258876)),$sum($product('X_3',0.305951947524789991),$sum($product('X_4',0.23169263946176194),$sum($product('X_5',$uminus(0.058046107628971055)),$sum($product('X_6',$uminus(0.260905027316403082)),$sum($product('X_7',0.140278727566981731),$sum($product('X_8',$uminus(0.119580601626665756)),$uminus(0.25399765408133701)))))))))),0.0),0.023098752982494614),$sum($product(max($sum($product('X_0',$uminus(0.180535942580106135)),$sum($product('X_1',$uminus(0.078816567104432078)),$sum($product('X_2',0.270339928183404965),$sum($product('X_3',0.167454511534455508),$sum($product('X_4',$uminus(0.331345024402933341)),$sum($product('X_5',$uminus(0.134734984988303996)),$sum($product('X_6',0.11646087972096425),$sum($product('X_7',$uminus(0.288940128920388006)),$sum($product('X_8',0.023771975478321161),0.119256284613703689))))))))),0.0),$uminus(0.042633078628132176)),$sum($product(max($sum($product('X_0',0.229344671986353832),$sum($product('X_1',0.077751196189045302),$sum($product('X_2',$uminus(0.299189374278061193)),$sum($product('X_3',$uminus(0.063015801812984884)),$sum($product('X_4',0.328319748032158965),$sum($product('X_5',0.157088214412941352),$sum($product('X_6',0.029268535381060168),$sum($product('X_7',0.274656616745850568),$sum($product('X_8',0.144313026206903172),$uminus(0.076488406458863623)))))))))),0.0),0.028755904445657815),$sum($product(max($sum($product('X_0',$uminus(0.295229121002945238)),$sum($product('X_1',0.250267751274626249),$sum($product('X_2',0.05458341403079503),$sum($product('X_3',$uminus(0.316841801114587041)),$sum($product('X_4',$uminus(0.010146514051700473)),$sum($product('X_5',0.028656171184171575),$sum($product('X_6',0.096331746773274329),$sum($product('X_7',$uminus(0.010367995907403615)),$sum($product('X_8',0.099029964077058219),0.23009073028369359))))))))),0.0),$uminus(0.119335312267801155)),$sum($product(max($sum($product('X_0',$uminus(0.024154254689310706)),$sum($product('X_1',$uminus(0.318461633220060603)),$sum($product('X_2',$uminus(0.099539216620869064)),$sum($product('X_3',$uminus(0.269059058694451791)),$sum($product('X_4',0.315147523984193823),$sum($product('X_5',0.040530443292059626),$sum($product('X_6',0.076347447009154579),$sum($product('X_7',$uminus(0.147734037206016217)),$sum($product('X_8',0.291049624306576049),0.08619313628106634))))))))),0.0),0.066694870286236413),$sum($product(max($sum($product('X_0',$uminus(0.112409864464090792)),$sum($product('X_1',0.01353162096107452),$sum($product('X_2',$uminus(0.02548901498770223)),$sum($product('X_3',0.032351808775658186),$sum($product('X_4',$uminus(0.162908946127287457)),$sum($product('X_5',$uminus(0.13855301706381265)),$sum($product('X_6',$uminus(0.123810348662606678)),$sum($product('X_7',$uminus(0.212094939047360098)),$sum($product('X_8',$uminus(0.216677291236464425)),$uminus(0.095959155784354933)))))))))),0.0),0.014763255248747831),$sum($product(max($sum($product('X_0',0.175651345260155523),$sum($product('X_1',0.188605425088383905),$sum($product('X_2',0.023435288099971918),$sum($product('X_3',0.248480660255076702),$sum($product('X_4',0.273942775226820479),$sum($product('X_5',$uminus(0.135710397401424709)),$sum($product('X_6',$uminus(0.30755508160556011)),$sum($product('X_7',0.144725408519543242),$sum($product('X_8',0.011562496541478506),0.079719747766130833))))))))),0.0),0.087028504640350196),$sum($product(max($sum($product('X_0',0.091009525495494847),$sum($product('X_1',$uminus(0.292547844235659493)),$sum($product('X_2',0.197565541562245206),$sum($product('X_3',$uminus(0.095680712033663573)),$sum($product('X_4',0.325005835691322853),$sum($product('X_5',0.196008450170439052),$sum($product('X_6',$uminus(0.291515907551800346)),$sum($product('X_7',0.194995070875606913),$sum($product('X_8',$uminus(0.164718689523304068)),0.163495981361108544))))))))),0.0),$uminus(0.072092186879369802)),$sum($product(max($sum($product('X_0',$uminus(0.05565613137069686)),$sum($product('X_1',0.059211661997694842),$sum($product('X_2',$uminus(0.209390279526032064)),$sum($product('X_3',$uminus(0.083248962597532949)),$sum($product('X_4',$uminus(0.108617811253452518)),$sum($product('X_5',$uminus(0.094488758575356713)),$sum($product('X_6',$uminus(0.284226770453594624)),$sum($product('X_7',0.23114465798782774),$sum($product('X_8',0.232274809206353294),$uminus(0.232150653009682018)))))))))),0.0),0.02097734458237227),0.118035789508800421)))))))))))))))))))))))))))))))) ).
%---∀ 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 ) ) ) ).
%------------------------------------------------------------------------------