Storm.exact

Benchmark
Model:oscillators v.1 (DTMC)
Parameter(s)N = 8, T = 10, epsilon = 0.1, R = 1, mu = 0.1, lambda = 1.0
Property:time_to_synch (exp-reward)
Invocation (exact)
/home/tq429871/storm/build/bin/storm --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/oscillators/oscillators.8-10-0.1-1.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/oscillators/oscillators.props time_to_synch --constants mu=0.1,lambda=1.0 --exact --timemem
Sparse engine with exact model checking
Execution
Walltime:213.60334658622742s
Return code:0
Relative Error:2.6357075426279515e-29
Log
Storm 1.6.2

Date: Sat Sep  5 20:45:56 2020
Command line arguments: --prism /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/oscillators/oscillators.8-10-0.1-1.prism --prop /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks/qcomp/benchmarks/dtmc/oscillators/oscillators.props time_to_synch --constants 'mu=0.1,lambda=1.0' --exact --timemem
Current working directory: /rwthfs/rz/cluster/home/tq429871/git/storm-qcomp-benchmarks

Time for model input parsing: 14.211s.

Time for model construction: 79.040s.

-------------------------------------------------------------- 
Model type: 	DTMC (sparse)
States: 	24311
Transitions: 	76623
Reward Models:  time_to_synch
State Labels: 	3 labels
   * deadlock -> 0 item(s)
   * (((((((((((((((1 * k_1) + (1294427191/1600000000 * k_2)) + (494427191/1600000000 * k_3)) + (-(494427191/1600000000) * k_4)) + (-(1294427191/1600000000) * k_5)) + (-(1) * k_6)) + (-(1294427191/1600000000) * k_7)) + (-(494427191/1600000000) * k_8)) + (494427191/1600000000 * k_9)) + (1294427191/1600000000 * k_10)) / 8) ^ 2) + ((((((((((((0 * k_1) + (146946313073/250000000000 * k_2)) + (190211303259/200000000000 * k_3)) + (190211303259/200000000000 * k_4)) + (146946313073/250000000000 * k_5)) + (0 * k_6)) + (-(146946313073/250000000000) * k_7)) + (-(190211303259/200000000000) * k_8)) + (-(190211303259/200000000000) * k_9)) + (-(146946313073/250000000000) * k_10)) / 8) ^ 2)) ^ 1/2) >= 1) -> 2 item(s)
   * init -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "time_to_synch": R[exp]{"time_to_synch"}=? [F (((((((((((((((1 * k_1) + (1294427191/1600000000 * k_2)) + (494427191/1600000000 * k_3)) + (-(494427191/1600000000) * k_4)) + (-(1294427191/1600000000) * k_5)) + (-(1) * k_6)) + (-(1294427191/1600000000) * k_7)) + (-(494427191/1600000000) * k_8)) + (494427191/1600000000 * k_9)) + (1294427191/1600000000 * k_10)) / 8) ^ 2) + ((((((((((((0 * k_1) + (146946313073/250000000000 * k_2)) + (190211303259/200000000000 * k_3)) + (190211303259/200000000000 * k_4)) + (146946313073/250000000000 * k_5)) + (0 * k_6)) + (-(146946313073/250000000000) * k_7)) + (-(190211303259/200000000000) * k_8)) + (-(190211303259/200000000000) * k_9)) + (-(146946313073/250000000000) * k_10)) / 8) ^ 2)) ^ 1/2) >= 1)] ...
