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-fpga45_43_sat_pb.cnf.cr.opb
MD5SUMf711bed5ebfe5c735a8c12d953afb97c
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
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 46
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark9.07862
Number of variables2903
Total number of constraints2066
Number of constraints which are clauses1978
Number of constraints which are cardinality constraints (but not clauses)88
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint22
Maximum length of a constraint45

Trace number 897

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        955448 kB
Buffers:         33012 kB
Cached:          18312 kB
SwapCached:        696 kB
Active:          48876 kB
Inactive:         4976 kB
HighTotal:      131008 kB
HighFree:       109116 kB
LowTotal:       903652 kB
LowFree:        846332 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            19880 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:56:42 (client local time) WITH STATUS 0 IN 1207.83 SECONDS
stats: 2394 7 1207.83 0

Solver Data

c Parsing PB file...
c Converting 2066 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  87]---> BDD-cost:   83
c ---[  86]---> BDD-cost:   83
c ---[  85]---> BDD-cost:   83
c ---[  84]---> BDD-cost:   83
c ---[  83]---> BDD-cost:   83
c ---[  82]---> BDD-cost:   83
c ---[  81]---> BDD-cost:   83
c ---[  80]---> BDD-cost:   83
c ---[  79]---> BDD-cost:   83
c ---[  78]---> BDD-cost:   83
c ---[  77]---> BDD-cost:   83
c ---[  76]---> BDD-cost:   83
c ---[  75]---> BDD-cost:   83
c ---[  74]---> BDD-cost:   83
c ---[  73]---> BDD-cost:   83
c ---[  72]---> BDD-cost:   83
c ---[  71]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   83
c ---[  69]---> BDD-cost:   83
c ---[  68]---> BDD-cost:   83
c ---[  67]---> BDD-cost:   83
c ---[  66]---> BDD-cost:   83
c ---[  65]---> BDD-cost:   83
c ---[  64]---> BDD-cost:   83
c ---[  63]---> BDD-cost:   83
c ---[  62]---> BDD-cost:   83
c ---[  61]---> BDD-cost:   83
c ---[  60]---> BDD-cost:   83
c ---[  59]---> BDD-cost:   83
c ---[  58]---> BDD-cost:   83
c ---[  57]---> BDD-cost:   83
c ---[  56]---> BDD-cost:   83
c ---[  55]---> BDD-cost:   83
c ---[  54]---> BDD-cost:   83
c ---[  53]---> BDD-cost:   83
c ---[  52]---> BDD-cost:   83
c ---[  51]---> BDD-cost:   83
c ---[  50]---> BDD-cost:   83
c ---[  49]---> BDD-cost:   83
c ---[  48]---> BDD-cost:   83
c ---[  47]---> BDD-cost:   83
c ---[  46]---> BDD-cost:   83
c ---[  45]---> BDD-cost:   83
c ---[  44]---> BDD-cost:   83
c ---[  43]---> BDD-cost:   83
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15701    81209 |    5233       0        0     nan |  0.000 % |
c |       101 |   15701    81209 |    5756     101    30091   297.9 |  1.042 % |
c |       251 |   15701    81209 |    6331     251    41172   164.0 |  1.042 % |
c |       477 |   15701    81209 |    6965     477   101249   212.3 |  1.042 % |
c |       816 |   15701    81209 |    7661     816   188784   231.4 |  1.042 % |
c |      1325 |   15701    81209 |    8427    1325   316955   239.2 |  1.042 % |
c |      2087 |   15701    81209 |    9270    2087   521561   249.9 |  1.042 % |
c |      3226 |   15701    81209 |   10197    3226   715932   221.9 |  1.042 % |
c |      4935 |   15701    81209 |   11217    4935  1355039   274.6 |  1.042 % |
c |      7498 |   15701    81209 |   12339    7498  2284715   304.7 |  1.042 % |
c |     11345 |   15701    81209 |   13573   11345  2854773   251.6 |  1.042 % |
c |     17112 |   15701    81209 |   14930   17112  5134950   300.1 |  1.042 % |
c |     25763 |   15701    81209 |   16423   17207  7147483   415.4 |  1.042 % |
c |     38737 |   15701    81209 |   18065   21578  6296769   291.8 |  1.042 % |
c |     58198 |   15701    81209 |   19872   18140 10242933   564.7 |  1.042 % |
c |     87390 |   15701    81209 |   21859   20249  6518874   321.9 |  1.042 % |
c |    131181 |   15701    81209 |   24045   16308  6553087   401.8 |  1.042 % |
c |    196872 |   15701    81209 |   26450   15779  9705190   615.1 |  1.042 % |

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/30051/stat): 30051 (minisat+_script) R 30050 30051 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841315267 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/30051/statm): 174 3 169 147 0 27 0
[pid=30051] 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=30052
New process pid=30053
New process pid=30054
execve syscall for /bin/sed executable
One traced child (pid=30053) 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=30054) exited with status: 0
One traced child (pid=30052) exited with status: 0
New process pid=30055
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-fpga45_43_sat_pb.cnf.cr.opb

