Require Import Reals.
From Flocq Require Import Raux Zaux.
Open Scope R_scope.

Parameter c0_3_0 : R.
Conjecture c0_3_0_bound : -81269145921618583042430391564992033505071826876175016278353823877155339289680 * (bpow radix2 (Z.opp 249)) <= c0_3_0 <= -81269145921618583042430391564992033505071826876175016278353823877155323659379 * (bpow radix2 (Z.opp 249)).

Parameter c6_0_2 : R.
Conjecture c6_0_2_bound : 106359929085650127040205954262331839289155243661980008656755232693239435977523 * (bpow radix2 (Z.opp 251)) <= c6_0_2 <= 106359929085650127040205954262331839289155243661980008656755232693239435983549 * (bpow radix2 (Z.opp 251)).

Parameter c11_1_0 : R.
Conjecture c11_1_0_bound : 73520242068556346395600439408929731723120785202957940052519381625118109677564 * (bpow radix2 (Z.opp 256)) <= c11_1_0 <= 73520242068556346395600439408929731723120785202957940052519381625118109679092 * (bpow radix2 (Z.opp 256)).

Parameter c0_0_0 : R.
Conjecture c0_0_0_bound : 81327592294979367460524402001085742413676535231713531417559921351548713308616 * (bpow radix2 (Z.opp 254)) <= c0_0_0 <= 81327592294979367460524402001085742413676535231713531417559921351548714926140 * (bpow radix2 (Z.opp 254)).

Parameter c3_3_0 : R.
Conjecture c3_3_0_bound : 72344199925961912425350935240310623748679654070294904684435307627032291265849 * (bpow radix2 (Z.opp 244)) <= c3_3_0 <= 72344199925961912425350935240310623748679654070294904684435307627032291333681 * (bpow radix2 (Z.opp 244)).

Parameter c4_2_0 : R.
Conjecture c4_2_0_bound : 111419372481992856501467441439554547181355763369491755621754683944527202451520 * (bpow radix2 (Z.opp 245)) <= c4_2_0 <= 111419372481992856501467441439554547181355763369491755621754683944527203141876 * (bpow radix2 (Z.opp 245)).

Parameter c1_2_2 : R.
Conjecture c1_2_2_bound : 103297785473237531245745606901215604100854317864004723887434989648576496652461 * (bpow radix2 (Z.opp 248)) <= c1_2_2 <= 103297785473237531245745606901215604100854317864004723887434989648576496676346 * (bpow radix2 (Z.opp 248)).

Parameter c2_0_1 : R.
Conjecture c2_0_1_bound : -84505188544718232628776539531405165805120711220972944303063158283616274911778 * (bpow radix2 (Z.opp 248)) <= c2_0_1 <= -84505188544718232628776539531405165805120711220972944303063158283616236793405 * (bpow radix2 (Z.opp 248)).

Parameter c7_2_0 : R.
Conjecture c7_2_0_bound : -107818038376425632687975410330883771784605035791225696830717065562151695374725 * (bpow radix2 (Z.opp 247)) <= c7_2_0 <= -107818038376425632687975410330883771784605035791225696830717065562151695366448 * (bpow radix2 (Z.opp 247)).

Parameter c8_1_0 : R.
Conjecture c8_1_0_bound : -74726828451689200141902901763579337830436930672231996163917023006073022190556 * (bpow radix2 (Z.opp 246)) <= c8_1_0 <= -74726828451689200141902901763579337830436930672231996163917023006073022178669 * (bpow radix2 (Z.opp 246)).

Parameter c4_0_0 : R.
Conjecture c4_0_0_bound : 84703640380074280628008805374788957463574550420907310053864484482532342810703 * (bpow radix2 (Z.opp 247)) <= c4_0_0 <= 84703640380074280628008805374788957463574550420907310053864484482532346075298 * (bpow radix2 (Z.opp 247)).

Parameter c1_0_2 : R.
Conjecture c1_0_2_bound : 59354693492952999739822328718746058006980604015240271067097629024505563135698 * (bpow radix2 (Z.opp 246)) <= c1_0_2 <= 59354693492952999739822328718746058006980604015240271067097629024505565949616 * (bpow radix2 (Z.opp 246)).

Parameter c4_0_3 : R.
Conjecture c4_0_3_bound : 98872743753191691682869933544755741529683304585843925882340864171659984145760 * (bpow radix2 (Z.opp 259)) <= c4_0_3 <= 98872743753191691682869933544755741529683304585843925882340864171659984232736 * (bpow radix2 (Z.opp 259)).

Parameter c1_3_1 : R.
Conjecture c1_3_1_bound : 103559275962656758516499245602405022667825297757805916585983101414113727338088 * (bpow radix2 (Z.opp 252)) <= c1_3_1 <= 103559275962656758516499245602405022667825297757805916585983101414113729470552 * (bpow radix2 (Z.opp 252)).

Parameter c8_0_0 : R.
Conjecture c8_0_0_bound : 63444729197369289696711331604021608418610390446636557307335287328178916068326 * (bpow radix2 (Z.opp 248)) <= c8_0_0 <= 63444729197369289696711331604021608418610390446636557307335287328178916310585 * (bpow radix2 (Z.opp 248)).

Parameter c0_3_1 : R.
Conjecture c0_3_1_bound : 66963650415554180396129431216452996456753808196997605237347771334124234988848 * (bpow radix2 (Z.opp 251)) <= c0_3_1 <= 66963650415554180396129431216452996456753808196997605237347771334124240592883 * (bpow radix2 (Z.opp 251)).

Parameter c2_1_3 : R.
Conjecture c2_1_3_bound : -90467208805202681381556755525831300716712956178155990481099351892611763008201 * (bpow radix2 (Z.opp 253)) <= c2_1_3 <= -90467208805202681381556755525831300716712956178155990481099351892611763005587 * (bpow radix2 (Z.opp 253)).

Parameter c6_3_0 : R.
Conjecture c6_3_0_bound : -76543526201569302253652343310675264846842462037925076781185031754881043279000 * (bpow radix2 (Z.opp 253)) <= c6_3_0 <= -76543526201569302253652343310675264846842462037925076781185031754881043202880 * (bpow radix2 (Z.opp 253)).

Parameter c3_1_2 : R.
Conjecture c3_1_2_bound : 79880199542213674568478929768435744615907101079989488484616330102540999400608 * (bpow radix2 (Z.opp 246)) <= c3_1_2 <= 79880199542213674568478929768435744615907101079989488484616330102540999412788 * (bpow radix2 (Z.opp 246)).

Parameter c1_1_0 : R.
Conjecture c1_1_0_bound : 93684016374816784119083898853539446040695283879119376733634999204677146245171 * (bpow radix2 (Z.opp 248)) <= c1_1_0 <= 93684016374816784119083898853539446040695283879119376733634999204677153235784 * (bpow radix2 (Z.opp 248)).

