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-fpga40_38_sat_pb.cnf.cr.opb
MD5SUM69d239b72e8d1a72f9c55329043493e1
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark14.9957
Number of variables2280
Total number of constraints1636
Number of constraints which are clauses1558
Number of constraints which are cardinality constraints (but not clauses)78
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint40

Trace number 894

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        945544 kB
Buffers:         33908 kB
Cached:          31364 kB
SwapCached:        960 kB
Active:          52748 kB
Inactive:        15204 kB
HighTotal:      131008 kB
HighFree:        97188 kB
LowTotal:       903652 kB
LowFree:        848356 kB
SwapTotal:     2097136 kB
SwapFree:      2095628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            15524 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:54:05 (client local time) WITH STATUS 0 IN 1208.81 SECONDS
stats: 2391 7 1208.81 0

Solver Data

c Parsing PB file...
c Converting 1636 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  77]---> BDD-cost:   73
c ---[  76]---> BDD-cost:   73
c ---[  75]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   73
c ---[  73]---> BDD-cost:   73
c ---[  72]---> BDD-cost:   73
c ---[  71]---> BDD-cost:   73
c ---[  70]---> BDD-cost:   73
c ---[  69]---> BDD-cost:   73
c ---[  68]---> BDD-cost:   73
c ---[  67]---> BDD-cost:   73
c ---[  66]---> BDD-cost:   73
c ---[  65]---> BDD-cost:   73
c ---[  64]---> BDD-cost:   73
c ---[  63]---> BDD-cost:   73
c ---[  62]---> BDD-cost:   73
c ---[  61]---> BDD-cost:   73
c ---[  60]---> BDD-cost:   73
c ---[  59]---> BDD-cost:   73
c ---[  58]---> BDD-cost:   73
c ---[  57]---> BDD-cost:   73
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:   73
c ---[  54]---> BDD-cost:   73
c ---[  53]---> BDD-cost:   73
c ---[  52]---> BDD-cost:   73
c ---[  51]---> BDD-cost:   73
c ---[  50]---> BDD-cost:   73
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:   73
c ---[  47]---> BDD-cost:   73
c ---[  46]---> BDD-cost:   73
c ---[  45]---> BDD-cost:   73
c ---[  44]---> BDD-cost:   73
c ---[  43]---> BDD-cost:   73
c ---[  42]---> BDD-cost:   73
c ---[  41]---> BDD-cost:   73
c ---[  40]---> BDD-cost:   73
c ---[  39]---> BDD-cost:   73
c ---[  38]---> BDD-cost:   73
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12256    59766 |    4085       0        0     nan |  0.000 % |
c |       103 |   12256    59766 |    4493     103    23189   225.1 |  1.181 % |
c |       253 |   12256    59766 |    4942     253    33793   133.6 |  1.181 % |
c |       480 |   12256    59766 |    5437     480    75308   156.9 |  1.181 % |
c |       817 |   12256    59766 |    5980     817   169756   207.8 |  1.181 % |
c |      1323 |   12256    59766 |    6578    1323   266622   201.5 |  1.181 % |
c |      2082 |   12256    59766 |    7236    2082   346944   166.6 |  1.181 % |
c |      3221 |   12256    59766 |    7960    3221   672994   208.9 |  1.181 % |
c |      4933 |   12256    59766 |    8756    4933   891745   180.8 |  1.181 % |
c |      7495 |   12256    59766 |    9632    7495  1795103   239.5 |  1.181 % |
c |     11340 |   12256    59766 |   10595   11340  2331890   205.6 |  1.181 % |
c |     17107 |   12256    59766 |   11654   11437  3336088   291.7 |  1.181 % |
c |     25760 |   12256    59766 |   12820   12101  3971454   328.2 |  1.181 % |
c |     38736 |   12256    59766 |   14102   16761  4472808   266.9 |  1.181 % |
c |     58201 |   12256    59766 |   15512   18480  7868227   425.8 |  1.181 % |
c |     87394 |   12256    59766 |   17064   17668  2277590   128.9 |  1.181 % |
c |    131184 |   12256    59766 |   18770   21073  9678978   459.3 |  1.181 % |
c |    196873 |   12256    59766 |   20647   20482  7435518   363.0 |  1.181 % |
c |    295403 |   12256    59766 |   22712   24813  4118111   166.0 |  1.181 % |

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/9432/stat): 9432 (minisat+_script) R 9431 9432 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783047228 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/9432/statm): 174 3 169 147 0 27 0
[pid=9432] 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=9433
New process pid=9434
New process pid=9435
execve syscall for /bin/sed executable
One traced child (pid=9434) 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=9435) exited with status: 0
One traced child (pid=9433) exited with status: 0
New process pid=9436
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb

[startup+10.004 s]
Raw data (loadavg): 0.82 0.91 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 2710 0 0 0 962 15 0 0 25 0 1 0 1783047233 11395072 2696 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 2782 2696 145 145 0 2637 0
[pid=9436] vsize: 11128
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 13252

[startup+20.0058 s]
Raw data (loadavg): 0.85 0.91 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 3212 0 0 0 1955 18 0 0 25 0 1 0 1783047233 13467648 3198 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 3288 3198 145 145 0 3143 0
[pid=9436] vsize: 13152
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 15276

[startup+30.0076 s]
Raw data (loadavg): 0.87 0.91 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 4573 0 0 0 2935 26 0 0 25 0 1 0 1783047233 19066880 4559 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 4655 4559 145 145 0 4510 0
[pid=9436] vsize: 18620
Current children cumulated CPU time (s) 29.62
Current children cumulated vsize (Kb) 20744

[startup+40.0074 s]
Raw data (loadavg): 0.89 0.91 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5754 0 0 0 3917 35 0 0 25 0 1 0 1783047233 23916544 5740 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 5839 5740 145 145 0 5694 0
[pid=9436] vsize: 23356
Current children cumulated CPU time (s) 39.53
Current children cumulated vsize (Kb) 25480

[startup+50.0092 s]
Raw data (loadavg): 0.91 0.92 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5786 0 0 0 4917 35 0 0 25 0 1 0 1783047233 24031232 5772 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 5867 5772 145 145 0 5722 0
[pid=9436] vsize: 23468
Current children cumulated CPU time (s) 49.53
Current children cumulated vsize (Kb) 25592

[startup+60.0101 s]
Raw data (loadavg): 0.92 0.92 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5787 0 0 0 5917 35 0 0 25 0 1 0 1783047233 24031232 5773 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 5867 5773 145 145 0 5722 0
[pid=9436] vsize: 23468
Current children cumulated CPU time (s) 59.53
Current children cumulated vsize (Kb) 25592

[startup+70.0119 s]
Raw data (loadavg): 0.93 0.92 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 6905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0
[pid=9436] vsize: 26620
Current children cumulated CPU time (s) 69.45
Current children cumulated vsize (Kb) 28744

[startup+80.0127 s]
Raw data (loadavg): 0.94 0.92 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 7905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0
[pid=9436] vsize: 26620
Current children cumulated CPU time (s) 79.45
Current children cumulated vsize (Kb) 28744

[startup+90.0135 s]
Raw data (loadavg): 0.95 0.92 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 8905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0
[pid=9436] vsize: 26620
Current children cumulated CPU time (s) 89.45
Current children cumulated vsize (Kb) 28744

[startup+100.014 s]
Raw data (loadavg): 0.96 0.93 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 9905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0
[pid=9436] vsize: 26620
Current children cumulated CPU time (s) 99.45
Current children cumulated vsize (Kb) 28744

[startup+110.015 s]
Raw data (loadavg): 0.96 0.93 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 10894 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0
[pid=9436] vsize: 29156
Current children cumulated CPU time (s) 109.39
Current children cumulated vsize (Kb) 31280