[startup+10.005 s]
Raw data (loadavg): 0.94 1.02 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 2857 0 3 0 948 14 0 0 25 0 1 0 1841315272 12181504 2846 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 2974 2846 145 145 0 2829 0
[pid=30055] vsize: 11896
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 14020

[startup+20.0068 s]
Raw data (loadavg): 0.95 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 4715 0 3 0 1923 24 0 0 25 0 1 0 1841315272 19800064 4704 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 4834 4704 145 145 0 4689 0
[pid=30055] vsize: 19336
Current children cumulated CPU time (s) 19.49
Current children cumulated vsize (Kb) 21460

[startup+30.0075 s]
Raw data (loadavg): 0.96 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 5971 0 3 0 2904 33 0 0 25 0 1 0 1841315272 24948736 5960 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 6091 5960 145 145 0 5946 0
[pid=30055] vsize: 24364
Current children cumulated CPU time (s) 29.39
Current children cumulated vsize (Kb) 26488

[startup+40.0072 s]
Raw data (loadavg): 0.96 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 6373 0 3 0 3898 35 0 0 25 0 1 0 1841315272 26669056 6362 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 6511 6362 145 145 0 6366 0
[pid=30055] vsize: 26044
Current children cumulated CPU time (s) 39.35
Current children cumulated vsize (Kb) 28168

[startup+50.0089 s]
Raw data (loadavg): 0.97 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 6712 0 3 0 4892 37 0 0 25 0 1 0 1841315272 28061696 6701 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 6851 6701 145 145 0 6706 0
[pid=30055] vsize: 27404
Current children cumulated CPU time (s) 49.31
Current children cumulated vsize (Kb) 29528

[startup+60.0097 s]
Raw data (loadavg): 0.97 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 7559 0 3 0 5880 42 0 0 25 0 1 0 1841315272 31551488 7548 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 7703 7548 145 145 0 7558 0
[pid=30055] vsize: 30812
Current children cumulated CPU time (s) 59.24
Current children cumulated vsize (Kb) 32936

[startup+70.0114 s]
Raw data (loadavg): 0.98 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8473 0 3 0 6865 49 0 0 25 0 1 0 1841315272 35307520 8462 4294967295 134512640 135094434 3221224432 3221223024 134557253 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 8620 8462 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 69.16
Current children cumulated vsize (Kb) 36604

[startup+80.0131 s]
Raw data (loadavg): 0.98 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8474 0 3 0 7864 49 0 0 25 0 1 0 1841315272 35307520 8463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 8620 8463 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 79.15
Current children cumulated vsize (Kb) 36604

[startup+90.0139 s]
Raw data (loadavg): 0.98 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8478 0 3 0 8864 50 0 0 25 0 1 0 1841315272 35307520 8467 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 8620 8467 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 89.16
Current children cumulated vsize (Kb) 36604

[startup+100.015 s]
Raw data (loadavg): 0.98 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8478 0 3 0 9864 50 0 0 25 0 1 0 1841315272 35307520 8467 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 8620 8467 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 99.16
Current children cumulated vsize (Kb) 36604

[startup+110.015 s]
Raw data (loadavg): 0.99 1.01 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8478 0 3 0 10862 51 0 0 25 0 1 0 1841315272 35307520 8467 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 8620 8467 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 109.15
Current children cumulated vsize (Kb) 36604