Parameter c2_0_3 : R.
Conjecture c2_0_3_bound : -86006118112143050500314572183966479631910912207782655202825037274032965009047 * (bpow radix2 (Z.opp 248)) <= c2_0_3 <= -86006118112143050500314572183966479631910912207782655202825037274032964995867 * (bpow radix2 (Z.opp 248)).

Parameter c12_0_0 : R.
Conjecture c12_0_0_bound : 63502421815358520831150870183542447137001017757845090789558443714612039121983 * (bpow radix2 (Z.opp 254)) <= c12_0_0 <= 63502421815358520831150870183542447137001017757845090789558443714612039123065 * (bpow radix2 (Z.opp 254)).

Parameter c7_0_1 : R.
Conjecture c7_0_1_bound : 100617711657603703094006166960423880683506643088848216200234481766827971819925 * (bpow radix2 (Z.opp 247)) <= c7_0_1 <= 100617711657603703094006166960423880683506643088848216200234481766827971841623 * (bpow radix2 (Z.opp 247)).

Parameter c6_1_1 : R.
Conjecture c6_1_1_bound : 79194367215727838698313311762421174137487646078701008501087035153886544347971 * (bpow radix2 (Z.opp 246)) <= c6_1_1 <= 79194367215727838698313311762421174137487646078701008501087035153886544354076 * (bpow radix2 (Z.opp 246)).

Parameter c1_5_0 : R.
Conjecture c1_5_0_bound : -73471603974349544831808830297444604978438195346956900420417254008686833516780 * (bpow radix2 (Z.opp 252)) <= c1_5_0 <= -73471603974349544831808830297444604978438195346956900420417254008686833444038 * (bpow radix2 (Z.opp 252)).

Parameter c0_2_1 : R.
Conjecture c0_2_1_bound : -74874341102190746544485282108087696049789620035646697136425653786184436331807 * (bpow radix2 (Z.opp 247)) <= c0_2_1 <= -74874341102190746544485282108087696049789620035646697136425653786184431149214 * (bpow radix2 (Z.opp 247)).

Parameter c5_4_0 : R.
Conjecture c5_4_0_bound : 106721879185070704997846652261431793893569966770649960007398821318610374562450 * (bpow radix2 (Z.opp 253)) <= c5_4_0 <= 106721879185070704997846652261431793893569966770649960007398821318610374564771 * (bpow radix2 (Z.opp 253)).

Parameter c7_1_1 : R.
Conjecture c7_1_1_bound : -67000051360132791838105282191012203939574683815923532180788471541022258315102 * (bpow radix2 (Z.opp 249)) <= c7_1_1 <= -67000051360132791838105282191012203939574683815923532180788471541022258311486 * (bpow radix2 (Z.opp 249)).

Parameter c0_1_3 : R.
Conjecture c0_1_3_bound : -107051621941543727739944413793476640193788088173692451473746258856968566427760 * (bpow radix2 (Z.opp 250)) <= c0_1_3 <= -107051621941543727739944413793476640193788088173692451473746258856968566386379 * (bpow radix2 (Z.opp 250)).

Parameter c2_4_0 : R.
Conjecture c2_4_0_bound : -74210293908111250429051583726229524334302655897976866623314884750021182740556 * (bpow radix2 (Z.opp 251)) <= c2_4_0 <= -74210293908111250429051583726229524334302655897976866623314884750021181878532 * (bpow radix2 (Z.opp 251)).

Parameter c2_2_1 : R.
Conjecture c2_2_1_bound : -62374719509001640583552762113097656902145904717635864826443218363214550849212 * (bpow radix2 (Z.opp 243)) <= c2_2_1 <= -62374719509001640583552762113097656902145904717635864826443218363214550775648 * (bpow radix2 (Z.opp 243)).

Parameter c1_0_0 : R.
Conjecture c1_0_0_bound : -67459383414246974692676409338578447544535791996667960085337809947194005727123 * (bpow radix2 (Z.opp 252)) <= c1_0_0 <= -67459383414246974692676409338578447544535791996667960085337809947193996780085 * (bpow radix2 (Z.opp 252)).

Parameter c0_2_2 : R.
Conjecture c0_2_2_bound : -67406958281423035306358220994485478589431449681774442381409491596130593621728 * (bpow radix2 (Z.opp 252)) <= c0_2_2 <= -67406958281423035306358220994485478589431449681774442381409491596130591325312 * (bpow radix2 (Z.opp 252)).

Parameter c7_1_0 : R.
Conjecture c7_1_0_bound : 66936654669869109515872447823147985475919198887356861851460596688421415599254 * (bpow radix2 (Z.opp 245)) <= c7_1_0 <= 66936654669869109515872447823147985475919198887356861851460596688421415642552 * (bpow radix2 (Z.opp 245)).

Parameter c0_2_0 : R.
Conjecture c0_2_0_bound : 58677276270021455728574363926560954535457212233024092658847841847170714823254 * (bpow radix2 (Z.opp 248)) <= c0_2_0 <= 58677276270021455728574363926560954535457212233024092658847841847170730340534 * (bpow radix2 (Z.opp 248)).

Parameter c1_2_1 : R.
Conjecture c1_2_1_bound : 90578024742472996821113406862795130477868366953093334765163248123235475602376 * (bpow radix2 (Z.opp 245)) <= c1_2_1 <= 90578024742472996821113406862795130477868366953093334765163248123235476054902 * (bpow radix2 (Z.opp 245)).

Parameter c3_2_0 : R.
Conjecture c3_2_0_bound : 73507033987014597957609433270874117426045969735565884660093873655176070117544 * (bpow radix2 (Z.opp 248)) <= c3_2_0 <= 73507033987014597957609433270874117426045969735565884660093873655176083587328 * (bpow radix2 (Z.opp 248)).

Parameter c4_1_0 : R.
Conjecture c4_1_0_bound : 81459867848161035919339981159647246271455997438579909636261088223878792293832 * (bpow radix2 (Z.opp 250)) <= c4_1_0 <= 81459867848161035919339981159647246271455997438579909636261088223878868784544 * (bpow radix2 (Z.opp 250)).

Parameter c2_3_1 : R.
Conjecture c2_3_1_bound : -68363058296344909669096130037865217949650191529994024280666509035205056250914 * (bpow radix2 (Z.opp 247)) <= c2_3_1 <= -68363058296344909669096130037865217949650191529994024280666509035205056230321 * (bpow radix2 (Z.opp 247)).

Parameter c5_1_0 : R.
Conjecture c5_1_0_bound : 64078953739589607213994623384761541374699638734673762944879044788010315411964 * (bpow radix2 (Z.opp 250)) <= c5_1_0 <= 64078953739589607213994623384761541374699638734673762944879044788010339549152 * (bpow radix2 (Z.opp 250)).

