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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:100.opb
MD5SUMb2c6bc03457d15976fdaf81252d9cdae
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3
Optimality of the best value was proved NO
Number of terms in the objective function 435
Biggest coefficient in the objective function 282
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 1168
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 282
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 1168
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.11
Number of variables435
Total number of constraints935
Number of constraints which are clauses403
Number of constraints which are cardinality constraints (but not clauses)532
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint16

Trace number 2601

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        865632 kB
Buffers:         38132 kB
Cached:         100700 kB
SwapCached:        908 kB
Active:          95348 kB
Inactive:        46344 kB
HighTotal:      131008 kB
HighFree:        35476 kB
LowTotal:       903652 kB
LowFree:        830156 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21724 kB
Committed_AS:    93168 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:29:25 (client local time) WITH STATUS 10 IN 1207.89 SECONDS
stats: 2746 7 1207.89 10

Solver Data

c Parsing PB file...
c Converting 500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    5
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   14
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    7
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:    7
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   29
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   32
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   32
c ---[  56]---> BDD-cost:   35
c ---[  55]---> BDD-cost:   38
c ---[  54]---> BDD-cost:   38
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   20
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   32
c ---[  45]---> BDD-cost:   41
c ---[  44]---> BDD-cost:   38
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   20
c ---[  37]---> BDD-cost:   29
c ---[  36]---> BDD-cost:   32
c ---[  35]---> BDD-cost:   35
c ---[  34]---> BDD-cost:   38
c ---[  33]---> BDD-cost:   29
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   32
c ---[  24]---> BDD-cost:   38
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   20
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4866    13838 |    1622       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 402
c ---[   0]---> Sorter-cost:24587     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   46776   111909 |   15592       0        0     nan |  0.000 % |
c |       100 |   46317   110889 |   17151      88      633     7.2 |  1.179 % |
c ==============================================================================
c Found solution: 137
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       212 |   47625   114092 |   15875     200     1276     6.4 |  1.179 % |
c |       312 |   47613   114068 |   17462     299     3874    13.0 |  1.213 % |
c ==============================================================================
c Found solution: 25
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       449 |   47950   114922 |   15983     435     7059    16.2 |  1.213 % |
c |       551 |   47904   114825 |   17581     535     8543    16.0 |  1.379 % |
c |       702 |   47840   114679 |   19339     682    12843    18.8 |  1.468 % |
c |       928 |   47588   114125 |   21273     900    16398    18.2 |  2.001 % |
c |      1265 |   47588   114125 |   23400    1237    27463    22.2 |  2.001 % |
c |      1771 |   47588   114125 |   25740    1743    41226    23.7 |  2.001 % |
c |      2530 |   47390   113674 |   28314    2498    55997    22.4 |  2.327 % |
c |      3669 |   47390   113674 |   31146    3637   114150    31.4 |  2.327 % |
c ==============================================================================
c Found solution: 24
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4447 |   47386   113668 |   15795    4413   134651    30.5 |  2.327 % |
c |      4547 |   47378   113650 |   17374    4512   137187    30.4 |  2.357 % |
c |      4697 |   46743   112215 |   19111    4639   139085    30.0 |  3.410 % |
c |      4922 |   46743   112215 |   21023    4864   142152    29.2 |  3.410 % |
c |      5259 |   46743   112215 |   23125    5201   148530    28.6 |  3.410 % |
c |      5765 |   46731   112187 |   25438    5705   191550    33.6 |  3.427 % |
c |      6526 |   46731   112187 |   27981    6466   304263    47.1 |  3.427 % |
c |      7665 |   46615   111930 |   30779    7597   411451    54.2 |  3.630 % |
c |      9373 |   46448   111543 |   33857    9289   486526    52.4 |  3.909 % |
c |     11935 |   46448   111543 |   37243   11851  1029192    86.8 |  3.909 % |
c |     15781 |   46448   111543 |   40968   15697  1265497    80.6 |  3.909 % |
c ==============================================================================
c Found solution: 21
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21427 |   46469   111611 |   15489   21338  2516856   118.0 |  3.909 % |
c |     21528 |   46469   111611 |   17037   10770  1498101   139.1 |  3.919 % |
c |     21680 |   46469   111611 |   18741   10922  1501083   137.4 |  3.919 % |
c |     21906 |   46435   111537 |   20615   11147  1506104   135.1 |  4.003 % |
c |     22243 |   46435   111537 |   22677   11484  1511405   131.6 |  4.003 % |
c |     22749 |   46431   111528 |   24945   11989  1525371   127.2 |  4.007 % |
c |     23511 |   46431   111528 |   27439   12751  1545253   121.2 |  4.007 % |
c |     24652 |   46358   111366 |   30183   13873  1579719   113.9 |  4.193 % |
c |     26362 |   46358   111366 |   33202   15583  1610608   103.4 |  4.193 % |
c |     28924 |   46358   111366 |   36522   18145  1783147    98.3 |  4.193 % |
c |     32768 |   46358   111366 |   40174   21989  1925348    87.6 |  4.193 % |
c |     38535 |   46358   111366 |   44191   27756  2700233    97.3 |  4.193 % |
c ==============================================================================
c Found solution: 15
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39790 |   46280   111212 |   15426   28997  2781549    95.9 |  4.193 % |
c |     39890 |   46280   111212 |   16968   13562  1053546    77.7 |  4.441 % |
c |     40042 |   46280   111212 |   18665   13714  1056755    77.1 |  4.441 % |
c ==============================================================================
c Found solution: 7
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40213 |   46330   111350 |   15443   13885  1063634    76.6 |  4.441 % |
c |     40314 |   46326   111342 |   16987   13983  1065435    76.2 |  4.447 % |
c |     40465 |   46326   111342 |   18686   14134  1069173    75.6 |  4.447 % |
c |     40690 |   46326   111342 |   20554   14359  1073625    74.8 |  4.447 % |
c |     41027 |   46326   111342 |   22610   14696  1080691    73.5 |  4.447 % |
c |     41533 |   46326   111342 |   24871   15202  1103496    72.6 |  4.447 % |
c |     42292 |   46326   111342 |   27358   15961  1147233    71.9 |  4.447 % |
c |     43431 |   46326   111342 |   30094   17100  1187597    69.5 |  4.447 % |
c |     45139 |   46326   111342 |   33103   18808  1251452    66.5 |  4.447 % |
c |     47705 |   46274   111223 |   36413   21358  1329833    62.3 |  4.523 % |
c |     51551 |   46274   111223 |   40055   25204  1603868    63.6 |  4.523 % |
c |     57319 |   46274   111223 |   44060   30972  2046499    66.1 |  4.523 % |
c |     65969 |   46274   111223 |   48466   39622  3306985    83.5 |  4.523 % |
c |     78943 |   46274   111223 |   53313   52596  4889094    93.0 |  4.523 % |
c |     98404 |   46274   111223 |   58644   24048  4042609   168.1 |  4.523 % |
c |    127597 |   46125   110880 |   64509   53233  8062774   151.5 |  4.818 % |
c |    171387 |   46125   110880 |   70960   37694  8220398   218.1 |  4.818 % |
c |    237072 |   46123   110876 |   78056   40578 10599055   261.2 |  4.823 % |

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/29117/stat): 29117 (minisat+_script) R 29116 29117 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1728938118 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29117/statm): 174 3 169 147 0 27 0
[pid=29117] 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=29118
New process pid=29119
New process pid=29120
execve syscall for /bin/sed executable
One traced child (pid=29119) 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=29120) exited with status: 0
One traced child (pid=29118) exited with status: 0
New process pid=29121
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-10:10:4.5:0.95:100.opb

