Some explanations

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

General information on the benchmark

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

Trace number 828

Launcher Data

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        944680 kB
Buffers:         34768 kB
Cached:          28216 kB
SwapCached:        868 kB
Active:          53532 kB
Inactive:        12080 kB
HighTotal:      131008 kB
HighFree:       100072 kB
LowTotal:       903652 kB
LowFree:        844608 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            18756 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:48:37 (client local time) WITH STATUS 0 IN 1207.8 SECONDS
stats: 2362 7 1207.8 0

Solver Data

c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> BDD-cost:  107
c ---[  98]---> BDD-cost:  107
c ---[  97]---> BDD-cost:  107
c ---[  96]---> BDD-cost:  107
c ---[  95]---> BDD-cost:  107
c ---[  94]---> BDD-cost:  107
c ---[  93]---> BDD-cost:  107
c ---[  92]---> BDD-cost:  107
c ---[  91]---> BDD-cost:  107
c ---[  90]---> BDD-cost:  107
c ---[  89]---> BDD-cost:  107
c ---[  88]---> BDD-cost:  107
c ---[  87]---> BDD-cost:  107
c ---[  86]---> BDD-cost:  107
c ---[  85]---> BDD-cost:  107
c ---[  84]---> BDD-cost:  107
c ---[  83]---> BDD-cost:  107
c ---[  82]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  107
c ---[  80]---> BDD-cost:  107
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  107
c ---[  76]---> BDD-cost:  107
c ---[  75]---> BDD-cost:  107
c ---[  74]---> BDD-cost:  107
c ---[  73]---> BDD-cost:  107
c ---[  72]---> BDD-cost:  107
c ---[  71]---> BDD-cost:  107
c ---[  70]---> BDD-cost:  107
c ---[  69]---> BDD-cost:  107
c ---[  68]---> BDD-cost:  107
c ---[  67]---> BDD-cost:  107
c ---[  66]---> BDD-cost:  107
c ---[  65]---> BDD-cost:  107
c ---[  64]---> BDD-cost:  107
c ---[  63]---> BDD-cost:  107
c ---[  62]---> BDD-cost:  107
c ---[  61]---> BDD-cost:  107
c ---[  60]---> BDD-cost:  107
c ---[  59]---> BDD-cost:  107
c ---[  58]---> BDD-cost:  107
c ---[  57]---> BDD-cost:  107
c ---[  56]---> BDD-cost:  107
c ---[  55]---> BDD-cost:  107
c ---[  54]---> BDD-cost:  107
c ---[  53]---> BDD-cost:  107
c ---[  52]---> BDD-cost:  107
c ---[  51]---> BDD-cost:  107
c ---[  50]---> BDD-cost:  107
c ---[  49]---> BDD-cost:  107
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  107
c ---[  46]---> BDD-cost:  107
c ---[  45]---> BDD-cost:  107
c ---[  44]---> BDD-cost:  107
c ---[  43]---> BDD-cost:  107
c ---[  42]---> BDD-cost:  107
c ---[  41]---> BDD-cost:  107
c ---[  40]---> BDD-cost:  107
c ---[  39]---> BDD-cost:  107
c ---[  38]---> BDD-cost:  107
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  107
c ---[  35]---> BDD-cost:  107
c ---[  34]---> BDD-cost:  107
c ---[  33]---> BDD-cost:  107
c ---[  32]---> BDD-cost:  107
c ---[  31]---> BDD-cost:  107
c ---[  30]---> BDD-cost:  107
c ---[  29]---> BDD-cost:  107
c ---[  28]---> BDD-cost:  107
c ---[  27]---> BDD-cost:  107
c ---[  26]---> BDD-cost:  107
c ---[  25]---> BDD-cost:  107
c ---[  24]---> BDD-cost:  107
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26710    74700 |    8903       0        0     nan |  0.000 % |
c |       101 |   26710    74700 |    9793     101    19540   193.5 |  0.617 % |
c |       254 |   26710    74700 |   10772     254    57136   224.9 |  0.617 % |
c |       479 |   26710    74700 |   11849     479   106928   223.2 |  0.617 % |
c |       820 |   26710    74700 |   13034     820   228012   278.1 |  0.617 % |
c |      1327 |   26710    74700 |   14338    1327   407337   307.0 |  0.617 % |
c |      2089 |   26710    74700 |   15772    2089   607183   290.7 |  0.617 % |
c |      3232 |   26710    74700 |   17349    3232   926679   286.7 |  0.617 % |
c |      4943 |   26710    74700 |   19084    4943  1483658   300.2 |  0.617 % |
c |      7507 |   26710    74700 |   20992    7507  2510030   334.4 |  0.617 % |
c |     11351 |   26710    74700 |   23092   11351  4018398   354.0 |  0.617 % |
c |     17118 |   26710    74700 |   25401   17118  7441464   434.7 |  0.617 % |
c |     25771 |   26710    74700 |   27941   25771 13547867   525.7 |  0.617 % |
c |     38747 |   26710    74700 |   30735   11992  5242030   437.1 |  0.617 % |
c |     58209 |   26710    74700 |   33809   31454 12687777   403.4 |  0.617 % |
c |     87404 |   26710    74700 |   37190   27207 15612638   573.8 |  0.617 % |
c |    131194 |   26710    74700 |   40909   35274 17941262   508.6 |  0.617 % |

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/19172/stat): 19172 (minisat+_script) R 19171 19172 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841267036 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/19172/statm): 174 3 169 147 0 27 0
[pid=19172] 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=19173
New process pid=19174
New process pid=19175
execve syscall for /bin/sed executable
One traced child (pid=19174) 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=19175) exited with status: 0
One traced child (pid=19173) exited with status: 0
New process pid=19176
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-chnl50_55_pb.cnf.cr.opb

