| Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-fiber.opb |
| MD5SUM | cc38717029ffa5880438a73ef1ac0ab0 |
| Bench Category | optimization, medium integers (OPTMEDINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 212205129 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 1254 |
| Biggest coefficient in the objective function | 72966962 |
| Number of bits for the biggest coefficient in the objective function | 27 |
| Sum of the numbers in the objective function | 4807778524 |
| Number of bits of the sum of numbers in the objective function | 33 |
| Biggest number in a constraint | 72966962 |
| Number of bits of the biggest number in a constraint | 27 |
| Biggest sum of numbers in a constraint | 4807778524 |
| Number of bits of the biggest sum of numbers | 33 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1238.47 |
| Number of variables | 2134 |
| Total number of constraints | 1617 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 1290 |
| Number of constraints which are nor clauses,nor cardinality constraints | 327 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 51 |
LAUNCH ON wulflinc28 THE 2005-09-20 04:16:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3354 boxname=wulflinc28 idbench=1010 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: cc38717029ffa5880438a73ef1ac0ab0 /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-fiber.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-fiber.opb IDLAUNCH: 3354 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 887500 kB Buffers: 25772 kB Cached: 92364 kB SwapCached: 660 kB Active: 32260 kB Inactive: 88404 kB HighTotal: 131008 kB HighFree: 35168 kB LowTotal: 903652 kB LowFree: 852332 kB SwapTotal: 2097640 kB SwapFree: 2096408 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5820 kB Slab: 20748 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 04:36:43 (client local time) WITH STATUS 10 IN 1200.01 SECONDS stats: 3354 7 1200.01 10
c Parsing PB file... c Converting 696 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 694]---> Sorter-cost: 1575 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 692]---> Adder-cost: 148 maxlim: 187647 bits: 19/18 c ---[ 690]---> BDD-cost: 1 c ---[ 688]---> BDD-cost: 3 c ---[ 686]---> BDD-cost: 1 c ---[ 684]---> BDD-cost: 13 c ---[ 682]---> BDD-cost: 17 c ---[ 680]---> BDD-cost: 13 c ---[ 678]---> BDD-cost: 9 c ---[ 676]---> BDD-cost: 5 c ---[ 674]---> BDD-cost: 30 c ---[ 672]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 670]---> BDD-cost: 6 c ---[ 668]---> BDD-cost: 13 c ---[ 666]---> BDD-cost: 21 c ---[ 664]---> BDD-cost: 6 c ---[ 662]---> BDD-cost: 6 c ---[ 660]---> BDD-cost: 6 c ---[ 658]---> BDD-cost: 6 c ---[ 656]---> BDD-cost: 6 c ---[ 654]---> BDD-cost: 13 c ---[ 652]---> BDD-cost: 1 c ---[ 650]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 648]---> BDD-cost: 6 c ---[ 646]---> BDD-cost: 13 c ---[ 644]---> BDD-cost: 17 c ---[ 642]---> BDD-cost: 22 c ---[ 640]---> BDD-cost: 22 c ---[ 638]---> BDD-cost: 0 c ---[ 636]---> BDD-cost: 13 c ---[ 634]---> BDD-cost: 1 c ---[ 632]---> BDD-cost: 1 c ---[ 630]---> BDD-cost: 1 c ---[ 628]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 626]---> BDD-cost: 13 c ---[ 624]---> BDD-cost: 14 c ---[ 622]---> BDD-cost: 13 c ---[ 620]---> BDD-cost: 9 c ---[ 618]---> BDD-cost: 5 c ---[ 616]---> BDD-cost: 30 c ---[ 614]---> BDD-cost: 6 c ---[ 612]---> BDD-cost: 13 c ---[ 610]---> BDD-cost: 16 c ---[ 608]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 606]---> BDD-cost: 6 c ---[ 604]---> BDD-cost: 9 c ---[ 602]---> BDD-cost: 6 c ---[ 600]---> BDD-cost: 6 c ---[ 598]---> BDD-cost: 6 c ---[ 596]---> BDD-cost: 13 c ---[ 594]---> BDD-cost: 1 c ---[ 592]---> BDD-cost: 9 c ---[ 590]---> BDD-cost: 17 c ---[ 588]---> BDD-cost: 17 c ---[ 586]---> Adder-cost: 148 maxlim: 189695 bits: 19/18 c ---[ 584]---> BDD-cost: 17 c ---[ 582]---> BDD-cost: 27 c ---[ 580]---> BDD-cost: 22 c ---[ 578]---> BDD-cost: 13 c ---[ 576]---> BDD-cost: 1 c ---[ 574]---> BDD-cost: 1 c ---[ 572]---> BDD-cost: 1 c ---[ 570]---> BDD-cost: 13 c ---[ 568]---> BDD-cost: 14 c ---[ 566]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 564]---> BDD-cost: 13 c ---[ 562]---> BDD-cost: 9 c ---[ 560]---> BDD-cost: 5 c ---[ 558]---> BDD-cost: 30 c ---[ 556]---> BDD-cost: 6 c ---[ 554]---> BDD-cost: 13 c ---[ 552]---> BDD-cost: 21 c ---[ 550]---> BDD-cost: 6 c ---[ 548]---> BDD-cost: 9 c ---[ 546]---> BDD-cost: 6 c ---[ 544]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 542]---> BDD-cost: 6 c ---[ 540]---> BDD-cost: 6 c ---[ 538]---> BDD-cost: 13 c ---[ 536]---> BDD-cost: 1 c ---[ 534]---> BDD-cost: 9 c ---[ 532]---> BDD-cost: 17 c ---[ 530]---> BDD-cost: 17 c ---[ 528]---> BDD-cost: 27 c ---[ 526]---> BDD-cost: 27 c ---[ 524]---> BDD-cost: 22 c ---[ 522]---> Adder-cost: 148 maxlim: 182783 bits: 19/18 c ---[ 520]---> BDD-cost: 0 c ---[ 518]---> BDD-cost: 13 c ---[ 516]---> BDD-cost: 1 c ---[ 514]---> BDD-cost: 1 c ---[ 512]---> BDD-cost: 1 c ---[ 510]---> BDD-cost: 14 c ---[ 508]---> BDD-cost: 13 c ---[ 506]---> BDD-cost: 9 c ---[ 504]---> BDD-cost: 5 c ---[ 502]---> Sorter-cost: 1001 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 500]---> BDD-cost: 27 c ---[ 498]---> BDD-cost: 6 c ---[ 496]---> BDD-cost: 13 c ---[ 494]---> BDD-cost: 21 c ---[ 492]---> BDD-cost: 6 c ---[ 490]---> BDD-cost: 9 c ---[ 488]---> BDD-cost: 6 c ---[ 486]---> BDD-cost: 6 c ---[ 484]---> BDD-cost: 3 c ---[ 482]---> BDD-cost: 9 c ---[ 480]---> Adder-cost: 148 maxlim: 189183 bits: 19/18 c ---[ 478]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 476]---> BDD-cost: 1 c ---[ 474]---> BDD-cost: 9 c ---[ 472]---> BDD-cost: 17 c ---[ 470]---> BDD-cost: 17 c ---[ 468]---> BDD-cost: 27 c ---[ 466]---> BDD-cost: 27 c ---[ 464]---> BDD-cost: 22 c ---[ 462]---> BDD-cost: 0 c ---[ 460]---> BDD-cost: 9 c ---[ 458]---> BDD-cost: 1 c ---[ 456]---> Sorter-cost: 1001 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 454]---> BDD-cost: 1 c ---[ 452]---> BDD-cost: 1 c ---[ 450]---> BDD-cost: 13 c ---[ 448]---> BDD-cost: 13 c ---[ 446]---> BDD-cost: 6 c ---[ 444]---> BDD-cost: 5 c ---[ 442]---> BDD-cost: 24 c ---[ 440]---> BDD-cost: 6 c ---[ 438]---> BDD-cost: 13 c ---[ 436]---> Sorter-cost: 1002 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 434]---> BDD-cost: 21 c ---[ 432]---> BDD-cost: 6 c ---[ 430]---> BDD-cost: 9 c ---[ 428]---> BDD-cost: 6 c ---[ 426]---> BDD-cost: 6 c ---[ 424]---> BDD-cost: 6 c ---[ 422]---> BDD-cost: 13 c ---[ 420]---> BDD-cost: 1 c ---[ 418]---> BDD-cost: 9 c ---[ 416]---> BDD-cost: 13 c ---[ 414]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 412]---> BDD-cost: 17 c ---[ 410]---> BDD-cost: 27 c ---[ 408]---> BDD-cost: 27 c ---[ 406]---> BDD-cost: 22 c ---[ 404]---> BDD-cost: 0 c ---[ 402]---> BDD-cost: 13 c ---[ 400]---> BDD-cost: 1 c ---[ 398]---> BDD-cost: 1 c ---[ 396]---> BDD-cost: 1 c ---[ 394]---> Sorter-cost: 1003 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 392]---> BDD-cost: 9 c ---[ 390]---> BDD-cost: 10 c ---[ 388]---> BDD-cost: 13 c ---[ 386]---> BDD-cost: 9 c ---[ 384]---> BDD-cost: 5 c ---[ 382]---> BDD-cost: 6 c ---[ 380]---> BDD-cost: 9 c ---[ 378]---> BDD-cost: 21 c ---[ 376]---> BDD-cost: 3 c ---[ 374]---> BDD-cost: 9 c ---[ 372]---> Adder-cost: 148 maxlim: 183039 bits: 19/18 c ---[ 370]---> BDD-cost: 6 c ---[ 368]---> BDD-cost: 6 c ---[ 366]---> BDD-cost: 6 c ---[ 364]---> BDD-cost: 13 c ---[ 362]---> BDD-cost: 1 c ---[ 360]---> BDD-cost: 9 c ---[ 358]---> BDD-cost: 17 c ---[ 356]---> BDD-cost: 17 c ---[ 354]---> BDD-cost: 27 c ---[ 352]---> BDD-cost: 27 c ---[ 350]---> Adder-cost: 148 maxlim: 189183 bits: 19/18 c ---[ 348]---> BDD-cost: 22 c ---[ 346]---> BDD-cost: 0 c ---[ 344]---> BDD-cost: 9 c ---[ 342]---> BDD-cost: 1 c ---[ 340]---> BDD-cost: 1 c ---[ 338]---> BDD-cost: 1 c ---[ 336]---> BDD-cost: 13 c ---[ 334]---> BDD-cost: 14 c ---[ 332]---> BDD-cost: 13 c ---[ 330]---> Adder-cost: 148 maxlim: 196607 bits: 19/18 c ---[ 328]---> BDD-cost: 9 c ---[ 326]---> BDD-cost: 5 c ---[ 324]---> BDD-cost: 24 c ---[ 322]---> BDD-cost: 3 c ---[ 320]---> BDD-cost: 21 c ---[ 318]---> BDD-cost: 6 c ---[ 316]---> BDD-cost: 9 c ---[ 314]---> BDD-cost: 6 c ---[ 312]---> BDD-cost: 6 c ---[ 310]---> BDD-cost: 6 c ---[ 308]---> Adder-cost: 148 maxlim: 198783 bits: 19/18 c ---[ 306]---> BDD-cost: 13 c ---[ 304]---> BDD-cost: 1 c ---[ 302]---> BDD-cost: 9 c ---[ 300]---> BDD-cost: 17 c ---[ 298]---> BDD-cost: 17 c ---[ 296]---> BDD-cost: 22 c ---[ 294]---> BDD-cost: 27 c ---[ 292]---> BDD-cost: 17 c ---[ 290]---> BDD-cost: 0 c ---[ 288]---> BDD-cost: 13 c ---[ 286]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 284]---> BDD-cost: 1 c ---[ 282]---> BDD-cost: 1 c ---[ 280]---> BDD-cost: 13 c ---[ 278]---> BDD-cost: 14 c ---[ 276]---> BDD-cost: 13 c ---[ 274]---> BDD-cost: 9 c ---[ 272]---> BDD-cost: 5 c ---[ 270]---> BDD-cost: 30 c ---[ 268]---> Adder-cost: 148 maxlim: 195199 bits: 19/18 c ---[ 266]---> Adder-cost: 148 maxlim: 199167 bits: 19/18 c ---[ 264]---> BDD-cost: 6 c ---[ 262]---> BDD-cost: 13 c ---[ 260]---> BDD-cost: 6 c ---[ 258]---> BDD-cost: 9 c ---[ 256]---> BDD-cost: 6 c ---[ 254]---> BDD-cost: 6 c ---[ 252]---> BDD-cost: 6 c ---[ 250]---> BDD-cost: 13 c ---[ 248]---> BDD-cost: 9 c ---[ 246]---> Adder-cost: 148 maxlim: 182271 bits: 19/18 c ---[ 244]---> BDD-cost: 17 c ---[ 242]---> BDD-cost: 17 c ---[ 240]---> BDD-cost: 27 c ---[ 238]---> BDD-cost: 27 c ---[ 236]---> BDD-cost: 22 c ---[ 234]---> BDD-cost: 0 c ---[ 232]---> BDD-cost: 13 c ---[ 230]---> BDD-cost: 1 c ---[ 228]---> BDD-cost: 1 c ---[ 226]---> BDD-cost: 1 c ---[ 224]---> Adder-cost: 148 maxlim: 166527 bits: 19/18 c ---[ 222]---> BDD-cost: 9 c ---[ 220]---> BDD-cost: 14 c ---[ 218]---> BDD-cost: 13 c ---[ 216]---> BDD-cost: 9 c ---[ 214]---> BDD-cost: 5 c ---[ 212]---> BDD-cost: 30 c ---[ 210]---> BDD-cost: 6 c ---[ 208]---> BDD-cost: 13 c ---[ 206]---> BDD-cost: 21 c ---[ 204]---> Adder-cost: 148 maxlim: 197887 bits: 19/18 c ---[ 202]---> BDD-cost: 6 c ---[ 200]---> BDD-cost: 9 c ---[ 198]---> BDD-cost: 6 c ---[ 196]---> BDD-cost: 6 c ---[ 194]---> BDD-cost: 9 c ---[ 192]---> BDD-cost: 1 c ---[ 190]---> BDD-cost: 9 c ---[ 188]---> BDD-cost: 17 c ---[ 186]---> BDD-cost: 17 c ---[ 184]---> BDD-cost: 27 c ---[ 182]---> Adder-cost: 148 maxlim: 198399 bits: 19/18 c ---[ 180]---> BDD-cost: 22 c ---[ 178]---> BDD-cost: 22 c ---[ 176]---> BDD-cost: 0 c ---[ 174]---> BDD-cost: 13 c ---[ 172]---> BDD-cost: 1 c ---[ 170]---> BDD-cost: 1 c ---[ 168]---> BDD-cost: 1 c ---[ 166]---> BDD-cost: 13 c ---[ 164]---> BDD-cost: 14 c ---[ 162]---> Adder-cost: 148 maxlim: 181503 bits: 19/18 c ---[ 160]---> BDD-cost: 13 c ---[ 158]---> BDD-cost: 9 c ---[ 156]---> BDD-cost: 5 c ---[ 154]---> BDD-cost: 30 c ---[ 152]---> BDD-cost: 6 c ---[ 150]---> BDD-cost: 13 c ---[ 148]---> BDD-cost: 21 c ---[ 146]---> BDD-cost: 6 c ---[ 144]---> BDD-cost: 6 c ---[ 142]---> BDD-cost: 6 c ---[ 140]---> Adder-cost: 148 maxlim: 181247 bits: 19/18 c ---[ 138]---> BDD-cost: 6 c ---[ 136]---> BDD-cost: 6 c ---[ 134]---> BDD-cost: 13 c ---[ 132]---> BDD-cost: 1 c ---[ 130]---> Adder-cost: 148 maxlim: 194559 bits: 19/18 c ---[ 128]---> Adder-cost: 148 maxlim: 195199 bits: 19/18 c ---[ 126]---> Sorter-cost: 1657 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 124]---> Adder-cost: 148 maxlim: 197375 bits: 19/18 c ---[ 122]---> Adder-cost: 148 maxlim: 196863 bits: 19/18 c ---[ 120]---> Adder-cost: 148 maxlim: 198911 bits: 19/18 c ---[ 118]---> Adder-cost: 148 maxlim: 198399 bits: 19/18 c ---[ 116]---> Adder-cost: 148 maxlim: 196479 bits: 19/18 c ---[ 114]---> Adder-cost: 148 maxlim: 196607 bits: 19/18 c ---[ 112]---> BDD-cost: 5 c ---[ 110]---> BDD-cost: 7 c ---[ 108]---> BDD-cost: 5 c ---[ 106]---> BDD-cost: 3 c ---[ 104]---> Adder-cost: 148 maxlim: 181119 bits: 19/18 c ---[ 102]---> BDD-cost: 5 c ---[ 100]---> BDD-cost: 7 c ---[ 98]---> BDD-cost: 3 c ---[ 96]---> BDD-cost: 1 c ---[ 94]---> BDD-cost: 1 c ---[ 92]---> BDD-cost: 3 c ---[ 90]---> BDD-cost: 15 c ---[ 88]---> BDD-cost: 15 c ---[ 86]---> BDD-cost: 15 c ---[ 84]---> BDD-cost: 15 c ---[ 82]---> Adder-cost: 148 maxlim: 193407 bits: 19/18 c ---[ 80]---> BDD-cost: 15 c ---[ 78]---> BDD-cost: 15 c ---[ 76]---> BDD-cost: 15 c ---[ 74]---> BDD-cost: 15 c ---[ 72]---> BDD-cost: 15 c ---[ 70]---> BDD-cost: 15 c ---[ 68]---> BDD-cost: 15 c ---[ 66]---> BDD-cost: 17 c ---[ 64]---> BDD-cost: 17 c ---[ 62]---> BDD-cost: 22 c ---[ 60]---> Sorter-cost: 1001 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 58]---> BDD-cost: 17 c ---[ 56]---> BDD-cost: 13 c ---[ 54]---> BDD-cost: 1 c ---[ 52]---> BDD-cost: 1 c ---[ 50]---> BDD-cost: 1 c ---[ 48]---> BDD-cost: 13 c ---[ 46]---> BDD-cost: 14 c ---[ 44]---> BDD-cost: 13 c ---[ 42]---> Sorter-cost: 1657 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 40]---> BDD-cost: 9 c ---[ 38]---> BDD-cost: 5 c ---[ 36]---> BDD-cost: 30 c ---[ 34]---> BDD-cost: 6 c ---[ 32]---> BDD-cost: 13 c ---[ 30]---> BDD-cost: 16 c ---[ 28]---> BDD-cost: 6 c ---[ 26]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 6 c ---[ 22]---> BDD-cost: 6 c ---[ 20]---> Sorter-cost: 1004 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[ 18]---> BDD-cost: 6 c ---[ 16]---> BDD-cost: 13 c ---[ 14]---> BDD-cost: 1 c ---[ 12]---> BDD-cost: 9 c ---[ 10]---> BDD-cost: 17 c ---[ 8]---> BDD-cost: 15 c ---[ 6]---> BDD-cost: 22 c ---[ 4]---> BDD-cost: 17 c ---[ 2]---> BDD-cost: 0 c ---[ 0]---> BDD-cost: 10 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 73454 211352 | 24484 0 0 nan | 0.000 % | c | 100 | 73440 211324 | 26932 97 607 6.3 | 10.323 % | c | 250 | 73440 211324 | 29625 247 2014 8.2 | 10.323 % | c | 475 | 73417 211273 | 32588 467 3647 7.8 | 10.349 % | c | 812 | 73393 211205 | 35847 799 6444 8.1 | 10.376 % | c | 1318 | 73389 211196 | 39431 1302 10584 8.1 | 10.380 % | c | 2078 | 73280 210944 | 43374 2049 18545 9.1 | 10.499 % | c | 3218 | 73250 210864 | 47712 3180 29887 9.4 | 10.538 % | c | 4926 | 73062 210418 | 52483 4857 44299 9.1 | 10.762 % | c | 7489 | 73019 210301 | 57731 7408 67396 9.1 | 10.820 % | c | 11333 | 72813 209821 | 63505 11206 99910 8.9 | 11.110 % | c | 17099 | 72506 209086 | 69855 16928 156867 9.3 | 11.549 % | c | 25748 | 71899 207602 | 76841 25474 248883 9.8 | 12.358 % | c | 38722 | 71583 206680 | 84525 38397 389196 10.1 | 12.652 % | c ============================================================================== c [1mFound solution: 2059971758[0m c ---[ 0]---> c *** TERMINATED *** s SATISFIABLE v -F040704_bit0 -F040407_bit0 -F040820_bit0 -F042008_bit0 -F040821_bit0 F042108_bit0 F040826_bit0 -F042608_bit0 -F040923_bit0 -F042309_bit0 F041603_bit0 F040316_bit0 -F040116_bit0 -F041727_bit0 -F042717_bit0 -F040103_bit0 F040321_bit0 -F042103_bit0 -F040322_bit0 F042203_bit0 -F040118_bit0 -F041924_bit0 F042419_bit0 -F041940_bit0 -F044019_bit0 F041941_bit0 -F044119_bit0 -F040120_bit0 -F042022_bit0 -F042220_bit0 -F042024_bit0 -F042420_bit0 F040122_bit0 -F040105_bit0 -F040102_bit0 -F040129_bit0 -F040104_bit0 -F040148_bit0 -F042123_bit0 -F042321_bit0 -F040506_bit0 -F040605_bit0 -F040529_bit0 -F042905_bit0 -F040504_bit0 F040405_bit0 -F040548_bit0 -F044805_bit0 -F042426_bit0 F042624_bit0 -F042402_bit0 -F040224_bit0 -F042428_bit0 -F042824_bit0 -F042526_bit0 -F042625_bit0 -F042530_bit0 -F043025_bit0 F040206_bit0 -F040602_bit0 -F040231_bit0 F043102_bit0 -F042706_bit0 -F040627_bit0 -F042704_bit0 F040427_bit0 F042743_bit0 F044327_bit0 -F042830_bit0 -F043028_bit0 F040604_bit0 -F040406_bit0 -F042948_bit0 -F044829_bit0 -F043141_bit0 F044131_bit0 -F044041_bit0 -F044140_bit0 -F050704_bit0 -F050407_bit0 -F050820_bit0 -F052008_bit0 -F050821_bit0 F052108_bit0 F050826_bit0 -F052608_bit0 -F050923_bit0 -F052309_bit0 F051603_bit0 -F050316_bit0 F050116_bit0 -F051727_bit0 -F052717_bit0 -F050103_bit0 F050321_bit0 -F052103_bit0 -F050322_bit0 -F052203_bit0 -F050118_bit0 F051924_bit0 F052419_bit0 -F051940_bit0 -F054019_bit0 -F051941_bit0 -F054119_bit0 -F050120_bit0 F052022_bit0 F052220_bit0 F052024_bit0 F052420_bit0 -F050122_bit0 -F050105_bit0 -F050102_bit0 -F050129_bit0 -F050104_bit0 -F050148_bit0 -F052123_bit0 -F052321_bit0 -F050506_bit0 -F050605_bit0 -F050529_bit0 -F052905_bit0 -F050504_bit0 F050405_bit0 F050548_bit0 -F054805_bit0 -F052426_bit0 F052624_bit0 F052402_bit0 -F050224_bit0 -F052428_bit0 -F052824_bit0 -F052526_bit0 -F052625_bit0 F052530_bit0 F053025_bit0 F050206_bit0 -F050602_bit0 -F050231_bit0 -F053102_bit0 -F052706_bit0 F050627_bit0 F052704_bit0 -F050427_bit0 F052743_bit0 F054327_bit0 -F052830_bit0 -F053028_bit0 -F050604_bit0 -F050406_bit0 -F052948_bit0 -F054829_bit0 -F053141_bit0 -F054131_bit0 -F054041_bit0 -F054140_bit0 F060704_bit0 F060407_bit0 -F060820_bit0 -F062008_bit0 F060821_bit0 -F062108_bit0 -F060826_bit0 F062608_bit0 -F060923_bit0 -F062309_bit0 -F061603_bit0 -F060316_bit0 -F060116_bit0 -F061727_bit0 -F062717_bit0 -F060103_bit0 -F060321_bit0 F062103_bit0 F060322_bit0 -F062203_bit0 -F060118_bit0 -F061924_bit0 -F062419_bit0 -F061940_bit0 -F064019_bit0 -F061941_bit0 -F064119_bit0 -F060120_bit0 -F062022_bit0 F062220_bit0 F062024_bit0 -F062420_bit0 -F060122_bit0 -F060105_bit0 F060102_bit0 -F060129_bit0 -F060104_bit0 -F060148_bit0 -F062123_bit0 -F062321_bit0 -F060506_bit0 -F060605_bit0 -F060529_bit0 -F062905_bit0 -F060504_bit0 -F060405_bit0 -F060548_bit0 -F064805_bit0 F062426_bit0 -F062624_bit0 -F062402_bit0 -F060224_bit0 F062428_bit0 F062824_bit0 -F062526_bit0 -F062625_bit0 F062530_bit0 F063025_bit0 F060206_bit0 F060602_bit0 -F060231_bit0 -F063102_bit0 -F062706_bit0 -F060627_bit0 -F062704_bit0 -F060427_bit0 F062743_bit0 F064327_bit0 F062830_bit0 F063028_bit0 F060604_bit0 -F060406_bit0 -F062948_bit0 -F064829_bit0 -F063141_bit0 -F064131_bit0 -F064041_bit0 -F064140_bit0 -F070704_bit0 F070407_bit0 F070820_bit0 F072008_bit0 F070821_bit0 -F072108_bit0 -F070826_bit0 F072608_bit0 -F070923_bit0 -F072309_bit0 -F071603_bit0 -F070316_bit0 -F070116_bit0 F071727_bit0 F072717_bit0 -F070103_bit0 -F070321_bit0 F072103_bit0 F070322_bit0 -F072203_bit0 -F070118_bit0 -F071924_bit0 -F072419_bit0 F071940_bit0 -F074019_bit0 -F071941_bit0 F074119_bit0 -F070120_bit0 -F072022_bit0 F072220_bit0 F072024_bit0 -F072420_bit0 -F070122_bit0 -F070105_bit0 -F070102_bit0 F070129_bit0 -F070104_bit0 -F070148_bit0 -F072123_bit0 -F072321_bit0 F070506_bit0 -F070605_bit0 -F070529_bit0 F072905_bit0 -F070504_bit0 -F070405_bit0 -F070548_bit0 -F074805_bit0 F072426_bit0 -F072624_bit0 -F072402_bit0 -F070224_bit0 F072428_bit0 F072824_bit0 F072526_bit0 F072625_bit0 -F072530_bit0 -F073025_bit0 -F070206_bit0 -F070602_bit0 -F070231_bit0 -F073102_bit0 -F072706_bit0 -F070627_bit0 -F072704_bit0 -F070427_bit0 -F072743_bit0 -F074327_bit0 -F072830_bit0 -F073028_bit0 F070604_bit0 -F070406_bit0 -F072948_bit0 -F074829_bit0 F073141_bit0 F074131_bit0 F074041_bit0 -F074140_bit0 F190704_bit0 F190407_bit0 -F190820_bit0 -F192008_bit0 F190821_bit0 F192108_bit0 -F190826_bit0 -F192608_bit0 -F190923_bit0 -F192309_bit0 -F191603_bit0 -F190316_bit0 -F190116_bit0 -F191727_bit0 -F192717_bit0 -F190103_bit0 -F190321_bit0 -F192103_bit0 -F190322_bit0 -F192203_bit0 -F190118_bit0 -F191924_bit0 -F192419_bit0 -F191940_bit0 -F194019_bit0 -F191941_bit0 F194119_bit0 -F190120_bit0 -F192022_bit0 F192220_bit0 F192024_bit0 -F192420_bit0 F190122_bit0 -F190105_bit0 -F190102_bit0 -F190129_bit0 -F190104_bit0 -F190148_bit0 -F192123_bit0 -F192321_bit0 -F190506_bit0 -F190605_bit0 -F190529_bit0 F192905_bit0 -F190504_bit0 -F190405_bit0 F190548_bit0 -F194805_bit0 -F192426_bit0 -F192624_bit0 F192402_bit0 -F190224_bit0 -F192428_bit0 -F192824_bit0 -F192526_bit0 -F192625_bit0 -F192530_bit0 -F193025_bit0 -F190206_bit0 -F190602_bit0 F190231_bit0 -F193102_bit0 -F192706_bit0 -F190627_bit0 F192704_bit0 F190427_bit0 F192743_bit0 F194327_bit0 -F192830_bit0 -F193028_bit0 F190604_bit0 F190406_bit0 -F192948_bit0 F194829_bit0 F193141_bit0 -F194131_bit0 -F194041_bit0 -F194140_bit0 -F200704_bit0 -F200407_bit0 F200820_bit0 F202008_bit0 -F200821_bit0 -F202108_bit0 -F200826_bit0 F202608_bit0 -F200923_bit0 -F202309_bit0 -F201603_bit0 -F200316_bit0 -F200116_bit0 F201727_bit0 F202717_bit0 -F200103_bit0 -F200321_bit0 -F202103_bit0 -F200322_bit0 -F202203_bit0 -F200118_bit0 F201924_bit0 F202419_bit0 -F201940_bit0 F204019_bit0 F201941_bit0 -F204119_bit0 -F200120_bit0 -F202022_bit0 -F202220_bit0 F202024_bit0 -F202420_bit0 -F200122_bit0 -F200105_bit0 F200102_bit0 -F200129_bit0 -F200104_bit0 -F200148_bit0 -F202123_bit0 -F202321_bit0 -F200506_bit0 F200605_bit0 F200529_bit0 F202905_bit0 F200504_bit0 -F200405_bit0 -F200548_bit0 -F204805_bit0 F202426_bit0 -F202624_bit0 -F202402_bit0 F200224_bit0 -F202428_bit0 -F202824_bit0 F202526_bit0 F202625_bit0 -F202530_bit0 -F203025_bit0 -F200206_bit0 -F200602_bit0 F200231_bit0 F203102_bit0 -F202706_bit0 -F200627_bit0 -F202704_bit0 -F200427_bit0 -F202743_bit0 -F204327_bit0 -F202830_bit0 -F203028_bit0 -F200604_bit0 F200406_bit0 F202948_bit0 F204829_bit0 -F203141_bit0 -F204131_bit0 -F204041_bit0 F204140_bit0 -F240704_bit0 -F240407_bit0 -F240820_bit0 -F242008_bit0 -F240821_bit0 -F242108_bit0 F240826_bit0 F242608_bit0 -F240923_bit0 -F242309_bit0 -F241603_bit0 -F240316_bit0 -F240116_bit0 -F241727_bit0 -F242717_bit0 -F240103_bit0 -F240321_bit0 -F242103_bit0 F240322_bit0 F242203_bit0 -F240118_bit0 -F241924_bit0 -F242419_bit0 -F241940_bit0 -F244019_bit0 -F241941_bit0 -F244119_bit0 -F240120_bit0 -F242022_bit0 -F242220_bit0 -F242024_bit0 -F242420_bit0 -F240122_bit0 -F240105_bit0 F240102_bit0 -F240129_bit0 -F240104_bit0 -F240148_bit0 -F242123_bit0 -F242321_bit0 -F240506_bit0 F240605_bit0 F240529_bit0 -F242905_bit0 F240504_bit0 -F240405_bit0 -F240548_bit0 F244805_bit0 F242426_bit0 -F242624_bit0 F242402_bit0 F240224_bit0 F242428_bit0 -F242824_bit0 F242526_bit0 F242625_bit0 -F242530_bit0 -F243025_bit0 -F240206_bit0 -F240602_bit0 -F240231_bit0 -F243102_bit0 F242706_bit0 -F240627_bit0 -F242704_bit0 F240427_bit0 F242743_bit0 F244327_bit0 -F242830_bit0 -F243028_bit0 F240604_bit0 F240406_bit0 F242948_bit0 -F244829_bit0 -F243141_bit0 -F244131_bit0 -F244041_bit0 -F244140_bit0 F260704_bit0 F260407_bit0 F260820_bit0 -F262008_bit0 -F260821_bit0 F262108_bit0 -F260826_bit0 -F262608_bit0 -F260923_bit0 -F262309_bit0 F261603_bit0 -F260316_bit0 F260116_bit0 F261727_bit0 F262717_bit0 -F260103_bit0 F260321_bit0 -F262103_bit0 -F260322_bit0 -F262203_bit0 -F260118_bit0 -F261924_bit0 -F262419_bit0 -F261940_bit0 -F264019_bit0 -F261941_bit0 -F264119_bit0 -F260120_bit0 -F262022_bit0 -F262220_bit0 F262024_bit0 -F262420_bit0 -F260122_bit0 -F260105_bit0 -F260102_bit0 -F260129_bit0 -F260104_bit0 -F260148_bit0 -F262123_bit0 -F262321_bit0 -F260506_bit0 -F260605_bit0 -F260529_bit0 -F262905_bit0 -F260504_bit0 -F260405_bit0 -F260548_bit0 -F264805_bit0 F262426_bit0 F262624_bit0 F262402_bit0 F260224_bit0 -F262428_bit0 -F262824_bit0 -F262526_bit0 -F262625_bit0 -F262530_bit0 -F263025_bit0 -F260206_bit0 -F260602_bit0 -F260231_bit0 -F263102_bit0 F262706_bit0 -F260627_bit0 -F262704_bit0 F260427_bit0 -F262743_bit0 -F264327_bit0 F262830_bit0 F263028_bit0 F260604_bit0 -F260406_bit0 -F262948_bit0 -F264829_bit0 -F263141_bit0 -F264131_bit0 -F264041_bit0 -F264140_bit0 -F270704_bit0 -F270407_bit0 F270820_bit0 F272008_bit0 F270821_bit0 -F272108_bit0 -F270826_bit0 F272608_bit0 -F270923_bit0 -F272309_bit0 F271603_bit0 F270316_bit0 -F270116_bit0 -F271727_bit0 -F272717_bit0 -F270103_bit0 -F270321_bit0 F272103_bit0 F270322_bit0 -F272203_bit0 -F270118_bit0 -F271924_bit0 -F272419_bit0 F271940_bit0 -F274019_bit0 -F271941_bit0 F274119_bit0 -F270120_bit0 -F272022_bit0 F272220_bit0 F272024_bit0 -F272420_bit0 -F270122_bit0 -F270105_bit0 -F270102_bit0 -F270129_bit0 F270104_bit0 -F270148_bit0 -F272123_bit0 -F272321_bit0 F270506_bit0 -F270605_bit0 -F270529_bit0 -F272905_bit0 -F270504_bit0 F270405_bit0 -F270548_bit0 -F274805_bit0 -F272426_bit0 -F272624_bit0 F272402_bit0 F270224_bit0 F272428_bit0 -F272824_bit0 F272526_bit0 -F272625_bit0 -F272530_bit0 F273025_bit0 F270206_bit0 F270602_bit0 F270231_bit0 F273102_bit0 -F272706_bit0 -F270627_bit0 F272704_bit0 F270427_bit0 -F272743_bit0 -F274327_bit0 F272830_bit0 -F273028_bit0 F270604_bit0 -F270406_bit0 F272948_bit0 F274829_bit0 -F273141_bit0 -F274131_bit0 F274041_bit0 -F274140_bit0 F400704_bit0 F400407_bit0 -F400820_bit0 F402008_bit0 -F400821_bit0 -F402108_bit0 F400826_bit0 -F402608_bit0 F400923_bit0 F402309_bit0 -F401603_bit0 -F400316_bit0 -F400116_bit0 -F401727_bit0 -F402717_bit0 F400103_bit0 F400321_bit0 F402103_bit0 F400322_bit0 -F402203_bit0 -F400118_bit0 -F401924_bit0 F402419_bit0 -F401940_bit0 F404019_bit0 F401941_bit0 -F404119_bit0 -F400120_bit0 -F402022_bit0 F402220_bit0 -F402024_bit0 -F402420_bit0 -F400122_bit0 -F400105_bit0 -F400102_bit0 -F400129_bit0 -F400104_bit0 -F400148_bit0 -F402123_bit0 -F402321_bit0 -F400506_bit0 -F400605_bit0 F400529_bit0 -F402905_bit0 F400504_bit0 F400405_bit0 -F400548_bit0 F404805_bit0 F402426_bit0 F402624_bit0 -F402402_bit0 -F400224_bit0 -F402428_bit0 F402824_bit0 -F402526_bit0 F402625_bit0 F402530_bit0 -F403025_bit0 -F400206_bit0 -F400602_bit0 -F400231_bit0 -F403102_bit0 -F402706_bit0 F400627_bit0 F402704_bit0 -F400427_bit0 -F402743_bit0 -F404327_bit0 -F402830_bit0 F403028_bit0 -F400604_bit0 F400406_bit0 F402948_bit0 -F404829_bit0 F403141_bit0 F404131_bit0 -F404041_bit0 F404140_bit0 -F480704_bit0 -F480407_bit0 F480820_bit0 F482008_bit0 -F480821_bit0 -F482108_bit0 F480826_bit0 F482608_bit0 -F480923_bit0 -F482309_bit0 F481603_bit0 F480316_bit0 -F480116_bit0 -F481727_bit0 -F482717_bit0 -F480103_bit0 F480321_bit0 F482103_bit0 F480322_bit0 F482203_bit0 -F480118_bit0 -F481924_bit0 F482419_bit0 -F481940_bit0 -F484019_bit0 F481941_bit0 -F484119_bit0 -F480120_bit0 -F482022_bit0 -F482220_bit0 -F482024_bit0 -F482420_bit0 -F480122_bit0 -F480105_bit0 -F480102_bit0 -F480129_bit0 -F480104_bit0 F480148_bit0 -F482123_bit0 -F482321_bit0 F480506_bit0 F480605_bit0 F480529_bit0 F482905_bit0 -F480504_bit0 -F480405_bit0 -F480548_bit0 -F484805_bit0 F482426_bit0 F482624_bit0 -F482402_bit0 F480224_bit0 -F482428_bit0 -F482824_bit0 F482526_bit0 F482625_bit0 F482530_bit0 F483025_bit0 F480206_bit0 F480602_bit0 -F480231_bit0 F483102_bit0 F482706_bit0 F480627_bit0 -F482704_bit0 -F480427_bit0 F482743_bit0 F484327_bit0 F482830_bit0 F483028_bit0 F480604_bit0 F480406_bit0 -F482948_bit0 F484829_bit0 -F483141_bit0 F484131_bit0 F484041_bit0 F484140_bit0 -Y010704_bit0 -Y020704_bit0 Y030704_bit0 Y040704_bit0 Y050704_bit0 -Y060704_bit0 Y070704_bit0 -Y080704_bit0 -Y090704_bit0 -Y010820_bit0 -Y020820_bit0 -Y030820_bit0 -Y040820_bit0 -Y050820_bit0 Y060820_bit0 -Y070820_bit0 Y080820_bit0 -Y090820_bit0 -Y010821_bit0 Y020821_bit0 -Y030821_bit0 -Y040821_bit0 Y050821_bit0 -Y060821_bit0 Y070821_bit0 Y080821_bit0 -Y090821_bit0 Y010826_bit0 Y020826_bit0 -Y030826_bit0 -Y040826_bit0 -Y050826_bit0 -Y060826_bit0 Y070826_bit0 -Y080826_bit0 Y090826_bit0 Y010923_bit0 -Y020923_bit0 -Y030923_bit0 -Y040923_bit0 -Y050923_bit0 Y060923_bit0 -Y070923_bit0 -Y080923_bit0 -Y090923_bit0 -Y011603_bit0 -Y021603_bit0 Y031603_bit0 Y041603_bit0 -Y051603_bit0 Y061603_bit0 Y071603_bit0 -Y081603_bit0 -Y091603_bit0 Y011601_bit0 Y021601_bit0 Y031601_bit0 Y041601_bit0 Y051601_bit0 Y061601_bit0 -Y071601_bit0 -Y081601_bit0 -Y091601_bit0 Y011727_bit0 Y021727_bit0 Y031727_bit0 -Y041727_bit0 Y051727_bit0 -Y061727_bit0 -Y071727_bit0 Y081727_bit0 -Y091727_bit0 -Y010301_bit0 -Y020301_bit0 Y030301_bit0 Y040301_bit0 Y050301_bit0 -Y060301_bit0 Y070301_bit0 Y080301_bit0 -Y090301_bit0 -Y010321_bit0 Y020321_bit0 -Y030321_bit0 -Y040321_bit0 -Y050321_bit0 -Y060321_bit0 -Y070321_bit0 Y080321_bit0 -Y090321_bit0 Y010322_bit0 Y020322_bit0 -Y030322_bit0 -Y040322_bit0 -Y050322_bit0 -Y060322_bit0 -Y070322_bit0 Y080322_bit0 Y090322_bit0 Y011801_bit0 Y021801_bit0 Y031801_bit0 -Y041801_bit0 Y051801_bit0 -Y061801_bit0 Y071801_bit0 -Y081801_bit0 Y091801_bit0 Y011924_bit0 -Y021924_bit0 -Y031924_bit0 -Y041924_bit0 -Y051924_bit0 Y061924_bit0 Y071924_bit0 -Y081924_bit0 -Y091924_bit0 -Y011940_bit0 -Y021940_bit0 Y031940_bit0 -Y041940_bit0 -Y051940_bit0 Y061940_bit0 Y071940_bit0 -Y081940_bit0 Y091940_bit0 Y011941_bit0 Y021941_bit0 Y031941_bit0 -Y041941_bit0 -Y051941_bit0 -Y061941_bit0 Y071941_bit0 -Y081941_bit0 -Y091941_bit0 Y012001_bit0 -Y022001_bit0 Y032001_bit0 -Y042001_bit0 Y052001_bit0 -Y062001_bit0 -Y072001_bit0 Y082001_bit0 -Y092001_bit0 Y012022_bit0 -Y022022_bit0 -Y032022_bit0 Y042022_bit0 Y052022_bit0 -Y062022_bit0 Y072022_bit0 -Y082022_bit0 -Y092022_bit0 -Y012024_bit0 -Y022024_bit0 -Y032024_bit0 Y042024_bit0 -Y052024_bit0 -Y062024_bit0 Y072024_bit0 -Y082024_bit0 -Y092024_bit0 Y010122_bit0 -Y020122_bit0 Y030122_bit0 Y040122_bit0 Y050122_bit0 -Y060122_bit0 Y070122_bit0 Y080122_bit0 Y090122_bit0 -Y010105_bit0 Y020105_bit0 -Y030105_bit0 -Y040105_bit0 -Y050105_bit0 -Y060105_bit0 Y070105_bit0 -Y080105_bit0 Y090105_bit0 Y010102_bit0 -Y020102_bit0 -Y030102_bit0 -Y040102_bit0 -Y050102_bit0 Y060102_bit0 Y070102_bit0 -Y080102_bit0 -Y090102_bit0 Y010129_bit0 -Y020129_bit0 Y030129_bit0 Y040129_bit0 Y050129_bit0 Y060129_bit0 -Y070129_bit0 Y080129_bit0 Y090129_bit0 -Y010104_bit0 -Y020104_bit0 Y030104_bit0 Y040104_bit0 Y050104_bit0 Y060104_bit0 -Y070104_bit0 -Y080104_bit0 Y090104_bit0 Y010148_bit0 -Y020148_bit0 -Y030148_bit0 Y040148_bit0 -Y050148_bit0 -Y060148_bit0 Y070148_bit0 Y080148_bit0 -Y090148_bit0 Y012123_bit0 -Y022123_bit0 -Y032123_bit0 -Y042123_bit0 -Y052123_bit0 -Y062123_bit0 -Y072123_bit0 -Y082123_bit0 -Y092123_bit0 Y010506_bit0 -Y020506_bit0 -Y030506_bit0 Y040506_bit0 Y050506_bit0 Y060506_bit0 Y070506_bit0 Y080506_bit0 -Y090506_bit0 Y010529_bit0 -Y020529_bit0 -Y030529_bit0 Y040529_bit0 -Y050529_bit0 -Y060529_bit0 -Y070529_bit0 -Y080529_bit0 Y090529_bit0 -Y010504_bit0 -Y020504_bit0 -Y030504_bit0 -Y040504_bit0 -Y050504_bit0 -Y060504_bit0 -Y070504_bit0 Y080504_bit0 -Y090504_bit0 -Y010548_bit0 -Y020548_bit0 -Y030548_bit0 Y040548_bit0 -Y050548_bit0 -Y060548_bit0 Y070548_bit0 -Y080548_bit0 -Y090548_bit0 -Y012426_bit0 -Y022426_bit0 -Y032426_bit0 -Y042426_bit0 Y052426_bit0 Y062426_bit0 Y072426_bit0 Y082426_bit0 -Y092426_bit0 Y012402_bit0 -Y022402_bit0 -Y032402_bit0 Y042402_bit0 -Y052402_bit0 Y062402_bit0 Y072402_bit0 -Y082402_bit0 Y092402_bit0 Y012428_bit0 -Y022428_bit0 -Y032428_bit0 -Y042428_bit0 -Y052428_bit0 Y062428_bit0 -Y072428_bit0 Y082428_bit0 Y092428_bit0 Y012526_bit0 -Y022526_bit0 -Y032526_bit0 -Y042526_bit0 -Y052526_bit0 Y062526_bit0 Y072526_bit0 -Y082526_bit0 Y092526_bit0 Y012530_bit0 -Y022530_bit0 -Y032530_bit0 -Y042530_bit0 -Y052530_bit0 Y062530_bit0 -Y072530_bit0 Y082530_bit0 -Y092530_bit0 Y010206_bit0 -Y020206_bit0 Y030206_bit0 -Y040206_bit0 -Y050206_bit0 Y060206_bit0 -Y070206_bit0 -Y080206_bit0 -Y090206_bit0 -Y010231_bit0 Y020231_bit0 Y030231_bit0 -Y040231_bit0 -Y050231_bit0 -Y060231_bit0 -Y070231_bit0 Y080231_bit0 Y090231_bit0 -Y012706_bit0 -Y022706_bit0 -Y032706_bit0 -Y042706_bit0 -Y052706_bit0 Y062706_bit0 Y072706_bit0 -Y082706_bit0 -Y092706_bit0 -Y012704_bit0 -Y022704_bit0 -Y032704_bit0 -Y042704_bit0 Y052704_bit0 Y062704_bit0 Y072704_bit0 Y082704_bit0 Y092704_bit0 -Y012743_bit0 -Y022743_bit0 -Y032743_bit0 Y042743_bit0 -Y052743_bit0 Y062743_bit0 -Y072743_bit0 Y082743_bit0 Y092743_bit0 -Y012830_bit0 -Y022830_bit0 Y032830_bit0 Y042830_bit0 Y052830_bit0 -Y062830_bit0 -Y072830_bit0 Y082830_bit0 -Y092830_bit0 -Y010604_bit0 -Y020604_bit0 Y030604_bit0 -Y040604_bit0 -Y050604_bit0 Y060604_bit0 Y070604_bit0 Y080604_bit0 -Y090604_bit0 -Y012948_bit0 -Y022948_bit0 -Y032948_bit0 -Y042948_bit0 -Y052948_bit0 -Y062948_bit0 Y072948_bit0 Y082948_bit0 Y092948_bit0 Y013141_bit0 -Y023141_bit0 -Y033141_bit0 -Y043141_bit0 -Y053141_bit0 Y063141_bit0 Y073141_bit0 -Y083141_bit0 -Y093141_bit0 Y014041_bit0 -Y024041_bit0 -Y034041_bit0 -Y044041_bit0 -Y054041_bit0 Y064041_bit0 Y074041_bit0 -Y084041_bit0 Y094041_bit0 -S010704_bit_7 -S010704_bit_6 -S010704_bit_5 -S010704_bit_4 -S010704_bit_3 -S010704_bit_2 -S010704_bit_1 -S010704_bit0 S010704_bit1 -S010704_bit2 S010704_bit3 -S010704_bit4 -S010704_bit5 -S010704_bit6 -S010704_bit7 -S010704_bit8 -S010704_bit9 -S010704_bit10 -S010704_bit11 -S010704_bit12 -S100321_bit_7 -S100321_bit_6 -S100321_bit_5 -S100321_bit_4 -S100321_bit_3 -S100321_bit_2 -S100321_bit_1 -S100321_bit0 -S100321_bit1 S100321_bit2 -S100321_bit3 S100321_bit4 -S100321_bit5 -S100321_bit6 -S100321_bit7 -S100321_bit8 -S100321_bit9 -S100321_bit10 -S100321_bit11 -S100321_bit12 -S110322_bit_7 -S110322_bit_6 -S110322_bit_5 -S110322_bit_4 -S110322_bit_3 -S110322_bit_2 -S110322_bit_1 -S110322_bit0 -S110322_bit1 -S110322_bit2 -S110322_bit3 S110322_bit4 S110322_bit5 -S110322_bit6 S110322_bit7 -S110322_bit8 -S110322_bit9 -S110322_bit10 -S110322_bit11 -S110322_bit12 -S121801_bit_7 -S121801_bit_6 -S121801_bit_5 -S121801_bit_4 -S121801_bit_3 -S121801_bit_2 -S121801_bit_1 -S121801_bit0 S121801_bit1 -S121801_bit2 S121801_bit3 -S121801_bit4 S121801_bit5 -S121801_bit6 S121801_bit7 S121801_bit8 -S121801_bit9 -S121801_bit10 -S121801_bit11 -S121801_bit12 -S131924_bit_7 -S131924_bit_6 -S131924_bit_5 -S131924_bit_4 -S131924_bit_3 -S131924_bit_2 -S131924_bit_1 -S131924_bit0 -S131924_bit1 S131924_bit2 S131924_bit3 -S131924_bit4 -S131924_bit5 -S131924_bit6 -S131924_bit7 -S131924_bit8 -S131924_bit9 -S131924_bit10 -S131924_bit11 -S131924_bit12 -S141940_bit_7 -S141940_bit_6 -S141940_bit_5 -S141940_bit_4 -S141940_bit_3 -S141940_bit_2 -S141940_bit_1 -S141940_bit0 -S141940_bit1 -S141940_bit2 -S141940_bit3 S141940_bit4 S141940_bit5 -S141940_bit6 -S141940_bit7 S141940_bit8 -S141940_bit9 -S141940_bit10 -S141940_bit11 -S141940_bit12 -S151941_bit_7 -S151941_bit_6 -S151941_bit_5 -S151941_bit_4 -S151941_bit_3 -S151941_bit_2 -S151941_bit_1 -S151941_bit0 -S151941_bit1 -S151941_bit2 S151941_bit3 -S151941_bit4 S151941_bit5 -S151941_bit6 -S151941_bit7 -S151941_bit8 -S151941_bit9 -S151941_bit10 -S151941_bit11 -S151941_bit12 -S162001_bit_7 -S162001_bit_6 -S162001_bit_5 -S162001_bit_4 -S162001_bit_3 -S162001_bit_2 -S162001_bit_1 -S162001_bit0 -S162001_bit1 S162001_bit2 -S162001_bit3 -S162001_bit4 S162001_bit5 S162001_bit6 S162001_bit7 -S162001_bit8 -S162001_bit9 -S162001_bit10 -S162001_bit11 -S162001_bit12 -S172022_bit_7 -S172022_bit_6 -S172022_bit_5 -S172022_bit_4 -S172022_bit_3 -S172022_bit_2 -S172022_bit_1 -S172022_bit0 -S172022_bit1 S172022_bit2 -S172022_bit3 -S172022_bit4 S172022_bit5 -S172022_bit6 -S172022_bit7 -S172022_bit8 -S172022_bit9 -S172022_bit10 -S172022_bit11 -S172022_bit12 -S182024_bit_7 -S182024_bit_6 -S182024_bit_5 -S182024_bit_4 -S182024_bit_3 -S182024_bit_2 -S182024_bit_1 -S182024_bit0 S182024_bit1 S182024_bit2 -S182024_bit3 S182024_bit4 S182024_bit5 -S182024_bit6 -S182024_bit7 -S182024_bit8 -S182024_bit9 -S182024_bit10 -S182024_bit11 -S182024_bit12 -S190122_bit_7 -S190122_bit_6 -S190122_bit_5 -S190122_bit_4 -S190122_bit_3 -S190122_bit_2 -S190122_bit_1 -S190122_bit0 -S190122_bit1 S190122_bit2 -S190122_bit3 -S190122_bit4 S190122_bit5 -S190122_bit6 -S190122_bit7 -S190122_bit8 S190122_bit9 -S190122_bit10 -S190122_bit11 -S190122_bit12 -S020820_bit_7 -S020820_bit_6 -S020820_bit_5 -S020820_bit_4 -S020820_bit_3 -S020820_bit_2 -S020820_bit_1 -S020820_bit0 -S020820_bit1 -S020820_bit2 -S020820_bit3 S020820_bit4 -S020820_bit5 -S020820_bit6 -S020820_bit7 -S020820_bit8 -S020820_bit9 -S020820_bit10 -S020820_bit11 -S020820_bit12 -S200105_bit_7 -S200105_bit_6 -S200105_bit_5 -S200105_bit_4 -S200105_bit_3 -S200105_bit_2 -S200105_bit_1 S200105_bit0 S200105_bit1 -S200105_bit2 -S200105_bit3 -S200105_bit4 S200105_bit5 S200105_bit6 -S200105_bit7 S200105_bit8 -S200105_bit9 -S200105_bit10 -S200105_bit11 -S200105_bit12 -S210102_bit_7 -S210102_bit_6 -S210102_bit_5 -S210102_bit_4 -S210102_bit_3 -S210102_bit_2 -S210102_bit_1 -S210102_bit0 -S210102_bit1 -S210102_bit2 S210102_bit3 S210102_bit4 S210102_bit5 S210102_bit6 -S210102_bit7 -S210102_bit8 -S210102_bit9 -S210102_bit10 -S210102_bit11 -S210102_bit12 -S220129_bit_7 -S220129_bit_6 -S220129_bit_5 -S220129_bit_4 -S220129_bit_3 -S220129_bit_2 -S220129_bit_1 -S220129_bit0 S220129_bit1 -S220129_bit2 -S220129_bit3 -S220129_bit4 -S220129_bit5 -S220129_bit6 -S220129_bit7 -S220129_bit8 S220129_bit9 -S220129_bit10 -S220129_bit11 -S220129_bit12 -S230104_bit_7 -S230104_bit_6 -S230104_bit_5 -S230104_bit_4 -S230104_bit_3 -S230104_bit_2 -S230104_bit_1 -S230104_bit0 S230104_bit1 S230104_bit2 -S230104_bit3 -S230104_bit4 -S230104_bit5 -S230104_bit6 -S230104_bit7 -S230104_bit8 S230104_bit9 -S230104_bit10 -S230104_bit11 -S230104_bit12 -S240148_bit_7 -S240148_bit_6 -S240148_bit_5 -S240148_bit_4 -S240148_bit_3 -S240148_bit_2 -S240148_bit_1 -S240148_bit0 -S240148_bit1 -S240148_bit2 S240148_bit3 -S240148_bit4 -S240148_bit5 -S240148_bit6 -S240148_bit7 S240148_bit8 -S240148_bit9 -S240148_bit10 -S240148_bit11 -S240148_bit12 -S252123_bit_7 -S252123_bit_6 -S252123_bit_5 -S252123_bit_4 -S252123_bit_3 -S252123_bit_2 -S252123_bit_1 -S252123_bit0 -S252123_bit1 S252123_bit2 -S252123_bit3 -S252123_bit4 -S252123_bit5 -S252123_bit6 S252123_bit7 -S252123_bit8 -S252123_bit9 -S252123_bit10 -S252123_bit11 -S252123_bit12 -S260506_bit_7 -S260506_bit_6 -S260506_bit_5 -S260506_bit_4 -S260506_bit_3 -S260506_bit_2 -S260506_bit_1 -S260506_bit0 -S260506_bit1 -S260506_bit2 -S260506_bit3 -S260506_bit4 -S260506_bit5 S260506_bit6 -S260506_bit7 S260506_bit8 -S260506_bit9 -S260506_bit10 -S260506_bit11 -S260506_bit12 -S270529_bit_7 -S270529_bit_6 -S270529_bit_5 -S270529_bit_4 -S270529_bit_3 -S270529_bit_2 -S270529_bit_1 -S270529_bit0 S270529_bit1 -S270529_bit2 S270529_bit3 -S270529_bit4 -S270529_bit5 S270529_bit6 -S270529_bit7 -S270529_bit8 -S270529_bit9 -S270529_bit10 -S270529_bit11 -S270529_bit12 -S280504_bit_7 -S280504_bit_6 -S280504_bit_5 -S280504_bit_4 -S280504_bit_3 -S280504_bit_2 -S280504_bit_1 S280504_bit0 -S280504_bit1 S280504_bit2 -S280504_bit3 -S280504_bit4 -S280504_bit5 -S280504_bit6 -S280504_bit7 -S280504_bit8 -S280504_bit9 -S280504_bit10 -S280504_bit11 -S280504_bit12 -S290548_bit_7 -S290548_bit_6 -S290548_bit_5 -S290548_bit_4 -S290548_bit_3 -S290548_bit_2 -S290548_bit_1 -S290548_bit0 -S290548_bit1 S290548_bit2 S290548_bit3 S290548_bit4 S290548_bit5 -S290548_bit6 -S290548_bit7 -S290548_bit8 -S290548_bit9 -S290548_bit10 -S290548_bit11 -S290548_bit12 -S030821_bit_7 -S030821_bit_6 -S030821_bit_5 -S030821_bit_4 -S030821_bit_3 -S030821_bit_2 -S030821_bit_1 S030821_bit0 -S030821_bit1 S030821_bit2 -S030821_bit3 -S030821_bit4 -S030821_bit5 -S030821_bit6 S030821_bit7 -S030821_bit8 -S030821_bit9 -S030821_bit10 -S030821_bit11 -S030821_bit12 -S302426_bit_7 -S302426_bit_6 -S302426_bit_5 -S302426_bit_4 -S302426_bit_3 -S302426_bit_2 -S302426_bit_1 -S302426_bit0 S302426_bit1 S302426_bit2 -S302426_bit3 -S302426_bit4 -S302426_bit5 S302426_bit6 -S302426_bit7 -S302426_bit8 -S302426_bit9 -S302426_bit10 -S302426_bit11 -S302426_bit12 -S312402_bit_7 -S312402_bit_6 -S312402_bit_5 -S312402_bit_4 -S312402_bit_3 -S312402_bit_2 -S312402_bit_1 -S312402_bit0 -S312402_bit1 -S312402_bit2 -S312402_bit3 S312402_bit4 S312402_bit5 -S312402_bit6 -S312402_bit7 S312402_bit8 -S312402_bit9 -S312402_bit10 -S312402_bit11 -S312402_bit12 -S322428_bit_7 -S322428_bit_6 -S322428_bit_5 -S322428_bit_4 -S322428_bit_3 -S322428_bit_2 -S322428_bit_1 S322428_bit0 -S322428_bit1 S322428_bit2 S322428_bit3 -S322428_bit4 -S322428_bit5 -S322428_bit6 -S322428_bit7 -S322428_bit8 S322428_bit9 -S322428_bit10 -S322428_bit11 -S322428_bit12 -S332526_bit_7 -S332526_bit_6 -S332526_bit_5 -S332526_bit_4 -S332526_bit_3 -S332526_bit_2 -S332526_bit_1 -S332526_bit0 -S332526_bit1 S332526_bit2 S332526_bit3 -S332526_bit4 -S332526_bit5 -S332526_bit6 S332526_bit7 -S332526_bit8 -S332526_bit9 -S332526_bit10 -S332526_bit11 -S332526_bit12 -S342530_bit_7 -S342530_bit_6 -S342530_bit_5 -S342530_bit_4 -S342530_bit_3 -S342530_bit_2 -S342530_bit_1 -S342530_bit0 -S342530_bit1 -S342530_bit2 -S342530_bit3 -S342530_bit4 -S342530_bit5 S342530_bit6 -S342530_bit7 -S342530_bit8 -S342530_bit9 -S342530_bit10 -S342530_bit11 -S342530_bit12 -S350206_bit_7 -S350206_bit_6 -S350206_bit_5 -S350206_bit_4 -S350206_bit_3 -S350206_bit_2 -S350206_bit_1 -S350206_bit0 -S350206_bit1 S350206_bit2 S350206_bit3 S350206_bit4 S350206_bit5 -S350206_bit6 -S350206_bit7 -S350206_bit8 -S350206_bit9 -S350206_bit10 -S350206_bit11 -S350206_bit12 -S360231_bit_7 -S360231_bit_6 -S360231_bit_5 -S360231_bit_4 -S360231_bit_3 -S360231_bit_2 -S360231_bit_1 -S360231_bit0 -S360231_bit1 -S360231_bit2 -S360231_bit3 -S360231_bit4 S360231_bit5 S360231_bit6 -S360231_bit7 S360231_bit8 -S360231_bit9 -S360231_bit10 -S360231_bit11 -S360231_bit12 -S372706_bit_7 -S372706_bit_6 -S372706_bit_5 -S372706_bit_4 -S372706_bit_3 -S372706_bit_2 -S372706_bit_1 -S372706_bit0 -S372706_bit1 -S372706_bit2 S372706_bit3 -S372706_bit4 -S372706_bit5 S372706_bit6 -S372706_bit7 -S372706_bit8 -S372706_bit9 -S372706_bit10 -S372706_bit11 -S372706_bit12 -S382704_bit_7 -S382704_bit_6 -S382704_bit_5 -S382704_bit_4 -S382704_bit_3 -S382704_bit_2 -S382704_bit_1 S382704_bit0 -S382704_bit1 -S382704_bit2 S382704_bit3 S382704_bit4 -S382704_bit5 -S382704_bit6 S382704_bit7 S382704_bit8 -S382704_bit9 -S382704_bit10 -S382704_bit11 -S382704_bit12 -S392743_bit_7 -S392743_bit_6 -S392743_bit_5 -S392743_bit_4 -S392743_bit_3 -S392743_bit_2 -S392743_bit_1 -S392743_bit0 -S392743_bit1 S392743_bit2 -S392743_bit3 S392743_bit4 S392743_bit5 S392743_bit6 S392743_bit7 -S392743_bit8 -S392743_bit9 -S392743_bit10 -S392743_bit11 -S392743_bit12 -S040826_bit_7 -S040826_bit_6 -S040826_bit_5 -S040826_bit_4 -S040826_bit_3 -S040826_bit_2 -S040826_bit_1 -S040826_bit0 S040826_bit1 -S040826_bit2 S040826_bit3 S040826_bit4 -S040826_bit5 S040826_bit6 -S040826_bit7 -S040826_bit8 -S040826_bit9 -S040826_bit10 -S040826_bit11 -S040826_bit12 -S402830_bit_7 -S402830_bit_6 -S402830_bit_5 -S402830_bit_4 -S402830_bit_3 -S402830_bit_2 -S402830_bit_1 -S402830_bit0 S402830_bit1 -S402830_bit2 S402830_bit3 -S402830_bit4 -S402830_bit5 S402830_bit6 -S402830_bit7 -S402830_bit8 -S402830_bit9 -S402830_bit10 -S402830_bit11 -S402830_bit12 -S410604_bit_7 -S410604_bit_6 -S410604_bit_5 -S410604_bit_4 -S410604_bit_3 -S410604_bit_2 -S410604_bit_1 -S410604_bit0 -S410604_bit1 -S410604_bit2 S410604_bit3 S410604_bit4 -S410604_bit5 -S410604_bit6 -S410604_bit7 -S410604_bit8 -S410604_bit9 -S410604_bit10 -S410604_bit11 -S410604_bit12 -S422948_bit_7 -S422948_bit_6 -S422948_bit_5 -S422948_bit_4 -S422948_bit_3 -S422948_bit_2 -S422948_bit_1 -S422948_bit0 -S422948_bit1 S422948_bit2 S422948_bit3 -S422948_bit4 -S422948_bit5 -S422948_bit6 -S422948_bit7 S422948_bit8 -S422948_bit9 -S422948_bit10 -S422948_bit11 -S422948_bit12 -S433141_bit_7 -S433141_bit_6 -S433141_bit_5 -S433141_bit_4 -S433141_bit_3 -S433141_bit_2 -S433141_bit_1 S433141_bit0 S433141_bit1 -S433141_bit2 -S433141_bit3 -S433141_bit4 S433141_bit5 -S433141_bit6 -S433141_bit7 -S433141_bit8 -S433141_bit9 -S433141_bit10 -S433141_bit11 -S433141_bit12 -S444041_bit_7 -S444041_bit_6 -S444041_bit_5 -S444041_bit_4 -S444041_bit_3 -S444041_bit_2 -S444041_bit_1 -S444041_bit0 S444041_bit1 -S444041_bit2 -S444041_bit3 -S444041_bit4 -S444041_bit5 -S444041_bit6 -S444041_bit7 S444041_bit8 -S444041_bit9 -S444041_bit10 -S444041_bit11 -S444041_bit12 -S050923_bit_7 -S050923_bit_6 -S050923_bit_5 -S050923_bit_4 -S050923_bit_3 -S050923_bit_2 -S050923_bit_1 S050923_bit0 S050923_bit1 -S050923_bit2 -S050923_bit3 -S050923_bit4 -S050923_bit5 S0
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/21282/stat): 21282 (minisat+_script) R 21281 21282 20115 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855598326 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/21282/statm): 174 3 169 147 0 27 0 [pid=21282] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=21283 New process pid=21284 New process pid=21285 execve syscall for /bin/sed executable One traced child (pid=21284) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=21285) exited with status: 0 One traced child (pid=21283) exited with status: 0 New process pid=21286 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-fiber.opb [startup+10.0028 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 2447 0 0 0 973 10 0 0 25 0 1 0 1855598331 10747904 2350 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 2624 2350 145 145 0 2479 0 [pid=21286] vsize: 10496 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 12620 [startup+20.0035 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 2637 0 0 0 1970 12 0 0 25 0 1 0 1855598331 11550720 2540 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 2820 2540 145 145 0 2675 0 [pid=21286] vsize: 11280 Current children cumulated CPU time (s) 19.84 Current children cumulated vsize (Kb) 13404 [startup+30.0041 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 2809 0 0 0 2967 12 0 0 25 0 1 0 1855598331 12214272 2712 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 2982 2712 145 145 0 2837 0 [pid=21286] vsize: 11928 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 14052 [startup+40.0048 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 3022 0 0 0 3964 14 0 0 25 0 1 0 1855598331 13172736 2925 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 3216 2925 145 145 0 3071 0 [pid=21286] vsize: 12864 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 14988 [startup+50.0055 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 3236 0 0 0 4961 15 0 0 25 0 1 0 1855598331 14004224 3139 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 3419 3139 145 145 0 3274 0 [pid=21286] vsize: 13676 Current children cumulated CPU time (s) 49.78 Current children cumulated vsize (Kb) 15800 [startup+60.0062 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 5952 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 59.74 Current children cumulated vsize (Kb) 19356 [startup+70.0069 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 6952 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219944 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 69.74 Current children cumulated vsize (Kb) 19356 [startup+80.0075 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 7952 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220032 134600167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 79.74 Current children cumulated vsize (Kb) 19356 [startup+90.0092 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 8953 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219772 134677081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 89.75 Current children cumulated vsize (Kb) 19356 [startup+100.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 9953 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 99.75 Current children cumulated vsize (Kb) 19356 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 10953 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 109.75 Current children cumulated vsize (Kb) 19356 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 11954 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 119.76 Current children cumulated vsize (Kb) 19356 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 12954 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220108 134676610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 129.76 Current children cumulated vsize (Kb) 19356 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 13954 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220556 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 139.76 Current children cumulated vsize (Kb) 19356 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 14954 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134677330 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 149.76 Current children cumulated vsize (Kb) 19356 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 15954 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220192 134518662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 159.76 Current children cumulated vsize (Kb) 19356 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 16955 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 169.77 Current children cumulated vsize (Kb) 19356 [startup+180.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 17955 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219968 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 179.77 Current children cumulated vsize (Kb) 19356 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 18955 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220320 134676317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 189.77 Current children cumulated vsize (Kb) 19356 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 19955 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134677320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 199.77 Current children cumulated vsize (Kb) 19356 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 20956 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219772 134677081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 209.78 Current children cumulated vsize (Kb) 19356 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 21956 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 219.78 Current children cumulated vsize (Kb) 19356 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 22956 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 229.78 Current children cumulated vsize (Kb) 19356 [startup+240.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 23956 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219768 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 239.78 Current children cumulated vsize (Kb) 19356 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 24956 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220496 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 249.78 Current children cumulated vsize (Kb) 19356 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 25957 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220496 134677007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 259.79 Current children cumulated vsize (Kb) 19356 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 26957 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 269.79 Current children cumulated vsize (Kb) 19356 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 27957 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 279.79 Current children cumulated vsize (Kb) 19356 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 28957 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220192 134677147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 289.79 Current children cumulated vsize (Kb) 19356 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 29957 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 299.79 Current children cumulated vsize (Kb) 19356 [startup+310.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 30958 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 309.8 Current children cumulated vsize (Kb) 19356 [startup+320.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 31958 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134677354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 319.8 Current children cumulated vsize (Kb) 19356 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 32958 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220120 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 329.8 Current children cumulated vsize (Kb) 19356 [startup+340.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 33958 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 339.8 Current children cumulated vsize (Kb) 19356 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 34959 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 349.81 Current children cumulated vsize (Kb) 19356 [startup+360.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 35959 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134676480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 359.81 Current children cumulated vsize (Kb) 19356 [startup+370.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 36959 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 369.81 Current children cumulated vsize (Kb) 19356 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 37959 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134600204 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 379.81 Current children cumulated vsize (Kb) 19356 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 38959 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220816 134676341 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 389.81 Current children cumulated vsize (Kb) 19356 [startup+400.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 39960 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220672 134676273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 399.82 Current children cumulated vsize (Kb) 19356 [startup+410.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 40960 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134676598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 409.82 Current children cumulated vsize (Kb) 19356 [startup+420.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 41960 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 419.82 Current children cumulated vsize (Kb) 19356 [startup+430.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 42960 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220380 134676382 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 429.82 Current children cumulated vsize (Kb) 19356 [startup+440.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 43961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 439.83 Current children cumulated vsize (Kb) 19356 [startup+450.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 44961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 449.83 Current children cumulated vsize (Kb) 19356 [startup+460.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 45961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220296 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 459.83 Current children cumulated vsize (Kb) 19356 [startup+470.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 46961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220976 134676465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 469.83 Current children cumulated vsize (Kb) 19356 [startup+480.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 47961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220292 134676335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 479.83 Current children cumulated vsize (Kb) 19356 [startup+490.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 48961 20 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134677271 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 489.83 Current children cumulated vsize (Kb) 19356 [startup+500.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 49962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220896 134518676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 499.85 Current children cumulated vsize (Kb) 19356 [startup+510.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 50962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 509.85 Current children cumulated vsize (Kb) 19356 [startup+520.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 51962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134676586 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 519.85 Current children cumulated vsize (Kb) 19356 [startup+530.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 52962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 529.85 Current children cumulated vsize (Kb) 19356 [startup+540.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 53962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220284 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 539.85 Current children cumulated vsize (Kb) 19356 [startup+550.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 54962 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 549.85 Current children cumulated vsize (Kb) 19356 [startup+560.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 55963 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134677366 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 559.86 Current children cumulated vsize (Kb) 19356 [startup+570.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 56963 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221024 134676376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 569.86 Current children cumulated vsize (Kb) 19356 [startup+580.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 57963 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219924 134676608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 579.86 Current children cumulated vsize (Kb) 19356 [startup+590.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 58963 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 589.86 Current children cumulated vsize (Kb) 19356 [startup+600.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 59964 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 599.87 Current children cumulated vsize (Kb) 19356 [startup+610.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 60964 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 609.87 Current children cumulated vsize (Kb) 19356 [startup+620.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 61964 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 619.87 Current children cumulated vsize (Kb) 19356 [startup+630.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 62964 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 629.87 Current children cumulated vsize (Kb) 19356 [startup+640.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 63965 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 639.88 Current children cumulated vsize (Kb) 19356 [startup+650.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 64965 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 649.88 Current children cumulated vsize (Kb) 19356 [startup+660.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 65965 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134677239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 659.88 Current children cumulated vsize (Kb) 19356 [startup+670.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 66965 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 669.88 Current children cumulated vsize (Kb) 19356 [startup+680.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 67966 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134600283 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 679.89 Current children cumulated vsize (Kb) 19356 [startup+690.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 68966 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 689.89 Current children cumulated vsize (Kb) 19356 [startup+700.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 69966 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134676471 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 699.89 Current children cumulated vsize (Kb) 19356 [startup+710.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 70966 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 709.89 Current children cumulated vsize (Kb) 19356 [startup+720.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 71966 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221280 134600204 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 719.89 Current children cumulated vsize (Kb) 19356 [startup+730.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 72967 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 729.9 Current children cumulated vsize (Kb) 19356 [startup+740.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 73967 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220320 134677021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 739.9 Current children cumulated vsize (Kb) 19356 [startup+750.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 74967 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 749.9 Current children cumulated vsize (Kb) 19356 [startup+760.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 75967 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221104 134600310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 759.9 Current children cumulated vsize (Kb) 19356 [startup+770.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 76967 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 769.9 Current children cumulated vsize (Kb) 19356 [startup+780.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 77968 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134677310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 779.91 Current children cumulated vsize (Kb) 19356 [startup+790.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 78968 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220564 134600159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 789.91 Current children cumulated vsize (Kb) 19356 [startup+800.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 79968 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 799.91 Current children cumulated vsize (Kb) 19356 [startup+810.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 80968 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 809.91 Current children cumulated vsize (Kb) 19356 [startup+820.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 81969 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221256 134676241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 819.92 Current children cumulated vsize (Kb) 19356 [startup+830.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 82969 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677366 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 829.92 Current children cumulated vsize (Kb) 19356 [startup+840.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 83969 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134599974 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 839.92 Current children cumulated vsize (Kb) 19356 [startup+850.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 84969 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221219792 134676273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 849.92 Current children cumulated vsize (Kb) 19356 [startup+860.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 85970 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 859.93 Current children cumulated vsize (Kb) 19356 [startup+870.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 86970 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 869.93 Current children cumulated vsize (Kb) 19356 [startup+880.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 87970 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220736 134600167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 879.93 Current children cumulated vsize (Kb) 19356 [startup+890.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 88970 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220284 134676610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 889.93 Current children cumulated vsize (Kb) 19356 [startup+900.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 89971 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 899.94 Current children cumulated vsize (Kb) 19356 [startup+910.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 90971 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 909.94 Current children cumulated vsize (Kb) 19356 [startup+920.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 91971 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134676489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 919.94 Current children cumulated vsize (Kb) 19356 [startup+930.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 92971 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 929.94 Current children cumulated vsize (Kb) 19356 [startup+940.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 93971 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 939.94 Current children cumulated vsize (Kb) 19356 [startup+950.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 94972 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221280 134677354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 949.95 Current children cumulated vsize (Kb) 19356 [startup+960.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 95972 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220576 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 959.95 Current children cumulated vsize (Kb) 19356 [startup+970.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 96972 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221072 134518677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 969.95 Current children cumulated vsize (Kb) 19356 [startup+980.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 97972 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220640 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 979.95 Current children cumulated vsize (Kb) 19356 [startup+990.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 98973 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220400 134677351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 989.96 Current children cumulated vsize (Kb) 19356 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 99973 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221200 134676999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 999.96 Current children cumulated vsize (Kb) 19356 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 100973 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221280 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1009.96 Current children cumulated vsize (Kb) 19356 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 101973 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1019.96 Current children cumulated vsize (Kb) 19356 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 102974 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1029.97 Current children cumulated vsize (Kb) 19356 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 103974 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220048 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1039.97 Current children cumulated vsize (Kb) 19356 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 104974 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1049.97 Current children cumulated vsize (Kb) 19356 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 105974 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220652 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1059.97 Current children cumulated vsize (Kb) 19356 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 106975 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221276 134600233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1069.98 Current children cumulated vsize (Kb) 19356 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 107975 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134600175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1079.98 Current children cumulated vsize (Kb) 19356 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 108975 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1089.98 Current children cumulated vsize (Kb) 19356 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 109975 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220224 134676552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1099.98 Current children cumulated vsize (Kb) 19356 [startup+1110.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 110976 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220916 134600238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1109.99 Current children cumulated vsize (Kb) 19356 [startup+1120.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 111976 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134676598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1119.99 Current children cumulated vsize (Kb) 19356 [startup+1130.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 112976 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1129.99 Current children cumulated vsize (Kb) 19356 [startup+1140.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 113976 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220496 134677069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1139.99 Current children cumulated vsize (Kb) 19356 [startup+1150.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 114976 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1149.99 Current children cumulated vsize (Kb) 19356 [startup+1160.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 115977 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220368 134780892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1160 Current children cumulated vsize (Kb) 19356 [startup+1170.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 116977 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220752 134599974 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1170 Current children cumulated vsize (Kb) 19356 [startup+1180.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 117977 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221221200 134676251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1180 Current children cumulated vsize (Kb) 19356 [startup+1190.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 118977 21 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220812 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1190 Current children cumulated vsize (Kb) 19356 [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 119977 22 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220832 134677078 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1200.01 Current children cumulated vsize (Kb) 19356 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 21286 Raw data (/proc/21282/stat): 21282 (minisat+_script) S 21281 21282 20115 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855598326 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/21282/statm): 531 226 485 147 0 384 0 [pid=21282] vsize: 2124 Raw data (/proc/21286/stat): 21286 (minisat+_64-bit) R 21282 21282 20115 0 -1 0 4496 0 0 0 119977 22 0 0 25 0 1 0 1855598331 17645568 4026 4294967295 134512640 135094434 3221224432 3221220928 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21286/statm): 4308 4026 145 145 0 4163 0 [pid=21286] vsize: 17232 Current children cumulated CPU time (s) 1200.01 Current children cumulated vsize (Kb) 19356 Sending SIGTERM to -21282 Sleeping 2 seconds One traced child (pid=21282) ended because it received signal 15 (SIGTERM) One traced child (pid=21286) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1200.1 CPU time (s): 1200.01 CPU user time (s): 1199.78 CPU system time (s): 0.229965 CPU usage (%): 99.9931 Max. virtual memory (cumulated for all children) (Kb): 19356
ERROR: no interpretation found !