[startup+10.003 s]
Raw data (loadavg): 0.58 0.78 0.88 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 2366 0 0 0 977 9 0 0 25 0 1 0 1728938123 10121216 2235 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 2471 2235 145 145 0 2326 0
[pid=29121] vsize: 9884
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 12008

[startup+20.0048 s]
Raw data (loadavg): 0.64 0.79 0.88 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 2843 0 0 0 1968 12 0 0 25 0 1 0 1728938123 12087296 2712 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 2951 2712 145 145 0 2806 0
[pid=29121] vsize: 11804
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 13928

[startup+30.0056 s]
Raw data (loadavg): 0.70 0.80 0.88 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 3338 0 0 0 2958 16 0 0 25 0 1 0 1728938123 14098432 3207 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 3442 3207 145 145 0 3297 0
[pid=29121] vsize: 13768
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 15892

[startup+40.0064 s]
Raw data (loadavg): 0.74 0.80 0.88 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 3884 0 0 0 3949 21 0 0 25 0 1 0 1728938123 16388096 3753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 4001 3753 145 145 0 3856 0
[pid=29121] vsize: 16004
Current children cumulated CPU time (s) 39.71
Current children cumulated vsize (Kb) 18128

[startup+50.0071 s]
Raw data (loadavg): 0.78 0.81 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 4476 0 0 0 4938 25 0 0 25 0 1 0 1728938123 18800640 4345 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 4590 4345 145 145 0 4445 0
[pid=29121] vsize: 18360
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 20484

