Name | submitted/een/normalized-p2756.opb |
MD5SUM | f3d955cf36894e7107b7f25ccaa97360 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3834 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2166 |
Biggest coefficient in the objective function | 11000 |
Number of bits for the biggest coefficient in the objective function | 14 |
Sum of the numbers in the objective function | 321831 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 11000 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 321831 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.06 |
Number of variables | 2734 |
Total number of constraints | 738 |
Number of constraints which are clauses | 132 |
Number of constraints which are cardinality constraints (but not clauses) | 220 |
Number of constraints which are nor clauses,nor cardinality constraints | 386 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 535 |
LAUNCH ON wulflinc25 THE 2005-09-18 18:25:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2622 boxname=wulflinc25 idbench=278 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f3d955cf36894e7107b7f25ccaa97360 /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb IDLAUNCH: 2622 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 916740 kB Buffers: 35336 kB Cached: 55704 kB SwapCached: 896 kB Active: 66060 kB Inactive: 27696 kB HighTotal: 131008 kB HighFree: 73864 kB LowTotal: 903652 kB LowFree: 842876 kB SwapTotal: 2097892 kB SwapFree: 2096496 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 18596 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:45:14 (client local time) WITH STATUS 10 IN 1209.09 SECONDS stats: 2622 7 1209.09 10
c Parsing PB file... c Converting 738 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: # c -- Clauses(.)/Splits(s): ....................................................................................................................................s..ssssssssss.s.sssssssssss c ---[ 627]---> BDD-cost: 3 c ---[ 626]---> BDD-cost: 3 c ---[ 625]---> BDD-cost: 3 c ---[ 624]---> BDD-cost: 3 c ---[ 623]---> BDD-cost: 3 c ---[ 622]---> BDD-cost: 3 c ---[ 621]---> BDD-cost: 3 c ---[ 620]---> BDD-cost: 3 c ---[ 619]---> BDD-cost: 3 c ---[ 618]---> BDD-cost: 3 c ---[ 617]---> BDD-cost: 3 c ---[ 616]---> BDD-cost: 3 c ---[ 615]---> BDD-cost: 3 c ---[ 614]---> BDD-cost: 3 c ---[ 613]---> BDD-cost: 3 c ---[ 612]---> BDD-cost: 3 c ---[ 611]---> BDD-cost: 3 c ---[ 610]---> BDD-cost: 3 c ---[ 609]---> BDD-cost: 3 c ---[ 608]---> BDD-cost: 3 c ---[ 607]---> BDD-cost: 3 c ---[ 606]---> BDD-cost: 3 c ---[ 605]---> BDD-cost: 3 c ---[ 604]---> BDD-cost: 3 c ---[ 603]---> BDD-cost: 3 c ---[ 602]---> BDD-cost: 3 c ---[ 601]---> BDD-cost: 3 c ---[ 600]---> BDD-cost: 3 c ---[ 599]---> BDD-cost: 3 c ---[ 598]---> BDD-cost: 3 c ---[ 597]---> BDD-cost: 3 c ---[ 596]---> BDD-cost: 3 c ---[ 595]---> BDD-cost: 3 c ---[ 594]---> BDD-cost: 3 c ---[ 593]---> BDD-cost: 3 c ---[ 592]---> BDD-cost: 3 c ---[ 591]---> BDD-cost: 3 c ---[ 590]---> BDD-cost: 3 c ---[ 589]---> BDD-cost: 3 c ---[ 588]---> BDD-cost: 3 c ---[ 587]---> BDD-cost: 3 c ---[ 586]---> BDD-cost: 3 c ---[ 585]---> BDD-cost: 3 c ---[ 584]---> BDD-cost: 5 c ---[ 583]---> BDD-cost: 5 c ---[ 582]---> BDD-cost: 5 c ---[ 581]---> BDD-cost: 5 c ---[ 580]---> BDD-cost: 5 c ---[ 579]---> BDD-cost: 5 c ---[ 578]---> BDD-cost: 5 c ---[ 577]---> BDD-cost: 5 c ---[ 576]---> BDD-cost: 5 c ---[ 575]---> BDD-cost: 5 c ---[ 574]---> BDD-cost: 5 c ---[ 573]---> BDD-cost: 5 c ---[ 572]---> BDD-cost: 5 c ---[ 571]---> BDD-cost: 5 c ---[ 570]---> BDD-cost: 5 c ---[ 569]---> BDD-cost: 5 c ---[ 568]---> BDD-cost: 5 c ---[ 567]---> BDD-cost: 5 c ---[ 566]---> BDD-cost: 5 c ---[ 565]---> BDD-cost: 5 c ---[ 564]---> BDD-cost: 5 c ---[ 563]---> BDD-cost: 5 c ---[ 562]---> BDD-cost: 5 c ---[ 561]---> BDD-cost: 5 c ---[ 560]---> BDD-cost: 5 c ---[ 559]---> BDD-cost: 5 c ---[ 558]---> BDD-cost: 5 c ---[ 557]---> BDD-cost: 5 c ---[ 556]---> BDD-cost: 5 c ---[ 555]---> BDD-cost: 5 c ---[ 554]---> BDD-cost: 5 c ---[ 553]---> BDD-cost: 5 c ---[ 552]---> BDD-cost: 5 c ---[ 551]---> BDD-cost: 5 c ---[ 550]---> BDD-cost: 5 c ---[ 549]---> BDD-cost: 5 c ---[ 548]---> BDD-cost: 5 c ---[ 547]---> BDD-cost: 5 c ---[ 546]---> BDD-cost: 5 c ---[ 545]---> BDD-cost: 5 c ---[ 544]---> BDD-cost: 5 c ---[ 543]---> BDD-cost: 5 c ---[ 542]---> BDD-cost: 5 c ---[ 541]---> BDD-cost: 5 c ---[ 540]---> BDD-cost: 5 c ---[ 539]---> BDD-cost: 5 c ---[ 538]---> BDD-cost: 5 c ---[ 537]---> BDD-cost: 5 c ---[ 536]---> BDD-cost: 5 c ---[ 535]---> BDD-cost: 5 c ---[ 534]---> BDD-cost: 5 c ---[ 533]---> BDD-cost: 5 c ---[ 532]---> BDD-cost: 5 c ---[ 531]---> BDD-cost: 5 c ---[ 530]---> BDD-cost: 5 c ---[ 529]---> BDD-cost: 5 c ---[ 528]---> BDD-cost: 5 c ---[ 527]---> BDD-cost: 5 c ---[ 526]---> BDD-cost: 5 c ---[ 525]---> BDD-cost: 5 c ---[ 524]---> BDD-cost: 5 c ---[ 523]---> BDD-cost: 5 c ---[ 522]---> BDD-cost: 5 c ---[ 521]---> BDD-cost: 5 c ---[ 520]---> BDD-cost: 5 c ---[ 519]---> BDD-cost: 5 c ---[ 518]---> BDD-cost: 5 c ---[ 517]---> BDD-cost: 5 c ---[ 516]---> BDD-cost: 5 c ---[ 515]---> BDD-cost: 5 c ---[ 514]---> BDD-cost: 5 c ---[ 513]---> BDD-cost: 5 c ---[ 512]---> BDD-cost: 5 c ---[ 511]---> BDD-cost: 5 c ---[ 510]---> BDD-cost: 5 c ---[ 509]---> BDD-cost: 5 c ---[ 508]---> BDD-cost: 5 c ---[ 507]---> BDD-cost: 5 c ---[ 506]---> BDD-cost: 5 c ---[ 505]---> BDD-cost: 5 c ---[ 504]---> BDD-cost: 5 c ---[ 503]---> BDD-cost: 5 c ---[ 502]---> BDD-cost: 5 c ---[ 501]---> BDD-cost: 5 c ---[ 500]---> BDD-cost: 5 c ---[ 499]---> BDD-cost: 5 c ---[ 498]---> BDD-cost: 5 c ---[ 497]---> BDD-cost: 5 c ---[ 496]---> BDD-cost: 5 c ---[ 495]---> BDD-cost: 5 c ---[ 494]---> BDD-cost: 5 c ---[ 493]---> BDD-cost: 5 c ---[ 492]---> BDD-cost: 5 c ---[ 491]---> BDD-cost: 5 c ---[ 490]---> BDD-cost: 5 c ---[ 489]---> BDD-cost: 5 c ---[ 488]---> BDD-cost: 5 c ---[ 487]---> BDD-cost: 5 c ---[ 486]---> BDD-cost: 5 c ---[ 485]---> BDD-cost: 5 c ---[ 484]---> BDD-cost: 5 c ---[ 483]---> BDD-cost: 5 c ---[ 482]---> BDD-cost: 5 c ---[ 481]---> BDD-cost: 5 c ---[ 480]---> BDD-cost: 5 c ---[ 479]---> BDD-cost: 5 c ---[ 478]---> BDD-cost: 5 c ---[ 477]---> BDD-cost: 5 c ---[ 476]---> BDD-cost: 5 c ---[ 475]---> BDD-cost: 5 c ---[ 474]---> BDD-cost: 5 c ---[ 473]---> BDD-cost: 5 c ---[ 472]---> BDD-cost: 5 c ---[ 471]---> BDD-cost: 5 c ---[ 470]---> BDD-cost: 5 c ---[ 469]---> BDD-cost: 5 c ---[ 468]---> BDD-cost: 5 c ---[ 467]---> BDD-cost: 5 c ---[ 466]---> BDD-cost: 5 c ---[ 465]---> BDD-cost: 5 c ---[ 464]---> BDD-cost: 5 c ---[ 463]---> BDD-cost: 5 c ---[ 462]---> BDD-cost: 5 c ---[ 461]---> BDD-cost: 5 c ---[ 460]---> BDD-cost: 5 c ---[ 459]---> BDD-cost: 5 c ---[ 458]---> BDD-cost: 5 c ---[ 457]---> BDD-cost: 5 c ---[ 456]---> BDD-cost: 5 c ---[ 455]---> BDD-cost: 5 c ---[ 454]---> BDD-cost: 5 c ---[ 453]---> BDD-cost: 5 c ---[ 452]---> BDD-cost: 5 c ---[ 451]---> BDD-cost: 5 c ---[ 450]---> BDD-cost: 5 c ---[ 449]---> BDD-cost: 5 c ---[ 448]---> BDD-cost: 5 c ---[ 447]---> BDD-cost: 5 c ---[ 446]---> BDD-cost: 5 c ---[ 445]---> BDD-cost: 5 c ---[ 444]---> BDD-cost: 5 c ---[ 443]---> BDD-cost: 5 c ---[ 442]---> BDD-cost: 5 c ---[ 441]---> BDD-cost: 5 c ---[ 440]---> BDD-cost: 5 c ---[ 439]---> BDD-cost: 5 c ---[ 438]---> BDD-cost: 5 c ---[ 437]---> BDD-cost: 5 c ---[ 436]---> BDD-cost: 5 c ---[ 435]---> BDD-cost: 5 c ---[ 434]---> BDD-cost: 5 c ---[ 433]---> BDD-cost: 5 c ---[ 432]---> BDD-cost: 5 c ---[ 431]---> BDD-cost: 5 c ---[ 430]---> BDD-cost: 5 c ---[ 429]---> BDD-cost: 5 c ---[ 428]---> BDD-cost: 5 c ---[ 427]---> BDD-cost: 5 c ---[ 426]---> BDD-cost: 5 c ---[ 425]---> BDD-cost: 5 c ---[ 424]---> BDD-cost: 5 c ---[ 423]---> BDD-cost: 5 c ---[ 422]---> BDD-cost: 5 c ---[ 421]---> BDD-cost: 5 c ---[ 420]---> BDD-cost: 5 c ---[ 419]---> BDD-cost: 5 c ---[ 418]---> BDD-cost: 5 c ---[ 417]---> BDD-cost: 5 c ---[ 416]---> BDD-cost: 5 c ---[ 415]---> BDD-cost: 5 c ---[ 414]---> BDD-cost: 5 c ---[ 413]---> BDD-cost: 5 c ---[ 412]---> BDD-cost: 5 c ---[ 411]---> BDD-cost: 5 c ---[ 410]---> BDD-cost: 5 c ---[ 409]---> BDD-cost: 5 c ---[ 408]---> BDD-cost: 5 c ---[ 405]---> BDD-cost: 5 c ---[ 404]---> BDD-cost: 5 c ---[ 403]---> BDD-cost: 11 c ---[ 401]---> BDD-cost: 7 c ---[ 400]---> BDD-cost: 11 c ---[ 399]---> BDD-cost: 8 c ---[ 398]---> BDD-cost: 21 c ---[ 397]---> BDD-cost: 15 c ---[ 396]---> BDD-cost: 11 c ---[ 395]---> BDD-cost: 20 c ---[ 394]---> BDD-cost: 18 c ---[ 393]---> BDD-cost: 18 c ---[ 392]---> BDD-cost: 15 c ---[ 391]---> BDD-cost: 19 c ---[ 389]---> BDD-cost: 19 c ---[ 388]---> BDD-cost: 15 c ---[ 386]---> BDD-cost: 10 c ---[ 385]---> BDD-cost: 22 c ---[ 384]---> BDD-cost: 11 c ---[ 383]---> BDD-cost: 13 c ---[ 382]---> BDD-cost: 17 c ---[ 381]---> BDD-cost: 8 c ---[ 380]---> BDD-cost: 25 c ---[ 379]---> BDD-cost: 3 c ---[ 378]---> BDD-cost: 27 c ---[ 376]---> BDD-cost: 23 c ---[ 375]---> BDD-cost: 2 c ---[ 374]---> BDD-cost: 28 c ---[ 373]---> BDD-cost: 20 c ---[ 372]---> BDD-cost: 9 c ---[ 371]---> BDD-cost: 10 c ---[ 370]---> BDD-cost: 17 c ---[ 369]---> BDD-cost: 13 c ---[ 365]---> BDD-cost: 31 c ---[ 364]---> BDD-cost: 29 c ---[ 363]---> BDD-cost: 34 c ---[ 362]---> BDD-cost: 9 c ---[ 361]---> BDD-cost: 27 c ---[ 360]---> BDD-cost: 36 c ---[ 359]---> BDD-cost: 32 c ---[ 358]---> BDD-cost: 52 c ---[ 357]---> BDD-cost: 12 c ---[ 356]---> BDD-cost: 68 c ---[ 355]---> BDD-cost: 21 c ---[ 354]---> BDD-cost: 74 c ---[ 353]---> BDD-cost: 67 c ---[ 352]---> BDD-cost: 10 c ---[ 351]---> BDD-cost: 19 c ---[ 349]---> BDD-cost: 70 c ---[ 348]---> BDD-cost: 15 c ---[ 347]---> BDD-cost: 35 c ---[ 346]---> BDD-cost: 44 c ---[ 345]---> BDD-cost: 75 c ---[ 344]---> BDD-cost: 37 c ---[ 343]---> BDD-cost: 34 c ---[ 342]---> BDD-cost: 63 c ---[ 341]---> BDD-cost: 48 c ---[ 340]---> BDD-cost: 26 c ---[ 339]---> BDD-cost: 50 c ---[ 337]---> BDD-cost: 15 c ---[ 336]---> BDD-cost: 52 c ---[ 335]---> BDD-cost: 39 c ---[ 334]---> BDD-cost: 61 c ---[ 333]---> BDD-cost: 15 c ---[ 332]---> BDD-cost: 55 c ---[ 331]---> BDD-cost: 18 c ---[ 330]---> BDD-cost: 64 c ---[ 329]---> BDD-cost: 27 c ---[ 328]---> BDD-cost: 37 c ---[ 327]---> BDD-cost: 50 c ---[ 326]---> BDD-cost: 96 c ---[ 325]---> BDD-cost: 35 c ---[ 324]---> BDD-cost: 81 c ---[ 323]---> BDD-cost: 34 c ---[ 322]---> BDD-cost: 34 c ---[ 321]---> BDD-cost: 93 c ---[ 320]---> BDD-cost: 55 c ---[ 319]---> BDD-cost: 56 c ---[ 318]---> BDD-cost: 104 c ---[ 317]---> BDD-cost: 27 c ---[ 316]---> BDD-cost: 10 c ---[ 315]---> BDD-cost: 66 c ---[ 314]---> BDD-cost: 79 c ---[ 313]---> BDD-cost: 19 c ---[ 312]---> BDD-cost: 54 c ---[ 311]---> BDD-cost: 146 c ---[ 310]---> BDD-cost: 93 c ---[ 309]---> BDD-cost: 102 c ---[ 308]---> BDD-cost: 123 c ---[ 307]---> BDD-cost: 65 c ---[ 306]---> BDD-cost: 104 c ---[ 305]---> BDD-cost: 70 c ---[ 304]---> BDD-cost: 109 c ---[ 303]---> BDD-cost: 66 c ---[ 302]---> BDD-cost: 115 c ---[ 301]---> BDD-cost: 13 c ---[ 300]---> BDD-cost: 154 c ---[ 299]---> BDD-cost: 60 c ---[ 298]---> BDD-cost: 112 c ---[ 297]---> BDD-cost: 123 c ---[ 296]---> BDD-cost: 90 c ---[ 295]---> Sorter-cost: 586 Base: 2 2 2 2 2 5 c ---[ 294]---> BDD-cost: 45 c ---[ 293]---> BDD-cost: 76 c ---[ 292]---> BDD-cost: 35 c ---[ 291]---> BDD-cost: 32 c ---[ 290]---> BDD-cost: 145 c ---[ 289]---> BDD-cost: 126 c ---[ 288]---> Sorter-cost: 539 Base: 2 2 2 2 2 2 2 c ---[ 287]---> BDD-cost: 69 c ---[ 286]---> BDD-cost: 131 c ---[ 285]---> BDD-cost: 109 c ---[ 284]---> BDD-cost: 107 c ---[ 283]---> BDD-cost: 67 c ---[ 282]---> BDD-cost: 87 c ---[ 281]---> BDD-cost: 59 c ---[ 280]---> BDD-cost: 87 c ---[ 279]---> BDD-cost: 133 c ---[ 278]---> BDD-cost: 109 c ---[ 277]---> BDD-cost: 82 c ---[ 276]---> BDD-cost: 43 c ---[ 275]---> BDD-cost: 82 c ---[ 274]---> BDD-cost: 87 c ---[ 273]---> BDD-cost: 132 c ---[ 272]---> BDD-cost: 38 c ---[ 271]---> BDD-cost: 19 c ---[ 270]---> BDD-cost: 15 c ---[ 269]---> BDD-cost: 159 c ---[ 268]---> BDD-cost: 68 c ---[ 267]---> BDD-cost: 104 c ---[ 266]---> BDD-cost: 62 c ---[ 265]---> BDD-cost: 101 c ---[ 264]---> BDD-cost: 21 c ---[ 263]---> BDD-cost: 91 c ---[ 262]---> BDD-cost: 15 c ---[ 261]---> BDD-cost: 31 c ---[ 260]---> BDD-cost: 52 c ---[ 259]---> BDD-cost: 148 c ---[ 258]---> BDD-cost: 37 c ---[ 257]---> Sorter-cost: 670 Base: 2 2 2 2 2 5 c ---[ 256]---> BDD-cost: 87 c ---[ 255]---> BDD-cost: 111 c ---[ 254]---> BDD-cost: 83 c ---[ 253]---> BDD-cost: 22 c ---[ 252]---> Sorter-cost: 555 Base: 2 2 2 2 2 2 2 c ---[ 251]---> BDD-cost: 75 c ---[ 250]---> BDD-cost: 70 c ---[ 249]---> BDD-cost: 73 c ---[ 248]---> BDD-cost: 23 c ---[ 247]---> BDD-cost: 78 c ---[ 246]---> BDD-cost: 59 c ---[ 245]---> BDD-cost: 37 c ---[ 244]---> BDD-cost: 67 c ---[ 243]---> BDD-cost: 29 c ---[ 242]---> BDD-cost: 132 c ---[ 241]---> BDD-cost: 53 c ---[ 240]---> BDD-cost: 36 c ---[ 239]---> BDD-cost: 30 c ---[ 238]---> BDD-cost: 4 c ---[ 237]---> BDD-cost: 93 c ---[ 236]---> BDD-cost: 82 c ---[ 235]---> Sorter-cost: 698 Base: 5 2 3 2 2 c ---[ 234]---> BDD-cost: 57 c ---[ 233]---> BDD-cost: 10 c ---[ 232]---> BDD-cost: 143 c ---[ 231]---> BDD-cost: 66 c ---[ 230]---> BDD-cost: 31 c ---[ 229]---> BDD-cost: 15 c ---[ 228]---> BDD-cost: 100 c ---[ 227]---> BDD-cost: 103 c ---[ 226]---> Sorter-cost: 820 Base: 3 3 3 2 3 c ---[ 225]---> BDD-cost: 110 c ---[ 224]---> Sorter-cost: 734 Base: 5 2 3 2 2 c ---[ 223]---> BDD-cost: 37 c ---[ 222]---> Sorter-cost: 728 Base: 5 2 3 2 2 c ---[ 221]---> BDD-cost: 14 c ---[ 219]---> BDD-cost: 142 c ---[ 217]---> Sorter-cost: 725 Base: 5 3 3 2 c ---[ 216]---> BDD-cost: 14 c ---[ 215]---> BDD-cost: 146 c ---[ 214]---> BDD-cost: 44 c ---[ 213]---> Sorter-cost: 688 Base: 5 3 3 2 c ---[ 212]---> BDD-cost: 21 c ---[ 211]---> BDD-cost: 127 c ---[ 210]---> BDD-cost: 133 c ---[ 209]---> Sorter-cost: 800 Base: 2 2 5 2 3 c ---[ 208]---> BDD-cost: 106 c ---[ 207]---> BDD-cost: 66 c ---[ 206]---> BDD-cost: 14 c ---[ 205]---> BDD-cost: 49 c ---[ 204]---> BDD-cost: 40 c ---[ 203]---> BDD-cost: 85 c ---[ 202]---> BDD-cost: 56 c ---[ 201]---> BDD-cost: 138 c ---[ 200]---> BDD-cost: 14 c ---[ 199]---> BDD-cost: 149 c ---[ 198]---> BDD-cost: 177 c ---[ 197]---> BDD-cost: 92 c ---[ 196]---> BDD-cost: 14 c ---[ 195]---> BDD-cost: 114 c ---[ 194]---> BDD-cost: 160 c ---[ 193]---> BDD-cost: 109 c ---[ 192]---> BDD-cost: 96 c ---[ 191]---> BDD-cost: 142 c ---[ 190]---> BDD-cost: 157 c ---[ 189]---> BDD-cost: 11 c ---[ 188]---> BDD-cost: 112 c ---[ 187]---> BDD-cost: 74 c ---[ 186]---> BDD-cost: 11 c ---[ 185]---> BDD-cost: 13 c ---[ 184]---> BDD-cost: 81 c ---[ 183]---> BDD-cost: 95 c ---[ 182]---> BDD-cost: 110 c ---[ 181]---> BDD-cost: 103 c ---[ 180]---> BDD-cost: 52 c ---[ 179]---> BDD-cost: 100 c ---[ 178]---> BDD-cost: 111 c ---[ 177]---> BDD-cost: 89 c ---[ 176]---> BDD-cost: 140 c ---[ 175]---> BDD-cost: 146 c ---[ 174]---> BDD-cost: 40 c ---[ 173]---> BDD-cost: 53 c ---[ 172]---> BDD-cost: 14 c ---[ 171]---> BDD-cost: 136 c ---[ 170]---> BDD-cost: 143 c ---[ 169]---> BDD-cost: 18 c ---[ 168]---> BDD-cost: 83 c ---[ 167]---> BDD-cost: 14 c ---[ 166]---> Sorter-cost: 689 Base: 5 2 3 5 c ---[ 165]---> BDD-cost: 14 c ---[ 164]---> BDD-cost: 113 c ---[ 163]---> BDD-cost: 99 c ---[ 162]---> BDD-cost: 146 c ---[ 161]---> Sorter-cost: 797 Base: 3 3 3 2 17 c ---[ 159]---> Sorter-cost: 929 Base: 3 3 5 2 c ---[ 158]---> BDD-cost: 47 c ---[ 157]---> BDD-cost: 110 c ---[ 156]---> Sorter-cost: 688 Base: 3 3 2 3 2 c ---[ 154]---> Sorter-cost: 996 Base: 3 3 3 2 2 c ---[ 153]---> BDD-cost: 96 c ---[ 152]---> BDD-cost: 63 c ---[ 151]---> BDD-cost: 191 c ---[ 150]---> BDD-cost: 140 c ---[ 149]---> BDD-cost: 77 c ---[ 148]---> BDD-cost: 104 c ---[ 147]---> Sorter-cost: 543 Base: 3 3 5 2 c ---[ 146]---> BDD-cost: 136 c ---[ 145]---> BDD-cost: 113 c ---[ 143]---> Sorter-cost: 662 Base: 3 3 3 2 3 c ---[ 142]---> BDD-cost: 9 c ---[ 141]---> BDD-cost: 9 c ---[ 140]---> Sorter-cost: 977 Base: 3 3 2 3 17 c ---[ 139]---> BDD-cost: 76 c ---[ 138]---> Sorter-cost: 905 Base: 3 3 5 2 c ---[ 137]---> BDD-cost: 10 c ---[ 136]---> Sorter-cost: 931 Base: 5 2 3 3 11 c ---[ 135]---> Sorter-cost: 774 Base: 3 3 2 3 17 c ---[ 134]---> BDD-cost: 90 c ---[ 133]---> Sorter-cost: 763 Base: 3 3 2 3 2 c ---[ 131]---> Sorter-cost: 818 Base: 3 3 3 2 2 c ---[ 130]---> Sorter-cost: 1096 Base: 3 3 5 2 c ---[ 129]---> BDD-cost: 76 c ---[ 127]---> Sorter-cost: 581 Base: 3 3 3 2 17 c ---[ 126]---> BDD-cost: 19 c ---[ 125]---> Sorter-cost: 1043 Base: 5 3 3 3 c ---[ 124]---> Sorter-cost: 1070 Base: 5 3 3 3 c ---[ 123]---> BDD-cost: 103 c ---[ 122]---> Sorter-cost: 995 Base: 5 2 3 3 c ---[ 121]---> Sorter-cost: 1035 Base: 5 3 3 2 c ---[ 120]---> Sorter-cost: 1021 Base: 5 2 3 3 5 c ---[ 119]---> Sorter-cost: 599 Base: 5 3 3 3 c ---[ 118]---> BDD-cost: 84 c ---[ 117]---> Sorter-cost: 775 Base: 5 2 3 3 c ---[ 116]---> Sorter-cost: 905 Base: 3 3 5 3 c ---[ 115]---> Sorter-cost: 744 Base: 5 3 3 3 c ---[ 114]---> BDD-cost: 184 c ---[ 112]---> Sorter-cost: 1080 Base: 3 3 3 2 3 c ---[ 111]---> Sorter-cost: 1154 Base: 5 2 3 3 c ---[ 109]---> Sorter-cost: 1012 Base: 3 3 5 2 11 c ---[ 108]---> Sorter-cost: 825 Base: 3 3 3 2 2 c ---[ 107]---> BDD-cost: 127 c ---[ 106]---> Sorter-cost: 993 Base: 3 3 3 2 17 c ---[ 105]---> BDD-cost: 17 c ---[ 103]---> BDD-cost: 75 c ---[ 102]---> Sorter-cost: 880 Base: 3 3 2 3 3 c ---[ 101]---> BDD-cost: 165 c ---[ 100]---> Sorter-cost: 774 Base: 3 3 3 2 17 c ---[ 99]---> BDD-cost: 134 c ---[ 98]---> BDD-cost: 135 c ---[ 97]---> Sorter-cost: 1077 Base: 5 2 3 3 c ---[ 96]---> BDD-cost: 132 c ---[ 94]---> BDD-cost: 143 c ---[ 93]---> Sorter-cost: 795 Base: 5 2 3 3 c ---[ 91]---> Sorter-cost: 704 Base: 5 2 3 3 11 c ---[ 90]---> BDD-cost: 18 c ---[ 89]---> BDD-cost: 182 c ---[ 87]---> BDD-cost: 98 c ---[ 86]---> Sorter-cost: 1061 Base: 5 3 3 2 11 c ---[ 85]---> BDD-cost: 125 c ---[ 84]---> BDD-cost: 96 c ---[ 83]---> Sorter-cost: 1204 Base: 3 3 3 2 2 c ---[ 82]---> BDD-cost: 177 c ---[ 81]---> Sorter-cost: 1098 Base: 3 3 3 2 2 c ---[ 80]---> BDD-cost: 18 c ---[ 79]---> Sorter-cost: 1200 Base: 3 3 3 2 2 c ---[ 77]---> BDD-cost: 164 c ---[ 76]---> BDD-cost: 17 c ---[ 75]---> Sorter-cost: 1097 Base: 3 3 3 2 2 c ---[ 74]---> BDD-cost: 18 c ---[ 73]---> Sorter-cost: 1224 Base: 3 3 3 2 2 c ---[ 72]---> BDD-cost: 22 c ---[ 71]---> BDD-cost: 87 c ---[ 70]---> BDD-cost: 6 c ---[ 69]---> BDD-cost: 13 c ---[ 68]---> Sorter-cost: 735 Base: 5 3 3 2 c ---[ 67]---> BDD-cost: 193 c ---[ 66]---> BDD-cost: 193 c ---[ 65]---> BDD-cost: 186 c ---[ 64]---> BDD-cost: 86 c ---[ 63]---> Sorter-cost: 789 Base: 3 3 3 2 17 c ---[ 61]---> Sorter-cost: 897 Base: 3 3 5 2 11 c ---[ 60]---> BDD-cost: 216 c ---[ 59]---> BDD-cost: 194 c ---[ 57]---> Sorter-cost: 792 Base: 3 3 3 2 17 c ---[ 56]---> BDD-cost: 104 c ---[ 55]---> Sorter-cost: 887 Base: 3 3 5 2 11 c ---[ 54]---> Sorter-cost: 1281 Base: 3 3 5 2 c ---[ 53]---> Sorter-cost: 842 Base: 3 3 5 2 7 c ---[ 52]---> Sorter-cost: 1225 Base: 3 3 3 2 2 c ---[ 51]---> BDD-cost: 179 c ---[ 50]---> Sorter-cost: 1432 Base: 3 3 5 2 5 c ---[ 49]---> BDD-cost: 138 c ---[ 48]---> Sorter-cost: 1114 Base: 3 3 3 2 2 c ---[ 47]---> Sorter-cost: 1360 Base: 3 3 3 2 2 c ---[ 46]---> Sorter-cost: 1514 Base: 3 3 3 2 2 c ---[ 45]---> Sorter-cost: 1616 Base: 3 3 3 2 13 c ---[ 44]---> Sorter-cost: 1331 Base: 3 3 5 2 5 c ---[ 43]---> Sorter-cost: 1065 Base: 3 3 3 2 2 c ---[ 42]---> Sorter-cost: 1750 Base: 3 3 3 2 3 c ---[ 41]---> Sorter-cost: 1184 Base: 3 3 3 2 2 c ---[ 40]---> BDD-cost: 152 c ---[ 39]---> BDD-cost: 265 c ---[ 38]---> BDD-cost: 32 c ---[ 37]---> BDD-cost: 33 c ---[ 36]---> Adder-cost: 168 maxlim: 399 bits: 10/9 c ---[ 35]---> BDD-cost: 40 c ---[ 34]---> BDD-cost: 46 c ---[ 33]---> BDD-cost: 60 c ---[ 32]---> Adder-cost: 307 maxlim: 274 bits: 10/9 c ---[ 31]---> Adder-cost: 426 maxlim: 1316 bits: 11/11 c ---[ 30]---> BDD-cost: 122 c ---[ 29]---> BDD-cost: 122 c ---[ 28]---> BDD-cost: 122 c ---[ 27]---> BDD-cost: 122 c ---[ 25]---> Adder-cost: 542 maxlim: 1513 bits: 11/11 c ---[ 24]---> Adder-cost: 533 maxlim: 98 bits: 8/7 c ---[ 23]---> BDD-cost: 189 c ---[ 22]---> Adder-cost: 1992 maxlim: 571 bits: 11/10 c ---[ 21]---> BDD-cost: 2 c ---[ 20]---> BDD-cost: 9 c ---[ 19]---> BDD-cost: 15 c ---[ 18]---> BDD-cost: 3 c ---[ 17]---> BDD-cost: 7 c ---[ 16]---> BDD-cost: 9 c ---[ 15]---> BDD-cost: 1 c ---[ 14]---> BDD-cost: 24 c ---[ 13]---> BDD-cost: 45 c ---[ 12]---> BDD-cost: 25 c ---[ 11]---> BDD-cost: 3 c ---[ 10]---> BDD-cost: 11 c ---[ 9]---> BDD-cost: 19 c ---[ 8]---> BDD-cost: 28 c ---[ 7]---> BDD-cost: 19 c ---[ 6]---> BDD-cost: 8 c ---[ 5]---> BDD-cost: 34 c ---[ 4]---> BDD-cost: 62 c ---[ 3]---> BDD-cost: 25 c ---[ 2]---> BDD-cost: 12 c ---[ 1]---> BDD-cost: 67 c ---[ 0]---> BDD-cost: 73 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 221233 577396 | 73744 0 0 nan | 0.000 % | c | 100 | 221167 577252 | 81118 97 372 3.8 | 0.867 % | c | 252 | 221095 577079 | 89230 243 1047 4.3 | 0.893 % | c | 477 | 220646 576037 | 98153 448 2272 5.1 | 1.045 % | c | 814 | 220625 575993 | 107968 783 4183 5.3 | 1.055 % | c | 1320 | 220204 575028 | 118765 1276 7731 6.1 | 1.207 % | c | 2079 | 219619 573677 | 130641 2017 14305 7.1 | 1.407 % | c | 3220 | 219007 572241 | 143706 3133 26300 8.4 | 1.608 % | c | 4929 | 218609 571364 | 158076 4818 45371 9.4 | 1.751 % | c | 7491 | 217674 569242 | 173884 7328 69732 9.5 | 2.089 % | c | 11335 | 216109 565713 | 191272 11081 119035 10.7 | 2.678 % | c | 17101 | 214370 561742 | 210400 16707 185907 11.1 | 3.329 % | c | 25750 | 212216 556694 | 231440 25151 298747 11.9 | 4.145 % | c | 38724 | 209000 549148 | 254584 37761 471557 12.5 | 5.424 % | c ============================================================================== c [1mFound solution: 148295[0m c ---[ 0]---> Adder-cost: 11288 maxlim: 173536 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47547 | 286258 827165 | 95419 46385 607168 13.1 | 5.424 % | c | 47649 | 286258 827165 | 104960 46487 608769 13.1 | 5.290 % | c | 47799 | 286258 827165 | 115456 46637 610706 13.1 | 5.290 % | c | 48025 | 286255 827156 | 127002 46857 613567 13.1 | 5.291 % | c | 48362 | 286178 826977 | 139702 47188 618317 13.1 | 5.316 % | c | 48868 | 286069 826689 | 153673 47670 624428 13.1 | 5.355 % | c | 49628 | 285893 826271 | 169040 48410 632819 13.1 | 5.411 % | c | 50767 | 285746 825934 | 185944 49538 645871 13.0 | 5.466 % | c | 52478 | 285363 825022 | 204539 51213 667728 13.0 | 5.594 % | c | 55040 | 284989 824118 | 224993 53731 703787 13.1 | 5.729 % | c | 58886 | 284670 823378 | 247492 57533 758801 13.2 | 5.848 % | c | 64653 | 284276 822465 | 272241 63248 845028 13.4 | 5.986 % | c | 73304 | 283628 820864 | 299465 71830 981690 13.7 | 6.187 % | c | 86278 | 282214 817132 | 329412 84608 1218113 14.4 | 6.589 % | c | 105739 | 281388 815131 | 362353 103944 1573655 15.1 | 6.867 % | c | 134931 | 280857 813905 | 398588 133047 2042140 15.3 | 7.066 % | c | 178720 | 279701 811239 | 438447 176644 2732528 15.5 | 7.491 % | c | 244404 | 278847 809210 | 482292 242201 3773942 15.6 | 7.783 % | c ============================================================================== c [1mFound solution: 139270[0m c ---[ 0]---> Adder-cost: 0 maxlim: 182561 bits: 19/18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 246489 | 278860 809303 | 92953 244286 3815826 15.6 | 7.783 % | c | 246589 | 278860 809303 | 102248 36602 304139 8.3 | 7.788 % | c | 246739 | 278860 809303 | 112473 36752 305062 8.3 | 7.788 % | c | 246966 | 278815 809200 | 123720 36976 307642 8.3 | 7.803 % | c | 247303 | 278815 809200 | 136092 37313 311157 8.3 | 7.803 % | c | 247809 | 278815 809200 | 149701 37819 315407 8.3 | 7.803 % | c | 248569 | 278777 809115 | 164671 38573 325041 8.4 | 7.820 % | c | 249709 | 278774 809106 | 181139 39712 337714 8.5 | 7.821 % | c | 251418 | 278774 809106 | 199253 41421 362663 8.8 | 7.821 % | c | 253980 | 278585 808670 | 219178 43974 396859 9.0 | 7.889 % | c | 257824 | 278537 808560 | 241096 47815 437368 9.1 | 7.905 % | c | 263590 | 278512 808499 | 265205 53576 511496 9.5 | 7.913 % | c | 272240 | 278464 808385 | 291726 62207 609435 9.8 | 7.933 % | c | 285214 | 278377 808188 | 320898 75168 819028 10.9 | 7.964 % | c | 304675 | 278197 807759 | 352988 94597 1089088 11.5 | 8.028 % | c | 333867 | 278006 807324 | 388287 123764 2677482 21.6 | 8.093 % | c c *** TERMINATED *** s SATISFIABLE v x0 -x1 -x2 -x3 -x4 x5 x6 x7 -x8 -x9 -x10 -x11 -x12 -x13 x14 -x15 -x16 -x17 -x18 -x19 x20 -x21 -x22 -x23 x24 x25 -x26 -x27 -x28 x29 -x30 -x31 x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 x47 -x48 -x49 x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 x86 x87 x88 -x89 -x90 -x91 -x92 x93 -x94 -x95 x96 x97 -x98 -x99 -x100 -x101 -x102 x103 -x104 x105 -x106 -x107 -x108 -x109 -x110 x111 -x112 x113 -x114 -x115 -x116 -x117 x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 x146 -x147 x148 -x149 -x150 -x151 x152 -x153 -x154 x155 -x156 -x157 x158 -x159 -x160 -x161 -x162 -x163 x164 -x165 -x166 -x167 x168 -x169 x170 -x171 -x172 x173 -x174 -x175 -x176 -x177 -x178 -x179 x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 x208 -x209 -x210 x211 x212 x213 -x214 -x215 -x216 -x217 -x218 -x219 x220 x221 -x222 -x223 -x224 -x225 x226 -x227 -x228 x229 -x230 x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 x247 x248 -x249 -x250 -x251 x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 x270 -x271 x272 -x273 x274 -x275 -x276 -x277 x278 x279 -x280 -x281 -x282 -x283 -x284 x285 x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 x301 -x302 x303 -x304 -x305 -x306 -x307 -x308 x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 x319 -x320 -x321 -x322 -x323 -x324 -x325 x326 -x327 x328 -x329 -x330 x331 -x332 -x333 -x334 -x335 -x336 x337 -x338 -x339 x340 -x341 -x342 -x343 -x344 x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 x354 -x355 -x356 -x357 -x358 x359 -x360 -x361 -x362 -x363 x364 -x365 -x366 x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 x378 -x379 -x380 -x381 -x382 x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 x392 -x393 -x394 -x395 -x396 -x397 -x398 x399 -x400 -x401 -x402 -x403 x404 x405 -x406 x407 -x408 -x409 -x410 -x411 -x412 -x413 x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 x422 x423 -x424 -x425 x426 -x427 -x428 -x429 x430 -x431 -x432 x433 x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 x442 x443 -x444 -x445 x446 -x447 -x448 -x449 -x450 x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 x474 x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 x484 x485 -x486 -x487 -x488 -x489 -x490 x491 -x492 -x493 x494 -x495 -x496 -x497 -x498 x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 x508 -x509 -x510 -x511 -x512 -x513 -x514 x515 -x516 -x517 -x518 x519 -x520 -x521 -x522 -x523 x524 -x525 -x526 x527 x528 -x529 x530 -x531 -x532 -x533 x534 -x535 -x536 -x537 -x538 x539 -x540 x541 -x542 -x543 -x544 -x545 -x546 x547 -x548 -x549 -x550 -x551 -x552 -x553 x554 -x555 -x556 x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 x565 -x566 -x567 x568 x569 -x570 -x571 -x572 -x573 x574 -x575 -x576 x577 -x578 x579 -x580 -x581 x582 x583 -x584 -x585 -x586 -x587 -x588 x589 -x590 -x591 -x592 -x593 x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 x624 -x625 -x626 -x627 -x628 -x629 x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 x644 -x645 x646 -x647 -x648 x649 -x650 -x651 -x652 -x653 -x654 x655 -x656 -x657 -x658 -x659 x660 -x661 -x662 x663 -x664 -x665 -x666 x667 -x668 -x669 -x670 -x671 -x672 x673 -x674 x675 -x676 x677 -x678 -x679 -x680 x681 x682 -x683 -x684 x685 -x686 -x687 -x688 -x689 x690 -x691 -x692 -x693 x694 -x695 -x696 x697 -x698 -x699 x700 -x701 -x702 x703 -x704 -x705 -x706 -x707 -x708 -x709 x710 -x711 -x712 -x713 -x714 x715 -x716 -x717 x718 -x719 -x720 x721 x722 x723 x724 x725 -x726 -x727 -x728 -x729 -x730 -x731 x732 -x733 -x734 x735 x736 x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 x745 -x746 -x747 x748 x749 -x750 -x751 -x752 -x753 -x754 x755 -x756 x757 x758 -x759 -x760 x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 x775 -x776 -x777 x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 x788 x789 x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 x799 x800 -x801 -x802 -x803 x804 -x805 -x806 -x807 -x808 -x809 -x810 x811 x812 -x813 -x814 -x815 -x816 -x817 -x818 x819 -x820 -x821 -x822 -x823 -x824 x825 x826 x827 -x828 x829 x830 -x831 x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 x852 -x853 -x854 x855 -x856 -x857 -x858 -x859 x860 -x861 x862 -x863 -x864 x865 x866 -x867 -x868 -x869 x870 -x871 -x872 x873 -x874 x875 -x876 -x877 x878 -x879 -x880 x881 -x882 x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 x894 x895 -x896 -x897 x898 -x899 -x900 -x901 -x902 -x903 x904 -x905 -x906 x907 -x908 -x909 x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 x919 x920 -x921 -x922 -x923 x924 -x925 -x926 -x927 -x928 -x929 x930 x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 x950 x951 -x952 -x953 x954 -x955 -x956 x957 x958 -x959 -x960 -x961 -x962 -x963 -x964 x965 x966 x967 x968 -x969 -x970 -x971 x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 x981 x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 x990 -x991 -x992 x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 -x1011 -x1012 -x1013 x1014 -x1015 -x1016 -x1017 -x1018 -x1019 x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 x1031 -x1032 -x1033 x1034 -x1035 -x1036 -x1037 -x1038 x1039 -x1040 x1041 -x1042 -x1043 x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 x1067 x1068 x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 x1079 x1080 -x1081 x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 x1089 -x1090 x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 x1098 x1099 -x1100 x1101 x1102 -x1103 x1104 x1105 x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 x1118 -x1119 -x1120 -x1121 x1122 -x1123 x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 x1131 -x1132 x1133 x1134 x1135 -x1136 -x1137 -x1138 x1139 -x1140 -x1141 -x1142 -x1143 -x1144 x1145 -x1146 -x1147 -x1148 -x1149 x1150 x1151 -x1152 -x1153 -x1154 x1155 -x1156 -x1157 -x1158 -x1159 x1160 -x1161 x1162 -x1163 -x1164 -x1165 x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 x1175 x1176 -x1177 -x1178 -x1179 x1180 -x1181 -x1182 -x1183 x1184 -x1185 x1186 -x1187 -x1188 -x1189 -x1190 x1191 -x1192 -x1193 -x1194 -x1195 x1196 x1197 x1198 x1199 x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 x1208 -x1209 x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 x1220 -x1221 -x1222 -x1223 -x1224 x1225 x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 x1233 x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 x1249 x1250 x1251 -x1252 -x1253 x1254 -x1255 -x1256 x1257 x1258 -x1259 -x1260 -x1261 -x1262 -x1263 x1264 x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 x1273 -x1274 -x1275 -x1276 -x1277 x1278 x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 x1307 -x1308 -x1309 -x1310 x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 x1331 x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 x1342 -x1343 x1344 x1345 x1346 -x1347 -x1348 -x1349 -x1350 -x1351 x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 x1362 -x1363 -x1364 x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 x1380 -x1381 x1382 -x1383 -x1384 -x1385 -x1386 x1387 -x1388 -x1389 x1390 -x1391 -x1392 x1393 -x1394 x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 x1404 x1405 -x1406 x1407 -x1408 -x1409 -x1410 -x1411 x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 x1420 x1421 -x1422 -x1423 -x1424 -x1425 -x1426 x1427 x1428 -x1429 -x1430 -x1431 x1432 -x1433 -x1434 -x1435 -x1436 -x1437 x1438 -x1439 -x1440 -x1441 x1442 x1443 -x1444 -x1445 x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 x1457 x1458 -x1459 x1460 x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 x1470 -x1471 x1472 -x1473 -x1474 -x1475 -x1476 x1477 -x1478 -x1479 -x1480 x1481 -x1482 -x1483 -x1484 x1485 x1486 -x1487 -x1488 -x1489 -x1490 x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 x1498 -x1499 -x1500 -x1501 x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 x1511 -x1512 -x1513 -x1514 x1515 -x1516 -x1517 -x1518 x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 x1527 x1528 x1529 -x1530 -x1531 -x1532 x1533 -x1534 -x1535 -x1536 x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 x1547 -x1548 -x1549 x1550 -x1551 x1552 -x1553 -x1554 -x1555 x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 x1564 -x1565 -x1566 -x1567 x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 x1580 x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 x1590 x1591 -x1592 x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 x1601 x1602 x1603 x1604 -x1605 x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 x1616 -x1617 x1618 -x1619 x1620 -x1621 -x1622 -x1623 -x1624 x1625 -x1626 x1627 -x1628 -x1629 x1630 -x1631 -x1632 x1633 -x1634 -x1635 -x1636 x1637 -x1638 -x1639 -x1640 -x1641 -x1642 x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 x1655 -x1656 -x1657 -x1658 -x1659 x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 x1670 -x1671 -x1672 x1673 x1674 -x1675 -x1676 x1677 x1678 -x1679 -x1680 x1681 -x1682 -x1683 -x1684 -x1685 x1686 -x1687 -x1688 x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 x1696 -x1697 -x1698 -x1699 x1700 -x1701 x1702 x1703 -x1704 -x1705 -x1706 x1707 x1708 -x1709 x1710 -x1711 -x1712 -x1713 -x1714 -x1715 x1716 -x1717 -x1718 -x1719 x1720 -x1721 x1722 -x1723 x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 x1741 -x1742 -x1743 -x1744 -x1745 -x1746 x1747 -x1748 x1749 -x1750 x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 x1758 x1759 -x1760 -x1761 x1762 -x1763 -x1764 -x1765 -x1766 x1767 -x1768 x1769 -x1770 -x1771 x1772 -x1773 -x1774 -x1775 -x1776 -x1777 x1778 -x1779 x1780 -x1781 -x1782 x1783 -x1784 x1785 -x1786 -x1787 x1788 x1789 -x1790 -x1791 -x1792 -x1793 x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 x1801 x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 x1813 -x1814 x1815 x1816 -x1817 x1818 -x1819 -x1820 -x1821 x1822 -x1823 -x1824 x1825 -x1826 -x1827 -x1828 x1829 -x1830 x1831 -x1832 -x1833 -x1834 x1835 -x1836 x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 x1846 -x1847 x1848 -x1849 -x1850 x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 x1869 -x1870 x1871 x1872 -x1873 -x1874 x1875 x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 x1895 x1896 -x1897 x1898 x1899 x1900 -x1901 -x1902 x1903 -x1904 -x1905 x1906 -x1907 x1908 -x1909 -x1910 x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 x1919 -x1920 x1921 -x1922 -x1923 -x1924 -x1925 -x1926 x1927 -x1928 -x1929 -x1930 x1931 x1932 -x1933 x1934 -x1935 -x1936 -x1937 -x1938 -x1939 x1940 -x1941 -x1942 -x1943 -x1944 -x1945 x1946 -x1947 x1948 -x1949 -x1950 -x1951 x1952 -x1953 x1954 -x1955 -x1956 x1957 -x1958 -x1959 -x1960 -x1961 x1962 -x1963 -x1964 x1965 -x1966 -x1967 x1968 -x1969 -x1970 -x1971 -x1972 x1973 -x1974 -x1975 -x1976 x1977 -x1978 -x1979 x1980 -x1981 -x1982 -x1983 x1984 -x1985 -x1986 -x1987 x1988 -x1989 x1990 -x1991 -x1992 -x1993 -x1994 -x1995 x1996 x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 x2005 -x2006 -x2007 x2008 -x2009 -x2010 -x2011 -x2012 x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 x2024 -x2025 -x2026 -x2027 -x2028 x2029 -x2030 -x2031 x2032 -x2033 -x2034 -x2035 -x2036 x2037 x2038 x2039 -x2040 -x2041 x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 x2054 x2055 -x2056 -x2057 -x2058 -x2059 -x2060 x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 x2096 -x2097 -x2098 x2099 -x2100 x2101 -x2102 -x2103 -x2104 x2105 -x2106 -x2107 -x2108 x2109 -x2110 -x2111 x2112 -x2113 -x2114 x2115 x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 x2126 -x2127 -x2128 -x2129 x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 x2139 -x2140 x2141 -x2142 -x2143 x2144 -x2145 -x2146 x2147 x2148 x2149 x2150 x2151 x2152 -x2153 -x2154 x2155 x2156 x2157 x2158 x2159 x2160 x2161 x2162 -x2163 -x2164 -x2165 -x2643 x2644 -x2640 -x2641 -x2635 -x2636 -x2632 -x2633 -x2629 -x2630 -x2626 -x2627 -x2623 -x2624 -x2618 x2619 -x2614 x2615 -x2611 x2612 -x2608 -x2609 -x2477 -x2478 -x2474 -x2475 -x2471 x2472 -x2467 -x2468 -x2463 x2464 -x2555 -x2556 -x2560 -x2561 -x2564 x2565 -x2568 x2569 -x2572 -x2573 -x2583 -x2584 -x2587 -x2588 -x2590 -x2591 -x2593 x2594 -x2597 -x2598 x2604 -x2605 -x2507 -x2508 -x2504 -x2505 x2501 -x2502 x2498 -x2499 -x2494 x2495 x2490 -x2491 x2485 -x2486 -x2480 -x2481 -x2458 -x2459 -x2453 -x2454 -x2448 x2449 x2444 -x2445 x2437 -x2438 x2432 -x2433 -x2425 -x2426 x2419 -x2420 x2413 -x2414 x2405 -x2406 -x2399 -x2400 -x2378 x2379 x2371 -x2372 -x2366 x2367 -x2363 x2364 -x2360 x2361 -x2357 -x2358 -x2352 x2353 x2348 -x2349 x2345 -x2346 -x2342 -x2343 x2331 -x2332 -x2328 x2329 -x2325 -x2326 -x2322 -x2323 -x2175 -x2176 -x2171 x2172 -x2250 -x2251 -x2263 -x2264 x2266 -x2267 x2269 -x2270 -x2272 x2273 -x2276 x2277 x2284 -x2285 -x2287 -x2288 -x2290 -x2291 -x2293 x2294 -x2296 -x2297 -x2307 -x2308 -x2310 -x2311 x2313 -x2314 x2317 -x2318 -x2392 -x2393 -x2386 x2387 -x2235 x2236 -x2231 -x2232 x2227 -x2228 x2223 -x2224 -x2219 x2220 -x2214 x2215 -x2202 x2203 -x2198 -x2199 x2194 -x2195 -x2191 x2192 x2187 -x2188 -x2183 -x2184 x2179 -x2180 -x2166 x2167 -x2246 -x2247 x2242 -x2243 -x2239 -x2240 x2578 x2404 x2258 -x2208 -x2647 -x2256 -x2257 -x2212 -x2190 x2193 x2390 x2435 x2752 -x2753 -x2301 x2170 -x2169 x2173 x2174 x2218 x2217 x2221 x2222 x2238 -x2241 -x2336 -x2305 -x2648 -x2649 x2340 -x2337 -x2302 -x2754 -x2750 -x2751 x2245 x2237 x2216 -x2197 -x2189 -x2168 -x2391 -x2389 x2394 -x2397 x2395 -x2396 x2398 -x2376 x2375 -x2377 -x2374 -x2380 -x2384 x2382 x2383 -x2381 x2385 x2338 -x2339 x2303 -x2304 x2559 x2558 x2562 -x2563 -x2225 x2226 -x2177 -x2178 x2607 -x2610 -x2628 x2586 -x2589 -x2489 x2488 x2492 x2493 -x2462 -x2461 x2465 x2466 -x2452 -x2455 -x2436 -x2439 x2442 -x2440 -x2441 x2443 x2424 -x2423 x2422 x2427 x2430 -x2428 x2429 x2431 x2412 x2415 -x2416 -x2204 -x2205 -x2233 -x2234 -x2298 -x2185 -x2186 -x2252 -x2253 -x2456 -x2457 -x2417 -x2418 x2275 x2278 -x2279 x2702 x2703 x2704 -x2292 x2320 x2321 -x2295 x2566 x2658 x2659 x2660 x2663 -x2662 -x2661 x2664 x2403 x2407 x2410 x2408 x2409 x2402 x2411 -x2631 x2280 x2282 -x2281 x2283 -x2274 -x2271 -x2670 -x2669 -x2672 -x2671 -x2673 -x2674 -x2675 x2676 x2679 x2678 -x2677 x2680 -x2312 x2685 -x2686 x2687 -x2362 -x2592 x2369 -x2370 -x2613 -x2700 -x2701 -x2355 -x2356 -x2654 x2653 x2656 -x2655 x2657 -x2543 -x2544 x2447 x2450 x2451 -x2697 x2698 x2699 -x2551 -x2552 x2710 -x2709 x2712 -x2711 x2713 -x2726 x2725 -x2728 -x2727 -x2729 -x2347 x2690 -x2691 x2692 x2688 x2689 -x2716 x2718 -x2717 x2719 -x2714 -x2715 x2732 x2734 x2733 x2735 -x2299 -x2300 -x2327 x2334 -x2335 -x2730 -x2731 x2341 -x2344 -x2681 -x2682 x2373 x2683 x2684 -x2359 x2606 -x
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/14139/stat): 14139 (minisat+_script) R 14138 14139 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843423195 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/14139/statm): 174 3 169 147 0 27 0 [pid=14139] 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=14140 New process pid=14141 New process pid=14142 execve syscall for /bin/sed executable One traced child (pid=14141) 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=14142) exited with status: 0 One traced child (pid=14140) exited with status: 0 New process pid=14143 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-p2756.opb [startup+10.0042 s] Raw data (loadavg): 0.87 0.95 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 6965 0 0 0 942 27 0 0 25 0 1 0 1843423200 31555584 6605 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 7704 6605 145 145 0 7559 0 [pid=14143] vsize: 30816 Current children cumulated CPU time (s) 9.7 Current children cumulated vsize (Kb) 32940 [startup+20.0058 s] Raw data (loadavg): 0.89 0.95 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7097 0 0 0 1938 28 0 0 25 0 1 0 1843423200 32034816 6737 4294967295 134512640 135094434 3221224448 3221223152 134559005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 7821 6737 145 145 0 7676 0 [pid=14143] vsize: 31284 Current children cumulated CPU time (s) 19.67 Current children cumulated vsize (Kb) 33408 [startup+30.0074 s] Raw data (loadavg): 0.90 0.95 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7190 0 0 0 2937 29 0 0 25 0 1 0 1843423200 32407552 6830 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 7912 6830 145 145 0 7767 0 [pid=14143] vsize: 31648 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 33772 [startup+40.0079 s] Raw data (loadavg): 0.92 0.95 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7282 0 0 0 3936 30 0 0 25 0 1 0 1843423200 32755712 6922 4294967295 134512640 135094434 3221224448 3221223136 134558992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 7997 6922 145 145 0 7852 0 [pid=14143] vsize: 31988 Current children cumulated CPU time (s) 39.67 Current children cumulated vsize (Kb) 34112 [startup+50.0085 s] Raw data (loadavg): 0.93 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7353 0 0 0 4935 31 0 0 25 0 1 0 1843423200 33030144 6993 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8064 6993 145 145 0 7919 0 [pid=14143] vsize: 32256 Current children cumulated CPU time (s) 49.67 Current children cumulated vsize (Kb) 34380 [startup+60.0092 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7414 0 0 0 5932 33 0 0 25 0 1 0 1843423200 33329152 7054 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8137 7054 145 145 0 7992 0 [pid=14143] vsize: 32548 Current children cumulated CPU time (s) 59.66 Current children cumulated vsize (Kb) 34672 [startup+70.0118 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7496 0 0 0 6930 34 0 0 25 0 1 0 1843423200 33652736 7136 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8216 7136 145 145 0 8071 0 [pid=14143] vsize: 32864 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 34988 [startup+80.0134 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7567 0 0 0 7929 34 0 0 25 0 1 0 1843423200 33927168 7207 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8283 7207 145 145 0 8138 0 [pid=14143] vsize: 33132 Current children cumulated CPU time (s) 79.64 Current children cumulated vsize (Kb) 35256 [startup+90.014 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7644 0 0 0 8928 35 0 0 25 0 1 0 1843423200 34230272 7284 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8357 7284 145 145 0 8212 0 [pid=14143] vsize: 33428 Current children cumulated CPU time (s) 89.64 Current children cumulated vsize (Kb) 35552 [startup+100.014 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7722 0 0 0 9927 35 0 0 25 0 1 0 1843423200 34541568 7362 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8433 7362 145 145 0 8288 0 [pid=14143] vsize: 33732 Current children cumulated CPU time (s) 99.63 Current children cumulated vsize (Kb) 35856 [startup+110.015 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7784 0 0 0 10927 36 0 0 25 0 1 0 1843423200 34914304 7424 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8524 7424 145 145 0 8379 0 [pid=14143] vsize: 34096 Current children cumulated CPU time (s) 109.64 Current children cumulated vsize (Kb) 36220 [startup+120.016 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7828 0 0 0 11926 36 0 0 25 0 1 0 1843423200 35074048 7468 4294967295 134512640 135094434 3221224448 3221223060 134563151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8563 7468 145 145 0 8418 0 [pid=14143] vsize: 34252 Current children cumulated CPU time (s) 119.63 Current children cumulated vsize (Kb) 36376 [startup+130.016 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7889 0 0 0 12925 36 0 0 25 0 1 0 1843423200 35307520 7529 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8620 7529 145 145 0 8475 0 [pid=14143] vsize: 34480 Current children cumulated CPU time (s) 129.62 Current children cumulated vsize (Kb) 36604 [startup+140.017 s] Raw data (loadavg): 0.98 0.96 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 7954 0 0 0 13924 37 0 0 25 0 1 0 1843423200 35557376 7594 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8681 7594 145 145 0 8536 0 [pid=14143] vsize: 34724 Current children cumulated CPU time (s) 139.62 Current children cumulated vsize (Kb) 36848 [startup+150.018 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 8029 0 0 0 14923 37 0 0 25 0 1 0 1843423200 35844096 7669 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 8751 7669 145 145 0 8606 0 [pid=14143] vsize: 35004 Current children cumulated CPU time (s) 149.61 Current children cumulated vsize (Kb) 37128 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.98 1/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) T 14139 14139 4419 0 -1 0 14604 0 0 0 15883 60 0 0 25 0 1 0 1843423200 62984192 13121 4294967295 134512640 135094434 3221224448 3221216140 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/14143/statm): 15377 13121 145 145 0 15232 0 [pid=14143] vsize: 61508 Current children cumulated CPU time (s) 159.44 Current children cumulated vsize (Kb) 63632 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15161 0 0 0 16875 64 0 0 25 0 1 0 1843423200 65961984 13678 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16104 13678 145 145 0 15959 0 [pid=14143] vsize: 64416 Current children cumulated CPU time (s) 169.4 Current children cumulated vsize (Kb) 66540 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15206 0 0 0 17875 64 0 0 25 0 1 0 1843423200 66138112 13723 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16147 13723 145 145 0 16002 0 [pid=14143] vsize: 64588 Current children cumulated CPU time (s) 179.4 Current children cumulated vsize (Kb) 66712 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15256 0 0 0 18874 64 0 0 25 0 1 0 1843423200 66334720 13773 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16195 13773 145 145 0 16050 0 [pid=14143] vsize: 64780 Current children cumulated CPU time (s) 189.39 Current children cumulated vsize (Kb) 66904 [startup+200.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15326 0 0 0 19873 65 0 0 25 0 1 0 1843423200 66609152 13843 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16262 13843 145 145 0 16117 0 [pid=14143] vsize: 65048 Current children cumulated CPU time (s) 199.39 Current children cumulated vsize (Kb) 67172 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15396 0 0 0 20872 65 0 0 25 0 1 0 1843423200 66879488 13913 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16328 13913 145 145 0 16183 0 [pid=14143] vsize: 65312 Current children cumulated CPU time (s) 209.38 Current children cumulated vsize (Kb) 67436 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15450 0 0 0 21872 66 0 0 25 0 1 0 1843423200 67088384 13967 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16379 13967 145 145 0 16234 0 [pid=14143] vsize: 65516 Current children cumulated CPU time (s) 219.39 Current children cumulated vsize (Kb) 67640 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15533 0 0 0 22870 66 0 0 25 0 1 0 1843423200 67416064 14050 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16459 14050 145 145 0 16314 0 [pid=14143] vsize: 65836 Current children cumulated CPU time (s) 229.37 Current children cumulated vsize (Kb) 67960 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15586 0 0 0 23869 67 0 0 25 0 1 0 1843423200 67887104 14103 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16574 14103 145 145 0 16429 0 [pid=14143] vsize: 66296 Current children cumulated CPU time (s) 239.37 Current children cumulated vsize (Kb) 68420 [startup+250.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15675 0 0 0 24868 67 0 0 25 0 1 0 1843423200 68235264 14192 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16659 14192 145 145 0 16514 0 [pid=14143] vsize: 66636 Current children cumulated CPU time (s) 249.36 Current children cumulated vsize (Kb) 68760 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15833 0 0 0 25866 69 0 0 25 0 1 0 1843423200 68866048 14350 4294967295 134512640 135094434 3221224448 3221223088 134562152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16813 14350 145 145 0 16668 0 [pid=14143] vsize: 67252 Current children cumulated CPU time (s) 259.36 Current children cumulated vsize (Kb) 69376 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15886 0 0 0 26865 69 0 0 25 0 1 0 1843423200 69074944 14403 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16864 14403 145 145 0 16719 0 [pid=14143] vsize: 67456 Current children cumulated CPU time (s) 269.35 Current children cumulated vsize (Kb) 69580 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 15927 0 0 0 27865 69 0 0 25 0 1 0 1843423200 69234688 14444 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16903 14444 145 145 0 16758 0 [pid=14143] vsize: 67612 Current children cumulated CPU time (s) 279.35 Current children cumulated vsize (Kb) 69736 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16008 0 0 0 28863 70 0 0 25 0 1 0 1843423200 69554176 14525 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 16981 14525 145 145 0 16836 0 [pid=14143] vsize: 67924 Current children cumulated CPU time (s) 289.34 Current children cumulated vsize (Kb) 70048 [startup+300.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16072 0 0 0 29862 70 0 0 25 0 1 0 1843423200 69804032 14589 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17042 14589 145 145 0 16897 0 [pid=14143] vsize: 68168 Current children cumulated CPU time (s) 299.33 Current children cumulated vsize (Kb) 70292 [startup+310.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16133 0 0 0 30861 71 0 0 25 0 1 0 1843423200 70041600 14650 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17100 14650 145 145 0 16955 0 [pid=14143] vsize: 68400 Current children cumulated CPU time (s) 309.33 Current children cumulated vsize (Kb) 70524 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16213 0 0 0 31860 72 0 0 25 0 1 0 1843423200 70356992 14730 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17177 14730 145 145 0 17032 0 [pid=14143] vsize: 68708 Current children cumulated CPU time (s) 319.33 Current children cumulated vsize (Kb) 70832 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16275 0 0 0 32859 72 0 0 25 0 1 0 1843423200 70602752 14792 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17237 14792 145 145 0 17092 0 [pid=14143] vsize: 68948 Current children cumulated CPU time (s) 329.32 Current children cumulated vsize (Kb) 71072 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16364 0 0 0 33857 73 0 0 25 0 1 0 1843423200 70955008 14881 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17323 14881 145 145 0 17178 0 [pid=14143] vsize: 69292 Current children cumulated CPU time (s) 339.31 Current children cumulated vsize (Kb) 71416 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16464 0 0 0 34854 74 0 0 25 0 1 0 1843423200 71352320 14981 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17420 14981 145 145 0 17275 0 [pid=14143] vsize: 69680 Current children cumulated CPU time (s) 349.29 Current children cumulated vsize (Kb) 71804 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16566 0 0 0 35853 75 0 0 25 0 1 0 1843423200 71757824 15083 4294967295 134512640 135094434 3221224448 3221223060 134563077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17519 15083 145 145 0 17374 0 [pid=14143] vsize: 70076 Current children cumulated CPU time (s) 359.29 Current children cumulated vsize (Kb) 72200 [startup+370.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16636 0 0 0 36851 76 0 0 25 0 1 0 1843423200 72032256 15153 4294967295 134512640 135094434 3221224448 3221223104 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17586 15153 145 145 0 17441 0 [pid=14143] vsize: 70344 Current children cumulated CPU time (s) 369.28 Current children cumulated vsize (Kb) 72468 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16762 0 0 0 37849 77 0 0 25 0 1 0 1843423200 72531968 15279 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17708 15279 145 145 0 17563 0 [pid=14143] vsize: 70832 Current children cumulated CPU time (s) 379.27 Current children cumulated vsize (Kb) 72956 [startup+390.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16808 0 0 0 38849 77 0 0 25 0 1 0 1843423200 72712192 15325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17752 15325 145 145 0 17607 0 [pid=14143] vsize: 71008 Current children cumulated CPU time (s) 389.27 Current children cumulated vsize (Kb) 73132 [startup+400.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 16899 0 0 0 39847 78 0 0 25 0 1 0 1843423200 73072640 15416 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17840 15416 145 145 0 17695 0 [pid=14143] vsize: 71360 Current children cumulated CPU time (s) 399.26 Current children cumulated vsize (Kb) 73484 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17050 0 0 0 40845 79 0 0 25 0 1 0 1843423200 73670656 15567 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 17986 15567 145 145 0 17841 0 [pid=14143] vsize: 71944 Current children cumulated CPU time (s) 409.25 Current children cumulated vsize (Kb) 74068 [startup+420.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17097 0 0 0 41845 80 0 0 25 0 1 0 1843423200 73854976 15614 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18031 15614 145 145 0 17886 0 [pid=14143] vsize: 72124 Current children cumulated CPU time (s) 419.26 Current children cumulated vsize (Kb) 74248 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17156 0 0 0 42844 80 0 0 25 0 1 0 1843423200 74092544 15673 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18089 15673 145 145 0 17944 0 [pid=14143] vsize: 72356 Current children cumulated CPU time (s) 429.25 Current children cumulated vsize (Kb) 74480 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17215 0 0 0 43842 81 0 0 25 0 1 0 1843423200 74321920 15732 4294967295 134512640 135094434 3221224448 3221223104 134550405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18145 15732 145 145 0 18000 0 [pid=14143] vsize: 72580 Current children cumulated CPU time (s) 439.24 Current children cumulated vsize (Kb) 74704 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17260 0 0 0 44841 81 0 0 25 0 1 0 1843423200 74498048 15777 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18188 15777 145 145 0 18043 0 [pid=14143] vsize: 72752 Current children cumulated CPU time (s) 449.23 Current children cumulated vsize (Kb) 74876 [startup+460.04 s] Raw data (loadavg): 1.07 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17318 0 0 0 45840 82 0 0 25 0 1 0 1843423200 75251712 15835 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18372 15835 145 145 0 18227 0 [pid=14143] vsize: 73488 Current children cumulated CPU time (s) 459.23 Current children cumulated vsize (Kb) 75612 [startup+470.041 s] Raw data (loadavg): 1.06 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17367 0 0 0 46839 82 0 0 25 0 1 0 1843423200 75444224 15884 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18419 15884 145 145 0 18274 0 [pid=14143] vsize: 73676 Current children cumulated CPU time (s) 469.22 Current children cumulated vsize (Kb) 75800 [startup+480.041 s] Raw data (loadavg): 1.05 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17429 0 0 0 47839 82 0 0 25 0 1 0 1843423200 75685888 15946 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18478 15946 145 145 0 18333 0 [pid=14143] vsize: 73912 Current children cumulated CPU time (s) 479.22 Current children cumulated vsize (Kb) 76036 [startup+490.043 s] Raw data (loadavg): 1.04 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17493 0 0 0 48838 82 0 0 25 0 1 0 1843423200 75935744 16010 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18539 16010 145 145 0 18394 0 [pid=14143] vsize: 74156 Current children cumulated CPU time (s) 489.21 Current children cumulated vsize (Kb) 76280 [startup+500.044 s] Raw data (loadavg): 1.04 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17561 0 0 0 49837 83 0 0 25 0 1 0 1843423200 76201984 16078 4294967295 134512640 135094434 3221224448 3221223108 134553533 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18604 16078 145 145 0 18459 0 [pid=14143] vsize: 74416 Current children cumulated CPU time (s) 499.21 Current children cumulated vsize (Kb) 76540 [startup+510.044 s] Raw data (loadavg): 1.03 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17630 0 0 0 50837 83 0 0 25 0 1 0 1843423200 76476416 16147 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18671 16147 145 145 0 18526 0 [pid=14143] vsize: 74684 Current children cumulated CPU time (s) 509.21 Current children cumulated vsize (Kb) 76808 [startup+520.045 s] Raw data (loadavg): 1.03 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17752 0 0 0 51835 84 0 0 25 0 1 0 1843423200 76959744 16269 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 18789 16269 145 145 0 18644 0 [pid=14143] vsize: 75156 Current children cumulated CPU time (s) 519.2 Current children cumulated vsize (Kb) 77280 [startup+530.045 s] Raw data (loadavg): 1.02 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17790 0 0 0 52834 85 0 0 25 0 1 0 1843423200 77107200 16307 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 18825 16307 145 145 0 18680 0 [pid=14143] vsize: 75300 Current children cumulated CPU time (s) 529.2 Current children cumulated vsize (Kb) 77424 [startup+540.047 s] Raw data (loadavg): 1.02 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17829 0 0 0 53832 85 0 0 25 0 1 0 1843423200 77258752 16346 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 18862 16346 145 145 0 18717 0 [pid=14143] vsize: 75448 Current children cumulated CPU time (s) 539.18 Current children cumulated vsize (Kb) 77572 [startup+550.048 s] Raw data (loadavg): 1.01 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17859 0 0 0 54831 86 0 0 25 0 1 0 1843423200 77373440 16376 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 18890 16376 145 145 0 18745 0 [pid=14143] vsize: 75560 Current children cumulated CPU time (s) 549.18 Current children cumulated vsize (Kb) 77684 [startup+560.049 s] Raw data (loadavg): 1.01 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17898 0 0 0 55830 87 0 0 25 0 1 0 1843423200 77524992 16415 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 18927 16415 145 145 0 18782 0 [pid=14143] vsize: 75708 Current children cumulated CPU time (s) 559.18 Current children cumulated vsize (Kb) 77832 [startup+570.05 s] Raw data (loadavg): 1.01 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 17942 0 0 0 56829 87 0 0 25 0 1 0 1843423200 77697024 16459 4294967295 134512640 135094434 3221224448 3221223104 134561482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 18969 16459 145 145 0 18824 0 [pid=14143] vsize: 75876 Current children cumulated CPU time (s) 569.17 Current children cumulated vsize (Kb) 78000 [startup+580.05 s] Raw data (loadavg): 1.01 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18006 0 0 0 57828 89 0 0 25 0 1 0 1843423200 77946880 16523 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19030 16523 145 145 0 18885 0 [pid=14143] vsize: 76120 Current children cumulated CPU time (s) 579.18 Current children cumulated vsize (Kb) 78244 [startup+590.051 s] Raw data (loadavg): 1.01 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18130 0 0 0 58826 90 0 0 25 0 1 0 1843423200 78442496 16647 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19151 16647 145 145 0 19006 0 [pid=14143] vsize: 76604 Current children cumulated CPU time (s) 589.17 Current children cumulated vsize (Kb) 78728 [startup+600.052 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18243 0 0 0 59824 91 0 0 25 0 1 0 1843423200 78888960 16760 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19260 16760 145 145 0 19115 0 [pid=14143] vsize: 77040 Current children cumulated CPU time (s) 599.16 Current children cumulated vsize (Kb) 79164 [startup+610.053 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18328 0 0 0 60823 91 0 0 25 0 1 0 1843423200 79224832 16845 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19342 16845 145 145 0 19197 0 [pid=14143] vsize: 77368 Current children cumulated CPU time (s) 609.15 Current children cumulated vsize (Kb) 79492 [startup+620.054 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18412 0 0 0 61821 92 0 0 25 0 1 0 1843423200 79552512 16929 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19422 16929 145 145 0 19277 0 [pid=14143] vsize: 77688 Current children cumulated CPU time (s) 619.14 Current children cumulated vsize (Kb) 79812 [startup+630.054 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18462 0 0 0 62820 93 0 0 25 0 1 0 1843423200 79749120 16979 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19470 16979 145 145 0 19325 0 [pid=14143] vsize: 77880 Current children cumulated CPU time (s) 629.14 Current children cumulated vsize (Kb) 80004 [startup+640.055 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18535 0 0 0 63818 94 0 0 25 0 1 0 1843423200 80035840 17052 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19540 17052 145 145 0 19395 0 [pid=14143] vsize: 78160 Current children cumulated CPU time (s) 639.13 Current children cumulated vsize (Kb) 80284 [startup+650.056 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18603 0 0 0 64817 95 0 0 25 0 1 0 1843423200 80306176 17120 4294967295 134512640 135094434 3221224448 3221223104 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19606 17120 145 145 0 19461 0 [pid=14143] vsize: 78424 Current children cumulated CPU time (s) 649.13 Current children cumulated vsize (Kb) 80548 [startup+660.057 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18663 0 0 0 65814 97 0 0 25 0 1 0 1843423200 80539648 17180 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19663 17180 145 145 0 19518 0 [pid=14143] vsize: 78652 Current children cumulated CPU time (s) 659.12 Current children cumulated vsize (Kb) 80776 [startup+670.059 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18761 0 0 0 66812 98 0 0 25 0 1 0 1843423200 80924672 17278 4294967295 134512640 135094434 3221224448 3221223060 134563134 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19757 17278 145 145 0 19612 0 [pid=14143] vsize: 79028 Current children cumulated CPU time (s) 669.11 Current children cumulated vsize (Kb) 81152 [startup+680.059 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18809 0 0 0 67811 99 0 0 25 0 1 0 1843423200 81117184 17326 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19804 17326 145 145 0 19659 0 [pid=14143] vsize: 79216 Current children cumulated CPU time (s) 679.11 Current children cumulated vsize (Kb) 81340 [startup+690.06 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18860 0 0 0 68810 100 0 0 25 0 1 0 1843423200 81317888 17377 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19853 17377 145 145 0 19708 0 [pid=14143] vsize: 79412 Current children cumulated CPU time (s) 689.11 Current children cumulated vsize (Kb) 81536 [startup+700.061 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18918 0 0 0 69808 101 0 0 25 0 1 0 1843423200 81543168 17435 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19908 17435 145 145 0 19763 0 [pid=14143] vsize: 79632 Current children cumulated CPU time (s) 699.1 Current children cumulated vsize (Kb) 81756 [startup+710.062 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 18983 0 0 0 70807 101 0 0 25 0 1 0 1843423200 81801216 17500 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 19971 17500 145 145 0 19826 0 [pid=14143] vsize: 79884 Current children cumulated CPU time (s) 709.09 Current children cumulated vsize (Kb) 82008 [startup+720.063 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19034 0 0 0 71805 102 0 0 25 0 1 0 1843423200 81997824 17551 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20019 17551 145 145 0 19874 0 [pid=14143] vsize: 80076 Current children cumulated CPU time (s) 719.08 Current children cumulated vsize (Kb) 82200 [startup+730.063 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19087 0 0 0 72804 103 0 0 25 0 1 0 1843423200 82206720 17604 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20070 17604 145 145 0 19925 0 [pid=14143] vsize: 80280 Current children cumulated CPU time (s) 729.08 Current children cumulated vsize (Kb) 82404 [startup+740.065 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19280 0 0 0 73800 105 0 0 25 0 1 0 1843423200 82984960 17797 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20260 17797 145 145 0 20115 0 [pid=14143] vsize: 81040 Current children cumulated CPU time (s) 739.06 Current children cumulated vsize (Kb) 83164 [startup+750.066 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19346 0 0 0 74799 106 0 0 25 0 1 0 1843423200 83243008 17863 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20323 17863 145 145 0 20178 0 [pid=14143] vsize: 81292 Current children cumulated CPU time (s) 749.06 Current children cumulated vsize (Kb) 83416 [startup+760.067 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19408 0 0 0 75798 106 0 0 25 0 1 0 1843423200 83484672 17925 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20382 17925 145 145 0 20237 0 [pid=14143] vsize: 81528 Current children cumulated CPU time (s) 759.05 Current children cumulated vsize (Kb) 83652 [startup+770.068 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19452 0 0 0 76797 107 0 0 25 0 1 0 1843423200 83656704 17969 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20424 17969 145 145 0 20279 0 [pid=14143] vsize: 81696 Current children cumulated CPU time (s) 769.05 Current children cumulated vsize (Kb) 83820 [startup+780.068 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19515 0 0 0 77795 108 0 0 25 0 1 0 1843423200 83906560 18032 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/14143/statm): 20485 18032 145 145 0 20340 0 [pid=14143] vsize: 81940 Current children cumulated CPU time (s) 779.04 Current children cumulated vsize (Kb) 84064 [startup+790.069 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19593 0 0 0 78793 109 0 0 25 0 1 0 1843423200 84213760 18110 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20560 18110 145 145 0 20415 0 [pid=14143] vsize: 82240 Current children cumulated CPU time (s) 789.03 Current children cumulated vsize (Kb) 84364 [startup+800.07 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19698 0 0 0 79791 110 0 0 25 0 1 0 1843423200 84631552 18215 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20662 18215 145 145 0 20517 0 [pid=14143] vsize: 82648 Current children cumulated CPU time (s) 799.02 Current children cumulated vsize (Kb) 84772 [startup+810.07 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19760 0 0 0 80790 110 0 0 25 0 1 0 1843423200 84873216 18277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20721 18277 145 145 0 20576 0 [pid=14143] vsize: 82884 Current children cumulated CPU time (s) 809.01 Current children cumulated vsize (Kb) 85008 [startup+820.071 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19866 0 0 0 81788 112 0 0 25 0 1 0 1843423200 85299200 18383 4294967295 134512640 135094434 3221224448 3221223120 134554872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20825 18383 145 145 0 20680 0 [pid=14143] vsize: 83300 Current children cumulated CPU time (s) 819.01 Current children cumulated vsize (Kb) 85424 [startup+830.071 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19915 0 0 0 82787 112 0 0 25 0 1 0 1843423200 85491712 18432 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20872 18432 145 145 0 20727 0 [pid=14143] vsize: 83488 Current children cumulated CPU time (s) 829 Current children cumulated vsize (Kb) 85612 [startup+840.073 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 19988 0 0 0 83786 113 0 0 25 0 1 0 1843423200 85778432 18505 4294967295 134512640 135094434 3221224448 3221223060 134563145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20942 18505 145 145 0 20797 0 [pid=14143] vsize: 83768 Current children cumulated CPU time (s) 839 Current children cumulated vsize (Kb) 85892 [startup+850.074 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20045 0 0 0 84784 114 0 0 25 0 1 0 1843423200 86003712 18562 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 20997 18562 145 145 0 20852 0 [pid=14143] vsize: 83988 Current children cumulated CPU time (s) 848.99 Current children cumulated vsize (Kb) 86112 [startup+860.074 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20100 0 0 0 85784 114 0 0 25 0 1 0 1843423200 86220800 18617 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21050 18617 145 145 0 20905 0 [pid=14143] vsize: 84200 Current children cumulated CPU time (s) 858.99 Current children cumulated vsize (Kb) 86324 [startup+870.075 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20179 0 0 0 86782 115 0 0 25 0 1 0 1843423200 86532096 18696 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21126 18696 145 145 0 20981 0 [pid=14143] vsize: 84504 Current children cumulated CPU time (s) 868.98 Current children cumulated vsize (Kb) 86628 [startup+880.075 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 87778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 878.96 Current children cumulated vsize (Kb) 87904 [startup+890.076 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 88778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 888.96 Current children cumulated vsize (Kb) 87904 [startup+900.077 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 89778 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 898.96 Current children cumulated vsize (Kb) 87904 [startup+910.078 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 90779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 908.97 Current children cumulated vsize (Kb) 87904 [startup+920.079 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 91779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 918.97 Current children cumulated vsize (Kb) 87904 [startup+930.079 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 92779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 928.97 Current children cumulated vsize (Kb) 87904 [startup+940.08 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 93779 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 938.97 Current children cumulated vsize (Kb) 87904 [startup+950.081 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 94780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 948.98 Current children cumulated vsize (Kb) 87904 [startup+960.082 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 95780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 958.98 Current children cumulated vsize (Kb) 87904 [startup+970.083 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 96780 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 968.98 Current children cumulated vsize (Kb) 87904 [startup+980.083 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 97781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223180 134561436 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 978.99 Current children cumulated vsize (Kb) 87904 [startup+990.084 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 98781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 988.99 Current children cumulated vsize (Kb) 87904 [startup+1000.08 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 99781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 998.99 Current children cumulated vsize (Kb) 87904 [startup+1010.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 100781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1008.99 Current children cumulated vsize (Kb) 87904 [startup+1020.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 101781 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223088 134562161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1018.99 Current children cumulated vsize (Kb) 87904 [startup+1030.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 102782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1029 Current children cumulated vsize (Kb) 87904 [startup+1040.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 103782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1039 Current children cumulated vsize (Kb) 87904 [startup+1050.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 104782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1049 Current children cumulated vsize (Kb) 87904 [startup+1060.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 105782 117 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1059 Current children cumulated vsize (Kb) 87904 [startup+1070.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 106782 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554760 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1069.01 Current children cumulated vsize (Kb) 87904 [startup+1080.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 107783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1079.02 Current children cumulated vsize (Kb) 87904 [startup+1090.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 108783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1089.02 Current children cumulated vsize (Kb) 87904 [startup+1100.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 109783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1099.02 Current children cumulated vsize (Kb) 87904 [startup+1110.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 110783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1109.02 Current children cumulated vsize (Kb) 87904 [startup+1120.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 111783 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1119.02 Current children cumulated vsize (Kb) 87904 [startup+1130.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 112784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1129.03 Current children cumulated vsize (Kb) 87904 [startup+1140.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 113784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1139.03 Current children cumulated vsize (Kb) 87904 [startup+1150.09 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 114784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1149.03 Current children cumulated vsize (Kb) 87904 [startup+1160.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 115784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1159.03 Current children cumulated vsize (Kb) 87904 [startup+1170.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 116784 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1169.03 Current children cumulated vsize (Kb) 87904 [startup+1180.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 117785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1179.04 Current children cumulated vsize (Kb) 87904 [startup+1190.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 118785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1189.04 Current children cumulated vsize (Kb) 87904 [startup+1200.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 119785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1199.04 Current children cumulated vsize (Kb) 87904 [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 120785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1209.04 Current children cumulated vsize (Kb) 87904 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 0.99 0.98 2/57 14143 Raw data (/proc/14139/stat): 14139 (minisat+_script) S 14138 14139 4419 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843423195 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/14139/statm): 531 226 485 147 0 384 0 [pid=14139] vsize: 2124 Raw data (/proc/14143/stat): 14143 (minisat+_64-bit) R 14139 14139 4419 0 -1 0 20593 0 0 0 120785 118 0 0 25 0 1 0 1843423200 87838720 18983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/14143/statm): 21445 18983 145 145 0 21300 0 [pid=14143] vsize: 85780 Current children cumulated CPU time (s) 1209.04 Current children cumulated vsize (Kb) 87904 Sending SIGTERM to -14139 Sleeping 2 seconds One traced child (pid=14139) ended because it received signal 15 (SIGTERM) One traced child (pid=14143) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1209.09 CPU user time (s): 1207.86 CPU system time (s): 1.22381 CPU usage (%): 99.9125 Max. virtual memory (cumulated for all children) (Kb): 87904
ERROR: no interpretation found !