Parameter c1_3_2 : R.
Conjecture c1_3_2_bound : -84742917017354905077149019686171121432982428426474340283514522090594737402064 * (bpow radix2 (Z.opp 261)) <= c1_3_2 <= -84742917017354905077149019686171121432982428426474340283514522090594736765832 * (bpow radix2 (Z.opp 261)).

Parameter c0_0_3 : R.
Conjecture c0_0_3_bound : -67135341539593399575465991601030616600339567844340642970787226195177174765442 * (bpow radix2 (Z.opp 246)) <= c0_0_3 <= -67135341539593399575465991601030616600339567844340642970787226195177174691203 * (bpow radix2 (Z.opp 246)).

Parameter c0_4_1 : R.
Conjecture c0_4_1_bound : 87830253196483106929138580368223947468461326578341686318075332357613368174360 * (bpow radix2 (Z.opp 253)) <= c0_4_1 <= 87830253196483106929138580368223947468461326578341686318075332357613368430408 * (bpow radix2 (Z.opp 253)).

Parameter c5_3_0 : R.
Conjecture c5_3_0_bound : 85241961891614079855792361593801932660841130977066338806630899108090223708650 * (bpow radix2 (Z.opp 247)) <= c5_3_0 <= 85241961891614079855792361593801932660841130977066338806630899108090223722998 * (bpow radix2 (Z.opp 247)).

Parameter c1_0_4 : R.
Conjecture c1_0_4_bound : 98976580488522378074387808057265084991805316009870777746722711762528093152273 * (bpow radix2 (Z.opp 256)) <= c1_0_4 <= 98976580488522378074387808057265084991805316009870777746722711762528093153568 * (bpow radix2 (Z.opp 256)).

Parameter c1_0_3 : R.
Conjecture c1_0_3_bound : 67352084183171962221035858620561528160479331422897184301907102346974215811578 * (bpow radix2 (Z.opp 246)) <= c1_0_3 <= 67352084183171962221035858620561528160479331422897184301907102346974215838624 * (bpow radix2 (Z.opp 246)).

Parameter c2_3_0 : R.
Conjecture c2_3_0_bound : -89474130374874580003048455533691169266685502462713910037499758488048047305415 * (bpow radix2 (Z.opp 245)) <= c2_3_0 <= -89474130374874580003048455533691169266685502462713910037499758488048046855391 * (bpow radix2 (Z.opp 245)).

Parameter c7_0_2 : R.
Conjecture c7_0_2_bound : -100699141537643180193304183998757662708321545883553019137181012352122486756886 * (bpow radix2 (Z.opp 256)) <= c7_0_2 <= -100699141537643180193304183998757662708321545883553019137181012352122486750844 * (bpow radix2 (Z.opp 256)).

Parameter c13_0_0 : R.
Conjecture c13_0_0_bound : -81317172740993345447388647868663968634275568063638327727006767164729552953182 * (bpow radix2 (Z.opp 259)) <= c13_0_0 <= -81317172740993345447388647868663968634275568063638327727006767164729552952430 * (bpow radix2 (Z.opp 259)).

Parameter c6_2_0 : R.
Conjecture c6_2_0_bound : 105614793223564511043398669771961878454663612069013827801465428924453347268450 * (bpow radix2 (Z.opp 245)) <= c6_2_0 <= 105614793223564511043398669771961878454663612069013827801465428924453347289060 * (bpow radix2 (Z.opp 245)).

Parameter c1_1_3 : R.
Conjecture c1_1_3_bound : 79042062380414692716078460669583136239444267509808321721692060957393568563989 * (bpow radix2 (Z.opp 250)) <= c1_1_3 <= 79042062380414692716078460669583136239444267509808321721692060957393568570541 * (bpow radix2 (Z.opp 250)).

Parameter c0_0_2 : R.
Conjecture c0_0_2_bound : -110032752244074567104838786521062702475278482279520092966458297259397878742398 * (bpow radix2 (Z.opp 247)) <= c0_0_2 <= -110032752244074567104838786521062702475278482279520092966458297259397872724562 * (bpow radix2 (Z.opp 247)).

Parameter c3_0_1 : R.
Conjecture c3_0_1_bound : -64223219479888418565703158275517180555066479746158086945285324337587153237793 * (bpow radix2 (Z.opp 247)) <= c3_0_1 <= -64223219479888418565703158275517180555066479746158086945285324337587143768357 * (bpow radix2 (Z.opp 247)).

Parameter c9_2_0 : R.
Conjecture c9_2_0_bound : -75958945108558964719887085371114599622071477309714200369388582096615410907652 * (bpow radix2 (Z.opp 256)) <= c9_2_0 <= -75958945108558964719887085371114599622071477309714200369388582096615410899448 * (bpow radix2 (Z.opp 256)).

Parameter c10_1_0 : R.
Conjecture c10_1_0_bound : -67237845424046789360374738583275678867273291083406232856729161696442298338409 * (bpow radix2 (Z.opp 251)) <= c10_1_0 <= -67237845424046789360374738583275678867273291083406232856729161696442298336543 * (bpow radix2 (Z.opp 251)).

Parameter c4_2_1 : R.
Conjecture c4_2_1_bound : -101763241964681361798097768764254074732612649885815636549200431662317709368224 * (bpow radix2 (Z.opp 246)) <= c4_2_1 <= -101763241964681361798097768764254074732612649885815636549200431662317709353029 * (bpow radix2 (Z.opp 246)).

Parameter c8_1_1 : R.
Conjecture c8_1_1_bound : 102823459938673487416979901211176710745145600502618926891420244906780705434016 * (bpow radix2 (Z.opp 255)) <= c8_1_1 <= 102823459938673487416979901211176710745145600502618926891420244906780705441548 * (bpow radix2 (Z.opp 255)).

Parameter c2_1_1 : R.
Conjecture c2_1_1_bound : -80197637944727966231977835008608375860299841005143960955423394955977238803201 * (bpow radix2 (Z.opp 245)) <= c2_1_1 <= -80197637944727966231977835008608375860299841005143960955423394955977236288299 * (bpow radix2 (Z.opp 245)).

Parameter c1_4_0 : R.
Conjecture c1_4_0_bound : -100407821768807686930933459126208681967854732654841403094725763134713902618966 * (bpow radix2 (Z.opp 252)) <= c1_4_0 <= -100407821768807686930933459126208681967854732654841403094725763134713896503040 * (bpow radix2 (Z.opp 252)).

Parameter c4_3_1 : R.
Conjecture c4_3_1_bound : -62921767759481534742698191712803673347873812474165232962238287495701153262357 * (bpow radix2 (Z.opp 251)) <= c4_3_1 <= -62921767759481534742698191712803673347873812474165232962238287495701153260703 * (bpow radix2 (Z.opp 251)).

Parameter c9_0_0 : R.
Conjecture c9_0_0_bound : -68048219556071412942587049288314300277395118998738220260214657322984936430773 * (bpow radix2 (Z.opp 248)) <= c9_0_0 <= -68048219556071412942587049288314300277395118998738220260214657322984936394931 * (bpow radix2 (Z.opp 248)).

