(set-param var-elim true)
(set-param arith-elim true)
;; (set-param branching theory)
(set-param bland-threshold 2000000)

(define s1_obj::real)
(define s2_obj::real)
(define s3_obj::real)
(define s4_obj::real)
(define s5_obj::real)
(define s6_obj::real)
(define s7_obj::real)
(define s8_obj::real)
(define s9_obj::real)
(define s10_obj::real)
(define s11_obj::real)
(define s12_obj::real)
(define s13_obj::real)
(define s14_obj::real)
(define s15_obj::real)
(define s16_obj::real)
(define s17_obj::real)
(define s18_obj::real)
(define s19_obj::real)
(define s20_obj::real)
(define s21_obj::real)
(define s22_obj::real)
(define s23_obj::real)
(define s24_obj::real)
(define s25_obj::real)
(define s26_obj::real)
(define s27_obj::real)
(define s29_obj::real)
(define s31_obj::real)
(define s32_obj::real)
(define s33_obj::real)
(define s34_obj::real)
(define s35_obj::real)
(define s36_obj::real)
(define s37_obj::real)
(define s38_nutr::real)
(define s39_nutr::real)
(define s40_nutr::real)
(define s41_nutr::real)
(define s42_nutr::real)
(define s43_nutr::real)
(define s44_nutr::real)
(define s45_nutr::real)
(define s46_nutr::real)
(define s47_nutr::real)
(define s48_nutr::real)
(define s49_nutr::real)
(define s50_nutr::real)
(define s51_nutr::real)
(define s52_secrt::real)
(define s53_secrt::real)
(define s54_secrt::real)


(define r38_nutr_r::real)
(define r39_nutr_r::real)
(define r40_nutr_r::real)
(define r41_nutr_r::real)
(define r42_nutr_r::real)
(define r43_nutr_r::real)
(define r44_nutr_r::real)
(define r45_nutr_r::real)
(define r46_nutr_r::real)
(define r47_nutr_r::real)
(define r48_nutr_r::real)
(define r49_nutr_r::real)
(define r50_nutr_r::real)
(define r51_nutr_r::real)
(define r52_secrt_r::real)
(define r53_secrt_r::real)
(define r54_secrt_r::real)
(define r55::real)
(define r56::real)
(define r57::real)
(define r58::real)
(define r59a::real)
(define r59b::real)
(define r60::real)
(define r61::real)
(define r62::real)
(define r63::real)
(define r64::real)
(define r65::real)
(define r66::real)
(define r67::real)
(define r68a::real)
(define r68b::real)
(define r69::real)
(define r70::real)
(define r71::real)
(define r72::real)
(define r73::real)
(define r74::real)
(define r75::real)
(define r76::real)
(define r77::real)
(define r78::real)
(define r79::real)
(define r80::real)
(define r81::real)
(define r82::real)
(define r83::real)
(define r84::real)
(define r85a::real)
(define r85b::real)
(define r86::real)
(define r87::real)
(define r88::real)
(define r89::real)
(define r90::real)
(define r91::real)
(define r92::real)
(define r93::real)
(define r94::real)
(define r95::real)
(define r96::real)
(define r97::real)
(define r98::real)
(define r99::real)
(define r100::real)
(define r101::real)
(define r102::real)
(define r103::real)
(define r104::real)
(define r105::real)
(define r106::real)
(define r107::real)
(define r108::real)
(define r109::real)
(define r110::real)
(define r111::real)
(define r112::real)
(define r113::real)
(define r114::real)
(define r115::real)
(define r116::real)
(define r117::real)
(define r118::real)
(define r119::real)
(define r120::real)
(define r121::real)
(define r122::real)
(define r123::real)
(define r124::real)
(define r125::real)
(define r126::real)
(define r127::real)
(define r128::real)
(define r129::real)
(define r130::real)
(define r131::real)
(define r132::real)
(define r133::real)
(define r134::real)
(define r135::real)
(define r136::real)
(define r137::real)
(define r138::real)
(define r139::real)
(define r140::real)
(define r141::real)
(define r142::real)
(define r143::real)
(define r144::real)
(define r145::real)
(define r146::real)
(define r147::real)
(define r148::real)
(define r149::real)
(define r150::real)
(define r151::real)
(define r152::real)
(define r153::real)
(define r154::real)
(define r155::real)
(define r156::real)
(define r157::real)
(define r158::real)
(define r159::real)
(define r160::real)
(define r161::real)
(define r162::real)
(define r163::real)
(define r164::real)
(define r165::real)
(define r166::real)
(define r167::real)
(define r168::real)
(define r169::real)
(define r170::real)
(define r171::real)
(define r172::real)
(define r173::real)
(define r174::real)
(define r175::real)
(define r176::real)
(define r177::real)
(define r178::real)
(define r179::real)
(define r180::real)
(define r181::real)
(define r182::real)
(define r183::real)
(define r184::real)
(define r185::real)
(define r186::real)
(define r187::real)
(define r188::real)
(define r189::real)
(define r190::real)
(define r191::real)
(define r192::real)
(define r193::real)
(define r194::real)
(define r195::real)
(define r196a::real)
(define r196b::real)
(define r197a::real)
(define r197b::real)
(define r198::real)
(define r199a::real)
(define r199b::real)
(define r200a::real)
(define r200b::real)
(define r201::real)
(define r202a::real)
(define r202b::real)
(define r203a::real)
(define r203b::real)
(define r204a::real)
(define r204b::real)
(define r205a::real)
(define r205b::real)
(define r206a::real)
(define r206b::real)
(define r207::real)
(define r208a::real)
(define r208b::real)
(define r209::real)
(define r210::real)
(define r211a::real)
(define r211b::real)
(define r212a::real)
(define r212b::real)
(define r213::real)
(define r214a::real)
(define r214b::real)
(define r215::real)
(define r216::real)
(define r217::real)
(define r218::real)
(define r219::real)
(define r220::real)
(define r221::real)
(define r222::real)
(define r223::real)
(define r224::real)
(define r225::real)
(define r226::real)
(define r227::real)
(define r228::real)
(define r229::real)
(define r230::real)
(define r231::real)
(define r232::real)
(define r233::real)
(define r234::real)
(define r235::real)
(define r236::real)
(define r237::real)
(define r238::real)
(define r239::real)
(define r240a::real)
(define r240b::real)
(define r241::real)
(define r242::real)
(define r243::real)
(define r244::real)
(define r245a::real)
(define r245b::real)
(define r246a::real)
(define r246b::real)
(define r247::real)
(define r248::real)
(define r249::real)
(define r250::real)
(define r251::real)
(define r252::real)
(define r253::real)
(define r254a::real)
(define r254b::real)
(define r255a::real)
(define r255b::real)
(define r256::real)
(define r257::real)
(define r258::real)
(define r259::real)
(define r260::real)
(define r261a::real)
(define r261b::real)
(define r262::real)
(define r263::real)
(define r264::real)
(define r265::real)
(define r266a::real)
(define r266b::real)
(define r267a::real)
(define r267b::real)
(define r268::real)
(define r269::real)
(define r270::real)
(define r271a::real)
(define r271b::real)
(define r272::real)
(define r273a::real)
(define r273b::real)
(define r274a::real)
(define r274b::real)
(define r275a::real)
(define r275b::real)
(define r276a::real)
(define r276b::real)
(define r277a::real)
(define r277b::real)
(define r278a::real)
(define r278b::real)
(define r279a::real)
(define r279b::real)
(define r280a::real)
(define r280b::real)
(define r281::real)
(define r282::real)
(define r283a::real)
(define r283b::real)
(define r284a::real)
(define r284b::real)
(define r285a::real)
(define r285b::real)
(define r286a::real)
(define r286b::real)
(define r287a::real)
(define r287b::real)
(define r288a::real)
(define r288b::real)
(define r289a::real)
(define r289b::real)
(define r290a::real)
(define r290b::real)
(define r291a::real)
(define r291b::real)
(define r292a::real)
(define r292b::real)
(define r293a::real)
(define r293b::real)
(define r294a::real)
(define r294b::real)
(define r295a::real)
(define r295b::real)
(define r296::real)
(define r297::real)
(define r298::real)
(define r299a::real)
(define r299b::real)
(define r300::real)
(define r301::real)
(define r302a::real)
(define r302b::real)
(define r303a::real)
(define r303b::real)
(define r304::real)
(define r305::real)
(define r306a::real)
(define r306b::real)
(define r307::real)
(define r308a::real)
(define r308b::real)
(define r309::real)
(define r310::real)
(define r311::real)
(define r312::real)
(define r313::real)
(define r314::real)
(define r315::real)
(define r316::real)
(define r317::real)
(define r318a::real)
(define r318b::real)
(define r319a::real)
(define r319b::real)
(define r320::real)
(define r321::real)
(define r322::real)
(define r323a::real)
(define r323b::real)
(define r324::real)
(define r325a::real)
(define r325b::real)
(define r326::real)
(define r327::real)
(define r328a::real)
(define r328b::real)
(define r329a::real)
(define r329b::real)
(define r330a::real)
(define r330b::real)
(define r331a::real)
(define r331b::real)
(define r332a::real)
(define r332b::real)
(define r333a::real)
(define r333b::real)
(define r334a::real)
(define r334b::real)
(define r335a::real)
(define r335b::real)
(define r336a::real)
(define r336b::real)
(define r337a::real)
(define r337b::real)
(define r338::real)
(define r339a::real)
(define r339b::real)
(define r340::real)
(define r341::real)
(define r342::real)
(define r343a::real)
(define r343b::real)
(define r344a::real)
(define r344b::real)
(define r345::real)
(define r346::real)
(define r347a::real)
(define r347b::real)
(define r348::real)
(define r349::real)
(define r350::real)
(define r351::real)
(define r352::real)
(define r353::real)
(define r354a::real)
(define r354b::real)
(define r355::real)
(define r356::real)
(define r357::real)
(define r358::real)
(define r359::real)
(define r360::real)
(define r361::real)
(define r362::real)
(define r363::real)
(define r364a::real)
(define r364b::real)
(define r365::real)
(define r366::real)
(define r367a::real)
(define r367b::real)
(define r368::real)
(define r369a::real)
(define r369b::real)
(define r370::real)
(define r371::real)
(define r372::real)
(define r373a::real)
(define r373b::real)
(define r374a::real)
(define r374b::real)
(define r375a::real)
(define r375b::real)
(define r376a::real)
(define r376b::real)
(define r377a::real)
(define r377b::real)
(define r378a::real)
(define r378b::real)
(define r379::real)
(define r380::real)
(define r381::real)
(define r382::real)
(define r383::real)
(define r384::real)
(define r385::real)
(define r386::real)
(define r387a::real)
(define r387b::real)
(define r388a::real)
(define r388b::real)
(define r389a::real)
(define r389b::real)
(define r390::real)
(define r391a::real)
(define r391b::real)
(define r392a::real)
(define r392b::real)
(define r393::real)
(define r394::real)
(define r395::real)
(define r396::real)
(define r397::real)
(define r398::real)
(define r399::real)
(define r400::real)
(define r401a::real)
(define r401b::real)
(define r402::real)
(define r403::real)
(define r404::real)
(define r405::real)
(define r406::real)
(define r407::real)
(define r408a::real)
(define r408b::real)
(define r409::real)
(define r410::real)
(define r411::real)
(define r412::real)
(define r413::real)
(define r414::real)
(define r415a::real)
(define r415b::real)
(define r416::real)
(define r417::real)
(define r418::real)
(define r419::real)
(define r420::real)
(define r421::real)
(define r422::real)
(define r423::real)
(define r424::real)
(define r425a::real)
(define r425b::real)
(define r426a::real)
(define r426b::real)
(define r427a::real)
(define r427b::real)
(define r428a::real)
(define r428b::real)
(define r429::real)
(define r430::real)
(define r431a::real)
(define r431b::real)
(define r432::real)
(define r433::real)
(define r434::real)
(define r435::real)
(define r436::real)
(define r437::real)
(define r438a::real)
(define r438b::real)
(define r439a::real)
(define r439b::real)
(define r440::real)
(define r441a::real)
(define r441b::real)
(define r442a::real)
(define r442b::real)
(define r443a::real)
(define r443b::real)
(define r444::real)
(define r445::real)
(define r446::real)
(define r447::real)
(define r448::real)
(define r449::real)
(define r450::real)
(define r451::real)
(define r452::real)
(define r453::real)
(define r454::real)
(define r455a::real)
(define r455b::real)
(define r456a::real)
(define r456b::real)
(define r457::real)
(define r458::real)
(define r459::real)
(define r460::real)
(define r461::real)
(define r462::real)
(define r463::real)
(define r464a::real)
(define r464b::real)
(define r465::real)
(define r466::real)
(define r467::real)
(define r468::real)
(define r469::real)
(define r470::real)
(define r471::real)
(define r472::real)
(define r473::real)
(define r474a::real)
(define r474b::real)
(define r475::real)
(define r476a::real)
(define r476b::real)
(define r477::real)
(define r478::real)
(define r479a::real)
(define r479b::real)
(define r480::real)
(define r481a::real)
(define r481b::real)
(define r482::real)
(define r483::real)
(define r484::real)
(define r485::real)
(define r486::real)
(define r487a::real)
(define r487b::real)
(define r488a::real)
(define r488b::real)
(define r489a::real)
(define r489b::real)
(define r490a::real)
(define r490b::real)
(define r491a::real)
(define r491b::real)
(define r492a::real)
(define r492b::real)
(define r493::real)
(define r494a::real)
(define r494b::real)
(define r495::real)
(define r496::real)
(define r497::real)
(define r498a::real)
(define r498b::real)
(define r499::real)
(define r500::real)
(define r501a::real)
(define r501b::real)
(define r502::real)
(define r503a::real)
(define r503b::real)
(define r504a::real)
(define r504b::real)
(define r505a::real)
(define r505b::real)
(define r506a::real)
(define r506b::real)
(define r507::real)
(define r508::real)
(define r509::real)
(define r510::real)
(define r511::real)
(define r512::real)
(define r513::real)
(define r514::real)
(define r515::real)
(define r516a::real)
(define r516b::real)
(define r517a::real)
(define r517b::real)
(define r518a::real)
(define r518b::real)
(define r519a::real)
(define r519b::real)
(define r520::real)
(define r521::real)
(define r522::real)
(define r523::real)
(define r524::real)
(define r525::real)
(define r526::real)
(define r527::real)
(define r528::real)
(define r529::real)
(define r530::real)
(define r531::real)
(define r532::real)
(define r533::real)
(define r534::real)
(define r535::real)
(define r536a::real)
(define r536b::real)
(define r537::real)
(define r538::real)
(define r539::real)
(define r540::real)
(define r541::real)
(define r542::real)
(define r543::real)
(define r544::real)
(define r545::real)
(define r546::real)
(define r547::real)
(define r548::real)
(define r549::real)
(define r550a::real)
(define r550b::real)
(define r551::real)
(define r552::real)
(define r553::real)
(define r554::real)
(define r555::real)
(define r556::real)
(define r557::real)
(define r558::real)
(define r559::real)
(define r560::real)
(define r561::real)
(define r562::real)
(define r563::real)
(define r564a::real)
(define r564b::real)
(define r565::real)
(define r566a::real)
(define r566b::real)
(define r567a::real)
(define r567b::real)
(define r568::real)
(define r569a::real)
(define r569b::real)
(define r570::real)
(define r571::real)
(define r572::real)
(define r573::real)
(define r574::real)
(define r575::real)
(define r576::real)
(define r577::real)
(define r578::real)
(define r579::real)
(define r580a::real)
(define r580b::real)
(define r581::real)
(define r582::real)
(define r583::real)
(define r584::real)
(define r585::real)
(define r586::real)
(define r587::real)
(define r588::real)
(define r589::real)
(define r590::real)
(define r591::real)
(define r592::real)
(define r593::real)
(define r594::real)
(define r595::real)
(define r596::real)
(define r597::real)
(define r598::real)
(define r599::real)
(define r600a::real)
(define r600b::real)
(define r601::real)
(define r602a::real)
(define r602b::real)
(define r603::real)
(define r604::real)
(define r605::real)
(define r606a::real)
(define r606b::real)
(define r607a::real)
(define r607b::real)
(define r608::real)
(define r609::real)
(define r610::real)
(define r611a::real)
(define r611b::real)
(define r612::real)
(define r613a::real)
(define r613b::real)
(define r614a::real)
(define r614b::real)
(define r618::real)
(define r619a::real)
(define r619b::real)
(define r620::real)
(define r621a::real)
(define r621b::real)
(define r622a::real)
(define r622b::real)
(define r623a::real)
(define r623b::real)
(define r624a::real)
(define r624b::real)
(define r625::real)
(define r626::real)
(define r632a::real)
(define r632b::real)
(define r633a::real)
(define r633b::real)
(define r634a::real)
(define r634b::real)
(define r635::real)
(define r636a::real)
(define r636b::real)
(define r637::real)
(define r638::real)
(define r639::real)
(define r640::real)
(define r641a::real)
(define r641b::real)
(define r642a::real)
(define r642b::real)
(define r643a::real)
(define r643b::real)
(define r644a::real)
(define r644b::real)
(define r645a::real)
(define r645b::real)
(define r646a::real)
(define r646b::real)
(define r647a::real)
(define r647b::real)
(define r648::real)
(define r649::real)
(define r650a::real)
(define r650b::real)
(define r651a::real)
(define r651b::real)
(define r652a::real)
(define r652b::real)
(define r653::real)
(define r657::real)
(define r658a::real)
(define r658b::real)
(define r662::real)
(define r663::real)
(define r664::real)
(define r668::real)
(define r674a::real)
(define r674b::real)
(define r687a::real)
(define r687b::real)
(define r688a::real)
(define r688b::real)
(define r689::real)
(define r690::real)
(define r691::real)
(define r692::real)
(define r693::real)
(define r694::real)
(define r695::real)
(define r696a::real)
(define r696b::real)
(define r697a::real)
(define r697b::real)
(define r698a::real)
(define r698b::real)
(define r699a::real)
(define r699b::real)
(define r700a::real)
(define r700b::real)
(define r701a::real)
(define r701b::real)
(define r702a::real)
(define r702b::real)
(define r703::real)
(define r704a::real)
(define r704b::real)
(define r705::real)
(define r706::real)
(define r707::real)
(define r708::real)
(define r709::real)
(define r710::real)
(define r711::real)
(define r712::real)
(define r713::real)
(define r714::real)
(define r715::real)
(define r716::real)
(define r717a::real)
(define r717b::real)
(define r718::real)
(define r719::real)
(define r720::real)
(define r721::real)
(define r722::real)
(define r723::real)
(define r724a::real)
(define r724b::real)
(define r725::real)
(define r726::real)
(define r727::real)
(define r728a::real)
(define r728b::real)
(define r729::real)
(define r730::real)
(define r731::real)
(define r732::real)
(define r733a::real)
(define r733b::real)
(define r734::real)
(define r735::real)
(define r736::real)
(define r737a::real)
(define r737b::real)
(define r738a::real)
(define r738b::real)
(define r739::real)
(define r740a::real)
(define r740b::real)
(define r741a::real)
(define r741b::real)
(define r742::real)
(define r743::real)
(define r744a::real)
(define r744b::real)
(define r745::real)
(define r746::real)
(define r747::real)
(define r748::real)
(define r749::real)
(define r750::real)
(define r751::real)
(define r752::real)
(define r753a::real)
(define r753b::real)
(define r754::real)
(define r755a::real)
(define r755b::real)
(define r756::real)
(define r757a::real)
(define r757b::real)
(define r758::real)
(define r759::real)
(define r760a::real)
(define r760b::real)
(define r761a::real)
(define r761b::real)
(define r762::real)
(define r763::real)
(define r764a::real)
(define r764b::real)
(define r765a::real)
(define r765b::real)
(define r766a::real)
(define r766b::real)
(define r767::real)
(define r768a::real)
(define r768b::real)
(define r769::real)
(define r770::real)
(define r771::real)
(define r772::real)
(define r773::real)
(define r774::real)
(define r775::real)
(define r776::real)
(define r777::real)
(define r778a::real)
(define r778b::real)
(define r779::real)
(define r780::real)
(define r781::real)
(define r782::real)
(define r783::real)
(define r784::real)
(define r785a::real)
(define r785b::real)
(define r786::real)
(define r787::real)
(define r788::real)
(define r789::real)
(define r790a::real)
(define r790b::real)
(define r791::real)
(define r792::real)
(define r793::real)
(define r794::real)
(define r795::real)
(define r796::real)
(define r797::real)
(define r798a::real)
(define r798b::real)
(define r799a::real)
(define r799b::real)
(define r800a::real)
(define r800b::real)
(define r801a::real)
(define r801b::real)
(define r802a::real)
(define r802b::real)
(define r803::real)
(define r804::real)
(define r805::real)
(define r806::real)
(define r807a::real)
(define r807b::real)
(define r808::real)
(define r809a::real)
(define r809b::real)
(define r810::real)
(define r811::real)
(define r812::real)
(define r813::real)
(define r814::real)
(define r815::real)
(define r816::real)
(define r817a::real)
(define r817b::real)
(define r818::real)
(define r819a::real)
(define r819b::real)
(define r820::real)
(define r821::real)
(define r822::real)
(define r823::real)
(define r824a::real)
(define r824b::real)
(define r825::real)
(define r826::real)
(define r827::real)
(define r828::real)
(define r829a::real)
(define r829b::real)
(define r830::real)
(define r831::real)
(define r832::real)
(define r833::real)
(define r834a::real)
(define r834b::real)
(define r835::real)
(define r836::real)
(define r837a::real)
(define r837b::real)
(define r838::real)
(define r839a::real)
(define r839b::real)
(define r840::real)
(define r841::real)
(define r842::real)
(define r843::real)
(define r844::real)
(define r845::real)
(define r846::real)
(define r847a::real)
(define r847b::real)
(define r848::real)
(define r849a::real)
(define r849b::real)
(define r850::real)
(define r851::real)
(define r852::real)
(define r853a::real)
(define r853b::real)
(define r854::real)
(define r855::real)
(define r856a::real)
(define r856b::real)
(define r857a::real)
(define r857b::real)
(define r858::real)
(define r859a::real)
(define r859b::real)
(define r860a::real)
(define r860b::real)
(define r861::real)
(define r862::real)
(define r863::real)
(define r864::real)
(define r865::real)
(define r866::real)
(define r867::real)
(define r870::real)
(define r871::real)
(define r872::real)
(define r873a::real)
(define r873b::real)
(define r874a::real)
(define r874b::real)
(define r875a::real)
(define r875b::real)
(define r876a::real)
(define r876b::real)
(define r877a::real)
(define r877b::real)
(define r878::real)
(define r879a::real)
(define r879b::real)
(define r880::real)
(define r881::real)
(define r882::real)
(define r883::real)
(define r884a::real)
(define r884b::real)
(define r885::real)
(define r886::real)
(define r887::real)
(define r888::real)
(define r889::real)
(define r890::real)
(define r891a::real)
(define r891b::real)
(define r892a::real)
(define r892b::real)
(define r893::real)
(define r894::real)
(define r895::real)
(define r896::real)
(define r897::real)
(define r898::real)
(define r899::real)
(define r900::real)
(define r901::real)
(define r902::real)
(define r903::real)
(define r904a::real)
(define r904b::real)
(define r905::real)
(define r906::real)
(define r907a::real)
(define r907b::real)
(define r908::real)
(define r909::real)
(define r910::real)
(define r911::real)
(define r912::real)
(define r913::real)
(define r914::real)
(define r915::real)
(define r916::real)
(define r917a::real)
(define r917b::real)