[startup+60.007 s]
Raw data (loadavg): 0.81 0.81 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 4805 0 0 0 5932 28 0 0 25 0 1 0 1728938123 20144128 4674 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 4918 4674 145 145 0 4773 0
[pid=29121] vsize: 19672
Current children cumulated CPU time (s) 59.61
Current children cumulated vsize (Kb) 21796

[startup+70.0087 s]
Raw data (loadavg): 0.84 0.82 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 4805 0 0 0 6932 28 0 0 25 0 1 0 1728938123 20144128 4674 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 4918 4674 145 145 0 4773 0
[pid=29121] vsize: 19672
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 21796

[startup+80.0095 s]
Raw data (loadavg): 0.87 0.83 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 4808 0 0 0 7932 28 0 0 25 0 1 0 1728938123 20144128 4677 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 4918 4677 145 145 0 4773 0
[pid=29121] vsize: 19672
Current children cumulated CPU time (s) 79.61
Current children cumulated vsize (Kb) 21796

[startup+90.0093 s]
Raw data (loadavg): 0.89 0.83 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5061 0 0 0 8927 31 0 0 25 0 1 0 1728938123 21168128 4930 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5168 4930 145 145 0 5023 0
[pid=29121] vsize: 20672
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 22796

[startup+100.01 s]
Raw data (loadavg): 0.90 0.84 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5184 0 0 0 9925 32 0 0 25 0 1 0 1728938123 21651456 5053 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5286 5053 145 145 0 5141 0
[pid=29121] vsize: 21144
Current children cumulated CPU time (s) 99.58
Current children cumulated vsize (Kb) 23268

[startup+110.011 s]
Raw data (loadavg): 0.92 0.84 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5184 0 0 0 10925 32 0 0 25 0 1 0 1728938123 21651456 5053 4294967295 134512640 135094434 3221224432 3221223152 134538541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5286 5053 145 145 0 5141 0
[pid=29121] vsize: 21144
Current children cumulated CPU time (s) 109.58
Current children cumulated vsize (Kb) 23268

[startup+120.012 s]
Raw data (loadavg): 0.93 0.85 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5184 0 0 0 11925 32 0 0 25 0 1 0 1728938123 21651456 5053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5286 5053 145 145 0 5141 0
[pid=29121] vsize: 21144
Current children cumulated CPU time (s) 119.58
Current children cumulated vsize (Kb) 23268

[startup+130.012 s]
Raw data (loadavg): 0.94 0.85 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5186 0 0 0 12925 32 0 0 25 0 1 0 1728938123 21651456 5055 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5286 5055 145 145 0 5141 0
[pid=29121] vsize: 21144
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 23268

[startup+140.012 s]
Raw data (loadavg): 0.95 0.85 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5220 0 0 0 13925 32 0 0 25 0 1 0 1728938123 21913600 5089 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5350 5089 145 145 0 5205 0
[pid=29121] vsize: 21400
Current children cumulated CPU time (s) 139.58
Current children cumulated vsize (Kb) 23524

[startup+150.013 s]
Raw data (loadavg): 0.96 0.86 0.89 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 5377 0 0 0 14923 33 0 0 25 0 1 0 1728938123 22544384 5246 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5504 5246 145 145 0 5359 0
[pid=29121] vsize: 22016
Current children cumulated CPU time (s) 149.57
Current children cumulated vsize (Kb) 24140