Parameter c2_4_1 : R.
Conjecture c2_4_1_bound : 115576108741594091561321198504087969565193683685288887978915833497152818189896 * (bpow radix2 (Z.opp 257)) <= c2_4_1 <= 115576108741594091561321198504087969565193683685288887978915833497152818235432 * (bpow radix2 (Z.opp 257)).

Parameter c3_2_2 : R.
Conjecture c3_2_2_bound : 114426014058111254416276874954774728625340505544794699208191003467450827418776 * (bpow radix2 (Z.opp 252)) <= c3_2_2 <= 114426014058111254416276874954774728625340505544794699208191003467450827422281 * (bpow radix2 (Z.opp 252)).

Parameter c3_1_0 : R.
Conjecture c3_1_0_bound : 70127378464568934917747264889186017034933458856282626197980354156629911387668 * (bpow radix2 (Z.opp 246)) <= c3_1_0 <= 70127378464568934917747264889186017034933458856282626197980354156629920377370 * (bpow radix2 (Z.opp 246)).

Parameter c2_0_0 : R.
Conjecture c2_0_0_bound : 74824600368467585790344871716491454495799937207024091844321047018143535393543 * (bpow radix2 (Z.opp 250)) <= c2_0_0 <= 74824600368467585790344871716491454495799937207024091844321047018143538886121 * (bpow radix2 (Z.opp 250)).

Parameter c0_2_3 : R.
Conjecture c0_2_3_bound : -71197132427518357224129448548037176655224029129911076518341286355643991177612 * (bpow radix2 (Z.opp 259)) <= c0_2_3 <= -71197132427518357224129448548037176655224029129911076518341286355643991132680 * (bpow radix2 (Z.opp 259)).

Parameter c2_0_2 : R.
Conjecture c2_0_2_bound : 106277946481852259367995819219123149409240887585723202402479144999609528805843 * (bpow radix2 (Z.opp 248)) <= c2_0_2 <= 106277946481852259367995819219123149409240887585723202402479144999609532406703 * (bpow radix2 (Z.opp 248)).

Parameter c10_0_1 : R.
Conjecture c10_0_1_bound : -63160714491799726116372995376952828801921141604422724006876980681349533753982 * (bpow radix2 (Z.opp 256)) <= c10_0_1 <= -63160714491799726116372995376952828801921141604422724006876980681349533752642 * (bpow radix2 (Z.opp 256)).

Parameter c0_1_0 : R.
Conjecture c0_1_0_bound : -80113641865940715398561704462387511173846627808204924824981283290500186763038 * (bpow radix2 (Z.opp 252)) <= c0_1_0 <= -80113641865940715398561704462387511173846627808204924824981283290500116087042 * (bpow radix2 (Z.opp 252)).

Parameter c3_5_0 : R.
Conjecture c3_5_0_bound : -108936965256715989659952067961362616451491372395681710514455650550807790100072 * (bpow radix2 (Z.opp 257)) <= c3_5_0 <= -108936965256715989659952067961362616451491372395681710514455650550807790084828 * (bpow radix2 (Z.opp 257)).

Parameter c0_0_4 : R.
Conjecture c0_0_4_bound : -61228525282237853648722086024650327404917934219338000612857155113752205772928 * (bpow radix2 (Z.opp 253)) <= c0_0_4 <= -61228525282237853648722086024650327404917934219338000612857155113752205768740 * (bpow radix2 (Z.opp 253)).

Parameter c6_0_0 : R.
Conjecture c6_0_0_bound : 68050303743038882184325538470579703355221011518347658348669486690476950644762 * (bpow radix2 (Z.opp 248)) <= c6_0_0 <= 68050303743038882184325538470579703355221011518347658348669486690476954516345 * (bpow radix2 (Z.opp 248)).

Parameter c0_3_2 : R.
Conjecture c0_3_2_bound : 71376442406869924161412202635184783740094536422966613949230877204825891342040 * (bpow radix2 (Z.opp 256)) <= c0_3_2 <= 71376442406869924161412202635184783740094536422966613949230877204825891552200 * (bpow radix2 (Z.opp 256)).

Parameter c3_1_1 : R.
Conjecture c3_1_1_bound : -75619449512461769359450762934783162053206367022485187231556991028276571523964 * (bpow radix2 (Z.opp 245)) <= c3_1_1 <= -75619449512461769359450762934783162053206367022485187231556991028276570460261 * (bpow radix2 (Z.opp 245)).

Parameter c0_5_0 : R.
Conjecture c0_5_0_bound : 72231910007703780986233688013149393886479370339514981007663496671335760551343 * (bpow radix2 (Z.opp 254)) <= c0_5_0 <= 72231910007703780986233688013149393886479370339514981007663496671335761786952 * (bpow radix2 (Z.opp 254)).

Parameter c4_0_1 : R.
Conjecture c4_0_1_bound : 61109375610464705044998577802844814571492649116692414828496649894000246281997 * (bpow radix2 (Z.opp 247)) <= c4_0_1 <= 61109375610464705044998577802844814571492649116692414828496649894000249026581 * (bpow radix2 (Z.opp 247)).

Parameter c0_1_1 : R.
Conjecture c0_1_1_bound : -92598191457411172472680360118882380491288305441952455631550681075458794819317 * (bpow radix2 (Z.opp 248)) <= c0_1_1 <= -92598191457411172472680360118882380491288305441952455631550681075458760622579 * (bpow radix2 (Z.opp 248)).

Parameter c4_4_0 : R.
Conjecture c4_4_0_bound : -59993525967804528197173008269896309316047743930125610711038826852253358219785 * (bpow radix2 (Z.opp 249)) <= c4_4_0 <= -59993525967804528197173008269896309316047743930125610711038826852253358215561 * (bpow radix2 (Z.opp 249)).

Parameter c10_0_0 : R.
Conjecture c10_0_0_bound : 69616996772435252878968628113854130964172417957668692841467864870997440434476 * (bpow radix2 (Z.opp 249)) <= c10_0_0 <= 69616996772435252878968628113854130964172417957668692841467864870997440443690 * (bpow radix2 (Z.opp 249)).

Parameter c6_2_1 : R.
Conjecture c6_2_1_bound : 76755834611250007590637013443323855794099885333139967549397095094036446914760 * (bpow radix2 (Z.opp 253)) <= c6_2_1 <= 76755834611250007590637013443323855794099885333139967549397095094036446920792 * (bpow radix2 (Z.opp 253)).

Parameter c2_1_2 : R.
Conjecture c2_1_2_bound : -69364441715439927627424307979746928922811530365158065788689605800443830303079 * (bpow radix2 (Z.opp 244)) <= c2_1_2 <= -69364441715439927627424307979746928922811530365158065788689605800443830283945 * (bpow radix2 (Z.opp 244)).