(assert 
  (and 
    (= (+ (- r566b) r566a (- r565) r423) 0)
    (= r315 0)
    (= (+ (- r798b) r798a) 0)
    (= (+ (- r891b) r891a r890 (- r544)) 0)
    (= (+ (- r859b) r859a) 0)
    (= (+ r916 (- r793)) 0)
    (= (+ r898) 0)
    (= (+ r86 (- r72)) 0)
    (= (+ r775 (- r620)) 0)
    (= (- r58) 0)
    (= (+ (- r896) r885 r884b (- r884a)) 0)
    (= (+ r604 (- r87)) 0)
    (= (+ r865) 0)
    (= (+ r861 r852 r798b (- r798a) (- r737b) r737a r663 (- r587) r408b (- r408a) (- r402) r198) 0)
    (= (+ r732 (- r722)) 0)
    (= (+ r847b (- r847a)) 0)
    (= (+ r864 (- r797) (- r346)) 0)
    (= (- r571) 0)
    (= (+ (- r273b) r273a) 0)
    (= (+ r752 r734 (- r583) r567b (- r567a) r559 (- r558) r457 (- r203b) r203a (- r202b) r202a r201) 0)
    (= (+ r324 r214b (- r214a)) 0)
    (= (+ r393 (- r390)) 0)
    (= (+ r227) 0)
    (= (+ r644b (- r644a) r442b (- r442a)) 0)
    (= (+ r406 (- r253)) 0)
    (= (+ (- r900) r507) 0)
    (= (+ r716 (- r532)) 0)
    (= (+ (- r788) r253) 0)
    (= (+ r377b (- r377a)) 0)
    (= (+ (- r493) (- r492b) r492a) 0)
    (= (+ (- r384) r236) 0)
    (= (+ (- r411)) 0)
    (= (+ r450 (- r449) (- r247)) 0)
    (= (+ r85b (- r85a)) 0)
    (= (+ r730 r532 r392b (- r392a)) 0)
    (= (+ (- r712) r710) 0)
    (= (+ r69) 0)
    (= (+ r913 r912 r909 (- r907b) r907a r906 r902 r890 r889 r881 (- r877b) r877a (- r876b) r876a (- r875b) r875a (- r873b) r873a r872 r871 r870 (- r829b) r829a (- r738b) r738a r733b (- r733a) r732 r731 r730 r726 r720 r653 r601 (* -2 r600b) (* +2 r600a) r599 r598 r597 r596 r595 r594 r593 r592 r591 r590 r589 r588 r499 r495 (- r494b) r494a r493 (- r492b) r492a (- r491b) r491a (- r490b) r490a (- r489b) r489a (- r488b) r488a (- r487b) r487a (- r476b) r476a r475 r473 r472 r471 r465 r459 r457 r455b (- r455a) r454 r453 r452 r451 r449 r448 r445 r444 r442b (- r442a) (- r240b) r240a r192 r185 r178 r171 r164 r157 r150 r143 r136) 0)
    (= (+ (- r813) r463) 0)
    (= (+ (- r917b) r917a r916 r915 (* +4 r914) r911 (* +2 r910) r908 r905 (- r904b) r904a r903 r900 r899 (- r898) r897 r896 r895 r894 r893 (- r892b) r892a r888 r887 r886 r885 (- r884b) r884a r883 r882 r880 (- r879b) r879a r878 (- r874b) r874a r756 (- r740b) r740a (* -2 r728b) (* +2 r728a) r708 r583 r582 r581 (- r580b) r580a r579 r578 r577 r576 r575 r574 r573 r572 r571 r570 (- r569b) r569a (* +2 r568) (- r567b) r567a (- r566b) r566a (- r565) (- r564b) r564a r563 r562 r561 (- r560) (- r558) r557 r556 r555 r554 r553 r552 r551 (- r550b) r550a r549 r548 r547 r546 (- r545) r544 r543 r542 r541 r540 r539 r538 r537 (- r536b) r536a r535 r534 r533 r532 r531 r530 r528 r527 r526 r525 r397 (- r200b) r200a (- r199b) r199a r198) 0)
    (= (+ r882 (- r589) r528) 0)
    (= (+ r633b (- r633a)) 0)
    (= (+ r902 (- r823)) 0)
    (= (+ r613b (- r613a)) 0)
    (= (+ r337b (- r337a)) 0)
    (= (+ r758 (- r497) (- r496)) 0)
    (= (+ r58) 0)
    (= (+ r840 (- r533)) 0)
    (= (+ (- r289b) r289a) 0)
    (= (+ r793 (- r772)) 0)
    (= (+ r374b (- r374a)) 0)
    (= (+ (- r704b) r704a) 0)
    (= (+ (- r611b) r611a) 0)
    (= (+ (- r895) r894) 0)
    (= (+ (- r902) r400) 0)
    (= (+ r385) 0)
    (= (+ r464b (- r464a)) 0)
    (= (+ r212b (- r212a)) 0)
    (= (+ r883 (- r241)) 0)
    (= (+ r194 r192 (- r191) r187 r185 (- r184) r180 r178 (- r177) r173 r171 (- r170) r166 r164 (- r163) r159 r157 (- r156) r152 r150 (- r149) r145 r143 (- r142) r138 r136 (- r135)) 0)
    (= (+ r128 r123 r118 r113 r108 r103 r98 r93 r88) 0)
    (= (+ (- r805) r780) 0)
    (= (+ (- r649) r513) 0)
    (= (+ (- r244) (- r243)) 0)
    (= (+ (- r786) r321) 0)
    (= (+ (- r713) r414) 0)
    (= (+ (- r336b) r336a) 0)
    (= (+ (- r917b) r917a (* -2 r314)) 0)
    (= (+ r699b (- r699a)) 0)
    (= (+ r805 (- r251)) 0)
    (= (+ (- r67)) 0)
    (= (+ r42_nutr_r r904b (- r904a) r776 r720 r719 r692 r690 (- r688b) r688a r626 r424 r419 (- r397) (- r316) (- r234)) 0)
    (= (+ r200b (- r200a) r199b (- r199a)) 0)
    (= (+ (- r765b) r765a r762) 0)
    (= (+ (- r812) r470) 0)
    (= (+ (- r82) r62) 0)
    (= (+ r329b (- r329a) r277b (- r277a)) 0)
    (= (+ (- r607b) r607a) 0)
    (= (+ (- r782) r238) 0)
    (= (+ (- r882)) 0)
    (= (+ (- r597)) 0)
    (= (+ r637 r290b (- r290a) (- r263)) 0)
    (= (+ (- r751) r689 r428b (- r428a) r416 (- r400)) 0)
    (= (+ r537 (- r56)) 0)
    (= (+ (- r757b) r757a) 0)
    (= (+ (- r858) (- r727) r695 r510) 0)
    (= (+ r132 (- r131) (- r130) r127 (- r126) (- r125) r122 (- r121) (- r120) r117 (- r116) (- r115) r112 (- r111) (- r110) r107 (- r106) (- r105) r102 (- r101) (- r100) r97 (- r96) (- r95) (- r91) (- r90)) 0)
    (= (+ r832) 0)
    (= (+ r863 (- r403)) 0)
    (= (+ (- r485) (* +2 r314)) 0)
    (= (+ (- r240b) r240a) 0)
    (= (+ (- r894) r892b (- r892a) r298) 0)
    (= (+ (- r791) r447) 0)
    (= (+ r917b (- r917a)) 0)
    (= (+ r514 (- r249)) 0)
    (= (+ (- r278b) r278a) 0)
    (= (+ r657 (- r436)) 0)
    (= (+ (- r331b) r331a) 0)
    (= (+ (- r698b) r698a) 0)
    (= (+ (- r471) (- r465)) 0)
    (= (+ r888 (- r887)) 0)
    (= (+ r372 r354b (- r354a) r353 r352 r350 r191 r184 r177 r170 r163 r156 r149 r142 r135) 0)
    (= (+ (- r904b) r904a (- r724b) r724a (- r692) (- r396) (- r395)) 0)
    (= (+ r76) 0)
    (= (+ r700b (- r700a)) 0)
    (= (+ (* +2 r351) (* +2 r79)) 0)
    (= (+ (- r897) r835 (- r747)) 0)
    (= (+ (- r895) r836) 0)
    (= (+ r815 (- r794)) 0)
    (= (+ r746 (- r711)) 0)
    (= (+ r223) 0)
    (= (+ r372 (- r370) (- r214b) r214a) 0)
    (= (+ (- r846) r305) 0)
    (= (+ r84 (- r74)) 0)
    (= (+ (- r725) r720) 0)
    (= (+ (- r819b) r819a) 0)
    (= (+ r207) 0)
    (= (+ r905 (- r397) (- r396)) 0)
    (= (+ (- r808) r350) 0)
    (= (+ r282) 0)
    (= (+ (- r765b) r765a r762 (- r586)) 0)
    (= (+ r688b (- r688a)) 0)
    (= (+ r201) 0)
    (= (+ r891b (- r891a) (- r890) r517b (- r517a) (- r501b) r501a) 0)
    (= (+ (* -2 r885) (- r834b) r834a (- r674b) r674a (- r245b) r245a r207) 0)
    (= (+ (- r594) r410) 0)
    (= (+ (- r850) r453) 0)
    (= (+ (- r743) r690) 0)
    (= (+ r624b (- r624a)) 0)
    (= (+ (- r640) r602b (- r602a) r446) 0)
    (= (+ (- r792) r612) 0)
    (= (+ (- r442b) r442a) 0)
    (= (+ (- r375b) r375a) 0)
    (= (+ r827 r481b (- r481a)) 0)
    (= (+ (- r769) r511) 0)
    (= (+ (- r535)) 0)
    (= (+ (- r80) r63) 0)
    (= (+ r351 r349 (- r348)) 0)
    (= (+ (- r612)) 0)
    (= (+ (- r708)) 0)
    (= (+ r405 (- r252) (- r218)) 0)
    (= (+ r548 r363 r362) 0)
    (= (+ r826 (- r618)) 0)
    (= (+ r489b (- r489a) (- r488b) r488a) 0)
    (= (+ r48_nutr_r r233) 0)
    (= (+ (- r838) r599) 0)
    (= (+ (- r658b) r658a (- r541) r242 r60) 0)
    (= (+ (- r704b) r704a r658b (- r658a)) 0)
    (= (+ r846 (- r742)) 0)
    (= (+ r273b (- r273a)) 0)
    (= (+ r701b (- r701a)) 0)
    (= (+ (- r335b) r335a) 0)
    (= (+ (- r764b) r764a (- r761b) r761a (- r560) r422) 0)
    (= (+ r607b (- r607a)) 0)
    (= (+ (- r721) (- r456b) r456a (- r448) (- r206b) r206a) 0)
    (= (+ (- r89) r77) 0)
    (= (+ (- r292b) r292a r291b (- r291a)) 0)
    (= (+ r46_nutr_r r714 (- r645b) r645a (- r540) (- r450)) 0)
    (= (+ r901 (- r741b) r741a r653 (- r584) r578 (- r577) r559 r529) 0)
    (= (+ (- r382)) 0)
    (= (+ (- r494b) r494a r487b (- r487a)) 0)
    (= (+ r891b (- r891a)) 0)
    (= (+ r563 (- r324)) 0)
    (= (+ (- r353) r317) 0)
    (= (+ r215) 0)
    (= (+ (- r688b) r688a) 0)
    (= (+ r737b (- r737a)) 0)
    (= (+ (- r806) r239) 0)
    (= (+ r285b (- r285a)) 0)
    (= (+ (- r92) r89) 0)
    (= (+ (- r308b) r308a) 0)
    (= (+ (- r731) r719) 0)
    (= (+ r415b (- r415a) r378b (- r378a)) 0)
    (= (+ (- r865)) 0)
    (= (+ r390 (- r345)) 0)
    (= (+ (- r245b) r245a) 0)
    (= (+ r844 r583 (- r582) (- r567b) r567a (- r439b) r439a (- r438b) r438a r437) 0)
    (= (+ (- r614b) r614a) 0)
    (= (+ r72) 0)
    (= (+ r302b (- r302a)) 0)
    (= (+ (- r54_secrt_r) (- r900) r807b (- r807a) r797 (- r785b) r785a (* +4 r759) r758 (* -4 r757b) (* +4 r757a) r756 (- r755b) r755a r754 (- r753b) r753a r752 r751 r750 r749 r748 r747 r746 r745 r713 r694 r471 r454 r411 r407 r406 r405 r403 (* +2 r351) (* +2 r349) r346 (- r343b) r343a r327 r317 r316 (- r306b) r306a r304 (- r293b) r293a (- r291b) r291a (- r283b) r283a r269 r268 (- r266b) r266a r265 r235 r234 r232 r231 r218 r217 r216 r213 r128 r123 r118 r113 r108 r103 r98 r93 r88 r77) 0)
    (= (+ (- r893) r867) 0)
    (= (+ (- r705) r520) 0)
    (= (+ r622b (- r622a)) 0)
    (= (+ r726) 0)
    (= (+ (- r730) r718 r576) 0)
    (= (+ (- r646b) r646a (- r538) r456b (- r456a) r206b (- r206a)) 0)
    (= (+ (- r513) r270) 0)
    (= (+ (- r420) r248) 0)
    (= (+ (- r467) (- r466) r380) 0)
    (= (+ (- r517b) r517a r501b (- r501a)) 0)
    (= (+ r224 (- r222)) 0)
    (= (+ (- r716)) 0)
    (= (+ (- r723) r395) 0)
    (= (+ r344b (- r344a)) 0)
    (= (+ (- r777) r551) 0)
    (= (+ (- r862)) 0)
    (= (+ (- r518b) r518a r508 (- r342) (- r341)) 0)
    (= (+ (- r802b) r802a r276b (- r276a)) 0)
    (= (+ (- r554) r437) 0)
    (= (+ r58) 0)
    (= (+ (- r63)) 0)
    (= (+ r772 r742 (- r609)) 0)
    (= (+ (- r745) r465) 0)
    (= (+ r332b (- r332a) r279b (- r279a)) 0)
    (= (+ (- r861) r460 r458 (- r456b) r456a r450 (- r443b) r443a) 0)
    (= (+ r917b (- r917a) (- r916) (- r915) (* -4 r914) (- r913) (- r912) (- r911) (* -2 r910) (- r909) (- r908) r907b (- r907a) (- r906) (- r905) r904b (- r904a) (- r903) (- r902) (- r900) (- r899) r898 (- r897) (- r896) (- r895) (- r894) (- r893) r892b (- r892a) (- r890) (- r888) (- r887) (- r886) (- r885) r884b (- r884a) (- r883) (- r882) (- r881) (- r880) r879b (- r879a) (- r878) r877b (- r877a) r876b (- r876a) r875b (- r875a) r874b (- r874a) r873b (- r873a) (- r872) (- r871) (- r870) r829b (- r829a) (- r756) r740b (- r740a) (- r708) (- r605) (- r604) (- r601) (- r599) (- r597) (- r596) (- r595) (- r593) (- r592) (- r587) (- r586) (- r585) (- r584) (- r583) (- r582) (- r581) r580b (- r580a) (- r579) (- r578) (- r577) (- r576) (- r575) (- r574) (- r573) (- r572) (- r571) (- r570) r569b (- r569a) (- r568) r567b (- r567a) r566b (- r566a) r565 r564b (- r564a) (- r563) (- r562) (- r561) r560 r558 (- r557) (- r556) (- r555) (- r554) (- r553) (- r552) (- r551) r550b (- r550a) (- r549) (- r548) (- r547) (- r546) r545 (- r544) (- r543) (- r542) (- r541) (- r540) (- r539) (- r538) (- r537) r536b (- r536a) (- r535) (- r534) (- r533) (- r532) (- r531) (- r530) (- r528) (- r527) (- r526) (- r525) (- r495) (- r485) (- r469) (- r468) (- r455b) r455a (- r445) (- r397) r200b (- r200a) r199b (- r199a) (- r198) (- r192) (- r185) (- r178) (- r171) (- r164) (- r157) (- r150) (- r143) (- r136)) 0)
    (= (+ (- r464b) r464a) 0)
    (= (+ r827 r820 r479b (- r479a) (- r419) (- r406)) 0)
    (= (+ r795 (- r763)) 0)
    (= (+ (- r876b) r876a) 0)
    (= (+ (- r498b) r498a) 0)
    (= (+ (- r873b) r873a) 0)
    (= (+ r734 (- r437)) 0)
    (= (+ r547 (- r362)) 0)
    (= (+ r497) 0)
    (= (+ r284b (- r284a)) 0)
    (= (+ r854 (- r809b) r809a (- r764b) r764a r763 (- r760b) r760a (- r409) (- r407) r404 r402 r334b (- r334a) r323b (- r323a) r239) 0)
    (= (+ r87) 0)
    (= (+ r872 (- r433) (- r423) r420 r419 (- r354b) r354a) 0)
    (= (+ (- r826) r360) 0)
    (= (+ r369b (- r369a)) 0)
    (= (+ r768b (- r768a)) 0)
    (= (+ (- r866)) 0)
    (= (+ (- r208b) r208a (- r193) (- r186) (- r179) (- r172) (- r165) (- r158) (- r151) (- r144) (- r137)) 0)
    (= (+ (- r469)) 0)
    (= (+ (- r915) r870 r772 (- r609) (- r435) (- r434) (- r432) (- r429) (- r427b) r427a (- r426b) r426a (- r425b) r425a r424 (- r422) (- r421) r420 (- r417) r415b (- r415a) r413 (* +2 r412) (- r410) r327 (- r319b) r319a r194 r187 r180 r173 r166 r159 r152 r145 r138 r78 (- r77)) 0)
    (= (+ (* -2 r246b) (* +2 r246a)) 0)
    (= (+ (- r84) r66) 0)
    (= (+ (- r195) r193 r189 (- r188) r186 r182 (- r181) r179 r175 (- r174) r172 r168 (- r167) r165 r161 (- r160) r158 r154 (- r153) r151 r147 (- r146) r144 r140 (- r139) r137 r133) 0)
    (= (+ r850 (- r749)) 0)
    (= (+ r190 (- r189) r183 (- r182) r176 (- r175) r169 (- r168) r162 (- r161) r155 (- r154) r148 (- r147) r141 (- r140) r134 (- r133)) 0)
    (= (+ (- r801b) r801a r275b (- r275a)) 0)
    (= (+ (- r367b) r367a) 0)
    (= (+ (- r233)) 0)
    (= (+ (- r381) r310) 0)
    (= (+ (- r81) r67) 0)
    (= (+ r791 (- r509)) 0)
    (= (+ r884b (- r884a)) 0)
    (= (+ r491b (- r491a) (- r490b) r490a) 0)
    (= (+ r286b (- r286a)) 0)
    (= (+ (- r600b) r600a) 0)
    (= (+ r879b (- r879a)) 0)
    (= (+ r887 (- r826) r626 r618 r474b (- r474a) r431b (- r431a) (* +2 r379) (* -2 r301) (- r212b) r212a) 0)
    (= (+ (- r648)) 0)
    (= (+ r234) 0)
    (= (+ (- r696b) r696a) 0)
    (= (+ r295b (- r295a)) 0)
    (= (+ (- r78)) 0)
    (= (+ (- r391b) r391a) 0)
    (= (+ (- r830) r525) 0)
    (= (+ (- r604)) 0)
    (= (+ r911 (- r899)) 0)
    (= (+ (- r766b) r766a r325b (- r325a)) 0)
    (= (+ r839b (- r839a) r657 r550b (- r550a)) 0)
    (= (+ r766b (- r766a)) 0)
    (= (+ r621b (- r621a)) 0)
    (= (+ r642b (- r642a)) 0)
    (= (+ (- r427b) r427a) 0)
    (= (+ r92 (- r69)) 0)
    (= (+ (- r839b) r839a (- r534) r436) 0)
    (= (+ r802b (- r802a)) 0)
    (= (+ (- r613b) r613a (- r329b) r329a) 0)
    (= (+ (- r916) (- r915) (- r910) (- r908) (- r807b) r807a) 0)
    (= (+ r241) 0)
    (= (+ (- r623b) r623a) 0)
    (= (+ (- r875b) r875a r619b (- r619a)) 0)
    (= (+ r857b (- r857a) r564b (- r564a) (- r536b) r536a (- r334b) r334a (- r270)) 0)
    (= (+ (- r468)) 0)
    (= (+ (- r864) (- r863) r813 (- r771) (- r770) (- r511)) 0)
    (= (+ (- r913) (- r881) r595) 0)
    (= (+ r318b (- r318a)) 0)
    (= (+ (- r242)) 0)
    (= (+ (- r608) r498b (- r498a)) 0)
    (= (+ (- r739) r493 (- r441b) r441a) 0)
    (= (+ r893 (- r821)) 0)
    (= (+ r765b (- r765a)) 0)
    (= (+ (- r898) r724b (- r724a) r368 r365) 0)
    (= (+ r79) 0)
    (= (+ r446) 0)
    (= (+ r515 (- r320)) 0)
    (= (+ (- r128) (- r123) (- r118) (- r113) (- r108) (- r103) (- r98) (- r93) (- r88) (- r77)) 0)
    (= (+ (- r651b) r651a (- r460) r205b (- r205a)) 0)
    (= (+ r575 (- r574)) 0)
    (= (+ (- r602b) r602a) 0)
    (= (+ (- r650b) r650a (- r643b) r643a (- r642b) r642a (- r641b) r641a) 0)
    (= (+ (- r914) r485) 0)
    (= (+ r598) 0)
    (= (+ r810 (- r710)) 0)
    (= (+ r877b (- r877a)) 0)
    (= (+ r78 (- r76)) 0)
    (= (+ r648 (- r599)) 0)
    (= (+ (- r197b) r197a) 0)
    (= (+ r777 (- r695) r541 r242) 0)
    (= (+ (- r201)) 0)
    (= (+ r590 (- r462) (- r461)) 0)
    (= (+ (- r204b) r204a) 0)
    (= (+ r771 (- r465)) 0)
    (= (+ r195 (- r194) r188 (- r187) r181 (- r180) r174 (- r173) r167 (- r166) r160 (- r159) r153 (- r152) r146 (- r145) r139 (- r138)) 0)
    (= (+ r45_nutr_r (- r714) (- r634b) r634a r443b (- r443a)) 0)
    (= (+ (- r302b) r302a) 0)
    (= (+ (- r413) r297 (- r213)) 0)
    (= (+ r394 (- r250)) 0)
    (= (+ r797 (- r516b) r516a (- r512) r306b (- r306a)) 0)
    (= (+ (- r310) r229) 0)
    (= (+ r249 (- r216)) 0)
    (= (+ (- r889) r544) 0)
    (= (+ r803 (- r371)) 0)
    (= (+ (- r800b) r800a r274b (- r274a)) 0)
    (= (+ r230 (- r229)) 0)
    (= (+ (- r476b) r476a) 0)
    (= (+ r745 (- r230)) 0)
    (= (+ (- r408b) r408a) 0)
    (= (+ (- r337b) r337a) 0)
    (= (+ r381 (- r236)) 0)
    (= (+ (- r305) r304) 0)
    (= (+ r289b (- r289a)) 0)
    (= (+ (- r441b) r441a) 0)
    (= (+ (- r901) r741b (- r741a) (- r726) (- r720) (- r719) (* +2 r600b) (* -2 r600a) (- r589) (- r585) r577 (- r559) (- r529) r240b (- r240a)) 0)
    (= (+ r521 (- r340)) 0)
    (= (+ (- r502) r326) 0)
    (= (+ r498b (- r498a) (- r467) r429) 0)
    (= (+ (- r732) r455b (- r455a) r445) 0)
    (= (+ r383) 0)
    (= (+ r801b (- r801a)) 0)
    (= (+ (- r709) r399) 0)
    (= (+ r308b (- r308a)) 0)
    (= (+ r754 (- r596)) 0)
    (= (+ r494b (- r494a) r476b (- r476a) r472) 0)
    (= (+ (- r787) r252) 0)
    (= (+ (- r833) r345) 0)
    (= (+ (- r284b) r284a) 0)
    (= (+ (- r62)) 0)
    (= (+ r784 (- r773) r292b (- r292a) r266b (- r266a) (- r265)) 0)
    (= (+ (- r843) r552) 0)
    (= (+ (- r799b) r799a) 0)
    (= (+ (- r912) (- r906) r651b (- r651a) r459 r264) 0)
    (= (+ (- r903) (- r594) r582) 0)
    (= (+ (- r271b) r271a) 0)
    (= (+ r587 (- r459) (- r457) (- r455b) r455a (- r454) (- r453) (- r452) (- r451) (- r449) (- r448) (- r445) (- r444) (- r442b) r442a) 0)
    (= (+ r500 (- r298)) 0)
    (= (+ (- r60)) 0)
    (= (+ r717b (- r717a) (- r530) (- r529)) 0)
    (= (+ r246b (- r246a)) 0)
    (= (+ (- r664) r497 r496) 0)
    (= (+ r427b (- r427a) (- r276b) r276a) 0)
    (= (+ r828 (- r225) (- r224)) 0)
    (= (+ (- r552) r210 r209) 0)
    (= (+ (- r430)) 0)
    (= (+ (- r557)) 0)
    (= (+ r47_nutr_r (- r872) r566b (- r566a) r565) 0)
    (= (+ r687b (- r687a)) 0)
    (= (+ r811 (- r759) (- r393)) 0)
    (= (+ r473 (- r472)) 0)
    (= (+ r844 (- r480)) 0)
    (= (+ (- r376b) r376a) 0)
    (= (+ r536b (- r536a) (- r325b) r325a r294b (- r294a) r261b (- r261a)) 0)
    (= (+ r553 (- r463)) 0)
    (= (+ (- r778b) r778a r756 (- r755b) r755a r605 (- r545) (- r500) (- r480) (- r477) (- r470) r464b (- r464a) (- r463)) 0)
    (= (+ r620 (- r471)) 0)
    (= (+ r281) 0)
    (= (+ r507) 0)
    (= (+ r788 (- r504b) r504a (- r231)) 0)
    (= (+ (- r314) (- r311) r308b (- r308a)) 0)
    (= (+ (- r854) (- r766b) r766a (- r760b) r760a (- r484) r56) 0)
    (= (+ (- r59b) r59a (- r58) (* -2 r57) r56 r55) 0)
    (= (+ (- r736) r597) 0)
    (= (+ r638 (- r590)) 0)
    (= (+ (- r687b) r687a) 0)
    (= (+ r785b (- r785a)) 0)
    (= (+ (- r295b) r295a) 0)
    (= (+ r384 (* +2 r299b) (* -2 r299a)) 0)
    (= (+ r408b (- r408a)) 0)
    (= (+ (- r555)) 0)
    (= (+ (- r192) (- r185) (- r178) (- r171) (- r164) (- r157) (- r150) (- r143) (- r136)) 0)
    (= (+ (- r837b) r837a r799b (- r799a) (- r255b) r255a) 0)
    (= (+ (- r780) r432) 0)
    (= (+ (- r215)) 0)
    (= (+ r787 (- r506b) r506a (- r432) (- r394) (- r317)) 0)
    (= (+ (- r702b) r702a) 0)
    (= (+ (- r539) (- r418) (- r417)) 0)
    (= (+ r830) 0)
    (= (+ r707) 0)
    (= (+ r698b (- r698a)) 0)
    (= (+ r800b (- r800a)) 0)
    (= (+ r915) 0)
    (= (+ (- r752) r451) 0)
    (= (+ (- r228)) 0)
    (= (+ (- r378b) r378a r343b (- r343a)) 0)
    (= (+ r640 (- r603)) 0)
    (= (+ r782 (- r774)) 0)
    (= (+ r490b (- r490a) (- r489b) r489a) 0)
    (= (+ r796 (* -4 r483)) 0)
    (= (+ r625) 0)
    (= (+ r354b (- r354a)) 0)
    (= (+ (- r576)) 0)
    (= (+ (- r425b) r425a) 0)
    (= (+ r704b (- r704a)) 0)
    (= (+ (- r520) r430) 0)
    (= (+ r874b (- r874a) (- r871) r794) 0)
    (= (+ r889 r830 (- r570) r530 r529 r462 r461) 0)
    (= (+ r221) 0)
    (= (+ r263 (- r262)) 0)
    (= (+ (- r908) r899) 0)
    (= (+ (- r415b) r415a (- r343b) r343a) 0)
    (= (+ r75) 0)
    (= (+ r831 r476b (- r476a)) 0)
    (= (+ (- r853b) r853a (- r849b) r849a r761b (- r761a) r727 r635 (- r526) (- r510) r409 r404) 0)
    (= (+ r401b (- r401a)) 0)
    (= (+ r773 (- r768b) r768a (- r435)) 0)
    (= (+ r897 (- r896) (- r892b) r892a) 0)
    (= (+ (- r68b) r68a) 0)
    (= (+ r271b (- r271a)) 0)
    (= (+ (- r626)) 0)
    (= (+ (- r832)) 0)
    (= (+ (- r549) r486 (- r369b) r369a) 0)
    (= (+ (- r734) (- r437)) 0)
    (= (+ r738b (- r738a) r652b (- r652a) r573) 0)
    (= (+ r860b (- r860a) (- r593) (- r591) r440 (- r220)) 0)
    (= (+ r245b (- r245a)) 0)
    (= (+ r59b (- r59a) r58 (* +2 r57) (- r56) (- r55)) 0)
    (= (+ (- r524) r216) 0)
    (= (+ (- r207)) 0)
    (= (+ r481b (- r481a) (- r466) r417) 0)
    (= (+ (- r482) (- r479b) r479a r418) 0)
    (= (+ r546 r524 (- r363)) 0)
    (= (+ (- r761b) r761a (- r470) r409 (- r404) (- r322) r311) 0)
    (= (+ r647b (- r647a)) 0)
    (= (+ r603 r469) 0)
    (= (+ (- r446) r311) 0)
    (= (+ r841 (- r257)) 0)
    (= (+ (- r287b) r287a) 0)
    (= (+ (- r83) r65) 0)
    (= (+ (- r591) r574) 0)
    (= (+ (- r294b) r294a) 0)
    (= (+ (- r817b) r817a) 0)
    (= (+ r225 (- r223)) 0)
    (= (+ (- r856b) r856a) 0)
    (= (+ r623b (- r623a)) 0)
    (= (+ (- r652b) r652a) 0)
    (= (+ r713 (- r521) (- r428b) r428a) 0)
    (= (+ (- r916) r352) 0)
    (= (+ (- r226)) 0)
    (= (+ r721 r460 (- r459) (- r315) r247 (- r205b) r205a) 0)
    (= (+ (- r632b) r632a) 0)
    (= (+ r728b (- r728a)) 0)
    (= (+ r832 (- r313)) 0)
    (= (+ (- r855) r494b (- r494a) (- r493) r492b (- r492a) r491b (- r491a) r490b (- r490a) r489b (- r489a) r488b (- r488a) r487b (- r487a) (- r473) (- r472)) 0)
    (= (+ (- r906) (- r881) (- r880) r827 r825 r820 (- r819b) r819a r818 (- r817b) r817a r816 r727 r725 r721 r718 (- r717b) r717a r716 r715 r714 (* +2 r713) r711 (- r696b) r696a r694 r693 r691 (* +4 r483) r479b (- r479a) r362 r360 r359 (- r358) r356 r355 r235 (- r233)) 0)
    (= (+ (- r497) r496) 0)
    (= (+ r220) 0)
    (= (+ (- r878) r877b (- r877a) r876b (- r876a) r875b (- r875a) r874b (- r874a) r873b (- r873a) (- r872) (- r871) (- r870) r625 (- r624b) r624a (- r623b) r623a (- r622b) r622a (- r621b) r621a r620 (- r619b) r619a r531 r435 r434 r433 r432 r430 r429 (- r428b) r428a r427b (- r427a) r426b (- r426a) r425b (- r425a) (- r424) r423 r422 r421 (- r420) (- r419) r418 r417 (- r415b) r415a r414 (- r413) (- r412) r411 r410 (- r327) r319b (- r319a) (- r317) (- r232) (- r231) (- r194) (- r192) (- r187) (- r185) (- r180) (- r178) (- r173) (- r171) (- r166) (- r164) (- r159) (- r157) (- r152) (- r150) (- r145) (- r143) (- r138) (- r136) (- r78) r77) 0)
    (= (+ (- r883) r751 r694 (- r515) (- r496)) 0)
    (= (+ r711 (- r694)) 0)
    (= (+ r313) 0)
    (= (+ r664) 0)
    (= (+ r664 r663 r662 (- r444) (- r443b) r443a) 0)
    (= (+ r804 (- r238)) 0)
    (= (+ r731 (- r729)) 0)
    (= (+ r712) 0)
    (= (+ r50_nutr_r (- r717b) r717a (- r559) r558 (- r458)) 0)
    (= (+ (- r657) r440 (- r436)) 0)
    (= (+ r471 (- r383)) 0)
    (= (+ r650b (- r650a)) 0)
    (= (+ (- r306b) r306a) 0)
    (= (+ r523 (- r522) r346 (- r304)) 0)
    (= (+ r596 (- r531)) 0)
    (= (+ r892b (- r892a)) 0)
    (= (+ r191 r184 r177 r170 r163 r156 r149 r142 r135) 0)
    (= (+ r866 r196b (- r196a)) 0)
    (= (+ r197b (- r197a)) 0)
    (= (+ (- r911) r397 r396) 0)
    (= (+ r828 r825 r466 r388b (- r388a) r387b (- r387a) (- r386) (- r385)) 0)
    (= (+ r606b (- r606a)) 0)
    (= (+ (- r784) r783) 0)
    (= (+ (- r352) r232) 0)
    (= (+ r80 (- r71)) 0)
    (= (+ (- r547)) 0)
    (= (+ r609 (- r412) r255b (- r255a)) 0)
    (= (+ (- r440) r436) 0)
    (= (+ (- r282) (- r281) r218) 0)
    (= (+ r328b (- r328a)) 0)
    (= (+ r735 (- r653) r584) 0)
    (= (+ (- r451) (- r347b) r347a) 0)
    (= (+ (- r333b) r333a) 0)
    (= (+ r904b (- r904a) r692 (- r398) r396 r395 r394 r386 r382 r366 (- r235) (- r219)) 0)
    (= (+ (- r546)) 0)
    (= (+ r257) 0)
    (= (+ (- r756) r755b (- r755a) r753b (- r753a) (- r503b) r503a (- r434) (- r433) (- r267b) r267a) 0)
    (= (+ (- r277b) r277a) 0)
    (= (+ r222 (- r221)) 0)
    (= (+ r44_nutr_r r777 r618 r256) 0)
    (= (+ (- r360) r213) 0)
    (= (+ r859b (- r859a)) 0)
    (= (+ (- r825) r482) 0)
    (= (+ (- r829b) r829a) 0)
    (= (+ (- r847b) r847a) 0)
    (= (+ r376b (- r376a)) 0)
    (= (+ (- r803) r309) 0)
    (= (+ r336b (- r336a)) 0)
    (= (+ r770 r743 (- r453) (- r377b) r377a) 0)
    (= (+ (- r581) r556 r499) 0)
    (= (+ r781) 0)
    (= (+ r272 (- r237)) 0)
    (= (+ r808 (- r248)) 0)
    (= (+ r702b (- r702a)) 0)
    (= (+ r914 (- r882) r879b (- r879a)) 0)
    (= (+ (- r507) r411) 0)
    (= (+ (- r718) r572) 0)
    (= (+ (- r65)) 0)
    (= (+ r769 (- r475)) 0)
    (= (+ (- r699b) r699a) 0)
    (= (+ r908 (- r867)) 0)
    (= (+ r848 (- r477)) 0)
    (= (+ r492b (- r492a) (- r491b) r491a) 0)
    (= (+ r363 r362 r361 r360 (* +3 r348) (- r347b) r347a r312 r303b (- r303a) r302b (- r302a) (- r301) (* -2 r300) r241) 0)
    (= (+ (- r841) r789) 0)
    (= (+ (- r595) r454 (- r446)) 0)
    (= (+ (- r814) r539) 0)
    (= (+ r709 r347b (- r347a)) 0)
    (= (+ r251 (- r217)) 0)
    (= (+ r608 (- r606b) r606a) 0)
    (= (+ r878 (- r430) r428b (- r428a) (- r418) (- r414)) 0)
    (= (+ (- r857b) r857a r778b (- r778a)) 0)
    (= (+ r391b (- r391a)) 0)
    (= (+ (- r804) r433) 0)
    (= (+ r208b (- r208a)) 0)
    (= (+ r862 (* -2 r796)) 0)
    (= (+ (- r598) r480) 0)
    (= (+ (- r132) r129 (- r127) r124 (- r122) r119 (- r117) r114 (- r112) r109 (- r107) r104 (- r102) r99 (- r97) r94) 0)
    (= (+ r204b (- r204a)) 0)
    (= (+ r759 (- r351) (- r349)) 0)
    (= (+ r858 (- r410)) 0)
    (= (+ r907b (- r907a) (- r401b) r401a) 0)
    (= (+ r244) 0)
    (= (+ (* -4 r917b) (* +4 r917a) (* +2 r916) (* +2 r915) (* +8 r914) (* +2 r913) (* +3 r912) (* +2 r911) (* +4 r910) (* +2 r909) (* +3 r908) (* -2 r907b) (* +2 r907a) (* +2 r906) (* +2 r905) r904b (- r904a) (* +3 r903) (* +2 r902) (* +2 r901) (* +4 r900) (* +2 r899) r898 (* +2 r897) (* +2 r896) (* +2 r895) (* +2 r894) (* +2 r893) (* -2 r892b) (* +2 r892a) (- r891b) r891a (* +2 r890) r889 (* +2 r888) (* +2 r887) r886 (* +2 r885) (* -2 r884b) (* +2 r884a) (* +2 r883) (* +2 r882) r881 r880 (* -2 r879b) (* +2 r879a) r878 (- r877b) r877a (- r876b) r876a (- r875b) r875a (- r874b) r874a (- r873b) r873a r872 r871 r870 r857b (- r857a) r855 (- r851) r844 (* -6 r833) (- r832) (* +2 r831) (- r829b) r829a r827 r825 r820 (- r819b) r819a r818 (- r817b) r817a r816 r815 r810 (- r807b) r807a (- r797) r796 r786 (- r778b) r778a r776 (- r775) r770 r769 (* -4 r759) (- r758) (* -4 r757b) (* +4 r757a) r756 r755b (- r755a) (- r754) r753b (- r753a) (- r752) (- r751) (- r750) (- r749) (- r748) (- r747) (- r746) (- r745) r743 r742 (- r741b) r741a (* -2 r740b) (* +2 r740a) r739 (- r738b) r738a (* -2 r737b) (* +2 r737a) (- r736) r735 (* +2 r734) (- r733b) r733a (* +2 r732) (* +2 r731) r730 (* -2 r728b) (* +2 r728a) r727 (- r724b) r724a (* +2 r720) r711 (- r710) (- r709) (* +2 r708) (- r696b) r696a (- r694) r693 (* +3 r692) r691 (* +3 r690) (- r688b) r688a (- r658b) r658a (- r652b) r652a (- r632b) r632a r626 r625 (- r624b) r624a (- r623b) r623a (- r622b) r622a (- r621b) r621a r620 (- r619b) r619a r618 (- r614b) r614a (- r613b) r613a r612 (- r611b) r611a r610 (* +2 r608) (* -2 r607b) (* +2 r607a) (- r606b) r606a (* +3 r605) r604 r603 r602b (- r602a) (- r594) (- r591) (- r589) (- r588) (* +2 r587) (* +2 r586) (* +2 r585) (* +2 r584) r583 r582 r581 (- r580b) r580a r579 r578 r577 r576 r575 r574 r573 r572 r570 (- r569b) r569a r568 (- r567b) r567a (- r566b) r566a (- r565) (- r564b) r564a r563 r562 r561 (- r560) r559 (* -2 r558) (* +2 r557) (* +2 r556) (* +2 r555) (* +2 r554) (* +2 r553) (* +2 r552) (* +2 r551) (* -2 r550b) (* +2 r550a) (* +2 r549) (* +2 r548) (* +2 r547) (* +2 r546) (* -2 r545) (* +2 r544) (* +2 r543) (* +2 r542) (* +2 r541) (* +2 r540) (* +2 r539) (* +2 r538) (* +2 r537) (* -3 r536b) (* +3 r536a) (* +2 r535) (* +2 r534) (* +2 r533) (* +2 r532) (* +2 r531) (* +2 r530) r529 (* +2 r528) (* +2 r527) (* +2 r526) (* +2 r525) r524 r504b (- r504a) (- r499) (- r498b) r498a r497 r496 r495 (- r494b) r494a r493 (- r492b) r492a (- r491b) r491a (- r490b) r490a (- r489b) r489a (- r488b) r488a (- r487b) r487a (- r486) r485 (* +4 r483) r482 (- r481b) r481a (* +2 r479b) (* -2 r479a) r478 (* +2 r476b) (* -2 r476a) (- r474b) r474a r473 r472 (- r471) r469 r468 r467 r466 r464b (- r464a) r462 r461 (* -2 r454) (* +2 r447) r446 (- r442b) r442a r441b (- r441a) (- r439b) r439a (- r438b) r438a r437 r435 r434 r433 r432 (- r428b) r428a r421 r414 (- r413) (- r411) r410 (- r407) (- r406) (- r405) (* -2 r403) r400 r399 (* -2 r398) (* +2 r397) (* +3 r396) (* +2 r395) (* +2 r394) r393 (- r392b) r392a r391b (- r391a) (- r389b) r389a (- r388b) r388a (- r387b) r387a (* +2 r386) (* +2 r384) r383 r382 r381 (* -5 r380) (- r379) (- r378b) r378a (* +2 r377b) (* -2 r377a) (* -3 r376b) (* +3 r376a) (* -2 r375b) (* +2 r375a) (* +3 r374b) (* -3 r374a) (- r371) r370 (* -2 r369b) (* +2 r369a) (- r367b) r367a (- r364b) r364a r362 r361 r360 (* +2 r359) (* -2 r358) (- r357) (* +2 r356) (* +2 r355) (- r354b) r354a (- r353) (- r352) (- r350) (* -2 r349) (* +2 r345) (- r344b) r344a r343b (- r343a) (* +2 r342) (* +2 r341) (* +2 r340) (* -2 r339b) (* +2 r339a) (* +2 r338) (* -2 r337b) (* +2 r337a) (* -2 r336b) (* +2 r336a) (* -2 r335b) (* +2 r335a) (* -2 r334b) (* +2 r334a) (* -2 r333b) (* +2 r333a) (- r332b) r332a (* -2 r331b) (* +2 r331a) (* -2 r330b) (* +2 r330a) (* -2 r329b) (* +2 r329a) (* -2 r328b) (* +2 r328a) (- r326) (- r325b) r325a (- r324) (- r323b) r323a (* +2 r322) (- r321) (* +2 r320) (- r319b) r319a (* -2 r318b) (* +2 r318a) r315 (* +3 r314) r313 (* -2 r312) (* -4 r310) (* -2 r308b) (* +2 r308a) (* -2 r307) r305 (- r298) (* +2 r297) (- r296) r295b (- r295a) (* -2 r294b) (* +2 r294a) (- r292b) r292a (* +2 r291b) (* -2 r291a) (* -3 r290b) (* +3 r290a) r289b (- r289a) r288b (- r288a) r287b (- r287a) r286b (- r286a) r285b (- r285a) (- r284b) r284a (- r282) (- r281) (- r280b) r280a r279b (- r279a) r278b (- r278a) r277b (- r277a) (- r276b) r276a (- r275b) r275a (- r274b) r274a (* -4 r273b) (* +4 r273a) (- r272) (- r271b) r271a r270 (- r267b) r267a r264 r263 (* +2 r262) (* -2 r261b) (* +2 r261a) r260 r259 (- r258) (- r257) (- r256) r255b (- r255a) (- r254b) r254a (- r253) (- r252) r251 (- r250) (* +2 r249) r248 (* +2 r247) r246b (- r246a) r240b (- r240a) (- r236) (- r235) (- r234) (* -2 r230) r229 r227 r226 (* -2 r219) r218 (- r217) (* -2 r216) (* -2 r215) (- r214b) r214a (* -2 r213) (* +2 r198) (- r197b) r197a (- r130) (- r129) (- r125) (- r124) (- r120) (- r119) (- r115) (- r114) (- r110) (- r109) (- r105) (- r104) (- r100) (- r99) (- r95) (- r94) (- r90) (- r89) r87 r76 (- r75) (- r74) (- r73) (- r72) (- r71) (- r70) (- r69) (- r68b) r68a (- r67) (- r66) (- r65) (- r64) (- r63) (- r62) (* -4 r57) (- r55)) 0)
    (= (+ (- r385)) 0)
    (= (+ r901 (- r822)) 0)
    (= (+ (- r332b) r332a) 0)
    (= (+ (* -2 r79)) 0)
    (= (+ r821 r447 (- r395)) 0)
    (= (+ r333b (- r333a) (- r280b) r280a) 0)
    (= (+ (- r901) r723 r645b (- r645a) r540 r449 (- r264)) 0)
    (= (+ (- r852) (- r848) (- r842) (- r776) (- r293b) r293a (- r283b) r283a) 0)
    (= (+ r786) 0)
    (= (+ (- r879b) r879a (- r528) r468) 0)
    (= (+ r571) 0)
    (= (+ (- r519b) r519a (- r261b) r261a) 0)
    (= (+ r555 (- r499)) 0)
    (= (+ r845) 0)
    (= (+ (- r897) r895) 0)
    (= (+ r562 (- r321)) 0)
    (= (+ r767 (- r338) r319b (- r319a) (- r308b) r308a (- r303b) r303a (- r254b) r254a) 0)
    (= (+ r81 (- r75)) 0)
    (= (+ r736 r240b (- r240a)) 0)
    (= (+ r322 (- r259)) 0)
    (= (+ r43_nutr_r r825 r816 r815 (- r786) r774 r771 r770 r769 (- r768b) r768a r763 (- r753b) r753a (- r606b) r606a (- r605) r545 r519b (- r519a) r518b (- r518a) (- r501b) r501a (- r424) (- r407) (- r406) (* -2 r405) r355 r343b (- r343a) (- r327) r269 r268 (- r256)) 0)
    (= (+ (- r588) r258) 0)
    (= (+ r83 (- r73)) 0)
    (= (+ r614b (- r614a)) 0)
    (= (+ (- r227)) 0)
    (= (+ (- r622b) r622a) 0)
    (= (+ r228) 0)
    (= (+ (- r66)) 0)
    (= (+ (- r736)) 0)
    (= (+ (- r735) r585) 0)
    (= (+ (- r601)) 0)
    (= (+ r910 r401b (- r401a) (- r400) (- r399)) 0)
    (= (+ (- r53_secrt_r) (- r870) r832 r707 r695 r689 (- r687b) r687a r609 r560 (- r498b) r498a (- r481b) r481a r467 r466 r338) 0)
    (= (+ r339b (- r339a)) 0)
    (= (+ (- r824b) r824a) 0)
    (= (+ r581) 0)
    (= (+ r779 (- r296)) 0)
    (= (+ r725 (- r272)) 0)
    (= (+ (- r828) r662) 0)
    (= (+ r131 r130 (- r128) r126 r125 (- r123) r121 r120 (- r118) r116 r115 (- r113) r111 r110 (- r108) r106 r105 (- r103) r101 r100 (- r98) r96 r95 (- r93) r91 r90 (- r88)) 0)
    (= (+ r431b (- r431a)) 0)
    (= (+ (- r474b) r474a) 0)
    (= (+ r570 r569b (- r569a)) 0)
    (= (+ (- r221)) 0)
    (= (+ r330b (- r330a) r278b (- r278a)) 0)
    (= (+ r331b (- r331a) r288b (- r288a)) 0)
    (= (+ r241) 0)
    (= (+ r561 (- r326)) 0)
    (= (+ r38_nutr_r (- r844) r594 (- r500) r439b (- r439a) r438b (- r438a)) 0)
    (= (+ (- r815) r403) 0)
    (= (+ (- r288b) r288a) 0)
    (= (+ r697b (- r697a)) 0)
    (= (+ (- r811) r483) 0)
    (= (+ r441b (- r441a)) 0)
    (= (+ r611b (- r611a)) 0)
    (= (+ r696b (- r696a)) 0)
    (= (+ r641b (- r641a)) 0)
    (= (+ r353) 0)
    (= (+ (- r647b) r647a r303b (- r303a) r254b (- r254a)) 0)
    (= (+ r601 (- r527)) 0)
    (= (+ r441b (- r441a) (- r438b) r438a) 0)
    (= (+ r593) 0)
    (= (+ r632b (- r632a)) 0)
    (= (+ (- r608) r606b (- r606a)) 0)
    (= (+ r917b (- r917a)) 0)
    (= (+ r74) 0)
    (= (+ (- r431b) r431a) 0)
    (= (+ (- r548)) 0)
    (= (+ (- r389b) r389a) 0)
    (= (+ r636b (- r636a)) 0)
    (= (+ r579 (- r499)) 0)
    (= (+ r488b (- r488a) (- r487b) r487a) 0)
    (= (+ (- r624b) r624a) 0)
    (= (+ r438b (- r438a) (- r203b) r203a) 0)
    (= (+ (- r700b) r700a) 0)
    (= (+ (- r689) r502 (- r416)) 0)
    (= (+ (- r344b) r344a) 0)
    (= (+ r739 r203b (- r203a) r202b (- r202a) (- r201)) 0)
    (= (+ r792 (- r781)) 0)
    (= (+ r311) 0)
    (= (+ (- r610) r260) 0)
    (= (+ (- r279b) r279a) 0)
    (= (+ (- r409) (- r408b) r408a r402) 0)
    (= (+ r757b (- r757a)) 0)
    (= (+ r833) 0)
    (= (+ (- r219) (- r212b) r212a) 0)
    (= (+ r913 r912 r909 (- r907b) r907a r906 r902 r890 r881 (- r877b) r877a (- r876b) r876a (- r875b) r875a (- r873b) r873a r872 r871 r870 r822 (- r737b) r737a r736 (- r663) r634b (- r634a) (- r633b) r633a r605 r604 r587 r586 r585 r584 (- r568) r444 r192 r185 r178 r171 r164 r157 r150 r143 r136) 0)
    (= (+ (- r907b) r907a r824b (- r824a)) 0)
    (= (+ (- r379) r301) 0)
    (= (+ (- r484) (- r364b) r364a r361) 0)
    (= (+ (- r874b) r874a r871 (- r775)) 0)
    (= (+ (- r706) r340) 0)
    (= (+ r71) 0)
    (= (+ (- r592) r549 r314 (- r308b) r308a) 0)
    (= (+ r439b (- r439a) (- r202b) r202a) 0)
    (= (+ r367b (- r367a)) 0)
    (= (+ r748 r703 r518b (- r518a) (- r508) r320 (- r318b) r318a) 0)
    (= (+ r900) 0)
    (= (+ r426b (- r426a) (- r275b) r275a) 0)
    (= (+ (- r644b) r644a) 0)
    (= (+ (- r339b) r339a) 0)
    (= (+ (- r564b) r564a (- r323b) r323a) 0)
    (= (+ (- r543)) 0)
    (= (+ (- r52_secrt_r) r917b (- r917a) (* -4 r914) (- r913) (- r912) (- r911) (- r910) (- r909) (- r903) (- r844) (- r827) (- r825) (- r814) r811 (- r810) (- r809b) r809a (- r808) r807b (- r807a) r806 (- r805) r804 r803 r802b (- r802a) r801b (- r801a) r800b (- r800a) (- r799b) r799a (- r798b) r798a r797 (* +2 r796) r795 r794 (- r793) r792 r791 (- r790b) r790a r789 r788 r787 (* +2 r786) (- r785b) r785a (- r784) r783 (- r782) r781 r780 r779 (- r778b) r778a (- r777) r775 (- r764b) r764a (- r761b) r761a (- r755b) r755a r749 r744b (- r744a) (- r743) (- r742) r741b (- r741a) r740b (- r740a) (- r739) r738b (- r738a) r737b (- r737a) r736 (- r735) (- r734) r733b (- r733a) (- r732) (- r731) (- r730) (- r729) r728b (- r728a) (- r727) (- r726) (- r725) r724b (- r724a) r723 (- r722) (- r721) (* -3 r720) (- r719) (- r718) r717b (- r717a) (- r716) (- r715) (- r714) (* -2 r713) (- r712) (- r711) (- r710) r709 (* -2 r708) (- r707) (- r706) (- r705) r704b (- r704a) (- r703) r702b (- r702a) r701b (- r701a) r700b (- r700a) r699b (- r699a) r698b (- r698a) r697b (- r697a) r696b (- r696a) (- r695) (- r694) (- r693) (- r692) (- r691) (- r690) (- r689) r688b (- r688a) r687b (- r687a) r674b (- r674a) (- r668) (- r664) (- r663) (- r662) r658b (- r658a) (- r657) (- r653) r652b (- r652a) r651b (- r651a) r650b (- r650a) (- r649) (- r648) r647b (- r647a) r646b (- r646a) r645b (- r645a) r644b (- r644a) r643b (- r643a) r642b (- r642a) r641b (- r641a) (- r640) (- r639) (- r638) (- r637) r636b (- r636a) (- r635) r634b (- r634a) r633b (- r633a) r632b (- r632a) (- r626) (- r625) r624b (- r624a) r623b (- r623a) r622b (- r622a) r621b (- r621a) (- r620) r619b (- r619a) (- r618) r614b (- r614a) r613b (- r613a) (- r612) r611b (- r611a) (- r610) (- r605) (- r604) (- r551) (* +2 r524) (- r495) (* +2 r484) (- r483) (- r480) (- r479b) r479a (* +2 r478) (- r477) r476b (- r476a) (- r470) r464b (- r464a) (- r452) (- r435) (- r434) (- r433) (- r432) (- r430) r398 (- r394) (* +3 r380) (* -2 r370) (* +2 r367b) (* -2 r367a) (- r362) (- r360) (- r359) r358 (- r356) (- r355) (* +2 r349) (- r342) (- r341) (- r340) r339b (- r339a) (- r338) r337b (- r337a) r336b (- r336a) r335b (- r335a) r334b (- r334a) r333b (- r333a) r332b (- r332a) r331b (- r331a) r330b (- r330a) r329b (- r329a) r328b (- r328a) r325b (- r325a) (- r322) (- r320) (* +2 r318b) (* -2 r318a) (- r315) r311 r310 (- r308b) r308a (* -2 r303b) (* +2 r303a) (* -2 r302b) (* +2 r302a) (* +2 r301) (* +2 r300) (* -2 r299b) (* +2 r299a) r290b (- r290a) r273b (- r273a) (- r264) (- r262) (- r247) (- r244) (- r242) (- r241) (- r237) r236 r233 r230 (- r223) (- r222) (* +2 r221) r219 (- r214b) r214a r208b (- r208a) (- r207) r206b (- r206a) r205b (- r205a) r204b (- r204a) r197b (- r197a) (- r189) (- r182) (- r175) (- r168) (- r161) (- r154) (- r147) (- r140) (- r133) r132 r127 r122 r117 r112 r107 r102 r97 r92 r86 (- r85b) r85a r84 r83 r82 r81 r80 (* +2 r57)) 0)
    (= (+ (- r350) r231) 0)
    (= (+ (- r85b) r85a) 0)
    (= (+ r586 (- r475)) 0)
    (= (+ (- r877b) r877a) 0)
    (= (+ (* -2 r486) r478) 0)
    (= (+ (- r668) (- r431b) r431a) 0)
    (= (+ (- r636b) r636a) 0)
    (= (+ (- r795) r610 r535 r293b (- r293a) r283b (- r283a)) 0)
    (= (+ r335b (- r335a)) 0)
    (= (+ (- r905) r452) 0)
    (= (+ (- r579) r543) 0)
    (= (+ r838) 0)
    (= (+ (- r884b) r884a r202b (- r202a)) 0)
    (= (+ (- r386) (- r382)) 0)
    (= (+ (- r637) r509) 0)
    (= (+ r776 (- r478)) 0)
    (= (+ (- r524) r407 (- r258)) 0)
    (= (+ (- r840)) 0)
    (= (+ (- r744b) r744a) 0)
    (= (+ (- r662) r393 (- r391b) r391a r390 (- r389b) r389a (- r387b) r387a r384 r383 r381 r229) 0)
    (= (+ (- r330b) r330a) 0)
    (= (+ (- r860b) r860a r853b (- r853a) (- r550b) r550a r211b (- r211a)) 0)
    (= (+ (- r523) r522 (- r521) r520 r517b (- r517a) r516b (- r516a) (- r515) r514 r513 r512 r509 (- r508) r506b (- r506a) r505b (- r505a) r504b (- r504a) r503b (- r503a) r502 (- r403) (- r358) (- r357) r356 (- r291b) r291a (- r266b) r266a r265) 0)
    (= (+ (- r573)) 0)
    (= (+ r388b (- r388a)) 0)
    (= (+ r226) 0)
    (= (+ r474b (- r474a)) 0)
    (= (+ r382) 0)
    (= (+ r837b (- r837a)) 0)
    (= (+ r674b (- r674a) (- r439b) r439a) 0)
    (= (+ (* -2 r312)) 0)
    (= (+ (- r658b) r658a (- r551)) 0)
    (= (+ (- r210) (- r209)) 0)
    (= (+ (- r652b) r652a r485 r469 r468) 0)
    (= (+ r462) 0)
    (= (+ r554 (- r461)) 0)
    (= (+ (- r789) r591) 0)
    (= (+ (- r462) r461) 0)
    (= (+ r68b (- r68a)) 0)
    (= (+ (- r285b) r285a) 0)
    (= (+ r425b (- r425a) (- r274b) r274a) 0)
    (= (+ (- r690) r307) 0)
    (= (+ r750) 0)
    (= (+ r287b (- r287a)) 0)
    (= (+ (- r561) r421 r416) 0)
    (= (+ r608 (- r380)) 0)
    (= (+ r818 (- r810)) 0)
    (= (+ (- r625) r243) 0)
    (= (+ r886 (- r392b) r392a (- r366)) 0)
    (= (+ (- r845)) 0)
    (= (+ r896 r203b (- r203a)) 0)
    (= (+ (- r603) r602b (- r602a) r589) 0)
    (= (+ (- r621b) r621a) 0)
    (= (+ r744b (- r744a)) 0)
    (= (+ (* -2 r299b) (* +2 r299a)) 0)
    (= (+ r812 (- r779)) 0)
    (= (+ r760b (- r760a) (- r635) r526) 0)
    (= (+ (- r697b) r697a) 0)
    (= (+ r484 (- r454)) 0)
    (= (+ (- r86) r64) 0)
    (= (+ r588 (- r525)) 0)
    (= (+ (- r553) r296) 0)
    (= (+ r533) 0)
    (= (+ r280b (- r280a)) 0)
    (= (+ (- r206b) r206a (- r205b) r205a (- r198) (- r196b) r196a) 0)
    (= (+ (- r87)) 0)
    (= (+ (- r514) r259) 0)
    (= (+ r398 (- r394) r392b (- r392a) (- r368) (- r365) r235 r219) 0)
    (= (+ (- r835) r705) 0)
    (= (+ (- r833) (- r831)) 0)
    (= (+ (* 0 r61)) 0)
    (= (+ (- r831) r348) 0)
    (= (+ r798b (- r798a) r715 r458 (- r457)) 0)
    (= (+ (- r715)) 0)
    (= (+ r843 r842 r764b (- r764a) (- r404) (- r402)) 0)
    (= (+ (- r614b) r614a (- r613b) r613a) 0)
    (= (+ (- r890) r250) 0)
    (= (+ (- r129) r128 (- r124) r123 (- r119) r118 (- r114) r113 (- r109) r108 (- r104) r103 (- r99) r98 (- r94) r93 r88) 0)
    (= (+ r371 (- r309)) 0)
    (= (+ (- r286b) r286a) 0)
    (= (+ r375b (- r375a)) 0)
    (= (+ (- r426b) r426a) 0)
    (= (+ r245b (- r245a)) 0)
    (= (+ (- r703)) 0)
    (= (+ (- r762) r729) 0)
    (= (+ (- r474b) r474a) 0)
    (= (+ r856b (- r856a)) 0)
    (= (+ r486 (- r478) r237) 0)
    (= (+ r82 (- r70)) 0)
    (= (+ r527) 0)
    (= (+ (- r556)) 0)
    (= (+ r70) 0)
    (= (+ (- r190) (- r183) (- r176) (- r169) (- r162) (- r155) (- r148) (- r141) (- r134)) 0)
    (= (+ r876b (- r876a) r389b (- r389a)) 0)
    (= (+ (- r374b) r374a) 0)
    (= (+ (* +4 r57)) 0)
    (= (+ r851 (- r447)) 0)
    (= (+ (- r79)) 0)
    (= (+ (- r707)) 0)
    (= (+ (- r377b) r377a r375b (- r375a)) 0)
    (= (+ (- r638) r477) 0)
    (= (+ (- r580b) r580a (- r572)) 0)
    (= (+ r809b (- r809a) r749 (- r239)) 0)
    (= (+ (- r674b) r674a) 0)
    (= (+ (- r886) r475) 0)
    (= (+ r855 (- r473)) 0)
    (= (+ (- r200b) r200a (- r199b) r199a) 0)
    (= (+ (- r851) r722) 0)
    (= (+ r903 (- r889) (- r598) (- r590) (- r588) (- r569b) r569a) 0)
    (= (+ (- r363) (- r362) (- r361) (- r360) (- r349) (* -3 r348) r347b (- r347a) r312 (- r311) (- r310) (- r309) r308b (- r308a) (- r307) r306b (- r306a) (- r305) (- r304) r300 r299b (- r299a) (- r241) (- r236) (- r230) (- r57)) 0)
    (= (+ r873b (- r873a) (- r701b) r701a (- r328b) r328a) 0)
    (= (+ r643b (- r643a)) 0)
    (= (+ (- r64)) 0)
    (= (+ (- r702b) r702a (- r701b) r701a (- r700b) r700a (- r699b) r699a (- r698b) r698a (- r697b) r697a) 0)
    (= (+ r912 r906 (- r744b) r744a r646b (- r646a) r603 (- r602b) r602a (- r578) r538 r448) 0)
    (= (+ r849b (- r849a) r534 (- r260) (- r211b) r211a) 0)
    (= (+ (- r758) (- r507) r495 (- r393) r391b (- r391a) (- r390) r389b (- r389a) r387b (- r387a) (- r384) (- r383) (- r381) (* -2 r351) (- r229) (* -2 r79)) 0)
    (= (+ (- r505b) r505a r359 (- r232) r217) 0)
    (= (+ r73) 0)
    (= (+ r889 (- r754)) 0)


    (= (+ (* -0.1 s1_obj) (- r917b) r917a r916 r915 (* +4 r914) r911 r910 r908 r905 (- r904b) r904a r903 r901 r900 r899 (- r898) r897 r896 r895 r894 r893 (- r892b) r892a r888 r887 r886 r885 (- r884b) r884a r883 r882 r880 (- r879b) r879a r878 (- r874b) r874a r814 r813 r812 r764b (- r764a) r761b (- r761a) r755b (- r755a) (- r741b) r741a (- r740b) r740a r739 r735 (* -2 r733b) (* +2 r733a) r729 r708 (- r651b) r651a (- r650b) r650a r649 r648 (- r647b) r647a (- r646b) r646a (- r645b) r645a (- r644b) r644a (- r643b) r643a (- r642b) r642a (- r641b) r641a r640 r639 r638 r637 (- r636b) r636a r635 (- r634b) r634a (- r633b) r633a (- r632b) r632a r605 r604 r524 r500 r495 r484 r480 r478 r477 r470 (- r464b) r464a r463 (- r460) (- r458) r456b (- r456a) (- r450) r443b (- r443a) (- r440) (- r423) (- r422) (- r401b) r401a r400 r399 r397 r326 r324 r323b (- r323a) r321 r237 r87) 0)
    (= (+ (* -0.1 s2_obj) (- r783) r434) 0)
    (= (+ (* -0.1 s3_obj) r580b (- r580a)) 0)
    (= (+ (* -0.1 s4_obj) (- r738b) r738a) 0)
    (= (+ (* -0.1 s5_obj) (- r824b) r824a r823 r822 r821 (- r790b) r790a r742 r364b (- r364a) (- r59b) r59a) 0)
    (= (+ (* -0.1 s6_obj) (- r537)) 0)
    (= (+ (* -0.1 s7_obj) (- r894) r834b (- r834a) r743 (- r519b) r519a (- r518b) r518a r501b (- r501a) (- r411) (- r355)) 0)
    (= (+ (* -0.1 s8_obj) r823 (- r746) (- r414)) 0)
    (= (+ (* -0.1 s9_obj) r909 (- r691)) 0)
    (= (+ (* -0.1 s10_obj) (- r909) r907b (- r907a) (- r902) (- r901) (- r893) r691 (- r562) r503b (- r503a) (- r399) r364b (- r364a) (- r361)) 0)
    (= (+ (* -0.1 s11_obj) (- r889) (- r888) r668 (- r482) r467) 0)
    (= (+ (* -0.1 s12_obj) r39_nutr_r (* -4 r914) (- r913) (- r912) (- r911) (- r910) (- r909) (- r903) r880 (- r770) (- r693) (- r511) (- r510) (- r452) (- r447) (- r357)) 0)
    (= (+ (* -0.1 s13_obj) r40_nutr_r (* +4 r914) r913 r912 r911 r910 r909 r903 (- r888) (- r886) (- r883) (- r880) (- r836) r770 (- r748) r712 r708 r706 r703 r693 (- r563) r523 (- r522) r521 (- r520) (- r517b) r517a (- r516b) r516a r515 (- r514) (- r513) (- r512) r511 r510 (- r509) r508 (- r506b) r506a (- r505b) r505a (- r504b) r504a (- r503b) r503a (- r502) r452 r447 (- r421) (- r416) r370 r358 (* +2 r357) (- r356)) 0)
    (= (+ (* -0.1 s14_obj) (- r905) (- r887) r767 r668 r413 r398 (- r235)) 0)
    (= (+ (* -0.1 s15_obj) (- r818) (- r290b) r290a r262) 0)
    (= (+ (* -0.1 s16_obj) r504b (- r504a)) 0)
    (= (+ (* -0.1 s17_obj) r505b (- r505a) (- r359)) 0)
    (= (+ (* -0.1 s18_obj) (- r750) r747) 0)
    (= (+ (* -0.1 s19_obj) (- r827) (- r495) (- r481b) r481a (* -2 r388b) (* +2 r388a) (- r387b) r387a r386 r385 (* +2 r351) (* +2 r79)) 0)
    (= (+ (* -0.1 s20_obj) r817b (- r817a) r516b (- r516a) r512 (- r309)) 0)
    (= (+ (* -0.1 s21_obj) (- r372)) 0)
    (= (+ (* -0.1 s22_obj) r49_nutr_r (- r816) r809b (- r809a) (- r806) r649 r519b (- r519a) (- r429) (- r398)) 0)
    (= (+ (* -0.1 s23_obj) r41_nutr_r (- r820) r814 (- r767) (- r297)) 0)
    (= (+ (* -0.1 s24_obj) (- r809b) r809a r806 (- r307)) 0)
    (= (+ (* -0.1 s25_obj) r819b (- r819a) (- r523) r522 r309) 0)
    (= (+ (* -0.1 s26_obj) r506b (- r506a)) 0)
    (= (+ (* -0.1 s27_obj) (- r575) r557 (- r392b) r392a) 0)
    (= (+ (* -0.1 s29_obj) r51_nutr_r (- r878) r774 r773 r706 r705 r482 r479b (- r479a) (- r364b) r364a r342 r341 r59b (- r59a)) 0)
    (= (+ (* -0.1 s31_obj) r790b (- r790a) r435 (- r269) (- r268) r267b (- r267a)) 0)
    (= (+ (* -0.1 s32_obj) r913 r881 r639 (- r542) r378b (- r378a) (* -2 r377b) (* +2 r377a) r373b (- r373a) r371 (- r370) r367b (- r367a) (- r365) (- r359) (- r356) (- r355) (- r346) (- r345) (- r341) (- r340) r339b (- r339a) (- r338) r337b (- r337a) r335b (- r335a) r334b (- r334a) r333b (- r333a) r332b (- r332a) r331b (- r331a) r330b (- r330a) r329b (- r329a) r328b (- r328a) (- r327) r325b (- r325a) r323b (- r323a) (- r322) (- r320) r319b (- r319a) r318b (- r318a) (- r317) (- r316) (- r315) (- r297) (- r295b) r295a r294b (- r294a) (* +2 r290b) (* -2 r290a) (- r289b) r289a (- r288b) r288a (- r287b) r287a (- r286b) r286a (- r285b) r285a r284b (- r284a) r283b (- r283a) r282 r281 r280b (- r280a) (- r279b) r279a (- r278b) r278a r276b (- r276a) r275b (- r275a) r274b (- r274a) (- r273b) r273a r271b (- r271a) (- r270) (- r268) r267b (- r267a) r266b (- r266a) (- r264) (- r263) (- r262) r261b (- r261a) (- r259) r256 (- r255b) r255a r254b (- r254a) (- r251) (- r249) (- r248) (- r235) (- r232) (- r231) r197b (- r197a) (- r195) (- r188) (- r181) (- r174) (- r167) (- r160) (- r153) (- r146) (- r139) r130 r125 r120 r115 r110 r105 r100 r95 r90 (- r76) r75 r74 r73 r72 r71 r70 r69 r68b (- r68a) r55) 0)
    (= (+ (* -0.1 s33_obj) (- r378b) r378a (* +2 r377b) (* -2 r377a) (- r373b) r373a (- r371) r370 (- r367b) r367a r365 r359 r356 r355 r346 r345 r341 r340 (- r339b) r339a r338 (- r337b) r337a (- r335b) r335a (- r334b) r334a (- r333b) r333a (- r332b) r332a (- r331b) r331a (- r330b) r330a (- r329b) r329a (- r328b) r328a r327 (- r325b) r325a (- r323b) r323a r322 r320 (- r319b) r319a (- r318b) r318a r317 r316 r315 r297 r295b (- r295a) (- r294b) r294a (* -2 r290b) (* +2 r290a) r289b (- r289a) r288b (- r288a) r287b (- r287a) r286b (- r286a) r285b (- r285a) (- r284b) r284a (- r283b) r283a (- r282) (- r281) (- r280b) r280a r279b (- r279a) r278b (- r278a) (- r276b) r276a (- r275b) r275a (- r274b) r274a r273b (- r273a) (- r271b) r271a r270 r268 (- r267b) r267a (- r266b) r266a r264 r263 r262 (- r261b) r261a r259 (- r256) r255b (- r255a) (- r254b) r254a r251 r249 r248 r235 r232 r231 (- r197b) r197a r195 r188 r181 r174 r167 r160 r153 r146 r139 (- r130) (- r125) (- r120) (- r115) (- r110) (- r105) (- r100) (- r95) (- r90) r76 (- r75) (- r74) (- r73) (- r72) (- r71) (- r70) (- r69) (- r68b) r68a (- r55)) 0)
    (= (+ (* -0.1 s34_obj) (- r639) r542 (* +3 r380) r379 (* +2 r376b) (* -2 r376a) (* +2 r375b) (* -2 r375a) (- r374b) r374a (- r373b) r373a r369b (- r369a) (- r368) r366 r358 r357 r344b (- r344a) (- r342) r336b (- r336a) r326 r324 r321 r313 r298 r296 r293b (- r293a) r292b (- r292a) r291b (- r291a) (- r277b) r277a r272 (- r269) (- r265) (- r260) r258 r257 r253 r252 r250 (- r246b) r246a r131 r129 r126 r124 r121 r119 r116 r114 r111 r109 r106 r104 r101 r99 r96 r94 r91 r89 r67 r66 r65 r64 r63 r62) 0)

    (= (+ (* -0.1 s35_obj) (* -3 r380) (- r379) (* -2 r376b) (* +2 r376a) (* -2 r375b) (* +2 r375a) r374b (- r374a) r373b (- r373a) (- r369b) r369a r368 (- r366) (- r358) (- r357) (- r344b) r344a r342 (- r336b) r336a (- r326) (- r324) (- r321) (- r313) (- r298) (- r296) (- r293b) r293a (- r292b) r292a (- r291b) r291a r277b (- r277a) (- r272) r269 r265 r260 (- r258) (- r257) (- r253) (- r252) (- r250) r246b (- r246a) (- r131) (- r129) (- r126) (- r124) (- r121) (- r119) (- r116) (- r114) (- r111) (- r109) (- r106) (- r104) (- r101) (- r99) (- r96) (- r94) (- r91) (- r89) (- r67) (- r66) (- r65) (- r64) (- r63) (- r62)) 0)
    (= (+ (* -0.1 s36_obj) r592 (- r372) (- r354b) r354a (- r353) (- r352) (- r350) (- r191) (- r184) (- r177) (- r170) (- r163) (- r156) (- r149) (- r142) (- r135)) 0)
    (= (+ (* -0.1 s37_obj) r875b (- r875a) (- r619b) r619a) 0)

    (<= (+ r38_nutr_r (* -1000 s38_nutr)) 0)
    (<= (- r38_nutr_r) 0)
    (<= (+ r39_nutr_r (* -1000 s39_nutr)) 0)
    (<= (- r39_nutr_r) 0)
    (<= (+ r40_nutr_r (* -1000 s40_nutr)) 0)
    (<= (- r40_nutr_r) 0)
    (<= (+ r41_nutr_r (* -1000 s41_nutr)) 0)
    (<= (- r41_nutr_r) 0)
    (<= (+ r42_nutr_r (* -1000 s42_nutr)) 0)
    (<= (- r42_nutr_r) 0)
    (<= (+ r43_nutr_r (* -1000 s43_nutr)) 0)
    (<= (- r43_nutr_r) 0)
    (<= (+ r44_nutr_r (* -1000 s44_nutr)) 0)
    (<= (- r44_nutr_r) 0)
    (<= (+ r45_nutr_r (* -1000 s45_nutr)) 0)
    (<= (- r45_nutr_r) 0)
    (<= (+ r46_nutr_r (* -1000 s46_nutr)) 0)
    (<= (- r46_nutr_r) 0)
    (<= (+ r47_nutr_r (* -1000 s47_nutr)) 0)
    (<= (- r47_nutr_r)  0)
    (<= (+ r48_nutr_r (* -1000 s48_nutr)) 0)
    (<= (- r48_nutr_r) 0)
    (<= (+ r49_nutr_r (* -1000 s49_nutr)) 0)
    (<= (- r49_nutr_r) 0)
    (<= (+ r50_nutr_r (* -1000 s50_nutr)) 0)
    (<= (- r50_nutr_r) 0)
    (<= (+ r51_nutr_r (* -1000 s51_nutr)) 0)
    (<= (- r51_nutr_r) 0)
    (<= (+ r52_secrt_r (* -1000 s52_secrt)) 0)
    (<= (- r52_secrt_r) 0)
    (<= (+ r53_secrt_r (* -1000 s53_secrt)) 0)
    (<= (- r53_secrt_r) 0)
    (<= (+ r54_secrt_r (* -1000 s54_secrt)) 0)
    (<= (- r54_secrt_r) 0)

    (and (<= 0 r55) (<= r55 1000))
    (and (<= 0 r56) (<= r56 1000))
    (and (<= 0 r57) (<= r57 1000))
    (and (<= 0 r58) (<= r58 1000))
    (and (<= 0 r59a) (<= r59a 1000))
    (and (<= 0 r59b) (<= r59b 1000))
    (and (<= 0 r60) (<= r60 1000))
    (and (<= 0 r61) (<= r61 1000))
    (and (<= 0 r62) (<= r62 1000))
    (and (<= 0 r63) (<= r63 1000))
    (and (<= 0 r64) (<= r64 1000))
    (and (<= 0 r65) (<= r65 1000))
    (and (<= 0 r66) (<= r66 1000))
    (and (<= 0 r67) (<= r67 1000))
    (and (<= 0 r68a) (<= r68a 1000))
    (and (<= 0 r68b) (<= r68b 1000))
    (and (<= 0 r69) (<= r69 1000))
    (and (<= 0 r70) (<= r70 1000))
    (and (<= 0 r71) (<= r71 1000))
    (and (<= 0 r72) (<= r72 1000))
    (and (<= 0 r73) (<= r73 1000))
    (and (<= 0 r74) (<= r74 1000))
    (and (<= 0 r75) (<= r75 1000))
    (and (<= 0 r76) (<= r76 1000))
    (and (<= 0 r77) (<= r77 1000))
    (and (<= 0 r78) (<= r78 1000))
    (and (<= 0 r79) (<= r79 1000))
    (and (<= 0 r80) (<= r80 1000))
    (and (<= 0 r81) (<= r81 1000))
    (and (<= 0 r82) (<= r82 1000))
    (and (<= 0 r83) (<= r83 1000))
    (and (<= 0 r84) (<= r84 1000))
    (and (<= 0 r85a) (<= r85a 1000))
    (and (<= 0 r85b) (<= r85b 1000))
    (and (<= 0 r86) (<= r86 1000))
    (and (<= 0 r87) (<= r87 1000))
    (and (<= 0 r88) (<= r88 1000))
    (and (<= 0 r89) (<= r89 1000))
    (and (<= 0 r90) (<= r90 1000))
    (and (<= 0 r91) (<= r91 1000))
    (and (<= 0 r92) (<= r92 1000))
    (and (<= 0 r93) (<= r93 1000))
    (and (<= 0 r94) (<= r94 1000))
    (and (<= 0 r95) (<= r95 1000))
    (and (<= 0 r96) (<= r96 1000))
    (and (<= 0 r97) (<= r97 1000))
    (and (<= 0 r98) (<= r98 1000))
    (and (<= 0 r99) (<= r99 1000))
    (and (<= 0 r100) (<= r100 1000))
    (and (<= 0 r101) (<= r101 1000))
    (and (<= 0 r102) (<= r102 1000))
    (and (<= 0 r103) (<= r103 1000))
    (and (<= 0 r104) (<= r104 1000))
    (and (<= 0 r105) (<= r105 1000))
    (and (<= 0 r106) (<= r106 1000))
    (and (<= 0 r107) (<= r107 1000))
    (and (<= 0 r108) (<= r108 1000))
    (and (<= 0 r109) (<= r109 1000))
    (and (<= 0 r110) (<= r110 1000))
    (and (<= 0 r111) (<= r111 1000))
    (and (<= 0 r112) (<= r112 1000))
    (and (<= 0 r113) (<= r113 1000))
    (and (<= 0 r114) (<= r114 1000))
    (and (<= 0 r115) (<= r115 1000))
    (and (<= 0 r116) (<= r116 1000))
    (and (<= 0 r117) (<= r117 1000))
    (and (<= 0 r118) (<= r118 1000))
    (and (<= 0 r119) (<= r119 1000))
    (and (<= 0 r120) (<= r120 1000))
    (and (<= 0 r121) (<= r121 1000))
    (and (<= 0 r122) (<= r122 1000))
    (and (<= 0 r123) (<= r123 1000))
    (and (<= 0 r124) (<= r124 1000))
    (and (<= 0 r125) (<= r125 1000))
    (and (<= 0 r126) (<= r126 1000))
    (and (<= 0 r127) (<= r127 1000))
    (and (<= 0 r128) (<= r128 1000))
    (and (<= 0 r129) (<= r129 1000))
    (and (<= 0 r130) (<= r130 1000))
    (and (<= 0 r131) (<= r131 1000))
    (and (<= 0 r132) (<= r132 1000))
    (and (<= 0 r133) (<= r133 1000))
    (and (<= 0 r134) (<= r134 1000))
    (and (<= 0 r135) (<= r135 1000))
    (and (<= 0 r136) (<= r136 1000))
    (and (<= 0 r137) (<= r137 1000))
    (and (<= 0 r138) (<= r138 1000))
    (and (<= 0 r139) (<= r139 1000))
    (and (<= 0 r140) (<= r140 1000))
    (and (<= 0 r141) (<= r141 1000))
    (and (<= 0 r142) (<= r142 1000))
    (and (<= 0 r143) (<= r143 1000))
    (and (<= 0 r144) (<= r144 1000))
    (and (<= 0 r145) (<= r145 1000))
    (and (<= 0 r146) (<= r146 1000))
    (and (<= 0 r147) (<= r147 1000))
    (and (<= 0 r148) (<= r148 1000))
    (and (<= 0 r149) (<= r149 1000))
    (and (<= 0 r150) (<= r150 1000))
    (and (<= 0 r151) (<= r151 1000))
    (and (<= 0 r152) (<= r152 1000))
    (and (<= 0 r153) (<= r153 1000))
    (and (<= 0 r154) (<= r154 1000))
    (and (<= 0 r155) (<= r155 1000))
    (and (<= 0 r156) (<= r156 1000))
    (and (<= 0 r157) (<= r157 1000))
    (and (<= 0 r158) (<= r158 1000))
    (and (<= 0 r159) (<= r159 1000))
    (and (<= 0 r160) (<= r160 1000))
    (and (<= 0 r161) (<= r161 1000))
    (and (<= 0 r162) (<= r162 1000))
    (and (<= 0 r163) (<= r163 1000))
    (and (<= 0 r164) (<= r164 1000))
    (and (<= 0 r165) (<= r165 1000))
    (and (<= 0 r166) (<= r166 1000))
    (and (<= 0 r167) (<= r167 1000))
    (and (<= 0 r168) (<= r168 1000))
    (and (<= 0 r169) (<= r169 1000))
    (and (<= 0 r170) (<= r170 1000))
    (and (<= 0 r171) (<= r171 1000))
    (and (<= 0 r172) (<= r172 1000))
    (and (<= 0 r173) (<= r173 1000))
    (and (<= 0 r174) (<= r174 1000))
    (and (<= 0 r175) (<= r175 1000))
    (and (<= 0 r176) (<= r176 1000))
    (and (<= 0 r177) (<= r177 1000))
    (and (<= 0 r178) (<= r178 1000))
    (and (<= 0 r179) (<= r179 1000))
    (and (<= 0 r180) (<= r180 1000))
    (and (<= 0 r181) (<= r181 1000))
    (and (<= 0 r182) (<= r182 1000))
    (and (<= 0 r183) (<= r183 1000))
    (and (<= 0 r184) (<= r184 1000))
    (and (<= 0 r185) (<= r185 1000))
    (and (<= 0 r186) (<= r186 1000))
    (and (<= 0 r187) (<= r187 1000))
    (and (<= 0 r188) (<= r188 1000))
    (and (<= 0 r189) (<= r189 1000))
    (and (<= 0 r190) (<= r190 1000))
    (and (<= 0 r191) (<= r191 1000))
    (and (<= 0 r192) (<= r192 1000))
    (and (<= 0 r193) (<= r193 1000))
    (and (<= 0 r194) (<= r194 1000))
    (and (<= 0 r195) (<= r195 1000))
    (and (<= 0 r196a) (<= r196a 1000))
    (and (<= 0 r196b) (<= r196b 1000))
    (and (<= 0 r197a) (<= r197a 1000))
    (and (<= 0 r197b) (<= r197b 1000))
    (and (<= 0 r198) (<= r198 1000))
    (and (<= 0 r199a) (<= r199a 1000))
    (and (<= 0 r199b) (<= r199b 1000))
    (and (<= 0 r200a) (<= r200a 1000))
    (and (<= 0 r200b) (<= r200b 1000))
    (and (<= 0 r201) (<= r201 1000))
    (and (<= 0 r202a) (<= r202a 1000))
    (and (<= 0 r202b) (<= r202b 1000))
    (and (<= 0 r203a) (<= r203a 1000))
    (and (<= 0 r203b) (<= r203b 1000))
    (and (<= 0 r204a) (<= r204a 1000))
    (and (<= 0 r204b) (<= r204b 1000))
    (and (<= 0 r205a) (<= r205a 1000))
    (and (<= 0 r205b) (<= r205b 1000))
    (and (<= 0 r206a) (<= r206a 1000))
    (and (<= 0 r206b) (<= r206b 1000))
    (and (<= 0 r207) (<= r207 1000))
    (and (<= 0 r208a) (<= r208a 1000))
    (and (<= 0 r208b) (<= r208b 1000))
    (and (<= 0 r209) (<= r209 1000))
    (and (<= 0 r210) (<= r210 1000))
    (and (<= 0 r211a) (<= r211a 1000))
    (and (<= 0 r211b) (<= r211b 1000))
    (and (<= 0 r212a) (<= r212a 1000))
    (and (<= 0 r212b) (<= r212b 1000))
    (and (<= 0 r213) (<= r213 1000))
    (and (<= 0 r214a) (<= r214a 1000))
    (and (<= 0 r214b) (<= r214b 1000))
    (and (<= 0 r215) (<= r215 1000))
    (and (<= 0 r216) (<= r216 1000))
    (and (<= 0 r217) (<= r217 1000))
    (and (<= 0 r218) (<= r218 1000))
    (and (<= 0 r219) (<= r219 1000))
    (and (<= 0 r220) (<= r220 1000))
    (and (<= 0 r221) (<= r221 1000))
    (and (<= 0 r222) (<= r222 1000))
    (and (<= 0 r223) (<= r223 1000))
    (and (<= 0 r224) (<= r224 1000))
    (and (<= 0 r225) (<= r225 1000))
    (and (<= 0 r226) (<= r226 1000))
    (and (<= 0 r227) (<= r227 1000))
    (and (<= 0 r228) (<= r228 1000))
    (and (<= 0 r229) (<= r229 1000))
    (and (<= 0 r230) (<= r230 1000))
    (and (<= 0 r231) (<= r231 1000))
    (and (<= 0 r232) (<= r232 1000))
    (and (<= 0 r233) (<= r233 1000))
    (and (<= 0 r234) (<= r234 1000))
    (and (<= 0 r235) (<= r235 1000))
    (and (<= 0 r236) (<= r236 1000))
    (and (<= 0 r237) (<= r237 1000))
    (and (<= 0 r238) (<= r238 1000))
    (and (<= 0 r239) (<= r239 1000))
    (and (<= 0 r240a) (<= r240a 1000))
    (and (<= 0 r240b) (<= r240b 1000))
    (and (<= 0 r241) (<= r241 1000))
    (and (<= 0 r242) (<= r242 1000))
    (and (<= 0 r243) (<= r243 1000))
    (and (<= 0 r244) (<= r244 1000))
    (and (<= 0 r245a) (<= r245a 1000))
    (and (<= 0 r245b) (<= r245b 1000))
    (and (<= 0 r246a) (<= r246a 1000))
    (and (<= 0 r246b) (<= r246b 1000))
    (and (<= 0 r247) (<= r247 1000))
    (and (<= 0 r248) (<= r248 1000))
    (and (<= 0 r249) (<= r249 1000))
    (and (<= 0 r250) (<= r250 1000))
    (and (<= 0 r251) (<= r251 1000))
    (and (<= 0 r252) (<= r252 1000))
    (and (<= 0 r253) (<= r253 1000))
    (and (<= 0 r254a) (<= r254a 1000))
    (and (<= 0 r254b) (<= r254b 1000))
    (and (<= 0 r255a) (<= r255a 1000))
    (and (<= 0 r255b) (<= r255b 1000))
    (and (<= 0 r256) (<= r256 1000))
    (and (<= 0 r257) (<= r257 1000))
    (and (<= 0 r258) (<= r258 1000))
    (and (<= 0 r259) (<= r259 1000))
    (and (<= 0 r260) (<= r260 1000))
    (and (<= 0 r261a) (<= r261a 1000))
    (and (<= 0 r261b) (<= r261b 1000))
    (and (<= 0 r262) (<= r262 1000))
    (and (<= 0 r263) (<= r263 1000))
    (and (<= 0 r264) (<= r264 1000))
    (and (<= 0 r265) (<= r265 1000))
    (and (<= 0 r266a) (<= r266a 1000))
    (and (<= 0 r266b) (<= r266b 1000))
    (and (<= 0 r267a) (<= r267a 1000))
    (and (<= 0 r267b) (<= r267b 1000))
    (and (<= 0 r268) (<= r268 1000))
    (and (<= 0 r269) (<= r269 1000))
    (and (<= 0 r270) (<= r270 1000))
    (and (<= 0 r271a) (<= r271a 1000))
    (and (<= 0 r271b) (<= r271b 1000))
    (and (<= 0 r272) (<= r272 1000))
    (and (<= 0 r273a) (<= r273a 1000))
    (and (<= 0 r273b) (<= r273b 1000))
    (and (<= 0 r274a) (<= r274a 1000))
    (and (<= 0 r274b) (<= r274b 1000))
    (and (<= 0 r275a) (<= r275a 1000))
    (and (<= 0 r275b) (<= r275b 1000))
    (and (<= 0 r276a) (<= r276a 1000))
    (and (<= 0 r276b) (<= r276b 1000))
    (and (<= 0 r277a) (<= r277a 1000))
    (and (<= 0 r277b) (<= r277b 1000))
    (and (<= 0 r278a) (<= r278a 1000))
    (and (<= 0 r278b) (<= r278b 1000))
    (and (<= 0 r279a) (<= r279a 1000))
    (and (<= 0 r279b) (<= r279b 1000))
    (and (<= 0 r280a) (<= r280a 1000))
    (and (<= 0 r280b) (<= r280b 1000))
    (and (<= 0 r281) (<= r281 1000))
    (and (<= 0 r282) (<= r282 1000))
    (and (<= 0 r283a) (<= r283a 1000))
    (and (<= 0 r283b) (<= r283b 1000))
    (and (<= 0 r284a) (<= r284a 1000))
    (and (<= 0 r284b) (<= r284b 1000))
    (and (<= 0 r285a) (<= r285a 1000))
    (and (<= 0 r285b) (<= r285b 1000))
    (and (<= 0 r286a) (<= r286a 1000))
    (and (<= 0 r286b) (<= r286b 1000))
    (and (<= 0 r287a) (<= r287a 1000))
    (and (<= 0 r287b) (<= r287b 1000))
    (and (<= 0 r288a) (<= r288a 1000))
    (and (<= 0 r288b) (<= r288b 1000))
    (and (<= 0 r289a) (<= r289a 1000))
    (and (<= 0 r289b) (<= r289b 1000))
    (and (<= 0 r290a) (<= r290a 1000))
    (and (<= 0 r290b) (<= r290b 1000))
    (and (<= 0 r291a) (<= r291a 1000))
    (and (<= 0 r291b) (<= r291b 1000))
    (and (<= 0 r292a) (<= r292a 1000))
    (and (<= 0 r292b) (<= r292b 1000))
    (and (<= 0 r293a) (<= r293a 1000))
    (and (<= 0 r293b) (<= r293b 1000))
    (and (<= 0 r294a) (<= r294a 1000))
    (and (<= 0 r294b) (<= r294b 1000))
    (and (<= 0 r295a) (<= r295a 1000))
    (and (<= 0 r295b) (<= r295b 1000))
    (and (<= 0 r296) (<= r296 1000))
    (and (<= 0 r297) (<= r297 1000))
    (and (<= 0 r298) (<= r298 1000))
    (and (<= 0 r299a) (<= r299a 1000))
    (and (<= 0 r299b) (<= r299b 1000))
    (and (<= 0 r300) (<= r300 1000))
    (and (<= 0 r301) (<= r301 1000))
    (and (<= 0 r302a) (<= r302a 1000))
    (and (<= 0 r302b) (<= r302b 1000))
    (and (<= 0 r303a) (<= r303a 1000))
    (and (<= 0 r303b) (<= r303b 1000))
    (and (<= 0 r304) (<= r304 1000))
    (and (<= 0 r305) (<= r305 1000))
    (and (<= 0 r306a) (<= r306a 1000))
    (and (<= 0 r306b) (<= r306b 1000))
    (and (<= 0 r307) (<= r307 1000))
    (and (<= 0 r308a) (<= r308a 1000))
    (and (<= 0 r308b) (<= r308b 1000))
    (and (<= 0 r309) (<= r309 1000))
    (and (<= 0 r310) (<= r310 1000))
    (and (<= 0 r311) (<= r311 1000))
    (and (<= 0 r312) (<= r312 1000))
    (and (<= 0 r313) (<= r313 1000))
    (and (<= 0 r314) (<= r314 1000))
    (and (<= 0 r315) (<= r315 1000))
    (and (<= 0 r316) (<= r316 1000))
    (and (<= 0 r317) (<= r317 1000))
    (and (<= 0 r318a) (<= r318a 1000))
    (and (<= 0 r318b) (<= r318b 1000))
    (and (<= 0 r319a) (<= r319a 1000))
    (and (<= 0 r319b) (<= r319b 1000))
    (and (<= 0 r320) (<= r320 1000))
    (and (<= 0 r321) (<= r321 1000))
    (and (<= 0 r322) (<= r322 1000))
    (and (<= 0 r323a) (<= r323a 1000))
    (and (<= 0 r323b) (<= r323b 1000))
    (and (<= 0 r324) (<= r324 1000))
    (and (<= 0 r325a) (<= r325a 1000))
    (and (<= 0 r325b) (<= r325b 1000))
    (and (<= 0 r326) (<= r326 1000))
    (and (<= 0 r327) (<= r327 1000))
    (and (<= 0 r328a) (<= r328a 1000))
    (and (<= 0 r328b) (<= r328b 1000))
    (and (<= 0 r329a) (<= r329a 1000))
    (and (<= 0 r329b) (<= r329b 1000))
    (and (<= 0 r330a) (<= r330a 1000))
    (and (<= 0 r330b) (<= r330b 1000))
    (and (<= 0 r331a) (<= r331a 1000))
    (and (<= 0 r331b) (<= r331b 1000))
    (and (<= 0 r332a) (<= r332a 1000))
    (and (<= 0 r332b) (<= r332b 1000))
    (and (<= 0 r333a) (<= r333a 1000))
    (and (<= 0 r333b) (<= r333b 1000))
    (and (<= 0 r334a) (<= r334a 1000))
    (and (<= 0 r334b) (<= r334b 1000))
    (and (<= 0 r335a) (<= r335a 1000))
    (and (<= 0 r335b) (<= r335b 1000))
    (and (<= 0 r336a) (<= r336a 1000))
    (and (<= 0 r336b) (<= r336b 1000))
    (and (<= 0 r337a) (<= r337a 1000))
    (and (<= 0 r337b) (<= r337b 1000))
    (and (<= 0 r338) (<= r338 1000))
    (and (<= 0 r339a) (<= r339a 1000))
    (and (<= 0 r339b) (<= r339b 1000))
    (and (<= 0 r340) (<= r340 1000))
    (and (<= 0 r341) (<= r341 1000))
    (and (<= 0 r342) (<= r342 1000))
    (and (<= 0 r343a) (<= r343a 1000))
    (and (<= 0 r343b) (<= r343b 1000))
    (and (<= 0 r344a) (<= r344a 1000))
    (and (<= 0 r344b) (<= r344b 1000))
    (and (<= 0 r345) (<= r345 1000))
    (and (<= 0 r346) (<= r346 1000))
    (and (<= 0 r347a) (<= r347a 1000))
    (and (<= 0 r347b) (<= r347b 1000))
    (and (<= 0 r348) (<= r348 1000))
    (and (<= 0 r349) (<= r349 1000))
    (and (<= 0 r350) (<= r350 1000))
    (and (<= 0 r351) (<= r351 1000))
    (and (<= 0 r352) (<= r352 1000))
    (and (<= 0 r353) (<= r353 1000))
    (and (<= 0 r354a) (<= r354a 1000))
    (and (<= 0 r354b) (<= r354b 1000))
    (and (<= 0 r355) (<= r355 1000))
    (and (<= 0 r356) (<= r356 1000))
    (and (<= 0 r357) (<= r357 1000))
    (and (<= 0 r358) (<= r358 1000))
    (and (<= 0 r359) (<= r359 1000))
    (and (<= 0 r360) (<= r360 1000))
    (and (<= 0 r361) (<= r361 1000))
    (and (<= 0 r362) (<= r362 1000))
    (and (<= 0 r363) (<= r363 1000))
    (and (<= 0 r364a) (<= r364a 1000))
    (and (<= 0 r364b) (<= r364b 1000))
    (and (<= 0 r365) (<= r365 1000))
    (and (<= 0 r366) (<= r366 1000))
    (and (<= 0 r367a) (<= r367a 1000))
    (and (<= 0 r367b) (<= r367b 1000))
    (and (<= 0 r368) (<= r368 1000))
    (and (<= 0 r369a) (<= r369a 1000))
    (and (<= 0 r369b) (<= r369b 1000))
    (and (<= 0 r370) (<= r370 1000))
    (and (<= 0 r371) (<= r371 1000))
    (and (<= 0 r372) (<= r372 1000))
    (and (<= 0 r373a) (<= r373a 1000))
    (and (<= 0 r373b) (<= r373b 1000))
    (and (<= 0 r374a) (<= r374a 1000))
    (and (<= 0 r374b) (<= r374b 1000))
    (and (<= 0 r375a) (<= r375a 1000))
    (and (<= 0 r375b) (<= r375b 1000))
    (and (<= 0 r376a) (<= r376a 1000))
    (and (<= 0 r376b) (<= r376b 1000))
    (and (<= 0 r377a) (<= r377a 1000))
    (and (<= 0 r377b) (<= r377b 1000))
    (and (<= 0 r378a) (<= r378a 1000))
    (and (<= 0 r378b) (<= r378b 1000))
    (and (<= 0 r379) (<= r379 1000))
    (and (<= 0 r380) (<= r380 1000))
    (and (<= 0 r381) (<= r381 1000))
    (and (<= 0 r382) (<= r382 1000))
    (and (<= 0 r383) (<= r383 1000))
    (and (<= 0 r384) (<= r384 1000))
    (and (<= 0 r385) (<= r385 1000))
    (and (<= 0 r386) (<= r386 1000))
    (and (<= 0 r387a) (<= r387a 1000))
    (and (<= 0 r387b) (<= r387b 1000))
    (and (<= 0 r388a) (<= r388a 1000))
    (and (<= 0 r388b) (<= r388b 1000))
    (and (<= 0 r389a) (<= r389a 1000))
    (and (<= 0 r389b) (<= r389b 1000))
    (and (<= 0 r390) (<= r390 1000))
    (and (<= 0 r391a) (<= r391a 1000))
    (and (<= 0 r391b) (<= r391b 1000))
    (and (<= 0 r392a) (<= r392a 1000))
    (and (<= 0 r392b) (<= r392b 1000))
    (and (<= 0 r393) (<= r393 1000))
    (and (<= 0 r394) (<= r394 1000))
    (and (<= 0 r395) (<= r395 1000))
    (and (<= 0 r396) (<= r396 1000))
    (and (<= 0 r397) (<= r397 1000))
    (and (<= 0 r398) (<= r398 1000))
    (and (<= 0 r399) (<= r399 1000))
    (and (<= 0 r400) (<= r400 1000))
    (and (<= 0 r401a) (<= r401a 1000))
    (and (<= 0 r401b) (<= r401b 1000))
    (and (<= 0 r402) (<= r402 1000))
    (and (<= 0 r403) (<= r403 1000))
    (and (<= 0 r404) (<= r404 1000))
    (and (<= 0 r405) (<= r405 1000))
    (and (<= 0 r406) (<= r406 1000))
    (and (<= 0 r407) (<= r407 1000))
    (and (<= 0 r408a) (<= r408a 1000))
    (and (<= 0 r408b) (<= r408b 1000))
    (and (<= 0 r409) (<= r409 1000))
    (and (<= 0 r410) (<= r410 1000))
    (and (<= 0 r411) (<= r411 1000))
    (and (<= 0 r412) (<= r412 1000))
    (and (<= 0 r413) (<= r413 1000))
    (and (<= 0 r414) (<= r414 1000))
    (and (<= 0 r415a) (<= r415a 1000))
    (and (<= 0 r415b) (<= r415b 1000))
    (and (<= 0 r416) (<= r416 1000))
    (and (<= 0 r417) (<= r417 1000))
    (and (<= 0 r418) (<= r418 1000))
    (and (<= 0 r419) (<= r419 1000))
    (and (<= 0 r420) (<= r420 1000))
    (and (<= 0 r421) (<= r421 1000))
    (and (<= 0 r422) (<= r422 1000))
    (and (<= 0 r423) (<= r423 1000))
    (and (<= 0 r424) (<= r424 1000))
    (and (<= 0 r425a) (<= r425a 1000))
    (and (<= 0 r425b) (<= r425b 1000))
    (and (<= 0 r426a) (<= r426a 1000))
    (and (<= 0 r426b) (<= r426b 1000))
    (and (<= 0 r427a) (<= r427a 1000))
    (and (<= 0 r427b) (<= r427b 1000))
    (and (<= 0 r428a) (<= r428a 1000))
    (and (<= 0 r428b) (<= r428b 1000))
    (and (<= 0 r429) (<= r429 1000))
    (and (<= 0 r430) (<= r430 1000))
    (and (<= 0 r431a) (<= r431a 1000))
    (and (<= 0 r431b) (<= r431b 1000))
    (and (<= 0 r432) (<= r432 1000))
    (and (<= 0 r433) (<= r433 1000))
    (and (<= 0 r434) (<= r434 1000))
    (and (<= 0 r435) (<= r435 1000))
    (and (<= 0 r436) (<= r436 1000))
    (and (<= 0 r437) (<= r437 1000))
    (and (<= 0 r438a) (<= r438a 1000))
    (and (<= 0 r438b) (<= r438b 1000))
    (and (<= 0 r439a) (<= r439a 1000))
    (and (<= 0 r439b) (<= r439b 1000))
    (and (<= 0 r440) (<= r440 1000))
    (and (<= 0 r441a) (<= r441a 1000))
    (and (<= 0 r441b) (<= r441b 1000))
    (and (<= 0 r442a) (<= r442a 1000))
    (and (<= 0 r442b) (<= r442b 1000))
    (and (<= 0 r443a) (<= r443a 1000))
    (and (<= 0 r443b) (<= r443b 1000))
    (and (<= 0 r444) (<= r444 1000))
    (and (<= 0 r445) (<= r445 1000))
    (and (<= 0 r446) (<= r446 1000))
    (and (<= 0 r447) (<= r447 1000))
    (and (<= 0 r448) (<= r448 1000))
    (and (<= 0 r449) (<= r449 1000))
    (and (<= 0 r450) (<= r450 1000))
    (and (<= 0 r451) (<= r451 1000))
    (and (<= 0 r452) (<= r452 1000))
    (and (<= 0 r453) (<= r453 1000))
    (and (<= 0 r454) (<= r454 1000))
    (and (<= 0 r455a) (<= r455a 1000))
    (and (<= 0 r455b) (<= r455b 1000))
    (and (<= 0 r456a) (<= r456a 1000))
    (and (<= 0 r456b) (<= r456b 1000))
    (and (<= 0 r457) (<= r457 1000))
    (and (<= 0 r458) (<= r458 1000))
    (and (<= 0 r459) (<= r459 1000))
    (and (<= 0 r460) (<= r460 1000))
    (and (<= 0 r461) (<= r461 1000))
    (and (<= 0 r462) (<= r462 1000))
    (and (<= 0 r463) (<= r463 1000))
    (and (<= 0 r464a) (<= r464a 1000))
    (and (<= 0 r464b) (<= r464b 1000))
    (and (<= 0 r465) (<= r465 1000))
    (and (<= 0 r466) (<= r466 1000))
    (and (<= 0 r467) (<= r467 1000))
    (and (<= 0 r468) (<= r468 1000))
    (and (<= 0 r469) (<= r469 1000))
    (and (<= 0 r470) (<= r470 1000))
    (and (<= 0 r471) (<= r471 1000))
    (and (<= 0 r472) (<= r472 1000))
    (and (<= 0 r473) (<= r473 1000))
    (and (<= 0 r474a) (<= r474a 1000))
    (and (<= 0 r474b) (<= r474b 1000))
    (and (<= 0 r475) (<= r475 1000))
    (and (<= 0 r476a) (<= r476a 1000))
    (and (<= 0 r476b) (<= r476b 1000))
    (and (<= 0 r477) (<= r477 1000))
    (and (<= 0 r478) (<= r478 1000))
    (and (<= 0 r479a) (<= r479a 1000))
    (and (<= 0 r479b) (<= r479b 1000))
    (and (<= 0 r480) (<= r480 1000))
    (and (<= 0 r481a) (<= r481a 1000))
    (and (<= 0 r481b) (<= r481b 1000))
    (and (<= 0 r482) (<= r482 1000))
    (and (<= 0 r483) (<= r483 1000))
    (and (<= 0 r484) (<= r484 1000))
    (and (<= 0 r485) (<= r485 1000))
    (and (<= 0 r486) (<= r486 1000))
    (and (<= 0 r487a) (<= r487a 1000))
    (and (<= 0 r487b) (<= r487b 1000))
    (and (<= 0 r488a) (<= r488a 1000))
    (and (<= 0 r488b) (<= r488b 1000))
    (and (<= 0 r489a) (<= r489a 1000))
    (and (<= 0 r489b) (<= r489b 1000))
    (and (<= 0 r490a) (<= r490a 1000))
    (and (<= 0 r490b) (<= r490b 1000))
    (and (<= 0 r491a) (<= r491a 1000))
    (and (<= 0 r491b) (<= r491b 1000))
    (and (<= 0 r492a) (<= r492a 1000))
    (and (<= 0 r492b) (<= r492b 1000))
    (and (<= 0 r493) (<= r493 1000))
    (and (<= 0 r494a) (<= r494a 1000))
    (and (<= 0 r494b) (<= r494b 1000))
    (and (<= 0 r495) (<= r495 1000))
    (and (<= 0 r496) (<= r496 1000))
    (and (<= 0 r497) (<= r497 1000))
    (and (<= 0 r498a) (<= r498a 1000))
    (and (<= 0 r498b) (<= r498b 1000))
    (and (<= 0 r499) (<= r499 1000))
    (and (<= 0 r500) (<= r500 1000))
    (and (<= 0 r501a) (<= r501a 1000))
    (and (<= 0 r501b) (<= r501b 1000))
    (and (<= 0 r502) (<= r502 1000))
    (and (<= 0 r503a) (<= r503a 1000))
    (and (<= 0 r503b) (<= r503b 1000))
    (and (<= 0 r504a) (<= r504a 1000))
    (and (<= 0 r504b) (<= r504b 1000))
    (and (<= 0 r505a) (<= r505a 1000))
    (and (<= 0 r505b) (<= r505b 1000))
    (and (<= 0 r506a) (<= r506a 1000))
    (and (<= 0 r506b) (<= r506b 1000))
    (and (<= 0 r507) (<= r507 1000))
    (and (<= 0 r508) (<= r508 1000))
    (and (<= 0 r509) (<= r509 1000))
    (and (<= 0 r510) (<= r510 1000))
    (and (<= 0 r511) (<= r511 1000))
    (and (<= 0 r512) (<= r512 1000))
    (and (<= 0 r513) (<= r513 1000))
    (and (<= 0 r514) (<= r514 1000))
    (and (<= 0 r515) (<= r515 1000))
    (and (<= 0 r516a) (<= r516a 1000))
    (and (<= 0 r516b) (<= r516b 1000))
    (and (<= 0 r517a) (<= r517a 1000))
    (and (<= 0 r517b) (<= r517b 1000))
    (and (<= 0 r518a) (<= r518a 1000))
    (and (<= 0 r518b) (<= r518b 1000))
    (and (<= 0 r519a) (<= r519a 1000))
    (and (<= 0 r519b) (<= r519b 1000))
    (and (<= 0 r520) (<= r520 1000))
    (and (<= 0 r521) (<= r521 1000))
    (and (<= 0 r522) (<= r522 1000))
    (and (<= 0 r523) (<= r523 1000))
    (and (<= 0 r524) (<= r524 1000))
    (and (<= 0 r525) (<= r525 1000))
    (and (<= 0 r526) (<= r526 1000))
    (and (<= 0 r527) (<= r527 1000))
    (and (<= 0 r528) (<= r528 1000))
    (and (<= 0 r529) (<= r529 1000))
    (and (<= 0 r530) (<= r530 1000))
    (and (<= 0 r531) (<= r531 1000))
    (and (<= 0 r532) (<= r532 1000))
    (and (<= 0 r533) (<= r533 1000))
    (and (<= 0 r534) (<= r534 1000))
    (and (<= 0 r535) (<= r535 1000))
    (and (<= 0 r536a) (<= r536a 1000))
    (and (<= 0 r536b) (<= r536b 1000))
    (and (<= 0 r537) (<= r537 1000))
    (and (<= 0 r538) (<= r538 1000))
    (and (<= 0 r539) (<= r539 1000))
    (and (<= 0 r540) (<= r540 1000))
    (and (<= 0 r541) (<= r541 1000))
    (and (<= 0 r542) (<= r542 1000))
    (and (<= 0 r543) (<= r543 1000))
    (and (<= 0 r544) (<= r544 1000))
    (and (<= 0 r545) (<= r545 1000))
    (and (<= 0 r546) (<= r546 1000))
    (and (<= 0 r547) (<= r547 1000))
    (and (<= 0 r548) (<= r548 1000))
    (and (<= 0 r549) (<= r549 1000))
    (and (<= 0 r550a) (<= r550a 1000))
    (and (<= 0 r550b) (<= r550b 1000))
    (and (<= 0 r551) (<= r551 1000))
    (and (<= 0 r552) (<= r552 1000))
    (and (<= 0 r553) (<= r553 1000))
    (and (<= 0 r554) (<= r554 1000))
    (and (<= 0 r555) (<= r555 1000))
    (and (<= 0 r556) (<= r556 1000))
    (and (<= 0 r557) (<= r557 1000))
    (and (<= 0 r558) (<= r558 1000))
    (and (<= 0 r559) (<= r559 1000))
    (and (<= 0 r560) (<= r560 1000))
    (and (<= 0 r561) (<= r561 1000))
    (and (<= 0 r562) (<= r562 1000))
    (and (<= 0 r563) (<= r563 1000))
    (and (<= 0 r564a) (<= r564a 1000))
    (and (<= 0 r564b) (<= r564b 1000))
    (and (<= 0 r565) (<= r565 1000))
    (and (<= 0 r566a) (<= r566a 1000))
    (and (<= 0 r566b) (<= r566b 1000))
    (and (<= 0 r567a) (<= r567a 1000))
    (and (<= 0 r567b) (<= r567b 1000))
    (and (<= 0 r568) (<= r568 1000))
    (and (<= 0 r569a) (<= r569a 1000))
    (and (<= 0 r569b) (<= r569b 1000))
    (and (<= 0 r570) (<= r570 1000))
    (and (<= 0 r571) (<= r571 1000))
    (and (<= 0 r572) (<= r572 1000))
    (and (<= 0 r573) (<= r573 1000))
    (and (<= 0 r574) (<= r574 1000))
    (and (<= 0 r575) (<= r575 1000))
    (and (<= 0 r576) (<= r576 1000))
    (and (<= 0 r577) (<= r577 1000))
    (and (<= 0 r578) (<= r578 1000))
    (and (<= 0 r579) (<= r579 1000))
    (and (<= 0 r580a) (<= r580a 1000))
    (and (<= 0 r580b) (<= r580b 1000))
    (and (<= 0 r581) (<= r581 1000))
    (and (<= 0 r582) (<= r582 1000))
    (and (<= 0 r583) (<= r583 1000))
    (and (<= 0 r584) (<= r584 1000))
    (and (<= 0 r585) (<= r585 1000))
    (and (<= 0 r586) (<= r586 1000))
    (and (<= 0 r587) (<= r587 1000))
    (and (<= 0 r588) (<= r588 1000))
    (and (<= 0 r589) (<= r589 1000))
    (and (<= 0 r590) (<= r590 1000))
    (and (<= 0 r591) (<= r591 1000))
    (and (<= 0 r592) (<= r592 1000))
    (and (<= 0 r593) (<= r593 1000))
    (and (<= 0 r594) (<= r594 1000))
    (and (<= 0 r595) (<= r595 1000))
    (and (<= 0 r596) (<= r596 1000))
    (and (<= 0 r597) (<= r597 1000))
    (and (<= 0 r598) (<= r598 1000))
    (and (<= 0 r599) (<= r599 1000))
    (and (<= 0 r600a) (<= r600a 1000))
    (and (<= 0 r600b) (<= r600b 1000))
    (and (<= 0 r601) (<= r601 1000))
    (and (<= 0 r602a) (<= r602a 1000))
    (and (<= 0 r602b) (<= r602b 1000))
    (and (<= 0 r603) (<= r603 1000))
    (and (<= 0 r604) (<= r604 1000))
    (and (<= 0 r605) (<= r605 1000))
    (and (<= 0 r606a) (<= r606a 1000))
    (and (<= 0 r606b) (<= r606b 1000))
    (and (<= 0 r607a) (<= r607a 1000))
    (and (<= 0 r607b) (<= r607b 1000))
    (and (<= 0 r608) (<= r608 1000))
    (and (<= 0 r609) (<= r609 1000))
    (and (<= 0 r610) (<= r610 1000))
    (and (<= 0 r611a) (<= r611a 1000))
    (and (<= 0 r611b) (<= r611b 1000))
    (and (<= 0 r612) (<= r612 1000))
    (and (<= 0 r613a) (<= r613a 1000))
    (and (<= 0 r613b) (<= r613b 1000))
    (and (<= 0 r614a) (<= r614a 1000))
    (and (<= 0 r614b) (<= r614b 1000))
    (and (<= 0 r618) (<= r618 1000))
    (and (<= 0 r619a) (<= r619a 1000))
    (and (<= 0 r619b) (<= r619b 1000))
    (and (<= 0 r620) (<= r620 1000))
    (and (<= 0 r621a) (<= r621a 1000))
    (and (<= 0 r621b) (<= r621b 1000))
    (and (<= 0 r622a) (<= r622a 1000))
    (and (<= 0 r622b) (<= r622b 1000))
    (and (<= 0 r623a) (<= r623a 1000))
    (and (<= 0 r623b) (<= r623b 1000))
    (and (<= 0 r624a) (<= r624a 1000))
    (and (<= 0 r624b) (<= r624b 1000))
    (and (<= 0 r625) (<= r625 1000))
    (and (<= 0 r626) (<= r626 1000))
    (and (<= 0 r632a) (<= r632a 1000))
    (and (<= 0 r632b) (<= r632b 1000))
    (and (<= 0 r633a) (<= r633a 1000))
    (and (<= 0 r633b) (<= r633b 1000))
    (and (<= 0 r634a) (<= r634a 1000))
    (and (<= 0 r634b) (<= r634b 1000))
    (and (<= 0 r635) (<= r635 1000))
    (and (<= 0 r636a) (<= r636a 1000))
    (and (<= 0 r636b) (<= r636b 1000))
    (and (<= 0 r637) (<= r637 1000))
    (and (<= 0 r638) (<= r638 1000))
    (and (<= 0 r639) (<= r639 1000))
    (and (<= 0 r640) (<= r640 1000))
    (and (<= 0 r641a) (<= r641a 1000))
    (and (<= 0 r641b) (<= r641b 1000))
    (and (<= 0 r642a) (<= r642a 1000))
    (and (<= 0 r642b) (<= r642b 1000))
    (and (<= 0 r643a) (<= r643a 1000))
    (and (<= 0 r643b) (<= r643b 1000))
    (and (<= 0 r644a) (<= r644a 1000))
    (and (<= 0 r644b) (<= r644b 1000))
    (and (<= 0 r645a) (<= r645a 1000))
    (and (<= 0 r645b) (<= r645b 1000))
    (and (<= 0 r646a) (<= r646a 1000))
    (and (<= 0 r646b) (<= r646b 1000))
    (and (<= 0 r647a) (<= r647a 1000))
    (and (<= 0 r647b) (<= r647b 1000))
    (and (<= 0 r648) (<= r648 1000))
    (and (<= 0 r649) (<= r649 1000))
    (and (<= 0 r650a) (<= r650a 1000))
    (and (<= 0 r650b) (<= r650b 1000))
    (and (<= 0 r651a) (<= r651a 1000))
    (and (<= 0 r651b) (<= r651b 1000))
    (and (<= 0 r652a) (<= r652a 1000))
    (and (<= 0 r652b) (<= r652b 1000))
    (and (<= 0 r653) (<= r653 1000))
    (and (<= 0 r657) (<= r657 1000))
    (and (<= 0 r658a) (<= r658a 1000))
    (and (<= 0 r658b) (<= r658b 1000))
    (and (<= 0 r662) (<= r662 1000))
    (and (<= 0 r663) (<= r663 1000))
    (and (<= 0 r664) (<= r664 1000))
    (and (<= 0 r668) (<= r668 1000))
    (and (<= 0 r674a) (<= r674a 1000))
    (and (<= 0 r674b) (<= r674b 1000))
    (and (<= 0 r687a) (<= r687a 1000))
    (and (<= 0 r687b) (<= r687b 1000))
    (and (<= 0 r688a) (<= r688a 1000))
    (and (<= 0 r688b) (<= r688b 1000))
    (and (<= 0 r689) (<= r689 1000))
    (and (<= 0 r690) (<= r690 1000))
    (and (<= 0 r691) (<= r691 1000))
    (and (<= 0 r692) (<= r692 1000))
    (and (<= 0 r693) (<= r693 1000))
    (and (<= 0 r694) (<= r694 1000))
    (and (<= 0 r695) (<= r695 1000))
    (and (<= 0 r696a) (<= r696a 1000))
    (and (<= 0 r696b) (<= r696b 1000))
    (and (<= 0 r697a) (<= r697a 1000))
    (and (<= 0 r697b) (<= r697b 1000))
    (and (<= 0 r698a) (<= r698a 1000))
    (and (<= 0 r698b) (<= r698b 1000))
    (and (<= 0 r699a) (<= r699a 1000))
    (and (<= 0 r699b) (<= r699b 1000))
    (and (<= 0 r700a) (<= r700a 1000))
    (and (<= 0 r700b) (<= r700b 1000))
    (and (<= 0 r701a) (<= r701a 1000))
    (and (<= 0 r701b) (<= r701b 1000))
    (and (<= 0 r702a) (<= r702a 1000))
    (and (<= 0 r702b) (<= r702b 1000))
    (and (<= 0 r703) (<= r703 1000))
    (and (<= 0 r704a) (<= r704a 1000))
    (and (<= 0 r704b) (<= r704b 1000))
    (and (<= 0 r705) (<= r705 1000))
    (and (<= 0 r706) (<= r706 1000))
    (and (<= 0 r707) (<= r707 1000))
    (and (<= 0 r708) (<= r708 1000))
    (and (<= 0 r709) (<= r709 1000))
    (and (<= 0 r710) (<= r710 1000))
    (and (<= 0 r711) (<= r711 1000))
    (and (<= 0 r712) (<= r712 1000))
    (and (<= 0 r713) (<= r713 1000))
    (and (<= 0 r714) (<= r714 1000))
    (and (<= 0 r715) (<= r715 1000))
    (and (<= 0 r716) (<= r716 1000))
    (and (<= 0 r717a) (<= r717a 1000))
    (and (<= 0 r717b) (<= r717b 1000))
    (and (<= 0 r718) (<= r718 1000))
    (and (<= 0 r719) (<= r719 1000))
    (and (<= 0 r720) (<= r720 1000))
    (and (<= 0 r721) (<= r721 1000))
    (and (<= 0 r722) (<= r722 1000))
    (and (<= 0 r723) (<= r723 1000))
    (and (<= 0 r724a) (<= r724a 1000))
    (and (<= 0 r724b) (<= r724b 1000))
    (and (<= 0 r725) (<= r725 1000))
    (and (<= 0 r726) (<= r726 1000))
    (and (<= 0 r727) (<= r727 1000))
    (and (<= 0 r728a) (<= r728a 1000))
    (and (<= 0 r728b) (<= r728b 1000))
    (and (<= 0 r729) (<= r729 1000))
    (and (<= 0 r730) (<= r730 1000))
    (and (<= 0 r731) (<= r731 1000))
    (and (<= 0 r732) (<= r732 1000))
    (and (<= 0 r733a) (<= r733a 1000))
    (and (<= 0 r733b) (<= r733b 1000))
    (and (<= 0 r734) (<= r734 1000))
    (and (<= 0 r735) (<= r735 1000))
    (and (<= 0 r736) (<= r736 1000))
    (and (<= 0 r737a) (<= r737a 1000))
    (and (<= 0 r737b) (<= r737b 1000))
    (and (<= 0 r738a) (<= r738a 1000))
    (and (<= 0 r738b) (<= r738b 1000))
    (and (<= 0 r739) (<= r739 1000))
    (and (<= 0 r740a) (<= r740a 1000))
    (and (<= 0 r740b) (<= r740b 1000))
    (and (<= 0 r741a) (<= r741a 1000))
    (and (<= 0 r741b) (<= r741b 1000))
    (and (<= 0 r742) (<= r742 1000))
    (and (<= 0 r743) (<= r743 1000))
    (and (<= 0 r744a) (<= r744a 1000))
    (and (<= 0 r744b) (<= r744b 1000))
    (and (<= 0 r745) (<= r745 1000))
    (and (<= 0 r746) (<= r746 1000))
    (and (<= 0 r747) (<= r747 1000))
    (and (<= 0 r748) (<= r748 1000))
    (and (<= 0 r749) (<= r749 1000))
    (and (<= 0 r750) (<= r750 1000))
    (and (<= 0 r751) (<= r751 1000))
    (and (<= 0 r752) (<= r752 1000))
    (and (<= 0 r753a) (<= r753a 1000))
    (and (<= 0 r753b) (<= r753b 1000))
    (and (<= 0 r754) (<= r754 1000))
    (and (<= 0 r755a) (<= r755a 1000))
    (and (<= 0 r755b) (<= r755b 1000))
    (and (<= 0 r756) (<= r756 1000))
    (and (<= 0 r757a) (<= r757a 1000))
    (and (<= 0 r757b) (<= r757b 1000))
    (and (<= 0 r758) (<= r758 1000))
    (and (<= 0 r759) (<= r759 1000))
    (and (<= 0 r760a) (<= r760a 1000))
    (and (<= 0 r760b) (<= r760b 1000))
    (and (<= 0 r761a) (<= r761a 1000))
    (and (<= 0 r761b) (<= r761b 1000))
    (and (<= 0 r762) (<= r762 1000))
    (and (<= 0 r763) (<= r763 1000))
    (and (<= 0 r764a) (<= r764a 1000))
    (and (<= 0 r764b) (<= r764b 1000))
    (and (<= 0 r765a) (<= r765a 1000))
    (and (<= 0 r765b) (<= r765b 1000))
    (and (<= 0 r766a) (<= r766a 1000))
    (and (<= 0 r766b) (<= r766b 1000))
    (and (<= 0 r767) (<= r767 1000))
    (and (<= 0 r768a) (<= r768a 1000))
    (and (<= 0 r768b) (<= r768b 1000))
    (and (<= 0 r769) (<= r769 1000))
    (and (<= 0 r770) (<= r770 1000))
    (and (<= 0 r771) (<= r771 1000))
    (and (<= 0 r772) (<= r772 1000))
    (and (<= 0 r773) (<= r773 1000))
    (and (<= 0 r774) (<= r774 1000))
    (and (<= 0 r775) (<= r775 1000))
    (and (<= 0 r776) (<= r776 1000))
    (and (<= 0 r777) (<= r777 1000))
    (and (<= 0 r778a) (<= r778a 1000))
    (and (<= 0 r778b) (<= r778b 1000))
    (and (<= 0 r779) (<= r779 1000))
    (and (<= 0 r780) (<= r780 1000))
    (and (<= 0 r781) (<= r781 1000))
    (and (<= 0 r782) (<= r782 1000))
    (and (<= 0 r783) (<= r783 1000))
    (and (<= 0 r784) (<= r784 1000))
    (and (<= 0 r785a) (<= r785a 1000))
    (and (<= 0 r785b) (<= r785b 1000))
    (and (<= 0 r786) (<= r786 1000))
    (and (<= 0 r787) (<= r787 1000))
    (and (<= 0 r788) (<= r788 1000))
    (and (<= 0 r789) (<= r789 1000))
    (and (<= 0 r790a) (<= r790a 1000))
    (and (<= 0 r790b) (<= r790b 1000))
    (and (<= 0 r791) (<= r791 1000))
    (and (<= 0 r792) (<= r792 1000))
    (and (<= 0 r793) (<= r793 1000))
    (and (<= 0 r794) (<= r794 1000))
    (and (<= 0 r795) (<= r795 1000))
    (and (<= 0 r796) (<= r796 1000))
    (and (<= 0 r797) (<= r797 1000))
    (and (<= 0 r798a) (<= r798a 1000))
    (and (<= 0 r798b) (<= r798b 1000))
    (and (<= 0 r799a) (<= r799a 1000))
    (and (<= 0 r799b) (<= r799b 1000))
    (and (<= 0 r800a) (<= r800a 1000))
    (and (<= 0 r800b) (<= r800b 1000))
    (and (<= 0 r801a) (<= r801a 1000))
    (and (<= 0 r801b) (<= r801b 1000))
    (and (<= 0 r802a) (<= r802a 1000))
    (and (<= 0 r802b) (<= r802b 1000))
    (and (<= 0 r803) (<= r803 1000))
    (and (<= 0 r804) (<= r804 1000))
    (and (<= 0 r805) (<= r805 1000))
    (and (<= 0 r806) (<= r806 1000))
    (and (<= 0 r807a) (<= r807a 1000))
    (and (<= 0 r807b) (<= r807b 1000))
    (and (<= 0 r808) (<= r808 1000))
    (and (<= 0 r809a) (<= r809a 1000))
    (and (<= 0 r809b) (<= r809b 1000))
    (and (<= 0 r810) (<= r810 1000))
    (and (<= 0 r811) (<= r811 1000))
    (and (<= 0 r812) (<= r812 1000))
    (and (<= 0 r813) (<= r813 1000))
    (and (<= 0 r814) (<= r814 1000))
    (and (<= 0 r815) (<= r815 1000))
    (and (<= 0 r816) (<= r816 1000))
    (and (<= 0 r817a) (<= r817a 1000))
    (and (<= 0 r817b) (<= r817b 1000))
    (and (<= 0 r818) (<= r818 1000))
    (and (<= 0 r819a) (<= r819a 1000))
    (and (<= 0 r819b) (<= r819b 1000))
    (and (<= 0 r820) (<= r820 1000))
    (and (<= 0 r821) (<= r821 1000))
    (and (<= 0 r822) (<= r822 1000))
    (and (<= 0 r823) (<= r823 1000))
    (and (<= 0 r824a) (<= r824a 1000))
    (and (<= 0 r824b) (<= r824b 1000))
    (and (<= 0 r825) (<= r825 1000))
    (and (<= 0 r826) (<= r826 1000))
    (and (<= 0 r827) (<= r827 1000))
    (and (<= 0 r828) (<= r828 1000))
    (and (<= 0 r829a) (<= r829a 1000))
    (and (<= 0 r829b) (<= r829b 1000))
    (and (<= 0 r830) (<= r830 1000))
    (and (<= 0 r831) (<= r831 1000))
    (and (<= 0 r832) (<= r832 1000))
    (and (<= 0 r833) (<= r833 1000))
    (and (<= 0 r834a) (<= r834a 1000))
    (and (<= 0 r834b) (<= r834b 1000))
    (and (<= 0 r835) (<= r835 1000))
    (and (<= 0 r836) (<= r836 1000))
    (and (<= 0 r837a) (<= r837a 1000))
    (and (<= 0 r837b) (<= r837b 1000))
    (and (<= 0 r838) (<= r838 1000))
    (and (<= 0 r839a) (<= r839a 1000))
    (and (<= 0 r839b) (<= r839b 1000))
    (and (<= 0 r840) (<= r840 1000))
    (and (<= 0 r841) (<= r841 1000))
    (and (<= 0 r842) (<= r842 1000))
    (and (<= 0 r843) (<= r843 1000))
    (and (<= 0 r844) (<= r844 1000))
    (and (<= 0 r845) (<= r845 1000))
    (and (<= 0 r846) (<= r846 1000))
    (and (<= 0 r847a) (<= r847a 1000))
    (and (<= 0 r847b) (<= r847b 1000))
    (and (<= 0 r848) (<= r848 1000))
    (and (<= 0 r849a) (<= r849a 1000))
    (and (<= 0 r849b) (<= r849b 1000))
    (and (<= 0 r850) (<= r850 1000))
    (and (<= 0 r851) (<= r851 1000))
    (and (<= 0 r852) (<= r852 1000))
    (and (<= 0 r853a) (<= r853a 1000))
    (and (<= 0 r853b) (<= r853b 1000))
    (and (<= 0 r854) (<= r854 1000))
    (and (<= 0 r855) (<= r855 1000))
    (and (<= 0 r856a) (<= r856a 1000))
    (and (<= 0 r856b) (<= r856b 1000))
    (and (<= 0 r857a) (<= r857a 1000))
    (and (<= 0 r857b) (<= r857b 1000))
    (and (<= 0 r858) (<= r858 1000))
    (and (<= 0 r859a) (<= r859a 1000))
    (and (<= 0 r859b) (<= r859b 1000))
    (and (<= 0 r860a) (<= r860a 1000))
    (and (<= 0 r860b) (<= r860b 1000))
    (and (<= 0 r861) (<= r861 1000))
    (and (<= 0 r862) (<= r862 1000))
    (and (<= 0 r863) (<= r863 1000))
    (and (<= 0 r864) (<= r864 1000))
    (and (<= 0 r865) (<= r865 1000))
    (and (<= 0 r866) (<= r866 1000))
    (and (<= 0 r867) (<= r867 1000))
    (and (<= 0 r870) (<= r870 1000))
    (and (<= 0 r871) (<= r871 1000))
    (and (<= 0 r872) (<= r872 1000))
    (and (<= 0 r873a) (<= r873a 1000))
    (and (<= 0 r873b) (<= r873b 1000))
    (and (<= 0 r874a) (<= r874a 1000))
    (and (<= 0 r874b) (<= r874b 1000))
    (and (<= 0 r875a) (<= r875a 1000))
    (and (<= 0 r875b) (<= r875b 1000))
    (and (<= 0 r876a) (<= r876a 1000))
    (and (<= 0 r876b) (<= r876b 1000))
    (and (<= 0 r877a) (<= r877a 1000))
    (and (<= 0 r877b) (<= r877b 1000))
    (and (<= 0 r878) (<= r878 1000))
    (and (<= 0 r879a) (<= r879a 1000))
    (and (<= 0 r879b) (<= r879b 1000))
    (and (<= 0 r880) (<= r880 1000))
    (and (<= 0 r881) (<= r881 1000))
    (and (<= 0 r882) (<= r882 1000))
    (and (<= 0 r883) (<= r883 1000))
    (and (<= 0 r884a) (<= r884a 1000))
    (and (<= 0 r884b) (<= r884b 1000))
    (and (<= 0 r885) (<= r885 1000))
    (and (<= 0 r886) (<= r886 1000))
    (and (<= 0 r887) (<= r887 1000))
    (and (<= 0 r888) (<= r888 1000))
    (and (<= 0 r889) (<= r889 1000))
    (and (<= 0 r890) (<= r890 1000))
    (and (<= 0 r891a) (<= r891a 1000))
    (and (<= 0 r891b) (<= r891b 1000))
    (and (<= 0 r892a) (<= r892a 1000))
    (and (<= 0 r892b) (<= r892b 1000))
    (and (<= 0 r893) (<= r893 1000))
    (and (<= 0 r894) (<= r894 1000))
    (and (<= 0 r895) (<= r895 1000))
    (and (<= 0 r896) (<= r896 1000))
    (and (<= 0 r897) (<= r897 1000))
    (and (<= 0 r898) (<= r898 1000))
    (and (<= 0 r899) (<= r899 1000))
    (and (<= 0 r900) (<= r900 1000))
    (and (<= 0 r901) (<= r901 1000))
    (and (<= 0 r902) (<= r902 1000))
    (and (<= 0 r903) (<= r903 1000))
    (and (<= 0 r904a) (<= r904a 1000))
    (and (<= 0 r904b) (<= r904b 1000))
    (and (<= 0 r905) (<= r905 1000))
    (and (<= 0 r906) (<= r906 1000))
    (and (<= 0 r907a) (<= r907a 1000))
    (and (<= 0 r907b) (<= r907b 1000))
    (and (<= 0 r908) (<= r908 1000))
    (and (<= 0 r909) (<= r909 1000))
    (and (<= 0 r910) (<= r910 1000))
    (and (<= 0 r911) (<= r911 1000))
    (and (<= 0 r912) (<= r912 1000))
    (and (<= 0 r913) (<= r913 1000))
    (and (<= 0 r914) (<= r914 1000))
    (and (<= 0 r915) (<= r915 1000))
    (and (<= 0 r916) (<= r916 1000))
    (and (<= 0 r917a) (<= r917a 1000))
    (and (<= 0 r917b) (<= r917b 1000))

    (or (= s1_obj 0) (= s1_obj 1))
    (or (= s2_obj 0) (= s2_obj 1))
    (or (= s3_obj 0) (= s3_obj 1))
    (or (= s4_obj 0) (= s4_obj 1))
    (or (= s5_obj 0) (= s5_obj 1))
    (or (= s6_obj 0) (= s6_obj 1))
    (or (= s7_obj 0) (= s7_obj 1))
    (or (= s8_obj 0) (= s8_obj 1))
    (or (= s9_obj 0) (= s9_obj 1))
    (or (= s10_obj 0) (= s10_obj 1))
    (or (= s11_obj 0) (= s11_obj 1))
    (or (= s12_obj 0) (= s12_obj 1))
    (or (= s13_obj 0) (= s13_obj 1))
    (or (= s14_obj 0) (= s14_obj 1))
    (or (= s15_obj 0) (= s15_obj 1))
    (or (= s16_obj 0) (= s16_obj 1))
    (or (= s17_obj 0) (= s17_obj 1))
    (or (= s18_obj 0) (= s18_obj 1))
    (or (= s19_obj 0) (= s19_obj 1))
    (or (= s20_obj 0) (= s20_obj 1))
    (or (= s21_obj 0) (= s21_obj 1))
    (or (= s22_obj 0) (= s22_obj 1))
    (or (= s23_obj 0) (= s23_obj 1))
    (or (= s24_obj 0) (= s24_obj 1))
    (or (= s25_obj 0) (= s25_obj 1))
    (or (= s26_obj 0) (= s26_obj 1))
    (or (= s27_obj 0) (= s27_obj 1))
    (or (= s29_obj 0) (= s29_obj 1))
    (or (= s31_obj 0) (= s31_obj 1))
    (or (= s32_obj 0) (= s32_obj 1))
    (or (= s33_obj 0) (= s33_obj 1))
    (or (= s34_obj 0) (= s34_obj 1))
    (or (= s35_obj 0) (= s35_obj 1))
    (or (= s36_obj 0) (= s36_obj 1))
    (or (= s37_obj 0) (= s37_obj 1))
    (or (= s38_nutr 0) (= s38_nutr 1))
    (or (= s39_nutr 0) (= s39_nutr 1))
    (or (= s40_nutr 0) (= s40_nutr 1))
    (or (= s41_nutr 0) (= s41_nutr 1))
    (or (= s42_nutr 0) (= s42_nutr 1))
    (or (= s43_nutr 0) (= s43_nutr 1))
    (or (= s44_nutr 0) (= s44_nutr 1))
    (or (= s45_nutr 0) (= s45_nutr 1))
    (or (= s46_nutr 0) (= s46_nutr 1))
    (or (= s47_nutr 0) (= s47_nutr 1))
    (or (= s48_nutr 0) (= s48_nutr 1))
    (or (= s49_nutr 0) (= s49_nutr 1))
    (or (= s50_nutr 0) (= s50_nutr 1))
    (or (= s51_nutr 0) (= s51_nutr 1))
    (or (= s52_secrt 0) (= s52_secrt 1))
    (or (= s53_secrt 0) (= s53_secrt 1))
    (or (= s54_secrt 0) (= s54_secrt 1))

    (and (>= s1_obj 0) (<= s1_obj 1))
    (and (>= s2_obj 0) (<= s2_obj 1))
    (and (>= s3_obj 0) (<= s3_obj 1))
    (and (>= s4_obj 0) (<= s4_obj 1))
    (and (>= s5_obj 0) (<= s5_obj 1))
    (and (>= s6_obj 0) (<= s6_obj 1))
    (and (>= s7_obj 0) (<= s7_obj 1))
    (and (>= s8_obj 0) (<= s8_obj 1))
    (and (>= s9_obj 0) (<= s9_obj 1))
    (and (>= s10_obj 0) (<= s10_obj 1))
    (and (>= s11_obj 0) (<= s11_obj 1))
    (and (>= s12_obj 0) (<= s12_obj 1))
    (and (>= s13_obj 0) (<= s13_obj 1))
    (and (>= s14_obj 0) (<= s14_obj 1))
    (and (>= s15_obj 0) (<= s15_obj 1))
    (and (>= s16_obj 0) (<= s16_obj 1))
    (and (>= s17_obj 0) (<= s17_obj 1))
    (and (>= s18_obj 0) (<= s18_obj 1))
    (and (>= s19_obj 0) (<= s19_obj 1))
    (and (>= s20_obj 0) (<= s20_obj 1))
    (and (>= s21_obj 0) (<= s21_obj 1))
    (and (>= s22_obj 0) (<= s22_obj 1))
    (and (>= s23_obj 0) (<= s23_obj 1))
    (and (>= s24_obj 0) (<= s24_obj 1))
    (and (>= s25_obj 0) (<= s25_obj 1))
    (and (>= s26_obj 0) (<= s26_obj 1))
    (and (>= s27_obj 0) (<= s27_obj 1))
    (and (>= s29_obj 0) (<= s29_obj 1))
    (and (>= s31_obj 0) (<= s31_obj 1))
    (and (>= s32_obj 0) (<= s32_obj 1))
    (and (>= s33_obj 0) (<= s33_obj 1))
    (and (>= s34_obj 0) (<= s34_obj 1))
    (and (>= s35_obj 0) (<= s35_obj 1))
    (and (>= s36_obj 0) (<= s36_obj 1))
    (and (>= s37_obj 0) (<= s37_obj 1))
    (and (>= s38_nutr 0) (<= s38_nutr 1))
    (and (>= s39_nutr 0) (<= s39_nutr 1))
    (and (>= s40_nutr 0) (<= s40_nutr 1))
    (and (>= s41_nutr 0) (<= s41_nutr 1))
    (and (>= s42_nutr 0) (<= s42_nutr 1))
    (and (>= s43_nutr 0) (<= s43_nutr 1))
    (and (>= s44_nutr 0) (<= s44_nutr 1))
    (and (>= s45_nutr 0) (<= s45_nutr 1))
    (and (>= s46_nutr 0) (<= s46_nutr 1))
    (and (>= s47_nutr 0) (<= s47_nutr 1))
    (and (>= s48_nutr 0) (<= s48_nutr 1))
    (and (>= s49_nutr 0) (<= s49_nutr 1))
    (and (>= s50_nutr 0) (<= s50_nutr 1))
    (and (>= s51_nutr 0) (<= s51_nutr 1))
    (and (>= s52_secrt 0) (<= s52_secrt 1))
    (and (>= s53_secrt 0) (<= s53_secrt 1))
    (and (>= s54_secrt 0) (<= s54_secrt 1))
))

(define obj::real 
  (+ (* 1000 (+ s1_obj s2_obj s3_obj s4_obj s5_obj s6_obj s7_obj s8_obj s9_obj s10_obj 
                s11_obj s12_obj s13_obj s14_obj s15_obj s16_obj s17_obj s18_obj s19_obj s20_obj
                s21_obj s22_obj s23_obj s24_obj s25_obj s26_obj s27_obj s29_obj s31_obj s32_obj 
                s33_obj s34_obj s35_obj s36_obj s37_obj))
      (* -1 (+ s38_nutr s39_nutr s40_nutr s41_nutr s42_nutr s43_nutr s44_nutr s45_nutr s46_nutr 
               s47_nutr s48_nutr s49_nutr s50_nutr s51_nutr))
      (* -2 (+ s52_secrt s53_secrt s54_secrt))))


;; optimal? 19992
(assert (>= obj 19992))

(check)

(show-model)