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

Namesubmitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb
MD5SUM00bdc6bb9bafd4b1100d8bfa4f886626
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 52
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.173973
Number of variables5100
Total number of constraints202
Number of constraints which are clauses102
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint51

Trace number 824

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-18 12:28:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2361 boxname=wulflinc15 idbench=17 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00bdc6bb9bafd4b1100d8bfa4f886626  /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb
IDLAUNCH: 2361
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        938296 kB
Buffers:         35344 kB
Cached:          32100 kB
SwapCached:        692 kB
Active:          53464 kB
Inactive:        16572 kB
HighTotal:      131008 kB
HighFree:        95676 kB
LowTotal:       903652 kB
LowFree:        842620 kB
SwapTotal:     2097136 kB
SwapFree:      2095920 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            20668 kB
Committed_AS:    64152 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:48:25 (client local time) WITH STATUS 0 IN 1207.08 SECONDS
stats: 2361 7 1207.08 0

Solver Data

c Parsing PB file...
c Converting 202 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................
c ---[  99]---> BDD-cost:   99
c ---[  98]---> BDD-cost:   99
c ---[  97]---> BDD-cost:   99
c ---[  96]---> BDD-cost:   99
c ---[  95]---> BDD-cost:   99
c ---[  94]---> BDD-cost:   99
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:   99
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:   99
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:   99
c ---[  87]---> BDD-cost:   99
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   99
c ---[  83]---> BDD-cost:   99
c ---[  82]---> BDD-cost:   99
c ---[  81]---> BDD-cost:   99
c ---[  80]---> BDD-cost:   99
c ---[  79]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   99
c ---[  77]---> BDD-cost:   99
c ---[  76]---> BDD-cost:   99
c ---[  75]---> BDD-cost:   99
c ---[  74]---> BDD-cost:   99
c ---[  73]---> BDD-cost:   99
c ---[  72]---> BDD-cost:   99
c ---[  71]---> BDD-cost:   99
c ---[  70]---> BDD-cost:   99
c ---[  69]---> BDD-cost:   99
c ---[  68]---> BDD-cost:   99
c ---[  67]---> BDD-cost:   99
c ---[  66]---> BDD-cost:   99
c ---[  65]---> BDD-cost:   99
c ---[  64]---> BDD-cost:   99
c ---[  63]---> BDD-cost:   99
c ---[  62]---> BDD-cost:   99
c ---[  61]---> BDD-cost:   99
c ---[  60]---> BDD-cost:   99
c ---[  59]---> BDD-cost:   99
c ---[  58]---> BDD-cost:   99
c ---[  57]---> BDD-cost:   99
c ---[  56]---> BDD-cost:   99
c ---[  55]---> BDD-cost:   99
c ---[  54]---> BDD-cost:   99
c ---[  53]---> BDD-cost:   99
c ---[  52]---> BDD-cost:   99
c ---[  51]---> BDD-cost:   99
c ---[  50]---> BDD-cost:   99
c ---[  49]---> BDD-cost:   99
c ---[  48]---> BDD-cost:   99
c ---[  47]---> BDD-cost:   99
c ---[  46]---> BDD-cost:   99
c ---[  45]---> BDD-cost:   99
c ---[  44]---> BDD-cost:   99
c ---[  43]---> BDD-cost:   99
c ---[  42]---> BDD-cost:   99
c ---[  41]---> BDD-cost:   99
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:   99
c ---[  36]---> BDD-cost:   99
c ---[  35]---> BDD-cost:   99
c ---[  34]---> BDD-cost:   99
c ---[  33]---> BDD-cost:   99
c ---[  32]---> BDD-cost:   99
c ---[  31]---> BDD-cost:   99
c ---[  30]---> BDD-cost:   99
c ---[  29]---> BDD-cost:   99
c ---[  28]---> BDD-cost:   99
c ---[  27]---> BDD-cost:   99
c ---[  26]---> BDD-cost:   99
c ---[  25]---> BDD-cost:   99
c ---[  24]---> BDD-cost:   99
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24702    69100 |    8234       0        0     nan |  0.000 % |
c |       103 |   24702    69100 |    9057     103    21251   206.3 |  0.667 % |
c |       257 |   24702    69100 |    9963     257    49705   193.4 |  0.667 % |
c |       483 |   24702    69100 |   10959     483   104379   216.1 |  0.667 % |
c |       820 |   24702    69100 |   12055     820   161617   197.1 |  0.667 % |
c |      1328 |   24702    69100 |   13260    1328   304812   229.5 |  0.667 % |
c |      2087 |   24702    69100 |   14587    2087   499248   239.2 |  0.667 % |
c |      3226 |   24702    69100 |   16045    3226   939931   291.4 |  0.667 % |
c |      4934 |   24702    69100 |   17650    4934  1692679   343.1 |  0.667 % |
c |      7497 |   24702    69100 |   19415    7497  2867483   382.5 |  0.667 % |
c |     11345 |   24702    69100 |   21356   11345  4334050   382.0 |  0.667 % |
c |     17113 |   24702    69100 |   23492   17113  7407340   432.8 |  0.667 % |
c |     25762 |   24702    69100 |   25841   25762 11735963   455.6 |  0.667 % |
c |     38736 |   24702    69100 |   28426   19007  8582103   451.5 |  0.667 % |
c |     58197 |   24702    69100 |   31268   16084  9622847   598.3 |  0.667 % |
c |     87391 |   24702    69100 |   34395   15805  8643661   546.9 |  0.667 % |
c |    131182 |   24702    69100 |   37835   29400 20102392   683.8 |  0.667 % |

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/1973/stat): 1973 (minisat+_script) R 1972 1973 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783017883 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/1973/statm): 174 3 169 147 0 27 0
[pid=1973] 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=1974
New process pid=1975
New process pid=1976
execve syscall for /bin/sed executable
One traced child (pid=1975) 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=1976) exited with status: 0
One traced child (pid=1974) exited with status: 0
New process pid=1977
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-chnl50_51_pb.cnf.cr.opb