Parameter c9_1_0 : R.
Conjecture c9_1_0_bound : 76470889247008575074718272173685021323159531512769133988616861104638418444389 * (bpow radix2 (Z.opp 248)) <= c9_1_0 <= 76470889247008575074718272173685021323159531512769133988616861104638418448609 * (bpow radix2 (Z.opp 248)).

Parameter c1_3_0 : R.
Conjecture c1_3_0_bound : 69871838892454627218452699557611391055405271585604634613721673793375266451635 * (bpow radix2 (Z.opp 246)) <= c1_3_0 <= 69871838892454627218452699557611391055405271585604634613721673793375267752904 * (bpow radix2 (Z.opp 246)).

Parameter c2_2_0 : R.
Conjecture c2_2_0_bound : -87986961494014364428648011937438680590687608560409095161836031235457546265927 * (bpow radix2 (Z.opp 246)) <= c2_2_0 <= -87986961494014364428648011937438680590687608560409095161836031235457538784990 * (bpow radix2 (Z.opp 246)).

Parameter c0_6_0 : R.
Conjecture c0_6_0_bound : -80233761617034197448102341538650635895145970152856618643232435217764280659453 * (bpow radix2 (Z.opp 259)) <= c0_6_0 <= -80233761617034197448102341538650635895145970152856618643232435217764280542295 * (bpow radix2 (Z.opp 259)).

Parameter c5_2_0 : R.
Conjecture c5_2_0_bound : -86237975845673747223348584734989935266848223109592217404009444209908087285222 * (bpow radix2 (Z.opp 244)) <= c5_2_0 <= -86237975845673747223348584734989935266848223109592217404009444209908087213886 * (bpow radix2 (Z.opp 244)).

Parameter c6_1_0 : R.
Conjecture c6_1_0_bound : -101674995997555266459207344156522292267818018577918862641325492087434912474613 * (bpow radix2 (Z.opp 246)) <= c6_1_0 <= -101674995997555266459207344156522292267818018577918862641325492087434912040418 * (bpow radix2 (Z.opp 246)).

Parameter c3_2_1 : R.
Conjecture c3_2_1_bound : 99431166325976776788006102100974320698768520171698149409449961674375748174908 * (bpow radix2 (Z.opp 244)) <= c3_2_1 <= 99431166325976776788006102100974320698768520171698149409449961674375748201952 * (bpow radix2 (Z.opp 244)).

Parameter c3_0_2 : R.
Conjecture c3_0_2_bound : -62633214599642473246367128291396391958619889011989039253274710690486227984309 * (bpow radix2 (Z.opp 245)) <= c3_0_2 <= -62633214599642473246367128291396391958619889011989039253274710690486227873048 * (bpow radix2 (Z.opp 245)).

Parameter c0_0_1 : R.
Conjecture c0_0_1_bound : -77704914935476733651852788113191071092258893723830720529423745233123978529904 * (bpow radix2 (Z.opp 249)) <= c0_0_1 <= -77704914935476733651852788113191071092258893723830720529423745233123947274801 * (bpow radix2 (Z.opp 249)).

Parameter c2_2_2 : R.
Conjecture c2_2_2_bound : -114093978510318359055811334036019072462431107980013066620913293212315820738491 * (bpow radix2 (Z.opp 249)) <= c2_2_2 <= -114093978510318359055811334036019072462431107980013066620913293212315820730446 * (bpow radix2 (Z.opp 249)).

Parameter c1_0_1 : R.
Conjecture c1_0_1_bound : 93594110231089959684355007405420578310962513241728871038540489164540988173027 * (bpow radix2 (Z.opp 248)) <= c1_0_1 <= 93594110231089959684355007405420578310962513241728871038540489164541028838471 * (bpow radix2 (Z.opp 248)).

Parameter c3_0_0 : R.
Conjecture c3_0_0_bound : -85679803603527643642839972308842121500328672189045912308925255005977516922268 * (bpow radix2 (Z.opp 248)) <= c3_0_0 <= -85679803603527643642839972308842121500328672189045912308925255005977516282675 * (bpow radix2 (Z.opp 248)).

Parameter c4_3_0 : R.
Conjecture c4_3_0_bound : -97403238239950333748441898099869334582868829431280242224212660105514877252350 * (bpow radix2 (Z.opp 245)) <= c4_3_0 <= -97403238239950333748441898099869334582868829431280242224212660105514877219801 * (bpow radix2 (Z.opp 245)).

Parameter c7_3_0 : R.
Conjecture c7_3_0_bound : -109552624107154304741110535571651689108025244808476849432421979724379730982473 * (bpow radix2 (Z.opp 254)) <= c7_3_0 <= -109552624107154304741110535571651689108025244808476849432421979724379730977682 * (bpow radix2 (Z.opp 254)).

Parameter c8_2_0 : R.
Conjecture c8_2_0_bound : 81417874092266823598838480834525962142137192432433739162445293297822318581542 * (bpow radix2 (Z.opp 250)) <= c8_2_0 <= 81417874092266823598838480834525962142137192432433739162445293297822318585894 * (bpow radix2 (Z.opp 250)).

Parameter c5_1_2 : R.
Conjecture c5_1_2_bound : -63342352911520073642902949125403430968384009677621495802309897295272124796048 * (bpow radix2 (Z.opp 254)) <= c5_1_2 <= -63342352911520073642902949125403430968384009677621495802309897295272124786408 * (bpow radix2 (Z.opp 254)).

Parameter c6_0_1 : R.
Conjecture c6_0_1_bound : -80001108596656891948593686472137615589669667112424441903901860824551166391352 * (bpow radix2 (Z.opp 246)) <= c6_0_1 <= -80001108596656891948593686472137615589669667112424441903901860824551166320033 * (bpow radix2 (Z.opp 246)).

Parameter c5_0_0 : R.
Conjecture c5_0_0_bound : -82120175288780890241806327886802530745940893177831091164137851440872693931881 * (bpow radix2 (Z.opp 247)) <= c5_0_0 <= -82120175288780890241806327886802530745940893177831091164137851440872690540707 * (bpow radix2 (Z.opp 247)).

Parameter c4_1_2 : R.
Conjecture c4_1_2_bound : -93714723178693700933763890387539081003571151023197664911056343536138192875482 * (bpow radix2 (Z.opp 250)) <= c4_1_2 <= -93714723178693700933763890387539081003571151023197664911056343536138192860198 * (bpow radix2 (Z.opp 250)).

Parameter c4_0_2 : R.
Conjecture c4_0_2_bound : 98027418634218773619250910348949169128774598392924865522492235345244213570083 * (bpow radix2 (Z.opp 246)) <= c4_0_2 <= 98027418634218773619250910348949169128774598392924865522492235345244213597131 * (bpow radix2 (Z.opp 246)).