[startup+160.013 s]
Raw data (loadavg): 0.96 0.86 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) T 29117 29117 17733 0 -1 0 5825 0 0 0 15915 36 0 0 25 0 1 0 1728938123 24371200 5694 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29121/statm): 5950 5694 145 145 0 5805 0
[pid=29121] vsize: 23800
Current children cumulated CPU time (s) 159.52
Current children cumulated vsize (Kb) 25924

[startup+170.014 s]
Raw data (loadavg): 0.97 0.87 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 6144 0 0 0 16910 38 0 0 25 0 1 0 1728938123 25665536 6013 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 6266 6013 145 145 0 6121 0
[pid=29121] vsize: 25064
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 27188

[startup+180.014 s]
Raw data (loadavg): 0.97 0.87 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 6603 0 0 0 17902 42 0 0 25 0 1 0 1728938123 27533312 6472 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 6722 6472 145 145 0 6577 0
[pid=29121] vsize: 26888
Current children cumulated CPU time (s) 179.45
Current children cumulated vsize (Kb) 29012

[startup+190.015 s]
Raw data (loadavg): 0.98 0.87 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 7038 0 0 0 18894 45 0 0 25 0 1 0 1728938123 29306880 6907 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 7155 6907 145 145 0 7010 0
[pid=29121] vsize: 28620
Current children cumulated CPU time (s) 189.4
Current children cumulated vsize (Kb) 30744

[startup+200.016 s]
Raw data (loadavg): 0.98 0.88 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 7303 0 0 0 19890 47 0 0 25 0 1 0 1728938123 30380032 7172 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 7417 7172 145 145 0 7272 0
[pid=29121] vsize: 29668
Current children cumulated CPU time (s) 199.38
Current children cumulated vsize (Kb) 31792

[startup+210.017 s]
Raw data (loadavg): 0.98 0.88 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 7608 0 0 0 20885 49 0 0 25 0 1 0 1728938123 31617024 7477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 7719 7477 145 145 0 7574 0
[pid=29121] vsize: 30876
Current children cumulated CPU time (s) 209.35
Current children cumulated vsize (Kb) 33000

[startup+220.019 s]
Raw data (loadavg): 0.98 0.89 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 7972 0 0 0 21878 51 0 0 25 0 1 0 1728938123 33095680 7841 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 8080 7841 145 145 0 7935 0
[pid=29121] vsize: 32320
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 34444

[startup+230.019 s]
Raw data (loadavg): 0.99 0.89 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 8384 0 0 0 22868 55 0 0 25 0 1 0 1728938123 34775040 8253 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 8490 8253 145 145 0 8345 0
[pid=29121] vsize: 33960
Current children cumulated CPU time (s) 229.24
Current children cumulated vsize (Kb) 36084

[startup+240.019 s]
Raw data (loadavg): 0.99 0.89 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 8772 0 0 0 23860 59 0 0 25 0 1 0 1728938123 36360192 8641 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 8877 8641 145 145 0 8732 0
[pid=29121] vsize: 35508
Current children cumulated CPU time (s) 239.2
Current children cumulated vsize (Kb) 37632

[startup+250.02 s]
Raw data (loadavg): 0.99 0.89 0.90 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9147 0 0 0 24853 61 0 0 25 0 1 0 1728938123 37888000 9016 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9250 9016 145 145 0 9105 0
[pid=29121] vsize: 37000
Current children cumulated CPU time (s) 249.15
Current children cumulated vsize (Kb) 39124