[startup+10.0048 s]
Raw data (loadavg): 0.93 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 3112 0 2 0 948 13 0 0 25 0 1 0 1783017888 13193216 3097 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 3221 3097 145 145 0 3076 0
[pid=1977] vsize: 12884
Current children cumulated CPU time (s) 9.62
Current children cumulated vsize (Kb) 15008

[startup+20.0066 s]
Raw data (loadavg): 0.94 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 4854 0 2 0 1922 25 0 0 25 0 1 0 1783017888 20348928 4839 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 4968 4839 145 145 0 4823 0
[pid=1977] vsize: 19872
Current children cumulated CPU time (s) 19.48
Current children cumulated vsize (Kb) 21996

[startup+30.0095 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 6469 0 2 0 2901 34 0 0 25 0 1 0 1783017888 26943488 6454 4294967295 134512640 135094434 3221224432 3221223024 134557244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 6578 6454 145 145 0 6433 0
[pid=1977] vsize: 26312
Current children cumulated CPU time (s) 29.36
Current children cumulated vsize (Kb) 28436

[startup+40.0113 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 8159 0 2 0 3878 43 0 0 25 0 1 0 1783017888 33857536 8144 4294967295 134512640 135094434 3221224432 3221223024 134556978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 8266 8144 145 145 0 8121 0
[pid=1977] vsize: 33064
Current children cumulated CPU time (s) 39.22
Current children cumulated vsize (Kb) 35188

[startup+50.0121 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 9633 0 2 0 4858 52 0 0 25 0 1 0 1783017888 39948288 9618 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 9753 9618 145 145 0 9608 0
[pid=1977] vsize: 39012
Current children cumulated CPU time (s) 49.11
Current children cumulated vsize (Kb) 41136

[startup+60.0119 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 10849 0 2 0 5840 59 0 0 25 0 1 0 1783017888 44924928 10834 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 10968 10834 145 145 0 10823 0
[pid=1977] vsize: 43872
Current children cumulated CPU time (s) 59
Current children cumulated vsize (Kb) 45996

[startup+70.0127 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 12077 0 2 0 6823 66 0 0 25 0 1 0 1783017888 49963008 12062 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 12198 12062 145 145 0 12053 0
[pid=1977] vsize: 48792
Current children cumulated CPU time (s) 68.9
Current children cumulated vsize (Kb) 50916

[startup+80.0136 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 13030 0 2 0 7808 73 0 0 25 0 1 0 1783017888 53874688 13015 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 13153 13015 145 145 0 13008 0
[pid=1977] vsize: 52612
Current children cumulated CPU time (s) 78.82
Current children cumulated vsize (Kb) 54736

[startup+90.0144 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 14276 0 2 0 8790 81 0 0 25 0 1 0 1783017888 58970112 14261 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 14397 14261 145 145 0 14252 0
[pid=1977] vsize: 57588
Current children cumulated CPU time (s) 88.72
Current children cumulated vsize (Kb) 59712

[startup+100.015 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 15419 0 2 0 9773 88 0 0 25 0 1 0 1783017888 63651840 15404 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 15540 15404 145 145 0 15395 0
[pid=1977] vsize: 62160
Current children cumulated CPU time (s) 98.62
Current children cumulated vsize (Kb) 64284

[startup+110.016 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16048 0 2 0 10765 90 0 0 25 0 1 0 1783017888 66240512 16033 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16033 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 108.56
Current children cumulated vsize (Kb) 66812

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 11765 90 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 118.56
Current children cumulated vsize (Kb) 66812

[startup+130.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 12765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 128.57
Current children cumulated vsize (Kb) 66812

[startup+140.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 13764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 138.56
Current children cumulated vsize (Kb) 66812

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 14764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 148.56
Current children cumulated vsize (Kb) 66812

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 15764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 158.56
Current children cumulated vsize (Kb) 66812

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 16764 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 168.56
Current children cumulated vsize (Kb) 66812

[startup+180.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 17765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134557185 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 178.57
Current children cumulated vsize (Kb) 66812

[startup+190.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 18765 91 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 188.57
Current children cumulated vsize (Kb) 66812

[startup+200.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16051 0 2 0 19765 92 0 0 25 0 1 0 1783017888 66240512 16036 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16172 16036 145 145 0 16027 0
[pid=1977] vsize: 64688
Current children cumulated CPU time (s) 198.58
Current children cumulated vsize (Kb) 66812

[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16137 0 2 0 20763 92 0 0 25 0 1 0 1783017888 66592768 16122 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 16258 16122 145 145 0 16113 0
[pid=1977] vsize: 65032
Current children cumulated CPU time (s) 208.56
Current children cumulated vsize (Kb) 67156

[startup+220.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 16835 0 2 0 21753 96 0 0 25 0 1 0 1783017888 69472256 16820 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 16961 16820 145 145 0 16816 0
[pid=1977] vsize: 67844
Current children cumulated CPU time (s) 218.5
Current children cumulated vsize (Kb) 69968

[startup+230.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 17349 0 2 0 22744 100 0 0 25 0 1 0 1783017888 71639040 17334 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 17490 17334 145 145 0 17345 0
[pid=1977] vsize: 69960
Current children cumulated CPU time (s) 228.45
Current children cumulated vsize (Kb) 72084

[startup+240.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 17848 0 2 0 23736 104 0 0 25 0 1 0 1783017888 73711616 17833 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 17996 17833 145 145 0 17851 0
[pid=1977] vsize: 71984
Current children cumulated CPU time (s) 238.41
Current children cumulated vsize (Kb) 74108

[startup+250.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 18418 0 2 0 24727 108 0 0 25 0 1 0 1783017888 76070912 18403 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 18572 18403 145 145 0 18427 0
[pid=1977] vsize: 74288
Current children cumulated CPU time (s) 248.36
Current children cumulated vsize (Kb) 76412

[startup+260.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 19154 0 2 0 25715 113 0 0 25 0 1 0 1783017888 79085568 19139 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 19308 19139 145 145 0 19163 0
[pid=1977] vsize: 77232
Current children cumulated CPU time (s) 258.29
Current children cumulated vsize (Kb) 79356

[startup+270.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 19672 0 2 0 26707 116 0 0 25 0 1 0 1783017888 81387520 19657 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 19870 19657 145 145 0 19725 0
[pid=1977] vsize: 79480
Current children cumulated CPU time (s) 268.24
Current children cumulated vsize (Kb) 81604

[startup+280.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20186 0 2 0 27699 119 0 0 25 0 1 0 1783017888 83480576 20171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20381 20171 145 145 0 20236 0
[pid=1977] vsize: 81524
Current children cumulated CPU time (s) 278.19
Current children cumulated vsize (Kb) 83648

[startup+290.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20657 0 2 0 28691 123 0 0 25 0 1 0 1783017888 85405696 20642 4294967295 134512640 135094434 3221224432 3221223024 134557357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20851 20642 145 145 0 20706 0
[pid=1977] vsize: 83404
Current children cumulated CPU time (s) 288.15
Current children cumulated vsize (Kb) 85528

[startup+300.034 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 29689 124 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 298.14
Current children cumulated vsize (Kb) 85804

[startup+310.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 30689 124 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 308.14
Current children cumulated vsize (Kb) 85804

[startup+320.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 31689 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 318.15
Current children cumulated vsize (Kb) 85804

[startup+330.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 32688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 328.14
Current children cumulated vsize (Kb) 85804

[startup+340.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 33688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 338.14
Current children cumulated vsize (Kb) 85804

[startup+350.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 34688 125 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 348.14
Current children cumulated vsize (Kb) 85804

[startup+360.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 35687 126 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 358.14
Current children cumulated vsize (Kb) 85804

[startup+370.04 s]
Raw data (loadavg): 1.07 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 20728 0 2 0 36687 126 0 0 25 0 1 0 1783017888 85688320 20713 4294967295 134512640 135094434 3221224432 3221223024 134551922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 20920 20713 145 145 0 20775 0
[pid=1977] vsize: 83680
Current children cumulated CPU time (s) 368.14
Current children cumulated vsize (Kb) 85804

[startup+380.041 s]
Raw data (loadavg): 1.14 1.02 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 21000 0 2 0 37683 127 0 0 25 0 1 0 1783017888 86802432 20985 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 21192 20985 145 145 0 21047 0
[pid=1977] vsize: 84768
Current children cumulated CPU time (s) 378.11
Current children cumulated vsize (Kb) 86892

[startup+390.043 s]
Raw data (loadavg): 1.11 1.02 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 22079 0 2 0 38667 135 0 0 25 0 1 0 1783017888 91262976 22064 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 22281 22064 145 145 0 22136 0
[pid=1977] vsize: 89124
Current children cumulated CPU time (s) 388.03
Current children cumulated vsize (Kb) 91248

[startup+400.044 s]
Raw data (loadavg): 1.10 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 23255 0 2 0 39651 140 0 0 25 0 1 0 1783017888 96088064 23240 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 23459 23240 145 145 0 23314 0
[pid=1977] vsize: 93836
Current children cumulated CPU time (s) 397.92
Current children cumulated vsize (Kb) 95960

[startup+410.045 s]
Raw data (loadavg): 1.08 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 24271 0 2 0 40635 146 0 0 25 0 1 0 1783017888 100274176 24256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 24481 24256 145 145 0 24336 0
[pid=1977] vsize: 97924
Current children cumulated CPU time (s) 407.82
Current children cumulated vsize (Kb) 100048

[startup+420.046 s]
Raw data (loadavg): 1.07 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 25301 0 2 0 41620 153 0 0 25 0 1 0 1783017888 104517632 25286 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 25517 25286 145 145 0 25372 0
[pid=1977] vsize: 102068
Current children cumulated CPU time (s) 417.74
Current children cumulated vsize (Kb) 104192

[startup+430.047 s]
Raw data (loadavg): 1.06 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 26155 0 2 0 42607 158 0 0 25 0 1 0 1783017888 108044288 26140 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 26378 26140 145 145 0 26233 0
[pid=1977] vsize: 105512
Current children cumulated CPU time (s) 427.66
Current children cumulated vsize (Kb) 107636

[startup+440.049 s]
Raw data (loadavg): 1.05 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 27219 0 2 0 43590 167 0 0 25 0 1 0 1783017888 112406528 27204 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 27443 27204 145 145 0 27298 0
[pid=1977] vsize: 109772
Current children cumulated CPU time (s) 437.58
Current children cumulated vsize (Kb) 111896

[startup+450.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28143 0 2 0 44576 172 0 0 25 0 1 0 1783017888 116191232 28128 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28367 28128 145 145 0 28222 0
[pid=1977] vsize: 113468
Current children cumulated CPU time (s) 447.49
Current children cumulated vsize (Kb) 115592

[startup+460.051 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28771 0 2 0 45565 176 0 0 25 0 1 0 1783017888 118767616 28756 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28756 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 457.42
Current children cumulated vsize (Kb) 118108

[startup+470.052 s]
Raw data (loadavg): 1.03 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28772 0 2 0 46565 176 0 0 25 0 1 0 1783017888 118767616 28757 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28757 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 467.42
Current children cumulated vsize (Kb) 118108

[startup+480.052 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 47565 176 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 477.42
Current children cumulated vsize (Kb) 118108

[startup+490.054 s]
Raw data (loadavg): 1.02 1.01 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 48565 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 487.43
Current children cumulated vsize (Kb) 118108

[startup+500.055 s]
Raw data (loadavg): 1.02 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 49564 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 497.42
Current children cumulated vsize (Kb) 118108

[startup+510.056 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 50564 177 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 507.42
Current children cumulated vsize (Kb) 118108

[startup+520.057 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 51564 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 517.43
Current children cumulated vsize (Kb) 118108

[startup+530.058 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 52563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 527.42
Current children cumulated vsize (Kb) 118108

[startup+540.059 s]
Raw data (loadavg): 1.01 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 53563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 537.42
Current children cumulated vsize (Kb) 118108

[startup+550.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 54563 178 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 547.42
Current children cumulated vsize (Kb) 118108

[startup+560.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 55562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 557.42
Current children cumulated vsize (Kb) 118108

[startup+570.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 56562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 567.42
Current children cumulated vsize (Kb) 118108

[startup+580.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 57562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 577.42
Current children cumulated vsize (Kb) 118108

[startup+590.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 58562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 587.42
Current children cumulated vsize (Kb) 118108

[startup+600.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 59562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 597.42
Current children cumulated vsize (Kb) 118108

[startup+610.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 60562 179 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 607.42
Current children cumulated vsize (Kb) 118108

[startup+620.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 28773 0 2 0 61561 180 0 0 25 0 1 0 1783017888 118767616 28758 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 28996 28758 145 145 0 28851 0
[pid=1977] vsize: 115984
Current children cumulated CPU time (s) 617.42
Current children cumulated vsize (Kb) 118108

[startup+630.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29029 0 2 0 62556 182 0 0 25 0 1 0 1783017888 119816192 29014 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 29252 29014 145 145 0 29107 0
[pid=1977] vsize: 117008
Current children cumulated CPU time (s) 627.39
Current children cumulated vsize (Kb) 119132

[startup+640.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29434 0 2 0 63550 185 0 0 25 0 1 0 1783017888 121475072 29419 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29419 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 637.36
Current children cumulated vsize (Kb) 120752

[startup+650.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29434 0 2 0 64550 186 0 0 25 0 1 0 1783017888 121475072 29419 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29419 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 647.37
Current children cumulated vsize (Kb) 120752

[startup+660.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 65550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 657.37
Current children cumulated vsize (Kb) 120752

[startup+670.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 66550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 667.37
Current children cumulated vsize (Kb) 120752

[startup+680.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 67550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 677.37
Current children cumulated vsize (Kb) 120752

[startup+690.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 68550 186 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 687.37
Current children cumulated vsize (Kb) 120752

[startup+700.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 69550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 697.38
Current children cumulated vsize (Kb) 120752

[startup+710.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 70550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 707.38
Current children cumulated vsize (Kb) 120752

[startup+720.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 71550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 717.38
Current children cumulated vsize (Kb) 120752

[startup+730.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 72549 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 727.37
Current children cumulated vsize (Kb) 120752

[startup+740.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 73550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 737.38
Current children cumulated vsize (Kb) 120752

[startup+750.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 74550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 747.38
Current children cumulated vsize (Kb) 120752

[startup+760.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 29435 0 2 0 75550 187 0 0 25 0 1 0 1783017888 121475072 29420 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 29657 29420 145 145 0 29512 0
[pid=1977] vsize: 118628
Current children cumulated CPU time (s) 757.38
Current children cumulated vsize (Kb) 120752

[startup+770.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 30207 0 2 0 76540 192 0 0 25 0 1 0 1783017888 124657664 30192 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 30434 30192 145 145 0 30289 0
[pid=1977] vsize: 121736
Current children cumulated CPU time (s) 767.33
Current children cumulated vsize (Kb) 123860

[startup+780.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 31112 0 2 0 77526 198 0 0 25 0 1 0 1783017888 128368640 31097 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 31340 31097 145 145 0 31195 0
[pid=1977] vsize: 125360
Current children cumulated CPU time (s) 777.25
Current children cumulated vsize (Kb) 127484

[startup+790.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) T 1973 1973 31778 0 -1 0 32021 0 2 0 78513 204 0 0 25 0 1 0 1783017888 132087808 32006 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/1977/statm): 32248 32006 145 145 0 32103 0
[pid=1977] vsize: 128992
Current children cumulated CPU time (s) 787.18
Current children cumulated vsize (Kb) 131116

[startup+800.082 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 32803 0 2 0 79502 209 0 0 25 0 1 0 1783017888 135360512 32788 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 33047 32788 145 145 0 32902 0
[pid=1977] vsize: 132188
Current children cumulated CPU time (s) 797.12
Current children cumulated vsize (Kb) 134312

[startup+810.082 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 33575 0 2 0 80492 213 0 0 22 0 1 0 1783017888 138616832 33560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 33842 33560 145 145 0 33697 0
[pid=1977] vsize: 135368
Current children cumulated CPU time (s) 807.06
Current children cumulated vsize (Kb) 137492

[startup+820.083 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34346 0 2 0 81480 218 0 0 25 0 1 0 1783017888 141791232 34331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 34617 34331 145 145 0 34472 0
[pid=1977] vsize: 138468
Current children cumulated CPU time (s) 816.99
Current children cumulated vsize (Kb) 140592

[startup+830.084 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34924 0 2 0 82472 221 0 0 25 0 1 0 1783017888 144224256 34909 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34909 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 826.94
Current children cumulated vsize (Kb) 142968

[startup+840.086 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34926 0 2 0 83472 222 0 0 25 0 1 0 1783017888 144224256 34911 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34911 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 836.95
Current children cumulated vsize (Kb) 142968

[startup+850.087 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34926 0 2 0 84471 222 0 0 25 0 1 0 1783017888 144224256 34911 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34911 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 846.94
Current children cumulated vsize (Kb) 142968

[startup+860.088 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34927 0 2 0 85471 222 0 0 25 0 1 0 1783017888 144224256 34912 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34912 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 856.94
Current children cumulated vsize (Kb) 142968

[startup+870.089 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34927 0 2 0 86470 223 0 0 25 0 1 0 1783017888 144224256 34912 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34912 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 866.94
Current children cumulated vsize (Kb) 142968

[startup+880.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34932 0 2 0 87470 223 0 0 25 0 1 0 1783017888 144224256 34917 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34917 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 876.94
Current children cumulated vsize (Kb) 142968

[startup+890.092 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34934 0 2 0 88470 223 0 0 25 0 1 0 1783017888 144224256 34919 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34919 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 886.94
Current children cumulated vsize (Kb) 142968

[startup+900.094 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 89469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 896.94
Current children cumulated vsize (Kb) 142968

[startup+910.095 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 90469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 906.94
Current children cumulated vsize (Kb) 142968

[startup+920.097 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34935 0 2 0 91469 224 0 0 25 0 1 0 1783017888 144224256 34920 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34920 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 916.94
Current children cumulated vsize (Kb) 142968

[startup+930.097 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34939 0 2 0 92468 224 0 0 25 0 1 0 1783017888 144224256 34924 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34924 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 926.93
Current children cumulated vsize (Kb) 142968

[startup+940.099 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34939 0 2 0 93468 225 0 0 25 0 1 0 1783017888 144224256 34924 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1977/statm): 35211 34924 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 936.94
Current children cumulated vsize (Kb) 142968

[startup+950.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34942 0 2 0 94468 225 0 0 25 0 1 0 1783017888 144224256 34927 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34927 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 946.94
Current children cumulated vsize (Kb) 142968

[startup+960.101 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34942 0 2 0 95468 225 0 0 25 0 1 0 1783017888 144224256 34927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34927 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 956.94
Current children cumulated vsize (Kb) 142968

[startup+970.103 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34946 0 2 0 96469 225 0 0 25 0 1 0 1783017888 144224256 34931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34931 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 966.95
Current children cumulated vsize (Kb) 142968

[startup+980.103 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34949 0 2 0 97469 225 0 0 25 0 1 0 1783017888 144224256 34934 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34934 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 976.95
Current children cumulated vsize (Kb) 142968

[startup+990.104 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34955 0 2 0 98469 225 0 0 25 0 1 0 1783017888 144224256 34940 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34940 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 986.95
Current children cumulated vsize (Kb) 142968

[startup+1000.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34955 0 2 0 99469 225 0 0 25 0 1 0 1783017888 144224256 34940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34940 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 996.95
Current children cumulated vsize (Kb) 142968

[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34956 0 2 0 100470 225 0 0 25 0 1 0 1783017888 144224256 34941 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34941 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1006.96
Current children cumulated vsize (Kb) 142968

[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 101470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1016.96
Current children cumulated vsize (Kb) 142968

[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 102470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1026.96
Current children cumulated vsize (Kb) 142968

[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 103470 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1036.96
Current children cumulated vsize (Kb) 142968

[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34961 0 2 0 104471 225 0 0 25 0 1 0 1783017888 144224256 34946 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34946 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1046.97
Current children cumulated vsize (Kb) 142968

[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 105471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1056.97
Current children cumulated vsize (Kb) 142968

[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 106471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1066.97
Current children cumulated vsize (Kb) 142968

[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 107471 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1076.97
Current children cumulated vsize (Kb) 142968

[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 108472 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1086.98
Current children cumulated vsize (Kb) 142968

[startup+1100.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34962 0 2 0 109472 225 0 0 25 0 1 0 1783017888 144224256 34947 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34947 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1096.98
Current children cumulated vsize (Kb) 142968

[startup+1110.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34969 0 2 0 110472 225 0 0 25 0 1 0 1783017888 144224256 34954 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34954 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1106.98
Current children cumulated vsize (Kb) 142968

[startup+1120.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34969 0 2 0 111472 225 0 0 25 0 1 0 1783017888 144224256 34954 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34954 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1116.98
Current children cumulated vsize (Kb) 142968

[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34971 0 2 0 112472 225 0 0 25 0 1 0 1783017888 144224256 34956 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34956 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1126.98
Current children cumulated vsize (Kb) 142968

[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34971 0 2 0 113473 225 0 0 25 0 1 0 1783017888 144224256 34956 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34956 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1136.99
Current children cumulated vsize (Kb) 142968

[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 114473 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1146.99
Current children cumulated vsize (Kb) 142968

[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 115473 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1156.99
Current children cumulated vsize (Kb) 142968

[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 116474 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1167
Current children cumulated vsize (Kb) 142968

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 117474 225 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1177
Current children cumulated vsize (Kb) 142968

[startup+1190.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 118474 226 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1187.01
Current children cumulated vsize (Kb) 142968

[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34972 0 2 0 119474 226 0 0 25 0 1 0 1783017888 144224256 34957 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34957 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1197.01
Current children cumulated vsize (Kb) 142968

[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34973 0 2 0 120474 226 0 0 25 0 1 0 1783017888 144224256 34958 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34958 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1207.01
Current children cumulated vsize (Kb) 142968



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/57 1977
Raw data (/proc/1973/stat): 1973 (minisat+_script) S 1972 1973 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783017883 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1973/statm): 531 226 485 147 0 384 0
[pid=1973] vsize: 2124
Raw data (/proc/1977/stat): 1977 (minisat+_64-bit) R 1973 1973 31778 0 -1 0 34973 0 2 0 120474 226 0 0 25 0 1 0 1783017888 144224256 34958 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1977/statm): 35211 34958 145 145 0 35066 0
[pid=1977] vsize: 140844
Current children cumulated CPU time (s) 1207.01
Current children cumulated vsize (Kb) 142968

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

Child status: 0
Real time (s): 1210.2
CPU time (s): 1207.08
CPU user time (s): 1204.75
CPU system time (s): 2.32765
CPU usage (%): 99.7422
Max. virtual memory (cumulated for all children) (Kb): 142968

Verifier Data

ERROR: no interpretation found !