Parameter c3_4_0 : R.
Conjecture c3_4_0_bound : 67652631221377048505652174764569019642707856238270679266395420349928601653988 * (bpow radix2 (Z.opp 248)) <= c3_4_0 <= 67652631221377048505652174764569019642707856238270679266395420349928601671730 * (bpow radix2 (Z.opp 248)).

Parameter c7_0_0 : R.
Conjecture c7_0_0_bound : -62228034841713456218831165981886530900698187208823556713280643063664108052251 * (bpow radix2 (Z.opp 249)) <= c7_0_0 <= -62228034841713456218831165981886530900698187208823556713280643063664105642023 * (bpow radix2 (Z.opp 249)).

Parameter c1_4_1 : R.
Conjecture c1_4_1_bound : -111221292374578325157346251302317966455384286881595117254508786546985158713334 * (bpow radix2 (Z.opp 254)) <= c1_4_1 <= -111221292374578325157346251302317966455384286881595117254508786546985158647656 * (bpow radix2 (Z.opp 254)).

Parameter c0_4_0 : R.
Conjecture c0_4_0_bound : -112960074785643541117512285362415670890091823182357550255556081440829503721823 * (bpow radix2 (Z.opp 254)) <= c0_4_0 <= -112960074785643541117512285362415670890091823182357550255556081440829449911964 * (bpow radix2 (Z.opp 254)).

Parameter c1_1_2 : R.
Conjecture c1_1_2_bound : 75844622802184196150428483246977974604318388537916182015830775028719840107382 * (bpow radix2 (Z.opp 244)) <= c1_1_2 <= 75844622802184196150428483246977974604318388537916182015830775028719840177568 * (bpow radix2 (Z.opp 244)).

Parameter c3_3_1 : R.
Conjecture c3_3_1_bound : 66817733864709111525326021419770928044526372240903676057617660423949869182680 * (bpow radix2 (Z.opp 248)) <= c3_3_1 <= 66817733864709111525326021419770928044526372240903676057617660423949869187156 * (bpow radix2 (Z.opp 248)).

Parameter c9_0_1 : R.
Conjecture c9_0_1_bound : 103690982649238547140783867875896507405504032389622982971756012271622918951509 * (bpow radix2 (Z.opp 252)) <= c9_0_1 <= 103690982649238547140783867875896507405504032389622982971756012271622918954707 * (bpow radix2 (Z.opp 252)).

Parameter c1_1_1 : R.
Conjecture c1_1_1_bound : 97067657474809411769036864299741683369739832538251265095725816074976933204739 * (bpow radix2 (Z.opp 245)) <= c1_1_1 <= 97067657474809411769036864299741683369739832538251265095725816074976936173737 * (bpow radix2 (Z.opp 245)).

Parameter c11_0_0 : R.
Conjecture c11_0_0_bound : -69459479418620031832921041331017321713860765945332182705155608948768132426092 * (bpow radix2 (Z.opp 251)) <= c11_0_0 <= -69459479418620031832921041331017321713860765945332182705155608948768132422922 * (bpow radix2 (Z.opp 251)).

Parameter c5_2_1 : R.
Conjecture c5_2_1_bound : 80428087243443079809407330448485121482615679363178306329732387554894381679016 * (bpow radix2 (Z.opp 250)) <= c5_2_1 <= 80428087243443079809407330448485121482615679363178306329732387554894381698852 * (bpow radix2 (Z.opp 250)).

Parameter c3_0_3 : R.
Conjecture c3_0_3_bound : 65664324387269664448445217218107187997767706646839015638646303451009684166270 * (bpow radix2 (Z.opp 251)) <= c3_0_3 <= 65664324387269664448445217218107187997767706646839015638646303451009684175566 * (bpow radix2 (Z.opp 251)).

Parameter c0_1_2 : R.
Conjecture c0_1_2_bound : -86848188988742383243014883958374826296419901300721914808250736530305920797181 * (bpow radix2 (Z.opp 247)) <= c0_1_2 <= -86848188988742383243014883958374826296419901300721914808250736530305919051023 * (bpow radix2 (Z.opp 247)).

Parameter c5_1_1 : R.
Conjecture c5_1_1_bound : -71037526025639601898680987475767166687791640190324575279766041791975376354503 * (bpow radix2 (Z.opp 244)) <= c5_1_1 <= -71037526025639601898680987475767166687791640190324575279766041791975376339039 * (bpow radix2 (Z.opp 244)).

Parameter c1_2_0 : R.
Conjecture c1_2_0_bound : -86136356571300122931963275238523394398520512643071976577649330845224761795080 * (bpow radix2 (Z.opp 249)) <= c1_2_0 <= -86136356571300122931963275238523394398520512643071976577649330845224733410137 * (bpow radix2 (Z.opp 249)).

Parameter c2_1_0 : R.
Conjecture c2_1_0_bound : -65419798596659179091626886853304973866143182396916423890432702477484365105423 * (bpow radix2 (Z.opp 246)) <= c2_1_0 <= -65419798596659179091626886853304973866143182396916423890432702477484355326402 * (bpow radix2 (Z.opp 246)).

Parameter c8_0_1 : R.
Conjecture c8_0_1_bound : -110420878874094864392970443410250501299461617950080993001861330900816453498862 * (bpow radix2 (Z.opp 249)) <= c8_0_1 <= -110420878874094864392970443410250501299461617950080993001861330900816453492140 * (bpow radix2 (Z.opp 249)).

Parameter c0_5_1 : R.
Conjecture c0_5_1_bound : 67834691372098352446447948677588939692039379181776076948712193743384517702536 * (bpow radix2 (Z.opp 259)) <= c0_5_1 <= 67834691372098352446447948677588939692039379181776076948712193743384517714380 * (bpow radix2 (Z.opp 259)).

Parameter c1_6_0 : R.
Conjecture c1_6_0_bound : -86396755773976630559497854120637438399590860458970092405912347251835221154832 * (bpow radix2 (Z.opp 259)) <= c1_6_0 <= -86396755773976630559497854120637438399590860458970092405912347251835221149964 * (bpow radix2 (Z.opp 259)).

Parameter c2_5_0 : R.
Conjecture c2_5_0_bound : 70124564451641519984497492907842605341985972900141393446869545306099531319342 * (bpow radix2 (Z.opp 253)) <= c2_5_0 <= 70124564451641519984497492907842605341985972900141393446869545306099531340006 * (bpow radix2 (Z.opp 253)).

Parameter c5_0_1 : R.
Conjecture c5_0_1_bound : 81377707192791360000580509020731442569017365124298017893110951186442989897348 * (bpow radix2 (Z.opp 247)) <= c5_0_1 <= 81377707192791360000580509020731442569017365124298017893110951186442990564516 * (bpow radix2 (Z.opp 247)).

Parameter c4_1_1 : R.
Conjecture c4_1_1_bound : 100654893814761289765314155592857607176558312269126491264649367640833567067760 * (bpow radix2 (Z.opp 244)) <= c4_1_1 <= 100654893814761289765314155592857607176558312269126491264649367640833567167646 * (bpow radix2 (Z.opp 244)).

