Some explanations

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

General information on the benchmark

Namesubmitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb
MD5SUMa8596c98551f801a6658f1ce91b33278
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1053
Optimality of the best value was proved YES
Number of terms in the objective function 304
Biggest coefficient in the objective function 61
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 12887
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 12887
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark63.6713
Number of variables304
Total number of constraints671
Number of constraints which are clauses671
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint28

Trace number 2210

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        926432 kB
Buffers:         34384 kB
Cached:          46996 kB
SwapCached:        832 kB
Active:          60252 kB
Inactive:        23688 kB
HighTotal:      131008 kB
HighFree:        83300 kB
LowTotal:       903652 kB
LowFree:        843132 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18740 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:31:06 (client local time) WITH STATUS 10 IN 1208.94 SECONDS
stats: 2596 7 1208.94 10

Solver Data

c Parsing PB file...
c Converting 667 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     667     3359 |     222       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1524
c ---[   0]---> Sorter-cost:43621     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  105121   247278 |   35040       0        0     nan |  0.000 % |
c |       103 |  104168   245118 |   38544      97     4313    44.5 |  0.665 % |
c |       253 |  103349   243238 |   42398     229     8034    35.1 |  1.287 % |
c |       479 |  103349   243238 |   46638     455    17849    39.2 |  1.287 % |
c |       816 |  103349   243238 |   51302     792    23717    29.9 |  1.287 % |
c |      1322 |  103349   243238 |   56432    1298    40177    31.0 |  1.287 % |
c |      2083 |  103122   242717 |   62075    2058    75941    36.9 |  1.487 % |
c |      3222 |  102780   241953 |   68283    3169   126886    40.0 |  1.754 % |
c |      4932 |  102722   241821 |   75111    4870   197921    40.6 |  1.797 % |
c |      7495 |  102722   241821 |   82622    7433   294908    39.7 |  1.797 % |
c ==============================================================================
c Found solution: 1514
c ---[   0]---> Sorter-cost:36082     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8239 |  189796   445156 |   63265    8177   316528    38.7 |  1.797 % |
c |      8339 |  189796   445156 |   69591    8277   322185    38.9 |  1.049 % |
c |      8490 |  189796   445156 |   76550    8428   326473    38.7 |  1.049 % |
c |      8715 |  189774   445107 |   84205    8650   331229    38.3 |  1.059 % |
c |      9052 |  189647   444838 |   92626    8982   333087    37.1 |  1.125 % |
c |      9558 |  189568   444660 |  101888    9486   337879    35.6 |  1.152 % |
c ==============================================================================
c Found solution: 1498
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9601 |  189573   444797 |   63191    9529   339448    35.6 |  1.152 % |
c ==============================================================================
c Found solution: 1490
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9608 |  189907   445610 |   63302    9536   339814    35.6 |  1.152 % |
c ==============================================================================
c Found solution: 1450
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9611 |  189928   445664 |   63309    9539   340630    35.7 |  1.152 % |
c ==============================================================================
c Found solution: 1416
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9623 |  190264   446559 |   63421    9551   341049    35.7 |  1.152 % |
c |      9724 |  190264   446559 |   69763    9652   348331    36.1 |  1.152 % |
c |      9874 |  190264   446559 |   76739    9802   364696    37.2 |  1.152 % |
c |     10099 |  190252   446532 |   84413   10026   380599    38.0 |  1.157 % |
c |     10439 |  190252   446532 |   92854   10366   387470    37.4 |  1.157 % |
c |     10945 |  190252   446532 |  102140   10872   406819    37.4 |  1.157 % |
c ==============================================================================
c Found solution: 1326
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11585 |  190286   446619 |   63428   11512   555064    48.2 |  1.157 % |
c |     11686 |  190286   446619 |   69770   11613   558245    48.1 |  1.158 % |
c |     11839 |  190286   446619 |   76747   11766   566083    48.1 |  1.158 % |
c |     12064 |  190286   446619 |   84422   11991   577304    48.1 |  1.158 % |
c |     12402 |  190286   446619 |   92864   12329   581418    47.2 |  1.158 % |
c |     12908 |  190258   446556 |  102151   12834   604153    47.1 |  1.167 % |
c |     13667 |  190204   446436 |  112366   13589   636533    46.8 |  1.190 % |
c |     14806 |  190153   446322 |  123603   14720   668941    45.4 |  1.212 % |
c |     16514 |  189969   445907 |  135963   16409   754857    46.0 |  1.289 % |
c |     19076 |  189969   445907 |  149559   18971   880480    46.4 |  1.289 % |
c |     22921 |  189969   445907 |  164515   22816  1083581    47.5 |  1.289 % |
c |     28688 |  189969   445907 |  180967   28583  1429962    50.0 |  1.289 % |
c |     37340 |  189969   445907 |  199064   37235  2157656    57.9 |  1.289 % |
c |     50318 |  189969   445907 |  218970   50213  4133473    82.3 |  1.289 % |
c |     69780 |  189969   445907 |  240867   69675  7316398   105.0 |  1.289 % |
c |     98972 |  189969   445907 |  264954   98867  9521248    96.3 |  1.289 % |

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/11662/stat): 11662 (minisat+_script) R 11661 11662 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843295459 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/11662/statm): 174 3 169 147 0 27 0
[pid=11662] 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=11663
New process pid=11664
New process pid=11665
execve syscall for /bin/sed executable
One traced child (pid=11664) 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=11665) exited with status: 0
One traced child (pid=11663) exited with status: 0
New process pid=11666
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-cmb.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3594 0 0 0 968 14 0 0 25 0 1 0 1843295464 15970304 3368 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 3899 3368 145 145 0 3754 0
[pid=11666] vsize: 15596
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 17720

