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-pp08a.opb
MD5SUMd14265fdf4e5a3ef733af1f15b884cbe
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 6661373
Optimality of the best value was proved NO
Number of terms in the objective function 2304
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 178464600
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 178464600
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables3584
Total number of constraints136
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints136
Minimum length of a constraint21
Maximum length of a constraint160

Trace number 6227

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-20 04:35:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3385 boxname=wulflinc11 idbench=1041 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d14265fdf4e5a3ef733af1f15b884cbe  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb
IDLAUNCH: 3385
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        871804 kB
Buffers:         26188 kB
Cached:         110324 kB
SwapCached:        916 kB
Active:          40464 kB
Inactive:        98672 kB
HighTotal:      131008 kB
HighFree:        20944 kB
LowTotal:       903652 kB
LowFree:        850860 kB
SwapTotal:     2097136 kB
SwapFree:      2095640 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            18180 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:55:34 (client local time) WITH STATUS 0 IN 1208.76 SECONDS
stats: 3385 7 1208.76 0

Solver Data

c Parsing PB file...
c Converting 200 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 199]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 198]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 190]---> BDD-cost:  158
c ---[ 188]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> BDD-cost:  158
c ---[ 140]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> BDD-cost:  154
c ---[  92]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  78]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   24
c ---[  62]---> BDD-cost:   24
c ---[  61]---> BDD-cost:   24
c ---[  60]---> BDD-cost:   21
c ---[  59]---> BDD-cost:   21
c ---[  58]---> BDD-cost:   21
c ---[  57]---> BDD-cost:   21
c ---[  56]---> BDD-cost:   23
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:   24
c ---[  46]---> BDD-cost:   24
c ---[  45]---> BDD-cost:   24
c ---[  44]---> BDD-cost:   21
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   21
c ---[  41]---> BDD-cost:   21
c ---[  40]---> BDD-cost:   23
c ---[  39]---> BDD-cost:   24
c ---[  38]---> BDD-cost:   24
c ---[  37]---> BDD-cost:   24
c ---[  36]---> BDD-cost:   21
c ---[  35]---> BDD-cost:   21
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:   21
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   18
c ---[  27]---> BDD-cost:   18
c ---[  26]---> BDD-cost:   18
c ---[  25]---> BDD-cost:   18
c ---[  24]---> BDD-cost:   18
c ---[  23]---> BDD-cost:   24
c ---[  22]---> BDD-cost:   24
c ---[  21]---> BDD-cost:   24
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   21
c ---[  16]---> BDD-cost:   21
c ---[  15]---> BDD-cost:   19
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   19
c ---[  12]---> BDD-cost:   19
c ---[  11]---> BDD-cost:   19
c ---[  10]---> BDD-cost:   19
c ---[   9]---> BDD-cost:   19
c ---[   8]---> BDD-cost:   19
c ---[   7]---> BDD-cost:   19
c ---[   6]---> BDD-cost:   19
c ---[   5]---> BDD-cost:   19
c ---[   4]---> BDD-cost:   19
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   19
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  192439   454988 |   64146       0        0     nan |  0.000 % |
c |       100 |  192239   454543 |   70560      73      246     3.4 |  5.672 % |
c |       250 |  192206   454471 |   77616     216      748     3.5 |  5.687 % |
c |       475 |  192016   454049 |   85378     412     1679     4.1 |  5.767 % |
c |       812 |  191856   453691 |   93916     721     3004     4.2 |  5.829 % |
c |      1319 |  191699   453343 |  103307    1205     7766     6.4 |  5.895 % |
c |      2079 |  191487   452868 |  113638    1929    14801     7.7 |  5.980 % |
c |      3219 |  191290   452428 |  125002    3045    26101     8.6 |  6.059 % |
c |      4927 |  191115   452036 |  137502    4729    52510    11.1 |  6.130 % |
c |      7490 |  190810   451355 |  151252    7247    81997    11.3 |  6.249 % |
c |     11334 |  189963   449458 |  166378   10976   116451    10.6 |  6.584 % |
c |     17100 |  189884   449279 |  183016   16736   248554    14.9 |  6.614 % |
c |     25749 |  189706   448881 |  201317   25359   431867    17.0 |  6.685 % |
c |     38724 |  189201   447754 |  221449   38259   749831    19.6 |  6.890 % |
c |     58187 |  188976   447252 |  243594   57689  1288213    22.3 |  6.979 % |
c |     87379 |  187270   443439 |  267953   86663  1918714    22.1 |  7.664 % |
c |    131168 |  186149   440936 |  294749  130304  3171694    24.3 |  8.119 % |
c |    196855 |  183362   434691 |  324224  195633  4851184    24.8 |  9.223 % |
c |    295384 |  182771   433365 |  356646  294057  7348160    25.0 |  9.461 % |

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/411/stat): 411 (minisat+_script) R 410 411 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797468589 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/411/statm): 174 3 169 147 0 27 0
[pid=411] 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=412
New process pid=413
New process pid=414
execve syscall for /bin/sed executable
One traced child (pid=413) 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=414) exited with status: 0
One traced child (pid=412) exited with status: 0
New process pid=415
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-pp08a.opb