[startup+120.017 s]
Raw data (loadavg): 0.97 0.93 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 11895 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0
[pid=9436] vsize: 29156
Current children cumulated CPU time (s) 119.4
Current children cumulated vsize (Kb) 31280

[startup+130.018 s]
Raw data (loadavg): 0.97 0.93 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 12895 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0
[pid=9436] vsize: 29156
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 31280

[startup+140.019 s]
Raw data (loadavg): 0.98 0.93 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7195 0 0 0 13894 44 0 0 25 0 1 0 1783047233 29855744 7181 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 7289 7181 145 145 0 7144 0
[pid=9436] vsize: 29156
Current children cumulated CPU time (s) 139.39
Current children cumulated vsize (Kb) 31280

[startup+150.02 s]
Raw data (loadavg): 0.98 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7363 0 0 0 14891 46 0 0 25 0 1 0 1783047233 30552064 7349 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 7459 7349 145 145 0 7314 0
[pid=9436] vsize: 29836
Current children cumulated CPU time (s) 149.38
Current children cumulated vsize (Kb) 31960

[startup+160.02 s]
Raw data (loadavg): 0.98 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7941 0 0 0 15883 49 0 0 25 0 1 0 1783047233 32956416 7927 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 8046 7927 145 145 0 7901 0
[pid=9436] vsize: 32184
Current children cumulated CPU time (s) 159.33
Current children cumulated vsize (Kb) 34308

[startup+170.022 s]
Raw data (loadavg): 0.98 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 8535 0 0 0 16874 52 0 0 25 0 1 0 1783047233 35405824 8521 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 8644 8521 145 145 0 8499 0
[pid=9436] vsize: 34576
Current children cumulated CPU time (s) 169.27
Current children cumulated vsize (Kb) 36700

[startup+180.023 s]
Raw data (loadavg): 0.99 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9138 0 0 0 17865 56 0 0 25 0 1 0 1783047233 37900288 9124 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9253 9124 145 145 0 9108 0
[pid=9436] vsize: 37012
Current children cumulated CPU time (s) 179.22
Current children cumulated vsize (Kb) 39136

[startup+190.024 s]
Raw data (loadavg): 0.99 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9606 0 0 0 18857 59 0 0 25 0 1 0 1783047233 39825408 9592 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9592 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 189.17
Current children cumulated vsize (Kb) 41016

[startup+200.026 s]
Raw data (loadavg): 0.99 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 19857 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 199.17
Current children cumulated vsize (Kb) 41016

[startup+210.026 s]
Raw data (loadavg): 0.99 0.94 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 20857 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 209.17
Current children cumulated vsize (Kb) 41016

