Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst2.opb
MD5SUM3c3e6264ad2029dcb2dc81be78ef5988
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
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 numbers24
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9183
Total number of constraints632
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints592
Minimum length of a constraint1
Maximum length of a constraint260

Trace number 6286

Launcher Data

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

Solver Data

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 % |

Watcher Data

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

Verifier Data

ERROR: no interpretation found !