[startup+10.0044 s]
Raw data (loadavg): 0.71 0.92 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 6010 0 0 0 945 25 0 0 25 0 1 0 1797468594 28827648 5818 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/415/statm): 7038 5818 145 145 0 6893 0
[pid=415] vsize: 28152
Current children cumulated CPU time (s) 9.7
Current children cumulated vsize (Kb) 30276

[startup+20.0051 s]
Raw data (loadavg): 0.75 0.92 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 6191 0 0 0 1941 27 0 0 25 0 1 0 1797468594 29585408 5999 4294967295 134512640 135094434 3221224432 3221222976 134562076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 7223 5999 145 145 0 7078 0
[pid=415] vsize: 28892
Current children cumulated CPU time (s) 19.68
Current children cumulated vsize (Kb) 31016

[startup+30.0059 s]
Raw data (loadavg): 0.79 0.92 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 6631 0 0 0 2934 30 0 0 25 0 1 0 1797468594 31399936 6439 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 7666 6439 145 145 0 7521 0
[pid=415] vsize: 30664
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 32788

[startup+40.0067 s]
Raw data (loadavg): 0.82 0.93 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 6971 0 0 0 3928 32 0 0 25 0 1 0 1797468594 32878592 6779 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 8027 6779 145 145 0 7882 0
[pid=415] vsize: 32108
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 34232

[startup+50.0075 s]
Raw data (loadavg): 0.85 0.93 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 7337 0 0 0 4922 36 0 0 25 0 1 0 1797468594 34340864 7145 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 8384 7145 145 145 0 8239 0
[pid=415] vsize: 33536
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 35660

[startup+60.0083 s]
Raw data (loadavg): 0.87 0.93 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 7730 0 0 0 5915 39 0 0 25 0 1 0 1797468594 35913728 7538 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 8768 7538 145 145 0 8623 0
[pid=415] vsize: 35072
Current children cumulated CPU time (s) 59.54
Current children cumulated vsize (Kb) 37196

[startup+70.0091 s]
Raw data (loadavg): 0.89 0.93 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 7988 0 0 0 6911 40 0 0 25 0 1 0 1797468594 36929536 7796 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9016 7796 145 145 0 8871 0
[pid=415] vsize: 36064
Current children cumulated CPU time (s) 69.51
Current children cumulated vsize (Kb) 38188

[startup+80.0098 s]
Raw data (loadavg): 0.91 0.93 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 8183 0 0 0 7909 41 0 0 25 0 1 0 1797468594 37978112 7991 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9272 7991 145 145 0 9127 0
[pid=415] vsize: 37088
Current children cumulated CPU time (s) 79.5
Current children cumulated vsize (Kb) 39212

[startup+90.0106 s]
Raw data (loadavg): 0.92 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 8292 0 0 0 8907 41 0 0 25 0 1 0 1797468594 38387712 8100 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9372 8100 145 145 0 9227 0
[pid=415] vsize: 37488
Current children cumulated CPU time (s) 89.48
Current children cumulated vsize (Kb) 39612

[startup+100.011 s]
Raw data (loadavg): 0.93 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 8390 0 0 0 9906 42 0 0 25 0 1 0 1797468594 38760448 8198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9463 8198 145 145 0 9318 0
[pid=415] vsize: 37852
Current children cumulated CPU time (s) 99.48
Current children cumulated vsize (Kb) 39976

[startup+110.015 s]
Raw data (loadavg): 0.94 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 8629 0 0 0 10902 43 0 0 25 0 1 0 1797468594 39723008 8437 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9698 8437 145 145 0 9553 0
[pid=415] vsize: 38792
Current children cumulated CPU time (s) 109.45
Current children cumulated vsize (Kb) 40916

[startup+120.016 s]
Raw data (loadavg): 0.95 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 8873 0 0 0 11898 45 0 0 25 0 1 0 1797468594 40681472 8681 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 9932 8681 145 145 0 9787 0
[pid=415] vsize: 39728
Current children cumulated CPU time (s) 119.43
Current children cumulated vsize (Kb) 41852

[startup+130.017 s]
Raw data (loadavg): 0.96 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 9109 0 0 0 12893 47 0 0 25 0 1 0 1797468594 41635840 8917 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 10165 8917 145 145 0 10020 0
[pid=415] vsize: 40660
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 42784

[startup+140.018 s]
Raw data (loadavg): 0.96 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 9237 0 0 0 13892 48 0 0 25 0 1 0 1797468594 42192896 9045 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 10301 9045 145 145 0 10156 0
[pid=415] vsize: 41204
Current children cumulated CPU time (s) 139.4
Current children cumulated vsize (Kb) 43328

[startup+150.018 s]
Raw data (loadavg): 0.97 0.94 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 9416 0 0 0 14889 50 0 0 25 0 1 0 1797468594 42909696 9224 4294967295 134512640 135094434 3221224432 3221223088 134557908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 10476 9224 145 145 0 10331 0
[pid=415] vsize: 41904
Current children cumulated CPU time (s) 149.39
Current children cumulated vsize (Kb) 44028