[startup+20.0061 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3720 0 0 0 1965 15 0 0 25 0 1 0 1843295464 16494592 3494 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 4027 3494 145 145 0 3882 0
[pid=11666] vsize: 16108
Current children cumulated CPU time (s) 19.81
Current children cumulated vsize (Kb) 18232

[startup+30.0069 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3881 0 0 0 2962 17 0 0 25 0 1 0 1843295464 17154048 3655 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 4188 3655 145 145 0 4043 0
[pid=11666] vsize: 16752
Current children cumulated CPU time (s) 29.8
Current children cumulated vsize (Kb) 18876

[startup+40.0077 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6367 0 0 0 3942 27 0 0 25 0 1 0 1843295464 30191616 6099 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7371 6099 145 145 0 7226 0
[pid=11666] vsize: 29484
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 31608

[startup+50.0095 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6675 0 0 0 4941 28 0 0 25 0 1 0 1843295464 30900224 6281 4294967295 134512640 135094434 3221224448 3221223072 134557619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7544 6281 145 145 0 7399 0
[pid=11666] vsize: 30176
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 32300

[startup+60.0103 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6760 0 0 0 5939 29 0 0 25 0 1 0 1843295464 31248384 6366 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7629 6366 145 145 0 7484 0
[pid=11666] vsize: 30516
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 32640

[startup+70.0121 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6953 0 0 0 6937 30 0 0 25 0 1 0 1843295464 31760384 6492 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7754 6492 145 145 0 7609 0
[pid=11666] vsize: 31016
Current children cumulated CPU time (s) 69.68
Current children cumulated vsize (Kb) 33140

[startup+80.0129 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7029 0 0 0 7935 31 0 0 25 0 1 0 1843295464 32063488 6568 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7828 6568 145 145 0 7683 0
[pid=11666] vsize: 31312
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 33436

[startup+90.0127 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7086 0 0 0 8934 32 0 0 25 0 1 0 1843295464 32292864 6625 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7884 6625 145 145 0 7739 0
[pid=11666] vsize: 31536
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 33660

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7165 0 0 0 9933 33 0 0 25 0 1 0 1843295464 32677888 6704 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 7978 6704 145 145 0 7833 0
[pid=11666] vsize: 31912
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 34036

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7233 0 0 0 10932 33 0 0 25 0 1 0 1843295464 32948224 6772 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8044 6772 145 145 0 7899 0
[pid=11666] vsize: 32176
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 34300

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7292 0 0 0 11931 34 0 0 25 0 1 0 1843295464 33185792 6831 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8102 6831 145 145 0 7957 0
[pid=11666] vsize: 32408
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 34532

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7346 0 0 0 12931 34 0 0 25 0 1 0 1843295464 33406976 6885 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8156 6885 145 145 0 8011 0
[pid=11666] vsize: 32624
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 34748

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7409 0 0 0 13930 35 0 0 25 0 1 0 1843295464 33660928 6948 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8218 6948 145 145 0 8073 0
[pid=11666] vsize: 32872
Current children cumulated CPU time (s) 139.66
Current children cumulated vsize (Kb) 34996

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7479 0 0 0 14928 35 0 0 25 0 1 0 1843295464 33943552 7018 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8287 7018 145 145 0 8142 0
[pid=11666] vsize: 33148
Current children cumulated CPU time (s) 149.64
Current children cumulated vsize (Kb) 35272

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7560 0 0 0 15927 36 0 0 25 0 1 0 1843295464 34267136 7099 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8366 7099 145 145 0 8221 0
[pid=11666] vsize: 33464
Current children cumulated CPU time (s) 159.64
Current children cumulated vsize (Kb) 35588

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7645 0 0 0 16926 37 0 0 25 0 1 0 1843295464 34611200 7184 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8450 7184 145 145 0 8305 0
[pid=11666] vsize: 33800
Current children cumulated CPU time (s) 169.64
Current children cumulated vsize (Kb) 35924

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7722 0 0 0 17925 37 0 0 25 0 1 0 1843295464 34922496 7261 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8526 7261 145 145 0 8381 0
[pid=11666] vsize: 34104
Current children cumulated CPU time (s) 179.63
Current children cumulated vsize (Kb) 36228

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7823 0 0 0 18923 38 0 0 25 0 1 0 1843295464 35332096 7362 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8626 7362 145 145 0 8481 0
[pid=11666] vsize: 34504
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 36628

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7933 0 0 0 19921 40 0 0 25 0 1 0 1843295464 35778560 7472 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8735 7472 145 145 0 8590 0
[pid=11666] vsize: 34940
Current children cumulated CPU time (s) 199.62
Current children cumulated vsize (Kb) 37064

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8009 0 0 0 20920 40 0 0 25 0 1 0 1843295464 36085760 7548 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8810 7548 145 145 0 8665 0
[pid=11666] vsize: 35240
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 37364

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8082 0 0 0 21918 41 0 0 25 0 1 0 1843295464 36388864 7621 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8884 7621 145 145 0 8739 0
[pid=11666] vsize: 35536
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 37660

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8166 0 0 0 22917 42 0 0 25 0 1 0 1843295464 36728832 7705 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 8967 7705 145 145 0 8822 0
[pid=11666] vsize: 35868
Current children cumulated CPU time (s) 229.6
Current children cumulated vsize (Kb) 37992

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8247 0 0 0 23915 43 0 0 25 0 1 0 1843295464 37056512 7786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9047 7786 145 145 0 8902 0
[pid=11666] vsize: 36188
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 38312

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8319 0 0 0 24915 43 0 0 25 0 1 0 1843295464 37351424 7858 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9119 7858 145 145 0 8974 0
[pid=11666] vsize: 36476
Current children cumulated CPU time (s) 249.59
Current children cumulated vsize (Kb) 38600

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8407 0 0 0 25914 44 0 0 25 0 1 0 1843295464 37838848 7946 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9238 7946 145 145 0 9093 0
[pid=11666] vsize: 36952
Current children cumulated CPU time (s) 259.59
Current children cumulated vsize (Kb) 39076

[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8454 0 0 0 26913 44 0 0 25 0 1 0 1843295464 38031360 7993 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9285 7993 145 145 0 9140 0
[pid=11666] vsize: 37140
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 39264

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8533 0 0 0 27912 45 0 0 25 0 1 0 1843295464 38350848 8072 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9363 8072 145 145 0 9218 0
[pid=11666] vsize: 37452
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 39576

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8602 0 0 0 28910 46 0 0 25 0 1 0 1843295464 38629376 8141 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9431 8141 145 145 0 9286 0
[pid=11666] vsize: 37724
Current children cumulated CPU time (s) 289.57
Current children cumulated vsize (Kb) 39848

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8661 0 0 0 29909 47 0 0 25 0 1 0 1843295464 38871040 8200 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9490 8200 145 145 0 9345 0
[pid=11666] vsize: 37960
Current children cumulated CPU time (s) 299.57
Current children cumulated vsize (Kb) 40084

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8731 0 0 0 30908 48 0 0 25 0 1 0 1843295464 39153664 8270 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9559 8270 145 145 0 9414 0
[pid=11666] vsize: 38236
Current children cumulated CPU time (s) 309.57
Current children cumulated vsize (Kb) 40360

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8794 0 0 0 31907 48 0 0 25 0 1 0 1843295464 39403520 8333 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9620 8333 145 145 0 9475 0
[pid=11666] vsize: 38480
Current children cumulated CPU time (s) 319.56
Current children cumulated vsize (Kb) 40604

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8866 0 0 0 32906 48 0 0 25 0 1 0 1843295464 39694336 8405 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9691 8405 145 145 0 9546 0
[pid=11666] vsize: 38764
Current children cumulated CPU time (s) 329.55
Current children cumulated vsize (Kb) 40888

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8933 0 0 0 33904 49 0 0 25 0 1 0 1843295464 39964672 8472 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9757 8472 145 145 0 9612 0
[pid=11666] vsize: 39028
Current children cumulated CPU time (s) 339.54
Current children cumulated vsize (Kb) 41152

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9020 0 0 0 34903 50 0 0 25 0 1 0 1843295464 40316928 8559 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9843 8559 145 145 0 9698 0
[pid=11666] vsize: 39372
Current children cumulated CPU time (s) 349.54
Current children cumulated vsize (Kb) 41496

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9128 0 0 0 35901 51 0 0 25 0 1 0 1843295464 40755200 8667 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 9950 8667 145 145 0 9805 0
[pid=11666] vsize: 39800
Current children cumulated CPU time (s) 359.53
Current children cumulated vsize (Kb) 41924

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9239 0 0 0 36899 52 0 0 25 0 1 0 1843295464 41205760 8778 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10060 8778 145 145 0 9915 0
[pid=11666] vsize: 40240
Current children cumulated CPU time (s) 369.52
Current children cumulated vsize (Kb) 42364

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9330 0 0 0 37898 52 0 0 25 0 1 0 1843295464 41574400 8869 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10150 8869 145 145 0 10005 0
[pid=11666] vsize: 40600
Current children cumulated CPU time (s) 379.51
Current children cumulated vsize (Kb) 42724

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9470 0 0 0 38895 53 0 0 25 0 1 0 1843295464 42147840 9009 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10290 9009 145 145 0 10145 0
[pid=11666] vsize: 41160
Current children cumulated CPU time (s) 389.49
Current children cumulated vsize (Kb) 43284

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9624 0 0 0 39893 54 0 0 25 0 1 0 1843295464 42774528 9163 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10443 9163 145 145 0 10298 0
[pid=11666] vsize: 41772
Current children cumulated CPU time (s) 399.48
Current children cumulated vsize (Kb) 43896

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9775 0 0 0 40891 55 0 0 25 0 1 0 1843295464 43388928 9314 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10593 9314 145 145 0 10448 0
[pid=11666] vsize: 42372
Current children cumulated CPU time (s) 409.47
Current children cumulated vsize (Kb) 44496

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9903 0 0 0 41889 57 0 0 25 0 1 0 1843295464 43913216 9442 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10721 9442 145 145 0 10576 0
[pid=11666] vsize: 42884
Current children cumulated CPU time (s) 419.47
Current children cumulated vsize (Kb) 45008

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10028 0 0 0 42887 57 0 0 25 0 1 0 1843295464 44421120 9567 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10845 9567 145 145 0 10700 0
[pid=11666] vsize: 43380
Current children cumulated CPU time (s) 429.45
Current children cumulated vsize (Kb) 45504

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10171 0 0 0 43885 58 0 0 25 0 1 0 1843295464 45002752 9710 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 10987 9710 145 145 0 10842 0
[pid=11666] vsize: 43948
Current children cumulated CPU time (s) 439.44
Current children cumulated vsize (Kb) 46072

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10332 0 0 0 44882 59 0 0 25 0 1 0 1843295464 45662208 9871 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11148 9871 145 145 0 11003 0
[pid=11666] vsize: 44592
Current children cumulated CPU time (s) 449.42
Current children cumulated vsize (Kb) 46716

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10480 0 0 0 45879 61 0 0 25 0 1 0 1843295464 46264320 10019 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11295 10019 145 145 0 11150 0
[pid=11666] vsize: 45180
Current children cumulated CPU time (s) 459.41
Current children cumulated vsize (Kb) 47304

[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10654 0 0 0 46876 63 0 0 25 0 1 0 1843295464 46989312 10193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11472 10193 145 145 0 11327 0
[pid=11666] vsize: 45888
Current children cumulated CPU time (s) 469.4
Current children cumulated vsize (Kb) 48012

[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10796 0 0 0 47874 64 0 0 25 0 1 0 1843295464 47562752 10335 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11612 10335 145 145 0 11467 0
[pid=11666] vsize: 46448
Current children cumulated CPU time (s) 479.39
Current children cumulated vsize (Kb) 48572

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10929 0 0 0 48872 65 0 0 25 0 1 0 1843295464 48115712 10468 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11747 10468 145 145 0 11602 0
[pid=11666] vsize: 46988
Current children cumulated CPU time (s) 489.38
Current children cumulated vsize (Kb) 49112

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11029 0 0 0 49870 66 0 0 25 0 1 0 1843295464 48517120 10568 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11845 10568 145 145 0 11700 0
[pid=11666] vsize: 47380
Current children cumulated CPU time (s) 499.37
Current children cumulated vsize (Kb) 49504

[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11118 0 0 0 50868 67 0 0 25 0 1 0 1843295464 48877568 10657 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 11933 10657 145 145 0 11788 0
[pid=11666] vsize: 47732
Current children cumulated CPU time (s) 509.36
Current children cumulated vsize (Kb) 49856

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11228 0 0 0 51866 68 0 0 25 0 1 0 1843295464 49324032 10767 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12042 10767 145 145 0 11897 0
[pid=11666] vsize: 48168
Current children cumulated CPU time (s) 519.35
Current children cumulated vsize (Kb) 50292

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11402 0 0 0 52864 70 0 0 19 0 1 0 1843295464 50032640 10941 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 12215 10941 145 145 0 12070 0
[pid=11666] vsize: 48860
Current children cumulated CPU time (s) 529.35
Current children cumulated vsize (Kb) 50984

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11525 0 0 0 53862 71 0 0 25 0 1 0 1843295464 50528256 11064 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12336 11064 145 145 0 12191 0
[pid=11666] vsize: 49344
Current children cumulated CPU time (s) 539.34
Current children cumulated vsize (Kb) 51468

[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11615 0 0 0 54860 72 0 0 25 0 1 0 1843295464 50892800 11154 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12425 11154 145 145 0 12280 0
[pid=11666] vsize: 49700
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 51824

[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11715 0 0 0 55858 73 0 0 25 0 1 0 1843295464 51302400 11254 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12525 11254 145 145 0 12380 0
[pid=11666] vsize: 50100
Current children cumulated CPU time (s) 559.32
Current children cumulated vsize (Kb) 52224

[startup+570.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11846 0 0 0 56856 74 0 0 25 0 1 0 1843295464 51838976 11385 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12656 11385 145 145 0 12511 0
[pid=11666] vsize: 50624
Current children cumulated CPU time (s) 569.31
Current children cumulated vsize (Kb) 52748

[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11976 0 0 0 57854 75 0 0 25 0 1 0 1843295464 52363264 11515 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12784 11515 145 145 0 12639 0
[pid=11666] vsize: 51136
Current children cumulated CPU time (s) 579.3
Current children cumulated vsize (Kb) 53260

[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12108 0 0 0 58853 76 0 0 25 0 1 0 1843295464 52899840 11647 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 12915 11647 145 145 0 12770 0
[pid=11666] vsize: 51660
Current children cumulated CPU time (s) 589.3
Current children cumulated vsize (Kb) 53784

[startup+600.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12249 0 0 0 59850 76 0 0 25 0 1 0 1843295464 53477376 11788 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13056 11788 145 145 0 12911 0
[pid=11666] vsize: 52224
Current children cumulated CPU time (s) 599.27
Current children cumulated vsize (Kb) 54348

[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12405 0 0 0 60848 78 0 0 25 0 1 0 1843295464 54112256 11944 4294967295 134512640 135094434 3221224448 3221223040 134557133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13211 11944 145 145 0 13066 0
[pid=11666] vsize: 52844
Current children cumulated CPU time (s) 609.27
Current children cumulated vsize (Kb) 54968

[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12543 0 0 0 61845 79 0 0 25 0 1 0 1843295464 54677504 12082 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13349 12082 145 145 0 13204 0
[pid=11666] vsize: 53396
Current children cumulated CPU time (s) 619.25
Current children cumulated vsize (Kb) 55520

[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12704 0 0 0 62843 79 0 0 25 0 1 0 1843295464 55377920 12243 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13520 12243 145 145 0 13375 0
[pid=11666] vsize: 54080
Current children cumulated CPU time (s) 629.23
Current children cumulated vsize (Kb) 56204

[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12841 0 0 0 63841 80 0 0 25 0 1 0 1843295464 55934976 12380 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13656 12380 145 145 0 13511 0
[pid=11666] vsize: 54624
Current children cumulated CPU time (s) 639.22
Current children cumulated vsize (Kb) 56748

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12965 0 0 0 64840 81 0 0 25 0 1 0 1843295464 56438784 12504 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13779 12504 145 145 0 13634 0
[pid=11666] vsize: 55116
Current children cumulated CPU time (s) 649.22
Current children cumulated vsize (Kb) 57240

[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13100 0 0 0 65837 82 0 0 25 0 1 0 1843295464 56995840 12639 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 13915 12639 145 145 0 13770 0
[pid=11666] vsize: 55660
Current children cumulated CPU time (s) 659.2
Current children cumulated vsize (Kb) 57784

[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13284 0 0 0 66835 83 0 0 25 0 1 0 1843295464 57757696 12823 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 14101 12823 145 145 0 13956 0
[pid=11666] vsize: 56404
Current children cumulated CPU time (s) 669.19
Current children cumulated vsize (Kb) 58528

[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13457 0 0 0 67832 85 0 0 25 0 1 0 1843295464 58728448 12996 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 14338 12996 145 145 0 14193 0
[pid=11666] vsize: 57352
Current children cumulated CPU time (s) 679.18
Current children cumulated vsize (Kb) 59476

[startup+690.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13609 0 0 0 68830 87 0 0 25 0 1 0 1843295464 59342848 13148 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 14488 13148 145 145 0 14343 0
[pid=11666] vsize: 57952
Current children cumulated CPU time (s) 689.18
Current children cumulated vsize (Kb) 60076

[startup+700.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13769 0 0 0 69828 88 0 0 25 0 1 0 1843295464 59990016 13308 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 14646 13308 145 145 0 14501 0
[pid=11666] vsize: 58584
Current children cumulated CPU time (s) 699.17
Current children cumulated vsize (Kb) 60708

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13897 0 0 0 70824 89 0 0 25 0 1 0 1843295464 60510208 13436 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 14773 13436 145 145 0 14628 0
[pid=11666] vsize: 59092
Current children cumulated CPU time (s) 709.14
Current children cumulated vsize (Kb) 61216

[startup+720.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14052 0 0 0 71823 90 0 0 25 0 1 0 1843295464 61140992 13591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 14927 13591 145 145 0 14782 0
[pid=11666] vsize: 59708
Current children cumulated CPU time (s) 719.14
Current children cumulated vsize (Kb) 61832

[startup+730.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14188 0 0 0 72820 91 0 0 25 0 1 0 1843295464 61698048 13727 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15063 13727 145 145 0 14918 0
[pid=11666] vsize: 60252
Current children cumulated CPU time (s) 729.12
Current children cumulated vsize (Kb) 62376

[startup+740.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14292 0 0 0 73817 92 0 0 25 0 1 0 1843295464 62140416 13831 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 15171 13831 145 145 0 15026 0
[pid=11666] vsize: 60684
Current children cumulated CPU time (s) 739.1
Current children cumulated vsize (Kb) 62808

[startup+750.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14343 0 0 0 74815 93 0 0 25 0 1 0 1843295464 62345216 13882 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 15221 13882 145 145 0 15076 0
[pid=11666] vsize: 60884
Current children cumulated CPU time (s) 749.09
Current children cumulated vsize (Kb) 63008

[startup+760.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14394 0 0 0 75814 94 0 0 25 0 1 0 1843295464 62554112 13933 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15272 13933 145 145 0 15127 0
[pid=11666] vsize: 61088
Current children cumulated CPU time (s) 759.09
Current children cumulated vsize (Kb) 63212

[startup+770.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14446 0 0 0 76813 94 0 0 25 0 1 0 1843295464 62763008 13985 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15323 13985 145 145 0 15178 0
[pid=11666] vsize: 61292
Current children cumulated CPU time (s) 769.08
Current children cumulated vsize (Kb) 63416

[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14502 0 0 0 77813 94 0 0 25 0 1 0 1843295464 62988288 14041 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15378 14041 145 145 0 15233 0
[pid=11666] vsize: 61512
Current children cumulated CPU time (s) 779.08
Current children cumulated vsize (Kb) 63636

[startup+790.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14563 0 0 0 78811 95 0 0 25 0 1 0 1843295464 63238144 14102 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15439 14102 145 145 0 15294 0
[pid=11666] vsize: 61756
Current children cumulated CPU time (s) 789.07
Current children cumulated vsize (Kb) 63880

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14614 0 0 0 79811 95 0 0 25 0 1 0 1843295464 63451136 14153 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15491 14153 145 145 0 15346 0
[pid=11666] vsize: 61964
Current children cumulated CPU time (s) 799.07
Current children cumulated vsize (Kb) 64088

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14671 0 0 0 80810 96 0 0 25 0 1 0 1843295464 63680512 14210 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15547 14210 145 145 0 15402 0
[pid=11666] vsize: 62188
Current children cumulated CPU time (s) 809.07
Current children cumulated vsize (Kb) 64312

[startup+820.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14731 0 0 0 81809 96 0 0 25 0 1 0 1843295464 63926272 14270 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15607 14270 145 145 0 15462 0
[pid=11666] vsize: 62428
Current children cumulated CPU time (s) 819.06
Current children cumulated vsize (Kb) 64552

[startup+830.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14782 0 0 0 82808 97 0 0 25 0 1 0 1843295464 64135168 14321 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15658 14321 145 145 0 15513 0
[pid=11666] vsize: 62632
Current children cumulated CPU time (s) 829.06
Current children cumulated vsize (Kb) 64756

[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14835 0 0 0 83808 97 0 0 25 0 1 0 1843295464 64348160 14374 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15710 14374 145 145 0 15565 0
[pid=11666] vsize: 62840
Current children cumulated CPU time (s) 839.06
Current children cumulated vsize (Kb) 64964

[startup+850.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14881 0 0 0 84807 97 0 0 25 0 1 0 1843295464 64536576 14420 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15756 14420 145 145 0 15611 0
[pid=11666] vsize: 63024
Current children cumulated CPU time (s) 849.05
Current children cumulated vsize (Kb) 65148

[startup+860.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14955 0 0 0 85806 98 0 0 25 0 1 0 1843295464 64831488 14494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15828 14494 145 145 0 15683 0
[pid=11666] vsize: 63312
Current children cumulated CPU time (s) 859.05
Current children cumulated vsize (Kb) 65436

[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15014 0 0 0 86804 99 0 0 25 0 1 0 1843295464 65069056 14553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15886 14553 145 145 0 15741 0
[pid=11666] vsize: 63544
Current children cumulated CPU time (s) 869.04
Current children cumulated vsize (Kb) 65668

[startup+880.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15064 0 0 0 87804 99 0 0 25 0 1 0 1843295464 65273856 14603 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15936 14603 145 145 0 15791 0
[pid=11666] vsize: 63744
Current children cumulated CPU time (s) 879.04
Current children cumulated vsize (Kb) 65868

[startup+890.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15116 0 0 0 88803 99 0 0 25 0 1 0 1843295464 65482752 14655 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 15987 14655 145 145 0 15842 0
[pid=11666] vsize: 63948
Current children cumulated CPU time (s) 889.03
Current children cumulated vsize (Kb) 66072

[startup+900.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15171 0 0 0 89802 100 0 0 25 0 1 0 1843295464 65703936 14710 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16041 14710 145 145 0 15896 0
[pid=11666] vsize: 64164
Current children cumulated CPU time (s) 899.03
Current children cumulated vsize (Kb) 66288

[startup+910.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15222 0 0 0 90801 100 0 0 25 0 1 0 1843295464 65912832 14761 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16092 14761 145 145 0 15947 0
[pid=11666] vsize: 64368
Current children cumulated CPU time (s) 909.02
Current children cumulated vsize (Kb) 66492

[startup+920.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15268 0 0 0 91801 100 0 0 25 0 1 0 1843295464 66097152 14807 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16137 14807 145 145 0 15992 0
[pid=11666] vsize: 64548
Current children cumulated CPU time (s) 919.02
Current children cumulated vsize (Kb) 66672

[startup+930.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15318 0 0 0 92801 101 0 0 25 0 1 0 1843295464 66301952 14857 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16187 14857 145 145 0 16042 0
[pid=11666] vsize: 64748
Current children cumulated CPU time (s) 929.03
Current children cumulated vsize (Kb) 66872

[startup+940.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15359 0 0 0 93800 101 0 0 25 0 1 0 1843295464 66461696 14898 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16226 14898 145 145 0 16081 0
[pid=11666] vsize: 64904
Current children cumulated CPU time (s) 939.02
Current children cumulated vsize (Kb) 67028

[startup+950.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15405 0 0 0 94800 101 0 0 25 0 1 0 1843295464 66646016 14944 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16271 14944 145 145 0 16126 0
[pid=11666] vsize: 65084
Current children cumulated CPU time (s) 949.02
Current children cumulated vsize (Kb) 67208

[startup+960.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15446 0 0 0 95799 101 0 0 25 0 1 0 1843295464 66818048 14985 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16313 14985 145 145 0 16168 0
[pid=11666] vsize: 65252
Current children cumulated CPU time (s) 959.01
Current children cumulated vsize (Kb) 67376

[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15521 0 0 0 96798 102 0 0 25 0 1 0 1843295464 67121152 15060 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16387 15060 145 145 0 16242 0
[pid=11666] vsize: 65548
Current children cumulated CPU time (s) 969.01
Current children cumulated vsize (Kb) 67672

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15577 0 0 0 97798 102 0 0 25 0 1 0 1843295464 67350528 15116 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16443 15116 145 145 0 16298 0
[pid=11666] vsize: 65772
Current children cumulated CPU time (s) 979.01
Current children cumulated vsize (Kb) 67896

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15627 0 0 0 98797 103 0 0 25 0 1 0 1843295464 67551232 15166 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16492 15166 145 145 0 16347 0
[pid=11666] vsize: 65968
Current children cumulated CPU time (s) 989.01
Current children cumulated vsize (Kb) 68092

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15682 0 0 0 99796 103 0 0 25 0 1 0 1843295464 67772416 15221 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16546 15221 145 145 0 16401 0
[pid=11666] vsize: 66184
Current children cumulated CPU time (s) 999
Current children cumulated vsize (Kb) 68308

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15739 0 0 0 100795 103 0 0 25 0 1 0 1843295464 68001792 15278 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16602 15278 145 145 0 16457 0
[pid=11666] vsize: 66408
Current children cumulated CPU time (s) 1008.99
Current children cumulated vsize (Kb) 68532

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15800 0 0 0 101794 104 0 0 25 0 1 0 1843295464 68247552 15339 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16662 15339 145 145 0 16517 0
[pid=11666] vsize: 66648
Current children cumulated CPU time (s) 1018.99
Current children cumulated vsize (Kb) 68772

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15864 0 0 0 102792 105 0 0 25 0 1 0 1843295464 68509696 15403 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16726 15403 145 145 0 16581 0
[pid=11666] vsize: 66904
Current children cumulated CPU time (s) 1028.98
Current children cumulated vsize (Kb) 69028

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15925 0 0 0 103791 105 0 0 25 0 1 0 1843295464 68759552 15464 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16787 15464 145 145 0 16642 0
[pid=11666] vsize: 67148
Current children cumulated CPU time (s) 1038.97
Current children cumulated vsize (Kb) 69272

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15997 0 0 0 104790 106 0 0 25 0 1 0 1843295464 69050368 15536 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16858 15536 145 145 0 16713 0
[pid=11666] vsize: 67432
Current children cumulated CPU time (s) 1048.97
Current children cumulated vsize (Kb) 69556

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16077 0 0 0 105788 107 0 0 25 0 1 0 1843295464 69373952 15616 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16937 15616 145 145 0 16792 0
[pid=11666] vsize: 67748
Current children cumulated CPU time (s) 1058.96
Current children cumulated vsize (Kb) 69872

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16138 0 0 0 106787 108 0 0 25 0 1 0 1843295464 69623808 15677 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 16998 15677 145 145 0 16853 0
[pid=11666] vsize: 67992
Current children cumulated CPU time (s) 1068.96
Current children cumulated vsize (Kb) 70116

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16195 0 0 0 107787 108 0 0 25 0 1 0 1843295464 69853184 15734 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 17054 15734 145 145 0 16909 0
[pid=11666] vsize: 68216
Current children cumulated CPU time (s) 1078.96
Current children cumulated vsize (Kb) 70340

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16261 0 0 0 108787 108 0 0 25 0 1 0 1843295464 70131712 15800 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11666/statm): 17122 15800 145 145 0 16977 0
[pid=11666] vsize: 68488
Current children cumulated CPU time (s) 1088.96
Current children cumulated vsize (Kb) 70612

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16326 0 0 0 109786 109 0 0 25 0 1 0 1843295464 70393856 15865 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17186 15865 145 145 0 17041 0
[pid=11666] vsize: 68744
Current children cumulated CPU time (s) 1098.96
Current children cumulated vsize (Kb) 70868

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16380 0 0 0 110785 109 0 0 25 0 1 0 1843295464 70615040 15919 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17240 15919 145 145 0 17095 0
[pid=11666] vsize: 68960
Current children cumulated CPU time (s) 1108.95
Current children cumulated vsize (Kb) 71084

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16444 0 0 0 111783 110 0 0 25 0 1 0 1843295464 70868992 15983 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17302 15983 145 145 0 17157 0
[pid=11666] vsize: 69208
Current children cumulated CPU time (s) 1118.94
Current children cumulated vsize (Kb) 71332

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16498 0 0 0 112782 111 0 0 25 0 1 0 1843295464 71081984 16037 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17354 16037 145 145 0 17209 0
[pid=11666] vsize: 69416
Current children cumulated CPU time (s) 1128.94
Current children cumulated vsize (Kb) 71540

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16554 0 0 0 113781 112 0 0 25 0 1 0 1843295464 71311360 16093 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17410 16093 145 145 0 17265 0
[pid=11666] vsize: 69640
Current children cumulated CPU time (s) 1138.94
Current children cumulated vsize (Kb) 71764

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16611 0 0 0 114779 113 0 0 25 0 1 0 1843295464 71544832 16150 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17467 16150 145 145 0 17322 0
[pid=11666] vsize: 69868
Current children cumulated CPU time (s) 1148.93
Current children cumulated vsize (Kb) 71992

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16662 0 0 0 115778 114 0 0 25 0 1 0 1843295464 71753728 16201 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17518 16201 145 145 0 17373 0
[pid=11666] vsize: 70072
Current children cumulated CPU time (s) 1158.93
Current children cumulated vsize (Kb) 72196

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16715 0 0 0 116776 115 0 0 25 0 1 0 1843295464 71966720 16254 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17570 16254 145 145 0 17425 0
[pid=11666] vsize: 70280
Current children cumulated CPU time (s) 1168.92
Current children cumulated vsize (Kb) 72404

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16780 0 0 0 117775 115 0 0 25 0 1 0 1843295464 72249344 16319 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17639 16319 145 145 0 17494 0
[pid=11666] vsize: 70556
Current children cumulated CPU time (s) 1178.91
Current children cumulated vsize (Kb) 72680

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16832 0 0 0 118774 116 0 0 25 0 1 0 1843295464 72454144 16371 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17689 16371 145 145 0 17544 0
[pid=11666] vsize: 70756
Current children cumulated CPU time (s) 1188.91
Current children cumulated vsize (Kb) 72880

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16882 0 0 0 119774 116 0 0 25 0 1 0 1843295464 72663040 16421 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17740 16421 145 145 0 17595 0
[pid=11666] vsize: 70960
Current children cumulated CPU time (s) 1198.91
Current children cumulated vsize (Kb) 73084

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16942 0 0 0 120772 117 0 0 25 0 1 0 1843295464 72904704 16481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17799 16481 145 145 0 17654 0
[pid=11666] vsize: 71196
Current children cumulated CPU time (s) 1208.9
Current children cumulated vsize (Kb) 73320



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 11666
Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/11662/statm): 531 226 485 147 0 384 0
[pid=11662] vsize: 2124
Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16942 0 0 0 120772 117 0 0 25 0 1 0 1843295464 72904704 16481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11666/statm): 17799 16481 145 145 0 17654 0
[pid=11666] vsize: 71196
Current children cumulated CPU time (s) 1208.9
Current children cumulated vsize (Kb) 73320

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.94
CPU user time (s): 1207.73
CPU system time (s): 1.20782
CPU usage (%): 99.901
Max. virtual memory (cumulated for all children) (Kb): 73320

Verifier Data

ERROR: no interpretation found !