Advanced Search

Question: How many significant decimal digits should be used for the internal CAD algorithm to succeed?

Question:How many significant decimal digits should be used for the internal CAD algorithm to succeed?

sursumCorda 1079 Maple 2023
accuracy precision digits quantifierelimination
July 01 2023
1

With a low numerical accuracy (for instance, Digits ≔ 10, 18, 22, 30, 50, …), the numeric calculation may fail (due to loss of precision). However, if I set the precision to 1011 digits, the error message will suggest that I need 2022 effective digits, and if I set the number of digits to 2023, the new error message will indicate that I need 4046 digits instead! 
 

> 

restart;
(* kernelopts(assertlevel = 2): *)
> 

f__||(1..2):=seq(:-Implies(:-And((x,y,z)>=~0,x+y+z>=x*y*z-2),(x+y+z-`k`)**2+12*`K`>=`K`*(y*z+z*x+x*y)+(6-`k`)**2),`k`in[-1,2]):
> 

Digits := 10
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  
> 

Digits := 15
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  
> 

Digits := 22
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  

Error, (in CADCell:-incrementalCADMerge) intervals the same at this precision

  
> 

Digits := 30
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in evalr/shake) -1745522223305217995292661862391649380423964537/713623846352979940529142984724747568191373312 .. -872761111652608997646330931195824690211982147/356811923176489970264571492362373784095686656 is an invalid range

  

Error, (in CADCell:-getRootOf) assertion failed, QuantifierElimination:-CADCell:-getRootOf expects its return value to be of type Or(realalgfun,polynom), but computed -4/(K-2)

  
> 

Digits := 500
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in fsolve) 51953924463883761901792418789194928235174905950382670549953648710446970664310543651007323799780435683230006536652706682836424797844925527680493588036601389375573240391357941112051916610030393510104292907027389236710859112839952847980210175362475743230722948239736701720236829869491083611577725129304524699348873290677105040453671573567321637853939258015148604288142746130200523992493313329625476885430355670361959662016545723317992326796888354706811339520905282493925959682290128861158489269192756541573370159292296031148260734007880772071719402902769848742402757080259718232411901509888033214784334659015401671/30819898673354155827250363053007080040401556653705104858522744586491255892627612012097550784609712089241712532922647494787330207014552041144455101381729395981436612479496952144384572744741108042522485388168399399067680567400569683229292005861736460180837293483768754046332908526936593826873352431415491471788324674024265615864453291689457482809883285556150743539884381923037553971012554468298204987396409146047538379400693757398222304489423414139178941357835089904048085865698642930722386457182818721265486280995041559157415387409546850813117528120412289939445116172250012974400824049572899006074481824503955456 .. 103907848927767523803584837578389856470349811900765341099907297420893941328621087302014647599560871366460013073305413365672849595689851055360987176073202778751146480782715882224103833220060787020208585814054778473421718225679905695960420350724951486461445896479473403440473659738982167223155450258609049398697746581354210080907343147134643275707878516030297208576285492260401047984986626659250953770860711340723919324033091446635984653593776709413622679041810564987851919364580257722316978538385513083146740318584592062296521468015761544143438805805539697484805514160519436464823803019776066429568669328491156545/61639797346708311654500726106014160080803113307410209717045489172982511785255224024195101569219424178483425065845294989574660414029104082288910202763458791962873224958993904288769145489482216085044970776336798798135361134801139366458584011723472920361674586967537508092665817053873187653746704862830982943576649348048531231728906583378914965619766571112301487079768763846075107942025108936596409974792818292095076758801387514796444608978846828278357882715670179808096171731397285861444772914365637442530972561990083118314830774819093701626235056240824579878890232344500025948801648099145798012148963649007910912 is an invalid range

  

Error, (in QuantifierElimination:-makeIntervalsDisjoint) intervals the same at this precision

  
> 