[startup+220.027 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 21858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 219.18
Current children cumulated vsize (Kb) 41016

[startup+230.028 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 22858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 229.18
Current children cumulated vsize (Kb) 41016

[startup+240.029 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 23858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 239.18
Current children cumulated vsize (Kb) 41016

[startup+250.03 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 24858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 249.18
Current children cumulated vsize (Kb) 41016

[startup+260.031 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 25858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 259.18
Current children cumulated vsize (Kb) 41016

[startup+270.033 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 26859 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 269.19
Current children cumulated vsize (Kb) 41016

[startup+280.033 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 27859 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 279.19
Current children cumulated vsize (Kb) 41016

[startup+290.034 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 28859 59 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 289.19
Current children cumulated vsize (Kb) 41016

[startup+300.036 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 29859 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 299.2
Current children cumulated vsize (Kb) 41016

[startup+310.037 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 30860 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 309.21
Current children cumulated vsize (Kb) 41016

[startup+320.039 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 31860 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0
[pid=9436] vsize: 38892
Current children cumulated CPU time (s) 319.21
Current children cumulated vsize (Kb) 41016

[startup+330.04 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9705 0 0 0 32858 62 0 0 25 0 1 0 1783047233 40230912 9691 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 9822 9691 145 145 0 9677 0
[pid=9436] vsize: 39288
Current children cumulated CPU time (s) 329.21
Current children cumulated vsize (Kb) 41412

[startup+340.041 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 10074 0 0 0 33852 63 0 0 25 0 1 0 1783047233 41787392 10060 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 10202 10060 145 145 0 10057 0
[pid=9436] vsize: 40808
Current children cumulated CPU time (s) 339.16
Current children cumulated vsize (Kb) 42932

[startup+350.042 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 10535 0 0 0 34846 66 0 0 25 0 1 0 1783047233 43663360 10521 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 10660 10521 145 145 0 10515 0
[pid=9436] vsize: 42640
Current children cumulated CPU time (s) 349.13
Current children cumulated vsize (Kb) 44764

[startup+360.043 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 11009 0 0 0 35839 70 0 0 25 0 1 0 1783047233 45666304 10995 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 11149 10995 145 145 0 11004 0
[pid=9436] vsize: 44596
Current children cumulated CPU time (s) 359.1
Current children cumulated vsize (Kb) 46720

[startup+370.044 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 11601 0 0 0 36829 74 0 0 25 0 1 0 1783047233 48082944 11587 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 11739 11587 145 145 0 11594 0
[pid=9436] vsize: 46956
Current children cumulated CPU time (s) 369.04
Current children cumulated vsize (Kb) 49080

[startup+380.045 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12011 0 0 0 37823 77 0 0 25 0 1 0 1783047233 49831936 11997 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12166 11997 145 145 0 12021 0
[pid=9436] vsize: 48664
Current children cumulated CPU time (s) 379.01
Current children cumulated vsize (Kb) 50788

[startup+390.046 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 38819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0
[pid=9436] vsize: 49532
Current children cumulated CPU time (s) 388.99
Current children cumulated vsize (Kb) 51656

[startup+400.047 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 39819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0
[pid=9436] vsize: 49532
Current children cumulated CPU time (s) 398.99
Current children cumulated vsize (Kb) 51656

[startup+410.047 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 40819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0
[pid=9436] vsize: 49532
Current children cumulated CPU time (s) 408.99
Current children cumulated vsize (Kb) 51656

[startup+420.049 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 41819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0
[pid=9436] vsize: 49532
Current children cumulated CPU time (s) 418.99
Current children cumulated vsize (Kb) 51656

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 42815 81 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0
[pid=9436] vsize: 50984
Current children cumulated CPU time (s) 428.97
Current children cumulated vsize (Kb) 53108

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 43815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0
[pid=9436] vsize: 50984
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 53108

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 44815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0
[pid=9436] vsize: 50984
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 53108

[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 45815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0
[pid=9436] vsize: 50984
Current children cumulated CPU time (s) 458.98
Current children cumulated vsize (Kb) 53108

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 46815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0
[pid=9436] vsize: 50984
Current children cumulated CPU time (s) 468.98
Current children cumulated vsize (Kb) 53108

[startup+480.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 47815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 478.98
Current children cumulated vsize (Kb) 53176

[startup+490.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 48815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 488.98
Current children cumulated vsize (Kb) 53176

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 49815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 498.98
Current children cumulated vsize (Kb) 53176

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 50815 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 508.99
Current children cumulated vsize (Kb) 53176

[startup+520.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 51815 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 518.99
Current children cumulated vsize (Kb) 53176

[startup+530.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 52816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 529
Current children cumulated vsize (Kb) 53176

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 53816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 539
Current children cumulated vsize (Kb) 53176

[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 54816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 549
Current children cumulated vsize (Kb) 53176

[startup+560.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 55816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 559
Current children cumulated vsize (Kb) 53176

[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 56816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 569
Current children cumulated vsize (Kb) 53176

[startup+580.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 57817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 579.01
Current children cumulated vsize (Kb) 53176

[startup+590.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 58817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 589.01
Current children cumulated vsize (Kb) 53176

[startup+600.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 59817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 599.01
Current children cumulated vsize (Kb) 53176

[startup+610.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 60817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 609.01
Current children cumulated vsize (Kb) 53176

[startup+620.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 61817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 619.01
Current children cumulated vsize (Kb) 53176

[startup+630.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 62818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 629.02
Current children cumulated vsize (Kb) 53176

[startup+640.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 63818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 639.02
Current children cumulated vsize (Kb) 53176

[startup+650.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 64818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 649.02
Current children cumulated vsize (Kb) 53176

[startup+660.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 65818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 659.02
Current children cumulated vsize (Kb) 53176

[startup+670.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 66818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 669.02
Current children cumulated vsize (Kb) 53176

[startup+680.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 67819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221222944 134783385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 679.03
Current children cumulated vsize (Kb) 53176

[startup+690.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 68819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 689.03
Current children cumulated vsize (Kb) 53176

[startup+700.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 69819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 699.03
Current children cumulated vsize (Kb) 53176

[startup+710.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 70819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 709.03
Current children cumulated vsize (Kb) 53176

[startup+720.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 71820 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 719.04
Current children cumulated vsize (Kb) 53176

[startup+730.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 72820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223104 134555758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 729.05
Current children cumulated vsize (Kb) 53176

[startup+740.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 73820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 739.05
Current children cumulated vsize (Kb) 53176

[startup+750.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 74820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 749.05
Current children cumulated vsize (Kb) 53176

[startup+760.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 75820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 759.05
Current children cumulated vsize (Kb) 53176

[startup+770.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 76821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 769.06
Current children cumulated vsize (Kb) 53176

[startup+780.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 77821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 779.06
Current children cumulated vsize (Kb) 53176

[startup+790.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 78821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 789.06
Current children cumulated vsize (Kb) 53176

[startup+800.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 79821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 799.06
Current children cumulated vsize (Kb) 53176

[startup+810.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 80820 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 809.05
Current children cumulated vsize (Kb) 53176

[startup+820.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 81820 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 819.05
Current children cumulated vsize (Kb) 53176

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 82821 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 829.06
Current children cumulated vsize (Kb) 53176

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 83821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 839.06
Current children cumulated vsize (Kb) 53176

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 84821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 849.06
Current children cumulated vsize (Kb) 53176

[startup+860.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 85821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 859.06
Current children cumulated vsize (Kb) 53176

[startup+870.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 86822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 869.07
Current children cumulated vsize (Kb) 53176

[startup+880.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 87822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 879.07
Current children cumulated vsize (Kb) 53176

[startup+890.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 88822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 889.07
Current children cumulated vsize (Kb) 53176

[startup+900.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 89822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 899.07
Current children cumulated vsize (Kb) 53176

[startup+910.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 90822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 909.07
Current children cumulated vsize (Kb) 53176

[startup+920.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 91822 85 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 919.08
Current children cumulated vsize (Kb) 53176

[startup+930.097 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 92822 85 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 929.08
Current children cumulated vsize (Kb) 53176

[startup+940.098 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 93821 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 939.08
Current children cumulated vsize (Kb) 53176

[startup+950.099 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 94821 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 949.08
Current children cumulated vsize (Kb) 53176

[startup+960.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 95822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 959.09
Current children cumulated vsize (Kb) 53176

[startup+970.101 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 96822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221221900 134563367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 969.09
Current children cumulated vsize (Kb) 53176

[startup+980.101 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 97822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 979.09
Current children cumulated vsize (Kb) 53176

[startup+990.102 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 98822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 989.1
Current children cumulated vsize (Kb) 53176

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 99822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134557108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 999.1
Current children cumulated vsize (Kb) 53176

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 100822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1009.1
Current children cumulated vsize (Kb) 53176

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 101823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1019.11
Current children cumulated vsize (Kb) 53176

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 102823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1029.11
Current children cumulated vsize (Kb) 53176

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 103823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1039.11
Current children cumulated vsize (Kb) 53176

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 104823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1049.11
Current children cumulated vsize (Kb) 53176

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 105823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1059.11
Current children cumulated vsize (Kb) 53176

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 106823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134552020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1069.11
Current children cumulated vsize (Kb) 53176

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 107823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1079.11
Current children cumulated vsize (Kb) 53176

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 108823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1089.11
Current children cumulated vsize (Kb) 53176

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 109824 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0
[pid=9436] vsize: 51052
Current children cumulated CPU time (s) 1099.12
Current children cumulated vsize (Kb) 53176

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12867 0 0 0 110820 89 0 0 25 0 1 0 1783047233 53350400 12853 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13025 12853 145 145 0 12880 0
[pid=9436] vsize: 52100
Current children cumulated CPU time (s) 1109.1
Current children cumulated vsize (Kb) 54224

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13560 0 0 0 111809 94 0 0 25 0 1 0 1783047233 56225792 13546 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13727 13546 145 145 0 13582 0
[pid=9436] vsize: 54908
Current children cumulated CPU time (s) 1119.04
Current children cumulated vsize (Kb) 57032

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 112809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0
[pid=9436] vsize: 54972
Current children cumulated CPU time (s) 1129.04
Current children cumulated vsize (Kb) 57096

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 113809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0
[pid=9436] vsize: 54972
Current children cumulated CPU time (s) 1139.04
Current children cumulated vsize (Kb) 57096

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 114809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0
[pid=9436] vsize: 54972
Current children cumulated CPU time (s) 1149.04
Current children cumulated vsize (Kb) 57096

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13596 0 0 0 115809 95 0 0 25 0 1 0 1783047233 56455168 13582 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 13783 13582 145 145 0 13638 0
[pid=9436] vsize: 55132
Current children cumulated CPU time (s) 1159.05
Current children cumulated vsize (Kb) 57256

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 14114 0 0 0 116802 97 0 0 25 0 1 0 1783047233 58593280 14100 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 14305 14100 145 145 0 14160 0
[pid=9436] vsize: 57220
Current children cumulated CPU time (s) 1169
Current children cumulated vsize (Kb) 59344

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 14732 0 0 0 117793 102 0 0 25 0 1 0 1783047233 61157376 14718 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 14931 14718 145 145 0 14786 0
[pid=9436] vsize: 59724
Current children cumulated CPU time (s) 1178.96
Current children cumulated vsize (Kb) 61848

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 15257 0 0 0 118784 105 0 0 25 0 1 0 1783047233 63320064 15243 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 15459 15243 145 145 0 15314 0
[pid=9436] vsize: 61836
Current children cumulated CPU time (s) 1188.9
Current children cumulated vsize (Kb) 63960

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16036 0 0 0 119773 110 0 0 25 0 1 0 1783047233 66502656 16022 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 16236 16022 145 145 0 16091 0
[pid=9436] vsize: 64944
Current children cumulated CPU time (s) 1198.84
Current children cumulated vsize (Kb) 67068

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16580 0 0 0 120763 114 0 0 25 0 1 0 1783047233 68763648 16566 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 16788 16566 145 145 0 16643 0
[pid=9436] vsize: 67152
Current children cumulated CPU time (s) 1208.78
Current children cumulated vsize (Kb) 69276



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 9436
Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9432/statm): 531 226 485 147 0 384 0
[pid=9432] vsize: 2124
Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16580 0 0 0 120764 114 0 0 25 0 1 0 1783047233 68763648 16566 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9436/statm): 16788 16566 145 145 0 16643 0
[pid=9436] vsize: 67152
Current children cumulated CPU time (s) 1208.79
Current children cumulated vsize (Kb) 69276

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.81
CPU user time (s): 1207.64
CPU system time (s): 1.17082
CPU usage (%): 99.8883
Max. virtual memory (cumulated for all children) (Kb): 69276

Verifier Data

ERROR: no interpretation found !