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/MIPLIB/miplib3/normalized-mps-v2-13-7-danoint.opb
MD5SUMbf9bbda6f586f0b888182a433f63f010
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 13107200
Number of bits of the biggest number in a constraint 24
Biggest sum of numbers in a constraint 52829966
Number of bits of the biggest sum of numbers26
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables9304
Total number of constraints728
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)72
Number of constraints which are nor clauses,nor cardinality constraints656
Minimum length of a constraint1
Maximum length of a constraint1000

Trace number 6186

Launcher Data

LAUNCH ON wulflinc23 THE 2005-09-20 04:12:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3350 boxname=wulflinc23 idbench=1006 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf9bbda6f586f0b888182a433f63f010  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-danoint.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-danoint.opb
IDLAUNCH: 3350
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        908160 kB
Buffers:         17308 kB
Cached:          81676 kB
SwapCached:        840 kB
Active:          28732 kB
Inactive:        72940 kB
HighTotal:      131008 kB
HighFree:        48188 kB
LowTotal:       903652 kB
LowFree:        859972 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            19320 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:32:31 (client local time) WITH STATUS 0 IN 1208.31 SECONDS
stats: 3350 7 1208.31 0

Solver Data

c Parsing PB file...
c Converting 816 PB-constraints to clauses...
c   -- Unit propagations: ppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssss
c ---[ 833]---> BDD-cost:   12
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:   13
c ---[ 825]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 823]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 821]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 819]---> Adder-cost: 322   maxlim: 88569   bits: 18/17
c ---[ 817]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 815]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 813]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 811]---> Adder-cost: 336   maxlim: 112889   bits: 18/17
c ---[ 809]---> Adder-cost: 336   maxlim: 112761   bits: 18/17
c ---[ 807]---> Adder-cost: 336   maxlim: 113017   bits: 18/17
c ---[ 805]---> Adder-cost: 336   maxlim: 113145   bits: 18/17
c ---[ 803]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 801]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 799]---> Adder-cost: 336   maxlim: 113529   bits: 18/17
c ---[ 797]---> Adder-cost: 312   maxlim: 55673   bits: 17/16
c ---[ 795]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 793]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 791]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 789]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 787]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 785]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 783]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 781]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 779]---> Adder-cost: 312   maxlim: 55417   bits: 17/16
c ---[ 777]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 775]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 773]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 771]---> Adder-cost: 312   maxlim: 56185   bits: 17/16
c ---[ 769]---> Adder-cost: 330   maxlim: 89081   bits: 18/17
c ---[ 767]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 765]---> Adder-cost: 322   maxlim: 96761   bits: 18/17
c ---[ 763]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 761]---> Adder-cost: 330   maxlim: 88953   bits: 18/17
c ---[ 759]---> Adder-cost: 322   maxlim: 96505   bits: 18/17
c ---[ 757]---> Adder-cost: 330   maxlim: 88697   bits: 18/17
c ---[ 755]---> Adder-cost: 323   maxlim: 64889   bits: 17/16
c ---[ 753]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 751]---> Adder-cost: 314   maxlim: 72313   bits: 17/17
c ---[ 749]---> Adder-cost: 314   maxlim: 72825   bits: 17/17
c ---[ 747]---> Adder-cost: 314   maxlim: 72569   bits: 17/17
c ---[ 745]---> Adder-cost: 314   maxlim: 71801   bits: 17/17
c ---[ 743]---> Adder-cost: 314   maxlim: 72185   bits: 17/17
c ---[ 741]---> Adder-cost: 312   maxlim: 64761   bits: 17/16
c ---[ 739]---> Adder-cost: 312   maxlim: 64377   bits: 17/16
c ---[ 737]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 735]---> Adder-cost: 312   maxlim: 63737   bits: 17/16
c ---[ 733]---> Adder-cost: 312   maxlim: 64249   bits: 17/16
c ---[ 731]---> Adder-cost: 312   maxlim: 63993   bits: 17/16
c ---[ 729]---> Adder-cost: 312   maxlim: 64633   bits: 17/16
c ---[ 727]---> Adder-cost: 312   maxlim: 55929   bits: 17/16
c ---[ 725]---> Adder-cost: 312   maxlim: 56441   bits: 17/16
c ---[ 723]---> Adder-cost: 312   maxlim: 56313   bits: 17/16
c ---[ 721]---> Adder-cost: 312   maxlim: 56569   bits: 17/16
c ---[ 719]---> Adder-cost: 312   maxlim: 56057   bits: 17/16
c ---[ 717]---> Adder-cost: 312   maxlim: 56697   bits: 17/16
c ---[ 715]---> Adder-cost: 312   maxlim: 55545   bits: 17/16
c ---[ 714]---> BDD-cost:  110
c ---[ 713]---> BDD-cost:  110
c ---[ 712]---> BDD-cost:  110
c ---[ 711]---> BDD-cost:  110
c ---[ 710]---> BDD-cost:  110
c ---[ 709]---> BDD-cost:  110
c ---[ 708]---> BDD-cost:  110
c ---[ 707]---> BDD-cost:  110
c ---[ 706]---> BDD-cost:  110
c ---[ 705]---> BDD-cost:  110
c ---[ 704]---> BDD-cost:  110
c ---[ 703]---> BDD-cost:  110
c ---[ 702]---> BDD-cost:  110
c ---[ 701]---> BDD-cost:  110
c ---[ 700]---> BDD-cost:  110
c ---[ 699]---> BDD-cost:  110
c ---[ 698]---> BDD-cost:  110
c ---[ 697]---> BDD-cost:  110
c ---[ 696]---> BDD-cost:  110
c ---[ 695]---> BDD-cost:  110
c ---[ 694]---> BDD-cost:  110
c ---[ 693]---> BDD-cost:  110
c ---[ 692]---> BDD-cost:  110
c ---[ 691]---> BDD-cost:  110
c ---[ 690]---> BDD-cost:  110
c ---[ 689]---> BDD-cost:  110
c ---[ 688]---> BDD-cost:  110
c ---[ 687]---> BDD-cost:  110
c ---[ 686]---> BDD-cost:  110
c ---[ 685]---> BDD-cost:  110
c ---[ 684]---> BDD-cost:  110
c ---[ 683]---> BDD-cost:  110
c ---[ 682]---> BDD-cost:  110
c ---[ 681]---> BDD-cost:  110
c ---[ 680]---> BDD-cost:  110
c ---[ 679]---> BDD-cost:  110
c ---[ 678]---> BDD-cost:  110
c ---[ 677]---> BDD-cost:  110
c ---[ 676]---> BDD-cost:  110
c ---[ 675]---> BDD-cost:  110
c ---[ 674]---> BDD-cost:  110
c ---[ 673]---> BDD-cost:  110
c ---[ 672]---> BDD-cost:  110
c ---[ 671]---> BDD-cost:  110
c ---[ 670]---> BDD-cost:  110
c ---[ 669]---> BDD-cost:  110
c ---[ 668]---> BDD-cost:  110
c ---[ 667]---> BDD-cost:  110
c ---[ 666]---> BDD-cost:  110
c ---[ 665]---> BDD-cost:  110
c ---[ 664]---> BDD-cost:  110
c ---[ 663]---> BDD-cost:  110
c ---[ 662]---> BDD-cost:  110
c ---[ 661]---> BDD-cost:  110
c ---[ 660]---> BDD-cost:  110
c ---[ 659]---> BDD-cost:  110
c ---[ 657]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost: 1784     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 631]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 629]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 625]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 617]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 603]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 601]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 585]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 583]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 581]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 579]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 577]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 569]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 567]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 563]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost: 1752     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 557]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 555]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 553]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 551]---> Sorter-cost: 1700     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost: 1728     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Adder-cost: 1225   maxlim: 1048575   bits: 21/20
c ---[ 543]---> Adder-cost: 1243   maxlim: 1048575   bits: 21/20
c ---[ 541]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 539]---> Adder-cost: 1155   maxlim: 524287   bits: 20/19
c ---[ 537]---> Adder-cost: 1180   maxlim: 1048575   bits: 21/20
c ---[ 535]---> Adder-cost: 1145   maxlim: 524287   bits: 20/19
c ---[ 533]---> Adder-cost: 1137   maxlim: 524287   bits: 20/19
c ---[ 531]---> Adder-cost: 1129   maxlim: 524287   bits: 20/19
c ---[ 529]---> BDD-cost:   15
c ---[ 527]---> BDD-cost:   15
c ---[ 525]---> BDD-cost:   15
c ---[ 523]---> BDD-cost:   15
c ---[ 521]---> BDD-cost:   15
c ---[ 519]---> BDD-cost:   15
c ---[ 517]---> BDD-cost:   15
c ---[ 515]---> BDD-cost:   15
c ---[ 513]---> BDD-cost:   15
c ---[ 511]---> BDD-cost:   15
c ---[ 509]---> BDD-cost:   15
c ---[ 507]---> BDD-cost:   15
c ---[ 505]---> BDD-cost:   15
c ---[ 503]---> BDD-cost:   15
c ---[ 501]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost: 1572     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 491]---> Sorter-cost: 1585     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1609     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 489]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost: 1489     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 474]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 472]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 470]---> Sorter-cost: 1537     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 469]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 468]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 466]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 465]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 464]---> Sorter-cost: 1596     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 463]---> Sorter-cost: 1583     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 462]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 460]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost: 1411     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 456]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 454]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 453]---> Sorter-cost: 1387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 452]---> Sorter-cost: 1374     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost: 1363     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost: 1398     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost: 1476     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 447]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost: 1463     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost: 1465     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 437]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 1925     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost: 1924     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost: 1923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 410]---> BDD-cost:   22
c ---[ 409]---> BDD-cost:   22
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   22
c ---[ 406]---> BDD-cost:   22
c ---[ 405]---> BDD-cost:   22
c ---[ 404]---> BDD-cost:   22
c ---[ 403]---> BDD-cost:   15
c ---[ 402]---> BDD-cost:   15
c ---[ 401]---> BDD-cost:   15
c ---[ 400]---> BDD-cost:   15
c ---[ 399]---> BDD-cost:   15
c ---[ 398]---> BDD-cost:   15
c ---[ 397]---> BDD-cost:   22
c ---[ 396]---> BDD-cost:   22
c ---[ 395]---> BDD-cost:   22
c ---[ 394]---> BDD-cost:   22
c ---[ 393]---> BDD-cost:   22
c ---[ 392]---> BDD-cost:   22
c ---[ 391]---> BDD-cost:   19
c ---[ 390]---> BDD-cost:   19
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   19
c ---[ 387]---> BDD-cost:   19
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   18
c ---[ 384]---> BDD-cost:   18
c ---[ 383]---> BDD-cost:   18
c ---[ 382]---> BDD-cost:   18
c ---[ 381]---> BDD-cost:   18
c ---[ 380]---> BDD-cost:   18
c ---[ 379]---> BDD-cost:   19
c ---[ 378]---> BDD-cost:   19
c ---[ 377]---> BDD-cost:   19
c ---[ 376]---> BDD-cost:   19
c ---[ 375]---> BDD-cost:   19
c ---[ 374]---> BDD-cost:   19
c ---[ 373]---> BDD-cost:   22
c ---[ 372]---> BDD-cost:   22
c ---[ 371]---> BDD-cost:   22
c ---[ 370]---> BDD-cost:   22
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   22
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:   19
c ---[ 365]---> BDD-cost:   19
c ---[ 364]---> BDD-cost:   19
c ---[ 363]---> BDD-cost:   19
c ---[ 362]---> BDD-cost:   19
c ---[ 361]---> BDD-cost:   22
c ---[ 360]---> BDD-cost:   22
c ---[ 359]---> BDD-cost:   22
c ---[ 358]---> BDD-cost:   22
c ---[ 357]---> BDD-cost:   22
c ---[ 356]---> BDD-cost:   22
c ---[ 355]---> BDD-cost:   22
c ---[ 354]---> BDD-cost:   22
c ---[ 353]---> BDD-cost:   22
c ---[ 352]---> BDD-cost:   22
c ---[ 351]---> BDD-cost:   22
c ---[ 350]---> BDD-cost:   22
c ---[ 349]---> BDD-cost:   22
c ---[ 348]---> BDD-cost:   20
c ---[ 347]---> BDD-cost:   20
c ---[ 346]---> BDD-cost:   20
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:   20
c ---[ 343]---> BDD-cost:   20
c ---[ 342]---> BDD-cost:   22
c ---[ 341]---> BDD-cost:   22
c ---[ 340]---> BDD-cost:   22
c ---[ 339]---> BDD-cost:   22
c ---[ 338]---> BDD-cost:   22
c ---[ 337]---> BDD-cost:   22
c ---[ 336]---> BDD-cost:   22
c ---[ 335]---> BDD-cost:   22
c ---[ 334]---> BDD-cost:   22
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   22
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:   22
c ---[ 329]---> BDD-cost:   22
c ---[ 328]---> BDD-cost:   22
c ---[ 327]---> BDD-cost:   22
c ---[ 326]---> BDD-cost:   22
c ---[ 325]---> BDD-cost:   22
c ---[ 324]---> BDD-cost:   22
c ---[ 323]---> BDD-cost:   22
c ---[ 322]---> BDD-cost:   22
c ---[ 321]---> BDD-cost:   22
c ---[ 320]---> BDD-cost:   22
c ---[ 319]---> BDD-cost:   22
c ---[ 318]---> BDD-cost:   22
c ---[ 317]---> BDD-cost:   22
c ---[ 316]---> BDD-cost:   22
c ---[ 315]---> BDD-cost:   22
c ---[ 314]---> BDD-cost:   22
c ---[ 313]---> BDD-cost:   22
c ---[ 312]---> BDD-cost:   18
c ---[ 311]---> BDD-cost:   18
c ---[ 310]---> BDD-cost:   18
c ---[ 309]---> BDD-cost:   18
c ---[ 308]---> BDD-cost:   18
c ---[ 307]---> BDD-cost:   18
c ---[ 306]---> BDD-cost:   18
c ---[ 305]---> BDD-cost:   18
c ---[ 304]---> BDD-cost:   18
c ---[ 303]---> BDD-cost:   18
c ---[ 302]---> BDD-cost:   18
c ---[ 301]---> BDD-cost:   18
c ---[ 300]---> BDD-cost:   19
c ---[ 299]---> BDD-cost:   19
c ---[ 298]---> BDD-cost:   19
c ---[ 297]---> BDD-cost:   19
c ---[ 296]---> BDD-cost:   19
c ---[ 295]---> BDD-cost:   19
c ---[ 294]---> BDD-cost:   19
c ---[ 293]---> BDD-cost:   17
c ---[ 292]---> BDD-cost:   17
c ---[ 291]---> BDD-cost:   17
c ---[ 290]---> BDD-cost:   17
c ---[ 289]---> BDD-cost:   17
c ---[ 288]---> BDD-cost:   17
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:   19
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:   19
c ---[ 282]---> BDD-cost:   19
c ---[ 281]---> BDD-cost:   18
c ---[ 280]---> BDD-cost:   18
c ---[ 279]---> BDD-cost:   18
c ---[ 278]---> BDD-cost:   18
c ---[ 277]---> BDD-cost:   18
c ---[ 276]---> BDD-cost:   18
c ---[ 275]---> BDD-cost:   17
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:   19
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:   16
c ---[ 262]---> BDD-cost:   16
c ---[ 261]---> BDD-cost:   16
c ---[ 260]---> BDD-cost:   16
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:   16
c ---[ 257]---> BDD-cost:   19
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:   19
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   15
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   15
c ---[ 245]---> BDD-cost:   19
c ---[ 244]---> BDD-cost:   19
c ---[ 243]---> BDD-cost:   19
c ---[ 242]---> BDD-cost:   19
c ---[ 241]---> BDD-cost:   19
c ---[ 240]---> BDD-cost:   19
c ---[ 239]---> BDD-cost:   19
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   16
c ---[ 235]---> BDD-cost:   16
c ---[ 234]---> BDD-cost:   16
c ---[ 233]---> BDD-cost:   16
c ---[ 232]---> BDD-cost:   19
c ---[ 231]---> BDD-cost:   19
c ---[ 230]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   19
c ---[ 228]---> BDD-cost:   19
c ---[ 227]---> BDD-cost:   19
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   17
c ---[ 221]---> BDD-cost:   17
c ---[ 220]---> BDD-cost:   18
c ---[ 219]---> BDD-cost:   18
c ---[ 218]---> BDD-cost:   18
c ---[ 217]---> BDD-cost:   18
c ---[ 216]---> BDD-cost:   18
c ---[ 215]---> BDD-cost:   18
c ---[ 214]---> BDD-cost:   22
c ---[ 213]---> BDD-cost:   22
c ---[ 212]---> BDD-cost:   22
c ---[ 211]---> BDD-cost:   22
c ---[ 210]---> BDD-cost:   22
c ---[ 209]---> BDD-cost:   22
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   19
c ---[ 203]---> BDD-cost:   19
c ---[ 202]---> BDD-cost:   19
c ---[ 201]---> BDD-cost:   19
c ---[ 200]---> BDD-cost:   19
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   19
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:   20
c ---[ 195]---> BDD-cost:   20
c ---[ 194]---> BDD-cost:   20
c ---[ 193]---> BDD-cost:   20
c ---[ 192]---> BDD-cost:   20
c ---[ 191]---> BDD-cost:   20
c ---[ 190]---> BDD-cost:   22
c ---[ 189]---> BDD-cost:   22
c ---[ 188]---> BDD-cost:   22
c ---[ 187]---> BDD-cost:   22
c ---[ 186]---> BDD-cost:   22
c ---[ 185]---> BDD-cost:   22
c ---[ 184]---> BDD-cost:   22
c ---[ 183]---> BDD-cost:   20
c ---[ 182]---> BDD-cost:   20
c ---[ 181]---> BDD-cost:   20
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   20
c ---[ 178]---> BDD-cost:   20
c ---[ 177]---> BDD-cost:   19
c ---[ 176]---> BDD-cost:   19
c ---[ 175]---> BDD-cost:   19
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> BDD-cost:   19
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   15
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   15
c ---[ 165]---> BDD-cost:   21
c ---[ 164]---> BDD-cost:   21
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   21
c ---[ 161]---> BDD-cost:   21
c ---[ 160]---> BDD-cost:   21
c ---[ 159]---> BDD-cost:   19
c ---[ 158]---> BDD-cost:   19
c ---[ 157]---> BDD-cost:   19
c ---[ 156]---> BDD-cost:   19
c ---[ 155]---> BDD-cost:   19
c ---[ 154]---> BDD-cost:   19
c ---[ 153]---> BDD-cost:   19
c ---[ 152]---> BDD-cost:   19
c ---[ 151]---> BDD-cost:   19
c ---[ 150]---> BDD-cost:   19
c ---[ 149]---> BDD-cost:   19
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
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:   22
c ---[ 134]---> BDD-cost:   22
c ---[ 133]---> BDD-cost:   22
c ---[ 132]---> BDD-cost:   22
c ---[ 131]---> BDD-cost:   22
c ---[ 130]---> BDD-cost:   22
c ---[ 129]---> BDD-cost:   22
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:   18
c ---[ 121]---> BDD-cost:   18
c ---[ 120]---> BDD-cost:   18
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   18
c ---[ 117]---> BDD-cost:   18
c ---[ 116]---> BDD-cost:   19
c ---[ 115]---> BDD-cost:   19
c ---[ 114]---> BDD-cost:   19
c ---[ 113]---> BDD-cost:   19
c ---[ 112]---> BDD-cost:   19
c ---[ 111]---> BDD-cost:   19
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   16
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   16
c ---[ 104]---> BDD-cost:   18
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   18
c ---[ 101]---> BDD-cost:   18
c ---[ 100]---> BDD-cost:   18
c ---[  99]---> BDD-cost:   18
c ---[  98]---> BDD-cost:   19
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:   19
c ---[  90]---> BDD-cost:   19
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   19
c ---[  86]---> BDD-cost:   19
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   19
c ---[  82]---> BDD-cost:   19
c ---[  81]---> BDD-cost:   19
c ---[  80]---> BDD-cost:   21
c ---[  79]---> BDD-cost:   21
c ---[  78]---> BDD-cost:   21
c ---[  77]---> BDD-cost:   21
c ---[  76]---> BDD-cost:   21
c ---[  75]---> BDD-cost:   21
c ---[  74]---> BDD-cost:   21
c ---[  73]---> BDD-cost:   18
c ---[  72]---> BDD-cost:   18
c ---[  71]---> BDD-cost:   18
c ---[  70]---> BDD-cost:   18
c ---[  69]---> BDD-cost:   18
c ---[  68]---> BDD-cost:   18
c ---[  67]---> BDD-cost:   18
c ---[  66]---> BDD-cost:   18
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   18
c ---[  63]---> BDD-cost:   18
c ---[  62]---> BDD-cost:   18
c ---[  61]---> BDD-cost:   18
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:   18
c ---[  58]---> BDD-cost:   18
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   18
c ---[  55]---> BDD-cost:   19
c ---[  54]---> BDD-cost:   19
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   19
c ---[  50]---> BDD-cost:   19
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   19
c ---[  47]---> BDD-cost:   19
c ---[  46]---> BDD-cost:   19
c ---[  45]---> BDD-cost:   19
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   19
c ---[  42]---> BDD-cost:   19
c ---[  41]---> BDD-cost:   19
c ---[  40]---> BDD-cost:   19
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   19
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   16
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   16
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]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:   49
c ---[  14]---> BDD-cost:   51
c ---[  13]---> BDD-cost:   54
c ---[  12]---> BDD-cost:   54
c ---[  11]---> BDD-cost:   51
c ---[  10]---> BDD-cost:   49
c ---[   9]---> BDD-cost:   54
c ---[   8]---> BDD-cost:   54
c ---[   7]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 2 2 3 5
c ---[   6]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[   5]---> Sorter-cost:  278     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  381     Base: 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  684870  1830796 |  228290       0        0     nan |  0.000 % |
c |       101 |  684759  1830552 |  251119      97      636     6.6 |  3.998 % |
c |       251 |  684510  1830001 |  276230     229     1244     5.4 |  4.033 % |
c |       476 |  684328  1829603 |  303853     438     2056     4.7 |  4.057 % |
c |       814 |  684074  1829046 |  334239     759     4337     5.7 |  4.091 % |
c |      1322 |  683597  1827998 |  367663    1221     6389     5.2 |  4.152 % |
c |      2083 |  683094  1826895 |  404429    1940    10927     5.6 |  4.219 % |
c |      3223 |  682836  1826324 |  444872    3054    31033    10.2 |  4.254 % |
c |      4931 |  682638  1825866 |  489359    4742    48373    10.2 |  4.279 % |
c |      7493 |  682372  1825273 |  538295    7275   102636    14.1 |  4.313 % |
c |     11337 |  681806  1824014 |  592125   11070   207376    18.7 |  4.387 % |
c |     17105 |  681025  1822251 |  651338   16771   295213    17.6 |  4.488 % |
c |     25754 |  680990  1822168 |  716471   25416   929099    36.6 |  4.493 % |
c |     38728 |  680190  1820370 |  788118   38300  1527789    39.9 |  4.597 % |
c |     58191 |  679494  1818789 |  866930   57694  2926039    50.7 |  4.685 % |
c |     87385 |  678608  1816825 |  953623   86797  4387678    50.6 |  4.802 % |
c |    131175 |  677544  1814408 | 1048986  130466  5833928    44.7 |  4.939 % |

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/27360/stat): 27360 (minisat+_script) R 27359 27360 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855572207 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27360/statm): 174 3 169 147 0 27 0
[pid=27360] 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=27361
New process pid=27362
New process pid=27363
execve syscall for /bin/sed executable
One traced child (pid=27362) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=27363) exited with status: 0
One traced child (pid=27361) exited with status: 0
New process pid=27364
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-danoint.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18413 0 0 0 842 74 0 0 25 0 1 0 1855572212 78073856 17699 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19061 17699 145 145 0 18916 0
[pid=27364] vsize: 76244
Current children cumulated CPU time (s) 9.16
Current children cumulated vsize (Kb) 78368

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18788 0 0 0 1838 76 0 0 25 0 1 0 1855572212 79159296 18074 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19326 18074 145 145 0 19181 0
[pid=27364] vsize: 77304
Current children cumulated CPU time (s) 19.14
Current children cumulated vsize (Kb) 79428