Digits := 1011
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in QuantifierElimination:-CylindricalAlgebraicDecompose) could not deduce sign of expression -342/25*RootOf(19*_Z^2+38*_Z-12,-4987910358199862617695009215709741605709429723398915706935981134367159645137702755744811848649748363964619233272334637596908427108379140961254846049673609374649230279927501442010021927667514449257826614057994448539998131000148492036947851465573508992822358525609812547821711206993013464583756238982808480726743494241044879932540380141333843955234896674594593548858060217618984313571272446618558610719387174513219009335839077580775050010186121998765445974558764352314930517401142857800948902933757634601020640904937469362743714271628486160227454116983764409999636638394510618606021312024472773815702904498322013237669791547497017096378031053343768560075850663597929486261657611626497278288155649674743772219645453376069718849586569846366137879582969431774492624897836480589922659958172908351367904597399703973894410690193526222594908197737029927077207602713412071670101566072357427300354219930601407610842782444349564488842636963556768876362858397663083302382595638845298193545672264754619772234178272290746956937279156515624590145750509771810057257684689393280341696527499483583228747445979211697575964881432846981852813748325889619627566484956410900755790611831189266287867465483821614902144107200456548248296812798080610603299934574758229/2190242231433355605713622580784790257176337184818218989800356017935910506010367663745430846303103999469714369076399728939211315611038213435059310088109666395374919565272594510439485989473503083630539455881503721340537549806680592080012228027942618514056665699358193649600501485383437221341624748544828173727431527449245595018874125036164766112100289249925552604295781042498954120430296550327376602551694310632084558811115265278732133694885722844329665311749311648443155699857726046036733671350799899480858664936372681036344974146721644440898110681165136923137290519909746607233907552787706349690264162243952654925480709861488974859234405170031021488597060203095413643180377467031761467054899561926327819660155232715013691046430578595248173829090757022165068459240233126520336989047813133418836332022225509059532367109158642449881902354788176931193425240152480134741178073848049456750152420954534977358016033159177392382388120254638070390740274321873764804488799398344035670289074976972793812288435440057985727882576434370707829983166800843365502001207193311581981631050252308788689282672795587582994136507873542034063961735413414980448082151652674767077303650987359007543869672189311605552663328523263480296563526975531705493155616571523072 .. -2493955179099931308847504607854870802854714861699457853467990567183579822568851377872405924324874181982309616636167318798454213554189570480627423024836804687324615139963750721005010963833757224628913307028997224269999065500074246018473925732786754496411179262804906273910855603496506732291878119491404240363371747120522439966270190070666921977617448337297296774429030108809492156785636223309279305359693587256609504667919538790387525005093060999382722987279382176157465258700571428900474451466878817300510320452468734681371857135814243080113727058491882204999818319197255309303010656012236386907851452249161006618834895773748508548189015526671884280037925331798964743130828805813248639144077824837371886109822726688034859424793284923183068939791484715887246312448918240294961329979086454175683952298699851986947205345096763111297454098868514963538603801356706035835050783036178713650177109965300703805421391222174782244421318481778384438181429198831541651191297819422649096772836132377309886117089136145373478468639578257812295072875254885905028628842344696640170848263749741791614373722989605848787982440716423490926406874162944809813783242478205450377895305915594633143933732741910807451072053600228274124148406399040305301649967287369273/1095121115716677802856811290392395128588168592409109494900178008967955253005183831872715423151551999734857184538199864469605657805519106717529655044054833197687459782636297255219742994736751541815269727940751860670268774903340296040006114013971309257028332849679096824800250742691718610670812374272414086863715763724622797509437062518082383056050144624962776302147890521249477060215148275163688301275847155316042279405557632639366066847442861422164832655874655824221577849928863023018366835675399949740429332468186340518172487073360822220449055340582568461568645259954873303616953776393853174845132081121976327462740354930744487429617202585015510744298530101547706821590188733515880733527449780963163909830077616357506845523215289297624086914545378511082534229620116563260168494523906566709418166011112754529766183554579321224940951177394088465596712620076240067370589036924024728375076210477267488679008016579588696191194060127319035195370137160936882402244399699172017835144537488486396906144217720028992863941288217185353914991583400421682751000603596655790990815525126154394344641336397793791497068253936771017031980867706707490224041075826337383538651825493679503771934836094655802776331664261631740148281763487765852746577808285761536)+328/25 from intermediate relation -342/25*RootOf(19*_Z^2+38*_Z-12,-4987910358199862617695009215709741605709429723398915706935981134367159645137702755744811848649748363964619233272334637596908427108379140961254846049673609374649230279927501442010021927667514449257826614057994448539998131000148492036947851465573508992822358525609812547821711206993013464583756238982808480726743494241044879932540380141333843955234896674594593548858060217618984313571272446618558610719387174513219009335839077580775050010186121998765445974558764352314930517401142857800948902933757634601020640904937469362743714271628486160227454116983764409999636638394510618606021312024472773815702904498322013237669791547497017096378031053343768560075850663597929486261657611626497278288155649674743772219645453376069718849586569846366137879582969431774492624897836480589922659958172908351367904597399703973894410690193526222594908197737029927077207602713412071670101566072357427300354219930601407610842782444349564488842636963556768876362858397663083302382595638845298193545672264754619772234178272290746956937279156515624590145750509771810057257684689393280341696527499483583228747445979211697575964881432846981852813748325889619627566484956410900755790611831189266287867465483821614902144107200456548248296812798080610603299934574758229/2190242231433355605713622580784790257176337184818218989800356017935910506010367663745430846303103999469714369076399728939211315611038213435059310088109666395374919565272594510439485989473503083630539455881503721340537549806680592080012228027942618514056665699358193649600501485383437221341624748544828173727431527449245595018874125036164766112100289249925552604295781042498954120430296550327376602551694310632084558811115265278732133694885722844329665311749311648443155699857726046036733671350799899480858664936372681036344974146721644440898110681165136923137290519909746607233907552787706349690264162243952654925480709861488974859234405170031021488597060203095413643180377467031761467054899561926327819660155232715013691046430578595248173829090757022165068459240233126520336989047813133418836332022225509059532367109158642449881902354788176931193425240152480134741178073848049456750152420954534977358016033159177392382388120254638070390740274321873764804488799398344035670289074976972793812288435440057985727882576434370707829983166800843365502001207193311581981631050252308788689282672795587582994136507873542034063961735413414980448082151652674767077303650987359007543869672189311605552663328523263480296563526975531705493155616571523072 .. -2493955179099931308847504607854870802854714861699457853467990567183579822568851377872405924324874181982309616636167318798454213554189570480627423024836804687324615139963750721005010963833757224628913307028997224269999065500074246018473925732786754496411179262804906273910855603496506732291878119491404240363371747120522439966270190070666921977617448337297296774429030108809492156785636223309279305359693587256609504667919538790387525005093060999382722987279382176157465258700571428900474451466878817300510320452468734681371857135814243080113727058491882204999818319197255309303010656012236386907851452249161006618834895773748508548189015526671884280037925331798964743130828805813248639144077824837371886109822726688034859424793284923183068939791484715887246312448918240294961329979086454175683952298699851986947205345096763111297454098868514963538603801356706035835050783036178713650177109965300703805421391222174782244421318481778384438181429198831541651191297819422649096772836132377309886117089136145373478468639578257812295072875254885905028628842344696640170848263749741791614373722989605848787982440716423490926406874162944809813783242478205450377895305915594633143933732741910807451072053600228274124148406399040305301649967287369273/1095121115716677802856811290392395128588168592409109494900178008967955253005183831872715423151551999734857184538199864469605657805519106717529655044054833197687459782636297255219742994736751541815269727940751860670268774903340296040006114013971309257028332849679096824800250742691718610670812374272414086863715763724622797509437062518082383056050144624962776302147890521249477060215148275163688301275847155316042279405557632639366066847442861422164832655874655824221577849928863023018366835675399949740429332468186340518172487073360822220449055340582568461568645259954873303616953776393853174845132081121976327462740354930744487429617202585015510744298530101547706821590188733515880733527449780963163909830077616357506845523215289297624086914545378511082534229620116563260168494523906566709418166011112754529766183554579321224940951177394088465596712620076240067370589036924024728375076210477267488679008016579588696191194060127319035195370137160936882402244399699172017835144537488486396906144217720028992863941288217185353914991583400421682751000603596655790990815525126154394344641336397793791497068253936771017031980867706707490224041075826337383538651825493679503771934836094655802776331664261631740148281763487765852746577808285761536) < -328/25, and hence the truth of the relation at extremely high precision (2022 digits)

  