[startup+160.019 s]
Raw data (loadavg): 0.97 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 9505 0 0 0 15888 50 0 0 25 0 1 0 1797468594 43261952 9313 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 10562 9313 145 145 0 10417 0
[pid=415] vsize: 42248
Current children cumulated CPU time (s) 159.38
Current children cumulated vsize (Kb) 44372

[startup+170.02 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 9770 0 0 0 16884 52 0 0 25 0 1 0 1797468594 44326912 9578 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 10822 9578 145 145 0 10677 0
[pid=415] vsize: 43288
Current children cumulated CPU time (s) 169.36
Current children cumulated vsize (Kb) 45412

[startup+180.021 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10086 0 0 0 17879 54 0 0 25 0 1 0 1797468594 45588480 9894 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11130 9894 145 145 0 10985 0
[pid=415] vsize: 44520
Current children cumulated CPU time (s) 179.33
Current children cumulated vsize (Kb) 46644

[startup+190.021 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10324 0 0 0 18876 56 0 0 25 0 1 0 1797468594 46530560 10132 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11360 10132 145 145 0 11215 0
[pid=415] vsize: 45440
Current children cumulated CPU time (s) 189.32
Current children cumulated vsize (Kb) 47564

[startup+200.021 s]
Raw data (loadavg): 0.98 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10509 0 0 0 19873 57 0 0 25 0 1 0 1797468594 47804416 10317 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11671 10317 145 145 0 11526 0
[pid=415] vsize: 46684
Current children cumulated CPU time (s) 199.3
Current children cumulated vsize (Kb) 48808

[startup+210.022 s]
Raw data (loadavg): 0.99 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10533 0 0 0 20872 57 0 0 25 0 1 0 1797468594 47902720 10341 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11695 10341 145 145 0 11550 0
[pid=415] vsize: 46780
Current children cumulated CPU time (s) 209.29
Current children cumulated vsize (Kb) 48904

[startup+220.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10589 0 0 0 21871 58 0 0 25 0 1 0 1797468594 48128000 10397 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11750 10397 145 145 0 11605 0
[pid=415] vsize: 47000
Current children cumulated CPU time (s) 219.29
Current children cumulated vsize (Kb) 49124

[startup+230.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10717 0 0 0 22869 59 0 0 25 0 1 0 1797468594 48644096 10525 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11876 10525 145 145 0 11731 0
[pid=415] vsize: 47504
Current children cumulated CPU time (s) 229.28
Current children cumulated vsize (Kb) 49628

[startup+240.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10795 0 0 0 23868 60 0 0 25 0 1 0 1797468594 48934912 10603 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 11947 10603 145 145 0 11802 0
[pid=415] vsize: 47788
Current children cumulated CPU time (s) 239.28
Current children cumulated vsize (Kb) 49912

[startup+250.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 10997 0 0 0 24865 61 0 0 25 0 1 0 1797468594 49741824 10805 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12144 10805 145 145 0 11999 0
[pid=415] vsize: 48576
Current children cumulated CPU time (s) 249.26
Current children cumulated vsize (Kb) 50700

[startup+260.025 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11194 0 0 0 25861 63 0 0 25 0 1 0 1797468594 50561024 11002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12344 11002 145 145 0 12199 0
[pid=415] vsize: 49376
Current children cumulated CPU time (s) 259.24
Current children cumulated vsize (Kb) 51500

[startup+270.026 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11291 0 0 0 26860 63 0 0 25 0 1 0 1797468594 50958336 11099 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12441 11099 145 145 0 12296 0
[pid=415] vsize: 49764
Current children cumulated CPU time (s) 269.23
Current children cumulated vsize (Kb) 51888

[startup+280.027 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11335 0 0 0 27859 63 0 0 25 0 1 0 1797468594 51142656 11143 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12486 11143 145 145 0 12341 0
[pid=415] vsize: 49944
Current children cumulated CPU time (s) 279.22
Current children cumulated vsize (Kb) 52068

[startup+290.027 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11462 0 0 0 28857 64 0 0 25 0 1 0 1797468594 51732480 11270 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12630 11270 145 145 0 12485 0
[pid=415] vsize: 50520
Current children cumulated CPU time (s) 289.21
Current children cumulated vsize (Kb) 52644

[startup+300.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11646 0 0 0 29855 65 0 0 25 0 1 0 1797468594 52531200 11454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12825 11454 145 145 0 12680 0
[pid=415] vsize: 51300
Current children cumulated CPU time (s) 299.2
Current children cumulated vsize (Kb) 53424

[startup+310.029 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11782 0 0 0 30852 66 0 0 25 0 1 0 1797468594 53121024 11590 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 12969 11590 145 145 0 12824 0
[pid=415] vsize: 51876
Current children cumulated CPU time (s) 309.18
Current children cumulated vsize (Kb) 54000

[startup+320.03 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 11866 0 0 0 31851 67 0 0 25 0 1 0 1797468594 53452800 11674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13050 11674 145 145 0 12905 0
[pid=415] vsize: 52200
Current children cumulated CPU time (s) 319.18
Current children cumulated vsize (Kb) 54324

[startup+330.03 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12021 0 0 0 32849 68 0 0 25 0 1 0 1797468594 54091776 11829 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13206 11829 145 145 0 13061 0
[pid=415] vsize: 52824
Current children cumulated CPU time (s) 329.17
Current children cumulated vsize (Kb) 54948

[startup+340.031 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12035 0 0 0 33848 68 0 0 25 0 1 0 1797468594 54145024 11843 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13219 11843 145 145 0 13074 0
[pid=415] vsize: 52876
Current children cumulated CPU time (s) 339.16
Current children cumulated vsize (Kb) 55000

[startup+350.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12134 0 0 0 34847 69 0 0 25 0 1 0 1797468594 54550528 11942 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13318 11942 145 145 0 13173 0
[pid=415] vsize: 53272
Current children cumulated CPU time (s) 349.16
Current children cumulated vsize (Kb) 55396

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12262 0 0 0 35846 70 0 0 25 0 1 0 1797468594 55115776 12070 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13456 12070 145 145 0 13311 0
[pid=415] vsize: 53824
Current children cumulated CPU time (s) 359.16
Current children cumulated vsize (Kb) 55948

[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12336 0 0 0 36845 70 0 0 25 0 1 0 1797468594 55427072 12144 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13532 12144 145 145 0 13387 0
[pid=415] vsize: 54128
Current children cumulated CPU time (s) 369.15
Current children cumulated vsize (Kb) 56252

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12370 0 0 0 37844 70 0 0 25 0 1 0 1797468594 55541760 12178 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13560 12178 145 145 0 13415 0
[pid=415] vsize: 54240
Current children cumulated CPU time (s) 379.14
Current children cumulated vsize (Kb) 56364

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12468 0 0 0 38843 71 0 0 25 0 1 0 1797468594 55951360 12276 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13660 12276 145 145 0 13515 0
[pid=415] vsize: 54640
Current children cumulated CPU time (s) 389.14
Current children cumulated vsize (Kb) 56764

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12521 0 0 0 39842 72 0 0 25 0 1 0 1797468594 56147968 12329 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13708 12329 145 145 0 13563 0
[pid=415] vsize: 54832
Current children cumulated CPU time (s) 399.14
Current children cumulated vsize (Kb) 56956

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12569 0 0 0 40842 72 0 0 25 0 1 0 1797468594 56336384 12377 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13754 12377 145 145 0 13609 0
[pid=415] vsize: 55016
Current children cumulated CPU time (s) 409.14
Current children cumulated vsize (Kb) 57140

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12617 0 0 0 41842 72 0 0 25 0 1 0 1797468594 56516608 12425 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13798 12425 145 145 0 13653 0
[pid=415] vsize: 55192
Current children cumulated CPU time (s) 419.14
Current children cumulated vsize (Kb) 57316

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12803 0 0 0 42838 74 0 0 25 0 1 0 1797468594 57262080 12611 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 13980 12611 145 145 0 13835 0
[pid=415] vsize: 55920
Current children cumulated CPU time (s) 429.12
Current children cumulated vsize (Kb) 58044

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12894 0 0 0 43837 75 0 0 25 0 1 0 1797468594 57647104 12702 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14074 12702 145 145 0 13929 0
[pid=415] vsize: 56296
Current children cumulated CPU time (s) 439.12
Current children cumulated vsize (Kb) 58420

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 12953 0 0 0 44836 75 0 0 25 0 1 0 1797468594 57872384 12761 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14129 12761 145 145 0 13984 0
[pid=415] vsize: 56516
Current children cumulated CPU time (s) 449.11
Current children cumulated vsize (Kb) 58640

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13066 0 0 0 45835 75 0 0 25 0 1 0 1797468594 58335232 12874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14242 12874 145 145 0 14097 0
[pid=415] vsize: 56968
Current children cumulated CPU time (s) 459.1
Current children cumulated vsize (Kb) 59092

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13233 0 0 0 46833 76 0 0 25 0 1 0 1797468594 58961920 13041 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14395 13041 145 145 0 14250 0
[pid=415] vsize: 57580
Current children cumulated CPU time (s) 469.09
Current children cumulated vsize (Kb) 59704

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13342 0 0 0 47831 77 0 0 25 0 1 0 1797468594 59363328 13150 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14493 13150 145 145 0 14348 0
[pid=415] vsize: 57972
Current children cumulated CPU time (s) 479.08
Current children cumulated vsize (Kb) 60096

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13396 0 0 0 48831 77 0 0 25 0 1 0 1797468594 59568128 13204 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14543 13204 145 145 0 14398 0
[pid=415] vsize: 58172
Current children cumulated CPU time (s) 489.08
Current children cumulated vsize (Kb) 60296

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13455 0 0 0 49830 77 0 0 25 0 1 0 1797468594 59801600 13263 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14600 13263 145 145 0 14455 0
[pid=415] vsize: 58400
Current children cumulated CPU time (s) 499.07
Current children cumulated vsize (Kb) 60524

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) T 411 411 9854 0 -1 0 13543 0 0 0 50829 78 0 0 25 0 1 0 1797468594 60149760 13351 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/415/statm): 14685 13351 145 145 0 14540 0
[pid=415] vsize: 58740
Current children cumulated CPU time (s) 509.07
Current children cumulated vsize (Kb) 60864

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13651 0 0 0 51828 79 0 0 25 0 1 0 1797468594 60559360 13459 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14785 13459 145 145 0 14640 0
[pid=415] vsize: 59140
Current children cumulated CPU time (s) 519.07
Current children cumulated vsize (Kb) 61264

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13728 0 0 0 52826 79 0 0 25 0 1 0 1797468594 60854272 13536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14857 13536 145 145 0 14712 0
[pid=415] vsize: 59428
Current children cumulated CPU time (s) 529.05
Current children cumulated vsize (Kb) 61552

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13793 0 0 0 53826 80 0 0 25 0 1 0 1797468594 61112320 13601 4294967295 134512640 135094434 3221224432 3221223056 134557587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14920 13601 145 145 0 14775 0
[pid=415] vsize: 59680
Current children cumulated CPU time (s) 539.06
Current children cumulated vsize (Kb) 61804

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13838 0 0 0 54825 80 0 0 25 0 1 0 1797468594 61276160 13646 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 14960 13646 145 145 0 14815 0
[pid=415] vsize: 59840
Current children cumulated CPU time (s) 549.05
Current children cumulated vsize (Kb) 61964

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13891 0 0 0 55824 80 0 0 25 0 1 0 1797468594 61485056 13699 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15011 13699 145 145 0 14866 0
[pid=415] vsize: 60044
Current children cumulated CPU time (s) 559.04
Current children cumulated vsize (Kb) 62168

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 13990 0 0 0 56823 81 0 0 25 0 1 0 1797468594 61857792 13798 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15102 13798 145 145 0 14957 0
[pid=415] vsize: 60408
Current children cumulated CPU time (s) 569.04
Current children cumulated vsize (Kb) 62532

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14075 0 0 0 57822 82 0 0 25 0 1 0 1797468594 62201856 13883 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15186 13883 145 145 0 15041 0
[pid=415] vsize: 60744
Current children cumulated CPU time (s) 579.04
Current children cumulated vsize (Kb) 62868

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14230 0 0 0 58820 83 0 0 25 0 1 0 1797468594 62812160 14038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15335 14038 145 145 0 15190 0
[pid=415] vsize: 61340
Current children cumulated CPU time (s) 589.03
Current children cumulated vsize (Kb) 63464

[startup+600.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14312 0 0 0 59819 84 0 0 25 0 1 0 1797468594 63172608 14120 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15423 14120 145 145 0 15278 0
[pid=415] vsize: 61692
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 63816

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14448 0 0 0 60817 84 0 0 25 0 1 0 1797468594 63717376 14256 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15556 14256 145 145 0 15411 0
[pid=415] vsize: 62224
Current children cumulated CPU time (s) 609.01
Current children cumulated vsize (Kb) 64348

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14551 0 0 0 61816 85 0 0 25 0 1 0 1797468594 64131072 14359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15657 14359 145 145 0 15512 0
[pid=415] vsize: 62628
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 64752

[startup+630.058 s]
Raw data (loadavg): 1.23 1.02 0.94 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14727 0 0 0 62813 86 0 0 25 0 1 0 1797468594 64839680 14535 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15830 14535 145 145 0 15685 0
[pid=415] vsize: 63320
Current children cumulated CPU time (s) 628.99
Current children cumulated vsize (Kb) 65444

[startup+640.059 s]
Raw data (loadavg): 1.27 1.04 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14840 0 0 0 63811 87 0 0 25 0 1 0 1797468594 65273856 14648 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15936 14648 145 145 0 15791 0
[pid=415] vsize: 63744
Current children cumulated CPU time (s) 638.98
Current children cumulated vsize (Kb) 65868

[startup+650.06 s]
Raw data (loadavg): 1.23 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14907 0 0 0 64810 87 0 0 25 0 1 0 1797468594 65523712 14715 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 15997 14715 145 145 0 15852 0
[pid=415] vsize: 63988
Current children cumulated CPU time (s) 648.97
Current children cumulated vsize (Kb) 66112

[startup+660.061 s]
Raw data (loadavg): 1.19 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 14948 0 0 0 65809 87 0 0 25 0 1 0 1797468594 65683456 14756 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16036 14756 145 145 0 15891 0
[pid=415] vsize: 64144
Current children cumulated CPU time (s) 658.96
Current children cumulated vsize (Kb) 66268

[startup+670.062 s]
Raw data (loadavg): 1.16 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15055 0 0 0 66808 88 0 0 25 0 1 0 1797468594 67153920 14863 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16395 14863 145 145 0 16250 0
[pid=415] vsize: 65580
Current children cumulated CPU time (s) 668.96
Current children cumulated vsize (Kb) 67704

[startup+680.063 s]
Raw data (loadavg): 1.14 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15146 0 0 0 67807 88 0 0 25 0 1 0 1797468594 67522560 14954 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16485 14954 145 145 0 16340 0
[pid=415] vsize: 65940
Current children cumulated CPU time (s) 678.95
Current children cumulated vsize (Kb) 68064

[startup+690.064 s]
Raw data (loadavg): 1.12 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15244 0 0 0 68806 89 0 0 25 0 1 0 1797468594 67915776 15052 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16581 15052 145 145 0 16436 0
[pid=415] vsize: 66324
Current children cumulated CPU time (s) 688.95
Current children cumulated vsize (Kb) 68448

[startup+700.065 s]
Raw data (loadavg): 1.10 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15339 0 0 0 69805 90 0 0 25 0 1 0 1797468594 68296704 15147 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16674 15147 145 145 0 16529 0
[pid=415] vsize: 66696
Current children cumulated CPU time (s) 698.95
Current children cumulated vsize (Kb) 68820

[startup+710.065 s]
Raw data (loadavg): 1.08 1.03 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15428 0 0 0 70804 90 0 0 25 0 1 0 1797468594 68648960 15236 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16760 15236 145 145 0 16615 0
[pid=415] vsize: 67040
Current children cumulated CPU time (s) 708.94
Current children cumulated vsize (Kb) 69164

[startup+720.066 s]
Raw data (loadavg): 1.07 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15521 0 0 0 71803 91 0 0 25 0 1 0 1797468594 69038080 15329 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16855 15329 145 145 0 16710 0
[pid=415] vsize: 67420
Current children cumulated CPU time (s) 718.94
Current children cumulated vsize (Kb) 69544

[startup+730.067 s]
Raw data (loadavg): 1.06 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15588 0 0 0 72802 91 0 0 25 0 1 0 1797468594 69316608 15396 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 16923 15396 145 145 0 16778 0
[pid=415] vsize: 67692
Current children cumulated CPU time (s) 728.93
Current children cumulated vsize (Kb) 69816

[startup+740.069 s]
Raw data (loadavg): 1.05 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15672 0 0 0 73801 92 0 0 25 0 1 0 1797468594 69652480 15480 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17005 15480 145 145 0 16860 0
[pid=415] vsize: 68020
Current children cumulated CPU time (s) 738.93
Current children cumulated vsize (Kb) 70144

[startup+750.069 s]
Raw data (loadavg): 1.04 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15759 0 0 0 74800 92 0 0 25 0 1 0 1797468594 69996544 15567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17089 15567 145 145 0 16944 0
[pid=415] vsize: 68356
Current children cumulated CPU time (s) 748.92
Current children cumulated vsize (Kb) 70480

[startup+760.07 s]
Raw data (loadavg): 1.03 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15867 0 0 0 75799 93 0 0 25 0 1 0 1797468594 70422528 15675 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17193 15675 145 145 0 17048 0
[pid=415] vsize: 68772
Current children cumulated CPU time (s) 758.92
Current children cumulated vsize (Kb) 70896

[startup+770.071 s]
Raw data (loadavg): 1.03 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 15968 0 0 0 76798 94 0 0 25 0 1 0 1797468594 70955008 15776 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17323 15776 145 145 0 17178 0
[pid=415] vsize: 69292
Current children cumulated CPU time (s) 768.92
Current children cumulated vsize (Kb) 71416

[startup+780.072 s]
Raw data (loadavg): 1.02 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16087 0 0 0 77796 94 0 0 25 0 1 0 1797468594 71401472 15895 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17432 15895 145 145 0 17287 0
[pid=415] vsize: 69728
Current children cumulated CPU time (s) 778.9
Current children cumulated vsize (Kb) 71852

[startup+790.073 s]
Raw data (loadavg): 1.02 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16190 0 0 0 78794 95 0 0 25 0 1 0 1797468594 71794688 15998 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17528 15998 145 145 0 17383 0
[pid=415] vsize: 70112
Current children cumulated CPU time (s) 788.89
Current children cumulated vsize (Kb) 72236

[startup+800.073 s]
Raw data (loadavg): 1.02 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16274 0 0 0 79793 95 0 0 25 0 1 0 1797468594 72122368 16082 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17608 16082 145 145 0 17463 0
[pid=415] vsize: 70432
Current children cumulated CPU time (s) 798.88
Current children cumulated vsize (Kb) 72556

[startup+810.075 s]
Raw data (loadavg): 1.01 1.02 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16401 0 0 0 80792 97 0 0 25 0 1 0 1797468594 72626176 16209 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17731 16209 145 145 0 17586 0
[pid=415] vsize: 70924
Current children cumulated CPU time (s) 808.89
Current children cumulated vsize (Kb) 73048

[startup+820.076 s]
Raw data (loadavg): 1.01 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16469 0 0 0 81791 97 0 0 25 0 1 0 1797468594 72884224 16277 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17794 16277 145 145 0 17649 0
[pid=415] vsize: 71176
Current children cumulated CPU time (s) 818.88
Current children cumulated vsize (Kb) 73300

[startup+830.077 s]
Raw data (loadavg): 1.01 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16533 0 0 0 82790 97 0 0 25 0 1 0 1797468594 73150464 16341 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17859 16341 145 145 0 17714 0
[pid=415] vsize: 71436
Current children cumulated CPU time (s) 828.87
Current children cumulated vsize (Kb) 73560

[startup+840.078 s]
Raw data (loadavg): 1.01 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16629 0 0 0 83789 97 0 0 25 0 1 0 1797468594 73535488 16437 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 17953 16437 145 145 0 17808 0
[pid=415] vsize: 71812
Current children cumulated CPU time (s) 838.86
Current children cumulated vsize (Kb) 73936

[startup+850.078 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16767 0 0 0 84786 98 0 0 25 0 1 0 1797468594 74084352 16575 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18087 16575 145 145 0 17942 0
[pid=415] vsize: 72348
Current children cumulated CPU time (s) 848.84
Current children cumulated vsize (Kb) 74472

[startup+860.08 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16843 0 0 0 85786 99 0 0 25 0 1 0 1797468594 74383360 16651 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18160 16651 145 145 0 18015 0
[pid=415] vsize: 72640
Current children cumulated CPU time (s) 858.85
Current children cumulated vsize (Kb) 74764

[startup+870.081 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 16939 0 0 0 86784 100 0 0 25 0 1 0 1797468594 74768384 16747 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18254 16747 145 145 0 18109 0
[pid=415] vsize: 73016
Current children cumulated CPU time (s) 868.84
Current children cumulated vsize (Kb) 75140

[startup+880.082 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17004 0 0 0 87783 100 0 0 25 0 1 0 1797468594 75026432 16812 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18317 16812 145 145 0 18172 0
[pid=415] vsize: 73268
Current children cumulated CPU time (s) 878.83
Current children cumulated vsize (Kb) 75392

[startup+890.082 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17077 0 0 0 88782 101 0 0 25 0 1 0 1797468594 75309056 16885 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18386 16885 145 145 0 18241 0
[pid=415] vsize: 73544
Current children cumulated CPU time (s) 888.83
Current children cumulated vsize (Kb) 75668

[startup+900.083 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17249 0 0 0 89780 102 0 0 25 0 1 0 1797468594 75997184 17057 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18554 17057 145 145 0 18409 0
[pid=415] vsize: 74216
Current children cumulated CPU time (s) 898.82
Current children cumulated vsize (Kb) 76340

[startup+910.084 s]
Raw data (loadavg): 1.00 1.01 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17318 0 0 0 90779 102 0 0 25 0 1 0 1797468594 76263424 17126 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18619 17126 145 145 0 18474 0
[pid=415] vsize: 74476
Current children cumulated CPU time (s) 908.81
Current children cumulated vsize (Kb) 76600

[startup+920.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17387 0 0 0 91778 103 0 0 25 0 1 0 1797468594 76533760 17195 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18685 17195 145 145 0 18540 0
[pid=415] vsize: 74740
Current children cumulated CPU time (s) 918.81
Current children cumulated vsize (Kb) 76864

[startup+930.086 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17470 0 0 0 92777 103 0 0 25 0 1 0 1797468594 76922880 17278 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18780 17278 145 145 0 18635 0
[pid=415] vsize: 75120
Current children cumulated CPU time (s) 928.8
Current children cumulated vsize (Kb) 77244

[startup+940.087 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17561 0 0 0 93776 104 0 0 25 0 1 0 1797468594 77271040 17369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18865 17369 145 145 0 18720 0
[pid=415] vsize: 75460
Current children cumulated CPU time (s) 938.8
Current children cumulated vsize (Kb) 77584

[startup+950.088 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17668 0 0 0 94774 105 0 0 25 0 1 0 1797468594 77701120 17476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 18970 17476 145 145 0 18825 0
[pid=415] vsize: 75880
Current children cumulated CPU time (s) 948.79
Current children cumulated vsize (Kb) 78004

[startup+960.089 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17777 0 0 0 95773 105 0 0 25 0 1 0 1797468594 78172160 17585 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19085 17585 145 145 0 18940 0
[pid=415] vsize: 76340
Current children cumulated CPU time (s) 958.78
Current children cumulated vsize (Kb) 78464

[startup+970.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 17883 0 0 0 96771 106 0 0 25 0 1 0 1797468594 78639104 17691 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19199 17691 145 145 0 19054 0
[pid=415] vsize: 76796
Current children cumulated CPU time (s) 968.77
Current children cumulated vsize (Kb) 78920

[startup+980.091 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18003 0 0 0 97770 107 0 0 25 0 1 0 1797468594 79138816 17811 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19321 17811 145 145 0 19176 0
[pid=415] vsize: 77284
Current children cumulated CPU time (s) 978.77
Current children cumulated vsize (Kb) 79408

[startup+990.091 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18107 0 0 0 98768 107 0 0 25 0 1 0 1797468594 79556608 17915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19423 17915 145 145 0 19278 0
[pid=415] vsize: 77692
Current children cumulated CPU time (s) 988.75
Current children cumulated vsize (Kb) 79816

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18191 0 0 0 99768 107 0 0 25 0 1 0 1797468594 79917056 17999 4294967295 134512640 135094434 3221224432 3221222976 134779242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19511 17999 145 145 0 19366 0
[pid=415] vsize: 78044
Current children cumulated CPU time (s) 998.75
Current children cumulated vsize (Kb) 80168

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18303 0 0 0 100767 108 0 0 25 0 1 0 1797468594 80416768 18111 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19633 18111 145 145 0 19488 0
[pid=415] vsize: 78532
Current children cumulated CPU time (s) 1008.75
Current children cumulated vsize (Kb) 80656

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18406 0 0 0 101766 108 0 0 25 0 1 0 1797468594 80814080 18214 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19730 18214 145 145 0 19585 0
[pid=415] vsize: 78920
Current children cumulated CPU time (s) 1018.74
Current children cumulated vsize (Kb) 81044

[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18517 0 0 0 102765 109 0 0 25 0 1 0 1797468594 81240064 18325 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19834 18325 145 145 0 19689 0
[pid=415] vsize: 79336
Current children cumulated CPU time (s) 1028.74
Current children cumulated vsize (Kb) 81460

[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18627 0 0 0 103764 109 0 0 25 0 1 0 1797468594 81698816 18435 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 19946 18435 145 145 0 19801 0
[pid=415] vsize: 79784
Current children cumulated CPU time (s) 1038.73
Current children cumulated vsize (Kb) 81908

[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18731 0 0 0 104762 110 0 0 25 0 1 0 1797468594 82092032 18539 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20042 18539 145 145 0 19897 0
[pid=415] vsize: 80168
Current children cumulated CPU time (s) 1048.72
Current children cumulated vsize (Kb) 82292

[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18858 0 0 0 105760 111 0 0 25 0 1 0 1797468594 82591744 18666 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20164 18666 145 145 0 20019 0
[pid=415] vsize: 80656
Current children cumulated CPU time (s) 1058.71
Current children cumulated vsize (Kb) 82780

[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 18966 0 0 0 106759 112 0 0 25 0 1 0 1797468594 83013632 18774 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20267 18774 145 145 0 20122 0
[pid=415] vsize: 81068
Current children cumulated CPU time (s) 1068.71
Current children cumulated vsize (Kb) 83192

[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19092 0 0 0 107757 113 0 0 25 0 1 0 1797468594 83640320 18900 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20420 18900 145 145 0 20275 0
[pid=415] vsize: 81680
Current children cumulated CPU time (s) 1078.7
Current children cumulated vsize (Kb) 83804

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19197 0 0 0 108755 113 0 0 25 0 1 0 1797468594 84078592 19005 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20527 19005 145 145 0 20382 0
[pid=415] vsize: 82108
Current children cumulated CPU time (s) 1088.68
Current children cumulated vsize (Kb) 84232

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 109755 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1098.68
Current children cumulated vsize (Kb) 84332

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 110755 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1108.68
Current children cumulated vsize (Kb) 84332

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 111756 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1118.69
Current children cumulated vsize (Kb) 84332

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 112756 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1128.69
Current children cumulated vsize (Kb) 84332

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 113756 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1138.69
Current children cumulated vsize (Kb) 84332

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 114756 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1148.69
Current children cumulated vsize (Kb) 84332

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 115757 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1158.7
Current children cumulated vsize (Kb) 84332

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 116757 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1168.7
Current children cumulated vsize (Kb) 84332

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 117757 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1178.7
Current children cumulated vsize (Kb) 84332

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 118757 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1188.7
Current children cumulated vsize (Kb) 84332

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 119758 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1198.71
Current children cumulated vsize (Kb) 84332

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 120758 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1208.71
Current children cumulated vsize (Kb) 84332



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 415
Raw data (/proc/411/stat): 411 (minisat+_script) S 410 411 9854 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797468589 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/411/statm): 531 226 485 147 0 384 0
[pid=411] vsize: 2124
Raw data (/proc/415/stat): 415 (minisat+_64-bit) R 411 411 9854 0 -1 0 19224 0 0 0 120758 113 0 0 25 0 1 0 1797468594 84180992 19032 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/415/statm): 20552 19032 145 145 0 20407 0
[pid=415] vsize: 82208
Current children cumulated CPU time (s) 1208.71
Current children cumulated vsize (Kb) 84332

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.76
CPU user time (s): 1207.59
CPU system time (s): 1.17382
CPU usage (%): 99.8848
Max. virtual memory (cumulated for all children) (Kb): 84332

Verifier Data

ERROR: no interpretation found !