Parameter c5_0_2 : R.
Conjecture c5_0_2_bound : -58324534777687816685036868289742223463922464217204347809894208751619942451082 * (bpow radix2 (Z.opp 247)) <= c5_0_2 <= -58324534777687816685036868289742223463922464217204347809894208751619942445751 * (bpow radix2 (Z.opp 247)).

Definition solution_poly_gens x y z := c0_3_0 * (powerRZ y 3) + c6_0_2 * (powerRZ x 6) * (powerRZ z 2) + c11_1_0 * (powerRZ x 11) * (powerRZ y 1) + c0_0_0 + c3_3_0 * (powerRZ x 3) * (powerRZ y 3) + c4_2_0 * (powerRZ x 4) * (powerRZ y 2) + c1_2_2 * (powerRZ x 1) * (powerRZ y 2) * (powerRZ z 2) + c2_0_1 * (powerRZ x 2) * (powerRZ z 1) + c7_2_0 * (powerRZ x 7) * (powerRZ y 2) + c8_1_0 * (powerRZ x 8) * (powerRZ y 1) + c4_0_0 * (powerRZ x 4) + c1_0_2 * (powerRZ x 1) * (powerRZ z 2) + c4_0_3 * (powerRZ x 4) * (powerRZ z 3) + c1_3_1 * (powerRZ x 1) * (powerRZ y 3) * (powerRZ z 1) + c8_0_0 * (powerRZ x 8) + c0_3_1 * (powerRZ y 3) * (powerRZ z 1) + c2_1_3 * (powerRZ x 2) * (powerRZ y 1) * (powerRZ z 3) + c6_3_0 * (powerRZ x 6) * (powerRZ y 3) + c3_1_2 * (powerRZ x 3) * (powerRZ y 1) * (powerRZ z 2) + c1_1_0 * (powerRZ x 1) * (powerRZ y 1) + c2_0_3 * (powerRZ x 2) * (powerRZ z 3) + c12_0_0 * (powerRZ x 12) + c7_0_1 * (powerRZ x 7) * (powerRZ z 1) + c6_1_1 * (powerRZ x 6) * (powerRZ y 1) * (powerRZ z 1) + c1_5_0 * (powerRZ x 1) * (powerRZ y 5) + c0_2_1 * (powerRZ y 2) * (powerRZ z 1) + c5_4_0 * (powerRZ x 5) * (powerRZ y 4) + c7_1_1 * (powerRZ x 7) * (powerRZ y 1) * (powerRZ z 1) + c0_1_3 * (powerRZ y 1) * (powerRZ z 3) + c2_4_0 * (powerRZ x 2) * (powerRZ y 4) + c2_2_1 * (powerRZ x 2) * (powerRZ y 2) * (powerRZ z 1) + c1_0_0 * (powerRZ x 1) + c0_2_2 * (powerRZ y 2) * (powerRZ z 2) + c7_1_0 * (powerRZ x 7) * (powerRZ y 1) + c0_2_0 * (powerRZ y 2) + c1_2_1 * (powerRZ x 1) * (powerRZ y 2) * (powerRZ z 1) + c3_2_0 * (powerRZ x 3) * (powerRZ y 2) + c4_1_0 * (powerRZ x 4) * (powerRZ y 1) + c2_3_1 * (powerRZ x 2) * (powerRZ y 3) * (powerRZ z 1) + c5_1_0 * (powerRZ x 5) * (powerRZ y 1) + c1_3_2 * (powerRZ x 1) * (powerRZ y 3) * (powerRZ z 2) + c0_0_3 * (powerRZ z 3) + c0_4_1 * (powerRZ y 4) * (powerRZ z 1) + c5_3_0 * (powerRZ x 5) * (powerRZ y 3) + c1_0_4 * (powerRZ x 1) * (powerRZ z 4) + c1_0_3 * (powerRZ x 1) * (powerRZ z 3) + c2_3_0 * (powerRZ x 2) * (powerRZ y 3) + c7_0_2 * (powerRZ x 7) * (powerRZ z 2) + c13_0_0 * (powerRZ x 13) + c6_2_0 * (powerRZ x 6) * (powerRZ y 2) + c1_1_3 * (powerRZ x 1) * (powerRZ y 1) * (powerRZ z 3) + c0_0_2 * (powerRZ z 2) + c3_0_1 * (powerRZ x 3) * (powerRZ z 1) + c9_2_0 * (powerRZ x 9) * (powerRZ y 2) + c10_1_0 * (powerRZ x 10) * (powerRZ y 1) + c4_2_1 * (powerRZ x 4) * (powerRZ y 2) * (powerRZ z 1) + c8_1_1 * (powerRZ x 8) * (powerRZ y 1) * (powerRZ z 1) + c2_1_1 * (powerRZ x 2) * (powerRZ y 1) * (powerRZ z 1) + c1_4_0 * (powerRZ x 1) * (powerRZ y 4) + c4_3_1 * (powerRZ x 4) * (powerRZ y 3) * (powerRZ z 1) + c9_0_0 * (powerRZ x 9) + c2_4_1 * (powerRZ x 2) * (powerRZ y 4) * (powerRZ z 1) + c3_2_2 * (powerRZ x 3) * (powerRZ y 2) * (powerRZ z 2) + c3_1_0 * (powerRZ x 3) * (powerRZ y 1) + c2_0_0 * (powerRZ x 2) + c0_2_3 * (powerRZ y 2) * (powerRZ z 3) + c2_0_2 * (powerRZ x 2) * (powerRZ z 2) + c10_0_1 * (powerRZ x 10) * (powerRZ z 1) + c0_1_0 * (powerRZ y 1) + c3_5_0 * (powerRZ x 3) * (powerRZ y 5) + c0_0_4 * (powerRZ z 4) + c6_0_0 * (powerRZ x 6) + c0_3_2 * (powerRZ y 3) * (powerRZ z 2) + c3_1_1 * (powerRZ x 3) * (powerRZ y 1) * (powerRZ z 1) + c0_5_0 * (powerRZ y 5) + c4_0_1 * (powerRZ x 4) * (powerRZ z 1) + c0_1_1 * (powerRZ y 1) * (powerRZ z 1) + c4_4_0 * (powerRZ x 4) * (powerRZ y 4) + c10_0_0 * (powerRZ x 10) + c6_2_1 * (powerRZ x 6) * (powerRZ y 2) * (powerRZ z 1) + c2_1_2 * (powerRZ x 2) * (powerRZ y 1) * (powerRZ z 2) + c9_1_0 * (powerRZ x 9) * (powerRZ y 1) + c1_3_0 * (powerRZ x 1) * (powerRZ y 3) + c2_2_0 * (powerRZ x 2) * (powerRZ y 2) + c0_6_0 * (powerRZ y 6) + c5_2_0 * (powerRZ x 5) * (powerRZ y 2) + c6_1_0 * (powerRZ x 6) * (powerRZ y 1) + c3_2_1 * (powerRZ x 3) * (powerRZ y 2) * (powerRZ z 1) + c3_0_2 * (powerRZ x 3) * (powerRZ z 2) + c0_0_1 * (powerRZ z 1) + c2_2_2 * (powerRZ x 2) * (powerRZ y 2) * (powerRZ z 2) + c1_0_1 * (powerRZ x 1) * (powerRZ z 1) + c3_0_0 * (powerRZ x 3) + c4_3_0 * (powerRZ x 4) * (powerRZ y 3) + c7_3_0 * (powerRZ x 7) * (powerRZ y 3) + c8_2_0 * (powerRZ x 8) * (powerRZ y 2) + c5_1_2 * (powerRZ x 5) * (powerRZ y 1) * (powerRZ z 2) + c6_0_1 * (powerRZ x 6) * (powerRZ z 1) + c5_0_0 * (powerRZ x 5) + c4_1_2 * (powerRZ x 4) * (powerRZ y 1) * (powerRZ z 2) + c4_0_2 * (powerRZ x 4) * (powerRZ z 2) + c3_4_0 * (powerRZ x 3) * (powerRZ y 4) + c7_0_0 * (powerRZ x 7) + c1_4_1 * (powerRZ x 1) * (powerRZ y 4) * (powerRZ z 1) + c0_4_0 * (powerRZ y 4) + c1_1_2 * (powerRZ x 1) * (powerRZ y 1) * (powerRZ z 2) + c3_3_1 * (powerRZ x 3) * (powerRZ y 3) * (powerRZ z 1) + c9_0_1 * (powerRZ x 9) * (powerRZ z 1) + c1_1_1 * (powerRZ x 1) * (powerRZ y 1) * (powerRZ z 1) + c11_0_0 * (powerRZ x 11) + c5_2_1 * (powerRZ x 5) * (powerRZ y 2) * (powerRZ z 1) + c3_0_3 * (powerRZ x 3) * (powerRZ z 3) + c0_1_2 * (powerRZ y 1) * (powerRZ z 2) + c5_1_1 * (powerRZ x 5) * (powerRZ y 1) * (powerRZ z 1) + c1_2_0 * (powerRZ x 1) * (powerRZ y 2) + c2_1_0 * (powerRZ x 2) * (powerRZ y 1) + c8_0_1 * (powerRZ x 8) * (powerRZ z 1) + c0_5_1 * (powerRZ y 5) * (powerRZ z 1) + c1_6_0 * (powerRZ x 1) * (powerRZ y 6) + c2_5_0 * (powerRZ x 2) * (powerRZ y 5) + c5_0_1 * (powerRZ x 5) * (powerRZ z 1) + c4_1_1 * (powerRZ x 4) * (powerRZ y 1) * (powerRZ z 1) + c5_0_2 * (powerRZ x 5) * (powerRZ z 2).

