/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 power_consumption --constants mu=0.1,lambda=1.0 --exact --timemem
Sparse engine with exact model checking
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 power_consumption --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.530s.
Time for model construction: 103.372s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 24311
Transitions: 76623
Reward Models: power_consumption
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 "power_consumption": R[exp]{"power_consumption"}=? [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): 31806279394039551082690491004328456004688316892020042679462972695555304034625029084185686021479176250467707398438372379621967838705141731703945618382608747852156707564760748592824384742183969678448069377522469594385589033366723995843788705097888500088921915946846649377869137823562650869728200691609442221526131700337466117525967988902563587794208445516193167618388379038750945585954610638704717592271331836578256144709697752565321746851932227917575996337864929400944168959293532388107535457188640525920004453403355259278435161381188474990652644458055780473935883420033549834550848156624803648952992285623234302963712332028000307051916330041666541136754568735808466999894723957476858240240596116710332618076836849143755621814434478541237446985502634262413162420635983820463091744075521601858657600309185535707610336533480918881517363842897872251161528725407725056344949830649880269374510765326010566256401083680032881963607040581164858598283124387986329755536777697734086828094175410886812814766940536413345900110283589643469002151105457539848028830114066139376412945509298416598580945036672974248472624848852624184885211508695912212524999262067349758071274891457776556971518328801971334802680284093928661305052344749275466532375832261411010009600475463751194251427781899298880401359138323784011411592044608283126853165468964178654303046386581795116109571581951647202242705968808887465854758990074665434220806574168050889931085579806331605226788957154526772080771795669545029446600880019405864911077053704723178833561165709753818521177210997943053811233302452860487556049997598558308180338056197512711182403206814859442055967146886726735716673742167967037926053977241731062321112499880022913582224849861820819991708015327719797195797944214414254878728466994390094334667483026082410210248421031702551714696197917100464478957370276156988475513437716805485486654617697803970156912043643049786374981943562070126779874763489585037450358359142472244443931220818766676635385056208652643470841875890251764319655854053512330097153787526597617293294050841638784816869040583813157538551202147060813487187233098895831861895717810446523908318383792520850911366960119369766088470255434198131947947513292383449346307256723462606721916946532368448265175978694980346473484780360160614841232442542566357993364072623836760887699573408162888372189039841802923855984319990645043704335212859103283678451741486668092399360804788914259636699983900221814729877858876461185582699957529814814608420529906309656747175088602421156938403193695390445892769796365772048485896001965486348357772236949328348835802475709741975377553401401884336643855706256786882599743571845972451512841561388282719935381938983498352853337465859794689191160339262785990249120789957937957799240946175385400854046165486657094104448967276665488763274244478144587275439272766639355254723432721983567600669935337088536005747061010164847512443526026037332504891808055819431069889271927990075575240655211806652157473293147719099732787228607373452526621188945651063001686388784469763367674830586481589812876259990572733144673152632507169950654638462875999329579750464848173839403675907871910381136444755303993060088717137164121908350410676114604991820465323819878999311846162759269350213959882358630547400388285405862861027156303437729469328107135101502973688354316510950736231400292389014090013722046796222905827353024304412955368870937870094956653501104331380339706016730687934503396925204132169654352959680470427597608584077910178623673387688948376432754787500421025234893905104364559222093513083260020347620416546268851159335710602501473983783925166374670512012615654188757716946012841573135404879463094857867573826896150841000329338057308671404571265952008897382726765688125891393982391430920099513945505327719571653278182814485225632390965646608371020035251452514466035932423863373796018809928041552686005499884551906974597112948973032337697127774142867737542064214390616278560710718811833691434180645385249600296755520866182894976688179489025156284575358872094952825938335789154882500945839102251073138531651805556298925089638087227422687022804438852511551872550295337625418310662047775432707748942840869710986641958213503695078262146575013044887282367861618926222602651638763915894087934726511975913822620760609203227972274839823416430890404705849928816411874297542161982058003419500681903572366812855746340001415985916809454495946743701815983668385107496647696473398513623416582061468870531612143929336960339309460326714005413794129077203398179604368244900936899188479743862781318091401284434684187594679300755277468148093985048250364130971574137175428536722264948733610212612052220142444945045611642387268035785634386070463617850976879446122743227076916574956745952036858837568903888937613576849921730174795088069938940685320377618170006780827077142646282916305850058081704698284145163299240567033577444140163668582388354412257908403239520609251835053098630365286025313079437700689495550591911878580966601333067985996596223108721795630685768058105800204008393348796444059664721038442268706790870769367423286912826006440773185984204857005754798822044848880446170438213352579444970959118306435239308449747915477631786085981943271183274460973360339751881168459558839673316030003305173368201865296008762272377170928013327648833933790705495452699436656273846443024065339528706571510538404269262326363640048857434106787737948064800449648242215172358567824671056115602855105750375538280156798112742936001866362861370632773003644327682305249481191658530404849358586794181230270339683055779175050001431860599616934261460686567878831613492575479739624580495554729835688864889270124662795344448929864261700267179446080830190116557510357989631154321474484076199979729931593046832674497418595433772065795923333029109401465793241586124550990543628731540718929585960382392184594269469126017498573965219946745246216803432907575003437411513434145694929187487386092579028808626647227323631756591676337149686357809297340874587055572662733665123185605058038229358206063004335499005428250177040081571481154309467799218687270953208494210080160012828368313092328626454681423954781967234650985411916052238722222796499776285587049994263795691635296925115776323124646534657845480345486267318142552865949483541599394418182312413368340470288783238690449352615577053739520561371949444942419563987163160468372297476815537842943445031617107833672028532673900611610593276692309356472374236510890516352214541782375714420818977740152274238802708428062982740179124684045765399145264220986618879291719655247632512186712442983505345907292512820462843694920749795362137727510732107725434343298502912852327074990689257843749938067588671257914615884380474986138309774143613255305807548729783584909498683175918213735009334590084860957267567730625756061292621707069888510789998878984116550355331747569078879337710548967714794764772836080822448120862016371283370275023949935900122132584333179405008130744123883138506010100085553795559222435983726039395672017633190299257545841283018124095715515242008527140833378491590732665252980896516093492179590692855944190852647026179518979215270310082568195486141247950519689217968163812857902591262026992762059738935669547081280432194928889662296088591630700588653454585973558520661214142074248241286752530505251839431980142957306207365798040255003511781877452354602627457551597642428020837132397640677015811647625638519812756352841516045965582204798190447851221585756931973842401232463521516128923950603741684960136199983376589113234851272388402340177151733654589264608372269192823481769997061086005599284192928370297474807835242278169956717884184120667018289507750980208303389063028281544070822711949822808638502792296540192747539603688408831565617269313880550089562406064063412455893857195660623036199316909018341818147065701243868335150706028035284612533267113918623103879226910901896849638191035781256882707175845178636484215605876355379373688020353118115272060754553628348970030744715900170799719189374684822860116484878741085180508161680167662761125647079360111958461647755120370857536314691224390227328340321199911378357525548429972489233316739310802013448739817738525493653237727650892308078321256033967632330510032276605931797491697183454500072860816423837950910361829890293726012643699813012017598121788418329042507294405285300900244897507974260919289701027639419225467055639914542634324729174654940079681398386132331892261859654570409342465748625819780390382316598207053762841996503072019656262047328681326090455007930986493425654483724578190358371695970306774882778019475605423501147845832245980553655804609883077956562015226837669214975128210005991254110746169458459425164444615703086602808076053174333384759152295429368005327823418070547181633150352141265308728265462203289785370567326516670948106028013172361596670061208345678032321802957768264573635985700014221391372831038391196244914921622092704474323387352775729530239568404136771872626931776081646519245801380434200540262222856850621747903425885042046703756427482542078857008188821692940899495223016435583211850472500872611459499123258360189166929611160613903823254279629684260916149673176745074929875141564143261138248289536812290968755033815850105016095593973100347494954918197724594783945774998102431523347420816946469010851201422278943256570756162912659055510483798847072868811340379733699877273966789941564815675693382011782659788468135575581264806125405225270125122317048009159777951782233718356258679353966929051693036987668116601598770480431515915259016989728673433405660416227432174465495651909589014983936990743457248382761225350400152734629442520459563664103196865085095174694908742459426305822445588876007816678294277818140678667818495516375752417979975843978208060650996148007760269702730970118336954366748914694810544866291540521774776462501209966783198170029604855617886504612829269489169312363184330982860913091443367727250470409622410207278901375669275882284784229279931759971775807754589664868943230466570676127911683994922622758655187779785988427757581084361913598611642759306300825786123563911896514304517466431597670152059237884819920873187508280834873514758732717223268784185696739338015922791161375079943211389491538142136584990504551391684419916752998544881242389587641078261992114334689365337035392092546186592901871937004444775062121853504758853064590401203061145808294164873224991764509664786152210023653418315022825421111861851417767531945053940322361441170927391844569009612865465539065598661385315757800887205804625908868479580479511170605915124206016740736797259988106892780191952087664186445228027679032693572361028086859186260720550323661073471963702314552283131685659831734687743620742633411201070411476865150848577218893600150578380327311337368193732024104053555208566208560108404142781180309511484947690328245457425629306472315795431022397721316220519218417592752714397680329101422362933680174756143333678050626066689382507365025547753063407086907532901986276673979971147923100414033761839007691822491965468926839149437190054017741403298080222736942497727255231815029852049774002479273431074854510974943600939006240715545648095567458173297994111712719240574306550564607396070358247924233863356238679157892452530242760976359849884303168351311909331271332477641714152225285148476930791348468281176332332044655192200977932469366046131604206685074070285966133162482145244353194791771663093810032794632652992505714297083576504381608534375643463985452039640549096158413472320669651007450556991629692750603583352481963143933614750030459128432945847188393141096630697366637936968147264607222555347023749204662472423426822302385383063106183432875091910359549351527695584615139886929209535480119954858158139296255929492863873336809061199950242601891501981953854204476749508297378490745245114154231052167492809702156679501097305708821117852142477258161549317465437645807195578991658803728128672042896729248708945454793155662058273674194723628444373493741484180629495330033174220326614765378346088578660794446437200776883170145490644971869745731584955805701526226310317456651254650685095064687944880615057052152900755539105830139933766014154857275475635540497489103321786247530145492583803672058733017414925672132755263694909632307076173754674522425147181857173263025957185132270022297519671560146748144089104591173629152734809302970303932528309187339934175415526144775701843905880957729083959887895999643041009916891559809503678334142650551279805376689448310379619388360553927670906486037439472611227746433347629421573998284133595113364283625279344155700240345242257866943951617089411195316142747447584342619096675248957921581721833249148644130499368027117542217821156544467031370236640521363758424613439612406471255594066077431935079342588649022807319377491551122101557744754759573730500872520740874217312766923707331110804216686369564435605020523935255946857240492220851850080645830262680237874922747672022298732310292002391858473706139934897166260990650569493436942678992429447811673373675301624751578248875796335950842627776163140257775638948980546857195771078102497414442886903453642676188052711608485756447868257873587156538804005032841405949763876843998337735819595960026868998149810231195256304904520310748886594889520457784287461950751561515982309901483957817882705114719718762816077462258430504345121322069469500479280564946133276358005274188745442011691071243484648242372271548562839716909867139270139108048377859990331131750601050164280242107717902578342493235630613801792555614037055609608800188579825527562555949619281383948871428963183663266327597233761427807843229012682131373903251946763189550103792543820251102186958719525902558770490892589118141474642180948095547150279159431670580611538038489935585992422256157863177429152481409494488092141026326739251287821912115343319785670231134542471405748013802183606099864934918050746191894014198228134733699433623497231617525575712852629390039608471681119534544537273581103443841533939149483517850497672978151751342795560611025580307824922824239676429911265182346670556110627178797032520771790772731700691604845250357308918480642942611418185703635084697899034968190122382350730791697243438347391544188880492645450371035824671412924573047944387325185482468070671239238730924489040141124029899674977614211024291704606518597628425719422421359488828981925995329896064155211654657458117671996448426809496548640170399192860350775869693352958583152161558346521985244770807243518616895268851708906369720653290639875263849047891910396271813764663172935884309452317684119790991844127135294720576474999889087355599816931107607541963378521928349563516077106724076334982779954808079962677738678825381154174273124280261664179493019976993806681292613453001292283443173496553975049418296333486344828982780980510317918769188976733077115223578422423173504661290124627202826581267574155496012882610403687519109247669039325540465908417551280256142355945701360640291440034284411982980101581962933803464369987416388695358436594477900721757775090912203923824477095768621934594754774541726386880301650072107970163061254881847966123179721868610842338682056146428594385718220416902455048633178996086054905307944203720267955693584383082525380988280125162574498700295300943537382128078162272601158065183491000713935368164577492804065165186720016562259986998164684896012927997626885792991014998972769762254476037640772994145550438902908755603236186522745759177190940497885432961642828493068517103208580537281718041788006755959721864775329142855905357133015912223093997417219165192373027135315211977910361223384216264499057855726844668719965421284815728434289345673782716415563324699940109842582340263757638228446579687922283288872919231893605112963500562693605108096625531773819955543202960821013242425612040416508019607691202343713253270996436832738237136924623203539625185159922692198449562223009357292213649596459058669956941062133532737140507572356728732348670500014020965370546113502509612315698108939624306555719124119185041156968143613332728688930077775100561564726493348266006544230719/5107799346796145543492528372660801797184046545811008089267512277497058920472322799888404426049606225997724873773378753451669754775786931107666960798811646285422842970330680163703688904496094739585759048124042364717024704519042178142018394619927820770886524008654289240950741463423461162704542327363337306351688944635973841344554360692349541246057972799978550624647851729582510977995049368811273731167999786458684291118597614822950999551994078971741073756408157368385486300315616775452171412553165125533612017407886911692399475554426720843365659781427202922530279959329751820175967051016039774864953777580553748604563440697830296294421336745759638228921875147173949762098647827585730202887570036414786116997389578258642968041109783498832987287726179346381210755796733274336065973303835887007521198382263712744924092028757757290998497299528260349539383456173319343059444905624498087725079051963632179955642821875401594053894322615422609061872573155339477509308456804703297263990114687145447306484586976400812026477503852108965721181126430645871702296523664169614907658729818347667120113286555399065874426182747927482607474327244219071610327222906251759967762955555920531088297102361644297570327032788229429755989102179243474639425800842774235076864478437081003621739785464464296828561463078278468530013235123018479723864612960247009955197537001956202350526078415270830861004928835684961097304363799665391829596627585881101379698079553146790451763842822868329211906294564258367687807441870815174766510502194094881114861374926718730075813586541706417324451556726707239858240263575403233004511337391452463042300164924352576474993473880468824980631393892250123710050069256475936872195607806974273686730003300524947218001695147305132973061491542110271518538014863458377188184253482189790173516350272496349819585458523871412368671717014323528881378670646185146703519691499083401775771503639517231983991881184124626858352396567170561888853874289292953609342187047610521514523957304326062337874743112206467367277715634547330453975374761602580598990983955042762618966125119287715132901190952318875811547778699485978043049223450563479648440927514563080851295342800027881242957380860167533342232810249739836547984019472021072564053707021297356668231214435731534327942455472004880369670930773845072035873949890379835957849461082590858418331463908499213968396197836212967203922516215444409990357625378555685958043795567118624466325111679696233518184009303926589615732602347003754512435097790828790034518934811870172030390256178912617861390118050327003703850160959289615623463723273965644142391039120608040761788914435920706935974939744826621924899983593652243210645801092321812952557627374983187697161494264070125414159344328458955255472306894473926835908785293530141692772815965687427334059962721438279227179384304879472229040083215997670306997286674646630164422575373099619713520531903174570861712490798558764725499796212726785399206267386379876148539523667969157368979339437283206063092923508563080555719385351228840866991933366932085101163635641769020816368686994992336818523341308079756709930835740430192818528742256800511265686196264015735830353126350250838353509007358881188565597773247545090514122750432621054301810202635925276299458926294724254221107896631303084141703267427590894322768715192728290094309576487243096667668147421280770216308344498343918455748370054906391774168666915604835934505037703211070908637200653471597557862579109390922682531634845814031921559133901008700983064591567933009369873887297348854733186466037803170019441084031746513246871240516618060103619319791777666236230020952296837584327599174620550863387827098387634847476182967584163047762904411858746403803528217020264824378608309946023624321578078276891836540446857410487336606708245988316046692431481553315842329749933619272567422721728178320892539167199468469007008182361674371579404819033841195418571519925408590540547302992149489167824489127160556093874207766099803770400868257518246720950003567505607208401581975498916364923975532378225569954178380025715280303080361576888692255533623893838042020975612965076062400778003766169561044807895164443766198032541601495613022494517193378574487425468836315118897579527085629374611680644620633197594398527398008958347011723112546017550280265871484497360928540171190224086678077786680908440456750385698922843029489583229450232424909175053102063335891111995946898542777732819347705380385686824292375736823450254684805482186639448452317817549630068830531095661538926079728989947845719351576395288965523345503534511888332700024001070896423865005400791792389761664880263799442076401704419504877964671646337899372241937689921700956185820633388980404611355180091420468408451756657188759948674540826306589719890393725440647238014124696947589317476328516891233283349078262075198671380145638456629570444353168421535389574739346210891383812144270046079397532501698934122084851282820209376309009987505085903851736637577300315645317909240511201630778100481541203618692343745030569019112495921350361184967957761581645354163404539435907384548391604776175344215298172033764692424053506196438246781519956673097097423828663466835880671930677513194684365762779880701675625740742030768481791110227672238197039666115379432393423183783766489765482642550193569115285593514981372250097556871923932085897641880530853109148329070026508191977653251081425326352259556685783701487830386338330025735968854921183655937591633577232609686293669474379903850785697200062270304869609778174775605775320328576618692034277981650783197802387960132949580501310047502747522146222734389801118613364994932280707364506802801412376698777143703476251511133521630018105506896055085790601300417605382129625092121009982873918361659182764243461615410578035670683650773162197507158473584072149303165334250974636625752097431372855834323064064271071028870316960119885597178238731415705823515932193676471073885915267799468515550753111417467549891820627082960244087522529368926716235380692519047244534351536200114573266639832319368013023155059391564293395266456623076527600466047589051307402202595899917058432762363819278219494661526690554227805196684519006426450400080326820849329715690481076918771033070725776270907896122187725822325354817747478939502810951711658101147070549349766286912382621257263322397001093056911124458810832180624926490068730755272914554275897110023223009687900975865038652547464137110297758594041844266159719469477415085429686548518513039135474007344709946671421465118948847194732082009656030098789543311661500650465831813965323561296466997567996150588395269644275168665588341125407983535224164253040074667076788020719240699879636586172458125483118968022752947820897693309149489335511523929956607322828066507715745652724478217104596430085271865991919019262355522799934357452770681810414906048475276679559725600194349993427195424910173335024096613080617767490923925452629203999132337898328964424358530374874315987449992336941211961656446211464469769219529433814169197404945472665766902397955592526711669453680843308224691253984854645912445751602142944545127426198977980157953179640998233472379443779587194989505481756483958045729692779905814056262283604210147272081273629492899930567648996408546274441069904685830681075828962584674952386326026954834637951142977677240190754106008383673909208836492560449098880530950532711899472918983998274041649677646662835891546728148741424410775681550693261887511512389227142314920006395439835348198331578491437609063446854221835236055446520117445981335374756799233428066985044945930471465957730414635893454061979894564052549785294599313374163540128661400927433223079948839694921543774114254463165274328336291516818631473089834680566512443550333223095848613643310103803659653418258154848608991918735623503704571406968756518199189256973890842241300133417981008118214136942384779123522755305226277879117062828195810298578760533972069076238475066603459382012386389277201725946070923220234436634624115457145033332325930096202190414320740785255525326376534636689322662826319622303586010550862970187997581054827700428313567969430283023976155489467990033430190056396360261533534944182495440621302880418154867805669927165359750166675797555985477355355936478091184256633015781461309012185558798592027779430311063324342258100838570655491053808942479361539116327700119408175316408290144932741951654903969486533581562654956548192874900958932842001161090907514429025562814504636743123333665946766285981334070257545138556885128621316735338156104138427701956545876491707055407055291059717888132663504701881913532626810467167872399884930756223016854026299471378457903103104756014173588039322130813134775445534248848115359349855706121806910450130376294633558174912309991359079302378025947308644346604970688038359979910420998104280301661521602843026235895436369285130927749453550204515268457525303298621376221544057454110156514020116146740914938618920384294115671010995113954461899968747494320876798476154191342960233600741738221875152880768974148829471032029881825790294563047002756004895948870421953505793753329946250317148701190953327776593063952884288838313304885799020526737395861446266106378128865208225492018357879847617739828645290403879024580607289400000988565010827843117313420192670387147159473133860511227501241446788109651470309371156531607391620132998468658801004338117534479602835536474905214101495209370363763083630578100819757289330092181821659285659109718692986214949759330968197854420127505716779752006392547446497810294998257979455819755319875497302715748263033368223245050813188335573385569675779655656409090258519577423359716749064450875628752784407413367918401384580623438558273672377776454344524461777835933755567361075023092979365921189402224469821132530498691231213634723191482098672700311509467050199160909762659653594994744445952700504545762264879770992376604805333716551769762776528748048992725585692695152790184225793878049416683119457066313493325167904015870042775511734324084625738899669487126846085400405371337774931881171055747773202542473840585455347448426872801449733583309261913912965537755297901637554797526499921791774893651661053323320193521242233537355646590465041625229828942809810757223712406647336526128635398116266540128069043908993942649339939301561620405758381555539222745680304951243141540536548927657147147048853638969256184154332167794288941572861367964506853026802386358512670467288453811101505983915881419309211722280552072115353342052671095553295315924832833636116610871339762906231291264347682341171014650773135255720771266290895914531641694443447764933112609362246517160682757444917752101715886010299079084314106586633774722436300972863097431217818603509055220894733403023147513265306770247565060458244122421248973760399853342713494617580386837668956981466079022479765802876956261065403014502224367551579469427905726754453220574862604327229704195678021147094881543665762684074023952485585512966560788753151769481205310824040441735543639409390741662134965859660838075757511509584292999965443137614815695814215328916168621303604325981490881683575078821866824527725776540882708360047014651674290109735765051605370181246390610129995912857770272885746935096844056043217707231106582815005803526539891465335639316436527727597514232035256094085340274660690963552473027735483039372198275938512186192205757789867322035134997850398976068624459172481649070169853976388312394184483026494740829251200687961014133971356452892323116205098647413622054283736755369272662641875470279944849993010144597662893019278883597414292120197786383477074469141590661034308407444222581237358548913750611664461216958418709541102534680368865421787597261226900498985999357024894148894194354005587121711875334243427777334478150169192933332778411852973264115868509962883886704962320991463398806751079821938397718082359048042757344677326038700997655550131380158752227439394572988858296687653287585717065014315596682848716507556792649536483182664057569307171126723587255421585838945133123483532301482963725430905799380543798775255628851187091627285245060694012220317343730637092561207904954341781584781689420933218139364197919364024818143956677876214613805152747031844128452496344317619951636121181305910770065286907893225540430097662361704873807948586727669810543532468385478460272981959097875016006547829815594590409261177339461962582843802390186736890432502824101662356351477797236763102291477175618651125814178679275902792433940660812770416408519546130448653795160185670835459562141258935815901574704882917450838111074965311612365312064470757089338775079716953528700318149110299498792124698103994613397630603176652412862005966424940136532080847029864183636388715853834510524399079461970719329342632343111944676958006107367896099691249892274504439997189675680738216104964133569045875800969655360823283064627190387509719101327687374910991195668887745127392940822412511388364961339411992748918572063228242797067513966935916100517542109957878982551849520232509819318342601022913594461260259047143218582351204290533327176636295014859409786261437256390124570249986319223844805697310464897752586082101144003003500710284867642069411905876689309029074843349458906667877739409789588777790792953563463226705779395064897446904344102702738814919104200021099746839066567822726766361386445885522528902810940480668778607334815161928973437976414865494318427619389735408822662642921396572101272823846659527862397061926024056428485534353878128284712674502943371795186256762605702292151374974006374315778706350533981344828413889019940934381289292782817612191632493907397144709390497155643128638565111301590942170866370893329181242999541125269449322020768133674853313988646017073090393004135508490373187003321939463286803414961044802868828967001048142228482706721680430107852400903237734359460398460297790706922921257959599803475806972914343537064513431388431177731241619327881974887308037546161044289404097440882993717773808319113856242778618715882641692928278752456151477273506241086146605594077185539155222592403866849261952826395013125930410242032857126629569945112788591488593158536407654084964926295525804399042785897090785112681878168518333910550698434875802741758239216862366536184791480562043013807427645040490816212075670656877638357897156307620721510414629520338194425269336980887495117617986236179870191022980598488790512106612971506910686112779045410092761060178204551011011324254143382946100449332374035358096870709103600775185274499642769059272280008320488469506249326966245580157405674966485787184325529203889400250139082966178603348710012928745057898926839954479074960867346015069972678309884656325310704215597744527272081856243613133688195393920924461465048951853138164045149887961082525321073193718556714742194750507398228425920876187446922610024037161388320985836756708633101101033178718744454897400911040582158290574741479198710494928414494719205798881003347567655370397416639204135343311726481745239511385138846147480633551995118419773582934142302745298870906288939553520268733566626843936916364297907921882300040287839978791611035307301639845968952803906164027819239443135317219492264376170096030786074757525839275807051144978658599620722111424720840148582036323678736776223020725759422744896033366383183529730524750955101896633665263018098051940693300555114160106389918791549090099617498108715765462435247689974986372719805325756145976825244208281951538680961941505883144320636080118499331251470766288886911543323879875190300313211043093637064616735346664437638263757196303687693819796423719262900411507220896989368411220250940740098049711482535853233409667543150554352134177205968863287450842491449136993910226860796533301123293855272176914530154528210462097333572998396754422361330874163263505367550192547342747596251607000390079915043232871572909488352224756318538988231372661452778310543766367328371965051700087700421317993331495075148147893065996051453757573005596887965604989358529950846649750900866453183065034586277032353276809315118617717285644536517032416007972801988313775794665871721657852483986977718555662482944000000000000000000 (approx. 0.006227002518)
Time for model checking: 115.687s.
Performance statistics:
* peak memory usage: 822MB
* CPU time: 237.049s
* wallclock time: 238.546s