Result (for initial states): 3068470145750197019452155173743345427002196607205252358197547539530749752313446396505989612420207485372977681924249624833422138868345925426826712219172768032304377558895494862271089209157222899304898311282297885765407174579481010887694071551538821564678623767964599154601524324867140109165722077981501716095016980386025577860550537902183698756027027892768209479940319573397132574443421863800419397678403647410009599065273888073783074538622198564896916734365548047093400587864929684981074536610655411280175751341052805592367946881652390793978148460742051251357967002387777623791524606277899644864589924907291772572391700667356838318848293200635310736616488404001641625267284495184993238828634682033887647775884693021574680908230498656305203859785214594970394107673732045432000328389247592379486567696467557010961560617428180306536405474267744389534194846565387692694378518369441223886715317508258811998157842918077251359092545408401672894396645881101219823511997529110130570263918536732011250997067536345494472869686196214471974728397426066518385373660296818838649113089767212553473752958291981933410562143310267473543520642852693929355799171216435469765971135585627731305389788145972543581983371495379215286988422792012905699510743766356795412246608926681702454682000884685479480880064492968968686402437161687314352949723321765336220094409207943489679637078435409187319397230679113296114627917674243024615374920530333502041883306371642226741989836084255507864990329620640445304138493558600343512675278726173790720154542400789769193712058651531753801173712735307032457365879887731988929597175662767967014188061635236771653469177592544917933760388915199408183749554078153447345818996090721112013522353743145597807497063133015438798118163941196541051744551731782567481070102899554690750851440473565345337351145260055467155766378045416343396876353772532211347736392225423111765485370696003579575253099213620522504780247191947567017296847092934486614961377430208381793344917955516121591274079703642288532099321971947765190385934956333731260090249208869191932854179725214295299595081571905852670742816747881679824638469558344572634376683479943120261906241435534464005645385518864836074088162080462353947848607242070977356041598044671750912575837886523191949929486467139074381873656197144501114236418038616519841269986672202151026208546803277214381652330965961677809675668937472552394802447076305406612968218149659273629508487008219854374622248243976396616391907279705937947852074462514988877942102350001529593205663147015693707602233296215998061758504553027993536180230814432053387565934712682057748773826112162024582914420644094803431230635972891542777855369374269038482532149499837052168314365474609976819272257198350437218629876361699960166510466849083354060248078001543608836281971872856081245605186101333573830668899766007144970086621676793917289805226597671434230124794459605303890096851330539452938790614764595095801810268033141849441498968748923443650963497340202792046960368158809565056581073088599836635180660924805945627250390581848411167113745397631247544534540132849823750837097603522720432630274195385836727264143386078078451855207300594080353938753607761066589197960321638095906378749844016329899539847303069386655746426921514193464101458781134135474647154629199423210396602407229831217215881994960292678370546540028729752610923602896264540035047420222105554493465794997606102500660339051099591849869222991178266564757733415656223962868425296518918698132373054970268312673787187210052869334926912422719568541387753436782500623979920628739979951300618271615986865125490072156389452948085717093167257835140245673843249063194319186148526189174739594625495486627913418916429778965494816050660031839159169776584605643537882376917000284727047668627771768531945184461973427199340807185522521006557109365213426840552041229244452703626088615132623763373260563561627479317718466442043920212086800820890804895852144525191428274279002858027648763263888065651587223870922983919293861304850276866966586909120207898773871927213477415246747480706881966745430471843703184183594583030448753847647885891055866719404155842600837260469954994953023904941386032977860661477517262297139813111631204098488413704329855566523630006630028904239652488684190794797370576118777223940656096045777788637167250699426904175219653745009702349724008069915338271682444152063666089356941735495673840384497777334227146609478794357486279587884599114324337734445401340662188672634641038657893686998086326282616510809227298526574858569998804439495620054044127809191943280665082616481243346215221277329519498302781886455903474616544188581449507118144876079337347799827291968802499609626077802816336438348035632361809421183133049121265478952478221118057145982944307366873322592336324384615542144842997217893494227546871382595096141726408922976796345690130040785982042958010443799932680940569362143506793139013571245174439979705030987757507796250073947316038775588335294963893247147961822820036277586612815710925983860493926525751717390076977813912916724659965286378288086042090959266032287395317775581332085008223389429755645524160394355412599683232611278593697942666640127535190937348623318476548956411638248351510818979543711057598666428550378881361966590931642558452818634100642991886165445677236875747430527770861932356188702383728763899728760502829315951185419789773919776656108144849704645158740432084610652975342156525793666590635169946121192222221324165743097292060694900709696826245075318848224154032290312561556464943202742007169140434449587975500622037885949337602841267298792345574581797908366833253978725935118962280553322877740177809915102896533686568092107331482761589910583572400380369879932781329251093740075429303772816361730060160280017102209295064934160116084846595599555248448018181070492133199623333415281763241416122706221297580994878954682734716648060861840787914982428124083209947114265416505162273846107489895302409182732060350153482871867601473883616970242500869791199552649554987730094573138259588458595622294833013844620107811345684463299412114334309775233484137973479218403880796576554146742766518612659983919370079407604522923435220911006189687446510235320364050676672826660535811373417363754132034901583654635063803889426473044260132578358895814468959959409718442495132212942709166006446604781270713839810534012715758138525684017729791182248793272566412751512596976630042476635694646788212291587312596635791758652111782285881271368376635423116338607420747442160290746008293335580854582933691443196187538522774726599143891357764054421530058916670964138900986570901935436007618930058829959084065651164464230019800455651728709635145231010660876757033331216031632456295358312568153398432374461542359922364953094161350744088875733326347526919427064855504324676118420673390925749232578217489995321325925167893140460251502661805638397385595210651439491278116744728282240946173598537068231152621475827165688969460769014753543542276421149353944145749798746280340768312950817549839003846884574418194058200771028595086647973906387189534990138283696250006982789201113218277900744284717240148595517806047139905465864372926423094706546331027756648763835047277813182299347117625347981987940533112998485639991578963748318157207711805704025215304913923629366977935359624361195764807270806969661783652989777572421614383419494190018553248968447070797967177096834166647496244455447789340812727399060581368758417612035356756243930062288359518124087201750983987291742876359316987733203153305982662282449950150436638291858148059895771838160245183627654815560060777629447330410678906340566631298685425254490061541452156384498648516504109166166627013283538620265800077462068573431432238265891965419843092439051878486634879260013441276492001627985905829813552511617340440016233723446254858451710054409245162012210216830709057590445673165424557705854632159498037584400097427629829228808201926750191356573724552389977385305751971121060173014424218705298270274683731691276072361400645618977613547371762595573315258276077539177613294855123796954885211631769928198937978550557117674513307043361937344554349460487627752977907279330871325830382501170695054034882541036010669363616516029111669142212539224328136776771686611240147996845776362504348538935738165092797872666305244151343151873183698130568155079470187047951000409664850623505271104020208681510645714494913029010261285827261286056215599114428641942493446472944204271512449203817434701692014870769431626502541437080527421100520633303416374859149682573378560390571636895189882484258623228447451507394664064895490460999961335598657460211550364030523515229029898937721510688429788015638431812363139370031202151403227126036202992212178015926157243204874851651413708034801530455881064626171597591553855644741793800983459174008918128012681535808255212197356467995951734024990823779382435279247158526502595443733593342757477324017771812165521323948238087699594030042421690951521469255935780540068074840884068458200656449997057074091866673453812192034749346008967516860475203376355779961501849535042056536659525995485827849927374211313014369248622924177252225328048813399973424792735797049896295500253726966788134162501246883462691238063923107687263646945129643741693186339161743676933118883995417810389137136253691458143884454330195374975131620558984398656063869049227959052782348444573112368566113531191212806603038594485793017079766545448027341562881043454685041876768242116611540995080045561328525420124904926845573226843553083988621737815098271271338698067578803684330395483171494537241580379380673647448365203298581061755433978031619344303707668281131343387607415693034250579761431439761957779395602539172209983397379891719290773890008437561367420046576251949001346905887966006249285616857444950825130607960598171582985922128983762680879643391830076983181202809923001091228332479922062889015851183713257843552575746980544292226485016674855722646967759330512770899089399510275173253194241552119748303896252078157717645335050928956373345338991706718427791158716367051867116415019784059917052379884126153768224017532293106023186534092793678423130026549916695719392400436065322373317844240564150245994517140871800974255781654854543752020948452801275281312199926532050900211552848878007395724941530051407280934705394386723557104064861908851510366518310677516551399775851539321524766260259948497323592462252563350983041372995570599433120588512230412600600105998407242061604074255318172320872365961017321562774095723533574978676494663837534710711724697574059227204062956197615096575752490158585673467187763910076766087711901741751616905160478705733070116017233619920473155917115524138681500758799853192525350420858719364060790926442116982049826005029396947436066078237413850794796987581409236898039639672932812392321752377901060897985299507369909756100857549505484855638830962180349230422623050476743276374015329392344529114227681588516961075810194209880506390197808135140098675161053164051857326116848287424006466973558478037940479238310511105338402337078593603348672178786583879191052504479008922691609579247943983475397978985472957720326172669725178215218192643388634319265396956021434808008296086501719584246512218527886579867022682140526526259396699520322709100306416669339834047511892094760977745220002209524346225343402502653798319524231585154067477905810666021940569297491002389482013769130717136798230108738747513511870878308084059659894532581603387286204120380196379615881278826327276067656180215190031047787978181127613369315087123181512887949610719141586130457989903986330969101285149987131358928279724095053663139385067133891483328028694135048290167417206979311658955404600136266441897930708532283058298876593518906809101589090486378043307666571589004811998325825208344271365563330654599674794379216002677804759793882954789876964962950658867856929721022574605684744503795059589621505255546288478743266623469168430633349284899956308123651642232839440988829642364757176259470121802281737538575406729696092060224468853867685254193093141748941917044084067226645491305582685695701851644009080388509887029582113616472172627963318215005291153269892371360721761141657137741349298411638154441160965747808769520780066854049515526283872106152101504832925444018434858152444194802168889355335141679569877108064466552887535481840938391934300416418822773378757778464616393142541158905133125059418976756151356654269586573317549163374398274800252891313818989444349295536487662665972776163709368638207581420375696708640261020879118151566904728918619052619913565943859573663529703632108829505824682573349696886384513945703309421126677740621175498095864551336977583145819602197120238241078313105296435200520435567417747079166454922329378507644107221033094085381323238909079778790950163911609017859597577596469959788267510959302658417794793949180188049551086983867231866257304004181499713685505446213542202445278097229210804157704253077596562981972277090060967551039212546386907993075960177993848431091930751145493440715797651172059933337234508279228905298437597054430525642330287292534384366141734865646370322288394729171293454057965056519276311829563333968428164146390075493446812546029675809878987349042931882252246368391996762462363377888716149949860002290700498810496292259810961059055913680761969295889361477217805611042508011309883472680801438672604807483214219623858095642907812562473494123177264538020597691467109775077462335428815231548996225933635997152854157573721670523291716240062527819049307762959465857450040146105746704453835959149447544547354396220089856683136056230999056209212484028840224572397055877888908383361199722686779834134864633730463834107878436473438458995590129266148999308019717307508317384639575742146494690608441127549040401994132072498334274050407017395290713508636348757098943498915272965225574895972158059045721614446547037134041915449073660068953424427109402922048123905520291371746231096184834148531614801464319407843508711751761898162431858698984192856335034350827392634866033694136519029762084643156875755924645057969975745468845550111957483538918465206808053641011058626947703632482262835130046719310135062818055322424049128623689086816097958682903900673991201689738322323131234702111659406491830120852065370224608643813274001195656006539323927043928759625624287802969490003487325787244487349675277404516699679800744657015386140892070182397964784811420239768934558524364781600363665520823613883156489503776294815918950262289768139593317551236633818542814240741146613265306928360865260497339575429232881815370121186816036668808485611133134722149290996534882040151908297163349471682257875450348948025566203918212588204557011950153970912003792306320307338225596498352333068574010019408964157407742572184692281168247711359255101476025739328087414119492849436443436779003636669662182590006312408289982300447298381821737343642946820549931474686992662523813319693914523252639838350946187295180534317008551079594014728141216883562983561860781454397858455258800667657861833195774282811173218478987220009199057490204830971852173350904748288736993309064369743340213867984308930626305897227522253198694336800644829866398552025679411777747789806806852715288824044660427200621053780591929328387140069883508625131868507128977359372927328482668215803206430538557901004785247504436205539100773349469245472207730767307939193334617830655969776365811574517974690263427481786485815529477517289971300042597157834512858911688766796458762308499631335621725304625466432670935164829114249200123569676613720602587462938223073440331056540394905791858870284913251653842769040194456948204421810293905837002723787240394380753342840611377298488420516864587852585024386087099552832107300572086951202276579019429531948364766325394204544706912824563379880281951738868113542754480791383824817780439564477439046860415734200740273735855003266547663746694909118657208280499651030163146155411866032854091038166688753354869626560118876240598522346080127257062622448082402097344214821044133729145277743194006714898724931067769083103582444963878504709694461/510779934679614554349252837266080179718404654581100808926751227749705892047232279988840442604960622599772487377337875345166975477578693110766696079881164628542284297033068016370368890449609473958575904812404236471702470451904217814201839461992782077088652400865428924095074146342346116270454232736333730635168894463597384134455436069234954124605797279997855062464785172958251097799504936881127373116799978645868429111859761482295099955199407897174107375640815736838548630031561677545217141255316512553361201740788691169239947555442672084336565978142720292253027995932975182017596705101603977486495377758055374860456344069783029629442133674575963822892187514717394976209864782758573020288757003641478611699738957825864296804110978349883298728772617934638121075579673327433606597330383588700752119838226371274492409202875775729099849729952826034953938345617331934305944490562449808772507905196363217995564282187540159405389432261542260906187257315533947750930845680470329726399011468714544730648458697640081202647750385210896572118112643064587170229652366416961490765872981834766712011328655539906587442618274792748260747432724421907161032722290625175996776295555592053108829710236164429757032703278822942975598910217924347463942580084277423507686447843708100362173978546446429682856146307827846853001323512301847972386461296024700995519753700195620235052607841527083086100492883568496109730436379966539182959662758588110137969807955314679045176384282286832921190629456425836768780744187081517476651050219409488111486137492671873007581358654170641732445155672670723985824026357540323300451133739145246304230016492435257647499347388046882498063139389225012371005006925647593687219560780697427368673000330052494721800169514730513297306149154211027151853801486345837718818425348218979017351635027249634981958545852387141236867171701432352888137867064618514670351969149908340177577150363951723198399188118412462685835239656717056188885387428929295360934218704761052151452395730432606233787474311220646736727771563454733045397537476160258059899098395504276261896612511928771513290119095231887581154777869948597804304922345056347964844092751456308085129534280002788124295738086016753334223281024973983654798401947202107256405370702129735666823121443573153432794245547200488036967093077384507203587394989037983595784946108259085841833146390849921396839619783621296720392251621544440999035762537855568595804379556711862446632511167969623351818400930392658961573260234700375451243509779082879003451893481187017203039025617891261786139011805032700370385016095928961562346372327396564414239103912060804076178891443592070693597493974482662192489998359365224321064580109232181295255762737498318769716149426407012541415934432845895525547230689447392683590878529353014169277281596568742733405996272143827922717938430487947222904008321599767030699728667464663016442257537309961971352053190317457086171249079855876472549979621272678539920626738637987614853952366796915736897933943728320606309292350856308055571938535122884086699193336693208510116363564176902081636868699499233681852334130807975670993083574043019281852874225680051126568619626401573583035312635025083835350900735888118856559777324754509051412275043262105430181020263592527629945892629472425422110789663130308414170326742759089432276871519272829009430957648724309666766814742128077021630834449834391845574837005490639177416866691560483593450503770321107090863720065347159755786257910939092268253163484581403192155913390100870098306459156793300936987388729734885473318646603780317001944108403174651324687124051661806010361931979177766623623002095229683758432759917462055086338782709838763484747618296758416304776290441185874640380352821702026482437860830994602362432157807827689183654044685741048733660670824598831604669243148155331584232974993361927256742272172817832089253916719946846900700818236167437157940481903384119541857151992540859054054730299214948916782448912716055609387420776609980377040086825751824672095000356750560720840158197549891636492397553237822556995417838002571528030308036157688869225553362389383804202097561296507606240077800376616956104480789516444376619803254160149561302249451719337857448742546883631511889757952708562937461168064462063319759439852739800895834701172311254601755028026587148449736092854017119022408667807778668090844045675038569892284302948958322945023242490917505310206333589111199594689854277773281934770538038568682429237573682345025468480548218663944845231781754963006883053109566153892607972898994784571935157639528896552334550353451188833270002400107089642386500540079179238976166488026379944207640170441950487796467164633789937224193768992170095618582063338898040461135518009142046840845175665718875994867454082630658971989039372544064723801412469694758931747632851689123328334907826207519867138014563845662957044435316842153538957473934621089138381214427004607939753250169893412208485128282020937630900998750508590385173663757730031564531790924051120163077810048154120361869234374503056901911249592135036118496795776158164535416340453943590738454839160477617534421529817203376469242405350619643824678151995667309709742382866346683588067193067751319468436576277988070167562574074203076848179111022767223819703966611537943239342318378376648976548264255019356911528559351498137225009755687192393208589764188053085310914832907002650819197765325108142532635225955668578370148783038633833002573596885492118365593759163357723260968629366947437990385078569720006227030486960977817477560577532032857661869203427798165078319780238796013294958050131004750274752214622273438980111861336499493228070736450680280141237669877714370347625151113352163001810550689605508579060130041760538212962509212100998287391836165918276424346161541057803567068365077316219750715847358407214930316533425097463662575209743137285583432306406427107102887031696011988559717823873141570582351593219367647107388591526779946851555075311141746754989182062708296024408752252936892671623538069251904724453435153620011457326663983231936801302315505939156429339526645662307652760046604758905130740220259589991705843276236381927821949466152669055422780519668451900642645040008032682084932971569048107691877103307072577627090789612218772582232535481774747893950281095171165810114707054934976628691238262125726332239700109305691112445881083218062492649006873075527291455427589711002322300968790097586503865254746413711029775859404184426615971946947741508542968654851851303913547400734470994667142146511894884719473208200965603009878954331166150065046583181396532356129646699756799615058839526964427516866558834112540798353522416425304007466707678802071924069987963658617245812548311896802275294782089769330914948933551152392995660732282806650771574565272447821710459643008527186599191901926235552279993435745277068181041490604847527667955972560019434999342719542491017333502409661308061776749092392545262920399913233789832896442435853037487431598744999233694121196165644621146446976921952943381416919740494547266576690239795559252671166945368084330822469125398485464591244575160214294454512742619897798015795317964099823347237944377958719498950548175648395804572969277990581405626228360421014727208127362949289993056764899640854627444106990468583068107582896258467495238632602695483463795114297767724019075410600838367390920883649256044909888053095053271189947291898399827404164967764666283589154672814874142441077568155069326188751151238922714231492000639543983534819833157849143760906344685422183523605544652011744598133537475679923342806698504494593047146595773041463589345406197989456405254978529459931337416354012866140092743322307994883969492154377411425446316527432833629151681863147308983468056651244355033322309584861364331010380365965341825815484860899191873562350370457140696875651819918925697389084224130013341798100811821413694238477912352275530522627787911706282819581029857876053397206907623847506660345938201238638927720172594607092322023443663462411545714503333232593009620219041432074078525552532637653463668932266282631962230358601055086297018799758105482770042831356796943028302397615548946799003343019005639636026153353494418249544062130288041815486780566992716535975016667579755598547735535593647809118425663301578146130901218555879859202777943031106332434225810083857065549105380894247936153911632770011940817531640829014493274195165490396948653358156265495654819287490095893284200116109090751442902556281450463674312333366594676628598133407025754513855688512862131673533815610413842770195654587649170705540705529105971788813266350470188191353262681046716787239988493075622301685402629947137845790310310475601417358803932213081313477544553424884811535934985570612180691045013037629463355817491230999135907930237802594730864434660497068803835997991042099810428030166152160284302623589543636928513092774945355020451526845752530329862137622154405745411015651402011614674091493861892038429411567101099511395446189996874749432087679847615419134296023360074173822187515288076897414882947103202988182579029456304700275600489594887042195350579375332994625031714870119095332777659306395288428883831330488579902052673739586144626610637812886520822549201835787984761773982864529040387902458060728940000098856501082784311731342019267038714715947313386051122750124144678810965147030937115653160739162013299846865880100433811753447960283553647490521410149520937036376308363057810081975728933009218182165928565910971869298621494975933096819785442012750571677975200639254744649781029499825797945581975531987549730271574826303336822324505081318833557338556967577965565640909025851957742335971674906445087562875278440741336791840138458062343855827367237777645434452446177783593375556736107502309297936592118940222446982113253049869123121363472319148209867270031150946705019916090976265965359499474444595270050454576226487977099237660480533371655176976277652874804899272558569269515279018422579387804941668311945706631349332516790401587004277551173432408462573889966948712684608540040537133777493188117105574777320254247384058545534744842687280144973358330926191391296553775529790163755479752649992179177489365166105332332019352124223353735564659046504162522982894280981075722371240664733652612863539811626654012806904390899394264933993930156162040575838155553922274568030495124314154053654892765714714704885363896925618415433216779428894157286136796450685302680238635851267046728845381110150598391588141930921172228055207211535334205267109555329531592483283363611661087133976290623129126434768234117101465077313525572077126629089591453164169444344776493311260936224651716068275744491775210171588601029907908431410658663377472243630097286309743121781860350905522089473340302314751326530677024756506045824412242124897376039985334271349461758038683766895698146607902247976580287695626106540301450222436755157946942790572675445322057486260432722970419567802114709488154366576268407402395248558551296656078875315176948120531082404044173554363940939074166213496585966083807575751150958429299996544313761481569581421532891616862130360432598149088168357507882186682452772577654088270836004701465167429010973576505160537018124639061012999591285777027288574693509684405604321770723110658281500580352653989146533563931643652772759751423203525609408534027466069096355247302773548303937219827593851218619220575778986732203513499785039897606862445917248164907016985397638831239418448302649474082925120068796101413397135645289232311620509864741362205428373675536927266264187547027994484999301014459766289301927888359741429212019778638347707446914159066103430840744422258123735854891375061166446121695841870954110253468036886542178759726122690049898599935702489414889419435400558712171187533424342777733447815016919293333277841185297326411586850996288388670496232099146339880675107982193839771808235904804275734467732603870099765555013138015875222743939457298885829668765328758571706501431559668284871650755679264953648318266405756930717112672358725542158583894513312348353230148296372543090579938054379877525562885118709162728524506069401222031734373063709256120790495434178158478168942093321813936419791936402481814395667787621461380515274703184412845249634431761995163612118130591077006528690789322554043009766236170487380794858672766981054353246838547846027298195909787501600654782981559459040926117733946196258284380239018673689043250282410166235635147779723676310229147717561865112581417867927590279243394066081277041640851954613044865379516018567083545956214125893581590157470488291745083811107496531161236531206447075708933877507971695352870031814911029949879212469810399461339763060317665241286200596642494013653208084702986418363638871585383451052439907946197071932934263234311194467695800610736789609969124989227450443999718967568073821610496413356904587580096965536082328306462719038750971910132768737491099119566888774512739294082241251138836496133941199274891857206322824279706751396693591610051754210995787898255184952023250981931834260102291359446126025904714321858235120429053332717663629501485940978626143725639012457024998631922384480569731046489775258608210114400300350071028486764206941190587668930902907484334945890666787773940978958877779079295356346322670577939506489744690434410270273881491910420002109974683906656782272676636138644588552252890281094048066877860733481516192897343797641486549431842761938973540882266264292139657210127282384665952786239706192602405642848553435387812828471267450294337179518625676260570229215137497400637431577870635053398134482841388901994093438128929278281761219163249390739714470939049715564312863856511130159094217086637089332918124299954112526944932202076813367485331398864601707309039300413550849037318700332193946328680341496104480286882896700104814222848270672168043010785240090323773435946039846029779070692292125795959980347580697291434353706451343138843117773124161932788197488730803754616104428940409744088299371777380831911385624277861871588264169292827875245615147727350624108614660559407718553915522259240386684926195282639501312593041024203285712662956994511278859148859315853640765408496492629552580439904278589709078511268187816851833391055069843487580274175823921686236653618479148056204301380742764504049081621207567065687763835789715630762072151041462952033819442526933698088749511761798623617987019102298059848879051210661297150691068611277904541009276106017820455101101132425414338294610044933237403535809687070910360077518527449964276905927228000832048846950624932696624558015740567496648578718432552920388940025013908296617860334871001292874505789892683995447907496086734601506997267830988465632531070421559774452727208185624361313368819539392092446146504895185313816404514988796108252532107319371855671474219475050739822842592087618744692261002403716138832098583675670863310110103317871874445489740091104058215829057474147919871049492841449471920579888100334756765537039741663920413534331172648174523951138513884614748063355199511841977358293414230274529887090628893955352026873356662684393691636429790792188230004028783997879161103530730163984596895280390616402781923944313531721949226437617009603078607475752583927580705114497865859962072211142472084014858203632367873677622302072575942274489603336638318352973052475095510189663366526301809805194069330055511416010638991879154909009961749810871576546243524768997498637271980532575614597682524420828195153868096194150588314432063608011849933125147076628888691154332387987519030031321104309363706461673534666443763826375719630368769381979642371926290041150722089698936841122025094074009804971148253585323340966754315055435213417720596886328745084249144913699391022686079653330112329385527217691453015452821046209733357299839675442236133087416326350536755019254734274759625160700039007991504323287157290948835222475631853898823137266145277831054376636732837196505170008770042131799333149507514814789306599605145375757300559688796560498935852995084664975090086645318306503458627703235327680931511861771728564453651703241600797280198831377579466587172165785248398697771855566248294400000000 (approx. 6.007421078)
Time for model checking: 115.467s.

Performance statistics:
  * peak memory usage: 822MB
  * CPU time: 212.035s
  * wallclock time: 213.521s