mslf_g mslf_g_r sat_g sat_g_r mslf_sat_g mslf_sat_g_r
Avg. runtime compare 7.73461 sec (#2230) 7.80199 sec (#2230) 2.15843 sec (#2230) 2.023 sec (#2230) 2.21536 sec (#2230) 2.04052 sec (#2230)
Avg. Choice Points compare 6851.25 CP (#2230) 6897.5 CP (#2230) 1614.5 CP (#2230) 1447.98 CP (#2230) 1747.39 CP (#2230) 1576.47 CP (#2230)
Avg. Fails compare 6804.24 Fails (#2230) 6793.02 Fails (#2230) 1567.49 Fails (#2230) 1363.12 Fails (#2230) 1684.51 Fails (#2230) 1475.73 Fails (#2230)
Avg. Clauses Begin compare 7668.95 Cl (#2230) 7668.95 Cl (#2230) 7668.95 Cl (#2230) 7668.95 Cl (#2230) 7668.95 Cl (#2230) 7668.95 Cl (#2230)
Avg. Clauses End compare 22145.6 Cl (#2230) 22232.4 Cl (#2230) 15186.2 Cl (#2230) 15519.3 Cl (#2230) 16107.1 Cl (#2230) 16555.7 Cl (#2230)
Avg. Nogoods compare 4212.7 Ng (#2230) 4211.52 Ng (#2230) 711.604 Ng (#2230) 613.494 Ng (#2230) 742.449 Ng (#2230) 631.276 Ng (#2230)
Avg. Restarts compare 0 Rs (#2230) 1.52915 Rs (#2230) 0 Rs (#2230) 0.9 Rs (#2230) 0 Rs (#2230) 0.890135 Rs (#2230)
Avg. runtime solved 8.29086 sec (#2237) 8.37174 sec (#2237) 5.01373 sec (#2276) 4.47357 sec (#2276) 5.07609 sec (#2277) 4.97931 sec (#2278)
Avg. Choice Points solved 7332.86 CP (#2237) 7347.09 CP (#2237) 3796.24 CP (#2276) 3350.74 CP (#2276) 4013.34 CP (#2277) 3699.68 CP (#2278)
Avg. Fails solved 7285.82 Fails (#2237) 7241.85 Fails (#2237) 3748.39 Fails (#2276) 3258.9 Fails (#2276) 3948.89 Fails (#2277) 3590.57 Fails (#2278)
Avg. Clauses Begin solved 7706.04 Cl (#2237) 7705.76 Cl (#2237) 8077.6 Cl (#2276) 8069.37 Cl (#2276) 8086.6 Cl (#2277) 8097.04 Cl (#2278)
Avg. Clauses End solved 22840 Cl (#2237) 22961.4 Cl (#2237) 18739.3 Cl (#2276) 19046.7 Cl (#2276) 19760.6 Cl (#2277) 20488.8 Cl (#2278)
Avg. Nogoods solved 4576.94 Ng (#2237) 4543.02 Ng (#2237) 2140.83 Ng (#2276) 1856.63 Ng (#2276) 2230.31 Ng (#2277) 2021.32 Ng (#2278)
Avg. Restarts solved 0 Rs (#2237) 1.55431 Rs (#2237) 0 Rs (#2276) 1.06371 Rs (#2276) 0 Rs (#2277) 1.06541 Rs (#2278)
Avg. runtime all 35.9591 sec (#2340) 36.0402 sec (#2340) 22.9057 sec (#2340) 22.3777 sec (#2340) 22.7105 sec (#2340) 22.364 sec (#2340)
Avg. Choice Points all 7010.09 CP (#2340) 7023.69 CP (#2340) 3692.41 CP (#2340) 3259.09 CP (#2340) 3905.29 CP (#2340) 3601.66 CP (#2340)
Infeasibility 351/351/2340 351/351/2340 351/351/2340 351/351/2340 351/351/2340 351/351/2340
Feasibility 1989/1989/2340 1989/1989/2340 1989/1989/2340 1989/1989/2340 1989/1989/2340 1989/1989/2340
Avg. LB distance all 3.96785 (No UB: #0) 3.96352 (No UB: #0) 3.76928 (No UB: #0) 3.73334 (No UB: #0) 3.84003 (No UB: #0) 3.73049 (No UB: #0)
Avg. LB distance shown 3.96785 (No UB: #0) 3.96352 (No UB: #0) 3.76928 (No UB: #0) 3.73334 (No UB: #0) 3.84003 (No UB: #0) 3.73049 (No UB: #0)
Avg. UB distance all -0.340013 (No UB: #0) -0.343166 (No UB: #0) -0.495157 (No UB: #0) -0.52308 (No UB: #0) -0.444492 (No UB: #0) -0.525536 (No UB: #0)
Avg. UB distance shown -0.340013 (No UB: #0) -0.343166 (No UB: #0) -0.495157 (No UB: #0) -0.52308 (No UB: #0) -0.444492 (No UB: #0) -0.525536 (No UB: #0)
Avg. Fails all 23781.6 Fails (#2340) 23787.9 Fails (#2340) 13211.3 Fails (#2340) 12212.9 Fails (#2340) 12933.1 Fails (#2340) 12341.6 Fails (#2340)
Avg. Clauses Begin all 9227.13 Cl (#2340) 9227.13 Cl (#2340) 9227.13 Cl (#2340) 9227.13 Cl (#2340) 9227.13 Cl (#2340) 9227.13 Cl (#2340)
Avg. Clauses End all 33336.6 Cl (#2340) 33467.3 Cl (#2340) 25929.3 Cl (#2340) 31798.6 Cl (#2340) 27640.1 Cl (#2340) 33256.7 Cl (#2340)
Avg. Nogoods all 16195.4 Ng (#2340) 16206.3 Ng (#2340) 8105.3 Ng (#2340) 7476.75 Ng (#2340) 7899.57 Ng (#2340) 7509.38 Ng (#2340)
Avg. Restarts all 0 Rs (#2340) 1.95171 Rs (#2340) 0 Rs (#2340) 1.33547 Rs (#2340) 0 Rs (#2340) 1.32607 Rs (#2340)
Problem Previously best mslf\_g mslf\_g\_r sat\_g sat\_g\_r mslf\_sat\_g mslf\_sat\_g\_r
LB UB LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts LBUBRun timeChoice Points FailsCl BeginCl EndNogoodsRestarts
psp_c_1 335336 3363360.62s1633 1564248013769414403363360.64s1717 1532248013789814233363360.67s1810 1741248013755410103363360.67s1687 1280248014062715843363360.61s1683 1575248013744213003363360.62s1424 109324801398652023
psp_c_2 576576 5765760.63s1603 1510277834374215205765760.66s1662 140527783437981413 5765760.18s160 672778330568705765760.18s161 66277833056881 5765760.25s454 2812778332333905765760.25s454 281277833233390
psp_c_3 372379 3793790.99s2366 23141750435687104703793791.06s2558 23541750436139106043793790.38s1267 121517504222452403793790.24s452 32717504216002423793790.45s1109 1022175042881518203793790.46s1146 89317504291331703
psp_c_4 244258 2582582.10s6710 66511359230685279902582582.14s6847 66381359230800280852582580.70s1650 1591135922577353002582580.78s1930 1668135922732649642582580.83s2325 2245135922747658202582580.80s2207 187013592274904544
psp_c_5 403403 4034031.20s3937 3847267124970720604034031.21s4128 374726712500452064 4034030.23s160 7026712289411704034030.22s160 672671228941171 4034030.28s457 30126712311881604034030.27s457 3012671231188160
psp_c_6 316336 3273275.62s13647 136011976651794705103273275.79s13741 135041976652778695963273270.53s1047 1001197663027322103273270.44s714 502197662952913533273270.71s1557 1461197663766642303273270.49s1045 75819766314331713
psp_c_7 426426 4264261.21s3392 3303236424712056704264261.24s3542 318523642475855614 4264260.68s2599 251023642316094404264260.75s2195 151923642368291754 4264261.22s3720 3566236424687332004264261.28s3823 336823642490982525
psp_c_8 493493 4934930.45s1315 124120963276379104934930.47s1368 12122096327699863 4934930.16s141 672096322529204934930.16s142 68209632251621 4934930.22s471 35420963252642904934930.23s471 3142096325264291
psp_c_9 253253 2532532.80s7293 72191636935391332402532532.83s7394 7136163693532732615 2532530.92s2224 2150163692924793602532530.56s1063 86916369288343133 2532535.73s11250 111161636956007709902532530.82s1756 144716369322185874
psp_c_10 374374 3743741.47s4794 4702287495652819303743741.48s4999 460428749572341905 3743740.76s1999 1907287494211216403743740.82s2070 168628749426372404 3743740.70s1782 1603287494035519003743740.59s1416 10272874940118943
psp_c_11 272272 2722720.17s208 15068237236002722720.18s208 1236823723601 2722720.15s86 2868237055002722720.14s86 286823705500 2722720.17s208 15068237236002722720.18s208 1506823723600
psp_c_12 320331 3313310.26s688 6025762882216003313310.26s774 5845762888316523313310.30s650 5645762954321103313310.26s527 4175762935114223313310.24s562 4215762927411403313310.26s664 500576293911802
psp_c_13 389389 3893890.13s130 5795749600003893890.13s130 579574960000 3893890.12s105 3295749638003893890.13s105 329574963800 3893890.13s130 5795749600003893890.13s130 579574960000
psp_c_14 379379 3793790.24s589 52016666196454903793790.26s634 5061666619741512 3793790.16s98 291666616963003793790.14s98 29166661696300 3793790.21s398 31216666189912703793790.22s398 3121666618991270
psp_c_15 510510 5105100.15s318 2271118511726005105100.14s325 162111851174001 5105100.11s112 211118511354005105100.10s112 21111851135400 5105100.14s318 2271118511726005105100.14s318 227111851172600
psp_c_16 412412 4124120.14s206 1301032510673004124120.13s206 124103251067301 4124120.13s108 321032510530004124120.13s108 32103251053000 4124120.14s206 1301032510673004124120.13s206 130103251067300
psp_c_17 320320 3203200.19s442 35475308549703203200.19s448 3507530855671 3203200.13s114 2675307744003203200.13s114 267530774400 3203200.19s442 28275308737703203200.18s442 2827530873770
psp_c_18 310310 3103100.18s334 25281038779003103100.18s367 2258103882911 3103100.13s121 3981038426103103100.14s121 398103842610 3103100.18s334 24581038779003103100.18s334 2458103877900
psp_c_19 440440 4404400.14s268 1811165611975004404400.14s268 123116561197501 4404400.11s119 321165611847004404400.12s119 32116561184700 4404400.14s268 1811165611975004404400.14s268 181116561197500
psp_c_20 380380 3803800.24s597 5061482015857003803800.26s674 463148201595102 3803800.14s128 371482015040003803800.16s128 37148201504000 3803800.22s461 2821482015888003803800.21s461 282148201588800
psp_c_21 393393 3933930.14s213 13185969027003933930.13s213 1228596902701 3933930.13s103 2185968838003933930.13s103 218596883800 3933930.14s213 13185969027003933930.14s213 1318596902700
psp_c_22 398398 3983980.14s205 11561176261003983980.13s205 1156117626100 3983980.12s111 2161176297003983980.13s111 216117629700 3983980.13s205 11561176261003983980.14s205 1156117626100
psp_c_23 239239 2392390.13s120 4241884241002392390.15s120 424188424100 2392390.12s103 2541884253002392390.13s103 254188425300 2392390.13s120 4241884241002392390.15s120 424188424100
psp_c_24 321321 3213210.15s141 5578837924003213210.14s141 557883792400 3213210.13s107 2178837953003213210.15s107 217883795300 3213210.15s141 5578837924003213210.13s141 557883792400
psp_c_25 225225 2252250.13s73 3556375693002252250.13s73 355637569300 2252250.13s65 2756375694002252250.13s65 275637569400 2252250.13s73 3556375693002252250.13s73 355637569300
psp_c_26 255255 2552550.15s118 5045684609002552550.14s118 504568460900 2552550.15s91 2345684678002552550.14s91 234568467800 2552550.15s118 5045684609002552550.15s118 504568460900
psp_c_27 231231 2312310.18s271 20050625671002312310.19s273 1755062570401 2312310.15s99 2850625340002312310.15s99 285062534000 2312310.19s271 20050625671002312310.19s271 2005062567100
psp_c_28 297297 2972970.12s84 3561006100002972970.11s84 356100610000 2972970.12s72 2361006112002972970.12s72 236100611200 2972970.13s84 3561006100002972970.12s84 356100610000
psp_c_29 373373 3733730.14s126 481214712203003733730.14s126 48121471220300 3733730.13s102 241214712212003733730.13s102 24121471221200 3733730.14s126 481214712203003733730.14s126 48121471220300
psp_c_30 346346 3463460.13s137 5589388959003463460.14s137 558938895900 3463460.13s109 2789388994003463460.14s109 278938899400 3463460.13s137 5589388959003463460.13s137 558938895900
psp_c_31 413413 4134131.99s3609 3518223534506851604134132.03s3771 344422353457695224 4134130.26s167 7622353251602304134130.26s167 682235325171211 4134130.36s465 34522353275793104134130.36s465 3142235327579301
psp_c_32 293370 367367371.78s365417 365358278442076372604930367367330.98s334029 33361827844204697236743113673676.12s8929 88702784495332549803673678.72s11924 1159627844108590742873673677.74s11003 1090327844977536539036736712.15s16381 1593127844119013100307
psp_c_33 345383 383383149.23s196878 196814252771371191260970383383141.89s186272 18581725277137406119411103833832.43s3335 32712527774083182703833834.10s5486 52412527781161325563833832.59s3561 34562527774694165103833833.58s4933 4706252778268327336
psp_c_34 334421 -409Time Out474198362383292593196410-407Time Out481874362383220483249381139139184.93s82430 8233936238214319518290391391107.10s84851 84434362382363625293710391391127.04s101117 1009563623822488262796039139160.40s57466 5689636238204101357039
psp_c_35 204259 -260Time Out453314223711445952970290-260Time Out 4463612237114326529534411 254254221.81s186110 186059223712377581259770-254Time Out2998602237122686719800212254254426.87s257147 257047223713183391736920-254Time Out3296162237127254021871712
psp_c_36 418418 4184184.14s6215 61272612670101206604184184.24s6428 6113261267062421165 4184182.05s3188 3100261264989718704184182.02s2919 247026126546633475 4184181.13s1568 1423261264108212104184180.93s1274 88726126407641753
psp_c_37 249325 -327Time Out410895270602529762906960-327Time Out 4094232706024511029038911 -315Time Out325577270603629282226360312312240.29s187544 1871682706031471512878811312312129.92s120093 11999227060269048843670312312145.40s128385 128051270602883408915710
psp_c_38 235306 -291Time Out516128277762368953471200-291Time Out515749277762368133471571229129140.96s54032 539672777614061434938029129167.05s84615 8416227776152085552491029129165.05s89087 889582777620193557310029129148.52s64104 6359327776142306415049
psp_c_39 398428 4214216.25s9462 93782781286338419704214216.41s9870 953927812865984269642142111.90s17818 1773427812955061019404214215.10s6961 6616278121018483702642142112.38s17958 1780927812921241106604214217.21s8945 8603278129208650206
psp_c_40 366395 38638657.38s129787 1297032120610867484390038638657.24s127433 127048212061077998278793863861.45s2385 2301212063973376703863861.57s2542 2372212064136384953863861.78s3085 2931212064339596303863862.29s4569 4210212064688016245
psp_c_41 280280 2802800.30s545 46778119482002802800.31s591 4487811958002 2802800.18s124 4678118166102802800.17s124 467811816610 2802800.25s371 28778119049102802800.25s371 2877811904910
psp_c_42 325325 3253250.24s496 41572288720003253250.23s501 3717228870602 3253250.14s107 2672287465003253250.13s107 267228746500 3253250.19s364 27272288455003253250.20s364 2727228845500
psp_c_43 321321 3213210.38s618 5391142413426003213210.39s639 456114241347702 3213210.19s137 581142411770203213210.18s137 58114241177020 3213210.32s454 3021142413098203213210.33s454 302114241309820
psp_c_44 322322 3223220.28s487 40357296955003223220.29s519 3705729702102 3223220.16s129 4557296028203223220.16s129 455729602820 3223220.26s435 29057297125203223220.25s435 2905729712520
psp_c_45 245245 2452450.26s357 297815196781002452450.27s362 2708151966691 2452450.16s89 2981518351002452450.18s89 298151835100 2452450.26s357 244815196781002452450.27s357 24481519678100
psp_c_46 377377 3773770.21s302 21094039918103773770.21s302 1219403991811 3773770.15s136 4494039834203773770.16s136 449403983420 3773770.22s302 21094039918103773770.21s302 2109403991810
psp_c_47 416416 4164160.34s722 6351278614913404164160.35s761 569127861496052 4164160.14s131 441278613048104164160.15s131 44127861304810 4164160.26s450 2911278614057104164160.26s450 291127861405710
psp_c_48 318318 3183180.20s216 1581012310521003183180.20s216 123101231052101 3183180.17s104 461012310315103183180.17s104 46101231031510 3183180.20s216 1581012310521003183180.20s216 158101231052100
psp_c_49 366366 3663660.26s465 3861210513345003663660.26s470 324121051334001 3663660.15s103 241210512296003663660.14s103 24121051229600 3663660.24s400 2711210513327003663660.25s400 271121051332700
psp_c_50 360360 3603600.14s126 7289959228303603600.15s126 728995922830 3603600.14s66 1289959189003603600.12s66 128995918900 3603600.14s126 7289959228303603600.15s126 728995922830
psp_c_51 302302 3023020.18s177 11159036146003023020.18s177 1115903614600 3023020.15s85 1959036073003023020.15s85 195903607300 3023020.18s177 11159036146003023020.17s177 1115903614600
psp_c_52 381381 3813810.17s222 12647264882003813810.18s222 1244726488201 3813810.14s117 2147264893003813810.15s117 214726489300 3813810.17s222 12647264882003813810.17s222 1264726488200
psp_c_53 204204 2042040.24s310 25140524790402042040.26s341 2444052487541 2042040.16s86 2740524303002042040.16s86 274052430300 2042040.26s310 24340524790402042040.25s310 2434052479040
psp_c_54 361361 3613610.21s308 22489119333003613610.22s326 2088911935201 3613610.15s112 2889119100003613610.15s112 288911910000 3613610.21s308 22489119333003613610.21s308 2248911933300
psp_c_55 706706 7067060.16s212 1221406314453007067060.16s212 122140631445300 7067060.12s106 161406314193007067060.12s106 16140631419300 7067060.16s212 1221406314453007067060.16s212 122140631445300
psp_c_56 510510 5105100.13s134 4574267458005105100.13s134 457426745800 5105100.13s105 1674267468005105100.13s105 167426746800 5105100.13s134 4574267458005105100.13s134 457426745800
psp_c_57 259259 2592590.16s107 4880028095002592590.17s107 488002809500 2592590.16s84 2580028099002592590.16s84 258002809900 2592590.16s107 4880028095002592590.16s107 488002809500
psp_c_58 469469 4694690.14s139 471312113128004694690.14s139 47131211312800 4694690.15s110 181312113178004694690.13s110 18131211317800 4694690.16s139 471312113128004694690.14s139 47131211312800
psp_c_59 271271 2712710.15s130 5952315252002712710.15s130 595231525200 2712710.15s102 3152315285002712710.15s102 315231528500 2712710.15s130 5952315252002712710.15s130 595231525200
psp_c_60 432432 4324320.16s161 821553815917004324320.16s161 82155381591700 4324320.14s96 171553815747004324320.14s96 17155381574700 4324320.18s161 821553815917004324320.18s161 82155381591700
psp_c_61 304407 -400Time Out503899267801777713497870-400Time Out5119442678017936635548812-400Time Out409920267802487702739190-405Time Out4340222678043526928770912-395Time Out391445267802377452594100-393Time Out4531392678046724829785712
psp_c_62 519621 60260263.16s37371 373124417532810326734060260262.01s37923 375544417532763126872860260210.72s6735 6676441751977603936060260220.18s10076 9714441752357065987760260213.69s8876 8774441752234255120060260221.18s11021 106534417525024764557
psp_c_63 302380 -393Time Out482614286741910953658180-393Time Out 4861632867419522236660611 -367Time Out383975286743742242507590-372Time Out3799052867438096325067012-382Time Out374650286743770912461770-366Time Out4101572867434042727007112
psp_c_64 669688 6886881.64s2305 2222225343358875906886881.71s2562 2233225343368078646886880.39s435 35222534281599206886880.42s467 255225342959411026886880.61s770 617225343087718106886880.66s802 57522534314741822
psp_c_65 285376 -364Time Out508307273062004943598920-364Time Out5112222730619717936336911355355102.25s88992 889242730617731457431035535594.88s86889 8640827306152855565231035535560.37s58768 586662730615909937031035535571.50s66448 6595327306148916429039
psp_c_66 315385 -382Time Out489969216061072003522760-382Time Out4981792160610725435876611-368Time Out536930216062624283514530-369Time Out5125602160626261033913512-372Time Out443275216062162072939410-372Time Out5259202160627363134812012
psp_c_67 291367 -365Time Out459194298631821893248060-365Time Out4391742986317620731050011-352Time Out388292298633087632539950-356Time Out3637422986336052423758612-350Time Out368510298633478642405870-353Time Out3745632986343893224528112
psp_c_68 unsat unsat0.89s898 8000000unsat0.89s898 8000000 unsat0.89s898 8000000unsat0.88s898 8000000 unsat0.91s898 8000000unsat0.87s898 8000000
psp_c_69 308388 -403Time Out471503276001702423358230-403Time Out 4724642760016910333704111 -386Time Out384830276002265842539420-382Time Out3729572760031215924848212-382Time Out366500276002181772439600-380Time Out3403432760032857922310612
psp_c_70 353391 -383Time Out393766259881734502887660-383Time Out3890292598817305228491211-389Time Out410544259882144912717150-385Time Out3292972598825338221360512-379Time Out322305259882538272076500-380Time Out3299042598828005821575412
psp_c_71 292292 2922920.39s440 37334614851202922920.40s448 3363461489601 2922920.18s92 2534613857102922920.17s92 253461385710 2922920.47s525 452346153222202922920.44s476 38534615385211
psp_c_72 195195 1951950.70s729 6635846878915001951950.67s757 644584688661432 1951950.28s156 90584668061001951950.27s156 8558466806101 1951950.78s805 7135846935520701951950.67s741 550584691081352
psp_c_73 630630 6306300.15s114 271336913388006306300.14s114 27133691338800 6306300.13s101 141336913387006306300.15s101 14133691338700 6306300.13s114 271336913388006306300.15s114 27133691338800
psp_c_74 365365 3653651.40s1923 182811464211894903653651.45s2024 17501146421365493 3653650.19s120 251146412122003653650.18s120 25114641212200 3653651.12s1455 131711464182127703653650.60s734 4491146415772362
psp_c_75 406406 4064060.36s457 371948010812004064060.37s460 32194801081701 4064060.18s125 3994809760204064060.17s125 399480976020 4064060.35s436 283948010918204064060.36s436 28394801091820
psp_c_76 409409 4094090.84s995 90912405178391304094090.89s1074 8521240517976133 4094090.22s143 571240513445604094090.22s143 57124051344560 4094090.43s452 2991240514994604094090.44s452 299124051499460
psp_c_77 365365 3653650.58s733 6511309715378003653650.58s766 571130971542702 3653650.20s123 411309713355103653650.20s123 41130971335510 3653650.40s448 2851309714665103653650.40s448 285130971466510
psp_c_78 239239 2392390.39s437 3798846107431702392390.40s467 359884610788171 2392390.18s82 2488469169002392390.18s82 248846916900 2392390.39s424 3328846107521702392390.39s424 304884610752171
psp_c_79 310310 3103100.76s1023 9511356717184103103100.80s1081 937135671731913 3103100.19s100 281356713890003103100.20s100 28135671389000 3103100.36s366 2731356715053003103100.36s366 273135671505300
psp_c_80 283283 2832830.79s1111 102559479298402832830.82s1168 9495947939243 2832830.18s108 2259476169002832830.18s108 225947616900 2832830.65s886 728594785211102832830.49s647 3875947813381
psp_c_81 342342 3423420.28s375 29074397980003423420.28s378 2097439798201 3423420.17s107 2274397645003423420.18s107 227439764500 3423420.29s375 24774397980003423420.28s375 2477439798000
psp_c_82 394394 3943940.24s272 1881168212112003943940.24s272 125116821211201 3943940.18s128 441168211953103943940.18s128 44116821195310 3943940.24s272 1881168212112003943940.24s272 188116821211200
psp_c_83 210210 2102100.21s152 10447935117402102100.22s152 1044793511740 2102100.18s92 4447935043202102100.18s92 444793504320 2102100.21s152 10447935117402102100.22s152 1044793511740
psp_c_84 584584 5845840.12s76 1869136913005845840.11s76 186913691300 5845840.11s72 1469136917005845840.10s72 146913691700 5845840.11s76 1869136913005845840.11s76 186913691300
psp_c_85 430430 4304300.64s926 8371259116301504304300.61s946 785125911631852 4304300.17s114 251259113021104304300.15s114 25125911302110 4304300.35s420 2701259114347104304300.34s420 270125911434710
psp_c_86 296296 2962960.30s334 2581045411147002962960.32s374 254104541119701 2962960.18s106 301045410668002962960.19s106 30104541066800 2962960.31s334 2451045411147002962960.30s334 245104541114700
psp_c_87 367367 3673670.22s191 11869487252003673670.21s191 1186948725200 3673670.17s96 2369487096003673670.17s96 236948709600 3673670.21s191 11869487252003673670.21s191 1186948725200
psp_c_88 258258 2582580.38s563 47455356568002582580.40s592 3695535661002 2582580.19s125 3655355726002582580.19s125 365535572600 2582580.31s401 28355356414002582580.31s401 2835535641400
psp_c_89 374374 3743740.17s95 3779557999003743740.17s95 377955799900 3743740.16s84 2679558009003743740.17s84 267955800900 3743740.17s95 3779557999003743740.17s95 377955799900
psp_c_90 289293 2932930.48s622 543555871361202932930.51s698 475555872321322932930.19s131 5255586393402932930.19s131 5255586393402932930.52s627 502555880923502932930.68s841 68155588583492
psp_c_91 258260 2602605.47s13123 130761449540201742402602605.41s13022 128191449540257727562602601.59s3498 34511449534103184702602600.85s1522 1404144953154677142602602.64s6069 59981449544386334202602600.74s1288 108014495331875603
psp_c_92 342360 3603600.31s467 402122941790212703603600.31s471 383122941792012813603600.24s278 21312294167377103603600.26s294 18812294174508913603600.30s479 393122941828713103603600.31s482 36912294183871321
psp_c_93 568568 5685680.54s1047 981274434646920005685680.58s1124 92127443466101983 5685680.33s695 6292744330413205685680.35s708 299274433122742 5685680.38s586 493274434421817705685680.39s602 45027443441111742
psp_c_94 425428 4284280.39s868 800181852666722104284280.41s962 812181852683422724284280.22s393 32518185227113104284280.22s345 20118185225782924284280.36s817 696181852779721004284280.43s1036 83218185297822053
psp_c_95 383399 3993992.97s8119 80282326157358330603993993.23s9267 88442326159167373763993990.60s1477 1386232613708619103993990.63s1233 828232614332520633993990.92s2251 2090232614683432503993990.58s907 63023261479591632
psp_c_96 481501 5015011.31s2030 1961228906045397705015011.33s2165 1951228906073997935015010.83s1578 1509228904702332305015010.81s1315 1074228904625526645015011.22s1959 1850228906716681805015011.00s1695 147822890585474334
psp_c_97 479489 4894891.62s5416 53252853059020182404894891.76s5609 52252853059499178154894890.99s2452 2361285305348850204894890.79s1745 1482285305094830644894890.53s1130 967285304307420404894890.71s1562 124928530494992674
psp_c_98 507518 5185182.15s5393 53082338258664160305185182.17s5457 51022338258730155155185180.55s1242 115723382335228205185180.59s1267 853233823744710235185180.68s1403 1248233823863512705185180.63s1426 97523382390161323
psp_c_99 299299 2992990.72s1987 1932109241912893302992990.73s2045 186910924191689464 2992990.19s135 8010924123951802992990.18s135 711092412395181 2992990.39s832 769109241765815502992990.40s921 69610924177561453
psp_c_100 371399 3993991.11s2178 2117195714296587603993991.12s2249 2090195714316887443993990.49s1199 1138195713330016303993990.42s792 574195713291017233993990.97s2253 2150195714119567203993990.56s1323 105819571346451713
psp_c_101 380380 3803800.17s396 30590559737003803800.18s412 2829055975501 3803800.13s128 3790559268003803800.14s128 379055926800 3803800.17s396 24790559737003803800.17s396 2479055973700
psp_c_102 295295 2952950.14s92 3758085874002952950.15s92 375808587400 2952950.14s80 2558085884002952950.14s80 255808588400 2952950.14s92 3758085874002952950.14s92 375808587400
psp_c_103 332332 3323320.19s512 42681869298003323320.19s525 3708186931602 3323320.12s126 4081868378003323320.14s126 408186837800 3323320.16s391 28781869184003323320.17s391 2878186918400
psp_c_104 610610 6106100.12s121 381451714518006106100.11s121 38145171451800 6106100.11s95 121451714547006106100.11s95 12145171454700 6106100.11s121 381451714518006106100.11s121 38145171451800
psp_c_105 568568 5685680.13s188 981334113543005685680.13s188 98133411354300 5685680.12s119 291334113747105685680.12s119 29133411374710 5685680.13s188 981334113543005685680.12s188 98133411354300
psp_c_106 350350 3503500.15s167 1001307713303003503500.15s167 100130771330300 3503500.15s106 391307713267103503500.16s106 39130771326710 3503500.17s167 1001307713303003503500.16s167 100130771330300
psp_c_107 424424 4244240.13s115 451231012334004244240.14s115 45123101233400 4244240.13s99 291231012379004244240.13s99 29123101237900 4244240.13s115 451231012334004244240.13s115 45123101233400
psp_c_108 280280 2802800.19s371 27958476831202802800.19s399 2215847685421 2802800.14s122 3058476127002802800.14s122 305847612700 2802800.19s371 24858476831202802800.19s371 2485847683120
psp_c_109 368368 3683680.18s419 3471000110982003683680.18s431 322100011100901 3683680.13s113 411000110281103683680.13s113 41100011028110 3683680.18s396 2931000111049303683680.18s396 293100011104930
psp_c_110 388388 3883880.17s419 33359516987603883880.17s420 3085951698861 3883880.13s130 4459516207103883880.13s130 445951620710 3883880.17s418 30059517330703883880.17s418 3005951733070
psp_c_111 380380 3803800.12s158 6651185233303803800.14s158 665118523330 3803800.12s119 2751185194003803800.14s119 275118519400 3803800.12s158 6651185233303803800.13s158 665118523330
psp_c_112 316316 3163160.12s96 3757105729003163160.12s96 375710572900 3163160.12s79 2057105752003163160.13s79 205710575200 3163160.13s96 3757105729003163160.13s96 375710572900
psp_c_113 393393 3933930.13s143 521143611456003933930.13s143 52114361145600 3933930.13s122 311143611531003933930.13s122 31114361153100 3933930.13s143 521143611456003933930.12s143 52114361145600
psp_c_114 540540 5405400.14s219 1351454815073205405400.14s219 123145481507321 5405400.12s119 351454814781105405400.12s119 35145481478110 5405400.14s219 1351454815073205405400.14s219 135145481507320
psp_c_115 467467 4674670.12s114 351066110671004674670.12s114 35106611067100 4674670.11s99 201066110687004674670.11s99 20106611068700 4674670.12s114 351066110671004674670.12s114 35106611067100
psp_c_116 429429 4294290.10s118 4373517356004294290.11s118 437351735600 4294290.10s102 2773517386004294290.10s102 277351738600 4294290.11s118 4373517356004294290.11s118 437351735600
psp_c_117 388388 3883880.14s148 811114111299003883880.14s148 81111411129900 3883880.13s98 311114111298003883880.12s98 31111411129800 3883880.14s148 811114111299003883880.14s148 81111411129900
psp_c_118 252252 2522520.14s88 3751535235002522520.13s88 375153523500 2522520.15s77 2651535221002522520.15s77 265153522100 2522520.12s88 3751535235002522520.14s88 375153523500
psp_c_119 247247 2472470.14s84 3546914737002472470.14s84 354691473700 2472470.14s75 2646914751002472470.14s75 264691475100 2472470.13s84 3546914737002472470.13s84 354691473700
psp_c_120 525525 5255250.11s98 351131911339005255250.10s98 35113191133900 5255250.10s88 251131911361005255250.11s88 25113191136100 5255250.11s98 351131911339005255250.11s98 35113191133900
psp_c_121 350410 39939955.90s89675 89605281759491659878039939959.13s92403 91975281759529861118939939928.60s46730 46660281751030782922503993998.99s16302 157222817577600892373993996.40s12749 126212817572271806303993996.19s11164 10857281756971770547
psp_c_122 unsat unsat1.00s1182 10040000unsat0.99s1182 10040000 unsat1.00s1182 10040000unsat0.99s1182 10040000 unsat1.00s1182 10040000unsat1.00s1182 10040000
psp_c_123 unsat unsat0.74s1080 9900000unsat0.73s1080 9900000 unsat0.75s1080 9900000unsat0.73s1080 9900000 unsat0.73s1080 9900000unsat0.73s1080 9900000
psp_c_124 237304 -286Time Out61519014987924803917600-286Time Out62293514987912163967831227027026.90s43782 43719149878722029140027027059.57s78132 7779114987103088512951027027031.25s47650 475491498795793314790270270106.87s121739 121269149871148838048110
psp_c_125 282351 -371Time Out538258313801802343812920-371Time Out 5436183138018355138728212 -336Time Out374662313802419742514890-316Time Out3538983138047344023373712-328Time Out450714313804381412896720-330Time Out3393423138043943522118112
psp_c_126 466502 50250222.74s28343 282632816416453314558050250223.65s29318 28855281641647871487075025022.64s3223 31432816482697151905025023.39s4365 39702816490234146055025024.12s5666 552428164101623284405025029.34s10737 103672816413278657197
psp_c_127 401404 4014015.64s8846 87622473854627475704014015.91s9259 88792473854931483764014010.24s169 8524738278733704014010.24s169 7124738278733714014012.08s3753 3595247384399249504014010.79s1347 89924738341651323
psp_c_128 499505 5055057.91s16472 163912281852462721805055057.87s16506 160652281853269707575055050.53s754 673228182807111805055050.63s907 578228183070416835055050.97s1560 1407228183577225405055051.28s2195 178922818383352954
psp_c_129 441517 50650675.60s80572 804832846726822550043050650673.91s81768 81176284672680415029995065069.42s11474 11385284671477665854050650612.59s15397 1510528467165772837875065069.26s11717 11542284671300086337050650611.09s11215 108732846714605662637
psp_c_130 359434 -417Time Out336361300163036432334500417417555.67s323490 322996300163066552239541141741782.03s65389 653073001618271042712041741728.87s29037 285433001617352117499841741763.90s57417 572623001619410136261041741729.00s28287 2777330016162918175278
psp_c_131 561561 5615610.31s707 6141354815364705615610.33s822 567135481550482 5615610.14s122 291354813950205615610.15s122 29135481395020 5615610.39s951 80713548166481105615610.41s857 6381354817149152
psp_c_132 481481 4814810.18s151 1001520515906304814810.18s151 100152051590630 4814810.14s75 241520515420004814810.14s75 24152051542000 4814810.18s151 1001520515906304814810.18s151 100152051590630
psp_c_133 474474 4744740.14s179 106976510011004744740.14s179 10697651001100 4744740.13s94 2197659924004744740.13s94 219765992400 4744740.14s179 106976510011004744740.15s179 10697651001100
psp_c_134 283283 2832830.18s123 7243644642002832830.17s123 724364464200 2832830.15s64 1343644515002832830.15s64 134364451500 2832830.18s123 7243644642002832830.17s123 724364464200
psp_c_135 443443 4434430.28s458 396887210844304434430.29s462 37088721084832 4434430.14s85 2388729077004434430.14s85 238872907700 4434430.24s375 277887210707104434430.26s375 27788721070710
psp_c_136 396396 3963960.18s201 11826202865003963960.16s201 1182620286500 3963960.13s108 2526202926003963960.12s108 252620292600 3963960.16s201 11826202865003963960.17s201 1182620286500
psp_c_137 281281 2812810.21s284 22255466509102812810.23s313 2215546655111 2812810.17s111 4955465913602812810.17s111 495546591360 2812810.22s284 22255466509102812810.22s284 2225546650910
psp_c_138 410410 4104100.20s247 16793459713004104100.21s247 1239345971301 4104100.16s107 2793459599004104100.15s107 279345959900 4104100.20s247 16793459713004104100.22s247 1679345971300
psp_c_139 306306 3063060.15s86 3462546393003063060.16s86 346254639300 3063060.16s75 2362546393003063060.15s75 236254639300 3063060.16s86 3462546393003063060.16s86 346254639300
psp_c_140 311311 3113110.19s228 15858506423603113110.20s228 1245850642361 3113110.17s114 4458506384303113110.16s114 445850638430 3113110.19s228 15858506423603113110.20s228 1585850642360
psp_c_141 290290 2902900.19s179 10571997377002902900.19s179 1057199737700 2902900.16s110 3671997374002902900.17s110 367199737400 2902900.19s179 10571997377002902900.19s179 1057199737700
psp_c_142 526526 5265260.21s344 2561200312577005265260.22s354 212120031260201 5265260.13s114 261200312182005265260.13s114 26120031218200 5265260.21s344 2481200312577005265260.21s344 248120031257700
psp_c_143 373373 3733730.13s141 6146904690003733730.14s141 614690469000 3733730.12s107 2746904743003733730.13s107 274690474300 3733730.13s141 6146904690003733730.13s141 614690469000
psp_c_144 420420 4204200.13s148 7598889946004204200.14s148 759888994600 4204200.13s102 29988810043004204200.13s102 2998881004300 4204200.14s148 7598889946004204200.13s148 759888994600
psp_c_145 668668 6686680.12s97 271321113211006686680.10s97 27132111321100 6686680.10s83 131321113225006686680.10s83 13132111322500 6686680.11s97 271321113211006686680.10s97 27132111321100
psp_c_146 420420 4204200.14s93 3185358556004204200.14s93 318535855600 4204200.14s80 1885358592004204200.14s80 188535859200 4204200.14s93 3185358556004204200.15s93 318535855600
psp_c_147 241241 2412410.14s91 4445754608002412410.15s91 444575460800 2412410.13s76 2945754644002412410.14s76 294575464400 2412410.14s91 4445754608002412410.15s91 444575460800
psp_c_148 197197 1971970.40s572 5285170806315001971970.41s601 508517081401552 1971970.18s104 60517061881401971970.18s104 6051706188140 1971970.34s456 392517077094901971970.42s618 50651708414872
psp_c_149 345345 3453450.18s198 12673987737003453450.17s198 1237398773701 3453450.14s95 2373987559003453450.14s95 237398755900 3453450.18s198 12673987737003453450.16s198 1267398773700
psp_c_150 396396 3963960.12s92 3269306957003963960.12s92 326930695700 3963960.13s80 2069306985003963960.12s80 206930698500 3963960.13s92 3269306957003963960.12s92 326930695700
psp_c_151 unsat unsat0.89s532 5120000unsat0.88s532 5120000 unsat0.91s532 5120000unsat0.88s532 5120000 unsat0.91s532 5120000unsat0.91s532 5120000
psp_c_152 307384 -400Time Out415320215401188703096110-400Time Out 4439212154011923533054311 -375Time Out438391215403063482893030-369Time Out4149182154034353227504812-393Time Out393662215401811942629000-371Time Out4417472154037619729023312
psp_c_153 533554 55355351.71s54855 547643561317889830255055355357.88s61434 60862356131829643460385535533.80s3417 33263561365121129005535534.57s4085 37483561374074168155535534.37s3837 36703561373257162205535533.76s3133 2823356137453112805
psp_c_154 444535 52452464.58s47384 473183754927467231194052452465.77s48654 482933754928125131699852452414.40s12333 12267375491884467143052452412.41s10291 9923375491828826207752452414.22s11397 11291375491959007005052452414.09s10669 102833754918677062867
psp_c_155 320375 -382Time Out504841184651490353635800-382Time Out 4964761846515027935640311 361361331.46s312587 312504184651467782082160361361296.13s264693 2642541846514325217519911361361201.56s200333 200186184651113881333300361361402.81s303644 3030621846514247220170612
psp_c_156 356399 -396Time Out412848240592273792971000-396Time Out3931642405922323228265711387387134.98s125560 12548024059159182813690387387215.61s190416 1899262405922091912210011387387216.76s184729 184590240591638861199000387387176.45s159621 1591242405916095010401011
psp_c_157 410475 45345393.10s141641 1415121487066950997630453453102.36s152269 1518151487068098107643104534532.08s3103 29741487030756112904534531.89s3399 31911487028930129954534538.73s21082 2091614870512581375404534532.28s4044 3668148703242017935
psp_c_158 349397 39739713.67s17945 17910293597392912842039739713.97s18128 1793229359741541285173973971.28s1383 1348293594823442403973971.34s1652 1389293595048678843973971.56s1655 1596293595057093403973971.39s1675 149429359512738674
psp_c_159 447488 4884884.81s6706 66142173963606227104884885.15s7338 69212173964726242254884882.93s3298 3206217395113464204884882.44s2687 2264217395732178154884882.72s3093 2931217395083072204884883.24s3721 3269217396462213655
psp_c_160 323394 -396Time Out472890263681523513265770-396Time Out 4734522636815273532673011 -375Time Out441175263682047622868610-377Time Out4932582636822681832279912-380Time Out445913263681888222884630-374Time Out4918732636821121932166412
psp_c_161 339339 3393390.37s448 36283299447003393390.39s453 3158329945411 3393390.20s128 4283298725103393390.20s128 428329872510 3393390.37s439 28983299600103393390.38s439 2898329960010
psp_c_162 458458 4584580.24s260 1871009710844004584580.25s260 122100971084401 4584580.17s96 231009710329004584580.17s96 23100971032900 4584580.25s260 1871009710844004584580.25s260 187100971084400
psp_c_163 434434 4344341.91s2601 2514163302584160604344341.96s2768 241216330260686074 4344340.18s122 351633016811204344340.19s122 35163301681120 4344341.18s1512 1361163302452118304344340.86s1095 8761633021935383
psp_c_164 292292 2922920.27s203 16176079127502922920.27s203 1227607912751 2922920.16s64 2276077929002922920.17s64 227607792900 2922920.26s203 16176079127502922920.26s203 1617607912750
psp_c_165 361371 37137140.50s55154 55084138555867732328037137142.39s55088 5464413855585973224183713717.95s9454 93841385552860520103713713.17s3708 34841385534077140353713718.52s12325 121961385540185722403713714.31s5351 5074138553643421096
psp_c_166 473473 4734730.16s128 4490899092004734730.16s128 449089909200 4734730.16s102 1890899128004734730.16s102 189089912800 4734730.16s128 4490899092004734730.17s128 449089909200
psp_c_167 373373 3733730.27s353 26554355883003733730.28s382 2135435592901 3733730.17s109 2154355688003733730.17s109 215435568800 3733730.28s353 24554355883003733730.28s353 2455435588300
psp_c_168 439439 4394390.46s567 494980611741304394390.48s614 44898061182622 4394390.17s104 31980610044204394390.18s104 3198061004420 4394390.37s405 282980611459604394390.36s405 28298061145960
psp_c_169 328328 3283280.25s234 16876028283403283280.25s234 1217602828341 3283280.18s104 3876027874103283280.18s104 387602787410 3283280.25s234 16876028283403283280.25s234 1687602828340
psp_c_170 410410 4104100.86s1032 97318063238554004104100.89s1068 9191806324004403 4104100.21s89 301806318498004104100.21s89 30180631849800 4104101.16s1393 1293180632778015004104101.03s1249 104418063275501203
psp_c_171 321321 3213210.17s122 5734703498003213210.17s122 573470349800 3213210.16s92 2734703528003213210.16s92 273470352800 3213210.17s122 5734703498003213210.17s122 573470349800
psp_c_172 378378 3783780.16s115 4683498374003783780.16s115 468349837400 3783780.16s97 2883498406003783780.16s97 288349840600 3783780.17s115 4683498374003783780.18s115 468349837400
psp_c_173 397397 3973970.26s339 25181888675003973970.26s342 2468188867701 3973970.16s109 2181888432003973970.16s109 218188843200 3973970.26s339 24781888675003973970.26s339 2478188867500
psp_c_174 489489 4894890.25s232 1561476015118004894890.25s232 123147601511801 4894890.17s99 231476014923104894890.17s99 23147601492310 4894890.25s232 1561476015118004894890.25s232 156147601511800
psp_c_175 288288 2882880.20s142 9070827431002882880.20s142 907082743100 2882880.17s77 2570827290002882880.16s77 257082729000 2882880.21s142 9070827431002882880.20s142 907082743100
psp_c_176 538538 5385380.57s805 7241656219140005385380.60s854 620165621919312 5385380.16s101 201656216892005385380.16s101 20165621689200 5385380.32s400 2641656218069005385380.33s400 264165621806900
psp_c_177 261261 2612610.20s114 6059806155002612610.20s114 605980615500 2612610.20s92 3859806472502612610.19s92 385980647250 2612610.20s114 6059806155002612610.20s114 605980615500
psp_c_178 412412 4124120.20s178 121975910352104124120.19s178 12197591035210 4124120.16s84 27975910024004124120.15s84 2797591002400 4124120.20s178 121975910352104124120.20s178 12197591035210
psp_c_179 362362 3623620.24s264 200948110059003623620.25s270 18794811007801 3623620.17s90 2694819642003623620.18s90 269481964200 3623620.24s264 200948110059003623620.25s264 20094811005900
psp_c_180 551551 5515510.35s401 3151438215166005515510.37s430 299143821520301 5515510.17s121 351438214570105515510.18s121 35143821457010 5515510.35s401 2451438215166005515510.36s401 245143821516600
psp_c_181 454456 4564560.75s1562 1494217254617836504564560.78s1672 1501217254665336134564560.66s1769 1701217253944710204564560.48s1115 62021725344817034564560.37s539 41821725365748604564560.36s536 3362172536492771
psp_c_182 360376 3763761.21s3971 38861229728582162303763761.25s4278 39621229728512170853763760.37s974 88912297193857103763760.45s1053 840122972164713233763760.45s1147 1012122972192714703763760.54s1407 104112297231941653
psp_c_183 447461 4614612.99s7988 79421628639164429504614612.65s7034 68441628636935357254614610.64s1367 1321162863287641104614610.77s1533 1304162863716055844614610.45s789 732162863046236804614610.67s1320 120816286346465093
psp_c_184 574574 5745740.98s1992 1920198963757188805745741.09s2445 2127198963814610144 5745740.42s1288 121619896293718005745740.43s1162 7451989629981783 5745740.48s1069 933198963602726205745740.45s708 52619896365162721
psp_c_185 318370 36436430.71s61669 61602184327588036159036436431.05s62471 6222718432764413661983643642.61s5357 52901843261323273003643642.41s4491 43411843256690273953643642.36s4850 47411843263532240603643643.00s5671 5377184327039130336
psp_c_186 408410 4104101.06s3021 2937235964417765504104101.07s3123 2850235964410264044104100.60s1977 189323596304985804104100.49s1325 60323596306714534104100.51s1246 1106235963566615804104100.40s769 47523596347861312
psp_c_187 585585 5855850.46s1526 144119318285633705855850.50s1632 13701931828875383 5855850.18s142 5719318216751005855850.18s142 571931821675100 5855850.23s466 30119318237251005855850.23s466 3011931823725100
psp_c_188 275321 30730761.23s115624 115563193837144465127030730753.46s104363 10403919383711215829293073071.29s2807 27461938342935139303073071.40s2906 26221938342535147053073070.97s1775 1682193834613087403073071.74s3496 3257193835704217775
psp_c_189 640640 6406400.50s1435 136116114273754006406400.51s1548 13291611427714383 6406400.35s1332 12581611420266806406400.39s1321 443161142165093 6406400.45s1680 156216114243861206406400.56s1912 12821611426314294
psp_c_190 390401 4014010.32s777 71297151425616704014010.34s866 69897151432417224014010.21s394 3299715127994004014010.19s371 2099715126382524014010.29s753 6579715141369604014010.28s709 4469715142041002
psp_c_191 492493 4934930.13s205 127901695292104934930.13s205 121901695292114934930.15s232 154901610070404934930.14s234 66901610092514934930.13s205 127901695292104934930.13s205 12790169529210
psp_c_192 274274 2742740.17s323 252479055321002742740.18s375 25147905611101 2742740.13s115 4447905258202742740.13s115 444790525820 2742740.17s323 238479055321002742740.17s323 23847905532100
psp_c_193 623623 6236230.07s118 271012410128006236230.08s118 27101241012800 6236230.08s108 171012410150006236230.09s108 17101241015000 6236230.07s118 271012410128006236230.08s118 27101241012800
psp_c_194 451451 4514510.13s231 17483558898704514510.12s231 1248355889871 4514510.12s86 2983558609104514510.13s86 298355860910 4514510.13s231 17483558898704514510.13s231 1748355889870
psp_c_195 475475 4754750.21s597 5138852105252004754750.21s642 433885210579212 4754750.13s128 4488529418304754750.12s128 448852941830 4754750.17s448 285885210365404754750.18s448 28588521036540
psp_c_196 340340 3403400.14s196 14265477201003403400.14s196 1206547720101 3403400.12s83 2965476827003403400.12s83 296547682700 3403400.14s196 14265477201003403400.14s196 1426547720100
psp_c_197 564564 5645640.16s425 3321103611845005645640.16s440 305110361186001 5645640.11s127 341103611337005645640.12s127 34110361133700 5645640.16s425 2441103611845005645640.16s425 244110361184500
psp_c_198 459459 4594590.15s294 24051405941004594590.16s297 2085140594401 4594590.11s92 3851405311104594590.11s92 385140531110 4594590.14s294 24051405941004594590.15s294 2405140594100
psp_c_199 417417 4174170.12s209 13746905150004174170.11s209 1234690515001 4174170.10s92 2046904842004174170.10s92 204690484200 4174170.12s209 13746905150004174170.12s209 1374690515000
psp_c_200 349349 3493490.14s223 16074158130503493490.14s223 1247415813051 3493490.12s89 2674157617003493490.12s89 267415761700 3493490.15s223 16074158130503493490.14s223 1607415813050
psp_c_201 461461 4614610.12s262 17076977967004614610.12s262 1237697796701 4614610.11s121 2976977836004614610.11s121 297697783600 4614610.12s262 17076977967004614610.12s262 1707697796700
psp_c_202 381381 3813810.16s323 24481978896603813810.16s332 2068197890561 3813810.13s123 4481978440203813810.13s123 448197844020 3813810.16s323 24481978896603813810.15s323 2448197889660
psp_c_203 392392 3923920.14s180 1101042210660003923920.13s180 110104221066000 3923920.12s97 271042210637003923920.12s97 27104221063700 3923920.13s180 1101042210660003923920.14s180 110104221066000
psp_c_204 333333 3333330.16s332 26851565854203333330.17s345 2535156590411 3333330.13s94 3051565337003333330.12s94 305156533700 3333330.16s332 24751565854203333330.16s332 2475156585420
psp_c_205 560560 5605600.12s231 13792909602005605600.12s231 1239290960201 5605600.10s113 1992909548005605600.10s113 199290954800 5605600.12s231 13792909602005605600.12s231 1379290960200
psp_c_206 425425 4254250.10s140 5361676181004254250.10s140 536167618100 4254250.11s124 3761676213004254250.12s124 376167621300 4254250.11s140 5361676181004254250.11s140 536167618100
psp_c_207 481481 4814810.12s129 411037010386004814810.12s129 41103701038600 4814810.12s133 451037010428104814810.12s133 45103701042810 4814810.12s129 411037010386004814810.13s129 41103701038600
psp_c_208 660660 6606600.08s118 281098911023006606600.08s118 28109891102300 6606600.09s106 161098911085006606600.08s106 16109891108500 6606600.08s118 281098911023006606600.08s118 28109891102300
psp_c_209 619619 6196190.09s94 2167876815006196190.09s94 216787681500 6196190.08s101 2867876889006196190.08s101 286787688900 6196190.08s94 2167876815006196190.08s94 216787681500
psp_c_210 290290 2902900.13s175 11563556697002902900.14s175 1156355669700 2902900.13s102 4263556671102902900.13s102 426355667110 2902900.14s175 11563556697002902900.13s175 1156355669700
psp_c_211 434445 4454454.71s9817 97342162061590480904454455.33s11085 107052162063179558264454450.93s1436 1353216203646621304454451.02s1737 1325216204015628644454450.93s1537 1401216204057425304454450.88s1361 103621620434932493
psp_c_212 554564 5645642.58s3912 38302067951931232505645642.59s4023 37272067952252224145645641.57s2855 2773206794503262305645640.89s1448 1215206793968730745645640.97s1530 1397206794001138305645641.05s1722 140920679413774444
psp_c_213 709710 7107103.42s4740 46623880999390139407107103.41s4769 447638809101478134757107101.46s2062 1984388096229222607107101.01s1409 804388095782415837107101.48s1737 1615388097533724807107102.02s2762 221338809877603544
psp_c_214 618624 62462419.11s22946 228663730818165011969062462418.50s21588 21076373081772671086576246243.31s3433 33533730894570126406246241.84s1924 1715373087246543346246241.60s2131 1988373086450044006246241.56s1752 144837308687383334
psp_c_215 573573 5735730.52s767 70411281172204905735730.50s794 6571128117486472 5735730.23s264 2011128113110905735730.23s268 801128113288101 5735730.32s439 33411281160182605735730.35s439 3191128116040231
psp_c_216 unsat unsat0.43s464 4640000unsat0.43s464 4640000 unsat0.43s464 4640000unsat0.43s464 4640000 unsat0.43s464 4640000unsat0.43s464 4640000
psp_c_217 275365 36236295.13s93168 931082519414705963154036236292.99s89825 89555251941476926035893623622.64s3513 34532519479673208803623622.99s3750 35582519493837231953623623.45s4655 45432519486732286103623623.24s4160 3818251948844523795
psp_c_218 247325 -317Time Out539501171331072623742960-317Time Out5344161713310716037119312-310Time Out445260171331787862993460-314Time Out4289741713325760328492612-310Time Out399585171331622102699210-309Time Out4129671713322121927596512
psp_c_219 761761 7617611.60s2594 2494266654799340907617611.70s2864 257326665490894474 7617610.65s1061 96126665352035407617610.59s882 4752666534913303 7617611.02s1763 1605266654080710207617610.78s1230 8112666540781883
psp_c_220 352403 3933935.32s8919 88412157661519398903933935.04s8567 82092157660109366163933932.74s4007 39292157652578205803933932.20s3416 31402157655676128353933931.98s3309 31732157651504130803933931.95s3345 2846215764864912575
psp_c_221 559559 5595590.16s239 15477998250505595590.15s239 1247799825051 5595590.12s126 4177998339205595590.12s126 417799833920 5595590.16s239 15477998250505595590.16s239 1547799825050
psp_c_222 647647 6476470.10s133 3370897115006476470.11s133 337089711500 6476470.10s113 1370897167006476470.10s113 137089716700 6476470.10s133 3370897115006476470.11s133 337089711500
psp_c_223 573573 5735730.14s205 12576848226405735730.14s205 1247684822641 5735730.11s122 4276848098005735730.12s122 427684809800 5735730.14s205 12576848226405735730.14s205 1257684822640
psp_c_224 292304 3043040.54s1052 9756058958633003043040.54s1141 9206058969132033043040.48s830 75360581088213003043040.56s1007 74960581145319133043040.45s771 65460581044114503043040.54s944 7556058107372053
psp_c_225 526526 5265260.17s325 23476268364005265260.17s333 2057626837401 5265260.11s120 2976267766005265260.12s120 297626776600 5265260.17s325 23476268364005265260.17s325 2347626836400
psp_c_226 357357 3573570.18s241 17183158745103573570.19s247 1648315876411 3573570.16s98 2883158500003573570.15s98 288315850000 3573570.19s241 17183158745103573570.18s241 1718315874510
psp_c_227 402402 4024020.30s552 4708689101091704024020.31s573 420868910148172 4024020.14s131 4986898907204024020.14s131 498689890720 4024020.30s560 4198689104581204024020.31s560 314868910458121
psp_c_228 515515 5155150.30s609 52510345120834105155150.31s662 4961034512144402 5155150.14s115 311034510625005155150.14s115 31103451062500 5155150.35s713 56610345128893205155150.35s707 4371034512917292
psp_c_229 314314 3143140.27s541 47057187200103143140.29s554 4385718720702 3143140.16s109 3857185991003143140.16s109 385718599100 3143140.23s376 28557187007003143140.24s376 2855718700700
psp_c_230 321321 3213210.24s314 24573178206303213210.24s351 2267317831511 3213210.19s172 10373178249003213210.19s172 647317824901 3213210.24s314 24173178206303213210.24s314 2417317820630
psp_c_231 285285 2852850.22s330 25174878125002852850.23s359 2427487816401 2852850.16s130 5174877815202852850.15s130 517487781520 2852850.22s330 24674878125002852850.23s330 2467487812500
psp_c_232 494494 4944940.14s219 13184258665004944940.15s219 1248425866501 4944940.12s112 2484258715004944940.12s112 248425871500 4944940.15s219 13184258665004944940.15s219 1318425866500
psp_c_233 551551 5515510.14s163 9071517289005515510.14s163 907151728900 5515510.12s91 1871517281005515510.12s91 187151728100 5515510.14s163 9071517289005515510.13s163 907151728900
psp_c_234 279279 2792790.13s60 2863126347002792790.14s60 286312634700 2792790.13s53 2163126367002792790.14s53 216312636700 2792790.14s60 2863126347002792790.14s60 286312634700
psp_c_235 327327 3273270.15s93 3455605595003273270.14s93 345560559500 3273270.15s85 2655605631003273270.15s85 265560563100 3273270.15s93 3455605595003273270.15s93 345560559500
psp_c_236 348348 3483480.21s312 23866907441003483480.21s339 2216690748301 3483480.13s96 2266906925003483480.13s96 226690692500 3483480.21s312 23866907441003483480.21s312 2386690744100
psp_c_237 328328 3283280.15s81 4059776065003283280.14s81 405977606500 3283280.15s63 2259776113003283280.15s63 225977611300 3283280.15s81 4059776065003283280.14s81 405977606500
psp_c_238 422422 4224220.13s111 3973407363004224220.13s111 397340736300 4224220.12s91 1973407381004224220.12s91 197340738100 4224220.12s111 3973407363004224220.13s111 397340736300
psp_c_239 332332 3323320.14s147 9953435898203323320.15s147 995343589820 3323320.14s65 1753435485003323320.13s65 175343548500 3323320.14s147 9953435898203323320.15s147 995343589820
psp_c_240 434434 4344340.25s472 38762087353304344340.26s489 3716208736822 4344340.14s119 3462086370004344340.13s119 346208637000 4344340.29s606 51762087946304344340.29s615 4346208800132
psp_c_241 382430 -489Time Out41677023712712223000030-489Time Out 417749237127206630025511 -431Time Out48054023712920383183490-416Time Out5176512371213975434452912-438Time Out41424323712947842808130-418Time Out4996952371215061033237912
psp_c_242 355431 -449Time Out364106312171781342559700-450Time Out 3671793121717955825928911 42542576.30s64902 6483731217215332429290425425105.25s85428 85038312172425555674310425425110.57s96030 959243121723450663179042542598.92s80165 79687312172402375341110
psp_c_243 463533 -539Time Out410644298882397702988570-539Time Out 4021152988824054629210211 51951922.96s27741 27670298881169921770805195198.40s10546 1019129888942256384751951910.53s13749 136102988888869832605195197.76s9070 8637298889362749026
psp_c_244 472514 508508161.72s186790 186719223711353071323530508508157.56s182968 18253922371135835129629105085086.54s7866 77952237167682515505085085.50s7042 67212237165803419565085085.68s7458 73422237166520461105085084.74s5929 5636223716785232496
psp_c_245 388468 -498Time Out33509625881871402513510-498Time Out 327366258818787024574111 -458Time Out393858258811641322629500-455Time Out4067562588126332727224012-463Time Out426708258811470902832620-453Time Out5179122588125881534472512
psp_c_246 543574 5745746.96s8226 81742301385960388205745747.76s9239 90112301386296419365745741.70s1794 1742230135927578605745741.70s1545 1387230136628178545745741.54s1528 1432230136378670005745742.24s2199 204223013749139814
psp_c_247 434478 47147161.44s83597 835131796811555954637047147160.94s83969 833701796811801354617947147132.39s42013 41929179689154225405047147120.07s31050 30641179688071718359847147121.10s33340 33181179687672220674047147115.98s22520 219561796878721131488
psp_c_248 372443 -431Time Out514165259202430033630730-431Time Out512081259202415203599561243043080.85s76849 767742592015295749050043043033.57s38162 377192592012049023442943043044.42s47846 477182592010649330079043043031.29s34388 3389625920118627211368
psp_c_249 608635 63363311.45s12697 12614295801223367043063363312.14s13265 1285929580124648723666336333.22s3471 33882958075468156106336331.95s1875 1562295806988459846336332.77s3155 3029295807194994906336332.97s3169 2859295808093212615
psp_c_250 unsat unsat0.45s678 6240000unsat0.45s678 6240000 unsat0.45s678 6240000unsat0.45s678 6240000 unsat0.46s678 6240000unsat0.46s678 6240000
psp_c_251 297308 3083082.91s4168 4087822415152209403083082.91s4322 3958822415339204653083081.46s1973 189282241690659803083081.61s2253 186082241877670243083081.45s2088 1956822416940106003083081.21s1759 15688224169238294
psp_c_252 420420 4204200.22s265 19276728237004204200.21s265 1207672823701 4204200.16s123 5076728090504204200.16s123 507672809050 4204200.22s265 19276728237004204200.22s265 1927672823700
psp_c_253 509509 5095090.43s576 4881276014258305095090.43s594 370127601429032 5095090.17s119 311276013092105095090.17s119 31127601309210 5095090.32s402 2801276014115105095090.32s402 280127601411510
psp_c_254 305305 3053050.40s495 40838255043003053050.38s499 3523825504601 3053050.21s153 6638254158403053050.21s153 653825415841 3053050.37s452 31238255167403053050.37s452 3123825516741
psp_c_255 599599 5995990.32s383 303806390412805995990.33s417 25980639144281 5995990.12s100 2080638286005995990.13s100 208063828600 5995990.31s383 243806390412805995990.31s383 24380639041280
psp_c_256 452452 4524520.14s102 5861966404004524520.14s102 586196640400 4524520.13s75 3161966342004524520.12s75 316196634200 4524520.14s102 5861966404004524520.14s102 586196640400
psp_c_257 319319 3193190.42s537 47549066903003193190.42s552 4424906693102 3193190.17s99 3749065097003193190.17s99 374906509700 3193190.32s374 28149066317003193190.32s374 2814906631700
psp_c_258 338338 3383380.39s459 38960557841103383380.41s473 3576055786321 3383380.18s115 4560556298103383380.18s115 456055629810 3383380.38s418 33760557618103383380.39s418 3086055761811
psp_c_259 396396 3963960.20s194 12450615678203963960.20s194 1245061567820 3963960.16s136 6650615644903963960.18s136 665061564491 3963960.20s194 12450615678203963960.20s194 1245061567820
psp_c_260 455469 4694690.62s858 782138931992911004694690.63s932 739138931998610424694690.67s889 81313893199185204694690.54s642 44613893204866434694690.58s715 58413893198345904694690.58s735 5061389319925572
psp_c_261 306306 3063060.16s119 5340374053003063060.18s119 534037405300 3063060.16s97 3140374081003063060.16s97 314037408100 3063060.16s119 5340374053003063060.16s119 534037405300
psp_c_262 400400 4004000.12s105 3549444958004004000.13s105 354944495800 4004000.12s86 1649444978004004000.13s86 164944497800 4004000.13s105 3549444958004004000.13s105 354944495800
psp_c_263 377377 3773770.22s204 12929123239103773770.22s204 1212912323911 3773770.18s118 4329123289203773770.18s118 432912328920 3773770.23s204 12929123239103773770.22s204 1292912323910
psp_c_264 429429 4294290.23s244 16662076802604294290.21s244 1266207683851 4294290.17s125 4762076930204294290.16s125 476207693020 4294290.20s244 16662076802604294290.21s244 1666207680260
psp_c_265 263263 2632630.29s341 25741285019002632630.29s344 2294128501501 2632630.20s138 5441284482102632630.20s138 544128448210 2632630.29s341 24641285019002632630.28s341 2464128501900
psp_c_266 430430 4304300.44s620 5361159613061004304300.45s640 460115961310102 4304300.17s114 301159611791004304300.18s114 30115961179100 4304300.36s449 2761159612924004304300.35s449 276115961292400
psp_c_267 563563 5635630.22s231 1551090911430005635630.22s231 123109091143001 5635630.14s105 291090911063005635630.15s105 29109091106300 5635630.22s231 1551090911430005635630.22s231 155109091143000
psp_c_268 366366 3663660.24s242 17162486789003663660.23s242 1226248678901 3663660.17s105 3462486466003663660.17s105 346248646600 3663660.24s242 17162486789003663660.24s242 1716248678900
psp_c_269 247247 2472470.23s134 10460967030902472470.22s134 1046096703090 2472470.18s59 2960966650402472470.17s59 296096665040 2472470.22s134 10460967030902472470.23s134 1046096703090
psp_c_270 437437 4374370.25s279 20880568629104374370.27s287 1958056864311 4374370.17s101 3080568258104374370.17s101 308056825810 4374370.26s279 20880568629104374370.26s279 2088056862910
psp_c_271 445498 49749712.09s7563 7538291592077135904049749712.53s8168 810729159206473640564974972.94s2418 239329159110915165404974976.94s5531 535429159157145361664974972.84s2665 263029159111060184504974973.25s2949 27852915912273419175
psp_c_272 261277 2772770.64s1921 1856115991790166102772770.70s2201 1951115991815875342772770.45s1164 1099115991835911902772770.43s1094 73811599183607432772770.43s1079 964115991831419402772770.39s839 63511599185861932
psp_c_273 575598 57957925.05s24685 246293162618986118406057957929.82s28648 28493316261946192172275795791.05s1551 1495316267473970505795791.81s2257 21433162692355104055795791.90s2560 24873162693560114605795791.39s1866 166331626846757534
psp_c_274 323323 3233230.29s782 70311425151592403233230.29s838 6561142515252202 3233230.14s133 541142512003103233230.14s133 54114251200310 3233230.22s469 33611425139052103233230.22s469 3091142513905211
psp_c_275 486486 4864860.84s2797 272024496403916104864860.89s2891 25892449640872704 4864860.32s729 65224496280071604864860.36s697 5502449629453313 4864860.37s816 69224496308214004864860.45s1193 7842449631383533
psp_c_276 unsat unsat0.57s1042 10040000unsat0.57s1042 10040000 unsat0.56s1042 10040000unsat0.57s1042 10040000 unsat0.58s1042 10040000unsat0.57s1042 10040000
psp_c_277 334448 41041031.46s41998 419302695015319826690041041029.31s40363 39987269501501212525884104104.18s4881 481326950118375266104104102.74s3232 30322695096178183154104102.08s2783 26662695092342149404104103.40s4408 40912695012242024125
psp_c_278 578587 5875870.51s1206 1130215283223338405875870.57s1345 1097215283244637635875870.27s355 27921528283327105875870.33s621 499215282993310735875870.34s648 525215282975814805875870.32s616 47021528298371411
psp_c_279 298298 2982980.58s1801 174916494288629202982980.59s1855 17091649429020943 2982980.15s102 501649417441402982980.14s102 50164941744140 2982980.24s453 35616494207013402982980.25s453 3131649420701341
psp_c_280 436451 4514511.98s3561 35192162148511174504514511.85s3353 32212162148459156944514510.32s404 362216213053311004514510.30s383 26521621305239224514510.53s974 895216213811621104514510.58s1037 83021621388602383
psp_c_281 207207 2072070.13s164 10244664671002072070.14s164 1024466467100 2072070.13s92 3044664642002072070.13s92 304466464200 2072070.16s164 10244664671002072070.15s164 1024466467100
psp_c_282 320320 3203200.11s106 4430563076003203200.11s106 443056307600 3203200.11s76 1430563176003203200.11s76 143056317600 3203200.10s106 4430563076003203200.10s106 443056307600
psp_c_283 302302 3023020.16s122 591103311203003023020.16s122 59110331120300 3023020.16s94 311103311217003023020.16s94 31110331121700 3023020.15s122 591103311203003023020.16s122 59110331120300
psp_c_284 279279 2792790.13s95 4144184473002792790.13s95 414418447300 2792790.13s79 2544184513002792790.13s79 254418451300 2792790.13s95 4144184473002792790.13s95 414418447300
psp_c_285 454454 4544540.14s133 871162412026004544540.14s133 87116241202600 4544540.12s70 241162411787004544540.12s70 24116241178700 4544540.14s133 871162412026004544540.14s133 87116241202600
psp_c_286 444444 4444440.13s191 1111292213148004444440.13s191 111129221314800 4444440.11s92 121292213078004444440.12s92 12129221307800 4444440.14s191 1111292213148004444440.12s191 111129221314800
psp_c_287 416416 4164160.18s161 12621796237823204164160.18s161 1232179623782321 4164160.15s72 372179622255104164160.15s72 37217962225510 4164160.19s161 12621796237823204164160.17s161 1262179623782320
psp_c_288 325325 3253250.17s247 18110729113571603253250.18s259 1681072911392161 3253250.15s102 361072911066103253250.15s102 36107291106610 3253250.18s247 18110729113571603253250.18s247 1811072911357160
psp_c_289 336336 3363360.25s763 6811079313302103363360.27s810 637107931336512 3363360.13s124 421079311190103363360.14s124 42107931119010 3363360.20s490 3821079312696503363360.22s490 308107931269651
psp_c_290 288288 2882880.11s122 5229143033002882880.13s122 522914303300 2882880.12s101 3129142994002882880.13s101 312914299400 2882880.13s122 5229143033002882880.14s122 522914303300
psp_c_291 346346 3463460.13s60 271079510825003463460.14s60 27107951082500 3463460.13s51 181079510834003463460.13s51 18107951083400 3463460.13s60 271079510825003463460.13s60 27107951082500
psp_c_292 224224 2242240.14s229 16254715844002242240.14s229 1235471584401 2242240.13s96 2954715630002242240.12s96 295471563000 2242240.13s229 16254715844002242240.15s229 1625471584400
psp_c_293 275275 2752750.14s159 12047805606102752750.14s159 1204780560610 2752750.12s57 1847805171002752750.12s57 184780517100 2752750.14s159 12047805606102752750.14s159 1204780560610
psp_c_294 401401 4014010.11s42 2068446892004014010.12s42 206844689200 4014010.12s37 1568446915004014010.12s37 156844691500 4014010.12s42 2068446892004014010.12s42 206844689200
psp_c_295 326326 3263260.15s151 9153135562003263260.15s151 915313556200 3263260.14s80 2053135671003263260.14s80 205313567100 3263260.14s151 9153135562003263260.15s151 915313556200
psp_c_296 379379 3793790.12s66 2390529101003793790.12s66 239052910100 3793790.13s55 1290529126003793790.13s55 129052912600 3793790.11s66 2390529101003793790.12s66 239052910100
psp_c_297 357357 3573570.14s182 9984568637003573570.15s182 998456863700 3573570.14s107 2484568622003573570.14s107 248456862200 3573570.16s182 9984568637003573570.15s182 998456863700
psp_c_298 328328 3283280.14s106 641035910682003283280.16s106 64103591068200 3283280.14s68 261035910645003283280.13s68 26103591064500 3283280.15s106 641035910682003283280.15s106 64103591068200
psp_c_299 352352 3523520.13s72 331061810661003523520.12s72 33106181066100 3523520.13s64 251061810684003523520.14s64 25106181068400 3523520.13s72 331061810661003523520.13s72 33106181066100
psp_c_300 330330 3303300.14s119 4688788943003303300.13s119 468878894300 3303300.13s101 2888788944003303300.13s101 288878894400 3303300.13s119 4688788943003303300.11s119 468878894300
psp_c_301 407412 4124122.85s4689 46291867944650232804124122.89s4795 45861867944759232654124121.70s2373 2313186793408792904124121.62s2206 2026186793372393244124121.92s2844 27401867942230108304124121.33s1865 162418679368536064
psp_c_302 unsat unsat0.68s878 8440000unsat0.67s878 8440000 unsat0.68s878 8440000unsat0.67s878 8440000 unsat0.66s878 8440000unsat0.68s878 8440000
psp_c_303 261329 31931916.71s29136 290822385111013119765031931916.54s28926 28672238511088041952173193192.10s4015 39612385154042206703193191.53s2825 265723851518401673531931915.54s27525 27444238511238341789903193192.62s4656 4284238516698021495
psp_c_304 268346 -344Time Out364856232502934392852520-341Time Out3649452325031592228752311333333146.73s129604 12956523250350306864860333333132.18s114107 113707232503196857550310333333233.42s165081 165022232503381581102340333333168.35s129757 129364232503192248705610
psp_c_305 unsat unsat0.55s790 7080000unsat0.54s790 7080000 unsat0.55s790 7080000unsat0.54s790 7080000 unsat0.55s790 7080000unsat0.54s790 7080000
psp_c_306 286296 2882886.98s12752 126932328460443661702882887.09s12904 126252328460844660762882881.78s2929 2870232843982066902882881.00s1454 1270232843267051442882882.40s3963 3847232844880280102882882.94s5339 4995232845295714016
psp_c_307 261342 -311Time Out454716182251547422915190-311Time Out4652301822515515629776911309309112.57s112727 11269318225135548749050309309110.16s112108 111804182251468167335110309309209.50s191506 191442182251463901278440309309121.65s120530 120180182251710287930710
psp_c_308 423564 545545246.03s85309 8528440030433121630670545545243.69s83398 832474003043192161972954554531.48s20318 202934003031931414030054554527.62s17184 169704003029242211552754554519.74s12759 12721400302604398873054554525.81s13853 136504003029240796047
psp_c_309 458503 50350310.75s7901 7864359341595696315050350311.03s7906 778135934160374628955035032.87s2806 276935934104136163505035034.44s4263 408435934137370246855035033.18s2876 281735934105410153805035033.62s3302 31863593412820121405
psp_c_310 207277 -282Time Out66340918684934894648340-282Time Out 664305186849063846359212 -290Time Out377738186843150252532180-267Time Out3845461868437630725326612-281Time Out402594186842846442680030-267Time Out4091081868435077527380712
psp_c_311 220220 2202200.15s104 4857345793002202200.16s104 485734579300 2202200.15s89 3357345842002202200.15s89 335734584200 2202200.15s104 4857345793002202200.16s104 485734579300
psp_c_312 431431 4314310.21s352 27211248122341204314310.22s339 2431124812233131 4314310.15s129 491124811969104314310.15s129 49112481196910 4314310.21s352 25011248122341104314310.22s352 2501124812234110
psp_c_313 328328 3283280.22s202 17510144117901503283280.22s203 1691014411786131 3283280.15s57 301014410888303283280.16s57 30101441088830 3283280.22s202 17510144117901503283280.22s202 1751014411790150
psp_c_314 294329 32432429.89s50413 5040173503156033646032432430.21s50645 505407350314383345083243243.44s5499 5487735027855380203243243.47s5623 5562735028630403563243242.03s3197 3181735025039235203243243.45s5634 558573502652940076
psp_c_315 274294 2942948.93s17093 170655913128311510802942948.93s16739 165645913129781464072942940.49s631 60359131288838102942940.51s673 61259131297440232942940.63s955 90559131278968402942940.75s1178 11125913133208643
psp_c_316 225225 2252250.17s82 3259305985002252250.17s82 325930598500 2252250.17s74 2459306010002252250.17s74 245930601000 2252250.17s82 3259305985002252250.17s82 325930598500
psp_c_317 465465 4654650.16s138 9712282130431804654650.15s138 971228213043180 4654650.13s84 431228212471004654650.13s84 43122821247100 4654650.16s138 9712282130431804654650.16s138 971228213043180
psp_c_318 354354 3543540.50s642 602138141949917003543540.48s654 58413814196081712 3543540.18s81 411381414437403543540.18s81 41138141443740 3543542.71s3701 36401381429969230803543540.56s650 57013814223112062
psp_c_319 386386 3863860.15s104 321265412694003863860.16s104 32126541269400 3863860.15s93 211265412701003863860.15s93 21126541270100 3863860.16s104 321265412694003863860.16s104 32126541269400
psp_c_320 274274 2742743.58s7839 7793911019000397902742743.88s8424 824091101923442886 2742740.21s148 1029110112654602742740.22s148 72911011265461 2742740.58s816 73991101597721402742740.81s1160 10129110184573153
psp_c_321 299299 2992990.25s246 207482764527502992990.26s279 20748276502751 2992990.18s76 37482758851702992990.17s76 3748275885170 2992990.25s246 207482764527502992990.25s246 20748276452750
psp_c_322 276276 2762760.19s152 10452665653002762760.18s152 1045266565300 2762760.16s64 1652665530002762760.15s64 165266553000 2762760.18s152 10452665653002762760.19s152 1045266565300
psp_c_323 324324 3243240.25s190 18110898153089903243240.25s199 18510898153871001 3243240.15s40 3110898126061703243240.15s40 311089812606170 3243240.25s190 18110898153089903243240.25s190 1811089815308990
psp_c_324 371371 3713710.17s123 451370813734003713710.17s123 45137081373400 3713710.16s107 291370813757003713710.16s107 29137081375700 3713710.16s123 451370813734003713710.16s123 45137081373400
psp_c_325 326326 3263260.17s215 13027762926003263260.17s215 1232776292601 3263260.15s104 1927762979203263260.14s104 192776297920 3263260.18s215 13027762926003263260.17s215 1302776292600
psp_c_326 304304 3043040.13s107 4363016317003043040.14s107 436301631700 3043040.14s83 1963016345003043040.13s83 196301634500 3043040.13s107 4363016317003043040.13s107 436301631700
psp_c_327 274274 2742740.21s175 132753284191102742740.21s175 13275328419111 2742740.17s82 3975327793002742740.17s82 397532779300 2742740.20s175 132753284191102742740.21s175 13275328419110
psp_c_328 248255 2552550.62s1253 120253831168548302552550.64s1288 120753831164249132552550.34s369 3185383981913702552550.34s379 2915383988013522552550.55s886 82053831147728602552550.51s758 6735383110942062
psp_c_329 291291 2912910.20s216 13825552806102912910.18s216 1232555280611 2912910.15s112 3425552754102912910.14s112 342555275410 2912910.18s216 13825552806102912910.19s216 1382555280610
psp_c_330 238238 2382380.17s95 5648205146002382380.17s95 564820514600 2382380.17s80 4148205375502382380.17s80 414820537550 2382380.17s95 5648205146002382380.17s95 564820514600
psp_c_331 311388 -401Time Out429666273891601193059680-400Time Out 4328782738915567530894811 -394Time Out497367273891649703304160-381Time Out4862712738923797832361612-392Time Out557335273891542853664220-381Time Out5501142738925709736604813
psp_c_332 317336 326326118.22s137879 13780624694137550951460326326119.96s138475 13812324694138133955221032632625.56s29922 298492469410290418979032632615.10s16814 165152469476217100907-369Time Out46319824694247866312235032632629.04s29903 2945824694111566180918
psp_c_333 332410 404404410.78s281452 281408279371902991963550404404387.47s266971 26663227937188454185445114044049.26s11474 1143027937125505753404044049.45s12045 1187427937119050776674044043.71s4891 48132793792944313904044045.91s7567 73972793710382348936
psp_c_334 384384 3843843.08s3703 36222305643209120803843843.31s3783 3546230564337312084 3843840.32s232 15123056257814503843840.58s640 46323056291912012 3843842.91s3145 3022230564760171903843842.32s2815 245023056466199175
psp_c_335 362426 41341346.77s63112 630582465111049644439041341344.67s60675 60366246511109364239884134133.67s3608 35542465159643181404134135.37s5636 53182465169284289964134133.03s3615 35172465159058185204134135.31s5525 5194246516974929656
psp_c_336 316393 -400Time Out453225229561358543278630-400Time Out 4520612295613625832679711 -374Time Out396804229561747972641290-375Time Out4662502295627421231092012-387Time Out429573229561748512865610-371Time Out4676192295628558230879112
psp_c_337 242296 -299Time Out36898517490822172606970-299Time Out 376141174908314426567611 -287Time Out369883174902216372480440-287Time Out3914151749031783325962512-335Time Out372057174902613552503090-287Time Out3883761749033540125964912
psp_c_338 363415 -403Time Out389742254542188922962930-403Time Out3994962545422248430293411403403264.72s188325 188263254541671461247950403403145.06s133619 133282254541646468667710403403193.73s161098 160989254541719101040510403403224.99s187588 1872082545417561012323211
psp_c_339 362429 -443Time Out432062299561880443099340-443Time Out 4304852995618899730812011 -415Time Out418439299562405722719050-412Time Out3844222995629157525172812-417Time Out415902299562889172728450-412Time Out3921842995628035825868812
psp_c_340 285322 -313Time Out504664171291758373515460-313Time Out495759171291742533434511131231217.03s16980 16921171296758310754031231212.76s13265 1305417129608108468731231212.46s13575 1348417129631728585031231220.43s21446 210761712967559133518
psp_c_341 405405 4054050.54s756 683890312228004054050.60s786 62289031226602 4054050.17s113 4089039136104054050.17s113 408903913610 4054050.34s392 284890310676104054050.34s392 28489031067610
psp_c_342 284284 2842840.68s640 60413656192133302842840.70s664 5811365619339352 2842840.19s72 361365614142102842840.21s72 36136561414210 2842840.75s774 71613656192264002842840.80s826 6051365619604432
psp_c_343 263263 2632630.31s239 166725485741502632630.32s239 13272548574151 2632630.24s115 4272547756102632630.24s115 427254775610 2632630.32s239 166725485741502632630.32s239 16672548574150
psp_c_344 316316 3163160.33s453 36786609991203163160.36s513 35586601007321 3163160.18s126 4086609250303163160.18s126 408660925030 3163160.35s463 2948660106781003163160.35s463 294866010678100
psp_c_345 282282 2822821.66s1816 1763159742665780402822821.70s1872 170615974267758103 2822820.20s83 301597416705302822820.21s83 30159741670530 2822820.43s391 30615974196141502822820.43s391 3051597419614151
psp_c_346 411446 446446118.80s91148 911302017987449718610446446114.31s88746 88623201798718370001944644611.25s11000 1098220179748827869044644620.57s21948 2183520179795901539584464468.43s8729 870020179720556504044644621.41s22505 223342017980142159038
psp_c_347 280280 2802800.43s461 4149271128003402802800.45s484 377927112831342 2802800.19s95 48927110102602802800.18s95 4892711010260 2802800.45s500 4079271128043802802800.49s549 392927113086411
psp_c_348 389389 3893890.55s786 7131543318458103893890.56s809 649154331848712 3893890.18s104 311543315665003893890.19s104 31154331566500 3893890.33s375 2751543317065003893890.32s375 275154331706500
psp_c_349 401451 444444340.68s232693 232656264871401091764410444444317.65s227934 227690264871402161714011044444437.51s43045 430082648711616030431044444445.35s55038 548052648712629637699944444417.53s23698 236432648710512516710044444452.08s63046 6272726487121999426649
psp_c_350 314314 3143140.18s151 9396049870103143140.19s151 939604987010 3143140.17s88 3096049767003143140.17s88 309604976700 3143140.19s151 9396049870103143140.20s151 939604987010
psp_c_351 379379 3793790.17s81 3986188680003793790.18s81 398618868000 3793790.18s86 4486188717203793790.18s86 448618871720 3793790.17s81 3986188680003793790.17s81 398618868000
psp_c_352 345345 3453450.32s377 299960710454203453450.34s426 27696071052421 3453450.19s123 45960710019303453450.19s123 4596071001930 3453450.33s377 246960710454203453450.32s377 24696071045420
psp_c_353 215215 2152150.21s115 85951210146802152150.20s115 8595121014680 2152150.18s65 3595129797102152150.18s65 359512979710 2152150.21s115 85951210146802152150.20s115 8595121014680
psp_c_354 293293 2932930.24s265 17437594021002932930.24s265 1243759402101 2932930.18s113 2237593939002932930.17s113 223759393900 2932930.24s265 17437594021002932930.25s265 1743759402100
psp_c_355 322322 3223220.17s92 3595409565003223220.17s92 359540956500 3223220.16s81 2495409581003223220.16s81 249540958100 3223220.18s92 3595409565003223220.17s92 359540956500
psp_c_356 251251 2512510.25s200 16674418262202512510.26s210 1637441830521 2512510.17s68 3474417697302512510.18s68 347441769730 2512510.25s200 16674418262202512510.25s200 1667441826220
psp_c_357 267267 2672670.21s188 11349855150002672670.21s188 1134985515000 2672670.18s107 3249855150002672670.18s107 324985515000 2672670.22s188 11349855150002672670.22s188 1134985515000
psp_c_358 201201 2012010.18s90 4133423385002012010.19s90 413342338500 2012010.17s78 2933423407002012010.18s78 293342340700 2012010.18s90 4133423385002012010.19s90 413342338500
psp_c_359 386386 3863860.32s331 26711512126541003863860.33s355 2591151212696101 3863860.18s80 161151211727003863860.17s80 16115121172700 3863860.32s331 24711512126541003863860.32s331 2471151212654100
psp_c_360 655655 6556550.11s94 1883888388006556550.11s94 188388838800 6556550.10s89 1383888393006556550.11s89 138388839300 6556550.11s94 1883888388006556550.12s94 188388838800
psp_c_361 441523 51351326.16s25778 257523401917839218656051351329.24s27976 27858340191799982027775135135.18s4878 485234019129994299405135137.12s6151 601834019147521403865135136.58s6079 604534019148146392505135137.53s6285 61493401915122441226
psp_c_362 529529 5295290.29s949 87011201170612805295290.30s969 8421120117107232 5295290.23s603 52411201146771505295290.20s568 3241120114077102 5295290.30s1057 94411201159391805295290.25s712 4341120116143132
psp_c_363 481566 5665667.86s5425 539430942172076427305665667.65s5125 502330942172512406155665662.17s1989 195830942104035120405665661.91s1862 175230942102221100545665661.77s1522 146930942102651106605665663.02s2922 27813094211457517795
psp_c_364 341372 3603602.29s6512 64601229327948404903603602.33s6516 63141229328310400953603600.42s828 776122932148815503603600.36s649 522122932118916533603600.39s741 656122932070926603603600.45s848 68012293219503482
psp_c_365 423445 4454458.03s13561 134992393591457655904454458.80s14869 145632393591607731764454450.76s1622 1560239354527229604454450.83s1628 1317239354910027644454450.65s933 837239354935534104454450.88s1814 137723935550874314
psp_c_366 411419 4194190.33s593 547131271926723704194190.33s627 528131271931022824194190.29s538 49213127190725804194190.25s396 21013127169682224194190.28s415 338131271923011704194190.27s415 32913127192041131
psp_c_367 319322 3223221.33s3260 32051720239850104403223221.37s3372 31811720240366106443223220.32s682 62717202222407403223220.41s836 570172022750815633223220.59s1485 1400172023109418903223220.65s1698 148517202320702094
psp_c_368 346346 3463460.24s517 45910605129493003463460.25s574 4481060513145302 3463460.16s106 481060511091203463460.15s106 48106051109120 3463460.33s876 77810605143153603463460.28s621 4451060513585312
psp_c_369 389390 3903900.34s991 909140671895421003903900.37s1110 871140671900520433903900.21s448 36614067170452303903900.28s782 33414067179383923903900.31s782 623140671931812103903900.30s774 54314067188081002
psp_c_370 378378 3783780.52s1814 173214631222665103783780.55s1913 17121463122487483 3783780.21s496 4141463116729203783780.23s496 68146311672921 3783780.49s1937 177614631210461803783780.60s2310 16411463121745234
psp_c_371 213213 2132130.13s102 4344004442002132130.13s102 434400444200 2132130.14s91 3244004475002132130.12s91 324400447500 2132130.13s102 4344004442002132130.13s102 434400444200
psp_c_372 368368 3683680.15s105 711137011889903683680.17s105 71113701188990 3683680.14s62 281137011760003683680.15s62 28113701176000 3683680.15s105 711137011889903683680.16s105 71113701188990
psp_c_373 553553 5535530.11s52 221232112492005535530.11s52 22123211249200 5535530.12s51 211232112588105535530.12s51 21123211258810 5535530.11s52 221232112492005535530.12s52 22123211249200
psp_c_374 316316 3163160.13s93 3884168459003163160.14s93 388416845900 3163160.14s95 4084168487103163160.13s95 408416848710 3163160.13s93 3884168459003163160.13s93 388416845900
psp_c_375 327327 3273270.26s370 33379361048211303273270.26s385 3397936105411181 3273270.15s90 5379368553103273270.16s90 537936855310 3273270.28s429 37279361128412203273270.28s429 3537936112841221
psp_c_376 307307 3073070.14s127 5755905629003073070.15s127 575590562900 3073070.12s110 4055905692003073070.14s110 405590569200 3073070.15s127 5755905629003073070.15s127 575590562900
psp_c_377 365365 3653650.14s208 14876698136003653650.15s208 1247669813601 3653650.11s93 3376697852003653650.12s93 337669785200 3653650.14s208 14876698136003653650.14s208 1487669813600
psp_c_378 259259 2592590.13s100 4855805738102592590.16s100 485580573810 2592590.13s94 4255805760202592590.13s94 425580576020 2592590.13s100 4855805738102592590.14s100 485580573810
psp_c_379 371371 3713710.12s124 4561426172003713710.11s124 456142617200 3713710.12s110 3161426203003713710.13s110 316142620300 3713710.11s124 4561426172003713710.11s124 456142617200
psp_c_380 264264 2642640.14s160 11367897246002642640.14s160 1136789724600 2642640.13s74 2767897016002642640.12s74 276789701600 2642640.14s160 11367897246002642640.14s160 1136789724600
psp_c_381 254254 2542540.12s91 4053785413002542540.12s91 405378541300 2542540.12s72 2153785459002542540.12s72 215378545900 2542540.13s91 4053785413002542540.12s91 405378541300
psp_c_382 273273 2732730.12s28 1225592659002732730.13s28 122559265900 2732730.12s28 1225592664002732730.12s28 122559266400 2732730.13s28 1225592659002732730.12s28 122559265900
psp_c_383 288288 2882880.12s84 3545294571002882880.13s84 354529457100 2882880.12s72 2345294574002882880.12s72 234529457400 2882880.12s84 3545294571002882880.12s84 354529457100
psp_c_384 338338 3383380.13s101 3785738604003383380.13s101 378573860400 3383380.13s91 2785738634003383380.12s91 278573863400 3383380.12s101 3785738604003383380.11s101 378573860400
psp_c_385 317317 3173170.12s69 3365166621003173170.12s69 336516662100 3173170.12s59 2365166623003173170.13s59 236516662300 3173170.13s69 3365166621003173170.12s69 336516662100
psp_c_386 418418 4184180.12s99 3265926610004184180.12s99 326592661000 4184180.11s79 1265926639004184180.12s79 126592663900 4184180.12s99 3265926610004184180.13s99 326592661000
psp_c_387 376376 3763760.11s67 2261846234003763760.11s67 226184623400 3763760.11s66 2161846253003763760.11s66 216184625300 3763760.11s67 2261846234003763760.12s67 226184623400
psp_c_388 279279 2792790.15s129 571020110271002792790.16s129 57102011027100 2792790.15s102 301020110287002792790.15s102 30102011028700 2792790.15s129 571020110271002792790.15s129 57102011027100
psp_c_389 426426 4264260.16s123 451295313012004264260.14s123 45129531301200 4264260.15s97 191295313040004264260.15s97 19129531304000 4264260.15s123 451295313012004264260.14s123 45129531301200
psp_c_390 401401 4014010.12s85 3345674592004014010.11s85 334567459200 4014010.10s79 2745674633004014010.11s79 274567463300 4014010.11s85 3345674592004014010.12s85 334567459200
psp_c_391 250323 31431434.61s48508 48442212759295132623031431434.33s48497 48112212759341332313831431412.64s18521 18455212751119111041603143146.78s11452 111522127584880655573143147.52s12750 126322127580273813803143147.96s12238 12025212758284873757
psp_c_392 287322 -312Time Out571112130601247123914360-312Time Out5638381306012369238590412311311157.95s197486 19740913060139113128962031131130.72s47234 46847130607553229935931131145.18s79977 79852130608295151806031131142.48s66674 661521306092814426899
psp_c_393 331337 3313314.95s7864 78032003552679361503313315.09s8120 78972003553017367463313310.37s316 255200352450412503313311.08s1503 1276200353316137743313311.25s1806 1707200353160647603313311.13s1525 132720035325854404
psp_c_394 466469 4694691.56s3047 29632217841117100504694691.62s3253 2944221784152298544694691.03s1748 1664221783329725604694690.50s893 46322178297335734694690.86s1480 1338221783362711304694690.70s1254 83322178325051003
psp_c_395 393393 3933931.71s3245 3155250554453517503933931.73s3417 306525055448761744 3933930.48s591 50125055306967803933930.60s826 5892505531431963 3933931.56s2451 2306250554104145003933931.08s1942 140325055379842834
psp_c_396 unsat unsat0.67s606 5680000unsat0.68s606 5680000 unsat0.66s606 5680000unsat0.67s606 5680000 unsat0.67s606 5680000unsat0.67s606 5680000
psp_c_397 402588 524524101.08s61370 613123263022684738454052452493.65s58688 584793263022769436127852452420.24s11640 11582326302416887993052452422.58s12349 12117326302767688428752452415.42s8991 890932630213585631905245248.76s5772 55723263017006539256
psp_c_398 303303 3033031.88s3878 38261739340249146903033031.92s3949 3797173934023014724 3033030.20s108 561739318235203033030.20s108 56173931823520 3033031.08s2005 1928173933140132203033030.94s1705 146217393314792624
psp_c_399 224315 -306Time Out41361918247888862959110-306Time Out406794182478968029226111290290143.70s165853 16580018247193035111042029029072.91s107260 10680718247158646711021029029097.69s127111 12700918247162611852720290290132.16s162557 1620321824718118310831011
psp_c_400 355420 41141114.41s20329 20269229769097811662041141114.89s20054 1982022976915201139874114112.21s3330 32702297667592173004114112.39s3650 33332297669350187554114113.73s5637 55342297680091332404114114.97s7383 7119229768734341996
psp_c_401 327327 3273270.15s102 4469226993103273270.15s102 446922699310 3273270.14s91 3369227010003273270.15s91 336922701000 3273270.16s102 4469226993103273270.15s102 446922699310
psp_c_402 284284 2842840.21s262 21666028014102842840.22s267 2076602801611 2842840.15s86 4066027081202842840.15s86 406602708120 2842840.21s262 21666028014102842840.22s262 2166602801410
psp_c_403 491491 4914910.12s105 3290289032004914910.12s105 329028903200 4914910.12s95 2290289044004914910.12s95 229028904400 4914910.12s105 3290289032004914910.13s105 329028903200
psp_c_404 326326 3263260.17s168 9864996705003263260.17s168 986499670500 3263260.15s99 2964996658003263260.14s99 296499665800 3263260.17s168 9864996705003263260.16s168 986499670500
psp_c_405 304304 3043040.16s80 4571437267003043040.15s80 457143726700 3043040.13s56 2171437320003043040.15s56 217143732000 3043040.14s80 4571437267003043040.15s80 457143726700
psp_c_406 356362 3623620.22s329 253511057912503623620.24s375 234511058422413623620.27s389 313511068641603623620.27s416 286511069461323623620.25s329 242511057912503623620.23s329 24251105791250
psp_c_407 324324 3243241.17s2282 2212110791604882603243241.21s2392 220011079162058304 3243240.19s132 621107911680603243240.19s132 62110791168060 3243240.59s932 806110791605225803243240.50s856 6191107914941722
psp_c_408 271271 2712710.20s168 11866987061002712710.19s168 1186698706100 2712710.16s82 3266986918002712710.16s82 326698691800 2712710.19s168 11866987061002712710.18s168 1186698706100
psp_c_409 393393 3933930.17s111 851064211923203933930.18s111 85106421192320 3933930.16s44 181064211054103933930.14s44 18106421105410 3933930.19s111 851064211923203933930.20s111 85106421192320
psp_c_410 487487 4874870.14s62 421368614338004874870.15s62 42136861433800 4874870.13s33 131368613882004874870.13s33 13136861388200 4874870.15s62 421368614338004874870.14s62 42136861433800
psp_c_411 325325 3253250.14s121 4552095224003253250.15s121 455209522400 3253250.14s99 2352095306003253250.15s99 235209530600 3253250.15s121 4552095224003253250.14s121 455209522400
psp_c_412 321321 3213210.16s134 5074187433003213210.16s134 507418743300 3213210.14s116 3274187480003213210.15s116 327418748000 3213210.15s134 5074187433003213210.16s134 507418743300
psp_c_413 333344 3443440.39s501 47457411098324703443440.37s476 42857411090221723443440.36s374 34757411056313003443440.46s606 54757411151126133443440.43s563 51757411156523903443440.43s541 4685741114072242
psp_c_414 352352 3523520.13s83 2874587493003523520.14s83 287458749300 3523520.12s69 1474587522003523520.14s69 147458752200 3523520.13s83 2874587493003523520.14s83 287458749300
psp_c_415 185185 1851850.16s105 4823272390001851850.16s105 482327239000 1851850.16s82 2523272438001851850.16s82 252327243800 1851850.16s105 4823272390001851850.15s105 482327239000
psp_c_416 458458 4584580.13s132 4288268847004584580.13s132 428826884700 4584580.12s106 1688268867004584580.13s106 168826886700 4584580.13s132 4288268847004584580.13s132 428826884700
psp_c_417 307307 3073070.14s91 4160416090003073070.16s91 416041609000 3073070.14s72 2260416170003073070.15s72 226041617000 3073070.15s91 4160416090003073070.16s91 416041609000
psp_c_418 365365 3653650.15s101 7284179187603653650.15s101 728417918760 3653650.13s58 2984178875403653650.13s58 298417887540 3653650.15s101 7284179187603653650.15s101 728417918760
psp_c_419 298298 2982980.15s52 2737143938002982980.15s52 273714393800 2982980.15s39 1437144099102982980.15s39 143714409910 2982980.14s52 2737143938002982980.14s52 273714393800
psp_c_420 422422 4224220.14s34 212038221586004224220.14s34 21203822158600 4224220.16s24 112038220802004224220.15s24 11203822080200 4224220.16s34 212038221586004224220.16s34 21203822158600
psp_c_421 396469 45845829.10s27423 273792908313644318949045845829.57s28735 28548290831360381959874584588.64s9122 9078290831049645024045845810.04s9843 961729083112933606574584587.04s6951 688529083101663439204584588.47s8368 81522908311169750466
psp_c_422 444794 77677663.54s14737 147056046565519010885077677665.06s14961 148306046565299510993677677650.55s16734 167026046543113111575077677634.83s11707 11432604654013358109777677634.66s12397 12335604653933828652077677633.42s12705 124436046540890687817
psp_c_423 359401 40140111.28s14155 1408521852550038230040140111.69s14549 141782185255370818664014011.11s1282 1212218523264355304014011.15s1366 1150218523280251944014011.19s1487 1357218523435261204014011.54s1854 155421852367776244
psp_c_424 352394 -390Time Out436360182281204293030350-390Time Out4298321822811969629878711382382468.83s377161 37709718228249802251208038238289.26s85362 8497818228131363564311038238297.09s97670 975651822811538464266038238274.41s81793 81212182281143225361410
psp_c_425 unsat unsat0.83s626 5660000unsat0.84s626 5660000 unsat0.83s626 5660000unsat0.83s626 5660000 unsat0.83s626 5660000unsat0.83s626 5660000
psp_c_426 283350 -347Time Out456172249201657223195760-347Time Out4617212492016543732273811333333302.85s302662 302605249203556042021060333333440.96s339725 3391532492032206522374512333333460.13s380866 380761249202851402551340333333420.41s326719 3261982492029904121657712
psp_c_427 305314 30830821.33s26414 26329145874766117747030830821.76s27232 2675214587481771807273083084.55s5175 50901458733660287603083082.07s2479 21901458728188111553083084.60s5740 55991458739779258203083082.71s3853 3510145873243814735
psp_c_428 514831 83183166.41s7359 7341589236326026707083183166.44s7477 7433589236249066737583183157.32s18346 183285892346500712742083183136.80s12600 12339589234305098541783183130.62s10684 10656589233887257549083183142.63s13213 129845892345140391607
psp_c_429 529529 5295290.89s1005 94820147280755705295290.91s1033 8622014728158593 5295290.16s80 232014720638005295290.15s80 23201472063800 5295290.70s808 73220147263484405295290.54s632 4392014725165302
psp_c_430 293361 -358Time Out426003189701328842937970-358Time Out4233431897013364429230211345345108.07s162748 162674189701235481064720345345298.05s320991 3205881897014822121101812345345435.48s406813 406680189701463102677770345345237.22s264299 2637511897015474317288711
psp_c_431 416416 4164160.30s295 2211039611083004164160.32s345 204103961114401 4164160.18s105 311039610735104164160.18s105 31103961073510 4164160.30s295 2211039611083004164160.29s295 221103961108300
psp_c_432 349349 3493490.87s1223 115214336183061503493490.90s1294 10791433618407163 3493490.19s104 331433614668003493490.19s104 33143361466800 3493490.58s748 6181433616436203493490.58s748 309143361643621
psp_c_433 293372 369369351.58s255515 255493180111158002031340369369350.51s254667 254493180111157502029071036936917.18s25904 25882180118561518967036936917.66s16992 1682918011947281268173693699.68s11962 1192818011736458788036936922.35s23463 232691801186968171068
psp_c_434 362362 3623620.20s182 11262246464003623620.19s182 1126224646400 3623620.15s92 2262246391003623620.16s92 226224639100 3623620.20s182 11262246464003623620.21s182 1126224646400
psp_c_435 353361 35935915.20s18404 18371270535972811668035935915.03s17894 1774627053599451140773593594.49s3956 39232705360278287603593596.27s6050 594227053586104280635935910.16s13397 133442705373517948803593593.53s3277 3076270535624620465
psp_c_436 287287 2872870.74s829 76911999164535702872870.75s851 7191199916518582 2872871.22s1319 1259119992308690302872874.20s4205 4033119993214223295 2872874.24s4238 41531199929168259302872872.88s3006 2761119992796215345
psp_c_437 360360 3603600.18s91 391044310468003603600.17s91 39104431046800 3603600.16s75 231044310521003603600.17s75 23104431052100 3603600.17s91 391044310468003603600.17s91 39104431046800
psp_c_438 267267 2672670.29s190 155737492064002672670.30s207 15473749283421 2672670.20s99 64737485022502672670.20s99 6473748502250 2672670.29s190 155737492064002672670.30s190 15573749206400
psp_c_439 377377 3773770.44s439 3801151514293403773770.44s464 370115151433742 3773770.18s91 321151512090303773770.19s91 32115151209030 3773770.39s374 2931151514272903773770.39s374 293115151427290
psp_c_440 257260 258258102.63s135497 135453110945760680569025825888.81s120909 12067211094568797222992582585.82s8475 84311109433298529002582585.52s7061 68621109436718435962582588.15s11060 109751109444678719502582586.00s8293 8154110943873254376
psp_c_441 281281 2812810.24s195 159867110022302812810.24s205 15686711006641 2812810.16s62 2686719079202812810.17s62 268671907920 2812810.24s195 159867110022302812810.23s195 15986711002230
psp_c_442 325325 3253251.08s1258 1195106471384940303253251.08s1309 117810647139753993 3253250.35s264 2011064711052203253250.32s264 201106471105220 3253250.90s1077 978106471363215903253250.88s1106 85610647137871663
psp_c_443 579579 5795790.14s96 291456214599005795790.14s96 29145621459900 5795790.14s86 191456214611005795790.15s86 19145621461100 5795790.14s96 291456214599005795790.13s96 29145621459900
psp_c_444 243243 2432430.19s137 8743094519102432430.19s137 874309451910 2432430.17s82 3243094544002432430.17s82 324309454400 2432430.19s137 8743094519102432430.20s137 874309451910
psp_c_445 306306 3063060.20s149 9727013098103063060.20s149 972701309810 3063060.16s78 2627012920003063060.16s78 262701292000 3063060.20s149 9727013098103063060.21s149 972701309810
psp_c_446 354354 3543540.19s144 8377578053003543540.20s144 837757805300 3543540.16s85 2477578127003543540.17s85 247757812700 3543540.18s144 8377578053003543540.19s144 837757805300
psp_c_447 416416 4164160.15s116 4056985715004164160.15s116 405698571500 4164160.13s97 2156985724004164160.13s97 215698572400 4164160.17s116 4056985715004164160.14s116 405698571500
psp_c_448 416416 4164160.17s112 371036610383004164160.17s112 37103661038300 4164160.16s89 141036610408004164160.17s89 14103661040800 4164160.17s112 371036610383004164160.17s112 37103661038300
psp_c_449 417417 4174170.22s293 20580298467004174170.24s325 1688029853301 4174170.16s119 3180298255004174170.14s119 318029825500 4174170.24s293 20580298467004174170.23s293 2058029846700
psp_c_450 362362 3623620.40s305 289145252058914303623620.38s308 28914525206171431 3623620.19s62 4614525157311903623620.20s62 461452515731190 3623620.88s791 763145252407551403623620.52s454 40514525232872261
psp_c_451 354365 3653650.43s774 709148072345224103653650.43s898 764148072372925823653650.26s275 21014807204966503653650.25s276 14614807203555913653650.32s542 440148072297914203653650.33s550 39914807230411371
psp_c_452 395420 4194191.67s2706 26601740147873183604194191.63s2764 26511740148129178444194190.62s1054 1008174013816338404194190.69s1304 1133174014134741444194190.65s1113 1048174014188145304194190.76s1349 116017401446795213
psp_c_453 467659 65965912.85s2822 2811407063021222370065965912.57s2805 277640706296732234346596595.46s3281 327040706160097226006596595.45s3273 314540706162950217456596597.21s4222 419940706187632288506596597.82s4463 43394070618382630235
psp_c_454 469498 4934931.73s4095 40082293355627182704934931.84s4511 41112293356742189854934931.00s2474 2387229334624155504934930.84s1845 1325229334888038944934930.78s1527 1358229334447546904934930.65s1047 80422933439613863
psp_c_455 300304 3043040.59s1194 1136111882083149803043040.61s1278 1170111882088252733043040.29s426 36811188152673503043040.30s477 28211188154104123043040.39s803 689111881799317103043040.50s1210 93011188201632273
psp_c_456 598609 6096090.26s542 487125391819412006096090.28s615 472125391842111926096090.26s519 46412539184038006096090.27s606 35812539190998826096090.28s575 48612539188739806096090.26s530 44012539189591011
psp_c_457 423430 4284280.67s1955 1886150592959749904284280.77s2348 2170150593017061044284280.29s413 34415059210106004284280.31s490 33015059218384924284280.34s686 56815059226747104284280.36s688 4881505923960942
psp_c_458 401402 4024020.58s1676 160015820276486704024020.61s1791 156315820279256834024020.24s469 39315820187852504024020.27s521 30915820187371724024020.42s1259 113115820216992904024020.36s878 5551582021640252
psp_c_459 352499 4474475.89s6244 62272224384950516704474476.33s6461 63902224384069526254474474.25s3781 376422243120517263204474471.50s1329 1264222437720089144474471.26s1360 13292224367833103204474472.08s1995 1931222438674614324
psp_c_460 unsat unsat0.47s1080 10020000unsat0.48s1080 10020000 unsat0.48s1080 10020000unsat0.48s1080 10020000 unsat0.47s1080 10020000unsat0.48s1080 10020000
psp_c_461 418418 4184180.18s382 33461877675904184180.17s390 3116187769281 4184180.12s80 3261876496104184180.11s80 326187649610 4184180.18s379 298618779131004184180.18s379 29861877913100
psp_c_462 602602 6026020.09s102 251103111040006026020.10s102 25110311104000 6026020.10s91 141103111058006026020.09s91 14110311105800 6026020.10s102 251103111040006026020.10s102 25110311104000
psp_c_463 457457 4574570.12s125 7975637816004574570.12s125 797563781600 4574570.12s71 2575637707004574570.11s71 257563770700 4574570.12s125 7975637816004574570.12s125 797563781600
psp_c_464 367367 3673670.14s90 7075408247003673670.13s90 707540824700 3673670.13s47 2775407992203673670.12s47 277540799220 3673670.13s90 7075408247003673670.14s90 707540824700
psp_c_465 316316 3163160.15s183 12968137450503163160.16s183 1246813745051 3163160.16s112 5868137061203163160.15s112 586813706120 3163160.15s183 12968137450503163160.16s183 1296813745050
psp_c_466 269269 2692690.12s66 2657045741002692690.12s66 265704574100 2692690.12s60 2057045749002692690.13s60 205704574900 2692690.13s66 2657045741002692690.12s66 265704574100
psp_c_467 423423 4234230.15s193 12991669585704234230.14s193 1299166958570 4234230.13s95 3191669349004234230.13s95 319166934900 4234230.14s193 12991669585704234230.15s193 1299166958570
psp_c_468 438438 4384380.12s129 4762426274004384380.13s129 476242627400 4384380.12s112 3062426308004384380.12s112 306242630800 4384380.13s129 4762426274004384380.12s129 476242627400
psp_c_469 365365 3653650.15s115 8312601145261703653650.15s115 831260114526170 3653650.14s49 171260112938003653650.14s49 17126011293800 3653650.15s115 8312601145261703653650.15s115 831260114526170
psp_c_470 313313 3133130.15s100 4956515817503133130.14s100 495651581750 3133130.12s83 3256515772003133130.14s83 325651577200 3133130.13s100 4956515817503133130.14s100 495651581750
psp_c_471 275275 2752750.13s123 5338033862002752750.15s123 533803386200 2752750.13s112 4238033980002752750.13s112 423803398000 2752750.13s123 5338033862002752750.13s123 533803386200
psp_c_472 395395 3953950.12s113 6247264821003953950.12s113 624726482100 3953950.11s75 2447264864003953950.11s75 244726486400 3953950.11s113 6247264821003953950.13s113 624726482100
psp_c_473 346346 3463460.14s352 26739304385103463460.14s394 2333930445701 3463460.11s127 4239304105103463460.12s127 423930410510 3463460.15s352 24539304385103463460.15s352 2453930438510
psp_c_474 368368 3683680.11s55 2526972762003683680.12s55 252697276200 3683680.12s62 3226972864003683680.12s62 322697286400 3683680.11s55 2526972762003683680.11s55 252697276200
psp_c_475 252252 2522520.15s58 2833213417002522520.15s58 283321341700 2522520.15s49 1933213470002522520.14s49 193321347000 2522520.15s58 2833213417002522520.14s58 283321341700
psp_c_476 292292 2922920.16s172 10333303558002922920.16s172 1033330355800 2922920.15s92 2333303620102922920.15s92 233330362010 2922920.17s172 10333303558002922920.17s172 1033330355800
psp_c_477 296296 2962960.13s73 3452225266002962960.14s73 345222526600 2962960.13s72 3352225277002962960.15s72 335222527700 2962960.14s73 3452225266002962960.15s73 345222526600
psp_c_478 415415 4154150.12s117 4970627073004154150.12s117 497062707300 4154150.12s104 3670627105004154150.12s104 367062710500 4154150.12s117 4970627073004154150.12s117 497062707300
psp_c_479 303303 3033030.14s116 6756255837103033030.15s116 675625583710 3033030.16s74 2556255856003033030.14s74 255625585600 3033030.13s116 6756255837103033030.15s116 675625583710
psp_c_480 427427 4274270.11s118 4066476666004274270.12s118 406647666600 4274270.12s103 2566476687004274270.11s103 256647668700 4274270.11s118 4066476666004274270.12s118 406647666600
psp_c_481 361433 4204208.95s17123 1705914956399911163104204209.11s17574 1722914956404341171474204202.06s4910 48461495636637295404204201.55s2886 26751495635293165254204201.77s4074 39601495636995255704204201.22s2644 2374149563527315964
psp_c_482 651905 90590516.12s3203 3182531683979462771090590516.12s3109 3029531684142712681490590517.27s6737 6716531682683944551090590525.50s8172 8007531683049075399690590528.25s8973 8937531683077476117090590519.88s7724 74515316830635751766
psp_c_483 363426 40240259.00s98663 985802063514485059536040240263.89s101773 101249206351490396111394024026.25s9928 98452063580610440804024025.14s7988 76512063580998425164024024.73s8142 80022063568474359404024027.32s10824 10393206359725950107
psp_c_484 532574 5745741.69s3037 29832482245252180505745741.79s3339 31602482244801185145745740.58s684 630248223917025505745740.61s794 680248223928127135745740.79s1108 1021248224615049305745740.82s1096 92424822465804943
psp_c_485 561561 5615611.22s2264 2186188083030625605615611.27s2323 204618808304742564 5615610.20s135 571880819461605615610.18s135 57188081946160 5615610.31s447 33218808217743705615610.30s447 3211880821774371
psp_c_486 390586 568568154.26s94491 9446030986268437685840568568180.92s104074 1038883098626835175525956856820.12s14043 14012309862355579569056856821.76s12903 12766309862423178896756856815.16s9976 9926309862035146932056856818.69s11640 114453098623466080777
psp_c_487 581734 73473471.89s17403 173674349544708215117073473473.44s17734 176144349545014415248773473415.72s9302 9266434952552976156073473411.47s7330 7149434952118294803673473415.58s8787 8731434952601815833073473414.95s8519 82154349525290854816
psp_c_488 462485 4834832.71s5719 56611577325427344004834832.75s5801 55481577325506333254834830.46s640 582157732713426404834830.66s1082 926157733094035434834830.47s717 613157732335219404834830.60s973 76715773243752353
psp_c_489 351397 382382249.25s312415 312341263241801492073690382382275.76s320184 31959626324183590212447113823829.88s18438 1836426324795281130603823826.55s11373 1110726324805426570738238245.32s68599 68448263241240044360403823827.82s12652 12256263248974563907
psp_c_490 456462 4624620.63s1200 1133135642085411904624620.64s1246 1080135642093312034624620.22s269 20213564154041704624620.22s289 20313564154451824624620.41s683 59713564187825804624620.44s755 6241356419107782
psp_c_491 563563 5635630.14s144 10484078962005635630.14s144 1048407896200 5635630.11s64 2484078565005635630.12s64 248407856500 5635630.14s144 10484078962005635630.13s144 1048407896200
psp_c_492 635635 6356350.12s171 9396659810006356350.12s171 939665981000 6356350.11s100 2296659814006356350.11s100 229665981400 6356350.13s171 9396659810006356350.13s171 939665981000
psp_c_493 485503 5035030.72s1039 1014124091887760905035030.71s1054 1009124091898560835035030.21s212 18712409164165305035030.22s214 12412409163695415035030.40s473 436124091791916905035030.41s502 45612409181101791
psp_c_494 462462 4624620.26s588 5019005107072804624620.28s643 451900510806222 4624620.25s555 4689005106731204624620.25s569 34790051068872 4624620.25s529 3779005111182304624620.25s529 307900511118221
psp_c_495 350353 3533530.20s168 1337823102174703533530.20s168 1277823102174713533530.16s110 75782390831303533530.17s114 7378239089913533530.20s168 1337823102174703533530.20s168 133782310217470
psp_c_496 360360 3603600.15s79 2960986140003603600.14s79 296098614000 3603600.14s69 1960986151003603600.14s69 196098615100 3603600.14s79 2960986140003603600.15s79 296098614000
psp_c_497 275333 3233239.52s17273 17249191705936815262032332310.22s17957 1788719170593371584173233233.77s5097 50731917058686381703233232.58s3596 34541917053786254653233238.73s13616 135811917068921986203233234.88s7083 6921191706256151836
psp_c_498 307307 3073070.31s497 42367748417803073070.32s529 3656774847682 3073070.18s126 5267747116203073070.18s126 526774711620 3073070.30s451 31467748676603073070.30s451 3056774867661
psp_c_499 364364 3643640.18s212 15464426966003643640.19s212 1236442696601 3643640.15s98 4064426695003643640.16s98 406442669500 3643640.19s212 15464426966003643640.19s212 1546442696600
psp_c_500 261261 2612610.27s413 35574589455802612610.29s473 3717458971282 2612610.16s82 2474587737002612610.16s82 247458773700 2612610.26s391 28074589381302612610.26s391 2807458938130
psp_c_501 276276 2762760.20s256 19529423596002762760.20s261 1892942360701 2762760.15s93 3229423149002762760.15s93 322942314900 2762760.21s256 19529423596002762760.20s256 1952942359600
psp_c_502 396396 3963960.13s78 4750075185103963960.13s78 475007518510 3963960.13s60 2950075208103963960.13s60 295007520810 3963960.14s78 4750075185103963960.13s78 475007518510
psp_c_503 286286 2862864.61s9855 9809682814300530502862864.57s9799 960968281450153186 2862860.19s114 68682875171302862860.19s114 6868287517130 2862860.51s786 71968281021015002862860.61s995 8116828114522473
psp_c_504 378378 3783780.13s68 3138513904003783780.13s68 313851390400 3783780.13s59 2238513969003783780.12s59 223851396900 3783780.12s68 3138513904003783780.13s68 313851390400
psp_c_505 417417 4174170.17s97 4970067326504174170.17s97 497006732650 4174170.16s71 2370067264004174170.16s71 237006726400 4174170.16s97 4970067326504174170.18s97 497006732650
psp_c_506 483483 4834830.12s124 3774707475004834830.12s124 377470747500 4834830.12s113 2674707495004834830.12s113 267470749500 4834830.12s124 3774707475004834830.11s124 377470747500
psp_c_507 505505 5055050.12s98 3662786289005055050.12s98 366278628900 5055050.12s90 2862786304005055050.11s90 286278630400 5055050.11s98 3662786289005055050.12s98 366278628900
psp_c_508 356356 3563560.14s