Name | mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst2.opb |
MD5SUM | 3c3e6264ad2029dcb2dc81be78ef5988 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 20 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 1048575 |
Number of bits of the sum of numbers in the objective function | 20 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 13633395 |
Number of bits of the biggest sum of numbers | 24 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 9183 |
Total number of constraints | 632 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 40 |
Number of constraints which are nor clauses,nor cardinality constraints | 592 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 260 |
LAUNCH ON wulflinc13 THE 2005-09-20 05:10:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3439 boxname=wulflinc13 idbench=1095 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3c3e6264ad2029dcb2dc81be78ef5988 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-bienst2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-bienst2.opb IDLAUNCH: 3439 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 2 cpu MHz : 451.242 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: 894796 kB Buffers: 32848 kB Cached: 79536 kB SwapCached: 700 kB Active: 40328 kB Inactive: 74708 kB HighTotal: 131008 kB HighFree: 47600 kB LowTotal: 903652 kB LowFree: 847196 kB SwapTotal: 2097136 kB SwapFree: 2095936 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5744 kB Slab: 19136 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:30:41 (client local time) WITH STATUS 0 IN 1208.08 SECONDS stats: 3439 7 1208.08 0
c Parsing PB file... c Converting 725 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 724]---> BDD-cost: 7 c ---[ 723]---> BDD-cost: 7 c ---[ 722]---> BDD-cost: 7 c ---[ 721]---> BDD-cost: 7 c ---[ 720]---> BDD-cost: 7 c ---[ 719]---> BDD-cost: 7 c ---[ 718]---> BDD-cost: 7 c ---[ 717]---> BDD-cost: 7 c ---[ 716]---> BDD-cost: 7 c ---[ 715]---> BDD-cost: 7 c ---[ 714]---> BDD-cost: 7 c ---[ 713]---> BDD-cost: 7 c ---[ 712]---> BDD-cost: 7 c ---[ 711]---> BDD-cost: 7 c ---[ 710]---> BDD-cost: 7 c ---[ 709]---> BDD-cost: 7 c ---[ 708]---> BDD-cost: 7 c ---[ 707]---> BDD-cost: 7 c ---[ 706]---> BDD-cost: 7 c ---[ 705]---> BDD-cost: 7 c ---[ 704]---> BDD-cost: 7 c ---[ 702]---> Adder-cost: 334 maxlim: 113401 bits: 18/17 c ---[ 700]---> Adder-cost: 334 maxlim: 113785 bits: 18/17 c ---[ 698]---> Adder-cost: 326 maxlim: 121209 bits: 18/17 c ---[ 696]---> Adder-cost: 326 maxlim: 121337 bits: 18/17 c ---[ 694]---> Adder-cost: 334 maxlim: 113017 bits: 18/17 c ---[ 692]---> Adder-cost: 343 maxlim: 97529 bits: 18/17 c ---[ 690]---> Adder-cost: 334 maxlim: 113017 bits: 18/17 c ---[ 688]---> Adder-cost: 338 maxlim: 162041 bits: 18/18 c ---[ 686]---> Adder-cost: 338 maxlim: 161913 bits: 18/18 c ---[ 684]---> Adder-cost: 338 maxlim: 162169 bits: 18/18 c ---[ 682]---> Adder-cost: 338 maxlim: 162297 bits: 18/18 c ---[ 680]---> Adder-cost: 352 maxlim: 146297 bits: 19/18 c ---[ 678]---> Adder-cost: 352 maxlim: 146297 bits: 19/18 c ---[ 676]---> Adder-cost: 352 maxlim: 146297 bits: 19/18 c ---[ 674]---> Adder-cost: 314 maxlim: 80249 bits: 17/17 c ---[ 672]---> Adder-cost: 314 maxlim: 80761 bits: 17/17 c ---[ 670]---> Adder-cost: 314 maxlim: 80505 bits: 17/17 c ---[ 668]---> Adder-cost: 314 maxlim: 81145 bits: 17/17 c ---[ 666]---> Adder-cost: 328 maxlim: 73081 bits: 18/17 c ---[ 664]---> Adder-cost: 328 maxlim: 72313 bits: 18/17 c ---[ 662]---> Adder-cost: 328 maxlim: 72697 bits: 18/17 c ---[ 660]---> Adder-cost: 314 maxlim: 81017 bits: 17/17 c ---[ 658]---> Adder-cost: 314 maxlim: 80889 bits: 17/17 c ---[ 656]---> Adder-cost: 314 maxlim: 79993 bits: 17/17 c ---[ 654]---> Adder-cost: 314 maxlim: 81017 bits: 17/17 c ---[ 652]---> Adder-cost: 328 maxlim: 72953 bits: 18/17 c ---[ 650]---> Adder-cost: 328 maxlim: 72313 bits: 18/17 c ---[ 648]---> Adder-cost: 328 maxlim: 72569 bits: 18/17 c ---[ 646]---> Adder-cost: 334 maxlim: 113657 bits: 18/17 c ---[ 644]---> Adder-cost: 326 maxlim: 121337 bits: 18/17 c ---[ 642]---> Adder-cost: 326 maxlim: 121337 bits: 18/17 c ---[ 640]---> Adder-cost: 334 maxlim: 113529 bits: 18/17 c ---[ 638]---> Adder-cost: 343 maxlim: 97145 bits: 18/17 c ---[ 636]---> Adder-cost: 334 maxlim: 112889 bits: 18/17 c ---[ 634]---> Adder-cost: 334 maxlim: 113273 bits: 18/17 c ---[ 632]---> Adder-cost: 328 maxlim: 97657 bits: 18/17 c ---[ 630]---> Adder-cost: 322 maxlim: 105081 bits: 18/17 c ---[ 628]---> Adder-cost: 322 maxlim: 105081 bits: 18/17 c ---[ 626]---> Adder-cost: 322 maxlim: 105593 bits: 18/17 c ---[ 624]---> Adder-cost: 322 maxlim: 105337 bits: 18/17 c ---[ 622]---> Adder-cost: 328 maxlim: 96377 bits: 18/17 c ---[ 620]---> Adder-cost: 328 maxlim: 96761 bits: 18/17 c ---[ 618]---> Adder-cost: 320 maxlim: 97529 bits: 18/17 c ---[ 616]---> Adder-cost: 320 maxlim: 97145 bits: 18/17 c ---[ 614]---> Adder-cost: 320 maxlim: 97401 bits: 18/17 c ---[ 612]---> Adder-cost: 320 maxlim: 96505 bits: 18/17 c ---[ 610]---> Adder-cost: 320 maxlim: 97017 bits: 18/17 c ---[ 608]---> Adder-cost: 328 maxlim: 88569 bits: 18/17 c ---[ 606]---> Adder-cost: 328 maxlim: 89209 bits: 18/17 c ---[ 604]---> Adder-cost: 314 maxlim: 80505 bits: 17/17 c ---[ 602]---> Adder-cost: 314 maxlim: 81017 bits: 17/17 c ---[ 600]---> Adder-cost: 314 maxlim: 80889 bits: 17/17 c ---[ 598]---> Adder-cost: 314 maxlim: 81145 bits: 17/17 c ---[ 596]---> Adder-cost: 314 maxlim: 80633 bits: 17/17 c ---[ 594]---> Adder-cost: 328 maxlim: 73081 bits: 18/17 c ---[ 592]---> Adder-cost: 328 maxlim: 71929 bits: 18/17 c ---[ 591]---> BDD-cost: 52 c ---[ 590]---> BDD-cost: 52 c ---[ 589]---> BDD-cost: 52 c ---[ 588]---> BDD-cost: 52 c ---[ 587]---> BDD-cost: 52 c ---[ 586]---> BDD-cost: 52 c ---[ 585]---> BDD-cost: 52 c ---[ 584]---> BDD-cost: 50 c ---[ 583]---> BDD-cost: 52 c ---[ 582]---> BDD-cost: 52 c ---[ 581]---> BDD-cost: 52 c ---[ 580]---> BDD-cost: 52 c ---[ 579]---> BDD-cost: 52 c ---[ 578]---> BDD-cost: 52 c ---[ 577]---> BDD-cost: 50 c ---[ 576]---> BDD-cost: 50 c ---[ 575]---> BDD-cost: 52 c ---[ 574]---> BDD-cost: 52 c ---[ 573]---> BDD-cost: 52 c ---[ 572]---> BDD-cost: 52 c ---[ 571]---> BDD-cost: 52 c ---[ 570]---> BDD-cost: 52 c ---[ 569]---> BDD-cost: 50 c ---[ 568]---> BDD-cost: 52 c ---[ 567]---> BDD-cost: 50 c ---[ 566]---> BDD-cost: 52 c ---[ 565]---> BDD-cost: 52 c ---[ 564]---> BDD-cost: 52 c ---[ 563]---> BDD-cost: 52 c ---[ 562]---> BDD-cost: 50 c ---[ 561]---> BDD-cost: 52 c ---[ 560]---> BDD-cost: 52 c ---[ 559]---> BDD-cost: 52 c ---[ 558]---> BDD-cost: 52 c ---[ 557]---> BDD-cost: 52 c ---[ 556]---> BDD-cost: 54 c ---[ 555]---> BDD-cost: 54 c ---[ 554]---> BDD-cost: 54 c ---[ 553]---> BDD-cost: 54 c ---[ 552]---> BDD-cost: 54 c ---[ 551]---> BDD-cost: 54 c ---[ 550]---> BDD-cost: 54 c ---[ 549]---> BDD-cost: 54 c ---[ 548]---> BDD-cost: 54 c ---[ 547]---> BDD-cost: 54 c ---[ 546]---> BDD-cost: 54 c ---[ 545]---> BDD-cost: 54 c ---[ 544]---> BDD-cost: 54 c ---[ 543]---> BDD-cost: 54 c ---[ 542]---> BDD-cost: 52 c ---[ 541]---> BDD-cost: 52 c ---[ 540]---> BDD-cost: 52 c ---[ 539]---> BDD-cost: 52 c ---[ 538]---> BDD-cost: 52 c ---[ 537]---> BDD-cost: 52 c ---[ 536]---> BDD-cost: 52 c ---[ 534]---> Sorter-cost: 1851 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 532]---> Sorter-cost: 1875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 530]---> Sorter-cost: 1875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 528]---> Sorter-cost: 1851 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 526]---> Sorter-cost: 1851 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 524]---> Sorter-cost: 1875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 522]---> Sorter-cost: 1875 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 520]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 518]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 516]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 512]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 510]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 508]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 506]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 504]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 502]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 500]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 498]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 496]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 494]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 492]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 490]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 488]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 486]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 484]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 482]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 480]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 478]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 476]---> Sorter-cost: 1701 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 474]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 472]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 470]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 468]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 466]---> Sorter-cost: 1848 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 464]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 462]---> Sorter-cost: 1981 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 460]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 458]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 456]---> Sorter-cost: 1981 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 454]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 452]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 450]---> Sorter-cost: 1981 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 448]---> Sorter-cost: 1981 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[ 446]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 444]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 442]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 440]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 438]---> Sorter-cost: 1984 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 436]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 434]---> Sorter-cost: 1913 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 432]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 430]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 428]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 426]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 424]---> Sorter-cost: 1834 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 422]---> BDD-cost: 93 c ---[ 420]---> BDD-cost: 93 c ---[ 418]---> BDD-cost: 93 c ---[ 416]---> BDD-cost: 93 c ---[ 414]---> BDD-cost: 93 c ---[ 412]---> BDD-cost: 50 c ---[ 410]---> BDD-cost: 50 c ---[ 408]---> BDD-cost: 50 c ---[ 406]---> BDD-cost: 15 c ---[ 404]---> BDD-cost: 15 c ---[ 402]---> BDD-cost: 15 c ---[ 400]---> BDD-cost: 15 c ---[ 398]---> BDD-cost: 15 c ---[ 396]---> Sorter-cost: 750 Base: 2 2 2 2 2 2 2 c ---[ 394]---> Sorter-cost: 750 Base: 2 2 2 2 2 2 2 c ---[ 392]---> Sorter-cost: 750 Base: 2 2 2 2 2 2 2 c ---[ 391]---> BDD-cost: 20 c ---[ 390]---> BDD-cost: 20 c ---[ 389]---> BDD-cost: 20 c ---[ 388]---> BDD-cost: 20 c ---[ 387]---> BDD-cost: 20 c ---[ 386]---> BDD-cost: 20 c ---[ 385]---> BDD-cost: 20 c ---[ 384]---> BDD-cost: 15 c ---[ 383]---> BDD-cost: 15 c ---[ 382]---> BDD-cost: 15 c ---[ 381]---> BDD-cost: 15 c ---[ 380]---> BDD-cost: 15 c ---[ 379]---> BDD-cost: 15 c ---[ 378]---> BDD-cost: 21 c ---[ 377]---> BDD-cost: 21 c ---[ 376]---> BDD-cost: 21 c ---[ 375]---> BDD-cost: 21 c ---[ 374]---> BDD-cost: 21 c ---[ 373]---> BDD-cost: 21 c ---[ 372]---> BDD-cost: 19 c ---[ 371]---> BDD-cost: 19 c ---[ 370]---> BDD-cost: 19 c ---[ 369]---> BDD-cost: 19 c ---[ 368]---> BDD-cost: 19 c ---[ 367]---> BDD-cost: 19 c ---[ 366]---> BDD-cost: 18 c ---[ 365]---> BDD-cost: 18 c ---[ 364]---> BDD-cost: 18 c ---[ 363]---> BDD-cost: 18 c ---[ 362]---> BDD-cost: 18 c ---[ 361]---> BDD-cost: 18 c ---[ 360]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 359]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 358]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 357]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 356]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 355]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 354]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 353]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 352]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 351]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 349]---> Sorter-cost: 181 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 348]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 347]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 346]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 345]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 344]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 343]---> Sorter-cost: 670 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 342]---> BDD-cost: 21 c ---[ 341]---> BDD-cost: 21 c ---[ 340]---> BDD-cost: 21 c ---[ 339]---> BDD-cost: 21 c ---[ 338]---> BDD-cost: 21 c ---[ 337]---> BDD-cost: 21 c ---[ 336]---> BDD-cost: 21 c ---[ 335]---> BDD-cost: 21 c ---[ 334]---> BDD-cost: 21 c ---[ 333]---> BDD-cost: 21 c ---[ 332]---> BDD-cost: 21 c ---[ 331]---> BDD-cost: 21 c ---[ 330]---> BDD-cost: 21 c ---[ 329]---> BDD-cost: 20 c ---[ 328]---> BDD-cost: 20 c ---[ 327]---> BDD-cost: 20 c ---[ 326]---> BDD-cost: 20 c ---[ 325]---> BDD-cost: 20 c ---[ 324]---> BDD-cost: 20 c ---[ 323]---> BDD-cost: 19 c ---[ 322]---> BDD-cost: 19 c ---[ 321]---> BDD-cost: 19 c ---[ 320]---> BDD-cost: 19 c ---[ 319]---> BDD-cost: 19 c ---[ 318]---> BDD-cost: 19 c ---[ 317]---> BDD-cost: 21 c ---[ 316]---> BDD-cost: 21 c ---[ 315]---> BDD-cost: 21 c ---[ 314]---> BDD-cost: 21 c ---[ 313]---> BDD-cost: 21 c ---[ 312]---> BDD-cost: 21 c ---[ 311]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 310]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 309]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 308]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 307]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 306]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 305]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 304]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 303]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 302]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 301]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 300]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 299]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 298]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 297]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 296]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 295]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 294]---> Sorter-cost: 182 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 293]---> BDD-cost: 18 c ---[ 292]---> BDD-cost: 18 c ---[ 291]---> BDD-cost: 18 c ---[ 290]---> BDD-cost: 18 c ---[ 289]---> BDD-cost: 18 c ---[ 288]---> BDD-cost: 18 c ---[ 287]---> BDD-cost: 18 c ---[ 286]---> BDD-cost: 18 c ---[ 285]---> BDD-cost: 18 c ---[ 284]---> BDD-cost: 18 c ---[ 283]---> BDD-cost: 18 c ---[ 282]---> BDD-cost: 18 c ---[ 281]---> BDD-cost: 19 c ---[ 280]---> BDD-cost: 19 c ---[ 279]---> BDD-cost: 19 c ---[ 278]---> BDD-cost: 19 c ---[ 277]---> BDD-cost: 19 c ---[ 276]---> BDD-cost: 19 c ---[ 275]---> BDD-cost: 19 c ---[ 274]---> BDD-cost: 17 c ---[ 273]---> BDD-cost: 17 c ---[ 272]---> BDD-cost: 17 c ---[ 271]---> BDD-cost: 17 c ---[ 270]---> BDD-cost: 17 c ---[ 269]---> BDD-cost: 17 c ---[ 268]---> BDD-cost: 19 c ---[ 267]---> BDD-cost: 19 c ---[ 266]---> BDD-cost: 19 c ---[ 265]---> BDD-cost: 19 c ---[ 264]---> BDD-cost: 19 c ---[ 263]---> BDD-cost: 19 c ---[ 262]---> Sorter-cost: 530 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 261]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 260]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 259]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 258]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 257]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 256]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 255]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 253]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 251]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 250]---> Sorter-cost: 618 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 249]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 248]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 247]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 246]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 245]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 244]---> BDD-cost: 16 c ---[ 243]---> BDD-cost: 16 c ---[ 242]---> BDD-cost: 16 c ---[ 241]---> BDD-cost: 16 c ---[ 240]---> BDD-cost: 16 c ---[ 239]---> BDD-cost: 16 c ---[ 238]---> BDD-cost: 19 c ---[ 237]---> BDD-cost: 19 c ---[ 236]---> BDD-cost: 19 c ---[ 235]---> BDD-cost: 19 c ---[ 234]---> BDD-cost: 19 c ---[ 233]---> BDD-cost: 19 c ---[ 232]---> BDD-cost: 15 c ---[ 231]---> BDD-cost: 15 c ---[ 230]---> BDD-cost: 15 c ---[ 229]---> BDD-cost: 15 c ---[ 228]---> BDD-cost: 15 c ---[ 227]---> BDD-cost: 15 c ---[ 226]---> BDD-cost: 19 c ---[ 225]---> BDD-cost: 19 c ---[ 224]---> BDD-cost: 19 c ---[ 223]---> BDD-cost: 19 c ---[ 222]---> BDD-cost: 19 c ---[ 221]---> BDD-cost: 19 c ---[ 220]---> BDD-cost: 19 c ---[ 219]---> BDD-cost: 16 c ---[ 218]---> BDD-cost: 16 c ---[ 217]---> BDD-cost: 16 c ---[ 216]---> BDD-cost: 16 c ---[ 215]---> BDD-cost: 16 c ---[ 214]---> BDD-cost: 16 c ---[ 213]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 212]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 211]---> Sorter-cost: 517 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 210]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 209]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 208]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 207]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 206]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 205]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 204]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 203]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 202]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 201]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 200]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 199]---> Sorter-cost: 457 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 198]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> BDD-cost: 21 c ---[ 194]---> BDD-cost: 21 c ---[ 193]---> BDD-cost: 21 c ---[ 192]---> BDD-cost: 21 c ---[ 191]---> BDD-cost: 21 c ---[ 190]---> BDD-cost: 21 c ---[ 189]---> BDD-cost: 19 c ---[ 188]---> BDD-cost: 19 c ---[ 187]---> BDD-cost: 19 c ---[ 186]---> BDD-cost: 19 c ---[ 185]---> BDD-cost: 19 c ---[ 184]---> BDD-cost: 19 c ---[ 183]---> BDD-cost: 19 c ---[ 182]---> BDD-cost: 19 c ---[ 181]---> BDD-cost: 19 c ---[ 180]---> BDD-cost: 19 c ---[ 179]---> BDD-cost: 19 c ---[ 178]---> BDD-cost: 19 c ---[ 177]---> BDD-cost: 20 c ---[ 176]---> BDD-cost: 20 c ---[ 175]---> BDD-cost: 20 c ---[ 174]---> BDD-cost: 20 c ---[ 173]---> BDD-cost: 20 c ---[ 172]---> BDD-cost: 20 c ---[ 171]---> BDD-cost: 21 c ---[ 170]---> BDD-cost: 21 c ---[ 169]---> BDD-cost: 21 c ---[ 168]---> BDD-cost: 21 c ---[ 167]---> BDD-cost: 21 c ---[ 166]---> BDD-cost: 21 c ---[ 165]---> BDD-cost: 21 c ---[ 164]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 163]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 161]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 159]---> Sorter-cost: 180 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 157]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 156]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 155]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 154]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 153]---> Sorter-cost: 668 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 152]---> BDD-cost: 29 c ---[ 151]---> BDD-cost: 29 c ---[ 150]---> BDD-cost: 29 c ---[ 149]---> BDD-cost: 29 c ---[ 148]---> BDD-cost: 29 c ---[ 147]---> BDD-cost: 29 c ---[ 146]---> BDD-cost: 21 c ---[ 145]---> BDD-cost: 21 c ---[ 144]---> BDD-cost: 21 c ---[ 143]---> BDD-cost: 21 c ---[ 142]---> BDD-cost: 21 c ---[ 141]---> BDD-cost: 21 c ---[ 140]---> BDD-cost: 19 c ---[ 139]---> BDD-cost: 19 c ---[ 138]---> BDD-cost: 19 c ---[ 137]---> BDD-cost: 19 c ---[ 136]---> BDD-cost: 19 c ---[ 135]---> BDD-cost: 19 c ---[ 134]---> BDD-cost: 19 c ---[ 133]---> BDD-cost: 19 c ---[ 132]---> BDD-cost: 19 c ---[ 131]---> BDD-cost: 19 c ---[ 130]---> BDD-cost: 19 c ---[ 129]---> BDD-cost: 19 c ---[ 128]---> BDD-cost: 19 c ---[ 127]---> BDD-cost: 19 c ---[ 126]---> BDD-cost: 19 c ---[ 125]---> BDD-cost: 19 c ---[ 124]---> BDD-cost: 19 c ---[ 123]---> BDD-cost: 19 c ---[ 122]---> BDD-cost: 19 c ---[ 121]---> BDD-cost: 19 c ---[ 120]---> BDD-cost: 19 c ---[ 119]---> BDD-cost: 19 c ---[ 118]---> BDD-cost: 19 c ---[ 117]---> BDD-cost: 19 c ---[ 116]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 115]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 113]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 111]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 109]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 107]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 105]---> Sorter-cost: 608 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 103]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 102]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 101]---> Sorter-cost: 524 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 100]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 99]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 98]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 97]---> BDD-cost: 19 c ---[ 96]---> BDD-cost: 19 c ---[ 95]---> BDD-cost: 19 c ---[ 94]---> BDD-cost: 19 c ---[ 93]---> BDD-cost: 19 c ---[ 92]---> BDD-cost: 19 c ---[ 91]---> BDD-cost: 16 c ---[ 90]---> BDD-cost: 16 c ---[ 89]---> BDD-cost: 16 c ---[ 88]---> BDD-cost: 16 c ---[ 87]---> BDD-cost: 16 c ---[ 86]---> BDD-cost: 16 c ---[ 85]---> BDD-cost: 18 c ---[ 84]---> BDD-cost: 18 c ---[ 83]---> BDD-cost: 18 c ---[ 82]---> BDD-cost: 18 c ---[ 81]---> BDD-cost: 18 c ---[ 80]---> BDD-cost: 18 c ---[ 79]---> BDD-cost: 19 c ---[ 78]---> BDD-cost: 19 c ---[ 77]---> BDD-cost: 19 c ---[ 76]---> BDD-cost: 19 c ---[ 75]---> BDD-cost: 19 c ---[ 74]---> BDD-cost: 19 c ---[ 73]---> BDD-cost: 19 c ---[ 72]---> BDD-cost: 19 c ---[ 71]---> BDD-cost: 19 c ---[ 70]---> BDD-cost: 19 c ---[ 69]---> BDD-cost: 19 c ---[ 68]---> BDD-cost: 19 c ---[ 67]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 65]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 62]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 61]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 53]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 52]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 51]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 50]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 49]---> Sorter-cost: 522 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 48]---> BDD-cost: 18 c ---[ 47]---> BDD-cost: 18 c ---[ 46]---> BDD-cost: 18 c ---[ 45]---> BDD-cost: 18 c ---[ 44]---> BDD-cost: 18 c ---[ 43]---> BDD-cost: 18 c ---[ 42]---> BDD-cost: 18 c ---[ 41]---> BDD-cost: 18 c ---[ 40]---> BDD-cost: 18 c ---[ 39]---> BDD-cost: 18 c ---[ 38]---> BDD-cost: 18 c ---[ 37]---> BDD-cost: 18 c ---[ 36]---> BDD-cost: 19 c ---[ 35]---> BDD-cost: 19 c ---[ 34]---> BDD-cost: 19 c ---[ 33]---> BDD-cost: 19 c ---[ 32]---> BDD-cost: 19 c ---[ 31]---> BDD-cost: 19 c ---[ 30]---> BDD-cost: 19 c ---[ 29]---> BDD-cost: 19 c ---[ 28]---> BDD-cost: 19 c ---[ 27]---> BDD-cost: 19 c ---[ 26]---> BDD-cost: 19 c ---[ 25]---> BDD-cost: 19 c ---[ 24]---> BDD-cost: 19 c ---[ 23]---> BDD-cost: 19 c ---[ 22]---> BDD-cost: 19 c ---[ 21]---> BDD-cost: 19 c ---[ 20]---> BDD-cost: 19 c ---[ 19]---> BDD-cost: 19 c ---[ 18]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 17]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 16]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 15]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 14]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 13]---> Sorter-cost: 380 Base: 2 2 2 2 2 2 2 2 2 7 c ---[ 12]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 5]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 4]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 3]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 2]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 1]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ---[ 0]---> Sorter-cost: 666 Base: 2 2 2 2 2 3 5 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 552683 1443539 | 184227 0 0 nan | 0.000 % | c | 101 | 552622 1443396 | 202649 96 741 7.7 | 3.822 % | c | 251 | 552418 1442952 | 222914 222 1347 6.1 | 3.855 % | c | 476 | 552277 1442642 | 245206 441 2460 5.6 | 3.878 % | c | 813 | 552156 1442378 | 269726 767 4316 5.6 | 3.898 % | c | 1319 | 551867 1441745 | 296699 1243 6992 5.6 | 3.944 % | c | 2078 | 551642 1441241 | 326369 1980 11537 5.8 | 3.979 % | c | 3219 | 551519 1440960 | 359006 3113 25439 8.2 | 3.997 % | c | 4927 | 551348 1440569 | 394906 4806 45981 9.6 | 4.021 % | c | 7489 | 551101 1440027 | 434397 7352 101130 13.8 | 4.059 % | c | 11333 | 550488 1438660 | 477837 11152 144294 12.9 | 4.153 % | c | 17099 | 550038 1437650 | 525621 16889 232388 13.8 | 4.220 % | c | 25748 | 548779 1434865 | 578183 25394 354007 13.9 | 4.422 % | c | 38722 | 547220 1431359 | 636001 38213 545026 14.3 | 4.667 % | c | 58186 | 546383 1429444 | 699601 57596 869826 15.1 | 4.793 % | c | 87378 | 545447 1427309 | 769561 86697 1630406 18.8 | 4.937 % | c | 131168 | 544860 1425980 | 846518 130423 3595472 27.6 | 5.024 % | c | 196852 | 543564 1423056 | 931169 195960 6063132 30.9 | 5.232 % |
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/22513/stat): 22513 (minisat+_script) R 22512 22513 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797702590 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22513/statm): 174 3 169 147 0 27 0 [pid=22513] 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=22514 New process pid=22515 New process pid=22516 execve syscall for /bin/sed executable 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=22515) exited with status: 0 One traced child (pid=22516) exited with status: 0 One traced child (pid=22514) exited with status: 0 New process pid=22517 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-bienst2.opb [startup+10.0039 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15371 0 0 0 873 63 0 0 25 0 1 0 1797702595 69021696 14658 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 16851 14658 145 145 0 16706 0 [pid=22517] vsize: 67404 Current children cumulated CPU time (s) 9.36 Current children cumulated vsize (Kb) 69528 [startup+20.0046 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15656 0 0 0 1870 65 0 0 25 0 1 0 1797702595 69820416 14943 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17046 14943 145 145 0 16901 0 [pid=22517] vsize: 68184 Current children cumulated CPU time (s) 19.35 Current children cumulated vsize (Kb) 70308 [startup+30.0053 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15685 0 0 0 2869 65 0 0 25 0 1 0 1797702595 69935104 14972 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22517/statm): 17074 14972 145 145 0 16929 0 [pid=22517] vsize: 68296 Current children cumulated CPU time (s) 29.34 Current children cumulated vsize (Kb) 70420 [startup+40.0059 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15732 0 0 0 3867 66 0 0 25 0 1 0 1797702595 70135808 15019 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17123 15019 145 145 0 16978 0 [pid=22517] vsize: 68492 Current children cumulated CPU time (s) 39.33 Current children cumulated vsize (Kb) 70616 [startup+50.0075 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15762 0 0 0 4867 66 0 0 25 0 1 0 1797702595 70254592 15049 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17152 15049 145 145 0 17007 0 [pid=22517] vsize: 68608 Current children cumulated CPU time (s) 49.33 Current children cumulated vsize (Kb) 70732 [startup+60.0082 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15805 0 0 0 5866 66 0 0 25 0 1 0 1797702595 70426624 15092 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17194 15092 145 145 0 17049 0 [pid=22517] vsize: 68776 Current children cumulated CPU time (s) 59.32 Current children cumulated vsize (Kb) 70900 [startup+70.0089 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15850 0 0 0 6866 66 0 0 25 0 1 0 1797702595 70606848 15137 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17238 15137 145 145 0 17093 0 [pid=22517] vsize: 68952 Current children cumulated CPU time (s) 69.32 Current children cumulated vsize (Kb) 71076 [startup+80.0095 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15908 0 0 0 7865 67 0 0 25 0 1 0 1797702595 70840320 15195 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17295 15195 145 145 0 17150 0 [pid=22517] vsize: 69180 Current children cumulated CPU time (s) 79.32 Current children cumulated vsize (Kb) 71304 [startup+90.0092 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15934 0 0 0 8865 67 0 0 25 0 1 0 1797702595 70942720 15221 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17320 15221 145 145 0 17175 0 [pid=22517] vsize: 69280 Current children cumulated CPU time (s) 89.32 Current children cumulated vsize (Kb) 71404 [startup+100.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 15983 0 0 0 9864 67 0 0 25 0 1 0 1797702595 71122944 15270 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17364 15270 145 145 0 17219 0 [pid=22517] vsize: 69456 Current children cumulated CPU time (s) 99.31 Current children cumulated vsize (Kb) 71580 [startup+110.01 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16013 0 0 0 10864 67 0 0 25 0 1 0 1797702595 71241728 15300 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17393 15300 145 145 0 17248 0 [pid=22517] vsize: 69572 Current children cumulated CPU time (s) 109.31 Current children cumulated vsize (Kb) 71696 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16106 0 0 0 11863 68 0 0 25 0 1 0 1797702595 71680000 15393 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17500 15393 145 145 0 17355 0 [pid=22517] vsize: 70000 Current children cumulated CPU time (s) 119.31 Current children cumulated vsize (Kb) 72124 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16142 0 0 0 12863 68 0 0 25 0 1 0 1797702595 71819264 15429 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17534 15429 145 145 0 17389 0 [pid=22517] vsize: 70136 Current children cumulated CPU time (s) 129.31 Current children cumulated vsize (Kb) 72260 [startup+140.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16190 0 0 0 13861 69 0 0 25 0 1 0 1797702595 72007680 15477 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17580 15477 145 145 0 17435 0 [pid=22517] vsize: 70320 Current children cumulated CPU time (s) 139.3 Current children cumulated vsize (Kb) 72444 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16238 0 0 0 14861 69 0 0 25 0 1 0 1797702595 72200192 15525 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17627 15525 145 145 0 17482 0 [pid=22517] vsize: 70508 Current children cumulated CPU time (s) 149.3 Current children cumulated vsize (Kb) 72632 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16262 0 0 0 15861 69 0 0 25 0 1 0 1797702595 72294400 15549 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17650 15549 145 145 0 17505 0 [pid=22517] vsize: 70600 Current children cumulated CPU time (s) 159.3 Current children cumulated vsize (Kb) 72724 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16290 0 0 0 16860 70 0 0 25 0 1 0 1797702595 72404992 15577 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22517/statm): 17677 15577 145 145 0 17532 0 [pid=22517] vsize: 70708 Current children cumulated CPU time (s) 169.3 Current children cumulated vsize (Kb) 72832 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16325 0 0 0 17858 71 0 0 25 0 1 0 1797702595 72540160 15612 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17710 15612 145 145 0 17565 0 [pid=22517] vsize: 70840 Current children cumulated CPU time (s) 179.29 Current children cumulated vsize (Kb) 72964 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16353 0 0 0 18857 71 0 0 25 0 1 0 1797702595 72650752 15640 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17737 15640 145 145 0 17592 0 [pid=22517] vsize: 70948 Current children cumulated CPU time (s) 189.28 Current children cumulated vsize (Kb) 73072 [startup+200.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16383 0 0 0 19857 71 0 0 25 0 1 0 1797702595 72769536 15670 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17766 15670 145 145 0 17621 0 [pid=22517] vsize: 71064 Current children cumulated CPU time (s) 199.28 Current children cumulated vsize (Kb) 73188 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16414 0 0 0 20857 71 0 0 25 0 1 0 1797702595 72867840 15701 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17790 15701 145 145 0 17645 0 [pid=22517] vsize: 71160 Current children cumulated CPU time (s) 209.28 Current children cumulated vsize (Kb) 73284 [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16456 0 0 0 21856 71 0 0 25 0 1 0 1797702595 73031680 15743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17830 15743 145 145 0 17685 0 [pid=22517] vsize: 71320 Current children cumulated CPU time (s) 219.27 Current children cumulated vsize (Kb) 73444 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16540 0 0 0 22855 72 0 0 25 0 1 0 1797702595 73494528 15827 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17943 15827 145 145 0 17798 0 [pid=22517] vsize: 71772 Current children cumulated CPU time (s) 229.27 Current children cumulated vsize (Kb) 73896 [startup+240.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16572 0 0 0 23855 72 0 0 25 0 1 0 1797702595 73621504 15859 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 17974 15859 145 145 0 17829 0 [pid=22517] vsize: 71896 Current children cumulated CPU time (s) 239.27 Current children cumulated vsize (Kb) 74020 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16612 0 0 0 24855 73 0 0 25 0 1 0 1797702595 73777152 15899 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18012 15899 145 145 0 17867 0 [pid=22517] vsize: 72048 Current children cumulated CPU time (s) 249.28 Current children cumulated vsize (Kb) 74172 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16665 0 0 0 25854 73 0 0 25 0 1 0 1797702595 73986048 15952 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18063 15952 145 145 0 17918 0 [pid=22517] vsize: 72252 Current children cumulated CPU time (s) 259.27 Current children cumulated vsize (Kb) 74376 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16759 0 0 0 26852 74 0 0 25 0 1 0 1797702595 74358784 16046 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18154 16046 145 145 0 18009 0 [pid=22517] vsize: 72616 Current children cumulated CPU time (s) 269.26 Current children cumulated vsize (Kb) 74740 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16816 0 0 0 27851 74 0 0 25 0 1 0 1797702595 74584064 16103 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18209 16103 145 145 0 18064 0 [pid=22517] vsize: 72836 Current children cumulated CPU time (s) 279.25 Current children cumulated vsize (Kb) 74960 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16912 0 0 0 28849 75 0 0 25 0 1 0 1797702595 74960896 16199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18301 16199 145 145 0 18156 0 [pid=22517] vsize: 73204 Current children cumulated CPU time (s) 289.24 Current children cumulated vsize (Kb) 75328 [startup+300.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 16986 0 0 0 29847 76 0 0 25 0 1 0 1797702595 75255808 16273 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18373 16273 145 145 0 18228 0 [pid=22517] vsize: 73492 Current children cumulated CPU time (s) 299.23 Current children cumulated vsize (Kb) 75616 [startup+310.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17077 0 0 0 30846 77 0 0 25 0 1 0 1797702595 75612160 16364 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18460 16364 145 145 0 18315 0 [pid=22517] vsize: 73840 Current children cumulated CPU time (s) 309.23 Current children cumulated vsize (Kb) 75964 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17108 0 0 0 31845 77 0 0 25 0 1 0 1797702595 75735040 16395 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18490 16395 145 145 0 18345 0 [pid=22517] vsize: 73960 Current children cumulated CPU time (s) 319.22 Current children cumulated vsize (Kb) 76084 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17128 0 0 0 32846 77 0 0 25 0 1 0 1797702595 75816960 16415 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18510 16415 145 145 0 18365 0 [pid=22517] vsize: 74040 Current children cumulated CPU time (s) 329.23 Current children cumulated vsize (Kb) 76164 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17206 0 0 0 33845 77 0 0 25 0 1 0 1797702595 76124160 16493 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18585 16493 145 145 0 18440 0 [pid=22517] vsize: 74340 Current children cumulated CPU time (s) 339.22 Current children cumulated vsize (Kb) 76464 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17270 0 0 0 34844 78 0 0 25 0 1 0 1797702595 76369920 16557 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18645 16557 145 145 0 18500 0 [pid=22517] vsize: 74580 Current children cumulated CPU time (s) 349.22 Current children cumulated vsize (Kb) 76704 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17357 0 0 0 35843 78 0 0 21 0 1 0 1797702595 76718080 16644 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18730 16644 145 145 0 18585 0 [pid=22517] vsize: 74920 Current children cumulated CPU time (s) 359.21 Current children cumulated vsize (Kb) 77044 [startup+370.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17417 0 0 0 36841 78 0 0 25 0 1 0 1797702595 77217792 16704 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18852 16704 145 145 0 18707 0 [pid=22517] vsize: 75408 Current children cumulated CPU time (s) 369.19 Current children cumulated vsize (Kb) 77532 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17547 0 0 0 37839 79 0 0 25 0 1 0 1797702595 77737984 16834 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 18979 16834 145 145 0 18834 0 [pid=22517] vsize: 75916 Current children cumulated CPU time (s) 379.18 Current children cumulated vsize (Kb) 78040 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17667 0 0 0 38837 80 0 0 25 0 1 0 1797702595 78217216 16954 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19096 16954 145 145 0 18951 0 [pid=22517] vsize: 76384 Current children cumulated CPU time (s) 389.17 Current children cumulated vsize (Kb) 78508 [startup+400.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17763 0 0 0 39835 80 0 0 25 0 1 0 1797702595 78598144 17050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19189 17050 145 145 0 19044 0 [pid=22517] vsize: 76756 Current children cumulated CPU time (s) 399.15 Current children cumulated vsize (Kb) 78880 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 17950 0 0 0 40832 82 0 0 25 0 1 0 1797702595 79343616 17237 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19371 17237 145 145 0 19226 0 [pid=22517] vsize: 77484 Current children cumulated CPU time (s) 409.14 Current children cumulated vsize (Kb) 79608 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 18019 0 0 0 41831 82 0 0 25 0 1 0 1797702595 79618048 17306 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19438 17306 145 145 0 19293 0 [pid=22517] vsize: 77752 Current children cumulated CPU time (s) 419.13 Current children cumulated vsize (Kb) 79876 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 18074 0 0 0 42831 82 0 0 25 0 1 0 1797702595 79835136 17361 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19491 17361 145 145 0 19346 0 [pid=22517] vsize: 77964 Current children cumulated CPU time (s) 429.13 Current children cumulated vsize (Kb) 80088 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 18277 0 0 0 43828 83 0 0 25 0 1 0 1797702595 80650240 17564 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 19690 17564 145 145 0 19545 0 [pid=22517] vsize: 78760 Current children cumulated CPU time (s) 439.11 Current children cumulated vsize (Kb) 80884 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 18963 0 0 0 44817 87 0 0 25 0 1 0 1797702595 83427328 18250 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 20368 18250 145 145 0 20223 0 [pid=22517] vsize: 81472 Current children cumulated CPU time (s) 449.04 Current children cumulated vsize (Kb) 83596 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) T 22513 22513 1333 0 -1 0 19439 0 0 0 45810 91 0 0 25 0 1 0 1797702595 85356544 18726 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434789 0 0 17 1 0 0 Raw data (/proc/22517/statm): 20839 18726 145 145 0 20694 0 [pid=22517] vsize: 83356 Current children cumulated CPU time (s) 459.01 Current children cumulated vsize (Kb) 85480 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 19541 0 0 0 46808 91 0 0 25 0 1 0 1797702595 85762048 18828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 20938 18828 145 145 0 20793 0 [pid=22517] vsize: 83752 Current children cumulated CPU time (s) 468.99 Current children cumulated vsize (Kb) 85876 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 19634 0 0 0 47807 92 0 0 25 0 1 0 1797702595 86130688 18921 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21028 18921 145 145 0 20883 0 [pid=22517] vsize: 84112 Current children cumulated CPU time (s) 478.99 Current children cumulated vsize (Kb) 86236 [startup+490.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 19738 0 0 0 48806 93 0 0 25 0 1 0 1797702595 86544384 19025 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21129 19025 145 145 0 20984 0 [pid=22517] vsize: 84516 Current children cumulated CPU time (s) 488.99 Current children cumulated vsize (Kb) 86640 [startup+500.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 19948 0 0 0 49803 93 0 0 25 0 1 0 1797702595 87392256 19235 4294967295 134512640 135094434 3221224432 3221223092 134553533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21336 19235 145 145 0 21191 0 [pid=22517] vsize: 85344 Current children cumulated CPU time (s) 498.96 Current children cumulated vsize (Kb) 87468 [startup+510.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20113 0 0 0 50801 95 0 0 25 0 1 0 1797702595 88051712 19400 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21497 19400 145 145 0 21352 0 [pid=22517] vsize: 85988 Current children cumulated CPU time (s) 508.96 Current children cumulated vsize (Kb) 88112 [startup+520.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20155 0 0 0 51800 95 0 0 25 0 1 0 1797702595 88219648 19442 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21538 19442 145 145 0 21393 0 [pid=22517] vsize: 86152 Current children cumulated CPU time (s) 518.95 Current children cumulated vsize (Kb) 88276 [startup+530.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20306 0 0 0 52797 96 0 0 25 0 1 0 1797702595 88821760 19593 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21685 19593 145 145 0 21540 0 [pid=22517] vsize: 86740 Current children cumulated CPU time (s) 528.93 Current children cumulated vsize (Kb) 88864 [startup+540.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20369 0 0 0 53797 97 0 0 25 0 1 0 1797702595 89075712 19656 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21747 19656 145 145 0 21602 0 [pid=22517] vsize: 86988 Current children cumulated CPU time (s) 538.94 Current children cumulated vsize (Kb) 89112 [startup+550.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20611 0 0 0 54791 100 0 0 25 0 1 0 1797702595 90046464 19898 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 21984 19898 145 145 0 21839 0 [pid=22517] vsize: 87936 Current children cumulated CPU time (s) 548.91 Current children cumulated vsize (Kb) 90060 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20693 0 0 0 55790 101 0 0 25 0 1 0 1797702595 90898432 19980 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22192 19980 145 145 0 22047 0 [pid=22517] vsize: 88768 Current children cumulated CPU time (s) 558.91 Current children cumulated vsize (Kb) 90892 [startup+570.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20761 0 0 0 56790 102 0 0 25 0 1 0 1797702595 91172864 20048 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22259 20048 145 145 0 22114 0 [pid=22517] vsize: 89036 Current children cumulated CPU time (s) 568.92 Current children cumulated vsize (Kb) 91160 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20846 0 0 0 57788 102 0 0 25 0 1 0 1797702595 91512832 20133 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22342 20133 145 145 0 22197 0 [pid=22517] vsize: 89368 Current children cumulated CPU time (s) 578.9 Current children cumulated vsize (Kb) 91492 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 20915 0 0 0 58787 103 0 0 25 0 1 0 1797702595 91791360 20202 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22410 20202 145 145 0 22265 0 [pid=22517] vsize: 89640 Current children cumulated CPU time (s) 588.9 Current children cumulated vsize (Kb) 91764 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) T 22513 22513 1333 0 -1 0 21093 0 0 0 59784 105 0 0 25 0 1 0 1797702595 92516352 20380 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22587 20380 145 145 0 22442 0 [pid=22517] vsize: 90348 Current children cumulated CPU time (s) 598.89 Current children cumulated vsize (Kb) 92472 [startup+610.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21207 0 0 0 60783 105 0 0 25 0 1 0 1797702595 92975104 20494 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22699 20494 145 145 0 22554 0 [pid=22517] vsize: 90796 Current children cumulated CPU time (s) 608.88 Current children cumulated vsize (Kb) 92920 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21278 0 0 0 61781 106 0 0 25 0 1 0 1797702595 93261824 20565 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22769 20565 145 145 0 22624 0 [pid=22517] vsize: 91076 Current children cumulated CPU time (s) 618.87 Current children cumulated vsize (Kb) 93200 [startup+630.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21359 0 0 0 62780 107 0 0 25 0 1 0 1797702595 93585408 20646 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22848 20646 145 145 0 22703 0 [pid=22517] vsize: 91392 Current children cumulated CPU time (s) 628.87 Current children cumulated vsize (Kb) 93516 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.91 1/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) T 22513 22513 1333 0 -1 0 21506 0 0 0 63777 108 0 0 25 0 1 0 1797702595 94179328 20793 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22517/statm): 22993 20793 145 145 0 22848 0 [pid=22517] vsize: 91972 Current children cumulated CPU time (s) 638.85 Current children cumulated vsize (Kb) 94096 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21760 0 0 0 64773 110 0 0 25 0 1 0 1797702595 95211520 21047 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23245 21047 145 145 0 23100 0 [pid=22517] vsize: 92980 Current children cumulated CPU time (s) 648.83 Current children cumulated vsize (Kb) 95104 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21856 0 0 0 65772 110 0 0 25 0 1 0 1797702595 95592448 21143 4294967295 134512640 135094434 3221224432 3221223056 134557633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23338 21143 145 145 0 23193 0 [pid=22517] vsize: 93352 Current children cumulated CPU time (s) 658.82 Current children cumulated vsize (Kb) 95476 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 21927 0 0 0 66771 110 0 0 25 0 1 0 1797702595 95875072 21214 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23407 21214 145 145 0 23262 0 [pid=22517] vsize: 93628 Current children cumulated CPU time (s) 668.81 Current children cumulated vsize (Kb) 95752 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22038 0 0 0 67769 111 0 0 25 0 1 0 1797702595 96321536 21325 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23516 21325 145 145 0 23371 0 [pid=22517] vsize: 94064 Current children cumulated CPU time (s) 678.8 Current children cumulated vsize (Kb) 96188 [startup+690.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22071 0 0 0 68769 111 0 0 25 0 1 0 1797702595 96452608 21358 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23548 21358 145 145 0 23403 0 [pid=22517] vsize: 94192 Current children cumulated CPU time (s) 688.8 Current children cumulated vsize (Kb) 96316 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22108 0 0 0 69768 112 0 0 25 0 1 0 1797702595 96600064 21395 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23584 21395 145 145 0 23439 0 [pid=22517] vsize: 94336 Current children cumulated CPU time (s) 698.8 Current children cumulated vsize (Kb) 96460 [startup+710.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22144 0 0 0 70768 112 0 0 25 0 1 0 1797702595 96743424 21431 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23619 21431 145 145 0 23474 0 [pid=22517] vsize: 94476 Current children cumulated CPU time (s) 708.8 Current children cumulated vsize (Kb) 96600 [startup+720.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22192 0 0 0 71767 112 0 0 25 0 1 0 1797702595 96935936 21479 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23666 21479 145 145 0 23521 0 [pid=22517] vsize: 94664 Current children cumulated CPU time (s) 718.79 Current children cumulated vsize (Kb) 96788 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22356 0 0 0 72766 113 0 0 25 0 1 0 1797702595 97599488 21643 4294967295 134512640 135094434 3221224432 3221223104 134555842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23828 21643 145 145 0 23683 0 [pid=22517] vsize: 95312 Current children cumulated CPU time (s) 728.79 Current children cumulated vsize (Kb) 97436 [startup+740.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22477 0 0 0 73764 114 0 0 25 0 1 0 1797702595 98086912 21764 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 23947 21764 145 145 0 23802 0 [pid=22517] vsize: 95788 Current children cumulated CPU time (s) 738.78 Current children cumulated vsize (Kb) 97912 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22568 0 0 0 74763 115 0 0 25 0 1 0 1797702595 98435072 21855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24032 21855 145 145 0 23887 0 [pid=22517] vsize: 96128 Current children cumulated CPU time (s) 748.78 Current children cumulated vsize (Kb) 98252 [startup+760.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22630 0 0 0 75762 115 0 0 25 0 1 0 1797702595 98684928 21917 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24093 21917 145 145 0 23948 0 [pid=22517] vsize: 96372 Current children cumulated CPU time (s) 758.77 Current children cumulated vsize (Kb) 98496 [startup+770.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22723 0 0 0 76760 115 0 0 25 0 1 0 1797702595 99057664 22010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24184 22010 145 145 0 24039 0 [pid=22517] vsize: 96736 Current children cumulated CPU time (s) 768.75 Current children cumulated vsize (Kb) 98860 [startup+780.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22920 0 0 0 77756 118 0 0 25 0 1 0 1797702595 99848192 22207 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24377 22207 145 145 0 24232 0 [pid=22517] vsize: 97508 Current children cumulated CPU time (s) 778.74 Current children cumulated vsize (Kb) 99632 [startup+790.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 22963 0 0 0 78755 118 0 0 25 0 1 0 1797702595 100020224 22250 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24419 22250 145 145 0 24274 0 [pid=22517] vsize: 97676 Current children cumulated CPU time (s) 788.73 Current children cumulated vsize (Kb) 99800 [startup+800.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23002 0 0 0 79755 118 0 0 25 0 1 0 1797702595 100175872 22289 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24457 22289 145 145 0 24312 0 [pid=22517] vsize: 97828 Current children cumulated CPU time (s) 798.73 Current children cumulated vsize (Kb) 99952 [startup+810.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23067 0 0 0 80754 119 0 0 25 0 1 0 1797702595 100433920 22354 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24520 22354 145 145 0 24375 0 [pid=22517] vsize: 98080 Current children cumulated CPU time (s) 808.73 Current children cumulated vsize (Kb) 100204 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23113 0 0 0 81753 119 0 0 25 0 1 0 1797702595 100614144 22400 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24564 22400 145 145 0 24419 0 [pid=22517] vsize: 98256 Current children cumulated CPU time (s) 818.72 Current children cumulated vsize (Kb) 100380 [startup+830.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23206 0 0 0 82751 120 0 0 25 0 1 0 1797702595 100986880 22493 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24655 22493 145 145 0 24510 0 [pid=22517] vsize: 98620 Current children cumulated CPU time (s) 828.71 Current children cumulated vsize (Kb) 100744 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23251 0 0 0 83751 120 0 0 25 0 1 0 1797702595 101175296 22538 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24701 22538 145 145 0 24556 0 [pid=22517] vsize: 98804 Current children cumulated CPU time (s) 838.71 Current children cumulated vsize (Kb) 100928 [startup+850.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23280 0 0 0 84751 120 0 0 25 0 1 0 1797702595 101289984 22567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24729 22567 145 145 0 24584 0 [pid=22517] vsize: 98916 Current children cumulated CPU time (s) 848.71 Current children cumulated vsize (Kb) 101040 [startup+860.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23347 0 0 0 85750 121 0 0 25 0 1 0 1797702595 101560320 22634 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24795 22634 145 145 0 24650 0 [pid=22517] vsize: 99180 Current children cumulated CPU time (s) 858.71 Current children cumulated vsize (Kb) 101304 [startup+870.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23399 0 0 0 86749 121 0 0 25 0 1 0 1797702595 101769216 22686 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 24846 22686 145 145 0 24701 0 [pid=22517] vsize: 99384 Current children cumulated CPU time (s) 868.7 Current children cumulated vsize (Kb) 101508 [startup+880.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23679 0 0 0 87744 124 0 0 25 0 1 0 1797702595 102899712 22966 4294967295 134512640 135094434 3221224432 3221223184 134559282 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25122 22966 145 145 0 24977 0 [pid=22517] vsize: 100488 Current children cumulated CPU time (s) 878.68 Current children cumulated vsize (Kb) 102612 [startup+890.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23753 0 0 0 88743 124 0 0 25 0 1 0 1797702595 103194624 23040 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25194 23040 145 145 0 25049 0 [pid=22517] vsize: 100776 Current children cumulated CPU time (s) 888.67 Current children cumulated vsize (Kb) 102900 [startup+900.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23821 0 0 0 89742 125 0 0 25 0 1 0 1797702595 103477248 23108 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25263 23108 145 145 0 25118 0 [pid=22517] vsize: 101052 Current children cumulated CPU time (s) 898.67 Current children cumulated vsize (Kb) 103176 [startup+910.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23911 0 0 0 90740 126 0 0 25 0 1 0 1797702595 103837696 23198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25351 23198 145 145 0 25206 0 [pid=22517] vsize: 101404 Current children cumulated CPU time (s) 908.66 Current children cumulated vsize (Kb) 103528 [startup+920.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23957 0 0 0 91740 126 0 0 25 0 1 0 1797702595 104026112 23244 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25397 23244 145 145 0 25252 0 [pid=22517] vsize: 101588 Current children cumulated CPU time (s) 918.66 Current children cumulated vsize (Kb) 103712 [startup+930.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 23991 0 0 0 92740 127 0 0 25 0 1 0 1797702595 104153088 23278 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25428 23278 145 145 0 25283 0 [pid=22517] vsize: 101712 Current children cumulated CPU time (s) 928.67 Current children cumulated vsize (Kb) 103836 [startup+940.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24062 0 0 0 93738 127 0 0 25 0 1 0 1797702595 104435712 23349 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25497 23349 145 145 0 25352 0 [pid=22517] vsize: 101988 Current children cumulated CPU time (s) 938.65 Current children cumulated vsize (Kb) 104112 [startup+950.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24418 0 0 0 94733 129 0 0 25 0 1 0 1797702595 105877504 23705 4294967295 134512640 135094434 3221224432 3221223072 134556681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 25849 23705 145 145 0 25704 0 [pid=22517] vsize: 103396 Current children cumulated CPU time (s) 948.62 Current children cumulated vsize (Kb) 105520 [startup+960.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24762 0 0 0 95727 132 0 0 25 0 1 0 1797702595 107274240 24049 4294967295 134512640 135094434 3221224432 3221223104 134553523 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 26190 24049 145 145 0 26045 0 [pid=22517] vsize: 104760 Current children cumulated CPU time (s) 958.59 Current children cumulated vsize (Kb) 106884 [startup+970.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24788 0 0 0 96727 132 0 0 25 0 1 0 1797702595 107376640 24075 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 26215 24075 145 145 0 26070 0 [pid=22517] vsize: 104860 Current children cumulated CPU time (s) 968.59 Current children cumulated vsize (Kb) 106984 [startup+980.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24834 0 0 0 97727 132 0 0 25 0 1 0 1797702595 107560960 24121 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 26260 24121 145 145 0 26115 0 [pid=22517] vsize: 105040 Current children cumulated CPU time (s) 978.59 Current children cumulated vsize (Kb) 107164 [startup+990.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 24923 0 0 0 98725 132 0 0 25 0 1 0 1797702595 107917312 24210 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 26347 24210 145 145 0 26202 0 [pid=22517] vsize: 105388 Current children cumulated CPU time (s) 988.57 Current children cumulated vsize (Kb) 107512 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 25538 0 0 0 99713 137 0 0 25 0 1 0 1797702595 110411776 24825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 26956 24825 145 145 0 26811 0 [pid=22517] vsize: 107824 Current children cumulated CPU time (s) 998.5 Current children cumulated vsize (Kb) 109948 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 26049 0 0 0 100704 141 0 0 25 0 1 0 1797702595 112488448 25336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 27463 25336 145 145 0 27318 0 [pid=22517] vsize: 109852 Current children cumulated CPU time (s) 1008.45 Current children cumulated vsize (Kb) 111976 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 26591 0 0 0 101694 145 0 0 23 0 1 0 1797702595 114696192 25878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 28002 25878 145 145 0 27857 0 [pid=22517] vsize: 112008 Current children cumulated CPU time (s) 1018.39 Current children cumulated vsize (Kb) 114132 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27098 0 0 0 102686 149 0 0 25 0 1 0 1797702595 116760576 26385 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 28506 26385 145 145 0 28361 0 [pid=22517] vsize: 114024 Current children cumulated CPU time (s) 1028.35 Current children cumulated vsize (Kb) 116148 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27284 0 0 0 103683 150 0 0 25 0 1 0 1797702595 117510144 26571 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 28689 26571 145 145 0 28544 0 [pid=22517] vsize: 114756 Current children cumulated CPU time (s) 1038.33 Current children cumulated vsize (Kb) 116880 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27374 0 0 0 104681 151 0 0 25 0 1 0 1797702595 117870592 26661 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 28777 26661 145 145 0 28632 0 [pid=22517] vsize: 115108 Current children cumulated CPU time (s) 1048.32 Current children cumulated vsize (Kb) 117232 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27522 0 0 0 105679 152 0 0 25 0 1 0 1797702595 118464512 26809 4294967295 134512640 135094434 3221224432 3221223056 134557653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 28922 26809 145 145 0 28777 0 [pid=22517] vsize: 115688 Current children cumulated CPU time (s) 1058.31 Current children cumulated vsize (Kb) 117812 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27736 0 0 0 106676 153 0 0 25 0 1 0 1797702595 119328768 27023 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29133 27023 145 145 0 28988 0 [pid=22517] vsize: 116532 Current children cumulated CPU time (s) 1068.29 Current children cumulated vsize (Kb) 118656 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 27837 0 0 0 107674 154 0 0 25 0 1 0 1797702595 119734272 27124 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29232 27124 145 145 0 29087 0 [pid=22517] vsize: 116928 Current children cumulated CPU time (s) 1078.28 Current children cumulated vsize (Kb) 119052 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28246 0 0 0 108667 157 0 0 25 0 1 0 1797702595 121393152 27533 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29637 27533 145 145 0 29492 0 [pid=22517] vsize: 118548 Current children cumulated CPU time (s) 1088.24 Current children cumulated vsize (Kb) 120672 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28348 0 0 0 109666 158 0 0 25 0 1 0 1797702595 121802752 27635 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29737 27635 145 145 0 29592 0 [pid=22517] vsize: 118948 Current children cumulated CPU time (s) 1098.24 Current children cumulated vsize (Kb) 121072 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28551 0 0 0 110662 159 0 0 25 0 1 0 1797702595 122621952 27838 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29937 27838 145 145 0 29792 0 [pid=22517] vsize: 119748 Current children cumulated CPU time (s) 1108.21 Current children cumulated vsize (Kb) 121872 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28593 0 0 0 111662 160 0 0 25 0 1 0 1797702595 122789888 27880 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 29978 27880 145 145 0 29833 0 [pid=22517] vsize: 119912 Current children cumulated CPU time (s) 1118.22 Current children cumulated vsize (Kb) 122036 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28790 0 0 0 112658 161 0 0 25 0 1 0 1797702595 123584512 28077 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 30172 28077 145 145 0 30027 0 [pid=22517] vsize: 120688 Current children cumulated CPU time (s) 1128.19 Current children cumulated vsize (Kb) 122812 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 28863 0 0 0 113657 161 0 0 25 0 1 0 1797702595 123875328 28150 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 30243 28150 145 145 0 30098 0 [pid=22517] vsize: 120972 Current children cumulated CPU time (s) 1138.18 Current children cumulated vsize (Kb) 123096 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 29379 0 0 0 114649 164 0 0 25 0 1 0 1797702595 127016960 28666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31010 28666 145 145 0 30865 0 [pid=22517] vsize: 124040 Current children cumulated CPU time (s) 1148.13 Current children cumulated vsize (Kb) 126164 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 29960 0 0 0 115640 168 0 0 25 0 1 0 1797702595 129384448 29247 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31588 29247 145 145 0 31443 0 [pid=22517] vsize: 126352 Current children cumulated CPU time (s) 1158.08 Current children cumulated vsize (Kb) 128476 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30089 0 0 0 116638 168 0 0 25 0 1 0 1797702595 129904640 29376 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31715 29376 145 145 0 31570 0 [pid=22517] vsize: 126860 Current children cumulated CPU time (s) 1168.06 Current children cumulated vsize (Kb) 128984 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30146 0 0 0 117637 169 0 0 25 0 1 0 1797702595 130134016 29433 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31771 29433 145 145 0 31626 0 [pid=22517] vsize: 127084 Current children cumulated CPU time (s) 1178.06 Current children cumulated vsize (Kb) 129208 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30251 0 0 0 118635 170 0 0 25 0 1 0 1797702595 130551808 29538 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31873 29538 145 145 0 31728 0 [pid=22517] vsize: 127492 Current children cumulated CPU time (s) 1188.05 Current children cumulated vsize (Kb) 129616 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30307 0 0 0 119635 170 0 0 25 0 1 0 1797702595 130772992 29594 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 31927 29594 145 145 0 31782 0 [pid=22517] vsize: 127708 Current children cumulated CPU time (s) 1198.05 Current children cumulated vsize (Kb) 129832 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30542 0 0 0 120630 172 0 0 25 0 1 0 1797702595 131719168 29829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 32158 29829 145 145 0 32013 0 [pid=22517] vsize: 128632 Current children cumulated CPU time (s) 1208.02 Current children cumulated vsize (Kb) 130756 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22517 Raw data (/proc/22513/stat): 22513 (minisat+_script) S 22512 22513 1333 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797702590 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22513/statm): 531 226 485 147 0 384 0 [pid=22513] vsize: 2124 Raw data (/proc/22517/stat): 22517 (minisat+_64-bit) R 22513 22513 1333 0 -1 0 30542 0 0 0 120630 172 0 0 25 0 1 0 1797702595 131719168 29829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22517/statm): 32158 29829 145 145 0 32013 0 [pid=22517] vsize: 128632 Current children cumulated CPU time (s) 1208.02 Current children cumulated vsize (Kb) 130756 Sending SIGTERM to -22513 Sleeping 2 seconds One traced child (pid=22513) ended because it received signal 15 (SIGTERM) One traced child (pid=22517) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.15 CPU time (s): 1208.08 CPU user time (s): 1206.31 CPU system time (s): 1.77873 CPU usage (%): 99.8292 Max. virtual memory (cumulated for all children) (Kb): 130756
ERROR: no interpretation found !