[startup+30.006 s]
Raw data (loadavg): 0.95 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18821 0 0 0 2838 76 0 0 25 0 1 0 1855572212 79265792 18107 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19352 18107 145 145 0 19207 0
[pid=27364] vsize: 77408
Current children cumulated CPU time (s) 29.14
Current children cumulated vsize (Kb) 79532

[startup+40.0066 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18841 0 0 0 3836 76 0 0 25 0 1 0 1855572212 79347712 18127 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27364/statm): 19372 18127 145 145 0 19227 0
[pid=27364] vsize: 77488
Current children cumulated CPU time (s) 39.12
Current children cumulated vsize (Kb) 79612

[startup+50.0083 s]
Raw data (loadavg): 0.96 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18877 0 0 0 4834 77 0 0 25 0 1 0 1855572212 79486976 18163 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27364/statm): 19406 18163 145 145 0 19261 0
[pid=27364] vsize: 77624
Current children cumulated CPU time (s) 49.11
Current children cumulated vsize (Kb) 79748

[startup+60.0089 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18933 0 0 0 5833 78 0 0 25 0 1 0 1855572212 79671296 18219 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19451 18219 145 145 0 19306 0
[pid=27364] vsize: 77804
Current children cumulated CPU time (s) 59.11
Current children cumulated vsize (Kb) 79928

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 18960 0 0 0 6832 78 0 0 25 0 1 0 1855572212 79773696 18246 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19476 18246 145 145 0 19331 0
[pid=27364] vsize: 77904
Current children cumulated CPU time (s) 69.1
Current children cumulated vsize (Kb) 80028

[startup+80.0112 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19034 0 0 0 7831 78 0 0 25 0 1 0 1855572212 80072704 18320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19549 18320 145 145 0 19404 0
[pid=27364] vsize: 78196
Current children cumulated CPU time (s) 79.09
Current children cumulated vsize (Kb) 80320

[startup+90.0118 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19074 0 0 0 8831 79 0 0 25 0 1 0 1855572212 80261120 18360 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19595 18360 145 145 0 19450 0
[pid=27364] vsize: 78380
Current children cumulated CPU time (s) 89.1
Current children cumulated vsize (Kb) 80504

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19211 0 0 0 9829 80 0 0 25 0 1 0 1855572212 80809984 18497 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19729 18497 145 145 0 19584 0
[pid=27364] vsize: 78916
Current children cumulated CPU time (s) 99.09
Current children cumulated vsize (Kb) 81040

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19250 0 0 0 10828 81 0 0 25 0 1 0 1855572212 80961536 18536 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19766 18536 145 145 0 19621 0
[pid=27364] vsize: 79064
Current children cumulated CPU time (s) 109.09
Current children cumulated vsize (Kb) 81188

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19271 0 0 0 11828 81 0 0 25 0 1 0 1855572212 81047552 18557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19787 18557 145 145 0 19642 0
[pid=27364] vsize: 79148
Current children cumulated CPU time (s) 119.09
Current children cumulated vsize (Kb) 81272

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19315 0 0 0 12827 81 0 0 25 0 1 0 1855572212 81223680 18601 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19830 18601 145 145 0 19685 0
[pid=27364] vsize: 79320
Current children cumulated CPU time (s) 129.08
Current children cumulated vsize (Kb) 81444

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19354 0 0 0 13826 82 0 0 25 0 1 0 1855572212 81440768 18640 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 19883 18640 145 145 0 19738 0
[pid=27364] vsize: 79532
Current children cumulated CPU time (s) 139.08
Current children cumulated vsize (Kb) 81656

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 19528 0 0 0 14823 84 0 0 25 0 1 0 1855572212 82112512 18814 4294967295 134512640 135094434 3221224432 3221223024 134557328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 20047 18814 145 145 0 19902 0
[pid=27364] vsize: 80188
Current children cumulated CPU time (s) 149.07
Current children cumulated vsize (Kb) 82312

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20086 0 0 0 15814 88 0 0 25 0 1 0 1855572212 84377600 19372 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 20600 19372 145 145 0 20455 0
[pid=27364] vsize: 82400
Current children cumulated CPU time (s) 159.02
Current children cumulated vsize (Kb) 84524

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20140 0 0 0 16813 88 0 0 25 0 1 0 1855572212 84586496 19426 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 20651 19426 145 145 0 20506 0
[pid=27364] vsize: 82604
Current children cumulated CPU time (s) 169.01
Current children cumulated vsize (Kb) 84728

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20199 0 0 0 17812 89 0 0 25 0 1 0 1855572212 84819968 19485 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 20708 19485 145 145 0 20563 0
[pid=27364] vsize: 82832
Current children cumulated CPU time (s) 179.01
Current children cumulated vsize (Kb) 84956

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20266 0 0 0 18811 89 0 0 25 0 1 0 1855572212 85090304 19552 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 20774 19552 145 145 0 20629 0
[pid=27364] vsize: 83096
Current children cumulated CPU time (s) 189
Current children cumulated vsize (Kb) 85220

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20822 0 0 0 19802 93 0 0 25 0 1 0 1855572212 87474176 20108 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21356 20108 145 145 0 21211 0
[pid=27364] vsize: 85424
Current children cumulated CPU time (s) 198.95
Current children cumulated vsize (Kb) 87548

[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) T 27360 27360 5299 0 -1 0 20864 0 0 0 20801 93 0 0 25 0 1 0 1855572212 87638016 20150 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21396 20150 145 145 0 21251 0
[pid=27364] vsize: 85584
Current children cumulated CPU time (s) 208.94
Current children cumulated vsize (Kb) 87708

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 20949 0 0 0 21800 94 0 0 25 0 1 0 1855572212 87973888 20235 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21478 20235 145 145 0 21333 0
[pid=27364] vsize: 85912
Current children cumulated CPU time (s) 218.94
Current children cumulated vsize (Kb) 88036

[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 21012 0 0 0 22799 94 0 0 25 0 1 0 1855572212 88231936 20298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21541 20298 145 145 0 21396 0
[pid=27364] vsize: 86164
Current children cumulated CPU time (s) 228.93
Current children cumulated vsize (Kb) 88288

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 21109 0 0 0 23797 95 0 0 25 0 1 0 1855572212 88621056 20395 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21636 20395 145 145 0 21491 0
[pid=27364] vsize: 86544
Current children cumulated CPU time (s) 238.92
Current children cumulated vsize (Kb) 88668

[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 21216 0 0 0 24795 96 0 0 25 0 1 0 1855572212 89051136 20502 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 21741 20502 145 145 0 21596 0
[pid=27364] vsize: 86964
Current children cumulated CPU time (s) 248.91
Current children cumulated vsize (Kb) 89088

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 22159 0 0 0 25779 102 0 0 25 0 1 0 1855572212 92872704 21445 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 22674 21445 145 145 0 22529 0
[pid=27364] vsize: 90696
Current children cumulated CPU time (s) 258.81
Current children cumulated vsize (Kb) 92820

[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 22544 0 0 0 26772 105 0 0 25 0 1 0 1855572212 94441472 21830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23057 21830 145 145 0 22912 0
[pid=27364] vsize: 92228
Current children cumulated CPU time (s) 268.77
Current children cumulated vsize (Kb) 94352

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 22711 0 0 0 27768 107 0 0 25 0 1 0 1855572212 95117312 21997 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23222 21997 145 145 0 23077 0
[pid=27364] vsize: 92888
Current children cumulated CPU time (s) 278.75
Current children cumulated vsize (Kb) 95012

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 22840 0 0 0 28766 108 0 0 25 0 1 0 1855572212 95641600 22126 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23350 22126 145 145 0 23205 0
[pid=27364] vsize: 93400
Current children cumulated CPU time (s) 288.74
Current children cumulated vsize (Kb) 95524

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 22905 0 0 0 29765 109 0 0 25 0 1 0 1855572212 95899648 22191 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23413 22191 145 145 0 23268 0
[pid=27364] vsize: 93652
Current children cumulated CPU time (s) 298.74
Current children cumulated vsize (Kb) 95776

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23018 0 0 0 30762 110 0 0 25 0 1 0 1855572212 96616448 22304 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23588 22304 145 145 0 23443 0
[pid=27364] vsize: 94352
Current children cumulated CPU time (s) 308.72
Current children cumulated vsize (Kb) 96476

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23066 0 0 0 31762 111 0 0 25 0 1 0 1855572212 96808960 22352 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23635 22352 145 145 0 23490 0
[pid=27364] vsize: 94540
Current children cumulated CPU time (s) 318.73
Current children cumulated vsize (Kb) 96664

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23131 0 0 0 32760 112 0 0 25 0 1 0 1855572212 97067008 22417 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23698 22417 145 145 0 23553 0
[pid=27364] vsize: 94792
Current children cumulated CPU time (s) 328.72
Current children cumulated vsize (Kb) 96916

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23186 0 0 0 33759 112 0 0 25 0 1 0 1855572212 97288192 22472 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23752 22472 145 145 0 23607 0
[pid=27364] vsize: 95008
Current children cumulated CPU time (s) 338.71
Current children cumulated vsize (Kb) 97132

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23279 0 0 0 34758 113 0 0 25 0 1 0 1855572212 97656832 22565 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23842 22565 145 145 0 23697 0
[pid=27364] vsize: 95368
Current children cumulated CPU time (s) 348.71
Current children cumulated vsize (Kb) 97492

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23369 0 0 0 35755 115 0 0 25 0 1 0 1855572212 98017280 22655 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 23930 22655 145 145 0 23785 0
[pid=27364] vsize: 95720
Current children cumulated CPU time (s) 358.7
Current children cumulated vsize (Kb) 97844

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23533 0 0 0 36752 117 0 0 25 0 1 0 1855572212 98648064 22819 4294967295 134512640 135094434 3221224432 3221223056 134557658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24084 22819 145 145 0 23939 0
[pid=27364] vsize: 96336
Current children cumulated CPU time (s) 368.69
Current children cumulated vsize (Kb) 98460

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23655 0 0 0 37749 119 0 0 25 0 1 0 1855572212 99143680 22941 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24205 22941 145 145 0 24060 0
[pid=27364] vsize: 96820
Current children cumulated CPU time (s) 378.68
Current children cumulated vsize (Kb) 98944

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23717 0 0 0 38748 120 0 0 25 0 1 0 1855572212 99393536 23003 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24266 23003 145 145 0 24121 0
[pid=27364] vsize: 97064
Current children cumulated CPU time (s) 388.68
Current children cumulated vsize (Kb) 99188

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23775 0 0 0 39746 121 0 0 25 0 1 0 1855572212 99631104 23061 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24324 23061 145 145 0 24179 0
[pid=27364] vsize: 97296
Current children cumulated CPU time (s) 398.67
Current children cumulated vsize (Kb) 99420

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23837 0 0 0 40745 121 0 0 25 0 1 0 1855572212 99880960 23123 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24385 23123 145 145 0 24240 0
[pid=27364] vsize: 97540
Current children cumulated CPU time (s) 408.66
Current children cumulated vsize (Kb) 99664

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23898 0 0 0 41744 122 0 0 25 0 1 0 1855572212 100126720 23184 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24445 23184 145 145 0 24300 0
[pid=27364] vsize: 97780
Current children cumulated CPU time (s) 418.66
Current children cumulated vsize (Kb) 99904

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 23974 0 0 0 42743 123 0 0 25 0 1 0 1855572212 100433920 23260 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24520 23260 145 145 0 24375 0
[pid=27364] vsize: 98080
Current children cumulated CPU time (s) 428.66
Current children cumulated vsize (Kb) 100204

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24050 0 0 0 43742 123 0 0 25 0 1 0 1855572212 100745216 23336 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24596 23336 145 145 0 24451 0
[pid=27364] vsize: 98384
Current children cumulated CPU time (s) 438.65
Current children cumulated vsize (Kb) 100508

[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24126 0 0 0 44740 124 0 0 25 0 1 0 1855572212 101052416 23412 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24671 23412 145 145 0 24526 0
[pid=27364] vsize: 98684
Current children cumulated CPU time (s) 448.64
Current children cumulated vsize (Kb) 100808

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24182 0 0 0 45739 125 0 0 25 0 1 0 1855572212 101277696 23468 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24726 23468 145 145 0 24581 0
[pid=27364] vsize: 98904
Current children cumulated CPU time (s) 458.64
Current children cumulated vsize (Kb) 101028

[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24236 0 0 0 46737 125 0 0 25 0 1 0 1855572212 101498880 23522 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24780 23522 145 145 0 24635 0
[pid=27364] vsize: 99120
Current children cumulated CPU time (s) 468.62
Current children cumulated vsize (Kb) 101244

[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24275 0 0 0 47736 126 0 0 25 0 1 0 1855572212 101650432 23561 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24817 23561 145 145 0 24672 0
[pid=27364] vsize: 99268
Current children cumulated CPU time (s) 478.62
Current children cumulated vsize (Kb) 101392

[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24349 0 0 0 48735 126 0 0 25 0 1 0 1855572212 101945344 23635 4294967295 134512640 135094434 3221224432 3221223108 134553524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 24889 23635 145 145 0 24744 0
[pid=27364] vsize: 99556
Current children cumulated CPU time (s) 488.61
Current children cumulated vsize (Kb) 101680

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24524 0 0 0 49732 128 0 0 25 0 1 0 1855572212 102645760 23810 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25060 23810 145 145 0 24915 0
[pid=27364] vsize: 100240
Current children cumulated CPU time (s) 498.6
Current children cumulated vsize (Kb) 102364

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24638 0 0 0 50730 129 0 0 25 0 1 0 1855572212 103104512 23924 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25172 23924 145 145 0 25027 0
[pid=27364] vsize: 100688
Current children cumulated CPU time (s) 508.59
Current children cumulated vsize (Kb) 102812

[startup+520.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24714 0 0 0 51728 129 0 0 25 0 1 0 1855572212 103407616 24000 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25246 24000 145 145 0 25101 0
[pid=27364] vsize: 100984
Current children cumulated CPU time (s) 518.57
Current children cumulated vsize (Kb) 103108

[startup+530.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24785 0 0 0 52727 130 0 0 25 0 1 0 1855572212 103690240 24071 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25315 24071 145 145 0 25170 0
[pid=27364] vsize: 101260
Current children cumulated CPU time (s) 528.57
Current children cumulated vsize (Kb) 103384

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24815 0 0 0 53726 130 0 0 25 0 1 0 1855572212 103809024 24101 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25344 24101 145 145 0 25199 0
[pid=27364] vsize: 101376
Current children cumulated CPU time (s) 538.56
Current children cumulated vsize (Kb) 103500

[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24838 0 0 0 54725 131 0 0 25 0 1 0 1855572212 103903232 24124 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25367 24124 145 145 0 25222 0
[pid=27364] vsize: 101468
Current children cumulated CPU time (s) 548.56
Current children cumulated vsize (Kb) 103592

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24858 0 0 0 55725 131 0 0 25 0 1 0 1855572212 103981056 24144 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25386 24144 145 145 0 25241 0
[pid=27364] vsize: 101544
Current children cumulated CPU time (s) 558.56
Current children cumulated vsize (Kb) 103668

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24877 0 0 0 56724 132 0 0 25 0 1 0 1855572212 104058880 24163 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25405 24163 145 145 0 25260 0
[pid=27364] vsize: 101620
Current children cumulated CPU time (s) 568.56
Current children cumulated vsize (Kb) 103744

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24894 0 0 0 57724 132 0 0 25 0 1 0 1855572212 104124416 24180 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25421 24180 145 145 0 25276 0
[pid=27364] vsize: 101684
Current children cumulated CPU time (s) 578.56
Current children cumulated vsize (Kb) 103808

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24907 0 0 0 58724 132 0 0 25 0 1 0 1855572212 104177664 24193 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25434 24193 145 145 0 25289 0
[pid=27364] vsize: 101736
Current children cumulated CPU time (s) 588.56
Current children cumulated vsize (Kb) 103860

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24927 0 0 0 59724 132 0 0 25 0 1 0 1855572212 104259584 24213 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25454 24213 145 145 0 25309 0
[pid=27364] vsize: 101816
Current children cumulated CPU time (s) 598.56
Current children cumulated vsize (Kb) 103940

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 24973 0 0 0 60723 133 0 0 25 0 1 0 1855572212 104439808 24259 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25498 24259 145 145 0 25353 0
[pid=27364] vsize: 101992
Current children cumulated CPU time (s) 608.56
Current children cumulated vsize (Kb) 104116

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25296 0 0 0 61718 135 0 0 25 0 1 0 1855572212 105746432 24582 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25817 24582 145 145 0 25672 0
[pid=27364] vsize: 103268
Current children cumulated CPU time (s) 618.53
Current children cumulated vsize (Kb) 105392

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25399 0 0 0 62716 136 0 0 25 0 1 0 1855572212 106156032 24685 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 25917 24685 145 145 0 25772 0
[pid=27364] vsize: 103668
Current children cumulated CPU time (s) 628.52
Current children cumulated vsize (Kb) 105792

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25538 0 0 0 63713 138 0 0 25 0 1 0 1855572212 106717184 24824 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26054 24824 145 145 0 25909 0
[pid=27364] vsize: 104216
Current children cumulated CPU time (s) 638.51
Current children cumulated vsize (Kb) 106340

[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25633 0 0 0 64710 139 0 0 25 0 1 0 1855572212 107094016 24919 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26146 24919 145 145 0 26001 0
[pid=27364] vsize: 104584
Current children cumulated CPU time (s) 648.49
Current children cumulated vsize (Kb) 106708

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25698 0 0 0 65709 140 0 0 25 0 1 0 1855572212 107352064 24984 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26209 24984 145 145 0 26064 0
[pid=27364] vsize: 104836
Current children cumulated CPU time (s) 658.49
Current children cumulated vsize (Kb) 106960

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25746 0 0 0 66708 141 0 0 25 0 1 0 1855572212 107544576 25032 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26256 25032 145 145 0 26111 0
[pid=27364] vsize: 105024
Current children cumulated CPU time (s) 668.49
Current children cumulated vsize (Kb) 107148

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25821 0 0 0 67707 142 0 0 25 0 1 0 1855572212 107843584 25107 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26329 25107 145 145 0 26184 0
[pid=27364] vsize: 105316
Current children cumulated CPU time (s) 678.49
Current children cumulated vsize (Kb) 107440

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 25965 0 0 0 68704 143 0 0 25 0 1 0 1855572212 108421120 25251 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26470 25251 145 145 0 26325 0
[pid=27364] vsize: 105880
Current children cumulated CPU time (s) 688.47
Current children cumulated vsize (Kb) 108004

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26089 0 0 0 69702 144 0 0 25 0 1 0 1855572212 108916736 25375 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26591 25375 145 145 0 26446 0
[pid=27364] vsize: 106364
Current children cumulated CPU time (s) 698.46
Current children cumulated vsize (Kb) 108488

[startup+710.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26227 0 0 0 70697 146 0 0 25 0 1 0 1855572212 109998080 25513 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26855 25513 145 145 0 26710 0
[pid=27364] vsize: 107420
Current children cumulated CPU time (s) 708.43
Current children cumulated vsize (Kb) 109544

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26300 0 0 0 71697 147 0 0 25 0 1 0 1855572212 110284800 25586 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26925 25586 145 145 0 26780 0
[pid=27364] vsize: 107700
Current children cumulated CPU time (s) 718.44
Current children cumulated vsize (Kb) 109824

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26367 0 0 0 72696 147 0 0 25 0 1 0 1855572212 110551040 25653 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 26990 25653 145 145 0 26845 0
[pid=27364] vsize: 107960
Current children cumulated CPU time (s) 728.43
Current children cumulated vsize (Kb) 110084

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26456 0 0 0 73694 148 0 0 25 0 1 0 1855572212 110911488 25742 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27078 25742 145 145 0 26933 0
[pid=27364] vsize: 108312
Current children cumulated CPU time (s) 738.42
Current children cumulated vsize (Kb) 110436

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26512 0 0 0 74694 148 0 0 25 0 1 0 1855572212 111136768 25798 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27133 25798 145 145 0 26988 0
[pid=27364] vsize: 108532
Current children cumulated CPU time (s) 748.42
Current children cumulated vsize (Kb) 110656

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26573 0 0 0 75693 149 0 0 25 0 1 0 1855572212 111386624 25859 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27194 25859 145 145 0 27049 0
[pid=27364] vsize: 108776
Current children cumulated CPU time (s) 758.42
Current children cumulated vsize (Kb) 110900

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26651 0 0 0 76691 150 0 0 25 0 1 0 1855572212 111702016 25937 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27271 25937 145 145 0 27126 0
[pid=27364] vsize: 109084
Current children cumulated CPU time (s) 768.41
Current children cumulated vsize (Kb) 111208

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26730 0 0 0 77689 151 0 0 25 0 1 0 1855572212 112021504 26016 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27349 26016 145 145 0 27204 0
[pid=27364] vsize: 109396
Current children cumulated CPU time (s) 778.4
Current children cumulated vsize (Kb) 111520

[startup+790.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26795 0 0 0 78688 152 0 0 25 0 1 0 1855572212 112283648 26081 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27413 26081 145 145 0 27268 0
[pid=27364] vsize: 109652
Current children cumulated CPU time (s) 788.4
Current children cumulated vsize (Kb) 111776

[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26850 0 0 0 79687 153 0 0 25 0 1 0 1855572212 112504832 26136 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27467 26136 145 145 0 27322 0
[pid=27364] vsize: 109868
Current children cumulated CPU time (s) 798.4
Current children cumulated vsize (Kb) 111992

[startup+810.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26906 0 0 0 80686 153 0 0 25 0 1 0 1855572212 112734208 26192 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27523 26192 145 145 0 27378 0
[pid=27364] vsize: 110092
Current children cumulated CPU time (s) 808.39
Current children cumulated vsize (Kb) 112216

[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 26962 0 0 0 81685 153 0 0 25 0 1 0 1855572212 112959488 26248 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27578 26248 145 145 0 27433 0
[pid=27364] vsize: 110312
Current children cumulated CPU time (s) 818.38
Current children cumulated vsize (Kb) 112436

[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27019 0 0 0 82684 154 0 0 25 0 1 0 1855572212 113197056 26305 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27636 26305 145 145 0 27491 0
[pid=27364] vsize: 110544
Current children cumulated CPU time (s) 828.38
Current children cumulated vsize (Kb) 112668

[startup+840.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27080 0 0 0 83683 154 0 0 25 0 1 0 1855572212 113442816 26366 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27696 26366 145 145 0 27551 0
[pid=27364] vsize: 110784
Current children cumulated CPU time (s) 838.37
Current children cumulated vsize (Kb) 112908

[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27147 0 0 0 84681 155 0 0 25 0 1 0 1855572212 113709056 26433 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27761 26433 145 145 0 27616 0
[pid=27364] vsize: 111044
Current children cumulated CPU time (s) 848.36
Current children cumulated vsize (Kb) 113168

[startup+860.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27209 0 0 0 85680 155 0 0 25 0 1 0 1855572212 113963008 26495 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27823 26495 145 145 0 27678 0
[pid=27364] vsize: 111292
Current children cumulated CPU time (s) 858.35
Current children cumulated vsize (Kb) 113416

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27277 0 0 0 86679 156 0 0 25 0 1 0 1855572212 114237440 26563 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27890 26563 145 145 0 27745 0
[pid=27364] vsize: 111560
Current children cumulated CPU time (s) 868.35
Current children cumulated vsize (Kb) 113684

[startup+880.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27346 0 0 0 87678 157 0 0 25 0 1 0 1855572212 114515968 26632 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 27958 26632 145 145 0 27813 0
[pid=27364] vsize: 111832
Current children cumulated CPU time (s) 878.35
Current children cumulated vsize (Kb) 113956

[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27415 0 0 0 88677 158 0 0 25 0 1 0 1855572212 114794496 26701 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28026 26701 145 145 0 27881 0
[pid=27364] vsize: 112104
Current children cumulated CPU time (s) 888.35
Current children cumulated vsize (Kb) 114228

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27481 0 0 0 89676 158 0 0 25 0 1 0 1855572212 115064832 26767 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28092 26767 145 145 0 27947 0
[pid=27364] vsize: 112368
Current children cumulated CPU time (s) 898.34
Current children cumulated vsize (Kb) 114492

[startup+910.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27549 0 0 0 90676 159 0 0 25 0 1 0 1855572212 115343360 26835 4294967295 134512640 135094434 3221224432 3221223120 134554750 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28160 26835 145 145 0 28015 0
[pid=27364] vsize: 112640
Current children cumulated CPU time (s) 908.35
Current children cumulated vsize (Kb) 114764

[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27599 0 0 0 91675 159 0 0 25 0 1 0 1855572212 115552256 26885 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28211 26885 145 145 0 28066 0
[pid=27364] vsize: 112844
Current children cumulated CPU time (s) 918.34
Current children cumulated vsize (Kb) 114968

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27663 0 0 0 92674 159 0 0 25 0 1 0 1855572212 115814400 26949 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28275 26949 145 145 0 28130 0
[pid=27364] vsize: 113100
Current children cumulated CPU time (s) 928.33
Current children cumulated vsize (Kb) 115224

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27713 0 0 0 93673 160 0 0 25 0 1 0 1855572212 116019200 26999 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28325 26999 145 145 0 28180 0
[pid=27364] vsize: 113300
Current children cumulated CPU time (s) 938.33
Current children cumulated vsize (Kb) 115424

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27756 0 0 0 94672 161 0 0 25 0 1 0 1855572212 116191232 27042 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28367 27042 145 145 0 28222 0
[pid=27364] vsize: 113468
Current children cumulated CPU time (s) 948.33
Current children cumulated vsize (Kb) 115592

[startup+960.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27811 0 0 0 95671 161 0 0 25 0 1 0 1855572212 116424704 27097 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28424 27097 145 145 0 28279 0
[pid=27364] vsize: 113696
Current children cumulated CPU time (s) 958.32
Current children cumulated vsize (Kb) 115820

[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27868 0 0 0 96669 163 0 0 25 0 1 0 1855572212 116654080 27154 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28480 27154 145 145 0 28335 0
[pid=27364] vsize: 113920
Current children cumulated CPU time (s) 968.32
Current children cumulated vsize (Kb) 116044

[startup+980.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27923 0 0 0 97667 165 0 0 25 0 1 0 1855572212 116883456 27209 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28536 27209 145 145 0 28391 0
[pid=27364] vsize: 114144
Current children cumulated CPU time (s) 978.32
Current children cumulated vsize (Kb) 116268

[startup+990.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 27983 0 0 0 98666 165 0 0 25 0 1 0 1855572212 117125120 27269 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27364/statm): 28595 27269 145 145 0 28450 0
[pid=27364] vsize: 114380
Current children cumulated CPU time (s) 988.31
Current children cumulated vsize (Kb) 116504

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28038 0 0 0 99664 166 0 0 25 0 1 0 1855572212 117342208 27324 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28648 27324 145 145 0 28503 0
[pid=27364] vsize: 114592
Current children cumulated CPU time (s) 998.3
Current children cumulated vsize (Kb) 116716

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28065 0 0 0 100663 166 0 0 25 0 1 0 1855572212 117452800 27351 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28675 27351 145 145 0 28530 0
[pid=27364] vsize: 114700
Current children cumulated CPU time (s) 1008.29
Current children cumulated vsize (Kb) 116824

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28089 0 0 0 101662 166 0 0 25 0 1 0 1855572212 117551104 27375 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28699 27375 145 145 0 28554 0
[pid=27364] vsize: 114796
Current children cumulated CPU time (s) 1018.28
Current children cumulated vsize (Kb) 116920

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28116 0 0 0 102662 167 0 0 25 0 1 0 1855572212 117657600 27402 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28725 27402 145 145 0 28580 0
[pid=27364] vsize: 114900
Current children cumulated CPU time (s) 1028.29
Current children cumulated vsize (Kb) 117024

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28138 0 0 0 103662 167 0 0 25 0 1 0 1855572212 117751808 27424 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28748 27424 145 145 0 28603 0
[pid=27364] vsize: 114992
Current children cumulated CPU time (s) 1038.29
Current children cumulated vsize (Kb) 117116

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28170 0 0 0 104661 168 0 0 25 0 1 0 1855572212 117878784 27456 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28779 27456 145 145 0 28634 0
[pid=27364] vsize: 115116
Current children cumulated CPU time (s) 1048.29
Current children cumulated vsize (Kb) 117240

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28210 0 0 0 105661 168 0 0 25 0 1 0 1855572212 118042624 27496 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28819 27496 145 145 0 28674 0
[pid=27364] vsize: 115276
Current children cumulated CPU time (s) 1058.29
Current children cumulated vsize (Kb) 117400

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28253 0 0 0 106660 168 0 0 25 0 1 0 1855572212 118214656 27539 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28861 27539 145 145 0 28716 0
[pid=27364] vsize: 115444
Current children cumulated CPU time (s) 1068.28
Current children cumulated vsize (Kb) 117568

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28295 0 0 0 107659 169 0 0 25 0 1 0 1855572212 118386688 27581 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28903 27581 145 145 0 28758 0
[pid=27364] vsize: 115612
Current children cumulated CPU time (s) 1078.28
Current children cumulated vsize (Kb) 117736

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28345 0 0 0 108659 169 0 0 25 0 1 0 1855572212 118587392 27631 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28952 27631 145 145 0 28807 0
[pid=27364] vsize: 115808
Current children cumulated CPU time (s) 1088.28
Current children cumulated vsize (Kb) 117932

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28385 0 0 0 109658 169 0 0 25 0 1 0 1855572212 118747136 27671 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 28991 27671 145 145 0 28846 0
[pid=27364] vsize: 115964
Current children cumulated CPU time (s) 1098.27
Current children cumulated vsize (Kb) 118088

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28397 0 0 0 110658 170 0 0 25 0 1 0 1855572212 118792192 27683 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29002 27683 145 145 0 28857 0
[pid=27364] vsize: 116008
Current children cumulated CPU time (s) 1108.28
Current children cumulated vsize (Kb) 118132

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28432 0 0 0 111658 170 0 0 25 0 1 0 1855572212 118935552 27718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29037 27718 145 145 0 28892 0
[pid=27364] vsize: 116148
Current children cumulated CPU time (s) 1118.28
Current children cumulated vsize (Kb) 118272

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28498 0 0 0 112656 171 0 0 25 0 1 0 1855572212 119201792 27784 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29102 27784 145 145 0 28957 0
[pid=27364] vsize: 116408
Current children cumulated CPU time (s) 1128.27
Current children cumulated vsize (Kb) 118532

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28561 0 0 0 113655 171 0 0 25 0 1 0 1855572212 119455744 27847 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29164 27847 145 145 0 29019 0
[pid=27364] vsize: 116656
Current children cumulated CPU time (s) 1138.26
Current children cumulated vsize (Kb) 118780

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28616 0 0 0 114654 172 0 0 25 0 1 0 1855572212 119681024 27902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29219 27902 145 145 0 29074 0
[pid=27364] vsize: 116876
Current children cumulated CPU time (s) 1148.26
Current children cumulated vsize (Kb) 119000

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28677 0 0 0 115653 173 0 0 25 0 1 0 1855572212 119926784 27963 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29279 27963 145 145 0 29134 0
[pid=27364] vsize: 117116
Current children cumulated CPU time (s) 1158.26
Current children cumulated vsize (Kb) 119240

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28734 0 0 0 116652 173 0 0 25 0 1 0 1855572212 120156160 28020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29335 28020 145 145 0 29190 0
[pid=27364] vsize: 117340
Current children cumulated CPU time (s) 1168.25
Current children cumulated vsize (Kb) 119464

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28791 0 0 0 117652 174 0 0 25 0 1 0 1855572212 120389632 28077 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29392 28077 145 145 0 29247 0
[pid=27364] vsize: 117568
Current children cumulated CPU time (s) 1178.26
Current children cumulated vsize (Kb) 119692

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28857 0 0 0 118650 175 0 0 25 0 1 0 1855572212 120655872 28143 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29457 28143 145 145 0 29312 0
[pid=27364] vsize: 117828
Current children cumulated CPU time (s) 1188.25
Current children cumulated vsize (Kb) 119952

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28907 0 0 0 119650 175 0 0 25 0 1 0 1855572212 120860672 28193 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29507 28193 145 145 0 29362 0
[pid=27364] vsize: 118028
Current children cumulated CPU time (s) 1198.25
Current children cumulated vsize (Kb) 120152

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28968 0 0 0 120649 175 0 0 25 0 1 0 1855572212 121106432 28254 4294967295 134512640 135094434 3221224432 3221223088 134558292 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29567 28254 145 145 0 29422 0
[pid=27364] vsize: 118268
Current children cumulated CPU time (s) 1208.24
Current children cumulated vsize (Kb) 120392



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 27364
Raw data (/proc/27360/stat): 27360 (minisat+_script) S 27359 27360 5299 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855572207 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/27360/statm): 531 226 485 147 0 384 0
[pid=27360] vsize: 2124
Raw data (/proc/27364/stat): 27364 (minisat+_64-bit) R 27360 27360 5299 0 -1 0 28968 0 0 0 120649 175 0 0 25 0 1 0 1855572212 121106432 28254 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27364/statm): 29567 28254 145 145 0 29422 0
[pid=27364] vsize: 118268
Current children cumulated CPU time (s) 1208.24
Current children cumulated vsize (Kb) 120392

Sending SIGTERM to -27360
Sleeping 2 seconds
One traced child (pid=27360) ended because it received signal 15 (SIGTERM)
One traced child (pid=27364) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.31
CPU user time (s): 1206.5
CPU system time (s): 1.81072
CPU usage (%): 99.8472
Max. virtual memory (cumulated for all children) (Kb): 120392

Verifier Data

ERROR: no interpretation found !