Error, (in QuantifierElimination:-makeIntervalsDisjoint) intervals the same at this precision

  
> 

Digits := 2023
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__1))
> 

QuantifierElimination:-QuantifierEliminate(forall([x, y, z], f__2))

Error, (in QuantifierElimination:-CylindricalAlgebraicDecompose) could not deduce sign of expression 729/40*RootOf(675*_Z^2+4320*_Z+164,-1819051677054954937088966774080402766362059925703142152107946489025251982259488522542780558822517219639316402494749234977258281452721872596195467650700476020010399039940415953392604294876123760949630414571003345043058536169063535023925283379147685829107161736070003830151116673428248900332716375268508211684501695562616939133437174041034441376584698560240247761556592415321007416402048900440163892437015276176011310337300603150533018026563587072171241416168011632612357238259475097590157678620412464707919841087893184829799608291285025311386141897443342339895008930069979119261329436269651109803887141662013343345028327523396605031443141030592979074596095070340312564687602986967266200786007714529350708962680726180746170956434173926017391622625291269300493801401238866649332201049213884005284754844622216036725883210484281900413018082044160765680068545730501956460127342127985093814606350480667478728863376261758126837050880274579949598697992842161056923512008600132544448294200841589522500515326481026313488530269470428635356327011931075754801614951075174943281308119508487291913235980410376079341266842196873651243603900681632567868476973069932723815255465392820291318664946519344004970009655907607290026098369856940246699413112568838033475782130066576063234579076743137582968573831428223962433352098283374416391165256378809417689587775337229883660926670436787439976431849966558550993282514936484057496667144689512472917843887180133273405223385986170784235669630977598328782913236835975031624750449407439661249572312121089303775982530127100839700140234991905818113971710361731139305433120908241626049142242735873123856240503836917158412187864194547248768993721977403521327683731515035047114172696485817179248917490009209278478328750960045799740279062179161178468677252070278317310005303968311912857579673877649352912714860003562400484198803659486481750057023973660961789869836076670154829167736376240161200125847190646923144768413174724141120886850577811686805775815646094267765594470851387169800231908554869073543084999111082531238009835181748494035935970910076369437309379264050957253821751370830501980946293743365352524897540097111077417153535148530365946003377270456284573336614403275690819299705785249615255373207238268158894348748901694197861637204936251002306785950527925538395112283254810817125107801796287753263520088494441764001321707715354826697830996588138426232125594311787009795513953576866779767507238429611460775227571898834531649707618706825138461254621/285933079263816169413144541851492774693637760482340422924850373902918308816255528525172371495374549738837060300611787233194113976284527739171236679536490525249740812803687839049609334024581468693383571469393366403454569425825778777488435590962056082494036443800744733494479442306669356210402336518388024856372969899345962769818846576604495220532163650595992697790510902477525797117452376619251798034179672088688151793713781307108470359703815344098725460329322524768313640863088573187756591027103963342796421522373286918376660042483773002613205961723332709362826545169611843629757234387605551976455877457493693953865813941840969457108135977362737464798302288012028141980718501366399402353496206345614818918005816405967882467721191462092319071898367278404829820529516870466533723175323267228077946836568930189170080735522195049968325809069203955926060272787397547736675795575839590753375585122289558762124625511690002057915913780530623908096317180723335928736059212712565961282141471592273501222852732975249204340095038537218518879766135315526153052783478929783824841084245345183380418156767455659749391454874190497732942505042314702438270010844904380041358852660613332618990316041162958561059105087174721043578510585586037018883777607101285014631497074790660455512147172458162490403406088894897345491526917085359232859073781679212773956396743059366079758002448932173591047353092646642250006864939981144436091698023571410966211278546501056482344198531633282489087150074329774491807869868050368702609984703595771804565836834489179348160844445540193048550640645198792507523856969968059666939586495986645094799427038656373395532817515208024290860201966377672535670288007162093067705611187049909308660654075245387894773696125716308180689547874594724726991214072286726609194594123546046311834963573671594387313500100696164673659280086447417875426696581692494526458146176679301179150583290119986885804029722309121636372378706353823225860830979411024341155084344850606916792608195089470069296753772078845728052404012245837962382000412647514568685282879743958443532144854688880680220910410363245043375128815756426793704162475769162846126374606153687055467620078012707585042405830514056366452312205131267339483538726957115365182305926482979742520728404408517614517229931165788697582013983929288006130824110416050264053600345212465247222295960752013886006340831930220757762077006824543397765618303089731475111467870392577006916542521433340399181876582852066590459341170466040812929024 .. -454762919263738734272241693520100691590514981425785538026986622256312995564872130635695139705629304909829100623687308744314570363180468149048866912675119005002599759985103988348151073719030940237407603642750836260764634042265883755981320844786921457276790434017500957537779168357062225083179093817127052921125423890654234783359293510258610344146174640060061940389148103830251854100512225110040973109253819044002827584325150787633254506640896768042810354042002908153089309564868774397539419655103116176979960271973296207449902072821256327846535474360835584973752232517494779815332359067412777450971785415503335836257081880849151257860785257648244768649023767585078141171900746741816550196501928632337677240670181545186542739108543481504347905656322817325123450350309716662333050262303471001321188711155554009181470802621070475103254520511040191420017136432625489115031835531996273453651587620166869682215844065439531709262720068644987399674498210540264230878002150033136112073550210397380625128831620256578372132567367607158839081752982768938700403737768793735820327029877121822978308995102594019835316710549218412810900975170408141967119243267483180953813866348205072829666236629836001242502413976901822506524592464235061674853278142209508368945532516644015808644769185784395742143457857055990608338024570843604097791314094702354422396943834307470915231667609196859994107962491639637748320628734121014374166786172378118229460971795033318351305846496542696058917407744399582195728309208993757906187612351859915312393078030272325943995632531775209925035058747976454528492927590432784826358280227060406512285560683968280964060125959229289603046966048636812192248430494350880331920932878758761778543174121454294812229372502302319619582187740011449935069765544790294617169313017569579327501325992077978214394918469412338228178715000890600121049700914871620437514255993415240447467459019167538707291934094060040300031461797661730786192103293681035280221712644452921701443953911523566941398617712846792450057977138717268385771249777770632809502458795437123508983992727519092359327344816012739313455437842707625495236573435841338131224385024277769354288383787132591486500844317614071143334153600818922704824926446312403813843301809567039723587187225423549465409301234062750576696487631981384598778070813702704281276950449071938315880022123610441000330426928838706674457749147034606558031398577946752448878488394216694941876809607402865193806892974708632912426904676706284615298893/71483269815954042353286135462873193673409440120585105731212593475729577204063882131293092873843637434709265075152946808298528494071131934792809169884122631312435203200921959762402333506145367173345892867348341600863642356456444694372108897740514020623509110950186183373619860576667339052600584129597006214093242474836490692454711644151123805133040912648998174447627725619381449279363094154812949508544918022172037948428445326777117589925953836024681365082330631192078410215772143296939147756775990835699105380593321729594165010620943250653301490430833177340706636292402960907439308596901387994113969364373423488466453485460242364277033994340684366199575572003007035495179625341599850588374051586403704729501454101491970616930297865523079767974591819601207455132379217616633430793830816807019486709142232547292520183880548762492081452267300988981515068196849386934168948893959897688343896280572389690531156377922500514478978445132655977024079295180833982184014803178141490320535367898068375305713183243812301085023759634304629719941533828881538263195869732445956210271061336295845104539191863914937347863718547624433235626260578675609567502711226095010339713165153333154747579010290739640264776271793680260894627646396509254720944401775321253657874268697665113878036793114540622600851522223724336372881729271339808214768445419803193489099185764841519939500612233043397761838273161660562501716234995286109022924505892852741552819636625264120586049632908320622271787518582443622951967467012592175652496175898942951141459208622294837040211111385048262137660161299698126880964242492014916734896623996661273699856759664093348883204378802006072715050491594418133917572001790523266926402796762477327165163518811346973693424031429077045172386968648681181747803518071681652298648530886511577958740893417898596828375025174041168414820021611854468856674145423123631614536544169825294787645822529996721451007430577280409093094676588455806465207744852756085288771086212651729198152048772367517324188443019711432013101003061459490595500103161878642171320719935989610883036213672220170055227602590811260843782203939106698426040618942290711531593651538421763866905019503176896260601457628514091613078051282816834870884681739278841295576481620744935630182101102129403629307482791447174395503495982322001532706027604012566013400086303116311805573990188003471501585207982555189440519251706135849441404575772432868777866967598144251729135630358335099795469145713016647614835292616510203232256)+185517/1600 from intermediate relation 729/40*RootOf(675*_Z^2+4320*_Z+164,-1819051677054954937088966774080402766362059925703142152107946489025251982259488522542780558822517219639316402494749234977258281452721872596195467650700476020010399039940415953392604294876123760949630414571003345043058536169063535023925283379147685829107161736070003830151116673428248900332716375268508211684501695562616939133437174041034441376584698560240247761556592415321007416402048900440163892437015276176011310337300603150533018026563587072171241416168011632612357238259475097590157678620412464707919841087893184829799608291285025311386141897443342339895008930069979119261329436269651109803887141662013343345028327523396605031443141030592979074596095070340312564687602986967266200786007714529350708962680726180746170956434173926017391622625291269300493801401238866649332201049213884005284754844622216036725883210484281900413018082044160765680068545730501956460127342127985093814606350480667478728863376261758126837050880274579949598697992842161056923512008600132544448294200841589522500515326481026313488530269470428635356327011931075754801614951075174943281308119508487291913235980410376079341266842196873651243603900681632567868476973069932723815255465392820291318664946519344004970009655907607290026098369856940246699413112568838033475782130066576063234579076743137582968573831428223962433352098283374416391165256378809417689587775337229883660926670436787439976431849966558550993282514936484057496667144689512472917843887180133273405223385986170784235669630977598328782913236835975031624750449407439661249572312121089303775982530127100839700140234991905818113971710361731139305433120908241626049142242735873123856240503836917158412187864194547248768993721977403521327683731515035047114172696485817179248917490009209278478328750960045799740279062179161178468677252070278317310005303968311912857579673877649352912714860003562400484198803659486481750057023973660961789869836076670154829167736376240161200125847190646923144768413174724141120886850577811686805775815646094267765594470851387169800231908554869073543084999111082531238009835181748494035935970910076369437309379264050957253821751370830501980946293743365352524897540097111077417153535148530365946003377270456284573336614403275690819299705785249615255373207238268158894348748901694197861637204936251002306785950527925538395112283254810817125107801796287753263520088494441764001321707715354826697830996588138426232125594311787009795513953576866779767507238429611460775227571898834531649707618706825138461254621/285933079263816169413144541851492774693637760482340422924850373902918308816255528525172371495374549738837060300611787233194113976284527739171236679536490525249740812803687839049609334024581468693383571469393366403454569425825778777488435590962056082494036443800744733494479442306669356210402336518388024856372969899345962769818846576604495220532163650595992697790510902477525797117452376619251798034179672088688151793713781307108470359703815344098725460329322524768313640863088573187756591027103963342796421522373286918376660042483773002613205961723332709362826545169611843629757234387605551976455877457493693953865813941840969457108135977362737464798302288012028141980718501366399402353496206345614818918005816405967882467721191462092319071898367278404829820529516870466533723175323267228077946836568930189170080735522195049968325809069203955926060272787397547736675795575839590753375585122289558762124625511690002057915913780530623908096317180723335928736059212712565961282141471592273501222852732975249204340095038537218518879766135315526153052783478929783824841084245345183380418156767455659749391454874190497732942505042314702438270010844904380041358852660613332618990316041162958561059105087174721043578510585586037018883777607101285014631497074790660455512147172458162490403406088894897345491526917085359232859073781679212773956396743059366079758002448932173591047353092646642250006864939981144436091698023571410966211278546501056482344198531633282489087150074329774491807869868050368702609984703595771804565836834489179348160844445540193048550640645198792507523856969968059666939586495986645094799427038656373395532817515208024290860201966377672535670288007162093067705611187049909308660654075245387894773696125716308180689547874594724726991214072286726609194594123546046311834963573671594387313500100696164673659280086447417875426696581692494526458146176679301179150583290119986885804029722309121636372378706353823225860830979411024341155084344850606916792608195089470069296753772078845728052404012245837962382000412647514568685282879743958443532144854688880680220910410363245043375128815756426793704162475769162846126374606153687055467620078012707585042405830514056366452312205131267339483538726957115365182305926482979742520728404408517614517229931165788697582013983929288006130824110416050264053600345212465247222295960752013886006340831930220757762077006824543397765618303089731475111467870392577006916542521433340399181876582852066590459341170466040812929024 .. -454762919263738734272241693520100691590514981425785538026986622256312995564872130635695139705629304909829100623687308744314570363180468149048866912675119005002599759985103988348151073719030940237407603642750836260764634042265883755981320844786921457276790434017500957537779168357062225083179093817127052921125423890654234783359293510258610344146174640060061940389148103830251854100512225110040973109253819044002827584325150787633254506640896768042810354042002908153089309564868774397539419655103116176979960271973296207449902072821256327846535474360835584973752232517494779815332359067412777450971785415503335836257081880849151257860785257648244768649023767585078141171900746741816550196501928632337677240670181545186542739108543481504347905656322817325123450350309716662333050262303471001321188711155554009181470802621070475103254520511040191420017136432625489115031835531996273453651587620166869682215844065439531709262720068644987399674498210540264230878002150033136112073550210397380625128831620256578372132567367607158839081752982768938700403737768793735820327029877121822978308995102594019835316710549218412810900975170408141967119243267483180953813866348205072829666236629836001242502413976901822506524592464235061674853278142209508368945532516644015808644769185784395742143457857055990608338024570843604097791314094702354422396943834307470915231667609196859994107962491639637748320628734121014374166786172378118229460971795033318351305846496542696058917407744399582195728309208993757906187612351859915312393078030272325943995632531775209925035058747976454528492927590432784826358280227060406512285560683968280964060125959229289603046966048636812192248430494350880331920932878758761778543174121454294812229372502302319619582187740011449935069765544790294617169313017569579327501325992077978214394918469412338228178715000890600121049700914871620437514255993415240447467459019167538707291934094060040300031461797661730786192103293681035280221712644452921701443953911523566941398617712846792450057977138717268385771249777770632809502458795437123508983992727519092359327344816012739313455437842707625495236573435841338131224385024277769354288383787132591486500844317614071143334153600818922704824926446312403813843301809567039723587187225423549465409301234062750576696487631981384598778070813702704281276950449071938315880022123610441000330426928838706674457749147034606558031398577946752448878488394216694941876809607402865193806892974708632912426904676706284615298893/71483269815954042353286135462873193673409440120585105731212593475729577204063882131293092873843637434709265075152946808298528494071131934792809169884122631312435203200921959762402333506145367173345892867348341600863642356456444694372108897740514020623509110950186183373619860576667339052600584129597006214093242474836490692454711644151123805133040912648998174447627725619381449279363094154812949508544918022172037948428445326777117589925953836024681365082330631192078410215772143296939147756775990835699105380593321729594165010620943250653301490430833177340706636292402960907439308596901387994113969364373423488466453485460242364277033994340684366199575572003007035495179625341599850588374051586403704729501454101491970616930297865523079767974591819601207455132379217616633430793830816807019486709142232547292520183880548762492081452267300988981515068196849386934168948893959897688343896280572389690531156377922500514478978445132655977024079295180833982184014803178141490320535367898068375305713183243812301085023759634304629719941533828881538263195869732445956210271061336295845104539191863914937347863718547624433235626260578675609567502711226095010339713165153333154747579010290739640264776271793680260894627646396509254720944401775321253657874268697665113878036793114540622600851522223724336372881729271339808214768445419803193489099185764841519939500612233043397761838273161660562501716234995286109022924505892852741552819636625264120586049632908320622271787518582443622951967467012592175652496175898942951141459208622294837040211111385048262137660161299698126880964242492014916734896623996661273699856759664093348883204378802006072715050491594418133917572001790523266926402796762477327165163518811346973693424031429077045172386968648681181747803518071681652298648530886511577958740893417898596828375025174041168414820021611854468856674145423123631614536544169825294787645822529996721451007430577280409093094676588455806465207744852756085288771086212651729198152048772367517324188443019711432013101003061459490595500103161878642171320719935989610883036213672220170055227602590811260843782203939106698426040618942290711531593651538421763866905019503176896260601457628514091613078051282816834870884681739278841295576481620744935630182101102129403629307482791447174395503495982322001532706027604012566013400086303116311805573990188003471501585207982555189440519251706135849441404575772432868777866967598144251729135630358335099795469145713016647614835292616510203232256) < -185517/1600, and hence the truth of the relation at extremely high precision (4046 digits)

  