[startup+120.017 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 8478 0 3 0 11863 51 0 0 25 0 1 0 1841315272 35307520 8467 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 8620 8467 145 145 0 8475 0
[pid=30055] vsize: 34480
Current children cumulated CPU time (s) 119.16
Current children cumulated vsize (Kb) 36604

[startup+130.018 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 9394 0 3 0 12849 55 0 0 25 0 1 0 1841315272 39084032 9383 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 9542 9383 145 145 0 9397 0
[pid=30055] vsize: 38168
Current children cumulated CPU time (s) 129.06
Current children cumulated vsize (Kb) 40292

[startup+140.017 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 10471 0 3 0 13831 64 0 0 25 0 1 0 1841315272 43495424 10460 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 10619 10460 145 145 0 10474 0
[pid=30055] vsize: 42476
Current children cumulated CPU time (s) 138.97
Current children cumulated vsize (Kb) 44600

[startup+150.018 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 10471 0 3 0 14830 65 0 0 25 0 1 0 1841315272 43495424 10460 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 10619 10460 145 145 0 10474 0
[pid=30055] vsize: 42476
Current children cumulated CPU time (s) 148.97
Current children cumulated vsize (Kb) 44600

[startup+160.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 10471 0 3 0 15830 65 0 0 25 0 1 0 1841315272 43495424 10460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 10619 10460 145 145 0 10474 0
[pid=30055] vsize: 42476
Current children cumulated CPU time (s) 158.97
Current children cumulated vsize (Kb) 44600

[startup+170.02 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 11106 0 3 0 16820 69 0 0 25 0 1 0 1841315272 46096384 11095 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 11254 11095 145 145 0 11109 0
[pid=30055] vsize: 45016
Current children cumulated CPU time (s) 168.91
Current children cumulated vsize (Kb) 47140

[startup+180.02 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 12253 0 3 0 17804 75 0 0 25 0 1 0 1841315272 50831360 12242 4294967295 134512640 135094434 3221224432 3221222976 134562133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 12410 12242 145 145 0 12265 0
[pid=30055] vsize: 49640
Current children cumulated CPU time (s) 178.81
Current children cumulated vsize (Kb) 51764

[startup+190.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13981 0 3 0 18781 85 0 0 25 0 1 0 1841315272 57905152 13970 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13970 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 188.68
Current children cumulated vsize (Kb) 58672

[startup+200.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13981 0 3 0 19781 85 0 0 25 0 1 0 1841315272 57905152 13970 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13970 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 198.68
Current children cumulated vsize (Kb) 58672

[startup+210.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13982 0 3 0 20781 85 0 0 25 0 1 0 1841315272 57905152 13971 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13971 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 208.68
Current children cumulated vsize (Kb) 58672

[startup+220.024 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13982 0 3 0 21781 85 0 0 25 0 1 0 1841315272 57905152 13971 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13971 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 218.68
Current children cumulated vsize (Kb) 58672

[startup+230.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13982 0 3 0 22782 85 0 0 25 0 1 0 1841315272 57905152 13971 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13971 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 228.69
Current children cumulated vsize (Kb) 58672

[startup+240.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13982 0 3 0 23782 85 0 0 25 0 1 0 1841315272 57905152 13971 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13971 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 238.69
Current children cumulated vsize (Kb) 58672

[startup+250.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13982 0 3 0 24782 86 0 0 25 0 1 0 1841315272 57905152 13971 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13971 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 248.7
Current children cumulated vsize (Kb) 58672

[startup+260.027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 25782 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 258.7
Current children cumulated vsize (Kb) 58672

[startup+270.028 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 26782 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 268.7
Current children cumulated vsize (Kb) 58672

[startup+280.028 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 27782 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 278.7
Current children cumulated vsize (Kb) 58672

[startup+290.029 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 28782 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 288.7
Current children cumulated vsize (Kb) 58672

[startup+300.03 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 29783 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 298.71
Current children cumulated vsize (Kb) 58672

[startup+310.03 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 30783 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 308.71
Current children cumulated vsize (Kb) 58672

[startup+320.031 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 31783 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 318.71
Current children cumulated vsize (Kb) 58672

[startup+330.032 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 32783 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 328.71
Current children cumulated vsize (Kb) 58672

[startup+340.032 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 33783 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 338.71
Current children cumulated vsize (Kb) 58672

[startup+350.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 34784 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 348.72
Current children cumulated vsize (Kb) 58672

[startup+360.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 35784 86 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 358.72
Current children cumulated vsize (Kb) 58672

[startup+370.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 36784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 368.73
Current children cumulated vsize (Kb) 58672

[startup+380.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 37784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 378.73
Current children cumulated vsize (Kb) 58672

[startup+390.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 38784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 388.73
Current children cumulated vsize (Kb) 58672

[startup+400.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 39784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 398.73
Current children cumulated vsize (Kb) 58672

[startup+410.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 40784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 58672

[startup+420.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 41784 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 58672

[startup+430.041 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 13984 0 3 0 42785 87 0 0 25 0 1 0 1841315272 57905152 13973 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14137 13973 145 145 0 13992 0
[pid=30055] vsize: 56548
Current children cumulated CPU time (s) 428.74
Current children cumulated vsize (Kb) 58672

[startup+440.041 s]
Raw data (loadavg): 0.99 1.00 0.96 1/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) T 30051 30051 20115 0 -1 0 14791 0 3 0 43775 91 0 0 25 0 1 0 1841315272 61210624 14780 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/30055/statm): 14944 14780 145 145 0 14799 0
[pid=30055] vsize: 59776
Current children cumulated CPU time (s) 438.68
Current children cumulated vsize (Kb) 61900

[startup+450.042 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15733 0 3 0 44760 98 0 0 25 0 1 0 1841315272 65069056 15722 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 15886 15722 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 448.6
Current children cumulated vsize (Kb) 65668

[startup+460.043 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15733 0 3 0 45759 98 0 0 25 0 1 0 1841315272 65069056 15722 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15722 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 458.59
Current children cumulated vsize (Kb) 65668

[startup+470.043 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15734 0 3 0 46759 98 0 0 25 0 1 0 1841315272 65069056 15723 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15723 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 468.59
Current children cumulated vsize (Kb) 65668

[startup+480.044 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 47759 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 478.6
Current children cumulated vsize (Kb) 65668

[startup+490.045 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 48759 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 488.6
Current children cumulated vsize (Kb) 65668

[startup+500.046 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 49759 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 498.6
Current children cumulated vsize (Kb) 65668

[startup+510.046 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 50760 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 508.61
Current children cumulated vsize (Kb) 65668

[startup+520.047 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 51760 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 518.61
Current children cumulated vsize (Kb) 65668

[startup+530.048 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 52760 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 528.61
Current children cumulated vsize (Kb) 65668

[startup+540.047 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 15735 0 3 0 53760 99 0 0 25 0 1 0 1841315272 65069056 15724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 15886 15724 145 145 0 15741 0
[pid=30055] vsize: 63544
Current children cumulated CPU time (s) 538.61
Current children cumulated vsize (Kb) 65668

[startup+550.048 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 16255 0 3 0 54751 103 0 0 25 0 1 0 1841315272 67244032 16244 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 16417 16244 145 145 0 16272 0
[pid=30055] vsize: 65668
Current children cumulated CPU time (s) 548.56
Current children cumulated vsize (Kb) 67792

[startup+560.048 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 16789 0 3 0 55742 107 0 0 25 0 1 0 1841315272 69500928 16778 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 16968 16778 145 145 0 16823 0
[pid=30055] vsize: 67872
Current children cumulated CPU time (s) 558.51
Current children cumulated vsize (Kb) 69996

[startup+570.049 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17322 0 3 0 56734 110 0 0 25 0 1 0 1841315272 71704576 17311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17506 17311 145 145 0 17361 0
[pid=30055] vsize: 70024
Current children cumulated CPU time (s) 568.46
Current children cumulated vsize (Kb) 72148

[startup+580.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 57731 111 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 578.44
Current children cumulated vsize (Kb) 73044

[startup+590.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 58732 111 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 588.45
Current children cumulated vsize (Kb) 73044

[startup+600.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 59732 111 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 598.45
Current children cumulated vsize (Kb) 73044

[startup+610.051 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 60732 111 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 608.45
Current children cumulated vsize (Kb) 73044

[startup+620.052 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 61732 111 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 618.45
Current children cumulated vsize (Kb) 73044

[startup+630.052 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17543 0 3 0 62732 112 0 0 25 0 1 0 1841315272 72622080 17532 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 17730 17532 145 145 0 17585 0
[pid=30055] vsize: 70920
Current children cumulated CPU time (s) 628.46
Current children cumulated vsize (Kb) 73044

[startup+640.053 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 17893 0 3 0 63728 113 0 0 25 0 1 0 1841315272 74063872 17882 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 18082 17882 145 145 0 17937 0
[pid=30055] vsize: 72328
Current children cumulated CPU time (s) 638.43
Current children cumulated vsize (Kb) 74452

[startup+650.054 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 18333 0 3 0 64723 115 0 0 25 0 1 0 1841315272 75870208 18322 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 18523 18322 145 145 0 18378 0
[pid=30055] vsize: 74092
Current children cumulated CPU time (s) 648.4
Current children cumulated vsize (Kb) 76216

[startup+660.054 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19000 0 3 0 65714 118 0 0 25 0 1 0 1841315272 78626816 18989 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 19196 18989 145 145 0 19051 0
[pid=30055] vsize: 76784
Current children cumulated CPU time (s) 658.34
Current children cumulated vsize (Kb) 78908

[startup+670.056 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19517 0 3 0 66706 121 0 0 25 0 1 0 1841315272 80736256 19506 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 19711 19506 145 145 0 19566 0
[pid=30055] vsize: 78844
Current children cumulated CPU time (s) 668.29
Current children cumulated vsize (Kb) 80968

[startup+680.057 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19887 0 3 0 67699 124 0 0 25 0 1 0 1841315272 82251776 19876 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19876 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 678.25
Current children cumulated vsize (Kb) 82448

[startup+690.056 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19887 0 3 0 68699 124 0 0 25 0 1 0 1841315272 82251776 19876 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19876 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 688.25
Current children cumulated vsize (Kb) 82448

[startup+700.058 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19887 0 3 0 69699 124 0 0 25 0 1 0 1841315272 82251776 19876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19876 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 698.25
Current children cumulated vsize (Kb) 82448

[startup+710.059 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19888 0 3 0 70699 124 0 0 25 0 1 0 1841315272 82251776 19877 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19877 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 708.25
Current children cumulated vsize (Kb) 82448

[startup+720.059 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19888 0 3 0 71700 124 0 0 25 0 1 0 1841315272 82251776 19877 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19877 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 718.26
Current children cumulated vsize (Kb) 82448

[startup+730.061 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19888 0 3 0 72700 124 0 0 25 0 1 0 1841315272 82251776 19877 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19877 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 728.26
Current children cumulated vsize (Kb) 82448

[startup+740.061 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 73699 126 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 738.27
Current children cumulated vsize (Kb) 82448

[startup+750.062 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 74698 126 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 748.26
Current children cumulated vsize (Kb) 82448

[startup+760.062 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 75698 127 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 758.27
Current children cumulated vsize (Kb) 82448

[startup+770.063 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 76698 127 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 768.27
Current children cumulated vsize (Kb) 82448

[startup+780.063 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 77698 128 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 778.28
Current children cumulated vsize (Kb) 82448

[startup+790.064 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 78698 128 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 788.28
Current children cumulated vsize (Kb) 82448

[startup+800.066 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 79698 128 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 798.28
Current children cumulated vsize (Kb) 82448

[startup+810.067 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19889 0 3 0 80699 128 0 0 25 0 1 0 1841315272 82251776 19878 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19878 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 808.29
Current children cumulated vsize (Kb) 82448

[startup+820.067 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 19890 0 3 0 81698 128 0 0 25 0 1 0 1841315272 82251776 19879 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20081 19879 145 145 0 19936 0
[pid=30055] vsize: 80324
Current children cumulated CPU time (s) 818.28
Current children cumulated vsize (Kb) 82448

[startup+830.068 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 20223 0 3 0 82693 131 0 0 25 0 1 0 1841315272 83644416 20212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20421 20212 145 145 0 20276 0
[pid=30055] vsize: 81684
Current children cumulated CPU time (s) 828.26
Current children cumulated vsize (Kb) 83808

[startup+840.068 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 20611 0 3 0 83685 135 0 0 25 0 1 0 1841315272 85229568 20600 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 20808 20600 145 145 0 20663 0
[pid=30055] vsize: 83232
Current children cumulated CPU time (s) 838.22
Current children cumulated vsize (Kb) 85356

[startup+850.068 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21064 0 3 0 84677 138 0 0 25 0 1 0 1841315272 87085056 21053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 21261 21053 145 145 0 21116 0
[pid=30055] vsize: 85044
Current children cumulated CPU time (s) 848.17
Current children cumulated vsize (Kb) 87168

[startup+860.069 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21586 0 3 0 85668 142 0 0 25 0 1 0 1841315272 89223168 21575 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 21783 21575 145 145 0 21638 0
[pid=30055] vsize: 87132
Current children cumulated CPU time (s) 858.12
Current children cumulated vsize (Kb) 89256

[startup+870.07 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 86663 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 868.1
Current children cumulated vsize (Kb) 90664

[startup+880.07 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 87663 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 878.1
Current children cumulated vsize (Kb) 90664

[startup+890.07 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 88662 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 888.09
Current children cumulated vsize (Kb) 90664

[startup+900.071 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 89662 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 898.09
Current children cumulated vsize (Kb) 90664

[startup+910.071 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 90662 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 908.09
Current children cumulated vsize (Kb) 90664

[startup+920.072 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 91662 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223024 134556969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 918.09
Current children cumulated vsize (Kb) 90664

[startup+930.073 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 92663 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 928.1
Current children cumulated vsize (Kb) 90664

[startup+940.073 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21932 0 3 0 93663 145 0 0 25 0 1 0 1841315272 90664960 21921 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21921 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 938.1
Current children cumulated vsize (Kb) 90664

[startup+950.074 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21933 0 3 0 94663 145 0 0 25 0 1 0 1841315272 90664960 21922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21922 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 948.1
Current children cumulated vsize (Kb) 90664

[startup+960.075 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 21934 0 3 0 95663 145 0 0 25 0 1 0 1841315272 90664960 21923 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22135 21923 145 145 0 21990 0
[pid=30055] vsize: 88540
Current children cumulated CPU time (s) 958.1
Current children cumulated vsize (Kb) 90664

[startup+970.076 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22415 0 3 0 96656 149 0 0 25 0 1 0 1841315272 92692480 22404 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 22630 22404 145 145 0 22485 0
[pid=30055] vsize: 90520
Current children cumulated CPU time (s) 968.07
Current children cumulated vsize (Kb) 92644

[startup+980.077 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22875 0 3 0 97648 152 0 0 25 0 1 0 1841315272 94588928 22864 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22864 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 978.02
Current children cumulated vsize (Kb) 94496

[startup+990.077 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22877 0 3 0 98649 152 0 0 25 0 1 0 1841315272 94588928 22866 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22866 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 988.03
Current children cumulated vsize (Kb) 94496

[startup+1000.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22878 0 3 0 99649 152 0 0 25 0 1 0 1841315272 94588928 22867 4294967295 134512640 135094434 3221224432 3221223104 134555837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22867 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 998.03
Current children cumulated vsize (Kb) 94496

[startup+1010.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22878 0 3 0 100649 152 0 0 25 0 1 0 1841315272 94588928 22867 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22867 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1008.03
Current children cumulated vsize (Kb) 94496

[startup+1020.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22878 0 3 0 101649 152 0 0 25 0 1 0 1841315272 94588928 22867 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22867 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1018.03
Current children cumulated vsize (Kb) 94496

[startup+1030.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22879 0 3 0 102649 152 0 0 25 0 1 0 1841315272 94588928 22868 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22868 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1028.03
Current children cumulated vsize (Kb) 94496

[startup+1040.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22880 0 3 0 103649 152 0 0 25 0 1 0 1841315272 94588928 22869 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22869 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1038.03
Current children cumulated vsize (Kb) 94496

[startup+1050.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22880 0 3 0 104650 152 0 0 25 0 1 0 1841315272 94588928 22869 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22869 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1048.04
Current children cumulated vsize (Kb) 94496

[startup+1060.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22881 0 3 0 105650 152 0 0 25 0 1 0 1841315272 94588928 22870 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22870 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1058.04
Current children cumulated vsize (Kb) 94496

[startup+1070.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22883 0 3 0 106650 152 0 0 25 0 1 0 1841315272 94588928 22872 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22872 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1068.04
Current children cumulated vsize (Kb) 94496

[startup+1080.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22883 0 3 0 107650 153 0 0 25 0 1 0 1841315272 94588928 22872 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22872 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1078.05
Current children cumulated vsize (Kb) 94496

[startup+1090.08 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22884 0 3 0 108650 153 0 0 25 0 1 0 1841315272 94588928 22873 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22873 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1088.05
Current children cumulated vsize (Kb) 94496

[startup+1100.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22884 0 3 0 109651 153 0 0 25 0 1 0 1841315272 94588928 22873 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22873 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1098.06
Current children cumulated vsize (Kb) 94496

[startup+1110.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 110651 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1108.06
Current children cumulated vsize (Kb) 94496

[startup+1120.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 111651 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1118.06
Current children cumulated vsize (Kb) 94496

[startup+1130.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 112651 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1128.06
Current children cumulated vsize (Kb) 94496

[startup+1140.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 113652 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1138.07
Current children cumulated vsize (Kb) 94496

[startup+1150.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 114651 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1148.06
Current children cumulated vsize (Kb) 94496

[startup+1160.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 115652 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1158.07
Current children cumulated vsize (Kb) 94496

[startup+1170.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 22885 0 3 0 116652 153 0 0 25 0 1 0 1841315272 94588928 22874 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23093 22874 145 145 0 22948 0
[pid=30055] vsize: 92372
Current children cumulated CPU time (s) 1168.07
Current children cumulated vsize (Kb) 94496

[startup+1180.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 23169 0 3 0 117647 155 0 0 25 0 1 0 1841315272 95752192 23158 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 23377 23158 145 145 0 23232 0
[pid=30055] vsize: 93508
Current children cumulated CPU time (s) 1178.04
Current children cumulated vsize (Kb) 95632

[startup+1190.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 24004 0 3 0 118633 161 0 0 25 0 1 0 1841315272 99172352 23993 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30055/statm): 24212 23993 145 145 0 24067 0
[pid=30055] vsize: 96848
Current children cumulated CPU time (s) 1187.96
Current children cumulated vsize (Kb) 98972

[startup+1200.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 24822 0 3 0 119620 166 0 0 25 0 1 0 1841315272 102522880 24811 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 25030 24811 145 145 0 24885 0
[pid=30055] vsize: 100120
Current children cumulated CPU time (s) 1197.88
Current children cumulated vsize (Kb) 102244

[startup+1210.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 25692 0 3 0 120606 171 0 0 25 0 1 0 1841315272 106086400 25681 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 25900 25681 145 145 0 25755 0
[pid=30055] vsize: 103600
Current children cumulated CPU time (s) 1207.79
Current children cumulated vsize (Kb) 105724



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 1.00 0.96 2/57 30055
Raw data (/proc/30051/stat): 30051 (minisat+_script) S 30050 30051 20115 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841315267 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30051/statm): 531 226 485 147 0 384 0
[pid=30051] vsize: 2124
Raw data (/proc/30055/stat): 30055 (minisat+_64-bit) R 30051 30051 20115 0 -1 0 25692 0 3 0 120606 171 0 0 25 0 1 0 1841315272 106086400 25681 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30055/statm): 25900 25681 145 145 0 25755 0
[pid=30055] vsize: 103600
Current children cumulated CPU time (s) 1207.79
Current children cumulated vsize (Kb) 105724

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.83
CPU user time (s): 1206.06
CPU system time (s): 1.76473
CPU usage (%): 99.8086
Max. virtual memory (cumulated for all children) (Kb): 105724

Verifier Data

ERROR: no interpretation found !