[startup+260.021 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 25848 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 259.13
Current children cumulated vsize (Kb) 40212

[startup+270.021 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 26848 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 269.13
Current children cumulated vsize (Kb) 40212

[startup+280.022 s]
Raw data (loadavg): 0.99 0.90 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 27848 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 279.13
Current children cumulated vsize (Kb) 40212

[startup+290.023 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 28849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 289.14
Current children cumulated vsize (Kb) 40212

[startup+300.024 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 29849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 299.14
Current children cumulated vsize (Kb) 40212

[startup+310.025 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 30849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 309.14
Current children cumulated vsize (Kb) 40212

[startup+320.025 s]
Raw data (loadavg): 0.99 0.91 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 31849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 319.14
Current children cumulated vsize (Kb) 40212

[startup+330.026 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 32849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 329.14
Current children cumulated vsize (Kb) 40212

[startup+340.027 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 33849 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 339.14
Current children cumulated vsize (Kb) 40212

[startup+350.028 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 34850 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 349.15
Current children cumulated vsize (Kb) 40212

[startup+360.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 35850 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 359.15
Current children cumulated vsize (Kb) 40212

[startup+370.029 s]
Raw data (loadavg): 0.99 0.92 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9420 0 0 0 36850 64 0 0 25 0 1 0 1728938123 39002112 9289 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9522 9289 145 145 0 9377 0
[pid=29121] vsize: 38088
Current children cumulated CPU time (s) 369.15
Current children cumulated vsize (Kb) 40212

[startup+380.03 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 9820 0 0 0 37843 67 0 0 25 0 1 0 1728938123 40640512 9689 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 9922 9689 145 145 0 9777 0
[pid=29121] vsize: 39688
Current children cumulated CPU time (s) 379.11
Current children cumulated vsize (Kb) 41812

[startup+390.03 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 10150 0 0 0 38836 69 0 0 25 0 1 0 1728938123 41992192 10019 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 10252 10019 145 145 0 10107 0
[pid=29121] vsize: 41008
Current children cumulated CPU time (s) 389.06
Current children cumulated vsize (Kb) 43132

[startup+400.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 10372 0 0 0 39831 72 0 0 25 0 1 0 1728938123 42905600 10241 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 10475 10241 145 145 0 10330 0
[pid=29121] vsize: 41900
Current children cumulated CPU time (s) 399.04
Current children cumulated vsize (Kb) 44024

[startup+410.032 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 10698 0 0 0 40826 73 0 0 25 0 1 0 1728938123 44240896 10567 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 10801 10567 145 145 0 10656 0
[pid=29121] vsize: 43204
Current children cumulated CPU time (s) 409
Current children cumulated vsize (Kb) 45328

[startup+420.033 s]
Raw data (loadavg): 0.99 0.93 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 10962 0 0 0 41822 75 0 0 25 0 1 0 1728938123 45322240 10831 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 11065 10831 145 145 0 10920 0
[pid=29121] vsize: 44260
Current children cumulated CPU time (s) 418.98
Current children cumulated vsize (Kb) 46384

[startup+430.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 11382 0 0 0 42813 77 0 0 25 0 1 0 1728938123 47042560 11251 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 11485 11251 145 145 0 11340 0
[pid=29121] vsize: 45940
Current children cumulated CPU time (s) 428.91
Current children cumulated vsize (Kb) 48064

[startup+440.034 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 11814 0 0 0 43804 82 0 0 25 0 1 0 1728938123 48812032 11683 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 11917 11683 145 145 0 11772 0
[pid=29121] vsize: 47668
Current children cumulated CPU time (s) 438.87
Current children cumulated vsize (Kb) 49792

[startup+450.035 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 12270 0 0 0 44798 85 0 0 25 0 1 0 1728938123 50679808 12139 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 12373 12139 145 145 0 12228 0
[pid=29121] vsize: 49492
Current children cumulated CPU time (s) 448.84
Current children cumulated vsize (Kb) 51616

[startup+460.035 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 12702 0 0 0 45788 89 0 0 25 0 1 0 1728938123 52449280 12571 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 12805 12571 145 145 0 12660 0
[pid=29121] vsize: 51220
Current children cumulated CPU time (s) 458.78
Current children cumulated vsize (Kb) 53344

[startup+470.036 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 13114 0 0 0 46780 92 0 0 25 0 1 0 1728938123 54136832 12983 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 13217 12983 145 145 0 13072 0
[pid=29121] vsize: 52868
Current children cumulated CPU time (s) 468.73
Current children cumulated vsize (Kb) 54992

[startup+480.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 13545 0 0 0 47771 96 0 0 25 0 1 0 1728938123 55898112 13414 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 13647 13414 145 145 0 13502 0
[pid=29121] vsize: 54588
Current children cumulated CPU time (s) 478.68
Current children cumulated vsize (Kb) 56712

[startup+490.037 s]
Raw data (loadavg): 0.99 0.94 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 13973 0 0 0 48763 99 0 0 25 0 1 0 1728938123 57909248 13842 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 14138 13842 145 145 0 13993 0
[pid=29121] vsize: 56552
Current children cumulated CPU time (s) 488.63
Current children cumulated vsize (Kb) 58676

[startup+500.038 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 14428 0 0 0 49754 103 0 0 25 0 1 0 1728938123 59764736 14297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 14591 14297 145 145 0 14446 0
[pid=29121] vsize: 58364
Current children cumulated CPU time (s) 498.58
Current children cumulated vsize (Kb) 60488

[startup+510.038 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 14804 0 0 0 50748 106 0 0 25 0 1 0 1728938123 61304832 14673 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 14967 14673 145 145 0 14822 0
[pid=29121] vsize: 59868
Current children cumulated CPU time (s) 508.55
Current children cumulated vsize (Kb) 61992

[startup+520.04 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 15229 0 0 0 51740 109 0 0 25 0 1 0 1728938123 63037440 15098 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 15390 15098 145 145 0 15245 0
[pid=29121] vsize: 61560
Current children cumulated CPU time (s) 518.5
Current children cumulated vsize (Kb) 63684

[startup+530.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 15603 0 0 0 52734 112 0 0 25 0 1 0 1728938123 64561152 15472 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 15762 15472 145 145 0 15617 0
[pid=29121] vsize: 63048
Current children cumulated CPU time (s) 528.47
Current children cumulated vsize (Kb) 65172

[startup+540.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 15969 0 0 0 53727 114 0 0 25 0 1 0 1728938123 66060288 15838 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 16128 15838 145 145 0 15983 0
[pid=29121] vsize: 64512
Current children cumulated CPU time (s) 538.42
Current children cumulated vsize (Kb) 66636

[startup+550.041 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16355 0 0 0 54720 117 0 0 25 0 1 0 1728938123 67637248 16224 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16513 16224 145 145 0 16368 0
[pid=29121] vsize: 66052
Current children cumulated CPU time (s) 548.38
Current children cumulated vsize (Kb) 68176

[startup+560.042 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 55720 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 558.38
Current children cumulated vsize (Kb) 68372

[startup+570.043 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 56720 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 568.38
Current children cumulated vsize (Kb) 68372

[startup+580.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 57720 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 578.38
Current children cumulated vsize (Kb) 68372

[startup+590.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 58721 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 588.39
Current children cumulated vsize (Kb) 68372

[startup+600.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 59721 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 598.39
Current children cumulated vsize (Kb) 68372

[startup+610.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16404 0 0 0 60721 117 0 0 25 0 1 0 1728938123 67837952 16273 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16273 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 608.39
Current children cumulated vsize (Kb) 68372

[startup+620.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16406 0 0 0 61721 117 0 0 25 0 1 0 1728938123 67837952 16275 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16275 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 618.39
Current children cumulated vsize (Kb) 68372

[startup+630.047 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16406 0 0 0 62722 117 0 0 25 0 1 0 1728938123 67837952 16275 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16275 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 68372

[startup+640.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 63722 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 638.4
Current children cumulated vsize (Kb) 68372

[startup+650.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 64722 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 648.4
Current children cumulated vsize (Kb) 68372

[startup+660.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 65722 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 658.4
Current children cumulated vsize (Kb) 68372

[startup+670.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 66723 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 668.41
Current children cumulated vsize (Kb) 68372

[startup+680.051 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 67722 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 678.4
Current children cumulated vsize (Kb) 68372

[startup+690.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 68722 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 688.4
Current children cumulated vsize (Kb) 68372

[startup+700.052 s]
Raw data (loadavg): 0.99 0.96 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 69723 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 698.41
Current children cumulated vsize (Kb) 68372

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 70723 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 708.41
Current children cumulated vsize (Kb) 68372

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 71723 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 718.41
Current children cumulated vsize (Kb) 68372

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 72723 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 728.41
Current children cumulated vsize (Kb) 68372

[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 73724 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 738.42
Current children cumulated vsize (Kb) 68372

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 74724 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 748.42
Current children cumulated vsize (Kb) 68372

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 75724 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 758.42
Current children cumulated vsize (Kb) 68372

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 76725 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 768.43
Current children cumulated vsize (Kb) 68372

[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 77725 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 778.43
Current children cumulated vsize (Kb) 68372

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16407 0 0 0 78725 117 0 0 25 0 1 0 1728938123 67837952 16276 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16562 16276 145 145 0 16417 0
[pid=29121] vsize: 66248
Current children cumulated CPU time (s) 788.43
Current children cumulated vsize (Kb) 68372

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16494 0 0 0 79723 118 0 0 25 0 1 0 1728938123 68194304 16363 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 16649 16363 145 145 0 16504 0
[pid=29121] vsize: 66596
Current children cumulated CPU time (s) 798.42
Current children cumulated vsize (Kb) 68720

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 16884 0 0 0 80715 121 0 0 25 0 1 0 1728938123 69791744 16753 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 17039 16753 145 145 0 16894 0
[pid=29121] vsize: 68156
Current children cumulated CPU time (s) 808.37
Current children cumulated vsize (Kb) 70280

[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 17250 0 0 0 81709 124 0 0 25 0 1 0 1728938123 71290880 17119 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 17405 17119 145 145 0 17260 0
[pid=29121] vsize: 69620
Current children cumulated CPU time (s) 818.34
Current children cumulated vsize (Kb) 71744

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 17620 0 0 0 82704 126 0 0 25 0 1 0 1728938123 72806400 17489 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 17775 17489 145 145 0 17630 0
[pid=29121] vsize: 71100
Current children cumulated CPU time (s) 828.31
Current children cumulated vsize (Kb) 73224

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 18012 0 0 0 83697 129 0 0 25 0 1 0 1728938123 74416128 17881 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 18168 17881 145 145 0 18023 0
[pid=29121] vsize: 72672
Current children cumulated CPU time (s) 838.27
Current children cumulated vsize (Kb) 74796

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 18414 0 0 0 84690 132 0 0 25 0 1 0 1728938123 76066816 18283 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 18571 18283 145 145 0 18426 0
[pid=29121] vsize: 74284
Current children cumulated CPU time (s) 848.23
Current children cumulated vsize (Kb) 76408

[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 18792 0 0 0 85683 136 0 0 25 0 1 0 1728938123 77615104 18661 4294967295 134512640 135094434 3221224432 3221223024 134557386 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 18949 18661 145 145 0 18804 0
[pid=29121] vsize: 75796
Current children cumulated CPU time (s) 858.2
Current children cumulated vsize (Kb) 77920

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 19174 0 0 0 86676 139 0 0 25 0 1 0 1728938123 79179776 19043 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 19331 19043 145 145 0 19186 0
[pid=29121] vsize: 77324
Current children cumulated CPU time (s) 868.16
Current children cumulated vsize (Kb) 79448

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 19549 0 0 0 87669 142 0 0 25 0 1 0 1728938123 80719872 19418 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 19707 19418 145 145 0 19562 0
[pid=29121] vsize: 78828
Current children cumulated CPU time (s) 878.12
Current children cumulated vsize (Kb) 80952

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 19941 0 0 0 88662 145 0 0 25 0 1 0 1728938123 82325504 19810 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 20099 19810 145 145 0 19954 0
[pid=29121] vsize: 80396
Current children cumulated CPU time (s) 888.08
Current children cumulated vsize (Kb) 82520

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 20318 0 0 0 89652 149 0 0 25 0 1 0 1728938123 83869696 20187 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 20476 20187 145 145 0 20331 0
[pid=29121] vsize: 81904
Current children cumulated CPU time (s) 898.02
Current children cumulated vsize (Kb) 84028

[startup+910.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 20691 0 0 0 90645 152 0 0 25 0 1 0 1728938123 85393408 20560 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 20848 20560 145 145 0 20703 0
[pid=29121] vsize: 83392
Current children cumulated CPU time (s) 907.98
Current children cumulated vsize (Kb) 85516

[startup+920.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 21071 0 0 0 91639 154 0 0 25 0 1 0 1728938123 86941696 20940 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 21226 20940 145 145 0 21081 0
[pid=29121] vsize: 84904
Current children cumulated CPU time (s) 917.94
Current children cumulated vsize (Kb) 87028

[startup+930.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 21416 0 0 0 92633 156 0 0 25 0 1 0 1728938123 88367104 21285 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 21574 21285 145 145 0 21429 0
[pid=29121] vsize: 86296
Current children cumulated CPU time (s) 927.9
Current children cumulated vsize (Kb) 88420

[startup+940.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 21773 0 0 0 93625 159 0 0 25 0 1 0 1728938123 89833472 21642 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 21932 21642 145 145 0 21787 0
[pid=29121] vsize: 87728
Current children cumulated CPU time (s) 937.85
Current children cumulated vsize (Kb) 89852

[startup+950.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22136 0 0 0 94618 162 0 0 25 0 1 0 1728938123 91316224 22005 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22294 22005 145 145 0 22149 0
[pid=29121] vsize: 89176
Current children cumulated CPU time (s) 947.81
Current children cumulated vsize (Kb) 91300

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 95616 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 957.8
Current children cumulated vsize (Kb) 91820

[startup+970.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 96616 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 967.8
Current children cumulated vsize (Kb) 91820

[startup+980.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 97616 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 977.8
Current children cumulated vsize (Kb) 91820

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 98617 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 987.81
Current children cumulated vsize (Kb) 91820

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 99617 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 997.81
Current children cumulated vsize (Kb) 91820

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 100617 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1007.81
Current children cumulated vsize (Kb) 91820

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 101617 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1017.81
Current children cumulated vsize (Kb) 91820

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 102617 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1027.81
Current children cumulated vsize (Kb) 91820

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 103618 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1037.82
Current children cumulated vsize (Kb) 91820

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 104618 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1047.82
Current children cumulated vsize (Kb) 91820

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22267 0 0 0 105618 163 0 0 25 0 1 0 1728938123 91848704 22136 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22136 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1057.82
Current children cumulated vsize (Kb) 91820

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 106618 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1067.82
Current children cumulated vsize (Kb) 91820

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 107619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1077.83
Current children cumulated vsize (Kb) 91820

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 108619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1087.83
Current children cumulated vsize (Kb) 91820

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 109619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134557331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1097.83
Current children cumulated vsize (Kb) 91820

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 110619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1107.83
Current children cumulated vsize (Kb) 91820

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 111620 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1117.84
Current children cumulated vsize (Kb) 91820

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 112620 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1127.84
Current children cumulated vsize (Kb) 91820

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 113619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1137.83
Current children cumulated vsize (Kb) 91820

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 114619 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1147.83
Current children cumulated vsize (Kb) 91820

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 115620 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1157.84
Current children cumulated vsize (Kb) 91820

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 116620 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1167.84
Current children cumulated vsize (Kb) 91820

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 117620 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1177.84
Current children cumulated vsize (Kb) 91820

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 118621 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1187.85
Current children cumulated vsize (Kb) 91820

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 119621 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1197.85
Current children cumulated vsize (Kb) 91820

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 120621 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1207.85
Current children cumulated vsize (Kb) 91820



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.07 0.99 0.91 2/58 29121
Raw data (/proc/29117/stat): 29117 (minisat+_script) S 29116 29117 17733 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1728938118 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29117/statm): 531 226 485 147 0 384 0
[pid=29117] vsize: 2124
Raw data (/proc/29121/stat): 29121 (minisat+_64-bit) R 29117 29117 17733 0 -1 0 22269 0 0 0 120621 163 0 0 25 0 1 0 1728938123 91848704 22138 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29121/statm): 22424 22138 145 145 0 22279 0
[pid=29121] vsize: 89696
Current children cumulated CPU time (s) 1207.85
Current children cumulated vsize (Kb) 91820

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1207.89
CPU user time (s): 1206.22
CPU system time (s): 1.67574
CPU usage (%): 99.8144
Max. virtual memory (cumulated for all children) (Kb): 91820

Verifier Data

ERROR: no interpretation found !