Error, (in QuantifierElimination:-CylindricalAlgebraicDecompose) could not deduce sign of expression 268320*RootOf(_Z^2-4*_Z-3108,-492127911263632402423205713918799836904518676377048162992425734429860793731692159936602972936481041248623526526994722874660367271768174356169928553332951393419498776555955286893869001918647998412799011529468450574092033732574096246243075031960795210042594808195798865398335267427983632719074123660562225097737665568262936856232311715568036890231233556152048222985357975992190080693288389791302366783810231268184440077584519639030645274422543999884562893777193243508118616743834957282569981104272280385835288085232560051621140377993888298476658250637201897294462189693950496517725957548756442463996367694331835037672629250759616685287612144860043644654894247263008208959006749596183427232967937431422131992093153508395261469381823996699091048161869871322071652835568855691765196772918496299912543255329175183515700920916067877879984017407026209322547432665038498259378068022546783929817083415128153235344508927096692783925852196758999834951193030350855575649918467465480693402751011140405500094860137192509783115336658146795491835972228617740390843735892922168944588246907048524545667312466256649220165552267706084791685040495928909128159630953978136334359128846698928333954854907841861076262567269324227398973214419132527091503404022663598784745346467992010414933195414002982430699763388214297190092795055680666828359564692048273660527199926376627631594055083012084088435742248121611350735646981726816404043276661827996076294397135036065481195660831387872762010772027078907852012584267238876804835818549566339095826846386847023797071776488095353806918389884858737649798124892405607894636830504617083938369000898745839129545274037806848045896556982412424357215235329103644691716255214336081649377276962865227433439937120188638909850019231053644056344491101277662549251041205859845425237391856172192100920248639011897043923753529872561012003061403244043871735543387329617818369718253806449654460263067871454693475736765964789544285886195045254635603660126254287013897244681993052578074137534691266635113429902841966392451431249361489947985342817220109659665533629189264855187085250679258065129754474016088808974529737297953415496038520242422516199294764395494117459002846504408607409681823267832824633900558672300395031011267063694399498779745192690363028084634374813283330322179279293244551829295401546537527094160742631891193175961979095253696393062479670340536436137190591148134722469329390555337754710690848744601498992850092835433086458564473547950847570049066609295603769/9149858536442117421220625339247768790196408335434893533595211964893385882120176912805515887851985591642785929619577191462211647241104887653479573745167696807991706009718010849587498688786606998188274287020587724910546221626424920879629938910785794639809166201623831471823342153813419398732874768588416795403935036779070808634203090451343847057029236819071766329296348879280825507758476051816057537093749506838020857398841001827471051510522091011159214730538320792586036507618834342008210912867326826969485488715945181388053121359480736083622590775146646699610449445427578996152231500403377663246588078639798206523706046138911022627460351275607598873545673216384900543382992043724780875311878603059674205376186124990972238967078126786954210300747752908954554256944539854929079141610344551298494298770205766053442583536710241598986425890214526589633928729196721527573625458426866904108018723913265880387988016374080065853309240976979965059082149783146749719553894806802110761028527090952752039131287455207974538883041233190992604152516330096836897689071325753082394914695851045868173381016558581111980526555974095927454160161354070478024640347036940161323483285139626643807690113317214673953891362789591073394512338738753184604280883427241120468207906393301134576388709518661199692908994844636715055728861346731495451490361013734808766604695777899714552256078365829554913515298964692552000219678079396621954934336754285150918760913488033807435014353012265039650788802378552783737851835777611798483519510515064697746106778703653739141147022257286177553620500646361360240763423038977909342066767871572643033581665237003948657050160486656777307526462924085521141449216229186978166579557985597097877140930407852412632758276022921861782065531987031191263718850313175251494227011953473481978718834357491020394032003222277269557096962766317372013654290614159824846660677653737637732818665283839580345728951113891892363916118603322343227546591341152778916962699035219421337363462242863042217496120706523063297676928391866814796224013204720466197929052151806670193028635350044181767069133131623841388004122104205657398533199224613211076043987396917985774963842496406642721356986576449803726473990564200554863473239262627691685833789647455351760663308941072563664551357797305238322624447485737216196186371533313608449715211046798887911113470744064444352202906621767064248386464218385388728499785698871407203566971852562464221329360685866892773820050651266130894698917454913306013728768 .. -246063955631816201211602856959399918452259338188524081496212867214930396865846079968301486468240520624311763263497361437330183635884087178084964276666475696709749388277977643446934500959323999206399505764734225287046016866287048123121537515980397605021297404097899432699167633713991816359537061830281112548868832784131468428116155857784018445115616778076024111492678987996095040346644194895651183391905115634092220038792259819515322637211271999942281446888596621754059308371917478641284990552136140192917644042616280025810570188996944149238329125318600948647231094846975248258862978774378221231998183847165917518836314625379808342643806072430021822327447123631504104479503374798091713616483968715711065996046576754197630734690911998349545524080934935661035826417784427845882598386459248149956271627664587591757850460458033938939992008703513104661273716332519249129689034011273391964908541707564076617672254463548346391962926098379499917475596515175427787824959233732740346701375505570202750047430068596254891557668329073397745917986114308870195421867946461084472294123453524262272833656233128324610082776133853042395842520247964454564079815476989068167179564423349464166977427453920930538131283634662113699486607209566263545751702011331799392372673233996005207466597707001491215349881694107148595046397527840333414179782346024136830263599963188313815797027541506042044217871124060805675367823490863408202021638330913998038147198567518032740597830415693936381005386013539453926006292133619438402417909274783169547913423193423511898535888244047676903459194942429368824899062446202803947318415252308541969184500449372919564772637018903424022948278491206212178607617664551822345858127607168040824688638481432613716719968560094319454925009615526822028172245550638831274625520602929922712618695928086096050460124319505948521961876764936280506001530701622021935867771693664808909184859126903224827230131533935727346737868382982394772142943097522627317801830063127143506948622340996526289037068767345633317556714951420983196225715624680744973992671408610054829832766814594632427593542625339629032564877237008044404487264868648976707748019260121211258099647382197747058729501423252204303704840911633916412316950279336150197515505633531847199749389872596345181514042317187406641665161089639646622275914647700773268763547080371315945596587980989547626848196531239835170268218068595295574067361234664695277668877355345424372300749496425046417716543229282236773975423785024533304647713311/4574929268221058710610312669623884395098204167717446766797605982446692941060088456402757943925992795821392964809788595731105823620552443826739786872583848403995853004859005424793749344393303499094137143510293862455273110813212460439814969455392897319904583100811915735911671076906709699366437384294208397701967518389535404317101545225671923528514618409535883164648174439640412753879238025908028768546874753419010428699420500913735525755261045505579607365269160396293018253809417171004105456433663413484742744357972590694026560679740368041811295387573323349805224722713789498076115750201688831623294039319899103261853023069455511313730175637803799436772836608192450271691496021862390437655939301529837102688093062495486119483539063393477105150373876454477277128472269927464539570805172275649247149385102883026721291768355120799493212945107263294816964364598360763786812729213433452054009361956632940193994008187040032926654620488489982529541074891573374859776947403401055380514263545476376019565643727603987269441520616595496302076258165048418448844535662876541197457347925522934086690508279290555990263277987047963727080080677035239012320173518470080661741642569813321903845056658607336976945681394795536697256169369376592302140441713620560234103953196650567288194354759330599846454497422318357527864430673365747725745180506867404383302347888949857276128039182914777456757649482346276000109839039698310977467168377142575459380456744016903717507176506132519825394401189276391868925917888805899241759755257532348873053389351826869570573511128643088776810250323180680120381711519488954671033383935786321516790832618501974328525080243328388653763231462042760570724608114593489083289778992798548938570465203926206316379138011460930891032765993515595631859425156587625747113505976736740989359417178745510197016001611138634778548481383158686006827145307079912423330338826868818866409332641919790172864475556945946181958059301661171613773295670576389458481349517609710668681731121431521108748060353261531648838464195933407398112006602360233098964526075903335096514317675022090883534566565811920694002061052102828699266599612306605538021993698458992887481921248203321360678493288224901863236995282100277431736619631313845842916894823727675880331654470536281832275678898652619161312223742868608098093185766656804224857605523399443955556735372032222176101453310883532124193232109192694364249892849435703601783485926281232110664680342933446386910025325633065447349458727456653006864384)+210100816 from intermediate relation 268320*RootOf(_Z^2-4*_Z-3108,-492127911263632402423205713918799836904518676377048162992425734429860793731692159936602972936481041248623526526994722874660367271768174356169928553332951393419498776555955286893869001918647998412799011529468450574092033732574096246243075031960795210042594808195798865398335267427983632719074123660562225097737665568262936856232311715568036890231233556152048222985357975992190080693288389791302366783810231268184440077584519639030645274422543999884562893777193243508118616743834957282569981104272280385835288085232560051621140377993888298476658250637201897294462189693950496517725957548756442463996367694331835037672629250759616685287612144860043644654894247263008208959006749596183427232967937431422131992093153508395261469381823996699091048161869871322071652835568855691765196772918496299912543255329175183515700920916067877879984017407026209322547432665038498259378068022546783929817083415128153235344508927096692783925852196758999834951193030350855575649918467465480693402751011140405500094860137192509783115336658146795491835972228617740390843735892922168944588246907048524545667312466256649220165552267706084791685040495928909128159630953978136334359128846698928333954854907841861076262567269324227398973214419132527091503404022663598784745346467992010414933195414002982430699763388214297190092795055680666828359564692048273660527199926376627631594055083012084088435742248121611350735646981726816404043276661827996076294397135036065481195660831387872762010772027078907852012584267238876804835818549566339095826846386847023797071776488095353806918389884858737649798124892405607894636830504617083938369000898745839129545274037806848045896556982412424357215235329103644691716255214336081649377276962865227433439937120188638909850019231053644056344491101277662549251041205859845425237391856172192100920248639011897043923753529872561012003061403244043871735543387329617818369718253806449654460263067871454693475736765964789544285886195045254635603660126254287013897244681993052578074137534691266635113429902841966392451431249361489947985342817220109659665533629189264855187085250679258065129754474016088808974529737297953415496038520242422516199294764395494117459002846504408607409681823267832824633900558672300395031011267063694399498779745192690363028084634374813283330322179279293244551829295401546537527094160742631891193175961979095253696393062479670340536436137190591148134722469329390555337754710690848744601498992850092835433086458564473547950847570049066609295603769/9149858536442117421220625339247768790196408335434893533595211964893385882120176912805515887851985591642785929619577191462211647241104887653479573745167696807991706009718010849587498688786606998188274287020587724910546221626424920879629938910785794639809166201623831471823342153813419398732874768588416795403935036779070808634203090451343847057029236819071766329296348879280825507758476051816057537093749506838020857398841001827471051510522091011159214730538320792586036507618834342008210912867326826969485488715945181388053121359480736083622590775146646699610449445427578996152231500403377663246588078639798206523706046138911022627460351275607598873545673216384900543382992043724780875311878603059674205376186124990972238967078126786954210300747752908954554256944539854929079141610344551298494298770205766053442583536710241598986425890214526589633928729196721527573625458426866904108018723913265880387988016374080065853309240976979965059082149783146749719553894806802110761028527090952752039131287455207974538883041233190992604152516330096836897689071325753082394914695851045868173381016558581111980526555974095927454160161354070478024640347036940161323483285139626643807690113317214673953891362789591073394512338738753184604280883427241120468207906393301134576388709518661199692908994844636715055728861346731495451490361013734808766604695777899714552256078365829554913515298964692552000219678079396621954934336754285150918760913488033807435014353012265039650788802378552783737851835777611798483519510515064697746106778703653739141147022257286177553620500646361360240763423038977909342066767871572643033581665237003948657050160486656777307526462924085521141449216229186978166579557985597097877140930407852412632758276022921861782065531987031191263718850313175251494227011953473481978718834357491020394032003222277269557096962766317372013654290614159824846660677653737637732818665283839580345728951113891892363916118603322343227546591341152778916962699035219421337363462242863042217496120706523063297676928391866814796224013204720466197929052151806670193028635350044181767069133131623841388004122104205657398533199224613211076043987396917985774963842496406642721356986576449803726473990564200554863473239262627691685833789647455351760663308941072563664551357797305238322624447485737216196186371533313608449715211046798887911113470744064444352202906621767064248386464218385388728499785698871407203566971852562464221329360685866892773820050651266130894698917454913306013728768 .. -246063955631816201211602856959399918452259338188524081496212867214930396865846079968301486468240520624311763263497361437330183635884087178084964276666475696709749388277977643446934500959323999206399505764734225287046016866287048123121537515980397605021297404097899432699167633713991816359537061830281112548868832784131468428116155857784018445115616778076024111492678987996095040346644194895651183391905115634092220038792259819515322637211271999942281446888596621754059308371917478641284990552136140192917644042616280025810570188996944149238329125318600948647231094846975248258862978774378221231998183847165917518836314625379808342643806072430021822327447123631504104479503374798091713616483968715711065996046576754197630734690911998349545524080934935661035826417784427845882598386459248149956271627664587591757850460458033938939992008703513104661273716332519249129689034011273391964908541707564076617672254463548346391962926098379499917475596515175427787824959233732740346701375505570202750047430068596254891557668329073397745917986114308870195421867946461084472294123453524262272833656233128324610082776133853042395842520247964454564079815476989068167179564423349464166977427453920930538131283634662113699486607209566263545751702011331799392372673233996005207466597707001491215349881694107148595046397527840333414179782346024136830263599963188313815797027541506042044217871124060805675367823490863408202021638330913998038147198567518032740597830415693936381005386013539453926006292133619438402417909274783169547913423193423511898535888244047676903459194942429368824899062446202803947318415252308541969184500449372919564772637018903424022948278491206212178607617664551822345858127607168040824688638481432613716719968560094319454925009615526822028172245550638831274625520602929922712618695928086096050460124319505948521961876764936280506001530701622021935867771693664808909184859126903224827230131533935727346737868382982394772142943097522627317801830063127143506948622340996526289037068767345633317556714951420983196225715624680744973992671408610054829832766814594632427593542625339629032564877237008044404487264868648976707748019260121211258099647382197747058729501423252204303704840911633916412316950279336150197515505633531847199749389872596345181514042317187406641665161089639646622275914647700773268763547080371315945596587980989547626848196531239835170268218068595295574067361234664695277668877355345424372300749496425046417716543229282236773975423785024533304647713311/4574929268221058710610312669623884395098204167717446766797605982446692941060088456402757943925992795821392964809788595731105823620552443826739786872583848403995853004859005424793749344393303499094137143510293862455273110813212460439814969455392897319904583100811915735911671076906709699366437384294208397701967518389535404317101545225671923528514618409535883164648174439640412753879238025908028768546874753419010428699420500913735525755261045505579607365269160396293018253809417171004105456433663413484742744357972590694026560679740368041811295387573323349805224722713789498076115750201688831623294039319899103261853023069455511313730175637803799436772836608192450271691496021862390437655939301529837102688093062495486119483539063393477105150373876454477277128472269927464539570805172275649247149385102883026721291768355120799493212945107263294816964364598360763786812729213433452054009361956632940193994008187040032926654620488489982529541074891573374859776947403401055380514263545476376019565643727603987269441520616595496302076258165048418448844535662876541197457347925522934086690508279290555990263277987047963727080080677035239012320173518470080661741642569813321903845056658607336976945681394795536697256169369376592302140441713620560234103953196650567288194354759330599846454497422318357527864430673365747725745180506867404383302347888949857276128039182914777456757649482346276000109839039698310977467168377142575459380456744016903717507176506132519825394401189276391868925917888805899241759755257532348873053389351826869570573511128643088776810250323180680120381711519488954671033383935786321516790832618501974328525080243328388653763231462042760570724608114593489083289778992798548938570465203926206316379138011460930891032765993515595631859425156587625747113505976736740989359417178745510197016001611138634778548481383158686006827145307079912423330338826868818866409332641919790172864475556945946181958059301661171613773295670576389458481349517609710668681731121431521108748060353261531648838464195933407398112006602360233098964526075903335096514317675022090883534566565811920694002061052102828699266599612306605538021993698458992887481921248203321360678493288224901863236995282100277431736619631313845842916894823727675880331654470536281832275678898652619161312223742868608098093185766656804224857605523399443955556735372032222176101453310883532124193232109192694364249892849435703601783485926281232110664680342933446386910025325633065447349458727456653006864384) < -210100816, and hence the truth of the relation at extremely high precision (4046 digits)

  
> 

Digits := 30
> 

timelimit(15, RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(`&A`([x, y, z]), eval(f__1, [:-And = :-`&and`, :-Implies = :-`&implies`])))
> 

timelimit(15, RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(`&A`([x, y, z]), eval(f__2, {:-And = :-`&and`, :-Implies = :-`&implies`})))

DBG> quit

  

Error, (in factors) time expired

  

Error, (in factor) time expired

  


 

Download cadpr.mw

So, how many digits of precision should be maintained for this question? 
Please Wait...