[startup+10.005 s]
Raw data (loadavg): 0.93 0.95 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 3096 0 2 0 950 14 0 0 25 0 1 0 1841267041 12746752 3002 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 3112 3002 145 145 0 2967 0
[pid=19176] vsize: 12448
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 14572

[startup+20.0066 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) T 19172 19172 16528 0 -1 0 4624 0 2 0 1927 25 0 0 25 0 1 0 1841267041 19021824 4530 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19176/statm): 4644 4530 145 145 0 4499 0
[pid=19176] vsize: 18576
Current children cumulated CPU time (s) 19.52
Current children cumulated vsize (Kb) 20700

[startup+30.0073 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 6144 0 2 0 2904 34 0 0 25 0 1 0 1841267041 25235456 6050 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 6161 6050 145 145 0 6016 0
[pid=19176] vsize: 24644
Current children cumulated CPU time (s) 29.38
Current children cumulated vsize (Kb) 26768

[startup+40.008 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 7524 0 2 0 3885 42 0 0 25 0 1 0 1841267041 30875648 7430 4294967295 134512640 135094434 3221224432 3221223104 134555683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 7538 7430 145 145 0 7393 0
[pid=19176] vsize: 30152
Current children cumulated CPU time (s) 39.27
Current children cumulated vsize (Kb) 32276

[startup+50.0107 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 8710 0 2 0 4867 50 0 0 25 0 1 0 1841267041 35794944 8616 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 8739 8616 145 145 0 8594 0
[pid=19176] vsize: 34956
Current children cumulated CPU time (s) 49.17
Current children cumulated vsize (Kb) 37080

[startup+60.0104 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 10062 0 2 0 5846 59 0 0 25 0 1 0 1841267041 41324544 9968 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 10089 9968 145 145 0 9944 0
[pid=19176] vsize: 40356
Current children cumulated CPU time (s) 59.05
Current children cumulated vsize (Kb) 42480

[startup+70.0111 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 11254 0 2 0 6828 68 0 0 25 0 1 0 1841267041 46198784 11160 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 11279 11160 145 145 0 11134 0
[pid=19176] vsize: 45116
Current children cumulated CPU time (s) 68.96
Current children cumulated vsize (Kb) 47240

[startup+80.0118 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 12397 0 2 0 7812 74 0 0 25 0 1 0 1841267041 50876416 12303 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 12421 12303 145 145 0 12276 0
[pid=19176] vsize: 49684
Current children cumulated CPU time (s) 78.86
Current children cumulated vsize (Kb) 51808

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 13437 0 2 0 8798 80 0 0 25 0 1 0 1841267041 55132160 13343 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 13460 13343 145 145 0 13315 0
[pid=19176] vsize: 53840
Current children cumulated CPU time (s) 88.78
Current children cumulated vsize (Kb) 55964

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) T 19172 19172 16528 0 -1 0 14328 0 2 0 9786 86 0 0 25 0 1 0 1841267041 58781696 14234 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/19176/statm): 14351 14234 145 145 0 14206 0
[pid=19176] vsize: 57404
Current children cumulated CPU time (s) 98.72
Current children cumulated vsize (Kb) 59528

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 15273 0 2 0 10773 91 0 0 25 0 1 0 1841267041 62656512 15179 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 15297 15179 145 145 0 15152 0
[pid=19176] vsize: 61188
Current children cumulated CPU time (s) 108.64
Current children cumulated vsize (Kb) 63312

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 17290 0 2 0 11751 100 0 0 25 0 1 0 1841267041 70905856 17196 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 17311 17196 145 145 0 17166 0
[pid=19176] vsize: 69244
Current children cumulated CPU time (s) 118.51
Current children cumulated vsize (Kb) 71368

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 18822 0 2 0 12732 108 0 0 25 0 1 0 1841267041 77303808 18728 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 18873 18728 145 145 0 18728 0
[pid=19176] vsize: 75492
Current children cumulated CPU time (s) 128.4
Current children cumulated vsize (Kb) 77616

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 19973 0 2 0 13718 115 0 0 25 0 1 0 1841267041 82014208 19879 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 20023 19879 145 145 0 19878 0
[pid=19176] vsize: 80092
Current children cumulated CPU time (s) 138.33
Current children cumulated vsize (Kb) 82216

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 20896 0 2 0 14705 120 0 0 20 0 1 0 1841267041 85852160 20802 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 20960 20802 145 145 0 20815 0
[pid=19176] vsize: 83840
Current children cumulated CPU time (s) 148.25
Current children cumulated vsize (Kb) 85964

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 15693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 158.18
Current children cumulated vsize (Kb) 89160

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 16693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 168.18
Current children cumulated vsize (Kb) 89160

[startup+180.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 17693 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 178.18
Current children cumulated vsize (Kb) 89160

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 18694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 188.19
Current children cumulated vsize (Kb) 89160

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 19694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 198.19
Current children cumulated vsize (Kb) 89160

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 20694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 208.19
Current children cumulated vsize (Kb) 89160

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 21694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 218.19
Current children cumulated vsize (Kb) 89160

[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 22694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 228.19
Current children cumulated vsize (Kb) 89160

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 23694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 238.19
Current children cumulated vsize (Kb) 89160

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 24695 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 248.2
Current children cumulated vsize (Kb) 89160

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 25694 125 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 258.19
Current children cumulated vsize (Kb) 89160

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21690 0 2 0 26694 126 0 0 25 0 1 0 1841267041 89124864 21596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21596 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 268.2
Current children cumulated vsize (Kb) 89160

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21691 0 2 0 27694 126 0 0 25 0 1 0 1841267041 89124864 21597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21597 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 278.2
Current children cumulated vsize (Kb) 89160

[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21692 0 2 0 28695 126 0 0 25 0 1 0 1841267041 89124864 21598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21598 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 288.21
Current children cumulated vsize (Kb) 89160

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 21694 0 2 0 29695 126 0 0 25 0 1 0 1841267041 89124864 21600 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 21759 21600 145 145 0 21614 0
[pid=19176] vsize: 87036
Current children cumulated CPU time (s) 298.21
Current children cumulated vsize (Kb) 89160

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 22341 0 2 0 30687 129 0 0 25 0 1 0 1841267041 91774976 22247 4294967295 134512640 135094434 3221224432 3221223104 134556462 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 22406 22247 145 145 0 22261 0
[pid=19176] vsize: 89624
Current children cumulated CPU time (s) 308.16
Current children cumulated vsize (Kb) 91748

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23151 0 2 0 31672 135 0 0 25 0 1 0 1841267041 95137792 23057 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23227 23057 145 145 0 23082 0
[pid=19176] vsize: 92908
Current children cumulated CPU time (s) 318.07
Current children cumulated vsize (Kb) 95032

[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23418 0 2 0 32668 137 0 0 25 0 1 0 1841267041 96223232 23324 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23324 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 328.05
Current children cumulated vsize (Kb) 96092

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23420 0 2 0 33668 137 0 0 25 0 1 0 1841267041 96223232 23326 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23326 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 338.05
Current children cumulated vsize (Kb) 96092

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23420 0 2 0 34669 137 0 0 25 0 1 0 1841267041 96223232 23326 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23326 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 348.06
Current children cumulated vsize (Kb) 96092

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23421 0 2 0 35669 137 0 0 25 0 1 0 1841267041 96223232 23327 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23327 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 358.06
Current children cumulated vsize (Kb) 96092

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 36669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 368.06
Current children cumulated vsize (Kb) 96092

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 37669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 378.06
Current children cumulated vsize (Kb) 96092

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 38669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 388.06
Current children cumulated vsize (Kb) 96092

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23424 0 2 0 39669 137 0 0 25 0 1 0 1841267041 96223232 23330 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23330 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 398.06
Current children cumulated vsize (Kb) 96092

[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 40670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 408.07
Current children cumulated vsize (Kb) 96092

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 41670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 418.07
Current children cumulated vsize (Kb) 96092

[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 42670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 428.07
Current children cumulated vsize (Kb) 96092

[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 43670 137 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 438.07
Current children cumulated vsize (Kb) 96092

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23425 0 2 0 44670 138 0 0 25 0 1 0 1841267041 96223232 23331 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23331 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 448.08
Current children cumulated vsize (Kb) 96092

[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 45670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 458.08
Current children cumulated vsize (Kb) 96092

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 46670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 468.08
Current children cumulated vsize (Kb) 96092

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 47670 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 478.08
Current children cumulated vsize (Kb) 96092

[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23426 0 2 0 48671 138 0 0 25 0 1 0 1841267041 96223232 23332 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23492 23332 145 145 0 23347 0
[pid=19176] vsize: 93968
Current children cumulated CPU time (s) 488.09
Current children cumulated vsize (Kb) 96092

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 23821 0 2 0 49666 140 0 0 25 0 1 0 1841267041 97845248 23727 4294967295 134512640 135094434 3221224432 3221223024 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 23888 23727 145 145 0 23743 0
[pid=19176] vsize: 95552
Current children cumulated CPU time (s) 498.06
Current children cumulated vsize (Kb) 97676

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 24767 0 2 0 50651 147 0 0 25 0 1 0 1841267041 101736448 24673 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 24838 24673 145 145 0 24693 0
[pid=19176] vsize: 99352
Current children cumulated CPU time (s) 507.98
Current children cumulated vsize (Kb) 101476

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 25724 0 2 0 51638 153 0 0 25 0 1 0 1841267041 105697280 25630 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 25805 25630 145 145 0 25660 0
[pid=19176] vsize: 103220
Current children cumulated CPU time (s) 517.91
Current children cumulated vsize (Kb) 105344

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 26489 0 2 0 52628 157 0 0 25 0 1 0 1841267041 108863488 26395 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 26578 26395 145 145 0 26433 0
[pid=19176] vsize: 106312
Current children cumulated CPU time (s) 527.85
Current children cumulated vsize (Kb) 108436

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 27370 0 2 0 53615 163 0 0 25 0 1 0 1841267041 112508928 27276 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 27468 27276 145 145 0 27323 0
[pid=19176] vsize: 109872
Current children cumulated CPU time (s) 537.78
Current children cumulated vsize (Kb) 111996

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 28158 0 2 0 54602 168 0 0 25 0 1 0 1841267041 115773440 28064 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 28265 28064 145 145 0 28120 0
[pid=19176] vsize: 113060
Current children cumulated CPU time (s) 547.7
Current children cumulated vsize (Kb) 115184

[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 28903 0 2 0 55591 174 0 0 25 0 1 0 1841267041 118841344 28809 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 29014 28809 145 145 0 28869 0
[pid=19176] vsize: 116056
Current children cumulated CPU time (s) 557.65
Current children cumulated vsize (Kb) 118180

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29472 0 2 0 56581 177 0 0 25 0 1 0 1841267041 121196544 29378 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 29589 29378 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 567.58
Current children cumulated vsize (Kb) 120480

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29473 0 2 0 57581 177 0 0 25 0 1 0 1841267041 121196544 29379 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19176/statm): 29589 29379 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 577.58
Current children cumulated vsize (Kb) 120480

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29478 0 2 0 58581 177 0 0 25 0 1 0 1841267041 121196544 29384 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29384 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 587.58
Current children cumulated vsize (Kb) 120480

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 59581 177 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 597.58
Current children cumulated vsize (Kb) 120480

[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 60581 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 607.59
Current children cumulated vsize (Kb) 120480

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 61582 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 617.6
Current children cumulated vsize (Kb) 120480

[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 62582 178 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223024 134557042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 627.6
Current children cumulated vsize (Kb) 120480

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 63581 179 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 637.6
Current children cumulated vsize (Kb) 120480

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 64580 180 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 647.6
Current children cumulated vsize (Kb) 120480

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 65580 180 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 657.6
Current children cumulated vsize (Kb) 120480

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 66580 181 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 667.61
Current children cumulated vsize (Kb) 120480

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29480 0 2 0 67580 181 0 0 25 0 1 0 1841267041 121196544 29386 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29386 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 677.61
Current children cumulated vsize (Kb) 120480

[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29486 0 2 0 68580 181 0 0 25 0 1 0 1841267041 121196544 29392 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29392 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 687.61
Current children cumulated vsize (Kb) 120480

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 69580 181 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223104 134556315 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 697.61
Current children cumulated vsize (Kb) 120480

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 70580 181 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 707.61
Current children cumulated vsize (Kb) 120480

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 71580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 717.62
Current children cumulated vsize (Kb) 120480

[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 72580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 727.62
Current children cumulated vsize (Kb) 120480

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 73580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 737.62
Current children cumulated vsize (Kb) 120480

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29490 0 2 0 74580 182 0 0 25 0 1 0 1841267041 121196544 29396 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29396 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 747.62
Current children cumulated vsize (Kb) 120480

[startup+760.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 75580 182 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 757.62
Current children cumulated vsize (Kb) 120480

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 76581 182 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 767.63
Current children cumulated vsize (Kb) 120480

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 77580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 777.63
Current children cumulated vsize (Kb) 120480

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 78580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 787.63
Current children cumulated vsize (Kb) 120480

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 79580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 797.63
Current children cumulated vsize (Kb) 120480

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 80581 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 807.64
Current children cumulated vsize (Kb) 120480

[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 81580 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 817.63
Current children cumulated vsize (Kb) 120480

[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29491 0 2 0 82581 183 0 0 25 0 1 0 1841267041 121196544 29397 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29397 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 827.64
Current children cumulated vsize (Kb) 120480

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29492 0 2 0 83581 183 0 0 25 0 1 0 1841267041 121196544 29398 4294967295 134512640 135094434 3221224432 3221223024 134556928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29398 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 837.64
Current children cumulated vsize (Kb) 120480

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29493 0 2 0 84581 183 0 0 25 0 1 0 1841267041 121196544 29399 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29589 29399 145 145 0 29444 0
[pid=19176] vsize: 118356
Current children cumulated CPU time (s) 847.64
Current children cumulated vsize (Kb) 120480

[startup+860.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 85581 183 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 857.64
Current children cumulated vsize (Kb) 119928

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 86581 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 867.65
Current children cumulated vsize (Kb) 119928

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 87582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 877.66
Current children cumulated vsize (Kb) 119928

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 88582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 887.66
Current children cumulated vsize (Kb) 119928

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 89582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 897.66
Current children cumulated vsize (Kb) 119928

[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 90582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 907.66
Current children cumulated vsize (Kb) 119928

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 91582 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 917.66
Current children cumulated vsize (Kb) 119928

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 92583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 927.67
Current children cumulated vsize (Kb) 119928

[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 93583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 937.67
Current children cumulated vsize (Kb) 119928

[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 94583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 947.67
Current children cumulated vsize (Kb) 119928

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 95583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 957.67
Current children cumulated vsize (Kb) 119928

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 96584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 967.68
Current children cumulated vsize (Kb) 119928

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 97583 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 977.67
Current children cumulated vsize (Kb) 119928

[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 98584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 987.68
Current children cumulated vsize (Kb) 119928

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 99584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 997.68
Current children cumulated vsize (Kb) 119928

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 100584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1007.68
Current children cumulated vsize (Kb) 119928

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 101584 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1017.68
Current children cumulated vsize (Kb) 119928

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 102585 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1027.69
Current children cumulated vsize (Kb) 119928

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 103585 184 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1037.69
Current children cumulated vsize (Kb) 119928

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 104585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1047.7
Current children cumulated vsize (Kb) 119928

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 105585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1057.7
Current children cumulated vsize (Kb) 119928

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 106585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1067.7
Current children cumulated vsize (Kb) 119928

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 107585 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1077.7
Current children cumulated vsize (Kb) 119928

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 108586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1087.71
Current children cumulated vsize (Kb) 119928

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 109586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1097.71
Current children cumulated vsize (Kb) 119928

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 110586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1107.71
Current children cumulated vsize (Kb) 119928

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 111587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1117.72
Current children cumulated vsize (Kb) 119928

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 112586 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1127.71
Current children cumulated vsize (Kb) 119928

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 113587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1137.72
Current children cumulated vsize (Kb) 119928

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 114587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1147.72
Current children cumulated vsize (Kb) 119928

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 115587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1157.72
Current children cumulated vsize (Kb) 119928

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 116587 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1167.72
Current children cumulated vsize (Kb) 119928

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 117588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1177.73
Current children cumulated vsize (Kb) 119928

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 118588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1187.73
Current children cumulated vsize (Kb) 119928

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 119588 185 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1197.73
Current children cumulated vsize (Kb) 119928

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 120588 186 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1207.74
Current children cumulated vsize (Kb) 119928



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 19176
Raw data (/proc/19172/stat): 19172 (minisat+_script) S 19171 19172 16528 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841267036 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19172/statm): 531 226 485 147 0 384 0
[pid=19172] vsize: 2124
Raw data (/proc/19176/stat): 19176 (minisat+_64-bit) R 19172 19172 16528 0 -1 0 29494 0 2 0 120588 186 0 0 25 0 1 0 1841267041 120631296 29262 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19176/statm): 29451 29262 145 145 0 29306 0
[pid=19176] vsize: 117804
Current children cumulated CPU time (s) 1207.74
Current children cumulated vsize (Kb) 119928

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.8
CPU user time (s): 1205.89
CPU system time (s): 1.91471
CPU usage (%): 99.806
Max. virtual memory (cumulated for all children) (Kb): 120480

Verifier Data

ERROR: no interpretation found !