Definition solution_poly x y z := solution_poly_gens (powerRZ x 2 + powerRZ y 2 + powerRZ z 2) (powerRZ x 4 + powerRZ y 4 + powerRZ z 4) (powerRZ x 6 + powerRZ y 6 + powerRZ z 6).

Tactic Notation "intro_poly_bounds" := pose c0_3_0_bound; pose c6_0_2_bound; pose c11_1_0_bound; pose c0_0_0_bound; pose c3_3_0_bound; pose c4_2_0_bound; pose c1_2_2_bound; pose c2_0_1_bound; pose c7_2_0_bound; pose c8_1_0_bound; pose c4_0_0_bound; pose c1_0_2_bound; pose c4_0_3_bound; pose c1_3_1_bound; pose c8_0_0_bound; pose c0_3_1_bound; pose c2_1_3_bound; pose c6_3_0_bound; pose c3_1_2_bound; pose c1_1_0_bound; pose c2_0_3_bound; pose c12_0_0_bound; pose c7_0_1_bound; pose c6_1_1_bound; pose c1_5_0_bound; pose c0_2_1_bound; pose c5_4_0_bound; pose c7_1_1_bound; pose c0_1_3_bound; pose c2_4_0_bound; pose c2_2_1_bound; pose c1_0_0_bound; pose c0_2_2_bound; pose c7_1_0_bound; pose c0_2_0_bound; pose c1_2_1_bound; pose c3_2_0_bound; pose c4_1_0_bound; pose c2_3_1_bound; pose c5_1_0_bound; pose c1_3_2_bound; pose c0_0_3_bound; pose c0_4_1_bound; pose c5_3_0_bound; pose c1_0_4_bound; pose c1_0_3_bound; pose c2_3_0_bound; pose c7_0_2_bound; pose c13_0_0_bound; pose c6_2_0_bound; pose c1_1_3_bound; pose c0_0_2_bound; pose c3_0_1_bound; pose c9_2_0_bound; pose c10_1_0_bound; pose c4_2_1_bound; pose c8_1_1_bound; pose c2_1_1_bound; pose c1_4_0_bound; pose c4_3_1_bound; pose c9_0_0_bound; pose c2_4_1_bound; pose c3_2_2_bound; pose c3_1_0_bound; pose c2_0_0_bound; pose c0_2_3_bound; pose c2_0_2_bound; pose c10_0_1_bound; pose c0_1_0_bound; pose c3_5_0_bound; pose c0_0_4_bound; pose c6_0_0_bound; pose c0_3_2_bound; pose c3_1_1_bound; pose c0_5_0_bound; pose c4_0_1_bound; pose c0_1_1_bound; pose c4_4_0_bound; pose c10_0_0_bound; pose c6_2_1_bound; pose c2_1_2_bound; pose c9_1_0_bound; pose c1_3_0_bound; pose c2_2_0_bound; pose c0_6_0_bound; pose c5_2_0_bound; pose c6_1_0_bound; pose c3_2_1_bound; pose c3_0_2_bound; pose c0_0_1_bound; pose c2_2_2_bound; pose c1_0_1_bound; pose c3_0_0_bound; pose c4_3_0_bound; pose c7_3_0_bound; pose c8_2_0_bound; pose c5_1_2_bound; pose c6_0_1_bound; pose c5_0_0_bound; pose c4_1_2_bound; pose c4_0_2_bound; pose c3_4_0_bound; pose c7_0_0_bound; pose c1_4_1_bound; pose c0_4_0_bound; pose c1_1_2_bound; pose c3_3_1_bound; pose c9_0_1_bound; pose c1_1_1_bound; pose c11_0_0_bound; pose c5_2_1_bound; pose c3_0_3_bound; pose c0_1_2_bound; pose c5_1_1_bound; pose c1_2_0_bound; pose c2_1_0_bound; pose c8_0_1_bound; pose c0_5_1_bound; pose c1_6_0_bound; pose c2_5_0_bound; pose c5_0_1_bound; pose c4_1_1_bound; pose c5_0_2_bound.